Static-byte capability construction

Static-byte candidates and first-order dispatchers form verified ExecFloat capabilities. Runtime planning remains in Plan.Runtime; the equations consumed here are isolated in Plan.Proof.

The planner chooses between a table and a direct kernel. These constructors attach the corresponding refinement theorem and expose the result through the shared operation interfaces.

class FloatLib.Floats.Formats.BinaryInterchange.StaticByte.Plans.TablePlan (F : Type u) [Family F] : Type

The common table plan for a nominal static-byte format.

The record supplies certified tables and profile choices for four binary operations and square root. FMA is separate: a package can offer a table candidate or use a model kernel directly.

Concrete instances should be marked instance_reducible. The capability instances below can then specialize each projection to the same first-order table kernel that a hand-written per-format instance would name.

• namePrefix : String

  Human-readable family prefix used in the five table candidate names.

• addSelection : BuiltinSelection (Family.format F) (namePrefix F ++ " addition table") ExecFloat.Backend.Operation.add

  Built-in profile decisions for addition.

• addTable : ExecFloat.Backend.TinyTable.CertifiedBinary (encoding (Family.format F) ⋯) Model.Spec.add

  Certified addition table.

• subSelection : BuiltinSelection (Family.format F) (namePrefix F ++ " subtraction table") ExecFloat.Backend.Operation.sub

  Built-in profile decisions for subtraction.

• subTable : ExecFloat.Backend.TinyTable.CertifiedBinary (encoding (Family.format F) ⋯) Model.Spec.sub

  Certified subtraction table.

• mulSelection : BuiltinSelection (Family.format F) (namePrefix F ++ " multiplication table") ExecFloat.Backend.Operation.mul

  Built-in profile decisions for multiplication.

• mulTable : ExecFloat.Backend.TinyTable.CertifiedBinary (encoding (Family.format F) ⋯) Model.Spec.mul

  Certified multiplication table.

• divSelection : BuiltinSelection (Family.format F) (namePrefix F ++ " division table") ExecFloat.Backend.Operation.div

  Built-in profile decisions for division.

• divTable : ExecFloat.Backend.TinyTable.CertifiedBinary (encoding (Family.format F) ⋯) Model.Spec.div

  Certified division table.

• sqrtSelection : BuiltinSelection (Family.format F) (namePrefix F ++ " square-root table") ExecFloat.Backend.Operation.sqrt

  Built-in profile decisions for square root.

• sqrtTable : ExecFloat.Backend.TinyTable.CertifiedUnary (encoding (Family.format F) ⋯) Model.Spec.sqrt

  Certified square-root table.

@[inline]

def FloatLib.Floats.Formats.BinaryInterchange.StaticByte.Plans.TablePlan.addName {F : Type u} [Family F] (plan : TablePlan F) : String

Name reported for the certified addition table.

@[inline]

def FloatLib.Floats.Formats.BinaryInterchange.StaticByte.Plans.TablePlan.subName {F : Type u} [Family F] (plan : TablePlan F) : String

Name reported for the certified subtraction table.

@[inline]

def FloatLib.Floats.Formats.BinaryInterchange.StaticByte.Plans.TablePlan.mulName {F : Type u} [Family F] (plan : TablePlan F) : String

Name reported for the certified multiplication table.

@[inline]

def FloatLib.Floats.Formats.BinaryInterchange.StaticByte.Plans.TablePlan.divName {F : Type u} [Family F] (plan : TablePlan F) : String

Name reported for the certified division table.

@[inline]

def FloatLib.Floats.Formats.BinaryInterchange.StaticByte.Plans.TablePlan.sqrtName {F : Type u} [Family F] (plan : TablePlan F) : String

Name reported for the certified square-root table.

@[instance_reducible, always_inline]

def FloatLib.Floats.Formats.BinaryInterchange.StaticByte.Plans.Internal.addCapability {F : Type u} [Family F] [ExecFloat.Backend.PolicyFor F] (name : String) (selection : BuiltinSelection (Family.format F) name ExecFloat.Backend.Operation.add) (run : ExecFloat F → ExecFloat F → ExecFloat F) (run_eq_spec : ∀ (left right : ExecFloat F), run left right = Spec.add left right) : ExecFloat.Add F

Construct a static-byte addition capability with certified profile selection.

@[instance_reducible, always_inline]

def FloatLib.Floats.Formats.BinaryInterchange.StaticByte.Plans.Internal.subCapability {F : Type u} [Family F] [ExecFloat.Backend.PolicyFor F] (name : String) (selection : BuiltinSelection (Family.format F) name ExecFloat.Backend.Operation.sub) (run : ExecFloat F → ExecFloat F → ExecFloat F) (run_eq_spec : ∀ (left right : ExecFloat F), run left right = Spec.sub left right) : ExecFloat.Sub F

Construct a static-byte subtraction capability with certified profile selection.

@[instance_reducible, always_inline]

