fips205.ht_loop_eq (Proofs/HtSpec.lean): the extracted ht_verify_free_loop
equals the explicit d-layer fold — at layer j: idx_leaf = idx_tree masked
to h' bits (mask+cast), idx_tree >>= h', layer address j, tree address to
the shifted index, node recomputed through xmss_pk_from_sig on the j-th
XMSS signature. Pins the hypertree layer schedule; the final node ==
pk_root comparison sits one bind above in ht_verify_free (apex material).
Exact cone: [propext, Classical.choice, Quot.sound, verify_mono.oracle.f,
verify_mono.oracle.h, verify_mono.oracle.t_l] — kernel-3 plus exactly the
three hash primitives the referenced WOTS+/XMSS machinery touches.
THE LAYER'S OBSTRUCTION (one per layer, on pattern) was not the proof but
the CONE: the first extraction of this loop carried Result-conversion
plumbing (try_from/is_err/unwrap; transitively a Take iterator and the
&u32 Sub instance) — all axioms, rightly rejected by the Phase-3 audit.
Fixed at SOURCE level (fips205-source 6f6a9d6, 8 sites, semantics
identical for every FIPS 205 parameter set, differential test re-run
green), then re-extracted: the loop body is now straight-line and the
proof is the plain chain/wots recipe (no branches; base case via
loop.eq_1; step lemma closes by rfl; induction = bind_congr ×12).
Also in this commit:
- gen/ regenerated from the patched snapshot (loop bodies of the three
prior certificates byte-identical modulo source line comments; all
three proofs recompiled unchanged and re-audited green).
- Dead-stub deletion (axiom-shadowing hygiene rule): the five obsoleted
plumbing axioms + vestigial take.default removed from FunsExternal, the
orphaned TryFromIntError type axiom removed from TypesExternal. The
model's external surface is now: 5 SHA-2 oracles (the boundary), the
Take iterator machinery used only by helpers::to_int (apex round's
de-plumbing item), 3 zeroize blanket impls (never on the verify path),
and the discharged-real u32 Step defs.
- check.sh: PROOFS += HtSpec, CERTS += fips205.ht_loop_eq, audit import
(self-test structure anchors untouched). README: four certificates +
the de-plumbing record.
Fidelity review at authorship (three-way): extracted body == Rust
ht_verify_free (verbatim from upstream hypertree.rs, calls -> *_free) ==
FIPS 205 Algorithm 12, incl. mask-then-shift order and layer-then-tree
address order.
Co-Authored-By: Claude Fable 5 <noreply@anthropic.com>
fips205.xmss_loop_eq (Proofs/XmssSpec.lean): the extracted
xmss_pk_from_sig_free_loop equals the explicit Merkle-path fold — at step
k set the tree height to k+1, test bit k of the leaf index; even bit:
tree_index := i/2 and H(node || auth[k]); odd bit: tree_index := (i-1)/2
and H(auth[k] || node). This pins the sibling hash ORDER, the address
schedule, and the auth-path indexing of Merkle verification. Exact cone:
[propext, Classical.choice, Quot.sound, verify_mono.oracle.h] — the first
certificate where H enters; F does not (the loop runs above the WOTS+
computation). check.sh green over all three certificates.
Fidelity review at authorship (three-way): extracted body (gen Funs.lean
761-801) == Rust verify_mono.rs xmss_pk_from_sig_free (verbatim from
upstream xmss.rs, hash calls -> oracle) == FIPS 205 Algorithm 10, incl.
the per-branch operation order (even: node-slice then auth[k]; odd:
auth[k] then node-slice) and the k+1 tree height.
Proof: the chain/wots recipe on a u32 range — u32_succ / fwd_succ / hnext
/ loop_unfold_bind reused VERBATIM from ChainSpec. New layer lesson (the
one novel obstruction, on pattern): the loop body BRANCHES on the index
bit, so the step lemma splits with by_cases + if_pos/if_neg; and the
get_tree_index pair-bind needs its matcher made concrete before the tail
normalizes — bind_congr + rintro to fix the scrutinee, then FULL simp
(only full simp iota-reduces the pair matcher; simp only will not) with
bind_assoc + bind_ok + the loop def closes each branch. The certificate's
own induction threads the IH under the opaque binds of BOTH branches with
bind_congr, per branch, ending exact ih.
check.sh: PROOFS += XmssSpec, CERTS += fips205.xmss_loop_eq, audit
imports XmssSpec (self-test structure anchors untouched). README: status
three certificates, Algorithm numbering per upstream comments (wots=8,
xmss=10).
Co-Authored-By: Claude Fable 5 <noreply@anthropic.com>
Five manual post-window drills each re-ran the same mechanical battery by
hand: worktree/head hygiene, sorry/admit/axiom sweep, check.sh, and
check-selftest.sh. verification/drill.sh is that battery as one
deterministic script, per the estate rule that enforcement lives in
buttons, not in model quality: a degraded work window cannot fake it — it
either exits 0 or it does not. Optional --full adds extract.sh
regeneration byte-identity.
Scope: one new executable script. No proof, model, or gate files touched.
The bespoke part of the drill — fidelity review of NEWLY written specs
against their extracted and upstream ground truth — remains a
per-new-artifact duty, recorded in each artifact's commit message.
Co-Authored-By: Claude Fable 5 <noreply@anthropic.com>
Full adversarial re-verification of the second-certificate window.
Everything of substance HELD:
- three-way fold fidelity EXACT: extracted wots_pk_from_sig_free_loop1
body == wotsChainFold step == Rust Algorithm 8, operation-for-operation
(chain_free with start=msg[i], steps=W-1-msg[i], slot tmp[i], addr
i as u32; adrs1 threaded forward; i' increment mirrors the range step)
- axiom sweep over all 7 WotsSpec decls minimal: pure iterator lemmas =
kernel-3; chain-touching = kernel-3 + oracle.f only
- button green fresh; non-vacuity PROVEN (a 1-index loop derives to
exactly one address-set + one chain_free at index 0)
- worktree clean, heads synced, Proofs/ free of sorry/admit/axiom
DRILL CATCH (self-test rot): check-selftest.sh hard-coded the single-cert
CERTS/PROOFS strings, so after the second certificate landed its
replacements silently no-oped and Attack 2 (smuggled axiom) started
failing via the DEAD-FILE gate instead of the AXIOM gate — a self-test
no longer testing what it claims. Fixed: inject the evil entries after
each array's opening paren (robust to the lists growing), with asserts
that abort if check.sh's array shape ever changes. Re-run: both attacks
now rejected via their correct gates, selftest green.
Lesson for the record: a self-test that pattern-matches the audited
config rots as the config grows; anchor on structure (the array opener),
never on current contents.
Co-Authored-By: Claude Fable 5 <noreply@anthropic.com>
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>
'What will be claimed' promised cones of exactly the three kernel
axioms — right for ed25519 field/scalar layers, wrong here: the hash
oracles permeate every SLH-DSA layer (chain already calls F). The
honest contract, now stated: each certificate cone = the three kernel
axioms + at most the five named oracles, nothing else; plumbing axioms
must be discharged before any certificate ships, audit-enforced.
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>
