mirror of
https://github.com/saymrwulf/ltl-accumulator-verified.git
synced 2026-09-03 19:53:48 +00:00
mrwulf
a0d11b44d9
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>
147 lines
7.3 KiB
Bash
Executable file
147 lines
7.3 KiB
Bash
Executable file
#!/usr/bin/env bash
|
|
# ─────────────────────────────────────────────────────────────────────────────
|
|
# selftest_statements.sh — adversarial self-test of check.sh Phase 3d.
|
|
#
|
|
# WHY A SECOND SELF-TEST. selftest_audit.sh attacks the coverage gate, which
|
|
# pins every constant's NAME, KIND and AXIOM CONE, both directions. That gate
|
|
# is strong and none of its nine attacks defeat it. It is also blind to what a
|
|
# declaration SAYS, and this script demonstrates that with a real, compiling
|
|
# edit rather than an argument:
|
|
#
|
|
# `LTLAcc.pinAccept` is a specification definition. Wrapping one branch of
|
|
# its body in `id (…)` is definitionally equal, so every downstream proof
|
|
# still compiles; the name, the kind, the type and the axiom cone are all
|
|
# unchanged. The inventory gate reports 222 constants, environment ==
|
|
# allowlist, GREEN. Only the statement digest sees it.
|
|
#
|
|
# That edit is deliberately harmless. The point is that the ONLY thing
|
|
# standing between it and a genuinely vacuous redefinition is the digest.
|
|
#
|
|
# Cases:
|
|
# 0 positive control: pristine tree passes Phase 3d
|
|
# 1 defeq body edit: old gate PASSES (asserted), Phase 3d FAILS (asserted)
|
|
# 2 committed AUDIT-MANIFEST.txt hand-edited → COMMITTED BLOCK STALE
|
|
# 3 statement block truncated → BLOCK TRUNCATED
|
|
# 4 a constant inventoried but carrying no statement → COVERAGE GAP
|
|
#
|
|
# Phase 3d is lifted out of check.sh at run time, so the tested logic IS the
|
|
# shipping logic. Run AFTER a green check.sh. All Lean work via lean-guard.
|
|
# ─────────────────────────────────────────────────────────────────────────────
|
|
set -uo pipefail
|
|
AENEAS_ENV="${AENEAS_ENV:-$HOME/aeneas-toolchain/env.sh}"
|
|
[ -f "$AENEAS_ENV" ] || { echo "FATAL: Aeneas environment not found: $AENEAS_ENV"; exit 1; }
|
|
source "$AENEAS_ENV"
|
|
SRC="$(cd "$(dirname "$0")" && pwd)"
|
|
AENEAS_LEAN="$AENEAS_HOME/backends/lean"
|
|
CORES="${LEAN_MAX_CORES:-0-3}"
|
|
FAILURES=0
|
|
|
|
WORK=$(mktemp -d /tmp/acc-stmt-selftest-XXXX)
|
|
trap 'rm -rf "$WORK"' EXIT
|
|
echo "=== statement-binding self-test (scratch: $WORK) ==="
|
|
cp -a "$SRC" "$WORK/verification"
|
|
T="$WORK/verification"
|
|
cp "$T/Proofs/PinStore.lean" "$T/PinStore.pristine"
|
|
cp "$T/AUDIT-MANIFEST.txt" "$T/MANIFEST.pristine"
|
|
|
|
# Phase 3d, lifted verbatim from the shipping button. HERE and INVLOG are the
|
|
# two variables it reads from its surroundings.
|
|
DRIVER="$T/phase3d.sh"
|
|
{
|
|
echo 'set -euo pipefail' # -e matches the button; see lift-drivers-drop-errexit
|
|
echo "HERE=\"$T\""
|
|
echo 'INVLOG="$1"'
|
|
sed -n '/^# -- Phase 3d/,/^# -- Phase 4/p' "$SRC/check.sh" | sed '$d'
|
|
} > "$DRIVER"
|
|
if [ "$(wc -l < "$DRIVER")" -lt 40 ]; then
|
|
echo "FATAL: could not lift Phase 3d 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
|
|
|
|
# Recompile the edited leaf module + the inventory into $T/inv.out.
|
|
build_inventory() {
|
|
cd "$AENEAS_LEAN"
|
|
lake env bash -c "
|
|
set -euo pipefail
|
|
cd '$T' && export LEAN_PATH=\"\$LEAN_PATH:$T/gen:$T\"
|
|
LEAN_TIMEOUT=600 LEAN_MAX_CORES=$CORES '$T/lean-guard' Proofs/PinStore.lean >/dev/null 2>&1
|
|
LEAN_TIMEOUT=600 LEAN_MAX_CORES=$CORES '$T/lean-guard' Proofs/Inventory.lean
|
|
" > "$T/inv.out" 2>&1
|
|
local rc=$?
|
|
cd "$T"
|
|
return $rc
|
|
}
|
|
|
|
expect() { # expect <label> <invlog> <want-rc> <want-substring>
|
|
local label="$1" invlog="$2" want_rc="$3" want_txt="$4" out rc
|
|
# Phase 3d removes its INVLOG on the way out — that is correct behaviour for
|
|
# the button and fatal for a fixture, so it always gets a disposable copy.
|
|
cp "$invlog" "$T/inv.feed"
|
|
out=$(bash "$DRIVER" "$T/inv.feed" 2>&1); rc=$?
|
|
if [ "$rc" -ne "$want_rc" ]; then
|
|
echo " ✗ $label: exit $rc, expected $want_rc"; echo "$out" | sed 's/^/ /'
|
|
FAILURES=$((FAILURES+1)); return
|
|
fi
|
|
if ! grep -qF "$want_txt" <<<"$out"; then
|
|
echo " ✗ $label: exit code right, diagnostic wrong (rejected for the wrong reason)"
|
|
echo " wanted: $want_txt"; echo "$out" | sed 's/^/ /'
|
|
FAILURES=$((FAILURES+1)); return
|
|
fi
|
|
echo " ✓ $label"
|
|
}
|
|
|
|
# ── 0. positive control ────────────────────────────────────────────────────
|
|
build_inventory || { echo " ✗ case 0: pristine tree did not compile"; exit 1; }
|
|
cp "$T/inv.out" "$T/inv.pristine"
|
|
expect "case 0 control: pristine tree passes Phase 3d" "$T/inv.pristine" 0 "statements bound"
|
|
|
|
# ── 1. THE ONE THAT MATTERS: a compiling, definitionally-equal body edit ───
|
|
python3 - "$T/Proofs/PinStore.lean" <<'PY'
|
|
import sys
|
|
f = sys.argv[1]; s = open(f).read()
|
|
old = " else ConsRec n n' C true r = some (r, r')"
|
|
assert s.count(old) == 1, "pinAccept body not found — this case is vacuous"
|
|
open(f, "w").write(s.replace(old, " else id (ConsRec n n' C true r = some (r, r'))", 1))
|
|
PY
|
|
if build_inventory; then
|
|
# The premise: the coverage gate must NOT see this. If it ever does, this
|
|
# case stops testing what it claims and must be re-examined, not re-labelled.
|
|
if "$T/inventory_gate.sh" "$T/inv.out" "$T/inventory-allowlist.txt" >/dev/null 2>&1; then
|
|
echo " ✓ case 1 premise: the coverage gate passes the edit (kind and cone unmoved)"
|
|
else
|
|
echo " ✗ case 1 premise: the coverage gate caught it — this case no longer isolates Phase 3d"
|
|
FAILURES=$((FAILURES+1))
|
|
fi
|
|
expect "case 1: defeq body edit caught by the statement digest" "$T/inv.out" 1 "STATEMENT DIGEST MISMATCH"
|
|
else
|
|
echo " ✗ case 1: the edited corpus did not compile (case is vacuous)"
|
|
FAILURES=$((FAILURES+1))
|
|
fi
|
|
cp "$T/PinStore.pristine" "$T/Proofs/PinStore.lean"
|
|
|
|
# ── 2. committed block hand-edited ─────────────────────────────────────────
|
|
sed -i '1s/$/ TAMPERED/' "$T/AUDIT-MANIFEST.txt"
|
|
expect "case 2: hand-edited committed block" "$T/inv.pristine" 1 "COMMITTED BLOCK STALE"
|
|
cp "$T/MANIFEST.pristine" "$T/AUDIT-MANIFEST.txt"
|
|
|
|
# ── 3. truncated block: "nothing found" must not pass for "nothing wrong" ──
|
|
grep -v '^STMT|LTLAcc.pinAccept|def|value=' "$T/inv.pristine" > "$T/inv.truncated"
|
|
expect "case 3: truncated statement block" "$T/inv.truncated" 1 "BLOCK TRUNCATED"
|
|
|
|
# ── 4. a constant inventoried but carrying no statement ────────────────────
|
|
# Drop one type line AND fix the trailer, so only the coverage comparison
|
|
# against the INV count can still object.
|
|
grep -v '^STMT|LTLAcc.pinAccept|def|type=' "$T/inv.pristine" > "$T/inv.gap"
|
|
NEW_N=$(awk '/^STMT-BEGIN/{f=1;next}/^STMT-END/{f=0}f' "$T/inv.gap" | grep -c '^STMT|')
|
|
sed -i "s/^STMT-COUNT|.*/STMT-COUNT|$NEW_N/" "$T/inv.gap"
|
|
expect "case 4: inventoried constant with no statement" "$T/inv.gap" 1 "STATEMENT COVERAGE GAP"
|
|
|
|
echo ""
|
|
if [ "$FAILURES" -eq 0 ]; then
|
|
echo "=== SELF-TEST GREEN: 4 attack cases defeated + positive control ==="
|
|
echo " Phase 3d catches what the coverage gate provably cannot see."
|
|
exit 0
|
|
fi
|
|
echo "=== SELF-TEST FAILED: $FAILURES case(s) did not behave as claimed ==="
|
|
exit 1
|