From bf982a5203e447bcc59ffe4ee9eb6ff838f11253 Mon Sep 17 00:00:00 2001 From: Brian Searls Date: Fri, 1 May 2026 14:57:59 +0000 Subject: [PATCH 1/7] =?UTF-8?q?docs(r3):=20Lane=201=20=E2=86=92=20Lane=202?= =?UTF-8?q?=20corpus=20identity=20import=20contract=20spec=20(research)?= MIME-Version: 1.0 Content-Type: text/plain; charset=UTF-8 Content-Transfer-Encoding: 8bit Co-authored-by: Cursor --- ...lane1-lane2-corpus-identity-import-spec.md | 96 +++++++++++++++++++ 1 file changed, 96 insertions(+) create mode 100644 docs/briefs/r3-v-lane1-lane2-corpus-identity-import-spec.md diff --git a/docs/briefs/r3-v-lane1-lane2-corpus-identity-import-spec.md b/docs/briefs/r3-v-lane1-lane2-corpus-identity-import-spec.md new file mode 100644 index 00000000000..f07af053483 --- /dev/null +++ b/docs/briefs/r3-v-lane1-lane2-corpus-identity-import-spec.md @@ -0,0 +1,96 @@ +# Lane 1 → Lane 2 corpus identity import contract + +**Status:** PROPOSAL — research-only concrete import contract for **P2 single-authority** program text between Lane 1 (T-V-L4-L7-Direct) and Lane 2 (T-V-L5-Corpus). Builds on PR [**#1412**](https://github.com/gunb-ai/gunbc/pull/1412) (`docs/briefs/r3-v-l5-corpus-extension-spec.md` §6), P2 anchor PR **#1393**, bridge-retirement posture PR **#1394**, Lane 1 readiness audit ([`r3-v-l4-l7-direct-readiness-audit.md`](r3-v-l4-l7-direct-readiness-audit.md) / loyal-ibex **#1392** failure taxonomy), and the interim L5 skeleton (**#1408**, SG-0 bridge note **#1409**). **No substrate edits, no fixtures, no new `TestPredicate` variants** in this brief. + +**Non-goals:** Steady-state **`include_str!`** corpus lifts in Rust (**#1394**); hand-maintained duplicate `TestClaim.source` strings; claiming L5 absorbs L4. + +--- + +## Shared requirements (all mechanisms) + +- **Single editable authority** per corpus program row — second copies are either generated or read-only structural imports. +- **`TestClaim.source` + `file_name` pairing** stays consistent everywhere (both fields participate in compile identity and diagnostics routing — see readiness audits). +- **CI-visible drift detection** — silent divergence between Lane 1 and Lane 2 rows is unacceptable (ratchet shape varies by mechanism below). +- **DB-3 / DB-20 posture** for future harness code: assert typed outcomes (`Pass` / `Fail` / `NotYetImplemented(_)`) without brittle substring coupling on diagnostics. + +--- + +## Mechanism (a) — Shared `.dag` corpus module + declaration import + +### Shape + +1. **One fixture module** holds authoritative program text per certification row, e.g. path + `src/v3/compiler/tests/fixtures/corpus/r3_certification_corpus.dag` + with module name aligned to existing fixture discipline (illustrative: `std.r3_certification_corpus` — match repo naming rules when implementing). + +2. **Per-program bindings** expose the **same** string the compiler uses for `compile_to_dag(source, file_name)` — today `TestClaim` carries `source: String` and `file_name: String` directly ([`src/v3/std/verification.dag`](../../src/v3/std/verification.dag)); there is **no** separate `ProgramSource { source, file_name }` nominal on substrate **at HEAD**. + +3. **Concrete binding pattern (research target):** + - **Preferred structural approach:** `data r3_cert_add_then_branch_source: String = ""` + plus `data r3_cert_add_then_branch_file: String = "add_then_branch_seed.v3"` (or `FilePath`-typed equivalent if already modeled), **or** a single imported binding pair validated by a trivial structural predicate — exact lowering must match compiler rules for multiline string bodies. + - Lane 1 fixture (`r3_verification_l4_emit_eval_match.dag` family) and Lane 2 fixture (`r3_verification_l5_corpus.dag` family) each **`import std.r3_certification_corpus { … }`** and construct their **`TestClaim`** rows referencing those bindings for **`source`** / **`file_name`** fields. + +4. **If imports cannot splice into `TestClaim` fields** at lowering time (tooling gap), do **not** fork strings by hand — fall through to mechanism **(b)** or file **INVARIANTS §P1** for a minimal **`CertifiedProgramText`** record type reused by both lanes. + +### CI ratchet (byte-level) + +- Add a **hermetic integration assertion**: compile Lane 1 claim DAG + Lane 2 claim DAG, extract the two `TestClaimValue` structs for the **same corpus key**, `assert_eq!(l4.source, l5.source)` and `assert_eq!(l4.file_name, l5.file_name)`. +- This is the **import-resolution ratchet**: both lanes must resolve to identical bytes even if authored as separate `TestClaim` rows. + +--- + +## Mechanism (b) — Generated rows from single source + freshness ratchet + +### Shape + +1. **Single text authority** on disk outside duplicated fixtures, e.g. + `src/v3/compiler/tests/corpus_sources/add_then_branch.v3` + (extension illustrative — pick one grammar consistent with both lanes). + +2. **Deterministic generator** (acceptable homes: `xtask/` command or **`build.rs`** scoped to `v3-compiler` tests — choose by repo policy; generator must be **deterministic**, **side-effect free**, stable ordering). + +3. **Outputs:** generated fragments **checked into git** that materialize Lane 1 `TestClaim.source` / Lane 2 `TestClaim.source` (and metadata) — either **two generated `.dag` patches** merged into respective fixtures or **one generated module** consumed by import. + +### CI ratchet + +- **`cargo … gen --check`** (pattern): regenerate into a temp dir or stdout; **fail** if `git diff` would be non-empty for tracked outputs. +- Alternative: integration test runs generator and compares to `include_bytes!` of checked-in expectation — still **generated bytes are canonical**, not hand-edited. + +### Constraints + +- No timestamps, no locale, no environment-dependent paths in output. +- Generator inputs are **the only** editable corpus prose for that row class. + +--- + +## Mechanism (c) — Director-approved alternative (escape hatch only) + +Use when **(a)** or **(b)** is blocked by a genuine toolchain limitation **and** Director documents the exception. + +### Acceptable patterns + +- **Single** programmatic owner (generator or substrate-adjacent template) with **read-only** consumption elsewhere. +- **Explicit** ledger entry tying the exception to bridge-retirement / P2 posture (no silent carve-outs). + +### Anti-patterns + +- Independently edited **duplicate** `TestClaim.source` blobs between Lane 1 and Lane 2 fixtures. +- **Serialized** copy/paste text with informal “keep in sync” comments but **no** CI equality ratchet. +- **Locale-sensitive** or **stdout-shaped** comparisons as stand-ins for source equality. + +--- + +## Interim posture (#1408 / #1409) + +The landed skeleton uses **sidecar `.v3` + embedded `TestClaim.source` + harness `assert_eq!`** — valid **only** as interim until `ForAllTargets` wiring + P2 steady-state mechanism lands; dissolution must **fold** that bridge per SG-0 census commentary (**#1409**). Do **not** treat Rust `include_str!` of corpus text as steady-state (**#1394**). + +--- + +## Coordination + +- **Lane 1 worker:** preserves failure taxonomy ordering from readiness audit (**#1392** surface) — import contract must not obscure emit vs run vs eval vs mismatch stages. +- **Lane 2 worker:** consumes **program identity only** — comparison semantics remain cross-target algebraic equivalence per PR [#1412](https://github.com/gunb-ai/gunbc/pull/1412) corpus extension spec. + +**§P1 flags:** introducing **`CertifiedProgramText`**, **`ProgramSource`**, or widening `TestClaim` requires Director ratification — not a fixture-layer workaround. + +**Reply path:** Verification Manager inbox [#1276](https://github.com/gunb-ai/gunbc/issues/1276). From 9e5559c622c1a20dc23be0679322bc63128cc38e Mon Sep 17 00:00:00 2001 From: Brian Searls Date: Fri, 1 May 2026 12:12:10 -0400 Subject: [PATCH 2/7] WIP: calm-gull-455 --- ...lane1-lane2-corpus-identity-import-spec.md | 34 +++++++++++++++---- 1 file changed, 28 insertions(+), 6 deletions(-) diff --git a/docs/briefs/r3-v-lane1-lane2-corpus-identity-import-spec.md b/docs/briefs/r3-v-lane1-lane2-corpus-identity-import-spec.md index f07af053483..02732b9e5dd 100644 --- a/docs/briefs/r3-v-lane1-lane2-corpus-identity-import-spec.md +++ b/docs/briefs/r3-v-lane1-lane2-corpus-identity-import-spec.md @@ -6,10 +6,32 @@ --- +## In-repo authority anchors (not PR labels alone) + +GitHub PR numbers (**#1393**, **#1394**, **#1412**, …) are **dispatch provenance**, not a substitute for merged design text. This contract’s **in-tree** anchors: + +- **[INVARIANTS.md](../INVARIANTS.md) — §P2 Boundary Discipline** — “every fact lives in exactly one authoritative place”; parallel copies are the failure mode import mechanisms must prevent. +- **[r3-v-l5-corpus-readiness-audit.md](r3-v-l5-corpus-readiness-audit.md) §4** — P2 program-text options + bridge-retirement posture for certification corpus lifts (authoritative Verification lane narrative on `main`). +- **[modeling-discipline.md](../modeling-discipline.md)** — read alongside any future **§P1** carrier that merges `source` + `file_name` into one nominal. + +--- + +## Program identity binding (logical contract) + +**Program identity** for one corpus row is the **inseparable pair** `(source_text, file_name)` passed to `compile_to_dag(source, file_name)`. Today `TestClaim` projects that identity into **two sibling fields** without a dedicated substrate record (**at HEAD** — see [`src/v3/std/verification.dag`](../../src/v3/std/verification.dag)). + +**Contract:** Authoring must treat the pair as **one binding** then **project** into `TestClaim`: + +- **Never** edit `source` or `file_name` **in isolation** in steady state (that re-opens parallel authority and breaks diagnostics consistency). +- **Mechanisms (a)/(b):** a **single** import resolution or **single** generator transaction produces **both** projections for each lane; Lane 1 vs Lane 2 differs in **predicate / suite**, not in independently maintained halves of the pair. +- **§P1 steady-state option:** a Director-ratified nominal (illustrative: **`CertifiedProgramText`**) holding both strings once, with lowering into `TestClaim` — eliminates the “two-field projection” drift surface at the substrate layer. + +--- + ## Shared requirements (all mechanisms) - **Single editable authority** per corpus program row — second copies are either generated or read-only structural imports. -- **`TestClaim.source` + `file_name` pairing** stays consistent everywhere (both fields participate in compile identity and diagnostics routing — see readiness audits). +- **Program identity** per row is **one binding** projecting to **`TestClaim.source` + `TestClaim.file_name` together** — see §Program identity binding (not two unrelated strings). - **CI-visible drift detection** — silent divergence between Lane 1 and Lane 2 rows is unacceptable (ratchet shape varies by mechanism below). - **DB-3 / DB-20 posture** for future harness code: assert typed outcomes (`Pass` / `Fail` / `NotYetImplemented(_)`) without brittle substring coupling on diagnostics. @@ -26,11 +48,11 @@ 2. **Per-program bindings** expose the **same** string the compiler uses for `compile_to_dag(source, file_name)` — today `TestClaim` carries `source: String` and `file_name: String` directly ([`src/v3/std/verification.dag`](../../src/v3/std/verification.dag)); there is **no** separate `ProgramSource { source, file_name }` nominal on substrate **at HEAD**. 3. **Concrete binding pattern (research target):** - - **Preferred structural approach:** `data r3_cert_add_then_branch_source: String = ""` - plus `data r3_cert_add_then_branch_file: String = "add_then_branch_seed.v3"` (or `FilePath`-typed equivalent if already modeled), **or** a single imported binding pair validated by a trivial structural predicate — exact lowering must match compiler rules for multiline string bodies. - - Lane 1 fixture (`r3_verification_l4_emit_eval_match.dag` family) and Lane 2 fixture (`r3_verification_l5_corpus.dag` family) each **`import std.r3_certification_corpus { … }`** and construct their **`TestClaim`** rows referencing those bindings for **`source`** / **`file_name`** fields. + - **Pair discipline (mandatory):** One authoring step / one generator emission defines **both** `source` and `file_name`. **Do not** maintain two independently hand-edited `data …: String` declarations for the same row without a freshness ratchet — that is a **parallel-authority** footgun (violates [INVARIANTS §P2](../INVARIANTS.md#p2-boundary-discipline) intent). + - **Acceptable at HEAD:** (i) generated `.dag` fragment that sets both `TestClaim` fields from a **single** template input; (ii) compiler-supported structural literal that supplies both strings **atomically** in one declaration; (iii) interim **paired** imports only if CI ratchet below proves **both** fields stay byte-identical across lanes on every change. + - Lane 1 fixture (`r3_verification_l4_emit_eval_match.dag` family) and Lane 2 fixture (`r3_verification_l5_corpus.dag` family) each consume the **same projected pair** for a given corpus key. -4. **If imports cannot splice into `TestClaim` fields** at lowering time (tooling gap), do **not** fork strings by hand — fall through to mechanism **(b)** or file **INVARIANTS §P1** for a minimal **`CertifiedProgramText`** record type reused by both lanes. +4. **If imports cannot splice into `TestClaim` fields** at lowering time (tooling gap), do **not** fork strings by hand — fall through to mechanism **(b)** or file **INVARIANTS §P1** for a minimal **`CertifiedProgramText`** record type reused by both lanes (single carrier → dual projection at lowering). ### CI ratchet (byte-level) @@ -49,7 +71,7 @@ 2. **Deterministic generator** (acceptable homes: `xtask/` command or **`build.rs`** scoped to `v3-compiler` tests — choose by repo policy; generator must be **deterministic**, **side-effect free**, stable ordering). -3. **Outputs:** generated fragments **checked into git** that materialize Lane 1 `TestClaim.source` / Lane 2 `TestClaim.source` (and metadata) — either **two generated `.dag` patches** merged into respective fixtures or **one generated module** consumed by import. +3. **Outputs:** generated fragments **checked into git** that materialize, **in one transaction per row**, Lane 1 `TestClaim.source` **and** `file_name` plus Lane 2 `TestClaim.source` **and** `file_name` — both lanes’ pairs derived from the **same** generator inputs (never regenerate only one field for one lane). ### CI ratchet From ad02b0ad36df32b2ce1146fe934e181d6d7d478b Mon Sep 17 00:00:00 2001 From: Brian Searls Date: Fri, 1 May 2026 17:07:48 +0000 Subject: [PATCH 3/7] =?UTF-8?q?docs(r3):=20anchor=20lane1=E2=86=92lane2=20?= =?UTF-8?q?corpus=20identity=20brief=20to=20merged=20design=20+=20fix=20IN?= =?UTF-8?q?VARIANTS=20paths?= MIME-Version: 1.0 Content-Type: text/plain; charset=UTF-8 Content-Transfer-Encoding: 8bit Co-authored-by: Cursor --- ...lane1-lane2-corpus-identity-import-spec.md | 23 +++++++++++-------- 1 file changed, 13 insertions(+), 10 deletions(-) diff --git a/docs/briefs/r3-v-lane1-lane2-corpus-identity-import-spec.md b/docs/briefs/r3-v-lane1-lane2-corpus-identity-import-spec.md index 02732b9e5dd..fc83da1bd42 100644 --- a/docs/briefs/r3-v-lane1-lane2-corpus-identity-import-spec.md +++ b/docs/briefs/r3-v-lane1-lane2-corpus-identity-import-spec.md @@ -1,6 +1,6 @@ # Lane 1 → Lane 2 corpus identity import contract -**Status:** PROPOSAL — research-only concrete import contract for **P2 single-authority** program text between Lane 1 (T-V-L4-L7-Direct) and Lane 2 (T-V-L5-Corpus). Builds on PR [**#1412**](https://github.com/gunb-ai/gunbc/pull/1412) (`docs/briefs/r3-v-l5-corpus-extension-spec.md` §6), P2 anchor PR **#1393**, bridge-retirement posture PR **#1394**, Lane 1 readiness audit ([`r3-v-l4-l7-direct-readiness-audit.md`](r3-v-l4-l7-direct-readiness-audit.md) / loyal-ibex **#1392** failure taxonomy), and the interim L5 skeleton (**#1408**, SG-0 bridge note **#1409**). **No substrate edits, no fixtures, no new `TestPredicate` variants** in this brief. +**Status:** PROPOSAL — research-only concrete import contract for **P2 single-authority** program text between Lane 1 (T-V-L4-L7-Direct) and Lane 2 (T-V-L5-Corpus). **Merged design/invariant anchors on `main`:** [`INVARIANTS.md`](../../INVARIANTS.md) §P2 (Boundary Discipline — no parallel editable authorities); [`r3-v-l5-corpus-readiness-audit.md`](r3-v-l5-corpus-readiness-audit.md) §4 ([§4 heading](r3-v-l5-corpus-readiness-audit.md#4-critical-path-consumption-from-lane-1-boundary)) — program-text import options + bridge **#4** posture; [`design-cross-target-equivalence.md`](../design-cross-target-equivalence.md) — L5 algebraic-equivalence lock; [`design-test-infra.md`](../design-test-infra.md) — `TestClaim` / DB-15 structural authority (no duplicate test-schema forks); [`r3-structure.md`](../r3-structure.md) — Verification gates including **`l5_cross_target_consistency`**. **Dispatch only (not merged authorities):** PR [**#1412**](https://github.com/gunb-ai/gunbc/pull/1412) (Lane 2 corpus extension spec — cite merged paths above for implementation contracts). Further context: P2 anchor PR **#1393**, bridge-retirement posture PR **#1394**, Lane 1 readiness audit ([`r3-v-l4-l7-direct-readiness-audit.md`](r3-v-l4-l7-direct-readiness-audit.md) / loyal-ibex **#1392** failure taxonomy), interim L5 skeleton (**#1408**, SG-0 bridge note **#1409**). **No substrate edits, no fixtures, no new `TestPredicate` variants** in this brief. **Non-goals:** Steady-state **`include_str!`** corpus lifts in Rust (**#1394**); hand-maintained duplicate `TestClaim.source` strings; claiming L5 absorbs L4. @@ -8,11 +8,14 @@ ## In-repo authority anchors (not PR labels alone) -GitHub PR numbers (**#1393**, **#1394**, **#1412**, …) are **dispatch provenance**, not a substitute for merged design text. This contract’s **in-tree** anchors: +GitHub PR numbers (**#1393**, **#1394**, **#1412**, …) are **dispatch provenance**, not a substitute for merged design text. This contract’s **in-tree** anchors (each path exists on `main`; verify with `git cat-file -e HEAD:` when authoring): -- **[INVARIANTS.md](../INVARIANTS.md) — §P2 Boundary Discipline** — “every fact lives in exactly one authoritative place”; parallel copies are the failure mode import mechanisms must prevent. -- **[r3-v-l5-corpus-readiness-audit.md](r3-v-l5-corpus-readiness-audit.md) §4** — P2 program-text options + bridge-retirement posture for certification corpus lifts (authoritative Verification lane narrative on `main`). -- **[modeling-discipline.md](../modeling-discipline.md)** — read alongside any future **§P1** carrier that merges `source` + `file_name` into one nominal. +- **[INVARIANTS.md](../../INVARIANTS.md#p2-boundary-discipline) — §P2 Boundary Discipline** — “every fact lives in exactly one authoritative place”; parallel copies are the failure mode import mechanisms must prevent. +- **[r3-v-l5-corpus-readiness-audit.md](r3-v-l5-corpus-readiness-audit.md#4-critical-path-consumption-from-lane-1-boundary) §4** — P2 program-text options + bridge-retirement posture for certification corpus lifts (Verification lane narrative). +- **[design-cross-target-equivalence.md](../design-cross-target-equivalence.md)** — corpus numeric policy, oracle policy, and algebraic equality domain L5 consumes. +- **[design-test-infra.md](../design-test-infra.md)** — DB-15 posture: `TestClaim` in [`src/v3/std/verification.dag`](../../src/v3/std/verification.dag) is the structural authority; duplicate prose/schema forks violate the same “single authority” discipline as P2 program text. +- **[r3-structure.md](../r3-structure.md)** — R3 gate **`l5_cross_target_consistency`** and Verification lane placement. +- **[modeling-discipline.md](../modeling-discipline.md)** — read alongside any future **[INVARIANTS §P1](../../INVARIANTS.md#p1-modeling-faithfulness)** carrier that merges `source` + `file_name` into one nominal. --- @@ -24,7 +27,7 @@ GitHub PR numbers (**#1393**, **#1394**, **#1412**, …) are **dispatch provenan - **Never** edit `source` or `file_name` **in isolation** in steady state (that re-opens parallel authority and breaks diagnostics consistency). - **Mechanisms (a)/(b):** a **single** import resolution or **single** generator transaction produces **both** projections for each lane; Lane 1 vs Lane 2 differs in **predicate / suite**, not in independently maintained halves of the pair. -- **§P1 steady-state option:** a Director-ratified nominal (illustrative: **`CertifiedProgramText`**) holding both strings once, with lowering into `TestClaim` — eliminates the “two-field projection” drift surface at the substrate layer. +- **[INVARIANTS §P1](../../INVARIANTS.md#p1-modeling-faithfulness) steady-state option:** a Director-ratified nominal (illustrative: **`CertifiedProgramText`**) holding both strings once, with lowering into `TestClaim` — eliminates the “two-field projection” drift surface at the substrate layer. --- @@ -48,11 +51,11 @@ GitHub PR numbers (**#1393**, **#1394**, **#1412**, …) are **dispatch provenan 2. **Per-program bindings** expose the **same** string the compiler uses for `compile_to_dag(source, file_name)` — today `TestClaim` carries `source: String` and `file_name: String` directly ([`src/v3/std/verification.dag`](../../src/v3/std/verification.dag)); there is **no** separate `ProgramSource { source, file_name }` nominal on substrate **at HEAD**. 3. **Concrete binding pattern (research target):** - - **Pair discipline (mandatory):** One authoring step / one generator emission defines **both** `source` and `file_name`. **Do not** maintain two independently hand-edited `data …: String` declarations for the same row without a freshness ratchet — that is a **parallel-authority** footgun (violates [INVARIANTS §P2](../INVARIANTS.md#p2-boundary-discipline) intent). + - **Pair discipline (mandatory):** One authoring step / one generator emission defines **both** `source` and `file_name`. **Do not** maintain two independently hand-edited `data …: String` declarations for the same row without a freshness ratchet — that is a **parallel-authority** footgun (violates [INVARIANTS §P2](../../INVARIANTS.md#p2-boundary-discipline) intent). - **Acceptable at HEAD:** (i) generated `.dag` fragment that sets both `TestClaim` fields from a **single** template input; (ii) compiler-supported structural literal that supplies both strings **atomically** in one declaration; (iii) interim **paired** imports only if CI ratchet below proves **both** fields stay byte-identical across lanes on every change. - Lane 1 fixture (`r3_verification_l4_emit_eval_match.dag` family) and Lane 2 fixture (`r3_verification_l5_corpus.dag` family) each consume the **same projected pair** for a given corpus key. -4. **If imports cannot splice into `TestClaim` fields** at lowering time (tooling gap), do **not** fork strings by hand — fall through to mechanism **(b)** or file **INVARIANTS §P1** for a minimal **`CertifiedProgramText`** record type reused by both lanes (single carrier → dual projection at lowering). +4. **If imports cannot splice into `TestClaim` fields** at lowering time (tooling gap), do **not** fork strings by hand — fall through to mechanism **(b)** or file a **[INVARIANTS §P1](../../INVARIANTS.md#p1-modeling-faithfulness)** substrate extension for a minimal **`CertifiedProgramText`** record type reused by both lanes (single carrier → dual projection at lowering). ### CI ratchet (byte-level) @@ -111,8 +114,8 @@ The landed skeleton uses **sidecar `.v3` + embedded `TestClaim.source` + harness ## Coordination - **Lane 1 worker:** preserves failure taxonomy ordering from readiness audit (**#1392** surface) — import contract must not obscure emit vs run vs eval vs mismatch stages. -- **Lane 2 worker:** consumes **program identity only** — comparison semantics remain cross-target algebraic equivalence per PR [#1412](https://github.com/gunb-ai/gunbc/pull/1412) corpus extension spec. +- **Lane 2 worker:** consumes **program identity only** — comparison semantics remain cross-target algebraic equivalence per [`design-cross-target-equivalence.md`](../design-cross-target-equivalence.md); PR [**#1412**](https://github.com/gunb-ai/gunbc/pull/1412) is dispatch for extension-shape detail once merged. -**§P1 flags:** introducing **`CertifiedProgramText`**, **`ProgramSource`**, or widening `TestClaim` requires Director ratification — not a fixture-layer workaround. +**[INVARIANTS §P1](../../INVARIANTS.md#p1-modeling-faithfulness) flags:** introducing **`CertifiedProgramText`**, **`ProgramSource`**, or widening `TestClaim` requires Director ratification — not a fixture-layer workaround. **Reply path:** Verification Manager inbox [#1276](https://github.com/gunb-ai/gunbc/issues/1276). From c4d71ccbbed76177a3e9ef0c98b18ba112950171 Mon Sep 17 00:00:00 2001 From: Brian Searls Date: Fri, 1 May 2026 17:15:52 +0000 Subject: [PATCH 4/7] =?UTF-8?q?docs(r3):=20tie=20lane1=E2=86=92lane2=20har?= =?UTF-8?q?ness=20posture=20to=20INVARIANTS=20DB-1/C-5=20+=20TESTING?= MIME-Version: 1.0 Content-Type: text/plain; charset=UTF-8 Content-Transfer-Encoding: 8bit Co-authored-by: Cursor --- docs/briefs/r3-v-lane1-lane2-corpus-identity-import-spec.md | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/docs/briefs/r3-v-lane1-lane2-corpus-identity-import-spec.md b/docs/briefs/r3-v-lane1-lane2-corpus-identity-import-spec.md index fc83da1bd42..4d827c6a011 100644 --- a/docs/briefs/r3-v-lane1-lane2-corpus-identity-import-spec.md +++ b/docs/briefs/r3-v-lane1-lane2-corpus-identity-import-spec.md @@ -36,7 +36,7 @@ GitHub PR numbers (**#1393**, **#1394**, **#1412**, …) are **dispatch provenan - **Single editable authority** per corpus program row — second copies are either generated or read-only structural imports. - **Program identity** per row is **one binding** projecting to **`TestClaim.source` + `TestClaim.file_name` together** — see §Program identity binding (not two unrelated strings). - **CI-visible drift detection** — silent divergence between Lane 1 and Lane 2 rows is unacceptable (ratchet shape varies by mechanism below). -- **DB-3 / DB-20 posture** for future harness code: assert typed outcomes (`Pass` / `Fail` / `NotYetImplemented(_)`) without brittle substring coupling on diagnostics. +- **Harness assertion posture** for future integration code: pin **`ClaimResult` / typed outcomes** (`Pass` / `Fail` / `NotYetImplemented(_)`) structurally — **[INVARIANTS DB-1](../../INVARIANTS.md#db-1)** (typed diagnostic carriers, not ad hoc warning text) and **[C-5](../../INVARIANTS.md#c-5)** (no string-sentinel probing); operational examples in [**TESTING.md**](../../TESTING.md#dont-assert-on-implementation-details) §“Don’t assert on implementation details.” --- From c16cdf093d9dbb90ee042e5b514113e1e8ec25ef Mon Sep 17 00:00:00 2001 From: Brian Searls Date: Fri, 1 May 2026 18:04:55 +0000 Subject: [PATCH 5/7] =?UTF-8?q?docs(r3):=20tighten=20INVARIANTS=20P1/P2=20?= =?UTF-8?q?anchors=20+=20path=20receipt=20(lane1=E2=86=92lane2=20brief)?= MIME-Version: 1.0 Content-Type: text/plain; charset=UTF-8 Content-Transfer-Encoding: 8bit Co-authored-by: Cursor --- ...lane1-lane2-corpus-identity-import-spec.md | 23 +++++++++++++++++-- 1 file changed, 21 insertions(+), 2 deletions(-) diff --git a/docs/briefs/r3-v-lane1-lane2-corpus-identity-import-spec.md b/docs/briefs/r3-v-lane1-lane2-corpus-identity-import-spec.md index 4d827c6a011..1ba92bdda02 100644 --- a/docs/briefs/r3-v-lane1-lane2-corpus-identity-import-spec.md +++ b/docs/briefs/r3-v-lane1-lane2-corpus-identity-import-spec.md @@ -1,6 +1,6 @@ # Lane 1 → Lane 2 corpus identity import contract -**Status:** PROPOSAL — research-only concrete import contract for **P2 single-authority** program text between Lane 1 (T-V-L4-L7-Direct) and Lane 2 (T-V-L5-Corpus). **Merged design/invariant anchors on `main`:** [`INVARIANTS.md`](../../INVARIANTS.md) §P2 (Boundary Discipline — no parallel editable authorities); [`r3-v-l5-corpus-readiness-audit.md`](r3-v-l5-corpus-readiness-audit.md) §4 ([§4 heading](r3-v-l5-corpus-readiness-audit.md#4-critical-path-consumption-from-lane-1-boundary)) — program-text import options + bridge **#4** posture; [`design-cross-target-equivalence.md`](../design-cross-target-equivalence.md) — L5 algebraic-equivalence lock; [`design-test-infra.md`](../design-test-infra.md) — `TestClaim` / DB-15 structural authority (no duplicate test-schema forks); [`r3-structure.md`](../r3-structure.md) — Verification gates including **`l5_cross_target_consistency`**. **Dispatch only (not merged authorities):** PR [**#1412**](https://github.com/gunb-ai/gunbc/pull/1412) (Lane 2 corpus extension spec — cite merged paths above for implementation contracts). Further context: P2 anchor PR **#1393**, bridge-retirement posture PR **#1394**, Lane 1 readiness audit ([`r3-v-l4-l7-direct-readiness-audit.md`](r3-v-l4-l7-direct-readiness-audit.md) / loyal-ibex **#1392** failure taxonomy), interim L5 skeleton (**#1408**, SG-0 bridge note **#1409**). **No substrate edits, no fixtures, no new `TestPredicate` variants** in this brief. +**Status:** PROPOSAL — research-only concrete import contract for **P2 single-authority** program text between Lane 1 (T-V-L4-L7-Direct) and Lane 2 (T-V-L5-Corpus). **Merged design/invariant anchors on `main`:** **[INVARIANTS §P2](../../INVARIANTS.md#p2-boundary-discipline)** (Boundary Discipline — no parallel editable authorities); **[INVARIANTS §P1](../../INVARIANTS.md#p1-modeling-faithfulness)** (Modeling Faithfulness — substrate-fact introduction before new carriers); [`r3-v-l5-corpus-readiness-audit.md`](r3-v-l5-corpus-readiness-audit.md) §4 ([§4 heading](r3-v-l5-corpus-readiness-audit.md#4-critical-path-consumption-from-lane-1-boundary)) — program-text import options + bridge **#4** posture; [`design-cross-target-equivalence.md`](../design-cross-target-equivalence.md) — L5 algebraic-equivalence lock; [`design-test-infra.md`](../design-test-infra.md) — `TestClaim` / DB-15 structural authority (no duplicate test-schema forks); [`r3-structure.md`](../r3-structure.md) — Verification gates including **`l5_cross_target_consistency`**. **Dispatch only (not merged authorities):** PR [**#1412**](https://github.com/gunb-ai/gunbc/pull/1412) (Lane 2 corpus extension spec — cite merged paths above for implementation contracts). Further context: P2 anchor PR **#1393**, bridge-retirement posture PR **#1394**, Lane 1 readiness audit ([`r3-v-l4-l7-direct-readiness-audit.md`](r3-v-l4-l7-direct-readiness-audit.md) / loyal-ibex **#1392** failure taxonomy), interim L5 skeleton (**#1408**, SG-0 bridge note **#1409**). **No substrate edits, no fixtures, no new `TestPredicate` variants** in this brief. **Non-goals:** Steady-state **`include_str!`** corpus lifts in Rust (**#1394**); hand-maintained duplicate `TestClaim.source` strings; claiming L5 absorbs L4. @@ -11,11 +11,30 @@ GitHub PR numbers (**#1393**, **#1394**, **#1412**, …) are **dispatch provenance**, not a substitute for merged design text. This contract’s **in-tree** anchors (each path exists on `main`; verify with `git cat-file -e HEAD:` when authoring): - **[INVARIANTS.md](../../INVARIANTS.md#p2-boundary-discipline) — §P2 Boundary Discipline** — “every fact lives in exactly one authoritative place”; parallel copies are the failure mode import mechanisms must prevent. +- **[INVARIANTS §P1](../../INVARIANTS.md#p1-modeling-faithfulness) — Modeling Faithfulness** — substrate extensions (`CertifiedProgramText`, widening `TestClaim`, …) route through the §P1 substrate-fact introduction procedure; not ad hoc fixture forks. - **[r3-v-l5-corpus-readiness-audit.md](r3-v-l5-corpus-readiness-audit.md#4-critical-path-consumption-from-lane-1-boundary) §4** — P2 program-text options + bridge-retirement posture for certification corpus lifts (Verification lane narrative). - **[design-cross-target-equivalence.md](../design-cross-target-equivalence.md)** — corpus numeric policy, oracle policy, and algebraic equality domain L5 consumes. - **[design-test-infra.md](../design-test-infra.md)** — DB-15 posture: `TestClaim` in [`src/v3/std/verification.dag`](../../src/v3/std/verification.dag) is the structural authority; duplicate prose/schema forks violate the same “single authority” discipline as P2 program text. - **[r3-structure.md](../r3-structure.md)** — R3 gate **`l5_cross_target_consistency`** and Verification lane placement. -- **[modeling-discipline.md](../modeling-discipline.md)** — read alongside any future **[INVARIANTS §P1](../../INVARIANTS.md#p1-modeling-faithfulness)** carrier that merges `source` + `file_name` into one nominal. +- **[modeling-discipline.md](../modeling-discipline.md)** — read alongside any future **§P1** carrier that merges `source` + `file_name` into one nominal. + +### In-tree anchor verification receipt + +Re-run whenever **`main`** moves materially: + +```bash +git fetch origin +for p in \ + INVARIANTS.md \ + docs/modeling-discipline.md \ + docs/design-cross-target-equivalence.md \ + docs/design-test-infra.md \ + docs/r3-structure.md \ + docs/briefs/r3-v-l5-corpus-readiness-audit.md \ + docs/briefs/r3-v-l4-l7-direct-readiness-audit.md \ + src/v3/std/verification.dag +do git cat-file -e "origin/main:$p" || exit 1; done +``` --- From fdbd357fbcfa75219c11b4792434c0f29c8c5733 Mon Sep 17 00:00:00 2001 From: Brian Searls Date: Fri, 1 May 2026 18:59:55 +0000 Subject: [PATCH 6/7] docs(r3): clarify repo-root vs docs/ relative links + widen anchor receipt (#1421) Co-authored-by: Cursor --- docs/briefs/r3-v-lane1-lane2-corpus-identity-import-spec.md | 5 +++-- 1 file changed, 3 insertions(+), 2 deletions(-) diff --git a/docs/briefs/r3-v-lane1-lane2-corpus-identity-import-spec.md b/docs/briefs/r3-v-lane1-lane2-corpus-identity-import-spec.md index 1ba92bdda02..4790d70ec46 100644 --- a/docs/briefs/r3-v-lane1-lane2-corpus-identity-import-spec.md +++ b/docs/briefs/r3-v-lane1-lane2-corpus-identity-import-spec.md @@ -8,7 +8,7 @@ ## In-repo authority anchors (not PR labels alone) -GitHub PR numbers (**#1393**, **#1394**, **#1412**, …) are **dispatch provenance**, not a substitute for merged design text. This contract’s **in-tree** anchors (each path exists on `main`; verify with `git cat-file -e HEAD:` when authoring): +GitHub PR numbers (**#1393**, **#1394**, **#1412**, …) are **dispatch provenance**, not a substitute for merged design text. This contract’s **in-tree** Markdown links resolve from **`docs/briefs/`** as **`../../…`** for repo-root files (`INVARIANTS.md`, `TESTING.md`, `src/…`) and **`../…`** for other files under `docs/` — a **`../INVARIANTS.md`** link would incorrectly resolve under `docs/` and **does not exist** (common false “missing authority” report). §P1 / §P2 URL fragments (`#p1-modeling-faithfulness`, `#p2-boundary-discipline`) target GitHub’s auto-generated heading anchors for `## P1: Modeling Faithfulness` and `## P2: Boundary Discipline` in [`INVARIANTS.md`](../../INVARIANTS.md). **Mechanical live check:** §In-tree anchor verification receipt below (`git cat-file -e origin/main:` on every hyperlinked path). - **[INVARIANTS.md](../../INVARIANTS.md#p2-boundary-discipline) — §P2 Boundary Discipline** — “every fact lives in exactly one authoritative place”; parallel copies are the failure mode import mechanisms must prevent. - **[INVARIANTS §P1](../../INVARIANTS.md#p1-modeling-faithfulness) — Modeling Faithfulness** — substrate extensions (`CertifiedProgramText`, widening `TestClaim`, …) route through the §P1 substrate-fact introduction procedure; not ad hoc fixture forks. @@ -20,12 +20,13 @@ GitHub PR numbers (**#1393**, **#1394**, **#1412**, …) are **dispatch provenan ### In-tree anchor verification receipt -Re-run whenever **`main`** moves materially: +Re-run whenever **`main`** moves materially. **Scope:** every repository-relative path hyperlinked from this brief (extend when adding new links). ```bash git fetch origin for p in \ INVARIANTS.md \ + TESTING.md \ docs/modeling-discipline.md \ docs/design-cross-target-equivalence.md \ docs/design-test-infra.md \ From d42c0c4eccd599fb98d13b3ff9ef2f5279145a06 Mon Sep 17 00:00:00 2001 From: Brian Searls Date: Fri, 1 May 2026 15:05:07 -0400 Subject: [PATCH 7/7] docs(r3): five-principles + ROADMAP anchors; cite live ClaimResult (#1421) Co-authored-by: Cursor --- .../briefs/r3-v-lane1-lane2-corpus-identity-import-spec.md | 7 +++++-- 1 file changed, 5 insertions(+), 2 deletions(-) diff --git a/docs/briefs/r3-v-lane1-lane2-corpus-identity-import-spec.md b/docs/briefs/r3-v-lane1-lane2-corpus-identity-import-spec.md index 4790d70ec46..5eed9fd16f7 100644 --- a/docs/briefs/r3-v-lane1-lane2-corpus-identity-import-spec.md +++ b/docs/briefs/r3-v-lane1-lane2-corpus-identity-import-spec.md @@ -8,7 +8,7 @@ ## In-repo authority anchors (not PR labels alone) -GitHub PR numbers (**#1393**, **#1394**, **#1412**, …) are **dispatch provenance**, not a substitute for merged design text. This contract’s **in-tree** Markdown links resolve from **`docs/briefs/`** as **`../../…`** for repo-root files (`INVARIANTS.md`, `TESTING.md`, `src/…`) and **`../…`** for other files under `docs/` — a **`../INVARIANTS.md`** link would incorrectly resolve under `docs/` and **does not exist** (common false “missing authority” report). §P1 / §P2 URL fragments (`#p1-modeling-faithfulness`, `#p2-boundary-discipline`) target GitHub’s auto-generated heading anchors for `## P1: Modeling Faithfulness` and `## P2: Boundary Discipline` in [`INVARIANTS.md`](../../INVARIANTS.md). **Mechanical live check:** §In-tree anchor verification receipt below (`git cat-file -e origin/main:` on every hyperlinked path). +GitHub PR numbers (**#1393**, **#1394**, **#1412**, …) are **dispatch provenance**, not a substitute for merged design text. This contract’s **in-tree** Markdown links resolve from **`docs/briefs/`** as **`../../…`** for repo-root files (`INVARIANTS.md`, `TESTING.md`, `src/…`) and **`../…`** for other files under `docs/` — a **`../INVARIANTS.md`** link would incorrectly resolve under `docs/` and **does not exist** (common false “missing authority” report). §P1 / §P2 URL fragments (`#p1-modeling-faithfulness`, `#p2-boundary-discipline`) target GitHub’s auto-generated heading anchors for `## P1: Modeling Faithfulness` and `## P2: Boundary Discipline` in [`INVARIANTS.md`](../../INVARIANTS.md). **Same commitments (compact):** list items **1–2** under **[The five principles](../../INVARIANTS.md#the-five-principles)** (“Modeling Faithfulness”, “Boundary Discipline”). **Mechanical live check:** §In-tree anchor verification receipt below (`git cat-file -e origin/main:` on every hyperlinked path). - **[INVARIANTS.md](../../INVARIANTS.md#p2-boundary-discipline) — §P2 Boundary Discipline** — “every fact lives in exactly one authoritative place”; parallel copies are the failure mode import mechanisms must prevent. - **[INVARIANTS §P1](../../INVARIANTS.md#p1-modeling-faithfulness) — Modeling Faithfulness** — substrate extensions (`CertifiedProgramText`, widening `TestClaim`, …) route through the §P1 substrate-fact introduction procedure; not ad hoc fixture forks. @@ -16,6 +16,7 @@ GitHub PR numbers (**#1393**, **#1394**, **#1412**, …) are **dispatch provenan - **[design-cross-target-equivalence.md](../design-cross-target-equivalence.md)** — corpus numeric policy, oracle policy, and algebraic equality domain L5 consumes. - **[design-test-infra.md](../design-test-infra.md)** — DB-15 posture: `TestClaim` in [`src/v3/std/verification.dag`](../../src/v3/std/verification.dag) is the structural authority; duplicate prose/schema forks violate the same “single authority” discipline as P2 program text. - **[r3-structure.md](../r3-structure.md)** — R3 gate **`l5_cross_target_consistency`** and Verification lane placement. +- **[ROADMAP.md](../../ROADMAP.md)** — program-level R3 Verification / debt narrative (dispatch context; named gates stay authoritative in [`r3-structure.md`](../r3-structure.md)). - **[modeling-discipline.md](../modeling-discipline.md)** — read alongside any future **§P1** carrier that merges `source` + `file_name` into one nominal. ### In-tree anchor verification receipt @@ -26,6 +27,7 @@ Re-run whenever **`main`** moves materially. **Scope:** every repository-relativ git fetch origin for p in \ INVARIANTS.md \ + ROADMAP.md \ TESTING.md \ docs/modeling-discipline.md \ docs/design-cross-target-equivalence.md \ @@ -33,6 +35,7 @@ for p in \ docs/r3-structure.md \ docs/briefs/r3-v-l5-corpus-readiness-audit.md \ docs/briefs/r3-v-l4-l7-direct-readiness-audit.md \ + src/v3/compiler/src/test_runner.rs \ src/v3/std/verification.dag do git cat-file -e "origin/main:$p" || exit 1; done ``` @@ -56,7 +59,7 @@ do git cat-file -e "origin/main:$p" || exit 1; done - **Single editable authority** per corpus program row — second copies are either generated or read-only structural imports. - **Program identity** per row is **one binding** projecting to **`TestClaim.source` + `TestClaim.file_name` together** — see §Program identity binding (not two unrelated strings). - **CI-visible drift detection** — silent divergence between Lane 1 and Lane 2 rows is unacceptable (ratchet shape varies by mechanism below). -- **Harness assertion posture** for future integration code: pin **`ClaimResult` / typed outcomes** (`Pass` / `Fail` / `NotYetImplemented(_)`) structurally — **[INVARIANTS DB-1](../../INVARIANTS.md#db-1)** (typed diagnostic carriers, not ad hoc warning text) and **[C-5](../../INVARIANTS.md#c-5)** (no string-sentinel probing); operational examples in [**TESTING.md**](../../TESTING.md#dont-assert-on-implementation-details) §“Don’t assert on implementation details.” +- **Harness assertion posture** for future integration code: pin **`ClaimResult` / typed outcomes** (`Pass` / `Fail` / `NotYetImplemented(_)`) structurally — today these variants are the Rust **`TestRunner`** carrier in [`src/v3/compiler/src/test_runner.rs`](../../src/v3/compiler/src/test_runner.rs) (`pub enum ClaimResult`, not a separate `.dag` nominal yet); combine with **[INVARIANTS DB-1](../../INVARIANTS.md#db-1)** (typed diagnostic carriers, not ad hoc warning text) and **[C-5](../../INVARIANTS.md#c-5)** (no string-sentinel probing); operational examples in [**TESTING.md**](../../TESTING.md#dont-assert-on-implementation-details) §“Don’t assert on implementation details.” ---