Static-byte backend correctness

Each supplied byte operation decodes to the model-level reference result. The proofs use the operation's certificate, so they apply to exhaustive tables and arithmetic kernels alike.

theorem FloatLib.Floats.Formats.BinaryInterchange.StaticByte.Backend.add_eq_spec {F : Type u} [Family F] (left right : ExecFloat F) : add left right = Spec.add left right

Static-byte addition agrees with the family's independent reference specification.

theorem FloatLib.Floats.Formats.BinaryInterchange.StaticByte.Backend.sub_eq_spec {F : Type u} [Family F] (left right : ExecFloat F) : sub left right = Spec.sub left right

Static-byte subtraction agrees with the family's independent reference specification.

theorem FloatLib.Floats.Formats.BinaryInterchange.StaticByte.Backend.mul_eq_spec {F : Type u} [Family F] (left right : ExecFloat F) : mul left right = Spec.mul left right

Static-byte multiplication agrees with the family's independent reference specification.

theorem FloatLib.Floats.Formats.BinaryInterchange.StaticByte.Backend.div_eq_spec {F : Type u} [Family F] (left right : ExecFloat F) : div left right = Spec.div left right

Static-byte division agrees with the family's independent reference specification.

theorem FloatLib.Floats.Formats.BinaryInterchange.StaticByte.Backend.sqrt_eq_spec {F : Type u} [Family F] (value : ExecFloat F) : sqrt value = Spec.sqrt value

Static-byte square root agrees with the family's independent reference specification.

theorem FloatLib.Floats.Formats.BinaryInterchange.StaticByte.Backend.fma_eq_spec {F : Type u} [Family F] (left right addend : ExecFloat F) : fma left right addend = Spec.fma left right addend

Static-byte fused multiply-add agrees with the family's independent reference specification.

theorem FloatLib.Floats.Formats.BinaryInterchange.StaticByte.Backend.Table.binary_eq_spec {F : Type u} [Family F] {modelSpec : ModelValue (Family.format F) → ModelValue (Family.format F) → ModelValue (Family.format F)} (width_le_eight : (Family.format F).bitWidth ≤ 8) (table : ExecFloat.Backend.TinyTable.CertifiedBinary (encoding (Family.format F) width_le_eight) modelSpec) (left right : ExecFloat F) : binary width_le_eight table left right = ofModel (modelSpec (toModel left) (toModel right))

A direct binary table agrees with the model operation certified by that table.

theorem FloatLib.Floats.Formats.BinaryInterchange.StaticByte.Backend.Table.unary_eq_spec {F : Type u} [Family F] {modelSpec : ModelValue (Family.format F) → ModelValue (Family.format F)} (width_le_eight : (Family.format F).bitWidth ≤ 8) (table : ExecFloat.Backend.TinyTable.CertifiedUnary (encoding (Family.format F) width_le_eight) modelSpec) (value : ExecFloat F) : unary width_le_eight table value = ofModel (modelSpec (toModel value))

A direct unary table agrees with the model operation certified by that table.

theorem FloatLib.Floats.Formats.BinaryInterchange.StaticByte.Backend.Table.ternary_eq_spec {F : Type u} [Family F] {modelSpec : ModelValue (Family.format F) → ModelValue (Family.format F) → ModelValue (Family.format F) → ModelValue (Family.format F)} (width_le_eight : (Family.format F).bitWidth ≤ 8) (table : ExecFloat.Backend.TinyTable.CertifiedTernary (encoding (Family.format F) width_le_eight) modelSpec) (left right addend : ExecFloat F) : ternary width_le_eight table left right addend = ofModel (modelSpec (toModel left) (toModel right) (toModel addend))

A direct ternary table agrees with the model operation certified by that table.

theorem FloatLib.Floats.Formats.BinaryInterchange.StaticByte.Backend.Model.ternary_eq_spec {F : Type u} [Family F] {modelSpec : ModelValue (Family.format F) → ModelValue (Family.format F) → ModelValue (Family.format F) → ModelValue (Family.format F)} (width_le_eight : (Family.format F).bitWidth ≤ 8) (op : ModelValue (Family.format F) → ModelValue (Family.format F) → ModelValue (Family.format F) → ModelValue (Family.format F)) (op_eq_spec : ∀ (left right addend : ModelValue (Family.format F)), op left right addend = modelSpec left right addend) (left right addend : ExecFloat F) : ternary width_le_eight op left right addend = ofModel (modelSpec (toModel left) (toModel right) (toModel addend))

A direct model adapter preserves any proved ternary specification.