Skip to content
Merged
88 changes: 46 additions & 42 deletions docs/briefs/r3-v-bridge-retirement-ledger-zero-audit.md
Original file line number Diff line number Diff line change
Expand Up @@ -29,23 +29,25 @@ The production fixture from PR #1352 is structurally wired:
`bridge_ledger`, checks the carrier is `List<BridgeLedgerRow>`, and returns
`Pass` iff every row's status constructor is `Retired`.

Current live ledger fold is red: rows #1, #4, and #5 are `Open`. This audit also
found one status drift candidate in the canonical-lens row. Director ratified
Option 2 for that drift: split the row by class, preserving the narrow PR #1183
retired slice and adding an open broader canonical-lens-name patching residual.
Substrate Manager owns the substrate row edit; this audit records the ratified
disposition only.
Current live ledger fold is red: only rows **#1** (`bridge_source_span_file_participation_retired`)
and **#6** (`bridge_exact_string_semantic_patching_residual`) are `Open` in
`bridge_ledger.dag`. Canonical-lens split rows **#3a** and **#3b** are both
**`Retired`** in the live ledger (authorities on each row in
`src/v3/std/bridge_ledger.dag`). Exact-string work uses the same *split shape* as
modeling discipline: narrow lower-helper row **#5** is `Retired`, Row-4 semantic
remainder **#6** stays explicitly `Open`.

## Row Audit

