diff --git a/docs/active-work.md b/docs/active-work.md index 423f9b6..0c9e1e4 100644 --- a/docs/active-work.md +++ b/docs/active-work.md @@ -265,13 +265,13 @@ 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 8 OPEN; the shipped code implements the REJECTED revision 7 +## Destination capture (Q#JR14 generalization) — revision 8 IMPLEMENTED, gate green, no PR yet -**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**. +`ca72461` implemented **revision 7**, which review then **also** +rejected; the commit below replaces it with **revision 8** and its +§3 enumeration is **performed and recorded in the framing**. No PR — the +lane was told not to open one. **The original blocker:** the panel profile skipped checks 2–4 on the claim that a panel result never touches a document window. **Panel @@ -297,14 +297,42 @@ re-learning:** 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.** +**THE ENUMERATION IS THE LOAD-BEARING PART, AND IT IS NOW CLOSED — for +a structural reason, not because inspection ran out of ideas.** Full +working in the framing §3; the short form: + +- **Only two pieces of state can matter**, because `resolve_placement` + reaches `Ordinary` from a side request through exactly two branches: + `panel_capable`, and the one side window's `dedicated`. +- **`panel_capable` is unreachable from a body.** It is written only + where a `FrontendView` is constructed, and nothing in + `src/lua_bindings/` constructs, registers or unregisters one — + `register_frontend_view` has callers only in `daemon.rs` and core + unit tests. +- **Eight writes to `dedicated` exist** (`rg 'params\.dedicated\s*=' + src/`); **five are reachable**: `apply_placement`'s `Side` created / + replacing / non-replacing arms, and `set_params`. Two `Ordinary` arms + are harmless (their target is never a side window; one only ever + clears the flag) and one is a unit test. +- **The guards are sited where the property converges, not per caller.** + All three `Side` arms are reached through `apply_placement`, which has + **exactly one caller** — so one guard in `display_buffer` covers every + request-driven dedication, including spellings that do not exist yet. + `set_params` is a genuinely separate write and is guarded separately; + dedication does **not** converge before the field itself, and that is + stated rather than papered over. +- **Closing the side window is NOT a route**, checked rather than + assumed: with no side leaf `side_window_for` returns `None` and + placement **creates** a fresh panel instead of falling back. Hiding is + likewise irrelevant — `panel_hidden` is not consulted by placement. +- **`quit_window`'s `QuitAction::Restore { dedicated: true }` is + UNREACHABLE**, and this was the surprise. `Restore` is stored only on + a *replacing* side placement, and a dedicated slot can never be the + target of one. Guarded anyway, labelled defensive, because its + unreachability is emergent from two rules in another function. +- **What this does not rule out:** the enumeration is closed over the + current tree, not future edits. `params.dedicated` is a public field, + so nothing but the acceptance rows would catch a new direct writer. **Also closed:** an invalid-UTF-8 profile (`string.char(255)`) reached `to_str()` and surfaced mlua's generic conversion error instead of the @@ -320,53 +348,61 @@ from #171 and #215. authoritative tip** — the ref, not a SHA. Recover with `git fetch githubsucks && git checkout destination-capture`. -- **Framing `docs/destination-capture-framing.md`, revision 7.** - Revisions 1–5 were approved over four review rounds; revisions 6 and 7 - are corrections carrying the blocker above, and **revision 7's design - is what the tree implements** — revision 6's preflight prediction is - NOT the shipped mechanism and must not be restored from that document. +- **Framing `docs/destination-capture-framing.md`, revision 8.** + Revisions 1–5 were approved over four review rounds; revisions 6, 7 + and 8 are corrections carrying the blocker above, and **revision 8's + design is what the tree implements**. Revisions 6 and 7 are described + in that document as the record of why *not* those; neither is in the + tree and neither should be restored from it. - **Implemented in three commits.** `779bb02` is the mechanism (`pmacs.window.capture_destination()`, the `ViewDestination` rename, the profile argument); `d5a6170` is - `tests/destination_capture_acceptance.rs`; the revision-7 commit is + `tests/destination_capture_acceptance.rs`; the revision-8 commit is the panel-profile correction plus the invalid-UTF-8 hole. **12 pins**, and both preservation suites pass **unchanged** (journey 47, dired 31) — §7's stop signal not firing rather than being suppressed. -- **HOW THE PANEL PROFILE IS ENFORCED, so revision 6's version does not - get reinstated by someone reading only that document.** - - `EditorCore::display_buffer` refuses **between** `resolve_placement` - and `apply_placement` when a side request resolved to - `PlacementKind::Ordinary` under an active `"panel"` contract whose - destination fails the document preconditions - (`fallback_commit_refusal`). Refusing there means a refused fallback - mutates nothing. +- **HOW THE PANEL PROFILE IS ENFORCED, in one sentence so no earlier + revision gets reinstated by someone reading only that document:** the + preflight stays exactly where it was, and the mutations that would + invalidate it are **refused at the attempt**. + - `EditorCore::panel_commit_dedication_refusal` is the one rule. It + fires while a `"panel"` `CommitContract` is on the core for this + frontend, and is consulted from `display_buffer` (before + `apply_placement`, so a refused attempt mutates nothing), + `pmacs.window.set_params` (before its borrow, so `fixed_rows` in the + same table is not applied either), and `quit_window`. + - **This is the same shape as `Handle:await` being refused inside a + commit scope**, and for the identical reason: something that would + invalidate the scope's guarantee is rejected outright rather than + predicted around or caught late. - The contract (`CommitContract { destination, profile }`) rides on the core, installed and restored by the **same** `ScopedFrontendGuard` that scopes the frontend, so a `"panel"` profile can never outlive the body that declared it. The field is private to the crate — Lua cannot claim a profile for a placement it did not commit to. - - **The preflight predicate survives as an EARLY REFUSAL, not as the - guarantee.** `panel_placement_can_fall_back` still gates the - relaxation in `commit_destination_refusal`, so the statically - knowable case — a frontend that cannot render a panel at all, and - will not acquire the capability mid-body — refuses *before* the body - allocates a buffer, registers a handle and paints. That is the same - reason `commit_to` preflights at all. Both layers are pinned - separately and neither test subsumes the other. + - **`panel_placement_can_fall_back` remains the preflight**, unchanged + in role: it measures whether this frontend places side requests in + the panel *right now*. With the invalidating mutations refused, that + measurement stays true for the life of the body, which is what makes + it a guarantee rather than a forecast. - The four document checks live once, in - `EditorCore::document_destination_refusal`, because they are now - evaluated from two sites and two hand-written copies is how a - backstop ends up weaker than the thing it backs. + `EditorCore::document_destination_refusal`. - **Three deliberate limits**, each a different decision rather than a stricter version of this one: the **document profile is untouched** - (re-running its checks at placement would newly refuse dired's own - documented panel path — a preservation-suite stop signal); only a - **fallback** is guarded, not every `Ordinary` placement (a `"panel"` - body calling `display_file` is pinned as succeeding by - `a_captured_destination_survives_a_frontend_switch`); and the - refusal is of the **placement**, not of falling back — a `"panel"` - commit with an intact destination still degrades gracefully into the - document window. + (constraining its body would newly refuse dired's own documented + panel path — a preservation-suite stop signal); **dedicating a + document window is still allowed** (it cannot change which of + panel-or-document a side request resolves to); and **falling back is + still allowed** — a frontend that cannot render a panel degrades + gracefully exactly as today, because this refuses the mutation that + *manufactures* a fallback, never the fallback itself. +- **Mutation-checked per guard, and the pattern is the evidence the rows + are independent rather than one assertion repeated.** Deleting the + `display_buffer` guard fails the three `display{side, dedicated}` rows + — verified **individually**, by rotating each to the front of the + table, since the first failure otherwise masks the rest. Deleting the + `set_params` guard fails only that row and leaves the display rows + passing. Both leave every other test in the file green. - **Audit: nothing else relied on "a panel never touches a document".** Four doc sites repeated the claim (`ViewDestination`'s own doc twice, `capture_view_destination`, `ViewDestinationLua`) and were corrected; @@ -409,23 +445,26 @@ authoritative tip** — the ref, not a SHA. Recover with frontend scope for the panel profile fails the survives-a-switch pin's panel row; dropping the no-document-window arm fails the Q#DC-4 pair. - **Revision 7's four, each isolating a different way to get it wrong** — - and the pattern of *which* rows survive each is the evidence the layers + **Revision 8's four, each isolating a different way to get it wrong** — + and the pattern of *which* rows survive each is the evidence the parts are independent rather than redundant: - 1. delete the `fallback_commit_refusal` call from `display_buffer` → - **only** the inside-the-body pin fails. Every other test passes, - which is exactly the hole revision 6 would have shipped. - 2. delete the `panel_placement_can_fall_back` arm from + 1. delete the `panel_commit_dedication_refusal` call from + `display_buffer` → the three `display{side, dedicated}` rows fail, + **verified individually** by rotating each to the front of the + table so the first failure cannot mask the rest. Every other test + passes — which is exactly the hole an implementation guarding only + `set_params` would ship. + 2. delete it from `set_params` → **only** that row fails; the three + display rows still pass. + 3. delete the `panel_placement_can_fall_back` arm from `commit_destination_refusal` → **only** the two pre-established - fallback rows fail, and they fail on shape (a raise from the - backstop, with the body having run) rather than on outcome. - 3. make `panel_placement_can_fall_back` unconditionally `true` (the + fallback rows fail, which is the preflight half. + 4. make `panel_placement_can_fall_back` unconditionally `true` (the "widen the predicate" non-fix) → the really-lands-in-the-panel pin, the Q#DC-4 panel pin and the matrix's three panel rows all fail. - That is the profiles collapsing into one, made visible. - 4. make `fallback_commit_refusal` refuse *every* panel fallback → only - the graceful-degradation pin fails, which is the guard - over-reaching. + That is the two profiles collapsing into one, made visible — the + named fallback design, showing up as a test diff rather than + silently. And reverting the byte comparison to `to_str()?` fails the `invalid utf-8` row with mlua's conversion error, on content. diff --git a/docs/destination-capture-framing.md b/docs/destination-capture-framing.md index f936230..fafa83e 100644 --- a/docs/destination-capture-framing.md +++ b/docs/destination-capture-framing.md @@ -1,8 +1,11 @@ # A destination capture any async continuation can use -**Status: revision 8. The mechanism is implemented at `0efc8c0`; -revisions 6–8 carry an OPEN correctness blocker that is NOT yet -implemented.** +**Status: revision 8. The mechanism is implemented at `0efc8c0`; the +correctness blocker revisions 6–8 carry is IMPLEMENTED, in revision 8's +shape, with §3's enumeration performed and recorded below.** Revisions +6 and 7 proposed fixes that review rejected; **neither is in the tree**, +and the two paragraphs describing them are kept as the record of why +this shape and not those. *(Revisions 2–5 said "Pre-implementation. Awaiting approval" while the ledger recorded the lane as approved and implemented. Same @@ -12,13 +15,14 @@ standing in its own header.)* **Revision 8 rejects BOTH of the previous two fixes and takes a third shape.** Revision 6 predicted the fallback at preflight (the body can change it). Revision 7 moved enforcement to the placement boundary — -which **breaks the invariant `commit_to` exists for**: handoff §748 -says it preflights *before* the callback because "validating at display -time is four mutations too late", so a placement-time refusal arrives -after arbitrary Lua has created buffers, handles and paint. Revision 8 -keeps the preflight and **refuses the mutations that would invalidate -it**, the same shape as the existing await refusal. Refusal stays -mutation-free on the `(false, reason)` path. +which **breaks the invariant `commit_to` exists for**: +`docs/agent-handoff.md:748` says it preflights *before* the callback +because "validating at display time is four mutations too late", so a +placement-time refusal arrives after arbitrary Lua has created buffers, +handles and paint. Revision 8 keeps the preflight and **refuses the +mutations that would invalidate it**, the same shape as the existing +await refusal. Refusal stays mutation-free on the `(false, reason)` +path. **Revision 6 fixes an UNSOUND matrix, not a preference.** Q#DC-2 gave the panel profile only check 1, on the claim that a panel result never @@ -137,8 +141,11 @@ that was declined for the `scripts/gate` repair, for the same reason. the finding that shapes the design: - `*git-status*` goes through `listview.open`, which resolves `display` with a **`"panel"`** default - (`builtin/runtime/listview.lua:550`). It lands in the bottom - panel, **not** in a document window. + (`builtin/runtime/listview.lua:550`). It **requests** the bottom + panel rather than a document window — *requests*, because a side + request FALLS BACK into a document window on a frontend that is not + `panel_capable` or whose one slot is dedicated elsewhere. That + fallback is this lane's blocker; §3 and Q#DC-2 carry it. - `*git-diff*` calls `pmacs.window.display(buf, { select = true })` — the **document** target, deliberately, "so the status panel it was invoked from stays visible beside it" @@ -152,11 +159,25 @@ loses to the user**"* — a user who replaced the buffer while work was in flight is newer information than the request. **That predicate is right for a document replacement and wrong for a -panel.** The git status panel does not replace the captured window's -buffer; it opens in the bottom panel beside it. Refusing to show it -because the user switched files in the document window would be a -refusal with no relationship to what the continuation actually does — -the panel case would inherit a check about a window it never touches. +panel — WHILE THE PANEL REALLY IS A PANEL, which is the qualification +the rest of this document exists to add.** A git status panel that +lands in the bottom panel does not replace the captured window's +buffer; it opens beside it. Refusing to show it because the user +switched files in the document window would be a refusal with no +relationship to what the continuation actually does, and that case +would inherit a check about a window it never touches. + +**Read the previous paragraph with its condition attached, not as a +standing fact.** Panel placement **falls back** into an ordinary +document window when the frontend is not `panel_capable` or its one +side slot is dedicated elsewhere — and then the panel case *does* touch +the captured window, replacing whatever the user put there. That +fallback is this lane's correctness blocker, and the unqualified +version of this claim is precisely what made revision 5's matrix +unsound. The resolution is below, at the end of Q#DC-2: the preflight +measures whether this frontend places side requests in the panel, and +the mutations that would falsify that measurement mid-commit are +refused. Meanwhile the diff case *is* a document replacement, and wants exactly the dired semantics. @@ -298,7 +319,7 @@ dedicate the side slot itself. Revision 7 then moved enforcement to the placement boundary. **That breaks the invariant `commit_to` exists for.** `docs/agent-handoff.md` -§748 states it without qualification: +`docs/agent-handoff.md:748` states it without qualification: > [`commit_to`] preflights every precondition *before* invoking the > callback — dired mutates handle state, `prev`, and paint long before @@ -326,9 +347,11 @@ than aspirational:** - `panel_capable` has **no Lua binding at all** — checked across `src/lua_bindings/`. A body cannot make a frontend panel-incapable. -**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:** +**FIVE WRITES REACH DEDICATION.** Review found the second *after* the +first was specified, which is the evidence that guarding one named call +site is not a design — and the enumeration below, performed against the +tree rather than by recall, found three more. The two review named +first are: 1. **`set_params`** — the writable-field path (`window_panel.rs:888`). 2. **`display(buf, { side = …, dedicated = true })`** — writes @@ -338,21 +361,82 @@ guarding one named call site is not a design:** 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. +**THE ENUMERATION, PERFORMED. It is CLOSED, and it is closed for a +structural reason rather than by inspection stopping when it ran out of +ideas.** Recorded here as the framing required, with what was looked +for, what was found, and what cannot be ruled out. -**If the enumeration turns out to be open-ended**, the fallback is to +*Step 1 — how few pieces of state can matter.* `resolve_placement` +reaches `Ordinary` from a side request through exactly two branches, so +only two pieces of state are levers at all: `FrontendView::panel_capable`, +and the one side window's `Window::params.dedicated`. Everything else a +body can touch is irrelevant by construction, which is what makes the +enumeration finite instead of "every mutation in the editor". + +*Step 2 — `panel_capable` is unreachable, not merely unguarded.* It is +written **only** where a `FrontendView` is constructed, and no +`FrontendView` is constructed, registered or unregistered anywhere in +`src/lua_bindings/` — `register_frontend_view` and +`unregister_frontend_view` have callers only in `daemon.rs` (attach and +detach) and in core unit tests. A body cannot reach it. + +*Step 3 — every write to `dedicated`, from `rg 'params\.dedicated\s*=' +src/`, classified.* Eight sites, no exceptions: + +| # | site | verdict | +|---|---|---| +| 1 | `apply_placement`, `Side` **created** | reachable — `display{side, dedicated}` with no panel yet | +| 2 | `apply_placement`, `Side` **replacing** | reachable — `display{side, dedicated}`, different buffer | +| 3 | `apply_placement`, `Side` **non-replacing** | reachable — `display{side, dedicated}`, same buffer | +| 4 | `apply_placement`, `Ordinary` (`!fell_back`) | harmless — every `Ordinary` target is filtered `!is_side`, so it is never the slot | +| 5 | `apply_placement`, `Ordinary` (clear) | harmless — only ever writes `false` | +| 6 | `set_params` | reachable — the direct write (Q#BP2c) | +| 7 | `quit_window`, `QuitAction::Restore` | **unreachable**, see below | +| 8 | an `EditorCore` unit test | not Lua-reachable | + +*Step 4 — the guards, sited where the property converges rather than at +each caller.* Sites 1, 2, 3 (and 4, 5) are all reached through +`apply_placement`, which has **exactly one caller**, `display_buffer`. +So one guard there covers every request-driven dedication, including +routes that do not exist yet. `set_params` is a genuinely separate write +and is guarded separately — dedication does *not* converge before the +field itself, and that is stated rather than papered over. Two live +guards, five reachable sites. + +*Step 5 — what was looked for and found NOT to be a route.* Closing the +side window is **not** one: with no side leaf `side_window_for` returns +`None` and `resolve_placement` **creates** a fresh panel rather than +falling back, so quitting or hiding the panel mid-commit is safe, and +`panel_hidden` is not consulted by placement at all. `params.side` is +likewise unreachable — `set_params` refuses it and only +`apply_placement`'s created branch writes it, so a body cannot promote +an already-dedicated document window into the slot. + +*Step 6 — site 7 is unreachable, and this is the one finding that +surprised.* `QuitAction::Restore` carries the outgoing `dedicated` flag, +so quitting the panel looked like a route with no `dedicated` argument +at the call site at all. It cannot be constructed: `Restore` is only +ever *stored* on a **replacing** side placement, and a dedicated slot +can never be the target of one — a side request with a different buffer +falls through to `Ordinary`, and an exact-target request is refused by +`window_accepts_buffer`. So `Restore { dedicated: true }` has no +producer. It is guarded anyway, defensively and labelled as such, +because its unreachability is an emergent property of two rules in a +different function. + +**What this does NOT rule out.** The enumeration is closed over the +current tree, not over future edits: relaxing `resolve_placement`'s +dedicated arm, or adding a binding that writes `params.dedicated` +directly, reopens it. `Window::params.dedicated` is a public field, so +the compiler does not enforce the funnel — the acceptance rows are what +would catch a regression, one per reachable site. + +**If the enumeration had turned out open-ended**, the fallback was to **collapse the two profiles** — run all four checks always, losing the panel relaxation. That is safe, simple, and honest; it is not the preferred answer only because it makes the parameterization pointless. Choosing it is a design decision needing its own approval, not a -silent retreat. +silent retreat. **It was not needed.** **What is NOT the fix: refusing a panel commit that would fall back.** Falling back to an ordinary window is existing, deliberate behaviour @@ -531,9 +615,12 @@ incidental: no arguments is what keeps capture profile-blind. 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. - **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 + **One row per reachable WRITE SITE** (§3), which is four and not two: + `set_params`, and `display{side, dedicated}` in each of + `apply_placement`'s **created**, **replacing** and **non-replacing** + arms. A single row against one route is what would let another keep + the defect — and rows per *call spelling* would have missed that one + spelling reaches three different writes. The two bullets above cannot catch this — both establish their fallback state *before* `commit_to` is entered, so a preflight-snapshot design passes them. diff --git a/src/editor_core.rs b/src/editor_core.rs index 43c6656..4cc92f1 100644 --- a/src/editor_core.rs +++ b/src/editor_core.rs @@ -3488,6 +3488,23 @@ impl EditorCore { } other => other, }; + // Q#DC-2 (revision 8). A `Restore` carries the OUTGOING + // presentation's `dedicated` flag (see `apply_placement`), so + // quitting the panel can re-dedicate the one slot without any + // `dedicated` argument appearing at the call site. Refused for + // the same reason and at the same point as the other attempts — + // before `quit_window` has touched anything. + if let QuitAction::Restore { + dedicated: true, .. + } = action + && self + .windows + .get(&target) + .is_some_and(crate::window::Window::is_side) + && let Some(reason) = self.panel_commit_dedication_refusal(fid) + { + return Err(format!("window.quit: {reason}")); + } match action { QuitAction::Delete => { // Capture the remembered origin BEFORE the window dies: @@ -4029,10 +4046,19 @@ impl EditorCore { .ok_or_else(|| format!("frontend {fid:?} has no window layout"))? .active; let placement = self.resolve_placement(fid, request)?; - // THE PLACEMENT BOUNDARY (Q#DC-2, revision 7). Refuse before - // `apply_placement` so a refused fallback mutates nothing. - if let Some(reason) = self.fallback_commit_refusal(request, &placement) { - return Err(reason); + // Q#DC-2 (revision 8): dedicating the side slot inside a + // `"panel"` commit is refused AT THE ATTEMPT, so the preflight's + // measurement cannot go stale. `resolve_placement` is pure, so + // this still refuses before anything is mutated. + // + // Note the guard is on the DEDICATION, not on the display: the + // body's ordinary `display(buf, {side = "bottom"})` is exactly + // what a panel continuation is for and always proceeds. + if request.dedicated == Some(true) + && matches!(placement.kind, PlacementKind::Side { .. }) + && let Some(reason) = self.panel_commit_dedication_refusal(fid) + { + return Err(format!("display: {reason}")); } self.apply_placement(fid, request, &placement)?; let select = request @@ -4207,62 +4233,97 @@ impl EditorCore { } /// **The guarantee** behind the `"panel"` commit profile (Q#DC-2, - /// revision 7): a side request that actually fell back into a - /// document window must satisfy the document preconditions. + /// revision 8): inside such a commit, the operations that would make + /// this frontend's side request fall back are **refused at the + /// attempt**. /// - /// Reaching [`PlacementKind::Ordinary`] while a side was REQUESTED is - /// exactly the fallback [`Self::apply_placement`] documents — not - /// panel-capable, or the one slot is dedicated elsewhere — and the - /// result is then installed into a **document** window. A `"panel"` - /// commit that skipped checks 2–4 on the strength of "a panel never - /// touches a document window" would, right here, replace a document - /// view with no stale-intent guard at all: capture A, the user opens - /// B, the continuation lands, B is gone. That is the failure - /// `commit_to` exists to prevent, arrived at through the profile - /// meant to be the safe one. + /// # The defect this closes /// - /// **Why here and not at preflight.** This is the first moment the - /// fallback is a *fact*. A preflight snapshot cannot bind it: the - /// body is arbitrary synchronous Lua and may create the very - /// condition — take the panel, set it `dedicated`, then ask for a - /// side — after the snapshot was taken. Refusing `await` inside the - /// commit scope stops a *second coroutine* interleaving; it places no - /// restriction on the body's own statements. + /// The panel profile skips preflight checks 2–4 on the strength of "a + /// panel result never touches a document window". Panel placement + /// **falls back** into an ordinary document window when the frontend + /// is not `panel_capable` or its one side slot is dedicated elsewhere + /// ([`Self::apply_placement`] says so in its own comment), and then + /// installs the result there. So a `"panel"` commit that reached a + /// fallback would replace a document view with no stale-intent guard: + /// capture A, the user opens B, the continuation lands, B is gone. /// - /// Three deliberate limits, each of which would be a different - /// decision rather than a stricter version of this one: + /// # Why this shape, and not the two that were tried first /// - /// * **The document profile is untouched.** Its preflight already ran - /// these checks against the same destination, and re-running them - /// here would newly refuse dired's own panel path, which documents - /// and accepts the fallback (`builtin/runtime/dired.lua`). - /// * **Only a fallback, not every document placement.** A panel-profile - /// body that displays into a document window *without asking for a - /// side* has mislabelled its profile; it has not exercised this - /// relaxation. Widening to every [`PlacementKind::Ordinary`] would - /// also refuse a `"panel"` commit whose body calls `display_file`, - /// which is pinned as succeeding. - /// * **Refusing the placement, not the fallback.** Falling back is - /// deliberate graceful degradation for a frontend without panel - /// capability; a `"panel"` commit whose destination is still valid - /// falls back and lands exactly as it does today. The profile - /// relaxes checks; it does not get to move where a result goes. - fn fallback_commit_refusal( - &self, - request: &DisplayRequest, - placement: &Placement, - ) -> Option { - if request.side.is_none() || !matches!(placement.kind, PlacementKind::Ordinary) { - return None; - } + /// * **Predicting the fallback at preflight is unsound.** The body is + /// arbitrary *synchronous* Lua and can create the condition itself. + /// Refusing `await` inside the commit scope stops a second + /// coroutine interleaving; it places no restriction on the body's + /// own statements. + /// * **Refusing at the placement boundary is too late.** `commit_to` + /// preflights *before* invoking the callback precisely because a + /// body creates buffers, registers handles and paints long before + /// it asks to display anything — "validating at display time is + /// four mutations too late" (`docs/agent-handoff.md`). A refusal + /// arriving after all of that is not a refusal; it is a partial + /// commit with an error return. + /// + /// So the preflight stays where it is and **the mutation that would + /// invalidate it is rejected** — the same shape as `Handle:await` + /// being refused inside a commit scope, for the identical reason. + /// With these refused, the preflight measurement cannot go stale, the + /// fallback never comes into existence, and nothing needs refusing + /// late. + /// + /// # The enumeration this rests on + /// + /// [`Self::resolve_placement`] can only reach + /// [`PlacementKind::Ordinary`] from a side request in two ways, so + /// only two pieces of state matter: + /// + /// 1. `FrontendView::panel_capable` is false. It is written **only** + /// where a `FrontendView` is constructed, and no `FrontendView` is + /// constructed, registered or unregistered anywhere in + /// `src/lua_bindings/` — that is the daemon's attach path. **A + /// body cannot reach it at all.** + /// 2. The frontend's one side slot exists **and is dedicated** to a + /// different buffer. `Window::params.dedicated` is the only + /// remaining lever, and every write to it is guarded or harmless: + /// the two in `apply_placement`'s `Ordinary` arm target a document + /// window (never a side one — every `Ordinary` target is filtered + /// `!is_side`) and one of them only ever clears the flag; the + /// three in its `Side` arm and the one in `pmacs.window.set_params` + /// are the attempts refused here; and `quit_window` restoring a + /// saved `dedicated: true` presentation is refused too. + /// + /// **Losing the side window is NOT a route** and was checked rather + /// than assumed: with no side leaf, `side_window_for` returns `None` + /// and `resolve_placement` **creates** a fresh panel instead of + /// falling back. Closing or hiding the panel mid-commit is therefore + /// safe, and `panel_hidden` is not consulted by placement at all. + /// `params.side` is likewise unreachable — `set_params` refuses it, + /// and only `apply_placement`'s created branch ever writes it, so a + /// body cannot turn an already-dedicated document window into the + /// side slot. + /// + /// # What is deliberately NOT refused + /// + /// * **The document profile is untouched.** Its preflight already + /// checked the same destination, and constraining its body would + /// newly refuse dired's own documented panel path. + /// * **Dedicating a *document* window is fine.** It cannot change + /// which of panel-or-document a side request resolves to. + /// * **Falling back is still allowed.** A frontend that cannot render + /// a panel degrades gracefully exactly as it does today; this + /// refuses the *mutation that manufactures* a fallback, never the + /// fallback itself. + pub(crate) fn panel_commit_dedication_refusal(&self, fid: FrontendId) -> Option { let contract = self.commit_contract.as_ref()?; - if contract.profile != CommitProfile::Panel { + if contract.profile != CommitProfile::Panel || contract.destination.frontend != fid { return None; } - let reason = self.document_destination_refusal(&contract.destination)?; - Some(format!( - "display: this \"panel\" commit fell back to a document window, and {reason}" - )) + Some( + "cannot dedicate the side window inside a \"panel\" commit_to --- the commit's \ + preflight was relaxed because this frontend places side requests in the panel, \ + and dedicating the one slot would silently redirect the result into a document \ + window instead (dedicate outside the commit, or use the \"document\" profile)" + .to_string(), + ) } /// Q#BP3's precedence: exact target, then side affinity, then diff --git a/src/lua_bindings/window_panel.rs b/src/lua_bindings/window_panel.rs index d9051a0..9f7f137 100644 --- a/src/lua_bindings/window_panel.rs +++ b/src/lua_bindings/window_panel.rs @@ -908,6 +908,24 @@ pub(crate) fn install(lua: &Lua, core: &SharedCore, win: &Table) -> mlua::Result None => None, }; let dedicated = opts.get::>("dedicated")?; + // Q#DC-2 (revision 8). The direct route to the one + // mutation that could make a `"panel"` commit's + // relaxed preflight wrong. Refused BEFORE the borrow + // below, so the attempt changes nothing --- including + // `fixed_rows`, which is in the same option table. + if dedicated == Some(true) { + let core = cc.borrow(); + if core + .windows + .get(&id) + .is_some_and(crate::window::Window::is_side) + && let Some(reason) = core.panel_commit_dedication_refusal(fid) + { + return Err(mlua::Error::runtime(format!( + "pmacs.window.set_params: {reason}" + ))); + } + } { let mut core = cc.borrow_mut(); let window = core.windows.get_mut(&id).ok_or_else(|| { diff --git a/tests/destination_capture_acceptance.rs b/tests/destination_capture_acceptance.rs index 842b39e..fee4ba9 100644 --- a/tests/destination_capture_acceptance.rs +++ b/tests/destination_capture_acceptance.rs @@ -20,17 +20,20 @@ //! * **A refusal is asserted on its reason**, never on the mere fact //! that something failed. `commit_to` has five distinct refusals and a //! raise; "it errored" would pass on any of the wrong ones. -//! * **The panel profile's relaxation is pinned at BOTH of its -//! evaluation sites** (revision 7). The preflight is an early refusal -//! that spares the body; the guarantee is enforced where placement -//! resolves, because the body is arbitrary synchronous Lua and can -//! create the fallback *after* any snapshot was taken — refusing -//! `await` stops a second coroutine interleaving, not the body's own -//! statements. Three tests carry that split and none subsumes another: +//! * **The panel profile's relaxation is pinned as a preflight PLUS the +//! refusal that keeps it true** (revision 8). The preflight measures +//! whether this frontend places side requests in the panel; the body is +//! arbitrary *synchronous* Lua, so refusing `await` — which only stops +//! another coroutine interleaving — does not stop it invalidating that +//! measurement. The answer is neither to predict the body nor to catch +//! it late at placement (by then it has created buffers, handles and +//! paint, which is "four mutations too late" all over again) but to +//! **refuse the mutation at the attempt**, exactly as `await` is +//! refused. Three tests carry it and none subsumes another: //! `a_panel_commit_that_falls_back_runs_the_document_preflight` (the -//! body must not run), -//! `a_panel_commit_whose_body_creates_the_fallback_is_refused_at_placement` -//! (the result must not land), and +//! body must not run at all when the fallback already holds), +//! `a_body_that_tries_to_create_the_fallback_is_refused_at_the_attempt` +//! (the mutation is refused, and nothing partial is left behind), and //! `a_panel_commit_that_falls_back_with_a_valid_destination_still_lands` //! (falling back is still graceful degradation, not an error). //! @@ -90,6 +93,32 @@ fn name_in(s: &EditorState, window: WindowId) -> String { registry.get(buffer).expect("buffer").name().to_string() } +/// Whether `window` is pinned to its buffer (Q#BP2c `dedicated`). +fn dedicated(s: &EditorState, window: WindowId) -> bool { + s.core + .borrow() + .windows + .get(&window) + .is_some_and(|w| w.params.dedicated) +} + +/// Whether a buffer by this name exists at all. +/// +/// The "nothing partial was installed" assertion needs to see a side +/// effect the body would have left *before* reaching any display, and a +/// created-but-never-shown buffer is exactly that. +fn buffer_exists(s: &EditorState, name: &str) -> bool { + eval( + s, + &format!( + "for _, id in ipairs(pmacs.buffer.list()) do + if pmacs.describe.buffer(id).name == {name:?} then return true end + end + return false" + ), + ) +} + fn local_window(s: &EditorState) -> WindowId { s.core .borrow() @@ -454,6 +483,13 @@ fn the_preflight_matrix_holds_in_both_profiles() { const PANEL_BODY: &str = "pmacs.window.display(pmacs.buffer.create('*result*'), \ { side = 'bottom' })"; +/// A reusable panel: present and **undedicated**, so the preflight +/// measures "this frontend places side requests in the panel" and the +/// relaxation applies. Every mutation row starts from here except the +/// one whose whole point is that no panel exists yet. +const PANEL_ARRANGED: &str = "pmacs.window.display(pmacs.buffer.create('*pinned*'), \ + { side = 'bottom', dedicated = false, select = false })"; + /// Arrange one of the two reasons a side request falls back into a /// document window, and assert the arrangement took. /// @@ -578,95 +614,185 @@ fn a_panel_commit_that_falls_back_runs_the_document_preflight() { } } -/// **N** — the case no preflight snapshot can catch: the **body itself** -/// creates the fallback, and the refusal still fires. +/// **N** — a body that tries to **create** the fallback is refused **at +/// the attempt**, and the refusal lands on the mutation rather than on +/// the outcome. /// -/// This is why the guarantee moved to the placement boundary. Revision 6 -/// argued that a prediction taken at preflight could not go stale, -/// because `commit_to`'s body cannot `await`. Refusing `await` prevents -/// another *coroutine* interleaving; it places no restriction on the body -/// itself, which is arbitrary Lua running synchronously: +/// This is the case no preflight snapshot can catch, and the two rows +/// above cannot reach it: both establish their fallback state *before* +/// `commit_to` is entered. The body is arbitrary **synchronous** Lua, so +/// refusing `await` — which stops another coroutine interleaving — +/// places no restriction on it: /// /// ```lua /// pmacs.window.set_params(pmacs.window.panel(), { dedicated = true }) /// pmacs.window.display(result, { side = "bottom" }) /// ``` /// -/// Two statements. The first invalidates the prediction, the second cashes -/// it in. The arrangement here is deliberately the **inverse** of the -/// preflight rows: an undedicated panel exists, so the prediction says -/// "this will land in the panel", the relaxation applies, and the body -/// runs. Only when placement resolves is the fallback a fact. +/// Two statements: the first invalidates the preflight, the second cashes +/// it in. The arrangement is deliberately the **inverse** of the rows +/// above — the preflight says "this lands in the panel", the relaxation +/// applies, and the body runs. /// -/// What it asserts, and why each is load-bearing: +/// **Asserting only "document B was not replaced" is insufficient**, and +/// an earlier version of this test made exactly that mistake: it passes +/// on a design that lets the body mutate freely and merely declines the +/// final installation, leaving every other side effect behind. So the +/// three assertions that matter are that the **dedication call itself is +/// refused**, the slot is **still undedicated afterwards**, and **nothing +/// partial was installed**. /// -/// * the body **did** run — otherwise the test would be re-proving the -/// preflight and this whole case would be untested; -/// * the refusal arrives as a **raise** from `display`, since the body was -/// already running and there is no `(false, reason)` left to return — -/// asserted on content, and it names both the fallback and the -/// stale-intent reason; -/// * `*newer*` is **still in the document window**. That is the actual -/// user-visible guarantee; everything above it is mechanism. +/// # One row per WRITE SITE, not per call spelling /// -/// *Mutation:* delete the `fallback_commit_refusal` call from -/// `display_buffer`. This test fails on all three; every other test in -/// this file still passes, which is precisely the hole revision 6 left. +/// A single row is exactly what would let a second route keep the +/// defect — which is not hypothetical: review found the +/// `display{side, dedicated}` route *after* `set_params` was specified. +/// So the rows are chosen to hit each distinct write to +/// `Window::params.dedicated` that a side window can receive, rather +/// than each way of phrasing the call: +/// +/// | row | reaches | +/// |---|---| +/// | `set_params` | the direct write in the binding (Q#BP2c) | +/// | `display{side, dedicated}` replacing | `apply_placement`'s **replacing** arm | +/// | `display{side, dedicated}` same buffer | its **non-replacing** arm | +/// | `display{side, dedicated}` with no panel | its **created** arm | +/// +/// The three `display` rows converge on one guard, in `display_buffer` — +/// `apply_placement` has exactly one caller, so every request-driven +/// dedication passes through it. They are still separate rows because +/// that convergence is a property of today's call graph, and a row per +/// arm fails loudly if it stops holding. +/// +/// The rest of the enumeration is **unreachable rather than refused** +/// and is recorded in `EditorCore::panel_commit_dedication_refusal`, +/// because a test cannot express it: `panel_capable` has no Lua binding; +/// **losing** the side window is not a fallback route at all +/// (`resolve_placement` creates a fresh panel instead); and `quit` +/// restoring a `dedicated: true` presentation cannot be constructed, +/// since `QuitAction::Restore` only captures that flag on a *replacing* +/// side placement and a dedicated slot can never be the target of one. +/// +/// *Mutation:* delete the `panel_commit_dedication_refusal` call from +/// either guarded site — `set_params` drops row 1, `display_buffer` +/// drops rows 2–4 — and every other test in this file still passes. #[test] -fn a_panel_commit_whose_body_creates_the_fallback_is_refused_at_placement() { - let s = editor(); - - // A REUSABLE panel: undedicated, so the preflight prediction says - // this frontend places side requests in the panel. - exec( - &s, - "pmacs.window.display(pmacs.buffer.create('*pinned*'), - { side = 'bottom', dedicated = false, select = false })", - ); - capture(&s); - let doc = local_window(&s); - exec( - &s, - "pmacs.window.switch_buffer(pmacs.buffer.create('*newer*'))", - ); - assert_eq!( - name_in(&s, doc), - "*newer*", - "the arrangement must make the captured window stale" - ); - - commit_body( - &s, - Some("'panel'"), - &format!( - "pmacs.window.set_params(pmacs.window.panel(), {{ dedicated = true }}) - {PANEL_BODY}" +fn a_body_that_tries_to_create_the_fallback_is_refused_at_the_attempt() { + // (label, panel arrangement before the capture, attempted mutation) + let routes: [(&str, &str, &str); 4] = [ + ( + "set_params", + PANEL_ARRANGED, + "pmacs.window.set_params(pmacs.window.panel(), { dedicated = true })", ), - ); + ( + "display{side, dedicated} replacing", + PANEL_ARRANGED, + "pmacs.window.display(pmacs.buffer.create('*usurp*'), + { side = 'bottom', dedicated = true, select = false })", + ), + ( + // The same buffer the panel already shows: `replacing` is + // false, so this lands in a DIFFERENT arm of the same + // function, which a row against the replacing arm alone + // would not exercise. + "display{side, dedicated} same buffer", + PANEL_ARRANGED, + "pmacs.window.display(pmacs.window.buffer(pmacs.window.panel()), + { side = 'bottom', dedicated = true, select = false })", + ), + ( + // NO panel at capture time: the preflight relaxes because + // `side_window_for` is None (a side request would CREATE a + // panel, never fall back). The body then creates one + // dedicated, which makes the next side request fall back. + "display{side, dedicated} creating the panel", + "", + "pmacs.window.display(pmacs.buffer.create('*usurp*'), + { side = 'bottom', dedicated = true, select = false })", + ), + ]; - assert!( - ran(&s), - "the body must have run -- the preflight could not have known, and a test where \ - it did not run would be re-proving the preflight" - ); - let raised = raised(&s).expect( - "the refusal arrives as a raise: the body was already running, so there is no \ - (false, reason) return left to make", - ); - assert!( - raised.contains("fell back to a document window"), - "the message must name what happened; got {raised:?}" - ); - assert!( - raised.contains("now shows another buffer"), - "and which document precondition failed; got {raised:?}" - ); - assert_eq!( - name_in(&s, doc), - "*newer*", - "the user's newer buffer must survive -- this is the guarantee, and it is what a \ - preflight-only design cannot provide" - ); + for (label, arrange, attempt) in routes { + let s = editor(); + exec(&s, arrange); + + let panel_before = s.core.borrow().side_window_for(FrontendId::LOCAL); + if let Some(panel) = panel_before { + assert!( + !dedicated(&s, panel), + "{label}: the slot must start UNDEDICATED, or the preflight would have \ + refused and this row would be re-proving the preflight" + ); + } + let panel_buffer_before = panel_before.map(|panel| name_in(&s, panel)); + + capture(&s); + let doc = local_window(&s); + exec( + &s, + "pmacs.window.switch_buffer(pmacs.buffer.create('*newer*'))", + ); + + commit_body(&s, Some("'panel'"), &format!("{attempt}\n{PANEL_BODY}")); + + assert!( + ran(&s), + "{label}: the body must have run -- the preflight could not have known" + ); + + // 1. THE MUTATION ITSELF IS REFUSED, on content. + let raised = raised(&s).unwrap_or_else(|| { + panic!("{label}: the attempted mutation must be refused, not merely declined later") + }); + assert!( + raised.contains("cannot dedicate the side window"), + "{label}: the refusal must name the operation it is refusing; got {raised:?}" + ); + assert!( + raised.contains("\"panel\" commit_to"), + "{label}: and why it is refused here specifically; got {raised:?}" + ); + + // 2. THE SLOT IS STILL UNDEDICATED -- including the row where + // the slot would have been created dedicated, which must + // leave no slot at all rather than an undedicated one. + let panel_after = s.core.borrow().side_window_for(FrontendId::LOCAL); + assert_eq!( + panel_after, panel_before, + "{label}: a refused mutation must not have created or removed the side slot" + ); + if let Some(panel) = panel_after { + assert!( + !dedicated(&s, panel), + "{label}: a refused mutation must not have happened -- the whole design \ + rests on the preflight's measurement still being true afterwards" + ); + } + + // 3. NOTHING PARTIAL WAS INSTALLED. + if let (Some(panel), Some(before)) = (panel_after, panel_buffer_before.as_ref()) { + assert_eq!( + &name_in(&s, panel), + before, + "{label}: the panel must still show what it showed" + ); + } + assert_eq!( + name_in(&s, doc), + "*newer*", + "{label}: and the user's newer buffer must survive" + ); + assert!( + !buffer_exists(&s, "*result*"), + "{label}: the refusal must land BEFORE the body's own display -- a `*result*` \ + buffer means the commit got partway and then stopped" + ); + assert!( + !buffer_exists(&s, "*usurp*") || panel_after == panel_before, + "{label}: no usurping presentation may have been installed" + ); + } } /// **P** — a `"panel"` commit that falls back with a **still-valid**