test: add third W1 L4 Rust Int receipt

src/v3/compiler/tests/fixtures/r3_verification_l4_emit_eval_match.dag

@@ -33,6 +33,12 @@ data r3_l4_emit_eval_false_program_input: ProgramOutputBind = {
   output_ref: l4_false_out
 }
 
+data l4_nested_out: Int = 0
+
+data r3_l4_emit_eval_nested_program_input: ProgramOutputBind = {
+  output_ref: l4_nested_out
+}
+
 data r3_verification_l4_emit_eval_match_skeleton: TestClaim = {
   name: "r3_verification_l4_emit_eval_match_skeleton",
   source: "// R3 L4 — branch-only claim program on the current eager PR-B spine (no Callable / fold lambdas) so `dag_eval_output` can use `evaluate_body` while Callable remains fail-closed.\n\nlet l4_pick: Bool = true\n\nlet l4_out: Int =\n  match l4_pick {\n    True => 3\n    False => 0\n  }\n",
@@ -57,13 +63,26 @@ data r3_verification_l4_emit_eval_false_branch: TestClaim = {
   requires: []
 }
 
+data r3_verification_l4_emit_eval_nested_branch: TestClaim = {
+  name: "r3_verification_l4_emit_eval_nested_branch",
+  source: "// R3 L4 — third W1 Rust/Int receipt inside the current Int-only ceiling: nested Bool branch, one named Int output bind.\n\nlet l4_outer_pick: Bool = true\nlet l4_inner_pick: Bool = false\n\nlet l4_nested_out: Int =\n  match l4_outer_pick {\n    True => match l4_inner_pick {\n      True => 5\n      False => 7\n    }\n    False => 0\n  }\n",
+  file_name: "r3_verification_l4_emit_eval_nested_branch.v3",
+  predicate: DifferentialEquals(
+    rust_emit_output,
+    dag_eval_output,
+    r3_l4_emit_eval_nested_program_input
+  ),
+  requires: []
+}
+
 // Declaration id is fixture-local and distinct from `r3_verification_l7_algebraic_laws.dag` so two
 // modules are never ambiguous under one loader. Lane 1 acceptance may later merge both claims into
 // one module under `r3_verification_l4_l7_direct_suite` (parent brief).
 data r3_verification_l4_emit_eval_skeleton_suite: TestSuite = {
   name: "r3_verification_l4_emit_eval_skeleton_suite",
   claims: [
     r3_verification_l4_emit_eval_match_skeleton,
-    r3_verification_l4_emit_eval_false_branch
+    r3_verification_l4_emit_eval_false_branch,
+    r3_verification_l4_emit_eval_nested_branch
   ]
 }

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

@@ -20,6 +20,7 @@ const L4_FIXTURE_PATH: &str =
 const L4_SUITE: &str = "r3_verification_l4_emit_eval_skeleton_suite";
 const L4_CLAIM: &str = "r3_verification_l4_emit_eval_match_skeleton";
 const L4_FALSE_CLAIM: &str = "r3_verification_l4_emit_eval_false_branch";
+const L4_NESTED_CLAIM: &str = "r3_verification_l4_emit_eval_nested_branch";
 
 const L4_MIXED_FIXTURE: &str =
     include_str!("../fixtures/r3_verification_l4_emit_eval_mixed_lineage.dag");
@@ -89,7 +90,7 @@ fn r3_verification_l4_emit_eval_match_skeleton_passes_w1_emit_vs_eval() {
     run_on_larger_stack(|| {
         let dag = cached_compile(L4_FIXTURE, L4_FIXTURE_PATH, &L4_DAG);
         let results = TestRunner::new(dag).run_suite(L4_SUITE);
-        assert_eq!(results.len(), 2);
+        assert_eq!(results.len(), 3);
         assert_eq!(results[0].claim_name, L4_CLAIM);
         assert!(
             matches!(results[0].result, ClaimResult::Pass),
@@ -104,7 +105,7 @@ fn r3_verification_l4_emit_eval_false_branch_passes_w1_emit_vs_eval() {
     run_on_larger_stack(|| {
         let dag = cached_compile(L4_FIXTURE, L4_FIXTURE_PATH, &L4_DAG);
         let results = TestRunner::new(dag).run_suite(L4_SUITE);
-        assert_eq!(results.len(), 2);
+        assert_eq!(results.len(), 3);
         assert_eq!(results[1].claim_name, L4_FALSE_CLAIM);
         assert!(
             matches!(results[1].result, ClaimResult::Pass),
@@ -114,6 +115,21 @@ fn r3_verification_l4_emit_eval_false_branch_passes_w1_emit_vs_eval() {
     });
 }
 
+#[test]
+fn r3_verification_l4_emit_eval_nested_branch_passes_w1_emit_vs_eval() {
+    run_on_larger_stack(|| {
+        let dag = cached_compile(L4_FIXTURE, L4_FIXTURE_PATH, &L4_DAG);
+        let results = TestRunner::new(dag).run_suite(L4_SUITE);
+        assert_eq!(results.len(), 3);
+        assert_eq!(results[2].claim_name, L4_NESTED_CLAIM);
+        assert!(
+            matches!(results[2].result, ClaimResult::Pass),
+            "expected W1 DifferentialEquals(rust_emit_output, dag_eval_output) Pass (nested branch Int 7); got {:?}",
+            results[2].result
+        );
+    });
+}
+
 #[test]
 fn r3_verification_l4_emit_eval_mixed_lineage_stays_not_yet_implemented() {
     run_on_larger_stack(|| {