fix(grounding-lifetime): fail-closed Dag extraction for user module surface (C-8)

docs/briefs/t-ground-diagnostic.md

@@ -9,7 +9,7 @@
 **Lineage / authorities consumed (no re-litigation):**
 - R2 manager lane row + acceptance gate: [`r2-grounding-manager.md`](r2-grounding-manager.md) lines 34, 67, 127 (`diagnostic_structural_ordering_landed`), 144.
 - Q6.5 two-layer authority: [`docs/design-lens-framework.md`](../design-lens-framework.md) §**"Q6.5 — Two-layer authority for diagnostic kinds"** — Layer 1 `CompilerDiagnosticKind` is Substrate-owned; **this lane consumes; does NOT extend**; anti-bridge: lens-instance kinds never enter `CompilerDiagnosticKind`.
-- Engine-reframe + fold failures: [`docs/design-emission-model.md`](../design-emission-model.md) — Modeling problems **4** (ordering is diagnostic-only; lines ~152–164) and **5** (fail-closed diagnostic surface; lines ~165–188); `EmissionDiagnostic` worked shapes (e.g. `UnderRefined`, `NoInhabitant`; search **EmissionDiagnostic** in that doc); lane table row ~386 (`T-Ground-Diagnostic` owns carrier + resolution-hint structure); Examples 1 / 5 / 6 as lifted test receipts.
+- Engine-reframe + fold failures: [`docs/design-emission-model.md`](../design-emission-model.md) — Modeling problems **4** (ordering is diagnostic-only; lines ~152–164) and **5** (fail-closed diagnostic surface; lines ~165–188); `EmissionDiagnostic` worked shapes (e.g. `UnderRefined`, `NoInhabitant`; search **EmissionDiagnostic** in that doc); lane table row ~386 (`T-Ground-Diagnostic` owns carrier + resolution-hint structure); **UnderRefined** worked receipts **Example 1** (bound / unrefined `Int`, lines ~417–464) **and Example 5** (algebra ambiguity, `unspecified_axis: "algebra"`, lines ~639–680) **plus** Example 6 as lifted test targets.
 - Fail-closed compilation: [`INVARIANTS.md`](../../INVARIANTS.md) **C-8** (P3) + C-series sentinels — no silent fabrication when the fold cannot determine.
 - Substrate-fact introduction: [`INVARIANTS.md`](../../INVARIANTS.md) §P1 — mandatory for every new substrate type / variant / field this lane authors.
 - Brief shape templates: [`t-ground-languagespec.md`](t-ground-languagespec.md), [`t-ground-lifetime-analyzer.md`](t-ground-lifetime-analyzer.md).
@@ -44,7 +44,7 @@ Per [`docs/design-lens-framework.md`](../design-lens-framework.md) §Q6.5:
 
 Author a **closed sum** (or equivalent substrate record + tagged variants) for emission/fold failures named in [`docs/design-emission-model.md`](../design-emission-model.md), including at minimum:
 
-- **`UnderRefined`** — program intent or a structural axis is under-specified; candidate set (or axis name) + **resolution hints** per Modeling problem 5. Align field names with worked examples (e.g. bound / algebra / growability axes cited in Examples 1, 3–5).
+- **`UnderRefined`** — program intent or a structural axis is under-specified; candidate set (or axis name) + **resolution hints** per Modeling problem 5. Align field names with worked examples: **Example 1** (bound / refinement gap on `Int`), **Example 5** (algebra ambiguity — `EmissionDiagnostic::UnderRefined { unspecified_axis: "algebra", .. }` per `fold_dag_int_ambiguous_algebra_fails_closed` in `design-emission-model.md` ~672–676), and growability / encoding axes cited in Examples 3–4 where applicable. **Do not collapse** bound-under-refinement and algebra-under-refinement into a single acceptance test — they are distinct `UnderRefined` shapes.
 - **`NoInhabitant`** — substrate does not declare a candidate covering the program’s stated refinement (Example 6 pattern).
 - **Contradiction / multi-site conflict** — when upstream analysis yields incompatible structural constraints (e.g. lifetime analyzer’s `ContradictoryUse` pattern; Coercion-Fold meet on facts).
 
