Byte-table lookup certificates

These theorems identify each native array read with the encoded result used to generate that entry. Runtime definitions use the equations to prove that the returned byte is a valid code; Generic.Proof then establishes equality of the decoded result with the model operation.

theorem FloatLib.Floats.ExecFloat.Backend.TinyTable.lookupBinary {Model : Type u} (encoding : Encoding Model) (op : Model → Model → Model) (left right : Code encoding) (hindex : (binaryByteIndex (radixWord encoding) left.val right.val).toNat < (binaryTotal encoding op).size) : (binaryTotal encoding op).uget (binaryByteIndex (radixWord encoding) left.val right.val) hindex = UInt8.ofNat ↑(encoding.encode (op (encoding.decodeCode left) (encoding.decodeCode right)))

A native binary table read returns the encoded model-operation result.

theorem FloatLib.Floats.ExecFloat.Backend.TinyTable.lookupUnary {Model : Type u} (encoding : Encoding Model) (op : Model → Model) (value : Code encoding) (hindex : (unaryByteIndex value.val).toNat < (unaryTotal encoding op).size) : (unaryTotal encoding op).uget (unaryByteIndex value.val) hindex = UInt8.ofNat ↑(encoding.encode (op (encoding.decodeCode value)))

A native unary table read returns the encoded model-operation result.

theorem FloatLib.Floats.ExecFloat.Backend.TinyTable.lookupTernary {Model : Type u} (encoding : Encoding Model) (op : Model → Model → Model → Model) (left right addend : Code encoding) (hindex : (ternaryByteIndex (radixWord encoding) left.val right.val addend.val).toNat < (ternaryTotal encoding op).size) : (ternaryTotal encoding op).uget (ternaryByteIndex (radixWord encoding) left.val right.val addend.val) hindex = UInt8.ofNat ↑(encoding.encode (op (encoding.decodeCode left) (encoding.decodeCode right) (encoding.decodeCode addend)))

A native ternary table read returns the encoded model-operation result.