diff --git a/.github/workflows/ci.yml b/.github/workflows/ci.yml index 692f639f994..8f2934e7a41 100644 --- a/.github/workflows/ci.yml +++ b/.github/workflows/ci.yml @@ -236,13 +236,10 @@ jobs: # `pub fn cost_of(&self, port: PortId) -> usize` wrapper that # shadowed the generated `CostLookup` carrier. # - # Scope: every `src/v3/compiler/src/lens_*.rs` wrapper except - # `lens_depth.rs` (hand-written legacy lens, not migrated - # from .dag, so out of L-8 scope). `*_generated.rs` files are - # also scanned — they should never contain a collapsing - # wrapper, and catching one there would mean the emitter - # regressed. - wrappers=$(ls src/v3/compiler/src/lens_*.rs 2>/dev/null | grep -v "/lens_depth.rs$" || true) + # Scope: every `src/v3/compiler/src/lens_*.rs` file (hand-written + # and `*_generated.rs` — catching a collapsed wrapper in generated + # code would mean the emitter regressed). + wrappers=$(ls src/v3/compiler/src/lens_*.rs 2>/dev/null || true) if [ -z "$wrappers" ]; then echo "L-8: no lens wrapper files to scan" exit 0 diff --git a/docs/briefs/r1-selfhosting-manager.md b/docs/briefs/r1-selfhosting-manager.md index c8f095d78be..a986eedd715 100644 --- a/docs/briefs/r1-selfhosting-manager.md +++ b/docs/briefs/r1-selfhosting-manager.md @@ -117,8 +117,10 @@ Lane-owner dispatch status (update as sub-deliverables close): T-TestGen extensions land **T-PB-B:** -- [x] T-PB-B-1 — Landed `src/v3/compiler/tests/dag/*.dag` + compile-only smoke - (`t_pb_b_1_tests_dag_smoke_test`); brief `docs/briefs/t-pb-b-1.md`. +- [x] T-PB-B-1 — Landed `src/v3/compiler/tests/dag/*.dag` + brief + `docs/briefs/t-pb-b-1.md` (former compile-only smoke + `t_pb_b_1_tests_dag_smoke_test` retired as redundant with + `t_pb_b_1_dag_runner_test` — 2026-04-24). **Not** Rust test deletion and **not** `pb_*` — those stay unchecked below until Testgen signs off. - [x] T-PB-B-1 — Runner-backed integration test landed (PR #736, @@ -136,10 +138,10 @@ Lane-owner dispatch status (update as sub-deliverables close): previous row; `contract_diagnostic_smoke.v3` + `contract_port_cost_smoke.v3`) - [x] Identify and scope the two TESTING.md residual categories per-test (extended D/G/A/B matrix in Brief D) -- [ ] Land **Rust deletions** for the three T-PB-B-1 claim shapes once Testgen - signals on checklist item (4) first-deletion batch (declarative data + - compile smoke + runner-backed evaluation for these three suites already - landed via PR #736 — see `docs/briefs/t-pb-b-1.md`) +- [ ] Land **Rust deletions** for the remaining T-PB-B-1 / thesis inventory + (checklist item (4) follow-on) once Testgen records sign-off in + `docs/briefs/r1-testgen-manager.md` (first slice: redundant compile-smoke + file **landed** 2026-04-24; see *Decisions log*). - [ ] `pb_test_file_generated_from_dag` + `pb_rust_tests_outside_residual_zero` predicates evaluate true @@ -161,8 +163,8 @@ Decisions log (append as they happen): floor read from `src/v3/compiler/tests/integration/sg0_census_test.rs`; the ≤5 irreducible-shim target not yet reached. - 2026-04-24: **T-PB-B-1** — landed `src/v3/compiler/tests/dag/*.dag` (`data` `TestClaim` / - `TestSuite` per `std.verification`) + `t_pb_b_1_tests_dag_smoke_test`; Rust tests not - deleted; Testgen runner / `pb_*` coordination still open (`docs/briefs/t-pb-b-1.md`). + `TestSuite` per `std.verification`); redundant compile-smoke file later + retired. Further Rust deletions / `pb_*` coordination: `docs/briefs/t-pb-b-1.md`. - 2026-04-23: **Brief D** (`docs/briefs/t-pb-b-brief-d.md`) — extended T-PB-B inventory + D/G/A/B matrix + draft `TestClaim` fixtures (`tests/fixtures/t_pb_b_brief_d/*.v3`); compile smoke via `t_pb_b_brief_d_fixture_smoke_test` (no `pb_*`, Rust tests unchanged). diff --git a/docs/briefs/r1-testgen-manager.md b/docs/briefs/r1-testgen-manager.md index 0000c4cd91f..684df91d3a0 100644 --- a/docs/briefs/r1-testgen-manager.md +++ b/docs/briefs/r1-testgen-manager.md @@ -93,8 +93,9 @@ compose. When this closes, the R1 release gates themselves signal, then converts pipeline / contract tests. Notify Self-hosting when the runner lands. **Landed batch (runner-backed):** `docs/briefs/t-pb-b-1.md` + `src/v3/compiler/tests/dag/` — - `t_pb_b_1_dag_runner_test` evaluates the landed suites (PR #736); - compile-smoke counterpart is `t_pb_b_1_tests_dag_smoke_test`. + `t_pb_b_1_dag_runner_test` evaluates the landed suites (PR #736); the + former compile-smoke-only `t_pb_b_1_tests_dag_smoke_test` is **retired** + (redundant with the runner test — *Decisions log* 2026-04-24). **Pre–Rust-deletion checklist (single source — edit here only; do not fork a competing numbered list in other briefs):** (1) **[done, PR #736]** Runner accepts v3 `.dag` modules under @@ -111,9 +112,15 @@ compose. When this closes, the R1 release gates themselves `t_pb_b_1_contract_port_cost.dag`; standalone `data _: TestPredicate = …` bodies remain NYI under the same class-5 restriction. Receipt paragraph in `docs/briefs/t-pb-b-1.md`. - (4) **First Rust deletion batch — prep, not yet signed off.** Target - shape: one thin `Compiles`-only duplicate whose claim is already - covered by a landed `.dag` suite evaluated under + (4) **First Rust deletion batch — partial sign-off (2026-04-24).** The + three `#[test]` functions in the former `t_pb_b_1_tests_dag_smoke_test.rs` + (redundant compile-only coverage for the landed `tests/dag/*.dag` modules) + are **deleted**; replacement coverage and the `#[test]` → `TestClaim` + mapping are recorded in the *Decisions log* below. **Still open** for the + remainder of the inventory until a follow-on sign-off entry lands + (same four-point guard). Target shape for the **next** slice: one thin + `Compiles`-only duplicate (or `thesis_validation_test.rs` subset) whose + claim is already covered by a landed `.dag` suite evaluated under `t_pb_b_1_dag_runner_test`. Candidate inventory (under `src/v3/compiler/tests/integration/`, registered in `integration.rs` and enumerated in `sg0_census_test.rs`): @@ -233,7 +240,37 @@ Lane-owner dispatch status (update as sub-deliverables close): Decisions log (append as they happen): -- 2026-04-24: **Pre–Rust-deletion checklist item (4) prepped, not signed +- 2026-04-24 (Lane B / #763): **Pre–Rust-deletion checklist item (4) — first slice signed + off (redundant T-PB-B-1 compile-smoke).** Receipts (1)–(3) re-verified + green (`cargo test -p v3-compiler t_pb_b_1_dag_runner_test`, + `test_runner_data_bodies_reject_requires_empty_call_today`); PR #735 + merged on main (`cf59f2288` — `CostBounded` witness for the candidate + claims is stable). **Deleted Rust tests** (file + `t_pb_b_1_tests_dag_smoke_test.rs` removed) and **replacement**: + `t_pb_b_1_dag_runner_test::lower` keeps the **empty module diagnostics** + compile-smoke receipt for each declaring `tests/dag/*.dag` harness, then + `TestRunner::run_suite` proves embedded `TestClaim` predicates (`ClaimResult::Pass` + for every claim — orthogonal to the outer harness diagnostic check). **Implementation + (current `lower` in `t_pb_b_1_dag_runner_test.rs`):** only `Ok(dag)` returns, with an + explicit `assert!(dag.diagnostics().is_empty())` on that arm; `Err(Semantic(_))` **panics** + (not a success path) — the declaring harness must compile with an empty module + diagnostic table before `run_suite` runs. + - `t_pb_b_1_pipeline_smoke_dag_lowers_cleanly` → + `t_pb_b_1_dag_runner_test::t_pb_b_1_pipeline_smoke_suite_passes_through_runner` + / suite `suite_pipeline_pipe_unary` / claim `claim_pipe_unary_compiles` + ("pipe unary call program compiles"). + - `t_pb_b_1_contract_diagnostic_smoke_dag_lowers_cleanly` → + `t_pb_b_1_dag_runner_test::t_pb_b_1_contract_diagnostic_smoke_suite_passes_through_runner` + / suite `suite_contract_diagnostic_negatives` / claim `claim_bool_int_rejected` + ("Bool annotation rejects Int literal"). + - `t_pb_b_1_contract_port_cost_dag_lowers_cleanly` → + `t_pb_b_1_dag_runner_test::t_pb_b_1_contract_port_cost_suite_passes_through_runner` + / suite `suite_contract_port_and_cost` / claims `claim_answer_resolved`, + `claim_answer_cost_bounded`. **Follow-on** first-batch work + (`thesis_validation_test.rs` subset; `pipe_desugar.rs` still excluded) + remains under the 2026-04-24 inventory + four-point guard until a + separate log entry names each `#[test]` → `TestClaim` pair. +- 2026-04-24 (PR #751): **Pre–Rust-deletion checklist item (4) prepped, not signed off.** Candidate inventory narrowed — `pipe_desugar.rs` **excluded** from first batch (asserts `Transform` target / input arity / literal order / return shape; `t_pb_b_1_pipeline_smoke.dag` only witnesses diff --git a/docs/briefs/t-pb-b-1.md b/docs/briefs/t-pb-b-1.md index 03f30bd4f7e..a55eadddda4 100644 --- a/docs/briefs/t-pb-b-1.md +++ b/docs/briefs/t-pb-b-1.md @@ -5,10 +5,9 @@ ## Landed in repo (this PR path) - **`src/v3/compiler/tests/dag/*.dag`** — `TestClaim` / `TestSuite` as `data` declarations (`module v3.compiler.tests.t_pb_b_1.*`), schema from `src/v3/std/verification.dag`. -- **`t_pb_b_1_tests_dag_smoke_test`** — `compile_to_dag` smoke only (no predicate evaluation, no `pb_*`). -- **`t_pb_b_1_dag_runner_test`** (PR #736) — runner evaluates each landed `TestSuite`'s claims via `TestRunner::run_suite`; covers `Compiles`, `FailsWithDiagnostic{TypeMismatch}`, `PortHasState`, `CostBounded`. See *Receipts for pre–Rust-deletion checklist* below for the per-item coverage. +- **`t_pb_b_1_dag_runner_test`** (PR #736) — `lower` asserts each declaring `tests/dag/*.dag` module compiles with **empty module diagnostics** (retired compile-smoke receipt), then `TestRunner::run_suite` evaluates each landed `TestSuite` (`Compiles`, `FailsWithDiagnostic{TypeMismatch}`, `PortHasState`, `CostBounded`). See *Receipts for pre–Rust-deletion checklist* below. (The former standalone `t_pb_b_1_tests_dag_smoke_test` file is **retired** as duplicate — see `docs/briefs/r1-testgen-manager.md` *Decisions log*.) -**Compile-smoke caveat (smoke tests only):** `t_pb_b_1_tests_dag_smoke_test` does **not** call `TestRunner`; it only asserts the declaring module lowers with empty diagnostics. Its helpers accept both `Ok(dag)` and `Err(CompileError::Semantic(dag))` and then check empty **module** diagnostics — that proves the declaring `.dag` / `.v3` file lowers as a harness artifact, it does **not** evaluate `TestPredicate` (`Compiles`, `FailsWithDiagnostic`, …). Predicate evaluation for the `.dag` suites lives in `t_pb_b_1_dag_runner_test` instead: `FailsWithDiagnostic` is proven there by the runner on the embedded program, **not** by empty diagnostics on the outer file (which would invert the predicate). **`t_pb_b_1_contract_diagnostic_smoke.dag`** is the sharp example: it names `FailsWithDiagnostic` for embedded `source: "let x: Bool = 1"`, the smoke still requires the **wrapper** module to lower without diagnostics, and the runner test is what actually witnesses the embedded negative. Do not treat the smoke pass as semantic proof of the negative, and do not promote diagnostic-negative fixtures to CI-backed assertions from the smoke path alone (see also Brief D duplicate-authority / dissolution; the Brief D `.v3` `let`-binding path is still smoke-only). +**Compile-smoke caveat (Brief D `.v3` only):** `t_pb_b_brief_d_fixture_smoke_test` does **not** call `TestRunner`; it only asserts the declaring module lowers with empty diagnostics. That proves the draft `.v3` harness artifact lowers, it does **not** evaluate `TestPredicate` on embedded sources. Predicate evaluation for the **landed** `.dag` suites lives in `t_pb_b_1_dag_runner_test` instead: `FailsWithDiagnostic` is proven there by the runner on the embedded program, **not** by empty diagnostics on the outer file (which would invert the predicate). **`t_pb_b_1_contract_diagnostic_smoke.dag`** is the sharp example: it names `FailsWithDiagnostic` for embedded `source: "let x: Bool = 1"`; the wrapper module still lowers without diagnostics, and the runner test witnesses the embedded negative. Do not treat compile-smoke as semantic proof of the negative, and do not promote diagnostic-negative fixtures to CI-backed assertions from the smoke path alone (see also Brief D duplicate-authority / dissolution; the Brief D `.v3` `let`-binding path is still smoke-only). **Compiler constraint (today):** M1(2.8) rejects standalone `data …: TestPredicate = PortHasState(…)` / `CostBounded(…)` bodies as opaque. Inline those predicates **inside** each `TestClaim` `data` record (see `t_pb_b_1_contract_port_cost.dag`) until class-5 data bodies lift the restriction — call this out when Testgen chooses how to factor shared predicates. @@ -24,7 +23,7 @@ Runner wiring for `src/v3/compiler/tests/dag/*.dag` **is** landed (PR #736 — s - **(1) Runner accepts the landed layout** — `src/v3/compiler/tests/integration/t_pb_b_1_dag_runner_test.rs` loads each landed `.dag` via `compile_to_dag` and evaluates its `TestSuite` through `TestRunner::run_suite`, asserting every claim reaches `ClaimResult::Pass`. Covers `Compiles`, `FailsWithDiagnostic{TypeMismatch}`, `PortHasState`, and `CostBounded`. - **(2) `requires: []` vs `empty()`** — **not equivalent in `data` bodies today.** `data …: TestClaim = { … requires: empty() }` is rejected by M1(2.8) class-5 ("data `…` field `requires` must be a list literal matching the declared `List<_>` type"). Receipt: `test_runner_data_bodies_reject_requires_empty_call_today` in `tests/integration/test_runner_test.rs` pins the diagnostic. The runner path (`src/v3/compiler/tests/dag/*.dag`) must therefore stay on the `[]` literal. `empty()` remains valid in `let` bindings (Brief D `.v3` fixtures), but those bindings are not `Declaration`s and so are not currently `run_suite`-consumable. When M1(2.8) class-5 lifts, the pinned test flips to a positive equivalence proof. - **(3) M1(2.8) inline `PortHasState` / `CostBounded`** — proven for the Day-1 predicate shapes on `t_pb_b_1_contract_port_cost.dag`, which inlines both variant literals on each `data …: TestClaim = { … }` record. `t_pb_b_1_pipeline_smoke.dag` / `t_pb_b_1_contract_diagnostic_smoke.dag` likewise inline `Compiles` / `FailsWithDiagnostic`. **Still NYI:** standalone `data _: TestPredicate = PortHasState(…)` / `CostBounded(…)` bodies — same class-5 restriction. Shared-predicate factoring (`let pred_*: TestPredicate = …` in `m1_5_verification_test` style) does not flow through the runner today for the same `Declaration`-vs-`Bind` reason as (2). -- **(4) First Rust deletion batch** — **still open; prepped, not signed off** (2026-04-24). Candidate inventory (`thesis_validation_test.rs` `Compiles`/`PortHasState`/`CostBounded` subset; `pipe_desugar.rs` excluded — its asserts cover `Transform` target / arity / literal order / return shape, which the `.dag` pipeline smoke does not witness) and the four-point Testgen sign-off guard live in `docs/briefs/r1-testgen-manager.md` → *Hand-off points → Sideways to Self-hosting Manager* (single source). Deletion PRs must not open until a sign-off entry appears in that brief's *Decisions log* naming the specific `#[test]` → `.dag` `TestClaim` mapping. +- **(4) First Rust deletion batch** — **partial (2026-04-24):** redundant `t_pb_b_1_tests_dag_smoke_test.rs` removed; Testgen sign-off + `#[test]` → `.dag` claim mapping in `docs/briefs/r1-testgen-manager.md` *Decisions log*. **Still open** for the `thesis_validation_test.rs` / `pipe_desugar` inventory (same sign-off guard) until a follow-on log entry names each `#[test]` → `TestClaim` pair. **Cross-PR coordination — #735 (symbolic cost / `Lookup`).** The landed `CostBounded("answer", Eq, 3)` witness in `t_pb_b_1_contract_port_cost.dag` is the current `cost_of(&dag, &bind.value)` result for `let answer: Int = 1 + 1 + 1 + 1` (three `+` additions). If #735 changes cost-witness semantics (symbolic-cost `Lookup` reshape, operator costing, or the `CostLookup::Hit` path), the `Eq 3` bound must be re-derived against the post-#735 runner output. Same check applies to the Brief D `.v3` sibling (`tests/fixtures/t_pb_b_brief_d/contract_port_cost_smoke.v3`). The runner-backed `t_pb_b_1_dag_runner_test` will fail loudly at `cost N did not satisfy bound 3` if the witness drifts; treat that failure as the #735 re-derivation signal, not a bug in this test. diff --git a/docs/briefs/t-pb-b-brief-d.md b/docs/briefs/t-pb-b-brief-d.md index 34a721a3fe0..cbe5629107c 100644 --- a/docs/briefs/t-pb-b-brief-d.md +++ b/docs/briefs/t-pb-b-brief-d.md @@ -10,7 +10,7 @@ **Duplicate authority (bounded, P2/P5):** The same three claims exist here (`.v3`, suite names `t-pb-b/…`) and under T-PB-B-1 (`.dag`, suite names `t-pb-b-1/…`). **`.dag` modules are runner-backed** via `t_pb_b_1_dag_runner_test` (PR #736); **Brief D `.v3` fixtures remain compile-smoke only** (`t_pb_b_brief_d_fixture_smoke_test`) until someone intentionally adds runner coverage for the `let`-binding path. **Dissolution trigger (named):** remove or shrink the `.v3` copies once Testgen accepts `src/v3/compiler/tests/dag/t_pb_b_1_*.dag` as the single maintained source for those claims—until then, any edit to claim text must keep both paths aligned (each `.v3` file header points at its `.dag` sibling, including the runner-evaluated `CostBounded` witness value). -**T-PB-B-1 (landed `.dag` home):** `src/v3/compiler/tests/dag/*.dag` + `docs/briefs/t-pb-b-1.md` + `t_pb_b_1_tests_dag_smoke_test` (compile smoke) + `t_pb_b_1_dag_runner_test` (runner-backed predicate evaluation; PR #736) — first batch as **`data` declarations** in real `.dag` modules. Rust-integration-test deletion is still gated on Testgen. +**T-PB-B-1 (landed `.dag` home):** `src/v3/compiler/tests/dag/*.dag` + `docs/briefs/t-pb-b-1.md` + `t_pb_b_1_dag_runner_test` (runner-backed predicate evaluation; PR #736) — first batch as **`data` declarations** in real `.dag` modules. The former `t_pb_b_1_tests_dag_smoke_test` compile-only harness is retired (redundant). Further Rust-integration-test deletion per inventory remains gated on Testgen (see *Decisions log* in `docs/briefs/r1-testgen-manager.md`). --- @@ -100,7 +100,7 @@ Paths are modules under `src/v3/compiler/tests/` unless noted. Primary classific | `sg6_hand_authored_census_test` | Meta | A | | | `sg7_prep_variant_payload_freshness_test` | Pipeline / prep | D + G | | | `t_pb_b_brief_d_fixture_smoke_test` | Fixture host | A | Intentionally thin: only verifies Brief D `.v3` fixtures compile. | -| `t_pb_b_1_tests_dag_smoke_test` | T-PB-B-1 `tests/dag/` host | A | Compile smoke for landed `.dag` `TestClaim` modules (`src/v3/compiler/tests/dag/`). | +| `t_pb_b_1_dag_runner_test` | T-PB-B-1 `tests/dag/` host | A + D | Runner-backed; former `t_pb_b_1_tests_dag_smoke_test` **retired** (redundant). | | `thesis_parallelism_test` | Contract (thesis) | D + G | | | `thesis_validation_test` | Contract (thesis) | D + G | | diff --git a/docs/invariants/l-8-lens-rust-surfaces-preserve-typed-failure-carriers.md b/docs/invariants/l-8-lens-rust-surfaces-preserve-typed-failure-carriers.md index 2bcec6277e9..a72ee099c48 100644 --- a/docs/invariants/l-8-lens-rust-surfaces-preserve-typed-failure-carriers.md +++ b/docs/invariants/l-8-lens-rust-surfaces-preserve-typed-failure-carriers.md @@ -54,9 +54,9 @@ public fn in a lens wrapper file: grep -nE "pub fn .*-> (usize|bool|i64)" src/v3/compiler/src/lens_*.rs ``` -Scope excludes `lens_depth.rs` (hand-written legacy lens, not -migrated from `.dag`; out of L-8 scope). Zero matches required. -Lens wrappers return typed carriers. +Zero matches required. Lens wrappers return typed carriers. (The +retired `lens_depth.rs` observational helper is deleted — no +remaining `.dag` migration carve-out.) **Origin:** Half A review feedback (2026-04-17) + round 1a.3 prose/ratchet alignment. Full design: diff --git a/docs/invariants/layer-opacity.md b/docs/invariants/layer-opacity.md index 5b5fb3fbcdb..16db6d22d2c 100644 --- a/docs/invariants/layer-opacity.md +++ b/docs/invariants/layer-opacity.md @@ -201,7 +201,7 @@ proposed:** flat list. - **Thesis-native.** The lens uses existing v3 infrastructure (reader lens over Dag, same shape as `lens_provenance`, - `lens_depth`, `lens_cost`). No new machinery. + `lens_cost`; `lens_depth` was a retired M0 experiment). No new machinery. - **Generalizes to other invariants.** The lens framework extends to every testable invariant over a DAG — scaffold boundaries, fail-closed discipline, structural duplication, diff --git a/docs/lens-library-design.md b/docs/lens-library-design.md index f774b0323bd..e224e6d12b9 100644 --- a/docs/lens-library-design.md +++ b/docs/lens-library-design.md @@ -11,10 +11,11 @@ ## What this document is -v3 already has three reader lenses working: `lens_provenance`, -`lens_depth`, and `lens_cost` (the first three added in M0 and -PR-B). Each is a pure function over `Dag` returning a structural -answer. This document specifies a **lens library** — a growing +v3 has reader lenses in active use: `lens_provenance`, `lens_cost`, +and `lens_unused_parameters` (M0, M1, and PR #445). An early M0 +`lens_depth` experiment is **retired** (no in-tree consumer; removed +in the pure-bootstrap paydown). Each remaining lens is a pure function +over `Dag` returning a structural answer. This document specifies a **lens library** — a growing set of reader lenses that enforce thesis-level invariants over arbitrary DAG segments. @@ -99,19 +100,18 @@ Lenses written as Rust modules are a **bootstrap shortcut**, not the endgame. **The canonical shape is "pure reader with lens-specific -output," not "pure reader returning violations."** The four -lenses shipping today demonstrate the range: +output," not "pure reader returning violations."** The three +lenses in use demonstrate the range: - `lens_provenance` returns per-port origin information. -- `lens_depth` returns per-port depth. - `lens_cost` returns per-node cost. - `lens_unused_parameters` returns a list of violations. -Three of the four are analyses; one is a violation list. The +Two of the three are analyses; one is a violation list. The common shape is **pure function, `Dag` in, structured output out**. "Violation list" is one instantiation. The canonical form must not bake "violation" into the signature, or else -analyses like cost and depth don't fit the template. +analyses like cost and provenance don't fit the template. **Why `.dag` form is canonical:** @@ -158,7 +158,7 @@ that execution path lands, lenses still ship as Rust bootstrap modules. [`docs/substrate-reflection-design.md`](substrate-reflection-design.md)** (merged into this branch in commit 700dba6). That design doc specifies substrate types as `.dag` declarations, a query -primitive set, and the migration path for the four existing +primitive set, and the migration path for the remaining Rust lenses. When the reflection primitive lands, the §1.5 "thin wrapper" gate becomes a **structural invariant** enforced by two ratchets: @@ -180,7 +180,7 @@ reflection design doc remains the design history and migration plan. remaining scope.** Reflection and field-binding realization are now in place, so the remaining blocker is not "the substrate is invisible"; it is "compiled `.dag` lenses are not yet invocable on a runtime -Dag value." `lens_provenance`, `lens_depth`, `lens_cost`, and +Dag value." `lens_provenance`, `lens_cost`, and `lens_unused_parameters` therefore remain bootstrap scaffolds, but their migration target is now mechanically clearer: the substrate surface and Rust realization bridge they need already exist. @@ -1001,18 +1001,17 @@ wrapper, not a deepening Rust-lens scaffold) before landing. ## §7. Relationship to the existing lens infrastructure -v3 already has four reader lenses: +v3 has three reader lens modules in the tree, plus generated lens outputs: - `lens_provenance.rs` (M0) — reads `produced_by` edges, returns the origin of each port. -- `lens_depth.rs` (post-M0) — reads the substrate walker, - returns port depth. - `lens_cost.rs` (M1) — reads substrate + language spec, returns per-node cost. - `lens_unused_parameters.rs` (M1, PR #445) — walks function body sub-DAGs and reports parameter ports the body never references. First library lens to ship; same reader-lens - template as the three above. + template as the modules above. +- *Retired:* `lens_depth.rs` (M0 experiment; per-port depth) — removed as unused observational code. The new lenses in this document follow the same shape: pure function over `Dag` + configuration, returns structured output. diff --git a/docs/substrate-reflection-design.md b/docs/substrate-reflection-design.md index 3d50425eaab..e9498706f0b 100644 --- a/docs/substrate-reflection-design.md +++ b/docs/substrate-reflection-design.md @@ -63,8 +63,9 @@ path, but they are the same mechanism.** source. The patch applier is a follow-up PR after reflection. **The concrete failure mode this work prevents — for lenses.** -The four lenses that ship today (`lens_provenance`, `lens_depth`, -`lens_cost`, `lens_unused_parameters`) are all Rust modules. +The reader lenses in active use today (`lens_provenance`, +`lens_cost`, `lens_unused_parameters`) are Rust modules. The early +`lens_depth` experiment is **retired** (unused observational code). Every new lens added as a Rust module grows a registry of known lens names, a dispatch pattern keyed on those names, and shared Rust-lens infrastructure. That is the same failure class as @@ -241,9 +242,10 @@ for complexity/ownership/effects/trace is retiring debt. **Out of scope (deferred):** -- Migrating `lens_provenance`, `lens_depth`, `lens_cost` to - `.dag`. The migration template is proven by - `lens_unused_parameters`; the other three are mechanical ports +- Migrating `lens_provenance`, `lens_cost` to + `.dag`. (`lens_depth` was retired without a `.dag` port — unused experiment.) + The migration template is proven by + `lens_unused_parameters`; the other two are mechanical ports left as a follow-up. - Building `lens_complexity` as the v2/v3 comparison vehicle. That depends on this work landing first but is a separate @@ -1829,8 +1831,8 @@ primitive lands MUST be a `.dag` program in `dsl/lenses/` operating over the query primitives in `std.substrate_query`. Rust lens modules (e.g., `src/v3/compiler/src/lens_*.rs`) are -forbidden for new lenses. Exception: the migration of the three -existing Rust lenses (`lens_provenance`, `lens_depth`, `lens_cost`) +forbidden for new lenses. Exception: the migration of the remaining Rust lenses +(`lens_provenance`, `lens_cost`; `lens_depth` already removed) is tracked as followup work; each deletion happens as its own PR, and no new Rust lens can land in the meantime. @@ -1868,11 +1870,9 @@ structure used internally, it's bootstrap and is exempt. - **§2.3 `lens_unused_parameters`** — the signature example rewrites to `.dag`. The Rust form disappears. The test plan references the `.dag` fixtures. -- **§7 "Existing infrastructure"** — the four-lens list updates - to reflect migration status. When this PR lands, the list is - `lens_unused_parameters (.dag), lens_provenance (Rust — - migration pending), lens_depth (Rust — migration pending), - lens_cost (Rust — migration pending)`. +- **§7 "Existing infrastructure"** — the lens list updates + to reflect migration status: e.g. `lens_unused_parameters` (`.dag` or hybrid per current tree), + `lens_provenance` / `lens_cost` (Rust — migration pending); `lens_depth` **retired**. --- diff --git a/dsl/gunbc/compiler.dag b/dsl/gunbc/compiler.dag index 3d7211581b7..bfa2cac88d5 100644 --- a/dsl/gunbc/compiler.dag +++ b/dsl/gunbc/compiler.dag @@ -89,7 +89,6 @@ data stage0: GeneratedCrate = { "python_target.rs", "rust_target.rs", "infer.rs", - "lens_depth.rs", "lens_testgen.rs", "lens_unused_parameters.rs", "lib.rs", diff --git a/src/v3/DOWNSTREAM_REQUIREMENTS.md b/src/v3/DOWNSTREAM_REQUIREMENTS.md index 20df762f301..ed502d84297 100644 --- a/src/v3/DOWNSTREAM_REQUIREMENTS.md +++ b/src/v3/DOWNSTREAM_REQUIREMENTS.md @@ -124,7 +124,7 @@ PR-B-unwind R1 closed this gap via `build.rs` + the generated file in `src/v3/spec/`, run `cargo build`, and the loader picks it up. **Status**: closed at PR-B-unwind R1. -**Scope.** Covers both the read side (`infer.rs`, `lens_depth.rs`, +**Scope.** Covers both the read side (`infer.rs`, `lens_provenance.rs`) and the write side (`parse.rs` → `lower.rs` boundary). The write side was added in a second pass after a reviewer surfaced five write-pipeline gaps; the lesson is @@ -420,7 +420,7 @@ full gap list visible. This enumeration covers both halves of the pipeline: -- **Read side** (Consumers 1–3): `infer.rs`, `lens_depth.rs`, +- **Read side** (Consumers 1–3): `infer.rs`, `lens_provenance.rs` — readers of the substrate. - **Write side** (Consumer 4): `lower.rs` viewed as a consumer of `parse.rs` output, with its `SurfaceItem` → declaration / diff --git a/src/v3/M1_DESIGN.md b/src/v3/M1_DESIGN.md index 3c3e7e011ce..2f00b12bc6f 100644 --- a/src/v3/M1_DESIGN.md +++ b/src/v3/M1_DESIGN.md @@ -93,7 +93,7 @@ This design note executes on the Open items only. **Unaffected:** - Tokenizer (`src/v3/compiler/src/tokenize.rs`) — minor updates only. -- Lens architecture (`lens_depth.rs`, `lens_provenance.rs`) — read +- Lens architecture (`lens_provenance.rs`, `lens_cost`, etc.) — read interfaces will need light updates to walk connectives instead of `DeclKind` variants, but the lens-as-read-only-observer pattern stands. diff --git a/src/v3/compiler/src/lens_depth.rs b/src/v3/compiler/src/lens_depth.rs deleted file mode 100644 index 5a319fd5247..00000000000 --- a/src/v3/compiler/src/lens_depth.rs +++ /dev/null @@ -1,74 +0,0 @@ -// Depth lens — for each port, computes the longest path (in edges) -// from a leaf port (one with no producer) to this port. A leaf is a -// function parameter or a Value literal — anything whose -// `produced_by` is None. -// -// Second observational lens. Purpose: validate the v3 success bar -// empirically — a new observational lens over the substrate should -// land in tens of lines with zero substrate modifications. The -// provenance lens (M0.4) was the first data point; this is the -// second. If the substrate supports observational queries cheaply, -// this lens costs no more than reading `produced_by` edges and -// dispatching on the producer's behavior kind. -// -// Size budget: ~50 lines. If this grows, the substrate is gapped -// for this kind of analysis and M1 should fix it before building -// anything bigger. -// -// NOT a writer lens — the depth is computed on demand by query, -// not stored anywhere. M1's cost lens will be the first writer -// and will force the "how do lenses store results" decision. - -use crate::dag::{Behavior, Dag, NodeId, PortId}; - -pub struct DepthLens<'a> { - dag: &'a Dag, -} - -impl<'a> DepthLens<'a> { - pub fn new(dag: &'a Dag) -> Self { - Self { dag } - } - - /// Longest path (in edges) from any leaf port to this port. - /// Leaves are: ports with `produced_by == None` (function - /// parameters), and Value node output ports (literal sources). - /// Values are sources by construction, so even though their - /// output port has a producer, the port itself counts as a - /// leaf for depth purposes. - pub fn depth_of(&self, port: PortId) -> usize { - match self.dag.port(port).produced_by { - None => 0, - Some(node_id) => match self.dag.node(node_id) { - Behavior::Value(_) => 0, - _ => 1 + self.node_input_depth(node_id), - }, - } - } - - fn node_input_depth(&self, node_id: NodeId) -> usize { - match self.dag.node(node_id) { - // Unreachable — depth_of short-circuits Value above. Kept - // for match exhaustiveness and clarity. - Behavior::Value(_) => 0, - Behavior::Transform(t) => t - .inputs - .iter() - .map(|&p| self.depth_of(p)) - .max() - .unwrap_or(0), - Behavior::Branch(b) => { - let cond = self.depth_of(b.input); - let paths_max = b - .paths - .iter() - .map(|path| self.depth_of(path.output)) - .max() - .unwrap_or(0); - cond.max(paths_max) - } - Behavior::Loop(l) => self.depth_of(l.source).max(self.depth_of(l.init)), - Behavior::Bind(b) => self.depth_of(b.value), - } - } -} diff --git a/src/v3/compiler/src/lib.rs b/src/v3/compiler/src/lib.rs index 985aa8b4020..afdf03c7fb7 100644 --- a/src/v3/compiler/src/lib.rs +++ b/src/v3/compiler/src/lib.rs @@ -37,7 +37,6 @@ pub mod emit_rust; /// T-LensAPI D1: bounded lens interpreter over substrate-shaped [`FieldValue`] /// (see module docs in `lens_apply.rs`). pub mod lens_apply; -pub mod lens_depth; pub mod lens_testgen; pub mod lens_unused_parameters; pub mod post_emit_verifier; diff --git a/src/v3/compiler/tests/dag/README.md b/src/v3/compiler/tests/dag/README.md index 10f12a79227..7f560a9fcef 100644 --- a/src/v3/compiler/tests/dag/README.md +++ b/src/v3/compiler/tests/dag/README.md @@ -6,10 +6,9 @@ This directory holds **landed** v3 `.dag` modules that declare `TestClaim` / `Te ## What is here vs what is not -- **Landed:** `.dag` sources + `t_pb_b_1_tests_dag_smoke_test` compile smoke (`compile_to_dag`, empty diagnostics). No `pb_*` predicates. -- **Landed (runner path):** `t_pb_b_1_dag_runner_test` evaluates each landed `TestSuite` through `TestRunner::run_suite` — proves line-item (1) of the pre–Rust-deletion checklist in `docs/briefs/r1-testgen-manager.md` (runner accepts the landed layout; `requires: []` lowers to a runner-consumable shape). Still not a `pb_*` gate and still not a Rust-deletion signal. -- **Not done here:** Rust test deletion or `pb_test_file_generated_from_dag` — those require **Testgen manager** sign-off on the remaining checklist items (M1(2.8) inlining coverage, first Rust-deletion batch). -- **Smoke vs predicates:** The *Compile-smoke caveat* applies **only** to `t_pb_b_1_tests_dag_smoke_test` (and the Brief D `.v3` fixture smoke): empty diagnostics on the declaring module are **not** proof of `Compiles` / `FailsWithDiagnostic` on embedded `TestClaim.source` strings — especially `t_pb_b_1_contract_diagnostic_smoke.dag`. `t_pb_b_1_dag_runner_test` is the complementary **runner-backed** integration test for these same suites: it *does* evaluate the predicates on the embedded `source`, so `FailsWithDiagnostic` negatives, `PortHasState`, and `CostBounded` bounds are real witnesses, not proxies. See `docs/briefs/t-pb-b-1.md` (*Compile-smoke caveat*). +- **Landed (runner path):** `t_pb_b_1_dag_runner_test` — `lower` keeps the empty-harness-diagnostics compile receipt for each on-disk `tests/dag/*.dag` file, then `TestRunner::run_suite` proves line-item (1) of the pre–Rust-deletion checklist in `docs/briefs/r1-testgen-manager.md`. The former standalone `t_pb_b_1_tests_dag_smoke_test` is **retired** (redundant; see Testgen *Decisions log*). Still not a `pb_*` gate by itself. +- **Not done here:** Further Rust test deletion or `pb_test_file_generated_from_dag` — follow-on work needs **Testgen** sign-off per the inventory in `docs/briefs/r1-testgen-manager.md`. +- **Compile-smoke vs `TestRunner` (Brief D vs landed):** **Brief D** `.v3` smoke (`t_pb_b_brief_d_fixture_smoke_test`) only checks that the declaring file lowers with empty **module** diagnostics — that is **not** by itself proof of `Compiles` / `FailsWithDiagnostic` on embedded `TestClaim.source` strings. **Landed** `tests/dag/*.dag` files use the same empty-harness check inside `t_pb_b_1_dag_runner_test::lower`, then `run_suite` evaluates the predicates on the embedded `source` — so `FailsWithDiagnostic` negatives, `PortHasState`, and `CostBounded` bounds are real witnesses, not compile-smoke proxies. See `docs/briefs/t-pb-b-1.md` (*Compile-smoke caveat*). ## Post-R2 residuals (unchanged) diff --git a/src/v3/compiler/tests/integration.rs b/src/v3/compiler/tests/integration.rs index 34a6378bc62..4026da6013b 100644 --- a/src/v3/compiler/tests/integration.rs +++ b/src/v3/compiler/tests/integration.rs @@ -137,8 +137,6 @@ mod sg6_hand_authored_census_test; mod sg7_prep_variant_payload_freshness_test; #[path = "integration/t_pb_b_1_dag_runner_test.rs"] mod t_pb_b_1_dag_runner_test; -#[path = "integration/t_pb_b_1_tests_dag_smoke_test.rs"] -mod t_pb_b_1_tests_dag_smoke_test; #[path = "integration/t_pb_b_brief_d_fixture_smoke_test.rs"] mod t_pb_b_brief_d_fixture_smoke_test; #[path = "integration/test_runner_test.rs"] diff --git a/src/v3/compiler/tests/integration/sg0_census_test.rs b/src/v3/compiler/tests/integration/sg0_census_test.rs index 29dc1c98cc3..d44d15e7d51 100644 --- a/src/v3/compiler/tests/integration/sg0_census_test.rs +++ b/src/v3/compiler/tests/integration/sg0_census_test.rs @@ -171,7 +171,7 @@ const EXPECTED_HAND_AUTHORED_NON_TEST: &[&str] = &[ "src/v3/compiler/src/emit_rust.rs", "src/v3/compiler/src/infer.rs", "src/v3/compiler/src/lens_apply.rs", - "src/v3/compiler/src/lens_depth.rs", + // T-PB-A: `lens_depth.rs` retired — unused observational lens (no in-tree consumer). "src/v3/compiler/src/lens_testgen.rs", "src/v3/compiler/src/lens_unused_parameters.rs", "src/v3/compiler/src/lib.rs", @@ -252,7 +252,6 @@ const EXPECTED_HAND_AUTHORED_TEST: &[&str] = &[ "src/v3/compiler/tests/integration/sg6_hand_authored_census_test.rs", "src/v3/compiler/tests/integration/sg7_prep_variant_payload_freshness_test.rs", "src/v3/compiler/tests/integration/t_pb_b_1_dag_runner_test.rs", - "src/v3/compiler/tests/integration/t_pb_b_1_tests_dag_smoke_test.rs", "src/v3/compiler/tests/integration/t_pb_b_brief_d_fixture_smoke_test.rs", "src/v3/compiler/tests/integration/test_runner_test.rs", "src/v3/compiler/tests/integration/testgen_structural_coverage_gate_test.rs", diff --git a/src/v3/compiler/tests/integration/t_pb_b_1_dag_runner_test.rs b/src/v3/compiler/tests/integration/t_pb_b_1_dag_runner_test.rs index fd322b38024..10498f1a685 100644 --- a/src/v3/compiler/tests/integration/t_pb_b_1_dag_runner_test.rs +++ b/src/v3/compiler/tests/integration/t_pb_b_1_dag_runner_test.rs @@ -6,7 +6,11 @@ //! line-item (1) of the pre–Rust-deletion checklist in //! `docs/briefs/r1-testgen-manager.md` (Hand-off → Self-hosting): runner path //! accepts the landed layout and `requires: []` lowers to a shape the runner -//! consumes. Still **not** a `pb_*` gate and still not a Rust-deletion signal. +//! consumes. `lower` requires `compile_to_dag` → `Ok` (empty module diagnostics +//! per `lib.rs`); `Err(Semantic(_))` panics with the same compile-smoke intent as +//! the retired `t_pb_b_1_tests_dag_smoke_test` (runner evaluation of embedded +//! `TestClaim.source` is orthogonal). Still +//! **not** a `pb_*` gate and still not a Rust-deletion signal. use v3_compiler::compile_to_dag; use v3_compiler::dag::Dag; @@ -14,9 +18,32 @@ use v3_compiler::test_runner::{ClaimResult, TestRunner}; use v3_compiler::CompileError; fn lower(source: &'static str, file: &'static str) -> Dag { + // `compile_to_dag` returns `Ok` iff the module diagnostic table is empty + // (`lib.rs` — any semantic issue is `Err(Semantic(dag))` with non-empty + // diagnostics). The retired `t_pb_b_1_tests_dag_smoke_test` required the + // same: declaring `tests/dag` harness compiles with no module diagnostics. match compile_to_dag(source, file) { - Ok(dag) => dag, - Err(CompileError::Semantic(dag)) => dag, + Ok(dag) => { + // Explicit compile-smoke receipt: same as the retired + // `t_pb_b_1_tests_dag_smoke_test` (in addition to `Ok` ⟺ empty in `lib.rs`). + // Belt-and-suspenders against C-8 / `compile_to_dag` contract drift; unreachable + // if `Ok` truly implies an empty table — kept so reviewers and grep see the + // harness receipt without relying only on the `Result` shape. + assert!( + dag.diagnostics().is_empty(), + "{file} (declaring `tests/dag` harness): expected empty module diagnostics, got {:?}", + dag.diagnostics().iter().collect::>() + ); + dag + } + Err(CompileError::Semantic(dag)) => { + panic!( + "{file} (declaring `tests/dag` harness) should lower without module diagnostics — \ + same compile-smoke receipt as the retired `t_pb_b_1_tests_dag_smoke_test`. \ + Got `Err(Semantic)`: {:?}", + dag.diagnostics().iter().collect::>() + ); + } Err(other) => panic!("unexpected compile error for {file}: {other:?}"), } } diff --git a/src/v3/compiler/tests/integration/t_pb_b_1_tests_dag_smoke_test.rs b/src/v3/compiler/tests/integration/t_pb_b_1_tests_dag_smoke_test.rs deleted file mode 100644 index 0727a908df7..00000000000 --- a/src/v3/compiler/tests/integration/t_pb_b_1_tests_dag_smoke_test.rs +++ /dev/null @@ -1,50 +0,0 @@ -//! **Layer:** integration -//! -//! T-PB-B-1 — `src/v3/compiler/tests/dag/*.dag` compile smoke. Landed `.dag` `TestClaim` -//! modules for the eventual Testgen runner; **does not** evaluate predicates or assert `pb_*`. -//! Coordinate with Testgen manager before deleting overlapping Rust tests. -//! -//! `assert_dag_module_lowers_cleanly` accepts `Ok(dag)` and `Err(CompileError::Semantic(dag))` -//! then requires empty module diagnostics — lowering shape only, not `TestPredicate` proof -//! (see `docs/briefs/t-pb-b-1.md` *Compile-smoke caveat*; revisit when the runner evaluates -//! `FailsWithDiagnostic` for real). - -use v3_compiler::compile_to_dag; -use v3_compiler::CompileError; - -fn assert_dag_module_lowers_cleanly(source: &'static str, file: &'static str) { - let dag = match compile_to_dag(source, file) { - Ok(dag) => dag, - Err(CompileError::Semantic(dag)) => dag, - Err(other) => panic!("unexpected compile error for {file}: {other:?}"), - }; - assert!( - dag.diagnostics().is_empty(), - "{file} should lower without diagnostics, got {:?}", - dag.diagnostics() - ); -} - -#[test] -fn t_pb_b_1_pipeline_smoke_dag_lowers_cleanly() { - assert_dag_module_lowers_cleanly( - include_str!("../dag/t_pb_b_1_pipeline_smoke.dag"), - "src/v3/compiler/tests/dag/t_pb_b_1_pipeline_smoke.dag", - ); -} - -#[test] -fn t_pb_b_1_contract_diagnostic_smoke_dag_lowers_cleanly() { - assert_dag_module_lowers_cleanly( - include_str!("../dag/t_pb_b_1_contract_diagnostic_smoke.dag"), - "src/v3/compiler/tests/dag/t_pb_b_1_contract_diagnostic_smoke.dag", - ); -} - -#[test] -fn t_pb_b_1_contract_port_cost_dag_lowers_cleanly() { - assert_dag_module_lowers_cleanly( - include_str!("../dag/t_pb_b_1_contract_port_cost.dag"), - "src/v3/compiler/tests/dag/t_pb_b_1_contract_port_cost.dag", - ); -} diff --git a/src/v3/compiler/tests/integration/t_pb_b_brief_d_fixture_smoke_test.rs b/src/v3/compiler/tests/integration/t_pb_b_brief_d_fixture_smoke_test.rs index 419ed799caa..289a58efe27 100644 --- a/src/v3/compiler/tests/integration/t_pb_b_brief_d_fixture_smoke_test.rs +++ b/src/v3/compiler/tests/integration/t_pb_b_brief_d_fixture_smoke_test.rs @@ -4,8 +4,10 @@ //! `tests/fixtures/t_pb_b_brief_d/`. These files exercise `std.verification` shapes from real //! v3 source; they are **not** a `pb_*` gate and do not replace existing Rust tests. //! -//! Same `Ok` / `Semantic` → empty-diagnostics pattern as `t_pb_b_1_tests_dag_smoke_test` -//! (lowering proxy only; see `docs/briefs/t-pb-b-1.md` *Compile-smoke caveat*). +//! Same `Ok` / `Semantic` → empty-diagnostics pattern as the former +//! `t_pb_b_1_tests_dag_smoke_test` (retired — `t_pb_b_1_dag_runner_test` subsumes +//! the landed `tests/dag/*.dag` sources). Lowering proxy only; see +//! `docs/briefs/t-pb-b-1.md` *Compile-smoke caveat*. use v3_compiler::compile_to_dag; use v3_compiler::CompileError;