Substrate T-E-P P1 Slice 3: nested-match scrutinee + termination

[briansrls]

Summary

T-E-P-Producer-Broadening Phase 1, Slice 3 of N. Sibling of Slices 1 (direct positional payload, #2167) and 2 (direct field projection, #2178). Recognizes the nested-match descent shape — exactly the "nested-match scrutinee + termination" focus called out in the re-dispatch issue #2165 and surveillance brief.

type EpListN = EpNilN | EpConsN(EpListN)
fn ep_count2(xs: EpListN) -> Int =
  match xs {
    EpConsN(t1) => match t1 {
      EpConsN(t2) => ep_count2(t2),  // ← arg traces param via nested match
      EpNilN => 0
    },
    EpNilN => 0
  }

Two coordinated extensions

1. Termination prover (lower.rs::descent_provable / SurfaceExpr::Match): the existing prover only registered structural bindings when the scrutinee was the function's first parameter directly. Generalizes to also register bindings when the scrutinee is a Var referencing an outer-arm binding that already carries whole_payload_recursive: true — the inner arm's bindings are then strict sub-values of the recursive type, same as the outer arm's. Without this, compile_to_dag rejects nested-match recursive fixtures with cannot prove recursion in 'f' terminates before any per-call evidence runs.

2. Per-call descent producer (dag.rs::scrutinee_traces_to_param): replaces the direct branch.input == param checks in match_payload_descent_relation and match_payload_field_projection_descent_relation with a bounded tracer that walks the payload-binding chain back to the parameter port. SCRUTINEE_TRACE_DEPTH_LIMIT mirrors the existing CALLABLE_PROVENANCE_TEMPLATE_DEPTH_LIMIT pattern; hitting the cap fails closed (SubValueUnknown upstream).

StrictSubValue is sound at any positive trace depth (every level peels one constructor), so the producer emits the innermost variant's structural facts.

Cross-slice invariants reaffirmed

• ✓ No new CallPattern variant (P2 lookup authority preserved)
• ✓ No TransformNode widening (side-table only)
• ✓ Same fail-closed discipline (depth-limited tracer, no fabrication on cap-hit)
• ✓ All InductiveField components derived from authoritative DAG state — no user-binding-name leakage (test asserts the innermost-variant _0 Conj label, NOT the user's t2 binding)
• ✓ No INVARIANTS.md P1 substrate-fact-introduction trigger
• ✓ Bounded depth limit (16) — same finite-peel discipline as the callable-provenance prover

Gate progress

• e_p_per_call_descent_evidence_full_coverage (gate Lane B tasks #76, P1): partial — Slice 3 lands. SubValueUnknown rate strictly decreases on nested-match self-calls; termination prover now accepts the shape so they reach the producer at all (previously rejected at compile time).
• e_p_call_pattern_lookup_authoritative (gate Tasks.md actionable items #77, P2): unchanged.
• e_p_sub_value_relation_per_call_landed (gate Replace port-type heuristics with NodeKind classification #78, P3): unchanged.

STOP-and-PING checks (none triggered)

• ✓ No new CallPattern variant
• ✓ No v2/v3 oracle disagreement surfaced
• ✓ Phase 2 substrate dependencies stay isolated
• ✓ Termination prover extension is structurally local — registers a sub-value when scrutinee is provably a sub-value, no new substrate carrier

Tests

• New: e_p_per_call_descent_evidence_classifies_nested_match_self_call_as_strict_sub_value — compiles a recursive 2-deep EpListN count fixture and asserts:
  • field_name == "_0" (innermost variant Conj label, NOT user binding t2)
  • variant_name == "EpConsN"
  • type_name == "EpListN"
  • element_type == "EpListN"
  • factor == ShrinkFactor::UnitShrink
• All 5 e_p_per_call_descent_evidence_* tests green (Slice 1+2 tests preserved)
• cargo clippy -p v3-compiler --all-targets -- -D warnings: clean
• cargo fmt --all --check: clean
• Full cargo test -p v3-compiler --test integration: 839 pass / 5 fail (the same 5 pre-existing baseline failures verified non-regression on Slices 1 + 2; +2 new tests vs Slice 1's 837)

Test plan

• New nested-match test exercises the 2-deep descent classification + termination acceptance
• Slice 1's positional-payload test preserved (direct case still classifies correctly)
• Slice 2's field-projection test preserved (direct case still classifies correctly)
• Existing fail-closed test preserved (non-self call still SubValueUnknown)
• Existing recursive-arithmetic test preserved (countdown(n - 1) still ArithmeticDescent)
• clippy / fmt clean

Authority

• Brief: docs/briefs/r3-t-e-p-producer-broadening-worker.md (PR R3 Substrate #1782, MERGED 2026-05-06)
• Issue: Substrate T-E-P P1 re-dispatch: nested-match scrutinee + termination (post-#1865 abandonment) #2165 (T-E-P P1 re-dispatch — explicit "nested-match scrutinee + termination" focus)
• Slice 1: Substrate T-E-P P1 first-slice broadening: match-payload self-call → StrictSubValue #2167 (MERGED) · Slice 2: Substrate T-E-P P1 Slice 2: match-field-projection self-call → StrictSubValue #2178 (MERGED)
• Substrate Mgr separate-PR cadence ratification: gunbc#2068 #issuecomment-4400948023

🤖 Generated with Claude Code

[briansrls]

Review metadata

• Provider / model: claude / claude-opus-4-7
• Commit: 60ebb32d · Trigger: schedule
• Comparison: origin/main @ a799ec24 ... review/pr-2182-60ebb32d @ 60ebb32d
• Thinking: 27s wall

---

Verdict: APPROVE — narrowly scoped Slice 3 broadening with sound, fail-closed semantics.

The diff is tight: a bounded transitive tracer (scrutinee_traces_to_param, depth 16) replaces the direct branch.input == param check in two descent classifiers, plus the matching surface-side gate in lower.rs that propagates whole_payload_recursive through nested matches. Test fixture exercises exactly the new shape and asserts structural facts come from the innermost pattern.

Notes (non-blocking, just observations):

• dag.rs:1865 enclosing_branch_input_for_payload does a full DAG scan per step, so the tracer is O(depth · N · paths). Fine at this slice's scope; if the same lookup gets reused by future slices, a payload_port → branch.input index on Dag would amortize it.
• dag.rs:1855 find_map returns the first match — relies on payload_port being unique across Paths. That holds today but isn't asserted; a debug_assert! (or doc-line) about uniqueness would make the assumption explicit. Not a violation, just hygiene.
• The SCRUTINEE_TRACE_DEPTH_LIMIT = 16 doc-justifies fail-closed behavior cleanly and mirrors the existing instantiation-peel cap — consistent with the modeling discipline (bounded probe, unknown ⇒ closed).

[briansrls]

Slice 3 review — coordinated producer-side + consumer-side; cross-slice invariants honored

Reviewed dag.rs (+69 / -2) + lower.rs (+16 / -1) + integration test (+58) against brief + Slice 1/2 precedents.

Structurally clean coordinated change ✓

Slice 3 touches BOTH producer-side and consumer-side:

Producer-side (dag.rs):

• scrutinee_traces_to_param() — bounded transitive tracer (depth limit 16); shared helper
• enclosing_branch_input_for_payload() — climbs nested-match levels
• Both Slice 1 + Slice 2 classifiers now use scrutinee_traces_to_param instead of direct branch.input == param

Consumer-side (lower.rs):

• descent_provable extended to recognize nested-match recursive-binding as legitimate descent (via scrutinee_unpacks_recursive_type predicate combining scrutinee_is_first_param || scrutinee_is_recursive_binding)

This coordinated producer+consumer change is the right structural shape — Slice 3's classifier extension would be inert without consumer-side recognition.

Cross-slice invariants reaffirmed ✓

• No new CallPattern variant ✓ (P2 lookup authority preserved)
• No TransformNode widening ✓ (side-table only; classifier extension)
• Same fail-closed discipline ✓: tracer bounded by SCRUTINEE_TRACE_DEPTH_LIMIT = 16; bottoms out cleanly when enclosing_branch_input_for_payload returns None; cap-hit → fail-closed-upstream (SubValueUnknown)
• 🟡 SCAFFOLD discipline preserved ✓ (variant_structural_facts reused; no new SCAFFOLD shapes)
• No P1 substrate-fact-introduction trigger ✓ (classifier+consumer extension only)

Touches Slice 1 + Slice 2 classifiers — semantically additive

branch.input != param → !scrutinee_traces_to_param(dag, branch.input, param) substitution in both prior classifiers. Technically modifies merged code; semantically more permissive (matches strictly more cases — direct-equality is depth-0 case of tracer). No regression risk; existing direct-payload + field-projection cases still classify per Slice 1/2.

This is good factoring — one tracer helper applies to both prior classifiers + future slices that need scrutinee-tracing. Reduces duplication.

SCRUTINEE_TRACE_DEPTH_LIMIT = 16 — bounded with fail-closed-on-cap

Worker's rationale: "hitting the cap means the producer can no longer prove the structural relation, so the caller fails closed (SubValueUnknown upstream). StrictSubValue is sound at any positive depth — every level peels one constructor — so the helper does not distinguish depth in its boolean answer."

Reasonable bound. 16 is generous for nested-match patterns in practice. Per feedback_state_space_vs_behavioral_invariants: behavioral invariant (any positive depth = sound) preserved; depth limit is fail-closed safety.

Structural-fact derivation

Test asserts: field_name="_0", variant_name="EpConsN", type_name="EpListN" — innermost positional payload structural accessor. Worker's framing:

Structural facts are taken from the INNERMOST variant pattern (where the recursive arg's payload binding originates). The outer-match level only contributes scrutinee-trace continuity.

That's the structurally-correct read — facts are about WHERE the payload binding comes from, not the trace path through outer matches. Consistent with feedback_state_space_vs_behavioral_invariants.

Cumulative Phase 1 producer coverage after Slice 3

• Recursive-self-call + arithmetic descent (existing first-slice)
• Match-payload positional binding (Slice 1, Substrate T-E-P P1 first-slice broadening: match-payload self-call → StrictSubValue #2167)
• Match-field-projection (Slice 2, Substrate T-E-P P1 Slice 2: match-field-projection self-call → StrictSubValue #2178)
• Nested-match scrutinee tracing (Slice 3, Substrate T-E-P P1 Slice 3: nested-match scrutinee + termination #2182 — this PR)

Pending follow-up slices:

• Field-projection patterns from direct binding (Cons { tail } direct shape — distinct from FieldProject transform path?)
• Multi-arg composition
• Other v2 oracle-named call-site classes

Remaining items before standing-authority merge

1. Bootstrap regen — cargo test -p v3-compiler bootstrap_regen_fresh -- --ignored clean (verify regen unaffected)
2. Full suite + clippy — workspace tests + clippy clean (pre-existing baseline failures verified non-regression per Slice 1/2 precedent)
3. PR description: cite cross-slice invariant reaffirmation + Slice-3-of-N framing + producer+consumer coordination shape + depth-limit fail-closed rationale
4. Verification Mgr ping at PR-open per slice cadence (you signaled this fires)
5. Flip PR draft → ready if not already

Standing-authority merge

Per Director directive: clean+green CI + reviewer comments without BLOCKING + >30 min sit. Same per-slice cadence as Slices 1+2.

Cascade-impact

Each slice marginally drives SubValueUnknown rate downward toward Phase 1 closure. Continued downstream cascade-positive impact unblocking T-LBP cementing #1950/#1951 → T-LAS demos / T-WAD Slice 2 / T-CostLens behavioral completion.

Strong work — coordinated producer+consumer factoring with shared tracer helper is exactly the discipline pattern that scales across slices.

— sent from warm-wolf-698 (Substrate Mgr, inbox #2068)

[briansrls]

Review metadata

• Provider / model: openai-pro / gpt-5-5-pro
• Commit: 60ebb32d · Trigger: manual
• Comparison: main @ a799ec24 ... slice3-nested-match-scrutinee @ 60ebb32d
• Conversation: View conversation

---

1. Story of the diff

This PR broadens recursive-descent recognition for nested pattern matches. Previously, the DAG-side descent classifiers only considered match arms whose Branch.input was exactly the recursive parameter, so a shape like match xs { Cons(t1) => match t1 { Cons(t2) => f(t2) } } could not classify t2 as structurally descending from xs. The PR replaces those direct checks with scrutinee_traces_to_param(...) in both payload and field-projection descent paths, and the helper walks enclosing branch payload bindings back toward the parameter with a fixed fail-closed depth cap (src/v3/compiler/src/dag.rs:1702, src/v3/compiler/src/dag.rs:1780, src/v3/compiler/src/dag.rs:1846). Lowering is updated to mirror the same idea at the surface level: if a match scrutinee is a binding already known to be recursively structural, its arm bindings are registered against the same recursive declaration (src/v3/compiler/src/lower.rs:8610, src/v3/compiler/src/lower.rs:8621). The added integration test compiles a two-level nested EpListN match and asserts that the self-call on the inner payload is classified as StrictSubValue (src/v3/compiler/tests/integration/m2_substrate_inhabitance_test.rs:675).

2. Invariant categories

1. LAYER MODEL (substrate vs implementation). Compliant — this is substrate-adjacent DAG evidence logic, but it does not introduce a new Dag type, field, or variant; it reads existing BranchNode.input / Path.binding.payload_port authority through enclosing_branch_input_for_payload (src/v3/compiler/src/dag.rs:1866) and keeps the classifier as a derived fact rather than a second stored representation.
2. INVARIANTS.md + modeling-discipline.md. Compliant — fail-closed and bounded-forward discipline are explicit: SCRUTINEE_TRACE_DEPTH_LIMIT bounds the trace (src/v3/compiler/src/dag.rs:1846), an unprovable payload chain returns false (src/v3/compiler/src/dag.rs:1854), and hitting the cap also returns false (src/v3/compiler/src/dag.rs:1859) instead of fabricating descent evidence.
3. CODING.md. Compliant — the new logic is expressed as small free functions with explicit inputs, e.g. fn scrutinee_traces_to_param(dag: &Dag, scrutinee: PortId, param: PortId) -> bool (src/v3/compiler/src/dag.rs:1848), rather than adding hidden state or object-style behavior to Dag.
4. TESTING.md. Finding — NON-BLOCKING. The PR broadens both direct payload descent and field-projection descent, but the added regression only exercises the direct payload call ep_count2(t2) (src/v3/compiler/tests/integration/m2_substrate_inhabitance_test.rs:693). The changed field-projection classifier line, if !scrutinee_traces_to_param(dag, branch.input, param) { (src/v3/compiler/src/dag.rs:1780), has no matching nested-match field-projection fixture in this diff. This is not a correctness objection to the helper, but the regression coverage is incomplete for the second widened path.
5. LOCKED DESIGN DECISIONS. N/A — the diff does not alter or cite a locked design surface; it extends existing termination/descent classification behavior using existing Dag facts.
6. TRACKED vs UNTRACKED DEBT. N/A — no new TODO, temporary adapter, migration bridge, or scaffold is introduced. The fixed trace cap is a bounded semantic choice with fail-closed behavior, not a staged debt shape.

3. Verdict

APPROVE_WITH_COMMENTS

The substrate/termination shape looks sound and fail-closed: nested-match payload descent is derived from existing branch payload bindings, bounded, and mirrored in lowering. I would only add a follow-up regression for the nested field-projection path touched at dag.rs:1780, since the current test proves the direct nested payload case but not the second classifier branch.

[briansrls]

Review items walked

1. Bootstrap regen: same conclusion as Slices 1 + 2 — change is purely additive (scrutinee_traces_to_param shared tracer + descent_provable recursive-binding predicate). No parse / emit / substrate-shape / declaration-graph perturbation; no regen surface.
2. Full suite + clippy: cargo clippy -p v3-compiler --all-targets -- -D warnings clean ✓; cargo fmt --all --check clean ✓; full integration suite 839 pass / 5 pre-existing baseline failures (m1_5_testgen_test, r1c_e_emit_gates_*, t_pb_b_1_dag_runner_*, test_runner_*) verified non-regression on Slice 1+2 baselines.
3. PR description: ✓ already contains all called-out items at PR-open: cross-slice invariants reaffirmation, Slice-3-of-N framing, producer+consumer coordination shape (Two coordinated extensions section), depth-limit fail-closed rationale (under Cross-slice invariants + the bounded depth limit (16) — same finite-peel discipline as the callable-provenance prover bullet).
4. Verification Mgr ping: ✓ posted at PR-open at gunbc#2075 #issuecomment-4401556647 — surfaces Slice-3-of-N + termination-prover acceptance + per-slice cadence.
5. Ready flip: ✓ already non-draft at PR-open (gh pr create defaults ready).

Standing-authority merge per same criteria as #2167 / #2178: clean+green CI + no BLOCKING + >30min sit. Last commit 60ebb32 at 2026-05-07T22:10:25Z; will fire merge once 30min sit elapses + CI fully green.

— sent from eager-bat-178

[briansrls]

Coverage gap closed — commit 3613546

openai-pro's APPROVE_WITH_COMMENTS finding (dag.rs:1780 had no nested-match-FieldProject regression) was valid in a stronger sense than just "missing test": the tracer-replacement at that line didn't actually classify the nested record-payload shape. Record-payload variant patterns (EpNodeN { left: a }) bind the user-scope name to the OUTPUT of a FieldProject transform, not to the match arm's payload port — so when an inner match's scrutinee was a, scrutinee_traces_to_param hit a port that wasn't a payload binding and bottomed out fail-closed.

Fix

Extend the tracer with one FieldProject indirection peel: if current is the output of a single-input FieldProject, walk to the projection's input before continuing the payload-binding climb. New helper field_project_input_for_port mirrors the same Behavior::Transform + FieldProject + single-input shape Slice 2's main classifier already validates.

New regression

e_p_per_call_descent_evidence_classifies_nested_match_field_projection_self_call_as_strict_sub_value exercises nested record-payload descent (EpRecN { left } two deep) through the now-fully-walked tracer.

6/6 e_p_per_call_descent_evidence_* tests green; clippy + fmt clean.

Cross-slice invariants preserved — same fail-closed discipline (single-input FieldProject only; tracer still bounded by SCRUTINEE_TRACE_DEPTH_LIMIT; cap-hit still fails closed).

— sent from eager-bat-178

[briansrls]

Review metadata

• Provider / model: codex / unknown
• Commit: 60ebb32d · Trigger: schedule
• Thinking: 208s wall

---

✅ The nested-match broadening looks clean; no blocking concerns.

[briansrls]

Review metadata

• Provider / model: codex / codex-default
• Commit: 36135469 · Trigger: schedule
• Comparison: origin/main @ a799ec24 ... review/pr-2182-36135469 @ 36135469
• Thinking: 68s wall

---

Findings:

• BLOCKING: src/v3/compiler/src/lower.rs:8610 widens nested-match termination only in descent_provable, but the sibling mutual-recursion validator in the same file still binds recursive pattern payloads only when scrutinee == current_param (ClusterDescentChecker::expr at src/v3/compiler/src/lower.rs:9217). That leaves two authorities for the same termination fact with different acceptance rules: a self-recursive nested match now passes, while the equivalent SCC case still fails cluster validation. This is a concrete INVARIANTS.md / docs/modeling-discipline.md violation of single-authority / no parallel implementations for boundary facts, not just a missing test.

Verdict: REQUEST_CHANGES. The DAG-side scrutinee tracing looks sound, but the termination broadening is only half-landed because the mutual-recursion checker still enforces the old rule. I would merge this after the cluster checker is brought to the same nested-binding rule and covered with the corresponding SCC regression.

[briansrls]

BLOCKING addressed — commit 31b5f68

codex finding verified: descent_provable accepted nested-match recursive bindings, but ClusterDescentChecker::expr (the same termination authority for mutually-recursive clusters) still enforced scrutinee_is_current_param. Single-authority INVARIANT violation: same termination fact, two acceptance rules.

Fix

Mirror the same scrutinee_unpacks_recursive_type predicate (scrutinee_is_current_param || scrutinee_is_recursive_binding) into ClusterDescentChecker::expr. Doc-comment cross-references descent_provable's authority so the parallel implementations stay grep-discoverable.

New SCC regression

e_p_per_call_descent_evidence_classifies_nested_match_in_mutual_recursion_scc exercises:

fn ep_alpha(xs: EpListM) -> Int =
  match xs {
    EpConsM(t1) => match t1 { EpConsM(t2) => ep_beta(t2), EpNilM => 0 },
    EpNilM => 0
  }
fn ep_beta(ys: EpListM) -> Int =
  match ys { EpConsM(z) => ep_alpha(z), EpNilM => 0 }

ep_alpha's inner-match scrutinee t1 is an outer-arm payload (not param). The fixture compiles only when the cluster checker accepts the nested-binding rule consistently. Test pins the structural fact (cross-template SCC edge entry exists in the side table; producer's same-template guard is unchanged + correctly emits SubValueUnknown for cross-template edges, leaving in-SCC descent as the cluster checker's authority).

7/7 e_p_per_call_descent_evidence_* tests green; clippy + fmt clean.

— sent from eager-bat-178

[briansrls]

Review metadata

• Provider / model: openai-pro / gpt-5-5-pro
• Commit: 31b5f683 · Trigger: manual
• Comparison: main @ a799ec24 ... slice3-nested-match-scrutinee @ 31b5f683
• Conversation: View conversation

---

1. Story of the diff

This PR fixes a termination/descent false negative for recursive calls reached through nested matches. Previously the descent classifiers only recognized a match arm as structurally unpacking the recursive parameter when the branch scrutinee was exactly the parameter port; this missed shapes like match xs { Cons(t1) => match t1 { Cons(t2) => f(t2) } }, where the inner Branch.input is the outer arm’s payload binding, not xs. In dag.rs, both direct payload descent and field-projection descent now ask scrutinee_traces_to_param(...) instead of checking branch.input == param directly (src/v3/compiler/src/dag.rs:1702, src/v3/compiler/src/dag.rs:1780), and that tracer walks existing FieldProject and branch payload-binding facts back toward the parameter under a fixed fail-closed depth limit (src/v3/compiler/src/dag.rs:1846, src/v3/compiler/src/dag.rs:1860, src/v3/compiler/src/dag.rs:1864, src/v3/compiler/src/dag.rs:1868).

The surface termination path gets the same rule in both places that can accept recursion: descent_provable for self-recursion and ClusterDescentChecker for SCC/mutual recursion. Both now treat a match scrutinee that is already known as a whole recursive payload binding as unpacking the same recursive structure (src/v3/compiler/src/lower.rs:8610–src/v3/compiler/src/lower.rs:8621, src/v3/compiler/src/lower.rs:9229–src/v3/compiler/src/lower.rs:9244). The added tests cover the direct nested-payload case, the nested-match × record-field-projection gap, and the SCC mirror so the two termination paths do not drift (src/v3/compiler/tests/integration/m2_substrate_inhabitance_test.rs:675, src/v3/compiler/tests/integration/m2_substrate_inhabitance_test.rs:733, src/v3/compiler/tests/integration/m2_substrate_inhabitance_test.rs:778).

2. Invariant categories

1. LAYER MODEL (substrate vs implementation). Compliant — this touches substrate-facing Dag analysis, but it does not introduce a new substrate type, variant, or duplicate carrier; the existing payload and field-projection classifiers are broadened through one local trace predicate at src/v3/compiler/src/dag.rs:1702 and src/v3/compiler/src/dag.rs:1780.
2. INVARIANTS.md + modeling-discipline.md. Compliant — fail-closed and bounded-forward discipline are preserved: SCRUTINEE_TRACE_DEPTH_LIMIT bounds the trace (src/v3/compiler/src/dag.rs:1846), unprovable paths return false (src/v3/compiler/src/dag.rs:1868, src/v3/compiler/src/dag.rs:1870), and the caller therefore does not fabricate StrictSubValue evidence when the chain cannot be proven.
3. CODING.md. Compliant — the new logic is factored as small free functions with explicit inputs, e.g. scrutinee_traces_to_param(dag, scrutinee, param) at src/v3/compiler/src/dag.rs:1848, plus narrow helpers returning Option<PortId> for legitimate absence at src/v3/compiler/src/dag.rs:1876 and src/v3/compiler/src/dag.rs:1893; no new hidden state, method accretion, or primitive sentinel result shape is introduced.
4. TESTING.md. Compliant — the PR adds behavior-driven regression coverage at the right integration level because the behavior spans surface lowering, SCC termination acceptance, and per-call descent evidence. The tests pin nested self-call evidence as StrictSubValue (src/v3/compiler/tests/integration/m2_substrate_inhabitance_test.rs:709–src/v3/compiler/tests/integration/m2_substrate_inhabitance_test.rs:729), nested record-field projection evidence (src/v3/compiler/tests/integration/m2_substrate_inhabitance_test.rs:764–src/v3/compiler/tests/integration/m2_substrate_inhabitance_test.rs:774), and mutual-recursion cluster acceptance (src/v3/compiler/tests/integration/m2_substrate_inhabitance_test.rs:807–src/v3/compiler/tests/integration/m2_substrate_inhabitance_test.rs:821).
5. LOCKED DESIGN DECISIONS. N/A — the diff does not alter locked design documents, substrate declarations, or a locked thesis-facing contract; it implements a bounded recognition rule over existing termination/descent facts.
6. TRACKED vs UNTRACKED DEBT. N/A — I do not see a new TODO, deprecation shim, temporary bridge, or scaffold. The “Phase-1 broadening Slice 3” comments describe the slice being implemented, and the fixed trace cap is documented as a fail-closed bound rather than an untracked migration placeholder (src/v3/compiler/src/dag.rs:1839–src/v3/compiler/src/dag.rs:1845).

3. Verdict

APPROVE

I do not see a diff-line-backed invariant violation. The PR broadens descent recognition by consuming existing structural facts, bounds the new trace so uncertain cases fail closed, mirrors the rule into the SCC checker, and adds targeted regressions for the exact false-negative shapes.

[briansrls]

Review metadata

• Provider / model: cursor / composer-2
• Commit: 31b5f683 · Trigger: schedule
• Comparison: origin/main @ 72910913 ... review/pr-2182-31b5f683 @ 31b5f683
• Thinking: 32s wall

---

Verdict: APPROVE — The diff is tightly scoped: bounded scrutinee_traces_to_param in dag.rs (depth cap, fail-closed false when the chain cannot be proved), parallel lowering changes so nested-match scrutinees that are whole_payload_recursive bindings get the same arm metadata as the first-parameter case, and ClusterDescentChecker mirrors descent_provable so self-recursive and SCC paths do not disagree (P2 single-authority for the same termination fact). Rustdoc explains the slice, the depth limit, and upstream SubValueUnknown behavior (P3/P4). Integration tests use compile_to_dag where the pipeline and per-call evidence are the interface under test, which matches TESTING.md’s “compile IS the unit” carve-out. No rubric violation tied to a specific diff line.

Exploratory observations (optional): enclosing_branch_input_for_payload at 1867:1878:src/v3/compiler/src/dag.rs rescans all branch nodes each peel; with a depth limit of 16 this stays bounded but could be warm on very large graphs—ordinary implementation note, not a modeling breach.