Static-byte planning correctness

Static profile selection and first-order dispatch agree with the shared cost model and exact operation specifications.

theorem FloatLib.Floats.Formats.BinaryInterchange.StaticByte.Plans.BuiltinSelection.select_eq_tablePreferred {format : FloatFormat} {name : String} {operation : ExecFloat.Backend.Operation} (selection : BuiltinSelection format name operation) (profile : ExecFloat.Backend.PolicyProfile) : selection.select profile = tablePreferred format profile.policy name operation

Static profile selection is extensionally the shared cost-model decision.

theorem FloatLib.Floats.Formats.BinaryInterchange.StaticByte.Plans.executeBinary_eq_spec {F : Type u} [Family F] [planning : ExecFloat.Backend.PolicyFor F] (name : String) (operation : ExecFloat.Backend.Operation) (selection : BuiltinSelection (Family.format F) name operation) (spec run : ExecFloat F → ExecFloat F → ExecFloat F) (run_eq_spec : ∀ (left right : ExecFloat F), run left right = spec left right) (left right : ExecFloat F) : executeBinary name operation selection spec run left right = spec left right

First-order binary dispatch preserves the specification for every planning policy.

theorem FloatLib.Floats.Formats.BinaryInterchange.StaticByte.Plans.executeUnary_eq_spec {F : Type u} [Family F] [planning : ExecFloat.Backend.PolicyFor F] (name : String) (operation : ExecFloat.Backend.Operation) (selection : BuiltinSelection (Family.format F) name operation) (spec run : ExecFloat F → ExecFloat F) (run_eq_spec : ∀ (value : ExecFloat F), run value = spec value) (value : ExecFloat F) : executeUnary name operation selection spec run value = spec value

First-order unary dispatch preserves the specification for every planning policy.

theorem FloatLib.Floats.Formats.BinaryInterchange.StaticByte.Plans.executeTernary_eq_spec {F : Type u} [Family F] [planning : ExecFloat.Backend.PolicyFor F] (name : String) (operation : ExecFloat.Backend.Operation) (selection : BuiltinSelection (Family.format F) name operation) (spec tableRun exactRun : ExecFloat F → ExecFloat F → ExecFloat F → ExecFloat F) (tableRun_eq_spec : ∀ (left right addend : ExecFloat F), tableRun left right addend = spec left right addend) (exactRun_eq_spec : ∀ (left right addend : ExecFloat F), exactRun left right addend = spec left right addend) (left right addend : ExecFloat F) : executeTernary name operation selection tableRun exactRun left right addend = spec left right addend

First-order ternary dispatch preserves the specification for every planning policy.