Verified byte tables for tiny binary formats

An operation on a format with at most eight stored bits can be compiled into a dense ByteArray. Generation uses the shared Tabulation constructors in Generic.Construction. Unlike a bijective Encoding, this interface accepts any radix; the lookup theorems therefore carry explicit input and result bounds.

Public low-bit kernels keep generated arrays in Lean runtime Thunk cells. Module initialization creates the cells without generating a table; the first lookup computes and memoizes the bytes. The defining Thunk.get equation keeps this startup optimization inside the proved boundary. See Lean Init.Core.Thunk: https://github.com/leanprover/lean4/blob/v4.34.0/src/Init/Core.lean#L109-L153.

def FloatLib.Floats.Formats.BinaryInterchange.Model.TinyTable.binaryTotal (fmt : FloatFormat) (radix : ℕ) (op : Model fmt → Model fmt → Model fmt) : ByteArray

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

Public arithmetic operations are total, so the table stores exactly one encoded result per input pair. Generating it directly avoids a sentinel encoding for an unused partial-operation case.

def FloatLib.Floats.Formats.BinaryInterchange.Model.TinyTable.unaryTotal (fmt : FloatFormat) (radix : ℕ) (op : Model fmt → Model fmt) : ByteArray

Build the dense byte table of a total unary operation.

def FloatLib.Floats.Formats.BinaryInterchange.Model.TinyTable.ternaryTotal (fmt : FloatFormat) (radix : ℕ) (op : Model fmt → Model fmt → Model fmt → Model fmt) : ByteArray

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

def FloatLib.Floats.Formats.BinaryInterchange.Model.TinyTable.lazyBinaryTotal (fmt : FloatFormat) (radix : ℕ) (op : Model fmt → Model fmt → Model fmt) : Thunk ByteArray

Delay a total binary table until its first lookup, then retain the generated bytes.

Lean's runtime implements Thunk as a thread-safe call-by-need cell. The logical equation below is definitional, so laziness changes initialization cost without changing the proof boundary. See Init.Core.Thunk in Lean: https://github.com/leanprover/lean4/blob/v4.34.0/src/Init/Core.lean#L109-L153.

@[simp]

theorem FloatLib.Floats.Formats.BinaryInterchange.Model.TinyTable.lazyBinaryTotal_get (fmt : FloatFormat) (radix : ℕ) (op : Model fmt → Model fmt → Model fmt) : (lazyBinaryTotal fmt radix op).get = binaryTotal fmt radix op

Forcing a delayed binary table returns exactly its logical generator.

def FloatLib.Floats.Formats.BinaryInterchange.Model.TinyTable.lazyUnaryTotal (fmt : FloatFormat) (radix : ℕ) (op : Model fmt → Model fmt) : Thunk ByteArray

Delay and memoize a total unary byte table.

@[simp]

theorem FloatLib.Floats.Formats.BinaryInterchange.Model.TinyTable.lazyUnaryTotal_get (fmt : FloatFormat) (radix : ℕ) (op : Model fmt → Model fmt) : (lazyUnaryTotal fmt radix op).get = unaryTotal fmt radix op

Forcing a delayed unary table returns exactly its logical generator.

def FloatLib.Floats.Formats.BinaryInterchange.Model.TinyTable.lazyTernaryTotal (fmt : FloatFormat) (radix : ℕ) (op : Model fmt → Model fmt → Model fmt → Model fmt) : Thunk ByteArray

Delay and memoize a total ternary byte table.

@[simp]

theorem FloatLib.Floats.Formats.BinaryInterchange.Model.TinyTable.lazyTernaryTotal_get (fmt : FloatFormat) (radix : ℕ) (op : Model fmt → Model fmt → Model fmt → Model fmt) : (lazyTernaryTotal fmt radix op).get = ternaryTotal fmt radix op

Forcing a delayed ternary table returns exactly its logical generator.

theorem FloatLib.Floats.Formats.BinaryInterchange.Model.TinyTable.lookupBinaryTotalByte (fmt : FloatFormat) (radix : ℕ) (radixWord : USize) (hradixWord : radixWord.toNat = radix) (_hradix : 0 < radix) (op : Model fmt → Model fmt → Model fmt) (left right : UInt8) (_hleft : left.toNat < radix) (hright : right.toNat < radix) (hword : left.toNat * radixWord.toNat + right.toNat < 2 ^ System.Platform.numBits) (hindex : (ExecFloat.Backend.TinyTable.binaryByteIndex radixWord left right).toNat < (binaryTotal fmt radix op).size) : (binaryTotal fmt radix op).uget (ExecFloat.Backend.TinyTable.binaryByteIndex radixWord left right) hindex = UInt8.ofNat (op (ofNatBits left.toNat) (ofNatBits right.toNat)).toNatBits

