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

Filter by extension

Filter by extension

Conversations
Failed to load comments.
Loading
Jump to
Jump to file
Failed to load files.
Loading
Diff view
Diff view
3 changes: 2 additions & 1 deletion docs/briefs/r1-selfhosting-manager.md
Original file line number Diff line number Diff line change
Expand Up @@ -179,7 +179,8 @@ Decisions log (append as they happen):
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).
the former `t_pb_b_brief_d_fixture_smoke_test` is retired in favor of the runner-backed
`.dag` siblings in `t_pb_b_1_dag_runner_test` (no `pb_*` gate claim).
- 2026-04-23: SG-0 file-level census split landed as non-test/test
sub-ratchets; `tokenize.rs` shim retired from the non-test subset.

Expand Down
30 changes: 30 additions & 0 deletions docs/briefs/r1-testgen-manager.md
Original file line number Diff line number Diff line change
Expand Up @@ -245,6 +245,36 @@ Lane-owner dispatch status (update as sub-deliverables close):

Decisions log (append as they happen):

- 2026-05-12 (R3 Cluster M #84 / PR #2716): **Deletion-guard — Brief D
compile-smoke shim retired after runner-backed TestClaim coverage.**
Receipts (1)–(3) re-verified green for the candidate surface:
`cargo test -p v3-compiler --test integration
t_pb_b_1_pipeline_smoke_suite_passes_through_runner`,
`t_pb_b_1_contract_diagnostic_smoke_suite_passes_through_runner`,
`t_pb_b_1_contract_port_cost_suite_passes_through_runner`, and
`r3_tests_as_data_demonstration_suite_passes_through_runner` all return
`ClaimResult::Pass` through `TestRunner`; `cargo test -p v3-compiler
--test integration sg0_census_test` confirms the SG-0 census shrink.
The deleted Rust file is `t_pb_b_brief_d_fixture_smoke_test.rs`; mapping:
- `t_pb_b_brief_d_pipeline_smoke_fixture_lowers_cleanly` →
`t_pb_b_1_dag_runner_test::r3_tests_as_data_demonstration_suite_passes_through_runner`
/ suite `suite_tests_as_data_demonstration` / `TestClaim.name`
**`tests-as-data port of pipeline smoke fixture compiles`**.
- `t_pb_b_brief_d_contract_diagnostic_smoke_fixture_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` / `TestClaim.name`
**`Bool annotation rejects Int literal`**.
- `t_pb_b_brief_d_contract_port_cost_smoke_fixture_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` / `TestClaim.name`s
**`answer bind resolves`** and
**`answer bind has bounded cost witness (Eq 3)`**.
This sign-off is intentionally narrow: it retires only the compile-only
Brief D host shim because equivalent landed `.dag` suites are
runner-backed. It does not assert `pb_test_file_generated_from_dag` or
`pb_rust_tests_outside_residual_zero`, and it does not authorize deletion
of structural files such as `pipe_desugar.rs` or mixed files such as
`thesis_validation_test.rs` without a separate per-`#[test]` mapping entry.
- 2026-04-26 (R1 shims / PR #899): **Deletion-guard — retired per-gate `#[test]`
files and structural claim-name receipt.** The integration modules
`r1_manual_claim_gate_test.rs` and `testgen_structural_coverage_gate_test.rs`
Expand Down
2 changes: 1 addition & 1 deletion docs/briefs/t-pb-b-1.md
Original file line number Diff line number Diff line change
Expand Up @@ -7,7 +7,7 @@
- **`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_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 (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).
**Compile-smoke caveat (historical Brief D `.v3` only):** the former `t_pb_b_brief_d_fixture_smoke_test` did **not** call `TestRunner`; it only asserted the declaring module lowered with empty diagnostics. That proved the draft `.v3` harness artifact lowered, it did **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 (see also Brief D duplicate-authority / dissolution; the Brief D `.v3` `let`-binding copies are historical draft artifacts).

**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.

Expand Down
7 changes: 3 additions & 4 deletions docs/briefs/t-pb-b-brief-d.md
Original file line number Diff line number Diff line change
Expand Up @@ -4,11 +4,11 @@

**Authority:** Post-R2 residuals in `TESTING.md` (compiler-internal `#[cfg(test)]` under `src/v3/compiler/src/`; boundary tests invoking external toolchains). **Schema:** `src/v3/std/verification.dag` (`TestClaim`, `TestPredicate`, `requires: List<ResourceReference>`).

**Gates (unchanged):** Do not remove or replace existing Rust integration tests as the source of truth. Do not assert `pb_test_file_generated_from_dag` or `pb_rust_tests_outside_residual_zero` until Testgen signals. Draft `.v3` / `.dag` modules here are **fixtures** for eventual runner wiring.
**Gates (updated after runner-backed coverage):** Do not assert `pb_test_file_generated_from_dag` or `pb_rust_tests_outside_residual_zero` from this brief alone. The former Brief D compile-smoke shim is retired because the matching `.dag` modules are already runner-backed; the remaining draft `.v3` modules are historical fixtures until their named Testgen dissolution trigger fires.

This comment was marked as resolved.


**Fixtures on disk:** `src/v3/compiler/tests/fixtures/t_pb_b_brief_d/*.v3` — each file is a self-contained v3 module declaring `TestSuite` / `TestClaim` values. **Compile smoke:** `t_pb_b_brief_d_fixture_smoke_test` in `tests/integration/` (lowers cleanly; not a pure-bootstrap gate).
**Fixtures on disk:** `src/v3/compiler/tests/fixtures/t_pb_b_brief_d/*.v3` — each file is a self-contained v3 module declaring `TestSuite` / `TestClaim` values. **Compile smoke retired:** the former `t_pb_b_brief_d_fixture_smoke_test` host shim dissolved into the runner-backed `.dag` suites in `src/v3/compiler/tests/dag/t_pb_b_1_*.dag` plus `t_pb_b_1_dag_runner_test`.

**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).
**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 are now historical draft copies only** and no longer have a dedicated host-side compile-smoke shim. **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_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`).

Expand Down Expand Up @@ -99,7 +99,6 @@ Paths are modules under `src/v3/compiler/tests/` unless noted. Primary classific
| `sg3_surface_reflection_consumer_test` | Pipeline | D + G | |
| `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_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 | |
Expand Down
2 changes: 1 addition & 1 deletion docs/r3-program-plan.md
Original file line number Diff line number Diff line change
Expand Up @@ -297,7 +297,7 @@ This principle is NOT a separate lane; it's a per-lane gate-shape requirement ap
| 71 | `v3_self_host_demonstration` | demonstration | T-V2-Retirement | DECLARED (NEW 2026-05-06) | bootstrap PB-Runtime trampoline runs end-to-end |
| 72 | `e_p_producer_demonstration` | demonstration | T-E-P-Producer-Broadening | **CONSUMER_LANDED** — integration `e_p_producer_demonstration` (`m2_substrate_inhabitance_test.rs`) | unary recursive self-call: `SubValueRelation` + scalar `per_call_pattern_at` → `lower_call_pattern` / `DescentEvidence::Strict` (multi-arg per-port vectors: other E-P tests) |
| 73 | `lens_behavioral_parity_demonstration` | demonstration | T-Lens-Behavioral-Parity | DECLARED (NEW 2026-05-06) | **R3 (post-carve-promotion 2026-05-09):** all 4 lenses (complexity + cost + parallelism + effect_enum) vs frozen v2-oracle snapshot. Parallelism + effect_enum **R3-load-bearing within Cluster F** per Director carve-promotion ratification at gunbc#846 c#4412330468 (prior R4-carved status DISSOLVED). |
| 74 | `tests_as_data_demonstration` | demonstration | T-Tests-As-Data-Completeness | **CONSUMER_LANDED + PASSING** — one-cell `.dag` carrier `src/v3/compiler/tests/dag/t_r3_tests_as_data_demonstration.dag` ports Rust integration test `t_pb_b_brief_d_pipeline_smoke_fixture_lowers_cleanly` to `TestClaim` (`Compiles`) and executes through `TestRunner` via `r3_tests_as_data_demonstration_suite_passes_through_runner` | Demonstration only; gate #84 owns bulk Rust-test port coverage |
| 74 | `tests_as_data_demonstration` | demonstration | T-Tests-As-Data-Completeness | **CONSUMER_LANDED + PASSING** — one-cell `.dag` carrier `src/v3/compiler/tests/dag/t_r3_tests_as_data_demonstration.dag` ports the retired Rust integration test `t_pb_b_brief_d_pipeline_smoke_fixture_lowers_cleanly` to `TestClaim` (`Compiles`) and executes through `TestRunner` via `r3_tests_as_data_demonstration_suite_passes_through_runner` | Demonstration only; gate #84 owns bulk Rust-test port coverage |
| 75 | `pr_anticipation_discipline_ci_active` | CI-discipline | R3 Debt-Paydown (standing) | **PASSING** — CI job runs `scripts/check-pr-sg0-net-shrink-discipline.sh --self-test` and PR-body enforcement before bootstrap verify | landed by PR #1807; tightened by PR #2335 + PR #2361; local self-test re-verified 2026-05-10 |
| 76 | `e_p_per_call_descent_evidence_full_coverage` | substrate-shape | T-E-P-Producer-Broadening | **CONSUMER_LANDED** (PR #2147 carrier + PR #2190 consumer; refresh per cluster-analysis audit §1) | per-call DescentEvidence covers all live call sites |
| 77 | `e_p_call_pattern_lookup_authoritative` | substrate-shape | T-E-P-Producer-Broadening | **CONSUMER_LANDED** — integration `e_p_call_pattern_lookup_authoritative` (`m2_substrate_inhabitance_test.rs`) pins `per_call_pattern_at` as the lens-facing query over the per-call evidence authority | CallPattern lookup authoritative |
Expand Down
2 changes: 1 addition & 1 deletion src/v3/compiler/tests/dag/README.md
Original file line number Diff line number Diff line change
Expand Up @@ -8,7 +8,7 @@ This directory holds **landed** v3 `.dag` modules that declare `TestClaim` / `Te

- **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*).
- **Compile-smoke vs `TestRunner` (Brief D vs landed):** the retired **Brief D** `.v3` smoke (`t_pb_b_brief_d_fixture_smoke_test`) only checked that the declaring file lowered with empty **module** diagnostics — that was 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)

Expand Down
Original file line number Diff line number Diff line change
@@ -1,6 +1,6 @@
// R3 gate #74 -- tests_as_data_demonstration.
//
// Port target: Rust integration test
// Port target: retired Rust integration test
// `t_pb_b_brief_d_pipeline_smoke_fixture_lowers_cleanly`
// (`src/v3/compiler/tests/integration/t_pb_b_brief_d_fixture_smoke_test.rs`).
//
Expand Down
2 changes: 0 additions & 2 deletions src/v3/compiler/tests/integration.rs
Original file line number Diff line number Diff line change
Expand Up @@ -223,8 +223,6 @@ mod t_las_complexity_contract_compile_error_test;
mod t_las_crdt_cost_basis_demo_test;
#[path = "integration/t_pb_b_1_dag_runner_test.rs"]
mod t_pb_b_1_dag_runner_test;
#[path = "integration/t_pb_b_brief_d_fixture_smoke_test.rs"]
mod t_pb_b_brief_d_fixture_smoke_test;
#[path = "integration/tc1_substrate_lens_eta_equivalence_deferred_test.rs"]
mod tc1_substrate_lens_eta_equivalence_deferred_test;
#[path = "integration/tc1_substrate_lens_eta_equivalence_strict_fire_test.rs"]
Expand Down
1 change: 0 additions & 1 deletion src/v3/compiler/tests/integration/sg0_census_test.rs
Original file line number Diff line number Diff line change
Expand Up @@ -643,7 +643,6 @@ const EXPECTED_HAND_AUTHORED_TEST: &[&str] = &[
"src/v3/compiler/tests/integration/t_las_complexity_contract_compile_error_test.rs",
"src/v3/compiler/tests/integration/t_las_crdt_cost_basis_demo_test.rs",
"src/v3/compiler/tests/integration/t_pb_b_1_dag_runner_test.rs",
"src/v3/compiler/tests/integration/t_pb_b_brief_d_fixture_smoke_test.rs",
// TC1 substrate lens eta-equivalence (deferred / R2 research): integration for
// `SubstrateResearchDeferredClaim` + `tc1_substrate_lens_eta_equivalence_deferred.dag`.
// SG-0 path ratchet: Director sign-off (gunb-ai/gunbc#1130, comment 4341571168;
Expand Down
4 changes: 2 additions & 2 deletions src/v3/compiler/tests/integration/t_pb_b_1_dag_runner_test.rs
Original file line number Diff line number Diff line change
Expand Up @@ -153,8 +153,8 @@ fn t_pb_b_1_execute_command_boundary_suite_passes_through_runner() {
/// R3 gate #74 — one Rust integration test ported to `.dag` `TestClaim` data and
/// executed end-to-end through `TestRunner`.
///
/// Port target: `t_pb_b_brief_d_pipeline_smoke_fixture_lowers_cleanly`
/// (`t_pb_b_brief_d_fixture_smoke_test.rs`). The original Rust test asserts the
/// Port target: retired `t_pb_b_brief_d_pipeline_smoke_fixture_lowers_cleanly`
/// (`t_pb_b_brief_d_fixture_smoke_test.rs`). The original Rust test asserted the
/// pipeline smoke fixture lowers cleanly; this carrier expresses the same
/// surface as a `Compiles` claim over the embedded subject program.
#[test]
Expand Down

This file was deleted.

Loading