Representation interface for configured binary values

A configured binary format chooses its storage plan statically, but numerical programs should not need separate APIs for byte, word, fixed-limb, and wide carriers. This module exposes one storage-independent boundary for packing, exact decoding, classification, and special values.

toModel and ofModel convert through the logical Model without loss. The module does not register arithmetic backends, so representation and conversion code can use configured values without importing the operation planner or native-width dispatch instances.

@[inline]

def FloatLib.Floats.ExecFloat.Binary.toModel {format : Formats.BinaryInterchange.FloatFormat} {plan : Formats.BinaryInterchange.Configured.StoragePlan format} {code : Type} [ModelCodec plan (Formats.BinaryInterchange.Model format) code] (value : Binary format.expWidth format.fracWidth format.encoding format.exponentBias ⋯ ⋯ ⋯ ⋯ plan code) : Formats.BinaryInterchange.Model format

Decode the statically selected runtime carrier into the exact-width binary proof model.

This boundary does not expose whether the carrier is a byte, machine word, or wide model.

@[inline]

def FloatLib.Floats.ExecFloat.Binary.ofModel {format : Formats.BinaryInterchange.FloatFormat} {plan : Formats.BinaryInterchange.Configured.StoragePlan format} {code : Type} [ModelCodec plan (Formats.BinaryInterchange.Model format) code] (value : Formats.BinaryInterchange.Model format) : Binary format.expWidth format.fracWidth format.encoding format.exponentBias ⋯ ⋯ ⋯ ⋯ plan code

Pack an exact-width binary model into the statically selected runtime carrier.

@[inline]

def FloatLib.Floats.ExecFloat.Binary.ofNatBits {format : Formats.BinaryInterchange.FloatFormat} {plan : Formats.BinaryInterchange.Configured.StoragePlan format} {code : Type} [ModelCodec plan (Formats.BinaryInterchange.Model format) code] (bits : ℕ) : Binary format.expWidth format.fracWidth format.encoding format.exponentBias ⋯ ⋯ ⋯ ⋯ plan code

Construct a configured binary value from its complete unsigned interchange word.

Inputs outside the configured width are reduced modulo 2 ^ format.bitWidth, matching Model.ofNatBits.

@[inline]

def FloatLib.Floats.ExecFloat.Binary.toNatBits {format : Formats.BinaryInterchange.FloatFormat} {plan : Formats.BinaryInterchange.Configured.StoragePlan format} {code : Type} [ModelCodec plan (Formats.BinaryInterchange.Model format) code] (value : Binary format.expWidth format.fracWidth format.encoding format.exponentBias ⋯ ⋯ ⋯ ⋯ plan code) : ℕ

Read the complete configured binary interchange word as an unsigned natural number.

@[inline]

def FloatLib.Floats.ExecFloat.Binary.exactValue {format : Formats.BinaryInterchange.FloatFormat} {plan : Formats.BinaryInterchange.Configured.StoragePlan format} {code : Type} [ModelCodec plan (Formats.BinaryInterchange.Model format) code] (value : Binary format.expWidth format.fracWidth format.encoding format.exponentBias ⋯ ⋯ ⋯ ⋯ plan code) : Formats.BinaryInterchange.Model.ExactValue

Decode the complete mathematical value, retaining signed zero and NaN metadata.

@[inline]

def FloatLib.Floats.ExecFloat.Binary.decode {format : Formats.BinaryInterchange.FloatFormat} {plan : Formats.BinaryInterchange.Configured.StoragePlan format} {code : Type} [ModelCodec plan (Formats.BinaryInterchange.Model format) code] (value : Binary format.expWidth format.fracWidth format.encoding format.exponentBias ⋯ ⋯ ⋯ ⋯ plan code) : Numerics.NumericalValue Numerics.SignedRat

Decode into the exact signed-rational semantic domain used by binary conversion.

Finite values become exact rationals together with their sign bit, so a negative zero decodes to SignedRat.negZero rather than to 0. Infinities retain their sign, and a NaN carries its diagnostic payload without the quiet bit, together with its sign bit and signaling class. Use toRat? when only the rational value of a finite number matters.

@[inline]

def FloatLib.Floats.ExecFloat.Binary.toRat? {format : Formats.BinaryInterchange.FloatFormat} {plan : Formats.BinaryInterchange.Configured.StoragePlan format} {code : Type} [ModelCodec plan (Formats.BinaryInterchange.Model format) code] (value : Binary format.expWidth format.fracWidth format.encoding format.exponentBias ⋯ ⋯ ⋯ ⋯ plan code) : Option ℚ

Exact rational value of a finite configured binary number, or none for NaN and infinity.

@[inline]

def FloatLib.Floats.ExecFloat.Binary.signBit {format : Formats.BinaryInterchange.FloatFormat} {plan : Formats.BinaryInterchange.Configured.StoragePlan format} {code : Type} [ModelCodec plan (Formats.BinaryInterchange.Model format) code] (value : Binary format.expWidth format.fracWidth format.encoding format.exponentBias ⋯ ⋯ ⋯ ⋯ plan code) : Bool

