Static-byte representation and lifting proofs

Byte/model round trips, certified table execution equations, injectivity, and lifting theorems justify nominal FP8 and other static-byte families.

theorem FloatLib.Floats.Formats.BinaryInterchange.StaticByte.model_toNatBits_lt_byte {F : Type u} [Family F] (value : ModelValue (Family.format F)) : Model.toNatBits value < 256

Every model code selected by a static-byte family fits in UInt8.

@[simp]

theorem FloatLib.Floats.Formats.BinaryInterchange.StaticByte.byteCodeToModel_modelToByteCode (format : FloatFormat) (width_le_eight : format.bitWidth ≤ 8) (value : ModelValue format) : byteCodeToModel (modelToByteCode format width_le_eight value) = value

Encoding a model value as a byte code and decoding it returns the value.

@[simp]

theorem FloatLib.Floats.Formats.BinaryInterchange.StaticByte.byteCodeToModel_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) : byteCodeToModel (runBinary width_le_eight kernel left right) = spec (byteCodeToModel left) (byteCodeToModel right)

Running a certified binary table on byte codes decodes to the specification applied to the decoded operands.

@[simp]

theorem FloatLib.Floats.Formats.BinaryInterchange.StaticByte.byteCodeToModel_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) : byteCodeToModel (runUnary width_le_eight kernel value) = spec (byteCodeToModel value)

Running a certified unary table on a byte code decodes to the specification applied to the decoded operand.

@[simp]

theorem FloatLib.Floats.Formats.BinaryInterchange.StaticByte.byteCodeToModel_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) : byteCodeToModel (runTernary width_le_eight kernel left right addend) = spec (byteCodeToModel left) (byteCodeToModel right) (byteCodeToModel addend)

Running a certified ternary table on byte codes decodes to the specification applied to the decoded operands.

@[simp]

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

Decoding the byte-level lift of a ternary model operation gives that operation on the decoded operands.

@[simp]

theorem FloatLib.Floats.Formats.BinaryInterchange.StaticByte.codeToModel_modelToCode {F : Type u} [Family F] (value : ModelValue (Family.format F)) : codeToModel (modelToCode value) = value

Encoding a model value as a family code and decoding it returns the value.

@[simp]

theorem FloatLib.Floats.Formats.BinaryInterchange.StaticByte.toModel_ofModel {F : Type u} [Family F] (value : ModelValue (Family.format F)) : toModel (ofModel value) = value

toModel inverts ofModel on model values.

@[simp]

theorem FloatLib.Floats.Formats.BinaryInterchange.StaticByte.modelToCode_codeToModel {F : Type u} [Family F] (code : Code F) : modelToCode (codeToModel code) = code

Decoding a stored code and encoding the result returns the same code.

@[simp]

theorem FloatLib.Floats.Formats.BinaryInterchange.StaticByte.ofModel_toModel {F : Type u} [Family F] (value : ExecFloat F) : ofModel (toModel value) = value

ofModel inverts toModel on stored values.

theorem FloatLib.Floats.Formats.BinaryInterchange.StaticByte.toModel_injective {F : Type u} [Family F] {left right : ExecFloat F} (equality : toModel left = toModel right) : left = right

The model conversion is injective because ofModel is its inverse.

theorem FloatLib.Floats.Formats.BinaryInterchange.StaticByte.liftBinary_eq_spec {F : Type u} [Family F] (run : Code F → Code F → Code F) (modelSpec : ModelValue (Family.format F) → ModelValue (Family.format F) → ModelValue (Family.format F)) (run_eq_spec : ∀ (left right : Code F), byteCodeToModel (run left right) = modelSpec (byteCodeToModel left) (byteCodeToModel right)) (left right : ExecFloat F) : ExecFloat.ofRaw (run left.raw right.raw) = ofModel (modelSpec (toModel left) (toModel right))

Lift a direct binary byte-kernel refinement equation to the universal static-byte carrier.

The executable function is an explicit argument. A capability can name its byte kernel directly and use this theorem to prove its refinement.

theorem FloatLib.Floats.Formats.BinaryInterchange.StaticByte.liftUnary_eq_spec {F : Type u} [Family F] (run : Code F → Code F) (modelSpec : ModelValue (Family.format F) → ModelValue (Family.format F)) (run_eq_spec : ∀ (value : Code F), byteCodeToModel (run value) = modelSpec (byteCodeToModel value)) (value : ExecFloat F) : ExecFloat.ofRaw (run value.raw) = ofModel (modelSpec (toModel value))

Lift a direct unary byte-kernel refinement equation to the universal static-byte carrier.

