Skip to content
Merged
Show file tree
Hide file tree
Changes from all commits
Commits
File filter

Filter by extension

Filter by extension

Conversations
Failed to load comments.
Loading
Jump to
Jump to file
Failed to load files.
Loading
Diff view
Diff view
51 changes: 51 additions & 0 deletions src/v3/compiler/src/test_runner.rs
Original file line number Diff line number Diff line change
Expand Up @@ -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
Expand Down Expand Up @@ -2387,6 +2394,50 @@ impl<'a> TestRunner<'a> {
};
}

// R3 gate #50 (`auto_memoization_no_caching_for_one_shot`): one-shot call sites must not

Copy link
Copy Markdown
Contributor Author

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

BLOCKING: The new src/v3 hand-Rust runner bridge has a dissolution note but no required P5 receipt: deleted scaffold path, SG-0 shrink, or deferral lane plus concrete ROADMAP row.

// 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::<i64>() {

Copy link
Copy Markdown
Contributor Author

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

BLOCKING: LiteralBits::Int is already the typed i64 carrier, so calling parse::() on it will not compile; this violates INVARIANTS.md P2 typed-boundary discipline.

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 = <literal>`"
));
}
};
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.
Expand Down
Original file line number Diff line number Diff line change
Expand Up @@ -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<AutoMemoizationEvidence>
type repeated_pure_call_expected_report = DimensionReport<AutoMemoizationEvidence>
type one_shot_call_observed_report = DimensionReport<AutoMemoizationEvidence>
Expand Down Expand Up @@ -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: []
}
Expand Down
Original file line number Diff line number Diff line change
Expand Up @@ -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};
Expand Down Expand Up @@ -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,
Expand All @@ -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}"),
}
}
Expand Down
Loading