Correctness of width-generic finite arithmetic

The executable arbitrary-precision kernels live in Kernel.Runtime. This module proves that the compact field-scale implementations agree with the exact dyadic specifications and installs the verified compiler substitutions.

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

Negating a conventional IEEE value flips only the decoded sign.

@[simp]

theorem FloatLib.Floats.Formats.BinaryInterchange.Model.FiniteKernel.Components.toDyadic_negative (fmt : FloatFormat) (value : Components) : (toDyadic fmt value).negative = value.sign

The dyadic of a component triple carries the component sign.

@[simp]

theorem FloatLib.Floats.Formats.BinaryInterchange.Model.FiniteKernel.Components.toDyadic_mant (fmt : FloatFormat) (value : Components) : (toDyadic fmt value).significand = value.mantissa

The dyadic of a component triple has the component mantissa as significand.

theorem FloatLib.Floats.Formats.BinaryInterchange.Model.FiniteKernel.Components.toDyadic_exp_of_mantissa_ne_zero (fmt : FloatFormat) (value : Components) (h : value.mantissa ≠ 0) : (toDyadic fmt value).exponent = dyadicExponent fmt value.exponent

For a nonzero mantissa, the dyadic exponent is the descriptor-adjusted component exponent.

theorem FloatLib.Floats.Formats.BinaryInterchange.Model.FiniteKernel.withFinite_eq {fmt : FloatFormat} {α : Type} (x : Model fmt) (k : Bool → ℕ → ℕ → Option α) : withFinite? x k = (decode? x).bind fun (value : Components) => k value.sign value.exponent value.mantissa

Scalar finite decoding is extensionally equal to binding the component decoder.

theorem FloatLib.Floats.Formats.BinaryInterchange.Model.FiniteKernel.exponent_eq_scale (fmt : FloatFormat) (encoded : ℕ) : dyadicExponent fmt encoded = Int.ofNat (scale encoded) - Int.ofNat (finiteScaleOffset fmt)

The unsigned finite scale denotes the same signed exponent as the public decoder.

theorem FloatLib.Floats.Formats.BinaryInterchange.Model.FiniteKernel.addComponents_sameSign_sameExponent (fmt : FloatFormat) (hfmt : fmt.isIEEE = true) (sign : Bool) (left right exponent : ℕ) (hleft : left ≠ 0) (hright : right ≠ 0) : addComponents fmt { sign := sign, exponent := exponent, mantissa := left } { sign := sign, exponent := exponent, mantissa := right } = FiniteProductRound.round fmt sign (left + right) (scale exponent + finiteScaleOffset fmt)

Adding nonzero components with the same sign and exponent reduces to one product-round call.

The scale is derived entirely from the format descriptor, so fixed-width backends do not need their own binary32, binary64, or binary128 versions of this argument.

theorem FloatLib.Floats.Formats.BinaryInterchange.Model.FiniteKernel.toDyadic_eq_decode {fmt : FloatFormat} (x : Model fmt) : x.toDyadic? = Option.map (Components.toDyadic fmt) (decode? x)

Compact decoding produces exactly the same finite dyadic as toDyadic?.

theorem FloatLib.Floats.Formats.BinaryInterchange.Model.FiniteKernel.addComponents_comm (fmt : FloatFormat) (x y : Components) : addComponents fmt x y = addComponents fmt y x

Finite component addition is commutative for every format descriptor.

theorem FloatLib.Floats.Formats.BinaryInterchange.Model.FiniteKernel.addComponentsImpl_eq (fmt : FloatFormat) (x y : Components) : addComponentsImpl fmt x y = addComponents fmt x y

Unsigned-scale finite addition is extensionally equal to the public component operation.

@[csimp]

theorem FloatLib.Floats.Formats.BinaryInterchange.Model.FiniteKernel.addComponents_eq_addComponentsImpl : addComponents = addComponentsImpl