@@ -126,20 +126,21 @@ Worker MUST run the 3-step procedure for **every** new substrate type / variant
 
 Hermetic, behavior-driven, unit-first (`TESTING.md`); sub-second per `feedback_test_timeout_2s.md`.
 
-1. **UnderRefined shape parity** — lift Example 1 (`design-emission-model.md` ~417-464): unrefined `Int` ⇒ `UnderRefined` with enumerated candidates + `unspecified_axis` / hint structure matching the doc sketch (field names may follow substrate naming; semantics must match).
-2. **NoInhabitant parity** — Example 6 (`design-emission-model.md` ~684-731): refinement present, no covering candidate ⇒ `NoInhabitant` (or equivalent authored name) with structured payload.
-3. **Contradiction / conflict** — two incompatible structural constraints ⇒ typed contradiction variant (align with lifetime analyzer migration path).
-4. **Ordering is diagnostic-only** — regression asserting fold emission path does **not** consult ordering tables for selection; diagnostics may reference declared order for enumeration only (tie to Modeling problem 4).
-5. **Q6.5 non-extension** — automated or manual guard: `CompilerDiagnosticKind` variant set unchanged by this lane’s diff (Layer-1 closed sum ratchet).
-6. **`cargo test` / `clippy` / `fmt`** gates per workspace rules.
+1. **UnderRefined — bound axis (Example 1)** — lift `design-emission-model.md` (~417–464): unrefined `Int` ⇒ `UnderRefined` with enumerated candidates + `unspecified_axis` / hint structure matching the `fold_dag_int_unrefined_fails_closed` `TestClaim` sketch (`unspecified_axis: "bound"` in that doc’s worked shape).
+2. **UnderRefined — algebra ambiguity (Example 5)** — lift `design-emission-model.md` (~639–680): program intent under-determines **which algebra** (distinct from “algebra known, bound missing” in Example 1) ⇒ `UnderRefined` with **`unspecified_axis: "algebra"`** and payload matching `fold_dag_int_ambiguous_algebra_fails_closed` / `expected_diagnostic: matches(EmissionDiagnostic::UnderRefined { unspecified_axis: "algebra", .. })`. **Both** Example 1 and Example 5 **must** land as separate `.dag` `TestClaim` receipts before implementation dispatch treats UnderRefined acceptance as complete.
+3. **NoInhabitant parity** — Example 6 (`design-emission-model.md` ~684–731): refinement present, no covering candidate ⇒ `NoInhabitant` (or equivalent authored name) with structured payload.
+4. **Contradiction / conflict** — two incompatible structural constraints ⇒ typed contradiction variant (align with lifetime analyzer migration path).
+5. **Ordering is diagnostic-only** — regression asserting fold emission path does **not** consult ordering tables for selection; diagnostics may reference declared order for enumeration only (tie to Modeling problem 4).
+6. **Q6.5 non-extension** — automated or manual guard: `CompilerDiagnosticKind` variant set unchanged by this lane’s diff (Layer-1 closed sum ratchet).
+7. **`cargo test` / `clippy` / `fmt`** gates per workspace rules.
 
 ---
 
 ## Dissolution claim
 
 When this lane merges:
 
