Semantic refinement of byte-table execution

These theorems prove that each direct byte lookup returns the encoding of the reference exact model operation. Format packages can therefore compose fast execution with their own arithmetic proofs without exposing table internals to users.

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

A binary thunk read returns the code generated by its reference model operation.

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

Binary table execution returns the direct encoding of the reference model operation.

@[simp]

theorem FloatLib.Floats.ExecFloat.Backend.TinyTable.decodeCode_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) : encoding.decodeCode (runBinary encoding op table table_eq left right) = op (encoding.decodeCode left) (encoding.decodeCode right)

Decoding a binary table result yields the reference model operation.

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

A unary thunk read returns the code generated by its reference model operation.

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

Unary table execution returns the direct encoding of the reference model operation.

@[simp]

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

Decoding a unary table result yields the reference model operation.

theorem FloatLib.Floats.ExecFloat.Backend.TinyTable.runTernaryCode_eq {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) : runTernaryCode encoding op table table_eq left right addend = UInt8.ofNat ↑(encoding.encode (op (encoding.decodeCode left) (encoding.decodeCode right) (encoding.decodeCode addend)))

A ternary thunk read returns the code generated by its reference model operation.

theorem FloatLib.Floats.ExecFloat.Backend.TinyTable.runTernary_eq_encodeCode {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) : runTernary encoding op table table_eq left right addend = encoding.encodeCode (op (encoding.decodeCode left) (encoding.decodeCode right) (encoding.decodeCode addend))

Ternary table execution returns the direct encoding of the reference model operation.

@[simp]

theorem FloatLib.Floats.ExecFloat.Backend.TinyTable.decodeCode_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) : encoding.decodeCode (runTernary encoding op table table_eq left right addend) = op (encoding.decodeCode left) (encoding.decodeCode right) (encoding.decodeCode addend)

Decoding a ternary table result yields the reference model operation.