R3 Verification

docs/briefs/r3-v-tc1-eta-equivalence-deeper-analysis.md

@@ -1,6 +1,20 @@
 # R3 TC1 Eta-Equivalence Deeper Structural Verification Analysis
 
-**Status:** PROPOSAL / research-only. TC1 fixture remains as-is; this brief explores the strict-fire extension surface only. No substrate, runner, or fixture changes are proposed here.
+**Status:** **DESIGN** (2026-05-06). Verification Mgr engineering choice among Pattern-A
+first-slice paths; **not** yet **ACCEPTED** (Director countersignature still required per
+`docs/r3-program-plan.md` §10.3 **Q-PAFS** and Brian directive: PROPOSAL → DESIGN →
+ACCEPTED).
+
+**Lifecycle**
+
+| Stage | Meaning |
+| --- | --- |
+| PROPOSAL | Exploratory surface map only (superseded by this revision). |
+| **DESIGN** (here) | Chooses a concrete first-slice shape, defers alternatives, states runtime prereqs and scope deltas. |
+| ACCEPTED | Director/Brian countersign; authorizes implementation dispatch (V1 TC1 executable slice + Evaluator **E6-G1.a** lens-fold first slice in lockstep). |
+
+TC1 deferred fixture remains **as-is** until ACCEPTED + routed implementation; this brief
+still does **not** authorize substrate, runner, or fixture edits by itself.
 
 **Owning manager:** R3 Verification Manager, absorbed formal-grounding responsibility.
 
@@ -59,7 +73,84 @@ Potential substrate paths, for Director/Substrate ratification:
 - generalize `LensOutputEquals` into a binary structural equality predicate over two lens applications;
 - model eta-equivalence as a substrate relation over reflected functions, then reuse a generic `DifferentialEquals`-style output comparison.
 
