diff --git a/STATEMENT-MAP.md b/STATEMENT-MAP.md index 03e3bc0..c89c388 100644 --- a/STATEMENT-MAP.md +++ b/STATEMENT-MAP.md @@ -66,8 +66,29 @@ cross-checked against the inventory's independently computed cones. asserted against the allowlist/CONES/harness by check.sh Phase 3c on every run — stale-count drift is now a red button, not an erratum: review R4-1, after three consecutive rounds of hand-edit failures.) -`verification/selftest_audit.sh` attacks the gate with nine injection -cases (attributed/indented/private/instance declarations, a nested -namespace reusing an audited basename, a smuggled axiom, a deleted -declaration, and unmanifested Proofs/ and gen/ modules) — each must -fail the exact production gate. +`verification/selftest_audit.sh` attacks the gate with fourteen +injection cases (attributed/indented/private/instance declarations, a +nested namespace reusing an audited basename, a smuggled axiom, a +deleted declaration, and unmanifested Proofs/ and gen/ modules) — each +must fail the exact production gate. Four were added on 2026-07-31 and +close two classes the earlier suite did not reach: + +* **A Lean file where no phase was looking.** The dead-file scan read + `Proofs/*.lean` and `gen/LTLAcc/*.lean` and nothing else, so a module + at the verification root or under any other `gen/` subdirectory was + neither compiled nor rejected — while remaining importable by name, + since `LEAN_PATH` contains both roots. Cases 10 and 11 forbid both. +* **The instruments' own declaration surface.** `Proofs/AxiomCheck.lean` + and `Proofs/Inventory.lean` perform the audit and are therefore not + corpus, so nothing inventoried what THEY declare. `Inventory.lean` now + walks both — including itself, as the module still being elaborated — + and fails closed on an axiom, or on a theorem that is not an artefact + of a definition declared alongside it. Cases 12 and 13 attack each + driver; case 12 uses an INDENTED axiom, because Phase 1's source grep + catches an unindented one and the point is to reach the kernel-side + walk behind it. + +Both new gates were negative-tested by removal. With the driver-surface +check disabled, `check.sh` PASSES a tree whose inventory driver declares +`axiom driver_cheat : False` — which is the whole reason the check +exists. diff --git a/verification/HARNESS.sha256 b/verification/HARNESS.sha256 index eb9e2e4..c922eec 100644 --- a/verification/HARNESS.sha256 +++ b/verification/HARNESS.sha256 @@ -1,5 +1,5 @@ e7d422f0be9a9e6f5465058292e30c711d52856428da2b01c470a57ec181540c AUDIT-MANIFEST.txt -7ab1bfbafc8ac9ab34d1e0eaa71ba2f1f9912121345cc1af281bcb1d2ec30ad2 check.sh +9118c39009196247655c3517626bba5447a59cf16484b1bb296ef6bc143fab13 check.sh 070147e2667053bd5d5e1174b969fc6c91bfcf15ded1a5bff57754e15f416885 fidelity/lean_defs.py 5d82462a002ac9fc782e95afe78b7719ba64b6410b5d2bfa620fe5317367dbf2 fidelity/run_fidelity.py 503babb3f4e6aff82ebd59e8752469ecd60fba440ed3b11b3f97c2b655fbd9bf gen/LTLAcc/HashExternal.lean @@ -8,8 +8,8 @@ f66fb98d2a09503d9bd0d60dc964545eea6dc94b9bbb9246d1021195b79f2601 inventory_gate 736ea4be712e1b5bcda10ecb466f0dec7008a2a36eabdfd77563976299c43cce lean-guard ce4c4e3d87434b9663f46de25ce34b48a0cf0d392e0a320a0787b4674a2d7b61 lean-toolchain eda93f520546a692926b2a46bcb79332e1795879e5083327a8bf2404aca5cf87 Proofs/AxiomCheck.lean -25344c8441077277addd6b4eb769b2c0e3b173afc28d3a6e8aeba0580c22a87f Proofs/Inventory.lean +de5cdf01724fd4333b0652769bfede3ee150fedfa0a6c4ffbc8e7ab065843928 Proofs/Inventory.lean 0b8a0fc6947af1d1e600a756eb2b07dc88d189b21df3220c4501a41be8b33f1e run_bare.sh -67a44e0db818efc48dede26f73f76f1221424bb23e40e29d859b12d0d300403b selftest_audit.sh +dd975f4682035fe3313ce85b70f1aa1e411f9534ff62a29f5591630859c55a75 selftest_audit.sh 3d5898161d663eccad162269a5a6c102319077e22e1f2d89a8bfcab6926d29f6 selftest-harness.sh cf6d4d8210e224a054d4ab693c28c83e7a9ddebda05da47d6ec311d825a606c0 selftest_statements.sh diff --git a/verification/Proofs/Inventory.lean b/verification/Proofs/Inventory.lean index 2ca827d..13dc9ff 100644 --- a/verification/Proofs/Inventory.lean +++ b/verification/Proofs/Inventory.lean @@ -40,6 +40,7 @@ import Proofs.Binding3 import Proofs.Refactor import Proofs.Theorem3 import Proofs.PinStore +import Proofs.AxiomCheck open Lean @@ -52,6 +53,17 @@ def corpusModules : Array Name := `Proofs.Consistency, `Proofs.Binding3, `Proofs.Refactor, `Proofs.Theorem3, `Proofs.PinStore] +/-- The audit INSTRUMENTS, as opposed to the corpus. They are Lean modules in + the audited tree, so what they declare is part of this repository's + surface — but they are not proofs, and nothing may rest on them. + + `Proofs.AxiomCheck` is reachable here because this module imports it; this + module ITSELF has no module index while it is being elaborated, so its own + declarations are the ones the environment reports with no originating + module, and they are checked that way below. That is what makes this + inventory cover the instrument that produces it. -/ +def driverModules : Array Name := #[`Proofs.AxiomCheck] + def kindOf : ConstantInfo → String | .axiomInfo _ => "axiom" | .defnInfo _ => "def" @@ -151,6 +163,63 @@ def ppAll (e : Expr) : MetaM String := do for l in sorted do IO.println l IO.println s!"INV-COUNT|{sorted.size}" + -- ── CLASS 9: the instruments' own declaration surface ──────────────────── + -- The loop above walks the CORPUS. It says nothing about the two modules + -- that perform the audit, and until 2026-07-31 nothing else did either: an + -- `axiom` or a `theorem` added to Proofs.AxiomCheck or to this file was + -- invisible to every phase of the button. Both are covered here. + -- + -- Proofs.AxiomCheck is reachable by module index because this module imports + -- it. THIS module has no index yet — it is still being elaborated — so its + -- own declarations are exactly those the environment reports with no + -- originating module, which is how the inventory covers the instrument that + -- produces it rather than exempting itself. + -- + -- The policy is not "declare nothing": this file legitimately declares the + -- machinery above. The policy is that an instrument may declare only inert + -- definitions. An `axiom` here would widen the trusted base without + -- appearing in any certificate's cone; a `theorem` here would be a claim + -- that no certificate covers and no allowlist pins. + let mut drvIdxs : Array Nat := #[] + for m in driverModules do + match env.getModuleIdx? m with + | some i => drvIdxs := drvIdxs.push i + | none => throwError "INVENTORY ERROR: driver module {m} is not imported" + let mut drvNames : Std.HashSet Name := {} + let mut drvConsts : Array (Name × ConstantInfo) := #[] + for (n, ci) in env.constants.toList do + let here : Bool := + match env.getModuleIdxFor? n with + | some i => drvIdxs.contains i + | none => true -- declared by this file, still being elaborated + if here then + drvNames := drvNames.insert n + drvConsts := drvConsts.push (n, ci) + let mut drv : Array String := #[] + for (n, ci) in drvConsts do + let k := kindOf ci + -- An AXIOM in an instrument is never acceptable: it would widen the trusted + -- base without appearing in any certificate's cone. + if k == "axiom" then + throwError "DRIVER SURFACE VIOLATION: {n} is an axiom declared by the audit \ + infrastructure. An instrument may not widen the trusted base." + -- A THEOREM needs care rather than a flat ban. Defining a function by + -- well-founded recursion makes the elaborator emit its own proof + -- obligations — `LTLAccAudit.axiomCone._proof_1` is one, and a flat ban + -- rejected this very file. The distinction that matters is whether the + -- theorem is a CLAIM someone wrote or an ARTEFACT of a definition here: + -- an artefact's name extends the name of a constant declared alongside it, + -- a standalone claim's does not. + if k == "theorem" && !drvNames.contains n.getPrefix then + throwError "DRIVER SURFACE VIOLATION: {n} is a standalone theorem declared by \ + the audit infrastructure. An instrument may declare definitions \ + and whatever the elaborator generates for them — never a claim \ + of its own, which no certificate covers and no allowlist pins." + drv := drv.push s!"DRV|{n}|{k}" + let drvSorted := drv.qsort (· < ·) + for l in drvSorted do + IO.println l + IO.println s!"DRV-COUNT|{drvSorted.size}" -- FAIL CLOSED: the statement surface must cover the inventory exactly. If -- these ever diverge, some constant is inventoried but unbound — which is -- precisely the gap this section exists to close. diff --git a/verification/check.sh b/verification/check.sh index c304ffe..9abd3ee 100755 --- a/verification/check.sh +++ b/verification/check.sh @@ -24,6 +24,13 @@ CORES="${LEAN_MAX_CORES:-0-3}" GEN_MODULES=( LTLAcc/HashExternal ) PROOFS=( Basic Completeness Extract Descent Consistency Binding3 Refactor Theorem3 PinStore ) +# The audit infrastructure, named ONCE. These are not corpus — they are the +# instruments — but they are Lean modules in the audited tree, so the dead-file +# scan must know them by membership rather than by two hard-coded basename +# comparisons, and Phase 3b must inventory what they declare. CLASS 9: until +# 2026-07-31 nothing looked at the drivers' own declaration surface, so an +# `axiom` or a `theorem` added to either was invisible to every phase. +DRIVERS=( AxiomCheck Inventory ) # Certificates and their exact expected cones (observed via #print axioms, # never guessed; any drift in EITHER direction is a failure). @@ -202,8 +209,7 @@ lake env bash -c " done for f in Proofs/*.lean; do b=\$(basename \"\$f\" .lean) - [ \"\$b\" = AxiomCheck ] && continue # audit infrastructure, compiled in Phase 3 - [ \"\$b\" = Inventory ] && continue # audit infrastructure, compiled in Phase 3b + case \" ${DRIVERS[*]} \" in (*\" \$b \"*) continue;; esac # audit infrastructure, compiled in Phase 3/3b case \" ${PROOFS[*]} \" in (*\" \$b \"*) ;; (*) echo \"DEAD FILE: \$f\"; exit 1;; esac done # gen/ gets the same unmanifested-source check (review round 2, GPT M1) @@ -211,6 +217,21 @@ lake env bash -c " b=\"LTLAcc/\$(basename \"\$f\" .lean)\" case \" ${GEN_MODULES[*]} \" in (*\" \$b \"*) ;; (*) echo \"DEAD FILE (gen): \$f\"; exit 1;; esac done + # CLASS 15. The two loops above look only INSIDE Proofs/ and gen/LTLAcc/, so + # until 2026-07-31 a Lean file anywhere else was invisible: one at the + # verification root, or under gen/AnythingElse/, was neither compiled nor + # rejected. It could be imported by name from a manifested module — the + # manifest names modules, and LEAN_PATH includes both roots — which is a + # source of the corpus that no phase reads and no pin covers. Nothing may + # live in either root but the two enumerated sets. + shopt -s nullglob + for f in *.lean; do echo \"DEAD FILE (verification root): \$f\"; exit 1; done + for d in gen/*/; do + [ \"\$d\" = 'gen/LTLAcc/' ] && continue + for f in \"\$d\"*.lean; do echo \"DEAD FILE (gen subdirectory): \$f\"; exit 1; done + done + for f in gen/*.lean; do echo \"DEAD FILE (gen root): \$f\"; exit 1; done + shopt -u nullglob " if grep -q "uses 'sorry'" "$LOG"; then echo "STUB: sorry detected"; exit 1; fi rm -f "$LOG" @@ -263,16 +284,56 @@ lake env bash -c " # The inventory's corpus-module list must BE the compile manifest — both # directions, so neither can drift from the other silently. +# Read the module LISTS, not the file. This comparison used to grep the whole +# of Inventory.lean for a backticked name, which meant any PROSE mention of a +# module counted: a doc comment naming `Proofs.AxiomCheck` broke the count, and +# — worse in the other direction — a doc mention of a module missing from the +# array would have satisfied the presence check and hidden the omission. The +# manifest is the arrays; read the arrays. +MODLISTS=$(sed -n '/^def corpusModules/,/\]/p;/^def driverModules/,/\]/p' "$HERE/Proofs/Inventory.lean") for m in "${GEN_MODULES[@]}" "${PROOFS[@]}"; do mod=$(echo "$m" | sed 's|^LTLAcc/|LTLAcc.|; s|^\([A-Z]\)|Proofs.\1|; s|^Proofs\.LTLAcc\.|LTLAcc.|') - grep -qF "\`$mod" "$HERE/Proofs/Inventory.lean" || { + grep -qF "\`$mod" <<<"$MODLISTS" || { echo " MANIFEST DRIFT: $mod compiled by check.sh but not inventoried"; COVFAIL=1; } done -NMANIFEST=$(( ${#GEN_MODULES[@]} + ${#PROOFS[@]} )) -NINV=$(grep -oE '`(LTLAcc|Proofs)\.[A-Za-z0-9_.]+' "$HERE/Proofs/Inventory.lean" | wc -l) +# The drivers are named in Inventory.lean too, now that it walks their +# declaration surface — so they count on both sides of this equality. +for d in "${DRIVERS[@]}"; do + [ "$d" = Inventory ] && continue # covered as the current module, which has + # no module index while it elaborates and + # so is not named in its own module list + grep -qF "\`Proofs.$d" <<<"$MODLISTS" || { + echo " MANIFEST DRIFT: driver Proofs.$d is not inventoried"; COVFAIL=1; } +done +NMANIFEST=$(( ${#GEN_MODULES[@]} + ${#PROOFS[@]} + ${#DRIVERS[@]} - 1 )) +NINV=$(grep -oE '`(LTLAcc|Proofs)\.[A-Za-z0-9_.]+' <<<"$MODLISTS" | wc -l) [ "$NMANIFEST" = "$NINV" ] || { echo " MANIFEST DRIFT: check.sh compiles $NMANIFEST modules, Inventory lists $NINV"; COVFAIL=1; } +# CLASS 9. The driver-surface block must actually have RUN. Its violations are +# raised inside Lean, so a walk that silently did not execute would look exactly +# like a clean one — the same vacuous-pass shape the INV-COUNT trailer exists to +# close. Require the trailer, and require it to agree with the lines. +NDRV=$(grep -c '^DRV|' "$INVLOG" || true) +DRVTRAILER=$(grep '^DRV-COUNT|' "$INVLOG" | tail -1 | cut -d'|' -f2) +if [ -z "$DRVTRAILER" ] || [ "$DRVTRAILER" != "$NDRV" ]; then + echo " DRIVER SURFACE NOT OBSERVED: trailer=${DRVTRAILER:-absent}, observed $NDRV lines" + COVFAIL=1 +elif [ "$NDRV" -eq 0 ]; then + echo " DRIVER SURFACE NOT OBSERVED: the instruments declare nothing at all," + echo " which cannot be true — Inventory.lean declares its own machinery." + COVFAIL=1 +else + echo " driver surface: $NDRV declarations across the audit instruments, no axiom, no claim" +fi +# NOTE ON WHAT THIS DOES NOT DO. It does not pin WHICH definitions the +# instruments declare — a new inert `def` in a driver is allowed. That is +# deliberate: both drivers are byte-pinned in HARNESS.sha256 (Phase 0c), so +# their contents cannot drift unnoticed, and a second policy file listing their +# internals would add a thing to maintain without adding a thing to catch. What +# the check above adds is the property byte-pinning cannot give: that no +# instrument declares an AXIOM or a CLAIM, whatever its bytes are. + # CONES ⊆ allowlist with IDENTICAL cones: the #print-axioms-pinned table # and the environment inventory are two independent computations of the # same facts — any disagreement is a failure of one of them. diff --git a/verification/selftest_audit.sh b/verification/selftest_audit.sh index 1e67629..609b88e 100755 --- a/verification/selftest_audit.sh +++ b/verification/selftest_audit.sh @@ -39,6 +39,16 @@ trap 'echo "(scratch tree kept for inspection: $WORK)"' ERR echo "=== audit-gate self-test (scratch: $WORK) ===" cp -a "$SRC" "$WORK/verification" T="$WORK/verification" +# The button also reads two documents from the REPOSITORY root, one level above +# verification/. Copying only verification/ left them missing, so check.sh in +# the scratch tree always died in Phase 3c with DOC DRIFT — which meant every +# `if check.sh; then ` guard below was unfirable: +# check.sh could not pass in here even with no attack at all, so those guards +# asserted nothing. Only the diagnostic greps were doing any work. Copy the +# documents so a genuinely-undetected attack would now show up as a PASS. +for d in README.md STATEMENT-MAP.md; do + [ -f "$SRC/../$d" ] && cp "$SRC/../$d" "$WORK/$d" +done cp "$T/Proofs/PinStore.lean" "$T/PinStore.pristine" # Recompile the injected leaf module + the inventory, then run the gate. @@ -148,6 +158,96 @@ grep -q "DEAD FILE (gen): gen/LTLAcc/Rogue.lean" "$T/check9b.out" || { echo " ✗ case 9b: check.sh failed without DEAD FILE (gen) diagnosis"; tail -5 "$T/check9b.out"; exit 1; } echo " ✓ case 9b pinned but unmanifested: check.sh dies with DEAD FILE (gen)" +# Case 9 was the last case when it was written, so it left its rogue file and +# its pin in place — harmless then, but the cases below inherit the tree. Undo +# it here rather than in case 9, so that case keeps testing exactly what it +# tested before. +rm -f "$T/gen/LTLAcc/Rogue.lean" +( cd "$T" && grep -v ' gen/LTLAcc/Rogue.lean$' HARNESS.sha256 > .h && mv .h HARNESS.sha256 ) + +# ── CLASS 15: a Lean file where no phase was looking ──────────────────────── +# Until 2026-07-31 the dead-file scan read Proofs/*.lean and gen/LTLAcc/*.lean +# and nothing else. A module at the verification root, or under any other gen/ +# subdirectory, was neither compiled nor rejected — while being importable by +# name, since LEAN_PATH contains both roots. A source of the corpus that no +# phase reads and no pin covers is precisely what the dead-file gate exists to +# forbid; it was simply looking in two places instead of everywhere. + +# 10 — a stray module at the verification root. NOTE: Phase 0c does not stand +# in front of this one. Its required-pin set is executables plus +# gen/**.lean, so a root .lean is invisible to it; the Phase 2 check added +# for this class is the only gate here. +printf '/- rogue -/\ntheorem rogue_root : 1 = 1 := rfl\n' > "$T/Rogue.lean" +if SKIP_FIDELITY=1 "$T/check.sh" > "$T/check10.out" 2>&1; then + echo " ✗ case 10: check.sh PASSED with a stray Rogue.lean at the verification root"; exit 1 +fi +grep -q "DEAD FILE (verification root): Rogue.lean" "$T/check10.out" || { + echo " ✗ case 10: check.sh failed without the root diagnosis"; tail -5 "$T/check10.out"; exit 1; } +echo " ✓ case 10 stray module at the verification root: DEAD FILE (verification root)" +rm -f "$T/Rogue.lean" + +# 11 — a module in a gen/ subdirectory that is not LTLAcc/. Two gates again, +# and both are exercised for the same reason as case 9. +mkdir -p "$T/gen/Rogue" +printf '/- rogue -/\ntheorem rogue_sub : 1 = 1 := rfl\n' > "$T/gen/Rogue/Extra.lean" +if SKIP_FIDELITY=1 "$T/check.sh" > "$T/check11a.out" 2>&1; then + echo " ✗ case 11a: check.sh PASSED with an unpinned gen/Rogue/Extra.lean"; exit 1 +fi +grep -q "does not match HARNESS.sha256" "$T/check11a.out" || { + echo " ✗ case 11a: check.sh failed without the harness-set diagnosis"; tail -5 "$T/check11a.out"; exit 1; } +echo " ✓ case 11a unpinned module in a foreign gen subdirectory: harness-set mismatch" + +( cd "$T" && sha256sum gen/Rogue/Extra.lean >> HARNESS.sha256 ) +if SKIP_FIDELITY=1 "$T/check.sh" > "$T/check11b.out" 2>&1; then + echo " ✗ case 11b: check.sh PASSED with a pinned gen/Rogue/Extra.lean"; exit 1 +fi +grep -q "DEAD FILE (gen subdirectory): gen/Rogue/Extra.lean" "$T/check11b.out" || { + echo " ✗ case 11b: check.sh failed without the subdirectory diagnosis"; tail -5 "$T/check11b.out"; exit 1; } +echo " ✓ case 11b pinned but in a foreign gen subdirectory: DEAD FILE (gen subdirectory)" +rm -rf "$T/gen/Rogue" +( cd "$T" && grep -v ' gen/Rogue/Extra.lean$' HARNESS.sha256 > .h && mv .h HARNESS.sha256 ) + +# ── CLASS 9: the instruments' own declaration surface ─────────────────────── +# The audit drivers are not corpus, so nothing inventoried what THEY declare. +# Both are byte-pinned, so each attack must re-pin to reach the new gate — +# which is the point: byte-pinning stops drift, it does not stop an author. +# What follows is what byte-pinning cannot give. + +# 12 — an axiom in the inventory driver itself, INDENTED. Phase 1 greps +# Proofs/*.lean for `^axiom `, so an unindented one is caught there and +# never reaches the new gate. Indentation is the documented evasion of +# that regex — measured on Lean v4.30.0-rc2 — so this case is the one +# that actually exercises the kernel-side driver walk rather than the +# source scan standing in front of it. +sed -i 's|^#eval show MetaM Unit| axiom driver_cheat : False\n\n#eval show MetaM Unit|' \ + "$T/Proofs/Inventory.lean" +grep -q '^ axiom driver_cheat' "$T/Proofs/Inventory.lean" || { + echo " ✗ case 12: could not inject the indented axiom (case would be vacuous)"; exit 1; } +( cd "$T" && grep -v ' Proofs/Inventory.lean$' HARNESS.sha256 > .h \ + && sha256sum Proofs/Inventory.lean >> .h && mv .h HARNESS.sha256 ) +if SKIP_FIDELITY=1 "$T/check.sh" > "$T/check12.out" 2>&1; then + echo " ✗ case 12: check.sh PASSED with an axiom declared in Proofs/Inventory.lean"; exit 1 +fi +grep -q "DRIVER SURFACE VIOLATION" "$T/check12.out" || { + echo " ✗ case 12: check.sh failed without the driver-surface diagnosis"; tail -5 "$T/check12.out"; exit 1; } +echo " ✓ case 12 indented axiom in the inventory driver: DRIVER SURFACE VIOLATION" +cp "$SRC/Proofs/Inventory.lean" "$T/Proofs/Inventory.lean" +( cd "$T" && grep -v ' Proofs/Inventory.lean$' HARNESS.sha256 > .h \ + && sha256sum Proofs/Inventory.lean >> .h && mv .h HARNESS.sha256 ) + +# 13 — a standalone claim in the OTHER driver. A theorem there is not a +# compiler artefact of any definition, which is exactly the distinction +# the gate draws: it must admit `axiomCone._proof_1` and reject this. +printf '\ntheorem driver_claim : 1 = 1 := rfl\n' >> "$T/Proofs/AxiomCheck.lean" +( cd "$T" && grep -v ' Proofs/AxiomCheck.lean$' HARNESS.sha256 > .h && sha256sum Proofs/AxiomCheck.lean >> .h && mv .h HARNESS.sha256 ) +if SKIP_FIDELITY=1 "$T/check.sh" > "$T/check13.out" 2>&1; then + echo " ✗ case 13: check.sh PASSED with a standalone theorem in Proofs/AxiomCheck.lean"; exit 1 +fi +grep -q "DRIVER SURFACE VIOLATION" "$T/check13.out" || { + echo " ✗ case 13: check.sh failed without the driver-surface diagnosis"; tail -5 "$T/check13.out"; exit 1; } +echo " ✓ case 13 standalone claim in the axiom-check driver: DRIVER SURFACE VIOLATION" +cp "$SRC/Proofs/AxiomCheck.lean" "$T/Proofs/AxiomCheck.lean" + rm -rf "$WORK" trap - ERR -echo "=== SELF-TEST GREEN: 10 attack cases defeated + positive control ===" +echo "=== SELF-TEST GREEN: 14 attack cases defeated + positive control ==="