The name is a little confusing. The way u32 is used in TweetNaCl, it doesn't have to be exactly 32 bits, only at least 32 bits.