-This analysis does not choose among those paths.
+**DESIGN resolution (which slice first):** concrete choice lives in **§DESIGN — Q-PAFS
+first executable slice** below. Predicate/carrier *shape* inside strict-fire remains
+Substrate-owned STOP+PING until ACCEPTED routing.
+
+## DESIGN — Q-PAFS first executable slice (Pattern-A / TC1)
+
+This section satisfies the Verification Mgr obligation called out in
+`r3-program-plan.md` §10.3 **Q-PAFS**: PM default ("TC1 first") is not engineering
+sign-off; **DESIGN** records the explicit tradeoff and recommended path.
+
+### Path A — TC1 **static representative** via **E6-G1.a** (**recommended**)
+
+**Shape:** Ratify a **finite**, Director-visible **representative set** (not universal
+quantification over all `Lens<C>` for the first executable slice): fixed eta pair of
+programs (`f` and `lambda x.apply(f, [x])`) plus a named list of lens instances (or
+substrate-approved typed lens handles) that the evaluator can fold with **existing**
+`fold_lens<C>` / `DimensionReport<C>` machinery.
+
+**Runtime prereqs (Evaluator / E6, aligned with Evaluator Mgr F4 + program-plan
+Q-EVAL-Lens-Fold-First-Slice / Q-Pattern-A-First-Slice-Subscope):**
+
+- **E6-G1.a** static lens fold: two **structurally named** programs in `.dag` (or
+  equivalent declared scope) each produce a **typed** `DimensionReport<C>` through the
+  same evaluator-owned fold authority—no X1.b generic transform-dispatch requirement for
+  this slice.
+- **T-Substrate-Lens-Primitive** + lens producer retirement progress assumed per existing
+  lane dependencies: TC1 strict-fire still does **not** rest on widening
+  `SubstrateResearchDeferredClaim` (see **Carrier Scope Analysis**).
+- **Pattern-A consumer envelope** unchanged: `BinaryDimensionReportEquals` over the two
+  reports once producers exist (`docs/briefs/r3-v-pattern-a-coverage-rollup.md`).
+
+**Substrate vs evaluator scope:** Substrate names the **representative lens set** and
+any eta-pair **declaration refs**; Evaluator proves it can **execute** the fold twice and
+lift reports without fixture-local producer identity or string bypass (Evaluator #1131
+safe contract).
+
+**Engineering justification:** Smallest executable surface that honors the PM default
+(TC1 before TC2/TC3/RustDagIsomorphism ordering) **without** blocking on **E6-G1.b** /
+**X1.b** S1/S3 generic dispatch. Unblocks **V1** “TC1 first slice” and **Evaluator E3**
+(E6-G1.a) on the **same** Director **ACCEPTED** gate, per PM coordination note.
+
+### Path B — TC1 **generic** via **E6-G1.b / X1.b** (**defer**)
+
+**Shape:** Universal or parametric coverage over `Lens<C>` / programs requiring **X1.b**
+transform dispatch and **G1.b** generic lens-fold substrate not required for Path A.
+
+**Runtime prereqs:** Substrate **X1.b** S1/S3 + generic dispatch path; substantially
+larger than G1.a; sequenced **after** Path A strict-fire is green or explicitly reprioritized
+by Director.
+
+**Scope delta vs A:** Shifts primary risk from “representative selection” to “generic
+dispatch + substrate carrier completion.” **Not** chosen for first executable slice.
+
+### Path C — **RustDagIsomorphism** first (**alternate, not recommended for Q-PAFS default**)
+
+**Shape:** Prioritize shape-report producers for `DimensionReport<Dag>` before TC1 eta
+pair (`docs/briefs/r3-v-pattern-a-coverage-rollup.md` §4 row **RustDagIsomorphism**).
+
+**Runtime prereqs:** Still requires generic typed `DimensionReport<C>` production and two
+structural shape reports; **fewer eta-specific** obligations than TC1.
+
+**Why not for Q-PAFS default:** Conflicts with stated PM/Brian **Pattern-A ordering**
+(TC1 first) unless Director explicitly reorders. Remains a **credible fallback** if Director
+rules TC1 eta unblockers dominate calendar—would require explicit scope edit, not silent
+Verification drift.
+
+### DESIGN verdict
+
+| Question | Decision |
+| --- | --- |
+| First Pattern-A executable slice for TC1? | **Path A** — static representative **E6-G1.a**. |
+| Generic TC1 (Path B)? | **Deferred** after Path A closes or Director reprioritizes. |
+| RustDagIsomorphism before TC1? | **Not** under Q-PAFS default; **Path C** only with Director reorder. |
+| Universal vs representative for first fire? | **Representative finite set** for slice one; universal quantification is a **later** ratchet question (see Open Questions). |
+
+**Surface for Director countersign (ACCEPTED):** Path A as written + explicit acknowledgment
+that PM default and **DESIGN** engineering choice align; any deviation (e.g., Path C first)
+is Director-owned scope calibration.
 
 ## Lens-Framework Anchors
 
@@ -96,13 +187,17 @@ Shared with TC3:
 
 ## Open Questions
 
-- Is TC1 universal over all `Lens<C>` instances, or strict-fire over the migrated built-in lens set plus user-authored lens fixture?
+- **Representative set contents:** which built-in / staged lens instances and which
+  single eta pair land in slice-one (Substrate + Director visibility)—DESIGN defers
+  enumeration to implementation routing post-ACCEPTED.
+- **Universal quantification:** remains **out of scope** for first executable slice (Path
+  A); revisit after Path A strict-fire or if Director mandates broader coverage.
 - Does eta-equivalence live as a function/program relation in substrate, or only inside a verification predicate?
 - Should equality include witness-list ordering, or compare `DimensionReport<C>` modulo semantically irrelevant witness ordering?
 - Does lens producer retirement provide enough reflection authority to construct eta-expanded forms structurally, or is a lambda-calculus grounding carrier still needed?
 
 ## Non-Goals
 
-- No fixture activation today.
+- No fixture activation or runner widening until **ACCEPTED** + implementation dispatch.
 - No runner validity widening for `SubstrateResearchDeferredClaim`.
