TRUSTED-BASE: record the kernel-side axiom gate and its residue

Adds one item naming what check.sh Phase 2b binds — every compiled
Proofs/*.olean, kernel-side, membership self-derived, fail-closed on a
missing module — and, more importantly, what it still does not bind:
declarations, not statements. A theorem gutted to a tautology with the same
axiom cone passes every phase. Reading the statements remains a human act,
and this document is where that has to be said rather than left for a
reviewer to discover.

Verified green at this commit's parent across all eight buttons on
2026-07-28; see formal-verification-control/RECORDED-RUN-2026-07-28.md.

Co-Authored-By: Claude Opus 4.8 <noreply@anthropic.com>

TRUSTED-BASE.md

@@ -37,3 +37,19 @@ running Rust code. Everything else is machine-checked.
 6. **Compilation of Rust to machine code** (rustc backend) is out of scope,
    as is side-channel behaviour (timing, speculation). The proofs are about
    functional correctness at the MIR/LLBC level.
+7. **What the axiom gate binds, and what it does not.** `check.sh` Phase 2b
+   reads every compiled `Proofs/*.olean` and fails the build if any
+   declaration there is an axiom. It asks the kernel rather than parsing
+   source text, because the source-text check in Phase 1 is evadable four
+   ways — an indented `axiom`, `@[simp] axiom`, `unsafe axiom`, and `axiom`
+   with the name on the following line all compile and all miss its pattern.
+   Membership self-derives from the filesystem, so `Scalar*` and `AxiomCheck`
+   are covered as well, and the count of compiled modules must equal the
+   count of shipped sources, so a deleted `.olean` cannot make the scan pass
+   vacuously. `selftest-axgate.sh` attacks the shipping gate rather than a
+   copy of it, and was itself negative-tested by removing the gate's error.
+   **The residue you must still supply yourself:** this binds *declarations*,
+   not *statements*. Nothing in the button establishes that a certificate's
+   theorem says what its name — or this document — suggests it says. A
+   theorem gutted to a tautology with the same axiom cone would pass every
+   phase. Reading the statements remains a human act.

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` <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 ───────────────────────────────
 echo "=== Phase 3: axiom audit ==="
 EXPECTED="[propext, Classical.choice, Quot.sound]"
@@ -194,7 +276,7 @@ lake env bash -c "
   } > \"\$AUD\"
   OUT=\$(LEAN_TIMEOUT=$TIMEOUT LEAN_MEM_MB=4096 '$HERE/lean-guard' \"\$AUD\" 2>&1)
   echo \"\$OUT\"
-  rm -f \"\$AUD\"
+  rm -f \"\$AUD\" \"\${AUD%.lean}.olean\"
   N_CLEAN=\$(echo \"\$OUT\" | grep -cF \"depends on axioms: $EXPECTED\" || true)
   if [ \"\$N_CLEAN\" -ne ${#CERTS[@]} ]; then
     echo \"AXIOM AUDIT FAILED: \$N_CLEAN/${#CERTS[@]} certificates clean\"
@@ -216,7 +298,7 @@ lake env bash -c "
   { echo 'import Proofs.SigApexSpec'; echo 'import Proofs.PointLiftSpec'; echo 'import Proofs.PointEqSpec'; echo 'import Proofs.DecompressMain'; echo '#print axioms CurveFieldProofs.verify_accepts_iff'; echo '#print axioms CurveFieldProofs.verify_accepts_iff_point'; echo '#print axioms CurveFieldProofs.verify_accepts_iff_point_eq'; echo '#print axioms CurveFieldProofs.verify_accepts_iff_decompress'; } > \"\$AUD\"
   OUT=\$(LEAN_TIMEOUT=$TIMEOUT LEAN_MEM_MB=4096 '$HERE/lean-guard' \"\$AUD\" 2>&1)
   echo \"\$OUT\"
-  rm -f \"\$AUD\"
+  rm -f \"\$AUD\" \"\${AUD%.lean}.olean\"
   FLAT=\$(echo \"\$OUT\" | tr '\\n' ' ' | tr -s ' ')
   if echo \"\$FLAT\" | grep -qF \"'CurveFieldProofs.verify_accepts_iff' depends on axioms: \$ALLOWED\" \
      && echo \"\$FLAT\" | grep -qF \"'CurveFieldProofs.verify_accepts_iff_point' depends on axioms: \$ALLOWED\" \

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