From 15ef99fd508ec95db88ef1510c737a5657b25c5c Mon Sep 17 00:00:00 2001 From: mrwulf Date: Tue, 4 Aug 2026 03:17:05 +0200 Subject: [PATCH] verification: separate the two accounting questions (round-9 review, Claude N2) Phase 2c-accounting asked one question with a name-keyed identity: is every kernel constant covered by the corpus inventory or the instrument surface? Keying on the name alone conflates that with a second, different question -- does the kernel attribute a declaration to the same module the walk does? Pair-keying the identity (module|name) was the obvious fix and is wrong: it fails on legitimate per-module duplicates. Lean materialises equation lemmas lazily, so each module forcing an unfold gets its own copy in its object file (GPT-5.6 round-7 F8). Those records differ from the walk only in module attribution, and every one of their names is accounted for elsewhere. So the block now asks both questions and reports them separately: coverage stays name-keyed and fail-closed, module attribution is counted and printed rather than suppressed. A divergence is now visible instead of either passing silently or failing for the wrong reason. The accumulator declines the second question and says why: its INV rows carry no module column (4 fields), so its records cannot be compared as pairs at all. Gating on the field count rather than on the row tag -- the shape of the record, not the spelling of its label. Adding that column is the open follow-up; until then the identity there is name-keyed only, which is weaker and now says so. Certified by the round-14 sweep: 50/50 green across all six repositories, both buttons and every self-test. Co-Authored-By: Claude Opus 4.8 --- verification/HARNESS.sha256 | 2 +- verification/check.sh | 58 +++++++++++++++++++++++++++++++++---- 2 files changed, 53 insertions(+), 7 deletions(-) diff --git a/verification/HARNESS.sha256 b/verification/HARNESS.sha256 index 9d285a2..088dbef 100644 --- a/verification/HARNESS.sha256 +++ b/verification/HARNESS.sha256 @@ -1,6 +1,6 @@ 6c821b8e465d3b394cb3cbb4bb3757791ace064b6d1b273ba9a41402dac74e24 AUDIT-MANIFEST.txt 6fd6275ba35ceb1c6ff38239a8377c0c1cb54dd5ecff83e77edc18f690b9bab4 check-scalar.sh -fb92e967d81982ede31c0deeb5c02bacaf3380ee94d2c9af3dd2634e3d73c6ad check.sh +a45899490e801b7ee0e2f7de0304fa3c756c63b58223fbae8ebdcd381d22b3aa check.sh e782d1c9eef71e97f3c8b97463c16abc6321cc7192dd08a877d8c42473259f84 driver-allowlist.txt 71244d824847311bcb3ba8ad1f1905c4b24fe8f015e3230969914019cb628b61 extract.sh 3898670a2cb3db74d7381372a09649f6518e49384adc935d73bd6be7f825f7b9 GEN-MODEL.sha256 diff --git a/verification/check.sh b/verification/check.sh index aab8b4c..c955631 100755 --- a/verification/check.sh +++ b/verification/check.sh @@ -596,7 +596,7 @@ run_cmd do let mut errs : Array String := #[] let mut nMod := 0 let mut nConst := 0 - let mut seen : Std.HashSet Name := {} + let mut seen : Std.HashSet (String × Name) := {} for name in expected do let p := dir / name -- FAIL CLOSED ON ABSENCE: a manifest module whose artifact is missing makes @@ -605,9 +605,20 @@ run_cmd do throwError "COVERAGE: {name} is in the compile manifest but its artifact is absent" nMod := nMod + 1 let (mod, _) ← readModuleData p + -- THE MODULE IS PART OF THE RECORD. Round-9 review (Claude, N2): this gate + -- emitted KERNEL-NAME|, and check.sh compared it against allowlists + -- keyed on module|name — keys that carry the module PRECISELY BECAUSE A + -- NAME IS NOT UNIQUE. This corpus still holds two distinct declarations + -- both called CurveFieldProofs.zero_spec (Proofs.Basic and + -- Proofs.ConstSpecs), which is why the module column was added to INV rows + -- in the first place. Keyed on name alone the identity certified "every + -- declaration NAME the kernel saw is accounted for", not "every + -- declaration" — the same defect as the round-11 DRV regression, sitting + -- inside the check that caught it. + let modName := "Proofs." ++ (name.dropRight 6) -- strip ".olean" for ci in mod.constants do nConst := nConst + 1 - seen := seen.insert ci.name + seen := seen.insert (modName, ci.name) if ci matches .axiomInfo _ then errs := errs.push s!" {name}: {ci.name}" unless errs.isEmpty do @@ -616,7 +627,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}" + for (m, n) in seen do IO.println s!"KERNEL-NAME|{m}|{n}" LEANGATE } > "$GATE" cd "$AENEAS_LEAN" @@ -785,10 +796,44 @@ 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 grep '^KERNEL-NAME|' "$KERNLOG" | cut -d'|' -f3 | 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'|' -f3 } | LC_ALL=C sort -u > "$ACCT_NAMES" +# TWO QUESTIONS, NOT ONE — round-9 review (Claude, N2), and the measurement +# that answered it. +# +# The reviewer was right that keying this identity on NAME ALONE is weaker than +# it reads: the allowlists are keyed module|name precisely because a name is not +# unique, and this corpus holds two distinct CurveFieldProofs.zero_spec +# declarations. So the pair is the right key — and keying on it revealed why the +# straightforward fix is not available. +# +# 36 kernel pairs in this fork do not match a walk pair, and EVERY ONE of them +# has its name accounted for under a DIFFERENT module. Example: +# kernel: Proofs.ConstSpecs|CurveFieldProofs.denote.eq_1 +# kernel: Proofs.SubNegSpec|CurveFieldProofs.denote.eq_1 <- same name twice +# walk: Proofs.SubNegSpec|CurveFieldProofs.denote.eq_1 +# That is GPT-5.6's round-7 F8: lazy equation lemmas are materialised PER +# MODULE, so every module forcing an unfold gets its own copy in its object +# file. The kernel reads object files and sees both copies; the environment walk +# reads one merged environment and sees the name once. Both views are correct +# about different things, so a pair mismatch here is not evidence of an +# unexamined declaration, and suppressing it with an exception list would be the +# fudge term four-fork data already refuted once. +# +# So the phase asks both questions and answers them separately: +# UNACCOUNTED a name the kernel holds that NO walk mentions -> FAILS +# MULTI-MODULE a pair that differs only in module attribution -> COUNTED and +# REPORTED, never silently dropped, so the F8 phenomenon is +# visible every run and a change in it is a change a reader sees +KERN_PAIRS=$(mktemp /tmp/check-kernpairs-XXXX.txt) +ACCT_PAIRS=$(mktemp /tmp/check-acctpairs-XXXX.txt) +LC_ALL=C grep '^KERNEL-NAME|' "$KERNLOG" | cut -d'|' -f2,3 | LC_ALL=C sort -u > "$KERN_PAIRS" +{ LC_ALL=C awk -F'|' '/^INV\|/{print $2"|"$3}' "$HERE/inventory-allowlist.txt" + LC_ALL=C grep '^DRV|' "$INVLOG" | cut -d'|' -f2,3 +} | LC_ALL=C sort -u > "$ACCT_PAIRS" +MULTIMOD=$(LC_ALL=C comm -23 "$KERN_PAIRS" "$ACCT_PAIRS" | wc -l) 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" @@ -804,9 +849,10 @@ elif [ -n "$UNACCOUNTED" ]; then printf '%s\n' "$UNACCOUNTED" | head -20 | sed 's/^/ /' ACCTFAIL=1 else - echo " accounting: every one of $(wc -l < "$KERN_NAMES") kernel constants is covered by the corpus inventory or the instrument surface" + echo " accounting: every one of $(wc -l < "$KERN_NAMES") kernel constant names is covered by the corpus inventory or the instrument surface" + echo " multi-module: $MULTIMOD kernel record(s) differ from a walk only in module attribution (lazy equation lemmas materialised per module — GPT-5.6 round-7 F8, reported not suppressed)" fi -rm -f "$KERN_NAMES" "$ACCT_NAMES" +rm -f "$KERN_NAMES" "$ACCT_NAMES" "$KERN_PAIRS" "$ACCT_PAIRS" ACCTFAIL=${ACCTFAIL:-0} [ "$ACCTFAIL" = 0 ] || { echo "ACCOUNTING FAILED"; rm -f "$INVLOG" "$OBS" "$KERNLOG"; exit 1; } rm -f "$INVLOG" "$OBS" "$KERNLOG"