Skip to content
Merged
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
12 changes: 6 additions & 6 deletions docs/r3-program-plan.md
Original file line number Diff line number Diff line change
Expand Up @@ -226,8 +226,8 @@ This principle is NOT a separate lane; it's a per-lane gate-shape requirement ap
|---|---|---|---|---|---|
| 1 | `tier3_termination_mirror_dissolved` | state-check | T-Tier3-Dissolution | DECLARED | r3-structure.md §Acceptance |
| 2 | `tier3_computation_mirror_dissolved` | state-check | T-Tier3-Dissolution | DECLARED | r3-structure.md §Acceptance |
| 3 | `tier3_induction_mirror_dissolved` | state-check | T-Tier3-Dissolution | DECLARED | r3-structure.md §Acceptance |
| 4 | `tier3_effect_carrier_mirror_dissolved` | state-check | T-Tier3-Dissolution | DECLARED | r3-structure.md §Acceptance |
| 3 | `tier3_induction_mirror_dissolved` | state-check | T-Tier3-Dissolution | **CONSUMER_LANDED** (PR #2678 squash 2026-05-11 — merry-wolf-735 T-Tier3 induction mirror retirement; scope-verified per R-7 vs C1 Phase-1 baseline now landed via PR #2702) | r3-structure.md §Acceptance |
| 4 | `tier3_effect_carrier_mirror_dissolved` | state-check | T-Tier3-Dissolution | **CONSUMER_LANDED + PASSING** (PR #2679 squash `6897445b` 2026-05-11 — warm-ibex-579 retired `workflow_idempotency.rs`, co-located Lane 2b idempotency projection in `dag/effects.rs` with P5/P2 receipts + bootstrap `ArrowBody::Unparsed` ratchet test) | r3-structure.md §Acceptance |
| 5 | `lens_apply_dot_rs_retired` | state-check | T-LensProducer-Retirement | DECLARED | gated on PB-Runtime interpreter-as-data |
| 6 | `lens_testgen_dot_rs_retired` | state-check | T-LensProducer-Retirement | **CONSUMER_LANDED + PASSING** (PR #2392 squash `b11c8014` 2026-05-10 06:03Z producer-retirement: `src/v3/compiler/src/lens_testgen.rs` deleted; PR #2594 squash `484c719e` 2026-05-10 15:40Z regression-guard `r3_gate_6_lens_testgen_rs_stays_retired` in `sg0_census_test.rs`) | producer + consumer-side ratchet pair per `feedback_grep_consumer_surfaces_for_lane_completeness` |
| 7 | `regen_lens_dot_rs_retired` | state-check | T-LensProducer-Retirement | DECLARED | gated on PB-1 bin-shim emit pattern |
Expand Down Expand Up @@ -264,8 +264,8 @@ This principle is NOT a separate lane; it's a per-lane gate-shape requirement ap
| 38 | `coercion_cost_equals_complexity_by_construction` | structural-fold | T-CostLens-Composition | **SATISFIED-BY-CONSTRUCTION** (α-narrow PR #2171; `Semiring<SymbolicCost>` `sequential`/`iterate` at `src/v3/std/algebra.dag:181-188` is sole composition authority — no parallel "complexity-vs-cost" reconciliation surface exists) | thesis unification holds structurally |
| 39 | `no_coercion_cost_dimension` | substrate-shape | T-CostLens-Composition | **SATISFIED-BY-CONSTRUCTION** (α-narrow PR #2171; `SymbolicCost` 7-variant at `src/v3/std/algebra.dag:181` is the sole cost dimension; no parallel `CoercionCost` carrier exists at HEAD per grep) | no separate cost dimension |
| 40 | `symbolic_cost_expr_equals_executable` | SymbolicCost-typed | T-CostLens-Composition | DECLARED — ε path RATIFIED 2026-05-07 (Q-Cost-Composition-Layering canvas); closes via Verification Mgr (#2075) ratchet authoring on Rust-side composition consumer + executable predicate per ε path | runtime prereq: cost lens consumer per ε |
| 41 | `v2_oracle_no_remaining_test_consumers` | state-check | T-V2-Retirement | DECLARED | no .rs test consumes src/v2/ |
| 42 | `v2_directory_deleted` | state-check | T-V2-Retirement | DECLARED | src/v2/ removed from workspace |
| 41 | `v2_oracle_no_remaining_test_consumers` | state-check | T-V2-Retirement | **CONSUMER_LANDED + PASSING** (PR #2695 squash 2026-05-11 — witty-crab-518 T-V2 G-1 ratchet: path/workspace/registry/TOML coverage + tc1 2s-ratchet exemption 79 rows; consumer-side check confirms no `.rs` test imports `src/v2/`) | no .rs test consumes src/v2/ |
| 42 | `v2_directory_deleted` | state-check | T-V2-Retirement | **CONSUMER_LANDED + PASSING** (PR #2693 squash 2026-05-11 — calm-seal-831 deleted entire `src/v2/` directory: -158,670 lines; row #97 `method_template_projection_emit_shim_retirement_coherence` fail-closed coherence test passes with v2/ absent, attesting G-2 guardrails per `docs/audit/t-v2-g2-deletion-plan-and-guardrails.md`) | src/v2/ removed from workspace |
| 43 | `auto_parallelism_independent_binds_emit_parallel` | demonstration | T-Free-Consequences-Demonstration | **PASSING** (PR #2495 — parallel emit for independent binds landed 2026-05-10) | bind-independent → parallel emit |
| 44 | `auto_parallelism_dependent_binds_pending_lens_fail_closed` | demonstration | T-Free-Consequences-Demonstration | **PASSING** (PR #2523 — dependent binds emit sequential landed 2026-05-10) | dependent-bind fixture fails closed on pending scalar parallelism lens until real schedule lands |
| 45 | `auto_parallelism_branch_arms_serialize` | demonstration | T-Free-Consequences-Demonstration | **PASSING** (PR #2527 — branch arms serialize landed 2026-05-10) | branch arms sequenced |
Expand Down Expand Up @@ -294,7 +294,7 @@ This principle is NOT a separate lane; it's a per-lane gate-shape requirement ap
| 68 | `anthropic_wire_demonstration` | demonstration | T-Anthropic-Wire | **PASSING** (PR #2506 — codex anthropic wire demo merged 2026-05-10; `anthropic_messages_wire_demo_test.rs`) | deterministic mock; live-API NOT closure gate |
| 69 | `bridge_retirement_demonstration` | demonstration | T-Bridge-Retirement | **PASSING** (PR #2551 — bridge retirement demonstration landed 2026-05-10) | integration `bridge_retirement_demonstration` (`canonical_lens_bridge_ratchet_test.rs`); typed-identity-surface executes through `LensOutputEquals` using fixture-local `DeclarationRef` resolution + production `apply_lens_declaration` |
| 70 | `cost_lens_demonstration` | demonstration | T-CostLens-Composition | DECLARED — ε path RATIFIED 2026-05-07 (Q-Cost-Composition-Layering canvas at PR #2181); closes via Rust-side composition fixture demonstrating end-to-end cost reading per ε in T-CostLens follow-on slice | ≥2 algebra-instances + ≥1 recursive call |
| 71 | `v3_self_host_demonstration` | demonstration | T-V2-Retirement | DECLARED (NEW 2026-05-06) | bootstrap PB-Runtime trampoline runs end-to-end |
| 71 | `v3_self_host_demonstration` | demonstration | T-V2-Retirement | **CONSUMER_LANDED + PASSING** (PR #2696 squash `3e4bd97a` 2026-05-11 — still-crab-219 demonstration harness: fail-closed `--r3-gate-71-demonstration` path with in-memory `fixed_point_diff_ok` (C-5), `.dag` TestClaim + integration splice, SG-0 census + PR-body append, DB-8 strict flag, CI prepend + full-suite budget + TC1 slow-test exemption) | 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 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 |
Expand All @@ -315,7 +315,7 @@ This principle is NOT a separate lane; it's a per-lane gate-shape requirement ap
| 89 | `section_ref_substrate_landed` | substrate-shape | T-Lens-Application-Surface | CONSUMER_LANDED (Slice A receipt PR #2145) | SectionRef disjoint sum (DeclarationScope / NodeScope) in `src/v3/std/lens_application.dag` |
| 90 | `lens_enforcement_carrier_landed` | substrate-shape | T-Lens-Application-Surface | CONSUMER_LANDED (Slice A receipt PR #2145) | parametric `LensEnforcement<Output, Budget>` + `EnforceableLens<Output, Budget>` carriers in `src/v3/std/lens_application.dag`; per-lens data instances co-located with each lens land in Slice B |
| 91 | `enforce_violation_routing_landed` | structural-fold | T-Lens-Application-Surface | DECLARED — substrate routing surface landed PR #2145 (`DiagnosticSeverity = Error` + `EnforcedApplication.diagnostic_severity` + `LensEnforcement.violates`); CONSUMER_LANDED requires the fold-pass consumer per design doc §10 step 2 — deferred to Slice B | Enforce-mode violation routing through `DiagnosticSeverity` per design §3 + INVARIANTS C-8 |
| 92 | `complexity_violation_compile_error_demonstrated` | demonstration | T-Lens-Application-Surface | **CONSUMER_LANDED + PASSING** (PR #2340 — feat(v3): gate #92 T-LAS complexity enforcement compile error; consumer: `t_las_complexity_contract_demo.dag` + `t_las_complexity_contract_compile_error_test.rs`) | `EnforcedApplication` + `complexity_enforceable`; `complexity_of` > `ClassLog` ⇒ `ParseError` "lens enforcement violation" |
| 92 | `complexity_violation_compile_error_demonstrated` | demonstration | T-Lens-Application-Surface | **CONSUMER_LANDED + PASSING (consumer-disabled hot-fix-2026-05-12)** (Original consumer landing: PR #2340 — `t_las_complexity_contract_demo.dag` + `t_las_complexity_contract_compile_error_test.rs`. **2026-05-12 hot-fix housekeeping**: consumer-disabled via PR #2723 `#[ignore]` cut (cold-CI wall-time reduction; gate #92 was 14s wall on cold CI). PASSING evidence preserved in-tree at `t_las_complexity_contract_compile_error_test.rs` under `#[ignore]` marker; re-enables when T-LAS rebuild dispatch lands OnceLock/cached_compile/shared-fixture amortization. Rebuild ownership routing: pending Director surface — no standing T-LAS Mgr seat at present per PB Mgr → Director internal-message dispatch (warm-dove-618 → zesty-bear-812; not a GitHub comment thread) + gunbc#846 operator greenlight + PR #2725 §6 Cluster F ownership-gap.) | `EnforcedApplication` + `complexity_enforceable`; `complexity_of` > `ClassLog` ⇒ `ParseError` "lens enforcement violation" |
| 93 | `crdt_cost_basis_demonstrated` | demonstration | T-Lens-Application-Surface | DECLARED (added to §"Acceptance" 2026-05-06) | CRDT cost basis via apply_lens |
| 94 | `memory_peak_cost_basis_demonstrated` | demonstration | T-Lens-Application-Surface | **CONSUMER_LANDED + PASSING** (#1954 — `memory_peak_cost` + cementing demo; **Enforce**: `memory_peak_enforcement_violates` is true iff `!dominates(declared_budget, observed_peak)` (budget covers peak in the `SymbolicCost` order; ties + incomparable cases unit-pinned); **`SizeVariable`** matches `src/v3/std/algebra.dag` incl. optional `display_name`; parser `apply_lens(cost, …, Enforce { dimension: Memory, … })` still awaits gate #91) | memory-peak cost basis |
| 95 | `opt_in_iteration_parallelism_via_lens_application_demonstrated` | demonstration | T-Lens-Application-Surface / **Cluster F (T-LP-Retirement)** | **R3-LOAD-BEARING (carve-promoted-IN-R3 2026-05-09)** per Director ratification at gunbc#846 #issuecomment-4412330468 (cascade-promotion with C1 #81). Worked-example demo via `apply_lens(parallelism, fn, Enforce)`. Cascade-gates on F-α completion (parallelism BEHAVIORALLY COMPLETE #81) + T-LAS Slice B substrate landing (#91 per-lens LensEnforcement projection per `docs/design-lens-application-surface.md` §4.4 / §7). Cluster F sub-phase F-γ.1. See `docs/audit/r3-cluster-f-sequencing-plan-2026-05-09.md` §1.4.1. Prior R4-CARVED (C1 cascade) status DISSOLVED. |
Expand Down
Loading