diff --git a/docs/briefs/r3-v-pattern-a-rust-dag-isomorphism-v1-worker.md b/docs/briefs/r3-v-pattern-a-rust-dag-isomorphism-v1-worker.md new file mode 100644 index 00000000000..bcb1ff655db --- /dev/null +++ b/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` (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`** (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" diff --git a/docs/briefs/r3-v-pattern-a-tc3-v1-worker.md b/docs/briefs/r3-v-pattern-a-tc3-v1-worker.md new file mode 100644 index 00000000000..998babecce6 --- /dev/null +++ b/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`** 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` 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` 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` diff --git a/docs/briefs/r3-v-t-lbp-narrowed-scope-partner-worker.md b/docs/briefs/r3-v-t-lbp-narrowed-scope-partner-worker.md new file mode 100644 index 00000000000..a8d0eaabe94 --- /dev/null +++ b/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 diff --git a/docs/briefs/r3-v-t-lens-application-surface-execution-split-worker.md b/docs/briefs/r3-v-t-lens-application-surface-execution-split-worker.md new file mode 100644 index 00000000000..c3b2c8b815f --- /dev/null +++ b/docs/briefs/r3-v-t-lens-application-surface-execution-split-worker.md @@ -0,0 +1,67 @@ +# R3 T-Lens-Application-Surface — execution split (substrate vs demonstration) + +**Status:** **PRE-AUTH DISPATCH-READY** — separates **carrier / routing execution** from **worked-example demonstration execution** for lane **T-Lens-Application-Surface** (tier-1 queue **#1859**). Cross-program: **Substrate Manager + Verification Manager** per `r3-structure.md` §"Lane structure". + +**Parent:** [`docs/briefs/r3-verification-manager.md`](r3-verification-manager.md). + +**Design lock:** [`docs/design-lens-application-surface.md`](../design-lens-application-surface.md). + +**Cascade / carve (INVARIANTS §P2):** Internal LAS cascade in [`docs/design-lens-application-surface.md`](../design-lens-application-surface.md) §**7** / §**9** requires each worked example’s lens to be **behaviorally substantive**. Under Director **option (b)** + [`docs/r4-carve-out-routing.md`](../r4-carve-out-routing.md) **C1**, **`parallelism_lens_behaviorally_complete`** is **R4-carved**, and **`opt_in_iteration_parallelism_via_lens_application_demonstrated` (#95) carves with it** — **no #95 PASSING in R3** (demo §4.4 needs parallelism lens parity per design §4.4). **R3** executes substrate **88–91** + demos **92–94** only after **complexity+cost** T-LBP completeness + register **C3**; **#95** schedules against **R4** parallelism landing. + +## Execution slice A — substrate-shape + routing (Substrate-primary) + +| Plan §1.8 # | Gate ID | Pass intent | +| --- | --- | --- | +| 88 | `lens_application_carrier_landed` | `EnforcedApplication` + `IntrospectApplication` | +| 89 | `section_ref_substrate_landed` | `SectionRef` disjoint sum | +| 90 | `lens_enforcement_carrier_landed` | Per-lens `LensEnforcement` projection | +| 91 | `enforce_violation_routing_landed` | Enforce-mode routing through `DiagnosticSeverity` (design §3 + **INVARIANTS** C-8) | + +**Verification partner:** conformance tests + `TestClaim` shells only after carriers exist — **does not** author top-level carriers (**§P1**). + +## Execution slice B — demonstrations (cross-program) + +### B1 — **R3** (after complexity+cost T-LBP + slice **A**) + +| Plan §1.8 # | Gate ID | Pass intent | +| --- | --- | --- | +| 92 | `complexity_violation_compile_error_demonstrated` | `apply_lens(complexity, …, Enforce)` compile-error worked example | +| 93 | `crdt_cost_basis_demonstrated` | CRDT cost basis via `apply_lens` | +| 94 | `memory_peak_cost_basis_demonstrated` | Memory-peak cost basis | + +### B2 — **R4 (C1)** — blocked on `parallelism_lens_behaviorally_complete` + +| Plan §1.8 # | Gate ID | Pass intent | +| --- | --- | --- | +| 95 | `opt_in_iteration_parallelism_via_lens_application_demonstrated` | Iteration-independence opt-in via lens application (**design** §4.4 — requires **parallelism** lens substantive semantics; **carves with C1** per `r4-carve-out-routing.md`) | + +**Verification-owned:** integration `TestClaim`s, corpus fixtures, diagnostic assertions by shape ([`TESTING.md`](../../TESTING.md)). + +## Dependencies + +| ID | Dependency | Notes | +| --- | --- | --- | +| A1 | Slice **A** gates green | Hard prerequisite for meaningful Slice **B** demos | +| A2 | Evaluator + lens runtime | Lane row R2-Evaluator gating | +| A3 | Class 2 gap-test narrative | `substrate_gap_function_valued_data_closed` traces through LAS + T-E-P per plan §1.8 — keep receipts aligned (**#828** chain-break discipline) | +| A4 | **`parallelism_lens_behaviorally_complete` (R4 C1)** | **Gate #95 only** — demos **92–94** do **not** wait on parallelism parity | + +## Dispatch triggers + +1. Substrate signals **88–91** consumer-ready. +2. Verification schedules demos **92–94** when **complexity+cost** T-LBP + slice **A** clear; schedules **#95** only after **R4** parallelism parity (**C1**) — **no parallel authority**. +3. Escalate substrate-shape questions → **[#1739](https://github.com/gunb-ai/gunbc/issues/1739)**; Verification inbox **[#1740](https://github.com/gunb-ai/gunbc/issues/1740)**. + +## STOP+PING + +| Item | Discipline | +| --- | --- | +| Demonstrations **before** enforce routing landed | **STOP+PING** — fail-closed semantics undefined | +| Claiming **T-LBP COMPLETE** for carved lenses | **STOP+PING** — **C1/C2** remain R4 | +| **`#95` PASSING under R3 thesis close** | **STOP+PING** — **R4 (C1)** per `r4-carve-out-routing.md` + design §7 | + +## Cross-refs + +- T-LBP partner (producer + cementing alignment): [`r3-v-t-lbp-narrowed-scope-partner-worker.md`](r3-v-t-lbp-narrowed-scope-partner-worker.md) +- Self-application lane consumer: [`docs/r3-structure.md`](../r3-structure.md) §"Acceptance" T-Lens-Self-Application (uses `EnforcedApplication` timing example) +- Substrate gap class row **#174**: [`docs/r3-program-plan.md`](../r3-program-plan.md) §1.8 diff --git a/docs/briefs/r3-v-tests-as-data-v1-worker.md b/docs/briefs/r3-v-tests-as-data-v1-worker.md new file mode 100644 index 00000000000..70095240a94 --- /dev/null +++ b/docs/briefs/r3-v-tests-as-data-v1-worker.md @@ -0,0 +1,71 @@ +# R3 T-Tests-As-Data-Completeness — unified dispatch-ready worker brief (V4) + +**Status:** **PRE-AUTH DISPATCH-READY** — consolidates lane closure gates into one worker-facing dispatch artifact (tier-1 queue **#1859**). **No substrate edits** in this brief; carrier introduction stays **§P1** Substrate-owned. + +**Parent:** [`docs/briefs/r3-verification-manager.md`](r3-verification-manager.md). + +**Lane authority:** [`docs/r3-structure.md`](../r3-structure.md) §"Lane structure" + §"Acceptance" — **T-Tests-As-Data-Completeness**. + +**Readiness audit (gap vs HEAD):** [`docs/briefs/r3-v-tests-as-data-completeness-readiness-audit.md`](r3-v-tests-as-data-completeness-readiness-audit.md) — census counts, gate A–D snapshots; **this brief** is the **dispatch overlay** (triggers, slices, STOP+PING). + +**Design lock (read-only):** [`docs/design-tests-as-data-completeness.md`](../design-tests-as-data-completeness.md). + +## Closure gates (lane — single worker coordinates) + +| Gate ID | Canonical name | Role | +| --- | --- | --- | +| — | `every_rust_test_ports_to_dag_or_generated` | Facet-3 close: hand-authored Rust test partition → **0** per design §1.1 | +| — | `forall_exists_quantifier_substrate_landed` | Mathematical `ForAll` / `Exists` over program families (**not** `ForAllTargets` emission shim) | +| — | `program_generator_carrier_landed` | `ProgramGenerator` / quantified claim substrate | +| — | `lens_cementing_test_discipline_complete` | Every **in-R3** `.dag` lens with behavioral-complete intent has cementing module vs frozen v2 oracle | + +**Demonstration sibling (plan §1.8):** `tests_as_data_demonstration` — at least one Rust test ports to `.dag` `TestClaim` and executes (early signal; **not** a substitute for gate row closure). + +## Worker pin + +| Preference | Worker | Condition | +| --- | --- | --- | +| **Primary** | **bold-crane-790** (**#1748**) or **cool-heron-521** when SB slice active | R2-Evaluator + TestClaim runtime precondition per lane row | +| **Alternate** | **New worker** | Partition per `feedback_idle_workers_dispatchable_directly` | + +## Scope (in) + +- **SG-0 census honesty** — [`sg0_census_test.rs`](../../src/v3/compiler/tests/integration/sg0_census_test.rs) list stays reconciled to tree (readiness audit §2). +- **Migration slices 2–5** from readiness audit §6 — predicate-class mapping → generated target tests → quantifiers → facet-3 zero census. +- **Cross-lane receipts** — Lane 1↔2 import contract ([`r3-v-lane1-lane2-corpus-identity-import-spec.md`](r3-v-lane1-lane2-corpus-identity-import-spec.md)); cementing alignment with **T-LBP** narrow scope ([`r3-v-t-lbp-narrowed-scope-partner-worker.md`](r3-v-t-lbp-narrowed-scope-partner-worker.md)). + +## Scope (out) — STOP+PING + +| Item | Discipline | +| --- | --- | +| **Inventing `ProgramGenerator` / quantifier variants in Verification PRs** | **STOP+PING** — §P1 substrate introduction only | +| **Dropping census entries without port or explicit carve-out** | **STOP+PING** — debt visibility discipline | +| **Claiming lens cementing COMPLETE while T-LBP rows PROXY/STUB for in-scope lenses** | **STOP+PING** — register authority [`docs/v3-lens-capability-register.md`](../v3-lens-capability-register.md) | + +## Dependencies (hard) + +| ID | Dependency | Owner | +| --- | --- | --- | +| T1 | R2-Evaluator test execution + `TestClaim` runner stable | Evaluator | +| T2 | Emission path for `TestPredicate` → generated target tests (design §1.3 Path B) | Substrate + Verification | +| T3 | Frozen v2-oracle snapshot infrastructure for cementing | Cross-program (see T-LBP partner brief) | +| T4 | Quantifier + generator carriers | Substrate (**§P1**) | + +## Dispatch triggers + +1. **T1** green — continuation **[#1743](https://github.com/gunb-ai/gunbc/issues/1743)** receipts. +2. **T2** slice scoped — first port lands **#1276** / Verification inbox signal as appropriate. +3. **Sub-issue** under Verification inbox **#1740** (or bold-crane **#1748** when Track A) + Director workflow. + +## Implementation slices (suggested PR sequence) + +1. **V4-a — Census + mapping:** refresh readiness audit §1; extend predicate coverage map (audit §6 slice 2). +2. **V4-b — First executable port:** satisfy `tests_as_data_demonstration` + shrink SG-0 net (audit §6 slice 3). +3. **V4-c — Quantifiers + generator:** land when **T4** clears (audit §6 slice 4). +4. **V4-d — Facet-3 close:** census **0** + cementing discipline satisfied (audit §6 slice 5). + +## Cross-refs + +- Slice-1 census: [`r3-v-tests-as-data-slice1-census-reconciliation.md`](r3-v-tests-as-data-slice1-census-reconciliation.md) +- Witness patterns: [`r3-v-witness-shape-pattern-survey.md`](r3-v-witness-shape-pattern-survey.md) +- TESTING / DB-15: [`TESTING.md`](../../TESTING.md), [`docs/design-test-infra.md`](../design-test-infra.md) diff --git a/docs/briefs/r3-verification-manager.md b/docs/briefs/r3-verification-manager.md index 763a02563ea..5bd193e2998 100644 --- a/docs/briefs/r3-verification-manager.md +++ b/docs/briefs/r3-verification-manager.md @@ -97,6 +97,11 @@ Each lane closes under a structural acceptance gate authored as a `.dag` `TestCl - [`r3-v-free-consequences-worker.md`](r3-v-free-consequences-worker.md) — Lane 3 standby brief. - [`r3-v-pattern-a-tc1-v1-worker.md`](r3-v-pattern-a-tc1-v1-worker.md) — Pattern-A V1 (TC1 first executable slice; Q-PAFS Path A **ACCEPTED** 2026-05-06). - [`r3-v-pattern-a-tc2-v1-worker.md`](r3-v-pattern-a-tc2-v1-worker.md) — Pattern-A TC2 (`tc2_church_rosser_executable`) dispatch-ready worker brief (**PRE-AUTH**; strategy-order / Church-Rosser slice). +- [`r3-v-pattern-a-tc3-v1-worker.md`](r3-v-pattern-a-tc3-v1-worker.md) — Pattern-A TC3 (`tc3_pattern_a_second_mover_executable`) dispatch-ready worker brief (**PRE-AUTH**; evaluation-step / second-mover; two-stage bundle). +- [`r3-v-pattern-a-rust-dag-isomorphism-v1-worker.md`](r3-v-pattern-a-rust-dag-isomorphism-v1-worker.md) — Pattern-A gate **#14** `rust_dag_isomorphism_executable` (**PRE-AUTH**; Dag-iso / shape-report consumer shell). +- [`r3-v-tests-as-data-v1-worker.md`](r3-v-tests-as-data-v1-worker.md) — T-Tests-As-Data-Completeness unified dispatch overlay (**PRE-AUTH**; facet-3 + quantifiers + cementing alignment). +- [`r3-v-t-lbp-narrowed-scope-partner-worker.md`](r3-v-t-lbp-narrowed-scope-partner-worker.md) — T-LBP Verification partner (**PRE-AUTH**; option **(b)** complexity+cost in R3; cementing + register **C3** receipts). +- [`r3-v-t-lens-application-surface-execution-split-worker.md`](r3-v-t-lens-application-surface-execution-split-worker.md) — T-LAS execution split (**PRE-AUTH**; substrate gates **88–91** vs demonstration **92–95**). - [`r3-v-formal-grounding-tc-bundle.md`](r3-v-formal-grounding-tc-bundle.md) — absorbed-responsibility TC1/TC2/TC3 bundle (NOT a lane; audit-cadence artifact per `r3-structure.md` §"Manager structure" Item 2 3-lane authority). **Pending (post-spawn manager authors autonomously):** diff --git a/docs/design-lens-application-surface.md b/docs/design-lens-application-surface.md index 7d78be2dcfd..1652a115d4a 100644 --- a/docs/design-lens-application-surface.md +++ b/docs/design-lens-application-surface.md @@ -380,12 +380,14 @@ The split mirrors the existing T-CostLens-Composition split: substrate authors c ## §7. Cascade gates -Per [`docs/r3-structure.md`](r3-structure.md): +Per [`docs/r3-structure.md`](r3-structure.md) + [`docs/r4-carve-out-routing.md`](r4-carve-out-routing.md): -- **Internal cascade**: T-Lens-Behavioral-Parity must reach BEHAVIORALLY COMPLETE before T-Lens-Application-Surface dispatches. Reason: a `complexity_violation_compile_error_demonstrated` TestClaim requires the complexity lens to actually compute correct asymptotic classes (not just the depth proxy currently shipped). Likewise for cost / parallelism / effect_enumeration. Behavioral parity gives lens-application substantive semantics. -- **External cascade**: R2-Evaluator landed (per the standard R3 worker-dispatch precondition). +- **Substantive-semantics principle:** each worked example requires its corresponding lens to be **behaviorally substantive** — a `complexity_violation_compile_error_demonstrated` TestClaim requires the complexity lens to compute correct asymptotic classes (not just the depth proxy currently shipped). Likewise cost / parallelism for their respective demos. +- **R3 program reconciliation (T-LBP option (b) RATIFIED 2026-05-06):** R3 T-LBP closes **complexity + cost** behavioral completeness only; **parallelism** + **effect_enumeration** completeness carve to **R4** (C1/C2). Therefore **R3** T-Lens-Application-Surface lands substrate **88–91** + demos **92–94** after **complexity+cost** parity + register **C3** — without waiting for parallelism / effect_enum completeness. +- **Gate #95 / §4.4:** `opt_in_iteration_parallelism_via_lens_application_demonstrated` requires the **parallelism** lens implementation referenced in §4.4 (T-LBP slice 3). That lens’s behavioral completeness is **R4-carved (C1)**; **#95** **carves alongside it** — **do not** claim **#95** PASSING as part of **R3** thesis close (**INVARIANTS** P2 single authority). +- **External cascade:** R2-Evaluator landed (per the standard R3 worker-dispatch precondition). -Pre-cascade *design-doc* work is permitted (this doc); pre-cascade *substrate work* (carriers landing, fold-integration code) waits for T-Lens-Behavioral-Parity COMPLETE. +Pre-cascade *design-doc* work is permitted (this doc); pre-cascade *substrate work* for carriers consumed by **R3** demos **92–94** waits for **R3** T-LBP (**complexity+cost**) COMPLETE + **C3**; substrate+demo work keyed solely on **#95** waits on **R4** parallelism parity per bullet above. ## §8. Resolved design questions @@ -451,14 +453,14 @@ Five design questions surfaced during authoring. Per `feedback_design_before_imp --- -All five questions resolved. Implementation can proceed without further Director ratification on these specific points. Cascade gates (T-Lens-Behavioral-Parity COMPLETE for §8.3 enforcement-flip) and external dependencies (R2-Evaluator landed) remain as the only outstanding preconditions. +All five questions resolved. Implementation can proceed without further Director ratification on these specific points. Cascade gates: **R3** LAS substrate+demos **88–94** wait on **complexity+cost** T-LBP COMPLETE + **C3**; **#95** waits on **R4** parallelism parity (**C1**). External dependency: R2-Evaluator landed. ## §9. Relationship to existing authority This design doc extends: - [`docs/lens-library-design.md`](lens-library-design.md) §3 — the existing file-glob `LensApplication`. **No changes to existing carrier**; this doc adds `EnforcedApplication` + `IntrospectApplication` as sibling carriers with structural section references. -- [`docs/v3-lens-capability-register.md`](v3-lens-capability-register.md) — the lens-capability register tracking PROXY/STUB/PARTIAL/COMPLETE status per lens. This design assumes T-Lens-Behavioral-Parity has driven all four target lenses to COMPLETE before T-Lens-Application-Surface implementation begins. +- [`docs/v3-lens-capability-register.md`](v3-lens-capability-register.md) — the lens-capability register tracking PROXY/STUB/PARTIAL/COMPLETE status per lens. **R3 (option b):** LAS demos **92–94** assume **complexity + cost** reach COMPLETE first; **`opt_in_iteration_parallelism_via_lens_application_demonstrated` (#95)** assumes **parallelism** COMPLETE and is **R4-carved (C1)** alongside that lens per `r4-carve-out-routing.md`. **R4 horizon:** register reaches ZERO PROXY / ZERO STUB across all four behavioral lenses per `r4-carve-out-routing.md` **C3** closing paragraph. - [`docs/design-lens-framework.md`](design-lens-framework.md) — the `Lens` framework. This design adds one fold-pass extension (lens-application discovery + budget comparison) but does not modify the underlying `Lens` shape. - [`../INVARIANTS.md`](../INVARIANTS.md) C-8 (fail-closed compilation) — load-bearing for §3 (no Warning, no Silent policies). - [`../INVARIANTS.md`](../INVARIANTS.md) P2 (boundary discipline) — load-bearing for §8.2 (single-authority for `(lens, section)` pairs). @@ -487,4 +489,4 @@ Total estimate (per L-XL sizing in the lane row): substrate carriers + fold-pass --- -**This document is a design spec, not a ship target.** It resolves the structural design questions blocking T-Lens-Application-Surface lane dispatch. The lane itself runs once cascade gates clear (T-Lens-Behavioral-Parity COMPLETE + R2-Evaluator landed). All §8 design questions resolved in-doc; no Director ratification required before substrate authoring begins. +**This document is a design spec, not a ship target.** It resolves the structural design questions blocking T-Lens-Application-Surface lane dispatch. The lane runs when cascade gates clear per §**7** (**R3** vs **R4** split for option **(b)**) + R2-Evaluator landed. All §8 design questions resolved in-doc; no Director ratification required before substrate authoring begins within that split. diff --git a/docs/r3-program-plan.md b/docs/r3-program-plan.md index e0d05f468a9..afc23c6d866 100644 --- a/docs/r3-program-plan.md +++ b/docs/r3-program-plan.md @@ -5,7 +5,7 @@ **Merge gates** (distinct from PR-open status — per openai-pro 2026-05-06 finding): - **PR open**: ✓ at sha `d1bfbbe22` - **Plan PR merge-eligible**: open RED escalations in §10.3 acknowledged + tracked (not necessarily resolved); PR can merge with RED items in flight provided they're explicitly tracked + assigned routing -- **R3 close** (NOT plan PR merge): all 95 closure gates GREEN (with §10.3 Q-Lens-Behavioral-Parity-R3-Closeability **RATIFIED option (b) 2026-05-06**: T-LBP R3 scope = complexity + cost lenses only; parallelism + effect_enum carved to R4 per `docs/r4-carve-out-routing.md`) + `r3_debt_paydown_zero_remaining` + comprehensive sweep zero-debt + other §10.3 RED items resolved per their owners +- **R3 close** (NOT plan PR merge): all **R3-load-bearing** §1.8 closure gates GREEN (**95** gate IDs enumerated; **#81**/**#82**/**#95** are **CARVED to R4** per `docs/r4-carve-out-routing.md` C1/C2/C1 — not in the R3 conjunction) + §10.3 Q-Lens-Behavioral-Parity-R3-Closeability **option (b)** (T-LBP = complexity + cost in R3; parallelism + effect_enum R4) + `r3_debt_paydown_zero_remaining` + comprehensive sweep zero-debt + other §10.3 RED items resolved per their owners **Purpose.** Forward-looking program plan for **R3 close with zero debt**. Per user directive 2026-05-05 (gunbc#846): *"clear dependency graph from here to R3 close"* + *"surface escalations now and solve them"*. @@ -87,10 +87,12 @@ Per `r3-debt-sweep-2026-05-06.md` §Class A (line 39): *"parser/grammar surface, **Per codex BLOCKING 2026-05-06 inline at line 79**: prior 70-count omitted the 5 NEW Pattern-A executable gates (`tc1_eta_equivalence_executable`, `tc2_church_rosser_executable`, `tc3_pattern_a_second_mover_executable`, `rust_dag_isomorphism_executable`, `symbolic_cost_expr_equals_executable`) declared in §1.1 but not yet in `r3-structure.md` §"Acceptance". This commit adds them to the canonical authority and bumps total from 70 → 75; single-authority restored (INVARIANTS P2/P5). -R3 closes when ALL gates pass + zero tracked-debt rows survive (`r3_debt_paydown_zero_remaining`). +R3 closes when **all non-carved §1.8 gates** pass + zero tracked-debt rows survive (`r3_debt_paydown_zero_remaining`). + +**R4-carved §1.8 rows** (enumerated for traceability; **excluded** from R3 thesis-close conjunction — **INVARIANTS** §P2): **`#81`** `parallelism_lens_behaviorally_complete`, **`#82`** `effect_enumeration_lens_behaviorally_complete`, **`#95`** `opt_in_iteration_parallelism_via_lens_application_demonstrated` — per `docs/r4-carve-out-routing.md` C1/C2/C1 cascade + `docs/design-lens-application-surface.md` §7. **Two distinct Pass surfaces** (per Debt-Paydown Mgr poke-hole 2026-05-06 — clarification prevents conflating predicates): -- **Lane `.dag` TestClaim gates (95 total)**: per-lane closure predicates passing via `.dag` evaluation, runtime demonstration, or CI consumer (per §1.7 status taxonomy). +- **Lane `.dag` TestClaim gates (95 enumerated; 92 load-bearing for R3 thesis close)**: per-lane closure predicates passing via `.dag` evaluation, runtime demonstration, or CI consumer (per §1.7 status taxonomy). - **`r3_debt_paydown_zero_remaining`**: standing-program ledger predicate — no tracked ROADMAP debt rows survive R3 close (per `r3-structure.md` §"Standing program — R3 Debt-Paydown" + §1.5 tracked-debt inclusion list). Both must hold for R3 close. "95 gates green" alone does not satisfy zero-debt; "zero debt rows" alone does not satisfy lane closure. @@ -163,7 +165,7 @@ Mgrs author per-gate spec citing the (a)/(b)/(c) satisfaction; closure-ledger en | T-V2-Retirement | deletion gates (state-check) | + `v3_self_host_demonstration` — bootstrap path through PB-Runtime trampoline executes end-to-end; v3-only self-host pipeline runs without v2 fallback (Director poke-hole 2026-05-06 finding 4.1: reframed from `v2_retirement_demonstration` "deletion's inverse" to direct positive-statement form) | | T-Free-Consequences-Demonstration | 10 demo gates ✓ | (existing — full demo suite) | | T-E-P-Producer-Broadening | substrate-shape gates | + `e_p_producer_demonstration` — representative call site produces full descent evidence at runtime | -| T-Lens-Behavioral-Parity | parity-complete gates | + `lens_behavioral_parity_demonstration` — each lens (complexity/cost/parallelism/effect_enumeration) demonstrates on representative input + matches **frozen v2-oracle cementing-test snapshot** (per `r3-structure.md` §"Lane structure" → T-Lens-Behavioral-Parity row "cementing test against v2 oracle on same source"). Snapshot is captured pre-v2-retirement; demo at R3 close consumes the frozen receipt, NOT a live v2 oracle — preserves `v2_oracle_no_remaining_test_consumers` gate (per openai-pro 2026-05-06 finding 5 — v2-oracle conflict resolved) | +| T-Lens-Behavioral-Parity | parity-complete gates | + `lens_behavioral_parity_demonstration` — **R3:** **complexity + cost** lenses demonstrate on representative input + match **frozen v2-oracle cementing-test snapshot** (per `r3-structure.md` §"Acceptance" T-Lens-Behavioral-Parity option **(b)** narrowing). **Parallelism + effect_enumeration** demos **R4-carved** — same frozen-receipt discipline when executed in R4; not R3 closure. Snapshot is captured pre-v2-retirement; demo at R3 close consumes the frozen receipt, NOT a live v2 oracle — preserves `v2_oracle_no_remaining_test_consumers` gate (per openai-pro 2026-05-06 finding 5 — v2-oracle conflict resolved) | | T-Tests-As-Data-Completeness | substrate-shape gates | + `tests_as_data_demonstration` — at least one Rust test ports to .dag TestClaim and executes | | T-Lens-Application-Surface | 4 worked-example demos ✓ | (existing) | | T-Workflow-As-Data | `ci_workflow_modeled_as_dag` ✓ | (existing) | @@ -267,7 +269,7 @@ This principle is NOT a separate lane; it's a per-lane gate-shape requirement ap | 70 | `cost_lens_demonstration` | demonstration | T-CostLens-Composition | DECLARED (NEW 2026-05-06) | ≥2 algebra-instances + ≥1 recursive call | | 71 | `v3_self_host_demonstration` | demonstration | T-V2-Retirement | DECLARED (NEW 2026-05-06) | bootstrap PB-Runtime trampoline runs end-to-end | | 72 | `e_p_producer_demonstration` | demonstration | T-E-P-Producer-Broadening | DECLARED (NEW 2026-05-06) | call-site produces full descent evidence | -| 73 | `lens_behavioral_parity_demonstration` | demonstration | T-Lens-Behavioral-Parity | DECLARED (NEW 2026-05-06) | matches frozen v2-oracle cementing-test snapshot | +| 73 | `lens_behavioral_parity_demonstration` | demonstration | T-Lens-Behavioral-Parity | DECLARED (NEW 2026-05-06) | **R3:** complexity+cost vs frozen v2-oracle snapshot; parallelism/effect_enum **R4-carved** (see `r3-structure.md` §"Acceptance") | | 74 | `tests_as_data_demonstration` | demonstration | T-Tests-As-Data-Completeness | DECLARED (NEW 2026-05-06) | Rust test ports to `.dag` TestClaim + executes | | 75 | `pr_anticipation_discipline_ci_active` | CI-discipline | R3 Debt-Paydown (standing) | DECLARED (NEW 2026-05-06) | `scripts/check-pr-sg0-net-shrink-discipline.sh` in CI | | 76 | `e_p_per_call_descent_evidence_full_coverage` | substrate-shape | T-E-P-Producer-Broadening | DECLARED (added to §"Acceptance" 2026-05-06 per codex BLOCKING) | per-call DescentEvidence covers all live call sites | diff --git a/docs/r3-structure.md b/docs/r3-structure.md index ab9abfc8a5f..b2767ba3781 100644 --- a/docs/r3-structure.md +++ b/docs/r3-structure.md @@ -35,9 +35,9 @@ R3 has **18 lanes + 1 standing program** (revised 2026-04-28 per Director review 11. **T-V2-Retirement (NEW 2026-04-30)** — retire `src/v2/` (~79 .rs + ~32 .dag files); workspace member removed; bootstrap routes through PB-Runtime trampoline only. Largely consequence of T-FixedPoint + T-LensProducer-Retirement closing; pulled into R3 per user directive *"nothing can be deferred past R3."* 12. **T-Free-Consequences-Demonstration (NEW 2026-04-30)** — operationalizes thesis "free consequences" framing with `docs/design-free-consequences.md` + 10-gate TestClaim suite (auto-parallelism × 3 + auto-loop-parallelism × 3 + auto-memoization × 2 + cross-target-optimization × 2). Loop-iteration parallelism: sequential default + opt-in via `Lens`. Per user directive *"what guarantees does the compiler ACTUALLY provide."* 13. **T-E-P-Producer-Broadening (NEW 2026-05-02)** — broaden per-call `DescentEvidence` / `CallPattern` / `SubValueRelation` producer coverage from current first slice (recursive self-call + arithmetic-descent only) to full `ExprCall.descent_evidence` parity at live call sites. **Foundational** — affects complexity + cost lens behavioral parity. Substrate Mgr; M-L sized. -14. **T-Lens-Behavioral-Parity (NEW 2026-05-02)** — bring complexity / cost / parallelism / effect_enumeration lenses from PROXY/STUB/PARTIAL to BEHAVIORALLY COMPLETE per `docs/v3-lens-capability-register.md`. Lens consumers read per-call substrate facts (gated on T-E-P-Producer-Broadening). Includes: symbolic CostExpr full algebra (Sum/Mul/Log/Const) consumed by lens; work/span dimension split for complexity; asymptotic classification; cementing test against v2 oracle on same source; Stage 2e parallelism walk port from Rust to `.dag`; resource-threading migration for effect_enumeration. Substrate + Verification cross-program; L-XL sized. **Closure gate**: `lens_capability_register_zero_proxy_zero_stub` — register status updated to ZERO PROXY / ZERO STUB at R3 close. +14. **T-Lens-Behavioral-Parity (NEW 2026-05-02)** — **R3 obligation (option (b) RATIFIED 2026-05-06 per [gunbc#828 #issuecomment-4385329180](https://github.com/gunb-ai/gunbc/issues/828#issuecomment-4385329180)):** bring **complexity** + **cost** lenses from PROXY/STUB/PARTIAL to BEHAVIORALLY COMPLETE per `docs/v3-lens-capability-register.md`. **Parallelism** + **effect_enumeration** behavioral-complete slices are **carved to R4** per `docs/r4-carve-out-routing.md` C1+C2 — not R3 closure work. Lens consumers read per-call substrate facts (gated on T-E-P-Producer-Broadening). **R3 slice includes:** symbolic CostExpr full algebra (Sum/Mul/Log/Const); work/span dimension split; asymptotic classification; cementing test against frozen v2-oracle snapshot. **Closure gate (R3):** `lens_capability_register_zero_proxy_zero_stub` — register reports ZERO PROXY / ZERO STUB **for complexity + cost only** at R3 close (C3); carved lenses documented per register discipline. **Full gate IDs / carve labels:** §"Acceptance" T-Lens-Behavioral-Parity — single authority (**INVARIANTS** §P2). Substrate + Verification cross-program; lane remains **L-XL** as an ambition label **across R3+R4**; R3 thesis close consumes only the in-scope rows above. 15. **T-Tests-As-Data-Completeness (NEW 2026-05-02)** — close Category E test/verification surface gaps per user directive: every Rust test ports to `.dag` TestClaim or generated target-language test code (thesis facet 3); property-based testing surface (`ForAll` / `Exists` quantifiers + `ProgramGenerator` substrate carrier); cementing test discipline for `.dag` lenses. Verification Mgr; L sized. **Closure gates**: `every_rust_test_ports_to_dag_or_generated`, `forall_exists_quantifier_substrate_landed`, `program_generator_carrier_landed`. -16. **T-Lens-Application-Surface (NEW 2026-05-02; design doc landed 2026-05-02 [`docs/design-lens-application-surface.md`](design-lens-application-surface.md))** — first-class authoring surface for applying lenses to arbitrary `.dag` sections (function / module / expression / declaration scope). Per user reframe: lens application is a `.dag` declaration with configurable behavior — `apply_lens(lens, section, config)`. **Subsumes** prior T-Complexity-Contract-Compile-Error + T-User-Authored-Cost-Basis-Discipline as configurations of one mechanism. Substrate carriers (per design doc §2): **two separate top-level carriers** — `EnforcedApplication` (lens, enforcement, section, budget, severity, span) and `IntrospectApplication` (lens, section, span; no Budget axis). NOT a sum wrapping the two — v3 `.dag` substrate cannot currently express per-variant generic parameters; "SectionedLensApplication" is a collective noun for both carriers, not a sum-type declaration. Plus `SectionRef` (DeclarationScope/NodeScope disjoint sum) + `LensEnforcement` projection carrier (per-lens, e.g., complexity → AsymptoticClass projection) + `DiagnosticSeverity`. `CompileError | Warning | Silent` original user framing resolved to fail-closed-compatible binary per design doc §3 + INVARIANTS C-8. Demonstrations: complexity-contract-compile-error + CRDT cost basis + memory-peak cost basis + opt-in cross-iteration parallelism (4 worked examples; orthogonal axes per Director ratification). **Default policy for complexity contracts**: user-driven (per design doc §3.2 + §8.3 resolution at e9d67113e). Unannotated functions get synthesized `Introspect`-only applications — no implicit baseline, no inferred Enforce. Enforcement requires explicit user authoring of `apply_lens(complexity, fn, Enforce { ... })`. The original "opt-out" framing is reframed: the user can opt out (no Enforce or explicit Introspect), and compile errors fire when the user opts IN with a budget the function exceeds. `ComplexityBudgetWaiver` retains its purpose for accepting known violations of explicit user contracts (NOT an annotation per `feedback_no_annotations`). Substrate + Verification cross-program; L-XL sized. **Closure gates**: `lens_application_carrier_landed`, `section_ref_substrate_landed`, `lens_enforcement_carrier_landed` (per-lens `LensEnforcement` projection + violation-relation declarations co-located with each lens), `enforce_violation_routing_landed`, `complexity_violation_compile_error_demonstrated`, `crdt_cost_basis_demonstrated`, `memory_peak_cost_basis_demonstrated`, `opt_in_iteration_parallelism_via_lens_application_demonstrated`. Depends on T-Lens-Behavioral-Parity (lenses must be COMPLETE first). +16. **T-Lens-Application-Surface (NEW 2026-05-02; design doc landed 2026-05-02 [`docs/design-lens-application-surface.md`](design-lens-application-surface.md))** — first-class authoring surface for applying lenses to arbitrary `.dag` sections (function / module / expression / declaration scope). Per user reframe: lens application is a `.dag` declaration with configurable behavior — `apply_lens(lens, section, config)`. **Subsumes** prior T-Complexity-Contract-Compile-Error + T-User-Authored-Cost-Basis-Discipline as configurations of one mechanism. Substrate carriers (per design doc §2): **two separate top-level carriers** — `EnforcedApplication` (lens, enforcement, section, budget, severity, span) and `IntrospectApplication` (lens, section, span; no Budget axis). NOT a sum wrapping the two — v3 `.dag` substrate cannot currently express per-variant generic parameters; "SectionedLensApplication" is a collective noun for both carriers, not a sum-type declaration. Plus `SectionRef` (DeclarationScope/NodeScope disjoint sum) + `LensEnforcement` projection carrier (per-lens, e.g., complexity → AsymptoticClass projection) + `DiagnosticSeverity`. `CompileError | Warning | Silent` original user framing resolved to fail-closed-compatible binary per design doc §3 + INVARIANTS C-8. Demonstrations: complexity-contract-compile-error + CRDT cost basis + memory-peak cost basis (**R3**) + opt-in cross-iteration parallelism (**gate #95 — R4-carved C1** with parallelism lens per `r4-carve-out-routing.md`). **Default policy for complexity contracts**: user-driven (per design doc §3.2 + §8.3 resolution at e9d67113e). Unannotated functions get synthesized `Introspect`-only applications — no implicit baseline, no inferred Enforce. Enforcement requires explicit user authoring of `apply_lens(complexity, fn, Enforce { ... })`. The original "opt-out" framing is reframed: the user can opt out (no Enforce or explicit Introspect), and compile errors fire when the user opts IN with a budget the function exceeds. `ComplexityBudgetWaiver` retains its purpose for accepting known violations of explicit user contracts (NOT an annotation per `feedback_no_annotations`). Substrate + Verification cross-program; L-XL sized. **Closure gates**: `lens_application_carrier_landed`, `section_ref_substrate_landed`, `lens_enforcement_carrier_landed` (per-lens `LensEnforcement` projection + violation-relation declarations co-located with each lens), `enforce_violation_routing_landed`, `complexity_violation_compile_error_demonstrated`, `crdt_cost_basis_demonstrated`, `memory_peak_cost_basis_demonstrated`, `opt_in_iteration_parallelism_via_lens_application_demonstrated` (**R4 C1 — see §"Acceptance" bullet**). **R3 cascade** for substrate **88–91** + demos **92–94:** **complexity+cost** lenses BEHAVIORALLY COMPLETE + register **C3** (option **(b)**). **Full** design §7 four-lens cascade applies to **#95** on **R4** horizon (**INVARIANTS** §P2). 17. **T-Workflow-As-Data (NEW 2026-05-04; per Director ratification at [gunbc#828 inbox-4374342708](https://github.com/gunb-ai/gunbc/issues/828))** — substrate work for modeling workflows as `.dag` data, including the **Shared External Attachment Pattern** (`WorkflowObservationAnchor` + observation/measurement carriers + report-not-scalar output distinguishing `Observed | Missing | Ambiguous | Stale`) per Substrate Mgr design stance at [gunbc#1130 comment-4374109666](https://github.com/gunb-ai/gunbc/issues/1130#issuecomment-4374109666). **First instance**: timing-lens substrate (`Lens` parallel to existing structural-static `Lens` instances; observation-driven lens-shape class). **Substrate carriers**: `TimingMeasurement` + `TimingObservationSet` + `WorkflowObservationAnchor` (factored separately from timing as reusable external-data attachment primitive; serves coverage / logs / failures / artifacts beyond just timing) + `TimingBudget`. **Workflow grammar**: at least one workflow modeled as `.dag` data (CI workflow recommended as demonstration target). **Bidirectional case** (CI YAML emission + ingestion): coordinates with `gunb-ai/gunbc#1586` thread anchor 7 (workflow-timing as bidirectional architecture concern). Substrate Mgr ownership; M-L sized; absorbs into Substrate Mgr continuation per `r3-structure.md:187` standing protocol. **Closure gates**: `workflow_substrate_carriers_landed`, `timing_lens_carrier_landed` (per Substrate Mgr STOP+PING design receipt for `docs/design-timing-lens.md`), `ci_workflow_modeled_as_dag`, `shared_external_attachment_pattern_documented`. Depends on T-Lens-Behavioral-Parity COMPLETE (for lens consumption); R2-Evaluator (for runtime). 18. **T-Lens-Self-Application (NEW 2026-05-04; per Director ratification at [gunbc#828 inbox-4374342708](https://github.com/gunb-ai/gunbc/issues/828))** — demonstration work: gunbc applies its own lenses (cost / complexity / parallelism / timing) to gunbc's own build/CI workflow. Operationalizes the **recursive-flex thesis claim**: *"the compiler that compiles gunbc programs validates the workflow that produces gunbc itself."* Concrete first instance: timing-lens applied to CI workflow producing `DimensionReport`; either emit-back-to-CI-YAML (bidirectional case via T-Workflow-As-Data) OR direct execution. <1 min CI target as informational SLO; **not a closure gate** (per Director ratification — performance metric, not structural commitment). Verification Mgr ownership; M-L sized. **Closure gates**: `lens_self_application_demonstrated` (gunbc lenses applied to gunbc's own build/CI workflow producing `DimensionReport`), `apply_lens_self_application_demonstrated` (`apply_lens(timing, ci_workflow, Enforce { budget })` enforced via existing T-Lens-Application-Surface carrier), `recursive_flex_demonstration_landed` (narrative-load-bearing claim cashes — "gunbc validates the workflows that produce gunbc"). Depends on T-Workflow-As-Data; T-Lens-Application-Surface; T-Lens-Behavioral-Parity COMPLETE; R2-Evaluator. @@ -158,7 +158,7 @@ L6 (`l6_structural_form_coverage`) was moved out of this lane during the engine- - `complexity_violation_compile_error_demonstrated` — first worked example: `apply_lens(complexity, fn, Enforce { ... })` fires compile error when budget exceeded - `crdt_cost_basis_demonstrated` — second worked example: CRDT cost basis applied via `apply_lens` - `memory_peak_cost_basis_demonstrated` — third worked example: memory-peak cost basis - - `opt_in_iteration_parallelism_via_lens_application_demonstrated` — fourth worked example: opt-in cross-iteration parallelism via `Lens` + - `opt_in_iteration_parallelism_via_lens_application_demonstrated` — fourth worked example (design §4.4): opt-in cross-iteration parallelism via `Lens` — **CARVED to R4 (C1)** per `docs/r4-carve-out-routing.md` **with** `parallelism_lens_behaviorally_complete`; **Pass requires parallelism lens BEHAVIORALLY COMPLETE** (design §7 / §9 substantive-semantics cascade). **Not** an R3 thesis-close obligation alongside option **(b)** T-LBP narrowing (**INVARIANTS** §P2). - **T-Workflow-As-Data** (NEW 2026-05-04; observation-driven lens-shape class). - `workflow_substrate_carriers_landed` — workflow grammar in `.dag` (`std.workflow` carriers); supports CI / build / internal-compiler workflows uniformly without per-shape special-casing @@ -184,7 +184,7 @@ L6 (`l6_structural_form_coverage`) was moved out of this lane during the engine- - `cost_lens_demonstration` — cost lens reads representative target program and composes algebra+realization cost end-to-end - `v3_self_host_demonstration` — bootstrap path through PB-Runtime trampoline executes end-to-end; v3-only self-host pipeline runs without v2 fallback (per `docs/r3-program-plan.md` §1.6 + Director poke-hole 2026-05-06 finding 4.1 + openai-pro 2026-05-06 finding 4 — gate name aligned across both docs; reframed from prior `v2_retirement_demonstration` to direct positive-statement form) - `e_p_producer_demonstration` — representative call site produces full descent evidence at runtime - - `lens_behavioral_parity_demonstration` — each lens (complexity / cost / parallelism / effect_enumeration) demonstrates on representative input + matches **frozen v2-oracle cementing-test snapshot** (snapshot captured pre-v2-retirement; demo at R3 close consumes the frozen receipt, NOT a live v2 oracle — preserves `v2_oracle_no_remaining_test_consumers` gate per openai-pro 2026-05-06 finding 5 — v2-oracle conflict resolved) + - `lens_behavioral_parity_demonstration` — **R3 obligation:** **complexity + cost** lenses demonstrate on representative input + match **frozen v2-oracle cementing-test snapshot** (snapshot captured pre-v2-retirement; demo at R3 close consumes the frozen receipt, NOT a live v2 oracle — preserves `v2_oracle_no_remaining_test_consumers` gate per openai-pro 2026-05-06 finding 5 — v2-oracle conflict resolved). **Parallelism + effect_enumeration** demos are **R4-carved** per `docs/r4-carve-out-routing.md` C1+C2 — same frozen-receipt discipline when executed in R4; **not** load-bearing for R3 lane closure. - `tests_as_data_demonstration` — at least one Rust test ports to `.dag` TestClaim and executes via Evaluator - **PR-authoring-discipline gate** (NEW 2026-05-06; per Brian directive at [gunbc#846](https://github.com/gunb-ai/gunbc/issues/846) Director poke-hole finding 3.2; per [`docs/r3-program-plan.md`](r3-program-plan.md) §7). - `pr_anticipation_discipline_ci_active` — CI is verifiably enforcing the §7 PR-authoring contract (per-PR debt-receipt + ratchet-only-down + anticipation discipline); fires when `scripts/check-pr-sg0-net-shrink-discipline.sh` is in CI workflow + self-test passes. R3 Debt-Paydown owner. @@ -206,9 +206,9 @@ L6 (`l6_structural_form_coverage`) was moved out of this lane during the engine- | **T-V2-Retirement** (NEW 2026-04-30) | S-M | **PB Manager (post-R2 continuation)** | v2 retirement is largely a *consequence* of T-FixedPoint + T-LensProducer-Retirement closing; pulling it into R3 is structurally cheap; the post-R3 framing was coordination convenience, not technical blocker. **Scope:** ~79 `.rs` files + ~32 `.dag` files in `src/v2/`; ~13 v2-using test files; legacy emit chain (`rust_method_template_contracts.dag` header note); dual `verification.dag` convergence (per `design-test-infra.md:14`). **Gates:** `v2_oracle_no_remaining_test_consumers` (no test references `src/v2/`); `v2_directory_deleted` (workspace member removed; bootstrap routes through PB-Runtime trampoline only). Rationale: user directive 2026-04-30 — *"nothing can be deferred past R3."* | T-FixedPoint + T-LensProducer-Retirement | | **T-Free-Consequences-Demonstration** (NEW 2026-04-30) | S-M | **Verification Manager** | Operationalizes thesis "free consequences" framing with structural test-claim suite. Per user directive 2026-04-30 — *"what guarantees does the compiler ACTUALLY provide - i expect a small doc/testcases."* **Deliverables:** (1) `docs/design-free-consequences.md` per-consequence guarantee analysis grounded in 5 substrate behaviors + Lens framework. (2) **TestClaim suite (10 gates):** auto-parallelism × 3 + auto-loop-parallelism × 3 + auto-memoization × 2 + cross-target-optimization × 2. **Loop-iteration parallelism design call (Director-ratified 2026-04-30):** sequential default + opt-in via `Lens` (zero-heuristic; same shape as `Lens`); aligns with `feedback_lenses_not_passes`. | R2-Evaluator (witness construction); R2-T-Substrate-Lens-Primitive (`Lens` shape); T-CostLens-Composition (cost-related claims) | | **T-E-P-Producer-Broadening** (NEW 2026-05-02) | M-L | **Substrate Manager (post-R2 continuation)** | Foundational. Broaden per-call `DescentEvidence` / `CallPattern` / `SubValueRelation` producer coverage from current first slice (recursive self-call + arithmetic-descent only) to full `ExprCall.descent_evidence` parity at live call sites. **Gates:** `e_p_per_call_descent_evidence_full_coverage`, `e_p_call_pattern_lookup_authoritative`, `e_p_sub_value_relation_per_call_landed`. Per Director ratification 2026-05-02 ([gunbc#828 comment 4362742638](https://github.com/gunb-ai/gunbc/issues/828#issuecomment-4362742638)). | R2 substrate carriers (already landed) + existing E-T/E-C/E-I vocabulary | -| **T-Lens-Behavioral-Parity** (NEW 2026-05-02) | L-XL | **Substrate Manager + Verification Manager (cross-program)** | Bring complexity / cost / parallelism / effect_enumeration lenses from PROXY/STUB/PARTIAL to BEHAVIORALLY COMPLETE per `docs/v3-lens-capability-register.md`. 4 sub-slices (parallel-dispatchable post-T-E-P-Producer-Broadening): (1) **complexity** — symbolic CostExpr full algebra (Sum/Mul/Log/Const) consumed by lens; work/span dimension split; asymptotic classification; cementing test against v2 oracle. (2) **cost** — same producer foundation as complexity; `SizeVar` value semantics; `Dimension` wiring; cementing test. (3) **parallelism** — Stage 2e walk port from `src/v3/compiler/src/workflow_parallelism.rs` to `.dag`; rewire via `lane2_workflow_at` / `std.effects` (idempotency closure template). (4) **effect_enumeration** — resource-threading migration; ambient metadata removal; caller-side effect-set pinning; full `OperationEffect` retirement. **Gates:** `complexity_lens_behaviorally_complete`, `cost_lens_behaviorally_complete`, `parallelism_lens_behaviorally_complete`, `effect_enumeration_lens_behaviorally_complete`, `lens_capability_register_zero_proxy_zero_stub`. Per user directive 2026-05-02. | T-E-P-Producer-Broadening (foundational); R2-Evaluator (lens runtime execution); R2-T-Substrate-Lens-Primitive (Lens shape) | +| **T-Lens-Behavioral-Parity** (NEW 2026-05-02) | L-XL | **Substrate Manager + Verification Manager (cross-program)** | **R3 lane scope (option (b) RATIFIED 2026-05-06):** **complexity** + **cost** lenses to BEHAVIORALLY COMPLETE per `docs/v3-lens-capability-register.md`. **Parallelism** + **effect_enumeration** behavioral-complete obligations are **R4-carved** per `docs/r4-carve-out-routing.md` C1+C2 (substrate continuation — **not** R3 closure). **R3 sub-slices:** (1) **complexity** — symbolic CostExpr full algebra consumed by lens; work/span dimension split; asymptotic classification; cementing test vs frozen v2-oracle snapshot. (2) **cost** — same producer foundation as complexity; `SizeVar` value semantics; `Dimension` wiring; cementing test. **Gate IDs / carve authority:** §"Acceptance" T-Lens-Behavioral-Parity — `complexity_lens_behaviorally_complete`, `cost_lens_behaviorally_complete`, `parallelism_lens_behaviorally_complete` (**carved R4**), `effect_enumeration_lens_behaviorally_complete` (**carved R4**), `lens_capability_register_zero_proxy_zero_stub` (**narrowed — complexity+cost only**, C3). | T-E-P-Producer-Broadening (foundational); R2-Evaluator (lens runtime execution); R2-T-Substrate-Lens-Primitive (Lens shape) | | **T-Tests-As-Data-Completeness** (NEW 2026-05-02) | L | **Verification Manager** | Close Category E test/verification surface gaps per user directive: (1) every Rust test ports to `.dag` TestClaim or generated target-language test code (thesis facet 3 — *"tests are data"* — full coverage); (2) property-based testing surface (`ForAll` / `Exists` quantifiers + `ProgramGenerator` substrate carrier; substrate-introduction); (3) cementing test discipline for `.dag` lenses (per-lens v2 oracle equivalence on same source). **Gates:** `every_rust_test_ports_to_dag_or_generated`, `forall_exists_quantifier_substrate_landed`, `program_generator_carrier_landed`, `lens_cementing_test_discipline_complete`. | R2-Evaluator (test execution runtime); existing TestClaim infrastructure (DB-15 R2) | -| **T-Lens-Application-Surface** (NEW 2026-05-02; design doc landed 2026-05-02 [`docs/design-lens-application-surface.md`](design-lens-application-surface.md)) | L-XL | **Substrate Manager + Verification Manager (cross-program)** | First-class authoring surface for applying lenses to arbitrary `.dag` sections (function / module / expression / declaration scope). Per user reframe 2026-05-02: lens application is a `.dag` declaration with configurable behavior — `apply_lens(lens, section, config)`. **Subsumes** prior T-Complexity-Contract-Compile-Error + T-User-Authored-Cost-Basis-Discipline as configurations of one mechanism. **Substrate carriers** (per design doc §2): **two separate top-level carriers** — `EnforcedApplication` and `IntrospectApplication`. NOT a sum wrapping the two — v3 `.dag` substrate cannot currently express per-variant generic parameters; "SectionedLensApplication" is a collective noun for both carriers. Plus `SectionRef` (DeclarationScope/NodeScope disjoint sum) + `LensEnforcement` projection carrier + `DiagnosticSeverity`. `CompileError | Warning | Silent` original user framing resolved to fail-closed-compatible binary per design doc §3 + INVARIANTS C-8. **Default policy for complexity contracts**: user-driven (per design doc §3.2 + §8.3 resolution at e9d67113e). Unannotated functions get synthesized `Introspect`-only applications — no implicit baseline, no inferred Enforce. Enforcement requires explicit user authoring of `apply_lens(complexity, fn, Enforce { ... })`. The original "opt-out" framing is reframed: the user can opt out (no Enforce or explicit Introspect), and compile errors fire when the user opts IN with a budget the function exceeds. `ComplexityBudgetWaiver` retains its purpose for accepting known violations of explicit user contracts (NOT an annotation per `feedback_no_annotations`). Demonstrations: complexity-contract-compile-error + CRDT cost basis + memory-peak cost basis + opt-in cross-iteration parallelism (4 worked examples; orthogonal axes per Director ratification; design doc §4). **Gates:** `lens_application_carrier_landed`, `section_ref_substrate_landed`, `lens_enforcement_carrier_landed` (per-lens `LensEnforcement` projection + violation-relation declarations), `enforce_violation_routing_landed`, `complexity_violation_compile_error_demonstrated`, `crdt_cost_basis_demonstrated`, `memory_peak_cost_basis_demonstrated`, `opt_in_iteration_parallelism_via_lens_application_demonstrated`. **Design doc §8 resolves all 5 originally-open questions** (module-scope semantics / multiple-applications / default-budget-inference / waiver lifecycle / cross-section composition); no Director ratification required before substrate authoring — only standard cascade-gate (T-Lens-Behavioral-Parity COMPLETE) + R2-Evaluator landed. | T-Lens-Behavioral-Parity (lenses must be COMPLETE first); R2-Evaluator | +| **T-Lens-Application-Surface** (NEW 2026-05-02; design doc landed 2026-05-02 [`docs/design-lens-application-surface.md`](design-lens-application-surface.md)) | L-XL | **Substrate Manager + Verification Manager (cross-program)** | First-class authoring surface for applying lenses to arbitrary `.dag` sections (function / module / expression / declaration scope). Per user reframe 2026-05-02: lens application is a `.dag` declaration with configurable behavior — `apply_lens(lens, section, config)`. **Subsumes** prior T-Complexity-Contract-Compile-Error + T-User-Authored-Cost-Basis-Discipline as configurations of one mechanism. **Substrate carriers** (per design doc §2): **two separate top-level carriers** — `EnforcedApplication` and `IntrospectApplication`. NOT a sum wrapping the two — v3 `.dag` substrate cannot currently express per-variant generic parameters; "SectionedLensApplication" is a collective noun for both carriers. Plus `SectionRef` (DeclarationScope/NodeScope disjoint sum) + `LensEnforcement` projection carrier + `DiagnosticSeverity`. `CompileError | Warning | Silent` original user framing resolved to fail-closed-compatible binary per design doc §3 + INVARIANTS C-8. **Default policy for complexity contracts**: user-driven (per design doc §3.2 + §8.3 resolution at e9d67113e). Unannotated functions get synthesized `Introspect`-only applications — no implicit baseline, no inferred Enforce. Enforcement requires explicit user authoring of `apply_lens(complexity, fn, Enforce { ... })`. The original "opt-out" framing is reframed: the user can opt out (no Enforce or explicit Introspect), and compile errors fire when the user opts IN with a budget the function exceeds. `ComplexityBudgetWaiver` retains its purpose for accepting known violations of explicit user contracts (NOT an annotation per `feedback_no_annotations`). Demonstrations: complexity-contract-compile-error + CRDT cost basis + memory-peak cost basis + opt-in cross-iteration parallelism (4 worked examples; orthogonal axes per Director ratification; design doc §4). **Gates:** `lens_application_carrier_landed`, `section_ref_substrate_landed`, `lens_enforcement_carrier_landed` (per-lens `LensEnforcement` projection + violation-relation declarations), `enforce_violation_routing_landed`, `complexity_violation_compile_error_demonstrated`, `crdt_cost_basis_demonstrated`, `memory_peak_cost_basis_demonstrated`, `opt_in_iteration_parallelism_via_lens_application_demonstrated`. **Design doc §8 resolves all 5 originally-open questions** (module-scope semantics / multiple-applications / default-budget-inference / waiver lifecycle / cross-section composition); no Director ratification required before substrate authoring — **R3** cascade per `design-lens-application-surface.md` §7 reconciliation: **complexity+cost** T-LBP COMPLETE + register **C3** before substrate **88–91** + demos **92–94**; **gate #95** is **R4 (C1)** with `parallelism_lens_behaviorally_complete`. | **R3:** T-Lens-Behavioral-Parity (**complexity+cost** + **C3**); **R4:** parallelism parity before **#95**; R2-Evaluator | | **T-Workflow-As-Data** (NEW 2026-05-04; per Director ratification at [gunbc#828 inbox-4374342708](https://github.com/gunb-ai/gunbc/issues/828); Substrate Mgr design stance at [gunbc#1130 comment-4374109666](https://github.com/gunb-ai/gunbc/issues/1130#issuecomment-4374109666)) | M-L | **Substrate Manager (post-R2 continuation)** | Substrate work for modeling workflows as `.dag` data; introduces observation-driven lens-shape class (parallel to existing structural-static `Lens` instances). **First instance**: timing-lens substrate (`Lens`). **Substrate carriers**: `TimingMeasurement` + `TimingObservationSet` + `WorkflowObservationAnchor` (factored separately as reusable external-data attachment primitive — Shared External Attachment Pattern with six invariants per Substrate Mgr design stance) + `TimingBudget`. **Workflow grammar**: at least one workflow modeled as `.dag` data (CI workflow recommended). **Bidirectional case** coordinates with `gunb-ai/gunbc#1586` thread anchor 7 (workflow-timing as bidirectional architecture concern). **Gates:** `workflow_substrate_carriers_landed`, `timing_lens_carrier_landed` (per Substrate Mgr STOP+PING design receipt for `docs/design-timing-lens.md`), `shared_external_attachment_pattern_documented`, `ci_workflow_modeled_as_dag`. Substrate Mgr's design-doc-first cadence per `r3-structure.md:187` substrate-completion protocol — design receipt lands first, carrier authoring follows sign-off. | T-Lens-Behavioral-Parity COMPLETE (timing-lens uses lens framework with parity-COMPLETE consumers); R2-Evaluator | | **T-Lens-Self-Application** (NEW 2026-05-04; per Director ratification at [gunbc#828 inbox-4374342708](https://github.com/gunb-ai/gunbc/issues/828)) | M-L | **Verification Manager** | Demonstration work: gunbc applies its own lenses (cost / complexity / parallelism / timing) to gunbc's own build/CI workflow. Operationalizes recursive-flex thesis claim: *"the compiler that compiles gunbc programs validates the workflow that produces gunbc itself."* Concrete first instance: timing-lens applied to CI workflow producing `DimensionReport`; `apply_lens(timing, ci_workflow, Enforce { budget: max_ns })` enforced via existing `EnforcedApplication` carrier. <1 min CI target as informational SLO; **NOT a closure gate** (per Director ratification 2026-05-04 — performance metric, not structural commitment). **Gates:** `lens_self_application_demonstrated`, `apply_lens_self_application_demonstrated`, `recursive_flex_demonstration_landed`. | T-Workflow-As-Data; T-Lens-Application-Surface; T-Lens-Behavioral-Parity COMPLETE; R2-Evaluator |