-- Fold failures are **typed structural facts** (`EmissionDiagnostic`), not ad hoc strings or engine exceptions — receipt: Examples 1 / 5 / 6 lifted to tests.
+- Fold failures are **typed structural facts** (`EmissionDiagnostic`), not ad hoc strings or engine exceptions — receipt: **Examples 1, 5, and 6** each lifted to at least one `.dag` `TestClaim` (Example 1 = bound `UnderRefined`; Example 5 = algebra `UnderRefined` with `unspecified_axis: "algebra"`; Example 6 = `NoInhabitant`).
 - **Diagnostic-only ordering** is substrate-declared — receipt: ordering tables / fields are data, not hidden engine policy (`design-emission-model.md:160-163`).
 - **Lane-local `EmissionDiagnostic` mirrors** (e.g. `v3-grounding-lifetime`) have a **named migration path** onto the substrate carrier — receipt tracked in PR sequence with Coercion-Fold / analyzer crates.
 

src/v3/grounding_lifetime/src/diagnostic.rs

@@ -34,4 +34,11 @@ pub enum EmissionDiagnostic {
     OutOfR2Scope {
         construct: String,
     },
+    /// `Dag` → `LifetimeProgram` lowering is not wired yet, but the reflected DAG
+    /// carries **non-authority** declarations (user / test modules) with `data` or
+    /// `fn` surface — returning `Ok(empty)` would silently drop load-bearing program
+    /// shape (C-8 / modeling-discipline principle 1).
+    LifetimeProgramExtractionPending {
+        detail: String,
+    },
 }

src/v3/grounding_lifetime/src/extract.rs

@@ -1,10 +1,15 @@
 //! Dag → `LifetimeProgram` projection (R2 extraction).
 //!
-//! Today’s `Dag::new()` bootstrap does not yet lower user `data` / `fn` bodies into
-//! the bind/use graph this analyzer needs. Extraction returns an empty program until
-//! that lowering lands; the structural fold is validated via [`LifetimeProgram`] fixtures.
+//! Bootstrap fixtures (`Dag::new()`) only carry declarations whose spans live under
+//! checked-in authority prefixes; those are not yet lowered into the bind/use graph,
+//! so extraction returns an **empty** program (the structural fold is validated via
+//! [`LifetimeProgram`] fixtures).
+//!
+//! Any **`data` or `fn` declaration** rooted in a **non-authority** source file (user
+//! or test modules) is treated as load-bearing program surface we cannot project yet:
+//! fail-closed per C-8 instead of returning `Ok(empty)` and dropping facts.
 
-use v3_compiler::dag::Dag;
+use v3_compiler::dag::{Dag, TypeConnective};
 
 use crate::analyze;
 use crate::axes::LanguageSpecAxes;
@@ -14,11 +19,57 @@ use crate::program::{BindingId, LifetimeProgram};
 
 use std::collections::BTreeMap;
 
+/// Span roots that appear on [`Dag::new()`] bootstrap fixtures (regenerated snapshots).
+///
+/// Keep aligned with `bootstrap_generated.rs` / `bootstrap_generated_without_parse_surface.rs`
+/// when new fixture corpora land; otherwise user/test modules may be misclassified.
+///
+/// Note: only **three** `src/v3/compiler/*.dag` stubs ship inside the fixture — not every path
+/// under `src/v3/compiler/` (tests live there too).
+fn is_bootstrap_fixture_authority_source_file(file: &str) -> bool {
+    if file.starts_with("dsl/std/")
+        || file.starts_with("dsl/extdeps/")
+        || file.starts_with("src/v3/std/")
+        || file.starts_with("src/v3/spec/")
+    {
+        return true;
+    }
+    matches!(
+        file,
+        "src/v3/compiler/operators.dag"
+            | "src/v3/compiler/pipeline.dag"
+            | "src/v3/compiler/regen.dag"
+    )
+}
+
+fn first_non_authority_lifetime_surface_declaration(dag: &Dag) -> Option<(String, String)> {
+    for decl in dag.declarations() {
+        if is_bootstrap_fixture_authority_source_file(&decl.span.file) {
+            continue;
+        }
+        let surface =
+            decl.value_body.is_some() || matches!(&decl.connective, TypeConnective::Arrow { .. });
+        if !surface {
+            continue;
+        }
+        let name = decl
+            .name
+            .clone()
+            .unwrap_or_else(|| format!("declaration#{}", decl.id.raw()));
+        return Some((name, decl.span.file.clone()));
+    }
+    None
+}
+
 /// Project the reflected `Dag` into the lifetime analyzer’s program slice.
 ///
 /// Fail-closed on constructs the R2 analyzer does not model (once lowering surfaces them).
 pub fn extract_lifetime_program(dag: &Dag) -> Result<LifetimeProgram, EmissionDiagnostic> {
-    let _ = dag;
+    if let Some((name, file)) = first_non_authority_lifetime_surface_declaration(dag) {
+        return Err(EmissionDiagnostic::LifetimeProgramExtractionPending {
+            detail: format!("{name} ({file})"),
+        });
+    }
     Ok(LifetimeProgram::empty())
 }
 

