Direct exhaustive runtime kernels for configured byte formats

Every binary-interchange descriptor occupying at most eight encoded bits admits the same format-independent tiny-table backend used by other finite encodings. Table generation evaluates the reference definition, while warm execution performs native indexing and one byte load.

The operation planner may reject a table when its setup cost or resident memory does not suit the workload. That choice does not affect the refinement proofs in ByteTable.Proof.

def FloatLib.Floats.Formats.BinaryInterchange.Configured.ByteTable.radix (format : FloatFormat) : ℕ

The number of codes of a descriptor, 2 ^ format.bitWidth.

A table lookup compiled for an arbitrary descriptor evaluates this on every call. Compiled code uses the shift of radix_eq_shift, because Nat.pow runs through arbitrary-precision arithmetic.

def FloatLib.Floats.Formats.BinaryInterchange.Configured.ByteTable.radixShift (format : FloatFormat) : ℕ

The shift that compiled code runs for radix.

@[csimp]

theorem FloatLib.Floats.Formats.BinaryInterchange.Configured.ByteTable.radix_eq_shift : radix = radixShift

radix and its compiled shift agree.

@[inline]

def FloatLib.Floats.Formats.BinaryInterchange.Configured.ByteTable.encoding (format : FloatFormat) (width_le_eight : format.bitWidth ≤ 8) : ExecFloat.Backend.TinyTable.Encoding (Model format)

The exact binary-interchange model as a proved finite byte encoding.

It is inlined so that a table lookup compiled for an arbitrary descriptor reads radix without allocating the encoding record on every call.

Tables generated from reference model kernels

def FloatLib.Floats.Formats.BinaryInterchange.Configured.ByteTable.addTable {format : FloatFormat} (width_le_eight : format.bitWidth ≤ 8) : ExecFloat.Backend.TinyTable.CertifiedBinary (encoding format width_le_eight) Model.Spec.add

Lazily generated direct addition table.

def FloatLib.Floats.Formats.BinaryInterchange.Configured.ByteTable.subTable {format : FloatFormat} (width_le_eight : format.bitWidth ≤ 8) : ExecFloat.Backend.TinyTable.CertifiedBinary (encoding format width_le_eight) Model.Spec.sub

Lazily generated direct subtraction table.

def FloatLib.Floats.Formats.BinaryInterchange.Configured.ByteTable.mulTable {format : FloatFormat} (width_le_eight : format.bitWidth ≤ 8) : ExecFloat.Backend.TinyTable.CertifiedBinary (encoding format width_le_eight) Model.Spec.mul

Lazily generated direct multiplication table.

def FloatLib.Floats.Formats.BinaryInterchange.Configured.ByteTable.divTable {format : FloatFormat} (width_le_eight : format.bitWidth ≤ 8) : ExecFloat.Backend.TinyTable.CertifiedBinary (encoding format width_le_eight) Model.Spec.div

Lazily generated direct division table.

def FloatLib.Floats.Formats.BinaryInterchange.Configured.ByteTable.sqrtTable {format : FloatFormat} (width_le_eight : format.bitWidth ≤ 8) : ExecFloat.Backend.TinyTable.CertifiedUnary (encoding format width_le_eight) Model.Spec.sqrt

Lazily generated direct square-root table.

def FloatLib.Floats.Formats.BinaryInterchange.Configured.ByteTable.fmaTable {format : FloatFormat} (width_le_eight : format.bitWidth ≤ 8) : ExecFloat.Backend.TinyTable.CertifiedTernary (encoding format width_le_eight) Model.Spec.fma

Lazily generated direct fused-multiply-add table.

Direct configured-carrier execution

@[inline]

def FloatLib.Floats.Formats.BinaryInterchange.Configured.ByteTable.runBinary {format : FloatFormat} {modelSpec : Model format → Model format → Model format} (width_le_eight : format.bitWidth ≤ 8) (kernel : ExecFloat.Backend.TinyTable.CertifiedBinary (encoding format width_le_eight) modelSpec) (left right : ExecFloat (Family format (Code (StoragePlan.byte width_le_eight)) (StoragePlan.byte width_le_eight))) : ExecFloat (Family format (Code (StoragePlan.byte width_le_eight)) (StoragePlan.byte width_le_eight))

Execute one already-constructed certified binary table on the configured byte carrier.

Taking the table as an argument lets the selected capability capture one memoizing Thunk instead of building a fresh cell on every arithmetic call.

@[inline]

def FloatLib.Floats.Formats.BinaryInterchange.Configured.ByteTable.runUnary {format : FloatFormat} {modelSpec : Model format → Model format} (width_le_eight : format.bitWidth ≤ 8) (kernel : ExecFloat.Backend.TinyTable.CertifiedUnary (encoding format width_le_eight) modelSpec) (value : ExecFloat (Family format (Code (StoragePlan.byte width_le_eight)) (StoragePlan.byte width_le_eight))) : ExecFloat (Family format (Code (StoragePlan.byte width_le_eight)) (StoragePlan.byte width_le_eight))

Execute one already-constructed certified unary table on the configured byte carrier.

@[inline]

def FloatLib.Floats.Formats.BinaryInterchange.Configured.ByteTable.runTernary {format : FloatFormat} {modelSpec : Model format → Model format → Model format → Model format} (width_le_eight : format.bitWidth ≤ 8) (kernel : ExecFloat.Backend.TinyTable.CertifiedTernary (encoding format width_le_eight) modelSpec) (left right addend : ExecFloat (Family format (Code (StoragePlan.byte width_le_eight)) (StoragePlan.byte width_le_eight))) : ExecFloat (Family format (Code (StoragePlan.byte width_le_eight)) (StoragePlan.byte width_le_eight))

Execute one already-constructed certified ternary table on the configured byte carrier.