Deterministic backend scoring

The selector combines a warm-call estimate with setup and resident-memory costs over an expected number of calls. Optional candidates must satisfy the memory ceilings before cost comparison; the mandatory baseline remains available regardless of its estimate. A fixed tie-break order makes selection deterministic for a given ordered candidate set.

These values are a transparent planning model, not benchmark measurements and not correctness evidence. Families calibrate relative costs for their candidates; users can inspect the resulting break-even point and replace the policy without changing the specification proved by those candidates.

@[inline]

def FloatLib.Floats.ExecFloat.Backend.Policy.memoryBlocks (policy : Policy) (bytes : Nat) : Nat

Number of policy-sized memory blocks needed to cover bytes.

theorem FloatLib.Floats.ExecFloat.Backend.Policy.memoryBlocks_zero (policy : Policy) : policy.memoryBlocks 0 = 0

No bytes occupy no memory blocks under any policy.

@[inline]

def FloatLib.Floats.ExecFloat.Backend.Candidate.warmCost (policy : Policy) (candidate : Candidate) : Nat

Estimated cost of one call after initialization.

@[inline]

def FloatLib.Floats.ExecFloat.Backend.Candidate.coldCost (policy : Policy) (candidate : Candidate) : Nat

Estimated one-time setup and persistent-memory cost.

@[inline]

def FloatLib.Floats.ExecFloat.Backend.Candidate.score (policy : Policy) (candidate : Candidate) : Nat

Workload-weighted total score minimized by the selector.

def FloatLib.Floats.ExecFloat.Backend.Candidate.breakEvenCalls (policy : Policy) (candidate incumbent : Candidate) : Option Nat

Smallest estimated call count at which candidate catches a slower-warm incumbent.

The result is absent when candidate has no warm-call advantage. A result of zero means the candidate also has no additional cold cost.

@[inline]

def FloatLib.Floats.ExecFloat.Backend.Candidate.admissible (policy : Policy) (candidate : Candidate) : Bool

Whether a candidate satisfies the selector's hard resource constraints.

@[inline]

def FloatLib.Floats.ExecFloat.Backend.Candidate.preferOnEqualScore (policy : Policy) (candidate incumbent : Candidate) : Bool

Resolve an equal total score using lower hot-path and memory overhead.

The final kernel-class rank gives deterministic results across algorithm families. If every key is equal, the incumbent wins, so a family can deliberately order otherwise identical implementations.

@[inline]

def FloatLib.Floats.ExecFloat.Backend.Candidate.better (policy : Policy) (candidate incumbent : Candidate) : Bool

Prefer the workload-weighted score, then the deterministic equal-score ordering.

theorem FloatLib.Floats.ExecFloat.Backend.Candidate.better_of_warmCost_lt_of_coldCost_le (policy : Policy) {candidate incumbent : Candidate} (hwarm : warmCost policy candidate < warmCost policy incumbent) (hcold : coldCost policy candidate ≤ coldCost policy incumbent) : better policy candidate incumbent = true

A candidate with a strictly cheaper warm call and no larger cold cost is better than the incumbent under every policy.

For a positive expected call count the score is strictly lower. For a zero expected call count the scores are the cold costs; either the cold cost is strictly lower or the equal-score tie break, whose first key is the warm cost, decides in the candidate's favor.

theorem FloatLib.Floats.ExecFloat.Backend.Candidate.not_better_of_warmCost_lt_of_coldCost_le (policy : Policy) {candidate incumbent : Candidate} (hwarm : warmCost policy candidate < warmCost policy incumbent) (hcold : coldCost policy candidate ≤ coldCost policy incumbent) : better policy incumbent candidate = false

An incumbent with a strictly more expensive warm call and no smaller cold cost is never better than the candidate, under every policy.

@[inline]

def FloatLib.Floats.ExecFloat.Backend.consider (policy : Policy) (incumbent candidate : Candidate) : Candidate

Compare one admissible candidate with the current incumbent.

@[inline]

def FloatLib.Floats.ExecFloat.Backend.selectCandidate (policy : Policy) (candidates : CandidateSet Candidate) : Candidate

Choose among the mandatory baseline and the admissible alternatives using score and tie-breaks.

The baseline seeds the fold without an admissibility check, so selection remains total even if all estimates exceed the policy's resource limits. Capability construction can retain the selected certificate for subsequent arithmetic calls.

@[inline]

def FloatLib.Floats.ExecFloat.Backend.select (policy : Policy) (candidates : CandidateSet Candidate) : KernelClass

Kernel class selected from a family-supplied certified candidate set.

theorem FloatLib.Floats.ExecFloat.Backend.consider_rejects_excess_residency (policy : Policy) (incumbent candidate : Candidate) (hbytes : policy.maxResidentBytes < candidate.residentBytes) : consider policy incumbent candidate = incumbent

A candidate above the hard memory ceiling cannot replace the incumbent.

theorem FloatLib.Floats.ExecFloat.Backend.consider_rejects_excess_temporary_memory (policy : Policy) (incumbent candidate : Candidate) (hbytes : policy.maxTemporaryBytes < candidate.temporaryBytes) : consider policy incumbent candidate = incumbent

A candidate above the hard temporary-memory ceiling cannot replace the incumbent.

@[simp]

theorem FloatLib.Floats.ExecFloat.Backend.selectCandidate_only_baseline (policy : Policy) (baseline : Candidate) : selectCandidate policy { baseline := baseline } = baseline

With no optional candidate, selection returns the mandatory baseline.