[codex] Add L4 add-then-branch emit/eval receipt

scripts/check-test-timeout.sh

@@ -45,7 +45,7 @@
 #   TEST_TIMEOUT_EXEMPT   Path to exemption file
 #                         (default scripts/slow-test-exemptions.txt).
 #   TEST_TIMEOUT_MAX_EXEMPTIONS
-#                         Ratchet floor for active exemption entries (default 45;
+#                         Ratchet floor for active exemption entries (default 46;
 #                         keep aligned with non-comment rows in
 #                         scripts/slow-test-exemptions.txt). Raise or lower in the same PR
 #                         as exemption rows; lower when deleting exemptions.
@@ -56,7 +56,7 @@ log_file_arg=${1:-}
 budget_ms=${2:-${TEST_TIMEOUT_MS:-2000}}
 pkg=${TEST_TIMEOUT_PACKAGE:-v3-compiler}
 exempt_file=${TEST_TIMEOUT_EXEMPT:-scripts/slow-test-exemptions.txt}
-max_exemptions=${TEST_TIMEOUT_MAX_EXEMPTIONS:-45}
+max_exemptions=${TEST_TIMEOUT_MAX_EXEMPTIONS:-46}
 
 script_dir=$(cd "$(dirname "$0")" && pwd)
 repo_root=$(cd "$script_dir/.." && pwd)

scripts/slow-test-exemptions.txt

@@ -63,6 +63,7 @@ m2_lens_idempotency_migration_test::idempotency_emitted_analyze_matches_oracle
 m2_lens_provenance_migration_test::lens_provenance_dag_runs_end_to_end_via_rustc_harness  # Lane 2 migration harness roundtrip; compile-heavy oracle test remains explicit until lens migration paydown.
 m2_lens_unused_parameters_migration_test::unused_parameters_dag_runs_end_to_end_via_rustc_harness  # Lane 2 migration harness roundtrip; compile-heavy oracle test remains explicit until lens migration paydown.
 m2_lens_unused_parameters_migration_test::unused_parameters_dag_self_analysis_reports_zero_findings  # Lane 2 migration harness roundtrip; compile-heavy self-analysis remains explicit until lens migration paydown.
+pb_method_template_projection_dag_emit::tests::legacy_map_key_collision_surfaces_typed_error  # R3 PB method-template projection producer: cold `generated_full_bootstrap_dag()` + projection write fail-closed collision receipt exceeded the 2s ratchet on PR #2585. Paydown: share bootstrap fixture or reduce the collision fixture once `docs/decisions/r3-row85-method-template-read-surface.md` projection surface is fully migrated.
 r1c_e_emit_gates_dag_test::r1c_e_emit_gates_suite_passes_through_runner  # R1C-E emit-gates `.dag` wrapper shells through the runner/binary harness and sits on the 2s CI edge (2166ms on PR #1233); paydown owned by R1C-E emit-gates runner/shared-setup work, not this impossible-bugs row-removal slice.
 r3_verification_l4_l7_l5_skeleton_test::r3_verification_l4_emit_eval_false_branch_passes_w1_emit_vs_eval  # R3-V L4 W1 direct consumer fixture runs the full emit-vs-eval suite through TestRunner and can sit just above 2s on CI (2072ms on PR #1799); paydown owned by R3-V L4/L7 direct harness shared runner setup, see docs/briefs/r3-v-l4-l7-direct-w1-consumer-spec.md.
 r3_verification_l4_l7_l5_skeleton_test::r3_verification_l7_algebraic_law_matrix_has_current_runner_receipts  # R3 gate #10 / issue #2382: single `L7_MATRIX_SUITE` runner pass + per-claim source receipts ~2.4s cold CI (PR #2394); paydown: slimmer witness applications or shared runner amortization with other Lane 1 L7 rows.

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

@@ -39,6 +39,12 @@ data r3_l4_emit_eval_nested_program_input: ProgramOutputBind = {
   output_ref: l4_nested_out
 }
 
