verification: pin the harness, audit drivers and policy files (P1-c)

This repository has the estate's strongest gates, which makes them the most
valuable to switch off. Until now every one of them was executed by scripts
that nothing pinned.

Phase 0c requires every harness file to match HARNESS.sha256 — 15 files:
check.sh, lean-guard, inventory_gate.sh, run_bare.sh, all three self-tests,
both audit drivers (Proofs/Inventory.lean, Proofs/AxiomCheck.lean), the policy
tables (inventory-allowlist.txt, AUDIT-MANIFEST.txt), the toolchain pin, the
fidelity harness and its Python transcription, and the extracted model.

WHICH files must be pinned is policy and lives in check.sh, never in the map
being consulted: the required set is derived from the filesystem (the
executable bit, plus gen/**.lean, plus an explicit list for the rest), so
deleting a pin entry is a set mismatch rather than a silent un-pinning.

gen/LTLAcc/HashExternal.lean was previously bound by nothing at all — it was
compiled and trusted. It is now pinned, and the derivation is by set, so a new
model file fails closed.

selftest_audit.sh case 9 is split rather than relabelled. Phase 0c now catches
an unpinned rogue gen module BEFORE the dead-file gate runs, so asserting only
the new diagnostic would have quietly retired the dead-file gate from the test
suite. 9a asserts the harness-set mismatch on the unpinned file; 9b pins it —
an author who added it deliberately — and asserts Phase 2 still dies with DEAD
FILE (gen). Ten cases now, all defeated.

KNOWN-GAPS and the trusted base record the circularity plainly: an author who
edits a script and refreshes its pin in one commit passes every phase. The pin
removes the silent path, not the possibility. Review at the pinned commit
remains the consumer's protection.

Verified green after the fix: button (75s), harness self-test, binding
self-test, and the ten-case audit self-test. ATTESTATION GREEN (Lean +
fidelity), all fidelity case counts identical to the pre-change run.

Co-Authored-By: Claude Opus 4.8 <noreply@anthropic.com>

KNOWN-GAPS.md

@@ -159,3 +159,24 @@ list is COMPLETE, not merely that the items are acceptable.
    ConsRec-equivalent acceptance; or (B) mechanize the signed-head +
    pin-store state machine and prove the refinement; or (C) keep the
    boundary and this scoped claim permanently.
+16. **The statement binding covers identity, not meaning** (added
+   2026-07-28 with `check.sh` Phase 3d). The coverage gate pins every
+   constant's name, kind and axiom cone, both directions; Phase 3d
+   additionally pins every constant's fully-elaborated TYPE and every
+   definition's fully-elaborated BODY, digest committed as
+   `AUDIT-MANIFEST.txt`. What that buys is that the corpus is the one
+   that was reviewed. What it does NOT buy: (a) whether those
+   statements say anything worth believing is a question a human
+   reading `STATEMENT-MAP.md` answers, not the button; (b) an author
+   who edits a definition and refreshes the digest in the same commit
+   passes every phase — the defence is that both changes are visible in
+   the diff at the pinned commit; (c) proof TERMS are deliberately not
+   bound, by proof irrelevance, so a proof rewritten to a different term
+   of the same statement and cone moves nothing.
+   Worth recording plainly, because it was measured rather than
+   reasoned: wrapping one branch of `pinAccept`'s body in `id (…)` is
+   definitionally equal, compiles, leaves name/kind/type/cone untouched,
+   and the coverage gate reports GREEN. Only the digest sees it. That is
+   the exact size of the gap Phase 3d closes, and
+   `selftest_statements.sh` case 1 replays it.
+

verification/HARNESS.sha256

@@ -0,0 +1,15 @@
+e7d422f0be9a9e6f5465058292e30c711d52856428da2b01c470a57ec181540c  AUDIT-MANIFEST.txt
+7ab1bfbafc8ac9ab34d1e0eaa71ba2f1f9912121345cc1af281bcb1d2ec30ad2  check.sh
+070147e2667053bd5d5e1174b969fc6c91bfcf15ded1a5bff57754e15f416885  fidelity/lean_defs.py
+5d82462a002ac9fc782e95afe78b7719ba64b6410b5d2bfa620fe5317367dbf2  fidelity/run_fidelity.py
+503babb3f4e6aff82ebd59e8752469ecd60fba440ed3b11b3f97c2b655fbd9bf  gen/LTLAcc/HashExternal.lean
+f1eb5cdd158e30df14c59065fe2050448c77b5262b282208fa831d050f6b6a71  inventory-allowlist.txt
+f66fb98d2a09503d9bd0d60dc964545eea6dc94b9bbb9246d1021195b79f2601  inventory_gate.sh
+736ea4be712e1b5bcda10ecb466f0dec7008a2a36eabdfd77563976299c43cce  lean-guard
+ce4c4e3d87434b9663f46de25ce34b48a0cf0d392e0a320a0787b4674a2d7b61  lean-toolchain
+eda93f520546a692926b2a46bcb79332e1795879e5083327a8bf2404aca5cf87  Proofs/AxiomCheck.lean
+25344c8441077277addd6b4eb769b2c0e3b173afc28d3a6e8aeba0580c22a87f  Proofs/Inventory.lean
+0b8a0fc6947af1d1e600a756eb2b07dc88d189b21df3220c4501a41be8b33f1e  run_bare.sh
+67a44e0db818efc48dede26f73f76f1221424bb23e40e29d859b12d0d300403b  selftest_audit.sh
+3d5898161d663eccad162269a5a6c102319077e22e1f2d89a8bfcab6926d29f6  selftest-harness.sh
+cf6d4d8210e224a054d4ab693c28c83e7a9ddebda05da47d6ec311d825a606c0  selftest_statements.sh

verification/Proofs/Inventory.lean

@@ -95,7 +95,23 @@ def axiomCone (env : Environment) (root : Name) : Array Name := Id.run do
           stack := stack ++ v.getUsedConstants
   return (axioms.qsort (fun a b => a.toString < b.toString))
 
-#eval show CoreM Unit from do
+/-- Whitespace-canonical: every whitespace run collapses to one space, so the
+    pretty-printer's line wrapping cannot perturb the digest. -/
+def normWs (s : String) : String :=
+  (s.foldl (fun (acc : String × Bool) c =>
+      let c := if c.isWhitespace then ' ' else c
+      if c == ' ' then (if acc.2 then acc else (acc.1.push ' ', true))
+      else (acc.1.push c, false))
+    ("", true)).1
+
+/-- Fully-explicit (`pp.all`) rendering, whitespace-canonicalized. Implicit
+    arguments, instances and universe levels are all made visible, so two
+    statements that merely LOOK alike cannot share a rendering. -/
+def ppAll (e : Expr) : MetaM String := do
+  let fmt ← withOptions (fun o => o.setBool `pp.all true) (Meta.ppExpr e)
+  return normWs fmt.pretty
+
+#eval show MetaM Unit from do
   let env ← getEnv
   -- Resolve every corpus module to its index; a miss is a hard error.
   let mut idxs : Array Nat := #[]
@@ -104,6 +120,17 @@ def axiomCone (env : Environment) (root : Name) : Array Name := Id.run do
     | some i => idxs := idxs.push i
     | none   => throwError "INVENTORY ERROR: corpus module {m} is not imported"
   let mut lines : Array String := #[]
+  -- STATEMENT SURFACE (P1-a). The INV lines above record what each constant
+  -- IS and what it RESTS ON. They do not record what it SAYS: a theorem gutted
+  -- to a tautology keeps its name, its kind and its axiom cone, and a `def`
+  -- redefined to BE the thing it was meant to specify keeps all three too,
+  -- while the certificate stated against it silently becomes vacuous. So every
+  -- constant additionally contributes its fully-elaborated TYPE, and every
+  -- definition its fully-elaborated BODY. Proof terms are NOT emitted: by
+  -- proof irrelevance a theorem's content is its statement, and its term is
+  -- both enormous and irrelevant to what is being claimed.
+  let mut stmts : Array String := #[]
+  let mut nTypes := 0
   for (n, ci) in env.constants.toList do
     if let some i := env.getModuleIdxFor? n then
       if idxs.contains i then
@@ -115,9 +142,25 @@ def axiomCone (env : Environment) (root : Name) : Array Name := Id.run do
           throwError "INVENTORY ERROR: cone divergence on {n}: walker={cone} core={coreCone}"
         let coneStr := ",".intercalate (cone.toList.map (·.toString))
         lines := lines.push s!"INV|{n}|{kindOf ci}|{coneStr}"
+        stmts := stmts.push s!"STMT|{n}|{kindOf ci}|type={← ppAll ci.type}"
+        nTypes := nTypes + 1
+        match ci with
+        | .defnInfo v => stmts := stmts.push s!"STMT|{n}|{kindOf ci}|value={← ppAll v.value}"
+        | _           => pure ()
   let sorted := lines.qsort (· < ·)
   for l in sorted do
     IO.println l
   IO.println s!"INV-COUNT|{sorted.size}"
+  -- FAIL CLOSED: the statement surface must cover the inventory exactly. If
+  -- these ever diverge, some constant is inventoried but unbound — which is
+  -- precisely the gap this section exists to close.
+  let sortedStmts := stmts.qsort (· < ·)
+  unless nTypes == sorted.size do
+    throwError "INVENTORY ERROR: {sorted.size} constants inventoried but {nTypes} carry a statement"
+  IO.println "STMT-BEGIN"
+  for l in sortedStmts do
+    IO.println l
+  IO.println "STMT-END"
+  IO.println s!"STMT-COUNT|{sortedStmts.size}"
 
 end LTLAccAudit

verification/check.sh

@@ -6,7 +6,9 @@
 # both directions.
 #
 # Phases: 0 resource/integrity · 1 stub+axiom-smuggling audit ·
-#         2 compile manifest · 3 boundary-exact axiom audit
+#         2 compile manifest · 3 boundary-exact axiom audit ·
+#         3b environment-derived coverage · 3c doc-consistency ·
+#         3d statement + specification binding · 4 definition fidelity
 # ─────────────────────────────────────────────────────────────────────────────
 set -euo pipefail
 # Toolchain bootstrap is overridable for reviewers with their own install
@@ -114,6 +116,59 @@ while IFS= read -r -d '' o; do
   [ -f "${o%.olean}.lean" ] || { echo "ORPHAN OLEAN: $o has no sibling .lean (stale artifact)"; exit 1; }
 done < <(find "$HERE" -name '*.olean' -print0)
 
+# ── Phase 0c: harness integrity ─────────────────────────────────────────────
+# WHY. Every gate below is executed by a script that, until now, nothing
+# pinned. Round-5 review of the companion SLH-DSA repository stubbed the
+# compiler wrapper alone and its button printed ALL GREEN in 3.6 seconds over
+# deliberately destroyed proofs. Depth of checking is worth nothing if the
+# thing doing the checking is unbound — and this repo's gates are the estate's
+# strongest, which makes them the most valuable to switch off.
+#
+# WHICH files must be pinned is POLICY, and policy lives here — in the root of
+# trust — never inside the map being consulted. If the required set were read
+# from HARNESS.sha256, deleting an entry would silently un-pin that file
+# instead of failing the build.
+#
+# Membership is SELF-DERIVING from two sources the filesystem can answer: the
+# executable bit (anything this script can shell out to) and gen/**.lean (the
+# extracted model, which nothing else byte-pins in this repo). Load-bearing
+# files that are neither — the audit drivers, the policy tables, the toolchain
+# pin, the fidelity harness — cannot be discovered and are listed explicitly.
+HARNESS_EXTRA=(
+  AUDIT-MANIFEST.txt        # the statement block Phase 3d's digest is taken over
+  inventory-allowlist.txt   # the pinned audit surface Phase 3b diffs against
+  lean-toolchain            # which Lean the corpus claims to have been checked by
+  fidelity/lean_defs.py     # the Python transcription the differential compares
+  fidelity/run_fidelity.py  # the differential itself
+  Proofs/Inventory.lean     # audit driver: emits the inventory AND the statements
+  Proofs/AxiomCheck.lean    # audit driver: the #print axioms queries of Phase 3
+)
+echo "=== Phase 0c: harness integrity ==="
+if [ ! -s "$HERE/HARNESS.sha256" ]; then
+  echo "FATAL: HARNESS.sha256 is missing or empty — the harness is unpinned."
+  exit 1
+fi
+# check.sh is pinned like everything else: that catches drift and accident. It
+# does NOT stop an author who edits this script and refreshes its pin in one
+# commit — nothing executed by the harness can. The defence there is that both
+# changes appear in the diff at the pinned commit.
+HARNESS_REQUIRED=$( { find "$HERE" -type f -executable -not -path '*/.git/*' -printf '%P\n'
+                      find "$HERE/gen" -type f -name '*.lean' -printf 'gen/%P\n'
+                      printf '%s\n' "${HARNESS_EXTRA[@]}"; } | sort -u )
+HARNESS_PINNED=$(awk '{print $2}' "$HERE/HARNESS.sha256" | sort -u)
+if [ "$HARNESS_REQUIRED" != "$HARNESS_PINNED" ]; then
+  echo "FATAL: the set of harness files does not match HARNESS.sha256."
+  echo "  (< pinned, > present and requiring a pin)"
+  diff <(echo "$HARNESS_PINNED") <(echo "$HARNESS_REQUIRED") | sed 's/^/    /'
+  exit 1
+fi
+if ! ( cd "$HERE" && sha256sum -c --quiet HARNESS.sha256 ) ; then
+  echo "FATAL: a harness file does not match its pin. The button you are"
+  echo "running is not the button that was reviewed."
+  exit 1
+fi
+echo "  $(wc -l < "$HERE/HARNESS.sha256") harness files match their pins"
+
 echo "=== Phase 1: stub + axiom-smuggling audit ==="
 if grep -rn 'by trivial' "$HERE"/Proofs/*.lean 2>/dev/null; then
   echo "STUB DETECTED"; exit 1; fi
@@ -239,7 +294,8 @@ for cert in "${!CONES[@]}"; do
       "$HERE/inventory-allowlist.txt" || {
     echo "  PINNED BUT NOT INVENTORIED: $cert (in CONES, not in allowlist)"; COVFAIL=1; }
 done
-rm -f "$INVLOG"
+# (INVLOG is NOT removed here: Phase 3d binds the statement block emitted by
+#  this same run. Removed at the end of 3d.)
 
 # every pinned cert must actually be queried by AxiomCheck (no pin-but-never-check)
 for cert in "${!CONES[@]}"; do
@@ -276,6 +332,69 @@ print(' '.join(f'{int(v.replace(chr(95),\"\")):,}' for v in vals))"); do
 done
 [ "$DOCFAIL" = 0 ] && echo "  docs agree with allowlist ($NALLOW), CONES ($NCONES), fidelity pins"
 [ "$DOCFAIL" = 0 ] || { echo "DOC-CONSISTENCY FAILED"; exit 1; }
+# -- Phase 3d: statement + specification binding (P1-a) ---------------------
+# WHAT PHASES 3/3b DO NOT ESTABLISH. Phase 3 pins each certificate's exact
+# axiom cone; Phase 3b pins the full environment surface, kind and cone, both
+# directions. Neither records what a declaration SAYS. A theorem gutted to a
+# tautology keeps its name, its kind and its cone. A `def` redefined to BE the
+# thing it was meant to specify keeps all three, and every certificate stated
+# against it silently becomes vacuous — with the allowlist unmoved.
+#
+# Proofs/Inventory.lean therefore also emits, for every inventoried constant,
+# its fully-elaborated TYPE, and for every definition its fully-elaborated
+# BODY. Proof terms are deliberately absent: by proof irrelevance a theorem's
+# content is its statement. This phase binds the SHA-256 of that block, and
+# the block itself is committed as AUDIT-MANIFEST.txt so a mismatch is DIFFED
+# rather than merely reported.
+#
+# To rotate deliberately: run check.sh, take the printed OBSERVED digest, and
+# update the constant below AND AUDIT-MANIFEST.txt in the same reviewable
+# commit. Visibility in review is the defence; no harness audits its author.
+EXPECTED_STMT_SHA256="e7d422f0be9a9e6f5465058292e30c711d52856428da2b01c470a57ec181540c"
+echo "=== Phase 3d: statement + specification binding ==="
+STMTFAIL=0
+STMT_BLOCK=$(awk '/^STMT-BEGIN/{f=1;next} /^STMT-END/{f=0} f' "$INVLOG")
+# FAIL CLOSED ON ABSENCE: no block and a matching block must not share a path.
+if [ -z "$STMT_BLOCK" ]; then
+  echo "  NO STATEMENT BLOCK emitted by Proofs/Inventory.lean (fail-closed)"; STMTFAIL=1
+else
+  # Output integrity, same discipline as the INV-COUNT trailer: a truncated or
+  # crashed run must not pass as a short-but-matching block.
+  N_STMT=$(printf '%s\n' "$STMT_BLOCK" | grep -c '^STMT|')
+  STMT_TRAILER=$(grep '^STMT-COUNT|' "$INVLOG" | tail -1 | cut -d'|' -f2)
+  if [ -z "$STMT_TRAILER" ] || [ "$STMT_TRAILER" != "$N_STMT" ]; then
+    echo "  STATEMENT BLOCK TRUNCATED: trailer=${STMT_TRAILER:-absent}, observed $N_STMT"; STMTFAIL=1
+  fi
+  # Every inventoried constant must carry a statement line. Inventory.lean
+  # asserts this internally too; asserting it here as well means a tampered
+  # Inventory.lean cannot simply drop its own check.
+  N_INV=$(grep -c '^INV|' "$INVLOG")
+  N_TYPES=$(printf '%s\n' "$STMT_BLOCK" | grep -c '|type=')
+  if [ "$N_TYPES" != "$N_INV" ]; then
+    echo "  STATEMENT COVERAGE GAP: $N_INV constants inventoried, $N_TYPES carry a statement"; STMTFAIL=1
+  fi
+  GOT_STMT_SHA=$(printf '%s\n' "$STMT_BLOCK" | sha256sum | cut -d' ' -f1)
+  if [ "$GOT_STMT_SHA" != "$EXPECTED_STMT_SHA256" ]; then
+    printf '%s\n' "$STMT_BLOCK" > "$HERE/.stmt-manifest.observed"
+    echo "  STATEMENT DIGEST MISMATCH."
+    echo "    expected: $EXPECTED_STMT_SHA256"
+    echo "    observed: $GOT_STMT_SHA"
+    echo "    A statement or a definition body changed. First differences:"
+    diff -u "$HERE/AUDIT-MANIFEST.txt" "$HERE/.stmt-manifest.observed" 2>/dev/null \
+      | head -30 | sed 's/^/      /' || echo "      (AUDIT-MANIFEST.txt absent — cannot diff)"
+    rm -f "$HERE/.stmt-manifest.observed"
+    STMTFAIL=1
+  elif ! printf '%s\n' "$STMT_BLOCK" | cmp -s - "$HERE/AUDIT-MANIFEST.txt"; then
+    # The digest's INPUT must be committed and current, or the diff above would
+    # compare against a stale reference and quietly mislead the next reader.
+    echo "  COMMITTED BLOCK STALE: AUDIT-MANIFEST.txt does not match the emitted block"
+    echo "  (the digest matched, so the committed copy needs refreshing)"; STMTFAIL=1
+  fi
+fi
+[ "$STMTFAIL" = 0 ] && echo "  statements bound: $N_STMT lines over $N_INV constants, sha256 = $GOT_STMT_SHA"
+[ "$STMTFAIL" = 0 ] || { echo "STATEMENT BINDING FAILED"; rm -f "$INVLOG"; exit 1; }
+rm -f "$INVLOG"
+
 # -- Phase 4: definition fidelity (Lean defs vs deployed pacta verifiers) --
 echo "=== Phase 4: definition fidelity ==="
 PACTA_SRC="${PACTA_SRC:-$HERE/../../proof-aware-crypto-tooling-agent/src}"

verification/fidelity/run_fidelity.py

@@ -39,10 +39,23 @@ import lean_defs as L                       # noqa: E402
 
 NMAX = int(os.environ.get("FIDELITY_NMAX", "256"))
 # lied-size family pins (gap 14; valid for the default FIDELITY_LIED_NMAX=60):
-# 73,573 boundary cases, 3,867 expected one-sided divergences
+# 73,573 boundary cases.
-# (3,405 lied-old-size + 462 lied-new-size), smallest witness (n=3, m=2 claimed 1)
+#
+# The divergence count was 3,867 (3,405 lied-old-size + 462 lied-new-size,
+# smallest witness n=3, m=2 claimed 1) until pacta `ddbb5a4` (2026-07-23)
+# restored the RFC 9162 2.1.4.2 Step-7 terminal condition `sn == 0` to
+# verify_consistency. That one conjunct removes EVERY divergence in this
+# family, so the pin is now 0: the deployed verifier and the mechanized
+# ConsRec model agree on all 73,573 boundary cases.
+#
+# The pin was left at 3,867 when the fix landed, which made this assertion —
+# and therefore check.sh Phase 4 — fail from 2026-07-23 until it was noticed
+# on 2026-07-28. KNOWN-GAPS.md gap 14 had already recorded the closure; only
+# this constant was stale. Nothing about the paper, public log entry 13, or
+# the attested commit 172a1d0 changes: the historical divergence remains
+# truthfully recorded and reproducible at `vulnerable/sn0-consistency-fd2f6ba`.
 LIED_PIN_TOTAL = 73_573
-LIED_PIN_DIV = 3_867
+LIED_PIN_DIV = 0
 
 
 def _h(b):

verification/selftest-harness.sh

@@ -0,0 +1,108 @@
+#!/usr/bin/env bash
+# ─────────────────────────────────────────────────────────────────────────────
+# selftest-harness.sh — adversarial self-test for check.sh Phase 0c.
+#
+# Phase 0c pins the scripts and policy files the button itself runs on. The
+# attack it exists to stop is the cheapest one in the estate: don't touch the
+# proofs at all, edit the checker. Round-5 review of the companion SLH-DSA
+# repository stubbed the compiler wrapper alone and got ALL GREEN in 3.6
+# seconds over deliberately destroyed proofs.
+#
+# Cases, each asserting a SPECIFIC diagnostic:
+#   0  positive control: untouched tree passes
+#   1  a pinned harness file edited by one byte      → does not match its pin
+#   2  a NEW executable appears, unpinned            → set mismatch
+#   3  an entry DELETED from HARNESS.sha256          → set mismatch, NOT a
+#      silent un-pin (this is the shape of the defect SLH-DSA round-6 found:
+#      dropping a key un-pinned two files with no diagnostic at all)
+#   4  HARNESS.sha256 itself removed                 → fail-closed
+#
+# Phase 0c is lifted out of check.sh at run time, so the tested logic IS the
+# shipping logic. Cheap: no Lean, runs in about a second.
+# ─────────────────────────────────────────────────────────────────────────────
+set -uo pipefail
+HERE="$(cd "$(dirname "$0")" && pwd)"
+FAILURES=0
+STASH="$(mktemp -d)"
+NEWEXE="$HERE/zz-selftest-helper.sh"
+
+cleanup() {
+  [ -f "$STASH/HARNESS.sha256" ] && cp "$STASH/HARNESS.sha256" "$HERE/HARNESS.sha256"
+  [ -f "$STASH/victim" ] && cp "$STASH/victim" "$HERE/$VICTIM"
+  rm -f "$NEWEXE"
+  rm -rf "$STASH"
+}
+trap cleanup EXIT INT TERM
+
+cp "$HERE/HARNESS.sha256" "$STASH/HARNESS.sha256"
+
+# Lift Phase 0c. The two repo families end the phase differently, so accept
+# either terminator rather than hardcoding one and silently lifting nothing.
+DRIVER="$STASH/phase0c.sh"
+{
+  echo 'set -uo pipefail'
+  echo "HERE=\"$HERE\""
+  awk '/^# ── Phase 0c/{f=1} f{print} /^# ── Phase 1|^echo "=== Phase 1/{if(f && !/Phase 0c/) exit}' "$HERE/check.sh" \
+    | sed '/^# ── Phase 1/d; /^echo "=== Phase 1/d'
+} > "$DRIVER"
+if [ "$(grep -c . "$DRIVER")" -lt 20 ]; then
+  echo "FATAL: could not lift Phase 0c out of check.sh — the phase markers moved."
+  echo "This self-test must attack the shipping gate; refusing to run against nothing."
+  exit 1
+fi
+
+expect() {  # expect <label> <want-rc> <want-substring>
+  local label="$1" want_rc="$2" want_txt="$3" out rc
+  out=$(bash "$DRIVER" 2>&1); rc=$?
+  if [ "$rc" -ne "$want_rc" ]; then
+    echo "  ✗ $label: exit $rc, expected $want_rc"; echo "$out" | sed 's/^/      /'
+    FAILURES=$((FAILURES+1)); return
+  fi
+  if ! grep -qF "$want_txt" <<<"$out"; then
+    echo "  ✗ $label: exit code right, diagnostic wrong (rejected for the wrong reason)"
+    echo "      wanted: $want_txt"; echo "$out" | sed 's/^/      /'
+    FAILURES=$((FAILURES+1)); return
+  fi
+  echo "  ✓ $label"
+}
+
+echo "=== selftest-harness: attacking check.sh Phase 0c ==="
+
+# ── 0. positive control ────────────────────────────────────────────────────
+expect "case 0 control: untouched harness passes" 0 "match their pins"
+
+# ── 1. edit a pinned file. lean-guard is the pointed choice: it is the memory
+#      cap protecting this machine, and stubbing it is the demonstrated
+#      3.6-second path to a false green.
+VICTIM=lean-guard
+cp "$HERE/$VICTIM" "$STASH/victim"
+printf '\n# selftest\n' >> "$HERE/$VICTIM"
+expect "case 1: edited lean-guard caught" 1 "does not match its pin"
+cp "$STASH/victim" "$HERE/$VICTIM"
+
+# ── 2. a new executable the button could shell out to ──────────────────────
+printf '#!/bin/sh\necho "unpinned"\n' > "$NEWEXE"; chmod +x "$NEWEXE"
+expect "case 2: new unpinned executable caught" 1 "does not match HARNESS.sha256"
+rm -f "$NEWEXE"
+
+# ── 3. delete a pin entry: the set must be derived from the filesystem, not
+#      read out of the map being consulted, or this is a silent un-pin.
+grep -v " ${VICTIM}\$" "$STASH/HARNESS.sha256" > "$HERE/HARNESS.sha256"
+expect "case 3: deleted pin entry is a failure, not a silent un-pin" 1 "does not match HARNESS.sha256"
+cp "$STASH/HARNESS.sha256" "$HERE/HARNESS.sha256"
+
+# ── 4. absence must not pass for cleanliness ───────────────────────────────
+rm -f "$HERE/HARNESS.sha256"
+expect "case 4: missing pin file is fail-closed" 1 "the harness is unpinned"
+cp "$STASH/HARNESS.sha256" "$HERE/HARNESS.sha256"
+
+# ── 5. restored ────────────────────────────────────────────────────────────
+expect "case 5: restored to green" 0 "match their pins"
+
+echo ""
+if [ "$FAILURES" -eq 0 ]; then
+  echo "SELFTEST PASSED — Phase 0c rejects harness tampering for the stated reason."
+  exit 0
+fi
+echo "SELFTEST FAILED: $FAILURES case(s) did not behave as claimed."
+exit 1

verification/selftest_audit.sh

@@ -123,15 +123,31 @@ grep -q "DEAD FILE: Proofs/Rogue.lean" "$T/check8.out" || {
 echo "  ✓ case 8 unmanifested Proofs module: check.sh dies with DEAD FILE"
 rm -f "$T/Proofs/Rogue.lean"
 
-# 9 — unmanifested gen/ module (full check.sh; dies in Phase 2)
+# 9 — unmanifested gen/ module. TWO gates stand here now and the case
+#     exercises BOTH, because asserting only the outer one would quietly
+#     retire the inner one from the test suite.
+#
+#     9a: Phase 0c (added 2026-07-29) derives the required pin set from
+#     gen/**.lean, so an unpinned model file is caught before compilation.
+#     9b: with the rogue file pinned — i.e. an author who added it
+#     deliberately — the dead-file gate in Phase 2 must still catch that it is
+#     absent from the compile manifest.
 printf '/- rogue -/\ntheorem rogue_gen : 1 = 1 := rfl\n' > "$T/gen/LTLAcc/Rogue.lean"
-if SKIP_FIDELITY=1 "$T/check.sh" > "$T/check9.out" 2>&1; then
+if SKIP_FIDELITY=1 "$T/check.sh" > "$T/check9a.out" 2>&1; then
-  echo "  ✗ case 9: check.sh PASSED with unmanifested gen/LTLAcc/Rogue.lean"; exit 1
+  echo "  ✗ case 9a: check.sh PASSED with an unpinned gen/LTLAcc/Rogue.lean"; exit 1
 fi
-grep -q "DEAD FILE (gen): gen/LTLAcc/Rogue.lean" "$T/check9.out" || {
+grep -q "does not match HARNESS.sha256" "$T/check9a.out" || {
-  echo "  ✗ case 9: check.sh failed without DEAD FILE (gen) diagnosis"; tail -5 "$T/check9.out"; exit 1; }
+  echo "  ✗ case 9a: check.sh failed without the harness-set diagnosis"; tail -5 "$T/check9a.out"; exit 1; }
-echo "  ✓ case 9 unmanifested gen module: check.sh dies with DEAD FILE (gen)"
+echo "  ✓ case 9a unpinned gen module: Phase 0c dies with a harness-set mismatch"
+
+( cd "$T" && sha256sum gen/LTLAcc/Rogue.lean >> HARNESS.sha256 )
+if SKIP_FIDELITY=1 "$T/check.sh" > "$T/check9b.out" 2>&1; then
+  echo "  ✗ case 9b: check.sh PASSED with unmanifested gen/LTLAcc/Rogue.lean"; exit 1
+fi
+grep -q "DEAD FILE (gen): gen/LTLAcc/Rogue.lean" "$T/check9b.out" || {
+  echo "  ✗ case 9b: check.sh failed without DEAD FILE (gen) diagnosis"; tail -5 "$T/check9b.out"; exit 1; }
+echo "  ✓ case 9b pinned but unmanifested: check.sh dies with DEAD FILE (gen)"
 
 rm -rf "$WORK"
 trap - ERR
-echo "=== SELF-TEST GREEN: 9 attack cases defeated + positive control ==="
+echo "=== SELF-TEST GREEN: 10 attack cases defeated + positive control ==="

verification/selftest_statements.sh

@@ -0,0 +1,147 @@
+#!/usr/bin/env bash
+# ─────────────────────────────────────────────────────────────────────────────
+# selftest_statements.sh — adversarial self-test of check.sh Phase 3d.
+#
+# WHY A SECOND SELF-TEST. selftest_audit.sh attacks the coverage gate, which
+# pins every constant's NAME, KIND and AXIOM CONE, both directions. That gate
+# is strong and none of its nine attacks defeat it. It is also blind to what a
+# declaration SAYS, and this script demonstrates that with a real, compiling
+# edit rather than an argument:
+#
+#   `LTLAcc.pinAccept` is a specification definition. Wrapping one branch of
+#   its body in `id (…)` is definitionally equal, so every downstream proof
+#   still compiles; the name, the kind, the type and the axiom cone are all
+#   unchanged. The inventory gate reports 222 constants, environment ==
+#   allowlist, GREEN. Only the statement digest sees it.
+#
+#   That edit is deliberately harmless. The point is that the ONLY thing
+#   standing between it and a genuinely vacuous redefinition is the digest.
+#
+# Cases:
+#   0  positive control: pristine tree passes Phase 3d
+#   1  defeq body edit: old gate PASSES (asserted), Phase 3d FAILS (asserted)
+#   2  committed AUDIT-MANIFEST.txt hand-edited      → COMMITTED BLOCK STALE
+#   3  statement block truncated                     → BLOCK TRUNCATED
+#   4  a constant inventoried but carrying no statement → COVERAGE GAP
+#
+# Phase 3d is lifted out of check.sh at run time, so the tested logic IS the
+# shipping logic. Run AFTER a green check.sh. All Lean work via lean-guard.
+# ─────────────────────────────────────────────────────────────────────────────
+set -uo pipefail
+AENEAS_ENV="${AENEAS_ENV:-$HOME/aeneas-toolchain/env.sh}"
+[ -f "$AENEAS_ENV" ] || { echo "FATAL: Aeneas environment not found: $AENEAS_ENV"; exit 1; }
+source "$AENEAS_ENV"
+SRC="$(cd "$(dirname "$0")" && pwd)"
+AENEAS_LEAN="$AENEAS_HOME/backends/lean"
+CORES="${LEAN_MAX_CORES:-0-3}"
+FAILURES=0
+
+WORK=$(mktemp -d /tmp/acc-stmt-selftest-XXXX)
+trap 'rm -rf "$WORK"' EXIT
+echo "=== statement-binding self-test (scratch: $WORK) ==="
+cp -a "$SRC" "$WORK/verification"
+T="$WORK/verification"
+cp "$T/Proofs/PinStore.lean" "$T/PinStore.pristine"
+cp "$T/AUDIT-MANIFEST.txt"   "$T/MANIFEST.pristine"
+
+# Phase 3d, lifted verbatim from the shipping button. HERE and INVLOG are the
+# two variables it reads from its surroundings.
+DRIVER="$T/phase3d.sh"
+{
+  echo 'set -uo pipefail'
+  echo "HERE=\"$T\""
+  echo 'INVLOG="$1"'
+  sed -n '/^# -- Phase 3d/,/^# -- Phase 4/p' "$SRC/check.sh" | sed '$d'
+} > "$DRIVER"
+if [ "$(wc -l < "$DRIVER")" -lt 40 ]; then
+  echo "FATAL: could not lift Phase 3d out of check.sh — the phase markers moved."
+  echo "This self-test must attack the shipping gate; refusing to run against nothing."
+  exit 1
+fi
+
+# Recompile the edited leaf module + the inventory into $T/inv.out.
+build_inventory() {
+  cd "$AENEAS_LEAN"
+  lake env bash -c "
+    set -euo pipefail
+    cd '$T' && export LEAN_PATH=\"\$LEAN_PATH:$T/gen:$T\"
+    LEAN_TIMEOUT=600 LEAN_MAX_CORES=$CORES '$T/lean-guard' Proofs/PinStore.lean >/dev/null 2>&1
+    LEAN_TIMEOUT=600 LEAN_MAX_CORES=$CORES '$T/lean-guard' Proofs/Inventory.lean
+  " > "$T/inv.out" 2>&1
+  local rc=$?
+  cd "$T"
+  return $rc
+}
+
+expect() {  # expect <label> <invlog> <want-rc> <want-substring>
+  local label="$1" invlog="$2" want_rc="$3" want_txt="$4" out rc
+  # Phase 3d removes its INVLOG on the way out — that is correct behaviour for
+  # the button and fatal for a fixture, so it always gets a disposable copy.
+  cp "$invlog" "$T/inv.feed"
+  out=$(bash "$DRIVER" "$T/inv.feed" 2>&1); rc=$?
+  if [ "$rc" -ne "$want_rc" ]; then
+    echo "  ✗ $label: exit $rc, expected $want_rc"; echo "$out" | sed 's/^/      /'
+    FAILURES=$((FAILURES+1)); return
+  fi
+  if ! grep -qF "$want_txt" <<<"$out"; then
+    echo "  ✗ $label: exit code right, diagnostic wrong (rejected for the wrong reason)"
+    echo "      wanted: $want_txt"; echo "$out" | sed 's/^/      /'
+    FAILURES=$((FAILURES+1)); return
+  fi
+  echo "  ✓ $label"
+}
+
+# ── 0. positive control ────────────────────────────────────────────────────
+build_inventory || { echo "  ✗ case 0: pristine tree did not compile"; exit 1; }
+cp "$T/inv.out" "$T/inv.pristine"
+expect "case 0 control: pristine tree passes Phase 3d" "$T/inv.pristine" 0 "statements bound"
+
+# ── 1. THE ONE THAT MATTERS: a compiling, definitionally-equal body edit ───
+python3 - "$T/Proofs/PinStore.lean" <<'PY'
+import sys
+f = sys.argv[1]; s = open(f).read()
+old = "  else ConsRec n n' C true r = some (r, r')"
+assert s.count(old) == 1, "pinAccept body not found — this case is vacuous"
+open(f, "w").write(s.replace(old, "  else id (ConsRec n n' C true r = some (r, r'))", 1))
+PY
+if build_inventory; then
+  # The premise: the coverage gate must NOT see this. If it ever does, this
+  # case stops testing what it claims and must be re-examined, not re-labelled.
+  if "$T/inventory_gate.sh" "$T/inv.out" "$T/inventory-allowlist.txt" >/dev/null 2>&1; then
+    echo "  ✓ case 1 premise: the coverage gate passes the edit (kind and cone unmoved)"
+  else
+    echo "  ✗ case 1 premise: the coverage gate caught it — this case no longer isolates Phase 3d"
+    FAILURES=$((FAILURES+1))
+  fi
+  expect "case 1: defeq body edit caught by the statement digest" "$T/inv.out" 1 "STATEMENT DIGEST MISMATCH"
+else
+  echo "  ✗ case 1: the edited corpus did not compile (case is vacuous)"
+  FAILURES=$((FAILURES+1))
+fi
+cp "$T/PinStore.pristine" "$T/Proofs/PinStore.lean"
+
+# ── 2. committed block hand-edited ─────────────────────────────────────────
+sed -i '1s/$/ TAMPERED/' "$T/AUDIT-MANIFEST.txt"
+expect "case 2: hand-edited committed block" "$T/inv.pristine" 1 "COMMITTED BLOCK STALE"
+cp "$T/MANIFEST.pristine" "$T/AUDIT-MANIFEST.txt"
+
+# ── 3. truncated block: "nothing found" must not pass for "nothing wrong" ──
+grep -v '^STMT|LTLAcc.pinAccept|def|value=' "$T/inv.pristine" > "$T/inv.truncated"
+expect "case 3: truncated statement block" "$T/inv.truncated" 1 "BLOCK TRUNCATED"
+
+# ── 4. a constant inventoried but carrying no statement ────────────────────
+#     Drop one type line AND fix the trailer, so only the coverage comparison
+#     against the INV count can still object.
+grep -v '^STMT|LTLAcc.pinAccept|def|type=' "$T/inv.pristine" > "$T/inv.gap"
+NEW_N=$(awk '/^STMT-BEGIN/{f=1;next}/^STMT-END/{f=0}f' "$T/inv.gap" | grep -c '^STMT|')
+sed -i "s/^STMT-COUNT|.*/STMT-COUNT|$NEW_N/" "$T/inv.gap"
+expect "case 4: inventoried constant with no statement" "$T/inv.gap" 1 "STATEMENT COVERAGE GAP"
+
+echo ""
+if [ "$FAILURES" -eq 0 ]; then
+  echo "=== SELF-TEST GREEN: 4 attack cases defeated + positive control ==="
+  echo "    Phase 3d catches what the coverage gate provably cannot see."
+  exit 0
+fi
+echo "=== SELF-TEST FAILED: $FAILURES case(s) did not behave as claimed ==="
+exit 1