Skip to content
Closed
Show file tree
Hide file tree
Changes from all commits
Commits
File filter

Filter by extension

Filter by extension

Conversations
Failed to load comments.
Loading
Jump to
Jump to file
Failed to load files.
Loading
Diff view
Diff view
27 changes: 18 additions & 9 deletions docs/briefs/r2-pb-canonical-lens-bridge-disposition.md
Original file line number Diff line number Diff line change
Expand Up @@ -15,7 +15,11 @@ These were retired in earlier PB / B4 work and survive structurally on main:

## What remains (the canonical lens-name dispatch bridge surface)

Three categories of structural debt remain in `src/v3/compiler/src/test_runner.rs`:
One category of structural debt remains in `src/v3/compiler/src/test_runner.rs`.
R3 gate #33 retired the runner-side lens-name dispatch by routing
`LensOutputEquals` through typed marker declarations
(`CanonicalNamedFunctionCountLens`, `CanonicalCostLens`) instead of
`lens_decl.name`.

### A. `include_str!` of canonical lens bytes (2 sites)

Expand All @@ -24,14 +28,17 @@ Three categories of structural debt remain in `src/v3/compiler/src/test_runner.r

The runner re-compiles these bytes via `compile_to_dag(...)` to obtain a "canonical" `Dag` for `apply_lens_declaration`, distinct from the fixture-compiled stub.

### B. String-name dispatch arms in `LensOutputEquals` (2 sites)
### B. String-name dispatch arms in `LensOutputEquals` (retired)

- `lens_decl.name.as_deref() == Some("cost_of")` (`test_runner.rs:1795`) — selects a `cost_of`-specific code path that reads `ProgramInputRole::output_bind_name` and computes `cost_of(&program_dag, &bind.value)`.
- `lens_decl.name.as_deref() == Some("named_function_count")` (`test_runner.rs:1834`) — selects the `R1_CANONICAL_NAMED_FUNCTION_COUNT_LENS` re-compile path.
Retired by R3 gate #33. The `cost_of` and `named_function_count` special paths
now dispatch on `lens_ref` declarations that inhabit closed marker types in
`std.verification`, not on function-name strings.

### C. Generic name-keyed lens lookup (2 sites)
### C. Generic name-keyed lens lookup (retired)

- `else if let Some(name) = lens_decl.name.as_deref() { program_dag.declaration_by_name(name) ... }` at `test_runner.rs:1877` (id-space selection) and `:1933` (lens-program selection). These resolve the lens body from `program_dag` (claim source) by **name** rather than by typed `DeclarationRef` identity.
Retired by R3 gate #33. Ordinary non-canonical `LensOutputEquals` lenses execute
from the fixture graph via their `DeclarationRef`; they no longer probe
`program_dag` by the lens declaration's name.

## Why these survive — the substrate gap

Expand All @@ -50,13 +57,15 @@ Concretely (see comment block at `test_runner.rs:1762-1772` and `:1832-1833`):
(b) a typed cross-`Dag` `DeclarationRef` carrier with reconciliation rules (substrate introduction), OR
(c) PB-Runtime interpreter-as-data that loads the canonical lens once and routes `lens_ref` resolution through typed identity rather than name-keyed lookup,

…the runner cannot drop the name-keyed dispatch without sacrificing the P2 cross-`Dag` invariant.
…the runner cannot drop the canonical byte bridge (A) without sacrificing the
P2 cross-`Dag` invariant. The name-keyed dispatch parts (B/C) are now replaced
by typed marker declarations.

## Precise dependency

Full retirement of `bridge_canonical_lens_name_dispatch_retired` is gated on **either**:

1. **PB-Runtime interpreter-as-data** landing (load-bearing for T-LensProducer-Retirement's `lens_apply.rs` retirement; see [`r2-pure-bootstrap-manager.md`](r2-pure-bootstrap-manager.md) §"Owns (R3 continuation)"). That work makes lens application a `.dag`-driven walk over typed `DeclarationRef` identity rather than Rust name-keyed dispatch, and dissolves both the name-arms (B) and the generic name-keyed lookup (C). This dependency is **explicitly gated on Items 4+5** per Director cascade and **must not be unblocked from this disposition PR**. OR
1. **PB-Runtime interpreter-as-data** landing (load-bearing for T-LensProducer-Retirement's `lens_apply.rs` retirement; see [`r2-pure-bootstrap-manager.md`](r2-pure-bootstrap-manager.md) §"Owns (R3 continuation)"). That work makes lens application a `.dag`-driven walk over typed `DeclarationRef` identity and can dissolve the remaining canonical byte bridge (A). OR
2. **A typed lens-registry carrier substrate-introduction** authored by Substrate Manager per [`INVARIANTS.md#p1-modeling-faithfulness`](../../INVARIANTS.md#p1-modeling-faithfulness) substrate-fact-introduction procedure — would dissolve the `include_str!` text bridges (A) by replacing canonical-lens-text with a typed `LensRegistryEntry` reference. The B4.1a worker brief explicitly STOPs and splits this as a sub-brief if it surfaces (per [`b4-1-declarationref-consumer-migration-worker.md`](b4-1-declarationref-consumer-migration-worker.md) §STOP-AND-ESCALATE: "Canonical lens identity requires loading a second DAG by path. Do not replace one `include_str!` bridge with another string registry; split a structural lens-registry carrier brief.").

