TRUSTED-BASE.md

@@ -39,19 +39,3 @@ 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,11 +12,6 @@
 #   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]
 # ─────────────────────────────────────────────────────────────────────────────
@@ -181,83 +176,6 @@ 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]"
@@ -273,7 +191,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\" \"\${AUD%.lean}.olean\"
+  rm -f \"\$AUD\"
   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\"
@@ -295,7 +213,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\" \"\${AUD%.lean}.olean\"
+  rm -f \"\$AUD\"
   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

@@ -1,123 +0,0 @@
-#!/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