From 5707189ef509cdc8b08b85c24582714be0e28baa Mon Sep 17 00:00:00 2001 From: mrwulf Date: Sun, 2 Aug 2026 13:07:28 +0200 Subject: [PATCH] verification: derive lift dependencies instead of hand-keeping them MIME-Version: 1.0 Content-Type: text/plain; charset=UTF-8 Content-Transfer-Encoding: 8bit Round-9 swept all ten instruments per fork instead of only the two buttons, and found selftest-axgate.sh red in all four. Root cause, identical to the KERNLOG defect fixed the day before: a self-test lifts one phase out of check.sh and supplies its variables from a HAND-WRITTEN preamble, and the phase later grew a dependency nobody told the preamble about. Phase 2b stopped globbing Proofs/*.olean and started reading $PROOFS by membership. Bash does not error on an unset array under `set -u` — it expands to nothing — so the gate silently received expected := [".olean"] one entry with an empty name, and rejected the baseline via its own fail-closed absence check. Exit code right, reason wrong. · lift-guard.sh (new, pinned): derives every variable the lifted payload reads, subtracts what the driver defines, and fails AT LIFT TIME naming the remainder. Wired into all five lifting self-tests; selftest-shapes.sh drops its inline copy. One implementation, not five, since drifting out of sync is the entire failure mode. · selftest-axgate.sh: lifts PROOFS verbatim, and its case 2 now poisons a MANIFESTED leaf module rather than adding a stray file. The stray-file attack was a no-op against membership semantics — that is the dead-file gate's job, proven by selftest-harness case 8 — and it is also the weaker attack, since adding files to Proofs/ must clear a gate that editing an already-manifested module does not. · Phase 2c's accounting identity moves behind its own marker with its own ACCTFAIL verdict, so the phase is liftable by construction rather than by a self-test knowing where to stop. Truncating the lift range alone would have dropped Phase 2c's own verdict and left the test unable to fail. · The other four lifting self-tests assert on the PAYLOAD rather than the assembled driver, so a marker in the preamble cannot satisfy a check meant to prove the lift landed. Certified: 8/8 self-tests green in all four forks (~212 assertions, none failing); check.sh bytes unchanged and still matching the pin written before the 3h08m round-9 sweep, whose 36 GREEN button rows therefore stand. --audit-only re-run against the new HARNESS.sha256 in every fork. Co-Authored-By: Claude Opus 4.8 --- verification/HARNESS.sha256 | 15 +-- verification/check.sh | 72 +++++++++----- verification/lift-guard.sh | 112 +++++++++++++++++++++ verification/selftest-axgate.sh | 126 +++++++++++++++++++----- verification/selftest-correspondence.sh | 9 +- verification/selftest-harness.sh | 9 +- verification/selftest-shapes.sh | 39 +++++++- verification/selftest-statements.sh | 27 +++-- verification/selftest-tiers.sh | 17 +++- 9 files changed, 347 insertions(+), 79 deletions(-) create mode 100755 verification/lift-guard.sh diff --git a/verification/HARNESS.sha256 b/verification/HARNESS.sha256 index 47580e6..9b037d0 100644 --- a/verification/HARNESS.sha256 +++ b/verification/HARNESS.sha256 @@ -1,12 +1,13 @@ 6c821b8e465d3b394cb3cbb4bb3757791ace064b6d1b273ba9a41402dac74e24 AUDIT-MANIFEST.txt d505e4dd9283673e78fb34e25780c94334e03de4ad20400f8289d594ab004daf check-scalar.sh -afe5511860d91f857f1179755facc83542f6bc75620263b264fdac69f05fa6b8 check.sh +9b0fa638179282b4dd74a6aad3d140ad1299b4e092d1f19dc337832c172947e3 check.sh 71244d824847311bcb3ba8ad1f1905c4b24fe8f015e3230969914019cb628b61 extract.sh c9672a28825cd1d4055fb9efbb4a1d94c921c7b5c79e4cd5d0626ba061e554c1 GEN-MODEL.sha256 e6f31b4303f5a344781d353f1dddefc185876df470e27b285c81556621e65c05 inventory-allowlist-scalar.txt 86ee83b703d17c1f04af654657219b344b0076bc994c0b791ca6b6c5a0090d4f inventory-allowlist.txt 0bb01bc4abaafa8537d460682004d1f336980b28bc4fe1968bcc9c3bc3bc71ba inventory_gate.sh 736ea4be712e1b5bcda10ecb466f0dec7008a2a36eabdfd77563976299c43cce lean-guard +b982bd1aa56b0648b10516985a2e0f6a9cacff4e1d19b441dadc5b35d69ec732 lift-guard.sh 7a9c89cf2b96313bd4bcddb534e8d06724bd7250234e670baadf6a9b0d1fbf81 model-correspondence.py 1ba5ff18b170e3139e10805c221b03188ca8c2a433ee807d7139b3afb9df2437 MODEL-CORRESPONDENCE.txt 772ca6dd22443c83dc35d5428598c8d17a01c69db5be008474d06476fa66f7f8 Proofs/Audit.lean @@ -14,10 +15,10 @@ e6f31b4303f5a344781d353f1dddefc185876df470e27b285c81556621e65c05 inventory-allo 660d35343f5673d4bc854787b6a34063c956567bd7e2eb62955a92e3c55bfa6b Proofs/Inventory.lean 6fbeb50d3951c7c5ac593f6dec91096fc798123ed0c500fdfa39fb20b118ea78 Proofs/InventoryScalar.lean bf71e8d4eb312ebc687bf7e218d90b910543cd92e782078174868d012aca7250 selftest-auditonly.sh -eb81df6d154b413b243ad282e3b1bfec92fde158a215f89993c08586a121f171 selftest-axgate.sh -9bf6559fb364bbfdec94649c459215061df80f1f813b4b0ec869c7f8e18a8cfc selftest-correspondence.sh -3d5898161d663eccad162269a5a6c102319077e22e1f2d89a8bfcab6926d29f6 selftest-harness.sh +6de61b2b08ab6e05c7d38377ea8f70178da4a105bb1df21c6ba6bc05a647090d selftest-axgate.sh +7822c007d12d7be70003ea9de234102a2c4165cfab65a108e2960e51b87bee82 selftest-correspondence.sh +41d16df48b15b99512d10a805bb811db301e9d9c8b00e5e3e0186f0110d3b71a selftest-harness.sh 1df031a075fc438c5229d01cbc44ee6ac489a272cd736624f7ca45ef1a4ddb7f selftest-inventory.sh -26f10a749e03cecd7ad173d0d621498386444d8e347f606a99a2fadb06738d86 selftest-shapes.sh -2c591fb2a0cc50cfdf76c3328e5d72d52b69c02f5b230ebc55c977d6570ecc0f selftest-statements.sh -df2389909839c5c2275097044b112bd254e48aa21b4b8f6c1430847c0a0c7cc6 selftest-tiers.sh +fc6d2905871500f2ee9c3f308fd8300cfcd1a7fa854d399d13812f7e2282f1fd selftest-shapes.sh +eb7367a1494f5203f0cbeace78c9522608d51825fdcbb7ae40962d2380a7bc79 selftest-statements.sh +7603b82c9c29a27f6659b8878d1a2e2365afb6541c3c5b2698ab2fee21bb2bde selftest-tiers.sh diff --git a/verification/check.sh b/verification/check.sh index 308e797..c086f1e 100755 --- a/verification/check.sh +++ b/verification/check.sh @@ -690,6 +690,42 @@ OBS=$(mktemp /tmp/check-inv-obs-XXXX.log) grep '^INV|' "$INVLOG" > "$OBS" echo "INV-COUNT|${SUM:-0}" >> "$OBS" "$HERE/inventory_gate.sh" "$OBS" "$HERE/inventory-allowlist.txt" || INVFAIL=1 + +# The drivers' corpus lists must together BE the compile manifest, minus the +# audit infrastructure and the scalar layer. Checked in both directions so a +# module cannot fall between the two drivers, and NO SILENT TRUNCATION: what +# this phase does not cover is named on stdout every run. +COVERED=$(for d in $DRIVERS; do grep -ohE '`Proofs\.[A-Za-z0-9]+' "$HERE/Proofs/$d.lean"; done \ + | sed 's/`Proofs\.//' | sort -u) +for m in "${PROOFS[@]}"; do + case "$m" in Audit|Inventory|InventoryBasic|InventoryCore) continue;; esac + grep -qx "$m" <<<"$COVERED" || { echo " UNINVENTORIED: $m is compiled by this script but no driver covers it"; INVFAIL=1; } +done +while read -r m; do + [ -z "$m" ] && continue + case " ${PROOFS[*]} " in (*" $m "*) ;; (*) echo " PHANTOM: driver claims $m, which this script does not compile"; INVFAIL=1;; esac +done <<<"$COVERED" +for f in "$HERE"/Proofs/*.lean; do + b=$(basename "$f" .lean) + case "$b" in Audit|Inventory|InventoryBasic|InventoryCore|InventoryScalar) continue;; esac + grep -qx "$b" <<<"$COVERED" || echo " NOT INVENTORIED HERE (separate button): Proofs/$b.lean" +done +[ "$INVFAIL" = 0 ] || { echo "INVENTORY COVERAGE FAILED"; exit 1; } + +# ── Phase 2c-accounting: every kernel constant is accounted for ───────────── +# SEPARATED FROM PHASE 2c DELIBERATELY, and the reason is a self-test that +# could not pass (round-7 finding F5). This block reads $KERNLOG, created one +# phase earlier in Phase 2b. selftest-shapes.sh lifts "Phase 2c" by text marker +# and runs it standalone; once this block lived inside that range, the lifted +# driver died on its first `$KERNLOG` expansion under `set -u`. The test failed +# loudly in all four forks from the moment the block was added — so the shapes +# property went unverified, though it never produced a false green. +# +# Truncating the lift is NOT the fix: Phase 2c's own verdict +# (`INVENTORY COVERAGE FAILED`) sits after this block, so a shorter range drops +# the phase's ability to fail at all. Instead the block gets its own marker and +# its own verdict, which makes Phase 2c liftable BY CONSTRUCTION rather than by +# the self-test knowing where to stop. # ── THE ACCOUNTING IDENTITY ─────────────────────────────────────────────── # Every declaration the kernel saw must be accounted for by exactly one walk: # the corpus inventory, or the instruments' own surface. Until 2026-07-31 the @@ -701,6 +737,10 @@ echo "INV-COUNT|${SUM:-0}" >> "$OBS" # indentation) but it was an unexamined remainder, and an unexamined remainder # is where the next defect hides. # +# Stating it as an IDENTITY rather than as two separate counts is what makes it +# fail closed: a declaration that slipped out of both walks leaves the sum +# short, and one counted twice leaves it long. +# # COUNT DISTINCT CONSTANTS, NOT PHYSICAL DECLARATIONS. The two sides of this # identity were, at first, counting different things, and the gap was papered # over with a `+ N_DRIVERS` term justified as a "self-observation blind spot". @@ -732,43 +772,25 @@ LC_ALL=C grep '^KERNEL-NAME|' "$KERNLOG" | cut -d'|' -f2 | LC_ALL=C sort -u > "$ UNACCOUNTED=$(LC_ALL=C comm -23 "$KERN_NAMES" "$ACCT_NAMES") if [ "$DRV_TRAILERS" -ne "$N_DRIVERS" ]; then echo " DRIVER SURFACE INCOMPLETE: expected a trailer from each of the $N_DRIVERS driver(s), saw $DRV_TRAILERS" - INVFAIL=1 + ACCTFAIL=1 elif [ "${DRV_SUM:-0}" != "$N_DRV" ]; then echo " DRIVER SURFACE TRUNCATED: trailers sum to ${DRV_SUM:-0}, observed $N_DRV lines" - INVFAIL=1 + ACCTFAIL=1 elif [ ! -s "$KERN_NAMES" ]; then echo " ACCOUNTING FAILED: Phase 2b reported no constant names — the scan was vacuous" - INVFAIL=1 + ACCTFAIL=1 elif [ -n "$UNACCOUNTED" ]; then echo " ACCOUNTING FAILED: the kernel holds constants that neither walk accounts for:" printf '%s\n' "$UNACCOUNTED" | head -20 | sed 's/^/ /' - INVFAIL=1 + ACCTFAIL=1 else echo " accounting: every one of $(wc -l < "$KERN_NAMES") kernel constants is covered by the corpus inventory or the instrument surface" fi rm -f "$KERN_NAMES" "$ACCT_NAMES" +ACCTFAIL=${ACCTFAIL:-0} +[ "$ACCTFAIL" = 0 ] || { echo "ACCOUNTING FAILED"; rm -f "$INVLOG" "$OBS" "$KERNLOG"; exit 1; } +rm -f "$INVLOG" "$OBS" "$KERNLOG" rm -f "$INVLOG" "$OBS" "$KERNLOG" - -# The drivers' corpus lists must together BE the compile manifest, minus the -# audit infrastructure and the scalar layer. Checked in both directions so a -# module cannot fall between the two drivers, and NO SILENT TRUNCATION: what -# this phase does not cover is named on stdout every run. -COVERED=$(for d in $DRIVERS; do grep -ohE '`Proofs\.[A-Za-z0-9]+' "$HERE/Proofs/$d.lean"; done \ - | sed 's/`Proofs\.//' | sort -u) -for m in "${PROOFS[@]}"; do - case "$m" in Audit|Inventory|InventoryBasic|InventoryCore) continue;; esac - grep -qx "$m" <<<"$COVERED" || { echo " UNINVENTORIED: $m is compiled by this script but no driver covers it"; INVFAIL=1; } -done -while read -r m; do - [ -z "$m" ] && continue - case " ${PROOFS[*]} " in (*" $m "*) ;; (*) echo " PHANTOM: driver claims $m, which this script does not compile"; INVFAIL=1;; esac -done <<<"$COVERED" -for f in "$HERE"/Proofs/*.lean; do - b=$(basename "$f" .lean) - case "$b" in Audit|Inventory|InventoryBasic|InventoryCore|InventoryScalar) continue;; esac - grep -qx "$b" <<<"$COVERED" || echo " NOT INVENTORIED HERE (separate button): Proofs/$b.lean" -done -[ "$INVFAIL" = 0 ] || { echo "INVENTORY COVERAGE FAILED"; exit 1; } # ── Phase 2d: SEMANTIC model/template correspondence ──────────────────────── # Phase 0d asks a text scanner what the extraction's boundary looks like. This # phase asks LEAN what it actually is, and requires the two to agree. diff --git a/verification/lift-guard.sh b/verification/lift-guard.sh new file mode 100755 index 0000000..fa13632 --- /dev/null +++ b/verification/lift-guard.sh @@ -0,0 +1,112 @@ +#!/usr/bin/env bash +# lift-guard.sh [] +# +# Every variable the LIFTED PAYLOAD reads must be one the DRIVER defines. +# Prints the offending names and exits 1 if any are missing. +# +# ─────────────────────────────────────────────────────────────────────────── +# WHY THIS EXISTS — 2026-08-02 +# +# Five of this repository's self-tests work by lifting one phase out of +# check.sh and running it standalone against a deliberately corrupted tree. +# That is the right design: the test then attacks the SHIPPING gate rather +# than a re-implementation of it. But a lifted phase is a fragment, and it +# reads variables its neighbours defined. Each self-test therefore carries a +# hand-written preamble supplying them. +# +# A hand-written preamble is a hand-kept list, and hand-kept lists drift. Twice +# in two days a phase grew a dependency and no preamble was told: +# +# · Phase 2c grew an accounting block reading $KERNLOG, a file Phase 2b +# creates. selftest-shapes.sh died on its first expansion under `set -u`. +# It could not pass on any fork from the moment that block was added. +# +# · Phase 2b changed from globbing Proofs/*.lean to reading the $PROOFS +# membership manifest — the spelling-versus-ownership fix ScalarPackSpec +# forced. selftest-axgate.sh's preamble was never told. Bash does NOT +# error on an unset array expansion under `set -u`; it expands to nothing, +# so `printf '"%s.olean", ' "${PROOFS[@]}"` silently produced +# expected := [".olean"] +# — one entry, empty name — and the gate's own fail-closed absence check +# rejected it. The baseline went red and both attack cases were then +# rejected for the WRONG REASON. +# +# Both failed loudly rather than passing vacuously, which is the only reason +# they were not false assurance. That is luck, not design: a missing variable +# that happens to make an ATTACK case die still looks like the attack being +# caught, and only the substring assertions in each `expect` helper stand +# between that and a green test measuring nothing. +# +# The fix for the CLASS is to stop maintaining the list by hand. This tool +# derives the requirement from the two artifacts themselves, so a phase that +# grows a new dependency fails AT LIFT TIME, naming it, instead of dying +# mid-run or — worse — passing for the wrong reason. +# +# WHAT IT IS NOT. This is a shell-text approximation, not a bash parser: it +# cannot see indirect expansion, `eval`, or a name built at runtime. It is a +# tripwire on the failure mode that actually occurred twice, not a proof of +# closure. Its answer is advisory in one direction only — it can miss a +# dependency, it does not invent one, and every name it reports is a name the +# payload genuinely mentions and the driver genuinely does not set. +# ─────────────────────────────────────────────────────────────────────────── +set -euo pipefail + +PAYLOAD="${1:?usage: lift-guard.sh [phase-label]}" +DRIVER="${2:?usage: lift-guard.sh [phase-label]}" +LABEL="${3:-the lifted phase}" + +for f in "$PAYLOAD" "$DRIVER"; do + [ -s "$f" ] || { echo "FATAL: lift-guard: '$f' is missing or empty."; exit 1; } +done + +UNBOUND=$(python3 - "$PAYLOAD" "$DRIVER" <<'PYGUARD' +import re, sys +payload = open(sys.argv[1]).read() +driver = open(sys.argv[2]).read() + +# What the payload READS. Deliberately over-approximates: a name mentioned in a +# comment costs one lifted definition, a name missed costs a broken self-test. +reads = set(re.findall(r'\$\{?([A-Za-z_][A-Za-z0-9_]*)', payload)) + +# What the DRIVER defines, in every form these scripts actually use. +# An assignment may open a line OR follow `;`, `&&`, `||`, `then`, `do`, `{` — +# `TIMEOUT=$T; CORES="$C"` is one line with two of them, and a start-anchored +# pattern sees only the first. That over-strictness is not harmless: a guard +# that cries wolf gets edited away, and then it guards nothing. +assigns = set(re.findall( + r'(?:^|;|&&|\|\||\bthen\b|\bdo\b|\{)\s*([A-Za-z_][A-Za-z0-9_]*)=', + driver, re.M)) +assigns |= set(re.findall(r'\b(?:export|declare|local|readonly)\s+(?:-\w+\s+)*' + r'([A-Za-z_][A-Za-z0-9_]*)', driver)) +assigns |= set(re.findall(r'\bfor\s+([A-Za-z_][A-Za-z0-9_]*)\s+in\b', driver)) +# `read` binds names too, and it is almost never at end of line: the shape that +# matters here is `while read -r n; do`. An end-anchored pattern misses it and +# the guard then demands a definition for a loop variable the payload binds +# itself — a false alarm, which is the one failure a guard cannot afford. +for m in re.finditer(r'\bread\b((?:\s+-\w+)*(?:\s+[A-Za-z_][A-Za-z0-9_]*)+)', driver): + assigns |= set(re.findall(r'[A-Za-z_][A-Za-z0-9_]*', m.group(1))) + +# Names the driver INHERITS rather than defines: the shell's own, and the ones +# `source ~/aeneas-toolchain/env.sh` puts in the environment. Keep this list +# short and justified — every entry is a hole in the guard. +ENV = {'PWD', 'HOME', 'PATH', 'IFS', 'PIPESTATUS', 'BASH_SOURCE', 'FUNCNAME', + 'LINENO', 'RANDOM', 'SECONDS', 'OSTYPE', 'HOSTNAME', 'USER', 'SHELL', + 'TMPDIR', 'LC_ALL', 'LANG', 'BASH_REMATCH', 'REPLY', 'PS4', + 'AENEAS_HOME', 'LEAN_PATH', 'LEAN_MEM_MB', 'LEAN_TIMEOUT', + 'LEAN_MAX_CORES'} + +print(' '.join(sorted(n for n in reads - assigns - ENV if not n.isdigit()))) +PYGUARD +) + +if [ -n "$UNBOUND" ]; then + cat < "$PAYLOAD" { echo 'set -euo pipefail' echo 'source ~/aeneas-toolchain/env.sh' echo "HERE=\"$HERE\"" echo 'AENEAS_LEAN="$AENEAS_HOME/backends/lean"' echo "TIMEOUT=$TIMEOUT; CORES=\"$CORES\"" - # Stop at the NEXT phase marker, whatever it is called. A hardcoded - # terminator ("...to Phase 3") silently widens the moment a phase is - # inserted between the two: adding Phase 2c made this driver swallow 2c as - # well and die on variables that phase expects check.sh to have defined, - # which surfaced as the BASELINE failing — a self-test blaming a gate for - # its own extraction bug. - awk '/^# ── Phase 2b/{f=1} f&&/^# ── (Phase |Phases end)/&&!/Phase 2b/{exit} f{print}' "$HERE/check.sh" + # THE COMPILE MANIFEST. Phase 2b used to glob Proofs/*.lean; it now reads + # $PROOFS by MEMBERSHIP, because a glob demands artifacts this button never + # makes (the spelling-versus-ownership error ScalarPackSpec exposed). This + # preamble was not told, and bash does not error on an unset array under + # `set -u` — it expands to nothing, so the gate got `expected := [".olean"]` + # and rejected the baseline for a reason that had nothing to do with axioms. + # Lifted VERBATIM, never re-derived: a re-derivation lets this test's idea of + # the manifest drift away from the button's, and then the test checks its own + # opinion. lift-guard.sh below is what makes the omission impossible to + # repeat silently. + sed -n '/^PROOFS=(/,/^)/p' "$HERE/check.sh" + cat "$PAYLOAD" } > "$DRIVER" -if [ "$(wc -l < "$DRIVER")" -lt 40 ]; then +# Guard on the PAYLOAD, not the concatenation: a marker appearing in the +# preamble or in a lifted definition would otherwise satisfy these. +if [ "$(wc -l < "$PAYLOAD")" -lt 40 ]; then echo "FATAL: could not lift Phase 2b 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 -if [ "$(grep -c '^# ── Phase ' "$DRIVER")" -ne 1 ]; then +if [ "$(grep -c '^# ── Phase ' "$PAYLOAD")" -ne 1 ]; then echo "FATAL: the lifted block spans more than one phase; the extraction is wrong." - grep '^# ── Phase ' "$DRIVER" | sed 's/^/ /' + grep '^# ── Phase ' "$PAYLOAD" | sed 's/^/ /' exit 1 fi +grep -qF 'PROOFS=(' "$DRIVER" || { + echo "FATAL: the lift carries no 'PROOFS=(' — the compile manifest is missing."; exit 1; } +"$HERE/lift-guard.sh" "$PAYLOAD" "$DRIVER" "check.sh Phase 2b" || exit 1 expect() { # expect local name="$1" want_rc="$2" want_txt="$3" @@ -85,31 +113,79 @@ expect "baseline green, coverage reported" 0 "none is an axiom" # ── 2. The attack Phase 1's grep cannot see: an indented top-level axiom. # Lean accepts it; the repo then proves False; the source-text gate is blind. -cat > "$ATTACK" <<'EOF' +# +# THE ATTACK GOES INTO A MANIFESTED MODULE, and that is the whole point of +# this case. Until 2026-08-02 it created a NEW file, Proofs/ZZSelftestAttack +# .lean, which worked while Phase 2b globbed Proofs/*.olean. Phase 2b now +# reads $PROOFS by MEMBERSHIP, so a stray module is simply not this gate's +# business — it is the dead-file gate's, and selftest-harness.sh case 8 +# already proves check.sh dies with DEAD FILE on exactly that. Against +# membership, the stray-file attack passed the gate and the case went red. +# It is also the WEAKER attack: an adversary who can add files to Proofs/ +# has to get past the dead-file gate, whereas an adversary who edits a +# module that is already manifested does not. So the case now poisons a +# real manifested module, which is what the kernel gate exists to catch. +MANIFEST=$(sed -n '/^PROOFS=(/,/^)/p' "$HERE/check.sh" \ + | sed 's/#.*//; s/PROOFS=(//; s/)//' | tr -s ' \t' '\n' | sed '/^$/d') +# A LEAF: nothing else in the manifest imports it, so poisoning it cannot make +# a sibling's artifact stale. Smallest such module, to keep the recompile cheap. +# +# The SEARCH SET excludes Inventory* and Audit, and that exclusion is +# load-bearing: those are the aggregators, they import the whole corpus, and +# grepping them makes every module look imported. Leave them in and the loop +# finds no leaf at all — which is precisely how this case first reported +# "the corpus shape changed" against a corpus that had not changed. +SEARCHERS=$(for m in $MANIFEST; do + case $m in Inventory*|Audit) ;; *) echo "$HERE/Proofs/$m.lean";; esac + done) +_best=999999 +for m in $MANIFEST; do + case $m in Inventory*|Audit) continue;; esac + [ -f "$HERE/Proofs/$m.lean" ] || continue + grep -qE "^import Proofs\.$m\$" $SEARCHERS 2>/dev/null && continue + n=$(wc -l < "$HERE/Proofs/$m.lean") + if [ "$n" -lt "$_best" ]; then _best=$n; VICTIM=$m; fi +done +if [ -z "$VICTIM" ]; then + echo " FAIL premise: no manifested leaf module to poison — the corpus shape changed." + FAILURES=$((FAILURES+1)) +else + cp "$HERE/Proofs/$VICTIM.lean" "$STASH/victim.lean" + cp "$HERE/Proofs/$VICTIM.olean" "$STASH/victim.olean" + cat >> "$HERE/Proofs/$VICTIM.lean" <<'EOF' + namespace ZZSelftestAttack axiom cheat : ∀ (P : Prop), P theorem repo_proves_false : False := cheat _ end ZZSelftestAttack EOF -if grep -rnE '^(private |protected |noncomputable )*axiom ' "$HERE"/Proofs/*.lean >/dev/null 2>&1; then - echo " FAIL premise: Phase 1's grep sees the attack — this test no longer tests what it claims" - FAILURES=$((FAILURES+1)) -else - echo " ok premise: Phase 1's source-text grep is blind to this attack" + if grep -rnE '^(private |protected |noncomputable )*axiom ' "$HERE"/Proofs/*.lean >/dev/null 2>&1; then + echo " FAIL premise: Phase 1's grep sees the attack — this test no longer tests what it claims" + FAILURES=$((FAILURES+1)) + else + echo " ok premise: Phase 1's source-text grep is blind to this attack" + fi + (cd "$AENEAS_LEAN" && lake env bash -c " + set -euo pipefail + cd '$HERE/gen' && export LEAN_PATH=\"\$LEAN_PATH:\$PWD:$HERE\" + cd '$HERE' + LEAN_TIMEOUT=$TIMEOUT LEAN_MAX_CORES=$CORES '$HERE/lean-guard' 'Proofs/$VICTIM.lean' + ") >/dev/null 2>&1 || { echo " FAIL setup: the poisoned module did not compile"; FAILURES=$((FAILURES+1)); } + expect "indented axiom in a manifested module caught kernel-side" 1 "AXIOM DECLARED under Proofs/" + cp "$STASH/victim.lean" "$HERE/Proofs/$VICTIM.lean" + cp "$STASH/victim.olean" "$HERE/Proofs/$VICTIM.olean" fi -(cd "$AENEAS_LEAN" && lake env bash -c " - set -euo pipefail - cd '$HERE/gen' && export LEAN_PATH=\"\$LEAN_PATH:\$PWD:$HERE\" - cd '$HERE' - LEAN_TIMEOUT=$TIMEOUT LEAN_MAX_CORES=$CORES '$HERE/lean-guard' 'Proofs/ZZSelftestAttack.lean' -") >/dev/null 2>&1 || { echo " FAIL setup: the attack module did not compile"; FAILURES=$((FAILURES+1)); } -expect "indented axiom caught kernel-side" 1 "AXIOM DECLARED under Proofs/" -rm -f "$ATTACK" "${ATTACK%.lean}.olean" # ── 3. Vacuity: delete a compiled module. "Nothing found" must not pass for # "nothing wrong" — the gate has to notice it stopped covering something. +# The expected wording tracks the SHIPPING diagnostic: it read "COVERAGE +# MISMATCH" while the gate compared two counts, and became a per-module +# message when the gate started walking $PROOFS by membership. Asserting +# the reason and not merely the exit code is deliberate — a gate that goes +# red for an unrelated cause has not been tested. mv "$HERE/Proofs/FeQ.olean" "$STASH/FeQ.olean" -expect "missing .olean is a failure, not a vacuous pass" 1 "COVERAGE MISMATCH" +expect "missing .olean is a failure, not a vacuous pass" 1 \ + "is in the compile manifest but its artifact is absent" mv "$STASH/FeQ.olean" "$HERE/Proofs/FeQ.olean" # ── 4. Litter: neither path may leave the temp gate source or its artifact diff --git a/verification/selftest-correspondence.sh b/verification/selftest-correspondence.sh index a826900..5310a81 100755 --- a/verification/selftest-correspondence.sh +++ b/verification/selftest-correspondence.sh @@ -44,14 +44,19 @@ cp "$HERE/$MODEL_REL" "$STASH/model" cp "$HERE/$TMPL_REL" "$STASH/tmpl" # Phase 0d lifted from the shipping button. +awk '/^# ── Phase 0d/{f=1} f&&/^# ── (Phase 1|Phases end)/{exit} f{print}' \ + "$HERE/check.sh" > "$STASH/payload.sh" { echo 'set -euo pipefail' echo "HERE=\"$HERE\"" - awk '/^# ── Phase 0d/{f=1} f&&/^# ── (Phase 1|Phases end)/{exit} f{print}' "$HERE/check.sh" + cat "$STASH/payload.sh" } > "$STASH/p0d.sh" +# Assert on the PAYLOAD, not the concatenation: a marker appearing in the +# preamble would otherwise satisfy a check meant to prove the lift landed. for want in 'Phase 0d' 'MODEL CORRESPONDENCE' 'model-correspondence.py'; do - grep -qF "$want" "$STASH/p0d.sh" || { + grep -qF "$want" "$STASH/payload.sh" || { echo "FATAL: the lifted driver has no '$want' — check.sh's phase markers moved."; exit 1; } done +"$HERE/lift-guard.sh" "$STASH/payload.sh" "$STASH/p0d.sh" "check.sh Phase 0d" || exit 1 expect() { # expect