Executable width-generic finite arithmetic

Arbitrary-precision kernels decode finite fields into a compact unsigned-scale representation. Compiled arithmetic uses their allocation-reduced entry points for addition, multiplication, division, and fused multiply-add. Refinement theorems live in Kernel.Proof.

structure FloatLib.Floats.Formats.BinaryInterchange.Model.FiniteKernel.Components : Type

Decoded finite fields before conversion to a signed dyadic exponent.

For a nonzero value, the magnitude is mantissa * 2^(scale exponent - finiteScaleOffset fmt), with the subtraction interpreted in Int. The separate sign field determines its sign.

• sign : Bool

  Sign bit of the encoded value.

• exponent : ℕ

  Biased exponent field; zero also identifies zeros and subnormals.

• mantissa : ℕ

  Integer significand, including the implicit bit for a normal value.

def FloatLib.Floats.Formats.BinaryInterchange.Model.FiniteKernel.instReprComponents.repr : Components → ℕ → Std.Format

@[instance_reducible]

instance FloatLib.Floats.Formats.BinaryInterchange.Model.FiniteKernel.instReprComponents : Repr Components

@[instance_reducible]

instance FloatLib.Floats.Formats.BinaryInterchange.Model.FiniteKernel.instDecidableEqComponents : DecidableEq Components

def FloatLib.Floats.Formats.BinaryInterchange.Model.FiniteKernel.instDecidableEqComponents.decEq (x✝ x✝¹ : Components) : Decidable (x✝ = x✝¹)

@[inline]

def FloatLib.Floats.Formats.BinaryInterchange.Model.FiniteKernel.scale (exponent : ℕ) : ℕ

Nonnegative scale associated with a finite exponent field.

@[inline]

def FloatLib.Floats.Formats.BinaryInterchange.Model.FiniteKernel.finiteScaleOffset (fmt : FloatFormat) : ℕ

Common nonnegative offset used by the compact finite-field scale.

@[inline]

def FloatLib.Floats.Formats.BinaryInterchange.Model.FiniteKernel.dyadicExponent (fmt : FloatFormat) (encoded : ℕ) : ℤ

Signed dyadic exponent associated with a finite exponent field, including subnormals.

@[inline]

def FloatLib.Floats.Formats.BinaryInterchange.Model.FiniteKernel.decodeMantissa (fmt : FloatFormat) (exponent fraction : ℕ) : ℕ

Decode the integer significand from finite exponent and fraction fields.

Subnormal values use the stored fraction directly. Normal values restore the implicit leading bit. The formula is width-generic and shared by every natural-number finite decoder.

@[inline]

def FloatLib.Floats.Formats.BinaryInterchange.Model.FiniteKernel.Components.toDyadic (fmt : FloatFormat) (value : Components) : Numerics.Dyadic

Convert compact finite components to the exact dyadic representation used by proofs.

@[inline]

def FloatLib.Floats.Formats.BinaryInterchange.Model.FiniteKernel.decode? {fmt : FloatFormat} (x : Model fmt) : Option Components

Decode the sign, exponent, and significand of a finite value.

none means the complete format descriptor classifies the input as non-finite. No precision-specific constant occurs here.

@[inline]

def FloatLib.Floats.Formats.BinaryInterchange.Model.FiniteKernel.withFinite? {fmt : FloatFormat} {α : Type} (x : Model fmt) (k : Bool → ℕ → ℕ → Option α) : Option α

Run k on scalar fields when x is finite.

The IEEE branch converts the storage word to Nat once and does not allocate an intermediate Components value. Other encodings retain the descriptor-aware decoder.

@[inline]

def FloatLib.Floats.Formats.BinaryInterchange.Model.FiniteKernel.addComponentsImpl (fmt : FloatFormat) (x y : Components) : Model fmt

Compiled finite addition aligns unsigned field scales before entering the rounder.

For non-IEEE descriptors it evaluates the same exact-dyadic definition used in the logic.

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

Add two already-decoded finite values and round once to fmt.

The exact dyadic sum is rounded by the descriptor-generic integer implementation. Importing Kernel.Proof also enables the verified compiler substitution to addComponentsImpl, which uses unsigned scale alignment on IEEE descriptors.

@[inline]

def FloatLib.Floats.Formats.BinaryInterchange.Model.FiniteKernel.add? {fmt : FloatFormat} (x y : Model fmt) : Option (Model fmt)

Finite addition through the compact decoder.

The component operation is kept separate so fixed-width storage backends can reuse the same exact dyadic addition and rounding policy after a cheaper field decode.

@[inline]

def FloatLib.Floats.Formats.BinaryInterchange.Model.FiniteKernel.mul? {fmt : FloatFormat} (x y : Model fmt) : Option (Model fmt)

Finite multiplication using compact field scales.

The exact significand product remains a Nat, preserving arbitrary precision. Only the two operand decodes and exponent algebra are fused; final rounding still uses the generic rounder.

@[inline]

def FloatLib.Floats.Formats.BinaryInterchange.Model.FiniteKernel.divComponents (fmt : FloatFormat) (x y : Components) : Model fmt

