R3 Verification

docs/briefs/r3-v-pattern-a-rust-dag-isomorphism-v1-worker.md

@@ -0,0 +1,69 @@
+# R3 Pattern-A — Rust Dag isomorphism first executable slice Worker Brief
+
+**Status:** **PRE-AUTH DISPATCH-READY** — brief authored ahead of runtime triggers (pre-auth queue **#1859**). **No strict-fire Implementation dispatch** until §Dependencies clear.
+
+**Parent:** [`docs/briefs/r3-verification-manager.md`](r3-verification-manager.md) — Pattern-A cluster under Lane 1 (`docs/r3-structure.md` §"Acceptance" T-V-L4-L7-Direct).
+
+**Research / producer framing:** [`docs/briefs/r3-v-reflected-dag-structural-assertion-analysis.md`](r3-v-reflected-dag-structural-assertion-analysis.md) — Director producer-first disposition (**#828**): Substrate-owned `Lens<DagShapeReport>` (or equivalent) projects reflected / emitted Dag into a structural **shape report**; **`BinaryDimensionReportEquals`** with the **shape-report modifier** is the comparison shell — **no** parallel predicate authority (**INVARIANTS** §P1).
+
+**Program plan (single operational authority):** [`docs/r3-program-plan.md`](../r3-program-plan.md) §10.3 **Q-PAFS** — Path **C** (RustDagIsomorphism before TC1) is **not** the default policy ordering; **this brief** only elaborates **gate #14** per §1.8 and `r3-structure.md` §"Acceptance". **Does not** override §10.3 (**INVARIANTS** §P2).
+
+## §1.8 closure predicate (this slice)
+
+| Gate ID | Gate name (canonical) | Target transition |
+| --- | --- | --- |
+| **#14** | `rust_dag_isomorphism_executable` | **DECLARED → CONSUMER_LANDED** when executable `TestClaim` + runner path land per this brief; **PASSING** when strict-fire evaluates green on CI. |
+
+Canonical Pass body (archive authority): `r3-structure.md` §"Acceptance" — structural Dag equivalence between Rust-emitted / reflected Dag authority and `.dag` source Dag. **Engineering route:** two comparable **shape-report** carriers feeding the unified binary predicate (research brief §"Producer Plus Comparison Shell"), unless Director revises the acceptance prose.
+
+## Worker pin (Verification Mgr partition)
+
+| Preference | Worker | Condition |
+| --- | --- | --- |
+| **Primary** | **bold-crane-790** ([gunbc#1748](https://github.com/gunb-ai/gunbc/issues/1748)) | Same Track A pin as TC2/TC3 when §Dependencies + staffing allow. |
+| **Alternate** | **New worker** | If bold-crane saturated — substitute per `feedback_idle_workers_dispatchable_directly`. |
+
+## Scope (in)
+
+- Executable **gate #14** slice: `TestClaim` + runner wiring once Substrate shape-report producer + unified predicate modifier exist.
+- **Representative programs:** finite, named set (bootstrap mirrors / lockstep schema checks called out in research §"Migration Audit" — start with **strong** fits such as carrier-shape tests before anthropic cross-source schema).
+- Verification-owned: integration receipts, fixture naming, strict-fire diagnostics **by shape** ([`TESTING.md`](../../TESTING.md)).
+
+## Scope (out) — STOP+PING
+
+| Item | Discipline |
+| --- | --- |
+| **Parallel `RustDagIsomorphism` predicate family** | **STOP+PING** — consumer instance on unified shell only (research §"RustDagIsomorphism Adjacency"). |
+| **Hand-maintained Rust↔.dag mirrors** | **STOP+PING** — generation-or-isomorphism discipline (`feedback_isomorphism_or_generation_for_mirrors`); Substrate owns producer evolution. |
+| **Folding TC1 η / TC2 / TC3 into this PR** | **STOP+PING** — separate gates **#11–#13**; coordinate only if a single substrate PR batches shared predicate evolution (then sequence only). |
+
+## Dependencies (hard)
+
+| ID | Dependency | Owner | Notes |
+| --- | --- | --- | --- |
+| R1 | **`Lens<DagShapeReport>`** (or equivalent structural projection) | Substrate | Producer-first #828 ratification |
+| R2 | **Shape-report role** on unified `BinaryDimensionReportEquals` | Substrate | Modifier lands via §P1 |
+| R3 | **Reflection / compile-to-dag** path stable enough to extract both sides of comparison | Substrate + Evaluator | parity with research §"Reflection-Completeness Residual" awareness |
+| R4 | **Coverage-shape ratification** (which declarations / rows are in-scope for v1 strict-fire) | Director + Verification | named finite harness before PASSING |
+
+## Dispatch triggers (mechanical)
+
+1. **R1 + R2** land — receipts linked from Substrate inbox **[#1739](https://github.com/gunb-ai/gunbc/issues/1739)** / Evaluator **[#1743](https://github.com/gunb-ai/gunbc/issues/1743)** as appropriate.
+2. **R4** named — Director-visible finite representative set.
+3. **Worker available** — bold-crane (or substitute).
+4. **Sub-issue** under **#1748** + `addSubIssue` + inbox pointer.
+
+## Implementation slices (suggested PR shape)
+
+1. **Slice 1 — substrate receipt:** shape-report producer + predicate modifier green on representative input (no ledger PASSING claim until Slice 2).
+2. **Slice 2 — executable `TestClaim`:** `rust_dag_isomorphism_executable` integration **Pass**.
+3. **Slice 3 — ledger / doc:** §1.8 status + cross-link [`r3-v-formal-grounding-tc-bundle.md`](r3-v-formal-grounding-tc-bundle.md) if bundle row is touched.
+
+**Substrate lands first** on any new carrier — Verification does not invent `DagShapeReport` schema.
+
+## Cross-refs
+
+- Research: [`r3-v-reflected-dag-structural-assertion-analysis.md`](r3-v-reflected-dag-structural-assertion-analysis.md)
+- TC1 neighbor (different gate / Branch B hold): [`r3-v-pattern-a-tc1-v1-worker.md`](r3-v-pattern-a-tc1-v1-worker.md)
+- TC2 / TC3 neighbors: [`r3-v-pattern-a-tc2-v1-worker.md`](r3-v-pattern-a-tc2-v1-worker.md), [`r3-v-pattern-a-tc3-v1-worker.md`](r3-v-pattern-a-tc3-v1-worker.md)
+- Plan §2.1 Pattern-A cluster: [`docs/r3-program-plan.md`](../r3-program-plan.md) §"§2.1 Pattern A executable"

docs/briefs/r3-v-pattern-a-tc3-v1-worker.md

@@ -0,0 +1,79 @@
+# R3 Pattern-A — TC3 first executable slice (Pattern-A second-mover / evaluation-step) Worker Brief
+
+**Status:** **PRE-AUTH DISPATCH-READY** — brief authored **ahead of** runtime triggers (pre-authored queue). **No strict-fire Implementation dispatch** until §Dependencies clear for the **intended stage** (see **Two-stage gate** below). **TC1 V1 Branch B (η vacuity)** is **orthogonal** to TC3’s **evaluation-step / termination-evidence** axis — coordinate **only** if a **single PR** lands shared **unified `BinaryDimensionReportEquals`** + **fold** substrate touching both gates.
+
+**Parent:** [`docs/briefs/r3-verification-manager.md`](r3-verification-manager.md) — absorbed formal-grounding / Pattern-A cluster (see [`docs/r3-structure.md`](../r3-structure.md) §"Manager structure").
+
+**Conformance audit (structural envelope):** [`docs/briefs/r3-v-tc3-pattern-a-second-mover-conformance-audit.md`](r3-v-tc3-pattern-a-second-mover-conformance-audit.md) — second-mover consumer shape vs `BinaryDimensionReportEquals` standby.
+
+**Program plan (single operational authority):** [`docs/r3-program-plan.md`](../r3-program-plan.md) §10.3 — **Q-PAFS** / Pattern-A **policy** lives in the table; **TC1 V1 supersession** does **not** block authoring **TC3** coverage requirements. **This brief** elaborates **gate #13** `tc3_pattern_a_second_mover_executable` per [`docs/r3-structure.md`](../r3-structure.md) §"Acceptance" — **does not** override §10.3 (**INVARIANTS** §P2).
+
+**Bundle authority (two-stage):** [`docs/briefs/r3-v-formal-grounding-tc-bundle.md`](r3-v-formal-grounding-tc-bundle.md) — TC3 **stage (a)** vs **stage (b)**; **strict-fire PASSING** requires **(b) T-FixedPoint** horizon per PB ownership transition ([`r3-pb-t-fixedpoint-worker.md`](r3-pb-t-fixedpoint-worker.md) L145–215, L181–185).
+
+**Consumer envelope:** `BinaryDimensionReportEquals` over **`DimensionReport<Dag>`** role pair — **baseline evaluation-step projection** vs **bounded-step / termination-evidence projection** (same carrier `C = Dag`; audit §Contract).
+
+## §1.8 closure predicate (this slice)
+
+| Gate ID | Gate name (canonical) | Target transition |
+| --- | --- | --- |
+| **#13** | `tc3_pattern_a_second_mover_executable` | **DECLARED → CONSUMER_LANDED** when executable `TestClaim` + runner path land per this brief; **PASSING** when strict-fire evaluates green on CI **including** bundle **stage (b)** when applicable. |
+
+**Do not** fold TC3 into **TC1** or **TC2** implementation PRs unless Substrate explicitly batches unified-predicate landing — separate **Verification** receipt PRs preferred.
+
+## Worker pin (Verification Mgr partition)
+
+| Preference | Worker | Condition |
+| --- | --- | --- |
+| **Primary** | **bold-crane-790** ([gunbc#1748](https://github.com/gunb-ai/gunbc/issues/1748)) | Route **TC3 V1** implementation PR(s) when §Dependencies + Track A staffing allow — same **Track A** pin as [`r3-v-pattern-a-tc2-v1-worker.md`](r3-v-pattern-a-tc2-v1-worker.md). |
+| **Alternate** | **New worker** | If bold-crane saturated — substitute per `feedback_idle_workers_dispatchable_directly`. |
+
+## Scope (in)
+
+- **Stage (a)** readiness: coverage requirements + fixture **shape** for the two `DimensionReport<Dag>` role producers land against **unified** predicate **evaluation-step modifier** (Substrate-owned predicate evolution per [#828](https://github.com/gunb-ai/gunbc/issues/828)).
+- **Stage (b)** strict-fire: **T-FixedPoint** termination semantics + evaluator **evaluation-step / bounded-step** producer surface ([`r3-v-tc3-pattern-a-second-mover-conformance-audit.md`](r3-v-tc3-pattern-a-second-mover-conformance-audit.md) §Strict-Fire Preconditions).
+- **Coverage decision** (Director-ratified shape when chosen): structural induction vs generated exhaustive producer over typed-fragment carrier vs **bounded representative harness** — must be **named** before strict-fire claims **PASSING** (audit §1 bullet 5).
+
+## Scope (out) — STOP+PING
+
+| Item | Discipline |
+| --- | --- |
+| **TC3-isolated `TestPredicate` / quantifier** | **STOP+PING** — unified `BinaryDimensionReportEquals` + **evaluation-step modifier** only (Director Option 2). |
+| **Deferred fixture hard rewrite** | **STOP+PING** — `tc3_strong_normalization_deferred.dag` (stage-(a) path) stays staging until substrate-introduction PR authorizes ([`r3-v-formal-grounding-tc-bundle.md`](r3-v-formal-grounding-tc-bundle.md)). |
+| **Fire-before-(b)** | **STOP+PING** — no **PASSING** strict-fire that pretends **T-FixedPoint** / termination horizon is satisfied when bundle says **(b)** is still open. |
+| **Serialized / string / byte comparisons** | **STOP+PING** — per conformance audit **§Non-Drift Findings**. |
+
+## Dependencies (hard)
+
+Synthesized from [`r3-v-tc3-pattern-a-second-mover-conformance-audit.md`](r3-v-tc3-pattern-a-second-mover-conformance-audit.md) §Strict-Fire Preconditions + [`r3-v-formal-grounding-tc-bundle.md`](r3-v-formal-grounding-tc-bundle.md):
+
+| # | Dependency | Owner | Notes |
+| --- | --- | --- | --- |
+| D1 | **B5** loop construction-closure green | R2 Release / Substrate | bounded `Loop` construction |
+| D2 | **T-Substrate-Lens-Primitive** + real `DimensionReport<Dag>` producers | Substrate + Evaluator | both role reports materialize |
+| D3 | **T-FixedPoint** termination semantics (**stage (b)**) | PB Manager | bundle gate |
+| D4 | **E5** `Descent` execution proof + evaluator **evaluation-step** producer | Evaluator + Substrate | audit §Strict-Fire items 4–7 narrative |
+| D5 | **Unified predicate** + **evaluation-step modifier** | Substrate | INVARIANTS §P1 |
+| D6 | **Coverage-shape ratification** (induction / exhaustive / bounded harness) | Director + Verification | named before PASSING |
+
+## Dispatch triggers (mechanical)
+
+1. **D5 + D2 (stage a)** land — substrate/evaluator receipts linked from [#1743](https://github.com/gunb-ai/gunbc/issues/1743) / Substrate / PB threads as appropriate.
+2. **D3 + D4** land for **full strict-fire** — **no PASSING** without **(b)** unless Director narrows milestone (explicit §1.8 revision).
+3. **Worker available** — **bold-crane-790** (or substitute).
+4. **Sub-issue** under **#1748** + `addSubIssue` + inbox pointer (Director workflow).
+
+## Implementation slices (suggested PR shape)
+
+1. **Slice A — coverage + fixture shape:** Verification + Substrate land **stage (a)** authoring against unified predicate proposal (no premature strict-fire green if **(b)** open).
+2. **Slice B — executable strict-fire:** `tc3_pattern_a_second_mover_executable` + integration **Pass** when **(a)+(b)** satisfied.
+3. **Slice C — ledger/doc:** §1.8 status + bundle row update in [`r3-v-formal-grounding-tc-bundle.md`](r3-v-formal-grounding-tc-bundle.md).
+
+**Substrate lands first** on predicate splits — Verification does not invent carriers.
+
+## Cross-refs
+
+- Conformance audit: [`r3-v-tc3-pattern-a-second-mover-conformance-audit.md`](r3-v-tc3-pattern-a-second-mover-conformance-audit.md)
+- TC bundle: [`r3-v-formal-grounding-tc-bundle.md`](r3-v-formal-grounding-tc-bundle.md)
+- PB declarative theorem: [`r3-pb-t-fixedpoint-worker.md`](r3-pb-t-fixedpoint-worker.md) §TC3
+- TC1 / TC2 worker neighbors: [`r3-v-pattern-a-tc1-v1-worker.md`](r3-v-pattern-a-tc1-v1-worker.md), [`r3-v-pattern-a-tc2-v1-worker.md`](r3-v-pattern-a-tc2-v1-worker.md)
+- Deferred fixture: `src/v3/compiler/tests/fixtures/tc3_strong_normalization_deferred.dag`

docs/briefs/r3-v-t-lbp-narrowed-scope-partner-worker.md

@@ -0,0 +1,57 @@
+# R3 T-Lens-Behavioral-Parity — Verification partner brief (option **(b)** narrow scope)
+
+**Status:** **PRE-AUTH DISPATCH-READY** — Verification-side cross-program partner after Director ratification **Q-Lens-Behavioral-Parity-R3-Closeability option (b)** (**#828**). Substrate owns S2 canvas + substrate folds; **this brief** owns Verification receipts that gate **cementing**, **demonstration**, and **register alignment** from the Verification lane.
+
+**Parent:** [`docs/briefs/r3-verification-manager.md`](r3-verification-manager.md).
+
+**Substrate canvas (authority for blocker matrix):** [`docs/briefs/r3-substrate-s2-t-lbp-scope-calibration-canvas.md`](r3-substrate-s2-t-lbp-scope-calibration-canvas.md).
+
+**Carve-out routing (IN R3 vs R4):** [`docs/r4-carve-out-routing.md`](../r4-carve-out-routing.md) **C1–C3** — **complexity** + **cost** lenses **IN R3**; **parallelism** + **effect_enumeration** **carved to R4**; register gate **#83** narrowed to in-scope lenses only.
+
+**Single authority (INVARIANTS §P2):** Option **(b)** obligation text is **`docs/r3-structure.md`** §"Acceptance" T-Lens-Behavioral-Parity **plus** the matching Summary lane bullet (item **14**) **plus** the §"Lane structure" table row — updated in lockstep. **This brief** elaborates Verification receipts only; it does **not** define lane scope independently of `r3-structure.md`.
+
+**Lane acceptance:** [`docs/r3-structure.md`](../r3-structure.md) §"Acceptance" T-Lens-Behavioral-Parity — gates **#79–#83** in [`docs/r3-program-plan.md`](../r3-program-plan.md) §1.8.
+
+## In-R3 obligations (Verification-owned or cross-program)
+
+| Plan gate # | Gate ID | Verification partner role |
+| --- | --- | --- |
+| 79 | `complexity_lens_behaviorally_complete` | Cementing tests + `ClaimResult` diagnostics; consumes T-E-P producer evidence; aligns witness shapes with [`r3-v-witness-shape-pattern-survey.md`](r3-v-witness-shape-pattern-survey.md) |
+| 80 | `cost_lens_behaviorally_complete` | Same — shared producer dependency as complexity (S2 matrix lens 2) |
+| 73 | `lens_behavioral_parity_demonstration` | Per **in-R3** lens demo (complexity, cost) matching **frozen** v2-oracle snapshot (plan §1.6 — **not** live v2 consumer); carved lenses **R4** |
+| 83 | `lens_capability_register_zero_proxy_zero_stub` | Receipt that register lists **ZERO PROXY / ZERO STUB** for **complexity + cost only**; **document** R4-carved rows per **C3** |
+
+## Out of R3 (partner discipline)
+
+| Gate ID | Discipline |
+| --- | --- |
+| `parallelism_lens_behaviorally_complete` | **STOP+PING for R3 closure** — carved **C1**; no Verification PASSING receipt pretending R3 owns this slice |
+| `effect_enumeration_lens_behaviorally_complete` | **STOP+PING for R3 closure** — carved **C2** |
+
+## Dependencies
+
+| ID | Dependency | Owner |
+| --- | --- | --- |
+| L1 | T-E-P Phase 1 producer coverage (`e_p_*` gates) | Substrate / Evaluator |
+| L2 | Behavioral lens folds for complexity + cost | Substrate |
+| L3 | Frozen snapshot capture **before** v2 retirement | Cross-program (PB + Verification timing) |
+| L4 | Capability register updates for narrowed scope | Substrate + Verification audit |
+
+## Dispatch triggers
+
+1. **L1** unblocks complexity/cost producer consumption (S2 matrix lens 1–2).
+2. **L3** plan locked — cementing demos won't reattach live v2 test consumers.
+3. **Cross-program PR** pattern: Substrate lands lens fold + register rows; Verification lands cementing integration + demonstration `TestClaim` receipts.
+
+## STOP+PING
+
+| Item | Discipline |
+| --- | --- |
+| Expanding T-LBP back to 4 lenses inside R3 | **STOP+PING** — requires Director revision of option **(b)** |
+| Cementing without frozen snapshot discipline | **STOP+PING** — conflicts with `v2_oracle_no_remaining_test_consumers` closure narrative |
+
+## Cross-refs
+
+- Tests-as-data lane (cementing gate D): [`r3-v-tests-as-data-v1-worker.md`](r3-v-tests-as-data-v1-worker.md)
+- Free-consequences / witness overlap: [`r3-v-free-consequences-worker.md`](r3-v-free-consequences-worker.md)
+- Program plan §10.3 Q-LBP row: [`docs/r3-program-plan.md`](../r3-program-plan.md) §10.3