Correctness of finite binary32 components

The representation lemmas here establish field bounds and connect runtime mantissa-and-scale coordinates to the generic exact-dyadic decoder. Binary32 word proofs for addition, multiplication, division, square root, and fused operations all reuse this boundary.

Runtime clients can import Finite.Runtime without these proofs. The operation proofs reuse the same field bounds and mantissa-scale decoding theorem.

theorem FloatLib.Floats.Formats.BinaryInterchange.Model.NativeBinary32.fracField_lt (x : Value) : (fracField (toUInt32 x)).toNat < 2 ^ 23

A decoded binary32 fraction fits in its 23-bit field.

theorem FloatLib.Floats.Formats.BinaryInterchange.Model.NativeBinary32.expField_lt (x : Value) : (expField (toUInt32 x)).toNat < 2 ^ 8

A decoded binary32 exponent fits in its eight-bit field.

theorem FloatLib.Floats.Formats.BinaryInterchange.Model.NativeBinary32.finiteMantissa_toNat (exponent fraction : UInt32) (hfraction : fraction.toNat < 2 ^ 23) : (finiteMantissa exponent fraction).toNat = if exponent = 0 then fraction.toNat else pow2 23 + fraction.toNat

Interpret the native finite mantissa as an ordinary natural number.

theorem FloatLib.Floats.Formats.BinaryInterchange.Model.NativeBinary32.finiteMantissa_lt (exponent fraction : UInt32) (hfraction : fraction.toNat < 2 ^ 23) : (finiteMantissa exponent fraction).toNat < 2 ^ 24

Every finite binary32 mantissa fits in 24 bits.

theorem FloatLib.Floats.Formats.BinaryInterchange.Model.NativeBinary32.finiteScale_toNat (exponent : UInt32) : (finiteScale exponent).toNat = if exponent = 0 then 0 else exponent.toNat - 1

Interpret the native finite scale as an ordinary natural number.

theorem FloatLib.Floats.Formats.BinaryInterchange.Model.NativeBinary32.finiteScale_le (exponent : UInt32) (hexponent : exponent.toNat < 2 ^ 8) (hfinite : exponent ≠ 255) : (finiteScale exponent).toNat ≤ 253

Every finite binary32 scale is at most 253.

theorem FloatLib.Floats.Formats.BinaryInterchange.Model.NativeBinary32.finiteMantissa_lt_of_value (x : Value) : (finiteMantissa (expField (toUInt32 x)) (fracField (toUInt32 x))).toNat < 2 ^ 24

The mantissa decoded directly from a binary32 value fits in the 24 bits used by the native finite-operation kernels.

Operation proofs should normally use this value-level lemma. The component-level finiteMantissa_lt theorem remains available when a proof constructs fields independently.

theorem FloatLib.Floats.Formats.BinaryInterchange.Model.NativeBinary32.finiteScale_le_of_value (x : Value) (hfinite : expField (toUInt32 x) ≠ 255) : (finiteScale (expField (toUInt32 x))).toNat ≤ 253

The scale decoded from a finite binary32 value is at most 253.

This is the value-level counterpart of finiteScale_le; it keeps field-width bookkeeping out of the individual arithmetic proofs.

theorem FloatLib.Floats.Formats.BinaryInterchange.Model.NativeBinary32.finiteMantissa_lt_of_components (x : Value) {exponent fraction : UInt32} {mantissa : UInt64} (hexponent : exponent = expField (toUInt32 x)) (hfraction : fraction = fracField (toUInt32 x)) (hmantissa : mantissa = finiteMantissa exponent fraction) : mantissa.toNat < 2 ^ 24

The 24-bit mantissa bound also holds for components identified with a value's decoded fields.

theorem FloatLib.Floats.Formats.BinaryInterchange.Model.NativeBinary32.finiteScale_le_of_components (x : Value) {exponent : UInt32} {scale : UInt64} (hexponent : exponent = expField (toUInt32 x)) (hscale : scale = finiteScale exponent) (hfinite : exponent ≠ 255) : scale.toNat ≤ 253

Transport the value-level finite-scale bound to the local component names used by a word kernel.

theorem FloatLib.Floats.Formats.BinaryInterchange.Model.NativeBinary32.toDyadic_eq_finiteComponents (x : Value) : toDyadic? (toUInt32 x) = have bits := toUInt32 x; have exponent := expField bits; have fraction := fracField bits; if exponent = 255 then none else have sign := signBit bits; have mantissa := finiteMantissa exponent fraction; have scale := finiteScale exponent; if mantissa = 0 then some { negative := sign, significand := 0, exponent := 0 } else some { negative := sign, significand := mantissa.toNat, exponent := Int.ofNat scale.toNat - 149 }

Native finite components decode to the same exact dyadic as the generic binary32 decoder.