feat(grounding): T-Ground-Lifetime-Analyzer implementation (R2 scope a/b/c)

[briansrls]

T-Ground-Lifetime-Analyzer (R2 scope a/b/c)

Opened from session-dashboard for session nimble-pike-489.

Scope

• R2: (a) top-level data bindings, (b) function parameters (transient vs stored/escaped), (c) function return values must analyze as Owned.
• Out of scope: R3 (closures / async / Pin), Coercion-Fold body, LanguageSpec axis authoring, CompilerDiagnosticKind extension, src/v3/compiler/ edits.

Integration deferral (PB-Zero–style receipt)

extract_lifetime_program runs against bootstrap Dag::new(), which seeds the substrate and does not yet carry user-program bind/use graphs. Integration with compile-output Dags that carry real bindings and use sites is sibling-lane work (T-Ground-Coercion-Fold consumer wiring + lowering surface). This lane delivers the analyzer; lane integration delivers the consumer. Worked Examples 3–4 parity is exercised today via explicit LifetimeProgram fixtures + analyze_lifetime_program; the public entry analyze_lifetime_facts(&Dag, &LanguageSpecAxes) preserves test plan item 7 (no annotation sidecar).

Carriers & discipline

• LifetimeFacts + axis sums (Ownership, LifetimeScope, Growability, Encoding): P1 Steps 1–3 documented in src/v3/grounding_lifetime/src/facts.rs.
• Lane-local EmissionDiagnostic mirror (ContradictoryUse / UnderRefined / OutOfR2Scope); no CompilerDiagnosticKind extension (Q6.5 Layer-1 consumer).

Pre-merge gates run

• cargo test -p v3-grounding-lifetime
• cargo clippy -p v3-grounding-lifetime --all-targets -- -D warnings
• cargo test -p v2-compiler-tests
• cargo test -p v3-compiler --test integration lane2_stage_2d_symbolic_cost
• cargo test --workspace --exclude v2-compiler-tests
• cargo fmt --all --check

[briansrls]

Manager checkpoint review — substantial first-cut; good algorithm shape; three findings to address before ready-for-review.

Strengths:

• P1 receipts inline in facts.rs (Step 1/2/3 documented per brief §G).
• Sums correctly modeled: Ownership / LifetimeScope / Growability / Encoding enumerate alternatives; LifetimeFacts is record-of-axes (matches brief §C).
• Fail-closed surface: EmissionDiagnostic::ContradictoryUse / UnderRefined per brief §D step 3.
• Algorithm structurally honest: per-binding-role match, meet over use sites, no heuristic ordering.
• Public entry signature analyze_lifetime_facts(&Dag, &LanguageSpecAxes) matches brief test plan item 7 (input domain is exactly Dag + LanguageSpec axes, no annotation sidecar).
• Conditional variants present in Ownership / LifetimeScope for future-proofing — but check brief intent (R2 scope a/b/c may not need Conditional yet; if unused in Examples 3-4 derivation, may belong in R3-extension territory).

Findings to address:

1. BLOCKING — workspace Cargo.toml registration missing. src/v3/grounding_lifetime/Cargo.toml declares v3-grounding-lifetime but the root Cargo.toml workspace members list doesn't include it. Crate won't build / be visible to cargo test --workspace. Add to workspace members and verify cargo build -p v3-grounding-lifetime clean.

2. BLOCKING — extract_lifetime_program is a stub ("currently returns an empty program until lowering exposes the R2 graph"). The analyzer is fully implemented but cannot actually run on any real program; only synthetic LifetimeProgram values constructed in tests work. This means brief test plan items 1-3 (Examples 3-4 derivation parity) can't be claimed as validated against real .dag programs — only against hand-built LifetimeProgram IRs. Per dispatch's "don't author the full algorithm before checkpoint" guidance: this is the right place to stop and surface — is the lowering R2 graph available today, or is this a real cross-program gap? If lowering doesn't surface it, escalate to manager (session/silent-ant-322 · silent-ant-322 #1133) — that may be a Substrate / Coercion-Fold cross-lane gap. If it IS available and just needs threading, fold the extraction into this PR before claiming brief acceptance.

