diff --git a/verification/HARNESS.sha256 b/verification/HARNESS.sha256 index 7b66cab..c54580a 100644 --- a/verification/HARNESS.sha256 +++ b/verification/HARNESS.sha256 @@ -1,6 +1,6 @@ c0cfe800f41ce6c12420afb97ad40330b14a2aaad232077e7579e376c48e2ae4 AUDIT-MANIFEST.txt 6b25b7e261633f4fa703de0be1dfd3c263d043107e3b3225d4c5079a93b6a64d check-scalar.sh -b3405d760d352249536f58bb4fcabef7d3329e49cd728ae90786717bd03663f4 check.sh +03de9a93e27698714ca90fbe92989296c5847f75f14e60f2eb289e7540ef2d53 check.sh 5e582e44dfd210cb5b8e56f6c31907162fc8e1adf7dac7caf3afb435bbaccb53 extract.sh d93d7b77831b7db7acc2f88c395526db850219389a967a0873f3d59ee1f64dd4 GEN-MODEL.sha256 9acc69d66d0c35a88da6d6d020027e5b66ce992763cef3af8de653319abfbb8c inventory-allowlist-scalar.txt @@ -10,9 +10,9 @@ d93d7b77831b7db7acc2f88c395526db850219389a967a0873f3d59ee1f64dd4 GEN-MODEL.sha2 fde2e987a9f69cb9f39b18ab8b405d73db4d9abee9f714f8be993a40ef617c03 model-correspondence.py 2281dfc465954b026ebc3ac20c12d8dbadf307b4e1fecfc2dab11376a825634f MODEL-CORRESPONDENCE.txt 79a001107928713a22e679e4c4028549df76d0733455bb9937a4f438a0c315c8 Proofs/Audit.lean -4f23dc814f02d3d0355327fd01ab9092dae8b87c76cc296058693428f75e9c7e Proofs/InventoryBasic.lean -84bc670991fd7456d8c8569ff7b7c32410513a63d3cb7fe8877bb19a82d36a7d Proofs/InventoryCore.lean -561f872e812c6e507b93a4424937d1d2fbb0672f6b46a0833369a5a1f58c1bb5 Proofs/Inventory.lean +18e0cef25366bdcda67e8e347a222c169469654547b87adb01eb5b12aa9a9529 Proofs/InventoryBasic.lean +2b4f2bad2c82c64a1d29c873554b1728b86148f0bc27324c6e0b16defda22ca9 Proofs/InventoryCore.lean +132a1b039c70f4252c43be0ad5823145887e3e8c9f199d7e0f12d184c65ce265 Proofs/Inventory.lean 6fbeb50d3951c7c5ac593f6dec91096fc798123ed0c500fdfa39fb20b118ea78 Proofs/InventoryScalar.lean bf71e8d4eb312ebc687bf7e218d90b910543cd92e782078174868d012aca7250 selftest-auditonly.sh eb81df6d154b413b243ad282e3b1bfec92fde158a215f89993c08586a121f171 selftest-axgate.sh diff --git a/verification/Proofs/Inventory.lean b/verification/Proofs/Inventory.lean index 30ec8d9..80e7f80 100644 --- a/verification/Proofs/Inventory.lean +++ b/verification/Proofs/Inventory.lean @@ -1,15 +1,24 @@ /- ────────────────────────────────────────────────────────────────────────── Proofs/Inventory.lean — environment-derived declaration inventory (main chain). - Audit INFRASTRUCTURE, not corpus: excluded from check.sh's compile manifest - and from its own inventory (its constants live in modules the corpus list - below does not name). It proves nothing and is imported by nothing. + Audit INFRASTRUCTURE, not corpus. It proves nothing and is imported by + nothing. It IS a member of check.sh's compile manifest — lines 42-44 of + PROOFS — so Phase 2b's kernel-side gate reads its `.olean` and an axiom + declared here is rejected. (An earlier version of this comment claimed the + drivers were excluded from the manifest. That was false, and the capability + matrix in the control repo found it on 2026-07-31.) + + Its constants are outside the corpus walk below, and are emitted separately + by `emitDrivers` as DRV rows: the kernel counted 3058 declarations where the + inventory accounted for 3022, and those 36 are this machinery. check.sh now + requires the two walks to account for the kernel's count exactly. Covers every module check.sh compiles except any listed as needing a separate driver (see Proofs/InventoryBasic.lean if present). Whether a split is needed was determined by compiling a probe, per repo. ────────────────────────────────────────────────────────────────────────── -/ import Proofs.InventoryCore +import Proofs.Audit import Proofs.Denote import Proofs.P25519 import Proofs.ReduceSpec @@ -67,4 +76,15 @@ def corpus : Array Name := `Proofs.SigApexSpec, `Proofs.PointLiftSpec, `Proofs.PointEqSpec, `Proofs.DecompressSpec, `Proofs.FromBytesSpec, `Proofs.DecompressMain] +/-- The instruments. `Proofs.Audit` is the statement-binding driver: it is a + member of check.sh's compile manifest and it was enumerated by NOTHING — + 26 of the 39 declarations the accounting identity found missing were its. + `Proofs.InventoryBasic` is reachable by module index only + if this driver imports it; it does not, so it emits its own DRV rows under + its own run and check.sh sums the two. This module has no index while it is + being elaborated, so `emitDrivers` picks its declarations up as the ones the + environment reports with no originating module. -/ +def drivers : Array Name := #[`Proofs.InventoryCore, `Proofs.Audit] + #eval show MetaM Unit from emitInventory corpus +#eval show MetaM Unit from emitDrivers drivers diff --git a/verification/Proofs/InventoryBasic.lean b/verification/Proofs/InventoryBasic.lean index aa57ab0..bde930d 100644 --- a/verification/Proofs/InventoryBasic.lean +++ b/verification/Proofs/InventoryBasic.lean @@ -22,3 +22,10 @@ def corpus : Array Name := #[`Proofs.Basic] #eval show MetaM Unit from emitInventory corpus + +-- This driver accounts for ITS OWN declarations only. `Proofs.InventoryCore` +-- is shared machinery and is accounted by `Proofs/Inventory.lean`; counting it +-- here as well would make the two walks overlap and the kernel-count identity +-- in check.sh Phase 2c would fail — correctly, since a declaration would then +-- be accounted twice. +#eval show MetaM Unit from emitDrivers #[] diff --git a/verification/Proofs/InventoryCore.lean b/verification/Proofs/InventoryCore.lean index e872017..ac6b742 100644 --- a/verification/Proofs/InventoryCore.lean +++ b/verification/Proofs/InventoryCore.lean @@ -107,4 +107,62 @@ def emitInventory (corpus : Array Name) : MetaM Unit := do -- received, in both directions. IO.println s!"INV-COUNT|{sorted.size}" +/-- THE INSTRUMENTS' OWN SURFACE. + + `emitInventory` walks the CORPUS. It says nothing about the modules that + perform the audit, and until 2026-07-31 nothing else enumerated them either: + the kernel counted 3058 declarations across this button's 43 modules while + the inventory accounted for 3022, and the 36-declaration difference — the + drivers' own machinery — was covered by no allowlist row. + + That difference was never a soundness hole. The drivers ARE members of + check.sh's compile manifest, so Phase 2b's kernel-side gate reads their + `.olean`s and an axiom in one is rejected whatever its indentation. What was + missing is the weaker but still real property: that an instrument declares + nothing but inert machinery, and that every declaration the kernel sees is + ACCOUNTED FOR by exactly one of the two walks. + + The policy is not "declare nothing" — these files legitimately declare their + own functions. It is that an instrument may not declare an AXIOM (which + would widen the trusted base outside every cone) nor a standalone CLAIM + (which no certificate covers and no allowlist pins). A theorem whose name + extends a constant declared alongside it is an artefact the elaborator + generated for a definition — well-founded recursion emits these — and is + allowed; a theorem whose parent is not a declared constant is not. -/ +def emitDrivers (drivers : Array Name) : MetaM Unit := do + let env ← getEnv + let mut idxs : Array Nat := #[] + for m in drivers do + match env.getModuleIdx? m with + | some i => idxs := idxs.push i + | none => throwError "DRIVER SURFACE ERROR: driver module {m} is not imported" + -- Two passes: collect the names first, so the artefact test can ask whether a + -- theorem's parent is itself declared by an instrument. + let mut names : Std.HashSet Name := {} + let mut here : Array (Name × ConstantInfo) := #[] + for (n, ci) in env.constants.toList do + let mine : Bool := + match env.getModuleIdxFor? n with + | some i => idxs.contains i + | none => true -- declared by the module being elaborated: this driver + if mine then + names := names.insert n + here := here.push (n, ci) + let mut lines : Array String := #[] + for (n, ci) in here do + let k := kindOf ci + 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." + if k == "theorem" && !names.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." + lines := lines.push s!"DRV|{n}|{k}" + let sorted := lines.qsort (· < ·) + for l in sorted do + IO.println l + IO.println s!"DRV-COUNT|{sorted.size}" + end Ed25519Inventory diff --git a/verification/check.sh b/verification/check.sh index 8212dde..e06df2f 100755 --- a/verification/check.sh +++ b/verification/check.sh @@ -594,6 +594,7 @@ run_cmd do let mut errs : Array String := #[] let mut nMod := 0 let mut nConst := 0 + let mut seen : Std.HashSet Name := {} for name in expected do let p := dir / name -- FAIL CLOSED ON ABSENCE: a manifest module whose artifact is missing makes @@ -604,6 +605,7 @@ run_cmd do let (mod, _) ← readModuleData p for ci in mod.constants do nConst := nConst + 1 + seen := seen.insert ci.name if ci matches .axiomInfo _ then errs := errs.push s!" {name}: {ci.name}" unless errs.isEmpty do @@ -612,6 +614,7 @@ run_cmd do -- a code path. A deleted .olean would make the scan above vacuous; an extra -- one is orphan litter with no shipped source. logInfo s!" kernel confirms: {nConst} declarations across {nMod} compiled modules (this button's manifest, by membership), none is an axiom" + for n in seen do IO.println s!"KERNEL-NAME|{n}" LEANGATE } > "$GATE" cd "$AENEAS_LEAN" @@ -619,12 +622,15 @@ cd "$AENEAS_LEAN" # `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 +# Kept, not just printed: Phase 2c needs the kernel's own declaration count to +# check that the two inventory walks account for every declaration it saw. +KERNLOG=$(mktemp /tmp/check-kernel-XXXX.log) 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=$? +" 2>&1 | tee "$KERNLOG" || GATE_RC=${PIPESTATUS[0]} rm -f "$GATE" "${GATE%.lean}.olean" if [ "$GATE_RC" -ne 0 ]; then echo "AXIOM SMUGGLING GATE FAILED (kernel-side) — see the error above." @@ -691,7 +697,69 @@ OBS=$(mktemp /tmp/check-inv-obs-XXXX.log) grep '^INV|' "$INVLOG" > "$OBS" echo "INV-COUNT|${SUM:-0}" >> "$OBS" "$HERE/inventory_gate.sh" "$OBS" "$HERE/inventory-allowlist.txt" || INVFAIL=1 -rm -f "$INVLOG" "$OBS" + +# ── THE ACCOUNTING IDENTITY ─────────────────────────────────────────────── +# Every declaration the kernel saw must be accounted for by exactly one walk: +# the corpus inventory, or the instruments' own surface. Until 2026-07-31 the +# two numbers were never compared — the kernel reported 3058 across this +# button's manifest, the inventory accounted for 3022, and the 36-declaration +# difference was the audit drivers' own machinery, covered by no allowlist row +# and by no other check. It was not a soundness hole (the drivers ARE in the +# manifest, so Phase 2b's kernel gate rejects an axiom in one whatever its +# indentation) but it was an unexamined remainder, and an unexamined remainder +# is where the next defect hides. +# +# Stating it as an IDENTITY rather than as two separate counts is what makes it +# fail closed: a declaration that slipped out of both walks leaves the sum +# short, and one counted twice leaves it long. +# +# COUNT DISTINCT CONSTANTS, NOT PHYSICAL DECLARATIONS. The two sides of this +# identity were, at first, counting different things, and the gap was papered +# over with a `+ N_DRIVERS` term justified as a "self-observation blind spot". +# That explanation was WRONG. It fitted dalek and anza (2 drivers, residual 2) +# and broke on risc0 and betrusted (1 driver, residual 2) — the residual is 2 +# everywhere and has nothing to do with drivers. +# +# The measured cause: Lean materialises equation lemmas LAZILY, when something +# forces an unfold, and each module that forces one gets its own copy in its +# object file. On every fork, `CurveFieldProofs.denote.eq_1` sits in both +# `SubNegSpec.olean` and `ConstSpecs.olean`, and `CurveFieldProofs.limbsVal.eq_1` +# in both `ReduceSpec.olean` and `ConstSpecs.olean`. The kernel gate reads each +# object file separately and counts both copies; the environment holds one +# constant per name and the inventory sees it once. Hence exactly 2. +# +# So the gate now reports DISTINCT names and the fudge term is gone. This still +# fails closed: a declaration missing from both walks leaves the sum short, and +# one counted twice leaves it long. A future mismatch must be explained — as +# this one finally was — never absorbed into a constant. +N_DRV=$(grep -c '^DRV|' "$INVLOG" || true) +DRV_TRAILERS=$(grep -c '^DRV-COUNT|' "$INVLOG" || true) +DRV_SUM=$(grep '^DRV-COUNT|' "$INVLOG" | cut -d'|' -f2 | paste -sd+ - | bc) +KERN_NAMES=$(mktemp /tmp/check-kernnames-XXXX.txt) +ACCT_NAMES=$(mktemp /tmp/check-acctnames-XXXX.txt) +LC_ALL=C grep '^KERNEL-NAME|' "$KERNLOG" | cut -d'|' -f2 | LC_ALL=C sort -u > "$KERN_NAMES" +{ LC_ALL=C awk -F'|' '/^INV\|/{print $3}' "$HERE/inventory-allowlist.txt" + LC_ALL=C grep '^DRV|' "$INVLOG" | cut -d'|' -f2 +} | LC_ALL=C sort -u > "$ACCT_NAMES" +UNACCOUNTED=$(LC_ALL=C comm -23 "$KERN_NAMES" "$ACCT_NAMES") +if [ "$DRV_TRAILERS" -ne "$N_DRIVERS" ]; then + echo " DRIVER SURFACE INCOMPLETE: expected a trailer from each of the $N_DRIVERS driver(s), saw $DRV_TRAILERS" + INVFAIL=1 +elif [ "${DRV_SUM:-0}" != "$N_DRV" ]; then + echo " DRIVER SURFACE TRUNCATED: trailers sum to ${DRV_SUM:-0}, observed $N_DRV lines" + INVFAIL=1 +elif [ ! -s "$KERN_NAMES" ]; then + echo " ACCOUNTING FAILED: Phase 2b reported no constant names — the scan was vacuous" + INVFAIL=1 +elif [ -n "$UNACCOUNTED" ]; then + echo " ACCOUNTING FAILED: the kernel holds constants that neither walk accounts for:" + printf '%s\n' "$UNACCOUNTED" | head -20 | sed 's/^/ /' + INVFAIL=1 +else + echo " accounting: every one of $(wc -l < "$KERN_NAMES") kernel constants is covered by the corpus inventory or the instrument surface" +fi +rm -f "$KERN_NAMES" "$ACCT_NAMES" +rm -f "$INVLOG" "$OBS" "$KERNLOG" # The drivers' corpus lists must together BE the compile manifest, minus the # audit infrastructure and the scalar layer. Checked in both directions so a