src/v3/grounding_lifetime/src/lib.rs

@@ -13,7 +13,8 @@
 //! - [`analyze_lifetime_program`](analyze::analyze_lifetime_program) is the structural fold
 //!   over a [`LifetimeProgram`](program::LifetimeProgram) (bindings + classified use sites).
 //! - [`extract_lifetime_program`](extract::extract_lifetime_program) projects `Dag` →
-//!   `LifetimeProgram` (currently returns an empty program until lowering exposes the R2 graph).
+//!   `LifetimeProgram` (bootstrap authority corpora only; **fail-closed** on user/test
+//!   `data` / `fn` surface until lowering exposes the R2 bind/use graph).
 //! - [`analyze_lifetime_facts`](extract::analyze_lifetime_facts) is the public entry:
 //!   **`(&Dag, &LanguageSpecAxes)` only** — test plan item 7 / no annotation sidecar.
 
@@ -144,6 +145,26 @@ mod tests {
         assert!(program.r3_markers.is_empty());
     }
 
+    /// User- or test-range `data` / `fn` declarations must not map to `Ok(empty)` (C-8).
+    #[test]
+    fn extract_fail_closed_for_user_range_module_with_data_or_fn() {
+        let source =
+            include_str!("../../compiler/tests/fixtures/r1_mock_backed_invariant_gate.dag");
+        let file = "src/v3/compiler/tests/fixtures/r1_mock_backed_invariant_gate.dag";
+        let dag = v3_compiler::compile_to_dag(source, file).expect("fixture compile");
+        let err = extract_lifetime_program(&dag).expect_err("extraction must fail closed");
+        match err {
+            EmissionDiagnostic::LifetimeProgramExtractionPending { detail } => {
+                assert!(
+                    detail.contains("mock_service_status")
+                        || detail.contains("r1_mock_backed_invariant_gate"),
+                    "unexpected detail: {detail}"
+                );
+            }
+            other => panic!("unexpected diagnostic: {other:?}"),
+        }
+    }
+
     #[test]
     fn function_param_indeterminate_growability_fails_closed_even_when_borrowed() {
         let mut bindings = BTreeMap::new();

src/v3/grounding_lifetime/src/program.rs

@@ -1,9 +1,10 @@
 //! Structural program slice the analyzer folds over.
 //!
-//! Populated from `Dag` via [`crate::extract::extract_lifetime_program`] (stub
-//! today: empty program when lowering does not yet surface R2 bind graphs).
-//! Worked examples 3–4 are encoded as explicit `LifetimeProgram` values in
-//! unit tests until extraction is complete.
+//! Populated from `Dag` via [`crate::extract::extract_lifetime_program`]. Bootstrap
+//! corpora map to an empty program until lowering surfaces R2 bind graphs; **non-authority**
+//! `data` / `fn` surface fails closed instead of returning an empty program (C-8).
+//! Worked examples 3–4 are encoded as explicit [`LifetimeProgram`] values in unit tests
+//! until extraction is complete.
 //!
 //! ## Practice 4 (`docs/modeling-discipline.md` §4)
 //!