Correctness of byte-sized posit tables

The generic byte encoding agrees with configured posit decoding, and every direct table call implements the corresponding carrier-independent configured operation.

@[simp]

theorem FloatLib.Floats.Formats.Posit.Configured.ByteTable.decodeCode_eq_toModel {format : Format} (width_le : format.bits ≤ 8) (code : ByteCode format) : (encoding format width_le).decodeCode code = Code.toModel code

Generic byte decoding is definitionally the configured posit byte decoder.

theorem FloatLib.Floats.Formats.Posit.Configured.ByteTable.runBinary_eq_lift {format : Format} {modelSpec : Model format → Model format → Model format} (width_le : format.bits ≤ 8) (kernel : ExecFloat.Backend.TinyTable.CertifiedBinary (encoding format width_le) modelSpec) (left right : ExecFloat (Family format (Code (StoragePlan.byte width_le)) (StoragePlan.byte width_le))) : runBinary width_le kernel left right = ExecFloat.ModelCodec.liftBinary modelSpec left right

A direct binary-table call is exactly the configured lifted model operation.

theorem FloatLib.Floats.Formats.Posit.Configured.ByteTable.runUnary_eq_lift {format : Format} {modelSpec : Model format → Model format} (width_le : format.bits ≤ 8) (kernel : ExecFloat.Backend.TinyTable.CertifiedUnary (encoding format width_le) modelSpec) (value : ExecFloat (Family format (Code (StoragePlan.byte width_le)) (StoragePlan.byte width_le))) : runUnary width_le kernel value = ExecFloat.ModelCodec.liftUnary modelSpec value

A direct unary-table call is exactly the configured lifted model operation.

theorem FloatLib.Floats.Formats.Posit.Configured.ByteTable.runTernary_eq_lift {format : Format} {modelSpec : Model format → Model format → Model format → Model format} (width_le : format.bits ≤ 8) (kernel : ExecFloat.Backend.TinyTable.CertifiedTernary (encoding format width_le) modelSpec) (left right addend : ExecFloat (Family format (Code (StoragePlan.byte width_le)) (StoragePlan.byte width_le))) : runTernary width_le kernel left right addend = ExecFloat.ModelCodec.liftTernary modelSpec left right addend

A direct ternary-table call is exactly the configured lifted model operation.