From db67e6661431f9d01a994c37fc6771a9bf7ed391 Mon Sep 17 00:00:00 2001 From: Brian Searls Date: Sun, 10 May 2026 09:04:11 +0000 Subject: [PATCH 1/2] Add L4 add-then-branch emit/eval receipt --- .../r3_verification_l4_emit_eval_match.dag | 21 ++++++++++++++- .../r3_verification_l4_l7_l5_skeleton_test.rs | 27 +++++++++++++++---- 2 files changed, 42 insertions(+), 6 deletions(-) diff --git a/src/v3/compiler/tests/fixtures/r3_verification_l4_emit_eval_match.dag b/src/v3/compiler/tests/fixtures/r3_verification_l4_emit_eval_match.dag index d644cf35b76..6ec9e1c5ebb 100644 --- a/src/v3/compiler/tests/fixtures/r3_verification_l4_emit_eval_match.dag +++ b/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 ] } diff --git a/src/v3/compiler/tests/integration/r3_verification_l4_l7_l5_skeleton_test.rs b/src/v3/compiler/tests/integration/r3_verification_l4_l7_l5_skeleton_test.rs index feda1aa0241..06d0d969bcb 100644 --- a/src/v3/compiler/tests/integration/r3_verification_l4_l7_l5_skeleton_test.rs +++ b/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:?}" From e22b26cb3fef032fdb8f096c8313fe935e997638 Mon Sep 17 00:00:00 2001 From: Brian Searls Date: Sun, 10 May 2026 05:18:17 -0400 Subject: [PATCH 2/2] WIP: R3 gate #9: l4 emit eval match --- scripts/check-test-timeout.sh | 4 ++-- scripts/slow-test-exemptions.txt | 1 + 2 files changed, 3 insertions(+), 2 deletions(-) diff --git a/scripts/check-test-timeout.sh b/scripts/check-test-timeout.sh index e066b8856a0..3679c68c176 100755 --- a/scripts/check-test-timeout.sh +++ b/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) diff --git a/scripts/slow-test-exemptions.txt b/scripts/slow-test-exemptions.txt index 80eee50a02b..5ff759af9c2 100644 --- a/scripts/slow-test-exemptions.txt +++ b/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.