mirror of
https://github.com/saymrwulf/betrusted-ed25519-verified.git
synced 2026-09-04 20:24:08 +00:00
mrwulf
5707189ef5
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>
174 lines
8.7 KiB
Bash
Executable file
174 lines
8.7 KiB
Bash
Executable file
#!/usr/bin/env bash
|
|
# ─────────────────────────────────────────────────────────────────────────────
|
|
# selftest-correspondence.sh — attacks check.sh Phase 0d.
|
|
#
|
|
# Phase 0d asserts HOW each external the extraction asks for is answered: with
|
|
# an assumption in the hand-written model, or with a proof already in the
|
|
# extracted corpus. The second class is the one the documents make a claim
|
|
# about — the curve calls and curve types are said to resolve to the proven
|
|
# model's own definitions rather than to axioms — and that claim was prose
|
|
# until this phase existed.
|
|
#
|
|
# 0 control: the committed table matches the files
|
|
# 1 the extraction asks for something NOTHING provides -> UNRESOLVED
|
|
# 2 a PROVEN external answered by an axiom in the model instead. This is the
|
|
# attack that matters: a proof silently downgraded to an assumption, in a
|
|
# name whose spelling does not change anywhere else.
|
|
# 3 a row deleted from the committed table -> drift
|
|
# 4 a row's verdict edited in the committed table -> drift
|
|
#
|
|
# No Lean: Phase 0d is pure text over gen/. Seconds, not minutes.
|
|
# ─────────────────────────────────────────────────────────────────────────────
|
|
set -uo pipefail
|
|
HERE="$(cd "$(dirname "$0")" && pwd)"
|
|
FAILURES=0
|
|
STASH="$(mktemp -d)"
|
|
|
|
cleanup() {
|
|
[ -f "$STASH/corr" ] && cp "$STASH/corr" "$HERE/MODEL-CORRESPONDENCE.txt"
|
|
[ -f "$STASH/model" ] && cp "$STASH/model" "$HERE/$MODEL_REL"
|
|
[ -f "$STASH/tmpl" ] && cp "$STASH/tmpl" "$HERE/$TMPL_REL"
|
|
rm -rf "$STASH"
|
|
}
|
|
|
|
# Derive the victims from this repo rather than naming them: the forks do not
|
|
# share a gen/ layout (anza has no CurveSig crate at all, so it has no PROVEN
|
|
# rows and case 2 does not apply there).
|
|
TMPL_REL=$(cd "$HERE" && ls gen/*/FunsExternal_Template.lean | head -1)
|
|
MODEL_REL="${TMPL_REL/_Template/}"
|
|
PROVEN_ROW=$(grep -m1 '|PROVEN$' "$HERE/MODEL-CORRESPONDENCE.txt" || true)
|
|
|
|
trap cleanup EXIT INT TERM
|
|
cp "$HERE/MODEL-CORRESPONDENCE.txt" "$STASH/corr"
|
|
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\""
|
|
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/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
|
|
out=$(bash "$STASH/p0d.sh" 2>&1); rc=$?
|
|
if [ "$rc" -ne "$want_rc" ]; then
|
|
echo " ✗ $label: exit $rc, expected $want_rc"; tail -6 <<<"$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"; tail -6 <<<"$out" | sed 's/^/ /'
|
|
FAILURES=$((FAILURES+1)); return
|
|
fi
|
|
echo " ✓ $label"
|
|
}
|
|
|
|
echo "=== selftest-correspondence: attacking check.sh Phase 0d ==="
|
|
echo " template: $TMPL_REL"
|
|
|
|
expect "control: the committed table matches the files" 0 "answered by PROVEN definitions"
|
|
|
|
# ── 1. the extraction asks for something nothing provides ──────────────────
|
|
printf '\naxiom selftest_unprovided_external : Nat\n' >> "$HERE/$TMPL_REL"
|
|
expect "case 1: an external nothing provides" 1 "MODEL CORRESPONDENCE FAILED"
|
|
cp "$STASH/tmpl" "$HERE/$TMPL_REL"
|
|
|
|
# ── 2. a proof silently downgraded to an assumption ────────────────────────
|
|
# Answer a PROVEN external with an axiom in the model. The name does not change
|
|
# anywhere; only the way it is answered does. Nothing else in the button sees
|
|
# this: the byte pins still match their files, the compiler is content because
|
|
# the signature is unchanged, and no certificate's cone moves unless something
|
|
# happens to depend on it.
|
|
if [ -n "$PROVEN_ROW" ]; then
|
|
PROVEN_NAME=$(cut -d'|' -f2 <<<"$PROVEN_ROW")
|
|
PROVEN_TMPL=$(cut -d'|' -f1 <<<"$PROVEN_ROW")
|
|
VICTIM_MODEL="gen/${PROVEN_TMPL}.lean"
|
|
cp "$HERE/$VICTIM_MODEL" "$STASH/model2"
|
|
printf '\naxiom %s : Nat\n' "$PROVEN_NAME" >> "$HERE/$VICTIM_MODEL"
|
|
expect "case 2: a PROVEN external downgraded to an assumption" 1 "MODEL CORRESPONDENCE DRIFT"
|
|
cp "$STASH/model2" "$HERE/$VICTIM_MODEL"
|
|
else
|
|
echo " · case 2 skipped: this fork's extraction has no PROVEN externals"
|
|
fi
|
|
|
|
# ── 3/4. the committed table itself ────────────────────────────────────────
|
|
# Delete the FIRST row, whatever its verdict. An earlier draft deleted the
|
|
# PROVEN rows, which was vacuous on anza — that fork's extraction has none, so
|
|
# nothing was removed, the table still matched, and the case passed by testing
|
|
# nothing. Pick a row every fork is guaranteed to have.
|
|
sed '0,/|/{/|/d}' "$STASH/corr" > "$HERE/MODEL-CORRESPONDENCE.txt"
|
|
if ! diff -q "$STASH/corr" "$HERE/MODEL-CORRESPONDENCE.txt" >/dev/null; then
|
|
expect "case 3: a row deleted from the committed table" 1 "MODEL CORRESPONDENCE DRIFT"
|
|
else
|
|
echo " ✗ case 3: the table was not actually modified — the case is vacuous"
|
|
FAILURES=$((FAILURES+1))
|
|
fi
|
|
cp "$STASH/corr" "$HERE/MODEL-CORRESPONDENCE.txt"
|
|
|
|
sed -i '0,/|MODEL$/s/|MODEL$/|PROVEN/' "$HERE/MODEL-CORRESPONDENCE.txt"
|
|
expect "case 4: a verdict edited in the committed table" 1 "MODEL CORRESPONDENCE DRIFT"
|
|
cp "$STASH/corr" "$HERE/MODEL-CORRESPONDENCE.txt"
|
|
|
|
# ── 5/6. THE ROUND-7 FINDINGS, so they cannot regress ──────────────────────
|
|
# Both were real. Case 5 is GPT-5.6's constructive counterexample: a definition
|
|
# that exists ONLY inside a block comment was read as a real declaration, so the
|
|
# scanner reported PROVEN for a name Lean resolves to an axiom. Case 6 is the
|
|
# one that was live in four committed tables: Aeneas wraps long declarations,
|
|
# the old scanner required keyword and name on one physical line, and so it
|
|
# SILENTLY DROPPED them — nine to ten externals per fork had no row at all.
|
|
#
|
|
# Case 6 is the more important of the two. A gate that drops what it cannot
|
|
# read is worse than no gate: it prints green across a gap that is invisible in
|
|
# the diff. The scanner must now FAIL rather than skip.
|
|
CX=$(mktemp -d)
|
|
mkdir -p "$CX/gen/Forged"
|
|
printf 'axiom Forged.value : Nat\n' > "$CX/gen/Forged/FunsExternal_Template.lean"
|
|
printf 'axiom\n Forged.value : Nat\n' > "$CX/gen/Forged/FunsExternal.lean"
|
|
printf '/-\nnamespace Forged\ndef value : Nat := 0\nend Forged\n-/\n' > "$CX/gen/Forged/Funs.lean"
|
|
OUT=$(python3 "$HERE/model-correspondence.py" "$CX" 2>&1)
|
|
if grep -q 'Forged.value|MODEL' <<<"$OUT"; then
|
|
echo " ✓ case 5: a definition inside a block comment is not read as a declaration"
|
|
else
|
|
echo " ✗ case 5: comment-only definition mis-read — scanner says:"; sed 's/^/ /' <<<"$OUT"
|
|
FAILURES=$((FAILURES+1))
|
|
fi
|
|
|
|
printf 'axiom\n Forged.wrapped\n :\n Nat\n' >> "$CX/gen/Forged/FunsExternal_Template.lean"
|
|
OUT=$(python3 "$HERE/model-correspondence.py" "$CX" 2>&1); RC=$?
|
|
if [ "$RC" -ne 0 ] && grep -q 'UNRESOLVED\|Forged.wrapped' <<<"$OUT"; then
|
|
echo " ✓ case 6: a declaration whose name wraps to the next line is SEEN, not dropped"
|
|
else
|
|
echo " ✗ case 6: wrapped declaration dropped or mis-handled (rc=$RC):"; sed 's/^/ /' <<<"$OUT"
|
|
FAILURES=$((FAILURES+1))
|
|
fi
|
|
|
|
printf 'axiom\n' > "$CX/gen/Forged/FunsExternal_Template.lean"
|
|
OUT=$(python3 "$HERE/model-correspondence.py" "$CX" 2>&1); RC=$?
|
|
if [ "$RC" -eq 2 ] && grep -q 'fails closed' <<<"$OUT"; then
|
|
echo " ✓ case 7: an unparseable declaration stops the scanner (exit 2), never silence"
|
|
else
|
|
echo " ✗ case 7: unparseable declaration did not fail closed (rc=$RC)"
|
|
FAILURES=$((FAILURES+1))
|
|
fi
|
|
rm -rf "$CX"
|
|
|
|
expect "restored: the table matches again" 0 "answered by PROVEN definitions"
|
|
|
|
echo ""
|
|
if [ "$FAILURES" -eq 0 ]; then
|
|
echo "SELFTEST PASSED — an external cannot change how it is answered, and a"
|
|
echo "proof cannot be downgraded to an assumption, without failing the button."
|
|
exit 0
|
|
fi
|
|
echo "SELFTEST FAILED: $FAILURES case(s) did not behave as claimed."
|
|
exit 1
|