mirror of
https://github.com/saymrwulf/risc0-ed25519-verified.git
synced 2026-09-04 20:03:41 +00:00
verification: kernel-side axiom-declaration gate (Phase 2b) + self-test
Phase 1's anti-smuggling check reads source text. Measured today on Lean
v4.30.0-rc2, four distinct declarations compile cleanly and slip past its
anchored pattern:
` axiom cheat : ...` one leading space
`@[simp] axiom cheat : ...` line starts with the attribute
`unsafe axiom cheat : ...` `unsafe` absent from the modifier list
`axiom` <newline> ` cheat` no space follows the keyword
Any of them yields a repository that proves False while the button prints
ALL GREEN. Only the tab variant is blocked, and by Lean, not by us.
Hardening the pattern would fix the exhibited syntax rather than the class,
which is the mistake this estate has made before. Phase 2b stops parsing text
and asks the kernel instead: it reads every compiled Proofs/*.olean with
readModuleData and rejects any declaration that is an axiom.
Design notes:
- reads compiled artifacts rather than importing the modules, because
Proofs.Basic and Proofs.ConstSpecs deliberately reuse `zero_spec` and a
whole-corpus import is impossible by construction;
- membership is self-deriving from the filesystem, so Scalar* and
AxiomCheck are covered too — both are skipped by the CERTS audit and by
the dead-file gate;
- fails closed on absence: a missing .olean would make the scan vacuous, so
the count of compiled modules must equal the count of shipped sources;
- removes its temp source AND artifact on both paths, since a bare `rm`
after the call never runs under `set -e` when the gate goes red — exactly
how this repo accumulated 101 orphan .olean files;
- ~3 s for the whole corpus, against ~53 s for one module-importing run.
Phase 1's grep stays as a fast first line of defence. Phase 2b is the gate
that is load-bearing.
selftest-axgate.sh attacks the shipping gate, lifted out of check.sh at run
time rather than copied. It asserts the specific diagnostic, so a rejection
for an unrelated reason fails too, and it was itself negative-tested: with
the gate's throwError removed, the self-test goes red on exactly that case.
No proof, statement, specification or certificate is touched. No attested
commit is altered — the log binds specific commit hashes, all of which remain
ancestors of HEAD.
Co-Authored-By: Claude Opus 4.8 <noreply@anthropic.com>
This commit is contained in:
parent
eebeb98c65
commit
521ae59283
2 changed files with 205 additions and 0 deletions
|
|
@ -12,6 +12,11 @@
|
||||||
# 2. compile gen/ + Proofs/ in dependency order (explicit -o, capped cores,
|
# 2. compile gen/ + Proofs/ in dependency order (explicit -o, capped cores,
|
||||||
# per-file timeout). Any "declaration uses 'sorry'" warning is a FAILURE
|
# per-file timeout). Any "declaration uses 'sorry'" warning is a FAILURE
|
||||||
# (this catches sorry robustly — text greps can't, comments mention it).
|
# (this catches sorry robustly — text greps can't, comments mention it).
|
||||||
|
# 2b. kernel-side axiom-declaration gate: read every compiled Proofs/*.olean
|
||||||
|
# and reject ANY axiom declared there. Phase 1's grep reads source text
|
||||||
|
# and is evadable four ways (see the phase header); this one asks the
|
||||||
|
# kernel, derives its scope from the filesystem, and fails closed if the
|
||||||
|
# set of compiled modules does not match the set of shipped sources.
|
||||||
# 3. axiom audit: #print axioms for every certificate in CERTS; each must
|
# 3. axiom audit: #print axioms for every certificate in CERTS; each must
|
||||||
# report exactly [propext, Classical.choice, Quot.sound]
|
# report exactly [propext, Classical.choice, Quot.sound]
|
||||||
# ─────────────────────────────────────────────────────────────────────────────
|
# ─────────────────────────────────────────────────────────────────────────────
|
||||||
|
|
@ -179,6 +184,83 @@ if grep -q "uses 'sorry'" "$LOG"; then
|
||||||
echo "STUB DETECTED: a compiled declaration uses 'sorry'"; exit 1; fi
|
echo "STUB DETECTED: a compiled declaration uses 'sorry'"; exit 1; fi
|
||||||
rm -f "$LOG"
|
rm -f "$LOG"
|
||||||
|
|
||||||
|
# ── Phase 2b: kernel-side axiom-declaration gate ────────────────────────────
|
||||||
|
# WHY THIS EXISTS. Phase 1's anti-smuggling check reads SOURCE TEXT, and a
|
||||||
|
# source-text grep is the wrong instrument. Measured on Lean v4.30.0-rc2
|
||||||
|
# (2026-07-28), each of the following compiles cleanly and slips past it:
|
||||||
|
# ` axiom cheat : ...` (one leading space — the pattern is anchored)
|
||||||
|
# `@[simp] axiom cheat : ...` (line starts with the attribute)
|
||||||
|
# `unsafe axiom cheat : ...` (`unsafe` is not in the modifier alternation)
|
||||||
|
# `axiom` <newline> ` cheat` (no space follows the keyword)
|
||||||
|
# Only the tab variant is blocked, and by Lean itself, not by us. Hardening the
|
||||||
|
# pattern would fix the exhibited syntax rather than the class; the class fix is
|
||||||
|
# to stop parsing text and ask the kernel, which is what this phase does.
|
||||||
|
# Ported from fips205-slhdsa-verified/verification/Proofs/Audit.lean.
|
||||||
|
#
|
||||||
|
# Phase 1's grep is kept as a fast, readable first line of defence. THIS is the
|
||||||
|
# gate that is load-bearing.
|
||||||
|
echo "=== Phase 2b: kernel-side axiom-declaration gate ==="
|
||||||
|
# dot-prefixed and inside $HERE: `lean` refuses a file outside the root
|
||||||
|
# directory, and a leading dot keeps it out of every *.lean glob.
|
||||||
|
# The gate reads the COMPILED ARTIFACTS directly (readModuleData) rather than
|
||||||
|
# importing the modules. Two reasons, both load-bearing:
|
||||||
|
# · Proofs.Basic and Proofs.ConstSpecs deliberately reuse the name
|
||||||
|
# `zero_spec` (they are never imported together), so a whole-corpus import
|
||||||
|
# is impossible by construction — it fails with "environment already
|
||||||
|
# contains". Reading oleans merges nothing, so collisions cannot arise.
|
||||||
|
# · Membership is then SELF-DERIVING from the filesystem: every .olean under
|
||||||
|
# Proofs/ is scanned, including Scalar* and AxiomCheck, which the CERTS
|
||||||
|
# audit and the dead-file gate both skip. Nothing is on a hand-kept list.
|
||||||
|
# Cost is ~3 s for the whole corpus (no mathlib import), against ~53 s for a
|
||||||
|
# single module-importing invocation.
|
||||||
|
N_PROOF_SRC=$(ls -1 "$HERE"/Proofs/*.lean 2>/dev/null | wc -l)
|
||||||
|
GATE=$(mktemp "$HERE/.axgate-XXXX.lean")
|
||||||
|
{
|
||||||
|
echo "import Lean"
|
||||||
|
echo "open Lean"
|
||||||
|
echo "def expectedModules : Nat := $N_PROOF_SRC"
|
||||||
|
cat <<'LEANGATE'
|
||||||
|
|
||||||
|
run_cmd do
|
||||||
|
let dir : System.FilePath := "Proofs"
|
||||||
|
let mut errs : Array String := #[]
|
||||||
|
let mut nMod := 0
|
||||||
|
let mut nConst := 0
|
||||||
|
for entry in (← dir.readDir) do
|
||||||
|
if entry.path.extension == some "olean" then
|
||||||
|
nMod := nMod + 1
|
||||||
|
let (mod, _) ← readModuleData entry.path
|
||||||
|
for ci in mod.constants do
|
||||||
|
nConst := nConst + 1
|
||||||
|
if ci matches .axiomInfo _ then
|
||||||
|
errs := errs.push s!" {entry.fileName}: {ci.name}"
|
||||||
|
unless errs.isEmpty do
|
||||||
|
throwError "AXIOM DECLARED under Proofs/ (kernel-side gate):\n{String.intercalate "\n" errs.toList}"
|
||||||
|
-- FAIL CLOSED ON ABSENCE: an empty result and a clean result must not share
|
||||||
|
-- a code path. A deleted .olean would make the scan above vacuous; an extra
|
||||||
|
-- one is orphan litter with no shipped source.
|
||||||
|
if nMod != expectedModules then
|
||||||
|
throwError "COVERAGE MISMATCH under Proofs/: scanned {nMod} compiled modules, but the directory ships {expectedModules} sources. A missing .olean makes this gate vacuous; an extra .olean is an orphan with no source."
|
||||||
|
logInfo s!" kernel confirms: {nConst} declarations across {nMod} compiled Proofs modules, none is an axiom"
|
||||||
|
LEANGATE
|
||||||
|
} > "$GATE"
|
||||||
|
cd "$AENEAS_LEAN"
|
||||||
|
# The temp source AND its compiled artifact are removed on BOTH paths. Under
|
||||||
|
# `set -e` a bare `rm` after the call never runs when the gate goes red, which
|
||||||
|
# is exactly how this repo accumulated 101 orphan .olean files (fixed today).
|
||||||
|
GATE_RC=0
|
||||||
|
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' '$GATE'
|
||||||
|
" || GATE_RC=$?
|
||||||
|
rm -f "$GATE" "${GATE%.lean}.olean"
|
||||||
|
if [ "$GATE_RC" -ne 0 ]; then
|
||||||
|
echo "AXIOM SMUGGLING GATE FAILED (kernel-side) — see the error above."
|
||||||
|
exit 1
|
||||||
|
fi
|
||||||
|
|
||||||
# ── Phase 3: axiom audit of every certificate ───────────────────────────────
|
# ── Phase 3: axiom audit of every certificate ───────────────────────────────
|
||||||
echo "=== Phase 3: axiom audit ==="
|
echo "=== Phase 3: axiom audit ==="
|
||||||
EXPECTED="[propext, Classical.choice, Quot.sound]"
|
EXPECTED="[propext, Classical.choice, Quot.sound]"
|
||||||
|
|
|
||||||
123
verification/selftest-axgate.sh
Executable file
123
verification/selftest-axgate.sh
Executable file
|
|
@ -0,0 +1,123 @@
|
||||||
|
#!/usr/bin/env bash
|
||||||
|
# ─────────────────────────────────────────────────────────────────────────────
|
||||||
|
# selftest-axgate.sh — adversarial self-test for check.sh Phase 2b.
|
||||||
|
#
|
||||||
|
# An untested guard is decoration. This script breaks the thing Phase 2b
|
||||||
|
# guards and asserts the gate goes red FOR THE STATED REASON — a rejection by
|
||||||
|
# some other gate, or with some other message, fails the test too.
|
||||||
|
#
|
||||||
|
# It extracts Phase 2b out of check.sh at run time, so it attacks THE SHIPPING
|
||||||
|
# GATE rather than a copy that can drift away from it.
|
||||||
|
#
|
||||||
|
# Requires: Proofs/*.olean already built (run check.sh first, or any prior
|
||||||
|
# green build). Takes ~10 s; compiles one tiny throwaway module.
|
||||||
|
# ─────────────────────────────────────────────────────────────────────────────
|
||||||
|
set -uo pipefail
|
||||||
|
source ~/aeneas-toolchain/env.sh
|
||||||
|
HERE="$(cd "$(dirname "$0")" && pwd)"
|
||||||
|
AENEAS_LEAN="$AENEAS_HOME/backends/lean"
|
||||||
|
TIMEOUT="${LEAN_TIMEOUT:-600}"
|
||||||
|
export LEAN_MEM_MB="${LEAN_MEM_MB:-8192}"
|
||||||
|
CORES="${LEAN_MAX_CORES:-0-3}"
|
||||||
|
|
||||||
|
ATTACK="$HERE/Proofs/ZZSelftestAttack.lean"
|
||||||
|
STASH="$(mktemp -d)"
|
||||||
|
FAILURES=0
|
||||||
|
|
||||||
|
cleanup() {
|
||||||
|
rm -f "$ATTACK" "${ATTACK%.lean}.olean"
|
||||||
|
[ -f "$STASH/FeQ.olean" ] && mv "$STASH/FeQ.olean" "$HERE/Proofs/FeQ.olean"
|
||||||
|
rm -rf "$STASH"
|
||||||
|
rm -f "$HERE"/.axgate-*.lean "$HERE"/.axgate-*.olean
|
||||||
|
}
|
||||||
|
trap cleanup EXIT INT TERM
|
||||||
|
|
||||||
|
# Phase 2b, lifted verbatim from the shipping button.
|
||||||
|
DRIVER="$STASH/phase2b.sh"
|
||||||
|
{
|
||||||
|
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\""
|
||||||
|
sed -n '/^# ── Phase 2b/,/^# ── Phase 3/p' "$HERE/check.sh" | sed '$d'
|
||||||
|
} > "$DRIVER"
|
||||||
|
if [ "$(wc -l < "$DRIVER")" -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
|
||||||
|
|
||||||
|
expect() { # expect <name> <expected-rc> <required-substring>
|
||||||
|
local name="$1" want_rc="$2" want_txt="$3"
|
||||||
|
local out rc
|
||||||
|
out=$(bash "$DRIVER" 2>&1); rc=$?
|
||||||
|
if [ "$rc" -ne "$want_rc" ]; then
|
||||||
|
echo " FAIL $name: exit $rc, expected $want_rc"; FAILURES=$((FAILURES+1)); return
|
||||||
|
fi
|
||||||
|
if ! grep -qF "$want_txt" <<<"$out"; then
|
||||||
|
echo " FAIL $name: exit code right but diagnostic wrong (rejected for the wrong reason)"
|
||||||
|
echo " wanted substring: $want_txt"
|
||||||
|
echo " got: $(tr '\n' '|' <<<"$out" | cut -c1-300)"
|
||||||
|
FAILURES=$((FAILURES+1)); return
|
||||||
|
fi
|
||||||
|
echo " ok $name"
|
||||||
|
}
|
||||||
|
|
||||||
|
echo "=== selftest-axgate: attacking check.sh Phase 2b ==="
|
||||||
|
|
||||||
|
# ── 1. Baseline: the untouched repo must pass, and say how much it covered.
|
||||||
|
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'
|
||||||
|
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"
|
||||||
|
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.
|
||||||
|
mv "$HERE/Proofs/FeQ.olean" "$STASH/FeQ.olean"
|
||||||
|
expect "missing .olean is a failure, not a vacuous pass" 1 "COVERAGE MISMATCH"
|
||||||
|
mv "$STASH/FeQ.olean" "$HERE/Proofs/FeQ.olean"
|
||||||
|
|
||||||
|
# ── 4. Litter: neither path may leave the temp gate source or its artifact
|
||||||
|
# behind (this repo accumulated 101 orphan .olean files exactly that way).
|
||||||
|
if ls "$HERE"/.axgate-* >/dev/null 2>&1; then
|
||||||
|
echo " FAIL litter: temp gate files survived a run"; FAILURES=$((FAILURES+1))
|
||||||
|
else
|
||||||
|
echo " ok no litter left by either the green or the red path"
|
||||||
|
fi
|
||||||
|
|
||||||
|
# ── 5. Restored: the self-test must leave the working tree exactly as found.
|
||||||
|
DIRT=$(cd "$HERE/.." && git status --porcelain -- verification/Proofs | wc -l)
|
||||||
|
if [ "$DIRT" -ne 0 ]; then
|
||||||
|
echo " FAIL restore: $DIRT file(s) under Proofs/ left modified"; FAILURES=$((FAILURES+1))
|
||||||
|
else
|
||||||
|
echo " ok working tree restored"
|
||||||
|
fi
|
||||||
|
|
||||||
|
echo ""
|
||||||
|
if [ "$FAILURES" -eq 0 ]; then
|
||||||
|
echo "SELFTEST PASSED — Phase 2b rejects what it claims to reject, for the stated reason."
|
||||||
|
exit 0
|
||||||
|
fi
|
||||||
|
echo "SELFTEST FAILED: $FAILURES check(s) did not behave as claimed."
|
||||||
|
exit 1
|
||||||
Loading…
Reference in a new issue