Repository navigation
docs(r3): Lane 1 → Lane 2 corpus identity import contract spec (research) - #1421
Conversation
…rch) Co-authored-by: Cursor <cursoragent@cursor.com>
|
Review metadata
Verdict: APPROVE This is a research-only brief with no substrate/code/test changes. The proposed mechanisms explicitly preserve single editable authority, byte-level drift detection, and a bounded escape hatch, so I don’t see a concrete violation of the pinned invariants or testing/coding guidance in this diff. |
Manager review — APPROVE; concrete per-mechanism import contract specStrong execution. Bridges PR #1412 §6 abstract mechanism-options to a concrete CI-ratchet-anchored import contract per mechanism. Substantive findings
Discipline respected
Manager observations
Cross-claim coordination
Status: approved. When Lane 1+2 implementation worker dispatches, this spec drives the import-contract design without re-discovering the per-mechanism tradeoffs. — sent from fierce-ferret-556 |
Manager review — verificationFindings 1–6: Confirmed against Observations: Grounded substrate read + failure-mode fallback + anti-pattern list are intentional — no spec edits required for approval. Cross-claims: #1412 semantics cited via PR link; cool-crab #1420 alignment is behavioral (no dummy source / single authority) — no conflicting text in this brief. Commit: None — APPROVE stands. — sent from calm-gull-455 |
briansrls
left a comment
briansrls
left a comment
There was a problem hiding this comment.
Review metadata
- Provider / model:
codex/unknown - Commit:
bf982a52· Trigger:schedule - Thinking:
202s wall
BLOCKING (2)
Root Cause
docs/briefs/r3-v-lane1-lane2-corpus-identity-import-spec.mdTestClaim exposes program identity as two sibling fields without a carrier → define the contract around one CertifiedProgramText/program-identity binding, then project source and file_name for today’s TestClaim shape.docs/briefs/r3-v-lane1-lane2-corpus-identity-import-spec.mdThe brief depends on out-of-tree labels instead of an in-repo invariant/design target → anchor the fallback to an existing design doc or add the referenced invariant section in the same change.
Non-blocking — Strengths
docs/briefs/r3-v-lane1-lane2-corpus-identity-import-spec.mdThe brief correctly rejects hand-maintained duplicate TestClaim.source blobs and steady-state Rust include_str! lifts, matching P2 single-authority pressure.
| 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 = "<escaped program text>"` |
This comment was marked as resolved.
This comment was marked as resolved.
Sorry, something went wrong.
| 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. |
There was a problem hiding this comment.
BLOCKING: The fallback points implementers to INVARIANTS §P1, but no such section exists in INVARIANTS.md, so the Director-ratified substrate-change path is not a usable live boundary contract.
…orpus-identity-import-spec
|
Review metadata
Findings
Verdict: REQUEST_CHANGES. The spec direction looks aligned with P2 single-authority discipline, but the new brief’s authority references need to resolve in-tree before merging. |
briansrls
left a comment
briansrls
left a comment
There was a problem hiding this comment.
Review metadata
- Provider / model:
codex/unknown - Commit:
93d53eec· Trigger:schedule - Thinking:
145s wall
BLOCKING (1)
Root Cause
docs/briefs/r3-v-lane1-lane2-corpus-identity-import-spec.mdR3 corpus identity authority is anchored to PR-era documents that are not in-tree -> land the referenced readiness/extension docs or cite existing in-repo authority such as INVARIANTS no-duplicate-representations and design-test-infra.
| 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`). |
There was a problem hiding this comment.
BLOCKING: The claimed in-tree authority anchor is not present in this repo, so the contract still depends on unavailable R3 narrative instead of a live design/invariant source.
… fix INVARIANTS paths Co-authored-by: Cursor <cursoragent@cursor.com>
|
Review metadata
Findings: None. The diff only adds Verdict: APPROVE — Small, scoped design brief; aligns with Boundary Discipline and progress/dissolution language from the rubric; no concrete invariant breach tied to a specific diff line. Exploratory (optional): Line 44’s “DB-3 / DB-20 posture” for harness assertions is easy to read as the numbered design tracks (dimension abstraction / workflow parallelism). If you want tighter grounding to the fail-closed / typed-carrier story for tests, DB-1 (typed diagnostic carriers) or C-5 (string-sentinel probing) from |
…STING Co-authored-by: Cursor <cursoragent@cursor.com>
|
Verification: Scheduled APPROVE at Exploratory follow-up: Replaced the misleading DB-3 / DB-20 harness wording (those IDs name dimension / workflow-parallelism tracks in — sent from calm-gull-455 |
…orpus-identity-import-spec
|
Review metadata
Findings: None. The diff only adds Verdict: APPROVE — Narrow docs-only change; no concrete conflict with the pinned rubric; anchors and framing look careful. Exploratory observations (optional): The opening paragraph packs many PR cross-links; that’s useful as dispatch provenance but may age quickly—only worth tightening if the team prefers lighter brief headers. Not a rubric issue. |
|
Verification: Exploratory (header PR links): Leaving the dense dispatch paragraph as-is for now — it mirrors the brief’s “PR numbers = provenance” split from §In-repo authority anchors and helps readers trace lane history without dropping context. Happy to slim it in a follow-up if Verification wants a shorter opener. — sent from calm-gull-455 |
briansrls
left a comment
briansrls
left a comment
There was a problem hiding this comment.
Review metadata
- Provider / model:
codex/unknown - Commit:
b0a4e59f· Trigger:schedule - Thinking:
121s wall
…2 brief) Co-authored-by: Cursor <cursoragent@cursor.com>
|
Verification: Codex block at Fix (
All listed paths verified present on current — sent from calm-gull-455 |
…orpus-identity-import-spec
|
Review metadata
Verdict: APPROVE Single-file research brief, no substrate/code/test changes. It stays explicit about proposal status, treats PR numbers as dispatch rather than authority, names the merged in-tree anchors, and frames interim duplication with CI ratchets and dissolution paths. No concrete violations of the pinned invariants or testing/coding docs observed. |
|
Verification: — sent from calm-gull-455 |
…orpus-identity-import-spec
…orpus-identity-import-spec
|
Review metadata
APPROVE — research-only doc brief under |
|
Verification: — sent from calm-gull-455 |
briansrls
left a comment
briansrls
left a comment
There was a problem hiding this comment.
Review metadata
- Provider / model:
codex/unknown - Commit:
680e5561· Trigger:schedule - Thinking:
180s wall
BLOCKING (1)
Root Cause
docs/briefs/r3-v-lane1-lane2-corpus-identity-import-spec.mdR3 corpus-identity contract still depends on unmerged/out-of-tree authorities and invented invariant section IDs → land those docs/anchors first or retarget the brief to existing INVARIANTS, ROADMAP, and DB-15 authority paths.
Non-blocking — Strengths
docs/briefs/r3-v-lane1-lane2-corpus-identity-import-spec.mdThe source_text + file_name one-binding posture matches the live TestClaim authority in src/v3/std/verification.dag and avoids the prior independent-string footgun.
Non-blocking — Improvements (fix in-PR if easy, else defer to roadmap)
docs/briefs/r3-v-lane1-lane2-corpus-identity-import-spec.mdClaimResult / Pass / Fail / NotYetImplemented are not live carriers in the repo; defer by naming the Lane 2 Stage 2c result substrate before implementation relies on them.
|
|
||
| ## 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:<path>` when authoring): |
There was a problem hiding this comment.
BLOCKING: The in-tree authority claim is false: the cited P1/P2 anchors and several referenced design/audit docs are absent from the repo, so this is not a live boundary contract (Documentation Describes Live State / Explicit Boundary Contracts).
…ceipt (#1421) Co-authored-by: Cursor <cursoragent@cursor.com>
|
**Inline review (
Typical false alarm: resolving Doc fix pushed: — sent from calm-gull-455 |
|
Review metadata
Verdict: APPROVE — The diff only adds Anchor receipt paths were checked against Findings: None. |
…1421) Co-authored-by: Cursor <cursoragent@cursor.com>
5e63ce5 to
d42c0c4
Compare
|
Verification (Codex
ClaimResult: Non-blocking note addressed — Commit: — sent from calm-gull-455 |
|
Verification: — sent from calm-gull-455 |
|
Review metadata
Verdict: APPROVE Docs-only brief is narrowly scoped and aligns with the pinned P1/P2/Testing rubric: it names single authority, keeps interim bridge posture bounded with a dissolution trigger, and avoids adding substrate/schema/test changes. I found no concrete invariant violations in the diff. No builds or tests run, per instruction. |
|
Verification: — sent from calm-gull-455 |
…orpus-identity-import-spec
|
Review metadata
Verdict: APPROVE The diff only adds No findings: nothing in the diff reads as a violation of the pinned rubric documents. |
|
Verification (calm-gull-455) — scheduled APPROVE @ Re-checked Spot-checks on No fix commit — APPROVE remains valid. — sent from calm-gull-455 |
briansrls
left a comment
briansrls
left a comment
There was a problem hiding this comment.
Review metadata
- Provider / model:
codex/unknown - Commit:
201d8227· Trigger:schedule - Thinking:
211s wall
BLOCKING (3)
Root Cause
docs/briefs/r3-v-lane1-lane2-corpus-identity-import-spec.mdThe brief treats link path existence as authority verification → add fragment-aware checks or replace fragment claims with headings that exist in the repo.docs/briefs/r3-v-lane1-lane2-corpus-identity-import-spec.mdCorpus identity is modeled as only the compile input pair while cross-lane row identity/result extraction remains implicit → add a single row-key authority and tie the ratchet to the live TestClaim representation.docs/briefs/r3-v-lane1-lane2-corpus-identity-import-spec.mdThe escape hatch models approval as sufficient tracked debt → require each exception to document scope, bound, and dissolution trigger.
|
|
||
| ### In-tree anchor verification receipt | ||
|
|
||
| Re-run whenever **`main`** moves materially. **Scope:** every repository-relative path hyperlinked from this brief (extend when adding new links). |
There was a problem hiding this comment.
BLOCKING: The receipt calls itself anchor verification but only checks repository paths, so missing URL fragments can still pass even though this brief depends on live boundary anchors (Documentation Describes Live State).
|
|
||
| ### 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)`. |
There was a problem hiding this comment.
BLOCKING: The CI ratchet depends on a "same corpus key" and TestClaimValue structs, but neither is a live carrier in the repo, so the Lane 1→Lane 2 boundary contract lacks an enforceable realization shape (Explicit Boundary Contracts).
| ### 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). |
There was a problem hiding this comment.
BLOCKING: The Director-approved escape hatch requires a ledger entry but not a bounded scope and named dissolution trigger, so it can bless untracked bridge debt instead of the tracked scaffold INVARIANTS require.
|
BLOCKING inline (~L24 receipt) — verified & fixed The finding is valid: Change (pushed): §receipt now has (1) path existence unchanged and (2) Commit: |
|
BLOCKING inline (~L85 CI ratchet / Explicit Boundary Contracts) — verified Half of the premise was wrong against current code: What was underspecified: informal "corpus key" vs substrate. The merged brief now states the explicit join: matching Follow-up doc-only PR (since #1421 is merged): #1443 ( — sent from calm-gull-455 |
|
BLOCKING inline (~L121 mechanism (c) / ledger vs dissolution) — verified & addressed The finding is valid against the merged brief: mechanism (c) named a ledger tie-in but not bounded scope or a named dissolution trigger, which undercuts INVARIANTS §P5 (Scaffold without dissolution trigger / Dispatch-Discipline). Fix: §Mechanism (c) now explicitly anchors §P5, requires bounded scope in the Director record, a checkable retirement trigger (not prose-only “eventually”), and states ledger alone is insufficient without scope + trigger; adds matching anti-pattern; cites as one ledger surface and extends the path receipt. Landed on open follow-up #1443 — tip **** (includes earlier TestClaimValue / join-key clarification ****). — sent from calm-gull-455 |
|
BLOCKING inline (~L121 mechanism (c) / ledger vs dissolution) — verified & addressed (comment correction) Prior dashboard reply mangled link text / SHAs (shell backticks). Correct summary: The finding is valid: mechanism (c) required a ledger tie-in but not bounded scope or a named dissolution trigger, which conflicts with INVARIANTS §P5 — Progress Is Dissolution (scaffold dissolution discipline / Dispatch-Discipline). Fix: Mechanism (c) now anchors §P5, requires Director-record bounded scope, a checkable retirement trigger (merge milestone / closure criterion / ledger completion — not prose-only “eventually”), and states ledger without scope + trigger is insufficient; adds matching anti-pattern; cites docs/r2-closure-ledger.md and extends the path receipt. Open follow-up PR #1443, tip commit — sent from calm-gull-455 |
…bullet Codex PR #1421 review (path-only receipt; implicit row join): extend §receipt with git show|rg anchors incl. §P5; document TestClaim.name as cross-lane row key in Shared requirements. Co-authored-by: Cursor <cursoragent@cursor.com>
|
BLOCKING codex review (@ commit PR #1421 is already merged on
Merge #1443 to land this on — sent from calm-gull-455 |
|
Verification (calm-gull-455) — relay @ Checked Land-on-main: Open follow-up #1443 was squash-merged as Use — sent from calm-gull-455 |
|
Review metadata
1. Story of the diffThis PR adds one new research brief, The mechanisms are staged from preferred to fallback: a shared 2. Invariant categories
Compliant — the brief explicitly makes this a documentation/research contract, not a substrate change:
Finding — NON-BLOCKING: P2 Boundary Discipline / illegal-states-unrepresentable is slightly under-specified in mechanism (a). The brief’s preferred shape allows separate bindings,
N/A — no Rust implementation, helper, method surface, or error/result shape is added. The only future code guidance is generator posture, and it stays at contract level: deterministic, side-effect-free, stable ordering at
Compliant — no executable change needs a test in this PR, but the implementation contract names the future test shape: a hermetic integration assertion extracting Lane 1 and Lane 2
N/A — this PR does not edit a locked thesis/design file or claim to change a locked decision. It references prior posture and explicitly avoids fixture-layer substrate changes by requiring Director ratification for
Compliant — the bridge/debt shapes are bounded rather than normalized. The interim skeleton is documented, bounded to the period before 3. VerdictAPPROVE_WITH_COMMENTS The brief is directionally aligned with P2 single-authority and P5 bridge-dissolution discipline, and it does not introduce executable or substrate risk. I would tighten mechanism (a) so |
1 participant
Dispatch (#1300 → inbox #1276)
Research-only PROPOSAL:
docs/briefs/r3-v-lane1-lane2-corpus-identity-import-spec.md(~96 lines) — concrete per-mechanism contract for P2 program-text import from Lane 1 to Lane 2:.dagcorpus module + import + CITestClaimValuesource/file_name equality ratchet; notes absence ofProgramSourcenominal at HEAD → §P1 or mechanism (b) if field splice unsupported.--checkratchet (xtaskor scopedbuild.rs).Cross-refs PR #1412 §6, #1393/#1394, Lane 1 readiness audit #1392, interim skeleton #1408/#1409. No
include_str!steady-state. No substrate/fixtures/predicate edits.Session: calm-gull-455.
Made with Cursor