From the compact finite kernels to the reference operations

The wide-limb kernels prove that an accepted result is the compact finite kernel (FiniteKernel.add?, mul?, or fma?) on the operand models. This module supplies the last step of each refinement: whenever a compact finite kernel accepts its operands, the reference operation Model.Spec.add, mul, or fma returns the same value (spec_add_of_add?_eq_some and its siblings). It also records that negating a model value flips only the decoded sign (decode?_neg) and that the unsigned-scale sum is commutative (roundSum_comm), which the alignment kernel uses to order its operands by scale.

theorem FloatLib.Floats.Formats.BinaryInterchange.Model.WideLimb.spec_add_of_add?_eq_some {fmt : FloatFormat} (x y r : Model fmt) (h : FiniteKernel.add? x y = some r) : Spec.add x y = r

An accepted compact finite addition is the reference addition.

theorem FloatLib.Floats.Formats.BinaryInterchange.Model.WideLimb.spec_mul_of_mul?_eq_some {fmt : FloatFormat} (x y r : Model fmt) (h : FiniteKernel.mul? x y = some r) : Spec.mul x y = r

An accepted compact finite multiplication is the reference multiplication.

theorem FloatLib.Floats.Formats.BinaryInterchange.Model.WideLimb.spec_fma_of_fma?_eq_some {fmt : FloatFormat} (x y z r : Model fmt) (h : FiniteKernel.fma? x y z = some r) : Spec.fma x y z = r

An accepted compact finite fused multiply-add is the reference fused multiply-add.

theorem FloatLib.Floats.Formats.BinaryInterchange.Model.WideLimb.decode?_neg {fmt : FloatFormat} (hieee : fmt.isIEEE = true) (m : Model fmt) : FiniteKernel.decode? m.neg = Option.map (fun (c : FiniteKernel.Components) => { sign := !c.sign, exponent := c.exponent, mantissa := c.mantissa }) (FiniteKernel.decode? m)

Negating a conventional IEEE value flips only the decoded sign.

theorem FloatLib.Floats.Formats.BinaryInterchange.Model.WideLimb.roundSum_comm {fmt : FloatFormat} (hieee : fmt.isIEEE = true) (roundOffset : ℕ) (aSign bSign : Bool) (a sa b sb : ℕ) : FiniteScaleAdd.roundSum fmt roundOffset aSign bSign a sa b sb = FiniteScaleAdd.roundSum fmt roundOffset bSign aSign b sb a sa

The unsigned-scale exact sum does not depend on the order of its operands.