From e8fc83ba50840641d6d302dbb71ab561577da575 Mon Sep 17 00:00:00 2001
From: mrwulf <mrwulf.cleaner@gmail.com>
Date: Thu, 23 Jul 2026 14:34:42 +0200
Subject: [PATCH] post-flip drill over the chain certificate: HELD; audit gates
 now self-tested

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-selftest.sh | 55 ++++++++++++++++++++++++++++++++++
 1 file changed, 55 insertions(+)
 create mode 100755 verification/check-selftest.sh

diff --git a/verification/check-selftest.sh b/verification/check-selftest.sh
new file mode 100755
index 0000000..5d1a565
--- /dev/null
+++ b/verification/check-selftest.sh
@@ -0,0 +1,55 @@
+#!/usr/bin/env bash
+# Adversarial self-test of the check.sh gates (the R3-5 tradition: an audit
+# that cannot fail is theater). Two attacks, both MUST make check.sh fail:
+#
+#   1. DEAD FILE   — a stray Proofs/*.lean not in the manifest.
+#   2. SMUGGLED AXIOM — a certificate whose cone contains an axiom outside
+#      {kernel-3} ∪ {the five SHA-2 oracles}.
+#
+# Green here means: the gates genuinely reject both. Self-cleaning.
+set -euo pipefail
+HERE="$(cd "$(dirname "$0")" && pwd)"
+cd "$HERE"
+
+cleanup() { rm -f Proofs/Stray.lean Proofs/Stray.olean Proofs/EvilSpec.lean \
+                  Proofs/EvilSpec.olean check-evil-tmp.sh; }
+trap cleanup EXIT
+
+echo "check-selftest: attacking the gates"
+echo "===================================="
+
+# ── Attack 1: dead file ─────────────────────────────────────────────────────
+echo "-- stray" > Proofs/Stray.lean
+if ./check.sh > /tmp/selftest-dead.out 2>&1; then
+  echo "✗ ATTACK 1 SUCCEEDED: check.sh stayed green with a dead file"; exit 1
+fi
+grep -q "DEAD FILE" /tmp/selftest-dead.out \
+  || { echo "✗ ATTACK 1: failed, but not via the dead-file gate"; exit 1; }
+rm -f Proofs/Stray.lean Proofs/Stray.olean
+echo "✓ attack 1 rejected (dead-file gate works)"
+
+# ── Attack 2: smuggled axiom ────────────────────────────────────────────────
+cat > Proofs/EvilSpec.lean <<'EOF'
+import Proofs.ChainSpec
+axiom evil_ax : True
+theorem evil_thm : True := evil_ax
+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)')
+s = s.replace('{ echo "import Proofs.ChainSpec"',
+              '{ echo "import Proofs.ChainSpec"; echo "import Proofs.EvilSpec"')
+open("check-evil-tmp.sh","w").write(s)
+PY
+chmod +x check-evil-tmp.sh
+if ./check-evil-tmp.sh > /tmp/selftest-evil.out 2>&1; then
+  echo "✗ ATTACK 2 SUCCEEDED: audit passed a smuggled axiom"; exit 1
+fi
+grep -q "DISALLOWED" /tmp/selftest-evil.out \
+  || { echo "✗ ATTACK 2: failed, but not via the axiom gate"; exit 1; }
+echo "✓ attack 2 rejected (axiom gate works)"
+
+echo
+echo "SELFTEST GREEN: both gates genuinely reject their attacks."