Wide-limb storage runtime

The wide-limb backend serves binary descriptors wider than 128 bits. A stored value is a LimbArray of exactly limbCount fmt little-endian 32-bit limbs whose bits at and above fmt.bitWidth are clear; Value fmt packages the array with that invariant, decided by one limb comparison in topLimbFits. Because the invariant is a Boolean test, the smart constructor ofLimbs checks a candidate array at runtime. Core.Proof proves that model conversion and field packing produce arrays that pass this check.

Field access reads the sign bit, the exponent field, and the fraction limbs directly from the array. pack assembles a result from its sign, exponent word, and fraction limbs with two carry-free additions at the field offsets. The correspondence with Model is proved in Core.Proof; every arithmetic kernel of this backend is written over these accessors.

def FloatLib.Floats.Formats.BinaryInterchange.Model.WideLimb.Eligible (fmt : FloatFormat) : Prop

Structural capability required by the wide-limb kernels.

The conventional IEEE encoding selects the exact binary semantics and default bias shared with the generic kernels. Widths above 128 bits are the formats no fixed-limb kernel serves. An exponent field of at most 32 bits lets the encoded exponent be read from one 32-bit window. Scale and position arithmetic uses Nat; the fraction width is unrestricted.

@[instance_reducible, inline]

instance FloatLib.Floats.Formats.BinaryInterchange.Model.WideLimb.instDecidableEligible (fmt : FloatFormat) : Decidable (Eligible fmt)

Eligibility is decided by an explicit conditional on descriptor fields, exposing those tests to specialization. See Dispatch.Add.Runtime for the shared dispatch convention.

@[inline]

def FloatLib.Floats.Formats.BinaryInterchange.Model.WideLimb.limbCount (fmt : FloatFormat) : ℕ

Number of 32-bit limbs holding one encoded value.

@[inline]

def FloatLib.Floats.Formats.BinaryInterchange.Model.WideLimb.topLimbFits (fmt : FloatFormat) (v : Numerics.LimbArray) : Bool

Whether the bits at and above bitWidth in the top limb are clear.

@[reducible, inline]

abbrev FloatLib.Floats.Formats.BinaryInterchange.Model.WideLimb.Value (fmt : FloatFormat) : Type

A value of fmt stored as exactly limbCount fmt limbs with clear spare bits.

The invariant is a decidable Boolean test so kernels can construct values through ofLimbs. topLimbFits_iff gives the numerical bound for arrays of the required size.

theorem FloatLib.Floats.Formats.BinaryInterchange.Model.WideLimb.zero_valid (fmt : FloatFormat) : (Numerics.LimbArray.zero (limbCount fmt)).size = limbCount fmt ∧ topLimbFits fmt (Numerics.LimbArray.zero (limbCount fmt)) = true

The all-zero array satisfies the storage invariant.

@[instance_reducible]

instance FloatLib.Floats.Formats.BinaryInterchange.Model.WideLimb.instInhabitedValue (fmt : FloatFormat) : Inhabited (Value fmt)

@[inline]

def FloatLib.Floats.Formats.BinaryInterchange.Model.WideLimb.ofLimbs (fmt : FloatFormat) (w : Numerics.LimbArray) : Value fmt

Wrap a kernel output as a stored value.

An array with the required size and clear spare bits is retained; any other array yields zero. ofLimbs_val proves the successful case from an explicit size equality and numerical bound.

@[inline]

def FloatLib.Floats.Formats.BinaryInterchange.Model.WideLimb.toModel {fmt : FloatFormat} (v : Value fmt) : Model fmt

Interpret a stored value in the exact-width proof model.

@[inline]

def FloatLib.Floats.Formats.BinaryInterchange.Model.WideLimb.ofModel {fmt : FloatFormat} (x : Model fmt) : Value fmt

Store a proof-model value as limbs.

Field access

@[inline]

def FloatLib.Floats.Formats.BinaryInterchange.Model.WideLimb.signBit {fmt : FloatFormat} (v : Value fmt) : Bool

The stored sign bit.

@[inline]

def FloatLib.Floats.Formats.BinaryInterchange.Model.WideLimb.expMask32 (fmt : FloatFormat) : UInt32

Mask of the exponent field within a 32-bit window, for exponent widths of at most 32.

@[inline]

def FloatLib.Floats.Formats.BinaryInterchange.Model.WideLimb.expWord {fmt : FloatFormat} (v : Value fmt) : UInt32

The biased exponent field as a machine word.

@[inline]

def FloatLib.Floats.Formats.BinaryInterchange.Model.WideLimb.expField {fmt : FloatFormat} (v : Value fmt) : ℕ

The biased exponent field.

@[inline]

def FloatLib.Floats.Formats.BinaryInterchange.Model.WideLimb.expAllOnes (fmt : FloatFormat) : UInt32

The all-ones exponent field as a machine word.

@[inline]

def FloatLib.Floats.Formats.BinaryInterchange.Model.WideLimb.fraction {fmt : FloatFormat} (v : Value fmt) : Numerics.LimbArray

The fraction field, in the stored limb count.

@[inline]

def FloatLib.Floats.Formats.BinaryInterchange.Model.WideLimb.normalMantissa {fmt : FloatFormat} (v : Value fmt) : Numerics.LimbArray

The significand of a normal value: the fraction with the implicit bit 2^fracWidth.

def FloatLib.Floats.Formats.BinaryInterchange.Model.WideLimb.pack (fmt : FloatFormat) (sign : Bool) (exponent : UInt32) (fraction : Numerics.LimbArray) : Value fmt

Pack a sign, an exponent word, and fraction limbs into a stored value.

The exponent word is masked to the exponent field and the fraction to fracWidth bits, so the result is meaningful for every input; Core.Proof.toModel_pack states the exact model produced.