From ec3fb8278ac82e05e384981e82fd424579b9076e Mon Sep 17 00:00:00 2001 From: Brian Searls Date: Wed, 29 Apr 2026 23:36:08 +0000 Subject: [PATCH] docs(briefs): post-merge line-citation + status-row audit Audit pass per manager dispatch (#1133 inbox 4348240942) over the 5 merged R2 Grounding briefs after the morning's regression+refactor cycle (#1187 / #1195 / #1196 / #1206 / #1218 / #1220 / #1229). Findings: - Status rows in r2-grounding-manager.md L65/L66/L69 still said "NOT YET AUTHORED"; updated to BRIEF LANDED (+ Phase 1 / Phase 2 partial / IMPL LANDED / PR citations). - Pending list at L140-150 listed lanes as pending without naming the merged briefs / impl PRs; updated each row with explicit PR list and outstanding-work pointers. - INVARIANTS.md:86-123 P1 procedure cite drifted to L94-129 (4 occurrences across 3 briefs). - emit_model.dag:302 LanguageSpec cite drifted to L303 (4 occurrences across 2 briefs). - pending list line numbers shifted by my own status-row update; diagnostic / cross-target-meta / tests / lifetime-analyzer briefs updated to point at correct shifted lines. No structural drift requiring escalation. Co-Authored-By: Claude Opus 4.7 (1M context) --- docs/briefs/r2-grounding-manager.md | 20 ++++++++++---------- docs/briefs/t-ground-cross-target-meta.md | 4 ++-- docs/briefs/t-ground-diagnostic.md | 4 ++-- docs/briefs/t-ground-languagespec.md | 10 +++++----- docs/briefs/t-ground-lifetime-analyzer.md | 4 ++-- docs/briefs/t-ground-tests.md | 8 ++++---- 6 files changed, 25 insertions(+), 25 deletions(-) diff --git a/docs/briefs/r2-grounding-manager.md b/docs/briefs/r2-grounding-manager.md index a13c6a0193d..646e90d5e1f 100644 --- a/docs/briefs/r2-grounding-manager.md +++ b/docs/briefs/r2-grounding-manager.md @@ -62,11 +62,11 @@ The 8-question design dialogue resolved into a cadence whose merge gates worker | T-Ground-Python | L | **PARTIALLY LANDED** — `dsl/extdeps/languages/python/primitives.dag` landed via #1080 (lively-wolf-462); remainder fill queue / gated on PR-G | Python primitive declarations | | T-Ground-Go | L | **PARTIALLY LANDED** — `go/primitives.dag` spec tranche 1 landed (`ac765ce10`); additional Go primitives via #1046 (bright-otter-594); remainder fill queue / gated on PR-H | Go primitive declarations | | **T-Ground-Coercion-Fold** *(NEW; replaces engine framing)* | S | **PRE-CASCADE FOOTPRINT LANDED** via PR #989 + commit `c0cc8b260` (Phase 2 pilot-list enumeration slice 1; mirror-consistency probe). Per `design-emission-model.md` §"Affected lanes" option (c): hold further engine-framed slices + queue cleanup wave once LanguageSpec lands. Future slices gated on PR-F + Substrate ValueBody-list/sum | Refinement composition as structural fold over substrate facts | -| **T-Ground-LanguageSpec** *(NEW)* | M | NOT YET AUTHORED — **gated on PR-I merge** | Structured language-spec substrate; absorbs Reflective Pattern E retirement; per-primitive `RealizationCost` | -| **T-Ground-Lifetime-Analyzer** *(NEW; no annotations)* | M | NOT YET AUTHORED | Structural ownership/lifetime derivation from program use | -| **T-Ground-Diagnostic** *(NEW)* | S | **BRIEF LANDED** — [`t-ground-diagnostic.md`](t-ground-diagnostic.md) | Declared structural ordering for diagnostic enumeration; `EmissionDiagnostic` carrier (implementation pending) | -| **T-Ground-CrossTarget-Meta** *(NEW)* | S | **BRIEF LANDED** — [`t-ground-cross-target-meta.md`](t-ground-cross-target-meta.md); **implementation gated on PR-J merge (likely no-op)** | Cross-target uniformity meta-spec; owns L6 per-(form × target) load-completeness check | -| T-Ground-Tests | S | NOT YET AUTHORED | L4 routing correctness verification | +| **T-Ground-LanguageSpec** *(NEW)* | M | **BRIEF LANDED** — [`t-ground-languagespec.md`](t-ground-languagespec.md) (#1168 + nits #1172 + rename #1174); **PHASE 1 LANDED** (registry-backed row population — Rust 9 + Python 18 + Go 13 rows via #1195 + hot-fix #1196); **PHASE 2 PARTIAL** (dead `MethodTranslation` × 3 retired via #1210 + ROADMAP closure #1213); remaining emit-side authorities (`*_method_templates`, `rust_simple_method_specs`, `rust_method_wraps_result`) deferred to Pure-Bootstrap-Zero / v2 retirement per audit. Phase 1.5 (Rust higher-order rows; gated on Substrate `MethodEmitTemplate` sum) + B (`RealizationCost` per-primitive; gated on PR-I) outstanding. | Structured language-spec substrate; absorbs Reflective Pattern E retirement; per-primitive `RealizationCost` | +| **T-Ground-Lifetime-Analyzer** *(NEW; no annotations)* | M | **BRIEF LANDED** — [`t-ground-lifetime-analyzer.md`](t-ground-lifetime-analyzer.md) (#1177); **IMPL LANDED** — R2 scope (a)/(b)/(c) (#1206) + fail-closed Dag-extraction fix (#1218) + path-prefix authority transitional-staging note (#1220) | Structural ownership/lifetime derivation from program use | +| **T-Ground-Diagnostic** *(NEW)* | S | **BRIEF LANDED** — [`t-ground-diagnostic.md`](t-ground-diagnostic.md) (#1216); implementation pending | Declared structural ordering for diagnostic enumeration; `EmissionDiagnostic` carrier | +| **T-Ground-CrossTarget-Meta** *(NEW)* | S | **BRIEF LANDED** — [`t-ground-cross-target-meta.md`](t-ground-cross-target-meta.md) (#1224 + L6 form-axis anchor #1229); **implementation gated on PR-J merge (likely no-op)** | Cross-target uniformity meta-spec; owns L6 per-(form × target) load-completeness check | +| T-Ground-Tests | S | **BRIEF LANDED** — [`t-ground-tests.md`](t-ground-tests.md) (#1223); implementation pending — gated on Q4 lock (PR-I) + Coercion-Fold body | L4 routing correctness verification | | T-Ground-Dissolve | S | NOT YET AUTHORED | Track-13 dissolution: delete `TypeCheckpoint` / `InhabitantDecl` / `carrier: String` | ## Cross-program dependencies @@ -140,11 +140,11 @@ Authored: Pending — post-spawn manager-authored autonomously: - T-Ground-Rust full implementation (gated on PR-F) - T-Ground-Coercion-Fold Phase 2 implementation (gated on PR-F + Substrate ValueBody-list/sum) -- T-Ground-LanguageSpec (gated on PR-I; absorbs target primitive/range duplication retirement) -- T-Ground-Lifetime-Analyzer (M; structural ownership/lifetime derivation) -- T-Ground-Diagnostic (S) — brief [`t-ground-diagnostic.md`](t-ground-diagnostic.md) -- T-Ground-CrossTarget-Meta (S; gated on PR-J no-op confirmation) — brief [`t-ground-cross-target-meta.md`](t-ground-cross-target-meta.md) -- T-Ground-Tests +- T-Ground-LanguageSpec brief + Phase 1 + Phase 2 partial — **LANDED** (#1168 + #1172 + #1174 + #1195 + #1196 + #1210 + #1213); Phase 1.5 (Rust higher-order; gated on Substrate `MethodEmitTemplate` sum) + B (`RealizationCost` per-primitive; gated on PR-I) outstanding +- T-Ground-Lifetime-Analyzer brief + R2 scope (a)/(b)/(c) impl — **LANDED** (#1177 + #1206 + #1218 + #1220); R3 scope (d)/(e)/(f) closures/async/Pin folds into R3 `T-LensProducer-Retirement` +- T-Ground-Diagnostic (S) — brief [`t-ground-diagnostic.md`](t-ground-diagnostic.md) **LANDED** (#1216); implementation pending +- T-Ground-CrossTarget-Meta (S; gated on PR-J no-op confirmation) — brief [`t-ground-cross-target-meta.md`](t-ground-cross-target-meta.md) **LANDED** (#1224 + #1229); implementation pending +- T-Ground-Tests (S) — brief [`t-ground-tests.md`](t-ground-tests.md) **LANDED** (#1223); implementation pending — gated on Q4 (PR-I) + Coercion-Fold body - T-Ground-Dissolve (Track-13 cleanup) - T-Ground-Python - T-Ground-Go diff --git a/docs/briefs/t-ground-cross-target-meta.md b/docs/briefs/t-ground-cross-target-meta.md index 2269abe785a..3c755087267 100644 --- a/docs/briefs/t-ground-cross-target-meta.md +++ b/docs/briefs/t-ground-cross-target-meta.md @@ -2,12 +2,12 @@ **Status:** PROPOSAL — **brief authoring dispatchable now** (per R2 Grounding Manager inbox #1203 / #1133, 2026-04-29). **Implementation gated** on **PR-J** merge with **Q5 no-op confirmation** (cardinality-as-connectives axis already collapsed via PR-PreF `Interval`; PR-J is the single cadence trigger before worker impl dispatch). -**Lane:** T-Ground-CrossTarget-Meta (S) — item **9** of 11 in [`r2-grounding-manager.md`](r2-grounding-manager.md) (lane description line 35, lane row line 68, pending list line 145). +**Lane:** T-Ground-CrossTarget-Meta (S) — item **9** of 11 in [`r2-grounding-manager.md`](r2-grounding-manager.md) (lane description line 35, lane row line 68, pending list line 146). **Manager:** R2 Grounding Manager ([`r2-grounding-manager.md`](r2-grounding-manager.md)). **Lineage / authorities consumed (no re-litigation):** -- R2 manager lane row + cadence row + acceptance gate: [`r2-grounding-manager.md`](r2-grounding-manager.md) lines 35, 52 (PR-J → this lane), 68, 128 (`cross_target_meta_l6_load_completeness_landed`), 145. +- R2 manager lane row + cadence row + acceptance gate: [`r2-grounding-manager.md`](r2-grounding-manager.md) lines 35, 52 (PR-J → this lane), 68, 128 (`cross_target_meta_l6_load_completeness_landed`), 146. - Modeling problem 7 + L6 placement + cross-product shape: [`docs/design-emission-model.md`](../design-emission-model.md) — search **Cross-target uniformity**, **Modeling problem 7**, **L6**, **`l6_structural_form_coverage`**, **Shape A**, **connectives × behaviors × targets**, Q5 / cardinality-as-connectives (lines ~1243–1280, ~408–410, ~818–833, ~959). - **Not-a-lens authority:** [`docs/design-lens-framework.md`](../design-lens-framework.md) §**D3 / I6** — L6 is **not** a `Lens` instance; input space is **per-(substrate form cell × Shape A target)**, not `Lens.read: (Dag, Behavior) → Witness`. - Q1 / PR-PreF consolidation: `Interval` parent; cardinality on connectives as `Interval` (`design-emission-model.md` ~1019–1024, ~1038, ~1265–1268). **L6 row/column substrate authority** (P2): **`TypeConnective`** + **`Behavior`** in [`src/v3/std/substrate.dag`](../../src/v3/std/substrate.dag) — see §Scope (six + five variants). diff --git a/docs/briefs/t-ground-diagnostic.md b/docs/briefs/t-ground-diagnostic.md index b7004735fe0..347a3087fc6 100644 --- a/docs/briefs/t-ground-diagnostic.md +++ b/docs/briefs/t-ground-diagnostic.md @@ -2,12 +2,12 @@ **Status:** PROPOSAL — dispatchable now. Q6.5 two-layer diagnostic authority is **LIVE** on main via PR [#1129](https://github.com/gunb-ai/gunbc/pull/1129); this lane is a **Layer-1 consumer** of `CompilerDiagnosticKind` and does **not** widen that closed sum. Authored 2026-04-29 (R2 Grounding Manager redirect from sibling dispatch). -**Lane:** T-Ground-Diagnostic (S) — item **8** of 11 in [`r2-grounding-manager.md`](r2-grounding-manager.md) (lane description line 34, lane row line 67, pending list line 144). +**Lane:** T-Ground-Diagnostic (S) — item **8** of 11 in [`r2-grounding-manager.md`](r2-grounding-manager.md) (lane description line 34, lane row line 67, pending list line 145). **Manager:** R2 Grounding Manager ([`r2-grounding-manager.md`](r2-grounding-manager.md)). **Lineage / authorities consumed (no re-litigation):** -- R2 manager lane row + acceptance gate: [`r2-grounding-manager.md`](r2-grounding-manager.md) lines 34, 67, 127 (`diagnostic_structural_ordering_landed`), 144. +- R2 manager lane row + acceptance gate: [`r2-grounding-manager.md`](r2-grounding-manager.md) lines 34, 67, 127 (`diagnostic_structural_ordering_landed`), 145. - Q6.5 two-layer authority: [`docs/design-lens-framework.md`](../design-lens-framework.md) §**"Q6.5 — Two-layer authority for diagnostic kinds"** — Layer 1 `CompilerDiagnosticKind` is Substrate-owned; **this lane consumes; does NOT extend**; anti-bridge: lens-instance kinds never enter `CompilerDiagnosticKind`. - Engine-reframe + fold failures: [`docs/design-emission-model.md`](../design-emission-model.md) — Modeling problems **4** (ordering is diagnostic-only; lines ~152–164) and **5** (fail-closed diagnostic surface; lines ~165–188); `EmissionDiagnostic` worked shapes (e.g. `UnderRefined`, `NoInhabitant`; search **EmissionDiagnostic** in that doc); lane table row ~386 (`T-Ground-Diagnostic` owns carrier + resolution-hint structure); **UnderRefined** worked receipts **Example 1** (bound / unrefined `Int`, lines ~417–464) **and Example 5** (algebra ambiguity, `unspecified_axis: "algebra"`, lines ~639–680) **plus** Example 6 as lifted test targets. - Fail-closed compilation: [`INVARIANTS.md`](../../INVARIANTS.md) **C-8** (P3) + C-series sentinels — no silent fabrication when the fold cannot determine. diff --git a/docs/briefs/t-ground-languagespec.md b/docs/briefs/t-ground-languagespec.md index 030d05b39fc..8c2d3d65e51 100644 --- a/docs/briefs/t-ground-languagespec.md +++ b/docs/briefs/t-ground-languagespec.md @@ -40,7 +40,7 @@ Author the `LanguageSpec` schema as `.dag` substrate. Per Modeling problem 6 (`d - **External-realization shape** — `Arrow.body` per E-9. - **Per-primitive `RealizationCost`** — see B below. -**Canonical home — existing type (P1-Step-1 DAG-ancestor receipt landed at brief-author time):** `LanguageSpec` is **already declared** at `src/v3/std/emit_model.dag:302` (12-field record carrying per-area `DeclarationRef` slots: statements / expressions / control_flow / literals / modules / functions / type_applications / type_definitions / record_derive_templates / patterns / collection_ops / values). A second declaration at `dsl/std/languages.dag:438` is a parallel-authority artifact predating the engine-reframe — its dissolution path is named below. **This lane EXTENDS the existing `src/v3/std/emit_model.dag` type; it does NOT author a new `language_spec.dag` file.** Author a new file only if Step 1 surfaces a structural reason the existing 12-field shape cannot host the engine-reframe additions; that decision escalates to manager (#1133) before any new file lands. +**Canonical home — existing type (P1-Step-1 DAG-ancestor receipt landed at brief-author time):** `LanguageSpec` is **already declared** at `src/v3/std/emit_model.dag:303` (12-field record carrying per-area `DeclarationRef` slots: statements / expressions / control_flow / literals / modules / functions / type_applications / type_definitions / record_derive_templates / patterns / collection_ops / values). A second declaration at `dsl/std/languages.dag:438` is a parallel-authority artifact predating the engine-reframe — its dissolution path is named below. **This lane EXTENDS the existing `src/v3/std/emit_model.dag` type; it does NOT author a new `language_spec.dag` file.** Author a new file only if Step 1 surfaces a structural reason the existing 12-field shape cannot host the engine-reframe additions; that decision escalates to manager (#1133) before any new file lands. **Extensions this lane lands on the existing type** (per Modeling problem 6, `design-emission-model.md:198-206`): - Primitive set with refinement-bound shape (Q1 `BoundDeclaration` consumer). @@ -52,9 +52,9 @@ Author the `LanguageSpec` schema as `.dag` substrate. Per Modeling problem 6 (`d - Per-primitive `RealizationCost` (B below; Q3 lock). - Consumer of Substrate-owned `MethodTemplateContract` (E below; rows attach to the LanguageSpec). Sibling to the existing cost/complexity `MethodContract` at `src/v3/std/algebra.dag:127` (independent authority; the two attach to method declarations as separate facts). -**Parallel-authority dissolution:** `dsl/std/languages.dag:438`'s `LanguageSpec` declaration + its `rust_spec` / `go_spec` / `python_spec` data items (lines 1244 / 1268 / 1292) converge with `src/v3/std/emit_model.dag:302` under one authority. If the two shapes have already drifted, this lane resolves the drift explicitly (no silent reconciliation) and lands the dissolution receipt in the PR body. If the shapes are reconcilable, T-Ground-Dissolve retires the duplicate; if they are not (i.e., `dsl/std/languages.dag` carries a structural fact `emit_model.dag` cannot absorb), escalate to manager (#1133) — that is itself a substrate-modeling call. +**Parallel-authority dissolution:** `dsl/std/languages.dag:438`'s `LanguageSpec` declaration + its `rust_spec` / `go_spec` / `python_spec` data items (lines 1244 / 1268 / 1292) converge with `src/v3/std/emit_model.dag:303` under one authority. If the two shapes have already drifted, this lane resolves the drift explicitly (no silent reconciliation) and lands the dissolution receipt in the PR body. If the shapes are reconcilable, T-Ground-Dissolve retires the duplicate; if they are not (i.e., `dsl/std/languages.dag` carries a structural fact `emit_model.dag` cannot absorb), escalate to manager (#1133) — that is itself a substrate-modeling call. -**P1 procedure receipts** (`INVARIANTS.md:86-123`): worker MUST cite which steps resolved each *new* field added to the existing type, in the PR body. Step 1 (DAG-ancestor) for the type itself is landed by this brief — the parent is `emit_model.dag`'s existing `LanguageSpec`. +**P1 procedure receipts** (`INVARIANTS.md:94-129`): worker MUST cite which steps resolved each *new* field added to the existing type, in the PR body. Step 1 (DAG-ancestor) for the type itself is landed by this brief — the parent is `emit_model.dag`'s existing `LanguageSpec`. ### B. Per-primitive `RealizationCost` (Q3 lock — `design-emission-model.md:1143-1208`) @@ -130,7 +130,7 @@ This is the load-bearing consequence of Q4's universal four-property gate (Faith ### G. Substrate-fact-introduction P1 procedure (per `INVARIANTS.md` §P1) -Worker MUST run the 3-step procedure (`INVARIANTS.md:86-123`) for every new substrate type / variant / field introduced under this lane and cite the receipts in the PR body: +Worker MUST run the 3-step procedure (`INVARIANTS.md:94-129`) for every new substrate type / variant / field introduced under this lane and cite the receipts in the PR body: - **Step 1 (DAG-ancestor):** which existing parent does the new fact attach to? (Worked example: `LanguageSpec` itself — does an ancestor target-spec carrier exist already?) - **Step 2 (Coproduct-vs-coordinate):** for each new sum, do all variants ever co-inhabit (→ record) or alternate (→ sum)? (`RealizationCost` is correctly a record — Q3 lock receipt; `BoundDeclaration` is correctly a sum — Q1 lock receipt.) - **Step 3 (Primitive-vs-lens-extensible):** for new leaves introduced under *this* lane's scope (e.g., `PlaceholderConvention` instances populated against the Substrate-owned `MethodTemplateContract` type), are they substrate primitives or lens-extensible labels? (Type-shape Step 1+2 receipts for `MethodTemplateContract` itself land on Substrate's PR per E above.) @@ -213,7 +213,7 @@ When this lane lands: - Heterogeneous per-target method authorities collapse to single `MethodTemplateContract` row per `(target, dag_method)`: Rust `SimpleMethodSpec` (record-list) + Python `python_method_templates` (map) + Go `go_method_templates` (map) on the emit side; `MethodTranslation` × 3 on the runtime side. `wraps_result` semantics resolved explicitly per target (not inherited from Rust). - Slice-1 mirror-consistency probe re-homes from `grounding_engine` to LanguageSpec's structural authority. - `extdeps/languages/{rust,python,go}/types.dag` table shape converges with `LanguageSpec` reflection (specifics depend on what schema authoring surfaces; if the table shape IS the LanguageSpec realization, the dissolution is in-place renaming + extension, not a separate file delete). -- **Parallel `LanguageSpec` authority retires:** `dsl/std/languages.dag:438`'s `LanguageSpec` declaration + its `rust_spec` / `go_spec` / `python_spec` data items (lines 1244 / 1268 / 1292) converge under the `src/v3/std/emit_model.dag:302` authority. Drift between the two shapes is resolved explicitly in this lane's PR (no silent reconciliation); structural facts not absorbable by the v3 shape escalate to manager (#1133) before any new file or split lands. +- **Parallel `LanguageSpec` authority retires:** `dsl/std/languages.dag:438`'s `LanguageSpec` declaration + its `rust_spec` / `go_spec` / `python_spec` data items (lines 1244 / 1268 / 1292) converge under the `src/v3/std/emit_model.dag:303` authority. Drift between the two shapes is resolved explicitly in this lane's PR (no silent reconciliation); structural facts not absorbable by the v3 shape escalate to manager (#1133) before any new file or split lands. The `coercion.dag` shape that retires is named per the receipt landed on PR — worker MUST cite the specific declarations dissolved (so the dissolution claim is verifiable, not aspirational, per `feedback_holistic_over_patches.md` + `feedback_root_causes_over_quick_fixes.md`). diff --git a/docs/briefs/t-ground-lifetime-analyzer.md b/docs/briefs/t-ground-lifetime-analyzer.md index a13967e152d..90dfaa588f6 100644 --- a/docs/briefs/t-ground-lifetime-analyzer.md +++ b/docs/briefs/t-ground-lifetime-analyzer.md @@ -2,7 +2,7 @@ **Status:** PROPOSAL — dispatchable now (no design-cadence gate; LanguageSpec ownership-axis declarations land alongside via lane 6, but lane authoring + skeleton don't block on PR-I). Authored 2026-04-29 in parallel to T-Ground-LanguageSpec row-population dispatch. -**Lane:** T-Ground-Lifetime-Analyzer (M) — item 7 of 11 in [`r2-grounding-manager.md`](r2-grounding-manager.md) (line 33 + lane row line 66 + planned-future line 143). +**Lane:** T-Ground-Lifetime-Analyzer (M) — item 7 of 11 in [`r2-grounding-manager.md`](r2-grounding-manager.md) (line 33 + lane row line 66 + planned-future line 144). **Manager:** R2 Grounding Manager ([`r2-grounding-manager.md`](r2-grounding-manager.md)). @@ -112,7 +112,7 @@ Every detectable under-determination / contradiction lands as a structured diagn ### G. Substrate-fact-introduction P1 procedure (per `INVARIANTS.md` §P1) -Worker MUST run the 3-step procedure (`INVARIANTS.md:86-123`) for every new substrate type / variant / field introduced under this lane and cite the receipts in the PR body: +Worker MUST run the 3-step procedure (`INVARIANTS.md:94-129`) for every new substrate type / variant / field introduced under this lane and cite the receipts in the PR body: - **Step 1 (DAG-ancestor):** `LifetimeFacts` and its component types (`Ownership`, `LifetimeScope`, `Growability`, `Encoding`) — does an ancestor structural-fact carrier already exist (e.g., is `Ownership` definable as inhabitance of some existing `Lattice` or algebra in `dsl/std/`)? Where to attach the fact: on `Binding` directly, on `Declaration`, or as a side-table? Default: structural attachment, cite receipt. - **Step 2 (Coproduct-vs-coordinate):** `LifetimeFacts` is a record (4 axes co-inhabit per binding); each axis (`Ownership` / `LifetimeScope` / etc.) is a sum (alternatives, not coordinates). Cite the worked-example substrate at `design-emission-model.md:534-546` as receipt. - **Step 3 (Primitive-vs-lens-extensible):** `Encoding` may be lens-extensible (per LanguageSpec axis vocabulary, which can grow as new targets land); `Ownership` / `LifetimeScope` / `Growability` are substrate primitives (every Shape-A target has these — they're computational primitives, not target-specific labels). diff --git a/docs/briefs/t-ground-tests.md b/docs/briefs/t-ground-tests.md index df5fdb245e1..0a434f48ad2 100644 --- a/docs/briefs/t-ground-tests.md +++ b/docs/briefs/t-ground-tests.md @@ -2,16 +2,16 @@ **Status:** PROPOSAL — dispatchable now (no design-cadence gate; consumer wiring is downstream and lands separately). Authored 2026-04-29. -**Lane:** T-Ground-Tests (S) — item **10** of 11 in [`r2-grounding-manager.md`](r2-grounding-manager.md) (lane description line 38, lane row line 69, acceptance gate line 129 `routing_correctness_l4_verified`, pending list line 146). +**Lane:** T-Ground-Tests (S) — item **10** of 11 in [`r2-grounding-manager.md`](r2-grounding-manager.md) (lane description line 38, lane row line 69, acceptance gate line 129 `routing_correctness_l4_verified`, pending list line 147). **Manager:** R2 Grounding Manager ([`r2-grounding-manager.md`](r2-grounding-manager.md)). **Lineage / authorities consumed (no re-litigation):** -- R2 manager lane row + acceptance gate: [`r2-grounding-manager.md`](r2-grounding-manager.md) lines 38, 69, 129, 146; pilot precedent at line 60 + receipt at line 120 (`pilot_inhabitance_routing_stability_landed` — DONE PR #765). +- R2 manager lane row + acceptance gate: [`r2-grounding-manager.md`](r2-grounding-manager.md) lines 38, 69, 129, 147; pilot precedent at line 60 + receipt at line 120 (`pilot_inhabitance_routing_stability_landed` — DONE PR #765). - Engine-reframe spec: [`docs/design-emission-model.md`](../design-emission-model.md) — Examples 1-7 are lifted as test cases (per `r2-grounding-manager.md:11` structural-acceptance-per-lane-close discipline); Q4 universal four-property gate (Faithful / Correct / Minimal / Performant; locked PR-I); R3-vs-R2 split for L4-L7 (lines 404-411 — R3 `T-Verification-L4-L7-Direct` is the runtime-equivalence harness; this R2 lane is the **routing-stability** structural sibling that runs purely off substrate facts). - Lens framework: [`docs/design-lens-framework.md`](../design-lens-framework.md) Q4 four-property entries and the Faithful/Performant/structural-Minimal lens-instance shape; `Lens.read: (Dag, Behavior) → Witness` substrate input (per design-emission-model.md:1107-1111 distinction: structural-fold properties are `Lens` instances; runtime-equivalence properties live in R3 harness — this lane covers the structural side). - Pilot routing-stability test stratum: `src/v3/grounding_pilot/src/lib.rs:408-460` — Stratum A (name-keyed parity) + Stratum B (algebra-homomorphism extension); precedent shape this lane generalizes. -- Substrate single-authority: row authorities at `src/v3/std/{rust,python,go}_method_template_contracts.dag` (Phase 1 / Phase 2 landed); LanguageSpec axes at `src/v3/std/emit_model.dag:302`; `MethodRef`/`MethodDeclaration` registry at `dsl/std/methods.dag` + `src/v3/std/methods.dag`. +- Substrate single-authority: row authorities at `src/v3/std/{rust,python,go}_method_template_contracts.dag` (Phase 1 / Phase 2 landed); LanguageSpec axes at `src/v3/std/emit_model.dag:303`; `MethodRef`/`MethodDeclaration` registry at `dsl/std/methods.dag` + `src/v3/std/methods.dag`. - Fail-closed: [`INVARIANTS.md`](../../INVARIANTS.md) C-8 (P3) + C-series — every detectable mis-routing is a typed `Diagnostic`; no silent passes. - Test discipline: [`TESTING.md`](../../TESTING.md) — hermetic, behavior-driven, unit-first; sub-second per `feedback_test_timeout_2s.md`. - Brief shape templates: [`t-ground-languagespec.md`](t-ground-languagespec.md), [`t-ground-lifetime-analyzer.md`](t-ground-lifetime-analyzer.md), [`t-ground-diagnostic.md`](t-ground-diagnostic.md). @@ -78,7 +78,7 @@ Examples 1-7 from `design-emission-model.md` (lines 415-792) are lifted as the s ### F. P1 substrate-fact-introduction receipts -Worker MUST run the 3-step procedure (`INVARIANTS.md:86-123`) for any new substrate type / variant / field introduced under this lane: +Worker MUST run the 3-step procedure (`INVARIANTS.md:94-129`) for any new substrate type / variant / field introduced under this lane: - **Step 1 (DAG-ancestor):** the per-axis `Witness` and `TestClaim` carriers — does an ancestor exist in `dsl/std/` or `src/v3/std/`? (`Witness` is from `src/v3/std/dimensions.dag`; `TestClaim` is from `src/v3/std/test_claims.dag` if present, else escalate.) - **Step 2 (Coproduct-vs-coordinate):** the test outcome shape — `TestClaim::Pass | Fail(Diagnostic)` is a proper alternative; per-axis verdicts on a single (program, target) inhabitance are coordinates of a record.