verification: lifted phases run under the buttons shell options, enforced in lift-guard

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 <noreply@anthropic.com>

verification/HARNESS.sha256

@@ -8,7 +8,7 @@ a0fb8a1a99bc991870b493796bf7bfe09463413298d83c6ae73a269712f96b55  inventory-allo
 86ee83b703d17c1f04af654657219b344b0076bc994c0b791ca6b6c5a0090d4f  inventory-allowlist.txt
 3ebc8027f14c9e037f36322ef4119183c33214658efcc1a7bc985a98a9c32e4e  inventory_gate.sh
 736ea4be712e1b5bcda10ecb466f0dec7008a2a36eabdfd77563976299c43cce  lean-guard
-cad0ae17ce506e1defeab3b9799993b3a2251c055247695832ecae2c2617772f  lift-guard.sh
+4f61c1135f8afc615e686bd267a062229bf349416caebe070eafca510036d1a4  lift-guard.sh
 1942177f13d6ae229d87a3b0b33f7fbb4b2ae20fe1059cc83010e73f6a156427  model-correspondence.py
 855134c50bc2ce374eb935058f808264ea6de5ee328ef766956e7e54366f75fe  MODEL-CORRESPONDENCE.txt
 772ca6dd22443c83dc35d5428598c8d17a01c69db5be008474d06476fa66f7f8  Proofs/Audit.lean
@@ -20,9 +20,9 @@ f921d028149e41016c75db2d316f26450768c614eb8b8b9764c49da84bbf6fc8  Proofs/Invento
 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

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()

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"

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"'

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"'