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
2 changes: 1 addition & 1 deletion docs/audit/r3-close-predicate-execution-2026-05-13.md
Original file line number Diff line number Diff line change
Expand Up @@ -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. |
Expand Down
2 changes: 1 addition & 1 deletion docs/design-section-1-8-acceptance-aggregator-pattern.md
Original file line number Diff line number Diff line change
Expand Up @@ -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

Expand Down
3 changes: 1 addition & 2 deletions docs/r3-actual-close-plan.md
Original file line number Diff line number Diff line change
Expand Up @@ -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)
Expand Down
Loading
Loading