From 8890beb15987fb8570a60a9436b51ac39c2c0f5f Mon Sep 17 00:00:00 2001 From: mrwulf Date: Thu, 23 Jul 2026 11:07:03 +0200 Subject: [PATCH] meta-drill over the previous drill: one false claim caught, substance held 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 --- verification/drafts/ChainSpec.lean | 5 +++++ 1 file changed, 5 insertions(+) diff --git a/verification/drafts/ChainSpec.lean b/verification/drafts/ChainSpec.lean index 631a1b6..5494c1e 100644 --- a/verification/drafts/ChainSpec.lean +++ b/verification/drafts/ChainSpec.lean @@ -23,6 +23,11 @@ dalek loop-spec pattern), which sidesteps the raw match/bind plumbing. Nothing here is claimed proven: this file carries sorries and lives in drafts/, never in Proofs/ or check.sh. + + RECORD NOTE: commit a2d8e5f's message body lost one backticked fragment + to shell command-substitution (it reads "the let-pair so"); the intended + text was: the let-pair (o,iter1) := (some start, {start:=w,end:=stop}). + This header is the authoritative technical record. -/ import SlhVerify.Funs open Aeneas Aeneas.Std Result ControlFlow