def FloatLib.Floats.Formats.BinaryInterchange.StaticByte.Plans.Internal.mulCapability {F : Type u} [Family F] [ExecFloat.Backend.PolicyFor F] (name : String) (selection : BuiltinSelection (Family.format F) name ExecFloat.Backend.Operation.mul) (run : ExecFloat F → ExecFloat F → ExecFloat F) (run_eq_spec : ∀ (left right : ExecFloat F), run left right = Spec.mul left right) : ExecFloat.Mul F

Construct a static-byte multiplication capability with certified profile selection.

@[instance_reducible, always_inline]

def FloatLib.Floats.Formats.BinaryInterchange.StaticByte.Plans.Internal.divCapability {F : Type u} [Family F] [ExecFloat.Backend.PolicyFor F] (name : String) (selection : BuiltinSelection (Family.format F) name ExecFloat.Backend.Operation.div) (run : ExecFloat F → ExecFloat F → ExecFloat F) (run_eq_spec : ∀ (left right : ExecFloat F), run left right = Spec.div left right) : ExecFloat.Div F

Construct a static-byte division capability with certified profile selection.

@[instance_reducible, always_inline]

def FloatLib.Floats.Formats.BinaryInterchange.StaticByte.Plans.Internal.sqrtCapability {F : Type u} [Family F] [ExecFloat.Backend.PolicyFor F] (name : String) (selection : BuiltinSelection (Family.format F) name ExecFloat.Backend.Operation.sqrt) (run : ExecFloat F → ExecFloat F) (run_eq_spec : ∀ (value : ExecFloat F), run value = Spec.sqrt value) : ExecFloat.Sqrt F

Construct a static-byte square-root capability with certified profile selection.

@[instance_reducible, always_inline]

def FloatLib.Floats.Formats.BinaryInterchange.StaticByte.Plans.Internal.fmaCapability {F : Type u} [Family F] [ExecFloat.Backend.PolicyFor F] (name : String) (selection : BuiltinSelection (Family.format F) name ExecFloat.Backend.Operation.fma) (run : ExecFloat F → ExecFloat F → ExecFloat F → ExecFloat F) (run_eq_spec : ∀ (left right addend : ExecFloat F), run left right addend = Spec.fma left right addend) (exactRun : ExecFloat F → ExecFloat F → ExecFloat F → ExecFloat F) (exactRun_eq_spec : ∀ (left right addend : ExecFloat F), exactRun left right addend = Spec.fma left right addend) : ExecFloat.Fma F

Construct a static-byte FMA capability from named table and exact kernels.

@[instance_reducible, always_inline]

def FloatLib.Floats.Formats.BinaryInterchange.StaticByte.Plans.Internal.directFmaCapability {F : Type u} [Family F] [ExecFloat.Backend.PolicyFor F] (run : ExecFloat F → ExecFloat F → ExecFloat F → ExecFloat F) (run_eq_spec : ∀ (left right addend : ExecFloat F), run left right addend = Spec.fma left right addend) : ExecFloat.Fma F

Construct an exact-only static-byte FMA without retaining certificate closure dispatch.

@[instance_reducible, always_inline]

def FloatLib.Floats.Formats.BinaryInterchange.StaticByte.Plans.Internal.addTableCapability {F : Type u} [Family F] [ExecFloat.Backend.PolicyFor F] (name : String) (selection : BuiltinSelection (Family.format F) name ExecFloat.Backend.Operation.add) (width_le_eight : (Family.format F).bitWidth ≤ 8) (table : ExecFloat.Backend.TinyTable.CertifiedBinary (encoding (Family.format F) width_le_eight) Model.Spec.add) : ExecFloat.Add F

Construct an addition capability directly from a certified byte table.

The executable table lookup and its refinement proof are derived from the same certificate, so a format package cannot accidentally pair a kernel with the wrong theorem.

@[instance_reducible, always_inline]

def FloatLib.Floats.Formats.BinaryInterchange.StaticByte.Plans.Internal.subTableCapability {F : Type u} [Family F] [ExecFloat.Backend.PolicyFor F] (name : String) (selection : BuiltinSelection (Family.format F) name ExecFloat.Backend.Operation.sub) (width_le_eight : (Family.format F).bitWidth ≤ 8) (table : ExecFloat.Backend.TinyTable.CertifiedBinary (encoding (Family.format F) width_le_eight) Model.Spec.sub) : ExecFloat.Sub F

Construct a subtraction capability directly from a certified byte table.

@[instance_reducible, always_inline]

def FloatLib.Floats.Formats.BinaryInterchange.StaticByte.Plans.Internal.mulTableCapability {F : Type u} [Family F] [ExecFloat.Backend.PolicyFor F] (name : String) (selection : BuiltinSelection (Family.format F) name ExecFloat.Backend.Operation.mul) (width_le_eight : (Family.format F).bitWidth ≤ 8) (table : ExecFloat.Backend.TinyTable.CertifiedBinary (encoding (Family.format F) width_le_eight) Model.Spec.mul) : ExecFloat.Mul F

