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.