fips205.wots_loop1_eq (Proofs/WotsSpec.lean): the extracted WOTS+ chain
loop wots_pk_from_sig_free_loop1 = the explicit fold that, at each index
i in [0, LEN), sets the chain address to i and runs chain_free on sig[i]
starting at digit msg[i] for W-1-msg[i] steps, writing tmp[i]. This is
the layer above chain: it CONSUMES chain_free and machine-checks that the
LEN chains are run with the right start indices, step counts, and output
slots — the WOTS+ verification recomputation.
Cone stays clean: [propext, Classical.choice, Quot.sound,
verify_mono.oracle.f] — the loop uses the REAL Aeneas StepUsize (usize
range, no plumbing axiom) and calls chain_free/index_usize/update, all
real; the try_from / Take-iterator / base_2b input-prep plumbing lives in
the enclosing wots_pk_from_sig_free, NOT in this loop.
Proof mirrors ChainSpec, reusing the generic loop_unfold_bind: usize_succ
+ fwd_succ_usize + hnext_usize (StepUsize iterator step), hbody1 (loop
body as clean do-block), wots_loop1_step (one loop step = one fold step),
wots_loop1_eq (induction, IH under the fatter binds via bind_congr x8).
No sorry; check.sh green over BOTH certificates with the axiom audit.
The chain-proof patterns transferred one-for-one to the next layer.
Co-Authored-By: Claude Fable 5 <noreply@anthropic.com>
The window under audit claimed the campaign's first certificate, so this
drill was maximally adversarial. Everything of substance HELD:
- three-way model fidelity EXACT: extracted chain_free_loop.body ==
chainFoldN step == the Rust origin, operation-for-operation including
address threading
- button green fresh; axiom sweep over ALL 8 declarations minimal
(pure lemmas = kernel-3; oracle-touching = kernel-3 + oracle.f only)
- non-vacuity PROVEN: the concrete 1-step consequence (one address-set +
one hash call) derives from the certificate by rfl
- commit body of cfd50bb intact (the one flagged fragment was a bad
drill grep pattern, not an artifact); worktree clean; heads synced
NEW, from the drill (R3-5 tradition): verification/check-selftest.sh -
permanent adversarial self-test of the check.sh gates. Attack 1 (dead
Proofs file) and attack 2 (certificate with a smuggled axiom) must both
make check.sh fail; both verified rejected, selftest green, self-cleaning.
An audit that cannot fail is theater; this one demonstrably can.
Two notes for the record: (a) bind_congr is the generic Bind-class
congruence from core/Mathlib, not Aeneas.Std.Primitives (memory
corrected); (b) the certificate covers chain_free_loop - the thin
chain_free wrapper (bound computation + massert + clone) gets its
trivial composition lemma in the wots layer, where it is consumed.
Co-Authored-By: Claude Fable 5 <noreply@anthropic.com>
verification/check.sh is green (exit 0): 3 phases — model compiles,
proofs compile, axiom audit passes.
fips205.chain_free_loop_eq (Proofs/ChainSpec.lean): the extracted
chain_free loop = the explicit s-fold hash chain, hash address i..i+s-1.
Machine-checked, for the deployed monomorphic SHA2-128s verify path, that
there is no off-by-one loop bound, no wrong address field, no wrong
threading. #print axioms cone = EXACTLY [propext, Classical.choice,
Quot.sound, verify_mono.oracle.f] — kernel three + the one hash oracle,
zero transpiler plumbing (the u32 Step machinery was discharged earlier
with real defs). check.sh Phase 3 enforces cone subset of kernel-3 + the
five SHA-2 oracles, failing the build otherwise.
Proof structure (all lemmas axiom-clean, no sorry): u32_succ + fwd_succ
(the monadic u32 increment, checked against pinned rustc semantics);
loop_unfold_bind (one turn of the Aeneas loop fixpoint, closed by cases
because a hand-written match compiles to a non-defeq matcher);
hnext + hbody (iterator step and loop body as clean equations);
chain_step (one loop step = one fold step); chain_free_loop_eq
(induction, IH threaded under the opaque binds with bind_congr).
Both prior sorries closed. Certificate lives in Proofs/ (not drafts/);
the WIP draft is retired. check.sh committed as -F stdin per the
no-backticks-in-commit-messages rule.
Co-Authored-By: Claude Fable 5 <noreply@anthropic.com>
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>
The verify cone iterates u32 ranges (for j in i..i+s). Aeneas.Std ships
a real Step instance only for usize (StepUsize), so u32 ranges extracted
as three opaque axioms (forward_checked / backward_checked /
steps_between) — which would poison every loop-bearing cone, i.e. chain
and everything above it.
Discharged in the hand-written external file (H4-sanctioned) with
FAITHFUL real definitions mirroring Rust's impl Step for u32
(core/src/iter/range.rs) and Aeneas.Std's StepUsize: forward/backward via
u32::try_from(n)-then-checked_{add,sub}, steps_between = saturating
difference. Verified in isolation (axiom-clean) and in place:
#print axioms on the u32 Step instance now reports exactly
[propext, Classical.choice, Quot.sound]. Model still compiles.
These are ordinary loop control, NOT the deployed hash boundary — the
five oracle axioms remain the only cryptographic externals.
Co-Authored-By: Claude Fable 5 <noreply@anthropic.com>
The skeleton-era docs said 'six hash oracles' including prf — written
before the cone analysis showed prf/prf_msg are sign-side only. The
extracted model and FunsExternal carry exactly FIVE oracle axioms
(h_msg, f, h, t_l, t_len); the documented boundary now matches the
real one in README, TRUSTED-BASE, and extract.sh. Caught by the
post-flip drill's cross-consistency pass.
Co-Authored-By: Claude Fable 5 <noreply@anthropic.com>
Full re-verification of the phase-1 window from primary sources, per the
standing drill after a model flip. Results:
- diff surface since snapshot 5dca0db: 414 additive lines only; every
generic algorithm file byte-untouched
- mechanical normalized diff: all 6 mono functions byte-identical to
their origins under ONLY the documented transforms (oracle renames,
call renames, single-slice M', is_err idiom)
- oracle wiring == deployed 128s HASHERS instance incl. the t_len: t_l
alias; constants == lib.rs 128s module; exactly 5 oracles in the cone
- FULL upstream suite in release WITH the patches: 13 lib + 3 ACVP KAT
integration + 12 py_vectors + 37 doc-tests, zero failures (stronger
regression evidence than the original window collected)
- extraction reproducible: regen byte-identical to committed gen/
- check.sh re-run green; commit-message numerics re-verified (62 defs,
0 sorry, 5+13 axioms, apex 63/30); remote heads match local
- hand externals proven to be header + template body exactly
One catch, fixed here: extract.sh still carried the pre-phase-1
'expect non-green' wording.
Co-Authored-By: Claude Fable 5 <noreply@anthropic.com>
The gate-0 fn-pointer blocker is cleared. This commits the phase-1
deliverable:
- verification/extract.sh: re-pointed at the monomorphic root
crate::verify_mono::slh_verify_128s with crate::verify_mono::oracle as
the opaque SHA-2 boundary (against fips205-source @ 2d89ee3).
- verification/gen/SlhVerify: the extracted Lean model — 62 defs, the
full verify cone (chain -> wots -> xmss -> ht -> fors ->
slh_verify_internal) up to the apex verify_mono.slh_verify_128s. No
sorry, no admit.
- verification/gen/SlhVerify/FunsExternal.lean + TypesExternal.lean:
hand-maintained externals with the two-class justification header —
(1) the five SHA-2 hash oracles = the deliberate cryptographic
boundary (the only axioms the apex certificate will carry beyond
Lean's three); (2) transpiler plumbing (try_from, is_err, iterator
Step/Take, zeroize) adopted as axioms for the phase-1 type-check, to
be discharged in the proof phase.
- verification/check.sh: real Phase-1 button — compiles the model under
lean-guard (memory-capped, serialized). GREEN. Still says NOTHING
PROVEN: a well-formed model is not a correct one.
Zero certificates. Proof layers (chain semantics -> ... -> acceptance
equation) are the next task.
Co-Authored-By: Claude Fable 5 <noreply@anthropic.com>
Subject pinned: integritychain/fips205 @ 30bac08 via
saymrwulf/fips205-source @ 5dca0db. Parameter set SLH-DSA-SHA2-128s.
Scope: verify path only (slh_verify -> ... -> chain); six SHA-2 hash
oracles opaque per the standing boundary.
Gate-0 record (2026-07-22): charon clean on the full verify cone;
aeneas translates everything except the Hashers fn-pointer struct
(3 unique errors, the sole obstruction) -> phase 1 = named-opaque-
free-function compat patch in the snapshot repo, the established
dalek sha512-shim pattern.
check.sh exits non-green and says NOTHING PROVEN YET (H5, R3).
lean-guard copied; every future compile runs under it (S1, S2).
Co-Authored-By: Claude Fable 5 <noreply@anthropic.com>
