Correctness of first-order byte-sized posit dispatch

The tagged selector agrees with the shared planner metadata, and every named execution branch implements the independent configured specification. These results ensure that removing closure dispatch changes performance only, never arithmetic semantics or inspection metadata.

theorem FloatLib.Floats.Formats.Posit.Configured.Plan.ByteDispatch.select_estimate (policy : ExecFloat.Backend.Policy) (format : Format) (width_le : format.bits ≤ 8) (operation : ExecFloat.Backend.Operation) : Choice.estimate format width_le operation (select policy format width_le operation) = ExecFloat.Backend.selectCandidate policy (estimates format width_le operation)

Tagged selection uses the same candidate comparison as the shared metadata planner.

Agreement with the public certified portfolios

theorem FloatLib.Floats.Formats.Posit.Configured.Plan.ByteDispatch.addByteCandidates_estimates (format : Format) (width_le : format.bits ≤ 8) : (addByteCandidates format width_le).estimates = estimates format width_le ExecFloat.Backend.Operation.add

Addition exposes exactly the metadata consumed by its first-order selector.

theorem FloatLib.Floats.Formats.Posit.Configured.Plan.ByteDispatch.subByteCandidates_estimates (format : Format) (width_le : format.bits ≤ 8) : (subByteCandidates format width_le).estimates = estimates format width_le ExecFloat.Backend.Operation.sub

Subtraction exposes exactly the metadata consumed by its first-order selector.

theorem FloatLib.Floats.Formats.Posit.Configured.Plan.ByteDispatch.mulByteCandidates_estimates (format : Format) (width_le : format.bits ≤ 8) : (mulByteCandidates format width_le).estimates = estimates format width_le ExecFloat.Backend.Operation.mul

Multiplication exposes exactly the metadata consumed by its first-order selector.

theorem FloatLib.Floats.Formats.Posit.Configured.Plan.ByteDispatch.divByteCandidates_estimates (format : Format) (width_le : format.bits ≤ 8) : (divByteCandidates format width_le).estimates = estimates format width_le ExecFloat.Backend.Operation.div

Division exposes exactly the metadata consumed by its first-order selector.

theorem FloatLib.Floats.Formats.Posit.Configured.Plan.ByteDispatch.sqrtByteCandidates_estimates (format : Format) (width_le : format.bits ≤ 8) : (sqrtByteCandidates format width_le).estimates = estimates format width_le ExecFloat.Backend.Operation.sqrt

Square root exposes exactly the metadata consumed by its first-order selector.

theorem FloatLib.Floats.Formats.Posit.Configured.Plan.ByteDispatch.fmaByteCandidates_estimates (format : Format) (width_le : format.bits ≤ 8) : (fmaByteCandidates format width_le).estimates = estimates format width_le ExecFloat.Backend.Operation.fma

FMA exposes exactly the metadata consumed by its first-order selector.

theorem FloatLib.Floats.Formats.Posit.Configured.Plan.ByteDispatch.select_add_estimate (policy : ExecFloat.Backend.Policy) (format : Format) (width_le : format.bits ≤ 8) : Choice.estimate format width_le ExecFloat.Backend.Operation.add (select policy format width_le ExecFloat.Backend.Operation.add) = ExecFloat.Backend.selectCandidate policy (addByteCandidates format width_le).estimates

Executed and reported addition selection agree.

theorem FloatLib.Floats.Formats.Posit.Configured.Plan.ByteDispatch.select_sub_estimate (policy : ExecFloat.Backend.Policy) (format : Format) (width_le : format.bits ≤ 8) : Choice.estimate format width_le ExecFloat.Backend.Operation.sub (select policy format width_le ExecFloat.Backend.Operation.sub) = ExecFloat.Backend.selectCandidate policy (subByteCandidates format width_le).estimates

Executed and reported subtraction selection agree.

theorem FloatLib.Floats.Formats.Posit.Configured.Plan.ByteDispatch.select_mul_estimate (policy : ExecFloat.Backend.Policy) (format : Format) (width_le : format.bits ≤ 8) : Choice.estimate format width_le ExecFloat.Backend.Operation.mul (select policy format width_le ExecFloat.Backend.Operation.mul) = ExecFloat.Backend.selectCandidate policy (mulByteCandidates format width_le).estimates

Executed and reported multiplication selection agree.

theorem FloatLib.Floats.Formats.Posit.Configured.Plan.ByteDispatch.select_div_estimate (policy : ExecFloat.Backend.Policy) (format : Format) (width_le : format.bits ≤ 8) : Choice.estimate format width_le ExecFloat.Backend.Operation.div (select policy format width_le ExecFloat.Backend.Operation.div) = ExecFloat.Backend.selectCandidate policy (divByteCandidates format width_le).estimates

Executed and reported division selection agree.