The theorem is proof-only; it does not add a conversion or dispatch layer to the executable kernel.

theorem FloatLib.Floats.Formats.BinaryInterchange.StaticByte.liftTernary_eq_spec {F : Type u} [Family F] (run : Code F → Code F → Code F → Code F) (modelSpec : ModelValue (Family.format F) → ModelValue (Family.format F) → ModelValue (Family.format F) → ModelValue (Family.format F)) (run_eq_spec : ∀ (left right addend : Code F), byteCodeToModel (run left right addend) = modelSpec (byteCodeToModel left) (byteCodeToModel right) (byteCodeToModel addend)) (left right addend : ExecFloat F) : ExecFloat.ofRaw (run left.raw right.raw addend.raw) = ofModel (modelSpec (toModel left) (toModel right) (toModel addend))

Lift a direct ternary byte-kernel refinement equation to the universal static-byte carrier.

This is the erased proof bridge used by monomorphic fused-multiply-add capabilities.

theorem FloatLib.Floats.Formats.BinaryInterchange.StaticByte.liftBinaryTable_eq_spec {F : Type u} [Family F] {modelSpec : ModelValue (Family.format F) → ModelValue (Family.format F) → ModelValue (Family.format F)} (width_le_eight : (Family.format F).bitWidth ≤ 8) (kernel : ExecFloat.Backend.TinyTable.CertifiedBinary (encoding (Family.format F) width_le_eight) modelSpec) (left right : ExecFloat F) : ExecFloat.ofRaw (runBinary width_le_eight kernel left.raw right.raw) = ofModel (modelSpec (toModel left) (toModel right))

Lift a certified binary byte table directly to the universal static-byte carrier.

This proof-only wrapper packages the recurring composition of liftBinary_eq_spec with the certificate carried by TinyTable.CertifiedBinary. Concrete format modules can therefore keep their executable functions monomorphic while sharing the erased refinement argument.

theorem FloatLib.Floats.Formats.BinaryInterchange.StaticByte.liftUnaryTable_eq_spec {F : Type u} [Family F] {modelSpec : ModelValue (Family.format F) → ModelValue (Family.format F)} (width_le_eight : (Family.format F).bitWidth ≤ 8) (kernel : ExecFloat.Backend.TinyTable.CertifiedUnary (encoding (Family.format F) width_le_eight) modelSpec) (value : ExecFloat F) : ExecFloat.ofRaw (runUnary width_le_eight kernel value.raw) = ofModel (modelSpec (toModel value))

Lift a certified unary byte table directly to the universal static-byte carrier.

The certificate is the same one used by byteCodeToModel_runUnary, lifted to ExecFloat.

theorem FloatLib.Floats.Formats.BinaryInterchange.StaticByte.liftTernaryTable_eq_spec {F : Type u} [Family F] {modelSpec : ModelValue (Family.format F) → ModelValue (Family.format F) → ModelValue (Family.format F) → ModelValue (Family.format F)} (width_le_eight : (Family.format F).bitWidth ≤ 8) (kernel : ExecFloat.Backend.TinyTable.CertifiedTernary (encoding (Family.format F) width_le_eight) modelSpec) (left right addend : ExecFloat F) : ExecFloat.ofRaw (runTernary width_le_eight kernel left.raw right.raw addend.raw) = ofModel (modelSpec (toModel left) (toModel right) (toModel addend))

Lift a certified ternary byte table directly to the universal static-byte carrier.

The concrete table remains named in the monomorphic executable definition; only its refinement proof is factored through this theorem.

theorem FloatLib.Floats.Formats.BinaryInterchange.StaticByte.liftModelTernary_eq_spec {F : Type u} [Family F] {modelSpec : ModelValue (Family.format F) → ModelValue (Family.format F) → ModelValue (Family.format F) → ModelValue (Family.format F)} (width_le_eight : (Family.format F).bitWidth ≤ 8) (op : ModelValue (Family.format F) → ModelValue (Family.format F) → ModelValue (Family.format F) → ModelValue (Family.format F)) (op_eq_spec : ∀ (left right addend : ModelValue (Family.format F)), op left right addend = modelSpec left right addend) (left right addend : ExecFloat F) : ExecFloat.ofRaw (modelTernary (Family.format F) width_le_eight op left.raw right.raw addend.raw) = ofModel (modelSpec (toModel left) (toModel right) (toModel addend))

Lift a proved model-level ternary kernel through the direct-byte representation.

This gives a table-free FMA construction. The executable function is modelTernary; op_eq_spec supplies its correctness proof.