Whether the stored sign bit is set.

@[inline]

def FloatLib.Floats.ExecFloat.Binary.isNaN {format : Formats.BinaryInterchange.FloatFormat} {plan : Formats.BinaryInterchange.Configured.StoragePlan format} {code : Type} [ModelCodec plan (Formats.BinaryInterchange.Model format) code] (value : Binary format.expWidth format.fracWidth format.encoding format.exponentBias ⋯ ⋯ ⋯ ⋯ plan code) : Bool

Whether the value is a NaN under its configured encoding policy.

@[inline]

def FloatLib.Floats.ExecFloat.Binary.isQuietNaN {format : Formats.BinaryInterchange.FloatFormat} {plan : Formats.BinaryInterchange.Configured.StoragePlan format} {code : Type} [ModelCodec plan (Formats.BinaryInterchange.Model format) code] (value : Binary format.expWidth format.fracWidth format.encoding format.exponentBias ⋯ ⋯ ⋯ ⋯ plan code) : Bool

Whether the value is a quiet NaN under its configured encoding policy.

@[inline]

def FloatLib.Floats.ExecFloat.Binary.isSignalingNaN {format : Formats.BinaryInterchange.FloatFormat} {plan : Formats.BinaryInterchange.Configured.StoragePlan format} {code : Type} [ModelCodec plan (Formats.BinaryInterchange.Model format) code] (value : Binary format.expWidth format.fracWidth format.encoding format.exponentBias ⋯ ⋯ ⋯ ⋯ plan code) : Bool

Whether the value is a signaling NaN under its configured encoding policy.

@[inline]

def FloatLib.Floats.ExecFloat.Binary.isInfinite {format : Formats.BinaryInterchange.FloatFormat} {plan : Formats.BinaryInterchange.Configured.StoragePlan format} {code : Type} [ModelCodec plan (Formats.BinaryInterchange.Model format) code] (value : Binary format.expWidth format.fracWidth format.encoding format.exponentBias ⋯ ⋯ ⋯ ⋯ plan code) : Bool

Whether the value is an infinity. Finite encodings always return false.

@[inline]

def FloatLib.Floats.ExecFloat.Binary.isFinite {format : Formats.BinaryInterchange.FloatFormat} {plan : Formats.BinaryInterchange.Configured.StoragePlan format} {code : Type} [ModelCodec plan (Formats.BinaryInterchange.Model format) code] (value : Binary format.expWidth format.fracWidth format.encoding format.exponentBias ⋯ ⋯ ⋯ ⋯ plan code) : Bool

Whether the value denotes a finite number under its configured encoding policy.

@[inline]

def FloatLib.Floats.ExecFloat.Binary.isZero {format : Formats.BinaryInterchange.FloatFormat} {plan : Formats.BinaryInterchange.Configured.StoragePlan format} {code : Type} [ModelCodec plan (Formats.BinaryInterchange.Model format) code] (value : Binary format.expWidth format.fracWidth format.encoding format.exponentBias ⋯ ⋯ ⋯ ⋯ plan code) : Bool

Whether the value is zero under its configured encoding policy.

@[inline]

def FloatLib.Floats.ExecFloat.Binary.isSubnormal {format : Formats.BinaryInterchange.FloatFormat} {plan : Formats.BinaryInterchange.Configured.StoragePlan format} {code : Type} [ModelCodec plan (Formats.BinaryInterchange.Model format) code] (value : Binary format.expWidth format.fracWidth format.encoding format.exponentBias ⋯ ⋯ ⋯ ⋯ plan code) : Bool

Whether the value is a finite subnormal.

@[inline]

def FloatLib.Floats.ExecFloat.Binary.zero {format : Formats.BinaryInterchange.FloatFormat} {plan : Formats.BinaryInterchange.Configured.StoragePlan format} {code : Type} [ModelCodec plan (Formats.BinaryInterchange.Model format) code] (sign : Bool := false) : Binary format.expWidth format.fracWidth format.encoding format.exponentBias ⋯ ⋯ ⋯ ⋯ plan code

Construct zero, positive by default. (sign := true) requests negative zero.

Encodings with one unsigned zero canonicalize a requested negative zero to positive zero.

@[inline]

def FloatLib.Floats.ExecFloat.Binary.infinity? {format : Formats.BinaryInterchange.FloatFormat} {plan : Formats.BinaryInterchange.Configured.StoragePlan format} {code : Type} [ModelCodec plan (Formats.BinaryInterchange.Model format) code] (sign : Bool := false) : Option (Binary format.expWidth format.fracWidth format.encoding format.exponentBias ⋯ ⋯ ⋯ ⋯ plan code)

Construct infinity, positive by default, when the configured encoding represents it.

IEEE encodings return some, while finite-only, maximum-NaN, and FNUZ encodings return none.

@[inline]

