From a6e5e89120ade97a452a6f930a7f6afba03789b5 Mon Sep 17 00:00:00 2001 From: mrwulf Date: Tue, 4 Aug 2026 12:58:28 +0200 Subject: [PATCH] verification: lifted phases run under the buttons shell options, enforced in lift-guard MIME-Version: 1.0 Content-Type: text/plain; charset=UTF-8 Content-Transfer-Encoding: 8bit A lift is evidence about the shipping gate only if it executes the way the shipping gate executes. Every button here runs `set -euo pipefail`. Eighteen lift sites prefixed their driver with `set -uo pipefail` and no -e — four per fork (selftest-harness, selftest-scalar-statements, selftest-statements twice) and both accumulator lifts — while sixteen other sites got it right. The estate did it both ways, which is what made this a defect and not a convention. Without -e a failing command does not abort: execution continues and the driver returns the LAST command status. A lifted phase can therefore reach a verdict the shipping phase would never reach while the self-test reports the gate "works". selftest_statements.sh:27 claims the tested logic IS the shipping logic; in this respect it was not. NO VERDICT CHANGED. Every self-test that passed before passes now, at the same timings, so -e was not masking a false green at these commits. The defect was fidelity and the claim is no larger than that. The durable part is not the 18 edits. lift-guard.sh already inspects every driver, so it now REFUSES any lift whose driver does not enable errexit and prints the drivers actual shell options. Negative-tested four ways: no -e rejects, `set -euo` passes, bare `set -e` passes, no set line at all rejects. Byte-identical across the four forks. The nineteenth lift someone writes fails closed rather than silently testing a more permissive shell. Certified by the round-15 sweep: 50/50 GREEN, six repositories, both buttons and every self-test, exit 0. Registered and NOT fixed here: ltl-accumulator-verified has no lift-guard.sh at all and calls it zero times, so its two lifts remain unguarded — the one place this class can still recur silently. Co-Authored-By: Claude Opus 4.8 --- verification/HARNESS.sha256 | 8 +++---- verification/lift-guard.sh | 25 ++++++++++++++++++++++ verification/selftest-harness.sh | 2 +- verification/selftest-scalar-statements.sh | 2 +- verification/selftest-statements.sh | 4 ++-- 5 files changed, 33 insertions(+), 8 deletions(-) diff --git a/verification/HARNESS.sha256 b/verification/HARNESS.sha256 index a3f957a..16f14b5 100644 --- a/verification/HARNESS.sha256 +++ b/verification/HARNESS.sha256 @@ -8,7 +8,7 @@ f14fd3c7ec25e96776c29a3899fe815c8899f70f00e8b820f1985d4ff784647c inventory-allo 8e2950712ce39ace9cffd3bb58a13984832ff7f3f43ba7b68aa2b1eaa2bc2116 inventory-allowlist.txt 3ebc8027f14c9e037f36322ef4119183c33214658efcc1a7bc985a98a9c32e4e inventory_gate.sh 736ea4be712e1b5bcda10ecb466f0dec7008a2a36eabdfd77563976299c43cce lean-guard -cad0ae17ce506e1defeab3b9799993b3a2251c055247695832ecae2c2617772f lift-guard.sh +4f61c1135f8afc615e686bd267a062229bf349416caebe070eafca510036d1a4 lift-guard.sh 1942177f13d6ae229d87a3b0b33f7fbb4b2ae20fe1059cc83010e73f6a156427 model-correspondence.py 1757e9c7d43aacc6d5930af62f6450ac336f7e881350ef0e5af35015442358dd MODEL-CORRESPONDENCE.txt 79a001107928713a22e679e4c4028549df76d0733455bb9937a4f438a0c315c8 Proofs/Audit.lean @@ -21,9 +21,9 @@ ecf3a3f87228f27fdfd25cb5104d04e0d90b7344b2ecee9c0138ca6b373838d0 SCALAR-AUDIT-M bf71e8d4eb312ebc687bf7e218d90b910543cd92e782078174868d012aca7250 selftest-auditonly.sh 6de61b2b08ab6e05c7d38377ea8f70178da4a105bb1df21c6ba6bc05a647090d selftest-axgate.sh 7822c007d12d7be70003ea9de234102a2c4165cfab65a108e2960e51b87bee82 selftest-correspondence.sh -41d16df48b15b99512d10a805bb811db301e9d9c8b00e5e3e0186f0110d3b71a selftest-harness.sh +8ca2bec8cdf88d9b46e6db1481839a60ac684dad242cd33859243750a3360ad4 selftest-harness.sh 1df031a075fc438c5229d01cbc44ee6ac489a272cd736624f7ca45ef1a4ddb7f selftest-inventory.sh -acfa40b0f45bf7969dd6e2a26ea72e9eaf824cedb695e498f863360772fd7c06 selftest-scalar-statements.sh +acd485670e1022270819f72fdb1aee9ce044ab9f53158300fccc69982fa37d43 selftest-scalar-statements.sh fc6d2905871500f2ee9c3f308fd8300cfcd1a7fa854d399d13812f7e2282f1fd selftest-shapes.sh -eb7367a1494f5203f0cbeace78c9522608d51825fdcbb7ae40962d2380a7bc79 selftest-statements.sh +560987651864f21bb042fc20839a03c34ce7155893b506cf060717e6d645b6c6 selftest-statements.sh 7603b82c9c29a27f6659b8878d1a2e2365afb6541c3c5b2698ab2fee21bb2bde selftest-tiers.sh diff --git a/verification/lift-guard.sh b/verification/lift-guard.sh index c670242..b6bee45 100755 --- a/verification/lift-guard.sh +++ b/verification/lift-guard.sh @@ -72,6 +72,31 @@ 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() diff --git a/verification/selftest-harness.sh b/verification/selftest-harness.sh index 091c2fb..c393266 100755 --- a/verification/selftest-harness.sh +++ b/verification/selftest-harness.sh @@ -43,7 +43,7 @@ PAYLOAD="$STASH/payload.sh" 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' > "$PAYLOAD" { - echo 'set -uo pipefail' + echo 'set -euo pipefail' # -e matches the button; see lift-drivers-drop-errexit echo "HERE=\"$HERE\"" cat "$PAYLOAD" } > "$DRIVER" diff --git a/verification/selftest-scalar-statements.sh b/verification/selftest-scalar-statements.sh index f32713e..07cc096 100755 --- a/verification/selftest-scalar-statements.sh +++ b/verification/selftest-scalar-statements.sh @@ -51,7 +51,7 @@ PAYLOAD="$STASH/payload.sh" build_driver() { awk '/^# ── Phase 3c/{f=1} f&&/^# ── (Phase |Phases end)/&&!/Phase 3c/{exit} f{print}' \ "$HERE/check-scalar.sh" > "$PAYLOAD" - { echo 'set -uo pipefail' + { echo 'set -euo pipefail' # -e matches the button; see lift-drivers-drop-errexit echo 'source ~/aeneas-toolchain/env.sh' echo "HERE=\"$HERE\"" echo 'AENEAS_LEAN="$AENEAS_HOME/backends/lean"' diff --git a/verification/selftest-statements.sh b/verification/selftest-statements.sh index 3659543..8eaba27 100755 --- a/verification/selftest-statements.sh +++ b/verification/selftest-statements.sh @@ -50,7 +50,7 @@ DRIVER0B="$STASH/phase0b.sh" PAYLOAD0B="$STASH/payload0b.sh" sed -n '/^# ── Phase 0b/,/^# ── Phase 1/p' "$HERE/check.sh" | sed '$d' > "$PAYLOAD0B" { - echo 'set -uo pipefail' + echo 'set -euo pipefail' # -e matches the button; see lift-drivers-drop-errexit echo "HERE=\"$HERE\"" cat "$PAYLOAD0B" } > "$DRIVER0B" @@ -69,7 +69,7 @@ build_driver() { awk '/^# ── Phase 3c/{f=1} f&&/^# ── (Phase |Phases end)/&&!/Phase 3c/{exit} f{print}' "$HERE/check.sh" \ | sed "s|\"\$0\"|\"$HERE/check.sh\"|g" > "$PAYLOAD" { - echo 'set -uo pipefail' + echo 'set -euo pipefail' # -e matches the button; see lift-drivers-drop-errexit echo 'source ~/aeneas-toolchain/env.sh' echo "HERE=\"$HERE\"" echo 'AENEAS_LEAN="$AENEAS_HOME/backends/lean"'