Static-byte runtime representation

Nominal binary formats of at most eight bits share a compact byte carrier, family interface, model adapters, raw table execution, and exact operation specifications. The persistent code is a UInt8 together with an erased range proof. No FloatFormat, BitVec, or arbitrary-precision integer is stored in a value.

Each standards package supplies a nominal type and a Family instance. The instance fixes the binary-interchange proof model, proves that its codes fit in one byte, and names the monomorphic kernels used at runtime. Table construction is isolated in Core.Construction; conversion and lifting theorems are isolated in Core.Proof.

Nominal Family and Plans.TablePlan instances use always_inline so the compiler can eliminate their closed format metadata and policy branches at a public call. The named table definitions remain shared and lazy.

OCP, IEEE, ONNX, and custom format packages can share these carrier and refinement interfaces. Each descriptor still determines its own exceptional-value policy.

Lean represents subtypes identically to their data carrier, so Code F has the runtime representation of UInt8; its bound is proof-only. See Lean Init.Prelude, https://github.com/leanprover/lean4/blob/v4.34.0/src/Init/Prelude.lean#L641-L643.

benchmarks/scripts/checks/static-lowbit-codegen.sh checks the intended allocation and specialization properties.

@[reducible, inline]

abbrev FloatLib.Floats.Formats.BinaryInterchange.StaticByte.ModelValue (format : FloatFormat) : Type

Bit-exact binary-interchange model value used to specify and prove a static byte format.

@[reducible, inline]

abbrev FloatLib.Floats.Formats.BinaryInterchange.StaticByte.ByteCode (format : FloatFormat) : Type

Direct byte code for one at-most-eight-bit binary-interchange model.

The proof excludes patterns above the declared format width and is erased by Lean's compiler.

@[inline]

def FloatLib.Floats.Formats.BinaryInterchange.StaticByte.byteCodeToModel {format : FloatFormat} (code : ByteCode format) : ModelValue format

Interpret a direct byte code in its exact-width binary proof model.

structure FloatLib.Floats.Formats.BinaryInterchange.StaticByte.Kernels (format : FloatFormat) : Type

Six byte kernels and their refinement equations for one binary-interchange model.

The executable fields consume and return direct byte codes. Their equations interpret those codes in the independent binary model and compare them with its specifications. A family may therefore select exhaustive native-index tables, direct byte arithmetic, or a model adapter independently for each operation without changing the universal carrier.

• add : ByteCode format → ByteCode format → ByteCode format

  Executable addition on direct byte codes.

• sub : ByteCode format → ByteCode format → ByteCode format

  Executable subtraction on direct byte codes.

• mul : ByteCode format → ByteCode format → ByteCode format

  Executable multiplication on direct byte codes.

• div : ByteCode format → ByteCode format → ByteCode format

  Executable division on direct byte codes.

• sqrt : ByteCode format → ByteCode format

  Executable square root on a direct byte code.

• fma : ByteCode format → ByteCode format → ByteCode format → ByteCode format

  Executable fused multiply-add on direct byte codes.

• add_eq_spec (left right : ByteCode format) : byteCodeToModel (self.add left right) = Model.Spec.add (byteCodeToModel left) (byteCodeToModel right)

  Addition refines the independent model specification.

• sub_eq_spec (left right : ByteCode format) : byteCodeToModel (self.sub left right) = Model.Spec.sub (byteCodeToModel left) (byteCodeToModel right)

  Subtraction refines the independent model specification.

• mul_eq_spec (left right : ByteCode format) : byteCodeToModel (self.mul left right) = Model.Spec.mul (byteCodeToModel left) (byteCodeToModel right)

  Multiplication refines the independent model specification.

• div_eq_spec (left right : ByteCode format) : byteCodeToModel (self.div left right) = Model.Spec.div (byteCodeToModel left) (byteCodeToModel right)

  Division refines the independent model specification.

• sqrt_eq_spec (value : ByteCode format) : byteCodeToModel (self.sqrt value) = Model.Spec.sqrt (byteCodeToModel value)

  Square root refines the independent model specification.

• fma_eq_spec (left right addend : ByteCode format) : byteCodeToModel (self.fma left right addend) = Model.Spec.fma (byteCodeToModel left) (byteCodeToModel right) (byteCodeToModel addend)

  Fused multiply-add refines the independent model specification.

class FloatLib.Floats.Formats.BinaryInterchange.StaticByte.Family (F : Type u) : Type

Descriptor and certified kernels for a nominal static-byte format.

The class contains no global registry. It is resolved from the nominal format type, and concrete packages provide monomorphic kernel fields rather than selecting a backend at runtime.

• format : FloatFormat

  Binary-interchange format used as the proof model.

• width_le_eight : (format F).bitWidth ≤ 8

  Every valid code fits in one byte.

• kernels : Kernels (format F)

  Statically selected proved kernels.

class FloatLib.Floats.Formats.BinaryInterchange.StaticByte.FamilyInfo (F : Type u) : Type

Inspection metadata for a nominal static-byte format.

This metadata is separate from Family so standards text never enters the runtime dictionaries used by arithmetic.

• standard : String

  Standard or specification that defines the nominal format.

@[reducible, inline]

abbrev FloatLib.Floats.Formats.BinaryInterchange.StaticByte.Code (F : Type u) [Family F] : Type

Direct byte carrier selected by a static-byte family.

@[instance_reducible]

instance FloatLib.Floats.Formats.BinaryInterchange.StaticByte.familyEncodedFormat (F : Type u) [Family F] : Numerics.EncodedFormat F

