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 equals binding the component decoder decode?.

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 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.Internal.addComponents_eq (fmt : FloatFormat) (x y : Components) : addComponents fmt x y = FiniteKernel.addComponents fmt x y

Unsigned-scale finite addition equals the public component operation addComponents.

@[csimp]

theorem FloatLib.Floats.Formats.BinaryInterchange.Model.FiniteKernel.addComponents_eq_internal : addComponents = Internal.addComponents

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

Compact finite multiplication 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

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

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

Unsigned-scale FMA equals the public component operation fmaComponents.

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. As in addComponents_sameSign_sameExponent, the exponent offset comes from the descriptor.

@[csimp]

theorem FloatLib.Floats.Formats.BinaryInterchange.Model.FiniteKernel.fmaComponents_eq_internal : fmaComponents = Internal.fmaComponents

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

Compact finite FMA 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

Scalar-field addition addRuntime? agrees with 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

Scalar-field multiplication mulRuntime? agrees with 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

Scalar-field division divRuntime? agrees with 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

Scalar-field FMA fmaRuntime? agrees with 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 fmaRuntimeFlat? agrees with the continuation form fmaRuntime?.

@[csimp]

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

Compile finite FMA through the straight-line scalar decoder fmaRuntimeFlat?.