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

src/v3/compiler/src/dag.rs

@@ -1699,7 +1699,7 @@ fn match_payload_descent_relation(
     arg: PortId,
 ) -> Option<SubValueRelation> {
     for branch in dag.nodes().iter().filter_map(Behavior::as_branch) {
-        if branch.input != param {
+        if !scrutinee_traces_to_param(dag, branch.input, param) {
             continue;
         }
         for path in &branch.paths {
@@ -1777,7 +1777,7 @@ fn match_payload_field_projection_descent_relation(
     let projected_input = transform.inputs[0];
 
     for branch in dag.nodes().iter().filter_map(Behavior::as_branch) {
-        if branch.input != param {
+        if !scrutinee_traces_to_param(dag, branch.input, param) {
             continue;
         }
         for path in &branch.paths {
@@ -1812,6 +1812,73 @@ fn match_payload_field_projection_descent_relation(
     None
 }
 
+/// Phase-1 broadening Slice 3: bounded transitive trace from a match
+/// scrutinee back to the caller's parameter port through nested-match
+/// payload-binding chains.
+///
+/// Surface shape this enables (sibling of Slices 1 + 2; the recursive call
+/// is two structural peels away from the parameter):
+///
+/// ```ignore
+/// 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
+///   }
+/// ```
+///
+/// The inner `Branch.input` is `t1` — a payload binding from the outer
+/// match — not the parameter. Slices 1 / 2's direct
+/// `branch.input == param` check rejects this; the tracer walks one or more
+/// payload-binding levels to confirm structural descent before classifying.
+///
+/// The trace is bounded by a fixed depth (`SCRUTINEE_TRACE_DEPTH_LIMIT`)
+/// for the same reason `callable_target_template_for_provenance` bounds its
+/// instantiation peel: 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.
+const SCRUTINEE_TRACE_DEPTH_LIMIT: usize = 16;
+
+fn scrutinee_traces_to_param(dag: &Dag, scrutinee: PortId, param: PortId) -> bool {
+    let mut current = scrutinee;
+    for _ in 0..SCRUTINEE_TRACE_DEPTH_LIMIT {
+        if current == param {
+            return true;
+        }
+        let Some(parent_input) = enclosing_branch_input_for_payload(dag, current) else {
+            return false;
+        };
+        current = parent_input;
+    }
+    false
+}
+
+/// If `port` is the payload binding port of some `Path`, return the
+/// enclosing `BranchNode.input`. Used by [`scrutinee_traces_to_param`] to
+/// climb one nested-match level. `None` indicates the chain bottoms out
+/// (port isn't a payload binding) — the tracer's fail-closed signal.
+fn enclosing_branch_input_for_payload(dag: &Dag, port: PortId) -> Option<PortId> {
+    dag.nodes()
+        .iter()
+        .filter_map(Behavior::as_branch)
+        .find_map(|b| {
+            b.paths.iter().find_map(|p| {
+                let binding = p.binding.as_ref()?;
+                if binding.payload_port == port {
+                    Some(b.input)
+                } else {
+                    None
+                }
+            })
+        })
+}
+
 /// Authoritative variant-structural facts derived from a resolved variant
 /// declaration. Returns `None` for `UnresolvedVariant` and for `ResolvedVariant`
 /// whose parent `Disj` cannot be located by scanning declarations — same

src/v3/compiler/src/lower.rs

@@ -8601,9 +8601,24 @@ fn descent_provable(
                 scrutinee.as_ref(),
                 SurfaceExpr::Var { name, .. } if name == first_param
             );
+            // Nested-match descent: an inner `match` whose scrutinee is a
+            // structural binding from an outer arm (e.g. `match xs { Cons(t1)
+            // => match t1 { Cons(t2) => f(t2) } }`) is itself unpacking a
+            // strict sub-value of the recursive type. The inner pattern's
+            // bindings are therefore also strict sub-values, so register them
+            // against the same recursive declaration the outer match did.
+            let scrutinee_is_recursive_binding = matches!(
+                scrutinee.as_ref(),
+                SurfaceExpr::Var { name, .. }
+                    if bindings
+                        .get(name)
+                        .is_some_and(|info| info.whole_payload_recursive)
+            );
+            let scrutinee_unpacks_recursive_type =
+                scrutinee_is_first_param || scrutinee_is_recursive_binding;
             arms.iter().all(|arm| {
                 let mut arm_bindings = bindings.clone();
-                if scrutinee_is_first_param {
+                if scrutinee_unpacks_recursive_type {
                     match &arm.pattern {
                         SurfacePattern::VariantWith { name, binding, .. } => {
                             if let Some(info) =

src/v3/compiler/tests/integration/m2_substrate_inhabitance_test.rs

@@ -672,6 +672,64 @@ fn ep_depth(t: EpRec) -> Int =
     }
 }
 
+#[test]
+fn e_p_per_call_descent_evidence_classifies_nested_match_self_call_as_strict_sub_value() {
+    // Phase-1 broadening Slice 3: a recursive self-call whose argument is
+    // the payload binding of an INNER match arm whose scrutinee is itself
+    // an outer-match payload binding (not the parameter directly). Slices 1
+    // and 2 reject this because `branch.input != param`; Slice 3's
+    // `scrutinee_traces_to_param` tracer walks the payload-binding chain
+    // until it hits the parameter port (or the depth limit, fail-closed).
+    //
+    // Cumulative classifier coverage after this slice: direct payload,
+    // direct field-projection, AND nested-match descent — all
+    // structurally-sound `StrictSubValue` evidence.
+    let dag = compile_to_dag(
+        "\
+type EpListN = EpNilN | EpConsN(EpListN)
+fn ep_count2(xs: EpListN) -> Int =
+  match xs {
+    EpConsN(t1) => match t1 {
+      EpConsN(t2) => ep_count2(t2),
+      EpNilN => 0
+    },
+    EpNilN => 0
+  }
+",
+        "e_p_nested_match.v3",
+    )
+    .expect("nested-match recursion fixture compiles");
+
+    let entries = per_call_descent_evidence(&dag);
+    let count = entries
+        .iter()
+        .find(|entry| entry.caller == "ep_count2" && entry.callee == "ep_count2")
+        .expect("expected ep_count2 self-call evidence in per-call side table");
+
+    assert_eq!(count.evidence.len(), 1);
+    match &count.evidence[0] {
+        SubValueRelation::StrictSubValue { field, factor } => {
+            // 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.
+            assert_eq!(
+                field.field_name, "_0",
+                "innermost positional payload structural accessor is the variant Conj's `_0`"
+            );
+            assert_eq!(field.variant_name, "EpConsN");
+            assert_eq!(field.type_name, "EpListN");
+            assert_eq!(field.element_type, "EpListN");
+            assert_eq!(
+                factor,
+                &ShrinkFactor::UnitShrink,
+                "nested descent is sound at any positive depth — \
+                 every level peels one constructor"
+            );
+        }
+        other => panic!("expected StrictSubValue for ep_count2(t2), got {other:?}"),
+    }
+}
+
 #[test]
 fn e_p_per_call_descent_evidence_fails_closed_for_non_self_call() {
     let dag = compile_to_dag(