diff --git a/docs/briefs/r3-verification-manager.md b/docs/briefs/r3-verification-manager.md index 151895f1061..bb86b2cfea1 100644 --- a/docs/briefs/r3-verification-manager.md +++ b/docs/briefs/r3-verification-manager.md @@ -1,27 +1,41 @@ # R3 Verification Manager Brief -**Status:** PROPOSAL — manager brief authored at R3 spin-up (post-R2-close 2026-04-30 per [`docs/r2-closure-ledger.md`](../r2-closure-ledger.md) §"Director closure acceptance"). Spawned per [`docs/r3-structure.md`](../r3-structure.md) §"Manager structure" Item 2 (Director-locked 2026-04-28). +**Status:** ACTIVE — manager brief authored at R3 spin-up (post-R2-close 2026-04-30 per [`docs/r2-closure-ledger.md`](../r2-closure-ledger.md) §"Director closure acceptance"), then refreshed for the 2026-05-13 actual-close ratification. Spawned per [`docs/r3-structure.md`](../r3-structure.md) §"Manager structure" Item 2 (Director-locked 2026-04-28). + +## 2026-05-13 actual-close lane update + +`docs/r3-actual-close-plan.md` is now the controlling close-plan artifact for Verification-owned work. The operator ratified the IN-R3 path for the Verification gaps on 2026-05-13; R4 deferral and narrowed Rust-only closure paths are structurally foreclosed for this lane. This manager therefore owns the lane-through-close implementation posture below, not the older standby-only posture in the original brief: + +| Actual-close item | Verification obligation | Close predicate | +|---|---|---| +| Gap 2 — L5 cross-target consistency / gate #15 | Land the certification corpus and the three-target Rust/Python/Go runtime-behavior parity assertion. Coordinate with Substrate only for missing carrier/emitter support; the gate remains Verification-owned. | `cargo test --release -p v3-compiler --test l5_cross_target_consistency` passes with `N > 0` corpus programs and all three Shape-A targets agreeing on runtime behavior. | +| Gap 5 — tests-as-data completeness / gates #84 + #85 | Drive Cluster M Phase 3 bulk-port to `.dag` `TestClaim` or generated test artifacts, including the generator-manifest authority for surviving generated Rust tests. | `EXPECTED_HAND_AUTHORED_TEST` is empty in `sg0_census_test.rs`; the generator manifest covers every surviving Rust test file and regeneration byte-comparison passes; SuiteClaim wrapper consumer for #85 is landed. | +| T-WAD Slice 7 — affected-set integration | Consume the affected-set lens output in the BinaryShim CI path once Slice 5 exists; remove Layer-2 path-regex workflow selection authority from remaining workflow files. | `ci_uses_affected_set_selection` is PASSING: BinaryShim CI selection is driven by affected-set lens output, with no path-regex `if:` bridge remaining as CI authority. | + +The manager should dispatch worker slices directly against these predicates. Brief maintenance that does not reduce one of these predicates is not lane-closing work. ## Orient before reading -- **R3 structure authority:** [`docs/r3-structure.md`](../r3-structure.md). Names this manager owner of T-Verification-L4-L7-Direct + T-Verification-L5-Corpus + T-Free-Consequences-Demonstration + the `bridge_retirement_ledger_zero` audit gate of T-Bridge-Retirement. -- **Program scope source:** [`THESIS.md`](../../THESIS.md) §"Tier 3 — Verification from structure" (L4, L5, L7 verification-surface claims) + [`docs/r3-structure.md`](../r3-structure.md) §"Lane structure" rows for T-Verification-L4-L7-Direct / T-Verification-L5-Corpus / T-Free-Consequences-Demonstration / T-Bridge-Retirement. +- **R3 structure authority:** [`docs/r3-structure.md`](../r3-structure.md), amended by the 2026-05-13 actual-close plan in [`docs/r3-actual-close-plan.md`](../r3-actual-close-plan.md). Names this manager owner of T-Verification-L4-L7-Direct + T-Verification-L5-Corpus + T-Free-Consequences-Demonstration + T-Tests-As-Data-Completeness + the `bridge_retirement_ledger_zero` audit gate of T-Bridge-Retirement. +- **Program scope source:** [`THESIS.md`](../../THESIS.md) §"Tier 3 — Verification from structure" (L4, L5, L7 verification-surface claims) + [`docs/r3-structure.md`](../r3-structure.md) §"Lane structure" rows for T-Verification-L4-L7-Direct / T-Verification-L5-Corpus / T-Free-Consequences-Demonstration / T-Tests-As-Data-Completeness / T-Bridge-Retirement, with T-WAD Slice 7 added as a cross-program Verification extension by [`docs/r3-t-workflow-as-data-full-r3-close-scope.md`](../r3-t-workflow-as-data-full-r3-close-scope.md). - **Why a new manager (per `r3-structure.md` §"Manager structure" Item 2):** the R3 verification surface {L4, L5, L7} + free-consequences-demonstration is structural-acceptance-by-construction — its own discipline, not foldable into Substrate (different concern) or PB (different concern). - **Cross-program producer:** **R2-Evaluator** gates lanes 1, 2, and 3 (Witness construction surface + cross-target equivalence harness primitives + consequence witnesses). R3-absorbed formal-grounding lane (TC1/TC2/TC3 bundling) consumes substrate primitives authored by Substrate Manager continuation. **PR-D semantic lock:** [`docs/design-cross-target-equivalence.md`](../design-cross-target-equivalence.md) defines the L5 equality / corpus / oracle / float / effect policy this manager consumes. - **Substrate-fact-introduction procedure** ([`INVARIANTS.md`](../../INVARIANTS.md) §P1): self-serve through the 3-step decision procedure before escalating substrate-shape questions to Director. Director ratified unified substrate-introduction for TC1/TC2/TC3 as `BinaryDimensionReportEquals` at [#828 c#4356050427](https://github.com/gunb-ai/gunbc/issues/828#issuecomment-4356050427) + [#828 c#4356138359](https://github.com/gunb-ai/gunbc/issues/828#issuecomment-4356138359); Substrate owns the predicate variant, while Verification supplies consuming coverage requirements. -## Owned program scope (3 lanes + 1 ledger gate, per `r3-structure.md` §"Manager structure" Item 2 authority) +## Owned program scope (4 lanes + 1 cross-program extension + 1 ledger gate) | Item | Size | Status (at brief authoring) | Gates on | |---|---|---|---| -| **Lane 1: T-V-L4-L7-Direct** | M | **Worker brief authored, standby** — [`r3-v-l4-l7-direct-worker.md`](r3-v-l4-l7-direct-worker.md). Per-target equivalence harness using `DifferentialEquals` predicate (consumes Worker B PR-D scaffold per [`r2-pr-d-cross-target-equivalence-harness-primitives.md`](r2-pr-d-cross-target-equivalence-harness-primitives.md) §slice 1). NOT a `Lens` instance per codex BLOCKING `f5f63c7d9` — runtime equivalence check, not structural fold. | R2-Evaluator PR-A.3 implementation carriers + PR-B body evaluator landing | -| **Lane 2: T-V-L5-Corpus** | M | **Worker brief authored, standby** — [`r3-v-l5-corpus-worker.md`](r3-v-l5-corpus-worker.md). Cross-target equivalence corpus authoring (L5 only; L6 reclassified to R2-T-Ground-CrossTarget-Meta per [`r3-structure.md`](../r3-structure.md) §"Acceptance" T-Verification-L5-Corpus L6-reclassification note). Consumes PR-D semantic policy in [`docs/design-cross-target-equivalence.md`](../design-cross-target-equivalence.md). | Lane 1 corpus existing + R2-Grounding-Rust + R2-Grounding-Python + R2-Grounding-Go (Shape A 3-target grounding precondition) | -| **Lane 3: T-Free-Consequences-Demonstration** | S-M | **Worker brief authored, standby** — [`r3-v-free-consequences-worker.md`](r3-v-free-consequences-worker.md). Small doc + testcase-driven demonstration of what guarantees the compiler actually provides: auto-parallelism (including effect/commutativity safety), auto-memoization, cross-target optimization, and space-bound CX status/reference (space-bound proofs remain NOT STARTED until the space lens is modeled). | R2-Evaluator witness construction + R2-T-Substrate-Lens-Primitive (`Lens` shape) + T-CostLens-Composition | +| **Lane 1: T-V-L4-L7-Direct** | M | **Worker brief authored; actual-close predicate active** — [`r3-v-l4-l7-direct-worker.md`](r3-v-l4-l7-direct-worker.md). Per-target equivalence harness using `DifferentialEquals` predicate (consumes Worker B PR-D scaffold per [`r2-pr-d-cross-target-equivalence-harness-primitives.md`](r2-pr-d-cross-target-equivalence-harness-primitives.md) §slice 1). NOT a `Lens` instance per codex BLOCKING `f5f63c7d9` — runtime equivalence check, not structural fold. | R2-Evaluator PR-A.3 implementation carriers + PR-B body evaluator landing | +| **Lane 2: T-V-L5-Corpus** | M | **Actual-close Gap 2 owner** — [`r3-v-l5-corpus-worker.md`](r3-v-l5-corpus-worker.md). Cross-target equivalence corpus authoring (L5 only; L6 reclassified to R2-T-Ground-CrossTarget-Meta per [`r3-structure.md`](../r3-structure.md) §"Acceptance" T-Verification-L5-Corpus L6-reclassification note). Consumes PR-D semantic policy in [`docs/design-cross-target-equivalence.md`](../design-cross-target-equivalence.md). The 2026-05-13 close plan forecloses Rust-only narrowing; the required surface is Rust + Python + Go. | Lane 1 corpus existing + R2-Grounding-Rust + R2-Grounding-Python + R2-Grounding-Go (Shape A 3-target grounding precondition) | +| **Lane 3: T-Free-Consequences-Demonstration** | S-M | **Worker brief authored; remains lane-close work** — [`r3-v-free-consequences-worker.md`](r3-v-free-consequences-worker.md). Small doc + testcase-driven demonstration of what guarantees the compiler actually provides: auto-parallelism (including effect/commutativity safety), auto-memoization, cross-target optimization, and space-bound CX status/reference (space-bound proofs remain NOT STARTED until the space lens is modeled). | R2-Evaluator witness construction + R2-T-Substrate-Lens-Primitive (`Lens` shape) + T-CostLens-Composition | +| **Lane 4: T-Tests-As-Data-Completeness** | L | **Actual-close Gap 5 owner** — Cluster M Phase 3 bulk-port is now lane-closing Verification work, not audit-only tracking. The manager owns worker dispatch for per-class ports and the generated-test manifest authority required by `docs/r3-actual-close-plan.md` §Gap 5. | ProgramGenerator substrate (#86) landed; #85 generated consumer + Cluster M Phase 3 generator-manifest work remain. | +| **Cross-program extension: T-WAD Slice 7 affected-set CI selection** | M | **Absorbed owner for `ci_uses_affected_set_selection`** per [`docs/r3-t-workflow-as-data-full-r3-close-scope.md`](../r3-t-workflow-as-data-full-r3-close-scope.md) §3/§7. This is a Verification extension to T-WAD, not a standalone Verification lane, because it consumes the affected-set lens output and removes regex bridge authority from CI selection. | Slice 5 BinaryShim projection arm + PR #2713 affected-set lens output. | | **Ledger gate: T-Bridge-Retirement (`bridge_retirement_ledger_zero`)** | S (audit cadence; no implementation) | **Bridge map row maintenance** — 5 named bridges per [`r3-structure.md`](../r3-structure.md) §"Lane structure" T-Bridge-Retirement row's distribution map. Verification owns the unified audit gate; retirement work distributes per natural-owner program. | Per-bridge: each bridge fires structurally in its owner program; ledger-zero gate fires when all 5 are green. | ### Absorbed cross-cutting responsibility — TC1/TC2/TC3 bundle (NOT a fourth owned lane) -Per [`r3-pb-t-fixedpoint-worker.md`](r3-pb-t-fixedpoint-worker.md) §"TC3 — Strong-normalization TestClaim (author-now-fire-later, PB → R3 Verification transition)" / §"Transition to R3 Verification" (PB→Verification handoff) + R2-Evaluator residual transition for TC2 + #1179 ratification for TC1: the three formal-grounding `TestClaim`s are an **absorbed cross-cutting responsibility** of this manager, not a fourth owned lane. The structural authority `r3-structure.md` §"Manager structure" Item 2 names exactly **3 lanes + 1 ledger gate** for Verification scope after the 2026-04-30 expansion; this brief defers to that authority. Audit cadence + strict-fire activation tracking is folded into manager cadence (not a separate dispatch program). Worker brief at [`r3-v-formal-grounding-tc-bundle.md`](r3-v-formal-grounding-tc-bundle.md) authors the bundle as an absorbed-responsibility audit-cadence artifact. +Per [`r3-pb-t-fixedpoint-worker.md`](r3-pb-t-fixedpoint-worker.md) §"TC3 — Strong-normalization TestClaim (author-now-fire-later, PB → R3 Verification transition)" / §"Transition to R3 Verification" (PB→Verification handoff) + R2-Evaluator residual transition for TC2 + #1179 ratification for TC1: the three formal-grounding `TestClaim`s are an **absorbed cross-cutting responsibility** of this manager, not an additional owned lane. The 2026-05-13 actual-close refresh makes T-Tests-As-Data the fourth owned lane; the TC bundle remains audit cadence + strict-fire activation tracking folded into manager cadence, not a separate dispatch program. Worker brief at [`r3-v-formal-grounding-tc-bundle.md`](r3-v-formal-grounding-tc-bundle.md) authors the bundle as an absorbed-responsibility audit-cadence artifact. **Unified-predicate disposition (Director-ratified):** PR #1309's TC1 analysis named Option 2 first — generalize `LensOutputEquals` into binary structural equality over `DimensionReport`. PR #1316 independently converged on the same shape for TC2. Director ratified the unified substrate target at [#828 c#4356050427](https://github.com/gunb-ai/gunbc/issues/828#issuecomment-4356050427) and [#828 c#4356138359](https://github.com/gunb-ai/gunbc/issues/828#issuecomment-4356138359): one Substrate-owned `BinaryDimensionReportEquals` `TestPredicate` variant with reflection-aware modifiers absorbs TC1 eta-equivalence, TC2 strategy-order equality, and TC3 evaluation-step witnessing. Verification authors coverage requirements and consuming `TestClaim`s; Substrate authors the predicate variant / carrier. The 2026-04-30 lane expansion added T-Free-Consequences-Demonstration as Lane 3, but did not elevate the TC bundle into a lane. @@ -54,6 +68,8 @@ Per [`docs/r3-structure.md`](../r3-structure.md) §"Lane structure" T-Bridge-Ret **Produces:** - **L4-L7 verification surface** — Lane 1 lands per-target equivalence; Lane 2 lands cross-target equivalence corpus. - **Free-consequences demonstration surface** — Lane 3 lands the design-free-consequences doc + 10-gate TestClaim suite for user-visible guarantees. +- **Tests-as-data completion surface** — Lane 4 lands Cluster M Phase 3 ports and the generator-manifest authority for surviving generated Rust tests. +- **T-WAD affected-set CI selection extension** — cross-program Slice 7 lands `ci_uses_affected_set_selection` by consuming affected-set lens output in BinaryShim CI selection. - **TC1/TC2/TC3 strict-fire activations** — absorbed-responsibility audit cadence strengthens deferred claims as the unified `BinaryDimensionReportEquals` substrate predicate and each TC's modifier/prerequisites land. - **Unified bridge-retirement audit cadence** — periodic ledger-zero gate check; signals to Director when all 5 bridges fire. @@ -86,6 +102,8 @@ Each lane closes under a structural acceptance gate authored as a `.dag` `TestCl - **Lane 1**: closes under both `l4_emit_eval_match` (per [`r3-structure.md`](../r3-structure.md) §"Acceptance" T-Verification-L4-L7-Direct gate definition — every `.dag` program in certification corpus has emit-target output equal to `.dag` eval output, algebraic equality) AND `l7_algebraic_laws_witnessed` (per [`r3-structure.md`](../r3-structure.md) §"Acceptance" T-Verification-L4-L7-Direct gate definition — every algebra × every applicable law has a runtime-constructed witness via `AlgebraicLaw` `TestPredicate`). Partial-coverage early slices do NOT close the lane; full coverage required. - **Lane 2**: `l5_cross_target_consistency` (per [`r3-structure.md`](../r3-structure.md) §"Acceptance" T-Verification-L5-Corpus gate definition) — for every `.dag` program, emitted Rust/Python/Go produce equivalent runtime behavior on the certification corpus (algebraic equivalence over computational results, not byte identity). - **Lane 3**: closes when [`docs/design-free-consequences.md`](../design-free-consequences.md) lands and the 10-gate suite from [`r3-v-free-consequences-worker.md`](r3-v-free-consequences-worker.md) is green: `auto_parallelism_independent_binds_emit_parallel`, `auto_parallelism_dependent_binds_pending_lens_fail_closed`, `auto_parallelism_branch_arms_serialize`, `auto_loop_parallelism_provable_independence_emits_parallel`, `auto_loop_parallelism_unproven_falls_back_sequential`, `auto_loop_parallelism_dependence_emits_sequential`, `auto_memoization_repeated_pure_call_cached`, `auto_memoization_no_caching_for_one_shot`, `cross_target_optimization_constant_fold_consistent`, and `cross_target_optimization_cost_structurally_derived`. +- **Lane 4**: `every_rust_test_ports_to_dag_or_generated` + `forall_exists_quantifier_substrate_landed` — `EXPECTED_HAND_AUTHORED_TEST` is empty, the generator manifest maps every surviving Rust test file to a `.dag` source, regeneration byte-comparison passes, and the #85 generated consumer lands. +- **Cross-program extension**: `ci_uses_affected_set_selection` — BinaryShim CI selection consumes affected-set lens output and no remaining workflow file carries Layer-2 path-regex `if:` authority. - **Absorbed responsibility (TC bundle)**: TC1/TC2/TC3 strict-fire activation across the three deferred-claim fixtures via unified `BinaryDimensionReportEquals` once Substrate lands the predicate and each reflection-aware modifier is covered — tracked via audit cadence, not as a lane-close gate. - **Ledger gate**: `bridge_retirement_ledger_zero` — unified ledger reports 0 named identity bridges remaining (per [`r3-structure.md`](../r3-structure.md) §"Acceptance" T-Bridge-Retirement gate definition). @@ -109,13 +127,21 @@ Each lane closes under a structural acceptance gate authored as a `.dag` `TestCl - Unified `BinaryDimensionReportEquals` coverage-requirements proposal (TC1/TC2/TC3 inputs; Substrate authors predicate variant when proposal is mature). - Lane 1 / Lane 2 / Lane 3 implementation worker briefs (gated on R2-Evaluator / substrate prerequisites — convert from standby to dispatch-ready when prerequisites fire). -## Working state (fill on dispatch) +## Working state (2026-05-13 refresh) + +The lane is no longer only "3 lanes in standby." It has four owned lane surfaces plus one cross-program extension: + +- **Gap 2 / gate #15** — dispatch L5 corpus + Rust/Python/Go parity implementation slices until the close predicate is executable in CI. +- **Gap 5 / gates #84-#85** — dispatch Cluster M Phase 3 per-class test ports plus the generator-manifest authority as Lane 4; negative SG-0 ratchet and positive manifest predicate both required. +- **T-WAD Slice 7 / `ci_uses_affected_set_selection`** — queue implementation as a cross-program extension once BinaryShim Slice 5 exists; acceptance requires affected-set lens output to drive CI selection and deletes path-regex bridge authority. -Lane status table refreshes here as work lands. Initial state: 3 lanes in standby + 1 ledger gate in audit cadence + TC bundle absorbed-responsibility audit cadence; bridge map row maintenance ongoing. +The TC bundle and bridge-retirement ledger remain absorbed audit responsibilities, but they are not substitutes for the three active close surfaces above. ## Cross-refs -- Parent: [`docs/r3-structure.md`](../r3-structure.md) §"Manager structure" Item 2 + §"Lane structure" rows for T-Verification-L4-L7-Direct / T-Verification-L5-Corpus / T-Free-Consequences-Demonstration / T-Bridge-Retirement +- Parent: [`docs/r3-structure.md`](../r3-structure.md) §"Manager structure" Item 2 + §"Lane structure" rows for T-Verification-L4-L7-Direct / T-Verification-L5-Corpus / T-Free-Consequences-Demonstration / T-Tests-As-Data-Completeness / T-Bridge-Retirement +- Actual-close authority: [`docs/r3-actual-close-plan.md`](../r3-actual-close-plan.md) Gap 2 + Gap 5 +- T-WAD cross-program extension: [`docs/r3-t-workflow-as-data-full-r3-close-scope.md`](../r3-t-workflow-as-data-full-r3-close-scope.md) §3/§7 - Closure ledger predecessor: [`docs/r2-closure-ledger.md`](../r2-closure-ledger.md) (R2 closed-with-residuals 2026-04-30) - R2 Evaluator producer brief: [`docs/briefs/r2-evaluator-manager.md`](r2-evaluator-manager.md) - TC3 upstream declarative shape: [`docs/briefs/r3-pb-t-fixedpoint-worker.md`](r3-pb-t-fixedpoint-worker.md) §"TC3 — Strong-normalization TestClaim (author-now-fire-later, PB → R3 Verification transition)"; ownership transitions to Verification per §"Transition to R3 Verification"