Agreement between native binary32 words and the generic model

The narrow-word core implements finite binary32 arithmetic with UInt32 and UInt64. This module proves that its finite operations equal the generic Model FloatFormat.binary32 formulas, using the field, decoding and rounding bridge of Narrow.ModelBridge.

The Addition, Multiplication and Fma proof modules connect their word kernels to these finite operations. Runtime clients can import the Runtime modules without these proofs.

theorem FloatLib.Floats.Formats.BinaryInterchange.Model.NativeBinary32.addFinite_eq (x y : Value) : addFinite? x y = match Model.toDyadic? x, Model.toDyadic? y with | some dx, some dy => some (Model.roundDyadic FloatFormat.binary32 (addDyadic dx dy)) | x, x_1 => none

Native finite binary32 addition rounds the generic exact dyadic sum.

theorem FloatLib.Floats.Formats.BinaryInterchange.Model.NativeBinary32.mulFinite_eq (x y : Value) : mulFinite? x y = match Model.toDyadic? x, Model.toDyadic? y with | some dx, some dy => have sign := dx.negative ^^ dy.negative; if (dx.significand == 0 || dy.significand == 0) = true then some (if sign = true then negZero FloatFormat.binary32 else posZero FloatFormat.binary32) else some (Model.roundDyadic FloatFormat.binary32 { negative := sign, significand := dx.significand * dy.significand, exponent := dx.exponent + dy.exponent }) | x, x_1 => none

Native finite binary32 multiplication equals the generic product, zero factors included.

theorem FloatLib.Floats.Formats.BinaryInterchange.Model.NativeBinary32.divFinite_eq (x y : Value) : divFinite? x y = match Model.toDyadic? x, Model.toDyadic? y with | some dx, some dy => have sign := dx.negative ^^ dy.negative; some (if (dy.significand == 0) = true then if (dx.significand == 0) = true then canonicalNaN FloatFormat.binary32 else if sign = true then negInf FloatFormat.binary32 else posInf FloatFormat.binary32 else if (dx.significand == 0) = true then if sign = true then negZero FloatFormat.binary32 else posZero FloatFormat.binary32 else Model.roundRatScaled FloatFormat.binary32 sign dx.significand dy.significand (dx.exponent - dy.exponent)) | x, x_1 => none

Native finite binary32 division equals the generic finite quotient, zero divisors included.

theorem FloatLib.Floats.Formats.BinaryInterchange.Model.NativeBinary32.fmaFinite_eq (x y z : Value) : fmaFinite? x y z = match Model.toDyadic? x, Model.toDyadic? y, Model.toDyadic? z with | some dx, some dy, some dz => have product := { negative := dx.negative ^^ dy.negative, significand := dx.significand * dy.significand, exponent := dx.exponent + dy.exponent }; some (Model.roundDyadic FloatFormat.binary32 (addDyadic product dz)) | x, x_1, x_2 => none

Native finite binary32 fused multiply-add rounds the exact product plus addend once.