Static-byte planning runtime

Nominal binary formats of at most eight bits use cost estimates, table candidates, profile selection, and dispatch specialized to static-byte storage.

Correctness theorems live in Plan.Proof, while capability construction lives in Plan.Construction. This runtime layer can therefore be reused without importing either module.

def FloatLib.Floats.Formats.BinaryInterchange.StaticByte.Plans.exactEstimate (operation : ExecFloat.Backend.Operation) : ExecFloat.Backend.Candidate

Cost estimate for evaluating the exact baseline directly.

This is the mandatory proved implementation in table-backed plans. The constants are calibration inputs, not semantic facts; changing them can alter a plan without changing any refinement theorem.

def FloatLib.Floats.Formats.BinaryInterchange.StaticByte.Plans.tableEstimate (format : FloatFormat) (name : String) (operation : ExecFloat.Backend.Operation) : ExecFloat.Backend.Candidate

Estimate a dense byte-result table from the format width and operation arity.

Table construction evaluates a certified kernel once per entry. residentBytes counts the result bytes in the cached ByteArray; it excludes object and allocator overhead.

@[inline]

def FloatLib.Floats.Formats.BinaryInterchange.StaticByte.Plans.binaryTableCertified {F : Type u} [Family F] (name : String) (operation : ExecFloat.Backend.Operation) (spec run : ExecFloat F → ExecFloat F → ExecFloat F) (run_eq_spec : ∀ (left right : ExecFloat F), run left right = spec left right) : ExecFloat.Backend.Certified spec

Certify a binary kernel with the table cost estimate.

def FloatLib.Floats.Formats.BinaryInterchange.StaticByte.Plans.binaryTable {F : Type u} [Family F] (name : String) (operation : ExecFloat.Backend.Operation) (spec run : ExecFloat F → ExecFloat F → ExecFloat F) (run_eq_spec : ∀ (left right : ExecFloat F), run left right = spec left right) : ExecFloat.Backend.CandidateSet (ExecFloat.Backend.Certified spec)

Certified binary table candidate paired with the executable exact baseline.

@[inline]

def FloatLib.Floats.Formats.BinaryInterchange.StaticByte.Plans.unaryTableCertified {F : Type u} [Family F] (name : String) (operation : ExecFloat.Backend.Operation) (spec run : ExecFloat F → ExecFloat F) (run_eq_spec : ∀ (value : ExecFloat F), run value = spec value) : ExecFloat.Backend.Certified spec

Certify a unary kernel with the table cost estimate.

def FloatLib.Floats.Formats.BinaryInterchange.StaticByte.Plans.unaryTable {F : Type u} [Family F] (name : String) (operation : ExecFloat.Backend.Operation) (spec run : ExecFloat F → ExecFloat F) (run_eq_spec : ∀ (value : ExecFloat F), run value = spec value) : ExecFloat.Backend.CandidateSet (ExecFloat.Backend.Certified spec)

Certified unary table candidate paired with the executable exact baseline.

@[inline]

def FloatLib.Floats.Formats.BinaryInterchange.StaticByte.Plans.ternaryTableCertified {F : Type u} [Family F] (name : String) (operation : ExecFloat.Backend.Operation) (spec run : ExecFloat F → ExecFloat F → ExecFloat F → ExecFloat F) (run_eq_spec : ∀ (left right addend : ExecFloat F), run left right addend = spec left right addend) : ExecFloat.Backend.Certified spec

Certify a ternary kernel with the table cost estimate.

def FloatLib.Floats.Formats.BinaryInterchange.StaticByte.Plans.ternaryTable {F : Type u} [Family F] (name : String) (operation : ExecFloat.Backend.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) : ExecFloat.Backend.CandidateSet (ExecFloat.Backend.Certified spec)

Certified ternary table candidate paired with a first-order executable exact baseline.

Keeping the baseline as a named proved kernel matters for formats whose balanced policy rejects a large FMA table: public execution can then specialize to that kernel without calling the generic family specification through a boxed dictionary.

