Specification-carrying generic byte-table kernels

These structures retain the model operation used to generate each lazy table together with its refinement theorem. Their executable run methods delegate to the arity-specific direct lookup paths, while their equations compose the generic lookup proof with the reference definition.

structure FloatLib.Floats.ExecFloat.Backend.TinyTable.CertifiedBinary {Model : Type u} (encoding : Encoding Model) (spec : Model → Model → Model) : Type u

A lazily memoized binary table certified against a reference model specification.

• model : Model → Model → Model

  Operation used to generate the table.

• table : Thunk ByteArray

  Lazy table generated from model.

• table_eq : self.table.get = binaryTotal encoding self.model

  The table and its declared model agree definitionally or by proof.

• model_eq_spec (left right : Model) : self.model left right = spec left right

  The generation model equals the reference definition.

def FloatLib.Floats.ExecFloat.Backend.TinyTable.CertifiedBinary.ofModel {Model : Type u} {spec : Model → Model → Model} (encoding : Encoding Model) (model : Model → Model → Model) (model_eq_spec : ∀ (left right : Model), model left right = spec left right) : CertifiedBinary encoding spec

Create a certified binary kernel whose table is generated lazily from its reference model.

The named constructor lets format packages use its table equation without unfolding the model operation. The definition remains transparent to Lean.

@[inline]

def FloatLib.Floats.ExecFloat.Backend.TinyTable.CertifiedBinary.run {Model : Type u} {encoding : Encoding Model} {spec : Model → Model → Model} (kernel : CertifiedBinary encoding spec) (left right : Code encoding) : Code encoding

Execute a certified binary table kernel on two encoded operands.

@[simp]

theorem FloatLib.Floats.ExecFloat.Backend.TinyTable.CertifiedBinary.decodeCode_run {Model : Type u} {encoding : Encoding Model} {spec : Model → Model → Model} (kernel : CertifiedBinary encoding spec) (left right : Code encoding) : encoding.decodeCode (kernel.run left right) = spec (encoding.decodeCode left) (encoding.decodeCode right)

Decoding certified binary execution yields the reference binary specification.

structure FloatLib.Floats.ExecFloat.Backend.TinyTable.CertifiedUnary {Model : Type u} (encoding : Encoding Model) (spec : Model → Model) : Type u

A lazily memoized unary table certified against a reference model specification.

• model : Model → Model

  Operation used to generate the table.

• table : Thunk ByteArray

  Lazy table generated from model.

• table_eq : self.table.get = unaryTotal encoding self.model

  The table and its declared model agree.

• model_eq_spec (value : Model) : self.model value = spec value

  The generation model equals the reference definition.

def FloatLib.Floats.ExecFloat.Backend.TinyTable.CertifiedUnary.ofModel {Model : Type u} {spec : Model → Model} (encoding : Encoding Model) (model : Model → Model) (model_eq_spec : ∀ (value : Model), model value = spec value) : CertifiedUnary encoding spec

Create a certified unary kernel whose table is generated lazily from its reference model.

@[inline]

def FloatLib.Floats.ExecFloat.Backend.TinyTable.CertifiedUnary.run {Model : Type u} {encoding : Encoding Model} {spec : Model → Model} (kernel : CertifiedUnary encoding spec) (value : Code encoding) : Code encoding

Execute a certified unary table kernel on one encoded operand.

@[simp]

theorem FloatLib.Floats.ExecFloat.Backend.TinyTable.CertifiedUnary.decodeCode_run {Model : Type u} {encoding : Encoding Model} {spec : Model → Model} (kernel : CertifiedUnary encoding spec) (value : Code encoding) : encoding.decodeCode (kernel.run value) = spec (encoding.decodeCode value)

Decoding certified unary execution yields the reference unary specification.

structure FloatLib.Floats.ExecFloat.Backend.TinyTable.CertifiedTernary {Model : Type u} (encoding : Encoding Model) (spec : Model → Model → Model → Model) : Type u

A lazily memoized ternary table certified against a reference model specification.

• model : Model → Model → Model → Model

  Operation used to generate the table.

• table : Thunk ByteArray

  Lazy table generated from model.

• table_eq : self.table.get = ternaryTotal encoding self.model

  The table and its declared model agree.

• model_eq_spec (left right addend : Model) : self.model left right addend = spec left right addend

  The generation model equals the reference definition.

def FloatLib.Floats.ExecFloat.Backend.TinyTable.CertifiedTernary.ofModel {Model : Type u} {spec : Model → Model → Model → Model} (encoding : Encoding Model) (model : Model → Model → Model → Model) (model_eq_spec : ∀ (left right addend : Model), model left right addend = spec left right addend) : CertifiedTernary encoding spec

Create a certified ternary kernel whose table is generated lazily from its reference model.

@[inline]

def FloatLib.Floats.ExecFloat.Backend.TinyTable.CertifiedTernary.run {Model : Type u} {encoding : Encoding Model} {spec : Model → Model → Model → Model} (kernel : CertifiedTernary encoding spec) (left right addend : Code encoding) : Code encoding

Execute a certified ternary table kernel on three encoded operands.

@[simp]

theorem FloatLib.Floats.ExecFloat.Backend.TinyTable.CertifiedTernary.decodeCode_run {Model : Type u} {encoding : Encoding Model} {spec : Model → Model → Model → Model} (kernel : CertifiedTernary encoding spec) (left right addend : Code encoding) : encoding.decodeCode (kernel.run left right addend) = spec (encoding.decodeCode left) (encoding.decodeCode right) (encoding.decodeCode addend)

Decoding certified ternary execution yields the reference ternary specification.