mirror of
https://github.com/saymrwulf/risc0-ed25519-verified.git
synced 2026-09-03 19:53:45 +00:00
verification: derive lift dependencies instead of hand-keeping them
Round-9 swept all ten instruments per fork instead of only the two buttons,
and found selftest-axgate.sh red in all four. Root cause, identical to the
KERNLOG defect fixed the day before: a self-test lifts one phase out of
check.sh and supplies its variables from a HAND-WRITTEN preamble, and the
phase later grew a dependency nobody told the preamble about.
Phase 2b stopped globbing Proofs/*.olean and started reading $PROOFS by
membership. Bash does not error on an unset array under `set -u` — it
expands to nothing — so the gate silently received
expected := [".olean"]
one entry with an empty name, and rejected the baseline via its own
fail-closed absence check. Exit code right, reason wrong.
· lift-guard.sh (new, pinned): derives every variable the lifted payload
reads, subtracts what the driver defines, and fails AT LIFT TIME naming
the remainder. Wired into all five lifting self-tests; selftest-shapes.sh
drops its inline copy. One implementation, not five, since drifting out
of sync is the entire failure mode.
· selftest-axgate.sh: lifts PROOFS verbatim, and its case 2 now poisons a
MANIFESTED leaf module rather than adding a stray file. The stray-file
attack was a no-op against membership semantics — that is the dead-file
gate's job, proven by selftest-harness case 8 — and it is also the
weaker attack, since adding files to Proofs/ must clear a gate that
editing an already-manifested module does not.
· Phase 2c's accounting identity moves behind its own marker with its own
ACCTFAIL verdict, so the phase is liftable by construction rather than
by a self-test knowing where to stop. Truncating the lift range alone
would have dropped Phase 2c's own verdict and left the test unable to fail.
· The other four lifting self-tests assert on the PAYLOAD rather than the
assembled driver, so a marker in the preamble cannot satisfy a check
meant to prove the lift landed.
Certified: 8/8 self-tests green in all four forks (~212 assertions, none
failing); check.sh bytes unchanged and still matching the pin written before
the 3h08m round-9 sweep, whose 36 GREEN button rows therefore stand.
--audit-only re-run against the new HARNESS.sha256 in every fork.
Co-Authored-By: Claude Opus 4.8 <noreply@anthropic.com>
This commit is contained in:
parent
4fafaab608
commit
cc571bf163
9 changed files with 347 additions and 79 deletions
|
|
@ -1,12 +1,13 @@
|
|||
6c821b8e465d3b394cb3cbb4bb3757791ace064b6d1b273ba9a41402dac74e24 AUDIT-MANIFEST.txt
|
||||
d505e4dd9283673e78fb34e25780c94334e03de4ad20400f8289d594ab004daf check-scalar.sh
|
||||
afe5511860d91f857f1179755facc83542f6bc75620263b264fdac69f05fa6b8 check.sh
|
||||
9b0fa638179282b4dd74a6aad3d140ad1299b4e092d1f19dc337832c172947e3 check.sh
|
||||
9b24f501b1e92b8ae41db0729ae9fbdbf10438ae89764ed29aa07efc2c3d6dd6 extract.sh
|
||||
0ea20d74cd359da404ee3be116058374cbb9fd992ed170e5f6c64f8d7a6b2733 GEN-MODEL.sha256
|
||||
e95982c15c7d754f0c9bcffef95d4c9d4c63589ac51ecdd40870133f377a005c inventory-allowlist-scalar.txt
|
||||
86ee83b703d17c1f04af654657219b344b0076bc994c0b791ca6b6c5a0090d4f inventory-allowlist.txt
|
||||
0bb01bc4abaafa8537d460682004d1f336980b28bc4fe1968bcc9c3bc3bc71ba inventory_gate.sh
|
||||
736ea4be712e1b5bcda10ecb466f0dec7008a2a36eabdfd77563976299c43cce lean-guard
|
||||
b982bd1aa56b0648b10516985a2e0f6a9cacff4e1d19b441dadc5b35d69ec732 lift-guard.sh
|
||||
7a9c89cf2b96313bd4bcddb534e8d06724bd7250234e670baadf6a9b0d1fbf81 model-correspondence.py
|
||||
174f6c5a3f0f48feabcf80ddfb031e6459aca5edd2b476d4015581df764165ba MODEL-CORRESPONDENCE.txt
|
||||
772ca6dd22443c83dc35d5428598c8d17a01c69db5be008474d06476fa66f7f8 Proofs/Audit.lean
|
||||
|
|
@ -14,10 +15,10 @@ e95982c15c7d754f0c9bcffef95d4c9d4c63589ac51ecdd40870133f377a005c inventory-allo
|
|||
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
|
||||
|
|
|
|||
|
|
@ -690,6 +690,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
|
||||
|
|
@ -701,6 +737,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".
|
||||
|
|
@ -732,43 +772,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.
|
||||
|
|
|
|||
112
verification/lift-guard.sh
Executable file
112
verification/lift-guard.sh
Executable file
|
|
@ -0,0 +1,112 @@
|
|||
#!/usr/bin/env bash
|
||||
# lift-guard.sh <payload> <driver> [<phase-label>]
|
||||
#
|
||||
# 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 <payload> <driver> [phase-label]}"
|
||||
DRIVER="${2:?usage: lift-guard.sh <payload> <driver> [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 <<EOF
|
||||
FATAL: $LABEL reads variables this lift does not define: $UNBOUND
|
||||
Either lift their definitions too — VERBATIM from check.sh, with a
|
||||
sed range, so this test cannot drift away from the button's idea of
|
||||
them — or end the lift range before the block that uses them.
|
||||
Do NOT stub them: a stub makes the test measure something the button
|
||||
never runs, which is how a self-test becomes decoration.
|
||||
EOF
|
||||
exit 1
|
||||
fi
|
||||
|
|
@ -27,9 +27,19 @@ FAILURES=0
|
|||
# reality rather than assuming a pristine checkout.
|
||||
TREE_AT_START="$(cd "$(dirname "$0")/.." && git status --porcelain -- verification/Proofs)"
|
||||
|
||||
# Declared before the trap: cleanup reads it, and under `set -u` an unset name
|
||||
# turns any early abort into a second, misleading failure.
|
||||
VICTIM=""
|
||||
|
||||
cleanup() {
|
||||
rm -f "$ATTACK" "${ATTACK%.lean}.olean"
|
||||
[ -f "$STASH/FeQ.olean" ] && mv "$STASH/FeQ.olean" "$HERE/Proofs/FeQ.olean"
|
||||
# Restore the poisoned module on EVERY path. A self-test that aborts midway
|
||||
# must not leave a proof module carrying `axiom cheat : ∀ P, P` behind it.
|
||||
if [ -n "$VICTIM" ] && [ -f "$STASH/victim.lean" ]; then
|
||||
cp "$STASH/victim.lean" "$HERE/Proofs/$VICTIM.lean"
|
||||
[ -f "$STASH/victim.olean" ] && cp "$STASH/victim.olean" "$HERE/Proofs/$VICTIM.olean"
|
||||
fi
|
||||
rm -rf "$STASH"
|
||||
rm -f "$HERE"/.axgate-*.lean "$HERE"/.axgate-*.olean
|
||||
}
|
||||
|
|
@ -37,30 +47,48 @@ trap cleanup EXIT INT TERM
|
|||
|
||||
# Phase 2b, lifted verbatim from the shipping button.
|
||||
DRIVER="$STASH/phase2b.sh"
|
||||
PAYLOAD="$STASH/payload.sh"
|
||||
# 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" > "$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 <name> <expected-rc> <required-substring>
|
||||
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
|
||||
|
|
|
|||
|
|
@ -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 <label> <want-rc> <want-substring>
|
||||
local label="$1" want_rc="$2" want_txt="$3" out rc
|
||||
|
|
|
|||
|
|
@ -39,17 +39,20 @@ cp "$HERE/HARNESS.sha256" "$STASH/HARNESS.sha256"
|
|||
# Lift Phase 0c. The two repo families end the phase differently, so accept
|
||||
# either terminator rather than hardcoding one and silently lifting nothing.
|
||||
DRIVER="$STASH/phase0c.sh"
|
||||
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 "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 <label> <want-rc> <want-substring>
|
||||
local label="$1" want_rc="$2" want_txt="$3" out rc
|
||||
|
|
|
|||
|
|
@ -92,6 +92,20 @@ cp "$HERE/Proofs/$VICTIM_MOD.lean" "$STASH/victim"
|
|||
# produced a green report for a red condition while selftest-tiers.sh was being
|
||||
# built; do not "simplify" it away.)
|
||||
lift() {
|
||||
# THE LIFT RANGE STOPS AT THE ACCOUNTING IDENTITY, and that boundary is the
|
||||
# fix for round-7 finding F5 (Claude). Phase 2c grew an accounting block that
|
||||
# reads $KERNLOG — a file created in Phase 2b, one phase ABOVE the lift. Under
|
||||
# `set -u` the driver aborted on its first expansion, so this self-test could
|
||||
# not pass on any fork from the moment that block was added. It failed loudly
|
||||
# rather than passing vacuously, which is why it was a red test and not a
|
||||
# false green; but it meant the four-shapes property went unverified.
|
||||
#
|
||||
# This test attacks the WALKER — can a declaration hide from the inventory —
|
||||
# and the accounting identity is a separate property with its own coverage.
|
||||
# Lifting it here would only drag in Phase 2b's state.
|
||||
awk '/^# ── Phase 2c/{f=1} f&&/^# ── (Phase 2c-accounting|Phase 3|Phases end)/{exit} f{print}' \
|
||||
"$HERE/check.sh" > "$STASH/payload.sh"
|
||||
|
||||
{ echo 'set -euo pipefail'
|
||||
echo 'source ~/aeneas-toolchain/env.sh'
|
||||
echo "HERE=\"$HERE\""
|
||||
|
|
@ -102,12 +116,29 @@ lift() {
|
|||
# test's idea of the manifest drift away from the button's, and then the
|
||||
# test would be checking its own opinion instead of the shipping one.
|
||||
sed -n '/^PROOFS=(/,/^)/p;/^SCALAR_SH=/p;/^SCALAR_MANIFEST=/p' "$HERE/check.sh"
|
||||
awk '/^# ── Phase 2c/{f=1} f&&/^# ── (Phase 3|Phases end)/{exit} f{print}' "$HERE/check.sh"
|
||||
cat "$STASH/payload.sh"
|
||||
} > "$STASH/p2c.sh"
|
||||
for want in 'Phase 2c' 'inventory_gate.sh' 'PROOFS=(' 'SCALAR_MANIFEST='; do
|
||||
grep -qF "$want" "$STASH/p2c.sh" || {
|
||||
echo "FATAL: the lifted driver has no '$want' — check.sh's phase markers moved."; exit 1; }
|
||||
|
||||
# Guard on the PAYLOAD, not the concatenation. The previous version grepped
|
||||
# the assembled file, so a marker appearing in the preamble or in a lifted
|
||||
# definition would have satisfied it — the same shape as the line-count check
|
||||
# that an empty driver once passed because the CERTS array padded it.
|
||||
for want in 'Phase 2c' 'inventory_gate.sh'; do
|
||||
grep -qF "$want" "$STASH/payload.sh" || {
|
||||
echo "FATAL: the lifted PAYLOAD has no '$want' — check.sh's phase markers moved."; exit 1; }
|
||||
done
|
||||
for want in 'PROOFS=(' 'SCALAR_MANIFEST='; do
|
||||
grep -qF "$want" "$STASH/p2c.sh" || {
|
||||
echo "FATAL: the lift carries no '$want' — a definition the phase needs is missing."; exit 1; }
|
||||
done
|
||||
|
||||
# AND THE DURABLE GUARD: every variable the payload READS must be one the
|
||||
# driver DEFINES. Derived mechanically rather than from a hand-kept list,
|
||||
# because a hand-kept list is exactly what failed — the phase grew a
|
||||
# dependency nobody thought to add. Shared with the other four lifting
|
||||
# self-tests: ONE implementation, pinned, rather than five copies of the
|
||||
# thing whose whole failure mode is drifting out of sync.
|
||||
"$HERE/lift-guard.sh" "$STASH/payload.sh" "$STASH/p2c.sh" "check.sh Phase 2c" || exit 1
|
||||
}
|
||||
lift
|
||||
|
||||
|
|
|
|||
|
|
@ -47,37 +47,44 @@ cp "$HERE/AUDIT-MANIFEST.txt" "$STASH/AUDIT-MANIFEST.txt"
|
|||
cp "$HERE/check.sh" "$STASH/check.sh"
|
||||
|
||||
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 "HERE=\"$HERE\""
|
||||
sed -n '/^# ── Phase 0b/,/^# ── Phase 1/p' "$HERE/check.sh" | sed '$d'
|
||||
cat "$PAYLOAD0B"
|
||||
} > "$DRIVER0B"
|
||||
if [ "$(wc -l < "$DRIVER0B")" -lt 20 ]; then
|
||||
if [ "$(wc -l < "$PAYLOAD0B")" -lt 20 ]; then
|
||||
echo "FATAL: could not lift Phase 0b out of check.sh."; exit 1
|
||||
fi
|
||||
"$HERE/lift-guard.sh" "$PAYLOAD0B" "$DRIVER0B" "check.sh Phase 0b" || exit 1
|
||||
|
||||
DRIVER="$STASH/phase3c.sh"
|
||||
PAYLOAD="$STASH/payload3c.sh"
|
||||
build_driver() {
|
||||
# `$0` inside Phase 3c must resolve to the shipping check.sh, not to this
|
||||
# driver, or the apex-name recovery would read the wrong file.
|
||||
# Stop at the next phase marker, not at a blank echo: a terminator that is
|
||||
# not itself a phase boundary breaks the moment the phase's body changes.
|
||||
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 'source ~/aeneas-toolchain/env.sh'
|
||||
echo "HERE=\"$HERE\""
|
||||
echo 'AENEAS_LEAN="$AENEAS_HOME/backends/lean"'
|
||||
echo "TIMEOUT=$TIMEOUT; CORES=\"$CORES\""
|
||||
# CERTS is referenced by the cross-check inside Phase 3c.
|
||||
# CERTS is referenced by the cross-check inside Phase 3c. Lifted verbatim,
|
||||
# never re-derived, so this test cannot drift away from the button's set.
|
||||
sed -n '/^CERTS=(/,/^)/p' "$HERE/check.sh"
|
||||
# `$0` inside Phase 3c must resolve to the shipping check.sh, not to this
|
||||
# driver, or the apex-name recovery would read the wrong file.
|
||||
# Stop at the next phase marker, not at a blank echo: a terminator that is
|
||||
# not itself a phase boundary breaks the moment the phase's body changes.
|
||||
awk '/^# ── Phase 3c/{f=1} f&&/^# ── (Phase |Phases end)/&&!/Phase 3c/{exit} f{print}' "$HERE/check.sh" \
|
||||
| sed "s|\"\$0\"|\"$HERE/check.sh\"|g"
|
||||
cat "$PAYLOAD"
|
||||
} > "$DRIVER"
|
||||
if [ "$(wc -l < "$DRIVER")" -lt 60 ]; then
|
||||
if [ "$(wc -l < "$PAYLOAD")" -lt 60 ]; then
|
||||
echo "FATAL: could not lift Phase 3c 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 3c" || exit 1
|
||||
}
|
||||
build_driver
|
||||
|
||||
|
|
|
|||
|
|
@ -126,20 +126,31 @@ lift() {
|
|||
# exits 1 is masked by the echo's success and the driver reports green while
|
||||
# printing APEX AUDIT FAILED. The button gets this right at check.sh:32; a
|
||||
# lift that does not copy it tests something the button never runs.
|
||||
awk '/^# ── Phase 3: axiom audit/{f=1} f&&/^# ── (Phase 3c|Phases end)/{exit} f{print}' \
|
||||
"$HERE/check.sh" > "$STASH/payload.sh"
|
||||
{ echo 'set -euo pipefail'
|
||||
echo 'source ~/aeneas-toolchain/env.sh'
|
||||
echo "HERE=\"$HERE\""
|
||||
echo 'AENEAS_LEAN="$AENEAS_HOME/backends/lean"'
|
||||
echo "TIMEOUT=$TIMEOUT"
|
||||
sed -n '/^EXPECTED=/p;/^AUDIT_IMPORTS=(/,/^)/p;/^CERTS=(/,/^)/p' "$HERE/check.sh"
|
||||
awk '/^# ── Phase 3: axiom audit/{f=1} f&&/^# ── (Phase 3c|Phases end)/{exit} f{print}' "$HERE/check.sh"
|
||||
cat "$STASH/payload.sh"
|
||||
} > "$STASH/p3.sh"
|
||||
for want in 'AXIOM AUDIT FAILED' 'APEX AUDIT FAILED' 'CERTS=(' 'AUDIT_IMPORTS=(' 'EXPECTED='; do
|
||||
if ! grep -qF "$want" "$STASH/p3.sh"; then
|
||||
# The two diagnostics must come from the PAYLOAD; the three definitions are
|
||||
# preamble, so those are asserted on the assembled driver.
|
||||
for want in 'AXIOM AUDIT FAILED' 'APEX AUDIT FAILED'; do
|
||||
if ! grep -qF "$want" "$STASH/payload.sh"; then
|
||||
echo "FATAL: the lifted driver has no '$want' — check.sh's phase markers moved."
|
||||
exit 1
|
||||
fi
|
||||
done
|
||||
for want in 'CERTS=(' 'AUDIT_IMPORTS=(' 'EXPECTED='; do
|
||||
if ! grep -qF "$want" "$STASH/p3.sh"; then
|
||||
echo "FATAL: the lift carries no '$want' — a definition the phase needs is missing."
|
||||
exit 1
|
||||
fi
|
||||
done
|
||||
"$HERE/lift-guard.sh" "$STASH/payload.sh" "$STASH/p3.sh" "check.sh Phase 3" || exit 1
|
||||
}
|
||||
lift
|
||||
|
||||
|
|
|
|||
Loading…
Reference in a new issue