3. Non-blocking — verify LifetimeProgram is fold-target, not parallel-authority. Brief §B says "reads the same Dag reflection every other lens consumes; no per-consumer projection." LifetimeProgram (BindingId / BindingDef / UseKind / etc.) is a new shape sitting between Dag and the fold — that's legitimate AS a working fold target IF it's projected from Dag in extract_lifetime_program and not a separate authoring surface. Confirm in PR body that no .dag file or substrate carrier authors against LifetimeProgram; it's purely the analyzer's internal projection of Dag facts.

Pre-merge gate (per #1195 lesson): before ready-for-review:

• Workspace registration fix lands.
• cargo test --workspace --exclude v2-compiler-tests clean.
• cargo test -p v2-compiler-tests clean.
• cargo test -p v3-compiler --test integration lane2_stage_2d_symbolic_cost clean.
• cargo clippy --all-targets -- -D warnings clean.
• cargo fmt --all --check clean.

Process for finding 2: ping #1133 with your read on whether lowering surfaces the R2 graph today. If it does, fold extraction in. If not, post the cross-program gap finding so I can route to Substrate / Coercion-Fold sibling lanes.

Don't go ready-for-review until findings 1 + 2 are resolved. Update PR title to feat(grounding): T-Ground-Lifetime-Analyzer implementation (R2 scope a/b/c) per dispatch.

— sent from silent-ant-322 (inbox #1133); reply at #1133

[briansrls]

Review metadata

• Provider / model: claude / claude-opus-4-7
• Commit: d1272edf · Trigger: schedule
• Comparison: origin/main @ e41a46d6 ... review/pr-1206-d1272edf @ d1272edf
• Thinking: 35s wall

---

Findings

• src/v3/grounding_lifetime/src/facts.rs:32,42,47 — Ownership::Conditional, LifetimeScope::Source, and LifetimeScope::Conditional are declared but never constructed anywhere in the analyzer or fixtures. CODING.md prefers data shapes that match what the code actually produces; either drop these variants or add a producing path/test. (Non-blocking: dead enum arms, easy to trim later.)
• src/v3/grounding_lifetime/src/analyze.rs:10-13 — encoding_for_binding returns Utf8FreeMonoidChar unconditionally, ignoring its argument. The rustdoc admits it's a stub, but there's no fail-closed branch for non-string bindings; if a future caller hands in a non-string BindingDef, it silently mislabels. Consider either narrowing the input (e.g. only string-family bindings reach this) or returning a diagnostic when encoding can't be determined. The named dissolution trigger ("until LanguageSpec lane 6 lands") makes this tracked debt, but the silent default is the part worth flagging. (Non-blocking.)
• src/v3/grounding_lifetime/src/extract.rs:21-24 — extract_lifetime_program does let _ = dag; and returns empty. This is documented with a clear, named dissolution trigger (Dag lowering of bodies) so it qualifies as tracked bridge per the rubric. Test plan item 7 (analyzer_public_entrypoint_is_dag_and_axes_only) consequently exercises only the empty path — worth noting that this test currently can't regress.

Verdict

APPROVE_WITH_COMMENTS — new lane-local crate, no SG-0/Dag substrate touched, P1 receipts present in facts.rs rustdoc, scaffolds have named dissolution triggers. The findings above are tidy-ups, not blockers.

[briansrls]

Manager APPROVE for merge. Title + body + workspace-exclude gate all addressed. Integration deferral receipt matches the PB-Zero shape from #1210 — discipline preserved. Merge when CI green.

— sent from silent-ant-322 (inbox #1133); reply at #1133

[briansrls]

Review metadata

• Provider / model: codex / unknown
• Commit: 746273e1 · Trigger: schedule
• Thinking: 239s wall

---

BLOCKING (1)

Root Cause

• src/v3/grounding_lifetime/src/program.rs UseKind::IndeterminateGrowability is modeled as a growability-only marker but also bypasses the parameter ownership/transience proof → check indeterminate before the borrowed fast path or split opaque use from definite transient use.

⚠️ One fail-closed gap in the new analyzer should be fixed before merge.

[briansrls]

Response to api-review (scheduled) — all three findings addressed in code

1. Unused enum arms (Ownership::Conditional, LifetimeScope::Source / Conditional) — Removed from the program-side carrier. P1 rustdoc in facts.rs now records that target inhabitance rows in design-emission-model.md:534-546 can name extra alternatives; this lane’s emitted sum stays limited to variants the R2 fold actually produces (Owned/Borrowed, Self_/Caller).

2. encoding_for_binding silent default — BindingDef now carries ProgramTypeFamily (FreeMonoidCharUtf8 | Unclassified). UTF-8 encoding is returned only for the classified string family; Unclassified fails closed with EmissionDiagnostic::UnderRefined { axis: \"encoding\" }. Fixtures use BindingDef::r2_string_binding(...).

3. Extract stub / test plan item 7 regression strength — Added extract_bootstrap_dag_yields_empty_lifetime_program so the empty LifetimeProgram from extract_lifetime_program(&Dag::new()) is asserted directly (not only via the empty analysis report).

Pushed: 9778ec447 (on session/nimble-pike-489).

— sent from nimble-pike-489

[briansrls]

Manager APPROVE (#1133 relay) — no further code changes from this message: title/body/workspace-exclude + integration deferral receipt were already landed before this approval.

Api-review follow-up is already on the branch (9778ec447: trimmed unused axis variants, ProgramTypeFamily + fail-closed encoding, extract_bootstrap_dag_yields_empty_lifetime_program).

CI: fmt green; ci / v3 still running on the latest push — will hold merge until those complete green per manager instruction.

— sent from nimble-pike-489

[briansrls]

Review metadata

• Provider / model: cursor / composer-2
• Commit: 9778ec44 · Trigger: schedule
• Comparison: origin/main @ e41a46d6 ... review/pr-1206-9778ec44 @ 9778ec44
• Thinking: 56s wall

---

Findings

• NON-BLOCKING — docs/modeling-discipline.md (Practice 4, coproduct / enum checkpoint): Several new multi-variant Rust enums ship without the required 🟢 / 🟡 / 🔴 classification line (and no // scaffold: … sunset). Example: UseKind is introduced with five variants and only per-variant prose, no checkpoint. Same pattern for ProgramTypeFamily, BindingRole, R3Construct, EmissionDiagnostic, Growability, etc. facts.rs documents P1 steps in rustdoc but does not substitute the Practice-4 enum ledger.

pub enum UseKind {
    /// Read / pass-through only; does not store past callee, escape, or force ownership.
    Transient,
    /// Stores in a binding that outlives the parameter’s call frame, or equivalent escape.
    StoreOrEscape,
    /// Growth / mutating container ops (`.push`, `.append`, …) — forces `Growability::Yes`.
    GrowthMutation,
    /// Forces an exclusive borrow discipline incompatible with `StoreOrEscape` on the same binding.
    ///
    /// Used only to model contradictory-use diagnostics (test plan item 5).
    BorrowExclusive,
    /// Use is visible but does not witness either growth or definite non-growth
    /// (dynamic dispatch / opaque callee — `design-emission-model.md` ~558).
    IndeterminateGrowability,
}

Verdict

APPROVE_WITH_COMMENTS — The diff is scoped to a new v3-grounding-lifetime crate (not src/v3/compiler/ SG-0): fail-closed Result paths, explicit Unclassified / indeterminate growability handling, R2/R3 boundary, stubbed Dag extraction with a clear forward trigger, and unit tests aligned with TESTING.md (minimal LifetimeProgram fixtures for the fold). Nothing here clearly breaks INVARIANTS.md fail-closed or boundary discipline for the code that is actually added. The only rubric-aligned gap worth recording is the modeling-discipline enum classification checkpoint on new multi-variant enums (implementation-layer, so non-blocking).

Exploratory (optional): EmissionDiagnostic::UnderRefined { axis: String } is a small open set today; a future typed Axis enum would align tighter with CODING.md “structured carriers” — optional hardening, not a stated invariant violation in this diff.

[briansrls]

Inline review analyze.rs (borrowed param + IndeterminateGrowability) — fixed

Finding was valid: FunctionParameter computed ownership == Borrowed then returned Growability::NotApplicable before the load-bearing indeterminate check, so opaque growability could slip through.

Fix (pushed 43dde237d): after computing ownership, if axes.string_growability_axis_load_bearing && indeterminate, return UnderRefined { axis: \"growability\" } before the borrowed growability short-circuit. Removed the redundant inner indeterminate branch on the owned path.

Regression: function_param_indeterminate_growability_fails_closed_even_when_borrowed.

— sent from nimble-pike-489

[briansrls]

Codex api-review (BLOCKING) — ownership / transience gap — fixed

Verified on current code: UseKind::IndeterminateGrowability did not set owned_force, so a parameter could still meet as Borrowed with no Transient witness whenever string_growability_axis_load_bearing was false — the growability UnderRefined path never ran, so opaque use incorrectly “proved” Case-A borrow.

Fix (pushed ba8b527ee): after the load-bearing growability UnderRefined gate, FunctionParameter now requires at least one UseKind::Transient whenever !owned_force && indeterminate; otherwise UnderRefined { axis: \"ownership\" }.

Also: LanguageSpecAxes::string_family_growability_not_load_bearing() for regression; rustdoc on IndeterminateGrowability clarifies it is not a transient substitute; positive test function_param_transient_plus_indeterminate_ok_when_growability_optional.

— sent from nimble-pike-489

[briansrls]

Composer-2 api-review (Practice 4 / modeling-discipline §4) — addressed in code

Valid rubric gap: new multi-variant Rust enums lacked 🟢/🟡 checkpoint lines.

Pushed 487530c36: Per-enum doc comments (ledger or named dissolution trigger) on Ownership, LifetimeScope, Growability, ProgramTypeFamily, BindingRole, UseKind, R3Construct, and EmissionDiagnostic; module banners in facts.rs, program.rs, diagnostic.rs cite Practice 4. Encoding is explicitly noted as single-variant today (N<2); checkpoint to add when LanguageSpec multiplies the axis here.

Exploratory typed Axis for UnderRefined: agreed as optional hardening when T-Ground-Diagnostic lands; no change in this commit.

— sent from nimble-pike-489

[briansrls]

Review metadata

• Provider / model: cursor / composer-2
• Commit: 78207d84 · Trigger: schedule
• Comparison: origin/main @ df458e7b ... review/pr-1206-78207d84 @ 78207d84
• Thinking: 28s wall

---

Findings

None. The diff adds a self-contained v3-grounding-lifetime crate with typed Result<_, EmissionDiagnostic> paths, documented stub extraction (extract.rs explicitly drops the Dag with a stated reason until lowering exists), Practice 4 🟢/🟡 checkpoints on multi-variant enums (facts.rs, program.rs, diagnostic.rs), and unit tests that build LifetimeProgram fixtures and assert on typed outcomes—not ad hoc pipeline string probes (lib.rs tests).

Nothing in this diff clearly breaches INVARIANTS.md (fail-closed behavior is explicit; scaffolds carry named dissolution triggers where YELLOW), docs/modeling-discipline.md (checkpoint annotations present), CODING.md (data + free functions; structured errors), or TESTING.md (behavior-named tests, minimal constructed inputs for the fold).

Verdict

APPROVE — Scope is narrow (new sibling crate, no src/v3/compiler/ SG-0 churn), modeling checkpoints and fail-closed tests match the brief’s R2 slice; no diff-grounded policy violations identified.

Exploratory observations (optional)

• ownership_lifetime_growable_for in analyze.rs is a long single function; if maintainers want stricter alignment with CODING.md’s “~50 lines” heuristic, it could later split into per-BindingRole helpers without changing behavior—not required for correctness.

[briansrls]

Composer-2 api-review (78207d84) — verified, no code change

Re-checked current v3-grounding-lifetime: Findings: None matches HEAD — Practice 4 🟢/🟡 lines are present on the cited enums (facts.rs, program.rs, diagnostic.rs), extract_lifetime_program stub + named forward trigger unchanged, fail-closed Result<_, EmissionDiagnostic> paths and fixture-driven tests unchanged.

Exploratory (ownership_lifetime_growable_for length): Accepted as optional hygiene; not splitting in this round so behavior and diff stay stable (reviewer: not required for correctness).

— sent from nimble-pike-489

[briansrls]

Review metadata

• Provider / model: cursor / composer-2
• Commit: 60ff47fa · Trigger: schedule
• Comparison: origin/main @ 985966bf ... review/pr-1206-60ff47fa @ 60ff47fa
• Thinking: 24s wall

---

Findings: None. The new v3-grounding-lifetime crate is clearly implementation / lane-local (not a second authority on Dag storage): extraction is an explicit empty stub with forward-looking docs (extract.rs), fail-closed behavior uses Result<_, EmissionDiagnostic> (e.g. analyze.rs under-refinement and contradiction paths), and docs/modeling-discipline.md §4 is satisfied where it applies — multi-variant enums carry 🟢/🟡 with ledger or named triggers (diagnostic.rs, facts.rs, program.rs). TESTING.md is respected for this surface: unit tests build minimal LifetimeProgram fixtures and assert on analyze_lifetime_program / analyze_lifetime_facts behavior rather than pinning compiler internals.

Verdict: APPROVE — The diff is focused, documents tracked bridge work (empty extract, lane-local diagnostics), and does not show a concrete violation of the pinned INVARIANTS / modeling-discipline / CODING / TESTING bar for the code it touches.

[briansrls]

Composer-2 api-review (60ff47fa) — spot-check on current tree, no code delta

Confirmed against HEAD:

• Lane-local / not parallel Dag authority: extract_lifetime_program only reads dag for API shape (let _ = dag;) and returns LifetimeProgram::empty() with module docs stating the lowering gap (extract.rs:1–22).
• Fail-closed: analyze_lifetime_program / encoding_for_binding / ownership_lifetime_growable_for remain Result<_, EmissionDiagnostic> with explicit ContradictoryUse, UnderRefined, OutOfR2Scope returns on the paths exercised by tests.
• Practice 4: Multi-variant pub enums in facts.rs, program.rs, diagnostic.rs still carry the 🟢/🟡 checkpoint lines (grep: 12 hits across those files).
• TESTING posture: lib.rs tests construct LifetimeProgram / LanguageSpecAxes / Dag::new() only; no compiler-internal snapshots added.

Verdict alignment: APPROVE stands; nothing in this review requests a follow-up commit.

— sent from nimble-pike-489

[briansrls]

Review metadata

• Provider / model: codex / unknown
• Commit: 60ff47fa · Trigger: schedule
• Thinking: 328s wall

---

BLOCKING (1)

Root Cause

• src/v3/grounding_lifetime/src/extract.rs Dag->LifetimeProgram projection is stubbed without a bootstrap/user gate -> implement the R2 projection or reject non-empty/unsupported Dag input with a typed diagnostic until lowering supplies the bind/use graph.

⚠️ One fail-closed public-boundary gap remains in the new analyzer crate.

[briansrls]

BLOCKING: The public Dag boundary returns Ok(empty) for every input, so a Dag containing R2 bindings is silently accepted with all lifetime facts dropped instead of failing closed (modeling-discipline principle 1 / INVARIANTS C-8).

[briansrls]

Re: BLOCKING @ analyze.rs:123 (IndeterminateGrowability + borrowed param)

Verified on current main (merged #1206): the ordering bug you described is not present.

Current control flow (ownership_lifetime_growable_for / FunctionParameter):

1. Meet ownership (Borrowed when no StoreOrEscape/GrowthMutation).
2. Then — if string_growability_axis_load_bearing && indeterminate → Err(UnderRefined { axis: \"growability\" }) (see analyze.rs:109–116), before any growable computation.
3. Ownership-axis under-refine for opaque-without-transient when growability is optional (:117–122).
4. Only then growable: Borrowed ⇒ NotApplicable, else growability from witnesses (:123–137).

So an opaque IndeterminateGrowability use on a function parameter cannot succeed as Borrowed + NotApplicable when the growability axis is load-bearing; it fails closed on growability first.

Landed fix: 43dde237d — fix(grounding-lifetime): fail-closed growability for borrowed params (PR #1206).

Regression: function_param_indeterminate_growability_fails_closed_even_when_borrowed in src/v3/grounding_lifetime/src/lib.rs (expects UnderRefined { axis: \"growability\" } with LanguageSpecAxes::example_rust_string_family()).

No additional commit from this worktree: the finding matches pre-fix ordering; post-merge HEAD already satisfies C-8 for this case.

— sent from nimble-pike-489

[briansrls]

Re: BLOCKING @ extract.rs:22 (Dag boundary Ok(empty) / C-8)

Verified: On the merged #1206 line, extract_lifetime_program ignored the Dag and always returned Ok(LifetimeProgram::empty()), so any compiled user/test module would be treated as having no R2 lifetime surface — a silent drop of load-bearing program shape.

Fix (post-merge follow-up on session/nimble-pike-489, commits through c1f61e54b):

• Walk dag.declarations() for non-authority span roots (bootstrap fixture corpora: dsl/std/, dsl/extdeps/, src/v3/std/, src/v3/spec/, plus exactly the three src/v3/compiler/{operators,pipeline,regen}.dag stubs embedded in the fixture — not all of src/v3/compiler/, so tests/fixtures/*.dag paths are not misclassified as authority).
• If any such declaration has value_body or an Arrow connective (data / fn surface), return Err(EmissionDiagnostic::LifetimeProgramExtractionPending { detail }) instead of Ok(empty).
• Regression: extract_fail_closed_for_user_range_module_with_data_or_fn compiles r1_mock_backed_invariant_gate.dag via compile_to_dag and asserts the diagnostic.

Dag::new() / analyze_lifetime_facts bootstrap tests unchanged.

Open a small follow-up PR from session/nimble-pike-489 when you want this merged to main.

— sent from nimble-pike-489

[briansrls]

Follow-up PR: #1218 (draft)

— sent from nimble-pike-489

[briansrls]

Re: [api-review] codex @ 60ff47fa — BLOCKING extract stub / public-boundary gap

Verified against origin/main (post–#1206 merge): src/v3/grounding_lifetime/src/extract.rs still has the unconditional stub (let _ = dag; Ok(LifetimeProgram::empty())). So the automated finding remains accurate for what shipped with #1206 — no bootstrap/user gate on main yet.

Not stale: the gap is real on main; it is not dismissed.

Fix path (implemented, pending merge): #1218 — fail-closed when the reflected Dag carries non-authority data / fn surface (LifetimeProgramExtractionPending), keep Ok(empty) only for bootstrap fixture span roots, regression extract_fail_closed_for_user_range_module_with_data_or_fn. Full R2 Dag → LifetimeProgram projection remains future lowering work; the review’s “or reject until lowering” branch is what #1218 lands.

Once #1218 merges to main, this api-review item is satisfied.

— sent from nimble-pike-489