diff --git a/ROADMAP.md b/ROADMAP.md index 9745009cf05..d990b775971 100644 --- a/ROADMAP.md +++ b/ROADMAP.md @@ -61,15 +61,15 @@ 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`~~ — phase-1 landed PR #693; **phase-2 reclassified to R2 substrate-capability** (top-level `ValueBody` list/sum + `std.unicode` bootstrap/load-set per Class 5 Gap 3 row below) — no longer an R1 T-Sub gate; tracked in `docs/r2-structure.md` Goal 3 / T-Substrate as a 4th scoped sub-lane (consumer: tokenizer) - **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-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. - **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] — 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`), 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. @@ -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 826002454d2..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` / - `complexity_v3_matches_v2_oracle`) — 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 0000c4cd91f..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 - — `complexity_v3_matches_v2_oracle`) — 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): diff --git a/docs/r2-structure.md b/docs/r2-structure.md index 8dab9759dea..6dc7ae7fff1 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` + `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: @@ -87,7 +87,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` + `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 — with two named exceptions: diff --git a/src/v3/compiler/build.rs b/src/v3/compiler/build.rs index f10355020e4..a7bb332023d 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,36 @@ 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 `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"; + + 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 +185,53 @@ 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!( + "failed to read R1 Lane E differential witness fixture {}: {}", + lane_e_diff_witness_v3.display(), + e + ) + }); + + let lens_count = template.matches(LENS_SPLICE_SENTINEL).count(); + if lens_count != 1 { panic!( - "{} must contain exactly one `{SPLICE_SENTINEL}` (found {splice_count})", + "{} must contain exactly one `{LENS_SPLICE_SENTINEL}` for named_function_count lens (found {lens_count})", template_path.display() ); } - let escaped = escape_dag_double_quoted_body(&lens); - let generated = template.replace(SPLICE_SENTINEL, &escaped); + 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 = + 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/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/src/test_runner.rs b/src/v3/compiler/src/test_runner.rs index cdaecf8139e..bf1ef35e3aa 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, Path, PortId, PortState, + TypeConnective, ValueBody, }; use crate::diagnostics::Diagnostic; use crate::lens_apply::{ @@ -22,6 +22,187 @@ 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`] (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" +)); + +/// 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`). **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"), + "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, + } +} + +/// 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 { + // 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); + acc.insert(0, entry); + } + acc +} + +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) + } + } + } +} + +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)), + }, + } +} + +/// 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, + bind_port: PortId, +) -> Result { + match lineage_name { + "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`)" + )), + } +} + #[derive(Debug, Clone, PartialEq, Eq)] pub enum ClaimResult { Pass, @@ -175,8 +356,26 @@ 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), + "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" )), @@ -318,6 +517,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 +536,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 +568,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 +751,123 @@ 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 + )); + }; + + 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})" + )); + } + + // 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, + bind.value, + ) { + 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, + bind.value, + ) { + Ok(v) => v, + Err(msg) => return ClaimResult::Fail(msg), + }; + + if subject_out == oracle_out { + ClaimResult::Pass + } else { + ClaimResult::Fail(format!( + "DifferentialEquals: subject `{subject_lineage}` output {subject_out:?} != oracle `{oracle_lineage}` output {oracle_out:?} (host forward-fold vs `lens_cost::cost_of`)" + )) + } + } + 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). @@ -581,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) { @@ -599,9 +966,13 @@ impl<'a> TestRunner<'a> { } } + /// 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, + claim: &TestClaimValue, payload: &[FieldValue], ) -> ClaimResult { let [subject, invariant] = payload else { @@ -610,17 +981,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..b0eb4759a76 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,19 @@ 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 (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() + +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 +165,60 @@ 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. `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", + file_name: "r1_merge_sort_pair.v3", + predicate: LensOutputEquals( + cost_of, + r1_lens_output_input_from_program, + complexity_merge_sort_expected_cost + ), + requires: [] +} + +// 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: [] +} + +// 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, + 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_merge_sort_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 96171dc22a1..e52f71c963e 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,19 @@ 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 (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() + +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 +165,60 @@ 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. `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: "R1_MERGE_SORT_PAIR_V3_SPLICE_V1", + file_name: "r1_merge_sort_pair.v3", + predicate: LensOutputEquals( + cost_of, + r1_lens_output_input_from_program, + complexity_merge_sort_expected_cost + ), + requires: [] +} + +// 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: [] +} + +// 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( + 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_merge_sort_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 new file mode 100644 index 00000000000..1122ce5a32a --- /dev/null +++ b/src/v3/compiler/tests/fixtures/r1_lane_e_differential_witness.v3 @@ -0,0 +1,15 @@ +// 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). + +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 + } 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..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,25 +1,22 @@ -// 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. +// R1 gate for `testgen_mock_backed_integration_safe` (ROADMAP). `MockBackedInvariant` names the +// `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 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..7d65b0290da 100644 --- a/src/v3/compiler/tests/integration.rs +++ b/src/v3/compiler/tests/integration.rs @@ -159,9 +159,13 @@ 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"; + /// 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("../../..") @@ -207,6 +211,70 @@ 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(); + let dag = compile_fixture(&source); + let results = TestRunner::new(&dag).run_suite("impossible_bug_class_suite_r1"); + 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_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(); + 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.starts_with("cost ") && msg.contains("did not satisfy bound"), + "unexpected CostBounded failure message (expected structural bound receipt, not compile skip): {msg}" + ); + } } 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..eae66d8983c 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,30 @@ 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!( + 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] -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 +446,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 +515,19 @@ data suite: TestSuite = { ); } +#[test] +fn r1_canonical_complexity_lens_bytes_include_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] fn test_runner_dispatches_r1_gates_lens_output_equals_claim() { let manifest_dir = PathBuf::from(env!("CARGO_MANIFEST_DIR")); @@ -541,6 +575,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(), 3); + 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..5a1ad70cffb 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,53 @@ // 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 { Behavior, ComparisonOp, Dag, PortId } +import std.verification { + AnyDetail, + Compiles, + Contains, + CostBounded, + FailsWithDiagnostic, + LensOutputEquals, + PortHasState, + Resolved, + TestClaim, + TestSuite, + 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 +72,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 +146,103 @@ 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: [] +} + +// 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_type_drift_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_type_drift_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` — 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`. 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 (`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", + 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: "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("named constructor `AppendEffect` is not a variant of the expected sum type") + }), + requires: [] +} + +data impossible_bug_class_suite_r1: TestSuite = { + name: "impossible_bug_class_suite_r1", + claims: [ + impossible_bug_type_drift, + impossible_bug_idempotency_violation + ] +} + +// 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", + 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] +}