Exhaustive byte-table construction

The Tabulation constructors share the row-major generation and lookup equations for arbitrary radices. The Encoding adapters supply exact model operations and byte-range guarantees. Tables are stored in Lean runtime Thunk cells, so construction is lazy and memoized while the warm path performs no model evaluation.

@[reducible, inline]

abbrev FloatLib.Floats.ExecFloat.Backend.TinyTable.Tabulation.binary (radix : Nat) (entry : Fin radix → Fin radix → UInt8) : ByteArray

Generate a row-major binary table; the coordinate bounds erase at runtime.

@[reducible, inline]

abbrev FloatLib.Floats.ExecFloat.Backend.TinyTable.Tabulation.ternary (radix : Nat) (entry : Fin radix → Fin radix → Fin radix → UInt8) : ByteArray

Generate a row-major ternary table with the final coordinate varying fastest.

theorem FloatLib.Floats.ExecFloat.Backend.TinyTable.Tabulation.getElem_binary (radix : Nat) (entry : Fin radix → Fin radix → UInt8) (left right : Fin radix) (hindex : ↑left * radix + ↑right < (binary radix entry).size) : (binary radix entry)[↑left * radix + ↑right] = entry left right

Reading a binary table at a row-major index recovers the generating entry.

theorem FloatLib.Floats.ExecFloat.Backend.TinyTable.Tabulation.getElem_ternary (radix : Nat) (entry : Fin radix → Fin radix → Fin radix → UInt8) (left right addend : Fin radix) (hindex : (↑left * radix + ↑right) * radix + ↑addend < (ternary radix entry).size) : (ternary radix entry)[(↑left * radix + ↑right) * radix + ↑addend] = entry left right addend

Reading a ternary table at a row-major index recovers all three generating coordinates.

def FloatLib.Floats.ExecFloat.Backend.TinyTable.binaryTotal {Model : Type u} (encoding : Encoding Model) (op : Model → Model → Model) : ByteArray

Build the row-major byte table of a total binary model operation.

def FloatLib.Floats.ExecFloat.Backend.TinyTable.unaryTotal {Model : Type u} (encoding : Encoding Model) (op : Model → Model) : ByteArray

Build the dense byte table of a total unary model operation.

def FloatLib.Floats.ExecFloat.Backend.TinyTable.ternaryTotal {Model : Type u} (encoding : Encoding Model) (op : Model → Model → Model → Model) : ByteArray

Build the row-major byte table of a total ternary model operation.

def FloatLib.Floats.ExecFloat.Backend.TinyTable.lazyBinaryTotal {Model : Type u} (encoding : Encoding Model) (op : Model → Model → Model) : Thunk ByteArray

Delay and memoize a total binary table.

def FloatLib.Floats.ExecFloat.Backend.TinyTable.lazyUnaryTotal {Model : Type u} (encoding : Encoding Model) (op : Model → Model) : Thunk ByteArray

Delay and memoize a total unary table.

def FloatLib.Floats.ExecFloat.Backend.TinyTable.lazyTernaryTotal {Model : Type u} (encoding : Encoding Model) (op : Model → Model → Model → Model) : Thunk ByteArray

Delay and memoize a total ternary table.

@[simp]

theorem FloatLib.Floats.ExecFloat.Backend.TinyTable.lazyBinaryTotal_get {Model : Type u} (encoding : Encoding Model) (op : Model → Model → Model) : (lazyBinaryTotal encoding op).get = binaryTotal encoding op

Forcing a lazy binary table yields the corresponding exhaustive table.

@[simp]

theorem FloatLib.Floats.ExecFloat.Backend.TinyTable.lazyUnaryTotal_get {Model : Type u} (encoding : Encoding Model) (op : Model → Model) : (lazyUnaryTotal encoding op).get = unaryTotal encoding op

Forcing a lazy unary table yields the corresponding exhaustive table.

@[simp]

theorem FloatLib.Floats.ExecFloat.Backend.TinyTable.lazyTernaryTotal_get {Model : Type u} (encoding : Encoding Model) (op : Model → Model → Model → Model) : (lazyTernaryTotal encoding op).get = ternaryTotal encoding op

Forcing a lazy ternary table yields the corresponding exhaustive table.