mrwulf 84cd00d377 phase 2: SECOND CERTIFICATE — WOTS+ chain loop (Algorithm 8) proven ... 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>		2026-07-23 14:48:39 +02:00
..
.gitkeep	SLH-DSA (FIPS 205) campaign skeleton: honest zero-certificate state	2026-07-22 21:00:57 +02:00
ChainSpec.lean	phase 2: FIRST CERTIFICATE — chain (Algorithm 5) proven, button green	2026-07-23 11:34:59 +02:00
WotsSpec.lean	phase 2: SECOND CERTIFICATE — WOTS+ chain loop (Algorithm 8) proven	2026-07-23 14:48:39 +02:00