diff --git a/docs/active-work.md b/docs/active-work.md index 0b16cf5..830ce56 100644 --- a/docs/active-work.md +++ b/docs/active-work.md @@ -265,7 +265,33 @@ 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) — IMPLEMENTED, gate green, no PR yet +## Destination capture (Q#JR14 generalization) — IMPLEMENTED at `0efc8c0`, then RE-OPENED by review + +**DO NOT PREPARE A PR FROM THIS LANE'S CURRENT STATE.** The mechanism +landed at `0efc8c0` with 8 pins green — and review of that +implementation found a **correctness blocker** that is still open. +Framing revisions 6 and 7 carry it; neither is implemented yet. + +**The blocker:** the panel profile skips 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:4138-4148`), 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 replaces it.** +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. **Enforcement belongs +at the placement boundary**, and §7 now requires an +inside-the-body test that no preflight-snapshot design can pass. + +**Also open:** an invalid-UTF-8 profile (`string.char(255)`) reaches +`to_str()` and surfaces mlua's generic conversion error instead of the +documented message naming the accepted values — the same reachability +class as revision 5's `Option` defect, one layer down. **Written with the lane's first commit**, per the standing correction from #171 and #215. @@ -275,15 +301,25 @@ 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 6**, - APPROVED after four review rounds. -- **Implemented in two commits.** `779bb02` is the mechanism - (`pmacs.window.capture_destination()`, the `ViewDestination` rename, - the profile argument); `d5a6170` is - `tests/destination_capture_acceptance.rs`, eight pins covering §7. - The full gate line below is green, and both preservation suites pass - **unchanged** (journey 47, dired 31) — no edit to either, which is - §7's stop signal not firing rather than being suppressed. +- **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 open blocker above** and have not + been implemented. +- **Implemented in two commits, and superseded in part.** `779bb02` is + the mechanism (`pmacs.window.capture_destination()`, the + `ViewDestination` rename, the profile argument); `d5a6170` is + `tests/destination_capture_acceptance.rs`. The gate line below was + green at `0efc8c0` and both preservation suites passed **unchanged** + (journey 47, dired 31) — §7's stop signal not firing rather than + being suppressed. + + **But those eight pins do NOT cover §7 as it now reads.** They were + written against revision 5's matrix, which review disproved: none of + them exercises a fallback placement, and none could — the two + fallback tests revision 6 asked for did not exist yet, and revision + 7 adds a third (the inside-the-body transition) that no + preflight-snapshot design can pass. Reading "eight pins covering §7" + off this entry is exactly the mistake it now exists to prevent. - **TWO FRAMING CLAIMS THE TREE DID NOT MATCH.** Neither changed a decision; both are recorded because the framing says "counted, not estimated" and a reader will check. diff --git a/docs/destination-capture-framing.md b/docs/destination-capture-framing.md index 233d33e..29c478e 100644 --- a/docs/destination-capture-framing.md +++ b/docs/destination-capture-framing.md @@ -1,14 +1,25 @@ # A destination capture any async continuation can use -**Status: revision 6. APPROVED and IMPLEMENTED at `0efc8c0`; revision 6 -carries a correctness blocker found in review of that implementation -and is NOT yet implemented.** +**Status: revision 7. The mechanism is implemented at `0efc8c0`; +revisions 6 and 7 carry an OPEN correctness blocker that is NOT yet +implemented.** *(Revisions 2–5 said "Pre-implementation. Awaiting approval" while the ledger recorded the lane as approved and implemented. Same contradiction class this document keeps correcting elsewhere, left standing in its own header.)* +**Revision 7 replaces revision 6's fix, which was unsound for the same +reason revision 6's target was.** Revision 6 moved the panel/document +decision to a **preflight prediction**, arguing nothing could change +before placement because the body cannot `await`. The await refusal +stops *concurrent interleaving*; it does not stop the body — arbitrary +synchronous Lua — from dedicating the side slot itself and causing the +very fallback the preflight just ruled out. **Enforcement moves to the +placement boundary**, where the fallback is a fact rather than a +forecast, and §7 gains the inside-the-body test that the two +pre-established-state tests could never catch. + **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 touches a document window. **Panel placement falls back to an ordinary @@ -277,17 +288,42 @@ on the placement actually being a panel. Whenever placement **can** fall back to a document window, the panel profile runs the **full document preflight**. -**Both fallback causes are predictable at preflight**, which is what -makes this implementable rather than a race: +**ENFORCEMENT IS AT THE PLACEMENT BOUNDARY, NOT AT PREFLIGHT — +revision 6 got this wrong too, and the reason is worth stating because +it is a whole class of mistake.** -1. `view.panel_capable` is false — a property of the frontend. -2. The frontend's single side slot is dedicated elsewhere — readable - from core state. +Revision 6 said the two fallback causes are "predictable at preflight", +because `commit_to` refuses `await` so "nothing can change between +preflight and placement". **The await refusal prevents *concurrent +interleaving* — another coroutine mutating state while this one is +parked. It says nothing about the body itself**, which is arbitrary +Lua running synchronously and perfectly able to change the state the +preflight just measured: -And nothing can change between preflight and placement: `commit_to` -runs its body synchronously inside a scope that **refuses `await`** -(`async.lua:87-90`), so the prediction cannot go stale under the -commit it guards. +> obtain the existing panel → set it `dedicated = true` → request panel +> display + +Preflight sees a reusable panel and relaxes checks 2–4; the body then +causes the fallback; the result replaces a stale document. **No +preflight predicate can close this**, however it is phrased — the +measurement is simply taken before the thing it measures is decided. + +**So the check moves to where the fact is known.** Placement resolving +to `PlacementKind::Ordinary` for a request that asked for a side *is* +the fallback (`editor_core.rs:4138-4148`). At that point, under an +active panel-profile commit, the document preconditions are evaluated +against the captured destination and refused if they fail. The commit +scope is already Rust-side app data (`CommitScopeActive`), so the +profile and the destination can ride there for the placement path to +consult. + +**And the tempting non-fix, named so nobody reaches for it:** widening +the preflight predicate from "will it fall back" to "*could* it ever". +Since the body can always dedicate the side slot, that predicate is +always true, the panel profile collapses into the document profile, and +the parameterization buys nothing. If collapsing them is genuinely +right, that is a design decision needing its own approval — not a way +to make a broken predicate safe. **What is NOT the fix: refusing a panel commit that would fall back.** Falling back to an ordinary window is existing, deliberate behaviour @@ -456,12 +492,19 @@ incidental: no arguments is what keeps capture profile-blind. a stale-buffer refusal. Asserting merely that it does not error would pass on a call silently downgraded to the panel profile, which is the regression that would quietly void Journey Stage 1a's guarantees. -- **A `"panel"` commit that FALLS BACK to a document window runs the - document preflight**, witnessed for **both** causes separately — - a non-panel-capable frontend, and a dedicated side slot. Each asserts - the stale-intent refusal fires: capture A, make B newer, commit - `"panel"`, and observe the refusal rather than B being replaced. - This is the defect revision 5's matrix admitted. +- **A `"panel"` commit that FALLS BACK to a document window is checked + against the document preconditions**, witnessed for **both** causes + separately — a non-panel-capable frontend, and a dedicated side slot. + Each asserts the stale-intent refusal fires: capture A, make B newer, + commit `"panel"`, observe the refusal rather than B being replaced. +- **THE FALLBACK STATE IS ALSO ESTABLISHED FROM INSIDE THE BODY**, in + its own test: the callback dedicates the side slot **mid-commit** and + then requests panel display. This is the case that distinguishes + placement-time enforcement from preflight prediction, and **the two + bullets above cannot catch it** — both set up their fallback state + *before* `commit_to` is entered, so a preflight-snapshot design + passes them. A design that passes only those two has not been shown + to work. - **A `"panel"` commit that really lands in the panel still skips checks 2–4** — otherwise the fix has quietly collapsed the two profiles into one and the parameterization buys nothing.