Compile finite addition through unsigned scale alignment on conventional IEEE formats.

theorem FloatLib.Floats.Formats.BinaryInterchange.Model.FiniteKernel.add_eq_spec {fmt : FloatFormat} (x y : Model fmt) : add? x y = match x.toDyadic?, y.toDyadic? with | some dx, some dy => some (roundDyadic fmt (addDyadic dx dy)) | x, x_1 => none

Compact finite addition equals the public exact-dyadic finite path.

theorem FloatLib.Floats.Formats.BinaryInterchange.Model.FiniteKernel.mul_eq_spec {fmt : FloatFormat} (x y : Model fmt) : mul? x y = match x.toDyadic?, y.toDyadic? with | some dx, some dy => have sign := dx.negative ^^ dy.negative; if (dx.significand == 0 || dy.significand == 0) = true then some (zero fmt sign) else some (roundDyadic fmt { negative := sign, significand := dx.significand * dy.significand, exponent := dx.exponent + dy.exponent }) | x, x_1 => none

The compact finite multiplication kernel equals the public exact-dyadic finite path.

theorem FloatLib.Floats.Formats.BinaryInterchange.Model.FiniteKernel.div_eq_spec {fmt : FloatFormat} (x y : Model fmt) : div? x y = match x.toDyadic?, y.toDyadic? with | some dx, some dy => have sign := dx.negative ^^ dy.negative; if (dy.significand == 0) = true then some (if (dx.significand == 0) = true then invalidResult fmt else nativeOverflow fmt sign) else if (dx.significand == 0) = true then some (zero fmt sign) else some (roundRatScaled fmt sign dx.significand dy.significand (dx.exponent - dy.exponent)) | x, x_1 => none

The compact finite division kernel equals the public exact-dyadic finite path.

theorem FloatLib.Floats.Formats.BinaryInterchange.Model.FiniteKernel.fmaComponentsImpl_eq (fmt : FloatFormat) (x y z : Components) : fmaComponentsImpl fmt x y z = fmaComponents fmt x y z

Unsigned-scale FMA is extensionally equal to the public exact component operation.

theorem FloatLib.Floats.Formats.BinaryInterchange.Model.FiniteKernel.fmaComponents_sameSign_aligned (fmt : FloatFormat) (hfmt : fmt.isIEEE = true) (alignment : ℕ) (xSign ySign : Bool) (xExponent yExponent zExponent xMantissa yMantissa zMantissa : ℕ) (hxExponent : xExponent ≠ 0) (hyExponent : yExponent ≠ 0) (hzExponent : zExponent ≠ 0) (hxMantissa : xMantissa ≠ 0) (hyMantissa : yMantissa ≠ 0) (hzMantissa : zMantissa ≠ 0) (haligned : xExponent - 1 + (yExponent - 1) + alignment = zExponent - 1 + finiteScaleOffset fmt) : fmaComponents fmt { sign := xSign, exponent := xExponent, mantissa := xMantissa } { sign := ySign, exponent := yExponent, mantissa := yMantissa } { sign := xSign ^^ ySign, exponent := zExponent, mantissa := zMantissa } = FiniteProductRound.round fmt (xSign ^^ ySign) (xMantissa * yMantissa + zMantissa <<< alignment) (xExponent - 1 + (yExponent - 1))

An aligned same-sign FMA reduces to one product-round call for every IEEE binary format.

The caller supplies the significand alignment width. The exponent offset remains descriptor derived, so binary32, binary64, binary128, and custom IEEE descriptors share this proof.

@[csimp]

theorem FloatLib.Floats.Formats.BinaryInterchange.Model.FiniteKernel.fmaComponents_eq_fmaComponentsImpl : fmaComponents = fmaComponentsImpl

Compile finite FMA through the verified unsigned-scale implementation on IEEE formats.

