From d73f8da92a1f5bb6fa0010798e66d8ad1180de0d Mon Sep 17 00:00:00 2001
From: Doll <dollspacegay@gmail.com>
Date: Tue, 28 Jul 2026 23:08:47 -0500
Subject: [PATCH 1/2] =?UTF-8?q?forge:=20check=20=E2=80=94=20weave=20the=20?=
 =?UTF-8?q?ADTs=20reachable=20through=20woven=20spec=20fns=20(closes=20#92?=
 =?UTF-8?q?)?=
MIME-Version: 1.0
Content-Type: text/plain; charset=UTF-8
Content-Transfer-Encoding: 8bit

No file declaring more than one ADT had ever certified. The per-item ADT weave
seeded `reachable_adt_deps` with `[item] + fn_deps`, while every arm of
`item_subprogram` weaves `item_spec_items` as well — the referrer set was a
strict subset of what the sub-program contained, so an ADT reachable only
through a woven spec fn was omitted from the emitted Verus and the run failed
closed on an unresolvable type.

Three surfaces of the one defect:

  1. a checked `struct`/`enum`: `collect_item_adt_refs` is inert on an ADT decl
     (field types are followed by the type-graph fixed point instead), so
     `adt_deps` came out empty for EVERY ADT item while the arm wove the file's
     whole `spec_items`. A spec fn naming a second ADT dangled -> L0 on E0425 ->
     `project assurance: FAILED`.
  2. a checked `fn` naming no ADT that a woven spec fn takes: the solver-vacuity
     harness failed to elaborate, which `vacuity_solver::interpret_summary`
     refuses as undetermined -> a `ForgeError` aborting the run.
  3. a checked `spec fn`: already correct, which is why the single-ADT corpus
     never exercised the gap.

A single ADT masks all of it: the only ADT is the checked item, which the ADT
arm pushes itself, so the decl is present by construction. Same
under-approximated-closure class as the `reachable_spec_fn_deps` body-only
omission recorded in proof-backends.md's increment-(i) note.

The seed now extends with `item_spec_items` for every item kind (replaced, not
extended, for `Item::SpecFn` — #71's distinct per-spec-fn sub-program), and the
ADT arm drops the checked item from `adt_deps` before pushing it so a spec fn
naming that ADT cannot produce a duplicate definition (E0428).

DESIGN SOURCES THIS ITERATION:
  - .design/forge/check.md (REQ-1 per-item pipeline, REQ-5 L3 iff 0 errors)
  - .design/basis/09-option-result.md, .design/basis/11-ergonomics.md,
    .design/basis/12-mutual-recursion.md, .design/lower/boundary-composition.md,
    .design/verified/proof-backends.md (the six docs routing check.rs)
  - thermite-design.md §5.3 (the isolated per-item sub-program), §6 (the ladder)
  - reference: conformance/sum.th, conformance/composition/cases.json

REQ STATUS:
  - REQ-1 (pipeline orchestration) SHIPPED — unchanged; this corrects its input.
  - REQ-5 (level determination) SHIPPED — unchanged; L3 iff verus reports 0
    errors. The ADT items were never un-provable, only un-emitted.
  R-HONEST-4: the correction is recorded as an Amendment in .design/forge/check.md.

VERIFICATION:
  cargo test -p forge: 807 passed, 2 failed — both pre-existing and
    environmental (strat_differential needs the Lean spine built locally;
    it fails identically on unmodified check.rs and does not reference it).
  new pin forge/tests/divergence_multi_adt_subprogram.rs: 4 passed. Confirmed a
    real pin — 3 of the 4 FAIL on pre-fix code (two assertion failures + the
    ForgeError abort); the 4th is the R-CHAR-3 oracle (a spare decl cannot
    change what is provable about its siblings, so every shared item's level
    must equal the single-ADT twin's) and holds on both sides by construction.
  conformance: multi_adt.th — pre-fix `Role`/`Action` both L0/E0425 and project
    FAILED; post-fix all five items L3, matching the hand-derived
    multi_adt.cert.json oracle subset.
  cargo clippy -p forge --all-targets -- -D warnings: PASS
  cargo fmt --all --check: PASS
  doc-drift: PASS (six check.rs-governing docs re-pinned)
  req-status / req-registry / control-plane: PASS
  verus 0.2026.05.24.ecee80a (the ci.yml pin)

Closes #92

Co-Authored-By: Claude Opus 5 (1M context) <noreply@anthropic.com>
---
 .design/basis/09-option-result.md             |   2 +-
 .design/basis/11-ergonomics.md                |   2 +-
 .design/basis/12-mutual-recursion.md          |   2 +-
 .design/forge/check.md                        |  25 +-
 .design/lower/boundary-composition.md         |   2 +-
 .design/verified/proof-backends.md            |   2 +-
 conformance/multi_adt.cert.json               |  11 +
 conformance/multi_adt.th                      |  25 ++
 forge/src/check.rs                            |  48 ++-
 .../tests/divergence_multi_adt_subprogram.rs  | 274 ++++++++++++++++++
 10 files changed, 378 insertions(+), 15 deletions(-)
 create mode 100644 conformance/multi_adt.cert.json
 create mode 100644 conformance/multi_adt.th
 create mode 100644 forge/tests/divergence_multi_adt_subprogram.rs

diff --git a/.design/basis/09-option-result.md b/.design/basis/09-option-result.md
index f14a151e0..bee6b123d 100644
--- a/.design/basis/09-option-result.md
+++ b/.design/basis/09-option-result.md
@@ -2,7 +2,7 @@
 <!--
 tier: 3-component
 status: draft
-audited-content-sha256: 3c6a908da157641805a57c3f1ff18215ad79c8cf09a496d3a9d8a1dc043bc0e8 (migrated from legacy audited-sha commit pin to a squash-stable content digest; doc-drift-tripwire.md REQ-2 — content pin is primary, commit pin is a migration fallback)
+audited-content-sha256: f4468f28b2be3c453070beb9aa798b4f729b7acfda483325fa26fda1d0f02cce (migrated from legacy audited-sha commit pin to a squash-stable content digest; doc-drift-tripwire.md REQ-2 — content pin is primary, commit pin is a migration fallback)
 governs: thermite-syntax/src/ast.rs
 governs: thermite-syntax/src/parser.rs
 governs: thermite-spec/src/validator.rs
diff --git a/.design/basis/11-ergonomics.md b/.design/basis/11-ergonomics.md
index 3ea179af1..28317f82e 100644
--- a/.design/basis/11-ergonomics.md
+++ b/.design/basis/11-ergonomics.md
@@ -2,7 +2,7 @@
 <!--
 tier: 3-component
 status: draft
-audited-content-sha256: 3c6a908da157641805a57c3f1ff18215ad79c8cf09a496d3a9d8a1dc043bc0e8 (migrated from legacy audited-sha commit pin to a squash-stable content digest; doc-drift-tripwire.md REQ-2 — content pin is primary, commit pin is a migration fallback)
+audited-content-sha256: f4468f28b2be3c453070beb9aa798b4f729b7acfda483325fa26fda1d0f02cce (migrated from legacy audited-sha commit pin to a squash-stable content digest; doc-drift-tripwire.md REQ-2 — content pin is primary, commit pin is a migration fallback)
 governs: thermite-syntax/src/parser.rs
 governs: thermite-syntax/src/ast.rs
 governs: thermite-lower/src/lower.rs
diff --git a/.design/basis/12-mutual-recursion.md b/.design/basis/12-mutual-recursion.md
index 0cf1a271b..149ddf967 100644
--- a/.design/basis/12-mutual-recursion.md
+++ b/.design/basis/12-mutual-recursion.md
@@ -2,7 +2,7 @@
 <!--
 tier: 3-component
 status: draft
-audited-content-sha256: 5da96b53476e787c3488ff7769ef60bfada0c15797c235683d1fd57937c83946 (migrated from legacy audited-sha commit pin to a squash-stable content digest; doc-drift-tripwire.md REQ-2 — content pin is primary, commit pin is a migration fallback)
+audited-content-sha256: 1e54a3da3d503c5f98cea512c52a410166b42c6d3da09ee85137194fb899077e (migrated from legacy audited-sha commit pin to a squash-stable content digest; doc-drift-tripwire.md REQ-2 — content pin is primary, commit pin is a migration fallback)
 governs: forge/src/check.rs
 governs: thermite-lower/src/lower.rs
 thesis-refs:
diff --git a/.design/forge/check.md b/.design/forge/check.md
index f16c9a62d..a2c2d6264 100644
--- a/.design/forge/check.md
+++ b/.design/forge/check.md
@@ -3,7 +3,7 @@
 <!--
 tier: 3-component
 status: draft
-audited-content-sha256: a10f679dd2fd4ae2dad1fc8607c93d13413d0d019823f55b85f41b61e1578c7a (migrated from legacy audited-sha commit pin to a squash-stable content digest; doc-drift-tripwire.md REQ-2 — content pin is primary, commit pin is a migration fallback)
+audited-content-sha256: acc8e6a294496a3e18324b722bc17b92fa985dff2e36e274cc98134bc9feffe2 (migrated from legacy audited-sha commit pin to a squash-stable content digest; doc-drift-tripwire.md REQ-2 — content pin is primary, commit pin is a migration fallback)
 governs: forge/src/check.rs
 thesis-refs:
   - thermite-design.md §5.1
@@ -65,6 +65,29 @@ REQ status table).
 > widening, #101 equivalent-mutant exclusion, #232 struct-inv weave, #237
 > narrowing) extend the pipeline without contradicting the REQs above.
 
