forge: check — weave the ADTs reachable through woven spec fns, and name harnesses after what they check (closes #92)

[dollspace-gay]

Closes #92. Two commits: the weave fix, and the diagnostics defect that made #92 look like two bugs.

1. Root cause — one defect, three surfaces

Not in build_vacuity_harness, and reachable_adt_deps / collect_item_adt_refs are both correct. The bug is the referrer seed in check_file_with_options:

let mut referrers: Vec<&Item> = vec![item];
referrers.extend(fn_deps.iter());
if matches!(item, Item::SpecFn(_)) { referrers.clear(); referrers.extend(item_spec_items.iter()); }
let adt_deps = reachable_adt_deps(&parsed.program, &referrers);

Every arm of item_subprogram weaves item_spec_items, but only the SpecFn arm seeded them as referrers. The referrer set was a strict subset of what the sub-program contained, so an ADT reachable only through a woven spec fn was never emitted. The pre-existing comment said so out loud: "The Item::Fn path is unchanged — its ADT referrers stay [item] + fn_deps exactly as before."

Item kind	Referrers	Symptom
Struct/Enum	[item] — and collect_item_adt_refs is inert on ADT decls, so adt_deps was always empty	a spec fn naming a different ADT dangles → E0425 → L0 → project assurance: FAILED
Fn	[item] + fn_deps	a spec fn taking an ADT the fn never names → vacuity harness won't elaborate → ForgeError aborts the run
SpecFn	reachable spec-fn closure	correct — which is why the single-ADT corpus never caught it

Why one ADT masked it: the only ADT is the checked item, which the ADT arm pushes itself. Same under-approximated-closure class proof-backends.md records for reachable_spec_fn_deps walking decl.body without decl.dec — and, as that note predicts, the pipeline fails closed (a Verus error, never a silent certification).

Fix: seed the referrers with everything woven — referrers.extend(item_spec_items) for every item kind, replaced rather than extended for Item::SpecFn (preserving #71's distinct per-spec-fn sub-program). The Struct/Enum arm drops the checked item from adt_deps before pushing it, so a spec fn naming that ADT cannot emit a duplicate definition (E0428).

2. The diagnostics defect that caused the misdiagnosis

run_verus took its scratch stem from program.items.first(). Since item_subprogram weaves ADT decls and spec fns ahead of the checked item, any item with something woven before it filed diagnostics under a sibling's name:

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

helper certifies L3 and had nothing to do with the failure — it was just woven first.

This is what made #92 read as two bugs. The reporter saw E0425 under 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 refusal path had a hole. It does not. The failing harness belonged to Unused (correctly L0); only its name pointed at is_owner.

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. The equivalence-probe site's single-item Program wrapper existed only to feed the old label machinery, so it and its f.clone() are gone.

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

Corrections to the issue as filed

1. "An unreferenced ADT grades L0" is a symptom, not a rule. An unreferenced ADT certifies L3 fine when no spec fn dangles. Unused was L0 only because its harness failed to compile — so there is no "spare declarations make files unshippable" policy question to settle. Claims 1 and 2 are the same bug.
2. The refusal path has no hole — see §2 above.
3. provenance_demo.th is not a bug. careless_query deliberately passes Tainted to a Sql sink — the negative case the demo exists to demonstrate. It has no .cert.json because it intentionally contains three must-fail functions; all six of its ADT items certify L3.

Verification

cargo test -p forge          807 passed, 2 failed*  (weave commit, full run)
new pins                     6 passed — all discriminating
conformance/multi_adt.th     pre-fix: Role/Action L0 E0425, project FAILED
                             post-fix: all five items L3
clippy -D warnings / fmt     PASS
doc-drift / req-status / req-registry / control-plane   PASS
verus 0.2026.05.24.ecee80a (the ci.yml pin)

* Both failures are pre-existing and environmental: strat_differential needs the Lean spine built locally (lake build Thermite.Strat.Cls.Wire). They fail identically on unmodified check.rs, which does not appear in that test file.

The pins are real pins, verified in both directions:

• divergence_multi_adt_subprogram.rs — 3 of 4 fail pre-fix (two assertion failures plus the ForgeError abort). The 4th is the R-CHAR-3 oracle: adding a declaration nothing references cannot change what is provable about its siblings, so every shared item's level must equal the single-ADT twin's. It holds on both sides by construction, which is the point.
• divergence_harness_names_checked_item.rs — fails pre-fix with got `helper_check.rs:13:9`. Its second test pins that helper genuinely certifies L3, because it was the pair of facts that fused into the phantom bug.

Corpus anchor: conformance/multi_adt.th, the first corpus program declaring more than one ADT, shaped as the Role×Action privilege lattice from the issue. Its golden pins authorize (following the fn-only golden convention — no existing golden pins an ADT item, and inventing that schema was out of scope); the ADT items' levels are pinned in the test.

Follow-up not taken here

map_kv.th breaks on verus 0.2026.06.14 — Set::new in the Map wrapper's generated spec_dom yields E0308: expected Set<int>, found Option<Set<int>>. Pre-existing, unrelated to this change, and invisible on the pinned 0.2026.05.24. Relevant whenever the verus pin gets bumped.

🤖 Generated with Claude Code