theorem FloatLib.Floats.Formats.BinaryInterchange.Model.FiniteKernel.fma_eq_spec {fmt : FloatFormat} (x y z : Model fmt) : fma? x y z = match x.toDyadic?, y.toDyadic?, z.toDyadic? 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 (roundDyadic fmt (addDyadic product dz)) | x, x_1, x_2 => none

The compact finite FMA kernel equals the public exact-dyadic finite path.

theorem FloatLib.Floats.Formats.BinaryInterchange.Model.FiniteKernel.addFields_eq (fmt : FloatFormat) (xSign : Bool) (xExponent xMantissa : ℕ) (ySign : Bool) (yExponent yMantissa : ℕ) : addFields fmt xSign xExponent xMantissa ySign yExponent yMantissa = addComponents fmt { sign := xSign, exponent := xExponent, mantissa := xMantissa } { sign := ySign, exponent := yExponent, mantissa := yMantissa }

Scalar-field addition agrees with component addition.

theorem FloatLib.Floats.Formats.BinaryInterchange.Model.FiniteKernel.addRuntime_eq {fmt : FloatFormat} (x y : Model fmt) : addRuntime? x y = add? x y

The scalar-field addition entry point preserves add?.

@[csimp]

theorem FloatLib.Floats.Formats.BinaryInterchange.Model.FiniteKernel.add_eq_addRuntime : @add? = @addRuntime?

Compile finite addition through the scalar decoder.

theorem FloatLib.Floats.Formats.BinaryInterchange.Model.FiniteKernel.mulRuntime_eq {fmt : FloatFormat} (x y : Model fmt) : mulRuntime? x y = mul? x y

The scalar-field multiplication entry point preserves mul?.

@[csimp]

theorem FloatLib.Floats.Formats.BinaryInterchange.Model.FiniteKernel.mul_eq_mulRuntime : @mul? = @mulRuntime?

Compile finite multiplication through the scalar decoder.

theorem FloatLib.Floats.Formats.BinaryInterchange.Model.FiniteKernel.divRuntime_eq {fmt : FloatFormat} (x y : Model fmt) : divRuntime? x y = div? x y

The scalar-field division entry point preserves div?.

@[csimp]

theorem FloatLib.Floats.Formats.BinaryInterchange.Model.FiniteKernel.div_eq_divRuntime : @div? = @divRuntime?

Compile finite division through the scalar decoder.

theorem FloatLib.Floats.Formats.BinaryInterchange.Model.FiniteKernel.fmaFields_eq (fmt : FloatFormat) (xSign : Bool) (xExponent xMantissa : ℕ) (ySign : Bool) (yExponent yMantissa : ℕ) (zSign : Bool) (zExponent zMantissa : ℕ) : fmaFields fmt xSign xExponent xMantissa ySign yExponent yMantissa zSign zExponent zMantissa = fmaComponents fmt { sign := xSign, exponent := xExponent, mantissa := xMantissa } { sign := ySign, exponent := yExponent, mantissa := yMantissa } { sign := zSign, exponent := zExponent, mantissa := zMantissa }

Scalar-field FMA agrees with component FMA.

theorem FloatLib.Floats.Formats.BinaryInterchange.Model.FiniteKernel.fmaRuntime_eq {fmt : FloatFormat} (x y z : Model fmt) : fmaRuntime? x y z = fma? x y z

The scalar-field FMA entry point preserves fma?.

theorem FloatLib.Floats.Formats.BinaryInterchange.Model.FiniteKernel.fmaRuntimeFlat_eq {fmt : FloatFormat} (x y z : Model fmt) : fmaRuntimeFlat? x y z = fmaRuntime? x y z

The straight-line decoder agrees with the continuation decoder.

@[csimp]

theorem FloatLib.Floats.Formats.BinaryInterchange.Model.FiniteKernel.fma_eq_fmaRuntime : @fma? = @fmaRuntimeFlat?

Compile finite FMA through the scalar decoder.