docs(r3): Lane 1 → Lane 2 corpus identity import contract spec (research)

docs/briefs/r3-v-lane1-lane2-corpus-identity-import-spec.md

@@ -0,0 +1,118 @@
+# 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.
+
+---
+
+## 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.
+- **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.
+
+---
+
+## 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):**
+   - **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).
+
+### 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, **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
+
+- **`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).