saymrwulf/betrusted-ed25519-verified
1
0
Fork 0
mirror of https://github.com/saymrwulf/betrusted-ed25519-verified.git synced 2026-09-04 20:24:08 +00:00
Code Issues Projects Releases Packages Wiki Activity Actions

verification: kernel-side axiom-declaration gate (Phase 2b) + self-test

Browse source 
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:
mrwulf 2026-07-28 18:24:18 +02:00
parent 5910ac9298
commit 8d431c19da
2 changed files with 205 additions and 0 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

82
verification/check.sh
View file

@ -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
View 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