Are you sure? The TweetNaCl paper says u32 is an unsigned >= 32-bit (see towards the end): http://tweetnacl.cr.yp.to/papers.html