/* 7.3.3: unsigned both-endian (little, then big) 32-bit value */