theorem FloatLib.Floats.Formats.Posit.Configured.Plan.ByteDispatch.select_sqrt_estimate (policy : ExecFloat.Backend.Policy) (format : Format) (width_le : format.bits ≤ 8) : Choice.estimate format width_le ExecFloat.Backend.Operation.sqrt (select policy format width_le ExecFloat.Backend.Operation.sqrt) = ExecFloat.Backend.selectCandidate policy (sqrtByteCandidates format width_le).estimates

Executed and reported square-root selection agree.

theorem FloatLib.Floats.Formats.Posit.Configured.Plan.ByteDispatch.select_fma_estimate (policy : ExecFloat.Backend.Policy) (format : Format) (width_le : format.bits ≤ 8) : Choice.estimate format width_le ExecFloat.Backend.Operation.fma (select policy format width_le ExecFloat.Backend.Operation.fma) = ExecFloat.Backend.selectCandidate policy (fmaByteCandidates format width_le).estimates

Executed and reported fused-multiply-add selection agree.

Arithmetic refinement

theorem FloatLib.Floats.Formats.Posit.Configured.Plan.ByteDispatch.addSelected_eq_spec {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) : addSelected selection width_le table left right = Spec.add left right

A byte-addition choice cannot change arithmetic semantics.

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

First-order byte addition refines the configured specification for every policy.

theorem FloatLib.Floats.Formats.Posit.Configured.Plan.ByteDispatch.subSelected_eq_spec {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) : subSelected selection width_le table left right = Spec.sub left right

A byte-subtraction choice cannot change arithmetic semantics.

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

First-order byte subtraction refines the configured specification for every policy.

theorem FloatLib.Floats.Formats.Posit.Configured.Plan.ByteDispatch.mulSelected_eq_spec {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) : mulSelected selection width_le table left right = Spec.mul left right

A byte-multiplication choice cannot change arithmetic semantics.

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

First-order byte multiplication refines the configured specification for every policy.

theorem FloatLib.Floats.Formats.Posit.Configured.Plan.ByteDispatch.divSelected_eq_spec {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) : divSelected selection width_le table left right = Spec.div left right

A byte-division choice cannot change arithmetic semantics.

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

First-order byte division refines the configured specification for every policy.

theorem FloatLib.Floats.Formats.Posit.Configured.Plan.ByteDispatch.sqrtSelected_eq_spec {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) : sqrtSelected selection width_le table value = Spec.sqrt value

A byte-square-root choice cannot change arithmetic semantics.

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

First-order byte square root refines the configured specification for every policy.

theorem FloatLib.Floats.Formats.Posit.Configured.Plan.ByteDispatch.fmaSelected_eq_spec {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) : fmaSelected selection width_le table left right addend = Spec.fma left right addend

A byte-FMA choice cannot change arithmetic semantics.

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

First-order byte FMA refines the configured specification for every policy.

Function equalities used by capability construction

theorem FloatLib.Floats.Formats.Posit.Configured.Plan.ByteDispatch.add_fun_eq_spec {format : Format} (policy : ExecFloat.Backend.Policy) (width_le : format.bits ≤ 8) : add policy width_le = Spec.add

Policy-selected byte addition equals the configured specification as a function.

theorem FloatLib.Floats.Formats.Posit.Configured.Plan.ByteDispatch.sub_fun_eq_spec {format : Format} (policy : ExecFloat.Backend.Policy) (width_le : format.bits ≤ 8) : sub policy width_le = Spec.sub

Policy-selected byte subtraction equals the configured specification as a function.

theorem FloatLib.Floats.Formats.Posit.Configured.Plan.ByteDispatch.mul_fun_eq_spec {format : Format} (policy : ExecFloat.Backend.Policy) (width_le : format.bits ≤ 8) : mul policy width_le = Spec.mul

Policy-selected byte multiplication equals the configured specification as a function.

theorem FloatLib.Floats.Formats.Posit.Configured.Plan.ByteDispatch.div_fun_eq_spec {format : Format} (policy : ExecFloat.Backend.Policy) (width_le : format.bits ≤ 8) : div policy width_le = Spec.div

Policy-selected byte division equals the configured specification as a function.

theorem FloatLib.Floats.Formats.Posit.Configured.Plan.ByteDispatch.sqrt_fun_eq_spec {format : Format} (policy : ExecFloat.Backend.Policy) (width_le : format.bits ≤ 8) : sqrt policy width_le = Spec.sqrt

Policy-selected byte square root equals the configured specification as a function.

theorem FloatLib.Floats.Formats.Posit.Configured.Plan.ByteDispatch.fma_fun_eq_spec {format : Format} (policy : ExecFloat.Backend.Policy) (width_le : format.bits ≤ 8) : fma policy width_le = Spec.fma

Policy-selected byte fused multiply-add equals the configured specification as a function.