diff --git a/docs/audit/r3-close-predicate-execution-2026-05-13.md b/docs/audit/r3-close-predicate-execution-2026-05-13.md index 3bee7e8e2a0..eb533a3e59b 100644 --- a/docs/audit/r3-close-predicate-execution-2026-05-13.md +++ b/docs/audit/r3-close-predicate-execution-2026-05-13.md @@ -146,7 +146,7 @@ Close-time canonical predicate harness for `PASSING` / `SATISFIED-BY-CONSTRUCTIO | 80 | `cost_lens_behaviorally_complete` | structural-fold | **HARNESS_NAMED** | `cargo test --workspace --exclude gunbc-dag-tests` (HEAD ratchet `cost_lens_behaviorally_complete` and sibling ratchets cited under §1.8 row #80 Notes); cross-ref `docs/r3-structure.md` §Acceptance gate #80. | Harness named; execution receipt is produced by the §10 close-ceremony 24h workspace re-sweep, not by this Phase 2 PR. See §Workspace batch receipt for the partial fmt + clippy receipts captured during Phase 2 authoring. | | 81 | `parallelism_lens_behaviorally_complete` | structural-fold | **N/A_NOT_PASSING** | Predicate not yet load-bearing: §1.8 Status `R3-LOAD-BEARING` carve-promoted (declaration-stage; no PASSING claim) per §1.8 row #81 Notes. | NOT_APPLICABLE_AT_HEAD — §8 predicate-execution requirement attaches only to PASSING gates. | | 82 | `effect_enumeration_lens_behaviorally_complete` | structural-fold | **N/A_NOT_PASSING** | Predicate not yet load-bearing: §1.8 Status `R3-LOAD-BEARING` carve-promoted (declaration-stage; no PASSING claim) per §1.8 row #82 Notes. | NOT_APPLICABLE_AT_HEAD — §8 predicate-execution requirement attaches only to PASSING gates. | -| 83 | `lens_capability_register_zero_proxy_zero_stub` | state-check | **N/A_NOT_PASSING** | Predicate not yet load-bearing: §1.8 Status `DECLARED` (no PASSING claim at HEAD) per §1.8 row #83 Notes. | NOT_APPLICABLE_AT_HEAD — §8 predicate-execution requirement attaches only to PASSING gates. | +| 83 | `lens_capability_register_zero_proxy_zero_stub` | state-check | **N/A_NOT_PASSING** | Predicate not yet load-bearing: §1.8 Status `DECLARED` (canonical Gap-4 / F-γ.2 Pass not satisfied at HEAD) per §1.8 row #83 Notes; partial supporting harness `lens_register_correspondence_test.rs` (`lens_register_correspondence` filter) does not advance the ledger status (INVARIANTS P2). | NOT_APPLICABLE_AT_HEAD — §8 predicate-execution requirement attaches only to PASSING gates. | | 84 | `every_rust_test_ports_to_dag_or_generated` | state-check | **N/A_NOT_PASSING** | Predicate not yet load-bearing: §1.8 Status `DECLARED` (no PASSING claim at HEAD) per §1.8 row #84 Notes. | NOT_APPLICABLE_AT_HEAD — §8 predicate-execution requirement attaches only to PASSING gates. | | 85 | `forall_exists_quantifier_substrate_landed` | substrate-shape | **N/A_NOT_PASSING** | Predicate not yet load-bearing: §1.8 Status `DECLARED` (no PASSING claim at HEAD) per §1.8 row #85 Notes. | NOT_APPLICABLE_AT_HEAD — §8 predicate-execution requirement attaches only to PASSING gates. | | 86 | `program_generator_carrier_landed` | substrate-shape | **HARNESS_NAMED** | `cargo test --workspace --exclude gunbc-dag-tests` (HEAD ratchet `program_generator_carrier_landed` and sibling ratchets cited under §1.8 row #86 Notes); cross-ref `docs/r3-structure.md` §Acceptance gate #86. | Harness named; execution receipt is produced by the §10 close-ceremony 24h workspace re-sweep, not by this Phase 2 PR. See §Workspace batch receipt for the partial fmt + clippy receipts captured during Phase 2 authoring. | diff --git a/docs/design-section-1-8-acceptance-aggregator-pattern.md b/docs/design-section-1-8-acceptance-aggregator-pattern.md index 917b630dbdd..99a7a37a175 100644 --- a/docs/design-section-1-8-acceptance-aggregator-pattern.md +++ b/docs/design-section-1-8-acceptance-aggregator-pattern.md @@ -109,7 +109,7 @@ These 6 NEW §1.8 rows participate in the canonical arithmetic (close-gate count Same view pattern generalizes to sibling clusters at low cost. Each candidate MUST pass the precondition + exclusion rules over its §1.8 constituents before being added to §1.9: - **Cluster M** (T-Tests-As-Data-Completeness) — view over §1.8 #84/#85/#86/#87 (per `docs/audit/r3-cluster-m-sequencing-plan-2026-05-09.md` 3-phase plan); view-ready once constituents' Status cells coerce cleanly -- **Cluster F** (T-Lens-Behavioral-Parity) — candidate view over the 4-lens parity rows (#79 complexity, #80 cost, #81 parallelism, #82 effect_enumeration). **NOT view-ready at HEAD**: §1.8 rows #81 and #82 (and #95) carry bare `R3-LOAD-BEARING` as scope-metadata in the Status cell with no closure-progress inlined; these rows fail the precondition. Row #83 (`lens_capability_register_zero_proxy_zero_stub`) is a positive counter-example — its Status cell already reads "**DECLARED — full scope IN R3 (carve-promotion-IN-R3 2026-05-09)**", inlining closure-progress alongside the scope-metadata, so #83 already coerces to `DECLARED` under the precondition rule. **Pre-pilot fix required for #81/#82/#95**: their §1.8 cells must follow #83's pattern and inline closure-progress (e.g., `R3-LOAD-BEARING — DECLARED`) before the Cluster F view can be added. +- **Cluster F** (T-Lens-Behavioral-Parity) — candidate view over the 4-lens parity rows (#79 complexity, #80 cost, #81 parallelism, #82 effect_enumeration). **NOT view-ready at HEAD**: §1.8 rows #81 and #82 (and #95) carry bare `R3-LOAD-BEARING` as scope-metadata in the Status cell with no closure-progress inlined; these rows fail the precondition. Row #83 (`lens_capability_register_zero_proxy_zero_stub`) is **DECLARED** in the §1.8 ledger (canonical Pass = Gap-4 / F-γ.2); `lens_register_correspondence_test.rs` supplies **supporting** executable evidence for a **narrow** register slice only (cited in row #83 Notes + Gap 4) and does **not** unblock the Cluster F view. **Pre-pilot fix required for #81/#82/#95**: their §1.8 cells must inline closure-progress (e.g., `R3-LOAD-BEARING — DECLARED` or PASSING receipts) before the Cluster F view can be added. - **Cluster K** — view scope TBD per `docs/audit/r3-cluster-analysis-2026-05-09.md` §2; precondition check required at pilot time - **T-V2-Retirement** — view over v2 retirement constituent gates; precondition check required at pilot time diff --git a/docs/r3-actual-close-plan.md b/docs/r3-actual-close-plan.md index a36975a1ed9..6aab7f34332 100644 --- a/docs/r3-actual-close-plan.md +++ b/docs/r3-actual-close-plan.md @@ -143,8 +143,7 @@ The closure-ledger was refreshed against HEAD on 2026-05-14 UTC. Close still req - #80 cost = **PASSING** ✓ - #81 parallelism = **R3-LOAD-BEARING**, F-α sub-phase pending (Stage 2e walker port from `workflow_parallelism.rs` → `.dag`) - #82 effect_enum = **R3-LOAD-BEARING**, F-β.1 canvas + F-β.2 atomic-migration pending -- #83 `lens_capability_register_zero_proxy_zero_stub` (**§1.8 program gate / Cluster F sub-phase F-γ.2**) = **DECLARED** — canonical receipt is the **post-all-four-BEHAVIORALLY-COMPLETE** register cascade per `docs/audit/r3-cluster-f-sequencing-plan-2026-05-09.md` §1.4.2 and `docs/r3-structure.md` §Acceptance (not merely "no PROXY/STUB" while two rows stay **PARTIAL**). `parallelism.dag` and `effect_enumeration.dag` remain **PARTIAL** in `docs/v3-lens-capability-register.md` and `std.verification` `lens_capability_register_rows` until **#81** / **#82** land; **§1.8 #83 PASSING** stays **downstream of F-γ.2** (INVARIANTS P2 — one close predicate; no dilution). -- **Narrow CI ratchet (green at HEAD, necessary not sufficient):** `lens_register_correspondence_test::r3_gate_83_lens_capability_register_has_zero_proxy_zero_stub` enforces **zero** `BEHAVIORALLY PROXY` / **zero** `BEHAVIORALLY STUB` on the four T-LBP basenames in the markdown capability table — does **not** replace the F-γ.2 §1.8 gate. +- #83 `lens_capability_register_zero_proxy_zero_stub` (**§1.8 program gate / Cluster F sub-phase F-γ.2**) = **DECLARED** — canonical receipt is the **post-all-four-BEHAVIORALLY-COMPLETE** register cascade per `docs/audit/r3-cluster-f-sequencing-plan-2026-05-09.md` §1.4.2 and `docs/r3-structure.md` §Acceptance (not merely PROXY/STUB-zero while two rows stay **PARTIAL**). `parallelism.dag` and `effect_enumeration.dag` remain **PARTIAL** in `docs/v3-lens-capability-register.md` and `std.verification` `lens_capability_register_rows` until **#81** / **#82** land. **Supporting CI (necessary not sufficient):** `lens_register_correspondence_test.rs` (`every_regen_lens_entry_has_a_capability_register_row`, `r3_gate_83_lens_capability_register_scope_is_explicit`, `r3_gate_83_lens_capability_register_has_zero_proxy_zero_stub`, `lens_capability_register_rows_match_md_v2_cementing_projection`) — regen→register discipline, **zero** `BEHAVIORALLY PROXY` / **zero** `BEHAVIORALLY STUB` on the four T-LBP basenames in the markdown capability table, and Band-C v2-cementing-slice alignment vs `std.verification` `lens_capability_register_rows`; **does not** advance the §1.8 ledger Status for gate #83 (INVARIANTS P2 — one predicate; no parallel "narrow PASSING" row state). **What's missing**: - Complexity: `ComplexitySummary` TestClaim literals (bridge-Rust to native-.dag migration) diff --git a/docs/r3-program-plan.md b/docs/r3-program-plan.md index 69860e164a1..4e09b30d7e4 100644 --- a/docs/r3-program-plan.md +++ b/docs/r3-program-plan.md @@ -105,7 +105,7 @@ Per PR #2358 §8 meta-finding (closure-claims-vs-HEAD drift): the prior "94 R3-l R3 closes when **all 105 R3-load-bearing §1.8 gates** pass + zero tracked-debt rows survive (`r3_debt_paydown_zero_remaining`). -**~~R4-carved §1.8 rows~~** — **DISSOLVED 2026-05-09** per Director carve-promotion-IN-R3 ratification at gunbc#846 #issuecomment-4412330468 + (a) ratification at #issuecomment-4412380947 + operator framing 2026-05-09 ("0 hand-Rust including tests AND stage0; bootstrap is data + self-generated"). Gates **#81** `parallelism_lens_behaviorally_complete` + **#82** `effect_enumeration_lens_behaviorally_complete` + **#95** `opt_in_iteration_parallelism_via_lens_application_demonstrated` are **R3-load-bearing** within **Cluster F (T-LP-Retirement)** per [`docs/audit/r3-cluster-f-sequencing-plan-2026-05-09.md`](audit/r3-cluster-f-sequencing-plan-2026-05-09.md) (landed via PR #2364 Task 12 amendment). Gate **#83** `lens_capability_register_zero_proxy_zero_stub` scope-narrowing dissolves; #83 now fires for ALL 4 in-R3 lenses (complexity + cost + parallelism + effect_enum). `docs/r4-carve-out-routing.md` C1/C2/C3 entries amended to dissolved-status. R3 close target: **105 R3-load-bearing gates green** (no carves; only #11 canvas-deferral subtracted per Director (a)-disposition 2026-05-09; +6 T-WAD FULL R3 gates 2026-05-12 + 1 Miss-class dissolution 2026-05-12 + 1 cost-textbook-coverage 2026-05-13 + 1 show-correct-code diagnostic coverage 2026-05-13 — see §1.5 canonicalization above + §1.8 row #11 status + §1.8 rows #98–#103 + §1.8 rows #105–#106). +**~~R4-carved §1.8 rows~~** — **DISSOLVED 2026-05-09** per Director carve-promotion-IN-R3 ratification at gunbc#846 #issuecomment-4412330468 + (a) ratification at #issuecomment-4412380947 + operator framing 2026-05-09 ("0 hand-Rust including tests AND stage0; bootstrap is data + self-generated"). Gates **#81** `parallelism_lens_behaviorally_complete` + **#82** `effect_enumeration_lens_behaviorally_complete` + **#95** `opt_in_iteration_parallelism_via_lens_application_demonstrated` are **R3-load-bearing** within **Cluster F (T-LP-Retirement)** per [`docs/audit/r3-cluster-f-sequencing-plan-2026-05-09.md`](audit/r3-cluster-f-sequencing-plan-2026-05-09.md) (landed via PR #2364 Task 12 amendment). Gate **#83** `lens_capability_register_zero_proxy_zero_stub` scope-narrowing dissolves; #83 now fires for ALL 4 in-R3 lenses (complexity + cost + parallelism + effect_enum). **§1.8 row #83 Status** stays **DECLARED** until the **single** Gap-4 / F-γ.2 Pass (all-four **BEHAVIORALLY COMPLETE** in register authority) is satisfied — INVARIANTS P2 single ledger row, no parallel “narrow PASSING” closure state. **`lens_register_correspondence_test.rs`** is **supporting evidence** (narrow PROXY/STUB-zero + regen↔register + Band-C projection; green at HEAD) cited in that row’s Notes + `docs/r3-actual-close-plan.md` Gap 4, **necessary not sufficient**, downstream of **#81**/**#82**. `docs/r4-carve-out-routing.md` C1/C2/C3 entries amended to dissolved-status. R3 close target: **105 R3-load-bearing gates green** (no carves; only #11 canvas-deferral subtracted per Director (a)-disposition 2026-05-09; +6 T-WAD FULL R3 gates 2026-05-12 + 1 Miss-class dissolution 2026-05-12 + 1 cost-textbook-coverage 2026-05-13 + 1 show-correct-code diagnostic coverage 2026-05-13 — see §1.5 canonicalization above + §1.8 row #11 status + §1.8 rows #98–#103 + §1.8 rows #105–#106). **Two distinct Pass surfaces** (per Debt-Paydown Mgr poke-hole 2026-05-06 — clarification prevents conflating predicates): - **Lane `.dag` TestClaim gates (106 enumerated; 105 R3-load-bearing post-carve-promotion 2026-05-09 + T-WAD FULL R3 elevation 2026-05-12 — only #11 canvas-deferred)**: per-lane closure predicates passing via `.dag` evaluation, runtime demonstration, or CI consumer (per §1.7 status taxonomy). @@ -128,7 +128,6 @@ Predicate cannot be satisfied by deletion-of-rows-without-actual-resolution; eac - §1.8 **#97** **`method_template_projection_emit_shim_retirement_coherence`** — **CONSUMER_LANDED + PASSING** via **`src/v3/compiler/tests/integration/method_template_projection_emit_shim_coherence_test.rs`** (Gunbc **[#1982](https://github.com/gunb-ai/gunbc/issues/1982)** / Q-V2-Retirement-Boundary-Matrix). - §1.8 **#28** **`omni_layers_share_one_node_tree`** (T-Omni-Shape-B structural-fold) — **CONSUMER_LANDED + PASSING** via **`src/v3/compiler/tests/integration/m1_5_omni_shape_b_openapi_test.rs`** (`omni_layers_share_one_node_tree`). - §1.8 **#29** **`anthropic_wire_typed_serde_alignment`** (T-Anthropic-Wire substrate-shape) — **PASSING** via **`src/v2/tests/src/pipeline.rs`** ratchets `anthropic_request_coproduct_wire_contracts_emit_targeted_serde` (`:6482`) + `anthropic_messages_request_body_json_matches_messages_wire_tags` (`:6918`); 200-body residual scoped separately to `structural_coverage_gap_anthropic_messages_200_residual`. - Per openai-pro meta-review on PR #1808 sha `cf249389` ([#issuecomment-4384405832](https://github.com/gunb-ai/gunbc/pull/1808#issuecomment-4384405832)) PAUSE_AND_REGROUP verdict — structurally honest framing of where this PR sits in the closure-evidence chain: **Per-gate status taxonomy:** @@ -143,7 +142,7 @@ Per openai-pro meta-review on PR #1808 sha `cf249389` ([#issuecomment-4384405832 **State-check / ledger / CI-discipline families (orthogonal to §P2 generated-consumer):** For **predicate-family** rows that are **not** substrate-shape (see §1.8 legend — e.g. **state-check**, **ledger-count**, **CI-discipline**), **CONSUMER_LANDED** means the **§1.7** sense only: an executable runner, integration harness, or fail-closed host ratchet exists for the gate id over the coverage it implements (same pattern as §1.8 **#1** `termination_lattice_rust_mirror_dissolved`, **#4** `tier3_effect_carrier_mirror_dissolved`, and **#97** shim coherence). That is **not** the INVARIANTS §P2 “generated consumer proof” bar, which applies only where this paragraph’s substrate-boundary condition is in scope. -**Status at HEAD**: per §1.8 canonical ledger Status column — most gates are **DECLARED**; `pb_self_compile_fixed_point` is a canonical CONSUMER_LANDED exemplar (R1 horizon Pass = current `verification.dag` + `test_runner` evaluation). **`method_template_projection_emit_shim_retirement_coherence` (§1.8 #97)**, **`omni_layers_share_one_node_tree` (§1.8 #28)**, and **`anthropic_wire_typed_serde_alignment` (§1.8 #29)** are **CONSUMER_LANDED + PASSING** via the integration tests / ratchets cited in the §1.8 ledger rows. **`numeric_abstract_carriers_landed` (§1.8 #17)** is **DECLARED** — carriers + lowering + hand-written ratchet are landed; **CONSUMER_LANDED** (§P2 sense: generated consumer proof) is **not** claimed until that generator exists. `tier3_*_mirror_dissolved` gates are advancing through T-Tier3-Dissolution per §1.8 row-level Status: **#1** `tier3_termination_mirror_dissolved` and **#4** `tier3_effect_carrier_mirror_dissolved` are **CONSUMER_LANDED + PASSING** at HEAD; **#2** `tier3_computation_mirror_dissolved` and **#3** `tier3_induction_mirror_dissolved` are **CONSUMER_LANDED** (stacked narrow-slice receipts per §1.8 Notes — e.g. **#2** includes PR #2789 trivial-constructor retirement plus `kernel_algebra_profile` substrate-authority delegation ratchet `tier3_computation_mirror_kernel_algebra_profile_substrate_authority` with INVARIANTS §P5 row for `m2_substrate_inhabitance_test.rs`; wider mirror dissolution remains lane-tracked pending evaluated `std.termination` / `std.computation` / `std.induction` block bodies). Per-gate status updates flow through the §1.8 ledger as Mgrs land consumer infrastructure per their lane scope; the 16 NEW gates added 2026-05-06 in PR #1808 were DECLARED-only at that time — current Status for each row is the §1.8 ledger value, not this paragraph. +**Status at HEAD**: per §1.8 canonical ledger Status column — most gates are **DECLARED**; `pb_self_compile_fixed_point` is a canonical CONSUMER_LANDED exemplar (R1 horizon Pass = current `verification.dag` + `test_runner` evaluation). **`method_template_projection_emit_shim_retirement_coherence` (§1.8 #97)**, **`omni_layers_share_one_node_tree` (§1.8 #28)**, and **`anthropic_wire_typed_serde_alignment` (§1.8 #29)** are **CONSUMER_LANDED + PASSING** via the integration tests / ratchets cited in the §1.8 ledger rows. **`lens_capability_register_zero_proxy_zero_stub` (§1.8 #83)** is **DECLARED** in the ledger (canonical Pass = Gap-4 / F-γ.2); supporting integration ratchet in `lens_register_correspondence_test.rs` is cited in row #83 Notes + Gap 4 — **not** a second §1.7 status for the same gate id. **`numeric_abstract_carriers_landed` (§1.8 #17)** is **DECLARED** — carriers + lowering + hand-written ratchet are landed; **CONSUMER_LANDED** (§P2 sense: generated consumer proof) is **not** claimed until that generator exists. `tier3_*_mirror_dissolved` gates are advancing through T-Tier3-Dissolution per §1.8 row-level Status: **#1** `tier3_termination_mirror_dissolved` and **#4** `tier3_effect_carrier_mirror_dissolved` are **CONSUMER_LANDED + PASSING** at HEAD; **#2** `tier3_computation_mirror_dissolved` and **#3** `tier3_induction_mirror_dissolved` are **CONSUMER_LANDED** (stacked narrow-slice receipts per §1.8 Notes — e.g. **#2** includes PR #2789 trivial-constructor retirement plus `kernel_algebra_profile` substrate-authority delegation ratchet `tier3_computation_mirror_kernel_algebra_profile_substrate_authority` with INVARIANTS §P5 row for `m2_substrate_inhabitance_test.rs`; wider mirror dissolution remains lane-tracked pending evaluated `std.termination` / `std.computation` / `std.induction` block bodies). Per-gate status updates flow through the §1.8 ledger as Mgrs land consumer infrastructure per their lane scope; the 16 NEW gates added 2026-05-06 in PR #1808 were DECLARED-only at that time — current Status for each row is the §1.8 ledger value, not this paragraph. **R3 close criteria implies CONSUMER_LANDED for all R3-load-bearing §1.8 gates** (106 enumerated **minus** **#11** canvas-deferred per Director (a)-disposition 2026-05-09 = **105 R3-load-bearing**; #81/#82/#95 carve-promoted-IN-R3 per Director ratification 2026-05-09 c#4412330468; +6 T-WAD FULL R3 gates #98–#103 per Director (b) ledger-sync disposition msg_2a68a4b5 — see §1.5 above): declarations alone don't satisfy `r3_debt_paydown_zero_remaining` or the substrate-gap-class closures or the demonstration principle. Per Brian directive `feedback_no_textual_enforcement_bridges` + Director poke-hole 2026-05-06 finding 1.1 (demo-gate minimum bar) — closure requires runtime-executable verification, not document-level claims. @@ -308,7 +307,7 @@ This principle is NOT a separate lane; it's a per-lane gate-shape requirement ap | 80 | `cost_lens_behaviorally_complete` | structural-fold | T-Lens-Behavioral-Parity | **PASSING** — gate #80 abstract-cost scope now has executable `DimensionReport` wiring via `analyze_symbolic_cost_dimension`, `SizeVariable` value identity by `source_port`, recursive `CallPattern` consumption, and Band-C frozen-projection cementing in `cost_lens_symbolic_consumer_test.rs`; target-realization composition remains tracked separately by T-CostLens gates #37/#40/#70 | Dimension wiring + SizeVar value semantics + cementing test | | 81 | `parallelism_lens_behaviorally_complete` | structural-fold | T-Lens-Behavioral-Parity / **Cluster F (T-LP-Retirement)** | **R3-LOAD-BEARING (carve-promoted-IN-R3 2026-05-09)** per Director ratification at gunbc#846 #issuecomment-4412330468; Stage 2e walker port from `workflow_parallelism.rs` → `.dag` per Cluster F sub-phase F-α (substrate-ready M-sized lane). See `docs/audit/r3-cluster-f-sequencing-plan-2026-05-09.md` §1.1. Prior R4-CARVED (C1) status DISSOLVED. | | 82 | `effect_enumeration_lens_behaviorally_complete` | structural-fold | T-Lens-Behavioral-Parity / **Cluster F (T-LP-Retirement)** | **R3-LOAD-BEARING (carve-promoted-IN-R3 2026-05-09)** per Director ratification cascade at gunbc#846 #issuecomment-4412380947 → #4412433924 → #4412475559. Cluster F sub-phases **F-β.1 (migration-shape ratification canvas)** + **F-β.2 (atomic-migration implementation)** using existing `services.dag::Operation` carrier per locked design `docs/design-effect-enumeration-resource-threading.md` §3.2 + §6.2 ("Operation carrier already exists at services.dag:122; no new top-level carrier required"). F-β.1 canvas authoring stays in Substrate Mgr standing authority; Director ratifies surfaced migration-shape questions (Operation field reads / walker rewire surface / test-consumer breaking changes); F-β.2 worker dispatches against ratified shape. See `docs/audit/r3-cluster-f-sequencing-plan-2026-05-09.md` §1.2-§1.3. Prior R4-CARVED (C2) status DISSOLVED. | -| 83 | `lens_capability_register_zero_proxy_zero_stub` | state-check | T-Lens-Behavioral-Parity / **Cluster F sub-phase F-γ** | **DECLARED — full scope IN R3 (carve-promotion-IN-R3 2026-05-09)** per Director carve-promotion ratification at gunbc#846 #issuecomment-4412330468. Prior C3 scope-narrowing ("ZERO PROXY / ZERO STUB for in-scope lenses (complexity + cost) only") DISSOLVED — register status now fires for **ALL 4 in-R3 lenses** (complexity + cost + parallelism + effect_enum) at R3 close per carve-promotion. Cluster F sub-phase F-γ.2 (post-all-4-lenses-BEHAVIORALLY-COMPLETE cascade). See `docs/audit/r3-cluster-f-sequencing-plan-2026-05-09.md` §1.4.2. | +| 83 | `lens_capability_register_zero_proxy_zero_stub` | state-check | T-Lens-Behavioral-Parity / **Cluster F sub-phase F-γ** | **DECLARED — full scope IN R3 (carve-promotion-IN-R3 2026-05-09)** per Director ratification at gunbc#846 #issuecomment-4412330468. Prior C3 scope-narrowing ("ZERO PROXY / ZERO STUB for in-scope lenses (complexity + cost) only") **DISSOLVED** — Pass condition fires for **all 4 in-R3 lenses** (complexity + cost + parallelism + effect_enum) at R3 close per carve-promotion. **Canonical §1.8 Pass** = **post-all-four-BEHAVIORALLY-COMPLETE** register cascade (Cluster F sub-phase F-γ.2 / Gap-4) per `docs/r3-actual-close-plan.md` and `docs/audit/r3-cluster-f-sequencing-plan-2026-05-09.md` §1.4.2 — **single** ledger status until satisfied (INVARIANTS P2). **`lens_register_correspondence_test.rs`** (`every_regen_lens_entry_has_a_capability_register_row`, `r3_gate_83_lens_capability_register_scope_is_explicit`, `r3_gate_83_lens_capability_register_has_zero_proxy_zero_stub`, `lens_capability_register_rows_match_md_v2_cementing_projection`) is **supporting CI evidence** only: regen→`docs/v3-lens-capability-register.md` `## Capability table`, **zero** `BEHAVIORALLY PROXY` / **zero** `BEHAVIORALLY STUB` on the four T-LBP basenames, Band-C v2-cementing-slice alignment vs `std.verification` `lens_capability_register_rows` — **necessary not sufficient**; does **not** advance this Status cell while `parallelism.dag` / `effect_enumeration.dag` stay **PARTIAL** pending **#81**/**#82**. | | 84 | `every_rust_test_ports_to_dag_or_generated` | state-check | T-Tests-As-Data-Completeness | **DECLARED — substrate-shape-readiness landed** (PR #3040, merge 7c2936150). `GeneratedFromDag` now carries `manifest_entries: List` with the `PendingFact | ResolvedFact` sum-variant split (no fabricated provenance per INVARIANTS P3 / C-9; Director ratification msg_3b99a90f). **Gap 5 actual close still gated** on the follow-up Evaluator-Mgr-owned runtime PR (3-way byte-equality assertion + directory-walk orphan-output detection at the well-known `tests/` scan-root) per Director Q-RegenCapability **β SPLIT** disposition (msg_606e0e50) + brief §7.1. Verification-Mgr-owned per-file FixtureMapping enumeration follow-up (§7.2) materialises `ResolvedFact` instances once the runtime PR lands. | thesis facet 3; every Rust test ports | | 85 | `forall_exists_quantifier_substrate_landed` | substrate-shape | T-Tests-As-Data-Completeness | **DECLARED** — Carriers landed: `Quantifier { ForAll, Exists }`, `QuantifiedTestClaim`, `SuiteClaim` in `src/v3/std/verification.dag` via PR #2647 (vivid-dove-106 / #2613 / Cluster M Phase 1a); bootstrap snapshots regenerated by `regen_bootstrap`; `m1_5_verification_test.rs` references the new types as a hand-written integration ratchet. **CONSUMER_LANDED not claimed**: per §1.7 P2 vs taxonomy + row #17 precedent, INVARIANTS §P2 requires a **generated** consumer of the declared surface; SuiteClaim wrapper migration of `TestSuite.claims` (Phase 1 follow-on per design §6 line 344) + V Mgr #87 (#2609) generated/runner consumer must land before CONSUMER_LANDED, then PASSING. | ForAll / Exists quantifier substrate | | 86 | `program_generator_carrier_landed` | substrate-shape | T-Tests-As-Data-Completeness | **CONSUMER_LANDED + PASSING** — `ProgramGenerator` + `ProgramShape` carriers landed in `src/v3/std/verification.dag`; generated bootstrap snapshots refreshed by `regen_bootstrap`. **Refined shape PASSING preserved in-place** (PR #3040, merge 7c2936150): `GeneratedFromDag.manifest_entries: List` (sum-variant `PendingFact | ResolvedFact` per Director msg_3b99a90f) replaces the prior `generated_paths: List` shape; `t_pb_b_1_dag_runner_test::r1c_d_pb_census_gates_suite_evaluates_through_runner` continues green under the refined carrier. | ProgramGenerator substrate carrier; follow-on quantified-claim consumer wiring remains under #85/#84 | diff --git a/docs/r3-structure.md b/docs/r3-structure.md index 92f6c4a4ee5..cd44d26568d 100644 --- a/docs/r3-structure.md +++ b/docs/r3-structure.md @@ -147,7 +147,7 @@ L6 (`l6_structural_form_coverage`) was moved out of this lane during the engine- - `cost_lens_behaviorally_complete` — **IN R3** — `Dimension` wiring; `SizeVar` value semantics; cementing test against frozen v2-oracle snapshot - `parallelism_lens_behaviorally_complete` — **R3-LOAD-BEARING (carve-promoted-IN-R3 2026-05-09)** within Cluster F sub-phase F-α — Stage 2e parallelism walker port from `workflow_parallelism.rs` to `.dag` (substrate-ready M-sized lane). Prior R4-CARVED (C1) status DISSOLVED. - `effect_enumeration_lens_behaviorally_complete` — **R3-LOAD-BEARING (carve-promoted-IN-R3 2026-05-09)** within Cluster F sub-phases F-β.1 (migration-shape canvas) + F-β.2 (atomic-migration implementation). Uses existing `services.dag::Operation` carrier per locked design `docs/design-effect-enumeration-resource-threading.md` §3.2 + §6.2 ("Operation carrier already exists at services.dag:122; no new top-level carrier required"). Prior R4-CARVED (C2) status DISSOLVED. - - `lens_capability_register_zero_proxy_zero_stub` — **DECLARED — full scope IN R3 (carve-promotion-IN-R3 2026-05-09)** — register status ZERO PROXY / ZERO STUB **for ALL 4 in-R3 lenses** (complexity + cost + parallelism + effect_enum) at R3 close per `docs/v3-lens-capability-register.md`. Cluster F sub-phase F-γ.2 (post-all-4-lenses-BEHAVIORALLY-COMPLETE cascade). Prior C3 scope-narrowing DISSOLVED. + - `lens_capability_register_zero_proxy_zero_stub` — **DECLARED — full scope IN R3 (carve-promotion-IN-R3 2026-05-09)** — canonical §1.8 Pass = Gap-4 / F-γ.2 **post-all-four-BEHAVIORALLY-COMPLETE** register cascade (INVARIANTS P2 single ledger status). Carve-promotion: prior C3 scope-narrowing DISSOLVED — obligation covers **all 4 in-R3 lenses**. **Supporting CI** (not a second closure state): `lens_register_correspondence_test.rs` fail-closes narrow regen→register + PROXY/STUB-zero + Band-C projection slice; **#81**/**#82** + PARTIAL→COMPLETE remain downstream per `docs/r3-actual-close-plan.md` Gap 4. - `lens_read_witness_shape_dissolved` (NEW 2026-05-12 per Director ratification msg_915aa2c1 + operator directive 2026-05-11 audit §0 "Miss should go away entirely; if something in substrate defines a Miss it should fail and be investigated asap") — All `Lookup` lens read-channel constructions dissolved; lens `read: (Dag, Behavior) → Witness` honors locked-discipline shape (`Witness::Inhabits | Violates { reason, at }`) without parallel `Lookup::Miss` deferral surface. Bundled-migration shape per Director ratification: TWO parallel migrations bundled atomically per §P5 — (1) **Substrate-level** (collapse `Lookup::Miss` → `Witness::Violates { reason, at }` across 70 sites in 6 files at HEAD: `src/v3/lenses/cost.dag` 25 + `complexity.dag` 25 + `infer_helpers.dag` 3 + `src/v3/std/algebra.dag` 3 + `substrate.dag` 3 + `lookup.dag` 11; Phase 1 cost+complexity bundle (50), Phase 2 monomorphized accessor sweep (9), Phase 3 lookup.dag terminal carrier deletion (11)); (2) **Testgen-level** (per-lens TestClaim asserting universal coverage `∀ bind ∈ bootstrap. lens_read(bind) ∈ Inhabits(_)`; fail-closed on `Violates`). Two-part predicate: Part A = `git grep -nE "Lookup<" src/v3/lenses/ src/v3/std/ ; expected = 0` (terminal); Part B = `git grep -nE "::Miss\b" src/v3/compiler/src/lens_*_generated.rs ; expected = 0` (regression guard). See `docs/r3-program-plan.md` §1.8 row #104 for full receipt - **T-Tests-As-Data-Completeness** (NEW 2026-05-02; gate IDs added 2026-05-06 to §"Acceptance" per codex BLOCKING).