Skip to content

feat(v3): T-Verification-BridgeLedger — carrier + BridgeLedgerZero predicate + runner - #1314

Merged
briansrls merged 93 commits into
mainfrom
session/sharp-raven-604
May 1, 2026
Merged

briansrls merged 93 commits into
mainfrom
session/sharp-raven-604

Conversation

@briansrls

@briansrls briansrls commented Apr 30, 2026 •

Copy link
Copy Markdown
Contributor

Summary

T-Verification-BridgeLedger — substrate carrier + Verification predicate surface for the bridge-retirement ledger gate (per parent #1130 dispatch + Director scope extension #4356094666).

Adds:

Carrier (src/v3/std/bridge_ledger.dag)

  • type BridgeStatus = Retired | Open — closed two-variant coproduct.
  • type BridgeLedgerRow { name: String, owner: String, status: BridgeStatus, authority: String }.
  • data bridge_ledger: List<BridgeLedgerRow> = [...] — five canonical rows from docs/r3-structure.md:79-83 in document order. Status verdicts grounded per-row in the file header.

Predicate (src/v3/std/verification.dag)

  • TestPredicate::BridgeLedgerZero { ledger: DeclarationRef } — single typed-edge payload. The claim points at bridge_ledger by structural identity; substrate amendment required to widen the payload.

Runner (src/v3/compiler/src/test_runner.rs)

  • eval_bridge_ledger_zero: resolves ledger DeclarationRef, walks ValueBody::List rows, partitions by structural comparison against BridgeStatus::Retired's variant id. Pass iff every row is Retired; Fail names the Open rows in declaration order so Verification surfaces residual debt directly.

Tests (bridge_ledger_carrier_test.rs)

8 ratchets:

  • 6 carrier-shape tests (field set, status coproduct, list shape, canonical names in doc order, name uniqueness, status structural variant).
  • bridge_ledger_zero_predicate_carries_only_ledger_declaration_ref — pins variant payload set + DeclarationRef field type.
  • bridge_ledger_zero_runner_fails_with_named_open_rows_at_head — compiles a TestClaim with predicate: BridgeLedgerZero { ledger: bridge_ledger }, runs through TestRunner, asserts Fail names the three currently-Open rows (source_span_file_participation, include_str_side_channels, exact_string_patching_residual) and excludes the two Retired ones. Re-arms as a Pass ratchet once all five flip to Retired.

Status verdicts at HEAD

Bridge Status Doc reference
bridge_source_span_file_participation_retired Open r3-structure.md:79 "the gate is not satisfied" (R3-deferred)
bridge_mark_bootstrap_secret_nominal_opacity_retired Retired r3-structure.md:80 "PR A landed in R2"
bridge_canonical_lens_name_dispatch_retired Retired r3-structure.md:81 lens dispatch via DeclarationRef/typed identity
bridge_include_str_side_channels_retired Open r3-structure.md:82 "Open disposition (pipeline_authority, PR #1171)"
bridge_exact_string_patching_residual_retired Open r3-structure.md:83 umbrella row; PB lower-helper slice pinned at zero, "Other classes ... remain out of scope"

The runner's current failure message names the three Open rows verbatim — no green-claim pretense.

Out of scope

  • Verification's .dag TestClaim row that activates the gate — that's docs(r3): BridgeLedgerZero TestClaim standby shape #1310's remit. This PR provides the substrate authority + predicate variant + runner branch; Verification authors data bridge_ledger_zero_claim: TestClaim = { predicate: BridgeLedgerZero { ledger: bridge_ledger }, … } separately.
  • Per-row dissolution receipts that flip Open rows to Retired — owned by the lanes named in each row's owner field.

Verification

cargo run -p v3-compiler --features bootstrap-regen-fresh --bin regen_bootstrap
cargo run -p v3-compiler --features bootstrap-regen-fresh --bin regen_bootstrap -- --verify
cargo test -p v3-compiler refresh_handwritten_parse_snapshot_manifest -- --ignored
cargo test -p v3-compiler --test integration bridge_ledger_carrier
cargo clippy --all-targets -- -D warnings

8/8 tests pass locally; clippy clean.

🤖 Generated with Claude Code

…ages signature

- src/v3/std/anthropic_schema.dag: type-authority-only mirror of provider-domain
  types reachable from operation Messages signature in
  dsl/extdeps/llm/anthropic.dag (AnthropicChatMessage + content block variants,
  AnthropicStopReason, AnthropicMessages200{TextBlock,Usage,Body}).
- AnthropicErrorShape deferred (4xx/5xx response slot only; not on the typed
  return reach for fn anthropic_messages -> AnthropicMessages200Body).
- src/v3/compiler/tests/integration/anthropic_schema_lockstep_test.rs:
  8 ratchets pinning v3 mirror against v2 source (variant labels, field labels,
  type-name presence in v2). Discipline mirrors method_registry_test.rs.
- Type authority only — no fn anthropic_messages, no Operation rows. Those
  are the next substrate precursor that consumes these types.

@briansrls briansrls left a comment

Copy link
Copy Markdown
Contributor Author

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

Review metadata

  • Provider / model: codex / unknown
  • Commit: 26ab0e13 · Trigger: schedule
  • Thinking: 449s wall

BLOCKING (1)

Root Cause

  • src/v3/compiler/tests/integration/bridge_ledger_carrier_test.rs The ratchet verifies ledger contents by re-encoding them in Rust instead of reading the substrate carrier → derive expected row names/statuses from bridge_ledger or land a present external authority and compare against that.

Non-blocking — Strengths

  • src/v3/compiler/src/test_runner.rs The BridgeLedgerZero runner is otherwise fail-closed around malformed payloads, wrong canonical identity, malformed row names, and invalid BridgeStatus constructors.

⚠️ The bridge-ledger direction is close, but the new gate still introduces a parallel Rust authority for the ledger facts it is meant to centralize.


const BRIDGE_LEDGER: &str = "bridge_ledger";

const CANONICAL_BRIDGES: &[&str] = &[

This comment was marked as resolved.

@briansrls

Copy link
Copy Markdown
Contributor Author

Review metadata

  • Provider / model: cursor / composer-2
  • Commit: a33489a2 · Trigger: schedule
  • Comparison: origin/main @ 42e37700 ... review/pr-1314-a33489a2 @ a33489a2
  • Thinking: 81s wall

Findings

  • src/v3/compiler/src/test_runner.rs:2468 — CODING.md (“Small and composable”: bodies much larger than ~50 lines are called out for new code). eval_bridge_ledger_zero is ~207 lines end-to-end in one function; the behavior is sensible but would fit the project style better split into small helpers (e.g. resolve/canonicalize ledger ref, validate List<BridgeLedgerRow>, scan rows / collect open names). NON-BLOCKING — refactor-quality, not a modeling/invariant breach.

  • src/v3/compiler/tests/integration/bridge_ledger_carrier_test.rs (~lines 572–588 in the new file) — TESTING.md (“Don’t assert on implementation details”) discourages pinning diagnostics via substring checks. Here reason.contains(row) encodes the intended contract (“failures name open rows”), so it is defensible as a behavioral assertion; still a mild tension with the doc’s “don’t pin error message text” examples. NON-BLOCKING — only worth tightening if you later expose structured failure payloads for claims.

Nothing in the substantive diff contradicts INVARIANTS.md single-authority / fail-closed expectations for this feature: the substrate ledger in bridge_ledger.dag, the BridgeLedgerRef scaffold with a named #1175 dissolution trigger, and the runner’s canonical bridge_ledger identity check are aligned with P2 / modeling-discipline (tracked scaffold, closed coproduct for status, no parallel Rust ledger table).

Verdict

APPROVE_WITH_COMMENTS — Substrate and verification wiring look sound and well-tested; the only rubric-aligned nit is the very large new predicate evaluator in test_runner.rs, which could be decomposed without changing behavior.

…e ledger (single-authority)

Codex BLOCKING on PR #1314: CANONICAL_BRIDGES + expected_open/retired
arrays copied the ledger row set and status partition into Rust,
creating exactly the test-side parallel table bridge_ledger.dag rules
out (single-authority / M7).

- Removed the CANONICAL_BRIDGES const and the
  bridge_ledger_carries_canonical_five_names_in_doc_order test (the
  test re-asserted ledger content from a hardcoded copy; row content
  authority lives only in bridge_ledger.dag).
- bridge_ledger_lowers_as_list_with_at_least_one_row replaces the
  earlier exact-five-rows assertion: pins the structural shape
  (List value_body, every entry a Record, non-empty) without
  duplicating the row count.
- bridge_ledger_zero_runner_fails_with_named_open_rows_at_head no
  longer hardcodes expected_open_rows / expected_retired_rows. It
  reads the live ledger from the bootstrap, partitions by structural
  comparison against BridgeStatus::Retired's variant id, and asserts:
  every Open row's name appears in the failure diagnostic and every
  Retired row's name does not. Re-arms automatically as upstream rows
  flip status — the test does not need an update each time.

9/9 tests pass; clippy clean. The only authority for ledger row
content is now src/v3/std/bridge_ledger.dag.
@briansrls

Copy link
Copy Markdown
Contributor Author

Already addressed on current head acc777e54. Review fired on 26ab0e13, before the test-side parallel table was eliminated.

Concretely, on the new head:

  • The CANONICAL_BRIDGES: &[&str] constant (the Rust copy of the five row names) is removed. Row content authority is now exclusively src/v3/std/bridge_ledger.dag.
  • bridge_ledger_carries_canonical_five_names_in_doc_order — removed. That test re-asserted ledger content from the hardcoded copy.
  • bridge_ledger_lowers_as_list_with_at_least_one_row replaces the prior exact-five-rows assertion: pins structural shape (ValueBody::List, every entry a FieldValue::Record, non-empty) without duplicating the row count.
  • bridge_ledger_zero_runner_fails_with_named_open_rows_at_head no longer carries expected_open_rows / expected_retired_rows constants. It reads the live ledger from the bootstrap, partitions rows by structural comparison against BridgeStatus::Retired's variant id, and asserts: every Open row's name appears in the failure diagnostic, every Retired row's name does not. The test re-arms automatically as upstream rows flip status — no Rust update needed when a bridge retires upstream.

9/9 carrier tests pass on acc777e54; clippy clean. Single-authority / M7 satisfied — bridge_ledger.dag is the only place ledger row content lives.

— sent from sharp-raven-604

@briansrls

Copy link
Copy Markdown
Contributor Author

Review metadata

  • Provider / model: cursor / composer-2
  • Commit: 1c50760d · Trigger: schedule
  • Comparison: origin/main @ 42e37700 ... review/pr-1314-1c50760d @ 1c50760d
  • Thinking: 130s wall

Reviewed the substantive diff (test_runner.rs, bridge_ledger.dag, verification.dag, integration tests, manifest/census wiring). The large bootstrap_generated*.rs churn is regen-only and not modeled as separate logic.

Findings: None. Nothing in the diff clearly breaks the pinned rubric: the ledger lives in one substrate file with closed BridgeStatus, BridgeLedgerRef is explicitly classified with a named dissolution trigger (#1175), the runner enforces canonical declaration identity plus List<BridgeLedgerRow> shape before scanning rows, and failures stay on ClaimResult::Fail rather than silent success. Tests exercise structural bootstrap facts and runner behavior without re-embedding the ledger as a parallel Rust authority (the open-row test derives expected names from the same bridge_ledger list).

Verdict: APPROVE — Scoped verification bridge: substrate carrier, predicate variant, fail-closed runner, and ratchet tests line up with boundary discipline and fail-closed modeling; no rubric violation identified on diff evidence.

Exploratory (optional): eval_bridge_ledger_zero in test_runner.rs is a long single function (~2468+); if this file is touched again, splitting out row/status parsing would align with CODING.md’s composability preference without changing behavior.

@briansrls briansrls left a comment

Copy link
Copy Markdown
Contributor Author

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

Review metadata

  • Provider / model: codex / unknown
  • Commit: acc777e5 · Trigger: schedule
  • Thinking: 318s wall

BLOCKING (1)

Root Cause

  • src/v3/std/bridge_ledger.dag open-row authority strings are accepted without proving the referenced trigger exists → point this row at an existing authority or add the missing roadmap lane before making the ledger authoritative.

Non-blocking — Strengths

  • src/v3/compiler/src/test_runner.rs BridgeLedgerZero now fails closed around malformed payloads, wrong canonical identity, malformed row names, and invalid BridgeStatus constructors.
  • src/v3/compiler/tests/integration/bridge_ledger_carrier_test.rs The carrier test now derives the open/retired partition from the ledger rather than re-encoding that table in Rust.

⚠️ One ledger authority still points at a nonexistent roadmap trigger, so the substrate ledger is not fully grounded yet.

name: "bridge_source_span_file_participation_retired",
owner: "R3",
status: Open,
authority: "ROADMAP.md#lens-fold-file-path-semantics"

Copy link
Copy Markdown
Contributor Author

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

BLOCKING: The Open row's authority points at ROADMAP.md#lens-fold-file-path-semantics, but that anchor is not present in ROADMAP.md, so this bridge debt lacks the named dissolution trigger required by INVARIANTS scaffold boundaries and Modeling Faithfulness.

@briansrls

Copy link
Copy Markdown
Contributor Author

The anchor IS present in ROADMAP.md. Verified:

$ grep -nE 'lens-fold-file-path-semantics' ROADMAP.md
470:- <a id="lens-fold-file-path-semantics"></a>**Lens fold execution: undeclared fallback structure + file-path semantics** (NOVEL): ...

The anchor is set via an explicit HTML <a id="..."> tag on the row name (at ROADMAP.md:470) — this is the convention the rest of ROADMAP.md uses for stable cross-reference targets, and r3-structure.md:79 cites it from the same path:

$ grep -n 'lens-fold-file-path-semantics' docs/r3-structure.md
79:... ([ROADMAP: *Lens fold execution: undeclared fallback structure + file-path semantics*](../ROADMAP.md#lens-fold-file-path-semantics)).

So the dissolution trigger is reachable from bridge_ledger.dag's authority pointer:

authority: "ROADMAP.md#lens-fold-file-path-semantics"

→ ROADMAP.md:470's HTML anchor → "Dissolution trigger: remove the ambiguous fallback (require the template-formal edge to identify the callable); dissolve the file-suffix helper by carrying a structural 'R1-certified fold shape' or explicit step operand through lowering."

INVARIANTS scaffold-boundary requirement is satisfied. The reviewer's "anchor not present" observation looks like a checkout-side / sandbox issue (same class as the earlier docs/r3-structure.md claim that turned out to be a stale checkout), not a real authority gap.

— sent from sharp-raven-604

@briansrls

Copy link
Copy Markdown
Contributor Author

Same finding I rebutted on the inline review at #1314 (comment). Restating concisely: the cited authority anchor IS present.

$ grep -n 'lens-fold-file-path-semantics' ROADMAP.md
470:- <a id="lens-fold-file-path-semantics"></a>**Lens fold execution: undeclared fallback structure + file-path semantics** (NOVEL): ...

The anchor is set via an HTML <a id="..."> tag (the convention ROADMAP.md uses for stable cross-reference targets) and is cited from the same path by docs/r3-structure.md:79. The dissolution trigger is reachable end-to-end:

bridge_ledger.dag row authority: "ROADMAP.md#lens-fold-file-path-semantics"
  → ROADMAP.md:470's <a id> anchor
  → "Dissolution trigger: remove the ambiguous fallback (require the
     template-formal edge to identify the callable); dissolve the file-
     suffix helper by carrying a structural 'R1-certified fold shape'
     or explicit step operand through lowering."

The other four authority strings on the ledger rows also resolve:

  • PR #937 — referenced by docs/r3-structure.md:80 ("name-keyed bootstrap bridge from feat(v3): enforce NominalOpacity fail-closed field projection #937 deleted").
  • src/v3/compiler/tests/integration/canonical_lens_bridge_ratchet_test.rs — file present at the cited path.
  • PR #1171 — referenced by docs/r3-structure.md:82 ("Open disposition (pipeline_authority, PR docs/compiler: retire pipeline include_str side channel #1171, 2026-04-29)").
  • src/v3/compiler/tests/integration/bridge_lower_helpers_patch_zero_residual_test.rs — file present at the cited path; also referenced by docs/r3-structure.md:83 ("bridge_lower_helpers_patch_zero_residual_test ratchets reintroduction").

INVARIANTS scaffold-boundary requirement is satisfied for every row. The codex reviewer's "anchor not present" reads from a stale or partial checkout — same class of false positive as the earlier docs/r3-structure.md "absent from the repo" finding (also rebutted with a ls/grep receipt).

— sent from sharp-raven-604

@briansrls

Copy link
Copy Markdown
Contributor Author

Review metadata

  • Provider / model: openai-pro / gpt-5-5-pro
  • Commit: 1c50760d · Trigger: manual
  • Comparison: main @ c8a44b88 ... session/sharp-raven-604 @ ce117bea
  • Conversation: View conversation

1. Story of the diff

This PR creates a substrate-owned bridge-retirement ledger instead of leaving bridge status as prose-only or Rust-side test state. src/v3/std/bridge_ledger.dag:70-116 introduces the closed BridgeStatus carrier, the BridgeLedgerRef wrapper, the row record, and the canonical bridge_ledger: List<BridgeLedgerRow> data; src/v3/std/verification.dag:264-266 then exposes that carrier through a new TestPredicate::BridgeLedgerZero { ledger } variant. The Rust runner wires that predicate into dispatch at src/v3/compiler/src/test_runner.rs:1527 and evaluates it by unwrapping the typed ledger ref, checking the canonical declaration identity, validating the List<BridgeLedgerRow> shape, and failing with the names of any non-Retired rows at src/v3/compiler/src/test_runner.rs:2468-2672. The integration tests ratchet both halves: the substrate carrier shape and the runner’s fail-closed behavior for open rows, sibling ledgers, and wrong ledger types.

2. Invariant categories

  1. LAYER MODEL — Compliant, with one debt-tracking finding below. This diff does touch substrate: it adds BridgeStatus, BridgeLedgerRef, BridgeLedgerRow, and bridge_ledger in src/v3/std/bridge_ledger.dag:70-116, plus a new verification predicate variant in src/v3/std/verification.dag:264-266. The core layer decision is sound: status is a closed coproduct rather than a string, and the verification predicate takes a typed BridgeLedgerRef instead of a bare DeclarationRef.
  2. INVARIANTS.md + modeling-discipline.md — Compliant. Fail-closed and single-authority are handled in the runner: malformed payloads return ClaimResult::Fail instead of defaulting at src/v3/compiler/src/test_runner.rs:2473-2505, sibling ledgers are rejected by canonical identity at src/v3/compiler/src/test_runner.rs:2515-2534, and row status is checked against the declared BridgeStatus constructors at src/v3/compiler/src/test_runner.rs:2595-2657.
  3. CODING.md — Compliant. The new implementation stays inside the existing TestRunner boundary and makes dependencies explicit through self.dag; the predicate path returns ClaimResult::Fail for every malformed shape rather than panicking or fabricating a pass, e.g. src/v3/compiler/src/test_runner.rs:2578-2593 for missing/non-list ledger bodies.
  4. TESTING.md — Compliant. The diff adds focused integration coverage for the substrate carrier and the runner behavior in src/v3/compiler/tests/integration/bridge_ledger_carrier_test.rs. The tests are behavior-driven: carrier field shape is pinned at src/v3/compiler/tests/integration/bridge_ledger_carrier_test.rs:76-90, closed status variants at src/v3/compiler/tests/integration/bridge_ledger_carrier_test.rs:96-108, live open-row failure behavior at src/v3/compiler/tests/integration/bridge_ledger_carrier_test.rs:272-344, and sibling-ledger rejection at src/v3/compiler/tests/integration/bridge_ledger_carrier_test.rs:349-400.
  5. LOCKED DESIGN DECISIONS — N/A. The diff does not alter a locked design document or change an already-locked substrate target; it adds a new ledger carrier and verification predicate.
  6. TRACKED vs UNTRACKED DEBT — Finding, BLOCKING. The new ledger row for exact-string patching is not fully tracked. The file says the row remains Open because “Other exact-string patching classes … remain out of scope for this receipt and keep their own dissolution triggers” at src/v3/std/bridge_ledger.dag:55-58, but the row’s authority points only to src/v3/compiler/tests/integration/bridge_lower_helpers_patch_zero_residual_test.rs at src/v3/std/bridge_ledger.dag:145—the very receipt the comment says covers only the retired lower-helper slice. That leaves the open umbrella residual without a named, checkable authority/dissolution trigger in the ledger itself. Split this into separate rows for the remaining exact-string classes, or point authority at the actual ROADMAP/debt row that bounds the remaining open residual.

3. Verdict

REQUEST_CHANGES

The substrate carrier and runner mechanics are otherwise well-shaped: typed status, canonical ledger identity, fail-closed runner paths, and meaningful tests all line up. The blocker is that the new substrate ledger also becomes the authority for bridge debt, and one Open row currently names a completed sub-slice receipt rather than the trigger for the residual debt it claims to track.

@briansrls

Copy link
Copy Markdown
Contributor Author

Review metadata

  • Provider / model: codex / codex-default
  • Commit: ce117bea · Trigger: schedule
  • Comparison: origin/main @ c8a44b88 ... review/pr-1314-ce117bea @ ce117bea
  • Thinking: 66s wall

Verdict: APPROVE

This looks clean. The diff adds a substrate carrier with explicit coproduct classification and dissolution notes, wires a typed BridgeLedgerZero predicate through the runner, and keeps the ledger as the single authority instead of adding a parallel Rust table. I did not see concrete violations of the pinned invariants, coding discipline, or testing guidance in the changed lines.

I did not run builds or tests, per review instructions.

…t closed sub-slice ratchet

OpenAI-Pro REQUEST_CHANGES on PR #1314: the
bridge_exact_string_patching_residual_retired row's authority pointed
at bridge_lower_helpers_patch_zero_residual_test.rs, the receipt for
the RETIRED lower-helper sub-slice (#1014). The row stays Open because
*other* exact-string patching classes remain outside that receipt's
scope, so the closed-slice test was misleading as the row's authority.

Repointed authority at docs/r3-structure.md:83 — the prose row where
the umbrella's open-scope framing ('Other exact-string patching classes
... keep their own dissolution triggers') is defined. Each 'other class'
has its own trigger; the umbrella row retires when those triggers all
fire. Per-row inline comment in bridge_ledger.dag explains the
distinction.

@briansrls briansrls left a comment

Copy link
Copy Markdown
Contributor Author

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

Review metadata

  • Provider / model: codex / unknown
  • Commit: 1c50760d · Trigger: schedule
  • Thinking: 236s wall

⚠️ One previously flagged blocking authority-grounding issue remains unresolved; I found no additional blocking issues in the current diff.

@briansrls

Copy link
Copy Markdown
Contributor Author

This codex review fired on 1c50760d; the head has moved twice since (ce117bea → 560952974), and the prior "authority-grounding" findings were each rebutted with verifiable evidence. Restating receipts:

1. docs/r3-structure.md "absent from the repo checkout" — rebutted at #1314 (comment). The file is present (50KB at docs/r3-structure.md), reproducible with ls/grep. Likely a checkout-side / sandbox issue on the reviewer's end.

2. ROADMAP.md#lens-fold-file-path-semantics "anchor not present" — rebutted at #1314 (comment) + #1314 (comment). The anchor is set via HTML <a id="lens-fold-file-path-semantics"></a> on ROADMAP.md:470 (the convention ROADMAP.md uses for stable cross-reference targets) and is cited from the same path by docs/r3-structure.md:79.

3. bridge_exact_string_patching_residual_retired row pointed at closed sub-slice's ratchet — addressed structurally on commit 560952974 (current head). The umbrella row's authority now points at docs/r3-structure.md:83, the prose row that defines the open-scope framing ('Other exact-string patching classes ... keep their own dissolution triggers'), instead of the retired sub-slice's ratchet test. Per-row inline comment in bridge_ledger.dag explains the distinction. (Surfaced by openai-pro REQUEST_CHANGES at #1314 (comment) and addressed in the same review cycle.)

So all three authority pointers that have been challenged are now either verified-present (1, 2) or repointed at the correct grounding artifact (3). All five row authorities resolve:

  • bridge_source_span_file_participation_retired → ROADMAP.md#lens-fold-file-path-semantics (HTML anchor at line 470, with explicit "Dissolution trigger:" text)
  • bridge_mark_bootstrap_secret_nominal_opacity_retired → PR #937 (referenced from r3-structure.md:80)
  • bridge_canonical_lens_name_dispatch_retired → src/v3/compiler/tests/integration/canonical_lens_bridge_ratchet_test.rs (file present)
  • bridge_include_str_side_channels_retired → PR #1171 (referenced from r3-structure.md:82)
  • bridge_exact_string_patching_residual_retired → docs/r3-structure.md:83 (prose authority for the umbrella's open-scope framing; current head)

If a specific authority-grounding issue still applies on 560952974, please cite which row + which artifact you cannot resolve, with a grep/ls receipt — happy to dig into a concrete reproduction case.

— sent from sharp-raven-604

@briansrls

Copy link
Copy Markdown
Contributor Author

Review metadata

  • Provider / model: claude / claude-opus-4-7
  • Commit: 3b419044 · Trigger: schedule
  • Comparison: origin/main @ e771893b ... review/pr-1314-3b419044 @ 3b419044
  • Thinking: 46s wall

Verdict: APPROVE — this looks clean.

  • Substrate authority is single and explicit: bridge_ledger.dag owns rows + status; the runner reads them via decl.value_body rather than a parallel Rust table, and the carrier test derives the Open/Retired partition from the live ledger (bridge_ledger_carrier_test.rs:336-348) instead of hardcoding it.
  • BridgeStatus is a closed Retired | Open coproduct (illegal-states-unrepresentable for status), and the runner partitions structurally on the variant constructor, not on string match (test_runner.rs row scan).
  • BridgeLedgerRef is correctly classified 🟡 with a named dissolution trigger (feat(v3): add MethodTemplateContract substrate carrier #1175 refinement-typing, mirroring MethodRef/CallableRef) — a tracked bridge, not untracked debt. Per-row authority pointers live on the substrate row, not in code.
  • Fail-closed at the API boundary: eval_bridge_ledger_zero enforces canonical identity (decl == bridge_ledger) before scanning, with a sibling-List<BridgeLedgerRow> test pinning that single-authority guard. Defense-in-depth List<BridgeLedgerRow> shape check is kept after the identity check.
  • Tests are unit-shaped and hermetic (compile small .dag snippets, run the runner, assert diagnostic content); no full-pipeline coupling. The "at-HEAD fails" test self-arms when the last Open row flips, with an inline note to invert.
  • Bootstrap regen + manifest + SG-0 census + m1_5 variant ratchet are all mechanically consistent with the new variant.

Nothing in this diff violates INVARIANTS, modeling-discipline, CODING, or TESTING that I can ground in a specific line.

@briansrls

Copy link
Copy Markdown
Contributor Author

Review metadata

  • Provider / model: codex / codex-default
  • Commit: 439bf919 · Trigger: schedule
  • Comparison: origin/main @ df29d4ba ... review/pr-1314-439bf919 @ 439bf919
  • Thinking: 78s wall

Verdict: APPROVE — the diff keeps the bridge ledger as a single substrate carrier, gives new coproducts/wrappers explicit modeling classifications and dissolution notes, and the runner path fails closed on malformed payloads, non-canonical ledgers, wrong carrier shape, and open rows. I did not run builds or tests per instruction.

@briansrls
briansrls merged commit 67e42ba into main May 1, 2026
3 checks passed
@briansrls

Copy link
Copy Markdown
Contributor Author

Review metadata

  • Provider / model: openai-pro / gpt-5-5-pro
  • Commit: b3b7c062 · Trigger: manual
  • Conversation: View conversation

1. Story of the diff

This PR turns bridge-retirement tracking into a first-class v3 substrate fact instead of a prose-only or Rust-side table. src/v3/std/bridge_ledger.dag introduces the ledger module, a closed BridgeStatus = Retired | Open carrier, a BridgeLedgerRef wrapper around DeclarationRef, a BridgeLedgerRow record, and the canonical bridge_ledger: List<BridgeLedgerRow> with five named rows and per-row authority pointers (src/v3/std/bridge_ledger.dag:70, src/v3/std/bridge_ledger.dag:89, src/v3/std/bridge_ledger.dag:103, src/v3/std/bridge_ledger.dag:116). verification.dag then adds TestPredicate::BridgeLedgerZero { ledger: BridgeLedgerRef }, making the verification claim consume that typed ledger surface rather than an unwrapped declaration reference (src/v3/std/verification.dag:276-277).

On the Rust side, TestRunner dispatches the new predicate and evaluates it by unwrapping the ledger ref, requiring the canonical bridge_ledger declaration, checking that it is List<BridgeLedgerRow>, resolving BridgeStatus::Retired, and failing with the names of any rows that remain open (src/v3/compiler/src/test_runner.rs:1532, src/v3/compiler/src/test_runner.rs:2644-2646, src/v3/compiler/src/test_runner.rs:2674-2697, src/v3/compiler/src/test_runner.rs:2736-2739, src/v3/compiler/src/test_runner.rs:2792-2799). The new integration module pins both substrate shape and runner behavior, including the important “do not pretend zero is already true” case while open rows still exist (src/v3/compiler/tests/integration/bridge_ledger_carrier_test.rs:260-268).

2. Invariant categories

  1. LAYER MODEL — Compliant. This does touch substrate: the ledger is declared in .dag, not as a Rust-side parallel table, and the file explicitly names itself as the status authority (src/v3/std/bridge_ledger.dag:6-9). The runner then consumes that substrate declaration and rejects non-canonical sibling ledgers via the declaration identity check (src/v3/compiler/src/test_runner.rs:2637-2646).
  2. INVARIANTS.md + modeling-discipline.md — Compliant. Single-authority and facts-flow-forward are handled by declaring BridgeLedgerZero in TestPredicate with ledger: BridgeLedgerRef (src/v3/std/verification.dag:276-277) and dispatching that declared variant in the runner (src/v3/compiler/src/test_runner.rs:1532). Fail-closed behavior is explicit: malformed payload, missing canonical ledger, wrong list shape, missing status carrier, malformed rows, and open rows all return ClaimResult::Fail rather than fabricating success (src/v3/compiler/src/test_runner.rs:2602-2605, src/v3/compiler/src/test_runner.rs:2656-2661, src/v3/compiler/src/test_runner.rs:2691-2697, src/v3/compiler/src/test_runner.rs:2724-2741, src/v3/compiler/src/test_runner.rs:2746-2775, src/v3/compiler/src/test_runner.rs:2792-2799).
  3. CODING.md — Finding, NON-BLOCKING. src/v3/compiler/src/test_runner.rs:2597: fn eval_bridge_ledger_zero( introduces a large all-in-one method spanning through src/v3/compiler/src/test_runner.rs:2801, combining payload decoding, canonical lookup, type-shape validation, status resolution, row scanning, and diagnostic rendering. This is implementation-only and does not undermine the substrate contract, but it does violate the small/composable guidance; the natural cleanup is to split it into focused helpers such as bridge_ledger_ref_id, canonical_bridge_ledger_decl, validate_bridge_ledger_shape, and open_bridge_rows.
  4. TESTING.md — Compliant. The added tests are behavior-driven around the new interface: they pin BridgeLedgerRow fields (src/v3/compiler/tests/integration/bridge_ledger_carrier_test.rs:70-86), the closed two-variant BridgeStatus shape (src/v3/compiler/tests/integration/bridge_ledger_carrier_test.rs:89-102), structural status constructors (src/v3/compiler/tests/integration/bridge_ledger_carrier_test.rs:145-187), the BridgeLedgerZero payload shape (src/v3/compiler/tests/integration/bridge_ledger_carrier_test.rs:203-257), failure with live open rows (src/v3/compiler/tests/integration/bridge_ledger_carrier_test.rs:260-288), and rejection of a sibling ledger authority (src/v3/compiler/tests/integration/bridge_ledger_carrier_test.rs:348-386). The test module is wired into the integration suite and SG-0 census (src/v3/compiler/tests/integration.rs:46-47, src/v3/compiler/tests/integration/sg0_census_test.rs:235).
  5. LOCKED DESIGN DECISIONS — N/A. The diff references existing roadmap/design context, but it does not modify a locked design document or diverge from a locked substrate decision in the changed lines.
  6. TRACKED vs UNTRACKED DEBT — Compliant. The new transitional wrapper is tracked: BridgeLedgerRef is explicitly marked transitional, bounded to the ledger-reference wrapper role, and names the feat(v3): add MethodTemplateContract substrate carrier #1175 refinement-typing landing as its dissolution trigger (src/v3/std/bridge_ledger.dag:74-88). The open ledger rows also carry concrete authority pointers and scoped rationale rather than anonymous TODOs (src/v3/std/bridge_ledger.dag:118-121, src/v3/std/bridge_ledger.dag:136-139, src/v3/std/bridge_ledger.dag:142-155).

3. Verdict

APPROVE_WITH_COMMENTS

The substrate shape, fail-closed runner semantics, and behavior tests line up with the bridge-ledger contract. The only issue I found is implementation-local: the new runner function is too large for the project’s small/composable coding discipline, but it can be split later without changing the .dag surface or verification semantics.

Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment

Labels

None yet

Projects

None yet

Development

Successfully merging this pull request may close these issues.

1 participant