def FloatLib.Floats.ExecFloat.Binary.infinity {format : Formats.BinaryInterchange.FloatFormat} {plan : Formats.BinaryInterchange.Configured.StoragePlan format} {code : Type} [ModelCodec plan (Formats.BinaryInterchange.Model format) code] (sign : Bool := false) (_supportsInfinity : format.supportsInfinity = true := by decide) : Binary format.expWidth format.fracWidth format.encoding format.exponentBias ⋯ ⋯ ⋯ ⋯ plan code

Construct infinity, positive by default, when the configured encoding is statically known to support it.

Calling this constructor for a finite encoding fails during elaboration.

@[inline]

def FloatLib.Floats.ExecFloat.Binary.canonicalNaN? {format : Formats.BinaryInterchange.FloatFormat} {plan : Formats.BinaryInterchange.Configured.StoragePlan format} {code : Type} [ModelCodec plan (Formats.BinaryInterchange.Model format) code] : Option (Binary format.expWidth format.fracWidth format.encoding format.exponentBias ⋯ ⋯ ⋯ ⋯ plan code)

Construct the encoding's canonical quiet NaN when it has a NaN representation.

IEEE, maximum-NaN, and FNUZ encodings return some, while fully finite encodings return none.

@[inline]

def FloatLib.Floats.ExecFloat.Binary.canonicalNaN {format : Formats.BinaryInterchange.FloatFormat} {plan : Formats.BinaryInterchange.Configured.StoragePlan format} {code : Type} [ModelCodec plan (Formats.BinaryInterchange.Model format) code] (_supportsNaN : format.supportsNaN = true := by decide) : Binary format.expWidth format.fracWidth format.encoding format.exponentBias ⋯ ⋯ ⋯ ⋯ plan code

Construct the canonical quiet NaN when support is statically known.

Fully finite encodings reject this constructor during elaboration.

@[inline]

def FloatLib.Floats.ExecFloat.Binary.maxFinite {format : Formats.BinaryInterchange.FloatFormat} {plan : Formats.BinaryInterchange.Configured.StoragePlan format} {code : Type} [ModelCodec plan (Formats.BinaryInterchange.Model format) code] (sign : Bool := false) : Binary format.expWidth format.fracWidth format.encoding format.exponentBias ⋯ ⋯ ⋯ ⋯ plan code

The finite value of greatest magnitude, positive by default.

@[inline]

def FloatLib.Floats.ExecFloat.Binary.minNormal {format : Formats.BinaryInterchange.FloatFormat} {plan : Formats.BinaryInterchange.Configured.StoragePlan format} {code : Type} [ModelCodec plan (Formats.BinaryInterchange.Model format) code] (sign : Bool := false) : Binary format.expWidth format.fracWidth format.encoding format.exponentBias ⋯ ⋯ ⋯ ⋯ plan code

The normal value of least magnitude, 2 ^ minNormalExponent, positive by default.

@[inline]

def FloatLib.Floats.ExecFloat.Binary.minSubnormal {format : Formats.BinaryInterchange.FloatFormat} {plan : Formats.BinaryInterchange.Configured.StoragePlan format} {code : Type} [ModelCodec plan (Formats.BinaryInterchange.Model format) code] (sign : Bool := false) : Binary format.expWidth format.fracWidth format.encoding format.exponentBias ⋯ ⋯ ⋯ ⋯ plan code

The subnormal value of least magnitude, 2 ^ minSubnormalExponent, positive by default.

Every binary encoding has gradual underflow, so this is the least nonzero magnitude.

@[inline]

def FloatLib.Floats.ExecFloat.Binary.ulp {format : Formats.BinaryInterchange.FloatFormat} {plan : Formats.BinaryInterchange.Configured.StoragePlan format} {code : Type} [ModelCodec plan (Formats.BinaryInterchange.Model format) code] (value : Binary format.expWidth format.fracWidth format.encoding format.exponentBias ⋯ ⋯ ⋯ ⋯ plan code) : Binary format.expWidth format.fracWidth format.encoding format.exponentBias ⋯ ⋯ ⋯ ⋯ plan code

Unit in the last place: the spacing of the representable values in the binade of value, as Java's Math.ulp. A finite value with exponent e gives 2 ^ (e - fractionBits). Subnormals and zeros use the least normal exponent, so ulp 0 is minSubnormal. Infinity gives positive infinity and a NaN the format's invalid result.

@[inline]

def FloatLib.Floats.ExecFloat.Binary.epsilon {format : Formats.BinaryInterchange.FloatFormat} {plan : Formats.BinaryInterchange.Configured.StoragePlan format} {code : Type} [ModelCodec plan (Formats.BinaryInterchange.Model format) code] : Binary format.expWidth format.fracWidth format.encoding format.exponentBias ⋯ ⋯ ⋯ ⋯ plan code

Machine epsilon 2 ^ -fractionBits, the gap between one and the next larger value: ulp 1, as C's DBL_EPSILON and PyTorch's finfo.eps. It is twice Model.epsilonAt format 1, the half-ulp rounding bound of the error theorems.