@[inline]

def FloatLib.Floats.Formats.BinaryInterchange.StaticByte.codeToModel {F : Type u} [Family F] (code : Code F) : ModelValue (Family.format F)

Convert a valid byte code to the exact-width binary proof model.

@[instance_reducible]

noncomputable instance FloatLib.Floats.Formats.BinaryInterchange.StaticByte.instFormatSemantics (F : Type u) [Family F] : Numerics.FormatSemantics F

@[inline]

def FloatLib.Floats.Formats.BinaryInterchange.StaticByte.modelToByteCode (format : FloatFormat) (width_le_eight : format.bitWidth ≤ 8) (value : ModelValue format) : ByteCode format

Convert one model value to its direct valid byte code.

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

View an at-most-eight-bit binary-interchange model through the shared finite-encoding backend.

The encoding is a proved bijection between exact model values and their stored words. It is the only binary-specific input required by the format-independent TinyTable implementation.

@[inline]

def FloatLib.Floats.Formats.BinaryInterchange.StaticByte.runBinary {format : FloatFormat} {spec : ModelValue format → ModelValue format → ModelValue format} (width_le_eight : format.bitWidth ≤ 8) (kernel : ExecFloat.Backend.TinyTable.CertifiedBinary (encoding format width_le_eight) spec) (left right : ByteCode format) : ByteCode format

Execute a shared certified binary table on the static-byte carrier.

@[inline]

def FloatLib.Floats.Formats.BinaryInterchange.StaticByte.runUnary {format : FloatFormat} {spec : ModelValue format → ModelValue format} (width_le_eight : format.bitWidth ≤ 8) (kernel : ExecFloat.Backend.TinyTable.CertifiedUnary (encoding format width_le_eight) spec) (value : ByteCode format) : ByteCode format

Execute a shared certified unary table on the static-byte carrier.

@[inline]

def FloatLib.Floats.Formats.BinaryInterchange.StaticByte.runTernary {format : FloatFormat} {spec : ModelValue format → ModelValue format → ModelValue format → ModelValue format} (width_le_eight : format.bitWidth ≤ 8) (kernel : ExecFloat.Backend.TinyTable.CertifiedTernary (encoding format width_le_eight) spec) (left right addend : ByteCode format) : ByteCode format

Execute a shared certified ternary table on the static-byte carrier.

@[inline]

def FloatLib.Floats.Formats.BinaryInterchange.StaticByte.modelTernary (format : FloatFormat) (width_le_eight : format.bitWidth ≤ 8) (op : ModelValue format → ModelValue format → ModelValue format → ModelValue format) (left right addend : ByteCode format) : ByteCode format

Adapt a model-level ternary operation to the direct byte carrier.

@[inline]

def FloatLib.Floats.Formats.BinaryInterchange.StaticByte.modelToCode {F : Type u} [Family F] (value : ModelValue (Family.format F)) : Code F

Convert one family model value to its direct valid byte code.

@[inline]

def FloatLib.Floats.Formats.BinaryInterchange.StaticByte.toModel {F : Type u} [Family F] (value : ExecFloat F) : ModelValue (Family.format F)

Interpret a universal static-byte value in the binary proof model.

@[inline]

def FloatLib.Floats.Formats.BinaryInterchange.StaticByte.ofModel {F : Type u} [Family F] (value : ModelValue (Family.format F)) : ExecFloat F

Repack a binary proof-model value into the direct static-byte carrier.

@[inline]

def FloatLib.Floats.Formats.BinaryInterchange.StaticByte.ofNatBits (F : Type u) [Family F] (bits : ℕ) : ExecFloat F

Construct a static-byte value from a natural bit pattern, reduced to the format width.

@[inline]

def FloatLib.Floats.Formats.BinaryInterchange.StaticByte.toUInt8 {F : Type u} [Family F] (value : ExecFloat F) : UInt8

Read the direct byte stored by a static-byte value.

@[inline]

def FloatLib.Floats.Formats.BinaryInterchange.StaticByte.toNatBits {F : Type u} [Family F] (value : ExecFloat F) : ℕ

Read the canonical natural-number bit pattern.

def FloatLib.Floats.Formats.BinaryInterchange.StaticByte.Spec.add {F : Type u} [Family F] (left right : ExecFloat F) : ExecFloat F

Static-byte addition specification lifted from the binary proof model.

def FloatLib.Floats.Formats.BinaryInterchange.StaticByte.Spec.sub {F : Type u} [Family F] (left right : ExecFloat F) : ExecFloat F

Static-byte subtraction specification lifted from the binary proof model.

def FloatLib.Floats.Formats.BinaryInterchange.StaticByte.Spec.mul {F : Type u} [Family F] (left right : ExecFloat F) : ExecFloat F

Static-byte multiplication specification lifted from the binary proof model.

def FloatLib.Floats.Formats.BinaryInterchange.StaticByte.Spec.div {F : Type u} [Family F] (left right : ExecFloat F) : ExecFloat F

Static-byte division specification lifted from the binary proof model.

def FloatLib.Floats.Formats.BinaryInterchange.StaticByte.Spec.sqrt {F : Type u} [Family F] (value : ExecFloat F) : ExecFloat F

Static-byte square-root specification lifted from the binary proof model.

def FloatLib.Floats.Formats.BinaryInterchange.StaticByte.Spec.fma {F : Type u} [Family F] (left right addend : ExecFloat F) : ExecFloat F

Static-byte fused multiply-add specification lifted from the binary proof model.