Native binary-table lookup returns the same code generated by the logical operation.

This is the refinement bridge used by direct UInt8 carriers. The index arithmetic is native at runtime; all range and no-overflow arguments are proof-only.

theorem FloatLib.Floats.Formats.BinaryInterchange.Model.TinyTable.lookupUnaryTotalByte (fmt : FloatFormat) (radix : ℕ) (op : Model fmt → Model fmt) (value : UInt8) (_hvalue : value.toNat < radix) (hindex : (ExecFloat.Backend.TinyTable.unaryByteIndex value).toNat < (unaryTotal fmt radix op).size) : (unaryTotal fmt radix op).uget (ExecFloat.Backend.TinyTable.unaryByteIndex value) hindex = UInt8.ofNat (op (ofNatBits value.toNat)).toNatBits

Native unary-table lookup returns the same code generated by the logical operation.

The byte-to-USize conversion is unboxed and the bound argument is erased.

theorem FloatLib.Floats.Formats.BinaryInterchange.Model.TinyTable.lookupTernaryTotalByte (fmt : FloatFormat) (radix : ℕ) (radixWord : USize) (hradixWord : radixWord.toNat = radix) (_hradix : 0 < radix) (op : Model fmt → Model fmt → Model fmt → Model fmt) (left right addend : UInt8) (_hleft : left.toNat < radix) (hright : right.toNat < radix) (haddend : addend.toNat < radix) (hleftMul : left.toNat * radixWord.toNat < 2 ^ System.Platform.numBits) (hpair : left.toNat * radixWord.toNat + right.toNat < 2 ^ System.Platform.numBits) (hpairMul : (left.toNat * radixWord.toNat + right.toNat) * radixWord.toNat < 2 ^ System.Platform.numBits) (hword : (left.toNat * radixWord.toNat + right.toNat) * radixWord.toNat + addend.toNat < 2 ^ System.Platform.numBits) (hindex : (ExecFloat.Backend.TinyTable.ternaryByteIndex radixWord left right addend).toNat < (ternaryTotal fmt radix op).size) : (ternaryTotal fmt radix op).uget (ExecFloat.Backend.TinyTable.ternaryByteIndex radixWord left right addend) hindex = UInt8.ofNat (op (ofNatBits left.toNat) (ofNatBits right.toNat) (ofNatBits addend.toNat)).toNatBits

Native ternary-table lookup returns the code generated by the logical operation.

The quotient and remainder equations reconstruct the three input coordinates from the native row-major index. All arithmetic side conditions are proof-only.

theorem FloatLib.Floats.Formats.BinaryInterchange.Model.TinyTable.binaryTotal_index_lt (fmt : FloatFormat) (radix : ℕ) (op : Model fmt → Model fmt → Model fmt) (x y : Model fmt) (hx : x.toNatBits < radix) (hy : y.toNatBits < radix) : x.toNatBits * radix + y.toNatBits < (binaryTotal fmt radix op).size

Two in-range words select an in-range row-major entry of a total-operation table.

theorem FloatLib.Floats.Formats.BinaryInterchange.Model.TinyTable.ternaryTotal_index_lt (fmt : FloatFormat) (radix : ℕ) (op : Model fmt → Model fmt → Model fmt → Model fmt) (x y z : Model fmt) (hx : x.toNatBits < radix) (hy : y.toNatBits < radix) (hz : z.toNatBits < radix) : (x.toNatBits * radix + y.toNatBits) * radix + z.toNatBits < (ternaryTotal fmt radix op).size

Three in-range words select an in-range row-major entry of a ternary table.

theorem FloatLib.Floats.Formats.BinaryInterchange.Model.TinyTable.lookupTotal (fmt : FloatFormat) (radix : ℕ) (hradix : 0 < radix) (op : Model fmt → Model fmt → Model fmt) (x y : Model fmt) (hy : y.toNatBits < radix) (hz : (op x y).toNatBits < 256) (hindex : x.toNatBits * radix + y.toNatBits < (binaryTotal fmt radix op).size) : ofNatBits (binaryTotal fmt radix op)[x.toNatBits * radix + y.toNatBits].toNat = op x y

Reading a total-operation table returns the logical operation result.

The result bound is explicit because the table stores one byte. The input bound reconstructs the two operands from their row-major index.

