Skip to content
2 changes: 1 addition & 1 deletion ROADMAP.md
Original file line number Diff line number Diff line change
Expand Up @@ -533,7 +533,7 @@ Surfaced by paired Exploratory Analysis (gpt-5-5-pro main@8cd5359; 9 findings ag

- **SubValueRelation claims `BoundedLattice<T>` but `meet(top, a) = a` law violated** (sharpened from already-tracked hand-rolled-lattice row at ROADMAP:362-365): `src/v3/std/induction.dag:372-376` claims `top = PreservedValue` (meet identity), `bottom = SubValueUnknown`, but `src/v3/std/induction.dag:281-288` implements `meet(PreservedValue, b) = PreservedValue` for any non-unknown `b` — the law `meet(top, a) = a` requires returning `b`, not `top`. Concrete counterexample: `meet_sub_value(PreservedValue, StrictSubValue { ... })` returns `PreservedValue` instead of `StrictSubValue`. Downstream consumers reading "this is a `BoundedLattice`" get false algebraic guarantees. **Dissolution**: either add a real top element, weaken the claim to a semilattice/partial-merge structure, or change ordering so implemented meet/join satisfy declared laws. **Stop claiming `BoundedLattice<SubValueRelation>` until law holds.** Surfaced 2026-05-01 (Exploratory Finding 2). Owner: R3 Substrate (fix substrate or weaken claim) + R3 Verification (`bounded_lattice_meet_top_identity_witness` for any T claiming `BoundedLattice<T>`).

- **Emitter `as_bind().expect()` panic paths violate fail-closed boundary** (NOVEL): 6 sites in `src/v3/compiler/src/emit.rs:2157-2166` + `:2205-2214`, `src/v3/compiler/src/emit/rust_target.rs:4475-4485` + `:4569-4579`, `src/v3/compiler/src/emit/python_target.rs:1307-1316` + `:1383-1392` use `as_bind().expect("UserDefined arrow body must point at a Bind")` instead of typed `EmitError` / `EmitPythonError`. Adjacent branches already return typed errors for non-Arrow declarations. Malformed substrate data crashes emitter instead of producing typed diagnostic. **Dissolution**: replace `expect` calls with typed emitter errors carrying offending `DeclarationId` / `NodeId`. Stronger: make `ArrowBody::UserDefined` carry a `BindNodeId` witness that cannot point at other behavior variants (state-space-vs-behavioral-invariants pattern). Surfaced 2026-05-01 (Exploratory Finding 8). Owner: R3 Substrate / R3 PB (adjacent to T-LensProducer-Retirement emit-module surface).
- **Emitter `as_bind().expect()` panic paths violate fail-closed boundary** (NOVEL — **RETIRED 2026-05-03 by PR #1548**): 6 sites in `src/v3/compiler/src/emit.rs:2157-2166` + `:2205-2214`, `src/v3/compiler/src/emit/rust_target.rs:4475-4485` + `:4569-4579`, `src/v3/compiler/src/emit/python_target.rs:1307-1316` + `:1383-1392` used `as_bind().expect("UserDefined arrow body must point at a Bind")`. **Dissolution chosen**: the stronger state-space-vs-behavioral-invariants path — `ArrowBody::UserDefined` now carries a typed `BindNodeId` witness (`src/v3/compiler/src/dag.rs:113`) that cannot point at non-Bind behavior variants. All six sites consume `(*bind_id).bind(self.dag)` (and the guarded `rust_target.rs:2503` site uses `.bind_opt(dag)` returning a typed `EmitError::MalformedUserDefinedCallable`). Local typed-error shape was **rejected** at design split (#1337-comment-4364992875 / #1134-comment-4364994796) as parallel-representation debt against the substrate fix. Surfaced 2026-05-01 (Exploratory Finding 8). Receipt: PR #1548 (`0427f96f7`). Owner closure: R3 Substrate.

#### B. Exploratory findings — sharpened tracked items

Expand Down
34 changes: 17 additions & 17 deletions docs/debt/r3-debt-paydown-ledger-2026-05-02.md
Original file line number Diff line number Diff line change
Expand Up @@ -17,9 +17,9 @@ This pass classifies 69 ROADMAP-tracked debt rows in the ledger range:

| Bucket | Count | Meaning |
|---|---:|---|
| Open implementation / retirement work | 59 | Needs a named retirement PR, executable gate, owner closure receipt, or disposition decision. |
| Open implementation / retirement work | 58 | Needs a named retirement PR, executable gate, owner closure receipt, or disposition decision. |
| Partially closed | 6 | Has a landed partial receipt but still names remaining work. |
| Retired / stale receipt row | 4 | ROADMAP already records retirement or stale-finding resolution; next action is ledger cleanup, not code. |
| Retired / stale receipt row | 5 | ROADMAP already records retirement or stale-finding resolution; next action is ledger cleanup, not code. |

The highest concentration is in Substrate-adjacent rows: operator authority, value-body / mirror isomorphism, illegal-state carriers, bootstrap diagnostics, and algebra-law conformance. The second concentration is PB/Verification scaffolding: `test_runner.rs`, author-now/fire-later claims, bridge-ledger open rows, and SG-0 hand-Rust growth.

Expand Down Expand Up @@ -89,7 +89,7 @@ The highest concentration is in Substrate-adjacent rows: operator authority, val
| `Json` + `Bytes` opaque kernel decomposition | 2026-05-01 | R3 Substrate | Open / disposition pending | Decide after T-Numeric-Construction whether this becomes an R3 lane. |
| SymbolicCost semiring annihilation violation | 2026-05-01 | R3 Substrate + Verification | Open | Fix normalization; add semiring law witnesses. |
| SubValueRelation bounded-lattice law violation | 2026-05-01 | R3 Substrate + Verification | Open | Fix ordering/top semantics or stop claiming `BoundedLattice`. |
| Emitter `as_bind().expect()` panic paths | 2026-05-01 | R3 Substrate / PB | Open | Replace `expect` with typed emit errors or typed `BindNodeId` witness. |
| Emitter `as_bind().expect()` panic paths | 2026-05-01 | R3 Substrate / PB | Retired | PR #1548 (`0427f96f7`) landed the typed `BindNodeId` witness on `ArrowBody::UserDefined`; all six emitter sites consume `(*bind_id).bind(self.dag)`, guarded site uses `.bind_opt(dag)` returning typed `EmitError::MalformedUserDefinedCallable`. Local-typed-error path was rejected at design split as parallel-representation debt. |
| `??` / `%` syntax authority mismatch | 2026-05-01 | R3 Substrate + Grounding | Open | Remove unsupported rows or add full token/parse/operator chain. |
| `CollectionOps` / `StringOps` / `MapOps` duplicate operation surfaces | 2026-05-01 | R3 Grounding | Open | Target templates reference algebra method contracts / declaration refs. |
| Author-now/fire-later verification style | 2026-05-01 | R3 Verification | Open | Make one `BinaryDimensionReportEquals` claim actually execute. |
Expand All @@ -105,37 +105,37 @@ These rows should not consume implementation-worker capacity unless the ledger t
2. **`lower_fn_body_into_existing_decl` defensive Arrow re-derive**: ROADMAP records the cited symbol no longer exists and live lowering fails closed.
3. **`patch_lower_helpers_generated_type_alias_refinement` exact-string patching**: retired by PR #1014.
4. **Go branch emits `UnknownVariant`**: retired by PR #820; live Go branch emission now returns `EmitError::VariantParentNotFound` with regression coverage.
5. **E-M method carrier parity framing** inside the substrate-carrier port program: closed by structural subsumption pick; remaining work belongs to E-P consumer/cementing and non-carrier lens blockers.
6. **P0 repeat-string oracle bridge**: the interim `p0_repeat_string_v2_oracle_rust_bridge` is retired, but the broader modeled-evaluation target remains open. Track as partial, not as a fresh P0 bug.
5. **Emitter `as_bind().expect()` panic paths**: retired by PR #1548 via the typed `BindNodeId` witness on `ArrowBody::UserDefined` (`src/v3/compiler/src/dag.rs:113`); all six emitter sites consume `(*bind_id).bind(self.dag)`; guarded `rust_target.rs:2503` site uses `.bind_opt(dag)` returning typed `EmitError::MalformedUserDefinedCallable`.
6. **E-M method carrier parity framing** inside the substrate-carrier port program: closed by structural subsumption pick; remaining work belongs to E-P consumer/cementing and non-carrier lens blockers.
7. **P0 repeat-string oracle bridge**: the interim `p0_repeat_string_v2_oracle_rust_bridge` is retired, but the broader modeled-evaluation target remains open. Track as partial, not as a fresh P0 bug.

## Highest-Leverage Retirement Targets

1. **Reject duplicate record-literal fields.**
Small, correctness-critical, and already has a sibling duplicate-key pattern in map lowering. Closure removes a silent fact-drop bug rather than adding a new scaffold.

2. **Replace emitter `as_bind().expect()` panics with typed errors.**
Six localized call sites; converts crash behavior into fail-closed diagnostics and is adjacent to existing emitter error paths.

3. **Bootstrap diagnostics-empty gate for method-template contracts.**
2. **Bootstrap diagnostics-empty gate for method-template contracts.**
One structural ratchet can close both the `go_method_template_contracts` mismatch and the broader "shape test passed over diagnostic Dag" pattern.

4. **SymbolicCost semiring zero law.**
3. **SymbolicCost semiring zero law.**
High correctness impact: fixes cost-lens facts and seeds the Verification law-witness closure path.

5. **SubValueRelation algebra-claim correction.**
4. **SubValueRelation algebra-claim correction.**
Pairs naturally with the law-witness lane; either fixes the law or removes an invalid guarantee.

6. **`ValueBody` mirror update + first isomorphism receipt.**
5. **`ValueBody` mirror update + first isomorphism receipt.**
Slightly larger, but it attacks multiple rows at once: ValueBody drift, FieldMap illegal-state mirror, reflection-overtrust, and hand-mirror growth.

7. **Method-template consumer migration audit-to-retirement slice.**
6. **Method-template consumer migration audit-to-retirement slice.**
PRs populated rows; the invariant gain lands only when old runtime/emit tables stop serving consumers.

8. **BridgeLedgerZero decreasing-open-count ratchet.**
7. **BridgeLedgerZero decreasing-open-count ratchet.**
Turns a reporting scaffold into pressure for actual row retirement across bridge owners.

9. **CI slow-test exemption fresh audit.**
Bounded docs/script work that turns a partial T-Receipts row into measurable deletion opportunities.
8. **CI slow-test exemption fresh audit.**
Bounded docs/script work that turns a partial T-Receipts row into measurable deletion opportunities.

(Two original highest-leverage targets are now retired and removed from this list: *Replace emitter `as_bind().expect()` panics with typed errors* — retired by PR #1548 via the stronger `BindNodeId` witness path (ledger row 92); *Go `UnknownVariant` fail-closed fix* — retired by PR #820, ledger close-out via PR #1545.)

## Velocity Tripwire Baseline

Expand All @@ -151,7 +151,7 @@ Next cadence pass should record:

Recommended first retirement bundle for the Debt-Paydown Manager to coordinate:

1. **Substrate fail-closed mini-bundle:** duplicate record labels and emitter `as_bind()` typed errors. Go `UnknownVariant` is already retired by PR #820.
1. **Substrate fail-closed mini-bundle:** duplicate record labels. (Emitter `as_bind()` retired by PR #1548 via `BindNodeId` witness; Go `UnknownVariant` retired by PR #820 / ledger close-out PR #1545.)
2. **Verification/substrate executable-gate bundle:** diagnostics-empty bootstrap ratchet plus one `BinaryDimensionReportEquals` claim that actually compares produced reports.
3. **Grounding consumer-retirement bundle:** method-template old-table consumer migration; prevent more row population from masking parallel authority.
4. **PB/Verification bridge discipline bundle:** BridgeLedgerZero decreasing-open-count ratchet and `test_runner.rs` bespoke-arm freeze rule.
Expand Down
Loading