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 5471f1a1b26..512e48f2e74 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 @@ -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,6 +63,18 @@ 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). @@ -64,6 +82,7 @@ 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 ] } 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 c70d0c8906e..f127ff80339 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 @@ -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(|| {