Finite division using compact field scales.

The format-dependent exponent offset cancels between numerator and denominator. The quotient still uses the exact arbitrary-precision rational rounder; only decoding and exponent construction are fused.

@[inline]

def FloatLib.Floats.Formats.BinaryInterchange.Model.FiniteKernel.div? {fmt : FloatFormat} (x y : Model fmt) : Option (Model fmt)

Decode finite operands once, then apply divComponents.

@[inline]

def FloatLib.Floats.Formats.BinaryInterchange.Model.FiniteKernel.productDyadic (fmt : FloatFormat) (x y : Components) : Numerics.Dyadic

Exact product used by the finite fused-multiply-add kernel.

The exponent is expressed with nonnegative field scales. When either significand is zero this exponent is observationally irrelevant: addDyadic identifies a zero from its mantissa and applies the same signed-zero rule as the public dyadic path.

@[inline]

def FloatLib.Floats.Formats.BinaryInterchange.Model.FiniteKernel.fmaComponentsImpl (fmt : FloatFormat) (x y z : Components) : Model fmt

Compiled finite FMA adds the exact product and addend in one unsigned scale coordinate.

The addend scale receives one format offset so both operands use the product rounder's two-offset coordinate. No intermediate dyadic exponent is allocated on the IEEE fast path.

def FloatLib.Floats.Formats.BinaryInterchange.Model.FiniteKernel.fmaComponents (fmt : FloatFormat) (x y z : Components) : Model fmt

Exact finite fused multiply-add from three already-decoded values.

The exact dyadic result is rounded once by the descriptor-generic integer implementation. Importing Kernel.Proof also enables the verified compiler substitution to fmaComponentsImpl, which uses unsigned scale alignment on IEEE descriptors.

@[inline]

def FloatLib.Floats.Formats.BinaryInterchange.Model.FiniteKernel.fma? {fmt : FloatFormat} (x y z : Model fmt) : Option (Model fmt)

Finite fused multiply-add using compact field scales for the exact product.

All three inputs are decoded once. The product and addend remain exact dyadics and the result is rounded only once, so this is still a true fused operation at every supported precision.

Scalar-field compiled entry points

@[inline]

def FloatLib.Floats.Formats.BinaryInterchange.Model.FiniteKernel.addFields (fmt : FloatFormat) (xSign : Bool) (xExponent xMantissa : ℕ) (ySign : Bool) (yExponent yMantissa : ℕ) : Model fmt

Add finite scalar fields without materializing decoded component records on IEEE formats.

@[inline]

def FloatLib.Floats.Formats.BinaryInterchange.Model.FiniteKernel.addRuntime? {fmt : FloatFormat} (x y : Model fmt) : Option (Model fmt)

Compiled finite addition with scalar field decoding.

@[inline]

def FloatLib.Floats.Formats.BinaryInterchange.Model.FiniteKernel.mulFields (fmt : FloatFormat) (xSign : Bool) (xExponent xMantissa : ℕ) (ySign : Bool) (yExponent yMantissa : ℕ) : Model fmt

Multiply finite scalar fields using the compact product scale.

@[inline]

def FloatLib.Floats.Formats.BinaryInterchange.Model.FiniteKernel.mulRuntime? {fmt : FloatFormat} (x y : Model fmt) : Option (Model fmt)

Compiled finite multiplication with scalar field decoding.

@[inline]

def FloatLib.Floats.Formats.BinaryInterchange.Model.FiniteKernel.divFields (fmt : FloatFormat) (xSign : Bool) (xExponent xMantissa : ℕ) (ySign : Bool) (yExponent yMantissa : ℕ) : Model fmt

Divide finite scalar fields using the compact exponent difference.

@[inline]

def FloatLib.Floats.Formats.BinaryInterchange.Model.FiniteKernel.divRuntime? {fmt : FloatFormat} (x y : Model fmt) : Option (Model fmt)

Compiled finite division with scalar field decoding.

@[inline]

def FloatLib.Floats.Formats.BinaryInterchange.Model.FiniteKernel.fmaFields (fmt : FloatFormat) (xSign : Bool) (xExponent xMantissa : ℕ) (ySign : Bool) (yExponent yMantissa : ℕ) (zSign : Bool) (zExponent zMantissa : ℕ) : Model fmt

FMA on finite scalar fields without allocating decoded component records on IEEE formats.

@[inline]

def FloatLib.Floats.Formats.BinaryInterchange.Model.FiniteKernel.fmaRuntime? {fmt : FloatFormat} (x y z : Model fmt) : Option (Model fmt)

Compiled finite FMA with scalar field decoding.

@[inline]

def FloatLib.Floats.Formats.BinaryInterchange.Model.FiniteKernel.fmaRuntimeFlat? {fmt : FloatFormat} (x y z : Model fmt) : Option (Model fmt)

Straight-line IEEE FMA decoder.

This calls the same fmaFields kernel as fmaRuntime?, with the three decodes written directly instead of through nested continuations. fmaRuntimeFlat_eq proves their equality.