From a0d69f029b615cac1eb9b524a29d539bbee3a795 Mon Sep 17 00:00:00 2001 From: mrwulf Date: Thu, 23 Jul 2026 15:07:07 +0200 Subject: [PATCH] post-flip drill over the WOTS+ certificate: HELD; one rotted gate fixed MIME-Version: 1.0 Content-Type: text/plain; charset=UTF-8 Content-Transfer-Encoding: 8bit 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 --- verification/check-selftest.sh | 11 ++++++++--- 1 file changed, 8 insertions(+), 3 deletions(-) diff --git a/verification/check-selftest.sh b/verification/check-selftest.sh index 5d1a565..83e8234 100755 --- a/verification/check-selftest.sh +++ b/verification/check-selftest.sh @@ -37,10 +37,15 @@ EOF python3 - <<'PY' s = open("check.sh").read() s = s.replace('PROOFS=(\n "ChainSpec"\n)', 'PROOFS=(\n "ChainSpec"\n "EvilSpec"\n)') -s = s.replace('CERTS=(\n "fips205.chain_free_loop_eq"\n)', - 'CERTS=(\n "fips205.chain_free_loop_eq"\n "evil_thm"\n)') +# Robust to the growing PROOFS / CERTS lists (do NOT hard-code their current +# contents — that rots the self-test as certificates are added): inject the +# evil entries right after each array's opening paren. +assert 'PROOFS=(\n' in s and 'CERTS=(\n' in s, "check.sh array shape changed" +s = s.replace('PROOFS=(\n', 'PROOFS=(\n "EvilSpec"\n', 1) +s = s.replace('CERTS=(\n', 'CERTS=(\n "evil_thm"\n', 1) +assert '{ echo "import Proofs.ChainSpec"' in s, "check.sh audit import shape changed" s = s.replace('{ echo "import Proofs.ChainSpec"', - '{ echo "import Proofs.ChainSpec"; echo "import Proofs.EvilSpec"') + '{ echo "import Proofs.EvilSpec"; echo "import Proofs.ChainSpec"', 1) open("check-evil-tmp.sh","w").write(s) PY chmod +x check-evil-tmp.sh