From 976a484226617134e8bbf9882072ff11dbd5a665 Mon Sep 17 00:00:00 2001 From: Brian Searls Date: Thu, 30 Apr 2026 12:57:22 -0400 Subject: [PATCH 1/9] WIP: R3 Verification --- .../briefs/r3-v-formal-grounding-tc-bundle.md | 66 +++++++++++ docs/briefs/r3-v-l4-l7-direct-worker.md | 51 +++++++++ docs/briefs/r3-v-l5-corpus-worker.md | 51 +++++++++ docs/briefs/r3-verification-manager.md | 107 ++++++++++++++++++ 4 files changed, 275 insertions(+) create mode 100644 docs/briefs/r3-v-formal-grounding-tc-bundle.md create mode 100644 docs/briefs/r3-v-l4-l7-direct-worker.md create mode 100644 docs/briefs/r3-v-l5-corpus-worker.md create mode 100644 docs/briefs/r3-verification-manager.md diff --git a/docs/briefs/r3-v-formal-grounding-tc-bundle.md b/docs/briefs/r3-v-formal-grounding-tc-bundle.md new file mode 100644 index 00000000000..0d3717e08e5 --- /dev/null +++ b/docs/briefs/r3-v-formal-grounding-tc-bundle.md @@ -0,0 +1,66 @@ +# R3 Lane 3 — T-FormalGrounding-Verification (TC1 / TC2 / TC3 bundle) Worker Brief + +**Status:** PROPOSAL — Lane 3 of R3 Verification Manager. Bundles three formal-grounding TestClaims under one ownership lane per PM R3-absorption mapping. Research-tier work (~3-5 days per TC strengthening per PM Tier C estimate). + +**Parent:** [`docs/briefs/r3-verification-manager.md`](r3-verification-manager.md) — Lane 3 of 3. + +## Scope (this lane) + +Manage the three formal-grounding `TestClaim` author-now-fire-later commitments through their strict-fire activation. Each TC has a different unblock condition; this lane coordinates across them and authors the substrate path for TC3 when its prerequisites land. + +| TC | Claim | Status (2026-04-30 audit) | Strict-fire gate | +|---|---|---|---| +| **TC1** | η-equivalence (substrate-lens research) | **Author-now-fire-later landed** — fixture `src/v3/compiler/tests/fixtures/tc1_substrate_lens_eta_equivalence_deferred.dag` via #1179; uses `SubstrateResearchDeferredClaim` carrier (runner-valid only for this fixture per [`r2-closure-ledger.md`](../r2-closure-ledger.md) L220). | T-Substrate-Lens-Primitive landing + lens producer retirement (per [`r2-closure-ledger.md`](../r2-closure-ledger.md) §216 ratification). | +| **TC2** | Church-Rosser / evaluation-order independence | **Slice-0 hook landed** — fixture `src/v3/compiler/tests/fixtures/tc2_evaluation_order_independence_deferred.dag` (per [`r2-evaluator-manager.md`](r2-evaluator-manager.md) L127); current predicate is deferred (`Compiles`-shaped). | **R3-deferred from R2-Evaluator** — needs ≥2 executable strategies. PR-B.1 lands a single eager strategy per [`r2-pr-b-body-evaluator-eager-baseline.md`](r2-pr-b-body-evaluator-eager-baseline.md) L154; second strategy is R3 residual. Strengthens to strict strategy-output equality over `DimensionReport`. | +| **TC3** | Strong normalization (meta-theorem over well-typed fragment) | **Text-form only** in [`r3-pb-t-fixedpoint-worker.md`](r3-pb-t-fixedpoint-worker.md) L145-215; no fixture. **Substrate-encoding gap** — every existing `TestPredicate` variant is per-program; TC3 is a meta-theorem universally quantified across all well-typed programs. No existing variant carries that quantifier shape (per L171 of that brief). | **Substrate-fact-introduction via [`INVARIANTS.md`](../../INVARIANTS.md) §P1** + B5 audit + T-Substrate-Lens-Primitive (provides the `Lens` shape TC3's evaluation-step witness consumes). Ownership transitions PB→Verification per L181-185 of `r3-pb-t-fixedpoint-worker.md`. | + +## Owned deliverables + +1. **TC strict-fire activation cadence** — when a TC's strict-fire prerequisites land, replace the deferred-claim variant with the strict predicate; preserve fixture path + claim name (stability invariant). +2. **TC3 substrate-fact-introduction (load-bearing)** — when B5 + T-Substrate-Lens-Primitive land, author the substrate path for the meta-theorem quantifier shape per INVARIANTS §P1 procedure. Cross-coordinate with Substrate Manager continuation (the carrier-type shape is substrate-owned per #1078 dispatch lock pattern). PB does not re-author after transition per L181-185 of `r3-pb-t-fixedpoint-worker.md`. +3. **Drift surfacing** — periodic audit (rolled into bridge-ledger audit cadence) that TC fixture paths + carrier shapes remain consistent on main. Surface drift to Director. + +## TC3 substrate-fact-introduction — open design questions (parked) + +These resolve when TC3 dispatch fires. Listed here for handoff continuity: + +- **Quantifier carrier shape** — does TC3 need a new `TestPredicate` variant (e.g., `MetaTheoremOverTypedFragment`), or does it dissolve into a structural fold once T-Substrate-Lens-Primitive provides the evaluation-step witness shape? Per [`r3-pb-t-fixedpoint-worker.md`](r3-pb-t-fixedpoint-worker.md) L171: "no existing variant carries that quantifier shape" — so substrate introduction is the live candidate, dissolution is the hope. +- **Witness construction** — what does an evaluation-step witness look like for "every well-typed program reduces to normal form"? Consumes T-FixedPoint termination semantics + `Lens` shape. +- **Fixture path** — proposed `src/v3/compiler/tests/fixtures/tc3_strong_normalization_deferred.dag` (mirroring TC1/TC2 naming convention). Lock at substrate-introduction PR. + +## Dependencies summary + +| TC | Blocker | Owner | +|---|---|---| +| TC1 | T-Substrate-Lens-Primitive + lens producer retirement | Substrate Manager + PB Manager continuations | +| TC2 | Second executable evaluation strategy | R3 Evaluator residual (post-R2-Evaluator close) | +| TC3 | B5 audit + T-Substrate-Lens-Primitive + substrate-fact-introduction | PB Manager (B5) + Substrate Manager + this lane (introduction authorship) | + +## Cadence + +- **No active worker dispatch** until at least one TC's strict-fire prerequisites land. +- **Audit cadence** — bundled with bridge-ledger audit; refresh status table at each manager-brief PR. +- **TC3 dispatch trigger** — when both B5 and T-Substrate-Lens-Primitive are green, this lane authors a TC3 substrate-introduction worker brief (~3-5 days research-tier per PM Tier C estimate). + +## Explicitly out of scope + +- **TC1 substrate-research authoring** — Substrate Manager continuation owns T-Substrate-Lens-Primitive; this lane only consumes the strengthening signal. +- **TC2 second-strategy implementation** — R3 Evaluator residual (per [`r2-closure-ledger.md`](../r2-closure-ledger.md) Evaluator row); this lane only consumes the strengthening signal. +- **TC3 declaration content** — already authored in [`r3-pb-t-fixedpoint-worker.md`](r3-pb-t-fixedpoint-worker.md) L145-215 (PB-authored declarative shape). This lane authors the substrate path + fixture, NOT the declaration text per L181-185 ownership-transition contract. +- **L4 / L5 / L7 verification claims** — Lanes 1 + 2 of this manager. + +## Acceptance — `.dag` gates (each TC fires independently) + +- `tc1_substrate_lens_eta_equivalence_strict_fire` — TC1 strengthens from `SubstrateResearchDeferredClaim` to strict predicate. +- `tc2_evaluation_order_independence_strict_fire` — TC2 strengthens from `Compiles`-shaped slice-0 to strict strategy-output equality over `DimensionReport` per [`r2-evaluator-manager.md`](r2-evaluator-manager.md) L127. +- `tc3_strong_normalization_substrate_introduced` — TC3 substrate path authored + fixture lands; subsequent strict-fire when T-FixedPoint completes. + +## Cross-refs + +- Parent manager: [`docs/briefs/r3-verification-manager.md`](r3-verification-manager.md) +- TC3 upstream declarative shape (PB-authored, transition contract): [`docs/briefs/r3-pb-t-fixedpoint-worker.md`](r3-pb-t-fixedpoint-worker.md) §"TC3 — Strong-normalization TestClaim" (L145-215; L181-185 ownership transition) +- TC1 fixture authority: [`docs/r2-closure-ledger.md`](../r2-closure-ledger.md) §216 (Director ratification of #1179 direction) +- TC2 slice-0 hook: [`docs/briefs/r2-evaluator-manager.md`](r2-evaluator-manager.md) L127 +- B5 dependency for TC3: [`docs/briefs/r2-release-b5-loop-construction-closure-audit-worker.md`](r2-release-b5-loop-construction-closure-audit-worker.md) +- INVARIANTS substrate-fact-introduction procedure: [`INVARIANTS.md`](../../INVARIANTS.md) §P1 (TC3 introduction path) +- P4 Decidability (TC3 formal home): [`INVARIANTS.md`](../../INVARIANTS.md) §P4 diff --git a/docs/briefs/r3-v-l4-l7-direct-worker.md b/docs/briefs/r3-v-l4-l7-direct-worker.md new file mode 100644 index 00000000000..5c29a1014e1 --- /dev/null +++ b/docs/briefs/r3-v-l4-l7-direct-worker.md @@ -0,0 +1,51 @@ +# R3 Lane 1 — T-Verification-L4-L7-Direct Worker Brief + +**Status:** STANDBY — gates on R2-Evaluator PR-A.3 implementation carriers + PR-B body evaluator landing. Brief authored at R3 Verification Manager spawn (2026-04-30); converts to dispatch-ready when prerequisites fire. + +**Parent:** [`docs/briefs/r3-verification-manager.md`](r3-verification-manager.md) — Lane 1 of 3. + +**R3 lane authority:** [`docs/r3-structure.md`](../r3-structure.md) §"Lane structure" row **T-Verification-L4-L7-Direct** (L92). + +## Scope (this lane) + +Per-target equivalence harness for the **L4** (emit/eval match) + **L7** (algebraic-law witness construction) verification claims. Direct-mode runtime equivalence: compares computational results between emit-target output and `.dag` evaluator result on the certification corpus. + +**NOT a `Lens` instance** per codex BLOCKING `f5f63c7d9` — the lens framework's `read: (Dag, Behavior) → Witness` cannot read emitted target artifacts; L4/L7 are runtime equivalence checks, not structural folds. The lane *consumes* `Lens` instances as inputs where useful (e.g., `Lens` for cost-related claims, `Lens` for structural pre-checks) but the lane itself is corpus-driven runtime, not structural fold. + +## Dependencies (gates) + +| Dependency | Source | Why | +|---|---|---| +| **R2-Evaluator PR-A.3 carriers** | [`r2-pr-a3-strategy-memoization-audit.md`](r2-pr-a3-strategy-memoization-audit.md) + [`r2-pr-a3-implementation-blocker-audit.md`](r2-pr-a3-implementation-blocker-audit.md) | Need closed strategy carrier + structural memo-key identity to evaluate `.dag` programs at the eval-side of the equivalence check. | +| **R2-Evaluator PR-B body evaluator (eager baseline)** | [`r2-pr-b-body-evaluator-eager-baseline.md`](r2-pr-b-body-evaluator-eager-baseline.md) | Body evaluator executes `.dag` bodies — without it, no eval-side computational result to compare. | +| **PR-D `DifferentialEquals` scaffold** | [`r2-pr-d-cross-target-equivalence-harness-primitives.md`](r2-pr-d-cross-target-equivalence-harness-primitives.md) §slice 1 | Worker B's #1226 scaffold provides the `TestPredicate::DifferentialEquals` runner-wiring primitive this lane consumes. **Already landed** at slice 1; lane standby is on PR-A.3 + PR-B, not PR-D. | +| **Shape A targets emit-ready** | R2-Grounding-Rust (production); R2-Grounding-Python / Go pending | L4 per-target evaluation needs at least 1 emit target on the same `Dag`; full L4 across Shape A requires 3. | + +## Implementation slices (when dispatch fires) + +1. **Slice 1 — single-target L4 receipt:** one `TestClaim` using `TestPredicate::DifferentialEquals` comparing Rust emit-target output vs `.dag` eval result on a minimal corpus program. Fixture: `src/v3/compiler/tests/fixtures/r3_verification_l4_direct_rust.dag` (proposed). Suite: `r3_verification_l4_direct_suite`. +2. **Slice 2 — multi-target L4:** add per-target receipts as Python / Go grounding lands. Each target adds one `DifferentialEquals` row using existing predicate; no new `TestPredicate` variants. +3. **Slice 3 — L7 algebraic-law witness:** use `TestPredicate::AlgebraicLaw` (already on substrate at `src/v3/std/verification.dag` L189; `AlgebraicLawKind` enum L103) for at least one named law (associativity / commutativity / identity) per the lens-framework I4 + I9 TestClaims. + +## Structural acceptance — `.dag` hook + +| Gate name | Fixture (proposed) | Suite | +|---|---|---| +| `verification_l4_l7_direct_per_target_equivalence_landed` | `src/v3/compiler/tests/fixtures/r3_verification_l4_l7_direct.dag` | `r3_verification_l4_l7_direct_suite` | + +**Dissolution trigger:** when L5 corpus (Lane 2) absorbs all per-target receipts as a single cross-target row, the per-target L4 stubs downgrade — but the **claim name** stays stable until a Director-amended acceptance table moves it. + +## Explicitly out of scope + +- **L5 cross-target equivalence corpus** — Lane 2 ([`r3-v-l5-corpus-worker.md`](r3-v-l5-corpus-worker.md)). +- **L6 form coverage** — moved to R2-T-Ground-CrossTarget-Meta per [`r3-structure.md`](../r3-structure.md) L92-93 (NOT in Verification Manager scope). +- **`Lens` authoring** — T-CostLens-Composition under Substrate continuation per Director-locked 2026-04-28; this lane consumes the lens, does not author it. +- **New `TestPredicate` variants** — substrate introduction via [`INVARIANTS.md`](../../INVARIANTS.md) §P1 only if existing scaffold (`DifferentialEquals` / `AlgebraicLaw` / `ForAllTargets` / `LensOutputEquals`) cannot express a future fact. + +## Cross-refs + +- Parent manager: [`docs/briefs/r3-verification-manager.md`](r3-verification-manager.md) +- R3 lane row: [`docs/r3-structure.md`](../r3-structure.md) §"Lane structure" T-Verification-L4-L7-Direct (L92) +- Upstream PR-D scaffold: [`docs/briefs/r2-pr-d-cross-target-equivalence-harness-primitives.md`](r2-pr-d-cross-target-equivalence-harness-primitives.md) +- Lens framework consumer: [`docs/design-lens-framework.md`](../design-lens-framework.md) +- THESIS surface: [`THESIS.md`](../../THESIS.md) §"Tier 3 — Verification from structure" (L4 + L7 claims) diff --git a/docs/briefs/r3-v-l5-corpus-worker.md b/docs/briefs/r3-v-l5-corpus-worker.md new file mode 100644 index 00000000000..aefb3ca7d81 --- /dev/null +++ b/docs/briefs/r3-v-l5-corpus-worker.md @@ -0,0 +1,51 @@ +# R3 Lane 2 — T-Verification-L5-Corpus Worker Brief + +**Status:** STANDBY — gates sequentially on Lane 1 (T-V-L4-L7-Direct) corpus existing + Shape A 3-target grounding (Rust + Python + Go). Brief authored at R3 Verification Manager spawn (2026-04-30); converts to dispatch-ready when prerequisites fire. + +**Parent:** [`docs/briefs/r3-verification-manager.md`](r3-verification-manager.md) — Lane 2 of 3. + +**R3 lane authority:** [`docs/r3-structure.md`](../r3-structure.md) §"Lane structure" row **T-Verification-L5-Corpus** (L93). + +## Scope (this lane) + +L5 cross-target equivalence corpus — algebraic equivalence of computational results across Rust / Python / Go on the certification corpus. **Not byte identity**; algebraic equivalence per [`docs/r3-structure.md`](../r3-structure.md) L11. + +L6 form coverage is **explicitly out of scope** — moved to R2-T-Ground-CrossTarget-Meta per [`r3-structure.md`](../r3-structure.md) L92-93 (different input space: per-(form × target) vs per-Behavior; lives as its own substrate-load-time completeness primitive per codex BLOCKING `90220bd97`). + +## Dependencies (gates — sequential) + +| Dependency | Source | Why | +|---|---|---| +| **Lane 1 corpus exists** | [`r3-v-l4-l7-direct-worker.md`](r3-v-l4-l7-direct-worker.md) | Critical path per [`r3-structure.md`](../r3-structure.md) L147: "Verification has its own internal critical path: T-V-L4-L7-Direct → T-V-L5-Corpus (because Corpus's L5 cross-target work consumes Direct's L4 corpus)." | +| **Shape A 3-target grounding** | R2-Grounding-Rust + R2-Grounding-Python + R2-Grounding-Go | L5 is by definition cross-target; needs all 3 emit paths on the same `Dag`. | +| **R2-T-Ground-LanguageSpec** | Grounding Manager continuation | Per-target primitive realization + typed capability edges for comparable observations across Rust / Python / Go. | + +## Implementation slices (when dispatch fires) + +1. **Slice 1 — corpus seed:** import Lane 1's per-target L4 corpus as the seed for L5 cross-target receipts. One `TestClaim` per corpus program using `TestPredicate::ForAllTargets` (substrate scaffold at `src/v3/std/verification.dag` ~L147; in-file 🟡 dissolution comment respected — emit-scoped use only after Director approval per [`r2-pr-d-cross-target-equivalence-harness-primitives.md`](r2-pr-d-cross-target-equivalence-harness-primitives.md) §slice 2). +2. **Slice 2 — corpus expansion:** grow the corpus along the certification axes (per Verification thesis). Each new program adds one row; no new predicates. +3. **Slice 3 — strict L5 fire:** when corpus is broad enough that `l5_cross_target_consistency` carries non-trivial coverage, fire the strict gate per [`r3-structure.md`](../r3-structure.md) L93. + +## Structural acceptance — `.dag` hook + +| Gate name | Fixture (proposed) | Suite | +|---|---|---| +| `verification_l5_cross_target_consistency_landed` | `src/v3/compiler/tests/fixtures/r3_verification_l5_corpus.dag` | `r3_verification_l5_corpus_suite` | + +**Stability invariant** (per [`r2-pr-d-cross-target-equivalence-harness-primitives.md`](r2-pr-d-cross-target-equivalence-harness-primitives.md) §"Deferred fixture path"): keep the **declaration name** stable; only update fixture-module path with manager-brief + integration-test co-update in one PR. + +## Explicitly out of scope + +- **L4 per-target equivalence** — Lane 1 ([`r3-v-l4-l7-direct-worker.md`](r3-v-l4-l7-direct-worker.md)). +- **L6 form coverage** — R2-T-Ground-CrossTarget-Meta (Grounding Manager). +- **Curated corpus authoring at R2** — explicitly post-R2 per [`r2-evaluator-manager.md`](r2-evaluator-manager.md) "primitives only — corpus authoring is post-R2". +- **New `TestPredicate` variants** — `ForAllTargets` already on substrate; INVARIANTS §P1 only for genuinely new facts. + +## Cross-refs + +- Parent manager: [`docs/briefs/r3-verification-manager.md`](r3-verification-manager.md) +- R3 lane row: [`docs/r3-structure.md`](../r3-structure.md) §"Lane structure" T-Verification-L5-Corpus (L93) +- Upstream Lane 1: [`docs/briefs/r3-v-l4-l7-direct-worker.md`](r3-v-l4-l7-direct-worker.md) +- Upstream PR-D scaffold: [`docs/briefs/r2-pr-d-cross-target-equivalence-harness-primitives.md`](r2-pr-d-cross-target-equivalence-harness-primitives.md) +- L6 reclassification: [`docs/r3-structure.md`](../r3-structure.md) L92-93 +- THESIS surface: [`THESIS.md`](../../THESIS.md) §"Tier 3 — Verification from structure" (L5 claim) diff --git a/docs/briefs/r3-verification-manager.md b/docs/briefs/r3-verification-manager.md new file mode 100644 index 00000000000..aa1be81ef67 --- /dev/null +++ b/docs/briefs/r3-verification-manager.md @@ -0,0 +1,107 @@ +# R3 Verification Manager Brief + +**Status:** PROPOSAL — manager brief authored at R3 spin-up (post-R2-close 2026-04-30 per [`docs/r2-closure-ledger.md`](../r2-closure-ledger.md) §"Director closure acceptance"). Spawned per [`docs/r3-structure.md`](../r3-structure.md) §"Manager structure" Item 2 (Director-locked 2026-04-28). + +## Orient before reading + +- **R3 structure authority:** [`docs/r3-structure.md`](../r3-structure.md). Names this manager owner of T-Verification-L4-L7-Direct + T-Verification-L5-Corpus + the `bridge_retirement_ledger_zero` audit gate of T-Bridge-Retirement. +- **Program scope source:** [`THESIS.md`](../../THESIS.md) §"Tier 3 — Verification from structure" (L4, L5, L7 verification-surface claims) + [`docs/r3-structure.md`](../r3-structure.md) §"Lane structure" rows for T-Verification-L4-L7-Direct / T-Verification-L5-Corpus / T-Bridge-Retirement. +- **Why a new manager (per `r3-structure.md` L108):** the R3 verification surface {L4, L5, L7} is structural-acceptance-by-construction — its own discipline, not foldable into Substrate (different concern) or PB (different concern). +- **Cross-program producer:** **R2-Evaluator** gates lanes 1 and 2 (Witness construction surface + cross-target equivalence harness primitives). R3-absorbed formal-grounding lane (TC1/TC2/TC3 bundling) consumes substrate primitives authored by Substrate Manager continuation. +- **Substrate-fact-introduction procedure** ([`INVARIANTS.md`](../../INVARIANTS.md) §P1): self-serve through the 3-step decision procedure before escalating substrate-shape questions to Director. TC3 is the live escalation candidate (per [`r3-pb-t-fixedpoint-worker.md`](r3-pb-t-fixedpoint-worker.md) §"TC3 — Strong-normalization TestClaim"). + +## Owned program scope (3 lanes + 1 ledger gate) + +| Lane | Size | Status (at brief authoring) | Gates on | +|---|---|---|---| +| **Lane 1: T-V-L4-L7-Direct** | M | **Worker brief authored, standby** — [`r3-v-l4-l7-direct-worker.md`](r3-v-l4-l7-direct-worker.md). Per-target equivalence harness using `DifferentialEquals` predicate (consumes Worker B PR-D scaffold per [`r2-pr-d-cross-target-equivalence-harness-primitives.md`](r2-pr-d-cross-target-equivalence-harness-primitives.md) §slice 1). NOT a `Lens` instance per codex BLOCKING `f5f63c7d9` — runtime equivalence check, not structural fold. | R2-Evaluator PR-A.3 implementation carriers + PR-B body evaluator landing | +| **Lane 2: T-V-L5-Corpus** | M | **Worker brief authored, standby** — [`r3-v-l5-corpus-worker.md`](r3-v-l5-corpus-worker.md). Cross-target equivalence corpus authoring (L5 only; L6 reclassified to R2-T-Ground-CrossTarget-Meta per [`r3-structure.md`](../r3-structure.md) L92-93). | Lane 1 corpus existing + R2-Grounding-Rust + R2-Grounding-Python (Shape A 3-target grounding precondition) | +| **Lane 3: T-FormalGrounding-Verification (TC1/TC2/TC3)** | L (research-tier) | **Worker brief authored** — [`r3-v-formal-grounding-tc-bundle.md`](r3-v-formal-grounding-tc-bundle.md). TC1 landed via #1179 fixture; TC2 slice-0 hook landed; TC3 substrate-encoding gap framed per [`r3-pb-t-fixedpoint-worker.md`](r3-pb-t-fixedpoint-worker.md) L145-215. PM Tier C estimate: ~3-5 days research per TC strengthening. | Per-claim: TC1 already author-now-fire-later; TC2 strengthens on ≥2 executable strategies (R3-deferred from R2-Evaluator); TC3 on T-FixedPoint + T-Substrate-Lens-Primitive + substrate-fact-introduction | +| **Ledger gate: T-Bridge-Retirement (`bridge_retirement_ledger_zero`)** | S (audit cadence; no implementation) | **Bridge map row maintenance** — 5 named bridges per [`r3-structure.md`](../r3-structure.md) L98 distribution map. Verification owns the unified audit gate; retirement work distributes per natural-owner program. | Per-bridge: each bridge fires structurally in its owner program; ledger-zero gate fires when all 5 are green. | + +## Bridge-retirement ledger — current state (2026-04-30 audit) + +Per [`docs/r3-structure.md`](../r3-structure.md) L98 distribution map; cross-checked against closure ledger #1275 + landed PRs: + +| # | Bridge | Owner | Status | Evidence | +|---|---|---|---|---| +| 1 | `SourceSpan.file` participation checks | **Substrate** | **R3-deferred** | #1273 STOP+PING audit landed; #1130 Director acceptance — partial string-check retirement rejected; structural prerequisites named (module/compilation-unit identity for lens reflection; typed authority/emit-scope carriers for lower/emit). Per [`r3-structure.md`](../r3-structure.md) L79. | +| 2 | `mark_bootstrap_secret_nominal_opacity()` | **Substrate** | **retired** | #1272 (refactor(v3): retire Secret bootstrap opacity bridge). | +| 3 | Canonical lens-name dispatch | **PB** | **slice landed; ledger-zero pending** | #1183 — narrow-scope canonical lens-name dispatch slice. Broader exact-string lens-name patching not yet structurally retired. | +| 4 | `include_str!` side channels (e.g., `pipeline_authority.rs`) | **PB** | **outstanding-or-waiting** | #1171 suspended `reconcile_with_compile_body` rather than swapping `include_str!` for runtime file IO; **`bridge_include_str_side_channels_retired` still open** per [`docs/design-emission-model.md:944`](../design-emission-model.md). Awaits derivation or structural compile-body witness. | +| 5 | `patch_lower_helpers_*` residual | **PB** | **slice landed; narrow scope** | #1014 (first slice — generated field native) + #1192 (`bridge_lower_helpers_patch_zero_residual_test.rs` — narrow ratchet-zero). Broader exact-string patching outside this slice not claimed retired. | + +**Net position:** 1 retired (#1272), 3 narrow slices landed (#1014/#1171/#1183/#1192 — but ledger-zero unification pending per #1275 PB row L147), 1 R3-deferred (#1273). **Unified `bridge_retirement_ledger_zero` gate remains open** until all 5 fire structurally — row stays in-flight per closure ledger discipline. + +## TestClaim author-now-fire-later state — audit (2026-04-30) + +| TC | Fixture / authority | Strict-fire gate | Audit result | +|---|---|---|---| +| **TC1 — η-equivalence** | `src/v3/compiler/tests/fixtures/tc1_substrate_lens_eta_equivalence_deferred.dag` (#1179); `SubstrateResearchDeferredClaim` runner-valid only for this fixture per [`r2-closure-ledger.md`](../r2-closure-ledger.md) L220 | T-Substrate-Lens-Primitive + lens producer retirement | **Consistent on main** — fixture exists; deferred-claim carrier authored per Director #1130 / dispatch #1139. | +| **TC2 — Church-Rosser / evaluation-order independence** | `src/v3/compiler/tests/fixtures/tc2_evaluation_order_independence_deferred.dag` slice-0 hook (per [`r2-evaluator-manager.md`](r2-evaluator-manager.md) L127) | Strict claim activation needs **≥2 executable strategies** (R3-deferred from R2-Evaluator; PR-B.1 lands a single eager strategy per [`r2-pr-b-body-evaluator-eager-baseline.md`](r2-pr-b-body-evaluator-eager-baseline.md) L154) | **Consistent on main** — slice-0 deferred fixture exists; strengthens to strict strategy-output equality over `DimensionReport` once second strategy lands. | +| **TC3 — strong normalization** | **Text-form only** in [`r3-pb-t-fixedpoint-worker.md`](r3-pb-t-fixedpoint-worker.md) L145-215; **no fixture on disk** | Substrate-fact-introduction required — no existing `TestPredicate` variant carries the meta-theorem-over-well-typed-fragment quantifier shape (per L171 of that brief) | **Consistent — declaration-as-PROPOSAL preserved.** TC3 ownership transitions from PB to Verification per L181-185 contract. Verification will author substrate path when B5 + T-Substrate-Lens-Primitive land; PB does not re-author. | + +**No drift surfaced to Director.** All three claims maintain author-now-fire-later discipline; structural unblock conditions are category-tagged per dispatch contract. + +## Cross-program dependencies + +**Produces:** +- **L4-L7 verification surface** — Lane 1 lands per-target equivalence; Lane 2 lands cross-target equivalence corpus. +- **TC1/TC2/TC3 strict-fire activations** — Lane 3 strengthens deferred claims as upstream substrate / evaluator dependencies land. +- **Unified bridge-retirement audit cadence** — periodic ledger-zero gate check; signals to Director when all 5 bridges fire. + +**Consumes:** +- **R2-Evaluator** — PR-A.3 carriers (closed strategy + memoization), PR-B body evaluator (eager baseline), PR-D harness primitives (`DifferentialEquals` runner wiring), PR-E lens application (`fold_lens_over_reflected_program` integration seam). +- **R2-Grounding** — Shape A 3-target grounding (Rust + Python + Go) for L5 cross-target receipts. +- **PB Manager continuation** — T-FixedPoint completion (TC3 dependency); T-LensProducer-Retirement (consumed indirectly via TC1 substrate-research strengthening); 3 PB-side bridge slices landing toward ledger-zero. +- **Substrate Manager continuation** — T-Substrate-Lens-Primitive (TC1/TC2 strengthening; TC3 evaluation-step witness shape per [`r3-pb-t-fixedpoint-worker.md`](r3-pb-t-fixedpoint-worker.md) L165); SourceSpan.file participation retirement (Bridge #1). + +## Autonomous dispatch authority + +- Authors all Verification sub-briefs without Director (per `feedback_standing_managers_need_owned_deliverables.md` discipline). +- Dispatches workers against Verification sub-briefs once cross-program prerequisites land. +- Resolves Verification-internal scope refinements; escalates substrate-shape questions / cross-program scope-changes to Director. +- Per `docs/r2-structure.md` P5 dispatch-discipline (carried into R3): every Verification worker brief that introduces a scaffold names its dissolution trigger + adjacent ROADMAP debt row + contributes-or-defers stance. +- **TC3 substrate-fact-introduction**: when B5 + T-Substrate-Lens-Primitive land, author substrate path through INVARIANTS §P1 procedure; cross-coordinate with Substrate Manager for the meta-theorem quantifier shape. + +## Reporting cadence + +- **Lane-close → R2 Release Manager continuation** (closure ledger maintenance via bold-lynx-173 #1135). Each lane's structural acceptance gate IS the demo per the structural-acceptance-per-lane-close discipline. +- **Cross-program signals** (e.g., bridge ledger-zero audit results) → cross-manager queue + Director. +- **TC strict-fire activation signals** → Director (gates R3 verification surface closure). +- **Blockers + scope changes** → Director (#828). +- **Brief-PR cadence** (per `feedback_brief_pr_cadence.md`): brief PRs only when carrying a new cross-manager signal; pure checkbox maintenance bundles into next signal PR or end-of-session sweep. + +## Acceptance — `.dag` gates + +Each lane closes under a structural acceptance gate authored as a `.dag` `TestClaim`: + +- **Lane 1**: `verification_l4_l7_direct_per_target_equivalence_landed` — per-target `DifferentialEquals` receipts on the certification corpus; emit-target output vs `.dag` eval result match for each Shape A target. +- **Lane 2**: `verification_l5_cross_target_consistency_landed` — Rust / Python / Go equivalent runtime behavior on the certification corpus (algebraic equivalence over computational results, not byte identity). +- **Lane 3**: TC1/TC2/TC3 strict-fire activation across the three deferred-claim fixtures (TC3 fixture authored under substrate path). +- **Ledger gate**: `bridge_retirement_ledger_zero` — unified ledger reports 0 named identity bridges remaining (per [`r3-structure.md`](../r3-structure.md) L84). + +## Sub-briefs (authored / pending) + +**Authored at spawn (this PR):** +- [`r3-v-l4-l7-direct-worker.md`](r3-v-l4-l7-direct-worker.md) — Lane 1 standby brief. +- [`r3-v-l5-corpus-worker.md`](r3-v-l5-corpus-worker.md) — Lane 2 standby brief. +- [`r3-v-formal-grounding-tc-bundle.md`](r3-v-formal-grounding-tc-bundle.md) — Lane 3 TC1/TC2/TC3 bundle. + +**Pending (post-spawn manager authors autonomously):** +- TC3 substrate-fact-introduction worker brief (gated on B5 + T-Substrate-Lens-Primitive). +- Lane 1 / Lane 2 implementation worker briefs (gated on R2-Evaluator landing — convert from standby to dispatch-ready when prerequisites fire). + +## Working state (fill on dispatch) + +Lane status table refreshes here as work lands. Initial state: 3 lanes in standby + 1 ledger gate in audit cadence; bridge map row maintenance ongoing. + +## Cross-refs + +- Parent: [`docs/r3-structure.md`](../r3-structure.md) §"Manager structure" Item 2 + §"Lane structure" rows for T-Verification-L4-L7-Direct / T-Verification-L5-Corpus / T-Bridge-Retirement +- Closure ledger predecessor: [`docs/r2-closure-ledger.md`](../r2-closure-ledger.md) (R2 closed-with-residuals 2026-04-30) +- R2 Evaluator producer brief: [`docs/briefs/r2-evaluator-manager.md`](r2-evaluator-manager.md) +- TC3 upstream declarative shape: [`docs/briefs/r3-pb-t-fixedpoint-worker.md`](r3-pb-t-fixedpoint-worker.md) §"TC3 — Strong-normalization TestClaim" (L145-215; ownership transitions to Verification per L181-185) +- Worker B PR-D scaffold consumer: [`docs/briefs/r2-pr-d-cross-target-equivalence-harness-primitives.md`](r2-pr-d-cross-target-equivalence-harness-primitives.md) +- Bridge distribution map: [`docs/r3-structure.md`](../r3-structure.md) L98 +- INVARIANTS substrate-fact-introduction procedure: [`INVARIANTS.md`](../../INVARIANTS.md) §P1 From ac1b35ca31c80ca91718cfe4d6e15ca7fe34d788 Mon Sep 17 00:00:00 2001 From: Brian Searls Date: Thu, 30 Apr 2026 17:07:54 +0000 Subject: [PATCH 2/9] docs(r3): fix Lane 2 grounding-target gate (add Go) MIME-Version: 1.0 Content-Type: text/plain; charset=UTF-8 Content-Transfer-Encoding: 8bit Manager brief Lane 2 gate listed only R2-Grounding-Rust + R2-Grounding-Python while calling it the "Shape A 3-target grounding precondition." Worker brief already correctly required all three (Rust + Python + Go). Add Go to manager gate to match — single-authority discipline per INVARIANTS §P2. Co-Authored-By: Claude Opus 4.7 (1M context) --- docs/briefs/r3-verification-manager.md | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/docs/briefs/r3-verification-manager.md b/docs/briefs/r3-verification-manager.md index aa1be81ef67..68f01349581 100644 --- a/docs/briefs/r3-verification-manager.md +++ b/docs/briefs/r3-verification-manager.md @@ -15,7 +15,7 @@ | Lane | Size | Status (at brief authoring) | Gates on | |---|---|---|---| | **Lane 1: T-V-L4-L7-Direct** | M | **Worker brief authored, standby** — [`r3-v-l4-l7-direct-worker.md`](r3-v-l4-l7-direct-worker.md). Per-target equivalence harness using `DifferentialEquals` predicate (consumes Worker B PR-D scaffold per [`r2-pr-d-cross-target-equivalence-harness-primitives.md`](r2-pr-d-cross-target-equivalence-harness-primitives.md) §slice 1). NOT a `Lens` instance per codex BLOCKING `f5f63c7d9` — runtime equivalence check, not structural fold. | R2-Evaluator PR-A.3 implementation carriers + PR-B body evaluator landing | -| **Lane 2: T-V-L5-Corpus** | M | **Worker brief authored, standby** — [`r3-v-l5-corpus-worker.md`](r3-v-l5-corpus-worker.md). Cross-target equivalence corpus authoring (L5 only; L6 reclassified to R2-T-Ground-CrossTarget-Meta per [`r3-structure.md`](../r3-structure.md) L92-93). | Lane 1 corpus existing + R2-Grounding-Rust + R2-Grounding-Python (Shape A 3-target grounding precondition) | +| **Lane 2: T-V-L5-Corpus** | M | **Worker brief authored, standby** — [`r3-v-l5-corpus-worker.md`](r3-v-l5-corpus-worker.md). Cross-target equivalence corpus authoring (L5 only; L6 reclassified to R2-T-Ground-CrossTarget-Meta per [`r3-structure.md`](../r3-structure.md) L92-93). | Lane 1 corpus existing + R2-Grounding-Rust + R2-Grounding-Python + R2-Grounding-Go (Shape A 3-target grounding precondition) | | **Lane 3: T-FormalGrounding-Verification (TC1/TC2/TC3)** | L (research-tier) | **Worker brief authored** — [`r3-v-formal-grounding-tc-bundle.md`](r3-v-formal-grounding-tc-bundle.md). TC1 landed via #1179 fixture; TC2 slice-0 hook landed; TC3 substrate-encoding gap framed per [`r3-pb-t-fixedpoint-worker.md`](r3-pb-t-fixedpoint-worker.md) L145-215. PM Tier C estimate: ~3-5 days research per TC strengthening. | Per-claim: TC1 already author-now-fire-later; TC2 strengthens on ≥2 executable strategies (R3-deferred from R2-Evaluator); TC3 on T-FixedPoint + T-Substrate-Lens-Primitive + substrate-fact-introduction | | **Ledger gate: T-Bridge-Retirement (`bridge_retirement_ledger_zero`)** | S (audit cadence; no implementation) | **Bridge map row maintenance** — 5 named bridges per [`r3-structure.md`](../r3-structure.md) L98 distribution map. Verification owns the unified audit gate; retirement work distributes per natural-owner program. | Per-bridge: each bridge fires structurally in its owner program; ledger-zero gate fires when all 5 are green. | From ac3bf24309c88c6169f0c4a2421f39dcd8795395 Mon Sep 17 00:00:00 2001 From: Brian Searls Date: Thu, 30 Apr 2026 17:23:21 +0000 Subject: [PATCH 3/9] docs(r3): fix bridge-ledger net-position count mismatch MIME-Version: 1.0 Content-Type: text/plain; charset=UTF-8 Content-Transfer-Encoding: 8bit Net-position summary listed "3 narrow slices landed (#1014/#1171/#1183/#1192)" which read as a 3-vs-4 count mismatch. #1171 is the outstanding/suspended bridge (#bridge_include_str_side_channels_retired open), not a landed slice. Restate as 2 landed (canonical lens / lower-helper) + 1 outstanding (#1171) + 1 R3-deferred + 1 retired, totaling 5 — and reference closure-ledger PR #1283 which now tracks the include_str row separately. Co-Authored-By: Claude Opus 4.7 (1M context) --- docs/briefs/r3-verification-manager.md | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/docs/briefs/r3-verification-manager.md b/docs/briefs/r3-verification-manager.md index 68f01349581..a3bce3e8368 100644 --- a/docs/briefs/r3-verification-manager.md +++ b/docs/briefs/r3-verification-manager.md @@ -31,7 +31,7 @@ Per [`docs/r3-structure.md`](../r3-structure.md) L98 distribution map; cross-che | 4 | `include_str!` side channels (e.g., `pipeline_authority.rs`) | **PB** | **outstanding-or-waiting** | #1171 suspended `reconcile_with_compile_body` rather than swapping `include_str!` for runtime file IO; **`bridge_include_str_side_channels_retired` still open** per [`docs/design-emission-model.md:944`](../design-emission-model.md). Awaits derivation or structural compile-body witness. | | 5 | `patch_lower_helpers_*` residual | **PB** | **slice landed; narrow scope** | #1014 (first slice — generated field native) + #1192 (`bridge_lower_helpers_patch_zero_residual_test.rs` — narrow ratchet-zero). Broader exact-string patching outside this slice not claimed retired. | -**Net position:** 1 retired (#1272), 3 narrow slices landed (#1014/#1171/#1183/#1192 — but ledger-zero unification pending per #1275 PB row L147), 1 R3-deferred (#1273). **Unified `bridge_retirement_ledger_zero` gate remains open** until all 5 fire structurally — row stays in-flight per closure ledger discipline. +**Net position:** 1 retired (#1272), 2 narrow slices landed (#1183 canonical lens / #1014 + #1192 lower-helper), 1 outstanding (#1171 suspended `reconcile_with_compile_body` only — `bridge_include_str_side_channels_retired` still open; tracked separately by closure-ledger update #1283), 1 R3-deferred (#1273). **Unified `bridge_retirement_ledger_zero` gate remains open** until all 5 fire structurally — row stays in-flight per closure ledger discipline. ## TestClaim author-now-fire-later state — audit (2026-04-30) From bfcece09d0cd1ed788b9862ef82a90f962732bcc Mon Sep 17 00:00:00 2001 From: Brian Searls Date: Thu, 30 Apr 2026 18:01:00 +0000 Subject: [PATCH 4/9] docs(r3): reframe TC bundle as absorbed responsibility, not 3rd lane MIME-Version: 1.0 Content-Type: text/plain; charset=UTF-8 Content-Transfer-Encoding: 8bit Manager brief promoted T-FormalGrounding-Verification to a third lane while the structural authority docs/r3-structure.md L108 names exactly "2 lanes + 1 ledger gate" for Verification scope. That created parallel scope authority violating INVARIANTS §P2. Resolved by deferring to r3-structure.md authority: TC1/TC2/TC3 bundle is now an absorbed cross-cutting responsibility (audit cadence + strict-fire tracking folded into manager cadence), matching r3-pb-t-fixedpoint-worker.md L181 "ownership moves" wording. TC3 substrate-introduction worker brief, when its prerequisites land, joins the existing 2-lane scope as a substrate-introduction sub-task — not a new lane row. If Director ratifies a third lane in r3-structure.md itself, this brief updates accordingly; until then 2-lane scope is the authority. Co-Authored-By: Claude Opus 4.7 (1M context) --- docs/briefs/r3-v-formal-grounding-tc-bundle.md | 6 +++--- docs/briefs/r3-v-l4-l7-direct-worker.md | 2 +- docs/briefs/r3-v-l5-corpus-worker.md | 2 +- docs/briefs/r3-verification-manager.md | 17 ++++++++++------- 4 files changed, 15 insertions(+), 12 deletions(-) diff --git a/docs/briefs/r3-v-formal-grounding-tc-bundle.md b/docs/briefs/r3-v-formal-grounding-tc-bundle.md index 0d3717e08e5..4f4de199638 100644 --- a/docs/briefs/r3-v-formal-grounding-tc-bundle.md +++ b/docs/briefs/r3-v-formal-grounding-tc-bundle.md @@ -1,8 +1,8 @@ -# R3 Lane 3 — T-FormalGrounding-Verification (TC1 / TC2 / TC3 bundle) Worker Brief +# R3 Verification — T-FormalGrounding TC1/TC2/TC3 Bundle (Absorbed Responsibility) -**Status:** PROPOSAL — Lane 3 of R3 Verification Manager. Bundles three formal-grounding TestClaims under one ownership lane per PM R3-absorption mapping. Research-tier work (~3-5 days per TC strengthening per PM Tier C estimate). +**Status:** PROPOSAL — **absorbed cross-cutting responsibility** of R3 Verification Manager (NOT a third owned lane). The structural authority [`docs/r3-structure.md`](../r3-structure.md) L108 names exactly **2 lanes + 1 ledger gate** for Verification scope; this brief tracks TC1/TC2/TC3 author-now-fire-later cadence + TC3 substrate-introduction triggering as audit-cadence work, not a dispatch lane. Research-tier work (~3-5 days per TC strengthening per PM Tier C estimate) when TC3 substrate-introduction worker brief is authored under the existing 2-lane scope. -**Parent:** [`docs/briefs/r3-verification-manager.md`](r3-verification-manager.md) — Lane 3 of 3. +**Parent:** [`docs/briefs/r3-verification-manager.md`](r3-verification-manager.md) — §"Absorbed cross-cutting responsibility — TC1/TC2/TC3 bundle". ## Scope (this lane) diff --git a/docs/briefs/r3-v-l4-l7-direct-worker.md b/docs/briefs/r3-v-l4-l7-direct-worker.md index 5c29a1014e1..9e1b8bfe8d5 100644 --- a/docs/briefs/r3-v-l4-l7-direct-worker.md +++ b/docs/briefs/r3-v-l4-l7-direct-worker.md @@ -2,7 +2,7 @@ **Status:** STANDBY — gates on R2-Evaluator PR-A.3 implementation carriers + PR-B body evaluator landing. Brief authored at R3 Verification Manager spawn (2026-04-30); converts to dispatch-ready when prerequisites fire. -**Parent:** [`docs/briefs/r3-verification-manager.md`](r3-verification-manager.md) — Lane 1 of 3. +**Parent:** [`docs/briefs/r3-verification-manager.md`](r3-verification-manager.md) — Lane 1 of 2 owned lanes (per `r3-structure.md` L108 authority). **R3 lane authority:** [`docs/r3-structure.md`](../r3-structure.md) §"Lane structure" row **T-Verification-L4-L7-Direct** (L92). diff --git a/docs/briefs/r3-v-l5-corpus-worker.md b/docs/briefs/r3-v-l5-corpus-worker.md index aefb3ca7d81..9ae68a9d74e 100644 --- a/docs/briefs/r3-v-l5-corpus-worker.md +++ b/docs/briefs/r3-v-l5-corpus-worker.md @@ -2,7 +2,7 @@ **Status:** STANDBY — gates sequentially on Lane 1 (T-V-L4-L7-Direct) corpus existing + Shape A 3-target grounding (Rust + Python + Go). Brief authored at R3 Verification Manager spawn (2026-04-30); converts to dispatch-ready when prerequisites fire. -**Parent:** [`docs/briefs/r3-verification-manager.md`](r3-verification-manager.md) — Lane 2 of 3. +**Parent:** [`docs/briefs/r3-verification-manager.md`](r3-verification-manager.md) — Lane 2 of 2 owned lanes (per `r3-structure.md` L108 authority). **R3 lane authority:** [`docs/r3-structure.md`](../r3-structure.md) §"Lane structure" row **T-Verification-L5-Corpus** (L93). diff --git a/docs/briefs/r3-verification-manager.md b/docs/briefs/r3-verification-manager.md index a3bce3e8368..f79364756ce 100644 --- a/docs/briefs/r3-verification-manager.md +++ b/docs/briefs/r3-verification-manager.md @@ -10,15 +10,18 @@ - **Cross-program producer:** **R2-Evaluator** gates lanes 1 and 2 (Witness construction surface + cross-target equivalence harness primitives). R3-absorbed formal-grounding lane (TC1/TC2/TC3 bundling) consumes substrate primitives authored by Substrate Manager continuation. - **Substrate-fact-introduction procedure** ([`INVARIANTS.md`](../../INVARIANTS.md) §P1): self-serve through the 3-step decision procedure before escalating substrate-shape questions to Director. TC3 is the live escalation candidate (per [`r3-pb-t-fixedpoint-worker.md`](r3-pb-t-fixedpoint-worker.md) §"TC3 — Strong-normalization TestClaim"). -## Owned program scope (3 lanes + 1 ledger gate) +## Owned program scope (2 lanes + 1 ledger gate, per `r3-structure.md` L108 authority) -| Lane | Size | Status (at brief authoring) | Gates on | +| Item | Size | Status (at brief authoring) | Gates on | |---|---|---|---| | **Lane 1: T-V-L4-L7-Direct** | M | **Worker brief authored, standby** — [`r3-v-l4-l7-direct-worker.md`](r3-v-l4-l7-direct-worker.md). Per-target equivalence harness using `DifferentialEquals` predicate (consumes Worker B PR-D scaffold per [`r2-pr-d-cross-target-equivalence-harness-primitives.md`](r2-pr-d-cross-target-equivalence-harness-primitives.md) §slice 1). NOT a `Lens` instance per codex BLOCKING `f5f63c7d9` — runtime equivalence check, not structural fold. | R2-Evaluator PR-A.3 implementation carriers + PR-B body evaluator landing | | **Lane 2: T-V-L5-Corpus** | M | **Worker brief authored, standby** — [`r3-v-l5-corpus-worker.md`](r3-v-l5-corpus-worker.md). Cross-target equivalence corpus authoring (L5 only; L6 reclassified to R2-T-Ground-CrossTarget-Meta per [`r3-structure.md`](../r3-structure.md) L92-93). | Lane 1 corpus existing + R2-Grounding-Rust + R2-Grounding-Python + R2-Grounding-Go (Shape A 3-target grounding precondition) | -| **Lane 3: T-FormalGrounding-Verification (TC1/TC2/TC3)** | L (research-tier) | **Worker brief authored** — [`r3-v-formal-grounding-tc-bundle.md`](r3-v-formal-grounding-tc-bundle.md). TC1 landed via #1179 fixture; TC2 slice-0 hook landed; TC3 substrate-encoding gap framed per [`r3-pb-t-fixedpoint-worker.md`](r3-pb-t-fixedpoint-worker.md) L145-215. PM Tier C estimate: ~3-5 days research per TC strengthening. | Per-claim: TC1 already author-now-fire-later; TC2 strengthens on ≥2 executable strategies (R3-deferred from R2-Evaluator); TC3 on T-FixedPoint + T-Substrate-Lens-Primitive + substrate-fact-introduction | | **Ledger gate: T-Bridge-Retirement (`bridge_retirement_ledger_zero`)** | S (audit cadence; no implementation) | **Bridge map row maintenance** — 5 named bridges per [`r3-structure.md`](../r3-structure.md) L98 distribution map. Verification owns the unified audit gate; retirement work distributes per natural-owner program. | Per-bridge: each bridge fires structurally in its owner program; ledger-zero gate fires when all 5 are green. | +### Absorbed cross-cutting responsibility — TC1/TC2/TC3 bundle (NOT a new lane) + +Per [`r3-pb-t-fixedpoint-worker.md`](r3-pb-t-fixedpoint-worker.md) L181 "TC3 ownership moves from PB to Verification" + R2-Evaluator residual transition for TC2 + #1179 ratification for TC1: the three formal-grounding `TestClaim`s are an **absorbed cross-cutting responsibility** of this manager, not a third owned lane. The structural authority `r3-structure.md` L108 names exactly **2 lanes + 1 ledger gate** for Verification scope; this brief defers to that authority. Audit cadence + strict-fire activation tracking is folded into manager cadence (not a separate dispatch program). Worker brief at [`r3-v-formal-grounding-tc-bundle.md`](r3-v-formal-grounding-tc-bundle.md) authors the bundle as an absorbed-responsibility audit-cadence artifact. **TC3 substrate-fact-introduction**, when its prerequisites land (B5 + T-Substrate-Lens-Primitive), is the only point at which absorbed work converts to a dispatched worker brief — at which time it joins the existing 2-lane scope as a substrate-introduction sub-task, not a new lane row. If Director ratifies a third lane in `r3-structure.md` itself, this brief updates accordingly; until then, 2-lane scope is the authority. + ## Bridge-retirement ledger — current state (2026-04-30 audit) Per [`docs/r3-structure.md`](../r3-structure.md) L98 distribution map; cross-checked against closure ledger #1275 + landed PRs: @@ -47,7 +50,7 @@ Per [`docs/r3-structure.md`](../r3-structure.md) L98 distribution map; cross-che **Produces:** - **L4-L7 verification surface** — Lane 1 lands per-target equivalence; Lane 2 lands cross-target equivalence corpus. -- **TC1/TC2/TC3 strict-fire activations** — Lane 3 strengthens deferred claims as upstream substrate / evaluator dependencies land. +- **TC1/TC2/TC3 strict-fire activations** — absorbed-responsibility audit cadence strengthens deferred claims as upstream substrate / evaluator dependencies land. - **Unified bridge-retirement audit cadence** — periodic ledger-zero gate check; signals to Director when all 5 bridges fire. **Consumes:** @@ -78,7 +81,7 @@ Each lane closes under a structural acceptance gate authored as a `.dag` `TestCl - **Lane 1**: `verification_l4_l7_direct_per_target_equivalence_landed` — per-target `DifferentialEquals` receipts on the certification corpus; emit-target output vs `.dag` eval result match for each Shape A target. - **Lane 2**: `verification_l5_cross_target_consistency_landed` — Rust / Python / Go equivalent runtime behavior on the certification corpus (algebraic equivalence over computational results, not byte identity). -- **Lane 3**: TC1/TC2/TC3 strict-fire activation across the three deferred-claim fixtures (TC3 fixture authored under substrate path). +- **Absorbed responsibility (TC bundle)**: TC1/TC2/TC3 strict-fire activation across the three deferred-claim fixtures (TC3 fixture authored under substrate path) — tracked via audit cadence, not as a lane-close gate. - **Ledger gate**: `bridge_retirement_ledger_zero` — unified ledger reports 0 named identity bridges remaining (per [`r3-structure.md`](../r3-structure.md) L84). ## Sub-briefs (authored / pending) @@ -86,7 +89,7 @@ Each lane closes under a structural acceptance gate authored as a `.dag` `TestCl **Authored at spawn (this PR):** - [`r3-v-l4-l7-direct-worker.md`](r3-v-l4-l7-direct-worker.md) — Lane 1 standby brief. - [`r3-v-l5-corpus-worker.md`](r3-v-l5-corpus-worker.md) — Lane 2 standby brief. -- [`r3-v-formal-grounding-tc-bundle.md`](r3-v-formal-grounding-tc-bundle.md) — Lane 3 TC1/TC2/TC3 bundle. +- [`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` L108 2-lane authority). **Pending (post-spawn manager authors autonomously):** - TC3 substrate-fact-introduction worker brief (gated on B5 + T-Substrate-Lens-Primitive). @@ -94,7 +97,7 @@ Each lane closes under a structural acceptance gate authored as a `.dag` `TestCl ## Working state (fill on dispatch) -Lane status table refreshes here as work lands. Initial state: 3 lanes in standby + 1 ledger gate in audit cadence; bridge map row maintenance ongoing. +Lane status table refreshes here as work lands. Initial state: 2 lanes in standby + 1 ledger gate in audit cadence + TC bundle absorbed-responsibility audit cadence; bridge map row maintenance ongoing. ## Cross-refs From f41de8cb9093707a72fdc51d7745899145a4ace5 Mon Sep 17 00:00:00 2001 From: Brian Searls Date: Thu, 30 Apr 2026 18:10:51 +0000 Subject: [PATCH 5/9] docs(r3): fix L4-vs-L5 categorical-equivalence drift Lane 1 brief had a dissolution-trigger note claiming L5 cross-target corpus could absorb per-target L4 receipts. That conflates two categorically different claims per THESIS.md L179-180: L4 compares emit-target output vs .dag evaluation (per-target), L5 compares Rust/Python/Go behavior cross-target. L5 passing does not entail any target matching .dag eval, so L5 cannot subsume L4. Replace with honest stability invariant matching upstream PR-D pattern, plus explicit note that L4 has no current structural dissolution trigger (per codex BLOCKING f5f63c7d9: NOT a Lens instance, runtime-corpus by design). Co-Authored-By: Claude Opus 4.7 (1M context) --- docs/briefs/r3-v-l4-l7-direct-worker.md | 4 +++- 1 file changed, 3 insertions(+), 1 deletion(-) diff --git a/docs/briefs/r3-v-l4-l7-direct-worker.md b/docs/briefs/r3-v-l4-l7-direct-worker.md index 9e1b8bfe8d5..98afcfbae5a 100644 --- a/docs/briefs/r3-v-l4-l7-direct-worker.md +++ b/docs/briefs/r3-v-l4-l7-direct-worker.md @@ -33,7 +33,9 @@ Per-target equivalence harness for the **L4** (emit/eval match) + **L7** (algebr |---|---|---| | `verification_l4_l7_direct_per_target_equivalence_landed` | `src/v3/compiler/tests/fixtures/r3_verification_l4_l7_direct.dag` | `r3_verification_l4_l7_direct_suite` | -**Dissolution trigger:** when L5 corpus (Lane 2) absorbs all per-target receipts as a single cross-target row, the per-target L4 stubs downgrade — but the **claim name** stays stable until a Director-amended acceptance table moves it. +**Stability invariant** (per [`r2-pr-d-cross-target-equivalence-harness-primitives.md`](r2-pr-d-cross-target-equivalence-harness-primitives.md) §"Deferred fixture path"): the **claim name** stays stable; only update fixture-module path with manager-brief + integration-test co-update in one PR. + +**No L5-absorbs-L4 dissolution.** L4 (per THESIS L179: emitted code executes and matches `.dag` evaluation) and L5 (per THESIS L180: same `.dag` produces same behavior across Rust/Python/Go) are categorically different equivalences — L5 passing does not entail any target matching `.dag` eval, so L5 cannot subsume L4. This lane is corpus-driven runtime by design (per codex BLOCKING `f5f63c7d9` — NOT a `Lens` instance) and has no current structural dissolution trigger; it stays as runtime-verification work absorbing per-target evidence as Shape A targets ground. ## Explicitly out of scope From f3ad5ba22b97a63db42ee06618f431dc30cd0a87 Mon Sep 17 00:00:00 2001 From: Brian Searls Date: Thu, 30 Apr 2026 18:15:20 +0000 Subject: [PATCH 6/9] docs(r3): drop "this lane" language from absorbed-responsibility brief TC bundle brief was reframed as absorbed responsibility (not a lane) but retained "this lane" wording in five places. Replace with "this bundle" throughout to match the locked 2-lane framing per r3-structure.md L108. Editorial fix per cursor reviewer optional finding. Co-Authored-By: Claude Opus 4.7 (1M context) --- docs/briefs/r3-v-formal-grounding-tc-bundle.md | 12 ++++++------ 1 file changed, 6 insertions(+), 6 deletions(-) diff --git a/docs/briefs/r3-v-formal-grounding-tc-bundle.md b/docs/briefs/r3-v-formal-grounding-tc-bundle.md index 4f4de199638..60661b6f80c 100644 --- a/docs/briefs/r3-v-formal-grounding-tc-bundle.md +++ b/docs/briefs/r3-v-formal-grounding-tc-bundle.md @@ -4,9 +4,9 @@ **Parent:** [`docs/briefs/r3-verification-manager.md`](r3-verification-manager.md) — §"Absorbed cross-cutting responsibility — TC1/TC2/TC3 bundle". -## Scope (this lane) +## Scope (this bundle) -Manage the three formal-grounding `TestClaim` author-now-fire-later commitments through their strict-fire activation. Each TC has a different unblock condition; this lane coordinates across them and authors the substrate path for TC3 when its prerequisites land. +Manage the three formal-grounding `TestClaim` author-now-fire-later commitments through their strict-fire activation. Each TC has a different unblock condition; this bundle coordinates across them and authors the substrate path for TC3 when its prerequisites land. | TC | Claim | Status (2026-04-30 audit) | Strict-fire gate | |---|---|---|---| @@ -34,18 +34,18 @@ These resolve when TC3 dispatch fires. Listed here for handoff continuity: |---|---|---| | TC1 | T-Substrate-Lens-Primitive + lens producer retirement | Substrate Manager + PB Manager continuations | | TC2 | Second executable evaluation strategy | R3 Evaluator residual (post-R2-Evaluator close) | -| TC3 | B5 audit + T-Substrate-Lens-Primitive + substrate-fact-introduction | PB Manager (B5) + Substrate Manager + this lane (introduction authorship) | +| TC3 | B5 audit + T-Substrate-Lens-Primitive + substrate-fact-introduction | PB Manager (B5) + Substrate Manager + this bundle (introduction authorship) | ## Cadence - **No active worker dispatch** until at least one TC's strict-fire prerequisites land. - **Audit cadence** — bundled with bridge-ledger audit; refresh status table at each manager-brief PR. -- **TC3 dispatch trigger** — when both B5 and T-Substrate-Lens-Primitive are green, this lane authors a TC3 substrate-introduction worker brief (~3-5 days research-tier per PM Tier C estimate). +- **TC3 dispatch trigger** — when both B5 and T-Substrate-Lens-Primitive are green, this bundle authors a TC3 substrate-introduction worker brief (~3-5 days research-tier per PM Tier C estimate). ## Explicitly out of scope -- **TC1 substrate-research authoring** — Substrate Manager continuation owns T-Substrate-Lens-Primitive; this lane only consumes the strengthening signal. -- **TC2 second-strategy implementation** — R3 Evaluator residual (per [`r2-closure-ledger.md`](../r2-closure-ledger.md) Evaluator row); this lane only consumes the strengthening signal. +- **TC1 substrate-research authoring** — Substrate Manager continuation owns T-Substrate-Lens-Primitive; this bundle only consumes the strengthening signal. +- **TC2 second-strategy implementation** — R3 Evaluator residual (per [`r2-closure-ledger.md`](../r2-closure-ledger.md) Evaluator row); this bundle only consumes the strengthening signal. - **TC3 declaration content** — already authored in [`r3-pb-t-fixedpoint-worker.md`](r3-pb-t-fixedpoint-worker.md) L145-215 (PB-authored declarative shape). This lane authors the substrate path + fixture, NOT the declaration text per L181-185 ownership-transition contract. - **L4 / L5 / L7 verification claims** — Lanes 1 + 2 of this manager. From aded18625bc5ff8ac233030e8df77d98a4bc7cc9 Mon Sep 17 00:00:00 2001 From: Brian Searls Date: Thu, 30 Apr 2026 18:32:00 +0000 Subject: [PATCH 7/9] docs(r3): align acceptance gates with r3-structure.md authority MIME-Version: 1.0 Content-Type: text/plain; charset=UTF-8 Content-Transfer-Encoding: 8bit Lane 1 brief had: - Slice 3 narrowing L7 to "at least one named law" (weakened the closure bar vs r3-structure.md L54 which requires every algebra × every applicable law). - Single made-up gate name verification_l4_l7_direct_per_target_equivalence_landed parallel to the authoritative l4_emit_eval_match + l7_algebraic_laws_witnessed pair (single-authority drift per INVARIANTS §P2). Lane 2 brief similarly used made-up verification_l5_cross_target_consistency_landed parallel to authoritative l5_cross_target_consistency. Manager brief acceptance section restated to cite both authority gates for Lane 1 + L5 authority gate for Lane 2; explicit "partial-coverage early slices do NOT close the lane" framing. Slice 3 in Lane 1 now explicitly marked as coverage-seed only with closure gate referring to full r3-structure.md authority. Co-Authored-By: Claude Opus 4.7 (1M context) --- docs/briefs/r3-v-l4-l7-direct-worker.md | 13 ++++++++----- docs/briefs/r3-v-l5-corpus-worker.md | 4 +++- docs/briefs/r3-verification-manager.md | 4 ++-- 3 files changed, 13 insertions(+), 8 deletions(-) diff --git a/docs/briefs/r3-v-l4-l7-direct-worker.md b/docs/briefs/r3-v-l4-l7-direct-worker.md index 98afcfbae5a..39dac45098d 100644 --- a/docs/briefs/r3-v-l4-l7-direct-worker.md +++ b/docs/briefs/r3-v-l4-l7-direct-worker.md @@ -25,13 +25,16 @@ Per-target equivalence harness for the **L4** (emit/eval match) + **L7** (algebr 1. **Slice 1 — single-target L4 receipt:** one `TestClaim` using `TestPredicate::DifferentialEquals` comparing Rust emit-target output vs `.dag` eval result on a minimal corpus program. Fixture: `src/v3/compiler/tests/fixtures/r3_verification_l4_direct_rust.dag` (proposed). Suite: `r3_verification_l4_direct_suite`. 2. **Slice 2 — multi-target L4:** add per-target receipts as Python / Go grounding lands. Each target adds one `DifferentialEquals` row using existing predicate; no new `TestPredicate` variants. -3. **Slice 3 — L7 algebraic-law witness:** use `TestPredicate::AlgebraicLaw` (already on substrate at `src/v3/std/verification.dag` L189; `AlgebraicLawKind` enum L103) for at least one named law (associativity / commutativity / identity) per the lens-framework I4 + I9 TestClaims. +3. **Slice 3 — L7 algebraic-law witness (early slice; does NOT close Lane 1):** use `TestPredicate::AlgebraicLaw` (already on substrate at `src/v3/std/verification.dag` L189; `AlgebraicLawKind` enum L103) for at least one named law (associativity / commutativity / identity) per the lens-framework I4 + I9 TestClaims. **This is a coverage-seed slice only.** L7 closure per [`docs/r3-structure.md`](../r3-structure.md) L54 (`l7_algebraic_laws_witnessed`) requires every algebra declared in `dsl/std/algebra.dag` to have a runtime-constructed witness for **each of its applicable laws** (associativity, commutativity, identity, distributivity). Subsequent slices grow to full coverage; Lane 1 closure gate is the full r3-structure.md authority, not the seed. -## Structural acceptance — `.dag` hook +## Structural acceptance — `.dag` hooks (per [`r3-structure.md`](../r3-structure.md) L53-54 authority) -| Gate name | Fixture (proposed) | Suite | -|---|---|---| -| `verification_l4_l7_direct_per_target_equivalence_landed` | `src/v3/compiler/tests/fixtures/r3_verification_l4_l7_direct.dag` | `r3_verification_l4_l7_direct_suite` | +| Gate name | Authority | Fixture (proposed) | Suite | +|---|---|---|---| +| `l4_emit_eval_match` | `r3-structure.md` L53 — every `.dag` program in the certification corpus has emitted target output equal to `.dag` evaluation output (algebraic equality, not byte-equal) | `src/v3/compiler/tests/fixtures/r3_verification_l4_emit_eval_match.dag` | `r3_verification_l4_l7_direct_suite` | +| `l7_algebraic_laws_witnessed` | `r3-structure.md` L54 — every algebra in `dsl/std/algebra.dag` has a runtime-constructed witness for each applicable law (associativity, commutativity, identity, distributivity); `AlgebraicLaw` `TestPredicate` evaluates via Evaluator-constructed witnesses, not host-mediated harness | `src/v3/compiler/tests/fixtures/r3_verification_l7_algebraic_laws.dag` | `r3_verification_l4_l7_direct_suite` | + +Both gates close under Lane 1; partial-coverage early slices (slice 1 single-target / slice 3 single-law seed) do NOT satisfy these gates and do NOT close the lane. **Stability invariant** (per [`r2-pr-d-cross-target-equivalence-harness-primitives.md`](r2-pr-d-cross-target-equivalence-harness-primitives.md) §"Deferred fixture path"): the **claim name** stays stable; only update fixture-module path with manager-brief + integration-test co-update in one PR. diff --git a/docs/briefs/r3-v-l5-corpus-worker.md b/docs/briefs/r3-v-l5-corpus-worker.md index 9ae68a9d74e..a00d74a5e38 100644 --- a/docs/briefs/r3-v-l5-corpus-worker.md +++ b/docs/briefs/r3-v-l5-corpus-worker.md @@ -30,7 +30,9 @@ L6 form coverage is **explicitly out of scope** — moved to R2-T-Ground-CrossTa | Gate name | Fixture (proposed) | Suite | |---|---|---| -| `verification_l5_cross_target_consistency_landed` | `src/v3/compiler/tests/fixtures/r3_verification_l5_corpus.dag` | `r3_verification_l5_corpus_suite` | +| `l5_cross_target_consistency` | `src/v3/compiler/tests/fixtures/r3_verification_l5_corpus.dag` | `r3_verification_l5_corpus_suite` | + +Per [`r3-structure.md`](../r3-structure.md) L56 authority — for every `.dag` program, emitted Rust/Python/Go produce equivalent runtime behavior on the certification corpus. **Stability invariant** (per [`r2-pr-d-cross-target-equivalence-harness-primitives.md`](r2-pr-d-cross-target-equivalence-harness-primitives.md) §"Deferred fixture path"): keep the **declaration name** stable; only update fixture-module path with manager-brief + integration-test co-update in one PR. diff --git a/docs/briefs/r3-verification-manager.md b/docs/briefs/r3-verification-manager.md index f79364756ce..88ba2cb8b64 100644 --- a/docs/briefs/r3-verification-manager.md +++ b/docs/briefs/r3-verification-manager.md @@ -79,8 +79,8 @@ Per [`docs/r3-structure.md`](../r3-structure.md) L98 distribution map; cross-che Each lane closes under a structural acceptance gate authored as a `.dag` `TestClaim`: -- **Lane 1**: `verification_l4_l7_direct_per_target_equivalence_landed` — per-target `DifferentialEquals` receipts on the certification corpus; emit-target output vs `.dag` eval result match for each Shape A target. -- **Lane 2**: `verification_l5_cross_target_consistency_landed` — Rust / Python / Go equivalent runtime behavior on the certification corpus (algebraic equivalence over computational results, not byte identity). +- **Lane 1**: closes under both `l4_emit_eval_match` (per [`r3-structure.md`](../r3-structure.md) L53 — every `.dag` program in certification corpus has emit-target output equal to `.dag` eval output, algebraic equality) AND `l7_algebraic_laws_witnessed` (per [`r3-structure.md`](../r3-structure.md) L54 — every algebra × every applicable law has a runtime-constructed witness via `AlgebraicLaw` `TestPredicate`). Partial-coverage early slices do NOT close the lane; full coverage required. +- **Lane 2**: `l5_cross_target_consistency` (per [`r3-structure.md`](../r3-structure.md) L56) — for every `.dag` program, emitted Rust/Python/Go produce equivalent runtime behavior on the certification corpus (algebraic equivalence over computational results, not byte identity). - **Absorbed responsibility (TC bundle)**: TC1/TC2/TC3 strict-fire activation across the three deferred-claim fixtures (TC3 fixture authored under substrate path) — tracked via audit cadence, not as a lane-close gate. - **Ledger gate**: `bridge_retirement_ledger_zero` — unified ledger reports 0 named identity bridges remaining (per [`r3-structure.md`](../r3-structure.md) L84). From 02ca1f29ed032ee9ff6b8bf5978319e91d12f6c1 Mon Sep 17 00:00:00 2001 From: Brian Searls Date: Thu, 30 Apr 2026 19:08:25 +0000 Subject: [PATCH 8/9] docs(r3): unify TC3 strict-fire gate into single two-stage authority MIME-Version: 1.0 Content-Type: text/plain; charset=UTF-8 Content-Transfer-Encoding: 8bit TC3 status table named only substrate-introduction prerequisites under "Strict-fire gate" while §Acceptance separately required T-FixedPoint completion for strict-fire. Two competing gate descriptions for one claim violated single-authority discipline. Restate as a single two-stage gate: (a) substrate-introduction prereqs land tc3_strong_normalization_substrate_introduced (b) T-FixedPoint completion fires the full theorem witness Both stages required; no fire-before-(b) path exists. Stage names match §Acceptance authority below. Co-Authored-By: Claude Opus 4.7 (1M context) --- docs/briefs/r3-v-formal-grounding-tc-bundle.md | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/docs/briefs/r3-v-formal-grounding-tc-bundle.md b/docs/briefs/r3-v-formal-grounding-tc-bundle.md index 60661b6f80c..d8dd6bb4fd4 100644 --- a/docs/briefs/r3-v-formal-grounding-tc-bundle.md +++ b/docs/briefs/r3-v-formal-grounding-tc-bundle.md @@ -12,7 +12,7 @@ Manage the three formal-grounding `TestClaim` author-now-fire-later commitments |---|---|---|---| | **TC1** | η-equivalence (substrate-lens research) | **Author-now-fire-later landed** — fixture `src/v3/compiler/tests/fixtures/tc1_substrate_lens_eta_equivalence_deferred.dag` via #1179; uses `SubstrateResearchDeferredClaim` carrier (runner-valid only for this fixture per [`r2-closure-ledger.md`](../r2-closure-ledger.md) L220). | T-Substrate-Lens-Primitive landing + lens producer retirement (per [`r2-closure-ledger.md`](../r2-closure-ledger.md) §216 ratification). | | **TC2** | Church-Rosser / evaluation-order independence | **Slice-0 hook landed** — fixture `src/v3/compiler/tests/fixtures/tc2_evaluation_order_independence_deferred.dag` (per [`r2-evaluator-manager.md`](r2-evaluator-manager.md) L127); current predicate is deferred (`Compiles`-shaped). | **R3-deferred from R2-Evaluator** — needs ≥2 executable strategies. PR-B.1 lands a single eager strategy per [`r2-pr-b-body-evaluator-eager-baseline.md`](r2-pr-b-body-evaluator-eager-baseline.md) L154; second strategy is R3 residual. Strengthens to strict strategy-output equality over `DimensionReport`. | -| **TC3** | Strong normalization (meta-theorem over well-typed fragment) | **Text-form only** in [`r3-pb-t-fixedpoint-worker.md`](r3-pb-t-fixedpoint-worker.md) L145-215; no fixture. **Substrate-encoding gap** — every existing `TestPredicate` variant is per-program; TC3 is a meta-theorem universally quantified across all well-typed programs. No existing variant carries that quantifier shape (per L171 of that brief). | **Substrate-fact-introduction via [`INVARIANTS.md`](../../INVARIANTS.md) §P1** + B5 audit + T-Substrate-Lens-Primitive (provides the `Lens` shape TC3's evaluation-step witness consumes). Ownership transitions PB→Verification per L181-185 of `r3-pb-t-fixedpoint-worker.md`. | +| **TC3** | Strong normalization (meta-theorem over well-typed fragment) | **Text-form only** in [`r3-pb-t-fixedpoint-worker.md`](r3-pb-t-fixedpoint-worker.md) L145-215; no fixture. **Substrate-encoding gap** — every existing `TestPredicate` variant is per-program; TC3 is a meta-theorem universally quantified across all well-typed programs. No existing variant carries that quantifier shape (per L171 of that brief). | **Two-stage gate (single authority — both stages required for strict-fire):** (a) **Substrate-introduction prerequisites:** [`INVARIANTS.md`](../../INVARIANTS.md) §P1 substrate-fact-introduction + B5 audit + T-Substrate-Lens-Primitive (provides the `Lens` shape TC3's evaluation-step witness consumes). Stage (a) lands `tc3_strong_normalization_substrate_introduced` per §Acceptance below. (b) **Strict-fire:** T-FixedPoint completion (termination semantics) — only after stage (a) lands. Ownership transitions PB→Verification per L181-185 of `r3-pb-t-fixedpoint-worker.md`. **No fire-before-(b) path exists** — stage (a) lands the substrate path + fixture only; full theorem witnessing requires (b). | ## Owned deliverables From 55566b11e9846ac4fcce13a1328d3c277250b3e9 Mon Sep 17 00:00:00 2001 From: Brian Searls Date: Thu, 30 Apr 2026 19:55:16 -0400 Subject: [PATCH 9/9] WIP: R3 Verification --- ...ected-dag-structural-assertion-analysis.md | 156 ++++++++++++++++++ 1 file changed, 156 insertions(+) create mode 100644 docs/briefs/r3-v-reflected-dag-structural-assertion-analysis.md diff --git a/docs/briefs/r3-v-reflected-dag-structural-assertion-analysis.md b/docs/briefs/r3-v-reflected-dag-structural-assertion-analysis.md new file mode 100644 index 00000000000..ecc8e4a244d --- /dev/null +++ b/docs/briefs/r3-v-reflected-dag-structural-assertion-analysis.md @@ -0,0 +1,156 @@ +# R3 Verification — Reflected-Dag Structural Assertion Analysis + +**Status:** PROPOSAL / research-only, updated after Director producer-first +ratification (#828 c4356368827). This brief does not edit substrate or assign +implementation. Substrate-fact introduction remains routed through +`INVARIANTS.md` §P1 and the Substrate Manager. + +## Scope + +Director surfaced a repeated acceptance-test pattern: new bootstrap carriers +land with hand-Rust tests that inspect the regenerated Dag for type, field, +variant, reference, and row-list shape. SG-0 already names the dissolution +target for several files as `.dag` `TestClaim` coverage for reflected-Dag +structural assertions over `std/` types. This brief asks what capability would +let those checks move out of bespoke Rust without pretending the substrate +change is already authorized. + +The adjacent reflection input is `reflect_program_dag_nodes_in_file` in +`lens_apply.rs`, locked by `docs/design-reflection-completeness.md`. That +function reflects program-Dag `Behavior` nodes into `FieldValue`; it is useful +input precedent, not proof that structural assertions are already first-class +`.dag` claims. + +## Candidate Capability Shape + +A research-tier capability could be named `ReflectedDagAssert`, +`DagShapeAssert`, or similar. The important shape is not the name: + +- **Observed carrier:** a reflected bootstrap Dag or source-file-scoped Dag + carrier, produced by the same authority family as + `reflect_program_dag_nodes_in_file` once reflection is generated rather than + hand-Rust. +- **Assertion program:** structural atoms such as `type X exists`, `type X is + Conj with exactly fields [a, b]`, `field X.a points at declaration Y`, + `type S is Disj with variants [A, B]`, `data row R instantiates T`, `row + field f is a Reference`, and `no declaration in file F has value_body`. +- **Result:** pass/fail with diagnostics naming the missing or surplus + structural element, e.g. `Operation.inputs expected Map` + or `MethodTemplateContract row 3 duplicate dag_method`. +- **Non-goal:** evaluating the reflected program. This is static Dag-shape + inspection, not L4 target-vs-eval output parity and not L5 cross-target + runtime behavior. + +The atoms need exact-set forms, not only existence checks. Most current Rust +tests are ratchets against unauthorized growth as much as unauthorized absence. + +## Producer Plus Comparison Shell + +Director ratified the producer-first framing at #828 c4356368827: the missing +substrate fact is a Substrate-authored `Lens` producer, not a +new Verification-owned predicate variant. The producer projects a reflected Dag +into a structural `DagShapeReport`; the already-ratified +`BinaryDimensionReportEquals` predicate is the consumer/comparison shell. + +That resolves the earlier unary-versus-binary tension without hiding it. A +raw Dag-shape assertion is a unary query over declarations and rows, while +`BinaryDimensionReportEquals` compares two `DimensionReport` outputs. The +load-bearing move is to make shape-query output a first-class report. Once +that producer exists, expected-shape reports, Rust-extracted shape reports, +and `.dag`-reflected shape reports all compare through the same binary shell. + +The unified predicate now has four reflection-aware modifier roles: +TC1 eta, TC2 strategy-order, TC3 evaluation-step, and shape-report. Verification +consumes that surface; Substrate owns the producer and any substrate carrier +introduction. + +## RustDagIsomorphism Adjacency + +The dispatch cites a Substrate-side `RustDagIsomorphism` proposal from the +ROADMAP 2026-04-30 debt row. The live `ROADMAP.md` on this branch exposes the +older 2026-04-25 reflection debt section and SG-0 comments naming reflected-Dag +structural assertions; it does not contain the exact `RustDagIsomorphism` token +or 2026-04-30 heading. + +Conceptually, these are adjacent but not identical: + +- `RustDagIsomorphism` sounds like whole-Dag equivalence between a Rust-emitted + or Rust-reflected Dag and a `.dag` authority. +- `ReflectedDagAssert` is a query/assertion surface over selected declarations, + fields, variants, rows, and absence constraints. + +Director's producer-first disposition also collapses `RustDagIsomorphism` into +the same consumer pattern: extract one `DagShapeReport` from Rust enum/source +shape, extract another from `.dag` reflection, then compare them through +`BinaryDimensionReportEquals`. That keeps isomorphism from becoming a parallel +predicate authority while preserving its purpose as a mirror-drift gate. + +## Migration Audit + +| Hand-Rust acceptance | Fit | Notes | +|---|---:|---| +| `anthropic_schema_lockstep_test.rs` | Partial | V3 mirror checks over `Anthropic*` records/sums fit. The v2-source extraction and lockstep comparison against `dsl/extdeps/llm/anthropic.dag` is cross-source schema diffing, not just reflected bootstrap shape. The "no data rows or fns" leak check fits. | +| `canonical_lens_bridge_ratchet_test.rs` | No | This is a Rust-source ratchet over `test_runner.rs`: `include_str!` constants, `lens_decl.name` equality arms, and generic name lookups. It dissolves via PB-Runtime or a lens registry carrier, not Dag-shape assertion. | +| `lens_substrate_carrier_test.rs` | Strong | Exact field sets for `Lens`, `Diagnostic.kind`, closed-sum variants for `CompilerDiagnosticKind` / `AnyDiagnosticKind`, and single-field `LensInstanceKindWitness` are canonical structural atoms. | +| `method_registry_test.rs` | Partial-strong | `MethodDeclaration` and `MethodRef` shapes fit directly. Registry coverage over names scraped from `dsl/std/algebra.dag` requires either a structural source for those template names or a cross-source expected-set input; otherwise the current lexical extraction remains outside the capability. | +| `method_template_contract_test.rs` | Strong | Distinct declaration IDs, disjoint field sets, forbidden fields, `MethodEmitTemplate` variants, per-target row-list uniqueness, and higher-order row payload shapes are good examples for exact-set, reference, variant, and list uniqueness atoms. | +| `services_carrier_shape_test.rs` | Strong | `Operation`, `InputField`, `RestEndpointBinding`, `CallableRef`, `Map`, path authority, and "no data rows in services.dag" are direct structural assertions. | +| `workflow_root_port_test.rs` | Partial | The `WorkflowRoot` carrier shape would fit, but the live tests assert `Dag::workflow_root_port()` behavior over compiled fixtures. That is accessor semantics, not merely reflected declaration shape. A future claim might express compile-and-fold structure, but not this basic shape predicate alone. | + +TC1's deferred fixture test is adjacent but separate: it verifies +`SubstrateResearchDeferredClaim` runner scoping, not a generic Dag-shape claim. + +## Research Finding + +The highest-value slice is the shared reflected-Dag query/report producer: +`Lens`. It carries exact-set and absence-sensitive structural +facts in a reusable report form. `BinaryDimensionReportEquals` remains the +comparison shell; it should not be treated as the producer. + +This matters for migration discipline. The old hand-Rust tests combine two +concerns: deriving shape facts from a live Dag, and comparing those facts to +an expected shape. The Director-ratified split makes the derivation a +Substrate-owned producer and the comparison a Verification-consumed predicate +instance. That avoids both a bespoke `ReflectedDagAssert` predicate and a +parallel `RustDagIsomorphism` authority. + +## Coordination Signal + +Director-ratified outcome (#828 c4356368827): + +- Substrate authors the single `Lens` producer. +- Verification consumes `BinaryDimensionReportEquals` with the new + shape-report modifier as the comparison shell. +- `RustDagIsomorphism` becomes a consumer instance comparing two + `DagShapeReport` outputs, not a separate predicate family. + +Follow-up dispatch should therefore target the producer shape and report +schema under Substrate ownership. Verification work should describe required +coverage and diagnostics, not author a competing predicate. + +## Reflection-Completeness Residual + +Lane 1 consumers under T-V-L4-L7-Direct should not treat post-#1170 reflection +completeness as a full substrate proof. The live implementation still routes +through hand-Rust `lens_apply.rs::substrate_reflection::reflect_behavior_list`, +even though `docs/design-reflection-completeness.md` locks the intended full +`Behavior` shape. + +That matters for L4/L7 standby implementation: a claim that consumes +`reflect_program_dag_nodes_in_file` can rely on the documented structural +contract, but closure should wait for a generated conformance walker or +Evaluator-backed substrate projection that proves every nested `FieldValue` +tree follows the declared substrate shape. Until then, reflection completeness +is a strong hand-Rust acceptance surface, not a mechanical theorem. + +The live ROADMAP reflection row is `ROADMAP.md` §"Post-merge debt +(2026-04-25 reflective + exploratory analyses)" / "Lossy user-lens reflection +vs full substrate"; Director's #828 c4356309499 records the newer residual +routing. This note is consumer-side awareness only. + +## Non-Claims + +- No substrate edit is authorized here. +- No hand-Rust test is declared obsolete until the generated `.dag` claim path + exists and each migrated acceptance surface has an equivalent diagnostic. +- No L4/L5/L7 lane is closed by this research note.