diff --git a/docs/r3-program-plan.md b/docs/r3-program-plan.md index dbc37a971b2..c0bbfe58f26 100644 --- a/docs/r3-program-plan.md +++ b/docs/r3-program-plan.md @@ -204,7 +204,7 @@ This principle is NOT a separate lane; it's a per-lane gate-shape requirement ap ### §1.8 Canonical R3 Closure-Authority Ledger (per openai-pro meta-review structural recommendation; Brian B2 path-(b) ratified 2026-05-06) -**Single canonical view of all 104 closure gates** (was 97; +6 T-WAD FULL R3 elevation 2026-05-12) — consolidates per-lane enumeration in `r3-structure.md` §"Acceptance" + plan §1.5 count summary + §1.6 demonstration audit + §1.7 status taxonomy into one row-per-gate table. Eliminates "duplicate authority" class of cross-doc consistency findings (per openai-pro 2026-05-06 PAUSE_AND_REGROUP verdict). +**Single canonical view of all 104 closure gates** (was 97; +6 T-WAD FULL R3 elevation 2026-05-12; +1 Miss-class dissolution 2026-05-12) — consolidates per-lane enumeration in `r3-structure.md` §"Acceptance" + plan §1.5 count summary + §1.6 demonstration audit + §1.7 status taxonomy into one row-per-gate table. Eliminates "duplicate authority" class of cross-doc consistency findings (per openai-pro 2026-05-06 PAUSE_AND_REGROUP verdict). **Predicate-family legend**: - **substrate-shape**: declarations of carriers/types/algebra in `dsl/std/` (state-fact) @@ -329,7 +329,7 @@ This principle is NOT a separate lane; it's a per-lane gate-shape requirement ap | 101 | `test_cost_dimension_landed` | substrate-shape | T-Workflow-As-Data + Debt-Paydown (Cluster M sub-component) | DECLARED (NEW 2026-05-12 per PR #2744 §1) | `Cost` dimension declared on test nodes. **Distinct from existing compiler-internal cost gates** (#37 `cost_lens_reads_target_realization` / #39 `no_coercion_cost_dimension` / #40 `symbolic_cost_expr_equals_executable` / #70 `cost_lens_demonstration` / #80 `cost_lens_behaviorally_complete` are about `SymbolicCost` as the compiler's cost lens reading target programs); this gate is about `Cost`-as-`Dimension` applied to **test nodes** so the slow-test ratchet **can** attach wall-clock facts to modeled test nodes instead of treating exemptions as an unstructured compiler-local table (substrate-shape sibling of state-check #102). | | 102 | `slow_test_exemptions_dissolved` | state-check | T-Workflow-As-Data + Debt-Paydown | DECLARED (NEW 2026-05-12 per PR #2744 §1) | **Pass target:** slow-test ratchet policy is read from modeled test-node timing / `TestNodeCostDimension` substrate facts (no checked-in warn-manifest side input). **Interim (not closure):** `scripts/slow-test-exemptions.txt` is deleted and warn rows live in structured `scripts/test-node-wall-clock-ratchet.jsonl` while CI still reads that file directly — bridge work toward #101/#102, not a claim that #102 is GREEN. Pair with kernel-modeling split per `feedback_state_space_vs_behavioral_invariants` + Director msg_f9fd669e. | | 103 | `ci_uses_affected_set_selection` | state-check | T-Workflow-As-Data + T-Verification | DECLARED (NEW 2026-05-12 per PR #2744 §1) | `BinaryShim` emitter consumes affected-set lens output from PR #2713 (merged); Layer 2 path-regex `if:` gates removed from any remaining workflow files (cross-tier co-owned with clever-tern-670 Slice 7 work). | -| 104 | `lens_read_witness_shape_dissolved` | state-check | T-Lens-Behavioral-Parity | **DECLARED** (NEW 2026-05-12 per Director ratification msg_915aa2c1 + operator directive 2026-05-11 at `docs/audit/r3-deferral-anti-pattern-audit-2026-05-11.md` §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. **Scope at HEAD** (Director-grep msg_cefcbe05): `src/v3/lenses/cost.dag` 25 sites + `src/v3/lenses/complexity.dag` 25 sites + `src/v3/std/substrate.dag` 3 sites + `src/v3/std/lookup.dag` 11 sites = 64 total; parallelism + effect_enumeration + timing_lens .dag layers already clean (0 sites). `ArrowBody::Pending` is related-but-distinct sibling per audit §3.6 — out of scope. **Bundled-migration shape** (Director ratification msg_915aa2c1 + atomic per §P5): TWO parallel migrations bundled, NOT one. (1) **Substrate-level (primary)**: collapse `Lookup::Miss` → `Witness::Violates { reason, at }` across the 64 sites; Phase 1 cost.dag + complexity.dag bundle (50 sites; canonical pattern), Phase 2 substrate.dag accessor (3 sites), Phase 3 lookup.dag terminal carrier deletion (11 sites + carrier itself). (2) **Testgen-level (companion)**: per-lens TestClaim asserting universal coverage `∀ bind ∈ bootstrap. lens_read(bind) ∈ Inhabits(_)`; fail-closed on `Violates`. Violates set becomes structural test fixture (named-reason enumeration of legitimate exclusions). Without (2), (1) leaves regression window; without (1), (2) has nothing to test. **Two-part predicate** (per Director ratification): Part A (terminal, primary) = `git grep -nE "Lookup<" src/v3/lenses/ src/v3/std/ ; expected = 0` (terminal state after Phase 3 lookup.dag deletion); Part B (regression guard) = `git grep -nE "::Miss\b" src/v3/compiler/src/lens_*_generated.rs ; expected = 0`. Both must pass = green. **Status progression**: DECLARED → CONSUMER_LANDED requires BOTH (a) Substrate Mgr brief authored covering ≥3 lens carriers AND (b) at least one universal-coverage TestClaim landed → PASSING requires Part A + Part B predicates both zero. **Canvas-framing** (operator-surfaced 2026-05-12 23:09Z; relayed to Substrate Mgr in brief): Q-MissOrError (why Miss instead of Error → answer: Miss carries neither reason nor at, forces caller to ignore or fabricate; correct shape is `Witness::Violates { reason: , at: }`); Q-WhyTestgenMissed (3 structural gaps: (a) TestClaim rows scenario-driven not universal-property-driven, (b) parity tests pin frozen v2-oracle snapshots not v3-coverage sweeps, (c) lens-discipline ratchet didn't exist — fix substrate, testgen has property to enforce). **Authority chain**: operator 2026-05-11 + audit §0/§3.1/§3.4 + design-lens-framework.md:51,326,382-384 + design-emission-model.md:958,1206 + R4.D §4 (WISHLIST.md:147 from PR #2800) + R4.D faithfulness framework. **Origin**: Director'\''s 2026-05-12 complexity-lens dump (msg_32a3775e) surfaced concrete evidence of 15 Miss returns at algebra.dag bind layer; operator surfaced the audit-doc precedent; Director provided concrete grep counts (msg_cefcbe05); PM proposed §1.8 row (msg_054e2a43); Director ratified (b) with refinements (msg_915aa2c1). | +| 104 | `lens_read_witness_shape_dissolved` | state-check | T-Lens-Behavioral-Parity | **DECLARED** (NEW 2026-05-12 per Director ratification msg_915aa2c1 + operator directive 2026-05-11 at `docs/audit/r3-deferral-anti-pattern-audit-2026-05-11.md` §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. **Scope at HEAD** (Part A predicate executed at PR #2807 HEAD per codex BLOCKING #4276876807 on PR #2804 — supersedes Director-grep msg_cefcbe05 which omitted 2 files): `src/v3/lenses/cost.dag` 25 sites + `src/v3/lenses/complexity.dag` 25 sites + `src/v3/lenses/infer_helpers.dag` 3 sites + `src/v3/std/algebra.dag` 3 sites + `src/v3/std/substrate.dag` 3 sites + `src/v3/std/lookup.dag` 11 sites = **70 total** across 6 files; parallelism + effect_enumeration + timing_lens .dag layers already clean (0 sites). `ArrowBody::Pending` is related-but-distinct sibling per audit §3.6 — out of scope. **Bundled-migration shape** (Director ratification msg_915aa2c1 + atomic per §P5): TWO parallel migrations bundled, NOT one. (1) **Substrate-level (primary)**: collapse `Lookup::Miss` → `Witness::Violates { reason, at }` across the 70 sites; Phase 1 cost.dag + complexity.dag bundle (50 sites; canonical pattern — `complexity_of` + `symbolic_cost_of` lens read-channel + helpers), Phase 2 monomorphized accessor sweep (substrate.dag 3 + algebra.dag 3 + infer_helpers.dag 3 = 9 sites; `miss_*_lookup` / `hit_*_lookup` constructor pairs at `substrate.dag:691,695` + `algebra.dag:225,229` + `Lookup` return-type at `infer_helpers.dag:141` + doc references at `algebra.dag:219` + `infer_helpers.dag:77,88`), Phase 3 lookup.dag terminal carrier deletion (11 sites + carrier itself). (2) **Testgen-level (companion)**: per-lens TestClaim asserting universal coverage `∀ bind ∈ bootstrap. lens_read(bind) ∈ Inhabits(_)`; fail-closed on `Violates`. Violates set becomes structural test fixture (named-reason enumeration of legitimate exclusions). Without (2), (1) leaves regression window; without (1), (2) has nothing to test. **Two-part predicate** (per Director ratification): Part A (terminal, primary) = `git grep -nE "Lookup<" src/v3/lenses/ src/v3/std/ ; expected = 0` (terminal state after Phase 3 lookup.dag deletion); Part B (regression guard) = `git grep -nE "::Miss\b" src/v3/compiler/src/lens_*_generated.rs ; expected = 0`. Both must pass = green. **Status progression**: DECLARED → CONSUMER_LANDED requires BOTH (a) Substrate Mgr brief authored covering ≥3 lens carriers AND (b) at least one universal-coverage TestClaim landed → PASSING requires Part A + Part B predicates both zero. **Canvas-framing** (operator-surfaced 2026-05-12 23:09Z; relayed to Substrate Mgr in brief): Q-MissOrError (why Miss instead of Error → answer: Miss carries neither reason nor at, forces caller to ignore or fabricate; correct shape is `Witness::Violates { reason: , at: }`); Q-WhyTestgenMissed (3 structural gaps: (a) TestClaim rows scenario-driven not universal-property-driven, (b) parity tests pin frozen v2-oracle snapshots not v3-coverage sweeps, (c) lens-discipline ratchet didn't exist — fix substrate, testgen has property to enforce). **Authority chain**: operator 2026-05-11 + audit §0/§3.1/§3.4 + design-lens-framework.md:51,326,382-384 + design-emission-model.md:958,1206 + R4.D §4 (WISHLIST.md:147 from PR #2800) + R4.D faithfulness framework. **Origin**: Director's 2026-05-12 complexity-lens dump (msg_32a3775e) surfaced concrete evidence of 15 Miss returns at algebra.dag bind layer; operator surfaced the audit-doc precedent; Director provided concrete grep counts (msg_cefcbe05; subsequently superseded — see scope correction below); PM proposed §1.8 row (msg_054e2a43); Director ratified (b) with refinements (msg_915aa2c1). **Scope correction at PR #2807** (codex BLOCKING #4276876807): Director's relayed 64-count omitted 2 files (`algebra.dag` 3 + `infer_helpers.dag` 3 = 6 missing sites). PM verified Part A predicate at `7a7c19d3` HEAD = 70 matches; algebra.dag inclusion is structurally required since `algebra.dag:225 miss_symbolic_cost_lookup()` is the canonical `Lookup::Miss` constructor at the bind layer that emits the 15 Miss returns Director's dump surfaced — excluding it would have left the row's own terminal predicate red post-migration. Scope-statement + Phase 2 reframed accordingly. | **Plus standing-program ledger predicate** (NOT a lane gate; separate Pass surface per §1): - `r3_debt_paydown_zero_remaining` — no tracked-debt rows survive R3 close (per §1.5 inclusion list); ROADMAP `Post-merge debt` rows + sweep §1 Class A/B/C/F/G entries + §10 RED escalations.