| # | Ledger row | Ledger status | Code state at HEAD | Ratchet / authority | Drift signal |
|---|---|---|---|---|---|
| 1 | `bridge_source_span_file_participation_retired` | `Open` | Open. Audit-packet progress (PR #2150 merged 2026-05-07): row #2 (kernel `Bool` bootstrap patch lookup) **partial** — path-string encapsulated behind `BootstrapAuthorityKey::for_kernel_bool()`, full dissolution awaits row #14 retirement; row #6 (pipeline authority file guard, bootstrap.rs slice) **retired** via typed `BootstrapAuthorityKey::for_pipeline_authority()` + witness-derived spans (`pipeline_authority.rs` stage-binding walk + `compile` arrow lowering remain under separate ownership). Production/lens paths still consult `SourceSpan.file` for participation or filtering: `lens_apply.rs::behavior_source_file`, `reflect_program_dag_nodes_in_file` / `fold_lens_over_reflected_program`, lower's `DIMENSION_STD_AUTHORITY_FILE` gates, and emit `source_filtering.excludes`. | `r3-structure.md` L87; `ROADMAP.md#lens-fold-file-path-semantics`; PR #2150 audit-packet receipt. | None. Ledger `Open` matches code. |
| 2 | `bridge_mark_bootstrap_secret_nominal_opacity_retired` | `Retired` | Retired. `dag.rs::bridge_mark_bootstrap_secret_nominal_opacity_retired` asserts `Secret.nominal_opacity` exists in std, full bootstrap, and without-parse-surface snapshots. No live `mark_bootstrap_secret_nominal_opacity` helper remains. | Rust unit test in `src/v3/compiler/src/dag.rs`; Secret nominal-opacity lineage #1272 / old row authority `PR #937`. | None for status. Authority string is historical but not contradictory. |
| 3a | `bridge_canonical_lens_name_dispatch_pr1183_slice_retired` | Pending substrate split; ratified target `Retired` | Retired at narrow PR #1183 scope. The specific dispatch path covered by #1183 is treated as closed by Director-ratified split. | PR #1183 dispatch path; `canonical_lens_bridge_ratchet_test.rs` narrow ratchet; Director #828 c#4358798673. | None after Substrate Mgr authors the split. The prior single-row drift is resolved by class enumeration, not by treating all canonical-lens-name patching as retired. |
| 3b | `bridge_canonical_lens_name_patching_residual` | Pending substrate split; ratified target `Open` | Open. `canonical_lens_bridge_ratchet_test.rs` pins two canonical-lens `include_str!` constants, two `lens_decl.name.as_deref() == Some(...)` dispatch arms, and two generic name-keyed lookups in `test_runner.rs`. Dissolution trigger: PB-Runtime interpreter-as-data or a typed lens-registry carrier. | Broader exact-string canonical-lens-name class; Director #828 c#4358798673. | None after Substrate Mgr authors the split. Until then, the live single substrate row remains coarser than the ratified class model. |
| 4 | `bridge_include_str_side_channels_retired` | `Open` | Open. `pipeline_authority.rs` explicitly says compile-body cross-check remains suspended because `fn compile` lowers to `ArrowBody::Unparsed`; the prior `include_str!`/file-read side-channel is rejected until a structural compile-body witness exists. | [`design-emission-model.md`](../design-emission-model.md) §"Per Director directive 2026-04-28 (gpt-5-5-pro reflective analysis)" (`include_str!` retirement / `bridge_include_str_side_channels_retired` bullet); `pipeline_authority.rs`; PR #1171. | None. Ledger `Open` matches code. |
| 5 | `bridge_exact_string_patching_residual_retired` | `Open` | Open at umbrella scope. The lower-helper sub-slice is retired and ratcheted by `bridge_lower_helpers_patch_zero_residual_test.rs`, but other exact-string patch classes remain. `bootstrap.rs::patch_kernel_bool_boolean_algebra_inhabits` is a live class-5-style residual called from bootstrap paths. | `r3-structure.md` L91; `r2-closure-ledger.md` Tier-2 row; #1014 + #1192 narrow receipt. | None. Ledger `Open` correctly refuses to treat the lower-helper sub-slice as umbrella closure. |
| 3a | `bridge_canonical_lens_name_dispatch_pr1183_slice_retired` | `Retired` | Retired in ledger. Narrow PR #1183 dispatch slice; ratchet `canonical_lens_bridge_ratchet_test.rs`. | `src/v3/compiler/tests/integration/canonical_lens_bridge_ratchet_test.rs`; Director #828 c#4358798673. | None. Ledger `Retired` matches substrate row. |
| 3b | `bridge_canonical_lens_name_patching_residual` | `Retired` | Retired in ledger per canonical-lens name-dispatch closure receipt; authority `docs/briefs/r3-pb-bridge-canonical-lens-name-dispatch-closure.md`. PB-Runtime may still carry transitional `include_str!` / name-keyed surfaces in `test_runner.rs` until interpreter-as-data — track via that brief, not a parallel `Open` ledger row. | Closure brief + `canonical_lens_bridge_ratchet_test.rs` pins; gate #33 lineage. | None. Ledger `Retired` matches substrate row (do not narrate this row as `Open` while the ledger says otherwise). |
| 4 | `bridge_include_str_side_channels_retired` | `Retired` | Retired for the pipeline-authority slice per `bridge_ledger.dag` authority (`l1_5_fixed_point_test.rs` ratchet). `fn compile` still lowers as `ArrowBody::Unparsed`; broader compile-body witness debt is out of scope for this row's retired verdict. | `src/v3/std/bridge_ledger.dag`; `src/v3/compiler/tests/integration/l1_5_fixed_point_test.rs`. | None. Ledger `Retired` matches the landed slice receipt. |
| 5 | `bridge_exact_string_patching_residual_retired` | `Retired` | Retired at PB Tier-2 lower-helper generated-Rust exact-string patch scope (#1014 / #1192). `bridge_lower_helpers_patch_zero_residual_test.rs` ratchets zero residual for the contiguous forbidden token class. | `src/v3/compiler/tests/integration/bridge_lower_helpers_patch_zero_residual_test.rs`. | None. Ledger `Retired` matches the narrow ratchet. |
| 6 | `bridge_exact_string_semantic_patching_residual` | `Open` | Open. Row-4 semantic exact-string patching outside the retired lower-helper slice (e.g. bootstrap `Bool` inhabits patch class, BR-06 non-canonical sentinel splice, infer-helper-driven rewrite classes). | `docs/briefs/r3-v-bridge-row-4-exact-string-deeper-detail-receipt.md`. | None. Ledger `Open` matches remaining class inventory. |

## Code-State Evidence

Expand All @@ -55,16 +57,17 @@ disposition only.
replace those path checks.
- #2 is backed by an executable Rust unit ratchet over generated snapshots. This
is a stronger signal than prose status, so `Retired` is grounded.
- #3's live ratchet is a nonzero-count pin, not a zero-residual gate. Director
ratified splitting the narrow PR #1183 retired path from the broader open
canonical-lens-name patching class, so the anti-growth evidence feeds the open
residual row instead of falsely closing the whole class.
- #4's authority is explicit in `pipeline_authority.rs`: compile-body drift
detection is suspended until a structural witness exists. That is a deliberate
open row, not missing coverage.
- #5 correctly distinguishes the retired lower-helper class from the umbrella.
The lower-helper ratchet should feed the umbrella; it should not be read as
the umbrella's only required evidence.
- #3a/#3b are both **`Retired`** in the live ledger (split landed in substrate;
see row authorities). PB may still carry transitional name-dispatch / `include_str!`
surfaces in Rust until interpreter-as-data; that debt is **not** an `Open`
`bridge_ledger` row — it is scoped by the closure brief on row **#3b**.
- #4 is `Retired` for the pipeline-authority `include_str!` slice at the ledger's
current authority pointer; broader `ArrowBody::Unparsed` compile-body witness
debt is tracked outside this row's closed verdict.
- #5/#6 split is the exact-string analogue of the canonical-lens **Q2 class
split**, but the ledger outcomes differ: canonical-lens **#3a/#3b are both
`Retired`** at HEAD, while exact-string keeps an explicit **`Open`** remainder
row **#6** for Row-4 semantic patching until that class retires.

## Production TestClaim Verification

Expand All @@ -75,7 +78,7 @@ The TestClaim shape is complete for the live carrier:
`BridgeLedgerZero { ledger: { decl: bridge_ledger } }`.
- The current mandatory `source: ""` field remains a known `TestClaim` shape
limitation; the typed predicate payload is the actual subject.
- `m1_5_verification_test.rs::r3_bridge_retirement_ledger_zero_fixture_reports_open_rows_at_head`
- `m1_5_verification_test.rs::r3_bridge_retirement_ledger_zero_open_row_count_ratchet`
compiles the fixture through a performance-only `OnceLock`, runs the suite,
derives the live open-row names from the bootstrap ledger, and asserts the
diagnostic names every open row.
Expand All @@ -98,25 +101,26 @@ the last bridge owner lands its structural retirement receipt and the canonical

## Routing

Director ratified Option 2: sub-class split per the Q2 pattern. Substrate Mgr
authors the substrate-row split per the ratified row structure in #828
c#4358798673:

- `bridge_canonical_lens_name_dispatch_pr1183_slice_retired`: `Retired`;
authority is the PR #1183 dispatch path / narrow ratchet.
- `bridge_canonical_lens_name_patching_residual`: `Open`; authority is the
broader exact-string canonical-lens-name class with two `include_str!`
constants, two `lens_decl.name.as_deref()` arms, and two generic name-keyed
lookups. Dissolution trigger is PB-Runtime interpreter-as-data or a typed
lens-registry carrier.

This PR does not change the row because status ownership lives in the substrate
ledger. Do not close `bridge_retirement_ledger_zero` while the ratified split is
pending in substrate.

**Q2 pattern second instance:** this row split mirrors bridge #5
(`bridge_exact_string_patching_residual_retired` umbrella =>
`bridge_lower_helpers_patch_zero_residual` narrow + open broader umbrella).
Future bridge-retirement work defaults to per-class enumeration per
`feedback_coproduct_dissolution` and
Director-ratified **Q2 split** for canonical-lens rows is **authored in
`bridge_ledger.dag`** at HEAD:

- `bridge_canonical_lens_name_dispatch_pr1183_slice_retired`: **`Retired`**;
authority `canonical_lens_bridge_ratchet_test.rs` (PR #1183 narrow slice).
- `bridge_canonical_lens_name_patching_residual`: **`Retired`**; authority
`docs/briefs/r3-pb-bridge-canonical-lens-name-dispatch-closure.md` (gate #33 /
closure receipt — not an `Open` ledger row).

Exact-string **Q2 split** is the same structural idea with a different ledger
outcome: remainder row **`bridge_exact_string_semantic_patching_residual` stays
`Open`** until Row-4 semantic classes retire.

Canonical-lens and exact-string **Q2 splits** are authored in the substrate
ledger (`src/v3/std/bridge_ledger.dag`); Verification audits
`bridge_retirement_ledger_zero` against the live rows — do not treat prose-only
updates as ledger flips.

**Q2 pattern second instance:** `bridge_exact_string_patching_residual_retired`
(narrow lower-helper slice, `Retired`) + `bridge_exact_string_semantic_patching_residual`
(open Row-4 remainder). Future bridge-retirement work defaults to per-class
enumeration per `feedback_coproduct_dissolution` and
`feedback_state_space_vs_behavioral_invariants`.
Original file line number Diff line number Diff line change
Expand Up @@ -3,7 +3,12 @@
**Status:** AUDIT RECEIPT - docs-only. This receipt does not flip any
`BridgeLedgerRow.status` and does not close a Debt-Paydown row directly.

**Row:** `bridge_exact_string_patching_residual_retired`.
**Ledger rows (split, substrate authority `src/v3/std/bridge_ledger.dag`):**
`bridge_exact_string_patching_residual_retired` (**Retired** — PB Tier-2
lower-helper exact-string patch class, #1014 / #1192 ratchet) and
`bridge_exact_string_semantic_patching_residual` (**Open** — Row-4 remainder).
This receipt inventories the **Open** Row-4 semantic class bucket; it does not
re-litigate the closed lower-helper slice.

**Primary inputs:** `docs/briefs/bridge-retirement-audit-include-str-family.md`
for family B BR-19 / BR-09 exact-string boundaries, and
Expand Down
2 changes: 1 addition & 1 deletion docs/r3-program-plan.md
Original file line number Diff line number Diff line change
Expand Up @@ -258,7 +258,7 @@ This principle is NOT a separate lane; it's a per-lane gate-shape requirement ap
| 32 | `bridge_mark_bootstrap_secret_nominal_opacity_retired` | state-check | T-Bridge-Retirement | **PASSING** | `dsl/std/types.dag` `type Secret nominal_opaque = String` + `src/v3/std/bridge_ledger.dag` row `Retired` + unit ratchet `dag.rs::bridge_mark_bootstrap_secret_nominal_opacity_retired` (bootstrap snapshots carry `Declaration.nominal_opacity` on `Secret`); historical name-keyed bootstrap bridge removed (#1272 / #937 lineage) |
| 33 | `bridge_canonical_lens_name_dispatch_retired` | state-check | T-Bridge-Retirement | DECLARED | DeclarationRef/typed identity |
| 34 | `bridge_include_str_side_channels_retired` | state-check | T-Bridge-Retirement | DECLARED | substrate query surface |
| 35 | `bridge_exact_string_patching_residual_retired` | state-check | T-Bridge-Retirement | DECLARED | umbrella for exact-string scaffolds |
| 35 | `bridge_exact_string_patching_residual_retired` | state-check | T-Bridge-Retirement | **PASSING** | PB lower-helper slice retired in `bridge_ledger.dag`; residual Row-4 classes → `bridge_exact_string_semantic_patching_residual` (Open) |
| 36 | `bridge_retirement_ledger_zero` | ledger-count | T-Bridge-Retirement | DECLARED | unified ledger reports 0 |
| 37 | `cost_lens_reads_target_realization` | structural-fold | T-CostLens-Composition | **INTEGRATION_RECEIPT (partial — ε-slice)** — PR #2181 ε path: `lens_cost_target_realization_test.rs` proves (i) **TypeRealization** slice: Rust-side `symbolic_cost_of` on a tiny program × `rust_int` row `cost` composed via `Semiring<SymbolicCost>` `sequential`; (ii) **CallableRealization** slice: bootstrap `rust_is_empty_callable` row `cost` readable as a lowered structural field (same row-shape discipline as (i), **without** a second `sequential` composition pin in that subtest). **Not** full emit-time / `LanguageSpec`-indexed cost-lens consumer (that closure remains with gates **#40** / **#70** / follow-on slices per program plan). Historical gate id; lens output stays abstract `SymbolicCost`. | ε-slice receipt; emit-time fold follow-on |
| 38 | `coercion_cost_equals_complexity_by_construction` | structural-fold | T-CostLens-Composition | **SATISFIED-BY-CONSTRUCTION** (α-narrow PR #2171; `Semiring<SymbolicCost>` `sequential`/`iterate` at `src/v3/std/algebra.dag:181-188` is sole composition authority — no parallel "complexity-vs-cost" reconciliation surface exists) | thesis unification holds structurally |
Expand Down
5 changes: 3 additions & 2 deletions docs/r3-structure.md
Original file line number Diff line number Diff line change
Expand Up @@ -116,8 +116,9 @@ L6 (`l6_structural_form_coverage`) was moved out of this lane during the engine-
- `bridge_source_span_file_participation_retired` — **Green predicate:** no production code path consults `SourceSpan.file` for participation/inclusion logic; participation is structural per declared facts. **Current state (R3-deferred; Director acceptance #1130 / dispatch #1139, 2026-04-29):** the gate is not satisfied; partial string-check retirement was rejected because parallel participation rules would remain. Production inclusion (distinct from diagnostics-only span use) is still keyed on path / `span.file` at: `src/v3/compiler/src/lens_apply.rs` (`behavior_source_file`, `reflect_program_dag_nodes_in_file` / `fold_lens_over_reflected_program`); `src/v3/compiler/src/lower.rs` (`lower_type_alias_refinements_phase` `dsl/std/types.dag` gate; `declaration_name_preference_rank` duplicate merge; `Dimension` + `DIMENSION_STD_AUTHORITY_FILE`); `src/v3/compiler/src/emit.rs` (`source_filtering.excludes` on declaration/bind spans). **Structural prerequisites:** module/compilation-unit identity for lens reflection; typed authority/emit-scope carriers for lower/emit; fold-shape / carrier work for remaining fold-path source-path semantics ([ROADMAP: *Lens fold execution: undeclared fallback structure + file-path semantics*](../ROADMAP.md#lens-fold-file-path-semantics)).
- `bridge_mark_bootstrap_secret_nominal_opacity_retired` — name-keyed bootstrap bridge from #937 deleted; nominal-opacity authority lives in source-level declaration (PR A landed in R2)
- `bridge_canonical_lens_name_dispatch_retired` — lens dispatch routes via `DeclarationRef`/typed identity, not canonical name strings
- `bridge_include_str_side_channels_retired` — no `include_str!` macro reads source-substrate identity; substrate query surface used instead. **Open disposition (`pipeline_authority`, PR #1171, 2026-04-29):** `compile` remains `ArrowBody::Unparsed`, so compile-body stage order is not yet a structural Dag fact; runtime ordering reads `PipelineStageBinding` only — full gate for this site awaits derivation / lowered compile witness, not file IO.
- `bridge_exact_string_patching_residual_retired` — umbrella row for exact-string patching scaffolds. **PB lower-helper slice (Tier-2 / #1014 lineage) is pinned at zero** in v3-compiler Rust: no `patch_lower_helpers*` code paths remain, and `bridge_lower_helpers_patch_zero_residual_test` ratchets reintroduction. **Other** exact-string patching classes (outside this retired lower-helper post-process bridge) remain **out of scope for this receipt** and keep their own dissolution triggers.
- `bridge_include_str_side_channels_retired` — **Ledger `Retired`** for the active `pipeline.dag` compile-time embed under `src/v3/compiler/`: replaced by a structural bootstrap witness over `PipelineStageBinding`, with `l1_5_fixed_point_test.rs` ratcheting reintroduction of `include_str!("pipeline.dag")` under the compiler crate (see `src/v3/std/bridge_ledger.dag` header). **Follow-on (`pipeline_authority`, PR #1171):** `fn compile` still lowers as `ArrowBody::Unparsed`, so compile-body stage order is not yet a structural Dag fact for broader authority; that emission-model work is separate from the ledger row’s closed slice verdict.
- `bridge_exact_string_patching_residual_retired` — **Retired** for the PB Tier-2 lower-helper generated-Rust exact-string patch class (#1014 / #1192 lineage): no `patch_lower_helpers*` code paths remain; `bridge_lower_helpers_patch_zero_residual_test` ratchets reintroduction; ledger authority is `src/v3/std/bridge_ledger.dag` + that test path.
- `bridge_exact_string_semantic_patching_residual` — **Open** ledger row for Row-4 semantic exact-string patching **outside** the retired lower-helper slice (bootstrap `Bool` inhabits patch class, BR-06 non-canonical sentinel splice, infer-helper-driven rewrite classes, etc.); authority and class inventory live in `docs/briefs/r3-v-bridge-row-4-exact-string-deeper-detail-receipt.md`.
- `bridge_retirement_ledger_zero` — unified ledger reports 0 named identity bridges remaining
- **T-V2-Retirement** (NEW 2026-04-30; pulled into R3 per user directive *"nothing can be deferred past R3"*).
- `v2_oracle_no_remaining_test_consumers` — no `.rs` test file under the workspace consumes anything from `src/v2/`; v2-oracle and v2-using test scaffolds retired
Expand Down
Loading
Loading