@[inline]

def FloatLib.Floats.Formats.BinaryInterchange.StaticByte.Plans.tablePreferred (format : FloatFormat) (policy : ExecFloat.Backend.Policy) (name : String) (operation : ExecFloat.Backend.Operation) : Bool

Whether the shared planner selects the exhaustive table over the exact baseline.

Static-byte portfolios contain exactly one optional table candidate. Repeating the selector's single comparison as a Bool lets a monomorphic operation branch between two named first-order kernels without projecting an executable closure from Certified. The cost calculation remains identical to Backend.selectCertified, so planning reports and execution use the same choice.

structure FloatLib.Floats.Formats.BinaryInterchange.StaticByte.Plans.BuiltinSelection (format : FloatFormat) (name : String) (operation : ExecFloat.Backend.Operation) : Type

Certified table choices for the three built-in planning profiles.

Closed nominal formats provide these three bits once per operation. Their equality fields prove that the literals are exactly the result of the shared cost model. The compiler can then reduce a built-in profile to a direct kernel while a custom profile retains the general runtime comparison.

• latency : Bool

  Whether the latency profile selects the table.

• balanced : Bool

  Whether the balanced profile selects the table.

• throughput : Bool

  Whether the throughput profile selects the table.

• latency_eq : self.latency = tablePreferred format ExecFloat.Backend.Policy.latency name operation

  The stored latency choice agrees with the cost model.

• balanced_eq : self.balanced = tablePreferred format ExecFloat.Backend.Policy.default name operation

  The stored balanced choice agrees with the cost model.

• throughput_eq : self.throughput = tablePreferred format ExecFloat.Backend.Policy.throughput name operation

  The stored throughput choice agrees with the cost model.

@[always_inline]

def FloatLib.Floats.Formats.BinaryInterchange.StaticByte.Plans.BuiltinSelection.balancedAndThroughput {format : FloatFormat} {name : String} {operation : ExecFloat.Backend.Operation} (latency_eq : false = tablePreferred format ExecFloat.Backend.Policy.latency name operation) (balanced_eq : true = tablePreferred format ExecFloat.Backend.Policy.default name operation) (throughput_eq : true = tablePreferred format ExecFloat.Backend.Policy.throughput name operation) : BuiltinSelection format name operation

The latency profile rejects a table accepted by balanced and throughput planning.

@[always_inline]

def FloatLib.Floats.Formats.BinaryInterchange.StaticByte.Plans.BuiltinSelection.throughputOnly {format : FloatFormat} {name : String} {operation : ExecFloat.Backend.Operation} (latency_eq : false = tablePreferred format ExecFloat.Backend.Policy.latency name operation) (balanced_eq : false = tablePreferred format ExecFloat.Backend.Policy.default name operation) (throughput_eq : true = tablePreferred format ExecFloat.Backend.Policy.throughput name operation) : BuiltinSelection format name operation

Among the built-in profiles, only throughput selects this table.

@[always_inline]

def FloatLib.Floats.Formats.BinaryInterchange.StaticByte.Plans.BuiltinSelection.select {format : FloatFormat} {name : String} {operation : ExecFloat.Backend.Operation} (selection : BuiltinSelection format name operation) : ExecFloat.Backend.PolicyProfile → Bool

Choose a table from a statically recognizable profile or evaluate an application-defined policy.

@[always_inline]

def FloatLib.Floats.Formats.BinaryInterchange.StaticByte.Plans.executeBinary {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) (left right : ExecFloat F) : ExecFloat F

Execute the supplied binary table kernel or baseline according to the planning profile.

@[always_inline]

def FloatLib.Floats.Formats.BinaryInterchange.StaticByte.Plans.executeUnary {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) (value : ExecFloat F) : ExecFloat F

Execute the supplied unary table kernel or baseline according to the planning profile.

@[always_inline]

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

Execute the supplied ternary table kernel or baseline according to the planning profile.