diff --git a/docs/briefs/r3-v-bridge-retirement-ledger-zero-audit.md b/docs/briefs/r3-v-bridge-retirement-ledger-zero-audit.md index a59442466f6..428fdc18119 100644 --- a/docs/briefs/r3-v-bridge-retirement-ledger-zero-audit.md +++ b/docs/briefs/r3-v-bridge-retirement-ledger-zero-audit.md @@ -29,12 +29,13 @@ The production fixture from PR #1352 is structurally wired: `bridge_ledger`, checks the carrier is `List`, 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 @@ -42,10 +43,11 @@ disposition only. |---|---|---|---|---|---| | 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 @@ -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 @@ -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. @@ -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`. diff --git a/docs/briefs/r3-v-bridge-row-4-exact-string-deeper-detail-receipt.md b/docs/briefs/r3-v-bridge-row-4-exact-string-deeper-detail-receipt.md index f1d98136682..8c6be49b503 100644 --- a/docs/briefs/r3-v-bridge-row-4-exact-string-deeper-detail-receipt.md +++ b/docs/briefs/r3-v-bridge-row-4-exact-string-deeper-detail-receipt.md @@ -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 diff --git a/docs/r3-program-plan.md b/docs/r3-program-plan.md index cbf5f14d142..058d43c3915 100644 --- a/docs/r3-program-plan.md +++ b/docs/r3-program-plan.md @@ -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` `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` `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 | diff --git a/docs/r3-structure.md b/docs/r3-structure.md index 484f1eb3ae3..d7f753f9eda 100644 --- a/docs/r3-structure.md +++ b/docs/r3-structure.md @@ -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 diff --git a/src/v3/compiler/src/bootstrap_generated.rs b/src/v3/compiler/src/bootstrap_generated.rs index 2de7ca6c8a9..f10f258053a 100644 --- a/src/v3/compiler/src/bootstrap_generated.rs +++ b/src/v3/compiler/src/bootstrap_generated.rs @@ -26951,7 +26951,7 @@ fn bootstrapped_fixture_dag_declarations() -> Vec { value_body: None, refinement: None, nominal_opacity: None, - span: SourceSpan::new("src/v3/std/bridge_ledger.dag", 4559, 4597), + span: SourceSpan::new("src/v3/std/bridge_ledger.dag", 4697, 4735), }); declarations.push(Declaration { id: DeclarationId(890), @@ -26970,7 +26970,7 @@ fn bootstrapped_fixture_dag_declarations() -> Vec { value_body: None, refinement: None, nominal_opacity: None, - span: SourceSpan::new("src/v3/std/bridge_ledger.dag", 5561, 5608), + span: SourceSpan::new("src/v3/std/bridge_ledger.dag", 5699, 5746), }); declarations.push(Declaration { id: DeclarationId(891), @@ -27003,9 +27003,9 @@ fn bootstrapped_fixture_dag_declarations() -> Vec { value_body: None, refinement: None, nominal_opacity: None, - span: SourceSpan::new("src/v3/std/bridge_ledger.dag", 6251, 6361), + span: SourceSpan::new("src/v3/std/bridge_ledger.dag", 6389, 6499), }); - declarations.push(Declaration { id: DeclarationId(892), name: Some("bridge_ledger".to_string()), connective: TypeConnective::Instantiation { template: DeclarationId(665), arguments: vec![TemplateArgument { parameter: DeclarationId(666), value: DeclarationId(891) }] }, type_params: vec![], phantom_params: Vec::new(), meta_tag: Some(DeclarationId(2032)), specialization_parent: None, inhabits: None, value_body: Some(ValueBody::List(vec![FieldValue::Record(vec![("name".to_string(), FieldValue::Literal(LiteralBits::String("bridge_source_span_file_participation_retired".to_string()))), ("owner".to_string(), FieldValue::Literal(LiteralBits::String("R3".to_string()))), ("status".to_string(), FieldValue::Variant { constructor: DeclarationId(2031), payload: vec![] }), ("authority".to_string(), FieldValue::Literal(LiteralBits::String("ROADMAP.md#lens-fold-file-path-semantics".to_string())))]), FieldValue::Record(vec![("name".to_string(), FieldValue::Literal(LiteralBits::String("bridge_mark_bootstrap_secret_nominal_opacity_retired".to_string()))), ("owner".to_string(), FieldValue::Literal(LiteralBits::String("R2-Substrate".to_string()))), ("status".to_string(), FieldValue::Variant { constructor: DeclarationId(2030), payload: vec![] }), ("authority".to_string(), FieldValue::Literal(LiteralBits::String("PR #937".to_string())))]), FieldValue::Record(vec![("name".to_string(), FieldValue::Literal(LiteralBits::String("bridge_canonical_lens_name_dispatch_pr1183_slice_retired".to_string()))), ("owner".to_string(), FieldValue::Literal(LiteralBits::String("R2-Substrate".to_string()))), ("status".to_string(), FieldValue::Variant { constructor: DeclarationId(2030), payload: vec![] }), ("authority".to_string(), FieldValue::Literal(LiteralBits::String("src/v3/compiler/tests/integration/canonical_lens_bridge_ratchet_test.rs".to_string())))]), FieldValue::Record(vec![("name".to_string(), FieldValue::Literal(LiteralBits::String("bridge_canonical_lens_name_patching_residual".to_string()))), ("owner".to_string(), FieldValue::Literal(LiteralBits::String("PB-Runtime".to_string()))), ("status".to_string(), FieldValue::Variant { constructor: DeclarationId(2030), payload: vec![] }), ("authority".to_string(), FieldValue::Literal(LiteralBits::String("docs/briefs/r3-pb-bridge-canonical-lens-name-dispatch-closure.md".to_string())))]), FieldValue::Record(vec![("name".to_string(), FieldValue::Literal(LiteralBits::String("bridge_include_str_side_channels_retired".to_string()))), ("owner".to_string(), FieldValue::Literal(LiteralBits::String("pipeline_authority".to_string()))), ("status".to_string(), FieldValue::Variant { constructor: DeclarationId(2030), payload: vec![] }), ("authority".to_string(), FieldValue::Literal(LiteralBits::String("src/v3/compiler/tests/integration/l1_5_fixed_point_test.rs".to_string())))]), FieldValue::Record(vec![("name".to_string(), FieldValue::Literal(LiteralBits::String("bridge_exact_string_patching_residual_retired".to_string()))), ("owner".to_string(), FieldValue::Literal(LiteralBits::String("PB-Tier-2".to_string()))), ("status".to_string(), FieldValue::Variant { constructor: DeclarationId(2031), payload: vec![] }), ("authority".to_string(), FieldValue::Literal(LiteralBits::String("docs/r3-structure.md:83".to_string())))])])), refinement: None, nominal_opacity: None, span: SourceSpan::new("src/v3/std/bridge_ledger.dag", 6825, 8648) }); + declarations.push(Declaration { id: DeclarationId(892), name: Some("bridge_ledger".to_string()), connective: TypeConnective::Instantiation { template: DeclarationId(665), arguments: vec![TemplateArgument { parameter: DeclarationId(666), value: DeclarationId(891) }] }, type_params: vec![], phantom_params: Vec::new(), meta_tag: Some(DeclarationId(2032)), specialization_parent: None, inhabits: None, value_body: Some(ValueBody::List(vec![FieldValue::Record(vec![("name".to_string(), FieldValue::Literal(LiteralBits::String("bridge_source_span_file_participation_retired".to_string()))), ("owner".to_string(), FieldValue::Literal(LiteralBits::String("R3".to_string()))), ("status".to_string(), FieldValue::Variant { constructor: DeclarationId(2031), payload: vec![] }), ("authority".to_string(), FieldValue::Literal(LiteralBits::String("ROADMAP.md#lens-fold-file-path-semantics".to_string())))]), FieldValue::Record(vec![("name".to_string(), FieldValue::Literal(LiteralBits::String("bridge_mark_bootstrap_secret_nominal_opacity_retired".to_string()))), ("owner".to_string(), FieldValue::Literal(LiteralBits::String("R2-Substrate".to_string()))), ("status".to_string(), FieldValue::Variant { constructor: DeclarationId(2030), payload: vec![] }), ("authority".to_string(), FieldValue::Literal(LiteralBits::String("PR #937".to_string())))]), FieldValue::Record(vec![("name".to_string(), FieldValue::Literal(LiteralBits::String("bridge_canonical_lens_name_dispatch_pr1183_slice_retired".to_string()))), ("owner".to_string(), FieldValue::Literal(LiteralBits::String("R2-Substrate".to_string()))), ("status".to_string(), FieldValue::Variant { constructor: DeclarationId(2030), payload: vec![] }), ("authority".to_string(), FieldValue::Literal(LiteralBits::String("src/v3/compiler/tests/integration/canonical_lens_bridge_ratchet_test.rs".to_string())))]), FieldValue::Record(vec![("name".to_string(), FieldValue::Literal(LiteralBits::String("bridge_canonical_lens_name_patching_residual".to_string()))), ("owner".to_string(), FieldValue::Literal(LiteralBits::String("PB-Runtime".to_string()))), ("status".to_string(), FieldValue::Variant { constructor: DeclarationId(2030), payload: vec![] }), ("authority".to_string(), FieldValue::Literal(LiteralBits::String("docs/briefs/r3-pb-bridge-canonical-lens-name-dispatch-closure.md".to_string())))]), FieldValue::Record(vec![("name".to_string(), FieldValue::Literal(LiteralBits::String("bridge_include_str_side_channels_retired".to_string()))), ("owner".to_string(), FieldValue::Literal(LiteralBits::String("pipeline_authority".to_string()))), ("status".to_string(), FieldValue::Variant { constructor: DeclarationId(2030), payload: vec![] }), ("authority".to_string(), FieldValue::Literal(LiteralBits::String("src/v3/compiler/tests/integration/l1_5_fixed_point_test.rs".to_string())))]), FieldValue::Record(vec![("name".to_string(), FieldValue::Literal(LiteralBits::String("bridge_exact_string_patching_residual_retired".to_string()))), ("owner".to_string(), FieldValue::Literal(LiteralBits::String("PB-Tier-2".to_string()))), ("status".to_string(), FieldValue::Variant { constructor: DeclarationId(2030), payload: vec![] }), ("authority".to_string(), FieldValue::Literal(LiteralBits::String("src/v3/compiler/tests/integration/bridge_lower_helpers_patch_zero_residual_test.rs".to_string())))]), FieldValue::Record(vec![("name".to_string(), FieldValue::Literal(LiteralBits::String("bridge_exact_string_semantic_patching_residual".to_string()))), ("owner".to_string(), FieldValue::Literal(LiteralBits::String("PB-Runtime".to_string()))), ("status".to_string(), FieldValue::Variant { constructor: DeclarationId(2031), payload: vec![] }), ("authority".to_string(), FieldValue::Literal(LiteralBits::String("docs/briefs/r3-v-bridge-row-4-exact-string-deeper-detail-receipt.md".to_string())))])])), refinement: None, nominal_opacity: None, span: SourceSpan::new("src/v3/std/bridge_ledger.dag", 6963, 8416) }); declarations.push(Declaration { id: DeclarationId(893), name: Some("CleanEmissionContract".to_string()), @@ -67676,7 +67676,7 @@ fn bootstrapped_fixture_dag_declarations() -> Vec { value_body: None, refinement: None, nominal_opacity: None, - span: SourceSpan::new("src/v3/std/bridge_ledger.dag", 4581, 4588), + span: SourceSpan::new("src/v3/std/bridge_ledger.dag", 4719, 4726), }); declarations.push(Declaration { id: DeclarationId(2031), @@ -67690,7 +67690,7 @@ fn bootstrapped_fixture_dag_declarations() -> Vec { value_body: None, refinement: None, nominal_opacity: None, - span: SourceSpan::new("src/v3/std/bridge_ledger.dag", 4593, 4597), + span: SourceSpan::new("src/v3/std/bridge_ledger.dag", 4731, 4735), }); declarations.push(Declaration { id: DeclarationId(2032), @@ -67710,7 +67710,7 @@ fn bootstrapped_fixture_dag_declarations() -> Vec { value_body: None, refinement: None, nominal_opacity: None, - span: SourceSpan::new("src/v3/std/bridge_ledger.dag", 6845, 6866), + span: SourceSpan::new("src/v3/std/bridge_ledger.dag", 6983, 7004), }); declarations.push(Declaration { id: DeclarationId(2033), diff --git a/src/v3/compiler/src/bootstrap_generated_without_parse_surface.rs b/src/v3/compiler/src/bootstrap_generated_without_parse_surface.rs index a6b7697b06f..bc5c94e867a 100644 --- a/src/v3/compiler/src/bootstrap_generated_without_parse_surface.rs +++ b/src/v3/compiler/src/bootstrap_generated_without_parse_surface.rs @@ -26951,7 +26951,7 @@ fn bootstrapped_fixture_without_parse_surface_dag_declarations() -> Vec Vec Vec Vec Vec Vec` with exactly the -//! five canonical bridge names from `docs/r3-structure.md:79-83`. +//! - `bridge_ledger` lowers as `List` carrying the canonical +//! bridge rows from `docs/r3-structure.md` T-Bridge-Retirement (including +//! split rows such as canonical-lens and exact-string slice vs residual). //! - Each row's `status` resolves to one of the two `BridgeStatus` //! constructors structurally (not a string check). diff --git a/src/v3/compiler/tests/integration/bridge_lower_helpers_patch_zero_residual_test.rs b/src/v3/compiler/tests/integration/bridge_lower_helpers_patch_zero_residual_test.rs index 1ad75360718..b9904ce32c9 100644 --- a/src/v3/compiler/tests/integration/bridge_lower_helpers_patch_zero_residual_test.rs +++ b/src/v3/compiler/tests/integration/bridge_lower_helpers_patch_zero_residual_test.rs @@ -1,12 +1,14 @@ //! **Layer:** integration //! //! Zero-residual **receipt + ratchet** for the PB Tier-2 lower-helper -//! post-processing bridge tracked in R3 under the exact-string umbrella -//! **`bridge_exact_string_patching_residual_retired`** (**lower-helper slice** -//! only; PB brief `docs/briefs/r2-pure-bootstrap-manager.md` names the sibling -//! Tier-2 row as `bridge_patch_lower` + `_helpers_residual_retired` split -//! across lines here so this source stays free of the contiguous forbidden -//! token under scan). +//! post-processing bridge: ledger row **`bridge_exact_string_patching_residual_retired`** +//! is **`Retired`** in `src/v3/std/bridge_ledger.dag` for the **lower-helper slice** +//! only (PB brief +//! `docs/briefs/r2-pure-bootstrap-manager.md` names the sibling Tier-2 row as +//! `bridge_patch_lower` + `_helpers_residual_retired` split across lines here +//! so this source stays free of the contiguous forbidden token under scan). +//! Remaining Row-4 semantic exact-string patching outside this slice is tracked +//! as the open ledger row `bridge_exact_string_semantic_patching_residual`. //! See `docs/r3-structure.md` (T-Bridge-Retirement). //! //! ## Audit (PB v3-compiler crate, post–PR #1014) diff --git a/src/v3/compiler/tests/integration/m1_5_verification_test.rs b/src/v3/compiler/tests/integration/m1_5_verification_test.rs index 1f583ce2c51..fd943f85279 100644 --- a/src/v3/compiler/tests/integration/m1_5_verification_test.rs +++ b/src/v3/compiler/tests/integration/m1_5_verification_test.rs @@ -564,7 +564,7 @@ static BRIDGE_LEDGER_OPEN_ROW_NAMES: OnceLock> = OnceLock::new(); /// count retire bridges, and PRs that need to increase it must update /// `r3-v-bridge-ratchet-test-design.md` §Per-Bridge Gate Audit and obtain /// Verification-Mgr acknowledgment. -const EXPECTED_OPEN_BOUND: usize = 4; +const EXPECTED_OPEN_BOUND: usize = 2; fn bridge_ledger_open_row_names() -> &'static [String] { BRIDGE_LEDGER_OPEN_ROW_NAMES.get_or_init(|| { diff --git a/src/v3/compiler/tests/integration/parse_corpus_manifest.txt b/src/v3/compiler/tests/integration/parse_corpus_manifest.txt index 3a1ef168128..f2ca418f476 100644 --- a/src/v3/compiler/tests/integration/parse_corpus_manifest.txt +++ b/src/v3/compiler/tests/integration/parse_corpus_manifest.txt @@ -32,7 +32,7 @@ src/v3/std/anthropic_schema.dag 14 69934 58a973240ec25777 src/v3/std/approximate_field.dag 11 16864 ccbe4826dc31c636 src/v3/std/bin_shim.dag 4 2544 9ac96f1b3feafe47 src/v3/std/bootstrap_authority.dag 4 70609 e228bb8bb2449ece -src/v3/std/bridge_ledger.dag 7 31728 e199a822d969d067 +src/v3/std/bridge_ledger.dag 7 36072 4c795fafb7530441 src/v3/std/clean_emission.dag 15 23867 e7bc1e6145f4781e src/v3/std/computation.dag 19 37870 25c5a33ef4d8735a src/v3/std/computation_model.dag 14 22953 20e458fe097d175a diff --git a/src/v3/std/bridge_ledger.dag b/src/v3/std/bridge_ledger.dag index 0198efb01b3..86afb6b3289 100644 --- a/src/v3/std/bridge_ledger.dag +++ b/src/v3/std/bridge_ledger.dag @@ -58,13 +58,15 @@ import v3.spec.v3_l1 { DeclarationRef } // lowers as `ArrowBody::Unparsed`; the retired row therefore means // no source-text side channel remains for this authority path, not // that compile-body drift is structurally checkable. -// - `bridge_exact_string_patching_residual_retired` — Open. Per -// `r3-structure.md:83`: PB lower-helper slice (Tier-2 / #1014 -// lineage) is pinned at zero, BUT "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" — the umbrella row stays Open until those -// other classes land their own retirement receipts. +// - `bridge_exact_string_patching_residual_retired` — Retired. PB +// Tier-2 lower-helper generated-Rust exact-string patch class +// (#1014 / #1192 lineage): zero residual ratcheted by +// `bridge_lower_helpers_patch_zero_residual_test.rs`. +// - `bridge_exact_string_semantic_patching_residual` — Open. Row-4 +// semantic exact-string patching outside the retired lower-helper +// slice (e.g. bootstrap `Bool` inhabits patch class, BR-06 sentinel +// splice, infer-helper-driven rewrite classes per +// `docs/briefs/r3-v-bridge-row-4-exact-string-deeper-detail-receipt.md`). // 🟢 TERMINAL. Closed retirement-state coproduct for ledger rows. Two // states are sufficient at this scope: a bridge has either landed its @@ -157,17 +159,13 @@ data bridge_ledger: List = [ { name: "bridge_exact_string_patching_residual_retired", owner: "PB-Tier-2", + status: Retired, + authority: "src/v3/compiler/tests/integration/bridge_lower_helpers_patch_zero_residual_test.rs" + }, + { + name: "bridge_exact_string_semantic_patching_residual", + owner: "PB-Runtime", status: Open, - // Umbrella row — `bridge_lower_helpers_patch_zero_residual_test.rs` - // ratchets only the retired sub-slice (PR #1014 lineage); the row - // stays Open because *other* exact-string patching classes remain - // outside that receipt's scope. Point `authority` at the prose - // row where the umbrella's open-scope framing is defined, - // not at the closed sub-slice's ratchet (the residual debt the - // open status tracks is exactly the "other classes" the prose - // row names — those classes' own dissolution triggers cover the - // remaining scope, and the umbrella retires when those triggers - // all fire). - authority: "docs/r3-structure.md:83" + authority: "docs/briefs/r3-v-bridge-row-4-exact-string-deeper-detail-receipt.md" } ]