docs: destination-capture revision 7 --- enforce at placement, not preflight
Review found revision 6 fix unsound for the same reason its target was. Revision 6 moved the panel/document decision to a preflight prediction, arguing nothing could change before placement because commit_to refuses await. That refusal stops CONCURRENT INTERLEAVING --- another coroutine mutating state while this one is parked. It does nothing about the body itself, which is arbitrary synchronous Lua and can obtain the panel, set dedicated = true, and then request panel display. Preflight sees a reusable panel and relaxes checks 2-4; the body causes the fallback; the result replaces a stale document. No preflight predicate closes this, however phrased --- the measurement is taken before the thing it measures is decided. So enforcement moves to the placement boundary, where resolving to Ordinary for a request that asked for a side IS the fallback rather than a forecast of one. The commit scope is already Rust-side app data, so the profile and the destination can ride there. The tempting non-fix is named so nobody reaches for it: widening the predicate from "will it fall back" to "could it ever" is always true, since the body can always dedicate the slot --- which collapses the two profiles and buys nothing. Section 7 gains the test that distinguishes the designs: the callback dedicates the side slot MID-COMMIT. Both fallback tests revision 6 asked for establish their state before commit_to is entered, so a preflight-snapshot design passes them. A design passing only those two has not been shown to work. The ledger claimed the lane implemented with eight pins covering section 7. Those pins were written against revision 5 matrix, which review disproved --- none exercises a fallback placement. A recovering machine reading that entry would have prepared a PR from a lane with an open correctness blocker. Co-Authored-By: Claude Opus 5 <noreply@anthropic.com> Claude-Session: https://claude.ai/code/session_016bqGA6s9tTUFzYpbeW3tai
This commit is contained in:
parent
6032ed1c2a
commit
edb84a520d
|
|
@ -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<String>` 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.
|
||||
|
|
|
|||
|
|
@ -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.
|
||||
|
|
|
|||
Loading…
Reference in New Issue