Context
Slot.justifiable_iff (CONT-2, LeanSpec/Forks/Lstar/Slot.lean) proves the characterization: a distance δ is justifiable iff δ ≤ 5 ∨ (∃ k, δ = k*k) ∨ (∃ k, δ = k*(k+1)).
The upstream Python predicate (is_justifiable_after) and our model both decide this via a hand-rolled isqrt loop per call. This sits on the fork-choice hot path (candidate-slot scans).
Proposal
- Define an O(1) decision procedure: compute
i = isqrt δ once, then test i*i = δ ∨ i*(i+1) = δ (the δ ≤ 5 window folds in trivially).
- Prove it equivalent to the spec predicate via
justifiable_iff (the existing isqrt_le / isqrt_lt_succ / isqrt_eq lemmas should discharge most of it).
- Optionally: an incremental variant for monotone δ scans, also proven equivalent.
- Feed the verified formulation back upstream (leanEthereum/leanSpec) as a spec simplification, in the spec-feedback.md format (theorem → spec-change proposal).
Why
This is the "verified refinement" pattern: the reference spec stays readable, clients adopt the optimized decision procedure backed by a machine-checked equivalence theorem instead of re-deriving it independently.
Estimated scope
Small — builds directly on existing proof assets (justifiable_iff, isqrt lemmas). Days, not weeks.
Context
Slot.justifiable_iff(CONT-2,LeanSpec/Forks/Lstar/Slot.lean) proves the characterization: a distance δ is justifiable iffδ ≤ 5 ∨ (∃ k, δ = k*k) ∨ (∃ k, δ = k*(k+1)).The upstream Python predicate (
is_justifiable_after) and our model both decide this via a hand-rolledisqrtloop per call. This sits on the fork-choice hot path (candidate-slot scans).Proposal
i = isqrt δonce, then testi*i = δ ∨ i*(i+1) = δ(theδ ≤ 5window folds in trivially).justifiable_iff(the existingisqrt_le/isqrt_lt_succ/isqrt_eqlemmas should discharge most of it).Why
This is the "verified refinement" pattern: the reference spec stays readable, clients adopt the optimized decision procedure backed by a machine-checked equivalence theorem instead of re-deriving it independently.
Estimated scope
Small — builds directly on existing proof assets (
justifiable_iff, isqrt lemmas). Days, not weeks.