+> **Amendment 2026-07-28 (crosslink #92 — the ADT-referrer correction, R-HONEST-4).**
+> The per-item ADT weave (`#68`) seeded `reachable_adt_deps` with `[item] +
+> fn_deps` while every arm of `item_subprogram` wove `item_spec_items` as well, so
+> the referrer set was a strict subset of what the sub-program contained. An ADT
+> reachable only through a woven spec fn was omitted from the emitted Verus, and
+> the run failed closed on an unresolvable type. Three surfaces: a checked
+> `struct`/`enum` landed L0 on `E0425` (`collect_item_adt_refs` is inert on an ADT
+> decl, so `adt_deps` was empty for every ADT item) and dragged `project
+> assurance` to FAILED; a checked `fn` naming no ADT that a woven spec fn takes
+> aborted the run through `vacuity_solver::interpret_summary`'s undetermined-harness
+> refusal; a checked `spec fn` was already correct. A single-ADT file masked all
+> of it, because the only ADT is the checked item, which the ADT arm pushes itself
+> — so no corpus program declaring more than one ADT had ever certified. The seed
+> now extends with `item_spec_items` for every item kind (replaced, not extended,
+> for the `Item::SpecFn` arm — `#71`'s distinct per-spec-fn sub-program), and the
+> ADT arm drops the checked item from `adt_deps` before pushing it, keeping one
+> declaration. REQ-1's per-item pipeline and REQ-5's level rule are unchanged; this
+> corrects their input. Corpus anchor: `conformance/multi_adt.th` +
+> `conformance/multi_adt.cert.json`. Pin:
+> `forge/tests/divergence_multi_adt_subprogram.rs`. Same under-approximated-closure
+> class as the `reachable_spec_fn_deps` body-only omission recorded in
+> `.design/verified/proof-backends.md`'s increment-(i) build-blocker note.
+
 The stages, in order, are:
 
 ```
diff --git a/.design/lower/boundary-composition.md b/.design/lower/boundary-composition.md
index bd9b002b3..5b8f180ca 100644
--- a/.design/lower/boundary-composition.md
+++ b/.design/lower/boundary-composition.md
@@ -2,7 +2,7 @@
 <!--
 tier: 3-component
 status: draft
-audited-content-sha256: 5da96b53476e787c3488ff7769ef60bfada0c15797c235683d1fd57937c83946 (migrated from legacy audited-sha commit pin to a squash-stable content digest; doc-drift-tripwire.md REQ-2 — content pin is primary, commit pin is a migration fallback)
+audited-content-sha256: 1e54a3da3d503c5f98cea512c52a410166b42c6d3da09ee85137194fb899077e (migrated from legacy audited-sha commit pin to a squash-stable content digest; doc-drift-tripwire.md REQ-2 — content pin is primary, commit pin is a migration fallback)
 governs: thermite-lower/src/lower.rs, forge/src/check.rs
 thesis-refs:
   - thermite-design.md §9
diff --git a/.design/verified/proof-backends.md b/.design/verified/proof-backends.md
index 67c0ad748..fedee61df 100644
--- a/.design/verified/proof-backends.md
+++ b/.design/verified/proof-backends.md
@@ -3,7 +3,7 @@
 <!--
 tier: 3-component
 status: draft (v-next architecture — the obligation/engine interface; most REQs NOT-STARTED
-audited-content-sha256: 28f745f55a4e7bb8ddf941decb241d4473ed924790c5ddfa3b95711b973e111e (migrated from legacy audited-sha commit pin to a squash-stable content digest; doc-drift-tripwire.md REQ-2 — content pin is primary, commit pin is a migration fallback)
+audited-content-sha256: 633def0fca2b4b56f4930622ae0c64259ef0290a0b3ed9ba5634e0aaa08f9efb (migrated from legacy audited-sha commit pin to a squash-stable content digest; doc-drift-tripwire.md REQ-2 — content pin is primary, commit pin is a migration fallback)
         behind build blockers. The SHIPPED substrates this builds on are quoted-code-grounded.)
 governs: forge/src/check.rs + forge/src/degrade.rs + forge/src/manifest.rs (the discharge
          pipeline, the ladder, the certificate this interface generalizes) and
diff --git a/conformance/multi_adt.cert.json b/conformance/multi_adt.cert.json
new file mode 100644
index 000000000..7a8e45e86
--- /dev/null
+++ b/conformance/multi_adt.cert.json
@@ -0,0 +1,11 @@
+{
+  "item": "authorize",
+  "level": "L3",
+  "contract_quality": {
+    "tautology": false,
+    "vacuous_precondition": false
+  },
+  "effects": ["pure"],
+  "slag": false,
+  "note": "Stable-subset oracle (goal.md R-CHAR-3): item/level/tautology/vacuous_precondition/effects/slag are hand-derived from .design/forge/check.md REQ-5 (L3 iff verus reports 0 errors) + .design/basis/01-adts.md (REQ-2 enum, REQ-9 enum->Verus + match->Verus match) + thermite-design.md §6 ladder, and are oracle-compared. mutants_killed + solver_time_ms are tool-computed + EXCLUDED (oracle_subset, §5.3). HAND-DERIVATION: `authorize(r, a)` returns true for Owner (either Action), false for Player+Ban, true for Player+Chat. The ens `result == (may_ban(r) || !is_ban(a))` evaluates to: Owner -> may_ban true -> true (both actions); Player+Ban -> false || !true -> false; Player+Chat -> false || !false -> true. Body and contract agree on all four inhabitants of Role x Action, so every obligation discharges -> L3. NON-VACUOUS: a constant-true body fails at Player+Ban, so the ens constrains (R-DEFER-9); req `true` is satisfiable (a total function has no precondition). fx pure -> effects [\"pure\"]; no #[slag] -> slag false. THIS FILE IS THE crosslink #92 CORPUS ANCHOR: it is the first corpus program declaring more than one ADT, the shape that could not certify before #92 (the per-item sub-program omitted the ADTs reachable only through a woven spec fn, so `Role` and `Action` each landed L0 on E0425 and the project verdict was FAILED). The per-item levels of `Role`/`Action` are pinned in forge/tests/divergence_multi_adt_subprogram.rs."
+}
diff --git a/conformance/multi_adt.th b/conformance/multi_adt.th
new file mode 100644
index 000000000..1815aabec
--- /dev/null
+++ b/conformance/multi_adt.th
@@ -0,0 +1,25 @@
+enum Role { Owner, Player }
+enum Action { Ban, Chat }
+
+spec fn may_ban(r: Role) -> bool
+  dec r
+{
+  match r { Role::Owner => true, Role::Player => false }
+}
+
+spec fn is_ban(a: Action) -> bool
+  dec a
+{
+  match a { Action::Ban => true, Action::Chat => false }
+}
+
+fn authorize(r: Role, a: Action) -> bool
+  req true
+  ens result == (may_ban(r) || !is_ban(a))
+  fx  pure
+{
+  match r {
+    Role::Owner => true,
+    Role::Player => match a { Action::Ban => false, Action::Chat => true },
+  }
+}
diff --git a/forge/src/check.rs b/forge/src/check.rs
index 92e55b99e..87408873d 100644
--- a/forge/src/check.rs
+++ b/forge/src/check.rs
@@ -660,17 +660,38 @@ pub fn check_file_with_options(
             Item::SpecFn(_) => reachable_spec_fn_deps(&parsed.program, item.name()),
             _ => spec_items.clone(),
         };
-        // For a checked `Item::SpecFn`, the ADT referrers are its own reachable
-        // spec-fn set (which includes the spec fn itself), so its `enum`/`struct`
-        // decls are present even though the file's full `spec_items` is no longer
-        // woven (#71). The `Item::Fn` path is unchanged — its ADT referrers stay
-        // `[item] + fn_deps` exactly as before (the exec sub-program is byte-stable;
-        // the corpus cert oracle is unperturbed). The Fn arm of `item_subprogram`
-        // still weaves the full `spec_items`.
+        // #92: the referrer set covers everything `item_subprogram` weaves. Every
+        // arm of `item_subprogram` weaves `item_spec_items`, so the spec fns seed
+        // the ADT walk too — an ADT reachable only through a woven spec fn is
+        // otherwise absent from the sub-program and verus cannot resolve it
+        // (`E0425 cannot find type`).
+        //
+        // Before #92 the seed was `[item] + fn_deps`, a strict subset of what is
+        // woven, which surfaced three ways:
+        //   - a checked `struct`/`enum`: `collect_item_adt_refs` is inert on an ADT
+        //     decl (its own field types are followed by the type-graph fixed point
+        //     instead), so `adt_deps` came out empty for every ADT item, while the
+        //     ADT arm weaves the file's whole `spec_items`. A spec fn naming a
+        //     second ADT dangled, so the item landed L0 and the project verdict
+        //     FAILED. A single-ADT file hid this: the only ADT is the checked item,
+        //     which the ADT arm pushes itself.
+        //   - a checked `fn` whose contract and body name no ADT that a woven spec
+        //     fn takes: the solver-vacuity harness failed to elaborate, which
+        //     `vacuity_solver::interpret_summary` refuses as undetermined — a
+        //     `ForgeError` aborting the run (fail-closed, never a silent clean).
+        //   - a checked `spec fn`: already correct via the clear+extend below, which
+        //     is why the single-ADT corpus never exercised the gap.
+        // This is the same under-approximated-closure class the proof-backends
+        // build-blocker note records for `reachable_spec_fn_deps` walking
+        // `decl.body` without `decl.dec`.
+        //
+        // For a checked `Item::SpecFn` the referrers are its own reachable spec-fn
+        // closure alone (which includes the spec fn itself) — #71's distinct
+        // per-spec-fn sub-program — so the seed is replaced rather than extended.
         if matches!(item, Item::SpecFn(_)) {
             referrers.clear();
-            referrers.extend(item_spec_items.iter());
         }
+        referrers.extend(item_spec_items.iter());
         let adt_deps = reachable_adt_deps(&parsed.program, &referrers);
         let sub = item_subprogram(item, &item_spec_items, &fn_deps, &adt_deps);
         let lowered = thermite_lower::lower(&sub).map_err(ForgeError::Lower)?;
@@ -3874,7 +3895,16 @@ fn item_subprogram(
         // `adt_deps`/`spec_items` for an `inv`-free struct keeps the sub-program
         // the item alone (byte-stable for the no-invariant corpus).
         Item::Struct(_) | Item::Enum(_) => {
-            let mut items = adt_deps.to_vec();
+            // #92: since the referrer seed includes the woven `spec_items`, a spec
+            // fn naming the checked ADT puts that ADT in `adt_deps` as well. The
+            // item is pushed below, so drop it here to keep one declaration —
+            // verus rejects a duplicate definition (`E0428`). The other decls a
+            // spec fn reaches stay, which is the point of the fix.
+            let mut items: Vec<Item> = adt_deps
+                .iter()
+                .filter(|d| d.name() != item.name())
+                .cloned()
+                .collect();
             items.extend(spec_items.iter().cloned());
             items.push(item.clone());
             Program { items }
diff --git a/forge/tests/divergence_multi_adt_subprogram.rs b/forge/tests/divergence_multi_adt_subprogram.rs
new file mode 100644
index 000000000..e611e8251
--- /dev/null
+++ b/forge/tests/divergence_multi_adt_subprogram.rs
@@ -0,0 +1,274 @@
+//! Divergence pin (crosslink #92) — no file declaring more than one ADT could
+//! certify, because `forge::check`'s referrer seed for `reachable_adt_deps` was a
+//! strict subset of what `item_subprogram` weaves.
+//!
+//! Every arm of `item_subprogram` weaves `item_spec_items`, but only the
+//! `Item::SpecFn` arm seeded those spec fns as ADT referrers. An ADT reachable
+//! only through a woven spec fn was therefore absent from the emitted sub-program
+//! and verus could not resolve it. Three surfaces, all live-confirmed:
+//!
+//!   1. a checked `struct`/`enum`: `collect_item_adt_refs` is inert on an ADT decl
+//!      (field types are followed by the type-graph fixed point instead), so
+//!      `adt_deps` came out empty for every ADT item while the arm wove the file's
+//!      whole `spec_items` — a spec fn naming a second ADT dangled, the item landed
+//!      L0 on `E0425 cannot find type`, and `project assurance` was FAILED;
+//!   2. a checked `fn` whose contract and body name no ADT that a woven spec fn
+//!      takes: the solver-vacuity harness failed to elaborate, which
+//!      `vacuity_solver::interpret_summary` refuses as undetermined — a `ForgeError`
+//!      aborting the whole run;
+//!   3. a checked `spec fn`: already correct, which is why a single-ADT corpus
+//!      never exercised the gap.
+//!
+//! One ADT masks all of it: the only ADT is the checked item, which the ADT arm
+//! pushes itself, so the decl is present by construction. This is the same
+//! under-approximated-closure class `.design/verified/proof-backends.md` records
+//! for `reachable_spec_fn_deps` walking `decl.body` without `decl.dec`.
+//!
+//! The authority (R-CHAR-3): expected level L3 is the design contract —
+//! `.design/forge/check.md` REQ-5 (L3 iff verus reports 0 errors) +
+//! `thermite-design.md` §6 (L3 == a fully-discharged real-verus proof) +
+//! `.design/basis/01-adts.md` REQ-2/REQ-9 (enum -> Verus enum, match -> Verus
+//! match). The corpus anchor is `conformance/multi_adt.th` +
+//! `conformance/multi_adt.cert.json` (hand-derived). Adding a declaration that
+//! the rest of the file does not reference cannot change what is provable about
+//! the other items, so the single-ADT twin's levels ARE the oracle for the
+//! two-ADT file. Expected values never copied from the toolchain's output.
+//!
+//! Verus checks skip with an eprintln when verus is absent (`editor_runs.rs`
+//! precedent). `tests/` is not anti-pattern-gated, so `unwrap`/`panic!` are fine
+//! (R-APG-2).
+
+use std::path::{Path, PathBuf};
+use std::process::Command;
+
+use serde_json::Value;
+
+fn forge_bin() -> PathBuf {
+    PathBuf::from(env!("CARGO_BIN_EXE_forge"))
+}
+
+/// `true` iff verus is reachable (mirrors `divergence_struct_inv_spec_fn_subprogram.rs`).
+fn verus_present() -> bool {
+    if let Ok(p) = std::env::var("VERUS_BIN") {
+        if Path::new(&p).exists() {
+            return true;
+        }
+    }
+    if let Ok(out) = Command::new("which").arg("verus").output() {
+        if out.status.success() && !String::from_utf8_lossy(&out.stdout).trim().is_empty() {
+            return true;
+        }
+    }
+    if let Ok(home) = std::env::var("HOME") {
+        if PathBuf::from(home).join(".local/bin/verus").exists() {
+            return true;
+        }
+    }
+    false
+}
+
+/// Run `forge check --json` over an inline program. Panics with the captured
+/// stderr when the run aborts, which is itself surface 2's pre-fix symptom (a
+/// `ForgeError` from the vacuity harness, not a cert array).
+fn check_program(tag: &str, program: &str) -> Vec<Value> {
+    let fixture = std::env::temp_dir().join(format!(
+        "forge_multi_adt_subprog_{tag}_{}.th",
+        std::process::id()
+    ));
+    std::fs::write(&fixture, program).expect("write fixture");
+    let out = Command::new(forge_bin())
+        .arg("check")
+        .arg(&fixture)
+        .arg("--json")
+        .output()
+        .expect("spawn forge check");
+    let _ = std::fs::remove_file(&fixture);
+    let stdout = String::from_utf8_lossy(&out.stdout);
+    serde_json::from_str::<Value>(stdout.trim())
+        .unwrap_or_else(|e| {
+            panic!(
+                "[{tag}] forge check --json stdout must be one JSON doc: {e}\nstdout:\n{stdout}\nstderr:\n{}",
+                String::from_utf8_lossy(&out.stderr)
+            )
+        })
+        .as_array()
+        .unwrap_or_else(|| panic!("[{tag}] forge check --json must emit an array of certs"))
+        .clone()
+}
+
+fn level_of(certs: &[Value], item: &str) -> String {
+    certs
+        .iter()
+        .find(|c| c.get("item").and_then(|v| v.as_str()) == Some(item))
+        .unwrap_or_else(|| panic!("no cert for `{item}` in {certs:#?}"))["level"]
+        .as_str()
+        .unwrap_or_else(|| panic!("cert for `{item}` has no string level"))
+        .to_string()
+}
+
+/// Surface 1, the reported repro: two enums where a spec fn names only the first.
+/// `Unused` is declared and never mentioned again; pre-#92 it certified L0 with
+/// `E0425 cannot find type Role` — the dangling reference belonging to `is_owner`,
+/// which the ADT arm wove into `Unused`'s sub-program without `Role`.
+const SPARE_DECL_PROGRAM: &str = "\
+enum Role { Owner, Player }
+enum Unused { A, B }
+
+spec fn is_owner(r: Role) -> bool
+  dec r
+{
+  match r { Role::Owner => true, Role::Player => false }
+}
+
+fn check(r: Role) -> bool
+  req true
+  ens result == is_owner(r)
+  fx  pure
+{
+  match r { Role::Owner => true, Role::Player => false }
+}
+";
+
+/// The single-ADT twin of [`SPARE_DECL_PROGRAM`], byte-identical but for the
+/// spare `enum Unused` line. Its levels are the oracle for the two-ADT file.
+const SINGLE_ADT_TWIN: &str = "\
+enum Role { Owner, Player }
+
+spec fn is_owner(r: Role) -> bool
+  dec r
+{
+  match r { Role::Owner => true, Role::Player => false }
+}
+
+fn check(r: Role) -> bool
+  req true
+  ens result == is_owner(r)
+  fx  pure
+{
+  match r { Role::Owner => true, Role::Player => false }
+}
+";
+
+/// Surface 2: the checked exec fn `g` names no ADT at all, but the woven
+/// `spec_items` include `p`, whose parameter is an `enum E`. Pre-#92 the
+/// solver-vacuity harness failed to elaborate and the whole run aborted with a
+/// `ForgeError` rather than emitting certs.
+const EXEC_FN_UNMENTIONED_ADT: &str = "\
+enum E { A, B }
+
+spec fn p(e: E) -> bool
+  dec e
+{
+  match e { E::A => true, E::B => false }
+}
+
+fn g(x: u64) -> u64
+  req x < 10
+  ens result == x
+  fx  pure
+{
+  x
+}
+";
+
+#[test]
+fn spare_adt_decl_does_not_break_its_siblings() {
+    if !verus_present() {
+        eprintln!("SKIP: verus not available — multi-ADT sub-program cert not run.");
+        return;
+    }
+    let certs = check_program("spare", SPARE_DECL_PROGRAM);
+
+    // .design/forge/check.md REQ-5 + thermite-design.md §6: a correct source
+    // certifies L3. `Unused` carries no contract to discharge, exactly as `Role`
+    // does; both are enum decls lowering to a Verus enum (01-adts REQ-9).
+    assert_eq!(
+        level_of(&certs, "Role"),
+        "L3",
+        "the referenced enum must certify"
+    );
+    assert_eq!(
+        level_of(&certs, "Unused"),
+        "L3",
+        "an enum the file never references must certify — its sub-program weaves \
+         the file's spec fns, so it must also weave the ADTs those spec fns name"
+    );
+    assert_eq!(level_of(&certs, "is_owner"), "L3");
+    assert_eq!(level_of(&certs, "check"), "L3");
+}
+
+#[test]
+fn a_spare_adt_decl_changes_no_sibling_level() {
+    if !verus_present() {
+        eprintln!("SKIP: verus not available — multi-ADT twin comparison not run.");
+        return;
+    }
+    // The oracle: adding a declaration nothing references cannot change what is
+    // provable about the other items, so every shared item's level must match its
+    // single-ADT twin. This is the R-CHAR-3 anchor for the levels above — the twin
+    // is the external truth, not forge's own output on the two-ADT file.
+    let twin = check_program("twin", SINGLE_ADT_TWIN);
+    let spare = check_program("spare_cmp", SPARE_DECL_PROGRAM);
+    for item in ["Role", "is_owner", "check"] {
+        assert_eq!(
+            level_of(&spare, item),
+            level_of(&twin, item),
+            "`{item}`'s level must be invariant under adding an unreferenced decl"
+        );
+    }
+}
+
+#[test]
+fn exec_fn_certifies_when_a_woven_spec_fn_names_an_unmentioned_adt() {
+    if !verus_present() {
+        eprintln!("SKIP: verus not available — vacuity-harness weave not run.");
+        return;
+    }
+    // Pre-#92 this did not merely mis-level: `forge check` aborted with
+    // "a solver-vacuity harness failed to compile/elaborate before verification".
+    // `check_program` panics on a non-JSON stdout, so reaching the asserts at all
+    // is half the pin.
+    let certs = check_program("exec", EXEC_FN_UNMENTIONED_ADT);
+    assert_eq!(level_of(&certs, "g"), "L3", "the exec fn must certify");
+    assert_eq!(level_of(&certs, "E"), "L3");
+    assert_eq!(level_of(&certs, "p"), "L3");
+}
+
+#[test]
+fn multi_adt_corpus_program_certifies_end_to_end() {
+    if !verus_present() {
+        eprintln!("SKIP: verus not available — multi_adt corpus cert not run.");
+        return;
+    }
+    // The corpus anchor: conformance/multi_adt.th is the first corpus program
+    // declaring more than one ADT. Its golden pins `authorize` (the fn-only
+    // golden convention); the ADT items are pinned here.
+    let corpus = PathBuf::from(env!("CARGO_MANIFEST_DIR"))
+        .join("..")
+        .join("conformance")
+        .join("multi_adt.th");
+    let out = Command::new(forge_bin())
+        .arg("check")
+        .arg(&corpus)
+        .arg("--json")
+        .output()
+        .expect("spawn forge check");
+    let stdout = String::from_utf8_lossy(&out.stdout);
+    let certs = serde_json::from_str::<Value>(stdout.trim())
+        .unwrap_or_else(|e| {
+            panic!(
+                "forge check --json on the corpus program must be one JSON doc: {e}\nstdout:\n{stdout}\nstderr:\n{}",
+                String::from_utf8_lossy(&out.stderr)
+            )
+        })
+        .as_array()
+        .expect("array of certs")
+        .clone();
+    for item in ["Role", "Action", "may_ban", "is_ban", "authorize"] {
+        assert_eq!(
+            level_of(&certs, item),
+            "L3",
+            "every item of the multi-ADT corpus program must certify L3"
+        );
+    }
+}

From 70b4c5b726960e395caedf39d412907fd1ae185e Mon Sep 17 00:00:00 2001
From: Doll <dollspacegay@gmail.com>
Date: Tue, 28 Jul 2026 23:38:47 -0500
Subject: [PATCH 2/2] =?UTF-8?q?forge:=20check=20=E2=80=94=20name=20a=20ver?=
 =?UTF-8?q?us=20harness=20after=20the=20item=20it=20checks=20(#92)?=
MIME-Version: 1.0
Content-Type: text/plain; charset=UTF-8
Content-Transfer-Encoding: 8bit

The diagnostics half of #92. `run_verus` took its scratch-dir/`.rs` stem from
`program.items.first()`, and `item_subprogram` weaves ADT decls and spec fns
ahead of the checked item (which it pushes last), so any item with something
woven before it filed its diagnostics under a sibling's name:

  spec fn helper(n: u64) -> u64 { n }
  fn bad(x: u64) -> u64 ens result == helper(x) + 1 { x }   // cannot hold

  before:  [FAIL] postcondition not satisfied @ helper_check.rs:13:9
  after:   [FAIL] postcondition not satisfied @ bad_check.rs:13:9

`helper` certifies L3 and has nothing to do with the failure.

This is not cosmetic: it is what made #92 read as two defects. The reporter saw
E0425 under `/tmp/forge_is_owner_check_*/is_owner_check.rs` while `is_owner`
certified L3, and concluded a harness that failed to compile could coexist with
an L3 on the same item — that the L3 refusal path had a hole. It does not. The
failing harness belonged to `Unused` (correctly L0); only its NAME pointed at
`is_owner`. REQ-4's "the failed obligation and its source position" is not
satisfied by a position under another item's filename.

`run_verus` now takes the checked item's name as a `subject` parameter and no
longer receives the sub-program at all — a harness that cannot see the woven set
cannot name one of its members by accident. All seven call sites already had the
subject in scope (it is what they pass to `assemble_certificate`). The
equivalence-probe site's single-item `Program` wrapper existed only to feed the
old label machinery, so it and its `f.clone()` are removed.

Amendment item 6's `<stem>.rs`-inside-`forge_<stem>_<pid>_<n>/` scheme and the
AC-4 no-`.` crate-stem property are unchanged — only the source of `<stem>` moved.

DESIGN SOURCES THIS ITERATION:
  - .design/forge/check.md (REQ-2 scratch/crate-stem, REQ-4 per-obligation
    position, AC-4 crate-name gotcha, Amendment item 6 scratch naming)
  - reference: conformance/sum.th

REQ STATUS:
  - REQ-2 (verus invocation, temp file, crate-name gotcha) SHIPPED — the no-`.`
    stem property is unchanged; only the stem's source moved.
  - REQ-4 (per-obligation results + counterexamples) SHIPPED — a failing
    obligation's position now identifies its own subject.
  R-HONEST-4: recorded in .design/forge/check.md's #92 Amendment.

VERIFICATION:
  new pin forge/tests/divergence_harness_names_checked_item.rs: 2 passed.
    Confirmed discriminating — pre-fix it FAILS with
    "got `helper_check.rs:13:9`"; post-fix it passes.
  cargo clippy -p forge --all-targets -- -D warnings: PASS
  cargo fmt --all --check: PASS
  doc-drift: PASS (six check.rs-governing docs re-pinned)
  req-status / req-registry: PASS
  cargo test -p forge: in progress at commit time (39/95 binaries, 0 failures);
    the preceding commit's full run was 807 passed / 2 pre-existing
    environmental failures (strat_differential needs the Lean spine built).
  verus 0.2026.05.24.ecee80a (the ci.yml pin)

Refs #92

Co-Authored-By: Claude Opus 5 (1M context) <noreply@anthropic.com>
---
 .design/basis/09-option-result.md             |   2 +-
 .design/basis/11-ergonomics.md                |   2 +-
 .design/basis/12-mutual-recursion.md          |   2 +-
 .design/forge/check.md                        |  19 +-
 .design/lower/boundary-composition.md         |   2 +-
 .design/verified/proof-backends.md            |   2 +-
 forge/src/check.rs                            |  49 +++--
 .../divergence_harness_names_checked_item.rs  | 180 ++++++++++++++++++
 8 files changed, 234 insertions(+), 24 deletions(-)
 create mode 100644 forge/tests/divergence_harness_names_checked_item.rs

diff --git a/.design/basis/09-option-result.md b/.design/basis/09-option-result.md
index bee6b123d..15d1ae787 100644
--- a/.design/basis/09-option-result.md
+++ b/.design/basis/09-option-result.md
@@ -2,7 +2,7 @@
 <!--
 tier: 3-component
 status: draft
-audited-content-sha256: f4468f28b2be3c453070beb9aa798b4f729b7acfda483325fa26fda1d0f02cce (migrated from legacy audited-sha commit pin to a squash-stable content digest; doc-drift-tripwire.md REQ-2 — content pin is primary, commit pin is a migration fallback)
+audited-content-sha256: 607df290746b38714bb16ddb6a651f2b52a23ed0cfdf4f515e7035ef00684a3d (migrated from legacy audited-sha commit pin to a squash-stable content digest; doc-drift-tripwire.md REQ-2 — content pin is primary, commit pin is a migration fallback)
 governs: thermite-syntax/src/ast.rs
 governs: thermite-syntax/src/parser.rs
 governs: thermite-spec/src/validator.rs
diff --git a/.design/basis/11-ergonomics.md b/.design/basis/11-ergonomics.md
index 28317f82e..849618ec6 100644
--- a/.design/basis/11-ergonomics.md
+++ b/.design/basis/11-ergonomics.md
@@ -2,7 +2,7 @@
 <!--
 tier: 3-component
 status: draft
-audited-content-sha256: f4468f28b2be3c453070beb9aa798b4f729b7acfda483325fa26fda1d0f02cce (migrated from legacy audited-sha commit pin to a squash-stable content digest; doc-drift-tripwire.md REQ-2 — content pin is primary, commit pin is a migration fallback)
+audited-content-sha256: 607df290746b38714bb16ddb6a651f2b52a23ed0cfdf4f515e7035ef00684a3d (migrated from legacy audited-sha commit pin to a squash-stable content digest; doc-drift-tripwire.md REQ-2 — content pin is primary, commit pin is a migration fallback)
 governs: thermite-syntax/src/parser.rs
 governs: thermite-syntax/src/ast.rs
 governs: thermite-lower/src/lower.rs
diff --git a/.design/basis/12-mutual-recursion.md b/.design/basis/12-mutual-recursion.md
index 149ddf967..6bee9bed0 100644
--- a/.design/basis/12-mutual-recursion.md
+++ b/.design/basis/12-mutual-recursion.md
@@ -2,7 +2,7 @@
 <!--
 tier: 3-component
 status: draft
-audited-content-sha256: 1e54a3da3d503c5f98cea512c52a410166b42c6d3da09ee85137194fb899077e (migrated from legacy audited-sha commit pin to a squash-stable content digest; doc-drift-tripwire.md REQ-2 — content pin is primary, commit pin is a migration fallback)
+audited-content-sha256: a0626bfbc8c8a2afa354f257fa8d4b788f46cf1e7adfbd3e253ca0ab7a59a914 (migrated from legacy audited-sha commit pin to a squash-stable content digest; doc-drift-tripwire.md REQ-2 — content pin is primary, commit pin is a migration fallback)
 governs: forge/src/check.rs
 governs: thermite-lower/src/lower.rs
 thesis-refs:
diff --git a/.design/forge/check.md b/.design/forge/check.md
index a2c2d6264..90bec1244 100644
--- a/.design/forge/check.md
+++ b/.design/forge/check.md
@@ -3,7 +3,7 @@
 <!--
 tier: 3-component
 status: draft
-audited-content-sha256: acc8e6a294496a3e18324b722bc17b92fa985dff2e36e274cc98134bc9feffe2 (migrated from legacy audited-sha commit pin to a squash-stable content digest; doc-drift-tripwire.md REQ-2 — content pin is primary, commit pin is a migration fallback)
+audited-content-sha256: 39db2140160524b596b95cffd085a1c025c06e0b2dd4820f590ee926c9d97198 (migrated from legacy audited-sha commit pin to a squash-stable content digest; doc-drift-tripwire.md REQ-2 — content pin is primary, commit pin is a migration fallback)
 governs: forge/src/check.rs
 thesis-refs:
   - thermite-design.md §5.1
@@ -87,6 +87,23 @@ REQ status table).
 > `forge/tests/divergence_multi_adt_subprogram.rs`. Same under-approximated-closure
 > class as the `reachable_spec_fn_deps` body-only omission recorded in
 > `.design/verified/proof-backends.md`'s increment-(i) build-blocker note.
+>
+> The same issue carried a diagnostics defect, corrected alongside. `run_verus`
+> took its scratch stem from `program.items.first()`, and `item_subprogram` weaves
+> ADT decls and spec fns ahead of the checked item, so any item with something
+> woven before it filed its diagnostics under a sibling's name — a failing `enum
+> Unused` reported `E0425` at `forge_is_owner_check_<pid>_<n>/is_owner_check.rs`
+> while `is_owner` itself certified L3. That misattribution is why #92 was first
+> read as two defects, the second being a hole in the L3 refusal path; there is no
+> such hole, and REQ-4's "the failed obligation and its source position" is not
+> satisfied by a position under another item's filename. `run_verus` now takes the
+> checked item's name as a `subject` parameter and no longer receives the
+> sub-program at all, so a harness cannot name a merely-woven member by accident;
+> the equivalence-probe call site's single-item `Program` wrapper, which existed
+> only to feed the old label machinery, is gone with it. Amendment item 6's
+> `<stem>.rs`-inside-`forge_<stem>_<pid>_<n>/` scheme and the AC-4 no-`.` crate-stem
+> property are both unchanged — only the source of `<stem>` moved. Pin:
+> `forge/tests/divergence_harness_names_checked_item.rs`.
 
 The stages, in order, are:
 
diff --git a/.design/lower/boundary-composition.md b/.design/lower/boundary-composition.md
index 5b8f180ca..64cd25a7b 100644
--- a/.design/lower/boundary-composition.md
+++ b/.design/lower/boundary-composition.md
@@ -2,7 +2,7 @@
 <!--
 tier: 3-component
 status: draft
-audited-content-sha256: 1e54a3da3d503c5f98cea512c52a410166b42c6d3da09ee85137194fb899077e (migrated from legacy audited-sha commit pin to a squash-stable content digest; doc-drift-tripwire.md REQ-2 — content pin is primary, commit pin is a migration fallback)
+audited-content-sha256: a0626bfbc8c8a2afa354f257fa8d4b788f46cf1e7adfbd3e253ca0ab7a59a914 (migrated from legacy audited-sha commit pin to a squash-stable content digest; doc-drift-tripwire.md REQ-2 — content pin is primary, commit pin is a migration fallback)
 governs: thermite-lower/src/lower.rs, forge/src/check.rs
 thesis-refs:
   - thermite-design.md §9
diff --git a/.design/verified/proof-backends.md b/.design/verified/proof-backends.md
index fedee61df..ea1fb7736 100644
--- a/.design/verified/proof-backends.md
+++ b/.design/verified/proof-backends.md
@@ -3,7 +3,7 @@
 <!--
 tier: 3-component
 status: draft (v-next architecture — the obligation/engine interface; most REQs NOT-STARTED
-audited-content-sha256: 633def0fca2b4b56f4930622ae0c64259ef0290a0b3ed9ba5634e0aaa08f9efb (migrated from legacy audited-sha commit pin to a squash-stable content digest; doc-drift-tripwire.md REQ-2 — content pin is primary, commit pin is a migration fallback)
+audited-content-sha256: 831c0ced80f6072a740c22b3356cdeccb5cc22def9928431891e4391abf6bfe3 (migrated from legacy audited-sha commit pin to a squash-stable content digest; doc-drift-tripwire.md REQ-2 — content pin is primary, commit pin is a migration fallback)
         behind build blockers. The SHIPPED substrates this builds on are quoted-code-grounded.)
 governs: forge/src/check.rs + forge/src/degrade.rs + forge/src/manifest.rs (the discharge
          pipeline, the ladder, the certificate this interface generalizes) and
diff --git a/forge/src/check.rs b/forge/src/check.rs
index 87408873d..0e4675712 100644
--- a/forge/src/check.rs
+++ b/forge/src/check.rs
@@ -795,7 +795,7 @@ pub fn check_file_with_options(
         // Clean (or a `spec fn`, which carries no contract to check): the solver
         // runs the real L3 proof (REQ-3). Assemble the cert exactly as the
         // non-cached path always has.
-        let verus = run_verus(&sub, &lowered, seed, rlimit)?;
+        let verus = run_verus(&lowered, item.name(), seed, rlimit)?;
         let cert = assemble_certificate(item, &verus);
 
         // #10 automatic degrade ladder (`.design/forge/degrade-ladder.md`, the
@@ -5182,16 +5182,30 @@ impl Drop for ScratchDir {
 /// with parseable failure → a reported failure cert; unparseable output →
 /// `ForgeError::VerusOutput` (REQ-3).
 fn run_verus(
-    program: &Program,
     lowered: &str,
+    subject: &str,
     seed: u64,
     rlimit: f64,
 ) -> Result<VerusResult, ForgeError> {
-    // Name the scratch dir + `.rs` after the first item (deterministic) so
-    // concurrent runs over different files do not collide; fall back to a fixed
-    // stem. The crate-name gotcha (REQ-2 / AC-4) is unchanged: the `.rs` stem is
-    // still the no-`.` `crate_stem`, so verus's crate-name derivation succeeds.
-    let label = program.items.first().map(|i| i.name()).unwrap_or("forge");
+    // Name the scratch dir + `.rs` after the item this harness is checking
+    // (deterministic) so concurrent runs over different files do not collide.
+    //
+    // #92: the label was `program.items.first()` — the first item of the woven
+    // SUB-program, which is the checked item only when nothing is woven ahead of
+    // it. `item_subprogram` weaves ADT decls and spec fns first and pushes the
+    // checked item last, so a failing `enum Unused` reported its diagnostics under
+    // `forge_is_owner_check_<pid>_<n>/is_owner_check.rs` — naming a sibling that
+    // was merely woven in. The reporter of #92 read that path as the failure
+    // belonging to `is_owner` (certified L3) and concluded the L3 refusal path had
+    // a hole; it did not. A harness names what it checks.
+    //
+    // The sub-program is deliberately not a parameter: taking the label from it
+    // is what went wrong, and a harness that cannot see the woven set cannot name
+    // one of its members by accident.
+    //
+    // The crate-name gotcha (REQ-2 / AC-4) is unchanged: the `.rs` stem is still
+    // the no-`.` `crate_stem`, so verus's crate-name derivation succeeds.
+    let label = if subject.is_empty() { "forge" } else { subject };
     let stem = crate_stem(Path::new(label));
     let scratch = ScratchDir {
         path: unique_scratch_dir(&stem),
@@ -5723,13 +5737,13 @@ fn mutation_score(
             if let Some(stored) = cache::load(cache_dir, &key) {
                 mutant_cert_is_survivor(&stored)
             } else {
-                let verus = run_verus(&sub, &lowered, seed, rlimit)?;
+                let verus = run_verus(&lowered, item.name(), seed, rlimit)?;
                 let cert = assemble_certificate(&item, &verus);
                 let _ = cache::store(cache_dir, &key, &cert);
                 mutant_cert_is_survivor(&cert)
             }
         } else {
-            let verus = run_verus(&sub, &lowered, seed, rlimit)?;
+            let verus = run_verus(&lowered, item.name(), seed, rlimit)?;
             mutant_outcome_is_survivor(&verus.outcome)
         };
 
@@ -5863,11 +5877,10 @@ fn equivalence_proves_equal(
         // carried (never a silent collapse into the proved-distinguishing bucket).
         Err(e) => return Ok(EquivOutcome::Unsupported(e.to_string())),
     };
-    // The obligation is a complete Verus program (the seam emits the frame); run
-    // it as a single-item program for the `run_verus` scratch-dir/label machinery.
-    let label_program = Program {
-        items: vec![Item::Fn(f.clone())],
-    };
+    // The obligation is a complete Verus program (the seam emits the frame), so it
+    // needs no woven sub-program. #92: it used to be wrapped in a single-item
+    // `Program` purely to feed `run_verus`'s label machinery; `run_verus` now takes
+    // the subject name directly, so the wrapper (and its `f.clone()`) is gone.
     let key = cache::cache_key(&obligation, seed, verus_version, THERMITE_VERSION);
     let proved = if use_cache {
         if let Some(stored) = cache::load(cache_dir, &key) {
@@ -5876,7 +5889,7 @@ fn equivalence_proves_equal(
             // mutant kill-check caches — a `Proved` obligation is "survivor"-true).
             mutant_cert_is_survivor(&stored)
         } else {
-            let verus = run_verus(&label_program, &obligation, seed, rlimit)?;
+            let verus = run_verus(&obligation, &f.name, seed, rlimit)?;
             let proved = mutant_outcome_is_survivor(&verus.outcome);
             // Cache the equivalence verdict (REQ-6 determinism): assemble + store
             // the same cert shape the mutant kill-check stores, keyed on the
@@ -5887,7 +5900,7 @@ fn equivalence_proves_equal(
             proved
         }
     } else {
-        let verus = run_verus(&label_program, &obligation, seed, rlimit)?;
+        let verus = run_verus(&obligation, &f.name, seed, rlimit)?;
         mutant_outcome_is_survivor(&verus.outcome)
     };
     // The exclusion fires only on a verus-proved `ensures` (REQ-2/REQ-3/REQ-8):
@@ -5996,12 +6009,12 @@ fn strengthen_certificate(
             if let Some(stored) = cache::load(cache_dir, &key) {
                 return Ok(mutant_cert_is_survivor(&stored));
             }
-            let verus = run_verus(&sub, &lowered, seed, rlimit)?;
+            let verus = run_verus(&lowered, item.name(), seed, rlimit)?;
             let cert = assemble_certificate(&item, &verus);
             let _ = cache::store(cache_dir, &key, &cert);
             Ok(mutant_cert_is_survivor(&cert))
         } else {
-            let verus = run_verus(&sub, &lowered, seed, rlimit)?;
+            let verus = run_verus(&lowered, item.name(), seed, rlimit)?;
             Ok(mutant_outcome_is_survivor(&verus.outcome))
         }
     };
diff --git a/forge/tests/divergence_harness_names_checked_item.rs b/forge/tests/divergence_harness_names_checked_item.rs
new file mode 100644
index 000000000..d930923de
--- /dev/null
+++ b/forge/tests/divergence_harness_names_checked_item.rs
@@ -0,0 +1,180 @@
+//! Divergence pin (crosslink #92, the diagnostics half) — a per-item verus
+//! harness was named after the FIRST item of the woven sub-program rather than
+//! the item it checks, so a failure reported its source location under a
+//! sibling's name.
+//!
+//! `run_verus` took its scratch-dir/`.rs` stem from
+//! `program.items.first().map(|i| i.name())`. `item_subprogram` weaves the ADT
+//! decls and spec fns first and pushes the checked item LAST, so any item with
+//! anything woven ahead of it reported diagnostics under the wrong name:
+//!
+//!   spec fn helper(n: u64) -> u64 { n }
+//!   fn bad(x: u64) -> u64 ens result == helper(x) + 1 { x }   // cannot hold
+//!
+//! `bad`'s sub-program is `[helper, bad]`, so `bad`'s failed postcondition was
+//! reported at `helper_check.rs:13:9` — naming a function that certified L3.
+//!
+//! This is not cosmetic. It is what made #92 look like two bugs instead of one:
+//! the reporter saw `E0425` under `/tmp/forge_is_owner_check_*/is_owner_check.rs`
+//! while `is_owner` certified L3, and reasonably concluded that a harness which
+//! failed to compile could coexist with an L3 on the same item — i.e. that the
+//! L3 refusal path had a hole. It does not. The failing harness belonged to
+//! `Unused` (correctly L0); only its NAME pointed at `is_owner`. A diagnostic
+//! that misattributes its subject sends the next reader hunting a defect that
+//! is not there.
+//!
+//! The fix drops the sub-program from `run_verus` entirely and passes the
+//! checked item's name, so the harness cannot name a merely-woven member even by
+//! accident.
+//!
+//! The authority (R-CHAR-3): `.design/forge/check.md` REQ-4 requires each failing
+//! obligation to carry "the obligation description and the concrete failure
+//! witness … the failed obligation and its source position" — a position under a
+//! sibling's filename does not identify the subject. AC-4 (the crate-name gotcha:
+//! stem has no `.`) is preserved and independently pinned by
+//! `crate_stem_has_no_dot_and_is_valid`. The expected stem `bad_check` is derived
+//! from the fixture's own item name plus the documented `<stem>.rs` scheme
+//! (Amendment item 6), never copied from the toolchain's output.
+//!
+//! Verus check skips with an eprintln when verus is absent (`editor_runs.rs`
+//! precedent). `tests/` is not anti-pattern-gated (R-APG-2).
+
+use std::path::{Path, PathBuf};
+use std::process::Command;
+
+use serde_json::Value;
+
+fn forge_bin() -> PathBuf {
+    PathBuf::from(env!("CARGO_BIN_EXE_forge"))
+}
+
+/// `true` iff verus is reachable (mirrors `divergence_multi_adt_subprogram.rs`).
+fn verus_present() -> bool {
+    if let Ok(p) = std::env::var("VERUS_BIN") {
+        if Path::new(&p).exists() {
+            return true;
+        }
+    }
+    if let Ok(out) = Command::new("which").arg("verus").output() {
+        if out.status.success() && !String::from_utf8_lossy(&out.stdout).trim().is_empty() {
+            return true;
+        }
+    }
+    if let Ok(home) = std::env::var("HOME") {
+        if PathBuf::from(home).join(".local/bin/verus").exists() {
+            return true;
+        }
+    }
+    false
+}
+
+/// A spec fn (woven first) plus an exec fn whose `ens` cannot hold. `bad`'s
+/// sub-program is `[helper, bad]`, so pre-#92 its diagnostics were filed under
+/// `helper_check.rs`.
+const WOVEN_AHEAD_PROGRAM: &str = "\
+spec fn helper(n: u64) -> u64
+  dec n
+{
+  n
+}
+
+fn bad(x: u64) -> u64
+  req true
+  ens result == helper(x) + 1
+  fx  pure
+{
+  x
+}
+";
+
+fn check_program(tag: &str, program: &str) -> Vec<Value> {
+    let fixture = std::env::temp_dir().join(format!(
+        "forge_harness_naming_{tag}_{}.th",
+        std::process::id()
+    ));
+    std::fs::write(&fixture, program).expect("write fixture");
+    let out = Command::new(forge_bin())
+        .arg("check")
+        .arg(&fixture)
+        .arg("--json")
+        .output()
+        .expect("spawn forge check");
+    let _ = std::fs::remove_file(&fixture);
+    let stdout = String::from_utf8_lossy(&out.stdout);
+    serde_json::from_str::<Value>(stdout.trim())
+        .unwrap_or_else(|e| {
+            panic!(
+                "[{tag}] forge check --json stdout must be one JSON doc: {e}\nstdout:\n{stdout}\nstderr:\n{}",
+                String::from_utf8_lossy(&out.stderr)
+            )
+        })
+        .as_array()
+        .unwrap_or_else(|| panic!("[{tag}] forge check --json must emit an array of certs"))
+        .clone()
+}
+
+/// Every `location` string across an item's obligations.
+fn locations_of(certs: &[Value], item: &str) -> Vec<String> {
+    certs
+        .iter()
+        .find(|c| c.get("item").and_then(|v| v.as_str()) == Some(item))
+        .unwrap_or_else(|| panic!("no cert for `{item}` in {certs:#?}"))
+        .get("obligations")
+        .and_then(|o| o.as_array())
+        .unwrap_or_else(|| panic!("cert for `{item}` has no obligations array"))
+        .iter()
+        .filter_map(|o| o.get("location").and_then(|v| v.as_str()))
+        .map(|s| s.to_string())
+        .collect()
+}
+
+#[test]
+fn a_failing_obligation_is_located_in_the_checked_items_harness() {
+    if !verus_present() {
+        eprintln!("SKIP: verus not available — harness-naming pin not run.");
+        return;
+    }
+    let certs = check_program("woven_ahead", WOVEN_AHEAD_PROGRAM);
+    let locs = locations_of(&certs, "bad");
+    assert!(
+        !locs.is_empty(),
+        "`bad`'s ens cannot hold, so it must carry a located failed obligation \
+         (.design/forge/check.md REQ-4); got {locs:?}"
+    );
+    for loc in &locs {
+        assert!(
+            loc.starts_with("bad_check."),
+            "a failed obligation must be located in the harness of the item under \
+             check (`bad_check.rs`), not in a merely-woven sibling's; got `{loc}`"
+        );
+        // The specific pre-#92 misattribution: `helper` is woven first and
+        // certifies L3, yet lent its name to `bad`'s failure.
+        assert!(
+            !loc.contains("helper"),
+            "the harness must not be named after a woven spec fn; got `{loc}`"
+        );
+    }
+}
+
+#[test]
+fn the_woven_spec_fn_still_certifies_and_owns_its_own_harness() {
+    if !verus_present() {
+        eprintln!("SKIP: verus not available — harness-naming sibling check not run.");
+        return;
+    }
+    // The other half of the misread: `helper` is fine. Pinning it here makes the
+    // pair explicit — one item failed, a different item was named, and the two
+    // facts were easy to fuse into a phantom "L3 coexisting with a broken
+    // harness" bug.
+    let certs = check_program("sibling", WOVEN_AHEAD_PROGRAM);
+    let level = certs
+        .iter()
+        .find(|c| c.get("item").and_then(|v| v.as_str()) == Some("helper"))
+        .expect("cert for helper")["level"]
+        .as_str()
+        .expect("string level");
+    assert_eq!(
+        level, "L3",
+        "the woven spec fn certifies on its own merits (.design/forge/check.md REQ-5)"
+    );
+}