From ccbed7ab558cec6a1e53bbdadd379f78345d128b Mon Sep 17 00:00:00 2001 From: Levi Neuwirth Date: Sun, 9 Aug 2026 18:38:41 +0200 Subject: [PATCH] docs: destination-capture --- a second dedication route, and the ledger head Review found dedication is reachable by a second path. Beyond set_params, a body can call display(buf, { side = "bottom", dedicated = true }), which writes request.dedicated straight into the side window at editor_core.rs:4535, then request a second panel buffer and cause the fallback. An implementation guarding only the named set_params call passes revision 8 test while keeping the original defect. That is the important part, and it is worth more than the route itself: the second route was found in review AFTER the first was specified, which is the evidence that guarding one named call site is not a design. The framing now requires every discovered route recorded and given its OWN acceptance row, states that the two known routes are not asserted exhaustive, and says finding a third is part of the work rather than a later review job. The ledger head still announced revision 7 as implemented and correct, declared the blocker closed, and prescribed placement-boundary enforcement --- the design review had just rejected. I corrected the lower Q#DC-2 paragraph last round and left the authoritative block alone, so recovery met the rejected design first and the correction second. That is the same one-site correction failure this session keeps reproducing, and this time in the file whose entire job is to be the volatile state of record. The head now names all three designs, which two were rejected and why, and that the shipped code implements the rejected one. Co-Authored-By: Claude Opus 5 Claude-Session: https://claude.ai/code/session_016bqGA6s9tTUFzYpbeW3tai --- docs/active-work.md | 58 ++++++++++++++++++----------- docs/destination-capture-framing.md | 31 +++++++++++---- 2 files changed, 61 insertions(+), 28 deletions(-) diff --git a/docs/active-work.md b/docs/active-work.md index 5667f33..423f9b6 100644 --- a/docs/active-work.md +++ b/docs/active-work.md @@ -265,30 +265,46 @@ also removed: this branch's "R8 NEEDS A LANE" investigation block, and durable facts are in the retired registry row and the handoff §6 census. -## Destination capture (Q#JR14 generalization) — revision 7 IMPLEMENTED, gate green, no PR yet +## Destination capture (Q#JR14 generalization) — revision 8 OPEN; the shipped code implements the REJECTED revision 7 -**The blocker review re-opened this lane for is CLOSED.** The mechanism -landed at `0efc8c0` with 8 pins green; review of that implementation -found a correctness blocker, framing revisions 6 and 7 carried it, and -revision 7's design is implemented in the commit named below with 12 -pins green. No PR yet — the lane was told not to open one. +**DO NOT PREPARE A PR, AND DO NOT READ THE SHIPPED DESIGN AS CORRECT.** +The mechanism landed at `0efc8c0`; review found a correctness blocker; +`ca72461` implements **revision 7**, which review then **also +rejected**. Framing **revision 8** is the current design and is **not +implemented**. -**The blocker was:** the panel profile skipped checks 2–4 on the claim -that a panel result never touches a document window. **Panel placement -falls back to an ordinary document window** when the frontend is not -panel-capable or its side slot is dedicated -(`src/editor_core.rs`, `apply_placement`), so a `"panel"` commit could -replace a **newer** document with every stale-intent guard skipped. -Reproduced in review. +**The original blocker:** the panel profile skipped checks 2–4 on the +claim that a panel result never touches a document window. **Panel +placement falls back to an ordinary document window** when the frontend +is not panel-capable or its side slot is dedicated, so a `"panel"` +commit could replace a **newer** document with every stale-intent guard +skipped. Reproduced in review. -**Revision 6's fix was itself unsound and revision 7 replaced it, which -is the part most worth not re-learning.** Revision 6 predicted the -fallback at preflight, arguing the body cannot `await`. That stops -concurrent interleaving, not the body: arbitrary synchronous Lua can -dedicate the side slot *inside the callback* and cause the fallback the -preflight just ruled out. **No preflight snapshot can carry this -invariant.** Enforcement is therefore at the **placement boundary**, and -§7's inside-the-body test is what no preflight-snapshot design passes. +**Three designs, two rejected — the sequence is the part worth not +re-learning:** + +1. **Revision 6 — predict at preflight.** Rejected: the `await` refusal + stops concurrent interleaving, not the body, which is arbitrary + synchronous Lua and can create the fallback itself. +2. **Revision 7 — enforce at the placement boundary.** Implemented at + `ca72461`, then rejected: `docs/agent-handoff.md:748` requires + `commit_to` to preflight **before** the callback, because + "validating at display time is four mutations too late". A body has + already created buffers, handles and paint by then, so a + placement-time refusal is a partial commit with an error return. +3. **Revision 8 — keep the preflight, REFUSE the scope-invalidating + mutation.** Current design. Same shape as `Handle:await` being + refused inside a commit scope: the fallback never comes into + existence, and refusal stays mutation-free on `(false, reason)`. + +**The enumeration is the load-bearing part, and it is NOT complete.** +Dedication is reachable by at least two routes — `set_params`, and +`display(buf, { side = …, dedicated = true })`, which writes +`request.dedicated` into the side window (`src/editor_core.rs:4535`). +The second was found in review *after* the first was specified, which +is the evidence that guarding one named call site is not a design. +**Every discovered route must be recorded here and carry its own +acceptance row.** **Also closed:** an invalid-UTF-8 profile (`string.char(255)`) reached `to_str()` and surfaced mlua's generic conversion error instead of the diff --git a/docs/destination-capture-framing.md b/docs/destination-capture-framing.md index b0c01f3..f936230 100644 --- a/docs/destination-capture-framing.md +++ b/docs/destination-capture-framing.md @@ -326,12 +326,26 @@ than aspirational:** - `panel_capable` has **no Lua binding at all** — checked across `src/lua_bindings/`. A body cannot make a frontend panel-incapable. -**The implementation must ENUMERATE the body-reachable transitions -rather than trust that list**, and report the enumeration — closing the -side window, or any other route to "no usable side slot", counts and I -have not proven the two above are exhaustive. This is the same -discipline `gate-protocol-build` applied to Q#GR-1: the fact the design -rests on gets observed. +**AT LEAST TWO ROUTES REACH DEDICATION, and the second was found in +review after the first was specified — which is the evidence that +guarding one named call site is not a design:** + +1. **`set_params`** — the writable-field path (`window_panel.rs:888`). +2. **`display(buf, { side = …, dedicated = true })`** — writes + `request.dedicated` straight into the side window + (`editor_core.rs:4535`). A body can take this route, then request a + second panel buffer and cause the fallback. **An implementation + guarding only route 1 passes revision 8's test while keeping the + original defect.** + +**The implementation must ENUMERATE every body-reachable transition, +record each one here, and give each reachable route its own acceptance +row.** Closing the side window, or any other path to "no usable side +slot", counts. The two above are what review has found so far and are +**not** asserted to be exhaustive — a third would not be surprising, +and finding it is part of the work rather than a later review's job. +This is the discipline `gate-protocol-build` applied to Q#GR-1: the +fact the design rests on gets observed, not assumed. **If the enumeration turns out to be open-ended**, the fallback is to **collapse the two profiles** — run all four checks always, losing the @@ -516,7 +530,10 @@ incidental: no arguments is what keeps capture profile-blind. in its own test: the callback dedicates the side slot **mid-commit**. Three assertions, and the second and third are the ones that matter: the dedication call itself is **refused**; the side slot is **still - undedicated afterwards**; and no partial result was installed. The + undedicated afterwards**; and no partial result was installed. + **One row per route** (§3): `set_params`, and the + `display{side, dedicated = true}` option path. A single row against + one route is what would let the other keep the defect. The two bullets above cannot catch this — both establish their fallback state *before* `commit_to` is entered, so a preflight-snapshot design passes them.