verification: --audit-only mode, and the guard that keeps it from becoming evidence (T1)

Gate work dominates this estate's wall-clock: on 2026-07-29, 3.9 hours of a
session went to Lean re-elaborating proofs nobody had edited while the audit
phases themselves took about fifteen seconds. --audit-only runs every gate
against the artifacts a previous full run left behind: ~60s against ~1280s.

IT IS SAFE ONLY BECAUSE IT REFUSES.

  - It requires every shipped .lean to be BYTE-IDENTICAL to a basis recorded by
    a previous full run. Not mtimes: `touch` defeats those, and a stale-artifact
    check that fails open is worse than no shortcut at all, because a green
    button would then describe a corpus that is no longer on disk.
  - The basis is gitignored build state, so a fresh clone cannot inherit
    permission to skip compiling.
  - The closing banner differs and says in words that the run is not evidence.

selftest-auditonly.sh exercises seven cases: no basis, an edited comment
character, a deleted source, a new source, a missing artifact, a truncated
basis, and — asserted as a PASS — every source's mtime touched with bytes
unchanged, which pins the bytes-not-mtimes decision rather than leaving it
implicit. Negative-tested: with the basis comparison disabled a changed source
is wrongly accepted, exit 0 and zero refusals, so the guard is load-bearing.

A PHASE TERMINATOR, because this broke twice. Every self-test lifts a phase
from check.sh by scanning to the next phase marker. The last phase had no
marker after it, so a lift ran to end-of-file and swallowed whatever was
appended later — first Phase 2c into the axgate lift, then T1's tail into the
binding lift, where it referenced $AUDIT_ONLY and died under `set -u`. Both
surfaced as the BASELINE case failing: a self-test blaming a gate for its own
extraction bug. The phases now end at an explicit sentinel and both lifters
stop there, so nothing appended below can silently become part of the last
phase from a lifter's point of view.

TRUSTED-BASE.md records what an audit-only transcript does and does not
establish, and — because it cost a confusing red run today — that lean-guard's
memory clamp presents as `FAIL: Proofs/<module>` while being a resource
condition, not a broken proof.

Verified green: 8 full button runs (four check.sh, four check-scalar.sh) and 20
self-tests across the four repositories, zero red. One earlier run failed on
the memory clamp because the author ran a test suite concurrently; re-run on a
quiet machine, green.

Co-Authored-By: Claude Opus 4.8 <noreply@anthropic.com>

.gitignore

@@ -1,3 +1,4 @@
 *.olean
 .lake/
 lake-manifest.json
+.audit-basis

TRUSTED-BASE.md

@@ -109,3 +109,99 @@ running Rust code. Everything else is machine-checked.
    consumer's protection is, and has always been, *review at the pinned
    commit* rather than the button's own verdict. A green button says "this is
    the apparatus that was reviewed", never "this apparatus is trustworthy".
+
+10. **The whole declaration surface is pinned, not just the certificates.**
+   `check.sh` Phase 2c reads the compiled environment and records, for EVERY
+   constant originating in an audited module — roughly three thousand of them,
+   compiler-generated auxiliaries included — its originating module, fully
+   qualified name, declaration kind and complete axiom cone. The observed set
+   must equal `inventory-allowlist.txt` exactly, in BOTH directions: a
+   declaration present but not allowlisted (`UNCLASSIFIED`) and an allowlist
+   entry with no declaration (`STALE`) are both build failures, and a count
+   trailer disagreeing with the lines received is a third.
+
+   The gap this closes: Phase 2b asks the kernel only whether an AXIOM is
+   declared, and Phase 3 pins the cones of the named certificates. Between
+   them sat every helper lemma in the corpus. One of those quietly acquiring
+   a hash oracle in its cone moved nothing either phase looked at.
+
+   **Two limits, stated because a reader would otherwise assume neither.**
+
+   · *No independent cone walker here.* The companion accumulator runs a
+     hand-written closure walker alongside the kernel's `collectAxioms` and
+     requires the two to agree on every constant, so each checks the other.
+     Ported to this corpus on 2026-07-29 that walker was wrong in BOTH
+     directions on mathlib's inductive shapes — it reported no axioms for
+     `CurveFieldProofs.EdPoint` where the kernel reported three, and after
+     being extended it reported three for `CurveFieldProofs.ProjPoint` where
+     the kernel reported none. Two implementations disagreeing both ways are
+     not a cross-check; they are a second wrong answer. The cone figures here
+     therefore rest on `collectAxioms` alone. The accumulator keeps its
+     cross-check, its corpus being mathlib-free.
+
+   · *The scalar layer is outside this phase.* Thirteen `Proofs/Scalar*`
+     modules belong to `check-scalar.sh` and are inventoried by nothing. That
+     is the two-button seam, still open. Phase 2c prints every uncovered
+     module by name on every run, so the omission is visible rather than
+     inferred.
+
+11. **Both buttons, and the seam between them.** This repository is checked by
+   two scripts: `check.sh` covers the field, curve and signature layers,
+   `check-scalar.sh` the scalar layer. Until 2026-07-30 neither asserted
+   anything about the other's scope and the main one simply SKIPPED anything
+   named `Scalar*`, so a new `Proofs/ScalarX.lean` was gated by nothing at all
+   — absent from one manifest by exemption, from the other by omission,
+   compiled by neither, inventoried by neither. Each button now reads the
+   other's manifest and requires every shipped proof source to belong to
+   EXACTLY ONE of them, both directions: neither orphaned nor double-claimed.
+
+   The scalar button was also brought to the main one's standard, having been
+   left behind by every hardening round: it now checks source integrity,
+   verifies the harness pins (so running it alone is protected too), asks the
+   KERNEL about axiom declarations instead of grepping source text, inventories
+   its ~1,880 declarations against its own allowlist, and asserts each of its
+   13 certificates by name rather than counting how many lines of output
+   matched. A count cannot say WHICH certificate is clean, and passes just as
+   happily if one cone is reported twice.
+
+   **What this cost, recorded because the lesson generalises.** Three separate
+   gates in this work reasoned about how a thing is SPELLED rather than what it
+   BELONGS TO, and the corpus punished each one: `Proofs/ScalarPackSpec.lean`
+   is named like the scalar layer and owned by the main button. A dead-file
+   gate globbing `Scalar*` demanded it be scalar-owned; an axiom gate scanning
+   `Scalar*.olean` swept in an artifact this button does not compile, which on
+   a fresh tree is absent and would have failed the run for a false reason; and
+   the inventory driver discovery globbing `Inventory*.lean` claimed the other
+   button's driver. All three now test membership in a manifest. This is the
+   same family as the source-text axiom grep that began this campaign:
+   reasoning about names instead of about the thing itself.
+
+12. **`--audit-only`, and why a green transcript from it is not evidence.**
+   `check.sh --audit-only` runs every gate but skips recompilation, against the
+   `.olean` files a previous full run left behind: about 60 seconds against
+   about 1280. It exists because gate work dominates this estate's wall-clock,
+   and it is safe only because it refuses.
+
+   It refuses unless every shipped `.lean` is BYTE-IDENTICAL to a basis
+   recorded by a previous full run — not mtimes, which `touch` defeats, and a
+   stale-artifact check that fails open would be worse than no shortcut at all:
+   a green button would then describe a corpus that is no longer on disk. The
+   basis is gitignored build state, so a fresh clone cannot inherit permission
+   to skip compiling, and the closing banner says in words that the run is not
+   evidence.
+
+   **The kernel re-elaborates nothing in such a run.** What it establishes is
+   that the gates accept artifacts produced earlier — useful while developing a
+   gate, worthless as a record. `formal-verification-control/tools/record-run.py`
+   enforces that: it refuses to archive any transcript bearing the audit-only
+   markers, and also any transcript without a terminal success banner, any
+   containing `error:`, and any repository whose tree is dirty at record time.
+   A banner is a request; that tool is the gate.
+
+   Also worth knowing when reading a red run: `lean-guard` clamps Lean's memory
+   budget to what the machine can spare, and under load that clamp can be too
+   small to elaborate a large module. It surfaces as `FAIL: Proofs/<module>`,
+   which reads exactly like a broken proof and is not one — it is a resource
+   condition, and the cap is what protects this machine from the global OOM
+   that killed a session on 2026-07-02. Check the transcript for a `clamping`
+   line before concluding anything about the mathematics.

verification/HARNESS.sha256

@@ -1,10 +1,18 @@
 6c821b8e465d3b394cb3cbb4bb3757791ace064b6d1b273ba9a41402dac74e24  AUDIT-MANIFEST.txt
-b88f4bc16d3188f4830f8333201fc7826d46acf829c37f7da398d6ae9bfca15e  check-scalar.sh
-813c31664484adddd1752ea3bb30da826ad1050fd378604c242bcafb105fb4a3  check.sh
+d505e4dd9283673e78fb34e25780c94334e03de4ad20400f8289d594ab004daf  check-scalar.sh
+a8f560f1d46560ee8b90f90ffeeb63b1eccf0afdf1d6652a37a2047786945434  check.sh
 7a55136cd15ab96b3ab77234ffb8a2fc7c9544cb8b36426d29e257ffb2d2ba6e  extract.sh
 c9672a28825cd1d4055fb9efbb4a1d94c921c7b5c79e4cd5d0626ba061e554c1  GEN-MODEL.sha256
+e6f31b4303f5a344781d353f1dddefc185876df470e27b285c81556621e65c05  inventory-allowlist-scalar.txt
+86ee83b703d17c1f04af654657219b344b0076bc994c0b791ca6b6c5a0090d4f  inventory-allowlist.txt
+0bb01bc4abaafa8537d460682004d1f336980b28bc4fe1968bcc9c3bc3bc71ba  inventory_gate.sh
 736ea4be712e1b5bcda10ecb466f0dec7008a2a36eabdfd77563976299c43cce  lean-guard
 772ca6dd22443c83dc35d5428598c8d17a01c69db5be008474d06476fa66f7f8  Proofs/Audit.lean
