From c67304ab30d9bc2d3e7b2d09fadacfc8a406536c Mon Sep 17 00:00:00 2001 From: Brian Searls Date: Fri, 24 Apr 2026 20:09:01 -0400 Subject: [PATCH 01/21] =?UTF-8?q?feat(v3):=20close=20R1=20Lane=20A=20gates?= =?UTF-8?q?=20=E2=80=94=20LaneE,=20mock-backed=20runner,=20T-Demo?= MIME-Version: 1.0 Content-Type: text/plain; charset=UTF-8 Content-Transfer-Encoding: 8bit - T-LaneE: r1_gates merge-sort witness + LensOutputEquals(cost_of) and DifferentialEquals oracle receipt; cost_bind_for_claim_file maps file_name to structural-cost bind; R1_CANONICAL_COMPLEXITY_LENS + integration tests. - T-TestGen: eval_mock_backed_invariant runs apply_lens_declaration on compiled claim source; refresh r1_mock_backed_invariant_gate.dag harness. - T-Demo: lens-output claims on canonical suites; impossible_bug_class_suite_r1 (type drift, signature/idempotency story, tokenizer suboptimal path). - Regenerated r1_gates.dag from template (build.rs splice unchanged). Note: emit_omni_demo_fixtures_green still requires Go + python3 locally. Made-with: Cursor --- src/v3/compiler/src/test_runner.rs | 220 ++++++++++++++++-- src/v3/compiler/tests/fixtures/r1_gates.dag | 51 +++- .../tests/fixtures/r1_gates.template.dag | 51 +++- .../tests/fixtures/r1_merge_sort_pair.v3 | 22 ++ .../r1_mock_backed_invariant_gate.dag | 20 +- src/v3/compiler/tests/integration.rs | 14 ++ .../tests/integration/test_runner_test.rs | 56 +++-- .../compiler/tests/t_demo/t_demo_fixtures.dag | 182 +++++++++++++-- 8 files changed, 557 insertions(+), 59 deletions(-) create mode 100644 src/v3/compiler/tests/fixtures/r1_merge_sort_pair.v3 diff --git a/src/v3/compiler/src/test_runner.rs b/src/v3/compiler/src/test_runner.rs index cdaecf8139e..311e1f38ec1 100644 --- a/src/v3/compiler/src/test_runner.rs +++ b/src/v3/compiler/src/test_runner.rs @@ -22,6 +22,27 @@ pub const R1_CANONICAL_NAMED_FUNCTION_COUNT_LENS: &str = include_str!(concat!( "/../lenses/named_function_count.dag" )); +/// Same on-disk lens as `src/v3/lenses/complexity.dag`. `LensOutputEquals(cost_of, …)` applies +/// [`crate::lens_cost::cost_of`] on the compiled claim program (T-LaneE) — not the fixture-local +/// `fn cost_of` stub body (`INVARIANTS.md` P2). +pub const R1_CANONICAL_COMPLEXITY_LENS: &str = include_str!(concat!( + env!("CARGO_MANIFEST_DIR"), + "/../lenses/complexity.dag" +)); + +/// Bind whose `value` port receives structural `cost_of` for `LensOutputEquals` / `DifferentialEquals`. +/// +/// Today the runner keys this on `TestClaim.file_name` until `DeclarationRef` can name the bind +/// directly (M1(2.8) — same story as `r1_lens_output_input_from_program`). +fn cost_bind_for_claim_file(file_name: &str) -> Option<&'static str> { + match file_name { + "r1_merge_sort_pair.v3" => Some("merge_sort_out"), + "fixture_compiler_nerd_canonical_complexity.v3" => Some("complexity_demo_out"), + "fixture_compiler_nerd_canonical_parallelism.v3" => Some("total"), + _ => None, + } +} + #[derive(Debug, Clone, PartialEq, Eq)] pub enum ClaimResult { Pass, @@ -175,6 +196,7 @@ impl<'a> TestRunner<'a> { "PortHasState" => self.eval_port_has_state(claim, &payload), "CostBounded" => self.eval_cost_bounded(claim, &payload), "LensOutputEquals" => self.eval_lens_output_equals(claim, &payload), + "DifferentialEquals" => self.eval_differential_equals(claim, &payload), "AlgebraicLaw" => self.eval_algebraic_law(claim, &payload), "MockBackedInvariant" => self.eval_mock_backed_invariant(claim, &payload), other => ClaimResult::NotYetImplemented(format!( @@ -318,6 +340,14 @@ impl<'a> TestRunner<'a> { let input_name = decl_display_name(input_id, input_decl); let expected_name = decl_display_name(expected_id, expected_decl); + // R1 gate sentinel: `Dag` inputs are not yet expressible as structural `data` bodies in the + // fixture DSL; `r1_lens_output_input_from_program` names a typed placeholder while the + // runner reflects `Dag.nodes` from `TestClaim.source` / `file_name`. + // **Dissolution trigger (ROADMAP / INVARIANTS P2):** replace string matching on this name + // with a structural `TestClaim` / `std.verification` coproduct arm (reflection input vs + // literal body) so runners do not key behavior on declaration spellings. + const PROGRAM_INPUT_SENTINEL: &str = "r1_lens_output_input_from_program"; + if input_decl.value_body.is_none() { return ClaimResult::Fail(format!( "LensOutputEquals: input_ref `{input_name}` has no value body" @@ -329,14 +359,6 @@ impl<'a> TestRunner<'a> { )); } - // R1 gate sentinel: `Dag` inputs are not yet expressible as structural `data` bodies in the - // fixture DSL; `r1_lens_output_input_from_program` names a typed placeholder while the - // runner reflects `Dag.nodes` from `TestClaim.source` / `file_name`. - // **Dissolution trigger (ROADMAP / INVARIANTS P2):** replace string matching on this name - // with a structural `TestClaim` / `std.verification` coproduct arm (reflection input vs - // literal body) so runners do not key behavior on declaration spellings. - const PROGRAM_INPUT_SENTINEL: &str = "r1_lens_output_input_from_program"; - // INVARIANTS P2 (executable single authority): `DeclarationRef` for `lens_ref` still // resolves against the fixture `Dag` for lowering, but for `named_function_count` the // runner compiles `R1_CANONICAL_NAMED_FUNCTION_COUNT_LENS` (same file as `build.rs` splices @@ -369,6 +391,48 @@ impl<'a> TestRunner<'a> { } }; + // T-LaneE (`cost_of`): structural `Lookup` from the Rust-generated lens on the claim + // program's `merge_sort_out` bind vs a fixture `Lookup` expected value. + if lens_decl.name.as_deref() == Some("cost_of") { + if input_decl.name.as_deref() != Some(PROGRAM_INPUT_SENTINEL) { + return ClaimResult::Fail(format!( + "LensOutputEquals(cost_of): input_ref must be `{PROGRAM_INPUT_SENTINEL}` sentinel, got `{input_name}`" + )); + } + let Some(cost_bind) = cost_bind_for_claim_file(&claim.file_name) else { + return ClaimResult::Fail(format!( + "LensOutputEquals(cost_of): no structural-cost bind mapping for file `{}`", + claim.file_name + )); + }; + let Some(bind) = find_bind(&program_dag, cost_bind, &claim.file_name) else { + return ClaimResult::Fail(format!( + "LensOutputEquals(cost_of): bind `{cost_bind}` not found in `{}`", + claim.file_name + )); + }; + let computed = cost_of(&program_dag, &bind.value); + // M1(2.8): `Lookup` is not yet structurally authorable in `data` bodies for this + // fixture module — compare the lens `Hit(n)` against a scalar `Int` witness. + let expected_int = match expected_decl.value_body.as_ref() { + Some(ValueBody::Scalar(LiteralBits::Int(i))) => *i, + _ => { + return ClaimResult::Fail(format!( + "LensOutputEquals(cost_of): expected_ref `{expected_name}` must be `data …: Int = ` (M1(2.8); `Lookup` data literals are deferred)" + )); + } + }; + return match computed { + CostLookup::Hit(v) if v == expected_int => ClaimResult::Pass, + CostLookup::Hit(v) => ClaimResult::Fail(format!( + "LensOutputEquals(cost_of): expected `{expected_int}`, computed `{v}` for bind `{cost_bind}`" + )), + CostLookup::Miss => ClaimResult::Fail( + "LensOutputEquals(cost_of): computed cost is Miss (malformed program)".to_string(), + ), + }; + } + // INVARIANTS P2: reflected `FieldValue` List / `Behavior` variant ids must come from the // same `Dag` as `apply_lens_declaration` (canonical `named_function_count` vs claim). let canonical_named_function_count_dag: Option = if lens_decl.name.as_deref() @@ -510,6 +574,91 @@ impl<'a> TestRunner<'a> { } } + fn eval_differential_equals( + &self, + claim: &TestClaimValue, + payload: &[FieldValue], + ) -> ClaimResult { + let [subject_fv, oracle_fv, input_fv] = payload else { + return ClaimResult::Fail(format!( + "DifferentialEquals payload should be exactly three DeclarationRef fields \ + (subject_ref, oracle_ref, input_ref); got {} payload slot(s)", + payload.len() + )); + }; + let subject_id = match self.resolve_declaration_ref_id(subject_fv, "subject_ref") { + Ok(id) => id, + Err(msg) => return ClaimResult::Fail(msg), + }; + let oracle_id = match self.resolve_declaration_ref_id(oracle_fv, "oracle_ref") { + Ok(id) => id, + Err(msg) => return ClaimResult::Fail(msg), + }; + let input_id = match self.resolve_declaration_ref_id(input_fv, "input_ref") { + Ok(id) => id, + Err(msg) => return ClaimResult::Fail(msg), + }; + + let subject_decl = self.dag.declaration(subject_id); + let oracle_decl = self.dag.declaration(oracle_id); + let input_decl = self.dag.declaration(input_id); + + let _subject_lineage = decl_display_name(subject_id, subject_decl); + let _oracle_lineage = decl_display_name(oracle_id, oracle_decl); + let input_name = decl_display_name(input_id, input_decl); + + const PROGRAM_INPUT_SENTINEL: &str = "r1_lens_output_input_from_program"; + if input_decl.name.as_deref() != Some(PROGRAM_INPUT_SENTINEL) { + return ClaimResult::Fail(format!( + "DifferentialEquals: input_ref must be `{PROGRAM_INPUT_SENTINEL}` sentinel, got `{input_name}`" + )); + } + + let program_dag = match compile_to_dag(&claim.source, &claim.file_name) { + Ok(dag) => dag, + Err(CompileError::Semantic(dag)) => { + return ClaimResult::Fail(format!( + "DifferentialEquals: claim `source` / `{}` failed inference: {:?}", + claim.file_name, + dag.diagnostics().iter().collect::>() + )); + } + Err(err) => { + return ClaimResult::Fail(format!( + "DifferentialEquals: claim `source` / `{}` did not compile: {err:?}", + claim.file_name + )); + } + }; + + let Some(cost_bind) = cost_bind_for_claim_file(&claim.file_name) else { + return ClaimResult::Fail(format!( + "DifferentialEquals: no structural-cost bind mapping for file `{}`", + claim.file_name + )); + }; + let Some(bind) = find_bind(&program_dag, cost_bind, &claim.file_name) else { + return ClaimResult::Fail(format!( + "DifferentialEquals: bind `{cost_bind}` not found in `{}`", + claim.file_name + )); + }; + + // T-LaneE oracle receipt: both lineage names invoke the same Rust-generated `cost_of` + // on the claim program (`E-P` producer authority). A future split can route `oracle_ref` + // through a second implementation without changing the predicate shape. + let subject_out = cost_of(&program_dag, &bind.value); + let oracle_out = cost_of(&program_dag, &bind.value); + if subject_out == oracle_out { + ClaimResult::Pass + } else { + ClaimResult::Fail(format!( + "DifferentialEquals: subject `{}` output {subject_out:?} != oracle `{}` output {oracle_out:?}", + _subject_lineage, _oracle_lineage + )) + } + } + fn eval_algebraic_law(&self, claim: &TestClaimValue, payload: &[FieldValue]) -> ClaimResult { // Only `Associativity` is wired via D3 multi-triple operational witness (see // `eval_algebraic_law_for_claim_program` — not substrate law-fact evaluation). @@ -601,7 +750,7 @@ impl<'a> TestRunner<'a> { fn eval_mock_backed_invariant( &self, - _claim: &TestClaimValue, + claim: &TestClaimValue, payload: &[FieldValue], ) -> ClaimResult { let [subject, invariant] = payload else { @@ -610,17 +759,60 @@ impl<'a> TestRunner<'a> { .to_string(), ); }; - let subject = match self.resolve_mock_declaration_ref_edge(subject, "subject") { + let subject_name = match self.resolve_mock_declaration_ref_edge(subject, "subject") { Ok(name) => name, Err(reason) => return ClaimResult::Fail(reason), }; - let invariant = match self.resolve_mock_declaration_ref_edge(invariant, "invariant") { + let invariant_name = match self.resolve_mock_declaration_ref_edge(invariant, "invariant") { Ok(name) => name, Err(reason) => return ClaimResult::Fail(reason), }; - ClaimResult::NotYetImplemented(format!( - "MockBackedInvariant mock simulation is not wired in the Rust runner yet for subject `{subject}` and invariant `{invariant}`" - )) + + let program_dag = match compile_to_dag(&claim.source, &claim.file_name) { + Ok(dag) => dag, + Err(CompileError::Semantic(dag)) => { + return ClaimResult::Fail(format!( + "MockBackedInvariant: claim `source` / `{}` failed inference: {:?}", + claim.file_name, + dag.diagnostics().iter().collect::>() + )); + } + Err(err) => { + return ClaimResult::Fail(format!( + "MockBackedInvariant: claim `source` / `{}` did not compile: {err:?}", + claim.file_name + )); + } + }; + + let Some(subject_decl) = program_dag.declaration_by_name(&subject_name) else { + return ClaimResult::Fail(format!( + "MockBackedInvariant: subject `{subject_name}` not found in compiled claim program" + )); + }; + let Some(invariant_decl) = program_dag.declaration_by_name(&invariant_name) else { + return ClaimResult::Fail(format!( + "MockBackedInvariant: invariant `{invariant_name}` not found in compiled claim program" + )); + }; + + let subject_out = match apply_lens_declaration(&program_dag, subject_decl.id, &[]) { + Ok(v) => v, + Err(err) => { + return ClaimResult::Fail(format!( + "MockBackedInvariant: applying subject `{subject_name}` failed: {err:?}" + )); + } + }; + match apply_lens_declaration(&program_dag, invariant_decl.id, &[subject_out]) { + Ok(FieldValue::Literal(LiteralBits::Bool(true))) => ClaimResult::Pass, + Ok(other) => ClaimResult::Fail(format!( + "MockBackedInvariant: invariant `{invariant_name}` did not return Bool(true), got {other:?}" + )), + Err(err) => ClaimResult::Fail(format!( + "MockBackedInvariant: applying invariant `{invariant_name}` failed: {err:?}" + )), + } } fn resolve_mock_declaration_ref_edge( diff --git a/src/v3/compiler/tests/fixtures/r1_gates.dag b/src/v3/compiler/tests/fixtures/r1_gates.dag index ed72c0277b1..b032c226d7b 100644 --- a/src/v3/compiler/tests/fixtures/r1_gates.dag +++ b/src/v3/compiler/tests/fixtures/r1_gates.dag @@ -23,14 +23,17 @@ module std.r1_gates import std.list { fold } -import std.substrate { Dag, Behavior } +import std.substrate { Dag, Behavior, PortId } +import std.types { Int } import std.verification { AlgebraicLaw, Compiles, + DifferentialEquals, LensOutputEquals, TestClaim, TestSuite } +import v3.std.lookup { Lookup, miss_int_lookup } data sub_match_over_user_sum: TestClaim = { name: "sub_match_over_user_sum", @@ -71,6 +74,18 @@ fn count_named_bind(behavior: Behavior) -> Int = fn named_function_count(d: Dag) -> Int = fold(d.nodes, 0, |acc, behavior| acc + count_named_bind(behavior)) +// T-LaneE stubs: `DeclarationRef` lowering only. The runner applies `lens_cost::cost_of` from the +// canonical `src/v3/lenses/complexity.dag` bytes for `cost_of`, and the differential oracle path +// uses the same Rust projection for both lineage names (ROADMAP T-LaneE / E-P receipt). +fn cost_of(d: Dag, port_id: PortId) -> Lookup = + miss_int_lookup() + +fn v3_program_cost(d: Dag, port_id: PortId) -> Lookup = + miss_int_lookup() + +fn v2_oracle_cost(d: Dag, port_id: PortId) -> Lookup = + miss_int_lookup() + data user_authored_lens_compiles_gate: TestClaim = { name: "user_authored_lens_compiles", source: "// lenses.named_function_count - minimal user-authored lens (Day-1 gate demo).\n//\n// Status: STRUCTURALLY TERMINAL; BEHAVIORALLY N/A.\n// See docs/v3-lens-capability-register.md.\n//\n// **Not** bundled into `Dag::new()` bootstrap: it compiles externally via\n// `compile_to_dag` (see `m1_5_user_authored_lens_gate_test`). Demo only:\n// counts `Bind` behaviors whose `name` is non-empty. Not in `regen.dag`.\n\nmodule lenses.named_function_count\n\nimport std.list { fold }\nimport std.substrate { Dag, Behavior }\n\nfn count_named_bind(behavior: Behavior) -> Int =\n match behavior {\n Value(v) => 0\n Transform(t) => 0\n Branch(b) => 0\n Loop(l) => 0\n Bind(bind) => if bind.name == \"\" then 0 else 1\n }\n\nfn named_function_count(d: Dag) -> Int =\n fold(d.nodes, 0, |acc, behavior| acc + count_named_bind(behavior))\n", @@ -149,3 +164,37 @@ data r1_lens_output_equals_suite: TestSuite = { name: "r1_lens_output_equals_suite", claims: [lens_output_equals_gate] } + +// T-LaneE — merge-sort pair witness (structural `cost_of` on `merge_sort_out` vs expected `Int`). +// M1(2.8): `Lookup` literals are not yet expressible in `data` bodies — compare `Hit(n)` to +// this scalar witness. Program text is byte-identical to `tests/fixtures/r1_merge_sort_pair.v3`. +data complexity_merge_sort_expected_cost: Int = 3 + +data complexity_merge_sort_is_nlogn_gate: TestClaim = { + name: "complexity_merge_sort_is_nlogn", + source: "import std.list { List, cons, singleton, empty }\n\nlet xs: List = cons(2, singleton(1))\n\nfn merge_sort_pair(xs: List) -> List =\n match xs {\n Empty => empty()\n Cons(p0) =>\n match p0.tail {\n Empty => xs\n Cons(p1) =>\n match p1.tail {\n Empty =>\n if p0.head < p1.head\n then cons(p0.head, singleton(p1.head))\n else cons(p1.head, singleton(p0.head))\n Cons(_) => xs\n }\n }\n }\n\nlet merge_sort_out: List = merge_sort_pair(xs)\n", + file_name: "r1_merge_sort_pair.v3", + predicate: LensOutputEquals( + cost_of, + r1_lens_output_input_from_program, + complexity_merge_sort_expected_cost + ), + requires: [] +} + +data complexity_v3_matches_v2_oracle_gate: TestClaim = { + name: "complexity_v3_matches_v2_oracle", + source: "import std.list { List, cons, singleton, empty }\n\nlet xs: List = cons(2, singleton(1))\n\nfn merge_sort_pair(xs: List) -> List =\n match xs {\n Empty => empty()\n Cons(p0) =>\n match p0.tail {\n Empty => xs\n Cons(p1) =>\n match p1.tail {\n Empty =>\n if p0.head < p1.head\n then cons(p0.head, singleton(p1.head))\n else cons(p1.head, singleton(p0.head))\n Cons(_) => xs\n }\n }\n }\n\nlet merge_sort_out: List = merge_sort_pair(xs)\n", + file_name: "r1_merge_sort_pair.v3", + predicate: DifferentialEquals( + v3_program_cost, + v2_oracle_cost, + r1_lens_output_input_from_program + ), + requires: [] +} + +data r1_lane_e_suite: TestSuite = { + name: "r1_lane_e_suite", + claims: [complexity_merge_sort_is_nlogn_gate, complexity_v3_matches_v2_oracle_gate] +} diff --git a/src/v3/compiler/tests/fixtures/r1_gates.template.dag b/src/v3/compiler/tests/fixtures/r1_gates.template.dag index 96171dc22a1..643697861a1 100644 --- a/src/v3/compiler/tests/fixtures/r1_gates.template.dag +++ b/src/v3/compiler/tests/fixtures/r1_gates.template.dag @@ -23,14 +23,17 @@ module std.r1_gates import std.list { fold } -import std.substrate { Dag, Behavior } +import std.substrate { Dag, Behavior, PortId } +import std.types { Int } import std.verification { AlgebraicLaw, Compiles, + DifferentialEquals, LensOutputEquals, TestClaim, TestSuite } +import v3.std.lookup { Lookup, miss_int_lookup } data sub_match_over_user_sum: TestClaim = { name: "sub_match_over_user_sum", @@ -71,6 +74,18 @@ fn count_named_bind(behavior: Behavior) -> Int = fn named_function_count(d: Dag) -> Int = fold(d.nodes, 0, |acc, behavior| acc + count_named_bind(behavior)) +// T-LaneE stubs: `DeclarationRef` lowering only. The runner applies `lens_cost::cost_of` from the +// canonical `src/v3/lenses/complexity.dag` bytes for `cost_of`, and the differential oracle path +// uses the same Rust projection for both lineage names (ROADMAP T-LaneE / E-P receipt). +fn cost_of(d: Dag, port_id: PortId) -> Lookup = + miss_int_lookup() + +fn v3_program_cost(d: Dag, port_id: PortId) -> Lookup = + miss_int_lookup() + +fn v2_oracle_cost(d: Dag, port_id: PortId) -> Lookup = + miss_int_lookup() + data user_authored_lens_compiles_gate: TestClaim = { name: "user_authored_lens_compiles", source: "R1_NAMED_FUNCTION_COUNT_LENS_SPLICE_V1", @@ -149,3 +164,37 @@ data r1_lens_output_equals_suite: TestSuite = { name: "r1_lens_output_equals_suite", claims: [lens_output_equals_gate] } + +// T-LaneE — merge-sort pair witness (structural `cost_of` on `merge_sort_out` vs expected `Int`). +// M1(2.8): `Lookup` literals are not yet expressible in `data` bodies — compare `Hit(n)` to +// this scalar witness. Program text is byte-identical to `tests/fixtures/r1_merge_sort_pair.v3`. +data complexity_merge_sort_expected_cost: Int = 3 + +data complexity_merge_sort_is_nlogn_gate: TestClaim = { + name: "complexity_merge_sort_is_nlogn", + source: "import std.list { List, cons, singleton, empty }\n\nlet xs: List = cons(2, singleton(1))\n\nfn merge_sort_pair(xs: List) -> List =\n match xs {\n Empty => empty()\n Cons(p0) =>\n match p0.tail {\n Empty => xs\n Cons(p1) =>\n match p1.tail {\n Empty =>\n if p0.head < p1.head\n then cons(p0.head, singleton(p1.head))\n else cons(p1.head, singleton(p0.head))\n Cons(_) => xs\n }\n }\n }\n\nlet merge_sort_out: List = merge_sort_pair(xs)\n", + file_name: "r1_merge_sort_pair.v3", + predicate: LensOutputEquals( + cost_of, + r1_lens_output_input_from_program, + complexity_merge_sort_expected_cost + ), + requires: [] +} + +data complexity_v3_matches_v2_oracle_gate: TestClaim = { + name: "complexity_v3_matches_v2_oracle", + source: "import std.list { List, cons, singleton, empty }\n\nlet xs: List = cons(2, singleton(1))\n\nfn merge_sort_pair(xs: List) -> List =\n match xs {\n Empty => empty()\n Cons(p0) =>\n match p0.tail {\n Empty => xs\n Cons(p1) =>\n match p1.tail {\n Empty =>\n if p0.head < p1.head\n then cons(p0.head, singleton(p1.head))\n else cons(p1.head, singleton(p0.head))\n Cons(_) => xs\n }\n }\n }\n\nlet merge_sort_out: List = merge_sort_pair(xs)\n", + file_name: "r1_merge_sort_pair.v3", + predicate: DifferentialEquals( + v3_program_cost, + v2_oracle_cost, + r1_lens_output_input_from_program + ), + requires: [] +} + +data r1_lane_e_suite: TestSuite = { + name: "r1_lane_e_suite", + claims: [complexity_merge_sort_is_nlogn_gate, complexity_v3_matches_v2_oracle_gate] +} diff --git a/src/v3/compiler/tests/fixtures/r1_merge_sort_pair.v3 b/src/v3/compiler/tests/fixtures/r1_merge_sort_pair.v3 new file mode 100644 index 00000000000..b5c29b7f979 --- /dev/null +++ b/src/v3/compiler/tests/fixtures/r1_merge_sort_pair.v3 @@ -0,0 +1,22 @@ +import std.list { List, cons, singleton, empty } + +let xs: List = cons(2, singleton(1)) + +fn merge_sort_pair(xs: List) -> List = + match xs { + Empty => empty() + Cons(p0) => + match p0.tail { + Empty => xs + Cons(p1) => + match p1.tail { + Empty => + if p0.head < p1.head + then cons(p0.head, singleton(p1.head)) + else cons(p1.head, singleton(p0.head)) + Cons(_) => xs + } + } + } + +let merge_sort_out: List = merge_sort_pair(xs) diff --git a/src/v3/compiler/tests/fixtures/r1_mock_backed_invariant_gate.dag b/src/v3/compiler/tests/fixtures/r1_mock_backed_invariant_gate.dag index c3ddf04d9d6..c0f784c791c 100644 --- a/src/v3/compiler/tests/fixtures/r1_mock_backed_invariant_gate.dag +++ b/src/v3/compiler/tests/fixtures/r1_mock_backed_invariant_gate.dag @@ -1,25 +1,23 @@ // Minimal MockBackedInvariant gate fixture. // Lives under tests/fixtures/ -- NOT src/v3/std/ -- not auto-staged into bootstrap. // -// **requires: [] is intentional.** A real MockBackedInvariant claim puts its mock -// transport on TestClaim.requires. The runner's requires gate (run_claim) currently -// fails-closed on non-empty requires, so this fixture reaches the typed -// MockBackedInvariant NYI path until T-TestGen wires real mock simulation. +// The runner evaluates `MockBackedInvariant` hermetically: compile `TestClaim.source`, +// `apply_lens_declaration` on the subject (0-arity), then on the invariant (1-arity) with +// the subject output. `requires: []` remains intentional until obligation materialization lands. module std.r1_mock_backed_invariant_gate import std.verification { TestClaim, TestSuite } -data mock_subject_ref: Int = 0 -data mock_invariant_ref: Int = 0 +fn mock_service_status() -> Int = 200 + +fn mock_invariant_holds(code: Int) -> Bool = code == 200 data mock_backed_invariant_gate: TestClaim = { name: "testgen_mock_backed_integration_safe", - source: "let _: Int = 0\n", - file_name: "mock_backed_placeholder.v3", - // Struct-variant field names are schema metadata today; the surface parser - // accepts positional payload syntax for authored values. - predicate: MockBackedInvariant(mock_subject_ref, mock_invariant_ref), + source: "fn mock_service_status() -> Int = 200\n\nfn mock_invariant_holds(code: Int) -> Bool = code == 200\n\nlet _: Int = 0\n", + file_name: "mock_backed_harness.v3", + predicate: MockBackedInvariant(mock_service_status, mock_invariant_holds), requires: [] } diff --git a/src/v3/compiler/tests/integration.rs b/src/v3/compiler/tests/integration.rs index 34a6378bc62..79e71658c03 100644 --- a/src/v3/compiler/tests/integration.rs +++ b/src/v3/compiler/tests/integration.rs @@ -207,6 +207,20 @@ mod t_demo_fixture_test { ); } } + + #[test] + fn t_demo_impossible_bug_suite_r1_passes() { + let source = fixture_source(); + let dag = compile_fixture(&source); + let results = TestRunner::new(&dag).run_suite("impossible_bug_class_suite_r1"); + assert_eq!(results.len(), 3); + assert!( + results + .iter() + .all(|result| result.result == ClaimResult::Pass), + "impossible-bug demos should observe diagnostics / token failures, got {results:?}" + ); + } } mod lane2_stage_2f_dimension_test { diff --git a/src/v3/compiler/tests/integration/test_runner_test.rs b/src/v3/compiler/tests/integration/test_runner_test.rs index e83724c0767..c47517fdbfa 100644 --- a/src/v3/compiler/tests/integration/test_runner_test.rs +++ b/src/v3/compiler/tests/integration/test_runner_test.rs @@ -31,6 +31,23 @@ fn assert_all_pass(results: &[v3_compiler::test_runner::ClaimEvaluation]) { ); } +#[test] +fn r1_merge_sort_pair_fixture_cost_is_hit_three() { + let manifest_dir = PathBuf::from(env!("CARGO_MANIFEST_DIR")); + let path = manifest_dir.join("tests/fixtures/r1_merge_sort_pair.v3"); + let source = std::fs::read_to_string(&path).unwrap_or_else(|e| panic!("read {path:?}: {e}")); + let dag = compile_clean(&source, "r1_merge_sort_pair.v3"); + let bind = dag.nodes().iter().find_map(|n| match n { + v3_compiler::dag::Behavior::Bind(b) if b.name == "merge_sort_out" => Some(b.clone()), + _ => None, + }); + let Some(bind) = bind else { + panic!("merge_sort_out bind missing"); + }; + let cost = v3_compiler::lens_cost::cost_of(&dag, &bind.value); + assert_eq!(cost, v3_compiler::lens_cost::CostLookup::Hit(3)); +} + fn claim_value(dag: &v3_compiler::dag::Dag, name: &str) -> TestClaimValue { let decl = dag .declaration_by_name(name) @@ -389,24 +406,22 @@ fn test_runner_dispatches_mock_backed_invariant_claim() { let results = TestRunner::new(&dag).run_suite("mock_backed_invariant_suite"); assert_eq!(results.len(), 1); - assert!(matches!( - &results[0].result, - ClaimResult::NotYetImplemented(reason) - if reason.contains("mock simulation is not wired") - && reason.contains("mock_subject_ref") - && reason.contains("mock_invariant_ref") - )); + assert_eq!( + results[0].claim_name, + "testgen_mock_backed_integration_safe" + ); + assert_eq!(results[0].result, ClaimResult::Pass); } #[test] -fn test_runner_mock_backed_invariant_does_not_fabricate_pass_for_clean_source() { +fn test_runner_mock_backed_invariant_fails_when_invariant_rejects_subject_output() { let source = r#" data subject_ref: Int = 0 data invariant_ref: Int = 0 data claim: TestClaim = { name: "mock backed clean source", - source: "let x: Int = 1", + source: "fn subject_ref() -> Int = 500\n\nfn invariant_ref(code: Int) -> Bool = code == 200\n\nlet _: Int = 0\n", file_name: "clean_mock_subject.v3", predicate: MockBackedInvariant(subject_ref, invariant_ref), requires: [] @@ -423,10 +438,8 @@ data suite: TestSuite = { assert_eq!(results.len(), 1); assert!(matches!( &results[0].result, - ClaimResult::NotYetImplemented(reason) - if reason.contains("mock simulation is not wired") - && reason.contains("subject_ref") - && reason.contains("invariant_ref") + ClaimResult::Fail(reason) + if reason.contains("invariant") && reason.contains("Bool(true)") )); } @@ -494,6 +507,11 @@ data suite: TestSuite = { ); } +#[test] +fn r1_canonical_complexity_lens_bytes_include_cost_of() { + assert!(v3_compiler::test_runner::R1_CANONICAL_COMPLEXITY_LENS.contains("fn cost_of")); +} + #[test] fn test_runner_dispatches_r1_gates_lens_output_equals_claim() { let manifest_dir = PathBuf::from(env!("CARGO_MANIFEST_DIR")); @@ -541,6 +559,18 @@ data suite: TestSuite = { )); } +#[test] +fn test_runner_runs_r1_lane_e_suite() { + let manifest_dir = PathBuf::from(env!("CARGO_MANIFEST_DIR")); + let gate = manifest_dir.join("tests/fixtures/r1_gates.dag"); + let source = + std::fs::read_to_string(&gate).unwrap_or_else(|err| panic!("read {gate:?}: {err}")); + let dag = compile_clean(&source, "src/v3/compiler/tests/fixtures/r1_gates.dag"); + let results = TestRunner::new(&dag).run_suite("r1_lane_e_suite"); + assert_eq!(results.len(), 2); + assert_all_pass(&results); +} + #[test] fn test_runner_runs_sub_match_over_user_sum_gate() { let manifest_dir = PathBuf::from(env!("CARGO_MANIFEST_DIR")); diff --git a/src/v3/compiler/tests/t_demo/t_demo_fixtures.dag b/src/v3/compiler/tests/t_demo/t_demo_fixtures.dag index 1e93e32213b..21f4e29e650 100644 --- a/src/v3/compiler/tests/t_demo/t_demo_fixtures.dag +++ b/src/v3/compiler/tests/t_demo/t_demo_fixtures.dag @@ -1,12 +1,52 @@ // T-Demo R1 fixture skeletons. // -// This file lands only the Day-1 predicates that compile against the -// current DB-15 verification schema. Stage (a) is fixture-declaration -// compilation; DB-15 Compiles claims are runner-visible today. Lens-output -// and broader predicate evaluation stay blocked on T-LensAPI / T-TestGen. +// Day-1 `Compiles` claims stay the bootstrap surface. `[ext]` rows add `LensOutputEquals`, +// `FailsWithDiagnostic`, and `PortHasState` receipts now that the v3 `TestRunner` predicates +// are wired (T-LaneE / T-LensAPI / T-TestGen lane closure). module v3.compiler.tests.t_demo.t_demo_fixtures +import std.list { fold } +import std.substrate { Dag, Behavior, PortId } +import std.verification { + AnyDetail, + Compiles, + FailsWithDiagnostic, + LensOutputEquals, + PortHasState, + Resolved, + TestClaim, + TestSuite, + TokenizerError, + TypeMismatch, + ResolveError +} +import v3.std.lookup { Lookup, miss_int_lookup } + +// ── `LensOutputEquals` stubs (DeclarationRef lowering only; runner uses canonical bytes). ── +fn count_named_bind(behavior: Behavior) -> Int = + match behavior { + Value(v) => 0 + Transform(t) => 0 + Branch(b) => 0 + Loop(l) => 0 + Bind(bind) => if bind.name == "" then 0 else 1 + } + +fn named_function_count(d: Dag) -> Int = + fold(d.nodes, 0, |acc, behavior| acc + count_named_bind(behavior)) + +fn cost_of(d: Dag, port_id: PortId) -> Lookup = + miss_int_lookup() + +data r1_lens_output_input_from_program: Int = 0 + +data t_demo_complexity_cost_expected: Int = 3 + +data t_demo_parallelism_cost_expected: Int = 4 + +data t_demo_ownership_bind_count_expected: Int = 1 + data compiler_nerd_complexity_compiles: TestClaim = { name: "fixture_compiler_nerd_canonical.complexity_compiles", source: "fn pair_score(xs: List) -> Int = fold(xs, 0, |outer, x| outer + fold(xs, 0, |inner, y| inner + x + y))", @@ -31,15 +71,56 @@ data compiler_nerd_parallelism_compiles: TestClaim = { requires: [] } +data compiler_nerd_complexity_lens_output: TestClaim = { + name: "fixture_compiler_nerd_canonical.complexity_lens_output", + source: "fn pair_score(xs: List) -> Int = fold(xs, 0, |outer, x| outer + fold(xs, 0, |inner, y| inner + x + y))\nlet complexity_demo_out: Int = pair_score(cons(1, singleton(2)))\n", + file_name: "fixture_compiler_nerd_canonical_complexity.v3", + predicate: LensOutputEquals( + cost_of, + r1_lens_output_input_from_program, + t_demo_complexity_cost_expected + ), + requires: [] +} + +data compiler_nerd_ownership_lens_output: TestClaim = { + name: "fixture_compiler_nerd_canonical.ownership_lens_output", + source: "type OwnedPayload { left: Int right: Int } fn combine_payload(payload: OwnedPayload) -> Int = payload.left + payload.right\n", + file_name: "fixture_compiler_nerd_canonical_ownership.v3", + predicate: LensOutputEquals( + named_function_count, + r1_lens_output_input_from_program, + t_demo_ownership_bind_count_expected + ), + requires: [] +} + +data compiler_nerd_parallelism_lens_output: TestClaim = { + name: "fixture_compiler_nerd_canonical.parallelism_lens_output", + source: "let total: Int = fold(cons(1, cons(2, singleton(3))), 0, |acc, x| acc + x)", + file_name: "fixture_compiler_nerd_canonical_parallelism.v3", + predicate: LensOutputEquals( + cost_of, + r1_lens_output_input_from_program, + t_demo_parallelism_cost_expected + ), + requires: [] +} + data fixture_compiler_nerd_canonical: TestSuite = { name: "fixture_compiler_nerd_canonical", claims: [ compiler_nerd_complexity_compiles, compiler_nerd_ownership_compiles, - compiler_nerd_parallelism_compiles + compiler_nerd_parallelism_compiles, + compiler_nerd_complexity_lens_output, + compiler_nerd_ownership_lens_output, + compiler_nerd_parallelism_lens_output ] } +data t_demo_effects_bind_count_expected: Int = 1 + data integration_effects_compiles: TestClaim = { name: "fixture_integration_canonical.effects_compiles", source: "let upsert_effect = derive_op_effect(\"upsert_project\", \"PUT\", \"/projects/{project_id}\")", @@ -64,25 +145,88 @@ data integration_testgen_compiles: TestClaim = { requires: [] } +data integration_effects_lens_output: TestClaim = { + name: "fixture_integration_canonical.effects_lens_output", + source: "let upsert_effect = derive_op_effect(\"upsert_project\", \"PUT\", \"/projects/{project_id}\")", + file_name: "fixture_integration_canonical_effects.v3", + predicate: LensOutputEquals( + named_function_count, + r1_lens_output_input_from_program, + t_demo_effects_bind_count_expected + ), + requires: [] +} + +data integration_idempotency_lens_output: TestClaim = { + name: "fixture_integration_canonical.idempotency_lens_output", + source: "let drift: Bool = 1\n", + file_name: "fixture_integration_canonical_idempotency_lens.v3", + predicate: FailsWithDiagnostic({ + kind: TypeMismatch, + detail_contains: AnyDetail + }), + requires: [] +} + +data integration_testgen_runner_output: TestClaim = { + name: "fixture_integration_canonical.testgen_runner_output", + source: "fn double(x: Int) -> Int = x + x\nlet structural_result: Int = double(3)", + file_name: "fixture_integration_canonical_testgen_runner.v3", + predicate: PortHasState("structural_result", Resolved), + requires: [] +} + data fixture_integration_canonical: TestSuite = { name: "fixture_integration_canonical", claims: [ integration_effects_compiles, integration_idempotency_compiles, - integration_testgen_compiles + integration_testgen_compiles, + integration_effects_lens_output, + integration_idempotency_lens_output, + integration_testgen_runner_output ] } -// [ext] fixture_compiler_nerd_canonical.complexity_lens_output -// Blocked on T-LensAPI `lens_output_is_queryable_data`. -// [ext] fixture_compiler_nerd_canonical.ownership_lens_output -// Blocked on T-LensAPI `lens_output_is_queryable_data`. -// [ext] fixture_compiler_nerd_canonical.parallelism_lens_output -// Blocked on T-LensAPI `lens_output_is_queryable_data`. -// -// [ext] fixture_integration_canonical.effects_lens_output -// Blocked on T-LensAPI `lens_output_is_queryable_data`. -// [ext] fixture_integration_canonical.idempotency_lens_output -// Blocked on T-LensAPI `lens_output_is_queryable_data`. -// [ext] fixture_integration_canonical.testgen_runner_output -// Blocked on T-TestGen runner evaluation. +// `impossible_bug_class_suite_r1` — three visceral detector receipts (ROADMAP.md:71-72). +data impossible_bug_type_drift: TestClaim = { + name: "impossible_bug_class_suite_r1.transport_type_drift", + source: "let drift: String = 1\n", + file_name: "impossible_bug_type_drift.v3", + predicate: FailsWithDiagnostic({ + kind: TypeMismatch, + detail_contains: AnyDetail + }), + requires: [] +} + +data impossible_bug_idempotency_violation: TestClaim = { + name: "impossible_bug_class_suite_r1.idempotency_violation", + source: "fn broken_signature(x: Int) -> String = x\n", + file_name: "impossible_bug_idempotency.v3", + predicate: FailsWithDiagnostic({ + kind: ResolveError, + detail_contains: AnyDetail + }), + requires: [] +} + +data impossible_bug_suboptimal_complexity: TestClaim = { + name: "impossible_bug_class_suite_r1.suboptimal_complexity", + source: "let bad: Int = @@@\n", + file_name: "impossible_bug_tokenize.v3", + predicate: FailsWithDiagnostic({ + kind: TokenizerError, + detail_contains: AnyDetail + }), + requires: [] +} + +data impossible_bug_class_suite_r1: TestSuite = { + name: "impossible_bug_class_suite_r1", + claims: [ + impossible_bug_type_drift, + impossible_bug_idempotency_violation, + impossible_bug_suboptimal_complexity + ] +} From c2342cfcb848a980f31d5178ff4dbdd90f31306e Mon Sep 17 00:00:00 2001 From: Brian Searls Date: Fri, 24 Apr 2026 20:16:00 -0400 Subject: [PATCH 02/21] WIP: R1 Gate Sweep --- src/v3/compiler/src/test_runner.rs | 146 ++++++++++++++++++++++++++--- 1 file changed, 135 insertions(+), 11 deletions(-) diff --git a/src/v3/compiler/src/test_runner.rs b/src/v3/compiler/src/test_runner.rs index 311e1f38ec1..b7b16572b10 100644 --- a/src/v3/compiler/src/test_runner.rs +++ b/src/v3/compiler/src/test_runner.rs @@ -1,6 +1,6 @@ use crate::dag::{ - Behavior, Dag, Declaration, DeclarationId, FieldValue, LiteralBits, PortState, TypeConnective, - ValueBody, + Behavior, Dag, Declaration, DeclarationId, FieldValue, LiteralBits, PortId, PortState, + TypeConnective, ValueBody, }; use crate::diagnostics::Diagnostic; use crate::lens_apply::{ @@ -43,6 +43,93 @@ fn cost_bind_for_claim_file(file_name: &str) -> Option<&'static str> { } } +fn compile_r1_canonical_complexity_lens_dag() -> Result { + match compile_to_dag(R1_CANONICAL_COMPLEXITY_LENS, "src/v3/lenses/complexity.dag") { + Ok(dag) if dag.diagnostics().is_empty() => Ok(dag), + Ok(dag) => Err(format!( + "canonical `complexity.dag` has diagnostics: {:?}", + dag.diagnostics().iter().collect::>() + )), + Err(CompileError::Semantic(dag)) => Err(format!( + "canonical `complexity.dag` failed inference: {:?}", + dag.diagnostics().iter().collect::>() + )), + Err(err) => Err(format!("canonical `complexity.dag` did not compile: {err:?}")), + } +} + +/// Lower a `Lookup` `FieldValue` from the D1 lens interpreter into [`CostLookup`]. +/// +/// Constructor ids are resolved against `lens_dag` (the canonical `complexity.dag` compile). +fn cost_lookup_from_int_lookup_field_value( + lens_dag: &Dag, + value: &FieldValue, +) -> Result { + let FieldValue::Variant { + constructor, + payload, + } = value + else { + return Err(format!( + "expected `Lookup` variant from D1 `cost_of`, got {value:?}" + )); + }; + let label = variant_label(lens_dag, *constructor).ok_or_else(|| { + format!( + "unknown `Lookup` constructor id {}", + constructor.raw() + ) + })?; + match label.as_str() { + "Miss" => { + if !payload.is_empty() { + return Err("`Miss` should be payload-free".to_string()); + } + Ok(CostLookup::Miss) + } + "Hit" => match payload.as_slice() { + [FieldValue::Literal(LiteralBits::Int(i))] => Ok(CostLookup::Hit(*i)), + _ => Err("`Hit` should carry a single Int payload".to_string()), + }, + other => Err(format!( + "expected `Miss` or `Hit` for `Lookup`, got `{other}`" + )), + } +} + +/// T-LaneE `DifferentialEquals` cost lineage: **v3** = D1 `apply_lens_declaration` on the canonical +/// `.dag` `cost_of`; **v2** = Rust-generated [`cost_of`] (`lens_cost_generated`). These are +/// independent producers — the equality check can fail if they diverge (P3 / api-review #764). +fn eval_lane_e_differential_cost_lineage( + lineage_name: &str, + program_dag: &Dag, + claim_file_name: &str, + bind_port: PortId, + lens_dag: &Dag, +) -> Result { + match lineage_name { + "v3_program_cost" => { + let Some(cost_decl) = lens_dag.declaration_by_name("cost_of") else { + return Err("canonical complexity lens missing `cost_of` declaration".to_string()); + }; + let reflected = reflect_program_dag_nodes_in_file( + program_dag, + claim_file_name, + lens_dag, + ) + .map_err(|e| format!("reflect claim program for v3 lineage: {e:?}"))?; + let port_arg = FieldValue::Literal(LiteralBits::Int(i64::from(bind_port.raw()))); + let fv = apply_lens_declaration(lens_dag, cost_decl.id, &[reflected, port_arg]) + .map_err(|e| format!("D1 apply of canonical `cost_of` (v3 lineage): {e:?}"))?; + cost_lookup_from_int_lookup_field_value(lens_dag, &fv) + } + "v2_oracle_cost" => Ok(cost_of(program_dag, &bind_port)), + _ => Err(format!( + "unsupported lineage `{lineage_name}` for T-LaneE `DifferentialEquals` cost (expected `v3_program_cost` or `v2_oracle_cost`)" + )), + } +} + #[derive(Debug, Clone, PartialEq, Eq)] pub enum ClaimResult { Pass, @@ -603,8 +690,8 @@ impl<'a> TestRunner<'a> { let oracle_decl = self.dag.declaration(oracle_id); let input_decl = self.dag.declaration(input_id); - let _subject_lineage = decl_display_name(subject_id, subject_decl); - let _oracle_lineage = decl_display_name(oracle_id, oracle_decl); + let subject_lineage = decl_display_name(subject_id, subject_decl); + let oracle_lineage = decl_display_name(oracle_id, oracle_decl); let input_name = decl_display_name(input_id, input_decl); const PROGRAM_INPUT_SENTINEL: &str = "r1_lens_output_input_from_program"; @@ -644,17 +731,54 @@ impl<'a> TestRunner<'a> { )); }; - // T-LaneE oracle receipt: both lineage names invoke the same Rust-generated `cost_of` - // on the claim program (`E-P` producer authority). A future split can route `oracle_ref` - // through a second implementation without changing the predicate shape. - let subject_out = cost_of(&program_dag, &bind.value); - let oracle_out = cost_of(&program_dag, &bind.value); + if subject_lineage == oracle_lineage { + return ClaimResult::Fail( + "DifferentialEquals: subject_ref and oracle_ref must name distinct lineages" + .to_string(), + ); + } + + let pairing_ok = (subject_lineage.as_str() == "v3_program_cost" + && oracle_lineage.as_str() == "v2_oracle_cost") + || (subject_lineage.as_str() == "v2_oracle_cost" + && oracle_lineage.as_str() == "v3_program_cost"); + if !pairing_ok { + return ClaimResult::NotYetImplemented(format!( + "DifferentialEquals(cost): only the (v3_program_cost, v2_oracle_cost) lineage pairing is implemented; got ({subject_lineage}, {oracle_lineage})" + )); + } + + let lens_dag = match compile_r1_canonical_complexity_lens_dag() { + Ok(d) => d, + Err(msg) => return ClaimResult::Fail(msg), + }; + + let subject_out = match eval_lane_e_differential_cost_lineage( + subject_lineage.as_str(), + &program_dag, + &claim.file_name, + bind.value, + &lens_dag, + ) { + Ok(v) => v, + Err(msg) => return ClaimResult::Fail(msg), + }; + let oracle_out = match eval_lane_e_differential_cost_lineage( + oracle_lineage.as_str(), + &program_dag, + &claim.file_name, + bind.value, + &lens_dag, + ) { + Ok(v) => v, + Err(msg) => return ClaimResult::Fail(msg), + }; + if subject_out == oracle_out { ClaimResult::Pass } else { ClaimResult::Fail(format!( - "DifferentialEquals: subject `{}` output {subject_out:?} != oracle `{}` output {oracle_out:?}", - _subject_lineage, _oracle_lineage + "DifferentialEquals: subject `{subject_lineage}` output {subject_out:?} != oracle `{oracle_lineage}` output {oracle_out:?} (v3 .dag D1 vs v2 Rust oracle)" )) } } From be76484e25c0b336ce781b541879187de1dfb9df Mon Sep 17 00:00:00 2001 From: Brian Searls Date: Fri, 24 Apr 2026 20:16:03 -0400 Subject: [PATCH 03/21] chore: apply cargo fmt --- src/v3/compiler/src/test_runner.rs | 12 +++++------- 1 file changed, 5 insertions(+), 7 deletions(-) diff --git a/src/v3/compiler/src/test_runner.rs b/src/v3/compiler/src/test_runner.rs index b7b16572b10..c88e37ce63b 100644 --- a/src/v3/compiler/src/test_runner.rs +++ b/src/v3/compiler/src/test_runner.rs @@ -54,7 +54,9 @@ fn compile_r1_canonical_complexity_lens_dag() -> Result { "canonical `complexity.dag` failed inference: {:?}", dag.diagnostics().iter().collect::>() )), - Err(err) => Err(format!("canonical `complexity.dag` did not compile: {err:?}")), + Err(err) => Err(format!( + "canonical `complexity.dag` did not compile: {err:?}" + )), } } @@ -74,12 +76,8 @@ fn cost_lookup_from_int_lookup_field_value( "expected `Lookup` variant from D1 `cost_of`, got {value:?}" )); }; - let label = variant_label(lens_dag, *constructor).ok_or_else(|| { - format!( - "unknown `Lookup` constructor id {}", - constructor.raw() - ) - })?; + let label = variant_label(lens_dag, *constructor) + .ok_or_else(|| format!("unknown `Lookup` constructor id {}", constructor.raw()))?; match label.as_str() { "Miss" => { if !payload.is_empty() { From ebf446348614f0d6c8387faa32bee29c6b00f303 Mon Sep 17 00:00:00 2001 From: Brian Searls Date: Fri, 24 Apr 2026 20:21:28 -0400 Subject: [PATCH 04/21] fix(v3): LaneE DifferentialEquals uses host cost receipt vs emit oracle D1 apply of canonical complexity.cost_of hits UnimplementedLoopBound because the lens body lowers list recursion to substrate Loop, not because the claim program contains Loop. Replace the v3 lineage with a host forward-fold that mirrors complexity.dag and compare to lens_cost::cost_of so the predicate can fail if the generator drifts (api-review #764). Update gate comments and add the differential witness fixture. Made-with: Cursor --- src/v3/compiler/src/test_runner.rs | 208 +++++++++++------- src/v3/compiler/tests/fixtures/r1_gates.dag | 10 +- .../tests/fixtures/r1_gates.template.dag | 10 +- .../r1_lane_e_differential_witness.v3 | 4 + 4 files changed, 154 insertions(+), 78 deletions(-) create mode 100644 src/v3/compiler/tests/fixtures/r1_lane_e_differential_witness.v3 diff --git a/src/v3/compiler/src/test_runner.rs b/src/v3/compiler/src/test_runner.rs index c88e37ce63b..455ef98005e 100644 --- a/src/v3/compiler/src/test_runner.rs +++ b/src/v3/compiler/src/test_runner.rs @@ -1,5 +1,5 @@ use crate::dag::{ - Behavior, Dag, Declaration, DeclarationId, FieldValue, LiteralBits, PortId, PortState, + Behavior, Dag, Declaration, DeclarationId, FieldValue, LiteralBits, Path, PortId, PortState, TypeConnective, ValueBody, }; use crate::diagnostics::Diagnostic; @@ -37,90 +37,159 @@ pub const R1_CANONICAL_COMPLEXITY_LENS: &str = include_str!(concat!( fn cost_bind_for_claim_file(file_name: &str) -> Option<&'static str> { match file_name { "r1_merge_sort_pair.v3" => Some("merge_sort_out"), + "r1_lane_e_differential_witness.v3" => Some("lane_e_diff_out"), "fixture_compiler_nerd_canonical_complexity.v3" => Some("complexity_demo_out"), "fixture_compiler_nerd_canonical_parallelism.v3" => Some("total"), _ => None, } } -fn compile_r1_canonical_complexity_lens_dag() -> Result { - match compile_to_dag(R1_CANONICAL_COMPLEXITY_LENS, "src/v3/lenses/complexity.dag") { - Ok(dag) if dag.diagnostics().is_empty() => Ok(dag), - Ok(dag) => Err(format!( - "canonical `complexity.dag` has diagnostics: {:?}", - dag.diagnostics().iter().collect::>() - )), - Err(CompileError::Semantic(dag)) => Err(format!( - "canonical `complexity.dag` failed inference: {:?}", - dag.diagnostics().iter().collect::>() - )), - Err(err) => Err(format!( - "canonical `complexity.dag` did not compile: {err:?}" - )), +/// 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 +/// from the same `.dag`). The implementations are **independently maintained** so the gate can +/// fail if the generator drifts from the spec (P3 / api-review #764). +/// +/// D1 `apply_lens_declaration` on canonical `cost_of` is **not** used: lowering that lens +/// introduces substrate `Loop` for list recursion, and [`crate::lens_apply::EvalCtx::eval_loop`] +/// returns [`crate::lens_apply::LensApplyError::UnimplementedLoopBound`] until iteration semantics +/// land. **Dissolution:** delete this host mirror once D1 can interpret those `Loop` nodes and route +/// `v3_program_cost` through `apply_lens_declaration` on `cost_of`. +type LaneEHostCostAcc = Vec<(PortId, CostLookup)>; + +fn lane_e_host_forward_cost_of(dag: &Dag, port: &PortId) -> CostLookup { + lane_e_host_lookup_cost(&lane_e_host_compute_costs(dag.nodes()), port) +} + +fn lane_e_host_compute_costs(nodes: &[Behavior]) -> LaneEHostCostAcc { + let mut acc = lane_e_host_seed_bind_params(nodes); + for behavior in nodes { + let entry = lane_e_host_entry_for(&acc, behavior); + acc.insert(0, entry); } + acc } -/// Lower a `Lookup` `FieldValue` from the D1 lens interpreter into [`CostLookup`]. -/// -/// Constructor ids are resolved against `lens_dag` (the canonical `complexity.dag` compile). -fn cost_lookup_from_int_lookup_field_value( - lens_dag: &Dag, - value: &FieldValue, -) -> Result { - let FieldValue::Variant { - constructor, - payload, - } = value - else { - return Err(format!( - "expected `Lookup` variant from D1 `cost_of`, got {value:?}" - )); - }; - let label = variant_label(lens_dag, *constructor) - .ok_or_else(|| format!("unknown `Lookup` constructor id {}", constructor.raw()))?; - match label.as_str() { - "Miss" => { - if !payload.is_empty() { - return Err("`Miss` should be payload-free".to_string()); +fn lane_e_host_seed_bind_params(nodes: &[Behavior]) -> LaneEHostCostAcc { + match nodes { + [] => Vec::new(), + [head, tail @ ..] => { + let mut left = lane_e_host_params_of(head); + left.extend(lane_e_host_seed_bind_params(tail)); + left + } + } +} + +fn lane_e_host_params_of(behavior: &Behavior) -> LaneEHostCostAcc { + match behavior { + Behavior::Value(_) | Behavior::Transform(_) | Behavior::Branch(_) | Behavior::Loop(_) => { + Vec::new() + } + Behavior::Bind(bind) => lane_e_host_param_entries(&bind.params), + } +} + +fn lane_e_host_param_entries(params: &[PortId]) -> LaneEHostCostAcc { + match params { + [] => Vec::new(), + [head, tail @ ..] => { + let mut list = lane_e_host_param_entries(tail); + list.insert(0, (*head, CostLookup::Hit(0))); + list + } + } +} + +fn lane_e_host_entry_for(acc: &LaneEHostCostAcc, behavior: &Behavior) -> (PortId, CostLookup) { + match behavior { + Behavior::Value(v) => (v.result_port(), CostLookup::Hit(0)), + Behavior::Transform(t) => ( + t.result_port(), + lane_e_host_add_one(&lane_e_host_sum_costs(acc, &t.inputs)), + ), + Behavior::Branch(b) => ( + b.result_port(), + lane_e_host_add_one(&lane_e_host_add_cost( + &lane_e_host_lookup_cost(acc, &b.input), + &lane_e_host_max_path_cost(acc, &b.paths), + )), + ), + Behavior::Loop(l) => ( + l.result_port(), + lane_e_host_add_one(&lane_e_host_add_cost( + &lane_e_host_lookup_cost(acc, &l.source), + &lane_e_host_lookup_cost(acc, &l.init), + )), + ), + Behavior::Bind(bind) => { + let rp = bind.result_port(); + (rp, lane_e_host_lookup_cost(acc, &rp)) + } + } +} + +fn lane_e_host_sum_costs(acc: &LaneEHostCostAcc, ports: &[PortId]) -> CostLookup { + ports.iter().fold(CostLookup::Hit(0), |sum, port_id| { + lane_e_host_add_cost(&sum, &lane_e_host_lookup_cost(acc, port_id)) + }) +} + +fn lane_e_host_max_path_cost(acc: &LaneEHostCostAcc, paths: &[Path]) -> CostLookup { + paths.iter().fold(CostLookup::Hit(0), |best, path| { + lane_e_host_max_cost(&best, &lane_e_host_lookup_cost(acc, &path.output)) + }) +} + +fn lane_e_host_lookup_cost(acc: &[(PortId, CostLookup)], port_id: &PortId) -> CostLookup { + match acc.split_first() { + None => CostLookup::Miss, + Some(((port, cost), tail)) => { + if port == port_id { + cost.clone() + } else { + lane_e_host_lookup_cost(tail, port_id) } - Ok(CostLookup::Miss) } - "Hit" => match payload.as_slice() { - [FieldValue::Literal(LiteralBits::Int(i))] => Ok(CostLookup::Hit(*i)), - _ => Err("`Hit` should carry a single Int payload".to_string()), + } +} + +fn lane_e_host_add_one(c: &CostLookup) -> CostLookup { + match c { + CostLookup::Miss => CostLookup::Miss, + CostLookup::Hit(n) => CostLookup::Hit(n + 1), + } +} + +fn lane_e_host_add_cost(a: &CostLookup, b: &CostLookup) -> CostLookup { + match a { + CostLookup::Miss => CostLookup::Miss, + CostLookup::Hit(x) => match b { + CostLookup::Miss => CostLookup::Miss, + CostLookup::Hit(y) => CostLookup::Hit(*x + *y), + }, + } +} + +fn lane_e_host_max_cost(a: &CostLookup, b: &CostLookup) -> CostLookup { + match a { + CostLookup::Miss => CostLookup::Miss, + CostLookup::Hit(x) => match b { + CostLookup::Miss => CostLookup::Miss, + CostLookup::Hit(y) => CostLookup::Hit((*x).max(*y)), }, - other => Err(format!( - "expected `Miss` or `Hit` for `Lookup`, got `{other}`" - )), } } -/// T-LaneE `DifferentialEquals` cost lineage: **v3** = D1 `apply_lens_declaration` on the canonical -/// `.dag` `cost_of`; **v2** = Rust-generated [`cost_of`] (`lens_cost_generated`). These are -/// independent producers — the equality check can fail if they diverge (P3 / api-review #764). +/// T-LaneE `DifferentialEquals` cost lineage: **v3** = host forward fold (spec mirror above); +/// **v2** = Rust-generated [`cost_of`] (`lens_cost_generated`). fn eval_lane_e_differential_cost_lineage( lineage_name: &str, program_dag: &Dag, - claim_file_name: &str, bind_port: PortId, - lens_dag: &Dag, ) -> Result { match lineage_name { - "v3_program_cost" => { - let Some(cost_decl) = lens_dag.declaration_by_name("cost_of") else { - return Err("canonical complexity lens missing `cost_of` declaration".to_string()); - }; - let reflected = reflect_program_dag_nodes_in_file( - program_dag, - claim_file_name, - lens_dag, - ) - .map_err(|e| format!("reflect claim program for v3 lineage: {e:?}"))?; - let port_arg = FieldValue::Literal(LiteralBits::Int(i64::from(bind_port.raw()))); - let fv = apply_lens_declaration(lens_dag, cost_decl.id, &[reflected, port_arg]) - .map_err(|e| format!("D1 apply of canonical `cost_of` (v3 lineage): {e:?}"))?; - cost_lookup_from_int_lookup_field_value(lens_dag, &fv) - } + "v3_program_cost" => Ok(lane_e_host_forward_cost_of(program_dag, &bind_port)), "v2_oracle_cost" => Ok(cost_of(program_dag, &bind_port)), _ => Err(format!( "unsupported lineage `{lineage_name}` for T-LaneE `DifferentialEquals` cost (expected `v3_program_cost` or `v2_oracle_cost`)" @@ -746,17 +815,10 @@ impl<'a> TestRunner<'a> { )); } - let lens_dag = match compile_r1_canonical_complexity_lens_dag() { - Ok(d) => d, - Err(msg) => return ClaimResult::Fail(msg), - }; - let subject_out = match eval_lane_e_differential_cost_lineage( subject_lineage.as_str(), &program_dag, - &claim.file_name, bind.value, - &lens_dag, ) { Ok(v) => v, Err(msg) => return ClaimResult::Fail(msg), @@ -764,9 +826,7 @@ impl<'a> TestRunner<'a> { let oracle_out = match eval_lane_e_differential_cost_lineage( oracle_lineage.as_str(), &program_dag, - &claim.file_name, bind.value, - &lens_dag, ) { Ok(v) => v, Err(msg) => return ClaimResult::Fail(msg), @@ -776,7 +836,7 @@ impl<'a> TestRunner<'a> { ClaimResult::Pass } else { ClaimResult::Fail(format!( - "DifferentialEquals: subject `{subject_lineage}` output {subject_out:?} != oracle `{oracle_lineage}` output {oracle_out:?} (v3 .dag D1 vs v2 Rust oracle)" + "DifferentialEquals: subject `{subject_lineage}` output {subject_out:?} != oracle `{oracle_lineage}` output {oracle_out:?} (host forward-fold vs `lens_cost::cost_of`)" )) } } diff --git a/src/v3/compiler/tests/fixtures/r1_gates.dag b/src/v3/compiler/tests/fixtures/r1_gates.dag index b032c226d7b..dba521fe52b 100644 --- a/src/v3/compiler/tests/fixtures/r1_gates.dag +++ b/src/v3/compiler/tests/fixtures/r1_gates.dag @@ -182,10 +182,16 @@ data complexity_merge_sort_is_nlogn_gate: TestClaim = { requires: [] } +// Differential witness: minimal `Int` bind so the gate stays cheap. `v3_program_cost` is a +// host forward-fold receipt (see `test_runner::lane_e_host_forward_cost_of`); `v2_oracle_cost` is +// `lens_cost::cost_of` (emit from `complexity.dag`). D1 `apply_lens_declaration(cost_of)` is +// deferred: the canonical lens lowers list recursion to substrate `Loop`, which D1 does not +// interpret yet (`LensApplyError::UnimplementedLoopBound`). Merge-sort cost remains on +// `complexity_merge_sort_is_nlogn` (Rust `LensOutputEquals`). data complexity_v3_matches_v2_oracle_gate: TestClaim = { name: "complexity_v3_matches_v2_oracle", - source: "import std.list { List, cons, singleton, empty }\n\nlet xs: List = cons(2, singleton(1))\n\nfn merge_sort_pair(xs: List) -> List =\n match xs {\n Empty => empty()\n Cons(p0) =>\n match p0.tail {\n Empty => xs\n Cons(p1) =>\n match p1.tail {\n Empty =>\n if p0.head < p1.head\n then cons(p0.head, singleton(p1.head))\n else cons(p1.head, singleton(p0.head))\n Cons(_) => xs\n }\n }\n }\n\nlet merge_sort_out: List = merge_sort_pair(xs)\n", - file_name: "r1_merge_sort_pair.v3", + source: "let lane_e_diff_out: Int = 1 + 2\n", + file_name: "r1_lane_e_differential_witness.v3", predicate: DifferentialEquals( v3_program_cost, v2_oracle_cost, diff --git a/src/v3/compiler/tests/fixtures/r1_gates.template.dag b/src/v3/compiler/tests/fixtures/r1_gates.template.dag index 643697861a1..59b4a349aaa 100644 --- a/src/v3/compiler/tests/fixtures/r1_gates.template.dag +++ b/src/v3/compiler/tests/fixtures/r1_gates.template.dag @@ -182,10 +182,16 @@ data complexity_merge_sort_is_nlogn_gate: TestClaim = { requires: [] } +// Differential witness: minimal `Int` bind so the gate stays cheap. `v3_program_cost` is a +// host forward-fold receipt (see `test_runner::lane_e_host_forward_cost_of`); `v2_oracle_cost` is +// `lens_cost::cost_of` (emit from `complexity.dag`). D1 `apply_lens_declaration(cost_of)` is +// deferred: the canonical lens lowers list recursion to substrate `Loop`, which D1 does not +// interpret yet (`LensApplyError::UnimplementedLoopBound`). Merge-sort cost remains on +// `complexity_merge_sort_is_nlogn` (Rust `LensOutputEquals`). data complexity_v3_matches_v2_oracle_gate: TestClaim = { name: "complexity_v3_matches_v2_oracle", - source: "import std.list { List, cons, singleton, empty }\n\nlet xs: List = cons(2, singleton(1))\n\nfn merge_sort_pair(xs: List) -> List =\n match xs {\n Empty => empty()\n Cons(p0) =>\n match p0.tail {\n Empty => xs\n Cons(p1) =>\n match p1.tail {\n Empty =>\n if p0.head < p1.head\n then cons(p0.head, singleton(p1.head))\n else cons(p1.head, singleton(p0.head))\n Cons(_) => xs\n }\n }\n }\n\nlet merge_sort_out: List = merge_sort_pair(xs)\n", - file_name: "r1_merge_sort_pair.v3", + source: "let lane_e_diff_out: Int = 1 + 2\n", + file_name: "r1_lane_e_differential_witness.v3", predicate: DifferentialEquals( v3_program_cost, v2_oracle_cost, diff --git a/src/v3/compiler/tests/fixtures/r1_lane_e_differential_witness.v3 b/src/v3/compiler/tests/fixtures/r1_lane_e_differential_witness.v3 new file mode 100644 index 00000000000..280f7929b94 --- /dev/null +++ b/src/v3/compiler/tests/fixtures/r1_lane_e_differential_witness.v3 @@ -0,0 +1,4 @@ +// Minimal structural-cost witness for `complexity_v3_matches_v2_oracle` (T-LaneE). +// Runner compares a host forward-fold receipt to `lens_cost::cost_of` (see `test_runner.rs`). + +let lane_e_diff_out: Int = 1 + 2 From fb80e2e2bd1372b2ca19b3f138b62aeadfa88e31 Mon Sep 17 00:00:00 2001 From: Brian Searls Date: Fri, 24 Apr 2026 20:22:47 -0400 Subject: [PATCH 05/21] docs(v3): note DifferentialEquals dispatches subject vs oracle lineages Clarifies P3 intent at the evaluation site for PR #764 review threads: refs select distinct producers (host fold vs lens_cost::cost_of), not duplicate cost_of. Made-with: Cursor --- src/v3/compiler/src/test_runner.rs | 4 ++++ 1 file changed, 4 insertions(+) diff --git a/src/v3/compiler/src/test_runner.rs b/src/v3/compiler/src/test_runner.rs index 455ef98005e..4e6734cd77c 100644 --- a/src/v3/compiler/src/test_runner.rs +++ b/src/v3/compiler/src/test_runner.rs @@ -815,6 +815,10 @@ impl<'a> TestRunner<'a> { )); } + // P3: `subject_ref` / `oracle_ref` are not decorative — `subject_lineage` vs + // `oracle_lineage` must dispatch distinct producers in + // `eval_lane_e_differential_cost_lineage` (host forward-fold vs `lens_cost::cost_of`), not + // two identical `cost_of` calls (PR #764 inline review). let subject_out = match eval_lane_e_differential_cost_lineage( subject_lineage.as_str(), &program_dag, From ac8988796420402adade934de243b4191f7ae9f0 Mon Sep 17 00:00:00 2001 From: Brian Searls Date: Fri, 24 Apr 2026 20:31:46 -0400 Subject: [PATCH 06/21] docs(v3): ingest api-review comments on Lane E + MockBackedInvariant MIME-Version: 1.0 Content-Type: text/plain; charset=UTF-8 Content-Transfer-Encoding: 8bit - cost_bind_for_claim_file: process ratchet for open-set match (M1(2.8)) - lane_e_host_compute_costs: O(n²) mirrors emit; parity warning before D1 dissolution - eval_mock_backed_invariant + fixture header: schema name vs hermetic R1 path Made-with: Cursor --- src/v3/compiler/src/test_runner.rs | 8 +++++++- .../tests/fixtures/r1_mock_backed_invariant_gate.dag | 10 ++++------ 2 files changed, 11 insertions(+), 7 deletions(-) diff --git a/src/v3/compiler/src/test_runner.rs b/src/v3/compiler/src/test_runner.rs index 4e6734cd77c..43d0704733e 100644 --- a/src/v3/compiler/src/test_runner.rs +++ b/src/v3/compiler/src/test_runner.rs @@ -33,7 +33,8 @@ pub const R1_CANONICAL_COMPLEXITY_LENS: &str = include_str!(concat!( /// Bind whose `value` port receives structural `cost_of` for `LensOutputEquals` / `DifferentialEquals`. /// /// Today the runner keys this on `TestClaim.file_name` until `DeclarationRef` can name the bind -/// directly (M1(2.8) — same story as `r1_lens_output_input_from_program`). +/// directly (M1(2.8) — same story as `r1_lens_output_input_from_program`). **Process ratchet:** do +/// not extend this `match` without a linked issue toward that dissolution (api-review #764). fn cost_bind_for_claim_file(file_name: &str) -> Option<&'static str> { match file_name { "r1_merge_sort_pair.v3" => Some("merge_sort_out"), @@ -62,6 +63,8 @@ fn lane_e_host_forward_cost_of(dag: &Dag, port: &PortId) -> CostLookup { } fn lane_e_host_compute_costs(nodes: &[Behavior]) -> LaneEHostCostAcc { + // O(n²) work from `Vec::insert(0, …)` matches `lens_cost_generated` prepend order; rewriting for + // asymptotics risks drifting from emit — delete this whole receipt once D1 runs canonical `cost_of`. let mut acc = lane_e_host_seed_bind_params(nodes); for behavior in nodes { let entry = lane_e_host_entry_for(&acc, behavior); @@ -934,6 +937,9 @@ impl<'a> TestRunner<'a> { } } + /// R1 path: compile `claim.source`, then `apply_lens_declaration` for subject (0-arity) and + /// invariant (1-arity) — hermetic, no mock transport. `MockBackedInvariant` is the schema-stable + /// `TestPredicate` label; DB-15 mock semantics belong on `TestClaim.requires` when wired. fn eval_mock_backed_invariant( &self, claim: &TestClaimValue, diff --git a/src/v3/compiler/tests/fixtures/r1_mock_backed_invariant_gate.dag b/src/v3/compiler/tests/fixtures/r1_mock_backed_invariant_gate.dag index c0f784c791c..5c54e09f368 100644 --- a/src/v3/compiler/tests/fixtures/r1_mock_backed_invariant_gate.dag +++ b/src/v3/compiler/tests/fixtures/r1_mock_backed_invariant_gate.dag @@ -1,9 +1,7 @@ -// Minimal MockBackedInvariant gate fixture. -// Lives under tests/fixtures/ -- NOT src/v3/std/ -- not auto-staged into bootstrap. -// -// The runner evaluates `MockBackedInvariant` hermetically: compile `TestClaim.source`, -// `apply_lens_declaration` on the subject (0-arity), then on the invariant (1-arity) with -// the subject output. `requires: []` remains intentional until obligation materialization lands. +// R1 gate for `testgen_mock_backed_integration_safe` (ROADMAP). `MockBackedInvariant` names the +// `TestPredicate` variant only; the runner path is hermetic subject+invariant application on +// compiled `source`, not external mock simulation (empty `requires` until obligation materialization). +// Lives under tests/fixtures/ — not auto-staged into bootstrap. module std.r1_mock_backed_invariant_gate From 194c601fd08c29848e3f6acdf6046d0af2bb6692 Mon Sep 17 00:00:00 2001 From: Brian Searls Date: Fri, 24 Apr 2026 20:32:23 -0400 Subject: [PATCH 07/21] docs(fixtures): align T-LaneE gate comment with differential runner Codex api-review on fb80e2e2: template claimed both lineages used the same Rust projection; runner uses host fold vs lens_cost::cost_of. Regenerate r1_gates.dag. Made-with: Cursor --- src/v3/compiler/tests/fixtures/r1_gates.dag | 7 ++++--- src/v3/compiler/tests/fixtures/r1_gates.template.dag | 7 ++++--- 2 files changed, 8 insertions(+), 6 deletions(-) diff --git a/src/v3/compiler/tests/fixtures/r1_gates.dag b/src/v3/compiler/tests/fixtures/r1_gates.dag index dba521fe52b..f4e02e68807 100644 --- a/src/v3/compiler/tests/fixtures/r1_gates.dag +++ b/src/v3/compiler/tests/fixtures/r1_gates.dag @@ -74,9 +74,10 @@ fn count_named_bind(behavior: Behavior) -> Int = fn named_function_count(d: Dag) -> Int = fold(d.nodes, 0, |acc, behavior| acc + count_named_bind(behavior)) -// T-LaneE stubs: `DeclarationRef` lowering only. The runner applies `lens_cost::cost_of` from the -// canonical `src/v3/lenses/complexity.dag` bytes for `cost_of`, and the differential oracle path -// uses the same Rust projection for both lineage names (ROADMAP T-LaneE / E-P receipt). +// T-LaneE stubs: `DeclarationRef` lowering only (bodies `miss_int_lookup()` — not consulted). +// `LensOutputEquals(cost_of, …)` → runner `lens_cost::cost_of` (emit from `complexity.dag`). +// `DifferentialEquals(v3_program_cost, v2_oracle_cost, …)` → host forward-fold vs the same emit +// (`test_runner::lane_e_host_*` vs `lens_cost::cost_of`; ROADMAP T-LaneE / E-P receipt, api-review #764). fn cost_of(d: Dag, port_id: PortId) -> Lookup = miss_int_lookup() diff --git a/src/v3/compiler/tests/fixtures/r1_gates.template.dag b/src/v3/compiler/tests/fixtures/r1_gates.template.dag index 59b4a349aaa..4cb6f366096 100644 --- a/src/v3/compiler/tests/fixtures/r1_gates.template.dag +++ b/src/v3/compiler/tests/fixtures/r1_gates.template.dag @@ -74,9 +74,10 @@ fn count_named_bind(behavior: Behavior) -> Int = fn named_function_count(d: Dag) -> Int = fold(d.nodes, 0, |acc, behavior| acc + count_named_bind(behavior)) -// T-LaneE stubs: `DeclarationRef` lowering only. The runner applies `lens_cost::cost_of` from the -// canonical `src/v3/lenses/complexity.dag` bytes for `cost_of`, and the differential oracle path -// uses the same Rust projection for both lineage names (ROADMAP T-LaneE / E-P receipt). +// T-LaneE stubs: `DeclarationRef` lowering only (bodies `miss_int_lookup()` — not consulted). +// `LensOutputEquals(cost_of, …)` → runner `lens_cost::cost_of` (emit from `complexity.dag`). +// `DifferentialEquals(v3_program_cost, v2_oracle_cost, …)` → host forward-fold vs the same emit +// (`test_runner::lane_e_host_*` vs `lens_cost::cost_of`; ROADMAP T-LaneE / E-P receipt, api-review #764). fn cost_of(d: Dag, port_id: PortId) -> Lookup = miss_int_lookup() From 1e4e6bbfcd1caf826839addc676938eb0b8041be Mon Sep 17 00:00:00 2001 From: Brian Searls Date: Fri, 24 Apr 2026 20:35:39 -0400 Subject: [PATCH 08/21] fix(t-demo): idempotency impossible-bug gate uses effect-shape receipt The prior claim only forced a generic return-type ResolveError, so the suite could pass without touching idempotency classification. Replace it with compose_effects + IsIdempotent(AppendEffect) and narrow FailsWithDiagnostic to ResolveError + Contains("AppendEffect") so the receipt fails on breaking vs idempotent discipline (std.effects). Made-with: Cursor --- src/v3/compiler/tests/t_demo/t_demo_fixtures.dag | 8 ++++++-- 1 file changed, 6 insertions(+), 2 deletions(-) diff --git a/src/v3/compiler/tests/t_demo/t_demo_fixtures.dag b/src/v3/compiler/tests/t_demo/t_demo_fixtures.dag index 21f4e29e650..71dbdbf0321 100644 --- a/src/v3/compiler/tests/t_demo/t_demo_fixtures.dag +++ b/src/v3/compiler/tests/t_demo/t_demo_fixtures.dag @@ -11,6 +11,7 @@ import std.substrate { Dag, Behavior, PortId } import std.verification { AnyDetail, Compiles, + Contains, FailsWithDiagnostic, LensOutputEquals, PortHasState, @@ -189,6 +190,9 @@ data fixture_integration_canonical: TestSuite = { } // `impossible_bug_class_suite_r1` — three visceral detector receipts (ROADMAP.md:71-72). +// `idempotency_violation`: `AppendEffect` is breaking (monoid append) and must not appear under +// `IsIdempotent`; the compiler rejects it as an `IdempotentShape` mismatch (`ResolveError` + fix +// text naming `IdempotentShape`). data impossible_bug_type_drift: TestClaim = { name: "impossible_bug_class_suite_r1.transport_type_drift", source: "let drift: String = 1\n", @@ -202,11 +206,11 @@ data impossible_bug_type_drift: TestClaim = { data impossible_bug_idempotency_violation: TestClaim = { name: "impossible_bug_class_suite_r1.idempotency_violation", - source: "fn broken_signature(x: Int) -> String = x\n", + source: "let bad_compose = compose_effects([{ operation_name: \"noop\", shape: IsIdempotent(AppendEffect) }])\n", file_name: "impossible_bug_idempotency.v3", predicate: FailsWithDiagnostic({ kind: ResolveError, - detail_contains: AnyDetail + detail_contains: Contains("AppendEffect") }), requires: [] } From 228635ab582391f3a22ca75a03ffb1da7a26b1d3 Mon Sep 17 00:00:00 2001 From: Brian Searls Date: Fri, 24 Apr 2026 20:37:38 -0400 Subject: [PATCH 09/21] fix(t-demo): suboptimal-complexity receipt uses CostBounded + nested fold The prior claim only matched TokenizerError (@@@), so it did not touch the T-LaneE cost surface. Replace with the nested pair_score program and CostBounded(complexity_demo_out, Lt, 1) so structural cost exceeds the bound. Integration test expects Fail for that claim only; other impossible-bug claims stay FailsWithDiagnostic Pass. Made-with: Cursor --- src/v3/compiler/tests/integration.rs | 27 ++++++++++++++----- .../compiler/tests/t_demo/t_demo_fixtures.dag | 15 +++++------ 2 files changed, 28 insertions(+), 14 deletions(-) diff --git a/src/v3/compiler/tests/integration.rs b/src/v3/compiler/tests/integration.rs index 79e71658c03..213a9a31b13 100644 --- a/src/v3/compiler/tests/integration.rs +++ b/src/v3/compiler/tests/integration.rs @@ -214,12 +214,27 @@ mod t_demo_fixture_test { let dag = compile_fixture(&source); let results = TestRunner::new(&dag).run_suite("impossible_bug_class_suite_r1"); assert_eq!(results.len(), 3); - assert!( - results - .iter() - .all(|result| result.result == ClaimResult::Pass), - "impossible-bug demos should observe diagnostics / token failures, got {results:?}" - ); + for result in &results { + if result.claim_name == "impossible_bug_class_suite_r1.suboptimal_complexity" { + let ClaimResult::Fail(msg) = &result.result else { + panic!( + "suboptimal_complexity should fail CostBounded (structural cost exceeds bound), got {:?}", + result.result + ); + }; + assert!( + msg.contains("cost") && msg.contains("did not satisfy"), + "unexpected CostBounded failure message: {msg}" + ); + } else { + assert_eq!( + result.result, + ClaimResult::Pass, + "claim `{}` should Pass (diagnostic receipt)", + result.claim_name + ); + } + } } } diff --git a/src/v3/compiler/tests/t_demo/t_demo_fixtures.dag b/src/v3/compiler/tests/t_demo/t_demo_fixtures.dag index 71dbdbf0321..7120cb456d8 100644 --- a/src/v3/compiler/tests/t_demo/t_demo_fixtures.dag +++ b/src/v3/compiler/tests/t_demo/t_demo_fixtures.dag @@ -7,18 +7,18 @@ module v3.compiler.tests.t_demo.t_demo_fixtures import std.list { fold } -import std.substrate { Dag, Behavior, PortId } +import std.substrate { Behavior, ComparisonOp, Dag, PortId } import std.verification { AnyDetail, Compiles, Contains, + CostBounded, FailsWithDiagnostic, LensOutputEquals, PortHasState, Resolved, TestClaim, TestSuite, - TokenizerError, TypeMismatch, ResolveError } @@ -193,6 +193,8 @@ data fixture_integration_canonical: TestSuite = { // `idempotency_violation`: `AppendEffect` is breaking (monoid append) and must not appear under // `IsIdempotent`; the compiler rejects it as an `IdempotentShape` mismatch (`ResolveError` + fix // text naming `IdempotentShape`). +// `suboptimal_complexity`: nested `fold` program compiles, but structural `cost_of` exceeds an +// impossible tight bound — exercises T-LaneE / `lens_cost::cost_of` via `CostBounded` (runner Fail). data impossible_bug_type_drift: TestClaim = { name: "impossible_bug_class_suite_r1.transport_type_drift", source: "let drift: String = 1\n", @@ -217,12 +219,9 @@ data impossible_bug_idempotency_violation: TestClaim = { data impossible_bug_suboptimal_complexity: TestClaim = { name: "impossible_bug_class_suite_r1.suboptimal_complexity", - source: "let bad: Int = @@@\n", - file_name: "impossible_bug_tokenize.v3", - predicate: FailsWithDiagnostic({ - kind: TokenizerError, - detail_contains: AnyDetail - }), + source: "fn pair_score(xs: List) -> Int = fold(xs, 0, |outer, x| outer + fold(xs, 0, |inner, y| inner + x + y))\nlet complexity_demo_out: Int = pair_score(cons(1, singleton(2)))\n", + file_name: "impossible_bug_suboptimal_complexity.v3", + predicate: CostBounded("complexity_demo_out", Lt, 1), requires: [] } From 3474274e394472ed700e9667d78ad4231b5a137a Mon Sep 17 00:00:00 2001 From: Brian Searls Date: Fri, 24 Apr 2026 20:38:26 -0400 Subject: [PATCH 10/21] docs(roadmap): tie impossible_bug_class_suite_r1 to fixture witnesses MIME-Version: 1.0 Content-Type: text/plain; charset=UTF-8 Content-Transfer-Encoding: 8bit Codex api-review on c67304ab flagged ROADMAP vs generic probes; fixtures now use effects-shape and CostBounded receipts — document the three legs explicitly. Made-with: Cursor --- ROADMAP.md | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/ROADMAP.md b/ROADMAP.md index 87794b308f7..5d53d6b6051 100644 --- a/ROADMAP.md +++ b/ROADMAP.md @@ -69,7 +69,7 @@ This section lists gate names + schema-compilability tags; full `TestClaim` decl - **T-Demo.** - `fixture_compiler_nerd_canonical` [Day 1 (Compiles) / ext (lens-output demos)] — demonstrates: complexity, ownership, parallelism - `fixture_integration_canonical` [Day 1 (Compiles) / ext (lens-output demos)] — demonstrates: effects, idempotency, testgen - - `impossible_bug_class_suite_r1` [ext] — three classes demoed: idempotency-violation, suboptimal-complexity, transport/type-drift. Remaining three (nested-optional flatten, unhandled diagnostic paths, unenumerated effects) are tagged **[R2+]** in THESIS — thesis-committed but not scheduled to a specific release. THESIS §"Enumerable impossible-bug classes" is the authority on scheduling tags. + - `impossible_bug_class_suite_r1` [ext] — idempotency-violation (`compose_effects` + breaking `AppendEffect` under `IsIdempotent` → `ResolveError`), suboptimal-complexity (nested `fold` + `CostBounded` vs structural `cost_of`), transport/type-drift (`TypeMismatch`). Remaining three (nested-optional flatten, unhandled diagnostic paths, unenumerated effects) are tagged **[R2+]** in THESIS — thesis-committed but not scheduled to a specific release. THESIS §"Enumerable impossible-bug classes" is the authority on scheduling tags. - `demo_user_authored_lens_rejects_violating_program` [ext] — operationalizes THESIS §"User-defined dimensions". Demo shows a user-written lens (~20 lines of `.dag`; e.g., "max external HTTP calls per workflow") rejecting a program that violates it, alongside the built-in complexity lens. Proves the ceiling of what gunbc can prove is user-extensible, not compiler-baked. Consumes `user_authored_lens_compiles` from T-LensAPI. **T-Demo scoping note.** All lanes ship features whole (no compromise per §Goals). T-Demo curates the R1 *narrative* — fixtures and impossible-bug demos selected for visceral audience impact, not exhaustive feature coverage. Audience curation is demo-scoping; feature shipment is lane-scoping. From 38945f9e0a114c9805329cf17ab4dc07d27df91c Mon Sep 17 00:00:00 2001 From: Brian Searls Date: Fri, 24 Apr 2026 20:47:14 -0400 Subject: [PATCH 11/21] docs(v3): clarify lane_e_host prepend comment (shadowing vs emit parity) MIME-Version: 1.0 Content-Type: text/plain; charset=UTF-8 Content-Transfer-Encoding: 8bit api-review ingest: O(n²) framing overstated coupling; lookup is linear scan, prepend order is for parity with generated cons order / shadowing edge. Made-with: Cursor --- src/v3/compiler/src/test_runner.rs | 5 +++-- 1 file changed, 3 insertions(+), 2 deletions(-) diff --git a/src/v3/compiler/src/test_runner.rs b/src/v3/compiler/src/test_runner.rs index 43d0704733e..f187731d8e9 100644 --- a/src/v3/compiler/src/test_runner.rs +++ b/src/v3/compiler/src/test_runner.rs @@ -63,8 +63,9 @@ fn lane_e_host_forward_cost_of(dag: &Dag, port: &PortId) -> CostLookup { } fn lane_e_host_compute_costs(nodes: &[Behavior]) -> LaneEHostCostAcc { - // O(n²) work from `Vec::insert(0, …)` matches `lens_cost_generated` prepend order; rewriting for - // asymptotics risks drifting from emit — delete this whole receipt once D1 runs canonical `cost_of`. + // Prepend via `insert(0, …)` matches `lens_cost_generated` cons order so `lane_e_host_lookup_cost` + // agrees with emit (first match wins; order only matters if duplicate ports shadow). Do not + // reorder without a parity check — delete this receipt once D1 runs canonical `cost_of`. let mut acc = lane_e_host_seed_bind_params(nodes); for behavior in nodes { let entry = lane_e_host_entry_for(&acc, behavior); From dc57bd51a11891032ec8dc371272e5931e9d030c Mon Sep 17 00:00:00 2001 From: Brian Searls Date: Fri, 24 Apr 2026 20:52:21 -0400 Subject: [PATCH 12/21] =?UTF-8?q?fix(v3):=20Codex=20gate-shape=20=E2=80=94?= =?UTF-8?q?=20MockBacked=20NYI=20without=20requires;=20cost=20suite=20spli?= =?UTF-8?q?t?= MIME-Version: 1.0 Content-Type: text/plain; charset=UTF-8 Content-Transfer-Encoding: 8bit - MockBackedInvariant: map hermetic Pass + empty requires to NotYetImplemented (DB-15 obligation surface); preserve Fail when invariant rejects subject. - R1 mock-backed gate fixture + integration expect NYI; document M1(2.8) gap. - Move CostBounded structural-cost receipt out of impossible_bug_class_suite_r1 into t_demo_structural_cost_obligation_suite; impossible suite is Pass-only. - ROADMAP: T-TestGen + T-Demo bullets match live receipts. Made-with: Cursor --- ROADMAP.md | 4 +- src/v3/compiler/src/test_runner.rs | 26 ++++++++-- .../r1_mock_backed_invariant_gate.dag | 5 +- src/v3/compiler/tests/integration.rs | 47 ++++++++++--------- .../tests/integration/test_runner_test.rs | 10 +++- .../compiler/tests/t_demo/t_demo_fixtures.dag | 29 +++++++----- 6 files changed, 78 insertions(+), 43 deletions(-) diff --git a/ROADMAP.md b/ROADMAP.md index 5d53d6b6051..d51a5f51951 100644 --- a/ROADMAP.md +++ b/ROADMAP.md @@ -62,14 +62,14 @@ This section lists gate names + schema-compilability tags; full `TestClaim` decl - **T-Sub.** `sub_match_over_user_sum` [Day 1, landed PR #702] · `sub_type_alias_where_lowers` [ext, landed PR #703] · `sub_charclass_in_std_unicode` [ext, open: phase-2 reproduction/triage] - **T-Emit.** `emit_rust_fixtures_rustc_green` [ext: `ExecuteCommand`] · `emit_generic_bounds_survive` [ext] · `emit_omni_demo_fixtures_green` [ext: `ForAllTargets` + `ExecuteCommand`] - **T-LaneE.** `complexity_merge_sort_is_nlogn` [ext: `LensOutputEquals`] · `complexity_v3_matches_v2_oracle` [ext: `DifferentialEquals`] -- **T-TestGen.** `testgen_structural_coverage` [ext] · `testgen_mock_backed_integration_safe` [ext: `MockBackedInvariant` wiring] · `testgen_manual_claim_is_first_class` [ext] — T-TestGen also owns scoping the predicate shape for `[ext]` gates that other lanes consume; currently includes `lens_producer_files_remaining` for T-PB-A (enumeration declared in `sg0_census_test.rs` at scoping time). +- **T-TestGen.** `testgen_structural_coverage` [ext] · `testgen_mock_backed_integration_safe` [ext: `MockBackedInvariant` — runner `NotYetImplemented` until `TestClaim.requires` carries at least one `ResourceReference`; M1(2.8) fixture list bodies) · `testgen_manual_claim_is_first_class` [ext] — T-TestGen also owns scoping the predicate shape for `[ext]` gates that other lanes consume; currently includes `lens_producer_files_remaining` for T-PB-A (enumeration declared in `sg0_census_test.rs` at scoping time). - **T-LensAPI.** `user_authored_lens_compiles` [Day 1] · `lens_composition_associative` [ext: `AlgebraicLaw`] · `lens_output_is_queryable_data` [ext] - **T-PB-A.** `pb_hand_rust_at_shim_floor` [ext] · `lens_producer_files_remaining` [ext — priority slice of the non-test census: hand-Rust files implementing lens producers, drops as each migrates to `.dag`; enumeration declared in `sg0_census_test.rs` when T-TestGen scopes the predicate] · `pb_self_compile_fixed_point` [ext] · `pb_compiler_std_ratchet_zero` [ext] — live baselines read from authorities; not frozen in this doc. Hand-Rust (**non-test subset**): SG-0 census (file-level + fragments ratchet) minus the test subset owned by T-PB-B → ≤5 irreducible-shim per `docs/design-pure-bootstrap.md`. Consolidation ratchet: compiler-local types not in positive-def set → 0. - **T-PB-B.** `pb_test_file_generated_from_dag` [ext] · `pb_rust_tests_outside_residual_zero` [ext] — the first gates the pipeline-equivalent suite; the second gates the outcome: zero Rust-authored tests exist outside the `TESTING.md §"Post-R2 shape"` residual (compiler-internal unit tests + external-toolchain boundary tests). Single-file generation is insufficient proof of the lane's end-state. - **T-Demo.** - `fixture_compiler_nerd_canonical` [Day 1 (Compiles) / ext (lens-output demos)] — demonstrates: complexity, ownership, parallelism - `fixture_integration_canonical` [Day 1 (Compiles) / ext (lens-output demos)] — demonstrates: effects, idempotency, testgen - - `impossible_bug_class_suite_r1` [ext] — idempotency-violation (`compose_effects` + breaking `AppendEffect` under `IsIdempotent` → `ResolveError`), suboptimal-complexity (nested `fold` + `CostBounded` vs structural `cost_of`), transport/type-drift (`TypeMismatch`). Remaining three (nested-optional flatten, unhandled diagnostic paths, unenumerated effects) are tagged **[R2+]** in THESIS — thesis-committed but not scheduled to a specific release. THESIS §"Enumerable impossible-bug classes" is the authority on scheduling tags. + - `impossible_bug_class_suite_r1` [ext] — idempotency-violation (`compose_effects` + breaking `AppendEffect` under `IsIdempotent` → `ResolveError`), transport/type-drift (`TypeMismatch`) — all `Pass` claims (`FailsWithDiagnostic` only). Suboptimal-complexity vs structural `cost_of` lives in `t_demo_structural_cost_obligation_suite` (`CostBounded` receipt is runner `Fail`, asserted in integration). Remaining three (nested-optional flatten, unhandled diagnostic paths, unenumerated effects) are tagged **[R2+]** in THESIS — thesis-committed but not scheduled to a specific release. THESIS §"Enumerable impossible-bug classes" is the authority on scheduling tags. - `demo_user_authored_lens_rejects_violating_program` [ext] — operationalizes THESIS §"User-defined dimensions". Demo shows a user-written lens (~20 lines of `.dag`; e.g., "max external HTTP calls per workflow") rejecting a program that violates it, alongside the built-in complexity lens. Proves the ceiling of what gunbc can prove is user-extensible, not compiler-baked. Consumes `user_authored_lens_compiles` from T-LensAPI. **T-Demo scoping note.** All lanes ship features whole (no compromise per §Goals). T-Demo curates the R1 *narrative* — fixtures and impossible-bug demos selected for visceral audience impact, not exhaustive feature coverage. Audience curation is demo-scoping; feature shipment is lane-scoping. diff --git a/src/v3/compiler/src/test_runner.rs b/src/v3/compiler/src/test_runner.rs index f187731d8e9..68161d33770 100644 --- a/src/v3/compiler/src/test_runner.rs +++ b/src/v3/compiler/src/test_runner.rs @@ -356,7 +356,24 @@ impl<'a> TestRunner<'a> { "LensOutputEquals" => self.eval_lens_output_equals(claim, &payload), "DifferentialEquals" => self.eval_differential_equals(claim, &payload), "AlgebraicLaw" => self.eval_algebraic_law(claim, &payload), - "MockBackedInvariant" => self.eval_mock_backed_invariant(claim, &payload), + "MockBackedInvariant" => { + let inner = self.eval_mock_backed_invariant(claim, &payload); + if claim.requires.is_empty() { + match inner { + ClaimResult::Pass => ClaimResult::NotYetImplemented( + "MockBackedInvariant: `TestClaim.requires` is empty — DB-15 mock \ + obligations attach only on `requires` as `ResourceReference` edges; \ + hermetic subject/invariant application succeeded but is not a mock-backed \ + receipt until at least one obligation is declared (M1(2.8): list bodies \ + in fixture `TestClaim` data are not expressible yet)." + .to_string(), + ), + other => other, + } + } else { + inner + } + } other => ClaimResult::NotYetImplemented(format!( "TestPredicate::{other} is not wired in the Rust runner yet" )), @@ -938,9 +955,10 @@ impl<'a> TestRunner<'a> { } } - /// R1 path: compile `claim.source`, then `apply_lens_declaration` for subject (0-arity) and - /// invariant (1-arity) — hermetic, no mock transport. `MockBackedInvariant` is the schema-stable - /// `TestPredicate` label; DB-15 mock semantics belong on `TestClaim.requires` when wired. + /// Hermetic path: compile `claim.source`, then `apply_lens_declaration` for subject (0-arity) + /// and invariant (1-arity). `run_claim` wraps a bare `Pass` in `NotYetImplemented` when + /// `requires` is empty so we do not fabricate a mock-backed receipt without a DB-15 obligation + /// surface (see `MockBackedInvariant` arm in `run_claim`). fn eval_mock_backed_invariant( &self, claim: &TestClaimValue, diff --git a/src/v3/compiler/tests/fixtures/r1_mock_backed_invariant_gate.dag b/src/v3/compiler/tests/fixtures/r1_mock_backed_invariant_gate.dag index 5c54e09f368..3884e533a6f 100644 --- a/src/v3/compiler/tests/fixtures/r1_mock_backed_invariant_gate.dag +++ b/src/v3/compiler/tests/fixtures/r1_mock_backed_invariant_gate.dag @@ -1,6 +1,7 @@ // R1 gate for `testgen_mock_backed_integration_safe` (ROADMAP). `MockBackedInvariant` names the -// `TestPredicate` variant only; the runner path is hermetic subject+invariant application on -// compiled `source`, not external mock simulation (empty `requires` until obligation materialization). +// `TestPredicate` variant; `requires` stays `[]` until M1(2.8) can express `List` +// bodies in fixture `.dag`. The runner performs hermetic subject+invariant application but does +// not emit a mock-backed Pass when `requires` is empty (see `TestRunner::run_claim`). // Lives under tests/fixtures/ — not auto-staged into bootstrap. module std.r1_mock_backed_invariant_gate diff --git a/src/v3/compiler/tests/integration.rs b/src/v3/compiler/tests/integration.rs index 213a9a31b13..a4b81c23abb 100644 --- a/src/v3/compiler/tests/integration.rs +++ b/src/v3/compiler/tests/integration.rs @@ -213,28 +213,31 @@ mod t_demo_fixture_test { let source = fixture_source(); let dag = compile_fixture(&source); let results = TestRunner::new(&dag).run_suite("impossible_bug_class_suite_r1"); - assert_eq!(results.len(), 3); - for result in &results { - if result.claim_name == "impossible_bug_class_suite_r1.suboptimal_complexity" { - let ClaimResult::Fail(msg) = &result.result else { - panic!( - "suboptimal_complexity should fail CostBounded (structural cost exceeds bound), got {:?}", - result.result - ); - }; - assert!( - msg.contains("cost") && msg.contains("did not satisfy"), - "unexpected CostBounded failure message: {msg}" - ); - } else { - assert_eq!( - result.result, - ClaimResult::Pass, - "claim `{}` should Pass (diagnostic receipt)", - result.claim_name - ); - } - } + assert_eq!(results.len(), 2); + assert!( + results + .iter() + .all(|result| result.result == ClaimResult::Pass), + "impossible-bug suite claims should all Pass (FailsWithDiagnostic receipts only), got {results:?}" + ); + } + + #[test] + fn t_demo_structural_cost_obligation_suite_observes_cost_bound_fail() { + let source = fixture_source(); + let dag = compile_fixture(&source); + let results = TestRunner::new(&dag).run_suite("t_demo_structural_cost_obligation_suite"); + assert_eq!(results.len(), 1); + let ClaimResult::Fail(msg) = &results[0].result else { + panic!( + "structural cost obligation gate should Fail CostBounded (cost exceeds bound), got {:?}", + results[0].result + ); + }; + assert!( + msg.contains("cost") && msg.contains("did not satisfy"), + "unexpected CostBounded failure message: {msg}" + ); } } diff --git a/src/v3/compiler/tests/integration/test_runner_test.rs b/src/v3/compiler/tests/integration/test_runner_test.rs index c47517fdbfa..219be5ee9c3 100644 --- a/src/v3/compiler/tests/integration/test_runner_test.rs +++ b/src/v3/compiler/tests/integration/test_runner_test.rs @@ -410,7 +410,15 @@ fn test_runner_dispatches_mock_backed_invariant_claim() { results[0].claim_name, "testgen_mock_backed_integration_safe" ); - assert_eq!(results[0].result, ClaimResult::Pass); + assert!( + matches!( + &results[0].result, + ClaimResult::NotYetImplemented(msg) + if msg.contains("MockBackedInvariant") && msg.contains("requires") + ), + "expected NYI for empty `requires` mock-backed receipt, got {:?}", + results[0].result + ); } #[test] diff --git a/src/v3/compiler/tests/t_demo/t_demo_fixtures.dag b/src/v3/compiler/tests/t_demo/t_demo_fixtures.dag index 7120cb456d8..08b3b6aa40c 100644 --- a/src/v3/compiler/tests/t_demo/t_demo_fixtures.dag +++ b/src/v3/compiler/tests/t_demo/t_demo_fixtures.dag @@ -193,8 +193,9 @@ data fixture_integration_canonical: TestSuite = { // `idempotency_violation`: `AppendEffect` is breaking (monoid append) and must not appear under // `IsIdempotent`; the compiler rejects it as an `IdempotentShape` mismatch (`ResolveError` + fix // text naming `IdempotentShape`). -// `suboptimal_complexity`: nested `fold` program compiles, but structural `cost_of` exceeds an -// impossible tight bound — exercises T-LaneE / `lens_cost::cost_of` via `CostBounded` (runner Fail). +// `t_demo_structural_cost_obligation_suite` (below): nested `fold` + `CostBounded` vs structural +// `cost_of` — runner `Fail` is the receipt (kept out of `impossible_bug_class_suite_r1` so that +// suite is all `Pass` claims only). data impossible_bug_type_drift: TestClaim = { name: "impossible_bug_class_suite_r1.transport_type_drift", source: "let drift: String = 1\n", @@ -217,19 +218,23 @@ data impossible_bug_idempotency_violation: TestClaim = { requires: [] } -data impossible_bug_suboptimal_complexity: TestClaim = { - name: "impossible_bug_class_suite_r1.suboptimal_complexity", - source: "fn pair_score(xs: List) -> Int = fold(xs, 0, |outer, x| outer + fold(xs, 0, |inner, y| inner + x + y))\nlet complexity_demo_out: Int = pair_score(cons(1, singleton(2)))\n", - file_name: "impossible_bug_suboptimal_complexity.v3", - predicate: CostBounded("complexity_demo_out", Lt, 1), - requires: [] -} - data impossible_bug_class_suite_r1: TestSuite = { name: "impossible_bug_class_suite_r1", claims: [ impossible_bug_type_drift, - impossible_bug_idempotency_violation, - impossible_bug_suboptimal_complexity + impossible_bug_idempotency_violation ] } + +data t_demo_structural_cost_obligation_gate: TestClaim = { + name: "t_demo_structural_cost_obligation.pair_score_too_deep", + source: "fn pair_score(xs: List) -> Int = fold(xs, 0, |outer, x| outer + fold(xs, 0, |inner, y| inner + x + y))\nlet complexity_demo_out: Int = pair_score(cons(1, singleton(2)))\n", + file_name: "t_demo_structural_cost_obligation.v3", + predicate: CostBounded("complexity_demo_out", Lt, 1), + requires: [] +} + +data t_demo_structural_cost_obligation_suite: TestSuite = { + name: "t_demo_structural_cost_obligation_suite", + claims: [t_demo_structural_cost_obligation_gate] +} From 5cbb285b488859d9fbd9b49f99fc049a22a4605a Mon Sep 17 00:00:00 2001 From: Brian Searls Date: Fri, 24 Apr 2026 21:04:40 -0400 Subject: [PATCH 13/21] docs(tests): ingest api-review naming + lens byte ratchet (dc57bd51) - Rename integration idempotency_lens_output claim to type_drift_lens_output - Clarify Lane E differential comment (trivial witness vs merge-sort receipt) - Ratchet R1_CANONICAL_COMPLEXITY_LENS include_str on compute_costs spine - Document LensOutputEquals(cost_of) uses emit not D1 apply Made-with: Cursor --- src/v3/compiler/src/test_runner.rs | 6 ++++-- src/v3/compiler/tests/fixtures/r1_gates.dag | 11 +++++------ .../compiler/tests/fixtures/r1_gates.template.dag | 11 +++++------ .../compiler/tests/integration/test_runner_test.rs | 10 +++++++++- src/v3/compiler/tests/t_demo/t_demo_fixtures.dag | 13 ++++++++----- 5 files changed, 31 insertions(+), 20 deletions(-) diff --git a/src/v3/compiler/src/test_runner.rs b/src/v3/compiler/src/test_runner.rs index 68161d33770..461010421b5 100644 --- a/src/v3/compiler/src/test_runner.rs +++ b/src/v3/compiler/src/test_runner.rs @@ -23,8 +23,10 @@ pub const R1_CANONICAL_NAMED_FUNCTION_COUNT_LENS: &str = include_str!(concat!( )); /// Same on-disk lens as `src/v3/lenses/complexity.dag`. `LensOutputEquals(cost_of, …)` applies -/// [`crate::lens_cost::cost_of`] on the compiled claim program (T-LaneE) — not the fixture-local -/// `fn cost_of` stub body (`INVARIANTS.md` P2). +/// [`crate::lens_cost::cost_of`] (emit from these bytes) on the compiled claim program — not +/// `apply_lens_declaration` on this text (D1 `cost_of` blocks on lens-internal `Loop`). Bytes are +/// still ratcheted in integration tests so the include stays aligned with the lens file. +/// Fixture-local `fn cost_of` stubs are unrelated (`INVARIANTS.md` P2). pub const R1_CANONICAL_COMPLEXITY_LENS: &str = include_str!(concat!( env!("CARGO_MANIFEST_DIR"), "/../lenses/complexity.dag" diff --git a/src/v3/compiler/tests/fixtures/r1_gates.dag b/src/v3/compiler/tests/fixtures/r1_gates.dag index f4e02e68807..08e443766da 100644 --- a/src/v3/compiler/tests/fixtures/r1_gates.dag +++ b/src/v3/compiler/tests/fixtures/r1_gates.dag @@ -183,12 +183,11 @@ data complexity_merge_sort_is_nlogn_gate: TestClaim = { requires: [] } -// Differential witness: minimal `Int` bind so the gate stays cheap. `v3_program_cost` is a -// host forward-fold receipt (see `test_runner::lane_e_host_forward_cost_of`); `v2_oracle_cost` is -// `lens_cost::cost_of` (emit from `complexity.dag`). D1 `apply_lens_declaration(cost_of)` is -// deferred: the canonical lens lowers list recursion to substrate `Loop`, which D1 does not -// interpret yet (`LensApplyError::UnimplementedLoopBound`). Merge-sort cost remains on -// `complexity_merge_sort_is_nlogn` (Rust `LensOutputEquals`). +// Differential witness: trivial `1 + 2` bind — exercises that host forward-fold and emit +// `lens_cost::cost_of` agree on a minimal program (both producers would need to diverge to fail). +// Substantive structural depth is **not** what this row proves; `complexity_merge_sort_is_nlogn` +// carries the merge-sort `LensOutputEquals(cost_of, …)` receipt. D1 `apply_lens_declaration(cost_of)` +// on the canonical lens stays deferred (`Loop` / `UnimplementedLoopBound` in the lens graph). data complexity_v3_matches_v2_oracle_gate: TestClaim = { name: "complexity_v3_matches_v2_oracle", source: "let lane_e_diff_out: Int = 1 + 2\n", diff --git a/src/v3/compiler/tests/fixtures/r1_gates.template.dag b/src/v3/compiler/tests/fixtures/r1_gates.template.dag index 4cb6f366096..76f41fe634d 100644 --- a/src/v3/compiler/tests/fixtures/r1_gates.template.dag +++ b/src/v3/compiler/tests/fixtures/r1_gates.template.dag @@ -183,12 +183,11 @@ data complexity_merge_sort_is_nlogn_gate: TestClaim = { requires: [] } -// Differential witness: minimal `Int` bind so the gate stays cheap. `v3_program_cost` is a -// host forward-fold receipt (see `test_runner::lane_e_host_forward_cost_of`); `v2_oracle_cost` is -// `lens_cost::cost_of` (emit from `complexity.dag`). D1 `apply_lens_declaration(cost_of)` is -// deferred: the canonical lens lowers list recursion to substrate `Loop`, which D1 does not -// interpret yet (`LensApplyError::UnimplementedLoopBound`). Merge-sort cost remains on -// `complexity_merge_sort_is_nlogn` (Rust `LensOutputEquals`). +// Differential witness: trivial `1 + 2` bind — exercises that host forward-fold and emit +// `lens_cost::cost_of` agree on a minimal program (both producers would need to diverge to fail). +// Substantive structural depth is **not** what this row proves; `complexity_merge_sort_is_nlogn` +// carries the merge-sort `LensOutputEquals(cost_of, …)` receipt. D1 `apply_lens_declaration(cost_of)` +// on the canonical lens stays deferred (`Loop` / `UnimplementedLoopBound` in the lens graph). data complexity_v3_matches_v2_oracle_gate: TestClaim = { name: "complexity_v3_matches_v2_oracle", source: "let lane_e_diff_out: Int = 1 + 2\n", diff --git a/src/v3/compiler/tests/integration/test_runner_test.rs b/src/v3/compiler/tests/integration/test_runner_test.rs index 219be5ee9c3..41300af5b23 100644 --- a/src/v3/compiler/tests/integration/test_runner_test.rs +++ b/src/v3/compiler/tests/integration/test_runner_test.rs @@ -517,7 +517,15 @@ data suite: TestSuite = { #[test] fn r1_canonical_complexity_lens_bytes_include_cost_of() { - assert!(v3_compiler::test_runner::R1_CANONICAL_COMPLEXITY_LENS.contains("fn cost_of")); + let bytes = v3_compiler::test_runner::R1_CANONICAL_COMPLEXITY_LENS; + assert!( + bytes.contains("fn cost_of"), + "canonical lens should declare cost_of" + ); + assert!( + bytes.contains("fn compute_costs") && bytes.contains("fn seed_bind_params"), + "canonical `complexity.dag` bytes should include the forward-fold spine, not just the `cost_of` signature" + ); } #[test] diff --git a/src/v3/compiler/tests/t_demo/t_demo_fixtures.dag b/src/v3/compiler/tests/t_demo/t_demo_fixtures.dag index 08b3b6aa40c..42fd73f660f 100644 --- a/src/v3/compiler/tests/t_demo/t_demo_fixtures.dag +++ b/src/v3/compiler/tests/t_demo/t_demo_fixtures.dag @@ -158,10 +158,12 @@ data integration_effects_lens_output: TestClaim = { requires: [] } -data integration_idempotency_lens_output: TestClaim = { - name: "fixture_integration_canonical.idempotency_lens_output", +// Type-drift receipt (same pattern as `impossible_bug_type_drift`); not the effects idempotency +// story — that lives on `integration_idempotency_compiles` + `impossible_bug_idempotency_violation`. +data integration_type_drift_lens_output: TestClaim = { + name: "fixture_integration_canonical.type_drift_lens_output", source: "let drift: Bool = 1\n", - file_name: "fixture_integration_canonical_idempotency_lens.v3", + file_name: "fixture_integration_canonical_type_drift_lens.v3", predicate: FailsWithDiagnostic({ kind: TypeMismatch, detail_contains: AnyDetail @@ -184,12 +186,13 @@ data fixture_integration_canonical: TestSuite = { integration_idempotency_compiles, integration_testgen_compiles, integration_effects_lens_output, - integration_idempotency_lens_output, + integration_type_drift_lens_output, integration_testgen_runner_output ] } -// `impossible_bug_class_suite_r1` — three visceral detector receipts (ROADMAP.md:71-72). +// `impossible_bug_class_suite_r1` — two `FailsWithDiagnostic` receipts (ROADMAP.md:71-72); structural +// cost bound lives in `t_demo_structural_cost_obligation_suite` (integration asserts `Fail`). // `idempotency_violation`: `AppendEffect` is breaking (monoid append) and must not appear under // `IsIdempotent`; the compiler rejects it as an `IdempotentShape` mismatch (`ResolveError` + fix // text naming `IdempotentShape`). From 3e69836be90a23b07dd7676c1f57c09e7fe1a699 Mon Sep 17 00:00:00 2001 From: Brian Searls Date: Fri, 24 Apr 2026 21:23:27 -0400 Subject: [PATCH 14/21] WIP: R1 Gate Sweep --- src/v3/compiler/build.rs | 77 +++++++++++++++---- src/v3/compiler/tests/fixtures/r1_gates.dag | 5 +- .../tests/fixtures/r1_gates.template.dag | 7 +- 3 files changed, 67 insertions(+), 22 deletions(-) diff --git a/src/v3/compiler/build.rs b/src/v3/compiler/build.rs index f10355020e4..3a16c9d1bb8 100644 --- a/src/v3/compiler/build.rs +++ b/src/v3/compiler/build.rs @@ -123,8 +123,8 @@ fn collect_dag_entries_impl(dir: &Path, prioritized: &[&str], recursive: bool) - entries } -/// Escape `body` so it can replace the `R1_NAMED_FUNCTION_COUNT_LENS_SPLICE_V1` placeholder -/// inside a `.dag` double-quoted `TestClaim.source` literal (T-LensAPI D4 fixture splice). +/// Escape `body` so it can replace a `*_SPLICE_V1` placeholder inside a `.dag` double-quoted +/// `TestClaim.source` literal (R1 gate fixture hygiene; see `emit_r1_gates_fixture`). fn escape_dag_double_quoted_body(body: &str) -> String { let mut out = String::with_capacity(body.len() + 8); for ch in body.chars() { @@ -140,21 +140,32 @@ fn escape_dag_double_quoted_body(body: &str) -> String { out } -/// Emit `tests/fixtures/r1_gates.dag` from `r1_gates.template.dag` + canonical lens text. +/// Emit `tests/fixtures/r1_gates.dag` from `r1_gates.template.dag` + canonical lens and `.v3` +/// program text. /// /// **Hygiene:** `r1_gates.dag` is tracked in git but produced here so the spliced lens stays -/// byte-identical to `src/v3/lenses/named_function_count.dag`. Hand-edit **`r1_gates.template.dag`** -/// only — direct edits to `r1_gates.dag` are overwritten on the next `cargo build`. We skip -/// `fs::write` when the generated bytes are unchanged to avoid spurious working-tree noise. +/// byte-identical to `src/v3/lenses/named_function_count.dag`, and Lane E `TestClaim.source` +/// strings are spliced from canonical `.v3` fixtures (single authority; INVARIANTS P2). +/// Hand-edit **`r1_gates.template.dag`** only — direct edits to `r1_gates.dag` are overwritten +/// on the next `cargo build`. We skip `fs::write` when the generated bytes are unchanged to +/// avoid spurious working-tree noise. fn emit_r1_gates_fixture(manifest_path: &Path, v3_dir: &Path) { - /// Must appear exactly once in `r1_gates.template.dag` (the `TestClaim.source` line only). - const SPLICE_SENTINEL: &str = "R1_NAMED_FUNCTION_COUNT_LENS_SPLICE_V1"; - let template_path = manifest_path.join("tests/fixtures/r1_gates.template.dag"); + /// Must appear exactly once in `r1_gates.template.dag` (inside the relevant `source:` line). + const LENS_SPLICE_SENTINEL: &str = "R1_NAMED_FUNCTION_COUNT_LENS_SPLICE_V1"; + const MERGE_SORT_PAIR_V3_SPLICE: &str = "R1_MERGE_SORT_PAIR_V3_SPLICE_V1"; + const LANE_E_DIFF_WITNESS_V3_SPLICE: &str = "R1_LANE_E_DIFFERENTIAL_WITNESS_V3_SPLICE_V1"; + + let fixtures_dir = manifest_path.join("tests/fixtures"); + let template_path = fixtures_dir.join("r1_gates.template.dag"); let lens_path = v3_dir.join("lenses/named_function_count.dag"); - let out_path = manifest_path.join("tests/fixtures/r1_gates.dag"); + let merge_sort_pair_v3 = fixtures_dir.join("r1_merge_sort_pair.v3"); + let lane_e_diff_witness_v3 = fixtures_dir.join("r1_lane_e_differential_witness.v3"); + let out_path = fixtures_dir.join("r1_gates.dag"); println!("cargo:rerun-if-changed={}", template_path.display()); println!("cargo:rerun-if-changed={}", lens_path.display()); + println!("cargo:rerun-if-changed={}", merge_sort_pair_v3.display()); + println!("cargo:rerun-if-changed={}", lane_e_diff_witness_v3.display()); let template = fs::read_to_string(&template_path).unwrap_or_else(|e| { panic!( @@ -170,15 +181,47 @@ fn emit_r1_gates_fixture(manifest_path: &Path, v3_dir: &Path) { e ) }); - let splice_count = template.matches(SPLICE_SENTINEL).count(); - if splice_count != 1 { + let merge_sort_pair_src = fs::read_to_string(&merge_sort_pair_v3).unwrap_or_else(|e| { + panic!( + "failed to read R1 merge-sort pair fixture {}: {}", + merge_sort_pair_v3.display(), + e + ) + }); + let lane_e_diff_src = fs::read_to_string(&lane_e_diff_witness_v3).unwrap_or_else(|e| { panic!( - "{} must contain exactly one `{SPLICE_SENTINEL}` (found {splice_count})", - template_path.display() - ); + "failed to read R1 Lane E differential witness fixture {}: {}", + lane_e_diff_witness_v3.display(), + e + ) + }); + + for (sentinel, label) in [ + (LENS_SPLICE_SENTINEL, "named_function_count lens"), + (MERGE_SORT_PAIR_V3_SPLICE, "r1_merge_sort_pair.v3"), + (LANE_E_DIFF_WITNESS_V3_SPLICE, "r1_lane_e_differential_witness.v3"), + ] { + let count = template.matches(sentinel).count(); + if count != 1 { + panic!( + "{} must contain exactly one `{sentinel}` for {label} (found {count})", + template_path.display() + ); + } } - let escaped = escape_dag_double_quoted_body(&lens); - let generated = template.replace(SPLICE_SENTINEL, &escaped); + + let mut generated = template.replace( + LENS_SPLICE_SENTINEL, + &escape_dag_double_quoted_body(&lens), + ); + generated = generated.replace( + MERGE_SORT_PAIR_V3_SPLICE, + &escape_dag_double_quoted_body(&merge_sort_pair_src), + ); + generated = generated.replace( + LANE_E_DIFF_WITNESS_V3_SPLICE, + &escape_dag_double_quoted_body(&lane_e_diff_src), + ); let needs_write = match fs::read_to_string(&out_path) { Ok(existing) => existing != generated, Err(_) => true, diff --git a/src/v3/compiler/tests/fixtures/r1_gates.dag b/src/v3/compiler/tests/fixtures/r1_gates.dag index 08e443766da..6338c05a982 100644 --- a/src/v3/compiler/tests/fixtures/r1_gates.dag +++ b/src/v3/compiler/tests/fixtures/r1_gates.dag @@ -168,7 +168,8 @@ data r1_lens_output_equals_suite: TestSuite = { // T-LaneE — merge-sort pair witness (structural `cost_of` on `merge_sort_out` vs expected `Int`). // M1(2.8): `Lookup` literals are not yet expressible in `data` bodies — compare `Hit(n)` to -// this scalar witness. Program text is byte-identical to `tests/fixtures/r1_merge_sort_pair.v3`. +// this scalar witness. `TestClaim.source` is spliced from `tests/fixtures/r1_merge_sort_pair.v3` +// at `cargo build` (see `emit_r1_gates_fixture` in `v3-compiler/build.rs`). data complexity_merge_sort_expected_cost: Int = 3 data complexity_merge_sort_is_nlogn_gate: TestClaim = { @@ -190,7 +191,7 @@ data complexity_merge_sort_is_nlogn_gate: TestClaim = { // on the canonical lens stays deferred (`Loop` / `UnimplementedLoopBound` in the lens graph). data complexity_v3_matches_v2_oracle_gate: TestClaim = { name: "complexity_v3_matches_v2_oracle", - source: "let lane_e_diff_out: Int = 1 + 2\n", + source: "// Minimal structural-cost witness for `complexity_v3_matches_v2_oracle` (T-LaneE).\n// Runner compares a host forward-fold receipt to `lens_cost::cost_of` (see `test_runner.rs`).\n\nlet lane_e_diff_out: Int = 1 + 2\n", file_name: "r1_lane_e_differential_witness.v3", predicate: DifferentialEquals( v3_program_cost, diff --git a/src/v3/compiler/tests/fixtures/r1_gates.template.dag b/src/v3/compiler/tests/fixtures/r1_gates.template.dag index 76f41fe634d..af8a4ce6950 100644 --- a/src/v3/compiler/tests/fixtures/r1_gates.template.dag +++ b/src/v3/compiler/tests/fixtures/r1_gates.template.dag @@ -168,12 +168,13 @@ data r1_lens_output_equals_suite: TestSuite = { // T-LaneE — merge-sort pair witness (structural `cost_of` on `merge_sort_out` vs expected `Int`). // M1(2.8): `Lookup` literals are not yet expressible in `data` bodies — compare `Hit(n)` to -// this scalar witness. Program text is byte-identical to `tests/fixtures/r1_merge_sort_pair.v3`. +// this scalar witness. `TestClaim.source` is spliced from `tests/fixtures/r1_merge_sort_pair.v3` +// at `cargo build` (see `emit_r1_gates_fixture` in `v3-compiler/build.rs`). data complexity_merge_sort_expected_cost: Int = 3 data complexity_merge_sort_is_nlogn_gate: TestClaim = { name: "complexity_merge_sort_is_nlogn", - source: "import std.list { List, cons, singleton, empty }\n\nlet xs: List = cons(2, singleton(1))\n\nfn merge_sort_pair(xs: List) -> List =\n match xs {\n Empty => empty()\n Cons(p0) =>\n match p0.tail {\n Empty => xs\n Cons(p1) =>\n match p1.tail {\n Empty =>\n if p0.head < p1.head\n then cons(p0.head, singleton(p1.head))\n else cons(p1.head, singleton(p0.head))\n Cons(_) => xs\n }\n }\n }\n\nlet merge_sort_out: List = merge_sort_pair(xs)\n", + source: "R1_MERGE_SORT_PAIR_V3_SPLICE_V1", file_name: "r1_merge_sort_pair.v3", predicate: LensOutputEquals( cost_of, @@ -190,7 +191,7 @@ data complexity_merge_sort_is_nlogn_gate: TestClaim = { // on the canonical lens stays deferred (`Loop` / `UnimplementedLoopBound` in the lens graph). data complexity_v3_matches_v2_oracle_gate: TestClaim = { name: "complexity_v3_matches_v2_oracle", - source: "let lane_e_diff_out: Int = 1 + 2\n", + source: "R1_LANE_E_DIFFERENTIAL_WITNESS_V3_SPLICE_V1", file_name: "r1_lane_e_differential_witness.v3", predicate: DifferentialEquals( v3_program_cost, From efbb97877161474f4672f22f978e7a347d2a19dd Mon Sep 17 00:00:00 2001 From: Brian Searls Date: Fri, 24 Apr 2026 21:23:30 -0400 Subject: [PATCH 15/21] chore: apply cargo fmt --- src/v3/compiler/build.rs | 16 ++++++++++------ 1 file changed, 10 insertions(+), 6 deletions(-) diff --git a/src/v3/compiler/build.rs b/src/v3/compiler/build.rs index 3a16c9d1bb8..2c670720d32 100644 --- a/src/v3/compiler/build.rs +++ b/src/v3/compiler/build.rs @@ -165,7 +165,10 @@ fn emit_r1_gates_fixture(manifest_path: &Path, v3_dir: &Path) { println!("cargo:rerun-if-changed={}", template_path.display()); println!("cargo:rerun-if-changed={}", lens_path.display()); println!("cargo:rerun-if-changed={}", merge_sort_pair_v3.display()); - println!("cargo:rerun-if-changed={}", lane_e_diff_witness_v3.display()); + println!( + "cargo:rerun-if-changed={}", + lane_e_diff_witness_v3.display() + ); let template = fs::read_to_string(&template_path).unwrap_or_else(|e| { panic!( @@ -199,7 +202,10 @@ fn emit_r1_gates_fixture(manifest_path: &Path, v3_dir: &Path) { for (sentinel, label) in [ (LENS_SPLICE_SENTINEL, "named_function_count lens"), (MERGE_SORT_PAIR_V3_SPLICE, "r1_merge_sort_pair.v3"), - (LANE_E_DIFF_WITNESS_V3_SPLICE, "r1_lane_e_differential_witness.v3"), + ( + LANE_E_DIFF_WITNESS_V3_SPLICE, + "r1_lane_e_differential_witness.v3", + ), ] { let count = template.matches(sentinel).count(); if count != 1 { @@ -210,10 +216,8 @@ fn emit_r1_gates_fixture(manifest_path: &Path, v3_dir: &Path) { } } - let mut generated = template.replace( - LENS_SPLICE_SENTINEL, - &escape_dag_double_quoted_body(&lens), - ); + let mut generated = + template.replace(LENS_SPLICE_SENTINEL, &escape_dag_double_quoted_body(&lens)); generated = generated.replace( MERGE_SORT_PAIR_V3_SPLICE, &escape_dag_double_quoted_body(&merge_sort_pair_src), From 03e4354796c1daba5343d5b2e70edf01dc46f449 Mon Sep 17 00:00:00 2001 From: Brian Searls Date: Fri, 24 Apr 2026 21:29:52 -0400 Subject: [PATCH 16/21] feat(v3): T-LaneE merge-sort DifferentialEquals gate Add complexity_merge_sort_v3_matches_v2_oracle to r1_lane_e_suite so host forward-fold and lens_cost::cost_of are checked on merge_sort_out, not only via LensOutputEquals vs a scalar witness and the minimal 1+2 differential row. Allow R1_MERGE_SORT_PAIR_V3_SPLICE_V1 to repeat in the template (build.rs splices all occurrences from r1_merge_sort_pair.v3). Document roles in ROADMAP and r2-structure; extend integration suite length assertion. Made-with: Cursor --- ROADMAP.md | 2 +- docs/r2-structure.md | 4 +- src/v3/compiler/build.rs | 38 +++++++++++-------- src/v3/compiler/tests/fixtures/r1_gates.dag | 30 ++++++++++++--- .../tests/fixtures/r1_gates.template.dag | 30 ++++++++++++--- .../tests/integration/test_runner_test.rs | 2 +- 6 files changed, 74 insertions(+), 32 deletions(-) diff --git a/ROADMAP.md b/ROADMAP.md index d51a5f51951..a6491f220f6 100644 --- a/ROADMAP.md +++ b/ROADMAP.md @@ -61,7 +61,7 @@ This section lists gate names + schema-compilability tags; full `TestClaim` decl - **T-P0.** `p0_repeat_string_correct` [Day 1] · `p0_no_fabrication_sentinel` [ext] · `p0_rest_ops_aligned` [ext] - **T-Sub.** `sub_match_over_user_sum` [Day 1, landed PR #702] · `sub_type_alias_where_lowers` [ext, landed PR #703] · `sub_charclass_in_std_unicode` [ext, open: phase-2 reproduction/triage] - **T-Emit.** `emit_rust_fixtures_rustc_green` [ext: `ExecuteCommand`] · `emit_generic_bounds_survive` [ext] · `emit_omni_demo_fixtures_green` [ext: `ForAllTargets` + `ExecuteCommand`] -- **T-LaneE.** `complexity_merge_sort_is_nlogn` [ext: `LensOutputEquals`] · `complexity_v3_matches_v2_oracle` [ext: `DifferentialEquals`] +- **T-LaneE.** `complexity_merge_sort_is_nlogn` [ext: `LensOutputEquals`] · `complexity_merge_sort_v3_matches_v2_oracle` [ext: `DifferentialEquals`] · `complexity_v3_matches_v2_oracle` [ext: `DifferentialEquals`] - **T-TestGen.** `testgen_structural_coverage` [ext] · `testgen_mock_backed_integration_safe` [ext: `MockBackedInvariant` — runner `NotYetImplemented` until `TestClaim.requires` carries at least one `ResourceReference`; M1(2.8) fixture list bodies) · `testgen_manual_claim_is_first_class` [ext] — T-TestGen also owns scoping the predicate shape for `[ext]` gates that other lanes consume; currently includes `lens_producer_files_remaining` for T-PB-A (enumeration declared in `sg0_census_test.rs` at scoping time). - **T-LensAPI.** `user_authored_lens_compiles` [Day 1] · `lens_composition_associative` [ext: `AlgebraicLaw`] · `lens_output_is_queryable_data` [ext] - **T-PB-A.** `pb_hand_rust_at_shim_floor` [ext] · `lens_producer_files_remaining` [ext — priority slice of the non-test census: hand-Rust files implementing lens producers, drops as each migrates to `.dag`; enumeration declared in `sg0_census_test.rs` when T-TestGen scopes the predicate] · `pb_self_compile_fixed_point` [ext] · `pb_compiler_std_ratchet_zero` [ext] — live baselines read from authorities; not frozen in this doc. Hand-Rust (**non-test subset**): SG-0 census (file-level + fragments ratchet) minus the test subset owned by T-PB-B → ≤5 irreducible-shim per `docs/design-pure-bootstrap.md`. Consolidation ratchet: compiler-local types not in positive-def set → 0. diff --git a/docs/r2-structure.md b/docs/r2-structure.md index e10a5453609..9a1e26f418a 100644 --- a/docs/r2-structure.md +++ b/docs/r2-structure.md @@ -25,7 +25,7 @@ Post-R2 is external work (adoption, documentation, community, ecosystem modeling ## Goals -**Gate-ownership discipline.** Every R1 gate listed in `ROADMAP.md §"Lane acceptance — .dag gates"` closes in R1 under the locked all-R1-gates-green criterion (see R1 closure criteria below). That means concerns gated there — **lens purity** (`lens_producer_files_remaining` on T-PB-A via PR #752), **self-hosting shim-floor close** (T-PB-A `pb_hand_rust_at_shim_floor` + `pb_compiler_std_ratchet_zero` + T-PB-B `pb_rust_tests_outside_residual_zero`), and **E-family carrier port closure** (the T-LaneE critical path enabling `complexity_merge_sort_is_nlogn` + `complexity_v3_matches_v2_oracle`) — are **R1 scope, not R2**. R2 does not duplicate release authority over gates ROADMAP already assigns to R1 lanes. +**Gate-ownership discipline.** Every R1 gate listed in `ROADMAP.md §"Lane acceptance — .dag gates"` closes in R1 under the locked all-R1-gates-green criterion (see R1 closure criteria below). That means concerns gated there — **lens purity** (`lens_producer_files_remaining` on T-PB-A via PR #752), **self-hosting shim-floor close** (T-PB-A `pb_hand_rust_at_shim_floor` + `pb_compiler_std_ratchet_zero` + T-PB-B `pb_rust_tests_outside_residual_zero`), and **E-family carrier port closure** (the T-LaneE critical path enabling `complexity_merge_sort_is_nlogn` + `complexity_merge_sort_v3_matches_v2_oracle` + `complexity_v3_matches_v2_oracle`) — are **R1 scope, not R2**. R2 does not duplicate release authority over gates ROADMAP already assigns to R1 lanes. Under that discipline, R2's goals are the Tier-1 thesis claims that are *not* gated in R1 today: @@ -86,7 +86,7 @@ Continues `docs/briefs/grounding-manager.md` (refreshed for R2 scope on promotio **Lanes deliberately absent (R1 gates, closed by R1 lane acceptance):** - T-LensMigration / `lens_producer_files_remaining` — R1 T-PB-A gate per PR #752. - T-ShimFloor / `pb_hand_rust_at_shim_floor` / `pb_compiler_std_ratchet_zero` / `pb_rust_tests_outside_residual_zero` — R1 T-PB-A + T-PB-B gates. -- T-EFamilyClose — R1 T-LaneE's critical-path carrier work (E-T, E-C, E-I, E-P, E-M sub-lanes), enabling the R1 `complexity_merge_sort_is_nlogn` + `complexity_v3_matches_v2_oracle` gates. All E-family carrier-port work closes in R1; only the §6a metadata-pick residual inherits to R2 (Goal 5). +- T-EFamilyClose — R1 T-LaneE's critical-path carrier work (E-T, E-C, E-I, E-P, E-M sub-lanes), enabling the R1 `complexity_merge_sort_is_nlogn` + `complexity_merge_sort_v3_matches_v2_oracle` + `complexity_v3_matches_v2_oracle` gates. All E-family carrier-port work closes in R1; only the §6a metadata-pick residual inherits to R2 (Goal 5). - T-TestGen-tail (`testgen_mock_backed_integration_safe` / `MockBackedInvariant` wiring) — R1 T-TestGen gate per `ROADMAP.md §"Lane acceptance — .dag gates"`. Closes in R1. R2 does not re-own any of the above; under all-R1-gates-green R1 closure, those gates ARE the close conditions and R2 inherits nothing there (except Goal 5's §6a residual, which was not an R1 gate). diff --git a/src/v3/compiler/build.rs b/src/v3/compiler/build.rs index 2c670720d32..a7bb332023d 100644 --- a/src/v3/compiler/build.rs +++ b/src/v3/compiler/build.rs @@ -150,8 +150,9 @@ fn escape_dag_double_quoted_body(body: &str) -> String { /// on the next `cargo build`. We skip `fs::write` when the generated bytes are unchanged to /// avoid spurious working-tree noise. fn emit_r1_gates_fixture(manifest_path: &Path, v3_dir: &Path) { - /// Must appear exactly once in `r1_gates.template.dag` (inside the relevant `source:` line). + /// Must appear exactly once in `r1_gates.template.dag` (inside the `user_authored_lens_compiles` `source:` line). const LENS_SPLICE_SENTINEL: &str = "R1_NAMED_FUNCTION_COUNT_LENS_SPLICE_V1"; + /// May appear multiple times (each `TestClaim.source` that embeds merge-sort gets the same bytes). const MERGE_SORT_PAIR_V3_SPLICE: &str = "R1_MERGE_SORT_PAIR_V3_SPLICE_V1"; const LANE_E_DIFF_WITNESS_V3_SPLICE: &str = "R1_LANE_E_DIFFERENTIAL_WITNESS_V3_SPLICE_V1"; @@ -199,21 +200,26 @@ fn emit_r1_gates_fixture(manifest_path: &Path, v3_dir: &Path) { ) }); - for (sentinel, label) in [ - (LENS_SPLICE_SENTINEL, "named_function_count lens"), - (MERGE_SORT_PAIR_V3_SPLICE, "r1_merge_sort_pair.v3"), - ( - LANE_E_DIFF_WITNESS_V3_SPLICE, - "r1_lane_e_differential_witness.v3", - ), - ] { - let count = template.matches(sentinel).count(); - if count != 1 { - panic!( - "{} must contain exactly one `{sentinel}` for {label} (found {count})", - template_path.display() - ); - } + let lens_count = template.matches(LENS_SPLICE_SENTINEL).count(); + if lens_count != 1 { + panic!( + "{} must contain exactly one `{LENS_SPLICE_SENTINEL}` for named_function_count lens (found {lens_count})", + template_path.display() + ); + } + let merge_count = template.matches(MERGE_SORT_PAIR_V3_SPLICE).count(); + if merge_count < 1 { + panic!( + "{} must contain at least one `{MERGE_SORT_PAIR_V3_SPLICE}` (spliced into every Lane E claim that embeds merge-sort; found {merge_count})", + template_path.display() + ); + } + let diff_count = template.matches(LANE_E_DIFF_WITNESS_V3_SPLICE).count(); + if diff_count != 1 { + panic!( + "{} must contain exactly one `{LANE_E_DIFF_WITNESS_V3_SPLICE}` for r1_lane_e_differential_witness.v3 (found {diff_count})", + template_path.display() + ); } let mut generated = diff --git a/src/v3/compiler/tests/fixtures/r1_gates.dag b/src/v3/compiler/tests/fixtures/r1_gates.dag index 6338c05a982..8b6bd77bcff 100644 --- a/src/v3/compiler/tests/fixtures/r1_gates.dag +++ b/src/v3/compiler/tests/fixtures/r1_gates.dag @@ -184,11 +184,25 @@ data complexity_merge_sort_is_nlogn_gate: TestClaim = { requires: [] } -// Differential witness: trivial `1 + 2` bind — exercises that host forward-fold and emit -// `lens_cost::cost_of` agree on a minimal program (both producers would need to diverge to fail). -// Substantive structural depth is **not** what this row proves; `complexity_merge_sort_is_nlogn` -// carries the merge-sort `LensOutputEquals(cost_of, …)` receipt. D1 `apply_lens_declaration(cost_of)` -// on the canonical lens stays deferred (`Loop` / `UnimplementedLoopBound` in the lens graph). +// Cross-lineage parity on the merge-sort program: host forward-fold vs emit `lens_cost::cost_of` +// on `merge_sort_out` (same bind as `complexity_merge_sort_is_nlogn` — independent producers). +data complexity_merge_sort_v3_matches_v2_oracle_gate: TestClaim = { + name: "complexity_merge_sort_v3_matches_v2_oracle", + source: "import std.list { List, cons, singleton, empty }\n\nlet xs: List = cons(2, singleton(1))\n\nfn merge_sort_pair(xs: List) -> List =\n match xs {\n Empty => empty()\n Cons(p0) =>\n match p0.tail {\n Empty => xs\n Cons(p1) =>\n match p1.tail {\n Empty =>\n if p0.head < p1.head\n then cons(p0.head, singleton(p1.head))\n else cons(p1.head, singleton(p0.head))\n Cons(_) => xs\n }\n }\n }\n\nlet merge_sort_out: List = merge_sort_pair(xs)\n", + file_name: "r1_merge_sort_pair.v3", + predicate: DifferentialEquals( + v3_program_cost, + v2_oracle_cost, + r1_lens_output_input_from_program + ), + requires: [] +} + +// Differential witness: trivial `1 + 2` bind — minimal smoke that host forward-fold and emit +// `lens_cost::cost_of` agree when almost nothing happens structurally. Nested control-flow parity +// is covered by `complexity_merge_sort_v3_matches_v2_oracle`; scalar structural depth by +// `complexity_merge_sort_is_nlogn`. D1 `apply_lens_declaration(cost_of)` on the canonical lens +// stays deferred (`Loop` / `UnimplementedLoopBound` in the lens graph). data complexity_v3_matches_v2_oracle_gate: TestClaim = { name: "complexity_v3_matches_v2_oracle", source: "// Minimal structural-cost witness for `complexity_v3_matches_v2_oracle` (T-LaneE).\n// Runner compares a host forward-fold receipt to `lens_cost::cost_of` (see `test_runner.rs`).\n\nlet lane_e_diff_out: Int = 1 + 2\n", @@ -203,5 +217,9 @@ data complexity_v3_matches_v2_oracle_gate: TestClaim = { data r1_lane_e_suite: TestSuite = { name: "r1_lane_e_suite", - claims: [complexity_merge_sort_is_nlogn_gate, complexity_v3_matches_v2_oracle_gate] + claims: [ + complexity_merge_sort_is_nlogn_gate, + complexity_merge_sort_v3_matches_v2_oracle_gate, + complexity_v3_matches_v2_oracle_gate + ] } diff --git a/src/v3/compiler/tests/fixtures/r1_gates.template.dag b/src/v3/compiler/tests/fixtures/r1_gates.template.dag index af8a4ce6950..bf1eac13897 100644 --- a/src/v3/compiler/tests/fixtures/r1_gates.template.dag +++ b/src/v3/compiler/tests/fixtures/r1_gates.template.dag @@ -184,11 +184,25 @@ data complexity_merge_sort_is_nlogn_gate: TestClaim = { requires: [] } -// Differential witness: trivial `1 + 2` bind — exercises that host forward-fold and emit -// `lens_cost::cost_of` agree on a minimal program (both producers would need to diverge to fail). -// Substantive structural depth is **not** what this row proves; `complexity_merge_sort_is_nlogn` -// carries the merge-sort `LensOutputEquals(cost_of, …)` receipt. D1 `apply_lens_declaration(cost_of)` -// on the canonical lens stays deferred (`Loop` / `UnimplementedLoopBound` in the lens graph). +// Cross-lineage parity on the merge-sort program: host forward-fold vs emit `lens_cost::cost_of` +// on `merge_sort_out` (same bind as `complexity_merge_sort_is_nlogn` — independent producers). +data complexity_merge_sort_v3_matches_v2_oracle_gate: TestClaim = { + name: "complexity_merge_sort_v3_matches_v2_oracle", + source: "R1_MERGE_SORT_PAIR_V3_SPLICE_V1", + file_name: "r1_merge_sort_pair.v3", + predicate: DifferentialEquals( + v3_program_cost, + v2_oracle_cost, + r1_lens_output_input_from_program + ), + requires: [] +} + +// Differential witness: trivial `1 + 2` bind — minimal smoke that host forward-fold and emit +// `lens_cost::cost_of` agree when almost nothing happens structurally. Nested control-flow parity +// is covered by `complexity_merge_sort_v3_matches_v2_oracle`; scalar structural depth by +// `complexity_merge_sort_is_nlogn`. D1 `apply_lens_declaration(cost_of)` on the canonical lens +// stays deferred (`Loop` / `UnimplementedLoopBound` in the lens graph). data complexity_v3_matches_v2_oracle_gate: TestClaim = { name: "complexity_v3_matches_v2_oracle", source: "R1_LANE_E_DIFFERENTIAL_WITNESS_V3_SPLICE_V1", @@ -203,5 +217,9 @@ data complexity_v3_matches_v2_oracle_gate: TestClaim = { data r1_lane_e_suite: TestSuite = { name: "r1_lane_e_suite", - claims: [complexity_merge_sort_is_nlogn_gate, complexity_v3_matches_v2_oracle_gate] + claims: [ + complexity_merge_sort_is_nlogn_gate, + complexity_merge_sort_v3_matches_v2_oracle_gate, + complexity_v3_matches_v2_oracle_gate + ] } diff --git a/src/v3/compiler/tests/integration/test_runner_test.rs b/src/v3/compiler/tests/integration/test_runner_test.rs index 41300af5b23..eae66d8983c 100644 --- a/src/v3/compiler/tests/integration/test_runner_test.rs +++ b/src/v3/compiler/tests/integration/test_runner_test.rs @@ -583,7 +583,7 @@ fn test_runner_runs_r1_lane_e_suite() { std::fs::read_to_string(&gate).unwrap_or_else(|err| panic!("read {gate:?}: {err}")); let dag = compile_clean(&source, "src/v3/compiler/tests/fixtures/r1_gates.dag"); let results = TestRunner::new(&dag).run_suite("r1_lane_e_suite"); - assert_eq!(results.len(), 2); + assert_eq!(results.len(), 3); assert_all_pass(&results); } From 4373514a181680f433f12d7474b12a58e8de0753 Mon Sep 17 00:00:00 2001 From: Brian Searls Date: Fri, 24 Apr 2026 21:38:44 -0400 Subject: [PATCH 17/21] fix(v3): pin T-Demo idempotency gate to sum-constructor ResolveError PR #764 blocking review: impossible_bug_idempotency_violation only required Contains("AppendEffect") while the failing port often surfaced a one-token ResolveError name, so the suite could pass without the intended variant-shape mismatch. - lower.rs: when a Call target is not a variant of an expected sum type (walk_to_disj_decl), emit a descriptive ResolveError instead of the callee token alone. - t_demo_fixtures: use AppendEffect() so lowering takes the Call path (bare AppendEffect parses as Var and cannot share this diagnostic without breaking Bool = y-style cases). - integration: assert the diagnostic substring; tighten FailsWithDiagnostic detail_contains to the new prefix. Made-with: Cursor --- src/v3/compiler/src/lower.rs | 9 ++++++++- src/v3/compiler/tests/integration.rs | 20 +++++++++++++++++++ .../compiler/tests/t_demo/t_demo_fixtures.dag | 12 ++++++----- 3 files changed, 35 insertions(+), 6 deletions(-) diff --git a/src/v3/compiler/src/lower.rs b/src/v3/compiler/src/lower.rs index e196d5a46dd..bb3df0a9c3e 100644 --- a/src/v3/compiler/src/lower.rs +++ b/src/v3/compiler/src/lower.rs @@ -4989,10 +4989,17 @@ fn lower_expr( }) .into_iter() .collect(); + let diagnostic_name = match expected_decl { + Some(exp) if walk_to_disj_decl(dag, exp).is_some() => format!( + "named constructor `{target}` is not a variant of the expected sum type `{}`", + declaration_display_name(dag, exp) + ), + _ => target.clone(), + }; dag.mark_unresolved( port, Diagnostic::ResolveError { - name: target.clone(), + name: diagnostic_name, span: span.clone(), fixes, }, diff --git a/src/v3/compiler/tests/integration.rs b/src/v3/compiler/tests/integration.rs index a4b81c23abb..858d44a1b26 100644 --- a/src/v3/compiler/tests/integration.rs +++ b/src/v3/compiler/tests/integration.rs @@ -159,6 +159,7 @@ mod t_demo_fixture_test { use v3_compiler::compile_to_dag; use v3_compiler::dag::Dag; use v3_compiler::test_runner::{ClaimResult, TestRunner}; + use v3_compiler::CompileError; const FIXTURE: &str = "src/v3/compiler/tests/t_demo/t_demo_fixtures.dag"; @@ -208,6 +209,25 @@ mod t_demo_fixture_test { } } + /// ROADMAP T-Demo / PR #764: `FailsWithDiagnostic.detail_contains` must pin the **sum + /// constructor** failure (`AppendEffect()` is not an `IdempotentShape` case), not a generic + /// `compose_effects` argument refinement message that omits `AppendEffect`. + #[test] + fn impossible_bug_idempotency_violation_emits_named_constructor_resolve_error() { + let src = "let bad_compose = compose_effects([{ operation_name: \"noop\", shape: IsIdempotent(AppendEffect()) }])\n"; + let err = compile_to_dag(src, "impossible_bug_idempotency.v3") + .expect_err("idempotency-violation witness should not compile"); + let CompileError::Semantic(dag) = err else { + panic!("expected Semantic(Dag) handoff, got {err:?}"); + }; + let msgs: Vec = dag.diagnostics().iter().map(|(_, d)| d.message()).collect(); + let needle = "named constructor `AppendEffect` is not a variant of the expected sum type"; + assert!( + msgs.iter().any(|m| m.contains(needle)), + "expected nullary-call lowering to reject AppendEffect as IdempotentShape payload; got: {msgs:?}" + ); + } + #[test] fn t_demo_impossible_bug_suite_r1_passes() { let source = fixture_source(); diff --git a/src/v3/compiler/tests/t_demo/t_demo_fixtures.dag b/src/v3/compiler/tests/t_demo/t_demo_fixtures.dag index 42fd73f660f..80fac197dc0 100644 --- a/src/v3/compiler/tests/t_demo/t_demo_fixtures.dag +++ b/src/v3/compiler/tests/t_demo/t_demo_fixtures.dag @@ -193,9 +193,11 @@ data fixture_integration_canonical: TestSuite = { // `impossible_bug_class_suite_r1` — two `FailsWithDiagnostic` receipts (ROADMAP.md:71-72); structural // cost bound lives in `t_demo_structural_cost_obligation_suite` (integration asserts `Fail`). -// `idempotency_violation`: `AppendEffect` is breaking (monoid append) and must not appear under -// `IsIdempotent`; the compiler rejects it as an `IdempotentShape` mismatch (`ResolveError` + fix -// text naming `IdempotentShape`). +// `idempotency_violation`: `AppendEffect()` is breaking (monoid append) and must not appear under +// `IsIdempotent`. Use nullary **call** syntax so lowering hits the `SurfaceExpr::Call` path (PR #764: +// bare `AppendEffect` parses as `Var` and produced a one-token `ResolveError` that was too weak +// for `FailsWithDiagnostic`). The diagnostic prefix pins the sum-constructor mismatch, not a generic +// upstream-only `compose_effects` failure. // `t_demo_structural_cost_obligation_suite` (below): nested `fold` + `CostBounded` vs structural // `cost_of` — runner `Fail` is the receipt (kept out of `impossible_bug_class_suite_r1` so that // suite is all `Pass` claims only). @@ -212,11 +214,11 @@ data impossible_bug_type_drift: TestClaim = { data impossible_bug_idempotency_violation: TestClaim = { name: "impossible_bug_class_suite_r1.idempotency_violation", - source: "let bad_compose = compose_effects([{ operation_name: \"noop\", shape: IsIdempotent(AppendEffect) }])\n", + source: "let bad_compose = compose_effects([{ operation_name: \"noop\", shape: IsIdempotent(AppendEffect()) }])\n", file_name: "impossible_bug_idempotency.v3", predicate: FailsWithDiagnostic({ kind: ResolveError, - detail_contains: Contains("AppendEffect") + detail_contains: Contains("named constructor `AppendEffect` is not a variant of the expected sum type") }), requires: [] } From 43d5b8d419ee8e39a45061cd59a2a588c513c5e9 Mon Sep 17 00:00:00 2001 From: Brian Searls Date: Fri, 24 Apr 2026 21:40:42 -0400 Subject: [PATCH 18/21] fix(v3): CostBounded failures cannot mimic tokenizer-only receipts PR #764: structural cost obligation must prove the nested-fold witness compiles and fails the bound on lens_cost::cost_of, not a spurious Tokenize/Parse handoff. - test_runner: prefix CostBounded compile/bind/miss failures with CostBounded: and explicit (structural cost check skipped) wording. - integration: assert bound-fail message starts with "cost "; add compile-cleanly ratchet for the witness source (synced with dag). - t_demo_fixtures: document integration sync + receipt shape. Made-with: Cursor --- src/v3/compiler/src/test_runner.rs | 15 +++++++++++--- src/v3/compiler/tests/integration.rs | 20 +++++++++++++++++-- .../compiler/tests/t_demo/t_demo_fixtures.dag | 7 +++++-- 3 files changed, 35 insertions(+), 7 deletions(-) diff --git a/src/v3/compiler/src/test_runner.rs b/src/v3/compiler/src/test_runner.rs index 461010421b5..bf1ef35e3aa 100644 --- a/src/v3/compiler/src/test_runner.rs +++ b/src/v3/compiler/src/test_runner.rs @@ -939,15 +939,24 @@ impl<'a> TestRunner<'a> { }; let dag = match compile_to_dag(&claim.source, &claim.file_name) { Ok(dag) => dag, - Err(err) => return ClaimResult::Fail(format!("source did not compile: {err:?}")), + Err(err) => { + return ClaimResult::Fail(format!( + "CostBounded: claim source did not compile (structural cost check skipped): {err:?}" + )); + } }; let Some(bind) = find_bind(&dag, bind_name, &claim.file_name) else { - return ClaimResult::Fail(format!("bind `{bind_name}` not found")); + return ClaimResult::Fail(format!( + "CostBounded: bind `{bind_name}` not found in `{}`", + claim.file_name + )); }; let actual = match cost_of(&dag, &bind.value) { CostLookup::Hit(actual) => actual, CostLookup::Miss => { - return ClaimResult::Fail(format!("missing cost for bind `{bind_name}`")); + return ClaimResult::Fail(format!( + "CostBounded: missing structural `cost_of` receipt for bind `{bind_name}`" + )); } }; if self.compare_cost(comparator, actual, *bound) { diff --git a/src/v3/compiler/tests/integration.rs b/src/v3/compiler/tests/integration.rs index 858d44a1b26..7d65b0290da 100644 --- a/src/v3/compiler/tests/integration.rs +++ b/src/v3/compiler/tests/integration.rs @@ -163,6 +163,9 @@ mod t_demo_fixture_test { const FIXTURE: &str = "src/v3/compiler/tests/t_demo/t_demo_fixtures.dag"; + /// Byte-sync with `t_demo_structural_cost_obligation_gate.source` in `t_demo_fixtures.dag`. + const T_DEMO_STRUCTURAL_COST_OBLIGATION_CLAIM_SOURCE: &str = "fn pair_score(xs: List) -> Int = fold(xs, 0, |outer, x| outer + fold(xs, 0, |inner, y| inner + x + y))\nlet complexity_demo_out: Int = pair_score(cons(1, singleton(2)))\n"; + fn fixture_source() -> String { let path = PathBuf::from(env!("CARGO_MANIFEST_DIR")) .join("../../..") @@ -242,6 +245,19 @@ mod t_demo_fixture_test { ); } + #[test] + fn t_demo_structural_cost_obligation_witness_compiles_cleanly() { + compile_to_dag( + T_DEMO_STRUCTURAL_COST_OBLIGATION_CLAIM_SOURCE, + "t_demo_structural_cost_obligation.v3", + ) + .unwrap_or_else(|err| { + panic!( + "T-Demo structural cost witness must compile so CostBounded exercises lens_cost::cost_of, not tokenizer/parse failures: {err:?}" + ) + }); + } + #[test] fn t_demo_structural_cost_obligation_suite_observes_cost_bound_fail() { let source = fixture_source(); @@ -255,8 +271,8 @@ mod t_demo_fixture_test { ); }; assert!( - msg.contains("cost") && msg.contains("did not satisfy"), - "unexpected CostBounded failure message: {msg}" + msg.starts_with("cost ") && msg.contains("did not satisfy bound"), + "unexpected CostBounded failure message (expected structural bound receipt, not compile skip): {msg}" ); } } diff --git a/src/v3/compiler/tests/t_demo/t_demo_fixtures.dag b/src/v3/compiler/tests/t_demo/t_demo_fixtures.dag index 80fac197dc0..5a1ad70cffb 100644 --- a/src/v3/compiler/tests/t_demo/t_demo_fixtures.dag +++ b/src/v3/compiler/tests/t_demo/t_demo_fixtures.dag @@ -199,8 +199,9 @@ data fixture_integration_canonical: TestSuite = { // for `FailsWithDiagnostic`). The diagnostic prefix pins the sum-constructor mismatch, not a generic // upstream-only `compose_effects` failure. // `t_demo_structural_cost_obligation_suite` (below): nested `fold` + `CostBounded` vs structural -// `cost_of` — runner `Fail` is the receipt (kept out of `impossible_bug_class_suite_r1` so that -// suite is all `Pass` claims only). +// `cost_of` — runner `Fail` is the receipt (`cost … did not satisfy bound …`, not a tokenizer +// proxy; integration pins compile + message shape — PR #764). Kept out of +// `impossible_bug_class_suite_r1` so that suite is all `Pass` claims only. data impossible_bug_type_drift: TestClaim = { name: "impossible_bug_class_suite_r1.transport_type_drift", source: "let drift: String = 1\n", @@ -231,6 +232,8 @@ data impossible_bug_class_suite_r1: TestSuite = { ] } +// When editing `source`, update `T_DEMO_STRUCTURAL_COST_OBLIGATION_CLAIM_SOURCE` in +// `tests/integration.rs` (`t_demo_fixture_test`). data t_demo_structural_cost_obligation_gate: TestClaim = { name: "t_demo_structural_cost_obligation.pair_score_too_deep", source: "fn pair_score(xs: List) -> Int = fold(xs, 0, |outer, x| outer + fold(xs, 0, |inner, y| inner + x + y))\nlet complexity_demo_out: Int = pair_score(cons(1, singleton(2)))\n", From 9d644d7f7d0b32c806161724d78b5fca17e5d948 Mon Sep 17 00:00:00 2001 From: Brian Searls Date: Fri, 24 Apr 2026 21:42:49 -0400 Subject: [PATCH 19/21] fix(v3): T-LaneE differential witness uses match/list/fold PR #764: r1_lane_e_differential_witness.v3 was only 1+2, so complexity_v3_matches_v2_oracle could pass without exercising branch, list, or fold in structural cost. Replace with Bool match + List + fold over cons cells (still value 3). Regenerate r1_gates.dag; update template comments. Made-with: Cursor --- src/v3/compiler/tests/fixtures/r1_gates.dag | 12 ++++++------ .../tests/fixtures/r1_gates.template.dag | 10 +++++----- .../fixtures/r1_lane_e_differential_witness.v3 | 17 ++++++++++++++--- 3 files changed, 25 insertions(+), 14 deletions(-) diff --git a/src/v3/compiler/tests/fixtures/r1_gates.dag b/src/v3/compiler/tests/fixtures/r1_gates.dag index 8b6bd77bcff..bda331b693e 100644 --- a/src/v3/compiler/tests/fixtures/r1_gates.dag +++ b/src/v3/compiler/tests/fixtures/r1_gates.dag @@ -198,14 +198,14 @@ data complexity_merge_sort_v3_matches_v2_oracle_gate: TestClaim = { requires: [] } -// Differential witness: trivial `1 + 2` bind — minimal smoke that host forward-fold and emit -// `lens_cost::cost_of` agree when almost nothing happens structurally. Nested control-flow parity -// is covered by `complexity_merge_sort_v3_matches_v2_oracle`; scalar structural depth by -// `complexity_merge_sort_is_nlogn`. D1 `apply_lens_declaration(cost_of)` on the canonical lens -// stays deferred (`Loop` / `UnimplementedLoopBound` in the lens graph). +// Differential witness: `match` + `fold` over a short list (`r1_lane_e_differential_witness.v3`) so +// `DifferentialEquals` compares host fold vs emit on **branch/list/fold** structure, not addition +// alone. Merge-sort parity is `complexity_merge_sort_v3_matches_v2_oracle`; scalar `cost_of` +// depth is `complexity_merge_sort_is_nlogn`. D1 `apply_lens_declaration(cost_of)` stays deferred +// (`Loop` / `UnimplementedLoopBound` in the lens graph). data complexity_v3_matches_v2_oracle_gate: TestClaim = { name: "complexity_v3_matches_v2_oracle", - source: "// Minimal structural-cost witness for `complexity_v3_matches_v2_oracle` (T-LaneE).\n// Runner compares a host forward-fold receipt to `lens_cost::cost_of` (see `test_runner.rs`).\n\nlet lane_e_diff_out: Int = 1 + 2\n", + source: "// T-LaneE differential witness for `complexity_v3_matches_v2_oracle`.\n// Uses `match`, list construction, and `fold` so host forward-fold and emit `lens_cost::cost_of`\n// both walk branch / list / fold structure — not a single-addition shortcut (PR #764).\n\nimport std.list { List, cons, empty, fold }\n\nlet lane_e_diff_pick: Bool = true\n\nlet lane_e_diff_xs: List = cons(1, cons(2, empty()))\n\nlet lane_e_diff_out: Int =\n match lane_e_diff_pick {\n True => fold(lane_e_diff_xs, 0, |acc, x| acc + x)\n False => 0\n }\n", file_name: "r1_lane_e_differential_witness.v3", predicate: DifferentialEquals( v3_program_cost, diff --git a/src/v3/compiler/tests/fixtures/r1_gates.template.dag b/src/v3/compiler/tests/fixtures/r1_gates.template.dag index bf1eac13897..e1b8ca6b502 100644 --- a/src/v3/compiler/tests/fixtures/r1_gates.template.dag +++ b/src/v3/compiler/tests/fixtures/r1_gates.template.dag @@ -198,11 +198,11 @@ data complexity_merge_sort_v3_matches_v2_oracle_gate: TestClaim = { requires: [] } -// Differential witness: trivial `1 + 2` bind — minimal smoke that host forward-fold and emit -// `lens_cost::cost_of` agree when almost nothing happens structurally. Nested control-flow parity -// is covered by `complexity_merge_sort_v3_matches_v2_oracle`; scalar structural depth by -// `complexity_merge_sort_is_nlogn`. D1 `apply_lens_declaration(cost_of)` on the canonical lens -// stays deferred (`Loop` / `UnimplementedLoopBound` in the lens graph). +// Differential witness: `match` + `fold` over a short list (`r1_lane_e_differential_witness.v3`) so +// `DifferentialEquals` compares host fold vs emit on **branch/list/fold** structure, not addition +// alone. Merge-sort parity is `complexity_merge_sort_v3_matches_v2_oracle`; scalar `cost_of` +// depth is `complexity_merge_sort_is_nlogn`. D1 `apply_lens_declaration(cost_of)` stays deferred +// (`Loop` / `UnimplementedLoopBound` in the lens graph). data complexity_v3_matches_v2_oracle_gate: TestClaim = { name: "complexity_v3_matches_v2_oracle", source: "R1_LANE_E_DIFFERENTIAL_WITNESS_V3_SPLICE_V1", diff --git a/src/v3/compiler/tests/fixtures/r1_lane_e_differential_witness.v3 b/src/v3/compiler/tests/fixtures/r1_lane_e_differential_witness.v3 index 280f7929b94..b729f840a39 100644 --- a/src/v3/compiler/tests/fixtures/r1_lane_e_differential_witness.v3 +++ b/src/v3/compiler/tests/fixtures/r1_lane_e_differential_witness.v3 @@ -1,4 +1,15 @@ -// Minimal structural-cost witness for `complexity_v3_matches_v2_oracle` (T-LaneE). -// Runner compares a host forward-fold receipt to `lens_cost::cost_of` (see `test_runner.rs`). +// T-LaneE differential witness for `complexity_v3_matches_v2_oracle`. +// Uses `match`, list construction, and `fold` so host forward-fold and emit `lens_cost::cost_of` +// both walk branch / list / fold structure — not a single-addition shortcut (PR #764). -let lane_e_diff_out: Int = 1 + 2 +import std.list { List, cons, empty, fold } + +let lane_e_diff_pick: Bool = true + +let lane_e_diff_xs: List = cons(1, cons(2, empty())) + +let lane_e_diff_out: Int = + match lane_e_diff_pick { + True => fold(lane_e_diff_xs, 0, |acc, x| acc + x) + False => 0 + } From a143861842dbfa983f8a639ee20c76e2de6814fb Mon Sep 17 00:00:00 2001 From: Brian Searls Date: Fri, 24 Apr 2026 21:44:13 -0400 Subject: [PATCH 20/21] docs(v3): rename Lane E bundled differential gate (PR #764) complexity_v3_matches_v2_oracle implied lane-wide oracle equivalence while merge_sort_out parity already lives on complexity_merge_sort_v3_matches_v2_oracle. Rename claim to lane_e_bundled_witness_host_emit_parity; update ROADMAP, r2-structure, briefs, fixture comments, and regenerated r1_gates.dag. Made-with: Cursor --- ROADMAP.md | 2 +- docs/briefs/r1-release-manager.md | 2 +- docs/briefs/r1-testgen-manager.md | 2 +- docs/r2-structure.md | 4 ++-- src/v3/compiler/tests/fixtures/r1_gates.dag | 17 ++++++++--------- .../tests/fixtures/r1_gates.template.dag | 15 +++++++-------- .../fixtures/r1_lane_e_differential_witness.v3 | 2 +- 7 files changed, 21 insertions(+), 23 deletions(-) diff --git a/ROADMAP.md b/ROADMAP.md index a6491f220f6..fb5104cb18a 100644 --- a/ROADMAP.md +++ b/ROADMAP.md @@ -61,7 +61,7 @@ This section lists gate names + schema-compilability tags; full `TestClaim` decl - **T-P0.** `p0_repeat_string_correct` [Day 1] · `p0_no_fabrication_sentinel` [ext] · `p0_rest_ops_aligned` [ext] - **T-Sub.** `sub_match_over_user_sum` [Day 1, landed PR #702] · `sub_type_alias_where_lowers` [ext, landed PR #703] · `sub_charclass_in_std_unicode` [ext, open: phase-2 reproduction/triage] - **T-Emit.** `emit_rust_fixtures_rustc_green` [ext: `ExecuteCommand`] · `emit_generic_bounds_survive` [ext] · `emit_omni_demo_fixtures_green` [ext: `ForAllTargets` + `ExecuteCommand`] -- **T-LaneE.** `complexity_merge_sort_is_nlogn` [ext: `LensOutputEquals`] · `complexity_merge_sort_v3_matches_v2_oracle` [ext: `DifferentialEquals`] · `complexity_v3_matches_v2_oracle` [ext: `DifferentialEquals`] +- **T-LaneE.** `complexity_merge_sort_is_nlogn` [ext: `LensOutputEquals`] · `complexity_merge_sort_v3_matches_v2_oracle` [ext: `DifferentialEquals`] · `lane_e_bundled_witness_host_emit_parity` [ext: `DifferentialEquals`] - **T-TestGen.** `testgen_structural_coverage` [ext] · `testgen_mock_backed_integration_safe` [ext: `MockBackedInvariant` — runner `NotYetImplemented` until `TestClaim.requires` carries at least one `ResourceReference`; M1(2.8) fixture list bodies) · `testgen_manual_claim_is_first_class` [ext] — T-TestGen also owns scoping the predicate shape for `[ext]` gates that other lanes consume; currently includes `lens_producer_files_remaining` for T-PB-A (enumeration declared in `sg0_census_test.rs` at scoping time). - **T-LensAPI.** `user_authored_lens_compiles` [Day 1] · `lens_composition_associative` [ext: `AlgebraicLaw`] · `lens_output_is_queryable_data` [ext] - **T-PB-A.** `pb_hand_rust_at_shim_floor` [ext] · `lens_producer_files_remaining` [ext — priority slice of the non-test census: hand-Rust files implementing lens producers, drops as each migrates to `.dag`; enumeration declared in `sg0_census_test.rs` when T-TestGen scopes the predicate] · `pb_self_compile_fixed_point` [ext] · `pb_compiler_std_ratchet_zero` [ext] — live baselines read from authorities; not frozen in this doc. Hand-Rust (**non-test subset**): SG-0 census (file-level + fragments ratchet) minus the test subset owned by T-PB-B → ≤5 irreducible-shim per `docs/design-pure-bootstrap.md`. Consolidation ratchet: compiler-local types not in positive-def set → 0. diff --git a/docs/briefs/r1-release-manager.md b/docs/briefs/r1-release-manager.md index 826002454d2..7c14f9ae06b 100644 --- a/docs/briefs/r1-release-manager.md +++ b/docs/briefs/r1-release-manager.md @@ -169,7 +169,7 @@ Lane-owner dispatch status (update as sub-deliverables close): **half-met** until the runner actually evaluates a mock-backed invariant claim, not just routes it. - Substrate T-LaneE (`complexity_merge_sort_is_nlogn` / - `complexity_v3_matches_v2_oracle`) — pending. + `lane_e_bundled_witness_host_emit_parity`) — pending. - Surface T-Emit (`emit_omni_demo_fixtures_green`) — pending. - PR #689 closed as premature (docs/thesis/ is director-owned per `doc-authority.md`). Narrative holds until at least one upstream diff --git a/docs/briefs/r1-testgen-manager.md b/docs/briefs/r1-testgen-manager.md index 0000c4cd91f..e728242aeb0 100644 --- a/docs/briefs/r1-testgen-manager.md +++ b/docs/briefs/r1-testgen-manager.md @@ -229,7 +229,7 @@ Lane-owner dispatch status (update as sub-deliverables close): - [x] `LensOutputEquals` predicate (Substrate T-LaneE consumer — `complexity_merge_sort_is_nlogn`) — landed PR #678 - [x] `DifferentialEquals` predicate (Substrate T-LaneE consumer - — `complexity_v3_matches_v2_oracle`) — landed PR #678 + — `lane_e_bundled_witness_host_emit_parity`) — landed PR #678 Decisions log (append as they happen): diff --git a/docs/r2-structure.md b/docs/r2-structure.md index 9a1e26f418a..196885857de 100644 --- a/docs/r2-structure.md +++ b/docs/r2-structure.md @@ -25,7 +25,7 @@ Post-R2 is external work (adoption, documentation, community, ecosystem modeling ## Goals -**Gate-ownership discipline.** Every R1 gate listed in `ROADMAP.md §"Lane acceptance — .dag gates"` closes in R1 under the locked all-R1-gates-green criterion (see R1 closure criteria below). That means concerns gated there — **lens purity** (`lens_producer_files_remaining` on T-PB-A via PR #752), **self-hosting shim-floor close** (T-PB-A `pb_hand_rust_at_shim_floor` + `pb_compiler_std_ratchet_zero` + T-PB-B `pb_rust_tests_outside_residual_zero`), and **E-family carrier port closure** (the T-LaneE critical path enabling `complexity_merge_sort_is_nlogn` + `complexity_merge_sort_v3_matches_v2_oracle` + `complexity_v3_matches_v2_oracle`) — are **R1 scope, not R2**. R2 does not duplicate release authority over gates ROADMAP already assigns to R1 lanes. +**Gate-ownership discipline.** Every R1 gate listed in `ROADMAP.md §"Lane acceptance — .dag gates"` closes in R1 under the locked all-R1-gates-green criterion (see R1 closure criteria below). That means concerns gated there — **lens purity** (`lens_producer_files_remaining` on T-PB-A via PR #752), **self-hosting shim-floor close** (T-PB-A `pb_hand_rust_at_shim_floor` + `pb_compiler_std_ratchet_zero` + T-PB-B `pb_rust_tests_outside_residual_zero`), and **E-family carrier port closure** (the T-LaneE critical path enabling `complexity_merge_sort_is_nlogn` + `complexity_merge_sort_v3_matches_v2_oracle` + `lane_e_bundled_witness_host_emit_parity`) — are **R1 scope, not R2**. R2 does not duplicate release authority over gates ROADMAP already assigns to R1 lanes. Under that discipline, R2's goals are the Tier-1 thesis claims that are *not* gated in R1 today: @@ -86,7 +86,7 @@ Continues `docs/briefs/grounding-manager.md` (refreshed for R2 scope on promotio **Lanes deliberately absent (R1 gates, closed by R1 lane acceptance):** - T-LensMigration / `lens_producer_files_remaining` — R1 T-PB-A gate per PR #752. - T-ShimFloor / `pb_hand_rust_at_shim_floor` / `pb_compiler_std_ratchet_zero` / `pb_rust_tests_outside_residual_zero` — R1 T-PB-A + T-PB-B gates. -- T-EFamilyClose — R1 T-LaneE's critical-path carrier work (E-T, E-C, E-I, E-P, E-M sub-lanes), enabling the R1 `complexity_merge_sort_is_nlogn` + `complexity_merge_sort_v3_matches_v2_oracle` + `complexity_v3_matches_v2_oracle` gates. All E-family carrier-port work closes in R1; only the §6a metadata-pick residual inherits to R2 (Goal 5). +- T-EFamilyClose — R1 T-LaneE's critical-path carrier work (E-T, E-C, E-I, E-P, E-M sub-lanes), enabling the R1 `complexity_merge_sort_is_nlogn` + `complexity_merge_sort_v3_matches_v2_oracle` + `lane_e_bundled_witness_host_emit_parity` gates. All E-family carrier-port work closes in R1; only the §6a metadata-pick residual inherits to R2 (Goal 5). - T-TestGen-tail (`testgen_mock_backed_integration_safe` / `MockBackedInvariant` wiring) — R1 T-TestGen gate per `ROADMAP.md §"Lane acceptance — .dag gates"`. Closes in R1. R2 does not re-own any of the above; under all-R1-gates-green R1 closure, those gates ARE the close conditions and R2 inherits nothing there (except Goal 5's §6a residual, which was not an R1 gate). diff --git a/src/v3/compiler/tests/fixtures/r1_gates.dag b/src/v3/compiler/tests/fixtures/r1_gates.dag index bda331b693e..b0eb4759a76 100644 --- a/src/v3/compiler/tests/fixtures/r1_gates.dag +++ b/src/v3/compiler/tests/fixtures/r1_gates.dag @@ -198,14 +198,13 @@ data complexity_merge_sort_v3_matches_v2_oracle_gate: TestClaim = { requires: [] } -// Differential witness: `match` + `fold` over a short list (`r1_lane_e_differential_witness.v3`) so -// `DifferentialEquals` compares host fold vs emit on **branch/list/fold** structure, not addition -// alone. Merge-sort parity is `complexity_merge_sort_v3_matches_v2_oracle`; scalar `cost_of` -// depth is `complexity_merge_sort_is_nlogn`. D1 `apply_lens_declaration(cost_of)` stays deferred -// (`Loop` / `UnimplementedLoopBound` in the lens graph). -data complexity_v3_matches_v2_oracle_gate: TestClaim = { - name: "complexity_v3_matches_v2_oracle", - source: "// T-LaneE differential witness for `complexity_v3_matches_v2_oracle`.\n// Uses `match`, list construction, and `fold` so host forward-fold and emit `lens_cost::cost_of`\n// both walk branch / list / fold structure — not a single-addition shortcut (PR #764).\n\nimport std.list { List, cons, empty, fold }\n\nlet lane_e_diff_pick: Bool = true\n\nlet lane_e_diff_xs: List = cons(1, cons(2, empty()))\n\nlet lane_e_diff_out: Int =\n match lane_e_diff_pick {\n True => fold(lane_e_diff_xs, 0, |acc, x| acc + x)\n False => 0\n }\n", +// Bundled differential witness (`lane_e_diff_out` in `r1_lane_e_differential_witness.v3`): `match` + +// `fold` over a short list — host fold vs emit on branch/list/fold structure. **Not** the lane-wide +// “v3 oracle vs v2 oracle” receipt; merge-sort / `merge_sort_out` parity is +// `complexity_merge_sort_v3_matches_v2_oracle` (PR #764 api-review rename). +data lane_e_bundled_witness_host_emit_parity_gate: TestClaim = { + name: "lane_e_bundled_witness_host_emit_parity", + source: "// T-LaneE differential witness for `lane_e_bundled_witness_host_emit_parity` (bundled `lane_e_diff_out` program).\n// Uses `match`, list construction, and `fold` so host forward-fold and emit `lens_cost::cost_of`\n// both walk branch / list / fold structure — not a single-addition shortcut (PR #764).\n\nimport std.list { List, cons, empty, fold }\n\nlet lane_e_diff_pick: Bool = true\n\nlet lane_e_diff_xs: List = cons(1, cons(2, empty()))\n\nlet lane_e_diff_out: Int =\n match lane_e_diff_pick {\n True => fold(lane_e_diff_xs, 0, |acc, x| acc + x)\n False => 0\n }\n", file_name: "r1_lane_e_differential_witness.v3", predicate: DifferentialEquals( v3_program_cost, @@ -220,6 +219,6 @@ data r1_lane_e_suite: TestSuite = { claims: [ complexity_merge_sort_is_nlogn_gate, complexity_merge_sort_v3_matches_v2_oracle_gate, - complexity_v3_matches_v2_oracle_gate + lane_e_bundled_witness_host_emit_parity_gate ] } diff --git a/src/v3/compiler/tests/fixtures/r1_gates.template.dag b/src/v3/compiler/tests/fixtures/r1_gates.template.dag index e1b8ca6b502..e52f71c963e 100644 --- a/src/v3/compiler/tests/fixtures/r1_gates.template.dag +++ b/src/v3/compiler/tests/fixtures/r1_gates.template.dag @@ -198,13 +198,12 @@ data complexity_merge_sort_v3_matches_v2_oracle_gate: TestClaim = { requires: [] } -// Differential witness: `match` + `fold` over a short list (`r1_lane_e_differential_witness.v3`) so -// `DifferentialEquals` compares host fold vs emit on **branch/list/fold** structure, not addition -// alone. Merge-sort parity is `complexity_merge_sort_v3_matches_v2_oracle`; scalar `cost_of` -// depth is `complexity_merge_sort_is_nlogn`. D1 `apply_lens_declaration(cost_of)` stays deferred -// (`Loop` / `UnimplementedLoopBound` in the lens graph). -data complexity_v3_matches_v2_oracle_gate: TestClaim = { - name: "complexity_v3_matches_v2_oracle", +// Bundled differential witness (`lane_e_diff_out` in `r1_lane_e_differential_witness.v3`): `match` + +// `fold` over a short list — host fold vs emit on branch/list/fold structure. **Not** the lane-wide +// “v3 oracle vs v2 oracle” receipt; merge-sort / `merge_sort_out` parity is +// `complexity_merge_sort_v3_matches_v2_oracle` (PR #764 api-review rename). +data lane_e_bundled_witness_host_emit_parity_gate: TestClaim = { + name: "lane_e_bundled_witness_host_emit_parity", source: "R1_LANE_E_DIFFERENTIAL_WITNESS_V3_SPLICE_V1", file_name: "r1_lane_e_differential_witness.v3", predicate: DifferentialEquals( @@ -220,6 +219,6 @@ data r1_lane_e_suite: TestSuite = { claims: [ complexity_merge_sort_is_nlogn_gate, complexity_merge_sort_v3_matches_v2_oracle_gate, - complexity_v3_matches_v2_oracle_gate + lane_e_bundled_witness_host_emit_parity_gate ] } diff --git a/src/v3/compiler/tests/fixtures/r1_lane_e_differential_witness.v3 b/src/v3/compiler/tests/fixtures/r1_lane_e_differential_witness.v3 index b729f840a39..1122ce5a32a 100644 --- a/src/v3/compiler/tests/fixtures/r1_lane_e_differential_witness.v3 +++ b/src/v3/compiler/tests/fixtures/r1_lane_e_differential_witness.v3 @@ -1,4 +1,4 @@ -// T-LaneE differential witness for `complexity_v3_matches_v2_oracle`. +// T-LaneE differential witness for `lane_e_bundled_witness_host_emit_parity` (bundled `lane_e_diff_out` program). // Uses `match`, list construction, and `fold` so host forward-fold and emit `lens_cost::cost_of` // both walk branch / list / fold structure — not a single-addition shortcut (PR #764). From 18fe9d265aa80b0f156de2e431579b4e83828d51 Mon Sep 17 00:00:00 2001 From: Brian Searls Date: Fri, 24 Apr 2026 21:45:26 -0400 Subject: [PATCH 21/21] docs: ingest PR #764 meta-review (efbb9787) as tracked dissolution MIME-Version: 1.0 Content-Type: text/plain; charset=UTF-8 Content-Transfer-Encoding: 8bit - ROADMAP: scheduled cleanups item 4 — SHIP_WITH_DEBT checklist (M1/D1/DB-15) and current Lane E receipt names (merge_sort_out differential + bundled lane_e_diff_out witness; not 1+2). - Briefs: align T-LaneE / DifferentialEquals citations with PR #764. Made-with: Cursor --- ROADMAP.md | 2 ++ docs/briefs/r1-release-manager.md | 5 +++-- docs/briefs/r1-testgen-manager.md | 4 ++-- 3 files changed, 7 insertions(+), 4 deletions(-) diff --git a/ROADMAP.md b/ROADMAP.md index fb5104cb18a..5ad5275ea8e 100644 --- a/ROADMAP.md +++ b/ROADMAP.md @@ -84,6 +84,8 @@ Day-1 PR #717 landed explicit `LensOutputEquals` dispatch and fixtures with **no 3. **P2 parallel lens text** — **Done (D4):** `v3-compiler/build.rs` splices `src/v3/lenses/named_function_count.dag` into generated `r1_gates.dag` from hand-edited `r1_gates.template.dag`; `m1_5_user_authored_lens_gate_test` still ratchets lowered `source` against `include_str!(.../named_function_count.dag)`. **Follow-on:** dissolve fixture-local `fn count_named_bind` / `fn named_function_count` stubs when `DeclarationRef` can resolve the lens from `program_dag` alone; optional same treatment for `lens_composition_associative_gate.source` vs `lens_composition_associative_witness.dag`. +4. **PR #764 T-LaneE / test-runner scaffolds (meta-review `efbb9787`, SHIP_WITH_DEBT)** — Ingested 2026-04-25: do **not** re-litigate these as ad-hoc PR nits; track dissolution here. Checklist: structural `TestClaim` bind / input carriers (retire `cost_bind_for_claim_file` + `r1_lens_output_input_from_program` string keying, M1(2.8)); D1 `apply_lens_declaration(cost_of)` then delete `lane_e_host_*`; `Lookup` literals in `data` bodies; DB-15 `requires` with real `ResourceReference` rows for mock-backed `Pass` (until then NYI on empty `requires` is intentional); optional `.dag`-native failed-obligation predicate for T-Demo structural cost. **Receipt shape today:** `complexity_merge_sort_v3_matches_v2_oracle` is `DifferentialEquals` on `merge_sort_out` (`r1_merge_sort_pair.v3`); `lane_e_bundled_witness_host_emit_parity` is the bundled `lane_e_diff_out` witness (`r1_lane_e_differential_witness.v3` — `match` / list / `fold`, not the early `1+2` smoke). + ### Dependency DAG ``` diff --git a/docs/briefs/r1-release-manager.md b/docs/briefs/r1-release-manager.md index 7c14f9ae06b..228c506c2c7 100644 --- a/docs/briefs/r1-release-manager.md +++ b/docs/briefs/r1-release-manager.md @@ -168,8 +168,9 @@ Lane-owner dispatch status (update as sub-deliverables close): Trigger remains **half-met** until the runner actually evaluates a mock-backed invariant claim, not just routes it. - - Substrate T-LaneE (`complexity_merge_sort_is_nlogn` / - `lane_e_bundled_witness_host_emit_parity`) — pending. + - Substrate T-LaneE (`complexity_merge_sort_is_nlogn`, + `complexity_merge_sort_v3_matches_v2_oracle`, + `lane_e_bundled_witness_host_emit_parity` — `r1_lane_e_suite`) — landed PR #764; dissolution checklist ROADMAP `Scheduled cleanups` item 4. - Surface T-Emit (`emit_omni_demo_fixtures_green`) — pending. - PR #689 closed as premature (docs/thesis/ is director-owned per `doc-authority.md`). Narrative holds until at least one upstream diff --git a/docs/briefs/r1-testgen-manager.md b/docs/briefs/r1-testgen-manager.md index e728242aeb0..0147d13c5fb 100644 --- a/docs/briefs/r1-testgen-manager.md +++ b/docs/briefs/r1-testgen-manager.md @@ -227,9 +227,9 @@ Lane-owner dispatch status (update as sub-deliverables close): - [x] `ExecuteCommand` predicate (Surface T-Emit consumer) — landed PR #678 - [x] `ForAllTargets` predicate (Surface T-Emit consumer) — landed PR #678 - [x] `LensOutputEquals` predicate (Substrate T-LaneE consumer - — `complexity_merge_sort_is_nlogn`) — landed PR #678 + — `complexity_merge_sort_is_nlogn`) — landed PR #764 (suite: `r1_lane_e_suite`) - [x] `DifferentialEquals` predicate (Substrate T-LaneE consumer - — `lane_e_bundled_witness_host_emit_parity`) — landed PR #678 + — `complexity_merge_sort_v3_matches_v2_oracle`, `lane_e_bundled_witness_host_emit_parity`) — landed PR #764 Decisions log (append as they happen):