docs: destination-capture revision 8 --- refuse the mutation, keep the preflight
Revisions 6 and 7 were both wrong, in opposite directions, and review caught each. Revision 6 predicted the fallback at preflight and argued the body could not change it. False: the await refusal stops concurrent interleaving, not the body, which is arbitrary synchronous Lua and can dedicate the side slot itself. Revision 7 moved enforcement to the placement boundary. That breaks the invariant commit_to exists for. Handoff section 748 states it without qualification --- it preflights every precondition BEFORE invoking the callback, because dired mutates handle state, prev and paint long before it reaches anything that could refuse, so validating at display time is four mutations too late. A refusal that arrives after arbitrary Lua has created buffers, handles and paint is not a refusal; it is a partial commit with an error return. So revision 8 does neither. It keeps the preflight where it is and REFUSES the mutations that would invalidate it --- the same shape as the await refusal already in this file, for the identical reason: something that would invalidate the scope guarantee is rejected rather than predicted around. Refusal stays mutation-free on the normal (false, reason) path. The mutation surface is narrow, which is what makes this tight rather than aspirational. dedicated is writable from Lua and is one of only two writable window fields per Q#BP2c; panel_capable has no Lua binding at all, checked across src/lua_bindings. But the implementation must ENUMERATE the body-reachable transitions rather than trust that list --- closing the side window, or any other route to no usable side slot, counts, and I have not proven those two exhaustive. If the enumeration is open-ended, the named fallback is to collapse the two profiles and always run all four checks. Safe, simple, honest, and it makes the parameterization pointless --- which is why it is the fallback and not the answer, and why choosing it needs its own approval. The inside-the-body test is strengthened accordingly. Revision 7 asked it to assert that document B was not replaced, which passes on a design that lets the body mutate freely and merely declines the final installation. It now asserts the dedication call is refused, the slot is still undedicated afterwards, and nothing partial was installed. The refusal must land on the mutation, not on the outcome. The ledger Q#DC-2 summary still repeated the disproved premise verbatim, so a recovering reader met two incompatible answers in one lane entry. Co-Authored-By: Claude Opus 5 <noreply@anthropic.com> Claude-Session: https://claude.ai/code/session_016bqGA6s9tTUFzYpbeW3tai
This commit is contained in:
parent
86cd08959a
commit
b72df34bc6
|
|
@ -464,10 +464,19 @@ authoritative tip** — the ref, not a SHA. Recover with
|
|||
(`listview.open` defaults `display` to `"panel"`,
|
||||
`builtin/runtime/listview.lua:550`); `*git-diff*` replaces a
|
||||
**document** window. `commit_to`'s stale-intent check (Q#JR14c) is
|
||||
right for the second and wrong for the first — the panel never
|
||||
touches the captured window's buffer, so refusing on its change is a
|
||||
refusal unrelated to what the continuation does. One shape
|
||||
over-refuses the panel or under-checks the document.
|
||||
right for the second and, *when the placement really is a panel*,
|
||||
irrelevant to the first. One shape over-refuses the panel or
|
||||
under-checks the document.
|
||||
|
||||
**DO NOT READ THE OLDER FORM OF THIS BULLET, WHICH SAID "the panel
|
||||
never touches the captured window's buffer".** That is the claim
|
||||
revisions 6–8 invalidate: panel placement **falls back** to an
|
||||
ordinary document window when the frontend is not panel-capable or
|
||||
its side slot is dedicated. The relaxation is conditional, and the
|
||||
mutations that could make it fall back are refused inside a
|
||||
panel-profile commit (revision 8) rather than predicted at preflight
|
||||
(revision 6) or caught at placement (revision 7, which would refuse
|
||||
after the callback had already mutated).
|
||||
- **Stop signal recorded in the framing:** if any existing dired test
|
||||
needs editing, the generalization changed Journey Stage 1a's
|
||||
semantics, and that is cause to stop rather than to adjust the test.
|
||||
|
|
|
|||
|
|
@ -1,7 +1,7 @@
|
|||
# A destination capture any async continuation can use
|
||||
|
||||
**Status: revision 7. The mechanism is implemented at `0efc8c0`;
|
||||
revisions 6 and 7 carry an OPEN correctness blocker that is NOT yet
|
||||
**Status: revision 8. The mechanism is implemented at `0efc8c0`;
|
||||
revisions 6–8 carry an OPEN correctness blocker that is NOT yet
|
||||
implemented.**
|
||||
|
||||
*(Revisions 2–5 said "Pre-implementation. Awaiting approval" while the
|
||||
|
|
@ -9,16 +9,16 @@ 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 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.
|
||||
|
||||
**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
|
||||
|
|
@ -288,42 +288,57 @@ on the placement actually being a panel. Whenever placement **can**
|
|||
fall back to a document window, the panel profile runs the **full
|
||||
document preflight**.
|
||||
|
||||
**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.**
|
||||
**PREFLIGHT STAYS WHERE IT IS; THE MUTATION THAT WOULD INVALIDATE IT IS
|
||||
REFUSED. Revisions 6 and 7 were both wrong, in opposite directions.**
|
||||
|
||||
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:
|
||||
Revision 6 predicted the fallback at preflight and argued the body
|
||||
could not change it. **False**: the await refusal stops *concurrent
|
||||
interleaving*, not the body, which is arbitrary synchronous Lua and can
|
||||
dedicate the side slot itself.
|
||||
|
||||
> obtain the existing panel → set it `dedicated = true` → request panel
|
||||
> display
|
||||
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:
|
||||
|
||||
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.
|
||||
> [`commit_to`] preflights every precondition *before* invoking the
|
||||
> callback — dired mutates handle state, `prev`, and paint long before
|
||||
> it reaches anything that could refuse, so **validating at display
|
||||
> time is four mutations too late**.
|
||||
|
||||
**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.
|
||||
Refusing at placement means refusing *after* arbitrary callback code has
|
||||
created buffers, handles and paint. A late refusal is not a refusal; it
|
||||
is a partial commit with an error return.
|
||||
|
||||
**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.
|
||||
**So neither predict nor refuse late — forbid the mutation.** Inside a
|
||||
panel-profile commit, the operations that could change the placement
|
||||
outcome are **refused**, exactly as `Handle:await` is refused inside a
|
||||
commit scope and for the identical reason: something that would
|
||||
invalidate the scope's guarantee is rejected rather than predicted
|
||||
around. With them refused, the preflight measurement cannot go stale,
|
||||
and refusal stays mutation-free on the normal `(false, reason)` path.
|
||||
|
||||
**The mutation surface is narrow, which is what makes this tight rather
|
||||
than aspirational:**
|
||||
|
||||
- `dedicated` **is** writable from Lua — and it is one of only two
|
||||
writable window fields (`window_panel.rs:888`, *"Only `fixed_rows`
|
||||
and `dedicated` are writable (Q#BP2c)"*).
|
||||
- `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.
|
||||
|
||||
**If the enumeration turns out to be open-ended**, the fallback is 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.
|
||||
|
||||
**What is NOT the fix: refusing a panel commit that would fall back.**
|
||||
Falling back to an ordinary window is existing, deliberate behaviour
|
||||
|
|
@ -497,14 +512,20 @@ incidental: no arguments is what keeps capture profile-blind.
|
|||
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 BODY THAT TRIES TO CREATE THE FALLBACK IS REFUSED AT THE ATTEMPT**,
|
||||
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
|
||||
two bullets above cannot catch this — both establish their fallback
|
||||
state *before* `commit_to` is entered, so a preflight-snapshot design
|
||||
passes them.
|
||||
|
||||
**Asserting only "document B was not replaced" is insufficient**, and
|
||||
revision 7's 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. The refusal must land on the mutation, not on the outcome.
|
||||
- **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.
|
||||
|
|
|
|||
Loading…
Reference in New Issue