Direct byte-table execution

The functions in this module are the warm execution path. They force a memoized table, compute a native row-major index, and perform one byte load. Proofs attached to Code and array bounds are erased. Once the table has been generated, lookup does not evaluate the model operation again.

@[inline]

def FloatLib.Floats.ExecFloat.Backend.TinyTable.runBinaryCode {Model : Type u} (encoding : Encoding Model) (op : Model → Model → Model) (table : Thunk ByteArray) (table_eq : table.get = binaryTotal encoding op) (left right : Code encoding) : UInt8

Read the encoded result from an arbitrary certified binary-table thunk.

@[inline]

def FloatLib.Floats.ExecFloat.Backend.TinyTable.runBinary {Model : Type u} (encoding : Encoding Model) (op : Model → Model → Model) (table : Thunk ByteArray) (table_eq : table.get = binaryTotal encoding op) (left right : Code encoding) : Code encoding

Execute one generated binary table directly on byte codes.

@[inline]

def FloatLib.Floats.ExecFloat.Backend.TinyTable.runUnaryCode {Model : Type u} (encoding : Encoding Model) (op : Model → Model) (table : Thunk ByteArray) (table_eq : table.get = unaryTotal encoding op) (value : Code encoding) : UInt8

Read the encoded result from an arbitrary certified unary-table thunk.

@[inline]

def FloatLib.Floats.ExecFloat.Backend.TinyTable.runUnary {Model : Type u} (encoding : Encoding Model) (op : Model → Model) (table : Thunk ByteArray) (table_eq : table.get = unaryTotal encoding op) (value : Code encoding) : Code encoding

Execute one generated unary table directly on a byte code.

@[inline]

def FloatLib.Floats.ExecFloat.Backend.TinyTable.runTernaryCode {Model : Type u} (encoding : Encoding Model) (op : Model → Model → Model → Model) (table : Thunk ByteArray) (table_eq : table.get = ternaryTotal encoding op) (left right addend : Code encoding) : UInt8

Read the encoded result from an arbitrary certified ternary-table thunk.

@[inline]

def FloatLib.Floats.ExecFloat.Backend.TinyTable.runTernary {Model : Type u} (encoding : Encoding Model) (op : Model → Model → Model → Model) (table : Thunk ByteArray) (table_eq : table.get = ternaryTotal encoding op) (left right addend : Code encoding) : Code encoding

Execute one generated ternary table directly on byte codes.