KNOWN-GAPS.md

@@ -159,24 +159,3 @@ 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

@@ -1,15 +0,0 @@
-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,23 +95,7 @@ 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))
 
-/-- 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
+#eval show CoreM Unit from do
   let env ← getEnv
   -- Resolve every corpus module to its index; a miss is a hard error.
   let mut idxs : Array Nat := #[]
@@ -120,17 +104,6 @@ def ppAll (e : Expr) : MetaM String := 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
@@ -142,25 +115,9 @@ def ppAll (e : Expr) : MetaM String := 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,9 +6,7 @@
 # both directions.
 #
 # Phases: 0 resource/integrity · 1 stub+axiom-smuggling audit ·
-#         2 compile manifest · 3 boundary-exact axiom audit ·
-#         3b environment-derived coverage · 3c doc-consistency ·
-#         3d statement + specification binding · 4 definition fidelity
+#         2 compile manifest · 3 boundary-exact axiom audit
 # ─────────────────────────────────────────────────────────────────────────────
 set -euo pipefail
 # Toolchain bootstrap is overridable for reviewers with their own install
@@ -116,59 +114,6 @@ 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
@@ -294,8 +239,7 @@ for cert in "${!CONES[@]}"; do
       "$HERE/inventory-allowlist.txt" || {
     echo "  PINNED BUT NOT INVENTORIED: $cert (in CONES, not in allowlist)"; COVFAIL=1; }
 done
-# (INVLOG is NOT removed here: Phase 3d binds the statement block emitted by
-#  this same run. Removed at the end of 3d.)
+rm -f "$INVLOG"
 
 # every pinned cert must actually be queried by AxiomCheck (no pin-but-never-check)
 for cert in "${!CONES[@]}"; do
@@ -332,69 +276,6 @@ 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,23 +39,10 @@ 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.
-#
-# 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`.
+# 73,573 boundary cases, 3,867 expected one-sided divergences
+# (3,405 lied-old-size + 462 lied-new-size), smallest witness (n=3, m=2 claimed 1)
 LIED_PIN_TOTAL = 73_573
-LIED_PIN_DIV = 0
+LIED_PIN_DIV = 3_867
 
 
 def _h(b):

verification/selftest-harness.sh

@@ -1,108 +0,0 @@
-#!/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,31 +123,15 @@ 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. 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.
+# 9 — unmanifested gen/ module (full check.sh; dies in Phase 2)
 printf '/- rogue -/\ntheorem rogue_gen : 1 = 1 := rfl\n' > "$T/gen/LTLAcc/Rogue.lean"
-if SKIP_FIDELITY=1 "$T/check.sh" > "$T/check9a.out" 2>&1; then
-  echo "  ✗ case 9a: check.sh PASSED with an unpinned gen/LTLAcc/Rogue.lean"; exit 1
+if SKIP_FIDELITY=1 "$T/check.sh" > "$T/check9.out" 2>&1; then
+  echo "  ✗ case 9: check.sh PASSED with unmanifested gen/LTLAcc/Rogue.lean"; exit 1
 fi
-grep -q "does not match HARNESS.sha256" "$T/check9a.out" || {
-  echo "  ✗ case 9a: check.sh failed without the harness-set diagnosis"; tail -5 "$T/check9a.out"; exit 1; }
-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)"
+grep -q "DEAD FILE (gen): gen/LTLAcc/Rogue.lean" "$T/check9.out" || {
+  echo "  ✗ case 9: check.sh failed without DEAD FILE (gen) diagnosis"; tail -5 "$T/check9.out"; exit 1; }
+echo "  ✓ case 9 unmanifested gen module: check.sh dies with DEAD FILE (gen)"
 
 rm -rf "$WORK"
 trap - ERR
-echo "=== SELF-TEST GREEN: 10 attack cases defeated + positive control ==="
+echo "=== SELF-TEST GREEN: 9 attack cases defeated + positive control ==="

verification/selftest_statements.sh

@@ -1,147 +0,0 @@
-#!/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