+data l4_add_then_branch_out: Int = 0
+
+data r3_l4_emit_eval_add_then_branch_program_input: ProgramOutputBind = {
+  output_ref: l4_add_then_branch_out
+}
+
 // §1.8 gate #9 `l4_emit_eval_match` — slice-1 certification seed (Rust / Int stdout); lane closure
 // still requires exhaustive corpus growth per `r3-structure.md` §Acceptance.
 data l4_emit_eval_match: TestClaim = {
@@ -77,6 +83,18 @@ data r3_verification_l4_emit_eval_nested_branch: TestClaim = {
   requires: []
 }
 
+data r3_verification_l4_emit_eval_add_then_branch: TestClaim = {
+  name: "r3_verification_l4_emit_eval_add_then_branch",
+  source: "// R3 L4 — corpus seed from the Lane 1 brief: function call + Int arithmetic + branch lowering + one named output bind.\n\nfn l4_add(a: Int, b: Int) -> Int = a + b\n\nlet l4_acc: Int = l4_add(1, 2)\nlet l4_add_then_branch_out: Int =\n  match l4_acc == 3 {\n    True => l4_acc\n    False => 0\n  }\n",
+  file_name: "r3_verification_l4_emit_eval_add_then_branch.v3",
+  predicate: DifferentialEquals(
+    rust_emit_output,
+    dag_eval_output,
+    r3_l4_emit_eval_add_then_branch_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. L7 claims join this suite name when lane 1 closes
 // under one loader module (parent brief); until then this suite lists L4 certification seeds only.
@@ -85,6 +103,7 @@ data r3_verification_l4_l7_direct_suite: TestSuite = {
   claims: [
     l4_emit_eval_match,
     r3_verification_l4_emit_eval_false_branch,
-    r3_verification_l4_emit_eval_nested_branch
+    r3_verification_l4_emit_eval_nested_branch,
+    r3_verification_l4_emit_eval_add_then_branch
   ]
 }

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

@@ -29,6 +29,7 @@ const L4_SUITE: &str = "r3_verification_l4_l7_direct_suite";
 const L4_CLAIM: &str = "l4_emit_eval_match";
 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_ADD_THEN_BRANCH_CLAIM: &str = "r3_verification_l4_emit_eval_add_then_branch";
 
 const L4_MIXED_FIXTURE: &str =
     include_str!("../fixtures/r3_verification_l4_emit_eval_mixed_lineage.dag");
@@ -142,19 +143,35 @@ fn r3_verification_l4_emit_eval_nested_branch_passes_w1_emit_vs_eval() {
     );
 }
 
-/// Suite-wide shape: exactly three named W1 claims, each passing (complements per-claim
+#[test]
+fn r3_verification_l4_emit_eval_add_then_branch_passes_w1_emit_vs_eval() {
+    let evaluation = l4_run_named_claim(L4_ADD_THEN_BRANCH_CLAIM);
+    assert_eq!(evaluation.claim_name, L4_ADD_THEN_BRANCH_CLAIM);
+    assert!(
+        matches!(evaluation.result, ClaimResult::Pass),
+        "expected W1 DifferentialEquals(rust_emit_output, dag_eval_output) Pass (call + Int arithmetic + branch Int 3); got {:?}",
+        evaluation.result
+    );
+}
+
+/// Suite-wide shape: exactly four named W1 claims, each passing (complements per-claim
 /// `run_claim` tests without pinning suite result order).
 #[test]
-fn r3_verification_l4_l7_direct_suite_lists_three_l4_certification_seed_claims() {
+fn r3_verification_l4_l7_direct_suite_lists_four_l4_certification_seed_claims() {
     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,
-            "`{L4_SUITE}` should wire exactly three W1 row claims"
+            4,
+            "`{L4_SUITE}` should wire exactly four W1 row claims"
         );
-        for name in [L4_CLAIM, L4_FALSE_CLAIM, L4_NESTED_CLAIM] {
+        for name in [
+            L4_CLAIM,
+            L4_FALSE_CLAIM,
+            L4_NESTED_CLAIM,
+            L4_ADD_THEN_BRANCH_CLAIM,
+        ] {
             assert!(
                 results.iter().any(|r| r.claim_name == name),
                 "missing `{name}` in suite results: {results:?}"