From 8d431c19dac205e436782b403f7d99f6f2010462 Mon Sep 17 00:00:00 2001 From: mrwulf Date: Tue, 28 Jul 2026 18:24:18 +0200 Subject: [PATCH] verification: kernel-side axiom-declaration gate (Phase 2b) + self-test MIME-Version: 1.0 Content-Type: text/plain; charset=UTF-8 Content-Transfer-Encoding: 8bit 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` ` 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 --- verification/check.sh | 82 +++++++++++++++++++++ verification/selftest-axgate.sh | 123 ++++++++++++++++++++++++++++++++ 2 files changed, 205 insertions(+) create mode 100755 verification/selftest-axgate.sh diff --git a/verification/check.sh b/verification/check.sh index 89e80d9..adb433c 100755 --- a/verification/check.sh +++ b/verification/check.sh @@ -12,6 +12,11 @@ # 2. compile gen/ + Proofs/ in dependency order (explicit -o, capped cores, # per-file timeout). Any "declaration uses 'sorry'" warning is a FAILURE # (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 # 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 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` ` 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 ─────────────────────────────── echo "=== Phase 3: axiom audit ===" EXPECTED="[propext, Classical.choice, Quot.sound]" diff --git a/verification/selftest-axgate.sh b/verification/selftest-axgate.sh new file mode 100755 index 0000000..367a740 --- /dev/null +++ b/verification/selftest-axgate.sh @@ -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 + 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