diff --git a/verification/HARNESS.sha256 b/verification/HARNESS.sha256 index e8e70f8..738a8fe 100644 --- a/verification/HARNESS.sha256 +++ b/verification/HARNESS.sha256 @@ -14,5 +14,6 @@ eda93f520546a692926b2a46bcb79332e1795879e5083327a8bf2404aca5cf87 Proofs/AxiomCh 82d41c634a2e9adfc2cc74c202d025e57411687796f820765d45608f3fb4cb20 Proofs/Inventory.lean 0b8a0fc6947af1d1e600a756eb2b07dc88d189b21df3220c4501a41be8b33f1e run_bare.sh 473e2463d9c26653c8435ad6758044742f200eb13ea0db4b8f076466c08bd87a selftest_audit.sh -5d2792996d5164022591f116ce9cbd03cdee8c9b886eb4aac6fa49c9de2bac32 selftest-harness.sh -b4a3ea633ac8a38c699e10b55b040718567cb60c5f7c7439c0c9720d4c9f8554 selftest_statements.sh +733eb2cf4eaf9101433d75dbedfc45681cff44e1dbfdc841e6b9dba350ef1570 selftest-harness.sh +c85d7a0fc39fbf06ec2c85d2f42a65813c475cae7cf60e6d140948215c62eabc selftest_statements.sh +4f61c1135f8afc615e686bd267a062229bf349416caebe070eafca510036d1a4 lift-guard.sh diff --git a/verification/lift-guard.sh b/verification/lift-guard.sh new file mode 100755 index 0000000..b6bee45 --- /dev/null +++ b/verification/lift-guard.sh @@ -0,0 +1,221 @@ +#!/usr/bin/env bash +# lift-guard.sh [] +# +# Every VARIABLE the LIFTED PAYLOAD reads must be one the DRIVER defines. +# +# VARIABLES ONLY — and the emphasis is a round-8 correction (Claude, N1). A +# lifted payload also inherits FUNCTIONS, shell options, traps and a working +# directory from the script it was cut out of. This tool models none of those. +# A lifted phase calling a function defined in a neighbouring phase fails with +# `command not found`, loud under `set -e`, which is why it is not urgent; but +# the banner used to read as a completeness claim about lifting and it is a +# completeness claim about variables. +# +# 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 +# still cannot see a name built at runtime or passed through `eval`, and it +# models variables only — not functions, shell options, traps or the working +# directory a lifted phase also inherits. It is a tripwire on failure modes +# that actually occurred, not a proof of closure. +# +# Where it CANNOT bound the reads it refuses rather than staying silent: +# indirect expansion (`${!name}`) is detected and fails the lift. That is the +# round-8 correction — a guard whose contract is "does not miss a dependency" +# must say so when it cannot honour it, instead of shrugging. +# ─────────────────────────────────────────────────────────────────────────── +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 + +# ── The driver must run the phase under the SAME shell options as the button ── +# A lift is only evidence about the shipping gate if it executes the way the +# shipping gate executes. Every button in this estate runs `set -euo pipefail`. +# Eighteen lift sites prefixed their driver with `set -uo pipefail` and no -e +# (four per fork, two in the accumulator) while sixteen others got it right, so +# the estate did it both ways and the self-tests silently ran a more permissive +# shell than the phase they claim to test: without -e a failing command does not +# abort, execution continues, and the driver returns the LAST command's status. +# A lifted phase can therefore reach a verdict the shipping phase would never +# reach, while the self-test reports the gate "works". +# +# This lives here rather than in each self-test because the same defect appeared +# in eighteen places and would return the nineteenth time someone writes a lift. +# Checked on the DRIVER, which is what bash actually executes; the payload is +# lifted verbatim and carries no `set` line of its own. +if ! grep -qE '^[[:space:]]*set[[:space:]]+-[a-z]*e' "$DRIVER"; then + echo "FATAL: lift-guard: the driver for $LABEL does not enable errexit." + echo " The button runs 'set -euo pipefail'; this driver does not set -e, so" + echo " the lifted phase would run past a failure the shipping phase aborts on" + echo " and the test would report a verdict the button cannot produce." + echo " Driver's shell options:" + grep -nE '^[[:space:]]*set[[:space:]]+-' "$DRIVER" | sed 's/^/ /' || echo " (none)" + exit 1 +fi + +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)) + +# ARITHMETIC CONTEXTS READ NAMES WITHOUT A `$`. Round-8 review (Claude, N1): +# echo $((X + 1)) reads X +# (( Y > 0 )) && ... reads Y +# and the pattern above cannot see either, because the character after `$` is +# `(`. This is the guard's own failure mode — a phase growing a dependency the +# guard is blind to — and `if [ $((inm + ins)) -eq 0 ]` is already live in +# check.sh's Phase 1b. Not lifted today, which made it latent, not absent. +for expr in (re.findall(r'\$\(\((.*?)\)\)', payload, re.S) + + re.findall(r'(? "$PAYLOAD" { echo 'set -euo pipefail' # -e matches the button; see lift-drivers-drop-errexit 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' + cat "$PAYLOAD" } > "$DRIVER" -if [ "$(grep -c . "$DRIVER")" -lt 20 ]; then +if [ "$(grep -c . "$PAYLOAD")" -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 +"$HERE/lift-guard.sh" "$PAYLOAD" "$DRIVER" "check.sh Phase 0c" || exit 1 expect() { # expect