Std.Float

REG-003 (PRD 08 N8): the uniform [0,1) contract. stdF32UnitFromWord32 w is EXACTLY (w >> 8) x 2^-24 — the 24-bit grid, so the largest input 0xFFFFFFFF gives (2^24 - 1) x 2^-24 = 1 - 2^-24 = 0x3f7fffff, never 1.0, and 0 gives +0.0. Bit assembly over U32 (no float arithmetic): m = w >> 8; if m = 0 the value is +0.0; otherwise the leading bit of m is found by shifting left until bit 23 is set (k shifts, 0..23), the exponent field is 126 - k (= 127 + (23 - k) - 24) and the fraction field is the shifted m without its leading bit. Verified on the native lane (debug/std-word-native-check.py, f32 rows) against an independent oracle: the evaluator lane runs the word shifts through unary bytes and is not a routine law here.

586def stdF32UnitLeadingBit =
587  (constructor ModelWord32 ModelWord32Value (byte 0) (byte 0) (byte 128) (byte 0))