-- No edits to `r2-closure-ledger.md`, `r3-v-formal-grounding-tc-bundle.md`, `r3-verification-manager.md`, or `r3-pb-t-fixedpoint-worker.md`.
+- No edits to `r2-closure-ledger.md`, `r3-v-formal-grounding-tc-bundle.md`, `r3-verification-manager.md`, or `r3-pb-t-fixedpoint-worker.md` from this DESIGN revision alone.

docs/r3-program-plan.md

@@ -950,7 +950,7 @@ Substrate canvas + plan-poke-hole both folded in. Key absorptions:
 
 | ID | Question | PM recommendation (applied as default) | Status |
 |---|---|---|---|
-| Q-PAFS | Which Pattern-A (DimensionReport-typed family) first executable slice (TC1 vs RustDagIsomorphism vs other) | **TC1 η-equivalence first as PM/Brian convenience default; needs Director countersignature** — `r3-v-tc1-eta-equivalence-deeper-analysis.md` is `Status: PROPOSAL / research-only` and explicitly does not choose among paths. PM-default ≠ Verification-Mgr engineering sign-off. | **PENDING DIRECTOR COUNTERSIGNATURE** (per Verification Mgr poke-hole 2026-05-06; PM convenience-default applies until then) |
+| Q-PAFS | Which Pattern-A (DimensionReport-typed family) first executable slice (TC1 vs RustDagIsomorphism vs other) | **TC1 first slice = static representative via E6-G1.a (Path A)** — `docs/briefs/r3-v-tc1-eta-equivalence-deeper-analysis.md` advanced to **DESIGN** (2026-05-06): Path B (TC1 generic G1.b / X1.b) **deferred**; Path C (RustDagIsomorphism before TC1) **not** under Q-PAFS default (Director reorder only). **ACCEPTED** still requires Director countersignature (Brian directive: PROPOSAL → DESIGN → ACCEPTED). PM default and Verification Mgr engineering choice **align on Path A**. | **PENDING DIRECTOR COUNTERSIGNATURE** for **ACCEPTED** (DESIGN landed 2026-05-06) |
 | Q-NYI-Accounting | NYI claim coverage/completeness accounting | Mark NYI incomplete in aggregation reporting; ratchet to executable per evaluator-slice landing | RATIFIED-by-default |
 | Q-Std-Carrier-Phasing | Rust std-carrier phasing (Option/Cardinal/HigherOrderMethodSpec/allocator-hasher) | Phase 1 = default-only/default-instance; later phases as separate Substrate slices post-Phase-1 | RATIFIED-by-default |
 | Q-Drift-Reconcile | Drift items routing (#1638, #1499, declaration_by_name) | Single Debt-Paydown worker reconciles all three → one PR closing rows in ledger + ROADMAP | RATIFIED-by-default |
@@ -960,10 +960,10 @@ Substrate canvas + plan-poke-hole both folded in. Key absorptions:
 | Q-PR-Anticipation-Gate | Add `pr_anticipation_discipline_ci_active` closure gate (CI verifiably enforcing §7 anticipation discipline) | Add to §1 closure-gate set; owner R3 Debt-Paydown Mgr (already routed at #1744 #issuecomment-4383628247); fires when `scripts/check-pr-sg0-net-shrink-discipline.sh` is in CI workflow + self-test passes | RATIFIED-by-default (per Director poke-hole 2026-05-06 finding 3.2) |
 | Q-PR-F | PR-F priority + sequencing (BoundDeclaration consumer + Rust ReferenceModel<T>) | **Bandwidth-aware dispatch** (per Substrate Mgr poke-hole 2026-05-06 Y3 — Substrate's queued workers are saturated): PR-F is 2-axis substantial work. Per Substrate Mgr canvas D: only loyal-wolf + valiant-ant fully idle; proud-lynx/smart-ram/valiant-ibex holding on #1794 cascade. Dispatch worker = loyal-wolf-828 OR valiant-ant-72 (Substrate Mgr selects); brief shape = T-E-P-Producer-Broadening adjacent (per `docs/briefs/r3-t-e-p-producer-broadening-worker.md` precedent); critical-path slot = post-#1782 wait-window close + parallel to T-E-P dispatch (B3). Substrate Mgr authors brief + dispatches. | RATIFIED-by-default-with-bandwidth-routing |
 | Q-Workflow-As-Data-Carriers | Substrate carriers for CI-workflow-as-`.dag`-data Class 4 closure path: `WorkflowTrigger` sum + `WorkflowStep`/`WorkflowMatrix` step-graph + `WorkflowSecret<Name>` binding + `RunnerResource<C>` + `Workflow<Trigger, Steps, Resources>` composing carrier | Substrate Mgr authors carriers as part of T-Workflow-As-Data lane; sequenced post-T-Lens-Behavioral-Parity COMPLETE (per `r3-structure.md` §"Dependency on R2"); folds into existing T-Workflow-As-Data scope without new lane spawn. Required for Class 4 substrate-gap-class closure per §1.4. | OPEN — Substrate Mgr scoping needed (NEW 2026-05-06 from Substrate Mgr poke-hole R3) |
-| Q-Pattern-A-First-Slice-Subscope | Q-PAFS sub-question: TC1 first means **static representative** (E6-G1.a) or **generic** (E6-G1.b/X1.b)? Plan defaulted to TC1 first without specifying which sub-shape. Per Evaluator Mgr F1 + EVAL-3: substantial substrate/evaluator scope difference. | Per `docs/briefs/r3-v-pattern-a-coverage-rollup.md` + Evaluator Mgr canvas: TC1-static-representative via E6-G1.a is achievable with current evaluator + lens-fold infrastructure; TC1-generic requires X1.b S1/S3 + G1.b. PM-recommended: **TC1-static-representative first** (smallest viable slice); generic deferred to subsequent ratchet. | OPEN — Director / Brian ratification needed (NEW 2026-05-06 from Evaluator Mgr F1 + EVAL-3; sub-question of Q-PAFS) |
+| Q-Pattern-A-First-Slice-Subscope | Q-PAFS sub-question: TC1 first means **static representative** (E6-G1.a) or **generic** (E6-G1.b/X1.b)? Plan defaulted to TC1 first without specifying which sub-shape. Per Evaluator Mgr F1 + EVAL-3: substantial substrate/evaluator scope difference. | Per `docs/briefs/r3-v-pattern-a-coverage-rollup.md` + Evaluator Mgr canvas: TC1-static-representative via E6-G1.a is achievable with current evaluator + lens-fold infrastructure; TC1-generic requires X1.b S1/S3 + G1.b. PM-recommended: **TC1-static-representative first** (smallest viable slice); generic deferred to subsequent ratchet. **Verification Mgr DESIGN** (`r3-v-tc1-eta-equivalence-deeper-analysis.md`, 2026-05-06) ratifies **G1.a static representative first**. | **PENDING DIRECTOR COUNTERSIGNATURE** for ACCEPTED (bundles with Q-PAFS / Q-EVAL-Lens-Fold-First-Slice) |
 | Q-EVAL-G0d-Dispatch | E6-G0d constructor runtime execution: authorize evaluator slice for non-Arrow constructor `Callable` using `Value::RecordValue` / `Value::VariantValue` + shared substrate declaration-walk authority | Evaluator Mgr (merry-gull-128) dispatches; Director needed only if shared helper extraction crosses ownership. Brief at `docs/briefs/r3-pr-e6-g0d-constructor-runtime-execution-worker.md` ready. | RATIFIED-by-default — Evaluator Mgr executes (NEW 2026-05-06 from Evaluator Mgr EVAL-1) |
 | Q-EVAL-Descent-Termination-Contract | E5 `LoopBound::Descent` execution: substrate carrier `descent_execution_proof(&Dag, ClusterId, PortId) -> Result<DescentExecutionProof, DescentResidual>` with `Missing \| Unknown \| Incomplete \| NonStrict` fail-closed residuals | Substrate Mgr authors carrier (quick-koi-190 implementation already authorized through quick-crab); Evaluator consume-side ack; sharp-ibex consumer wiring dispatch. | RATIFIED-by-default — Substrate-side already authorized; Evaluator consume-side dependency (NEW 2026-05-06 from Evaluator Mgr EVAL-2) |
-| Q-EVAL-Lens-Fold-First-Slice | Overlaps with Q-Pattern-A-First-Slice-Subscope: E6-G1.a static representative vs G1.b generic for first executable lens/report slice | Same recommendation as Q-Pattern-A-First-Slice-Subscope: **G1.a static-representative first**; G1.b generic deferred. | OPEN — same scope-question as Q-Pattern-A-First-Slice-Subscope (NEW 2026-05-06 from Evaluator Mgr EVAL-3) |
+| Q-EVAL-Lens-Fold-First-Slice | Overlaps with Q-Pattern-A-First-Slice-Subscope: E6-G1.a static representative vs G1.b generic for first executable lens/report slice | Same recommendation as Q-Pattern-A-First-Slice-Subscope: **G1.a static-representative first**; G1.b generic deferred. **Verification Mgr DESIGN** (`r3-v-tc1-eta-equivalence-deeper-analysis.md`, 2026-05-06) locks the same **G1.a** first-slice shape for Evaluator E3 sequencing. | **PENDING DIRECTOR COUNTERSIGNATURE** for ACCEPTED (same gate as Q-PAFS) |
 | Q-Class-6-Substrate-Extension-Lens | 3 ctrl-side substrate proposals (`SchemaPreservation<TableId>` per ctrl#370/#407 LLVM TBAA; `ResourceCap<T>` per ctrl#404/#405 Cloudflare; `TotalResult<E>` per ctrl#404/#405) don't fit Classes 1-5; PM-side routing to Substrate Mgr (#1130) committed per ctrl#408 §3 | PER Brian no-post-R3-deferral discipline: include as Class 6 substrate-gap-class with closure-criterion. Add §4.6 "Class 6 — typed-metadata-preservation / extension-lens slice" with representative gap-test per substrate. Alternative: Director ratification of explicit post-R3-ecosystem-by-design scope-cession. **Director disposition 2026-05-06 at gunbc#828 #issuecomment-4384615320: HOLD pending more context** — needs (i) which proposals are R3-blocking vs nice-to-have; (ii) substrate-author capacity for the 3 carriers; (iii) cross-lane cascade implications. PM surfaces from Research PM with sharper framing before Director ratification. | HOLD pending Research PM sharper framing (Director disposition; NEW 2026-05-06 from Research PM R-1) |
 | Q-Timeline-Risk-Alternates | §6 8-12 week estimate is commitment, not bottoms-up derivation. Missing risk-weighted alternates for: C1-class candidate-gap budget (2-6 weeks/gap) + WEDGE-CORE-CLAIM Part A thesis-edit scope + ~9 demo-gate authoring (1-3 weeks/lane) | Per `feedback_holistic_over_patches`: §9.2 add explicit "+X weeks if {C1-gap surfaces / Tier-4 thesis-edit lands in scope / demo authoring exceeds budget}" branches. R3 close horizon: 2026-08-01 ± 2 weeks PROVISIONAL → range with explicit risk-weighted alternates. | RATIFIED-by-default — PM updates §9.2 with risk-weighted branches in subsequent commit (NEW 2026-05-06 from Research PM R-2) |
 | Q-Plan-vs-Structure-Drift-Discipline | §3 lane status table holds 19 rows replicating r3-structure.md §"Lane structure" data; drift risk if PM updates one but not the other | Per Research PM R-3 recommendation (a): §3 lane status becomes pointer-with-delta to r3-structure.md §"Lane structure" + delta-only annotations (current dispatch + blocker + ETA). Lane name/Mgr/scope columns NOT restated; r3-structure.md retains architectural-decision authority. | RATIFIED-by-default — PM refactors §3 in subsequent commit OR canonical-ledger-landing absorbs (path-(a) decision pending; NEW 2026-05-06 from Research PM R-3) |