Construct a multiplication capability directly from a certified byte table.

@[instance_reducible, always_inline]

def FloatLib.Floats.Formats.BinaryInterchange.StaticByte.Plans.Internal.divTableCapability {F : Type u} [Family F] [ExecFloat.Backend.PolicyFor F] (name : String) (selection : BuiltinSelection (Family.format F) name ExecFloat.Backend.Operation.div) (width_le_eight : (Family.format F).bitWidth ≤ 8) (table : ExecFloat.Backend.TinyTable.CertifiedBinary (encoding (Family.format F) width_le_eight) Model.Spec.div) : ExecFloat.Div F

Construct a division capability directly from a certified byte table.

@[instance_reducible, always_inline]

def FloatLib.Floats.Formats.BinaryInterchange.StaticByte.Plans.Internal.sqrtTableCapability {F : Type u} [Family F] [ExecFloat.Backend.PolicyFor F] (name : String) (selection : BuiltinSelection (Family.format F) name ExecFloat.Backend.Operation.sqrt) (width_le_eight : (Family.format F).bitWidth ≤ 8) (table : ExecFloat.Backend.TinyTable.CertifiedUnary (encoding (Family.format F) width_le_eight) Model.Spec.sqrt) : ExecFloat.Sqrt F

Construct a square-root capability directly from a certified byte table.

@[instance_reducible, always_inline]

def FloatLib.Floats.Formats.BinaryInterchange.StaticByte.Plans.fmaTableCapability {F : Type u} [Family F] [ExecFloat.Backend.PolicyFor F] (name : String) (selection : BuiltinSelection (Family.format F) name ExecFloat.Backend.Operation.fma) (width_le_eight : (Family.format F).bitWidth ≤ 8) (table : ExecFloat.Backend.TinyTable.CertifiedTernary (encoding (Family.format F) width_le_eight) Model.Spec.fma) (exactRun : ModelValue (Family.format F) → ModelValue (Family.format F) → ModelValue (Family.format F) → ModelValue (Family.format F)) (exactRun_eq_spec : ∀ (left right addend : ModelValue (Family.format F)), exactRun left right addend = Model.Spec.fma left right addend) : ExecFloat.Fma F

Construct a policy-selected FMA capability from a certified table and a proved exact kernel.

@[instance_reducible, always_inline]

def FloatLib.Floats.Formats.BinaryInterchange.StaticByte.Plans.modelFmaCapability {F : Type u} [Family F] [ExecFloat.Backend.PolicyFor F] (width_le_eight : (Family.format F).bitWidth ≤ 8) (run : ModelValue (Family.format F) → ModelValue (Family.format F) → ModelValue (Family.format F) → ModelValue (Family.format F)) (run_eq_spec : ∀ (left right addend : ModelValue (Family.format F)), run left right addend = Model.Spec.fma left right addend) : ExecFloat.Fma F

Construct an exact-only FMA capability from a proved model-level kernel.

The planned instances deliberately outrank the direct-family instances in StaticByte.Backend.Construction. A static-byte family without a TablePlan therefore keeps its ordinary family kernels. With a TablePlan, the planning profile chooses between a table and the exact baseline.

@[instance_reducible, always_inline, instance 200]

instance FloatLib.Floats.Formats.BinaryInterchange.StaticByte.Plans.tablePlanAddCapability (F : Type u) [Family F] [plan : TablePlan F] [planning : ExecFloat.Backend.PolicyFor F] : ExecFloat.Add F

@[instance_reducible, always_inline, instance 200]

instance FloatLib.Floats.Formats.BinaryInterchange.StaticByte.Plans.tablePlanSubCapability (F : Type u) [Family F] [plan : TablePlan F] [planning : ExecFloat.Backend.PolicyFor F] : ExecFloat.Sub F

@[instance_reducible, always_inline, instance 200]

instance FloatLib.Floats.Formats.BinaryInterchange.StaticByte.Plans.tablePlanMulCapability (F : Type u) [Family F] [plan : TablePlan F] [planning : ExecFloat.Backend.PolicyFor F] : ExecFloat.Mul F

@[instance_reducible, always_inline, instance 200]

instance FloatLib.Floats.Formats.BinaryInterchange.StaticByte.Plans.tablePlanDivCapability (F : Type u) [Family F] [plan : TablePlan F] [planning : ExecFloat.Backend.PolicyFor F] : ExecFloat.Div F

@[instance_reducible, always_inline, instance 200]

instance FloatLib.Floats.Formats.BinaryInterchange.StaticByte.Plans.tablePlanSqrtCapability (F : Type u) [Family F] [plan : TablePlan F] [planning : ExecFloat.Backend.PolicyFor F] : ExecFloat.Sqrt F