Certified backend selection

Certified spec packages an executable kernel with both an engineering estimate and an equation showing that it implements spec. The operation type is abstract, so the same mechanism handles unary, binary, ternary, stateful, and family-specific kernels.

Selection is a deterministic fold over already certified alternatives and a mandatory exact baseline. The cost heuristic decides only which implementation to run; it never participates in the arithmetic proof. Erasing proofs yields the same estimate selected by inspection tools, so the reported plan cannot silently diverge from execution.

structure FloatLib.Floats.ExecFloat.Backend.Certified {α : Type u} (spec : α) : Type u

Executable kernel bundled with a static estimate and a refinement certificate.

The operation type α may be unary, binary, ternary, stateful, or family-specific. This keeps the planning mechanism independent of floating-point layout and of the six core arithmetic operations.

• estimate : Candidate

  Static cost and resource estimate attached to the executable kernel.

• run : α

  Executable implementation offered to the selector.

• run_eq_spec : self.run = spec

  The executable kernel equals the supplied specification.

def FloatLib.Floats.ExecFloat.Backend.Certified.reference {α : Type u} (estimate : Candidate) (spec : α) : Certified spec

Use the specification itself as the complete executable baseline.

The baseline runs spec directly. Specialized candidates can refine the same specification and compete with the supplied estimate.

def FloatLib.Floats.ExecFloat.Backend.Certified.nullary {α : Type u} (estimate : Candidate) (spec run : α) (run_eq_spec : run = spec) : Certified spec

Construct a certified nullary result from an ordinary equality.

def FloatLib.Floats.ExecFloat.Backend.Certified.unary {α β : Type u} (estimate : Candidate) (spec run : α → β) (run_eq_spec : ∀ (value : α), run value = spec value) : Certified spec

Construct a certified unary kernel from its pointwise refinement theorem.

def FloatLib.Floats.ExecFloat.Backend.Certified.binary {α β γ : Type u} (estimate : Candidate) (spec run : α → β → γ) (run_eq_spec : ∀ (left : α) (right : β), run left right = spec left right) : Certified spec

Construct a certified binary kernel from its pointwise refinement theorem.

def FloatLib.Floats.ExecFloat.Backend.Certified.ternary {α β γ δ : Type u} (estimate : Candidate) (spec run : α → β → γ → δ) (run_eq_spec : ∀ (left : α) (right : β) (addend : γ), run left right addend = spec left right addend) : Certified spec

Construct a certified ternary kernel from its pointwise refinement theorem.

@[inline]

def FloatLib.Floats.ExecFloat.Backend.CandidateSet.withReference {α : Type u} (estimate : Candidate) (spec : α) (alternatives : List (Certified spec) := []) : CandidateSet (Certified spec)

Build a candidate portfolio whose mandatory baseline executes the specification itself.

This is the uniform shape used by exact executable specifications: specialized alternatives are considered in the supplied order, and the reference operation remains the final total baseline.

def FloatLib.Floats.ExecFloat.Backend.CandidateSet.estimates {α : Type u} {spec : α} (candidates : CandidateSet (Certified spec)) : CandidateSet Candidate

Erase executable functions and proofs, retaining the inspectable cost model.

@[inline]

def FloatLib.Floats.ExecFloat.Backend.considerCertified {α : Type u} {spec : α} (policy : Policy) (incumbent candidate : Certified spec) : Certified spec

Compare one certified candidate while retaining its executable refinement theorem.

@[simp]

theorem FloatLib.Floats.ExecFloat.Backend.considerCertified_estimate {α : Type u} {spec : α} (policy : Policy) (incumbent candidate : Certified spec) : (considerCertified policy incumbent candidate).estimate = consider policy incumbent.estimate candidate.estimate

Erasing a certified comparison to its estimate gives the metadata-only comparison.

Keeping this correspondence explicit prevents inspection tools from reporting a different plan from the executable dispatcher.

@[inline]

def FloatLib.Floats.ExecFloat.Backend.selectCertified {α : Type u} {spec : α} (policy : Policy) (candidates : CandidateSet (Certified spec)) : Certified spec

Select an executable certified kernel by the same fold as metadata-only selection.

No correctness proof is reconstructed from the heuristic: whichever branch is selected already contains its own refinement theorem.

theorem FloatLib.Floats.ExecFloat.Backend.selectCertified_estimate {α : Type u} {spec : α} (policy : Policy) (candidates : CandidateSet (Certified spec)) : (selectCertified policy candidates).estimate = selectCandidate policy candidates.estimates

Executable selection and metadata-only selection choose the same estimate.

theorem FloatLib.Floats.ExecFloat.Backend.selectCertified_run_eq_spec {α : Type u} {spec : α} (policy : Policy) (candidates : CandidateSet (Certified spec)) : (selectCertified policy candidates).run = spec

Selection cannot invalidate refinement because every eligible branch is certified.

theorem FloatLib.Floats.ExecFloat.Backend.firstOrder_eq_selected {α : Type u} {spec : α} (policy : Policy) (candidates : CandidateSet (Certified spec)) (execute : α) (execute_eq_spec : execute = spec) : execute = (selectCertified policy candidates).run

A direct entry point equal to the specification agrees with the selected certified kernel.

The operation type is arbitrary: no format, arity, or typeclass policy is required. Returning an equality lets callers keep a named executable entry point without constructing a capability through a helper that might retain a runtime record or an indirect call.

theorem FloatLib.Floats.ExecFloat.Backend.foldl_considerCertified_eq_of_not_better {α : Type u} {spec : α} (policy : Policy) (incumbent : Certified spec) (rest : List (Certified spec)) (hrest : ∀ (other : Certified spec), other ∈ rest → Candidate.better policy other.estimate incumbent.estimate = false) : List.foldl (considerCertified policy) incumbent rest = incumbent

A fold that never finds a better candidate returns its incumbent.

theorem FloatLib.Floats.ExecFloat.Backend.selectCertified_cons_of_dominant {α : Type u} {spec : α} (policy : Policy) (dominant : Certified spec) (rest : List (Certified spec)) (baseline : Certified spec) (hadmissible : Candidate.admissible policy dominant.estimate = true) (hbaseline : Candidate.better policy dominant.estimate baseline.estimate = true) (hrest : ∀ (other : Certified spec), other ∈ rest → Candidate.better policy other.estimate dominant.estimate = false) : selectCertified policy { alternatives := dominant :: rest, baseline := baseline } = dominant

An admissible head alternative that beats the baseline and is beaten by no later alternative is the selected certificate, under the given policy.

This is the lemma a statically specialized capability uses to name the planner's winner directly while remaining provably consistent with the advertised candidate set.