Verified wide-limb normal rounding

The proof proceeds through a natural-number specification roundJammed, which restates the normal branch of FiniteProductRound.round for a significand whose jam low bits have been jammed into one sticky bit. Two theorems connect it to its neighbours.

• roundNormal?_map_toModel: the limb kernel computes roundJammed on the value of its nonzero significand, assuming the exponent field fits in 32 bits.
• round_eq_of_roundJammed: an accepted roundJammed result on the jammed value is the exact rounder FiniteProductRound.round on the exact value, by roundShiftRightEven_shiftRightJam.

Together they let each arithmetic kernel prove toModel result = FiniteProductRound.round ... and then reuse the generic kernel's own refinement theorems.

The natural-number specification

def FloatLib.Floats.Formats.BinaryInterchange.Model.WideLimb.roundJammed (fmt : FloatFormat) (sign : Bool) (significand jam scale : ℕ) : Option (Model fmt)

The normal branch of FiniteProductRound.round for a jammed significand.

For a sufficiently large exact value, significand = shiftRightJam exact jam has its leading bit jam positions below that of exact. round_eq_of_roundJammed states the required bound; roundNormal?_map_toModel relates this specification to the limb kernel on nonzero inputs.

Bounds on the rounded significand

theorem FloatLib.Floats.Formats.BinaryInterchange.Model.WideLimb.rounded_bounds {fmt : FloatFormat} (S : ℕ) (hS : S ≠ 0) : have rounded := if fmt.fracWidth ≤ S.log2 then Numerics.roundShiftRightEven S (S.log2 - fmt.fracWidth) else S * 2 ^ (fmt.fracWidth - S.log2); 2 ^ fmt.fracWidth ≤ rounded ∧ rounded ≤ 2 ^ (fmt.fracWidth + 1)

Rounding a nonzero value to fracWidth + 1 bits lands in [2^fracWidth, 2^(fracWidth + 1)].

theorem FloatLib.Floats.Formats.BinaryInterchange.Model.WideLimb.log2_eq_succ_iff (rounded f : ℕ) (hlow : 2 ^ f ≤ rounded) (hhigh : rounded ≤ 2 ^ (f + 1)) : rounded.log2 = f + 1 ↔ rounded = 2 ^ (f + 1)

A value in [2^f, 2^(f + 1)] equals 2^(f + 1) exactly when its leading bit is at f + 1.

The limb kernel computes the specification

theorem FloatLib.Floats.Formats.BinaryInterchange.Model.WideLimb.roundNormal?_map_toModel {fmt : FloatFormat} (hexp : fmt.expWidth ≤ 32) (sign : Bool) (S : Numerics.LimbArray) (jam scale : ℕ) (hS : S.toNat ≠ 0) : Option.map toModel (roundNormal? fmt sign S jam scale) = roundJammed fmt sign S.toNat jam scale

An accepted limb rounding is the natural-number specification on the significand's value.

The specification refines the exact rounder

theorem FloatLib.Floats.Formats.BinaryInterchange.Model.WideLimb.shiftRightJam_zero (T : ℕ) : Numerics.shiftRightJam T 0 = T

shiftRightJam by zero bits is the identity.

theorem FloatLib.Floats.Formats.BinaryInterchange.Model.WideLimb.round_eq_of_roundJammed {fmt : FloatFormat} (sign : Bool) (exact jam scale : ℕ) (hexact : exact ≠ 0) (hjam : jam = 0 ∨ 2 ^ (fmt.fracWidth + jam + 2) ≤ exact) (result : Model fmt) (hresult : roundJammed fmt sign (Numerics.shiftRightJam exact jam) jam scale = some result) : FiniteProductRound.round fmt sign exact scale = result

An accepted roundJammed result on shiftRightJam exact jam is the exact rounder on exact.

The hypothesis 2 ^ (fracWidth + jam + 2) ≤ exact (vacuous for jam = 0) is what roundShiftRightEven_shiftRightJam needs: at least the guard bit and one more bit of the rounded quotient lie above the jammed position.