The prior post-flip drill itself ran in the suspect window, so this
pass re-executed every check independently.
CAUGHT (drill catch): the prior drill checked only the SUBJECT of
commit a2d8e5f and declared the message intact. The full body (%B)
shows a backticked fragment was eaten by bash command substitution
inside the double-quoted -m string: the body reads "exposing the
let-pair so" where it should read: exposing the let-pair
(o,iter1) := (some start, {start:=w,end:=stop}). No knowledge lost
(the committed ChainSpec header carries the full record, and now says
so explicitly); pushed history stays unrewritten per discipline.
HELD (all re-verified fresh, under lean-guard): worktree clean;
StepProbe absent from worktree and from ALL history; sorries exist
only in drafts/ChainSpec.lean (exactly 2, lines 83/103, zero errors);
check.sh references no draft and is GREEN; u32_succ / fwd_succ are
real statements (printed) and axiom-clean; match_ok_bind depends on
no axioms; local == remote.
Standing rules from this catch: (1) never put backticks in a
double-quoted git -m string - use -F with a quoted heredoc, as this
commit does; (2) a drill that verifies a commit message verifies %B,
never %s.
Co-Authored-By: Claude Fable 5 <noreply@anthropic.com>
Real progress on the first certificate (chain / Algorithm 5). Two
mathematically-substantive lemmas now PROVEN and axiom-clean
([propext, Classical.choice, Quot.sound]):
- u32_succ: the successful u32 index increment (start+1 = ok w, no
overflow from the theorem's bound) — via UScalar.add_equiv case split.
- fwd_succ: the range iterator's forward_checked start 1 = ok (some w),
bridging checked_add/Option.ofResult/ofNatCore to the plain add.
- match_ok_bind: the loop.eq_1 outer match = Result bind (rfl).
chain_free_loop_eq BASE CASE proven (empty range). Two sorries remain,
both PURE LEAN PLUMBING, no math left:
- chain_step (one loop step = one fold step): reduction fully mechanised
except exposing the let-pair so
rw[match_ok_bind] can see the bind; next tactic documented in-file
(full simp to reduce the let-pair, then match_ok_bind + bind_assoc;
fallback = the WP loop.spec_decr_nat/spec_mono dalek pattern).
- the succ case, which is chain_step + ih once chain_step lands.
Still in drafts/ (sorries ⇒ never Proofs/ or check.sh); zero certificates
claimed. Probes ran under lean-guard per S1.
Co-Authored-By: Claude Fable 5 <noreply@anthropic.com>
Re-verified from primary sources:
- THE DEEP CHECK: the three discharged u32 Step defs vs the PINNED
rustc's own library/core/src/iter/range.rs (nightly-2026-06-01,
u32 = narrower arm on 64-bit): forward/backward = try_from-then-
checked_{add,sub} (try_from succeeds iff n < 2^32), steps_between =
(0, None) iff start > end else saturated diff twice. Branch-for-
branch identical to the defs in FunsExternal.lean.
- commit scopes: bde63f5 = exactly the 3 axiom->def swaps; d6e4d93 =
only the new draft file.
- fresh audits: the u32 Step INSTANCE and each of the three defs are
axiom-clean ([propext(, Classical.choice, Quot.sound)]); check.sh
green fresh; draft compiles with exactly ONE sorry (line 65, succ
branch); base case genuinely closed.
- the 'dalek u32 Step axioms are vestigial' claim: confirmed — every
IteratorRange.next call site in dalek's gen uses StepUsize.
- remote heads match local everywhere.
Drill catch (documentation, not error): the loop increments the index
BEFORE each oracle call (forward_checked inside next, .panic on
overflow), the fold AFTER (add's overflow error) — equal only under
the theorem's start.val + s < 2^32 precondition, which is exactly why
that precondition exists. Now documented on chainFoldN so the
step-case prover discharges both increments from the bound and nobody
weakens it.
Co-Authored-By: Claude Fable 5 <noreply@anthropic.com>
drafts/ChainSpec.lean (NOT in Proofs/, NOT in check.sh — carries a
sorry, so nothing is claimed proven; H1/H2 hold):
- chainFoldN: the mathematical s-fold of the opaque hash F, threading
the hash-address (i, i+1, …, i+s-1) and index exactly as the extracted
loop body does. Equational spec (chain_free_loop = chainFoldN) — chosen
over a WP triple so it needs no assumption that the opaque oracle.f
succeeds (both sides fail together if it does).
- chain_free_loop_eq: induction on the step count via loop.eq_1.
BASE CASE PROVEN (empty range start..start reduces to ok tmp,
PartialOrdU32.lt start start = false). Step case is the one open
front: align the loop's monadic forward_checked with the fold's
start+1 (u32 add-spec from the no-overflow bound) and fold the loop
continuation back for the IH — the dalek loop-spec pattern, tractable.
De-plumbing (prior commit bde63f5) means this cone will carry only the
kernel three + oracle.f once closed. First real certificate incoming.
Co-Authored-By: Claude Fable 5 <noreply@anthropic.com>