Either path is a substrate-level change outside PB authoring authority. PB territory cannot self-serve here without violating the dispatch guardrail "do not replace one string/path side channel with another."
Expand All @@ -65,7 +74,7 @@ Either path is a substrate-level change outside PB authoring authority. PB terri

- [x] No `PROGRAM_INPUT_SENTINEL` remains (already retired pre-PR; verified by grep).
- [x] Canonical lens lookup status documented; **not** retired in this PR (substrate gap above).
- [x] Ratchet test added that fails if the bridge surface grows: pins counts of (1) `include_str!` of `lenses/*.dag` files in `test_runner.rs`, (2) `lens_decl.name.as_deref() == Some("...")` arms, and (3) generic `lens_decl.name.as_deref()` name-keyed lookups. Rule per `feedback_ratchet_only_down`: never increase. See `tests/integration/canonical_lens_bridge_ratchet_test.rs`.
- [x] Ratchet test added that fails if the bridge surface grows: pins counts of (1) `include_str!` of `lenses/*.dag` files in `test_runner.rs`, (2) `lens_decl.name.as_deref() == Some("...")` arms, and (3) generic `lens_decl.name.as_deref()` name-keyed lookups. R3 gate #33 lowers (2) and (3) to zero. Rule per `feedback_ratchet_only_down`: never increase. See `tests/integration/canonical_lens_bridge_ratchet_test.rs`.
- [x] Manager brief annotated with partial-retirement / blocker state for the slice (this disposition file). **No per-bridge retirement signal to Verification** — `bridge_retirement_ledger_zero` (the actual unified ledger authority) is not advanced by this PR; the bridge is not retired. This is a blocker/disposition receipt, not a ledger-advance.
- [x] No replacement string / path side channel introduced.

