diff --git a/verification/HARNESS.sha256 b/verification/HARNESS.sha256 index 197378f..4fb93b6 100644 --- a/verification/HARNESS.sha256 +++ b/verification/HARNESS.sha256 @@ -1,12 +1,13 @@ 12dc724bffd590e6f706573d97bf07425b8f268a1be2d72a3bbd9aef48f9c277 AUDIT-MANIFEST.txt 6b25b7e261633f4fa703de0be1dfd3c263d043107e3b3225d4c5079a93b6a64d check-scalar.sh -aae30cc435865688ed12a5a8071f7c7c41f157584bebeddc77e9c20c2c88ea44 check.sh +b55a405e1af95d28a6d222f4cfc1d1e33428da2650b7a6668ecdda852eea6330 check.sh fdd1337f1f44fa73fdb14e6cda001e4e7358513b9c178c517456b24511d96a8e extract.sh 52afbe130c5551686f45643a35065729fd5bb8166b5fa3db67b74c60ba3eff62 GEN-MODEL.sha256 6033c86eb08b4c2ea0bd7cdbd2cfb5748059179ece3efa9673270dc17a2e38b9 inventory-allowlist-scalar.txt 80cdd232c9a0f3078b2b712957e34797add5421b51bd695a151bf64a7855687a inventory-allowlist.txt 0bb01bc4abaafa8537d460682004d1f336980b28bc4fe1968bcc9c3bc3bc71ba inventory_gate.sh 736ea4be712e1b5bcda10ecb466f0dec7008a2a36eabdfd77563976299c43cce lean-guard +b982bd1aa56b0648b10516985a2e0f6a9cacff4e1d19b441dadc5b35d69ec732 lift-guard.sh 7a9c89cf2b96313bd4bcddb534e8d06724bd7250234e670baadf6a9b0d1fbf81 model-correspondence.py 6c1503880f38e4b827df32a4854902b66b7b2ea4783f9eb5c44e691a2c293ae1 MODEL-CORRESPONDENCE.txt 34c102ca7a38719ef8890b8dedd3f07c3f92e10ae4a1ce2c47a7db4d53523354 Proofs/Audit.lean @@ -15,10 +16,10 @@ dd957bb260df0bd33266418a6594b45720c4754c5687bfab4ecb30ad573a286c Proofs/Invento 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 5026bf7..342ae9c 100755 --- a/verification/check.sh +++ b/verification/check.sh @@ -689,6 +689,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 @@ -700,6 +736,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". @@ -731,43 +771,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