From 73e1353a136176bf4df137e34b060a041246a6af Mon Sep 17 00:00:00 2001 From: Brian Searls Date: Sun, 3 May 2026 03:42:40 +0000 Subject: [PATCH 1/3] docs(r3): retire emitter as_bind().expect() debt row (PR #1548 receipt) MIME-Version: 1.0 Content-Type: text/plain; charset=UTF-8 Content-Transfer-Encoding: 8bit PR #1548 (`0427f96f7`) landed the typed `BindNodeId` witness on `ArrowBody::UserDefined`, retiring the six emitter panic paths surfaced as Exploratory Finding 8. All cited sites now consume `(*bind_id).bind(self.dag)`; the guarded `rust_target.rs:2503` site uses `.bind_opt(dag)` returning a typed `EmitError::MalformedUserDefinedCallable`. The local-typed-error path was rejected at design split as parallel-representation debt against the substrate fix. This PR closes the docs receipt: - ROADMAP.md Exploratory Finding 8 — flipped to RETIRED with PR #1548 receipt; preserved historical finding text and noted the chosen `BindNodeId` dissolution path. - docs/debt/r3-debt-paydown-ledger-2026-05-02.md row 92 — flipped from Open to Retired; baseline counts updated (Open 60→59, Retired 3→4); highest-leverage list item 2 removed and remaining items renumbered; Substrate fail-closed mini-bundle scope adjusted. R3 debt receipt: Debt paid (via Substrate #1548) for ledger row 92 / ROADMAP.md Exploratory Finding 8. Co-Authored-By: Claude Opus 4.7 (1M context) --- ROADMAP.md | 2 +- .../debt/r3-debt-paydown-ledger-2026-05-02.md | 31 +++++++++---------- 2 files changed, 16 insertions(+), 17 deletions(-) diff --git a/ROADMAP.md b/ROADMAP.md index d9f4bfc504a..a9e42835f5f 100644 --- a/ROADMAP.md +++ b/ROADMAP.md @@ -533,7 +533,7 @@ Surfaced by paired Exploratory Analysis (gpt-5-5-pro main@8cd5359; 9 findings ag - **SubValueRelation claims `BoundedLattice` 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` 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`). -- **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 diff --git a/docs/debt/r3-debt-paydown-ledger-2026-05-02.md b/docs/debt/r3-debt-paydown-ledger-2026-05-02.md index 3dd4c8e5a12..ac7eff82a1f 100644 --- a/docs/debt/r3-debt-paydown-ledger-2026-05-02.md +++ b/docs/debt/r3-debt-paydown-ledger-2026-05-02.md @@ -17,9 +17,9 @@ This pass classifies 69 ROADMAP-tracked debt rows in the ledger range: | Bucket | Count | Meaning | |---|---:|---| -| Open implementation / retirement work | 60 | Needs a named retirement PR, executable gate, owner closure receipt, or disposition decision. | +| Open implementation / retirement work | 59 | 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 | 3 | ROADMAP already records retirement or stale-finding resolution; next action is ledger cleanup, not code. | +| Retired / stale receipt row | 4 | 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. @@ -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. | @@ -112,32 +112,31 @@ These rows should not consume implementation-worker capacity unless the ledger t 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. **Go `UnknownVariant` fail-closed fix.** +2. **Go `UnknownVariant` fail-closed fix.** Small emit-surface bug with direct P3/C-6/C-9 payoff. A typed `VariantParentNotFound` error is an easy receipt. -4. **Bootstrap diagnostics-empty gate for method-template contracts.** +3. **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. -5. **SymbolicCost semiring zero law.** +4. **SymbolicCost semiring zero law.** High correctness impact: fixes cost-lens facts and seeds the Verification law-witness closure path. -6. **SubValueRelation algebra-claim correction.** +5. **SubValueRelation algebra-claim correction.** Pairs naturally with the law-witness lane; either fixes the law or removes an invalid guarantee. -7. **`ValueBody` mirror update + first isomorphism receipt.** +6. **`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. -8. **Method-template consumer migration audit-to-retirement slice.** +7. **Method-template consumer migration audit-to-retirement slice.** PRs populated rows; the invariant gain lands only when old runtime/emit tables stop serving consumers. -9. **BridgeLedgerZero decreasing-open-count ratchet.** +8. **BridgeLedgerZero decreasing-open-count ratchet.** Turns a reporting scaffold into pressure for actual row retirement across bridge owners. -10. **CI slow-test exemption fresh audit.** - Bounded docs/script work that turns a partial T-Receipts row into measurable deletion opportunities. +9. **CI slow-test exemption fresh audit.** + Bounded docs/script work that turns a partial T-Receipts row into measurable deletion opportunities. + +(Previously item 2 — *Replace emitter `as_bind().expect()` panics with typed errors* — retired by PR #1548 via the stronger `BindNodeId` witness path; see ledger row 92.) ## Velocity Tripwire Baseline @@ -153,7 +152,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, emitter `as_bind()` typed errors, Go `UnknownVariant`. +1. **Substrate fail-closed mini-bundle:** duplicate record labels, Go `UnknownVariant`. (Emitter `as_bind()` retired by PR #1548 via `BindNodeId` witness — no longer in this bundle.) 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. From a326ad6b867ec0273aaffa2ec16fd866688c6e81 Mon Sep 17 00:00:00 2001 From: Brian Searls Date: Sun, 3 May 2026 04:30:13 +0000 Subject: [PATCH 2/3] docs(r3): list emitter as_bind() retirement in De Facto Closed rows MIME-Version: 1.0 Content-Type: text/plain; charset=UTF-8 Content-Transfer-Encoding: 8bit Per codex review on 0e0dfa86 (non-blocking improvement): the emitter row flipped to Retired with the count delta but was not added to the "De Facto Closed Or Cleanup-Only Rows" enumeration alongside the other PR #1548-class retirements. Adds it as item 5 between Go UnknownVariant (PR #820) and the E-M carrier-parity note; renumbers subsequent items 5→6, 6→7. Co-Authored-By: Claude Opus 4.7 (1M context) --- docs/debt/r3-debt-paydown-ledger-2026-05-02.md | 5 +++-- 1 file changed, 3 insertions(+), 2 deletions(-) diff --git a/docs/debt/r3-debt-paydown-ledger-2026-05-02.md b/docs/debt/r3-debt-paydown-ledger-2026-05-02.md index 82f4a303be5..8deb1f7b439 100644 --- a/docs/debt/r3-debt-paydown-ledger-2026-05-02.md +++ b/docs/debt/r3-debt-paydown-ledger-2026-05-02.md @@ -105,8 +105,9 @@ 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 From cc122315f2fbaad6bd267f8cee6790a4b97cb255 Mon Sep 17 00:00:00 2001 From: Brian Searls Date: Sun, 3 May 2026 04:50:10 +0000 Subject: [PATCH 3/3] docs(r3): drop ambiguous "previously item N" labels in highest-leverage footnote MIME-Version: 1.0 Content-Type: text/plain; charset=UTF-8 Content-Transfer-Encoding: 8bit Per cursor review on 50708739 (APPROVE_WITH_COMMENTS): the footnote claimed "Previously item 3 — Go UnknownVariant" which was correct against the pre-both-retirements 10-item list but ambiguous against the post-merge pre-renumber state where item 3 was Bootstrap diagnostics-empty gate. Drop the numeric labels and reference both retired targets by content alone; no information lost, no positional ambiguity. Co-Authored-By: Claude Opus 4.7 (1M context) --- docs/debt/r3-debt-paydown-ledger-2026-05-02.md | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/docs/debt/r3-debt-paydown-ledger-2026-05-02.md b/docs/debt/r3-debt-paydown-ledger-2026-05-02.md index 8deb1f7b439..cd1d555453d 100644 --- a/docs/debt/r3-debt-paydown-ledger-2026-05-02.md +++ b/docs/debt/r3-debt-paydown-ledger-2026-05-02.md @@ -135,7 +135,7 @@ These rows should not consume implementation-worker capacity unless the ledger t 8. **CI slow-test exemption fresh audit.** Bounded docs/script work that turns a partial T-Receipts row into measurable deletion opportunities. -(Previously item 2 — *Replace emitter `as_bind().expect()` panics with typed errors* — retired by PR #1548 via the stronger `BindNodeId` witness path; see ledger row 92. Previously item 3 — *Go `UnknownVariant` fail-closed fix* — retired by PR #820, ledger close-out via PR #1545.) +(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