Certified construction of byte-sized posit tables

Every posit occupying at most eight encoded bits has at most 256 possible words. These constructors evaluate the proved direct exact-dyadic kernels lazily for every table entry. Warm execution then performs only native indexing and one ByteArray load.

Dense unary and binary tables remain small through eight bits. A dense ternary table has 2 ^ (3 * bits) bytes, so the execution planner may reject FMA when setup or resident memory cannot be amortized.

def FloatLib.Floats.Formats.Posit.Configured.ByteTable.addTable {format : Format} (width_le : format.bits ≤ 8) : ExecFloat.Backend.TinyTable.CertifiedBinary (encoding format width_le) Model.Spec.add

Lazily generated direct addition table.

The generator is the model-valued direct kernel Model.DirectDyadicArithmetic.add, so the refinement theorem add_eq_spec makes the resulting table a table for Model.Spec.add.

def FloatLib.Floats.Formats.Posit.Configured.ByteTable.subTable {format : Format} (width_le : format.bits ≤ 8) : ExecFloat.Backend.TinyTable.CertifiedBinary (encoding format width_le) Model.Spec.sub

Lazily generated direct subtraction table from the model-valued direct kernel.

def FloatLib.Floats.Formats.Posit.Configured.ByteTable.mulTable {format : Format} (width_le : format.bits ≤ 8) : ExecFloat.Backend.TinyTable.CertifiedBinary (encoding format width_le) Model.Spec.mul

Lazily generated direct multiplication table from the model-valued direct kernel.

def FloatLib.Floats.Formats.Posit.Configured.ByteTable.divTable {format : Format} (width_le : format.bits ≤ 8) : ExecFloat.Backend.TinyTable.CertifiedBinary (encoding format width_le) Model.Spec.div

Lazily generated direct division table using one quotient prefix and exact remainder.

def FloatLib.Floats.Formats.Posit.Configured.ByteTable.sqrtTable {format : Format} (width_le : format.bits ≤ 8) : ExecFloat.Backend.TinyTable.CertifiedUnary (encoding format width_le) Model.Spec.sqrt

Lazily generated direct square-root table using one root prefix and exact square remainder.

def FloatLib.Floats.Formats.Posit.Configured.ByteTable.fmaTable {format : Format} (width_le : format.bits ≤ 8) : ExecFloat.Backend.TinyTable.CertifiedTernary (encoding format width_le) Model.Spec.fma

Lazily generated direct fused-multiply-add table from the model-valued direct kernel.