From f2f262ae909183bd5393bf205ab4c4be38c88540 Mon Sep 17 00:00:00 2001 From: mrwulf Date: Mon, 3 Aug 2026 15:57:48 +0200 Subject: [PATCH] Phase 3b: a kernel-side axiom gate, because the environment walk has a blind spot MIME-Version: 1.0 Content-Type: text/plain; charset=UTF-8 Content-Transfer-Encoding: 8bit Ported from the ed25519 forks and the accumulator, where it exists because a round-7 reviewer DEMONSTRATED the gap rather than argued it. Phase 3's audit runs inside Lean and reads `env.constants` after the imports — an ELABORATION-TIME view. Anything declared AFTER the command that performs the walk is in the compiled object file but not in the environment while the walk runs. The walker then reports "no axiom, no claim" and is telling the truth about what it could see. This phase reads the OBJECT FILES via `readModuleData`: a different view of the same modules, with no such ordering. Deliberately a second, independently implemented gate on the property that matters most — that nothing in the proof corpus DECLARES AN AXIOM, whatever its indentation, attributes or position. DEMONSTRATED, not asserted. An `axiom cheat : ∀ (P : Prop), P` appended to Proofs/Audit.lean after its audit command: === Phase 3: in-Lean audit … <- PASSED, saw nothing === Phase 3b: kernel-side axiom gate <- AXIOM DECLARED under Proofs/ Audit.olean: cheat exit 1 The environment walk passed it and the kernel gate caught it, which is the whole argument for having both. PLACEMENT IS LOAD-BEARING. Written first as Phase 2b — the forks' position — it died with COVERAGE, because Phase 2 compiles the eight certificate modules and Proofs/Audit.lean is only compiled by Phase 3. That failure was correct: a gate that skipped a missing module would be vacuous exactly where it matters, since the audit driver is the one module whose own declarations no other gate examines. Covering it requires waiting for it, so the gate runs after Phase 3. Fails closed three ways: a manifest module whose artifact is absent, an axiom in any module, and a scan that read zero declarations (an empty result and a clean result must not share a code path). Membership from this script's PROOFS array plus the driver, never a glob. Result: 298 declarations across 9 compiled modules, none an axiom. Co-Authored-By: Claude Opus 4.8 --- verification/check.sh | 79 +++++++++++++++++++++++++++++++++++++++++++ 1 file changed, 79 insertions(+) diff --git a/verification/check.sh b/verification/check.sh index 3a42508..708f23e 100755 --- a/verification/check.sh +++ b/verification/check.sh @@ -257,6 +257,85 @@ fi echo " ✓ $(grep -oF 'exact-cone audit PASSED' <<<"$AUD_OUT" | head -1)" echo " ✓ audit-manifest digest matches (sha256 ${EXPECTED_AUDIT_SHA256:0:16}…)" +# ── Phase 3b: kernel-side axiom-declaration gate ──────────────────────────── +# WHY A SECOND GATE ON THE SAME PROPERTY. Phase 3's audit runs INSIDE Lean and +# reads `env.constants` after the imports — an ELABORATION-TIME view. That view +# has a documented blind spot, demonstrated on the accumulator during round-7 +# review and reproduced there: anything declared AFTER the command that performs +# the walk exists in the compiled object file but is not in the environment +# while the walk runs. The walker reports "no axiom, no claim" and is telling +# the truth about what it could see. +# +# This phase reads the OBJECT FILES instead, via `readModuleData`, which is a +# different view of the same modules and has no such ordering. It is deliberately +# a second, independently-implemented gate on the property that matters most: +# that nothing in the proof corpus DECLARES AN AXIOM, whatever its indentation, +# attributes, or position in the file. +# +# Membership, not a glob: the manifest below is this script's PROOFS array plus +# the audit driver, so a module the button never compiled cannot be silently +# demanded, and a module it did compile cannot be silently skipped. +# +# IT RUNS AFTER PHASE 3, and that placement is load-bearing rather than +# cosmetic. Phase 2 compiles the eight certificate modules; Proofs/Audit.lean is +# only compiled by Phase 3. Placed at 2b the gate demanded an artifact that did +# not exist yet and died with COVERAGE — correctly, since a gate that skipped +# the missing module would have been vacuous exactly where it matters. The +# audit driver is the one module whose own declarations no other gate examines, +# so covering it is the point, and covering it requires waiting for it. +echo "=== Phase 3b: kernel-side axiom-declaration gate ===" +KERN_MODS=$(printf '"%s.olean", ' "${PROOFS[@]}" "Audit" | sed 's/, $//') +GATE=$(mktemp "$HERE/.axgate-XXXX.lean") +{ + echo "import Lean" + echo "open Lean" + echo "def expected : List String := [$KERN_MODS]" + cat <<'LEANGATE' + +run_cmd do + let dir : System.FilePath := "Proofs" + let mut errs : Array String := #[] + let mut nMod := 0 + let mut nConst := 0 + for name in expected do + let p := dir / name + -- FAIL CLOSED ON ABSENCE: a manifest module whose artifact is missing makes + -- this gate vacuous for that module. An error, never a skip. + unless (← p.pathExists) do + throwError "COVERAGE: {name} is in the compile manifest but its artifact is absent" + nMod := nMod + 1 + let (mod, _) ← readModuleData p + for ci in mod.constants do + nConst := nConst + 1 + if ci matches .axiomInfo _ then + errs := errs.push s!" {name}: {ci.name}" + unless errs.isEmpty do + throwError "AXIOM DECLARED under Proofs/ (kernel-side gate):\n{String.intercalate "\n" errs.toList}" + -- FAIL CLOSED ON EMPTINESS: an empty scan and a clean scan must not share a + -- code path, or a gate that read nothing would report the same as one that + -- read everything and found nothing wrong. + if nConst == 0 then + throwError "KERNEL GATE VACUOUS: read {nMod} module(s) and saw no declarations at all" + logInfo s!" kernel confirms: {nConst} declarations across {nMod} compiled modules, none is an axiom" +LEANGATE +} > "$GATE" +GATE_RC=0 +# The temp source AND its artifact are removed on BOTH paths: under `set -e` a +# bare rm after the call never runs when the gate goes red, which is how the +# ed25519 repos once accumulated 101 orphan .olean files. +( 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_MEM_MB=$MEM '$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 + + echo echo "ALL GREEN — model compiles, proofs compile, and every certificate cone" echo "equals EXACTLY the three kernel axioms plus its documented SHA-2 oracles."