-79611f9689ba714fb8d3f57aee86ad9655509303445beaad766bf8b049de8c44  selftest-axgate.sh
+84bc670991fd7456d8c8569ff7b7c32410513a63d3cb7fe8877bb19a82d36a7d  Proofs/InventoryCore.lean
+4b1d7f5249a80375b4ef849a760ae8e4bbcecf103c3f8b9e8d0a5d5a9ae377fc  Proofs/Inventory.lean
+6fbeb50d3951c7c5ac593f6dec91096fc798123ed0c500fdfa39fb20b118ea78  Proofs/InventoryScalar.lean
+bf71e8d4eb312ebc687bf7e218d90b910543cd92e782078174868d012aca7250  selftest-auditonly.sh
+eb81df6d154b413b243ad282e3b1bfec92fde158a215f89993c08586a121f171  selftest-axgate.sh
 3d5898161d663eccad162269a5a6c102319077e22e1f2d89a8bfcab6926d29f6  selftest-harness.sh
-a14acaafe914aabb9df44fcd05fd50d475804280fab9e332fdb5ea0b0d35f164  selftest-statements.sh
+1df031a075fc438c5229d01cbc44ee6ac489a272cd736624f7ca45ef1a4ddb7f  selftest-inventory.sh
+2c591fb2a0cc50cfdf76c3328e5d72d52b69c02f5b230ebc55c977d6570ecc0f  selftest-statements.sh

verification/Proofs/Inventory.lean

@@ -0,0 +1,70 @@
+/- ──────────────────────────────────────────────────────────────────────────
+   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.
+
+   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.Denote
+import Proofs.P25519
+import Proofs.ReduceSpec
+import Proofs.SubNegSpec
+import Proofs.ConstSpecs
+import Proofs.AddSpec
+import Proofs.MulSpec
+import Proofs.SquareSpec
+import Proofs.Square2Spec
+import Proofs.Field
+import Proofs.InvertSpec
+import Proofs.FieldMain
+import Proofs.FeQ
+import Proofs.EdCurve
+import Proofs.EdDenote
+import Proofs.EdDouble
+import Proofs.EdAddProjNiels
+import Proofs.EdAddAffNiels
+import Proofs.EdConvert
+import Proofs.EdMain
+import Proofs.DsmTableSpec
+import Proofs.DsmStepSpec
+import Proofs.DsmLoopSpec
+import Proofs.DsmNafLoadSpec
+import Proofs.DsmNafMath
+import Proofs.DsmNafLoopSpec
+import Proofs.DsmNafSpec
+import Proofs.DsmMulSpec
+import Proofs.ToBytesMath
+import Proofs.ToBytesSpec
+import Proofs.ScalarPackSpec
+import Proofs.CompressSpec
+import Proofs.SigApexSpec
+import Proofs.PointLiftSpec
+import Proofs.PointEqSpec
+import Proofs.DecompressSpec
+import Proofs.FromBytesSpec
+import Proofs.DecompressMain
+open Lean Ed25519Inventory
+
+/-- Exactly the modules this driver covers. check.sh verifies, in BOTH
+    directions, that the union of the two drivers' lists is its PROOFS
+    manifest minus the audit infrastructure. -/
+def corpus : Array Name :=
+  #[`Proofs.Denote, `Proofs.P25519, `Proofs.ReduceSpec, `Proofs.SubNegSpec,
+   `Proofs.ConstSpecs, `Proofs.AddSpec, `Proofs.MulSpec,
+   `Proofs.SquareSpec, `Proofs.Square2Spec, `Proofs.Field,
+   `Proofs.InvertSpec, `Proofs.FieldMain, `Proofs.FeQ, `Proofs.EdCurve,
+   `Proofs.EdDenote, `Proofs.EdDouble, `Proofs.EdAddProjNiels,
+   `Proofs.EdAddAffNiels, `Proofs.EdConvert, `Proofs.EdMain,
+   `Proofs.DsmTableSpec, `Proofs.DsmStepSpec, `Proofs.DsmLoopSpec,
+   `Proofs.DsmNafLoadSpec, `Proofs.DsmNafMath, `Proofs.DsmNafLoopSpec,
+   `Proofs.DsmNafSpec, `Proofs.DsmMulSpec, `Proofs.ToBytesMath,
+   `Proofs.ToBytesSpec, `Proofs.ScalarPackSpec, `Proofs.CompressSpec,
+   `Proofs.SigApexSpec, `Proofs.PointLiftSpec, `Proofs.PointEqSpec,
+   `Proofs.DecompressSpec, `Proofs.FromBytesSpec, `Proofs.DecompressMain]
+
+#eval show MetaM Unit from emitInventory corpus

verification/Proofs/InventoryCore.lean

@@ -0,0 +1,110 @@
+/- ──────────────────────────────────────────────────────────────────────────
+   Proofs/InventoryCore.lean — shared machinery for the declaration inventory.
+
+   PORTED, NOT REINVENTED. This is the ltl-accumulator-verified design
+   (Proofs/Inventory.lean there), which survived a nine-attack self-test that
+   defeated a source-regex enumerator: attributed, private, indented and
+   `instance` declarations were all invisible to the regex, and a nested
+   `namespace Hidden theorem MTH` collided with the basename of an audited
+   declaration. Reading the compiled ENVIRONMENT sees exactly what the kernel
+   saw, and there is no name shape that can hide from it.
+
+   WHY TWO DRIVERS IMPORT THIS. Unlike the accumulator, this corpus cannot be
+   imported as one environment: `Proofs.Basic` and `Proofs.ConstSpecs` both
+   declare `CurveFieldProofs.zero_spec`. That is deliberate and documented —
+   Basic.lean is compiled by check.sh but imported by nothing, so the reuse is
+   harmless — but it makes a single whole-corpus import impossible. The corpus
+   therefore splits into the main chain and Basic, one driver each, and
+   check.sh concatenates their output before gating. The split is asserted in
+   check.sh against the compile manifest, so a module cannot fall between the
+   two drivers unnoticed.
+
+   The corpus module list lives in each DRIVER, not here, and is checked
+   textually against check.sh's manifest in both directions. A listed module
+   that is not actually imported is an elaboration error, not a silent skip.
+   ────────────────────────────────────────────────────────────────────────── -/
+import Lean
+
+open Lean
+
+namespace Ed25519Inventory
+
+def kindOf : ConstantInfo → String
+  | .axiomInfo  _ => "axiom"
+  | .defnInfo   _ => "def"
+  | .thmInfo    _ => "theorem"
+  | .opaqueInfo _ => "opaque"
+  | .quotInfo   _ => "quot"
+  | .inductInfo _ => "inductive"
+  | .ctorInfo   _ => "ctor"
+  | .recInfo    _ => "recursor"
+
+/-- Axiom cone of `n`, from the kernel's own collector — the same machinery
+    `#print axioms` uses.
+
+    NO INDEPENDENT SECOND WALKER HERE, and that is a deliberate REDUCTION in
+    strength against the ltl-accumulator design this is ported from. There, a
+    hand-written closure walker runs alongside `collectAxioms` and every
+    constant must get the same answer from both, so the two implementations
+    check each other. Porting that walker to this corpus was tried on
+    2026-07-29 and abandoned on evidence:
+
+      · without traversing inductive families it UNDER-approximated —
+        `CurveFieldProofs.EdPoint`: walker [] vs kernel [Classical.choice,
+        Quot.sound, propext];
+      · adding constructors, recursor rules and `all` groups made it
+        OVER-approximate — `CurveFieldProofs.ProjPoint`: walker
+        [Classical.choice, Quot.sound, propext] vs kernel [].
+
+    Disagreeing in BOTH directions means the second implementation is not an
+    independent check, it is a second wrong answer. Matching the kernel's
+    traversal exactly over mathlib's inductive shapes is a Lean-internals
+    project, not a gate, and shipping a walker that is wrong in two directions
+    would be worse than shipping none: it would fail builds for reasons that
+    are the checker's fault and teach everyone to ignore it.
+
+    CONSEQUENCE, stated so nobody assumes otherwise: on this corpus the cone
+    figures rest on `collectAxioms` alone. The accumulator's corpus is
+    mathlib-free, its walker agrees there, and it KEEPS the cross-check. This
+    is recorded in TRUSTED-BASE.md. -/
+def axiomCone (n : Name) : MetaM (Array Name) := do
+  let cone ← collectAxioms n
+  return cone.qsort (fun a b => a.toString < b.toString)
+
+/-- Emit `INV|name|kind|cone` for every constant originating in `corpus`.
+    EVERY constant is emitted — fully qualified, NO filtering. Compiler-
+    generated auxiliaries (equation lemmas, match/eq/induct helpers, private
+    manglings) are emitted too and pinned in the allowlist, so anything new,
+    renamed, removed, or with a changed cone shows up as a diff. -/
+def emitInventory (corpus : Array Name) : MetaM Unit := do
+  let env ← getEnv
+  let mut idxs : Array Nat := #[]
+  for m in corpus do
+    match env.getModuleIdx? m with
+    | some i => idxs := idxs.push i
+    | none   => throwError "INVENTORY ERROR: corpus module {m} is not imported"
+  let mut lines : Array String := #[]
+  for (n, ci) in env.constants.toList do
+    if let some i := env.getModuleIdxFor? n then
+      if idxs.contains i then
+        let cone ← axiomCone n
+        let coneStr := ",".intercalate (cone.toList.map (·.toString))
+        -- The ORIGINATING MODULE is part of the record, unlike the accumulator's
+        -- format. It has to be: this corpus contains two distinct declarations
+        -- both named `CurveFieldProofs.zero_spec` (Proofs.Basic and
+        -- Proofs.ConstSpecs), inventoried by different drivers. Keyed on name
+        -- alone their records were byte-identical, so the merged allowlist held
+        -- 3021 entries for 3022 declarations and one real declaration was
+        -- covered by an entry describing a different one. The count trailer
+        -- caught it; the module field is what fixes it.
+        let mdl := env.header.moduleNames[i]!
+        lines := lines.push s!"INV|{mdl}|{n}|{kindOf ci}|{coneStr}"
+  let sorted := lines.qsort (· < ·)
+  for l in sorted do
+    IO.println l
+  -- Output-integrity trailer: a truncated or crashed run must never pass as an
+  -- empty diff. inventory_gate.sh compares this against the lines it actually
+  -- received, in both directions.
+  IO.println s!"INV-COUNT|{sorted.size}"
+
+end Ed25519Inventory