Expand Down
2 changes: 1 addition & 1 deletion docs/briefs/r2-pure-bootstrap-manager.md
Original file line number Diff line number Diff line change
Expand Up @@ -108,7 +108,7 @@ Each lane closes under a structural acceptance gate authored as a `.dag` `TestCl
- `lens_testgen_dot_rs_retired` — `src/v3/compiler/src/lens_testgen.rs` deleted
- `regen_lens_dot_rs_retired` — `src/v3/compiler/src/bin/regen_lens.rs` deleted
- `pb_self_compile_fixed_point_strong` — bit-identical stage0 + emitted artifacts
- `bridge_canonical_lens_name_dispatch_retired` — distributed bridge #3 (**partial retirement; full close blocked.** §0.1 `PROGRAM_INPUT_SENTINEL` + §0.2 `cost_bind_for_claim_file` already retired structurally on main. Remaining surface: 2 `include_str!` of canonical lens bytes + 2 `lens_decl.name == Some("…")` arms + 2 generic name-keyed lookups in `test_runner.rs`. Pinned by `tests/integration/canonical_lens_bridge_ratchet_test.rs`. Full close gated on PB-Runtime interpreter-as-data **or** typed lens-registry carrier substrate-introduction; see [`docs/briefs/r2-pb-canonical-lens-bridge-disposition.md`](r2-pb-canonical-lens-bridge-disposition.md))
- `bridge_canonical_lens_name_dispatch_retired` — distributed bridge #3 (**partial retirement; full close blocked.** §0.1 `PROGRAM_INPUT_SENTINEL` + §0.2 `cost_bind_for_claim_file` already retired structurally on main. R3 gate #33 retired the 2 `lens_decl.name == Some("…")` arms + 2 generic name-keyed lookups in `test_runner.rs`; remaining surface is 2 `include_str!` canonical lens byte bridges. Pinned by `tests/integration/canonical_lens_bridge_ratchet_test.rs`. Full close gated on PB-Runtime interpreter-as-data **or** typed lens-registry carrier substrate-introduction; see [`docs/briefs/r2-pb-canonical-lens-bridge-disposition.md`](r2-pb-canonical-lens-bridge-disposition.md))
- `bridge_include_str_side_channels_retired` — distributed bridge #4 (e.g., `pipeline_authority.rs`)
- `bridge_patch_lower_helpers_residual_retired` — distributed bridge #5 (**PB Tier-2 lower-helper exact-string patch class:** #1014 deleted the helper + `regen_lens` / SG-6 special cases; **zero code residual** in `src/v3/compiler/**/*.rs` + `build.rs` per 2026-04-29 grep audit. **Ratchet:** `tests/integration/bridge_lower_helpers_patch_zero_residual_test.rs` fails CI if contiguous `patch_lower`+`_helpers` reappears — scoped to that retired bridge, not other string transforms.)

Expand Down
Original file line number Diff line number Diff line change
Expand Up @@ -82,8 +82,8 @@ they are the live Row 2 bridge rather than a separate BR id.
| --- | --- | --- | --- | --- |
| 3 | BR-17 `lens_apply.rs` unit-test canonical lens bytes | If a PR claims canonical-lens byte retirement and touches these tests, the tests must stop treating `../../lenses/named_function_count.dag` as a second canonical byte authority. A shared helper that only moves the string read is not retirement unless the test consumes the same structural lens identity as production. | Ideally the same typed lens registry, `program_dag` lens body identity, or PB-Runtime lens loader used by BR-07. If kept test-only, it remains adjacent cleanup and does not close Row 2 alone. | Optional same-wave cleanup with BR-07. Full `lens_apply.rs` retirement remains PB-Runtime sub-gate 1, not this receipt. |
| 10a | BR-07 `test_runner` canonical lens public consts | Delete `R1_CANONICAL_NAMED_FUNCTION_COUNT_LENS` / `R1_CANONICAL_COMPLEXITY_LENS` as production byte authorities, and remove runner recompilation paths that use those bytes to manufacture canonical lens identity. | PB-Runtime interpreter-as-data, typed lens registry, or structural `program_dag` lens body identity consumed by `LensOutputEquals` / lens application. The replacement must preserve cross-Dag declaration-id coherence without another path/string registry. | Row 1 owns file-stamped reflection participation after compilation. Row 3 may count generic `include_str!` channel mechanics, but Row 2 owns these canonical lens bytes. |
| 10b | Canonical disposition name-dispatch arms | Remove `lens_decl.name.as_deref() == Some("cost_of")` and `Some("named_function_count")` semantic dispatch arms. A PR cannot claim retirement while either arm still selects behavior by string name. | PB-Runtime structural dispatch over typed lens identity, or a typed lens-registry carrier that maps claim/lens refs to executable lens bodies. | This is the core `bridge_canonical_lens_name_patching_residual` surface. Do not conflate with Row 1 broad `declaration_by_name` duplicate-preference cleanup. |
| 10c | Canonical disposition generic name-keyed lens lookup | Remove generic `lens_decl.name.as_deref()` lookup that calls `program_dag.declaration_by_name(name)` for id-space selection or lens-program selection. | Cross-Dag typed lens identity or PB-Runtime loader that resolves the lens body structurally. Fixture-local names may remain display data only if they no longer select semantics. | Adjacent to Row 1 entry #14's broad `declaration_by_name` retirement, but Row 2 owns only canonical-lens body selection by name. |
| 10b | Canonical disposition name-dispatch arms | **Retired by R3 gate #33:** `LensOutputEquals` no longer has `lens_decl.name.as_deref() == Some("cost_of")` or `Some("named_function_count")` semantic dispatch arms. | Typed marker declarations in `std.verification` (`CanonicalCostLens`, `CanonicalNamedFunctionCountLens`) select the two legacy runner paths without matching function-name strings. | Remaining Row 2 surface is BR-07/BR-08 byte authority, not name dispatch. |
| 10c | Canonical disposition generic name-keyed lens lookup | **Retired by R3 gate #33:** generic `lens_decl.name.as_deref()` lookup no longer calls `program_dag.declaration_by_name(name)` for id-space or lens-program selection. | Ordinary non-canonical `LensOutputEquals` lenses execute from their fixture `DeclarationRef`; canonical named-function-count still compiles canonical bytes until BR-07 closes. | Adjacent Row 1 broad `declaration_by_name` retirement remains separate. |
| 10d | BR-08 user-authored lens gate on-disk vs runner bytes | Remove byte equality / import coupling between the gate test and `R1_CANONICAL_NAMED_FUNCTION_COUNT_LENS`; the test must consume the same structural canonical lens identity as runner production. | Same carrier as BR-07, visible to the integration test through structural fixture/test-claim identity rather than duplicate on-disk bytes. | BR-08 also has hermetic fixture bytes; those are not Row 2 unless they assert canonical lens byte identity. |
| 10e | Appendix B canonical lens ratchet | When BR-07/BR-08/name-dispatch surfaces shrink, update or delete the ratchet so it pins only live residuals. A retired bridge must not remain documented as an expected positive count. | No new carrier; consumes the same production counts as a verification ratchet. | Ratchet is evidence for Row 2 only, not an independent bridge entry. |
| 11 | BR-06 R1 gates fixture splice, canonical-lens slice only | If a canonical-lens retirement PR edits `emit_r1_gates_fixture`, it must remove duplicate canonical lens text splicing rather than merely renaming sentinels or moving escaped bytes. | Structural `TestClaim` / declaration-ref lens-body carrier or single substrate-owned generator that embeds lens identity without parallel text authority. | Row 4 owns exact-string/sentinel splice retirement generally. Row 2 counts only the canonical-lens byte identity portion if it lands in the same wave as BR-07/BR-08. |
Expand All @@ -92,15 +92,15 @@ they are the live Row 2 bridge rather than a separate BR id.

Row 2 routes primarily to PB-Runtime / T-LensProducer-Retirement:

- PB-Runtime interpreter-as-data is the preferred owner-program path for
retiring `test_runner.rs` name arms and name-keyed lens-body selection while
preserving the P2 cross-Dag reflection invariant.
- PB-Runtime interpreter-as-data remains the preferred owner-program path for
retiring the remaining canonical byte bridge while preserving the P2
cross-Dag reflection invariant.
- A typed lens-registry carrier remains the Substrate alternative if PB-Runtime
does not provide enough structural lens identity. That carrier must not be a
new string/path registry.
- `program_dag` lens body identity is acceptable only when the runner no longer
recompiles separate canonical bytes or chooses behavior through
`lens_decl.name`.
recompiles separate canonical bytes; behavior selection through
`lens_decl.name` was retired by R3 gate #33.
- BR-08 and BR-17 should consume the same production structural lens identity as
BR-07, or remain adjacent test cleanup rather than row closure.
- BR-06's canonical-lens splice pressure should be coordinated with Row 4
Expand Down
Loading