theorem FloatLib.Floats.Formats.BinaryInterchange.Model.TinyTable.lookupUnaryTotal (fmt : FloatFormat) (radix : ℕ) (op : Model fmt → Model fmt) (x : Model fmt) (hz : (op x).toNatBits < 256) (hindex : x.toNatBits < (unaryTotal fmt radix op).size) : ofNatBits (unaryTotal fmt radix op)[x.toNatBits].toNat = op x

Reading a total unary-operation table returns the logical operation result.

theorem FloatLib.Floats.Formats.BinaryInterchange.Model.TinyTable.lookupTernaryTotal (fmt : FloatFormat) (radix : ℕ) (hradix : 0 < radix) (op : Model fmt → Model fmt → Model fmt → Model fmt) (x y z : Model fmt) (hy : y.toNatBits < radix) (hz : z.toNatBits < radix) (hresult : (op x y z).toNatBits < 256) (hindex : (x.toNatBits * radix + y.toNatBits) * radix + z.toNatBits < (ternaryTotal fmt radix op).size) : ofNatBits (ternaryTotal fmt radix op)[(x.toNatBits * radix + y.toNatBits) * radix + z.toNatBits].toNat = op x y z

Reading a total ternary-operation table returns the logical operation result.

@[inline]

def FloatLib.Floats.Formats.BinaryInterchange.Model.TinyTable.runLazyBinaryTotal (fmt : FloatFormat) (radix : ℕ) (op : Model fmt → Model fmt → Model fmt) (table : Thunk ByteArray) (table_eq : table.get = binaryTotal fmt radix op) (x y : Model fmt) (hx : x.toNatBits < radix) (hy : y.toNatBits < radix) : Model fmt

Read a lazily memoized binary table through the ordinary Model carrier.

The table equation is an explicit argument so concrete format modules never need to unfold a large generator while elaborating either the implementation or its refinement theorem.

theorem FloatLib.Floats.Formats.BinaryInterchange.Model.TinyTable.runLazyBinaryTotal_eq (fmt : FloatFormat) (radix : ℕ) (hradix : 0 < radix) (op : Model fmt → Model fmt → Model fmt) (table : Thunk ByteArray) (table_eq : table.get = binaryTotal fmt radix op) (x y : Model fmt) (hx : x.toNatBits < radix) (hy : y.toNatBits < radix) (hresult : (op x y).toNatBits < 256) : runLazyBinaryTotal fmt radix op table table_eq x y hx hy = op x y

A lazy binary-table read returns the operation used to generate the table.

@[inline]

def FloatLib.Floats.Formats.BinaryInterchange.Model.TinyTable.runLazyUnaryTotal (fmt : FloatFormat) (radix : ℕ) (op : Model fmt → Model fmt) (table : Thunk ByteArray) (table_eq : table.get = unaryTotal fmt radix op) (x : Model fmt) (hx : x.toNatBits < radix) : Model fmt

Read a lazily memoized unary table through the ordinary Model carrier.

theorem FloatLib.Floats.Formats.BinaryInterchange.Model.TinyTable.runLazyUnaryTotal_eq (fmt : FloatFormat) (radix : ℕ) (op : Model fmt → Model fmt) (table : Thunk ByteArray) (table_eq : table.get = unaryTotal fmt radix op) (x : Model fmt) (hx : x.toNatBits < radix) (hresult : (op x).toNatBits < 256) : runLazyUnaryTotal fmt radix op table table_eq x hx = op x

A lazy unary-table read returns the operation used to generate the table.

@[inline]

def FloatLib.Floats.Formats.BinaryInterchange.Model.TinyTable.runLazyTernaryTotal (fmt : FloatFormat) (radix : ℕ) (op : Model fmt → Model fmt → Model fmt → Model fmt) (table : Thunk ByteArray) (table_eq : table.get = ternaryTotal fmt radix op) (x y z : Model fmt) (hx : x.toNatBits < radix) (hy : y.toNatBits < radix) (hz : z.toNatBits < radix) : Model fmt

Read a lazily memoized ternary table through the ordinary Model carrier.

theorem FloatLib.Floats.Formats.BinaryInterchange.Model.TinyTable.runLazyTernaryTotal_eq (fmt : FloatFormat) (radix : ℕ) (hradix : 0 < radix) (op : Model fmt → Model fmt → Model fmt → Model fmt) (table : Thunk ByteArray) (table_eq : table.get = ternaryTotal fmt radix op) (x y z : Model fmt) (hx : x.toNatBits < radix) (hy : y.toNatBits < radix) (hz : z.toNatBits < radix) (hresult : (op x y z).toNatBits < 256) : runLazyTernaryTotal fmt radix op table table_eq x y z hx hy hz = op x y z

A lazy ternary-table read returns the operation used to generate the table.