From 15101f32bdfab1aa4ae9f862b780e84f8a8fbdc4 Mon Sep 17 00:00:00 2001 From: mrwulf Date: Sat, 1 Aug 2026 16:10:59 +0200 Subject: [PATCH] Account for every constant the kernel sees, by set containment MIME-Version: 1.0 Content-Type: text/plain; charset=UTF-8 Content-Transfer-Encoding: 8bit THE GAP. The capability matrix in the control repo — built after the author answered a capability question by grepping for a FILENAME rather than for the property, three times in one session — asked whether each repository's auditor enumerates itself. The four ed25519 forks answered no. Following that up found something larger: `Proofs/Audit.lean`, the statement-binding driver from P1-a, is compiled, is a member of the manifest, and was enumerated by NOTHING. The kernel counted 3058 declarations where the inventory accounted for 3022, and 26 of the 36 missing were its. THE PROPERTY, now enforced: every constant the kernel sees under this button's manifest must appear, BY NAME, in either the corpus inventory or the instruments' own surface. `emitDrivers` in InventoryCore walks the audit modules and fails closed on an axiom (which would widen the trusted base outside every cone) or on a standalone claim (which no certificate covers and no allowlist pins), while admitting the obligations the elaborator generates for a definition declared alongside it. TWO WRONG FORMULATIONS FIRST, both recorded because the second is instructive: · `kernel = corpus + instruments + N_DRIVERS`, where the last term was justified as a per-driver "self-observation blind spot". 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. This was curve-fitting from a sample of one, and it was named as the highest-risk claim in the round-7 self-assessment BEFORE the data refuted it. · distinct-by-name counting, which collapses `CurveFieldProofs.zero_spec` — a name that genuinely denotes two different declarations, in Proofs.Basic and Proofs.ConstSpecs, walked by two drivers with separate environments. THE MEASURED CAUSE of the residual. Lean materialises equation lemmas lazily, when something forces an unfold, and each module that forces one gets its own copy in its object file. `CurveFieldProofs.denote.eq_1` sits in both SubNegSpec.olean and ConstSpecs.olean; `CurveFieldProofs.limbsVal.eq_1` in both ReduceSpec.olean and ConstSpecs.olean. The kernel gate reads object files and counts both copies; the environment holds one constant per name. Counts cannot relate those two views in either direction — so the check compares SETS, which is the idiom the rest of this estate already uses, and no constant remains that could be widened to make a red run green. Negative-tested: with the instrument walk disabled, the check names Proofs.Audit's declarations as unaccounted. ANZA also lacked one allowlist row, `subtle.Choice...from.eq_1`, the same lazy-materialisation effect seen from the other side. Verified rather than assumed before adding it: the parent is declared in gen/CurveField/ FunsExternal.lean — the model, pinned by bytes and not inventoried by declaration — the lemma materialised in Proofs.CompressSpec which forced the unfold, and all three other forks carry the lemma row while none carries the parent. CONSEQUENCE WORTH DISCLOSING: the audited declaration surface is not purely a function of the corpus source. It depends on which proofs forced which unfolds. This is now a known gap in the round-7 kit. Also corrected here: Proofs/Inventory.lean's header claimed the audit drivers were excluded from the compile manifest. They are lines 42-44 of PROOFS. Certified by a full sweep: both buttons, all four forks, purged trees. 8/8. --- verification/HARNESS.sha256 | 10 ++-- verification/Proofs/Inventory.lean | 8 +++ verification/Proofs/InventoryBasic.lean | 3 ++ verification/Proofs/InventoryCore.lean | 60 +++++++++++++++++++++++ verification/check.sh | 65 ++++++++++++++++++++++++- verification/inventory-allowlist.txt | 11 +++-- 6 files changed, 145 insertions(+), 12 deletions(-) diff --git a/verification/HARNESS.sha256 b/verification/HARNESS.sha256 index 902786a..65fb0fb 100644 --- a/verification/HARNESS.sha256 +++ b/verification/HARNESS.sha256 @@ -1,18 +1,18 @@ 12dc724bffd590e6f706573d97bf07425b8f268a1be2d72a3bbd9aef48f9c277 AUDIT-MANIFEST.txt 6b25b7e261633f4fa703de0be1dfd3c263d043107e3b3225d4c5079a93b6a64d check-scalar.sh -9f2e324cc6569872aea18437f87ec0f1ea715a230e9fec42ea3430ca084ba3f3 check.sh +5f1611459785a8c261007f9234606aaac4f8ba6e0fe37e74b0c7d14cb7eabbbd check.sh fdd1337f1f44fa73fdb14e6cda001e4e7358513b9c178c517456b24511d96a8e extract.sh 52afbe130c5551686f45643a35065729fd5bb8166b5fa3db67b74c60ba3eff62 GEN-MODEL.sha256 6033c86eb08b4c2ea0bd7cdbd2cfb5748059179ece3efa9673270dc17a2e38b9 inventory-allowlist-scalar.txt -b2c79ccf7005051946d49ee1fb0b51fbee58819c5909c6efb00965547b56fa5d inventory-allowlist.txt +80cdd232c9a0f3078b2b712957e34797add5421b51bd695a151bf64a7855687a inventory-allowlist.txt 0bb01bc4abaafa8537d460682004d1f336980b28bc4fe1968bcc9c3bc3bc71ba inventory_gate.sh 736ea4be712e1b5bcda10ecb466f0dec7008a2a36eabdfd77563976299c43cce lean-guard fde2e987a9f69cb9f39b18ab8b405d73db4d9abee9f714f8be993a40ef617c03 model-correspondence.py a8e2fa50e6f14278e9d088eb6339debc846419df297b0cdb2b9fbb77294545bd MODEL-CORRESPONDENCE.txt 34c102ca7a38719ef8890b8dedd3f07c3f92e10ae4a1ce2c47a7db4d53523354 Proofs/Audit.lean -4f23dc814f02d3d0355327fd01ab9092dae8b87c76cc296058693428f75e9c7e Proofs/InventoryBasic.lean -84bc670991fd7456d8c8569ff7b7c32410513a63d3cb7fe8877bb19a82d36a7d Proofs/InventoryCore.lean -4b1d7f5249a80375b4ef849a760ae8e4bbcecf103c3f8b9e8d0a5d5a9ae377fc Proofs/Inventory.lean +dd957bb260df0bd33266418a6594b45720c4754c5687bfab4ecb30ad573a286c Proofs/InventoryBasic.lean +859dcb7fcef13e8b49a8b36a496f46e9fc56448410d3bde16c78361215f4bc19 Proofs/InventoryCore.lean +660d35343f5673d4bc854787b6a34063c956567bd7e2eb62955a92e3c55bfa6b 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 1d71ca4..67e87ed 100644 --- a/verification/Proofs/Inventory.lean +++ b/verification/Proofs/Inventory.lean @@ -10,6 +10,7 @@ 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 +68,11 @@ 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: a member of +-- check.sh's compile manifest that was enumerated by NOTHING until 2026-07-31. +-- This module has no index while it is being elaborated, so `emitDrivers` picks +-- its own declarations up as the ones 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..7951a14 100644 --- a/verification/Proofs/InventoryBasic.lean +++ b/verification/Proofs/InventoryBasic.lean @@ -22,3 +22,6 @@ def corpus : Array Name := #[`Proofs.Basic] #eval show MetaM Unit from emitInventory corpus + +-- Its OWN declarations only; InventoryCore is accounted by Inventory.lean. +#eval show MetaM Unit from emitDrivers #[] diff --git a/verification/Proofs/InventoryCore.lean b/verification/Proofs/InventoryCore.lean index e872017..0d8b2ee 100644 --- a/verification/Proofs/InventoryCore.lean +++ b/verification/Proofs/InventoryCore.lean @@ -107,4 +107,64 @@ 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 4276cc7..eaffa2f 100755 --- a/verification/check.sh +++ b/verification/check.sh @@ -588,6 +588,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 @@ -598,6 +599,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 @@ -606,6 +608,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" @@ -613,12 +616,13 @@ 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 +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." @@ -685,7 +689,64 @@ 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. +# +# 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 diff --git a/verification/inventory-allowlist.txt b/verification/inventory-allowlist.txt index 42213ce..f544a24 100644 --- a/verification/inventory-allowlist.txt +++ b/verification/inventory-allowlist.txt @@ -1,15 +1,15 @@ -# inventory-allowlist.txt — the pinned audit surface (check.sh Phase 2c). # -# One line per constant in the compiled environment of the audited corpus: +# +# # INV||| -# # Generated from a green run; every entry reviewed as a DIFF, not read +# One line per constant in the compiled environment of the audited corpus: +# Regenerate deliberately: run check.sh, take the observed inventory, and +# inventory-allowlist.txt — the pinned audit surface (check.sh Phase 2c). # line by line — 3000 compiler-generated auxiliaries are not human-readable # prose, and pretending otherwise would be the point of failure. What a # reader checks is that a change to this file is explained by a change to # the proofs. -# -# Regenerate deliberately: run check.sh, take the observed inventory, and INV|Proofs.AddSpec|Aeneas.Std.core.cmp.impls.PartialOrdUsize.lt.eq_1|theorem| INV|Proofs.AddSpec|Aeneas.Std.core.iter.range.StepUsize.forward_checked.eq_1|theorem|propext INV|Proofs.AddSpec|CurveFieldProofs.add_limbs_spec._proof_1_18|theorem|Classical.choice,Quot.sound,propext @@ -122,6 +122,7 @@ INV|Proofs.CompressSpec|CurveFieldProofs.is_negative_spec._simp_1_8|theorem|prop INV|Proofs.CompressSpec|CurveFieldProofs.is_negative_spec._simp_1_9|theorem|propext INV|Proofs.CompressSpec|CurveFieldProofs.is_negative_spec|theorem|Classical.choice,Quot.sound,propext INV|Proofs.CompressSpec|CurveFieldProofs.to_bytes_spec'|theorem|Classical.choice,Quot.sound,propext +INV|Proofs.CompressSpec|subtle.Choice.Insts.CoreConvertFromU8.from.eq_1|theorem| INV|Proofs.CompressSpec|subtle.Choice.unwrap_u8.eq_1|theorem| INV|Proofs.ConstSpecs|Aeneas.Std.Array.make.eq_1|theorem| INV|Proofs.ConstSpecs|CurveFieldProofs.feVal._sparseCasesOn_1.else_eq|theorem|propext