First-order runtime dispatch for byte-sized posits

Byte-sized posits have exhaustive tables, direct packed-word arithmetic, width-generic dyadic arithmetic, and the reference specification. The general planner stores functions in candidate records, but projecting the winner through that representation leaves an indirect closure call in otherwise monomorphic UInt8 arithmetic.

This module runs the same deterministic comparison over a compact tag and matches the result to a named first-order kernel. Closed public formats hoist the tag and lazy-table resource as static values, preserving shared memoization without closure dispatch. Correctness and planner-agreement proofs live in ByteDispatch.Proof.

inductive FloatLib.Floats.Formats.Posit.Configured.Plan.ByteDispatch.Choice : Type

The four certified implementation classes available to every byte-sized posit operation.

• reference : Choice
• table : Choice
• word : Choice
• dyadic : Choice

@[instance_reducible]

instance FloatLib.Floats.Formats.Posit.Configured.Plan.ByteDispatch.instDecidableEqChoice : DecidableEq Choice

@[instance_reducible]

instance FloatLib.Floats.Formats.Posit.Configured.Plan.ByteDispatch.instReprChoice : Repr Choice

def FloatLib.Floats.Formats.Posit.Configured.Plan.ByteDispatch.instReprChoice.repr : Choice → ℕ → Std.Format

@[inline]

def FloatLib.Floats.Formats.Posit.Configured.Plan.ByteDispatch.Choice.estimate (format : Format) (width_le : format.bits ≤ 8) (operation : ExecFloat.Backend.Operation) : Choice → ExecFloat.Backend.Candidate

Planner metadata represented by one byte-kernel tag.

@[inline]

def FloatLib.Floats.Formats.Posit.Configured.Plan.ByteDispatch.Choice.consider (policy : ExecFloat.Backend.Policy) (format : Format) (width_le : format.bits ≤ 8) (operation : ExecFloat.Backend.Operation) (incumbent candidate : Choice) : Choice

Compare two byte-kernel tags using the shared planner ordering.

@[noinline]

def FloatLib.Floats.Formats.Posit.Configured.Plan.ByteDispatch.select (policy : ExecFloat.Backend.Policy) (format : Format) (width_le : format.bits ≤ 8) (operation : ExecFloat.Backend.Operation) : Choice

Select a byte kernel without constructing a list or retaining executable closures.

The order is table, packed word, then width-generic dyadic arithmetic, seeded by the reference baseline. This is the same ordering used by the certified candidate portfolios.

def FloatLib.Floats.Formats.Posit.Configured.Plan.ByteDispatch.estimates (format : Format) (width_le : format.bits ≤ 8) (operation : ExecFloat.Backend.Operation) : ExecFloat.Backend.CandidateSet ExecFloat.Backend.Candidate

Metadata-only candidates corresponding exactly to the tag selector.

@[reducible, inline]

abbrev FloatLib.Floats.Formats.Posit.Configured.Plan.ByteDispatch.ByteFloat (format : Format) (width_le : format.bits ≤ 8) : Type

Configured posit execution using the proved byte-sized storage plan.

Direct operation entry points

@[noinline]

def FloatLib.Floats.Formats.Posit.Configured.Plan.ByteDispatch.addSelected {format : Format} (selection : Choice) (width_le : format.bits ≤ 8) (table : ExecFloat.Backend.TinyTable.CertifiedBinary (ByteTable.encoding format width_le) Model.Spec.add) (left right : ByteFloat format width_le) : ByteFloat format width_le

Execute byte-sized posit addition from a first-order choice tag.

@[always_inline]

def FloatLib.Floats.Formats.Posit.Configured.Plan.ByteDispatch.add {format : Format} (policy : ExecFloat.Backend.Policy) (width_le : format.bits ≤ 8) (left right : ByteFloat format width_le) : ByteFloat format width_le

Execute policy-selected byte-sized posit addition through a first-order kernel.

@[noinline]