verification/Proofs/InventoryScalar.lean

@@ -0,0 +1,30 @@
+/- ──────────────────────────────────────────────────────────────────────────
+   Proofs/InventoryScalar.lean — declaration inventory for the scalar layer.
+
+   Audit INFRASTRUCTURE, not corpus. Compiled by check-scalar.sh Phase 2c,
+   which is where these modules' compiled artifacts exist: check.sh does not
+   compile the scalar layer, so its own inventory could not cover them and
+   named them as uncovered on every run instead. This closes that.
+────────────────────────────────────────────────────────────────────────── -/
+import Proofs.InventoryCore
+import Proofs.ScalarDenote
+import Proofs.ScalarLoop
+import Proofs.ScalarSubSpec
+import Proofs.ScalarAddSpec
+import Proofs.ScalarMulSpec
+import Proofs.ScalarMontSpec
+import Proofs.ScalarReduceSpec
+import Proofs.ScalarFullMulSpec
+import Proofs.ScalarMain
+import Proofs.ScalarWideSpec
+import Proofs.ScalarBytesSpec
+import Proofs.ScalarUnpackSpec
+import Proofs.ScalarFromBytesSpec
+open Lean Ed25519Inventory
+
+/-- Exactly check-scalar.sh's PROOFS manifest; that script asserts the
+    correspondence in both directions. -/
+def corpus : Array Name :=
+  #[`Proofs.ScalarDenote, `Proofs.ScalarLoop, `Proofs.ScalarSubSpec, `Proofs.ScalarAddSpec, `Proofs.ScalarMulSpec, `Proofs.ScalarMontSpec, `Proofs.ScalarReduceSpec, `Proofs.ScalarFullMulSpec, `Proofs.ScalarMain, `Proofs.ScalarWideSpec, `Proofs.ScalarBytesSpec, `Proofs.ScalarUnpackSpec, `Proofs.ScalarFromBytesSpec]
+
+#eval show MetaM Unit from emitInventory corpus

verification/check-scalar.sh

@@ -1,45 +1,232 @@
 #!/usr/bin/env bash
-# Scalar-layer check (Scalar52 arithmetic mod ℓ) — the layer is COMPLETE:
-# add, sub, Montgomery mul, and the byte-parsing chain, all kernel-audited.
+# ─────────────────────────────────────────────────────────────────────────────
+# check-scalar.sh — THE SECOND BUTTON (Scalar52 arithmetic mod ℓ).
+#
 # Runs against the merged gen/CurveField universe (the scalar module lives
 # there since the merge; see extract.sh). Guarded compiles throughout.
+#
+# Brought to the same standard as check.sh on 2026-07-30 (P0-b). Before that
+# it was the weakest link in the estate, and increasingly so as the main button
+# was hardened: no source-integrity check, no harness pin, no dead-file gate,
+# no declaration inventory, an EVADABLE source-text grep for axioms where the
+# main button asks the kernel, and a count of matching output lines where the
+# main button asserts each certificate's cone individually.
+#
+# Phases:
+#   0  source integrity + harness pin (so running this button alone is also
+#      protected, not only running it after check.sh)
+#   1  the two-button seam: every shipped proof source belongs to exactly one
+#      of the two manifests, asserted against check.sh's, both directions
+#   2  compile the scalar layer, with a dead-file gate over Scalar*
+#  2b  kernel-side axiom-declaration gate over the compiled artifacts
+#  2c  environment-derived declaration inventory, diffed both directions
+#   3  per-certificate exact-cone audit
+# ─────────────────────────────────────────────────────────────────────────────
 set -uo pipefail
 source ~/aeneas-toolchain/env.sh
 HERE="$(cd "$(dirname "$0")" && pwd)"
 AENEAS_LEAN="$AENEAS_HOME/backends/lean"
-GEN=(CurveField/TypesExternal CurveField/Types CurveField/FunsExternal CurveField/Funs)  # MERGED GEN: scalar module now lives in CurveField
+TIMEOUT="${LEAN_TIMEOUT:-300}"
+CORES="${LEAN_MAX_CORES:-0-3}"
+GEN=(CurveField/TypesExternal CurveField/Types CurveField/FunsExternal CurveField/Funs)
 PROOFS=(ScalarDenote ScalarLoop ScalarSubSpec ScalarAddSpec ScalarMulSpec ScalarMontSpec ScalarReduceSpec ScalarFullMulSpec ScalarMain ScalarWideSpec ScalarBytesSpec ScalarUnpackSpec ScalarFromBytesSpec)
+# Fully-qualified scalar certificates. Each must report EXACTLY the standard
+# three axioms — asserted per certificate, not by counting how many lines of
+# output happened to match. A count cannot tell you WHICH certificate is clean.
+CERTS=(
+  ScalarProofs.L_val
+  ScalarProofs.sub_loop_spec
+  ScalarProofs.sub_loop1_one_spec
+  ScalarProofs.sub_val_spec
+  ScalarProofs.add_val_spec
+  ScalarProofs.mul_internal_spec
+  ScalarProofs.part1_spec
+  ScalarProofs.montgomery_reduce_spec
+  ScalarProofs.mul_spec
+  ScalarProofs.scalarImplementation
+  ScalarProofs.montgomery_mul_spec
+  ScalarProofs.bytes_unpack_spec
+  ScalarProofs.from_bytes_wide_spec
+)
+EXPECTED="[propext, Classical.choice, Quot.sound]"
 
