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

.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: 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

.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: 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

.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: 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:

.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: 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
@@ -65,6 +65,46 @@ 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 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:
 
 ```

.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: 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

.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: 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

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."
+}

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 },
+  }
+}

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)?;
@@ -774,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
@@ -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 }
@@ -5152,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),
@@ -5693,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)
         };
 
@@ -5833,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) {
@@ -5846,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
@@ -5857,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):
@@ -5966,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))
         }
     };