def FloatLib.Floats.Formats.Posit.Configured.Plan.ByteDispatch.subSelected {format : Format} (selection : Choice) (width_le : format.bits ≤ 8) (table : ExecFloat.Backend.TinyTable.CertifiedBinary (ByteTable.encoding format width_le) Model.Spec.sub) (left right : ByteFloat format width_le) : ByteFloat format width_le

Execute byte-sized posit subtraction from a first-order choice tag.

@[always_inline]

def FloatLib.Floats.Formats.Posit.Configured.Plan.ByteDispatch.sub {format : Format} (policy : ExecFloat.Backend.Policy) (width_le : format.bits ≤ 8) (left right : ByteFloat format width_le) : ByteFloat format width_le

Execute policy-selected byte-sized posit subtraction through a first-order kernel.

@[noinline]

def FloatLib.Floats.Formats.Posit.Configured.Plan.ByteDispatch.mulSelected {format : Format} (selection : Choice) (width_le : format.bits ≤ 8) (table : ExecFloat.Backend.TinyTable.CertifiedBinary (ByteTable.encoding format width_le) Model.Spec.mul) (left right : ByteFloat format width_le) : ByteFloat format width_le

Execute byte-sized posit multiplication from a first-order choice tag.

@[always_inline]

def FloatLib.Floats.Formats.Posit.Configured.Plan.ByteDispatch.mul {format : Format} (policy : ExecFloat.Backend.Policy) (width_le : format.bits ≤ 8) (left right : ByteFloat format width_le) : ByteFloat format width_le

Execute policy-selected byte-sized posit multiplication through a first-order kernel.

@[noinline]

def FloatLib.Floats.Formats.Posit.Configured.Plan.ByteDispatch.divSelected {format : Format} (selection : Choice) (width_le : format.bits ≤ 8) (table : ExecFloat.Backend.TinyTable.CertifiedBinary (ByteTable.encoding format width_le) Model.Spec.div) (left right : ByteFloat format width_le) : ByteFloat format width_le

Execute byte-sized posit division from a first-order choice tag.

@[always_inline]

def FloatLib.Floats.Formats.Posit.Configured.Plan.ByteDispatch.div {format : Format} (policy : ExecFloat.Backend.Policy) (width_le : format.bits ≤ 8) (left right : ByteFloat format width_le) : ByteFloat format width_le

Execute policy-selected byte-sized posit division through a first-order kernel.

@[noinline]

def FloatLib.Floats.Formats.Posit.Configured.Plan.ByteDispatch.sqrtSelected {format : Format} (selection : Choice) (width_le : format.bits ≤ 8) (table : ExecFloat.Backend.TinyTable.CertifiedUnary (ByteTable.encoding format width_le) Model.Spec.sqrt) (value : ByteFloat format width_le) : ByteFloat format width_le

Execute byte-sized posit square root from a first-order choice tag.

@[always_inline]

def FloatLib.Floats.Formats.Posit.Configured.Plan.ByteDispatch.sqrt {format : Format} (policy : ExecFloat.Backend.Policy) (width_le : format.bits ≤ 8) (value : ByteFloat format width_le) : ByteFloat format width_le

Execute policy-selected byte-sized posit square root through a first-order kernel.

@[noinline]

def FloatLib.Floats.Formats.Posit.Configured.Plan.ByteDispatch.fmaSelected {format : Format} (selection : Choice) (width_le : format.bits ≤ 8) (table : ExecFloat.Backend.TinyTable.CertifiedTernary (ByteTable.encoding format width_le) Model.Spec.fma) (left right addend : ByteFloat format width_le) : ByteFloat format width_le

Execute byte-sized posit FMA from a first-order choice tag.

@[always_inline]

def FloatLib.Floats.Formats.Posit.Configured.Plan.ByteDispatch.fma {format : Format} (policy : ExecFloat.Backend.Policy) (width_le : format.bits ≤ 8) (left right addend : ByteFloat format width_le) : ByteFloat format width_le

Execute policy-selected byte-sized posit FMA through a first-order kernel.