-echo "=== stub/axiom audit ==="
-grep -rnE '^(private |protected |noncomputable )*axiom ' "$HERE"/Proofs/Scalar*.lean 2>/dev/null && { echo "axiom under Proofs/"; exit 1; }
-echo "  clean"
-echo "=== compile (guarded) ==="
+# ── Phase 0: source integrity + harness pin ─────────────────────────────────
+echo "=== Phase 0: source integrity + harness pin ==="
+free -m | awk '/Mem:/{if($7<2048){print "FATAL: <2GB RAM available — refusing to compile"; exit 1}}' || exit 1
+for f in "$HERE"/Proofs/Scalar*.lean; do
+  [ -f "$f" ] || continue
+  if ! grep -qE '^(/-|import |namespace |theorem |def |open |set_option |--)' "$f"; then
+    echo "CORRUPTED: $f is not Lean source (olean clobber?). Restore: git checkout HEAD -- $f"
+    exit 1
+  fi
+done
+# The pin file and its policy live with check.sh; this button verifies the same
+# pins so that running it ALONE is protected too. If check.sh is absent the
+# harness is not pinned and that is a hard stop, not a warning.
+if [ ! -s "$HERE/HARNESS.sha256" ]; then
+  echo "FATAL: HARNESS.sha256 is missing or empty — the harness is unpinned."; exit 1
+fi
+if ! ( cd "$HERE" && sha256sum -c --quiet HARNESS.sha256 ) ; then
+  echo "FATAL: a harness file does not match its pin. The button you are running"
+  echo "is not the button that was reviewed."; exit 1
+fi
+echo "  sources valid; $(wc -l < "$HERE/HARNESS.sha256") harness files match their pins"
+
+# ── Phase 1: the two-button seam ────────────────────────────────────────────
+# The mirror of check.sh's Phase 1b. Each button reads the other's manifest, so
+# a new Proofs/ScalarX.lean cannot be absent from one by exemption and from the
+# other by omission — which is exactly what it was until today.
+echo "=== Phase 1: two-button seam ==="
+SEAMFAIL=0
+MAIN_SH="$HERE/check.sh"
+if [ ! -f "$MAIN_SH" ]; then
+  echo "  FATAL: check.sh is absent — most of the corpus would go unchecked."; exit 1
+fi
+MAIN_MANIFEST=$(sed -n '/^PROOFS=(/,/^)/p' "$MAIN_SH" | grep -oE '^  [A-Za-z][A-Za-z0-9]*' | tr -d ' ' | sort -u)
+if [ -z "$MAIN_MANIFEST" ]; then
+  echo "  FATAL: could not read check.sh's manifest; refusing to guess its scope."; exit 1
+fi
+SCALAR_MANIFEST=$(printf '%s\n' "${PROOFS[@]}" | sort -u)
+for f in "$HERE"/Proofs/*.lean; do
+  b=$(basename "$f" .lean)
+  case "$b" in AxiomCheck|Inventory|InventoryBasic|InventoryCore|InventoryScalar) continue;; esac
+  inm=0; ins=0
+  grep -qx "$b" <<<"$MAIN_MANIFEST"   && inm=1
+  grep -qx "$b" <<<"$SCALAR_MANIFEST" && ins=1
+  if [ $((inm + ins)) -eq 0 ]; then
+    echo "  ORPHAN: Proofs/$b.lean is in NEITHER manifest — compiled and audited by no button"; SEAMFAIL=1
+  elif [ $((inm + ins)) -eq 2 ]; then
+    echo "  DOUBLE-CLAIMED: Proofs/$b.lean is in BOTH manifests"; SEAMFAIL=1
+  fi
+done
+[ "$SEAMFAIL" = 0 ] && echo "  every proof source belongs to exactly one button"
+[ "$SEAMFAIL" = 0 ] || { echo "SEAM CHECK FAILED"; exit 1; }
+
+# ── Phase 2: compile ────────────────────────────────────────────────────────
+echo "=== Phase 2: compile (guarded) ==="
 cd "$AENEAS_LEAN"
 lake env bash -c "
   set -uo pipefail
   cd '$HERE/gen' && export LEAN_PATH=\"\$LEAN_PATH:\$PWD:$HERE\"
-  for m in ${GEN[*]}; do echo \"  · gen \$m\"; LEAN_TIMEOUT=300 LEAN_MEM_MB=6144 '$HERE/lean-guard' \"\$m.lean\" || exit 1; done
+  for m in ${GEN[*]}; do echo \"  · gen \$m\"; LEAN_TIMEOUT=$TIMEOUT LEAN_MEM_MB=6144 '$HERE/lean-guard' \"\$m.lean\" || exit 1; done
   cd '$HERE'
-  for m in ${PROOFS[*]}; do echo \"  · proof \$m\"; LEAN_TIMEOUT=300 LEAN_MEM_MB=4096 '$HERE/lean-guard' \"Proofs/\$m.lean\" || exit 1; done
+  for m in ${PROOFS[*]}; do echo \"  · proof \$m\"; LEAN_TIMEOUT=$TIMEOUT LEAN_MEM_MB=4096 '$HERE/lean-guard' \"Proofs/\$m.lean\" || exit 1; done
+  # NO NAME-PREFIX DEAD-FILE GATE HERE. A Scalar* NAME does not imply this
+  # button owns the file: Proofs/ScalarPackSpec.lean is in check.sh's manifest,
+  # and a prefix gate demanded it be in this one. Phase 1 above is the correct
+  # test and strictly stronger — it requires every proof source to be in
+  # EXACTLY ONE of the two manifests, by membership rather than by spelling.
 " || { echo FAIL; exit 1; }
-echo "=== Phase 3: axiom audit (kernel-level) ==="
+
+# ── Phase 2b: kernel-side axiom-declaration gate ────────────────────────────
+# The source-text grep this button used until today is evadable four ways on
+# Lean v4.30.0-rc2 (indented, @[simp], unsafe, and name-on-the-next-line — all
+# compile, none match an anchored pattern). Ask the kernel instead, reading the
+# compiled artifacts, exactly as check.sh Phase 2b does.
+echo "=== Phase 2b: kernel-side axiom-declaration gate ==="
+# The scanned set is this button's MANIFEST, not everything spelled Scalar*.
+# Proofs/ScalarPackSpec.lean is compiled by check.sh, so a glob swept in an
+# artifact this button does not own — and on a tree where check.sh had not run,
+# that olean is absent and the coverage count would fail for a false reason.
+SCALAR_OLEANS=$(printf '"%s.olean", ' "${PROOFS[@]}" | sed 's/, $//')
+GATE=$(mktemp "$HERE/.axgate-scalar-XXXX.lean")
+{
+  echo "import Lean"
+  echo "open Lean"
+  echo "def expected : List String := [$SCALAR_OLEANS]"
+  cat <<'LEANGATE'
+
+run_cmd do
+  let dir : System.FilePath := "Proofs"
+  let mut errs : Array String := #[]
+  let mut nMod := 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, which must be an error, not a skip.
+    unless (← p.pathExists) do
+      throwError "COVERAGE: {name} is in the manifest but its compiled artifact is absent"
+    nMod := nMod + 1
+    let (mod, _) ← readModuleData p
+    for ci in mod.constants do
+      if ci matches .axiomInfo _ then
+        errs := errs.push s!"  {name}: {ci.name}"
+  unless errs.isEmpty do
+    throwError "AXIOM DECLARED in the scalar layer:\n{String.intercalate "\n" errs.toList}"
+  logInfo s!"  kernel confirms: {nMod} compiled scalar modules (the manifest, by membership), none declares an axiom"
+LEANGATE
+} > "$GATE"
+cd "$AENEAS_LEAN"
+GATE_RC=0
+lake env bash -c "
+  set -uo 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=$?
+rm -f "$GATE" "${GATE%.lean}.olean"
+[ "$GATE_RC" -eq 0 ] || { echo "SCALAR AXIOM GATE FAILED"; exit 1; }
+
+# ── Phase 2c: declaration inventory ─────────────────────────────────────────
+# Until today these 13 modules were the only part of the proof corpus with no
+# declaration inventory: check.sh Phase 2c covers the main chain and named them
+# as uncovered on every run. This closes that.
+echo "=== Phase 2c: scalar declaration inventory ==="
+INVFAIL=0
+INVLOG=$(mktemp /tmp/check-scalar-inv-XXXX.log)
 cd "$AENEAS_LEAN"
 lake env bash -c "
+  set -uo pipefail
+  cd '$HERE/gen' && export LEAN_PATH=\"\$LEAN_PATH:\$PWD:$HERE\"
+  cd '$HERE'
+  LEAN_TIMEOUT=$TIMEOUT LEAN_MEM_MB=8192 '$HERE/lean-guard' Proofs/InventoryScalar.lean
+" > "$INVLOG" 2>&1 || { cat "$INVLOG"; echo "SCALAR INVENTORY COMPILE FAILED"; rm -f "$INVLOG"; exit 1; }
+OBS=$(mktemp /tmp/check-scalar-obs-XXXX.log)
+grep -E '^INV\|' "$INVLOG" > "$OBS"
+grep '^INV-COUNT|' "$INVLOG" | tail -1 >> "$OBS"
+"$HERE/inventory_gate.sh" "$OBS" "$HERE/inventory-allowlist-scalar.txt" || INVFAIL=1
+rm -f "$INVLOG" "$OBS"
+# The driver's corpus list must BE this script's manifest, both directions.
+COVERED=$(grep -oE '`Proofs\.[A-Za-z0-9]+' "$HERE/Proofs/InventoryScalar.lean" | sed 's/`Proofs\.//' | sort -u)
+for m in "${PROOFS[@]}"; do
+  grep -qx "$m" <<<"$COVERED" || { echo "  UNINVENTORIED: $m is compiled here but the driver does not cover it"; INVFAIL=1; }
+done
+while read -r m; do
+  [ -z "$m" ] && continue
+  case " ${PROOFS[*]} " in (*" $m "*) ;; (*) echo "  PHANTOM: driver claims $m, not in this manifest"; INVFAIL=1;; esac
+done <<<"$COVERED"
+[ "$INVFAIL" = 0 ] || { echo "SCALAR INVENTORY FAILED"; exit 1; }
+
+# ── Phase 3: per-certificate exact-cone audit ───────────────────────────────
+# Was: count the lines of #print axioms output that matched the clean cone and
+# compare against 13. A count cannot say WHICH certificate is clean, and it
+# passes just as happily if one certificate's cone is reported twice. Each
+# certificate is now asserted by name.
+echo "=== Phase 3: per-certificate exact-cone audit ==="
+cd "$AENEAS_LEAN"
+AUD_OUT=$(lake env bash -c "
   set -uo pipefail
   export LEAN_PATH=\"\$LEAN_PATH:$HERE/gen:$HERE\"
   cd '$HERE'
   AUD=\$(mktemp '$HERE/.audit-scalar-XXXX.lean')
-  { echo 'import Proofs.ScalarMain'; echo 'import Proofs.ScalarWideSpec'; echo 'import Proofs.ScalarUnpackSpec'; echo 'import Proofs.ScalarFromBytesSpec'; echo '#print axioms ScalarProofs.L_val'
-    echo '#print axioms ScalarProofs.sub_loop_spec'
-    echo '#print axioms ScalarProofs.sub_loop1_one_spec'; echo '#print axioms ScalarProofs.sub_val_spec'; echo '#print axioms ScalarProofs.add_val_spec'; echo '#print axioms ScalarProofs.mul_internal_spec'
-    echo '#print axioms ScalarProofs.part1_spec'; echo '#print axioms ScalarProofs.montgomery_reduce_spec'; echo '#print axioms ScalarProofs.mul_spec'; echo '#print axioms ScalarProofs.scalarImplementation'; echo '#print axioms ScalarProofs.montgomery_mul_spec'; echo '#print axioms ScalarProofs.bytes_unpack_spec'; echo '#print axioms ScalarProofs.from_bytes_wide_spec'; } > \"\$AUD\"
-  OUT=\$(LEAN_TIMEOUT=120 LEAN_MEM_MB=4096 '$HERE/lean-guard' \"\$AUD\" 2>&1)
-  echo \"\$OUT\"
+  { echo 'import Proofs.ScalarFromBytesSpec'; echo 'import Proofs.ScalarMain'; echo 'import Proofs.ScalarUnpackSpec'; echo 'import Proofs.ScalarWideSpec'
+    for c in ${CERTS[*]}; do echo \"#print axioms \$c\"; done; } > \"\$AUD\"
+  OUT=\$(LEAN_TIMEOUT=$TIMEOUT LEAN_MEM_MB=4096 '$HERE/lean-guard' \"\$AUD\" 2>&1)
   rm -f \"\$AUD\" \"\${AUD%.lean}.olean\"
-  N=\$(echo \"\$OUT\" | grep -cF \"depends on axioms: [propext, Classical.choice, Quot.sound]\" || true)
-  [ \"\$N\" -eq 13 ] || { echo \"AXIOM AUDIT FAILED: \$N/13 clean\"; exit 1; }
-" || { echo FAIL; exit 1; }
-echo "  L_val axiom-clean"
+  echo \"\$OUT\"
+") || { echo "$AUD_OUT"; echo "SCALAR AUDIT COMPILE FAILED"; exit 1; }
+FLAT=$(tr '\n' ' ' <<<"$AUD_OUT" | tr -s ' ')
+AUDFAIL=0
+for c in "${CERTS[@]}"; do
+  grep -qF "'$c' depends on axioms: $EXPECTED" <<<"$FLAT" \
+    || { echo "  NOT CLEAN or NOT FOUND: $c"; AUDFAIL=1; }
+done
+if [ "$AUDFAIL" != 0 ]; then
+  echo "SCALAR AXIOM AUDIT FAILED"; echo "$AUD_OUT" | tail -20 | sed 's/^/    /'; exit 1
+fi
+echo "  ${#CERTS[@]}/${#CERTS[@]} scalar certificates report exactly $EXPECTED"
 
 echo ""
-echo "SCALAR LAYER COMPLETE: add, sub, mul (Montgomery reduction, double round through RR) proven mod ℓ; aggregate certificate scalarImplementation kernel-audited."
+echo "SCALAR LAYER COMPLETE: add, sub, mul (Montgomery reduction, double round"
+echo "through RR) proven mod ℓ; aggregate certificate scalarImplementation"
+echo "kernel-audited; declaration surface inventoried; harness pinned."

verification/check.sh

@@ -37,6 +37,41 @@ TIMEOUT="${LEAN_TIMEOUT:-300}"
 export LEAN_MEM_MB="${LEAN_MEM_MB:-8192}"  # 8192: ReduceSpec exceeds 6144 (coherence pass 2)
 CORES="${LEAN_MAX_CORES:-0-3}"
 
+# ── Mode selection ──────────────────────────────────────────────────────────
+# --audit-only runs every gate EXCEPT the compile, against the .olean files a
+# previous full run left behind. It exists because gate work dominates this
+# estate's wall-clock: on 2026-07-29, 3.9 hours of a session went to Lean
+# re-elaborating proofs nobody had edited, while the audit phases themselves
+# take about fifteen seconds.
+#
+# IT MUST BE IMPOSSIBLE TO MISUSE, so:
+#   · it refuses to run unless a previous FULL run recorded a basis of source
+#     hashes AND every source still matches it byte-for-byte. Not mtimes —
+#     `touch` defeats those, and a stale-artifact check that fails open is
+#     worse than no shortcut at all, because a green button would then
+#     describe a corpus that is no longer on disk;
+#   · the basis file is build state, never committed, so a fresh clone cannot
+#     inherit permission to skip compiling;
+#   · the final banner DIFFERS, and says in words that the run is not evidence.
+#     A transcript must never be mistakable for a full one.
+AUDIT_ONLY=0
+for arg in "$@"; do
+  case "$arg" in
+    --audit-only) AUDIT_ONLY=1 ;;
+    --help|-h) echo "usage: check.sh [--audit-only]"; exit 0 ;;
+    *) echo "unknown argument: $arg (see --help)"; exit 1 ;;
+  esac
+done
+BASIS="$HERE/.audit-basis"          # gitignored build state, written by full runs
+
+# Every .lean this repository ships, with its hash: the exact set whose
+# recompilation --audit-only proposes to skip.
+source_basis() {
+  { find "$HERE/Proofs" -name '*.lean' -type f -printf '%P\n' | sed 's|^|Proofs/|'
+    find "$HERE/gen" -name '*.lean' -type f -printf '%P\n' | sed 's|^|gen/|'; } \
+  | LC_ALL=C sort | while read -r f; do printf '%s  %s\n' "$(sha256sum "$HERE/$f" | cut -d' ' -f1)" "$f"; done
+}
+
 # Layer manifests (extended as the pyramid grows; ORDER = import order).
 GEN_MODULES=(
   CurveField/TypesExternal
@@ -205,9 +240,14 @@ echo "  $(wc -l < "$HERE/GEN-MODEL.sha256") extracted-model files match their pi
 # the audit driver, the committed manifests, the policy tables — cannot be
 # discovered that way and are listed explicitly.
 HARNESS_EXTRA=(
-  AUDIT-MANIFEST.txt      # the statement block Phase 3c's digest is taken over
-  GEN-MODEL.sha256        # the extracted-model pins Phase 0b enforces
-  Proofs/Audit.lean       # the audit driver: it computes the digest it is judged by
+  AUDIT-MANIFEST.txt        # the statement block Phase 3c's digest is taken over
+  GEN-MODEL.sha256          # the extracted-model pins Phase 0b enforces
+  inventory-allowlist.txt   # the audit surface Phase 2c diffs against
+  inventory-allowlist-scalar.txt # the scalar layer's audit surface (second button)
+  Proofs/Audit.lean         # the audit driver: it computes the digest it is judged by
+  Proofs/InventoryCore.lean # inventory machinery
+  Proofs/InventoryScalar.lean # inventory driver: the scalar layer
+  Proofs/Inventory.lean     # inventory driver: main chain
 )
 echo "=== Phase 0c: harness integrity ==="
 if [ ! -s "$HERE/HARNESS.sha256" ]; then
@@ -248,7 +288,80 @@ if grep -rnE '^(private |protected |noncomputable )*axiom ' "$HERE"/Proofs/*.lea
 fi
 echo "  clean: no trivial stubs, no True targets, no axioms outside gen/"
 
+# ── Phase 1b: the two-button seam ───────────────────────────────────────────
+# WHY. This repository is checked by TWO buttons: this script covers the field,
+# curve and signature layers, and check-scalar.sh covers the scalar layer.
+# Until 2026-07-30 neither asserted anything about the other's scope, and this
+# script's dead-file gate simply SKIPPED anything named Scalar*. A new
+# Proofs/ScalarX.lean was therefore gated by nothing at all: absent from this
+# manifest by exemption, absent from the other by omission, compiled by
+# neither, inventoried by neither.
+#
+# The fix is mutual: each button reads the OTHER's manifest and asserts that
+# every shipped proof source belongs to exactly one of them. Both directions,
+# so a file can neither fall between the two nor be claimed by both.
+echo "=== Phase 1b: two-button seam ==="
+SEAMFAIL=0
+SCALAR_SH="$HERE/check-scalar.sh"
+if [ ! -f "$SCALAR_SH" ]; then
+  echo "  FATAL: check-scalar.sh is absent — half the corpus would go unchecked."
+  exit 1
+fi
+SCALAR_MANIFEST=$(grep -m1 '^PROOFS=(' "$SCALAR_SH" | sed 's/^PROOFS=(//; s/).*$//' | tr ' ' '\n' | sed '/^$/d' | sort -u)
+if [ -z "$SCALAR_MANIFEST" ]; then
+  echo "  FATAL: could not read check-scalar.sh's manifest; refusing to guess its scope."
+  exit 1
+fi
+MAIN_MANIFEST=$(printf '%s\n' "${PROOFS[@]}" | sort -u)
+# 1. Every shipped proof source belongs to exactly one manifest.
+for f in "$HERE"/Proofs/*.lean; do
+  b=$(basename "$f" .lean)
+  case "$b" in AxiomCheck|Inventory|InventoryBasic|InventoryCore|InventoryScalar) continue;; esac
+  inm=0; ins=0
+  grep -qx "$b" <<<"$MAIN_MANIFEST"   && inm=1
+  grep -qx "$b" <<<"$SCALAR_MANIFEST" && ins=1
+  if [ $((inm + ins)) -eq 0 ]; then
+    echo "  ORPHAN: Proofs/$b.lean is in NEITHER manifest — compiled and audited by no button"; SEAMFAIL=1
+  elif [ $((inm + ins)) -eq 2 ]; then
+    echo "  DOUBLE-CLAIMED: Proofs/$b.lean is in BOTH manifests — the buttons disagree about scope"; SEAMFAIL=1
+  fi
+done
+# 2. Neither manifest may name a file that does not exist.
+while read -r m; do
+  [ -z "$m" ] && continue
+  [ -f "$HERE/Proofs/$m.lean" ] || { echo "  PHANTOM: check-scalar.sh lists $m, which does not exist"; SEAMFAIL=1; }
+done <<<"$SCALAR_MANIFEST"
+[ "$SEAMFAIL" = 0 ] && echo "  every proof source belongs to exactly one button ($(grep -c . <<<"$MAIN_MANIFEST") here, $(grep -c . <<<"$SCALAR_MANIFEST") scalar)"
+[ "$SEAMFAIL" = 0 ] || { echo "SEAM CHECK FAILED"; exit 1; }
 # ── Phase 2: compile everything shipped ─────────────────────────────────────
+if [ "$AUDIT_ONLY" = 1 ]; then
+  echo "=== Phase 2: SKIPPED (--audit-only) ==="
+  if [ ! -s "$BASIS" ]; then
+    echo "REFUSING: no basis from a previous full run ($BASIS absent)."
+    echo "  --audit-only may only follow a full green run in this working tree."
+    echo "  Run ./check.sh with no arguments first."
+    exit 1
+  fi
+  if ! diff -q <(source_basis) "$BASIS" >/dev/null 2>&1; then
+    echo "REFUSING: the sources no longer match the basis of the last full run."
+    echo "  The .olean files on disk describe a corpus that has changed, so every"
+    echo "  audit below would be judging artifacts that no source produces."
+    echo "  Differences (< basis, > now):"
+    diff <(source_basis) "$BASIS" | head -20 | sed 's/^/    /'
+    echo "  Run ./check.sh with no arguments."
+    exit 1
+  fi
+  # Fail closed on absence too: a source with no artifact cannot be audited.
+  MISSING=0
+  for m in "${PROOFS[@]}"; do
+    [ -f "$HERE/Proofs/$m.olean" ] || { echo "  MISSING ARTIFACT: Proofs/$m.olean"; MISSING=1; }
+  done
+  for m in "${GEN_MODULES[@]}"; do
+    [ -f "$HERE/gen/$m.olean" ] || { echo "  MISSING ARTIFACT: gen/$m.olean"; MISSING=1; }
+  done
+  [ "$MISSING" = 0 ] || { echo "REFUSING: run ./check.sh with no arguments."; exit 1; }
+  echo "  sources byte-identical to the last full run's basis; $(grep -c . "$BASIS") files"
+else
 echo "=== Phase 2: compile ==="
 LOG=$(mktemp /tmp/check-compile-XXXX.log)
 cd "$AENEAS_LEAN"
@@ -269,6 +382,11 @@ lake env bash -c "
   for f in Proofs/*.lean; do
     b=\$(basename \"\$f\" .lean)
     [ \"\$b\" = AxiomCheck ] && continue
+    # Inventory drivers are compiled by Phase 2c, not here: they must elaborate
+    # with the corpus already in the environment, and the two of them cannot be
+    # imported together. They are NOT unchecked — Phase 2b reads their compiled
+    # .olean like every other module, and Phase 0c pins their sources.
+    case \"\$b\" in Inventory|InventoryBasic|InventoryCore|InventoryScalar) continue;; esac
     case \"\$b\" in Scalar*) continue;; esac  # scalar layer: checked by check-scalar.sh (coherence pass 2)
     case \" ${PROOFS[*]} \" in (*\" \$b \"*) ;; (*) echo \"DEAD FILE: \$f not in check manifest\"; exit 1;; esac
   done
@@ -276,6 +394,7 @@ lake env bash -c "
 if grep -q "uses 'sorry'" "$LOG"; then
   echo "STUB DETECTED: a compiled declaration uses 'sorry'"; exit 1; fi
 rm -f "$LOG"
+fi
 
 # ── Phase 2b: kernel-side axiom-declaration gate ────────────────────────────
 # WHY THIS EXISTS. Phase 1's anti-smuggling check reads SOURCE TEXT, and a
@@ -354,6 +473,88 @@ if [ "$GATE_RC" -ne 0 ]; then
   exit 1
 fi
 
+# ── Phase 2c: environment-derived declaration inventory ─────────────────────
+# WHAT THIS ADDS over Phase 2b. Phase 2b asks the kernel whether any AXIOM is
+# declared under Proofs/. It says nothing about the ~3000 other declarations:
+# a `def` or `theorem` whose cone quietly acquired an oracle, a declaration
+# renamed, added or removed, or a compiler-generated auxiliary that changed
+# shape, all pass 2b unremarked.
+#
+# This phase pins the whole surface. Every constant originating in an audited
+# module contributes NAME, MODULE, KIND and full AXIOM CONE, and the observed
+# set must equal inventory-allowlist.txt EXACTLY, both directions:
+# UNCLASSIFIED (in the environment, not allowlisted) and STALE (allowlisted,
+# not in the environment) are both build failures.
+#
+# PORTED from ltl-accumulator-verified, where a nine-attack self-test proved a
+# source-regex enumerator evadable by attributed, private, indented and
+# `instance` declarations and by a nested-namespace basename collision.
+#
+# TWO DRIVERS, because this corpus cannot be imported as one environment:
+# Proofs.Basic and Proofs.ConstSpecs both declare CurveFieldProofs.zero_spec.
+# The records carry their originating module precisely so those two remain
+# distinct entries — keyed on name alone they were byte-identical, and the
+# merged allowlist covered 3022 declarations with 3021 entries.
+echo "=== Phase 2c: environment-derived declaration inventory ==="
+INVFAIL=0
+INVLOG=$(mktemp /tmp/check-inv-XXXX.log)
+cd "$AENEAS_LEAN"
+# The DRIVERS are discovered, not listed: whether this corpus needs one or two
+# is a per-repo fact (dalek and anza cannot import Proofs.Basic together with
+# Proofs.ConstSpecs; risc0 and betrusted have no Proofs.Basic at all). A
+# hardcoded pair would silently look for a file that does not exist here.
+DRIVERS=$(ls "$HERE"/Proofs/Inventory*.lean 2>/dev/null | xargs -r -n1 basename \
+          | sed 's/\.lean$//' | grep -vE '^(InventoryCore|InventoryScalar)$' | sort)
+# InventoryScalar belongs to check-scalar.sh, which compiles the modules it
+# covers. Globbing Inventory*.lean swept it in here, after which this phase
+# correctly complained that its own manifest lacks the scalar modules.
+if [ -z "$DRIVERS" ]; then
+  echo "  NO INVENTORY DRIVER FOUND — the audit surface would go unchecked."; exit 1
+fi
+N_DRIVERS=$(printf '%s\n' "$DRIVERS" | grep -c .)
+for drv in $DRIVERS; do
+  lake env bash -c "
+    set -uo pipefail
+    cd '$HERE/gen' && export LEAN_PATH=\"\$LEAN_PATH:\$PWD:$HERE\"
+    cd '$HERE'
+    LEAN_TIMEOUT=$TIMEOUT LEAN_MEM_MB=8192 '$HERE/lean-guard' Proofs/$drv.lean
+  " >> "$INVLOG" 2>&1 || { cat "$INVLOG"; echo "INVENTORY COMPILE FAILED ($drv)"; rm -f "$INVLOG"; exit 1; }
+done
+# Reconcile the two trailers into one. Summing them and comparing against the
+# lines actually collected preserves the integrity property in the presence of
+# the split: truncation in EITHER driver shows up as a mismatch.
+N_TRAILERS=$(grep -c '^INV-COUNT|' "$INVLOG")
+if [ "$N_TRAILERS" -ne "$N_DRIVERS" ]; then
+  echo "  INVENTORY INCOMPLETE: expected a count trailer from each of the $N_DRIVERS driver(s), saw $N_TRAILERS"
+  INVFAIL=1
+fi
+SUM=$(grep '^INV-COUNT|' "$INVLOG" | cut -d'|' -f2 | paste -sd+ - | bc)
+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 drivers' corpus lists must together BE the compile manifest, minus the
+# audit infrastructure and the scalar layer. Checked in both directions so a
+# module cannot fall between the two drivers, and NO SILENT TRUNCATION: what
+# this phase does not cover is named on stdout every run.
+COVERED=$(for d in $DRIVERS; do grep -ohE '`Proofs\.[A-Za-z0-9]+' "$HERE/Proofs/$d.lean"; done \
+          | sed 's/`Proofs\.//' | sort -u)
+for m in "${PROOFS[@]}"; do
+  case "$m" in Audit|Inventory|InventoryBasic|InventoryCore) continue;; esac
+  grep -qx "$m" <<<"$COVERED" || { echo "  UNINVENTORIED: $m is compiled by this script but no driver covers it"; INVFAIL=1; }
+done
+while read -r m; do
+  [ -z "$m" ] && continue
+  case " ${PROOFS[*]} " in (*" $m "*) ;; (*) echo "  PHANTOM: driver claims $m, which this script does not compile"; INVFAIL=1;; esac
+done <<<"$COVERED"
+for f in "$HERE"/Proofs/*.lean; do
+  b=$(basename "$f" .lean)
+  case "$b" in Audit|Inventory|InventoryBasic|InventoryCore|InventoryScalar) continue;; esac
+  grep -qx "$b" <<<"$COVERED" || echo "  NOT INVENTORIED HERE (separate button): Proofs/$b.lean"
+done
+[ "$INVFAIL" = 0 ] || { echo "INVENTORY COVERAGE FAILED"; exit 1; }
 # ── Phase 3: axiom audit of every certificate ───────────────────────────────
 echo "=== Phase 3: axiom audit ==="
 EXPECTED="[propext, Classical.choice, Quot.sound]"
@@ -500,6 +701,22 @@ fi
 grep -o 'statement audit PASSED:.*' <<<"$AUD_OUT" | sed 's/^/  /'
 echo "  audit-manifest sha256 = $GOT_SHA (matches the committed block byte-for-byte)"
 
+# ── Phases end ──────────────────────────────────────────────────────────────
+# Sentinel. Self-tests lift a phase by scanning from its header to the NEXT
+# marker; without this the final phase's lift ran to end-of-file and picked up
+# everything appended afterwards. Do not remove: anything added below this line
+# would otherwise silently become part of the last phase from a lifter's point
+# of view.
+
 echo ""
+if [ "$AUDIT_ONLY" = 1 ]; then
+  echo "AUDIT-ONLY RUN — GATES PASSED, PROOFS NOT RECOMPILED."
+  echo "This is NOT evidence: the kernel did not re-elaborate a single proof in"
+  echo "this run. It says the gates accept the artifacts a previous full run"
+  echo "left behind. For a recorded result, run ./check.sh with no arguments."
+  exit 0
+fi
+# Only a full run earns the right to let a later --audit-only skip compiling.
+source_basis > "$BASIS"
 echo "ALL PROOFS PASS. ALL CERTIFICATES AXIOM-CLEAN. NO DEAD FILES."
 echo "STATEMENTS AND SPECIFICATIONS BOUND TO THE COMMITTED AUDIT MANIFEST."

verification/inventory_gate.sh

@@ -0,0 +1,64 @@
+#!/usr/bin/env bash
+# ─────────────────────────────────────────────────────────────────────────────
+# inventory_gate.sh — diff an observed environment inventory against the
+# pinned allowlist. PORTED VERBATIM from ltl-accumulator-verified apart from
+# the axiom-surface assertion, which is repo-specific: there the corpus admits
+# exactly one sanctioned axiom, here it admits none.
+#
+# This is THE production coverage gate: check.sh Phase 2c calls it, and the
+# self-test exercises this exact script — the tested logic IS the shipping
+# logic.
+#
+# Usage: inventory_gate.sh <observed-lean-output> <allowlist-file>
+#
+# Fail-closed in BOTH directions:
+#   UNCLASSIFIED — constant in the environment, absent from the allowlist
+#                  (new/renamed decl, changed kind, or changed axiom cone)
+#   STALE        — allowlist entry absent from the environment
+# plus an output-integrity check: the INV-COUNT trailer emitted by
+# Proofs/Inventory.lean must equal the number of INV lines actually seen,
+# so a truncated or crashed run can never pass as an empty diff.
+# ─────────────────────────────────────────────────────────────────────────────
+set -uo pipefail
+export LC_ALL=C   # byte-order collation: sort/comm must agree with Lean's String order
+obs_file="$1"; allow_file="$2"
+
+OBS=$(grep '^INV|' "$obs_file" | sort -u)
+N_OBS=$(printf '%s' "$OBS" | grep -c '^INV|' || true)
+TRAILER=$(grep '^INV-COUNT|' "$obs_file" | tail -1 | cut -d'|' -f2)
+if [ -z "$TRAILER" ] || [ "$TRAILER" != "$N_OBS" ]; then
+  echo "  INVENTORY TRUNCATED: trailer=${TRAILER:-absent}, observed $N_OBS lines"
+  exit 1
+fi
+
+ALLOW=$(grep '^INV|' "$allow_file" | sort -u)
+FAILGATE=0
+UNCLASS=$(comm -23 <(printf '%s\n' "$OBS") <(printf '%s\n' "$ALLOW"))
+STALE=$(comm -13 <(printf '%s\n' "$OBS") <(printf '%s\n' "$ALLOW"))
+if [ -n "$UNCLASS" ]; then
+  printf '%s\n' "$UNCLASS" | sed 's/^/  UNCLASSIFIED (in environment, not allowlisted): /'
+  FAILGATE=1
+fi
+if [ -n "$STALE" ]; then
+  printf '%s\n' "$STALE" | sed 's/^/  STALE (allowlisted, not in environment): /'
+  FAILGATE=1
+fi
+
+# The audited corpus admits NO axiom declarations at all: the sanctioned
+# external models live in gen/, outside every module these drivers cover, and
+# are byte-pinned by Phase 0b. An axiom appearing here would be a declaration
+# smuggled into the proof corpus, which Phase 2b also catches kernel-side —
+# two independent gates on the same property, deliberately.
+AXLINES=$(printf '%s\n' "$OBS" | grep '|axiom|' || true)
+if [ -n "$AXLINES" ]; then
+  echo "  AXIOM SURFACE DRIFT: the audited corpus must declare no axioms; observed:"
+  printf '%s\n' "$AXLINES" | sed 's/^/    /'
+  FAILGATE=1
+fi
+
+# The message must describe what was actually checked. It said "single
+# sanctioned axiom" when ported, which is the accumulator's policy; here the
+# audited corpus permits NONE, and a success line describing a different rule
+# is how an assertion quietly stops meaning anything.
+[ "$FAILGATE" = 0 ] && echo "  inventory gate: $N_OBS constants, environment == allowlist, zero axioms declared in the audited corpus"
+exit "$FAILGATE"

verification/selftest-auditonly.sh

@@ -0,0 +1,112 @@
+#!/usr/bin/env bash
+# ─────────────────────────────────────────────────────────────────────────────
+# selftest-auditonly.sh — adversarial self-test for check.sh --audit-only.
+#
+# --audit-only skips recompilation, which makes it the most dangerous thing in
+# this repository: if it ever accepted a tree whose sources had changed, a green
+# transcript would describe a corpus that is not on disk. Its whole safety rests
+# on refusing, so refusal is what this tests.
+#
+# Cases, each asserting a SPECIFIC diagnostic:
+#   0  no basis recorded                     -> REFUSING, may only follow a full run
+#   1  a proof source edited by one comment  -> REFUSING, sources no longer match
+#   2  a proof source DELETED                -> REFUSING (the basis lists it)
+#   3  a NEW proof source added              -> ORPHAN, from the seam check,
+#      which runs BEFORE the mode gate and catches it first
+#   4  an artifact deleted, sources intact   -> MISSING ARTIFACT
+#   5  the basis file truncated              -> REFUSING (mismatch, not a pass)
+#   6  mtimes touched but bytes unchanged    -> PASSES, because bytes are the
+#      test and mtimes are not: `touch` must neither grant nor deny permission
+#
+# Requires a prior full green run in this tree (that is what writes the basis).
+# No Lean runs here; the whole thing takes seconds.
+# ─────────────────────────────────────────────────────────────────────────────
+set -uo pipefail
+HERE="$(cd "$(dirname "$0")" && pwd)"
+FAILURES=0
+STASH="$(mktemp -d)"
+BASIS="$HERE/.audit-basis"
+VICTIM_SRC="Proofs/FeQ.lean"
+VICTIM_ART="Proofs/FeQ.olean"
+NEWSRC="$HERE/Proofs/ZZAuditOnlyProbe.lean"
+
+cleanup() {
+  [ -f "$STASH/basis" ]  && cp "$STASH/basis" "$BASIS"
+  [ -f "$STASH/src" ]    && cp "$STASH/src" "$HERE/$VICTIM_SRC"
+  [ -f "$STASH/art" ]    && cp "$STASH/art" "$HERE/$VICTIM_ART"
+  rm -f "$NEWSRC" "${NEWSRC%.lean}.olean"
+  rm -rf "$STASH"
+}
+trap cleanup EXIT INT TERM
+
+if [ ! -s "$BASIS" ]; then
+  echo "FATAL: no basis in this tree. Run ./check.sh with no arguments first;"
+  echo "this self-test exercises --audit-only, which requires one."
+  exit 1
+fi
+cp "$BASIS" "$STASH/basis"
+cp "$HERE/$VICTIM_SRC" "$STASH/src"
+cp "$HERE/$VICTIM_ART" "$STASH/art"
+
+expect() {  # expect <label> <want-rc> <want-substring>
+  local label="$1" want_rc="$2" want_txt="$3" out rc
+  out=$( cd "$HERE" && ./check.sh --audit-only 2>&1 ); rc=$?
+  if [ "$rc" -ne "$want_rc" ]; then
+    echo "  ✗ $label: exit $rc, expected $want_rc"; tail -6 <<<"$out" | sed 's/^/      /'
+    FAILURES=$((FAILURES+1)); return
+  fi
+  if ! grep -qF "$want_txt" <<<"$out"; then
+    echo "  ✗ $label: exit code right, diagnostic wrong (refused for the wrong reason)"
+    echo "      wanted: $want_txt"; tail -6 <<<"$out" | sed 's/^/      /'
+    FAILURES=$((FAILURES+1)); return
+  fi
+  echo "  ✓ $label"
+}
+
+echo "=== selftest-auditonly: attacking check.sh --audit-only ==="
+
+expect "control: unchanged tree passes" 0 "sources byte-identical to the last full run"
+
+rm -f "$BASIS"
+expect "case 0: no basis recorded" 1 "may only follow a full green run"
+cp "$STASH/basis" "$BASIS"
+
+printf '\n-- selftest\n' >> "$HERE/$VICTIM_SRC"
+expect "case 1: a proof source edited by one comment" 1 "no longer match the basis"
+cp "$STASH/src" "$HERE/$VICTIM_SRC"
+
+mv "$HERE/$VICTIM_SRC" "$STASH/moved"
+expect "case 2: a proof source deleted" 1 "no longer match the basis"
+mv "$STASH/moved" "$HERE/$VICTIM_SRC"
+
+# A new source is refused EARLIER than the basis comparison: the seam check
+# (Phase 1b) runs first and reports it as belonging to no manifest. Asserting
+# the seam's diagnostic rather than the basis's is not a weaker test — it is the
+# true one, and demanding the basis message here would go red the day the seam
+# check does its job.
+printf 'namespace ZZProbe\ntheorem t : 1 = 1 := rfl\nend ZZProbe\n' > "$NEWSRC"
+expect "case 3: a new proof source added -> caught by the seam check first" 1 "is in NEITHER manifest"
+rm -f "$NEWSRC"
+
+mv "$HERE/$VICTIM_ART" "$STASH/movedart"
+expect "case 4: an artifact deleted, sources intact" 1 "MISSING ARTIFACT"
+mv "$STASH/movedart" "$HERE/$VICTIM_ART"
+
+head -3 "$STASH/basis" > "$BASIS"
+expect "case 5: the basis truncated" 1 "no longer match the basis"
+cp "$STASH/basis" "$BASIS"
+
+# BYTES, NOT MTIMES. Touching every source must change nothing: a check keyed on
+# timestamps would both deny this legitimate run and, worse, ACCEPT a modified
+# file whose mtime had been reset. Asserting the pass is what pins that choice.
+find "$HERE/Proofs" "$HERE/gen" -name '*.lean' -exec touch {} +
+expect "case 6: mtimes touched, bytes unchanged -> still passes" 0 "sources byte-identical to the last full run"
+
+echo ""
+if [ "$FAILURES" -eq 0 ]; then
+  echo "SELFTEST PASSED — --audit-only refuses every stale tree it was shown, and"
+  echo "accepts only one whose sources are byte-identical to the recorded basis."
+  exit 0
+fi
+echo "SELFTEST FAILED: $FAILURES case(s) did not behave as claimed."
+exit 1

verification/selftest-axgate.sh

@@ -43,13 +43,24 @@ DRIVER="$STASH/phase2b.sh"
   echo "HERE=\"$HERE\""
   echo 'AENEAS_LEAN="$AENEAS_HOME/backends/lean"'
   echo "TIMEOUT=$TIMEOUT; CORES=\"$CORES\""
-  sed -n '/^# ── Phase 2b/,/^# ── Phase 3/p' "$HERE/check.sh" | sed '$d'
+  # Stop at the NEXT phase marker, whatever it is called. A hardcoded
+  # terminator ("...to Phase 3") silently widens the moment a phase is
+  # inserted between the two: adding Phase 2c made this driver swallow 2c as
+  # well and die on variables that phase expects check.sh to have defined,
+  # which surfaced as the BASELINE failing — a self-test blaming a gate for
+  # its own extraction bug.
+  awk '/^# ── Phase 2b/{f=1} f&&/^# ── (Phase |Phases end)/&&!/Phase 2b/{exit} f{print}' "$HERE/check.sh"
 } > "$DRIVER"
 if [ "$(wc -l < "$DRIVER")" -lt 40 ]; then
   echo "FATAL: could not lift Phase 2b out of check.sh — the phase markers moved."
   echo "This self-test must attack the shipping gate; refusing to run against nothing."
   exit 1
 fi
+if [ "$(grep -c '^# ── Phase ' "$DRIVER")" -ne 1 ]; then
+  echo "FATAL: the lifted block spans more than one phase; the extraction is wrong."
+  grep '^# ── Phase ' "$DRIVER" | sed 's/^/    /'
+  exit 1
+fi
 
 expect() {   # expect <name> <expected-rc> <required-substring>
   local name="$1" want_rc="$2" want_txt="$3"

verification/selftest-inventory.sh

@@ -0,0 +1,108 @@
+#!/usr/bin/env bash
+# ─────────────────────────────────────────────────────────────────────────────
+# selftest-inventory.sh — adversarial self-test for check.sh Phase 2c.
+#
+# WHAT PHASE 2c IS FOR. Phase 2b asks the kernel whether any AXIOM is declared
+# under Proofs/. It says nothing about the ~3000 other declarations. Phase 3
+# pins the cones of the 31 named certificates. Between them sits everything
+# else: a helper lemma that quietly acquired an oracle in its cone, a
+# declaration added, removed or renamed, a compiler-generated auxiliary that
+# changed shape. Phase 2c pins that whole surface and diffs it both ways.
+#
+# Cases, each asserting a SPECIFIC diagnostic:
+#   0  positive control: the untouched tree passes
+#   1  an allowlist row deleted        -> UNCLASSIFIED (in env, not allowlisted)
+#   2  an allowlist row invented       -> STALE (allowlisted, not in env)
+#   3  a cone silently widened         -> BOTH, because the record changed
+#   4  an axiom row appears            -> AXIOM SURFACE DRIFT
+#   5  the count trailer disagrees     -> INVENTORY TRUNCATED (no vacuous pass)
+#
+# It runs the SHIPPING inventory_gate.sh against a recorded observation, so no
+# Lean is needed and the whole thing takes a second. The observation itself is
+# produced by check.sh Phase 2c; this test attacks the gate that judges it.
+# ─────────────────────────────────────────────────────────────────────────────
+set -uo pipefail
+HERE="$(cd "$(dirname "$0")" && pwd)"
+FAILURES=0
+STASH="$(mktemp -d)"
+trap 'rm -rf "$STASH"' EXIT INT TERM
+
+ALLOW="$HERE/inventory-allowlist.txt"
+[ -s "$ALLOW" ] || { echo "FATAL: inventory-allowlist.txt missing or empty"; exit 1; }
+
+# The observation a green run would produce: the allowlist itself plus a
+# trailer. Deriving it from the allowlist is exactly right for this test — the
+# question is whether the GATE reacts correctly to differences, and each case
+# below introduces one.
+mkobs() {  # mkobs <file> [extra-line...]
+  local out="$1"; shift
+  grep '^INV|' "$ALLOW" > "$out"
+  for l in "$@"; do printf '%s\n' "$l" >> "$out"; done
+  LC_ALL=C sort -o "$out" "$out"
+  echo "INV-COUNT|$(grep -c '^INV|' "$out")" >> "$out"
+}
+
+expect() {  # expect <label> <obs> <allow> <want-rc> <want-substring>
+  local label="$1" obs="$2" allow="$3" want_rc="$4" want_txt="$5" out rc
+  out=$("$HERE/inventory_gate.sh" "$obs" "$allow" 2>&1); rc=$?
+  if [ "$rc" -ne "$want_rc" ]; then
+    echo "  ✗ $label: exit $rc, expected $want_rc"; echo "$out" | sed 's/^/      /'
+    FAILURES=$((FAILURES+1)); return
+  fi
+  if ! grep -qF "$want_txt" <<<"$out"; then
+    echo "  ✗ $label: exit code right, diagnostic wrong (rejected for the wrong reason)"
+    echo "      wanted: $want_txt"; echo "$out" | sed 's/^/      /'
+    FAILURES=$((FAILURES+1)); return
+  fi
+  echo "  ✓ $label"
+}
+
+echo "=== selftest-inventory: attacking check.sh Phase 2c's gate ==="
+
+# ── 0. positive control ────────────────────────────────────────────────────
+mkobs "$STASH/obs.txt"
+expect "case 0 control: a faithful observation passes" "$STASH/obs.txt" "$ALLOW" 0 "environment == allowlist"
+
+# ── 1. a row deleted from the allowlist: the declaration is still there, so
+#      the gate must report it as unclassified rather than shrug.
+VICTIM=$(grep '^INV|' "$ALLOW" | grep '|theorem|' | head -1)
+grep -vxF "$VICTIM" "$ALLOW" > "$STASH/allow-short.txt"
+expect "case 1: allowlist row deleted -> UNCLASSIFIED" "$STASH/obs.txt" "$STASH/allow-short.txt" 1 "UNCLASSIFIED"
+
+# ── 2. a row invented in the allowlist: nothing in the environment matches it.
+cp "$ALLOW" "$STASH/allow-extra.txt"
+echo "INV|Proofs.Ghost|CurveFieldProofs.ghost_lemma|theorem|Classical.choice" >> "$STASH/allow-extra.txt"
+expect "case 2: allowlist row with no declaration -> STALE" "$STASH/obs.txt" "$STASH/allow-extra.txt" 1 "STALE"
+
+# ── 3. THE ONE THAT MATTERS: a cone silently widened. Same module, same name,
+#      same kind — only the axiom cone grew. Phases 2b and 3 both pass this:
+#      2b only looks for axiom DECLARATIONS, and 3 only pins the 31 named
+#      certificates. If the victim is not one of those, nothing else sees it.
+WIDENED=$(sed 's/$/,sha2.Sha512/' <<<"$VICTIM")
+mkobs "$STASH/obs-wide.txt"
+grep -vxF "$VICTIM" "$STASH/obs-wide.txt" > "$STASH/t" && mv "$STASH/t" "$STASH/obs-wide.txt"
+printf '%s\n' "$WIDENED" >> "$STASH/obs-wide.txt"
+LC_ALL=C sort -o "$STASH/obs-wide.txt" "$STASH/obs-wide.txt"
+echo "INV-COUNT|$(grep -c '^INV|' "$STASH/obs-wide.txt")" >> "$STASH/obs-wide.txt"
+expect "case 3: a cone widened by one oracle -> UNCLASSIFIED" "$STASH/obs-wide.txt" "$ALLOW" 1 "UNCLASSIFIED"
+
+# ── 4. an axiom appears in the audited corpus. The sanctioned external models
+#      live in gen/, outside every module the drivers cover, so any axiom here
+#      is a declaration smuggled into the proof corpus.
+mkobs "$STASH/obs-ax.txt" "INV|Proofs.FeQ|CurveFieldProofs.rogue|axiom|"
+expect "case 4: an axiom in the corpus -> AXIOM SURFACE DRIFT" "$STASH/obs-ax.txt" "$ALLOW" 1 "AXIOM SURFACE DRIFT"
+
+# ── 5. truncation. "Nothing found" and "nothing wrong" must not share a path:
+#      a crashed or cut-short run has to fail, not pass as an empty diff.
+grep '^INV|' "$ALLOW" | head -100 > "$STASH/obs-trunc.txt"
+echo "INV-COUNT|$(grep -c '^INV|' "$ALLOW")" >> "$STASH/obs-trunc.txt"
+expect "case 5: trailer disagrees with the lines -> INVENTORY TRUNCATED" "$STASH/obs-trunc.txt" "$ALLOW" 1 "INVENTORY TRUNCATED"
+
+echo ""
+if [ "$FAILURES" -eq 0 ]; then
+  echo "SELFTEST PASSED — Phase 2c's gate rejects surface drift in both directions,"
+  echo "for the stated reason in each case."
+  exit 0
+fi
+echo "SELFTEST FAILED: $FAILURES case(s) did not behave as claimed."
+exit 1

verification/selftest-statements.sh

@@ -68,7 +68,9 @@ build_driver() {
     sed -n '/^CERTS=(/,/^)/p' "$HERE/check.sh"
     # `$0` inside Phase 3c must resolve to the shipping check.sh, not to this
     # driver, or the apex-name recovery would read the wrong file.
-    sed -n '/^# ── Phase 3c/,/^echo ""$/p' "$HERE/check.sh" | sed '$d' \
+    # Stop at the next phase marker, not at a blank echo: a terminator that is
+    # not itself a phase boundary breaks the moment the phase's body changes.
+    awk '/^# ── Phase 3c/{f=1} f&&/^# ── (Phase |Phases end)/&&!/Phase 3c/{exit} f{print}' "$HERE/check.sh" \
       | sed "s|\"\$0\"|\"$HERE/check.sh\"|g"
   } > "$DRIVER"
   if [ "$(wc -l < "$DRIVER")" -lt 60 ]; then