Correctness of configured binary byte tables #
These theorems connect direct table execution to the representation-independent configured operations. They apply to every binary-interchange descriptor whose complete encoding fits in eight bits.
theorem
FloatLib.Floats.Formats.BinaryInterchange.Configured.ByteTable.runBinary_eq_lift
{format : FloatFormat}
{modelSpec : Model format → Model format → Model format}
(width_le_eight : format.bitWidth ≤ 8)
(kernel : ExecFloat.Backend.TinyTable.CertifiedBinary (encoding format width_le_eight) modelSpec)
(left right : ExecFloat (Family format (Code (StoragePlan.byte width_le_eight)) (StoragePlan.byte width_le_eight)))
:
A direct binary-table call is exactly the configured lifted model operation.
theorem
FloatLib.Floats.Formats.BinaryInterchange.Configured.ByteTable.runUnary_eq_lift
{format : FloatFormat}
{modelSpec : Model format → Model format}
(width_le_eight : format.bitWidth ≤ 8)
(kernel : ExecFloat.Backend.TinyTable.CertifiedUnary (encoding format width_le_eight) modelSpec)
(value : ExecFloat (Family format (Code (StoragePlan.byte width_le_eight)) (StoragePlan.byte width_le_eight)))
:
A direct unary-table call is exactly the configured lifted model operation.
theorem
FloatLib.Floats.Formats.BinaryInterchange.Configured.ByteTable.runTernary_eq_lift
{format : FloatFormat}
{modelSpec : Model format → Model format → Model format → Model format}
(width_le_eight : format.bitWidth ≤ 8)
(kernel : ExecFloat.Backend.TinyTable.CertifiedTernary (encoding format width_le_eight) modelSpec)
(left right addend :
ExecFloat (Family format (Code (StoragePlan.byte width_le_eight)) (StoragePlan.byte width_le_eight)))
:
runTernary width_le_eight kernel left right addend = ExecFloat.ModelCodec.liftTernary modelSpec left right addend
A direct ternary-table call is exactly the configured lifted model operation.