From b3ed4e2ff2c1601c05f4e2efff5d8dc0f1cd2a42 Mon Sep 17 00:00:00 2001 From: Brian Searls Date: Sun, 10 May 2026 02:22:36 +0000 Subject: [PATCH] r3 gate 50 one-shot memoization witness --- src/v3/compiler/src/test_runner.rs | 51 +++++++++++++++++++ .../r3_free_consequences_first_batch.dag | 14 +++-- .../r3_free_consequences_first_batch_test.rs | 19 ++++--- 3 files changed, 73 insertions(+), 11 deletions(-) diff --git a/src/v3/compiler/src/test_runner.rs b/src/v3/compiler/src/test_runner.rs index 7ab345e4564..a25d63109fa 100644 --- a/src/v3/compiler/src/test_runner.rs +++ b/src/v3/compiler/src/test_runner.rs @@ -54,6 +54,13 @@ const R3_PARALLEL_EMIT_WITNESS_LENS_NAME: &str = "r3_auto_parallelism_parallel_e const R3_BRANCH_ARMS_SERIALIZE_WITNESS_LENS_NAME: &str = "r3_auto_parallelism_branch_arms_serialize_witness"; +/// R3 gate #50 (`LensOutputEquals` witness in `r3_free_consequences_first_batch.dag`). +/// +/// A one-shot pure call may emit a direct call / inlined expression, but must not introduce +/// memoization scaffolding. Repeated-call caching remains deferred to the purity+cost lens +/// composition producer. +const R3_ONE_SHOT_NO_MEMO_WITNESS_LENS_NAME: &str = "r3_auto_memoization_one_shot_no_cache_witness"; + /// Host-written forward fold for structural depth costs (see `src/v3/lenses/complexity.dag`). /// /// T-LaneE `DifferentialEquals` compares this receipt to [`crate::lens_cost::cost_of`] (emit output @@ -2387,6 +2394,50 @@ impl<'a> TestRunner<'a> { }; } + // R3 gate #50 (`auto_memoization_no_caching_for_one_shot`): one-shot call sites must not + // emit memo/cache scaffolding. Structural witness via emitted Rust text; dissolution when + // the AutoMemoizationEvidence producer reaches `.dag`. + if lens_decl.name.as_deref() == Some(R3_ONE_SHOT_NO_MEMO_WITNESS_LENS_NAME) { + let expected_int = match expected_decl.value_body.as_ref() { + Some(ValueBody::Scalar(LiteralBits::Int(s))) => match s.parse::() { + Ok(v) => v, + Err(_) => { + return ClaimResult::Fail(format!( + "LensOutputEquals(r3_auto_memoization_one_shot_no_cache_witness): expected Int literal is not a valid i64 decimal for `{expected_name}`" + )); + } + }, + _ => { + return ClaimResult::Fail(format!( + "LensOutputEquals(r3_auto_memoization_one_shot_no_cache_witness): expected_ref `{expected_name}` must be `data ...: Int = `" + )); + } + }; + let emitted = match crate::emit_rust::emit_rust(&program_dag) { + Ok(s) => s, + Err(err) => { + return ClaimResult::Fail(format!( + "LensOutputEquals(r3_auto_memoization_one_shot_no_cache_witness): emit_rust failed for `{}`: {err:?}", + claim.file_name + )); + } + }; + let scaffolding_absent = !emitted.contains("memo") + && !emitted.contains("Memo") + && !emitted.contains("cache") + && !emitted.contains("Cache") + && !emitted.contains("HashMap"); + let computed_int = i64::from(scaffolding_absent); + return if computed_int == expected_int { + ClaimResult::Pass + } else { + ClaimResult::Fail(format!( + "LensOutputEquals(r3_auto_memoization_one_shot_no_cache_witness): expected `{expected_int}` (1 = no memo/cache scaffolding), computed `{computed_int}` for `{}`", + claim.file_name + )) + }; + } + // T-LaneE cost receipt: `ProgramOutputBind` is the structural contract for a claim // source output-bind cost check. Dispatch on that input role, not on lens declaration // spelling; otherwise the canonical lens-name bridge would survive under a helper. diff --git a/src/v3/compiler/tests/fixtures/r3_free_consequences_first_batch.dag b/src/v3/compiler/tests/fixtures/r3_free_consequences_first_batch.dag index 00918fbc17c..ae83f2b5d91 100644 --- a/src/v3/compiler/tests/fixtures/r3_free_consequences_first_batch.dag +++ b/src/v3/compiler/tests/fixtures/r3_free_consequences_first_batch.dag @@ -54,6 +54,11 @@ fn r3_auto_parallelism_branch_arms_serialize_witness(_d: Dag) -> Int = 0 data r3_auto_parallelism_branch_arms_serialize_expected: Int = 1 +// R3 #50 witness: one-shot pure call sites must not emit memo/cache scaffolding. +fn r3_auto_memoization_one_shot_no_cache_witness(_d: Dag) -> Int = 0 + +data r3_auto_memoization_one_shot_no_cache_expected: Int = 1 + type repeated_pure_call_observed_report = DimensionReport type repeated_pure_call_expected_report = DimensionReport type one_shot_call_observed_report = DimensionReport @@ -108,11 +113,12 @@ data auto_memoization_repeated_pure_call_cached: TestClaim = { data auto_memoization_no_caching_for_one_shot: TestClaim = { name: "auto_memoization_no_caching_for_one_shot", - source: "// free-consequences fixture: one-shot calls do not emit memoization scaffolding.\nlet _: Int = 0\n", + source: "// free-consequences fixture: one-shot calls do not emit memoization scaffolding.\nfn bump(x: Int) -> Int = x + 1\nlet _: Int = bump(41)\n", file_name: "r3_free_consequences_auto_memoization_one_shot.v3", - predicate: BinaryDimensionReportEquals( - one_shot_call_observed_report, - one_shot_call_expected_report + predicate: LensOutputEquals( + r3_auto_memoization_one_shot_no_cache_witness, + auto_parallelism_program_input, + r3_auto_memoization_one_shot_no_cache_expected ), requires: [] } diff --git a/src/v3/compiler/tests/integration/r3_free_consequences_first_batch_test.rs b/src/v3/compiler/tests/integration/r3_free_consequences_first_batch_test.rs index 658eba1f301..a746e8a9927 100644 --- a/src/v3/compiler/tests/integration/r3_free_consequences_first_batch_test.rs +++ b/src/v3/compiler/tests/integration/r3_free_consequences_first_batch_test.rs @@ -2,11 +2,10 @@ //! //! R3 T-Free-Consequences first-batch author-now/fire-later claims. //! Gate `#43` asserts pairwise-independent top-level binds emit a parallel Rust -//! schedule, and gate `#45` asserts a Bool branch lowers to `if … else` with no -//! `thread::scope` scheduling on the arms (both `LensOutputEquals` + runner -//! witnesses). Gate `#44` stays fail-closed on the scalar parallelism -//! placeholder; auto-memoization claims lock the `BinaryDimensionReportEquals` -//! shape. +//! schedule; gate `#44` stays fail-closed on the scalar parallelism placeholder; +//! gate `#45` asserts a Bool branch lowers to `if … else` with no `thread::scope` +//! scheduling on the arms; gate `#50` asserts one-shot pure calls do not emit +//! memo/cache scaffolding. Repeated-call memoization remains deferred. use v3_compiler::compile_to_dag; use v3_compiler::test_runner::{ClaimResult, TestRunner}; @@ -76,8 +75,7 @@ fn r3_free_consequences_first_batch_reaches_unified_predicate_shape_inner() { result.result ); } - "auto_memoization_repeated_pure_call_cached" - | "auto_memoization_no_caching_for_one_shot" => { + "auto_memoization_repeated_pure_call_cached" => { assert!( matches!( &result.result, @@ -89,6 +87,13 @@ fn r3_free_consequences_first_batch_reaches_unified_predicate_shape_inner() { result.result ); } + "auto_memoization_no_caching_for_one_shot" => { + assert!( + matches!(&result.result, ClaimResult::Pass), + "expected {expected_name} to Pass (one-shot memoization absence witness), got {:?}", + result.result + ); + } _ => panic!("unexpected claim name: {expected_name}"), } }