docs: destination-capture --- a second dedication route, and the ledger head
Review found dedication is reachable by a second path. Beyond
set_params, a body can call display(buf, { side = "bottom", dedicated =
true }), which writes request.dedicated straight into the side window
at editor_core.rs:4535, then request a second panel buffer and cause
the fallback. An implementation guarding only the named set_params call
passes revision 8 test while keeping the original defect.
That is the important part, and it is worth more than the route itself:
the second route was found in review AFTER the first was specified,
which is the evidence that guarding one named call site is not a
design. The framing now requires every discovered route recorded and
given its OWN acceptance row, states that the two known routes are not
asserted exhaustive, and says finding a third is part of the work
rather than a later review job.
The ledger head still announced revision 7 as implemented and correct,
declared the blocker closed, and prescribed placement-boundary
enforcement --- the design review had just rejected. I corrected the
lower Q#DC-2 paragraph last round and left the authoritative block
alone, so recovery met the rejected design first and the correction
second. That is the same one-site correction failure this session keeps
reproducing, and this time in the file whose entire job is to be the
volatile state of record.
The head now names all three designs, which two were rejected and why,
and that the shipped code implements the rejected one.
Co-Authored-By: Claude Opus 5 <noreply@anthropic.com>
Claude-Session: https://claude.ai/code/session_016bqGA6s9tTUFzYpbeW3tai
This commit is contained in:
parent
b72df34bc6
commit
ccbed7ab55
|
|
@ -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
|
durable facts are in the retired registry row and the handoff §6
|
||||||
census.
|
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
|
**DO NOT PREPARE A PR, AND DO NOT READ THE SHIPPED DESIGN AS CORRECT.**
|
||||||
landed at `0efc8c0` with 8 pins green; review of that implementation
|
The mechanism landed at `0efc8c0`; review found a correctness blocker;
|
||||||
found a correctness blocker, framing revisions 6 and 7 carried it, and
|
`ca72461` implements **revision 7**, which review then **also
|
||||||
revision 7's design is implemented in the commit named below with 12
|
rejected**. Framing **revision 8** is the current design and is **not
|
||||||
pins green. No PR yet — the lane was told not to open one.
|
implemented**.
|
||||||
|
|
||||||
**The blocker was:** the panel profile skipped checks 2–4 on the claim
|
**The original blocker:** the panel profile skipped checks 2–4 on the
|
||||||
that a panel result never touches a document window. **Panel placement
|
claim that a panel result never touches a document window. **Panel
|
||||||
falls back to an ordinary document window** when the frontend is not
|
placement falls back to an ordinary document window** when the frontend
|
||||||
panel-capable or its side slot is dedicated
|
is not panel-capable or its side slot is dedicated, so a `"panel"`
|
||||||
(`src/editor_core.rs`, `apply_placement`), so a `"panel"` commit could
|
commit could replace a **newer** document with every stale-intent guard
|
||||||
replace a **newer** document with every stale-intent guard skipped.
|
skipped. Reproduced in review.
|
||||||
Reproduced in review.
|
|
||||||
|
|
||||||
**Revision 6's fix was itself unsound and revision 7 replaced it, which
|
**Three designs, two rejected — the sequence is the part worth not
|
||||||
is the part most worth not re-learning.** Revision 6 predicted the
|
re-learning:**
|
||||||
fallback at preflight, arguing the body cannot `await`. That stops
|
|
||||||
concurrent interleaving, not the body: arbitrary synchronous Lua can
|
1. **Revision 6 — predict at preflight.** Rejected: the `await` refusal
|
||||||
dedicate the side slot *inside the callback* and cause the fallback the
|
stops concurrent interleaving, not the body, which is arbitrary
|
||||||
preflight just ruled out. **No preflight snapshot can carry this
|
synchronous Lua and can create the fallback itself.
|
||||||
invariant.** Enforcement is therefore at the **placement boundary**, and
|
2. **Revision 7 — enforce at the placement boundary.** Implemented at
|
||||||
§7's inside-the-body test is what no preflight-snapshot design passes.
|
`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
|
**Also closed:** an invalid-UTF-8 profile (`string.char(255)`) reached
|
||||||
`to_str()` and surfaced mlua's generic conversion error instead of the
|
`to_str()` and surfaced mlua's generic conversion error instead of the
|
||||||
|
|
|
||||||
|
|
@ -326,12 +326,26 @@ than aspirational:**
|
||||||
- `panel_capable` has **no Lua binding at all** — checked across
|
- `panel_capable` has **no Lua binding at all** — checked across
|
||||||
`src/lua_bindings/`. A body cannot make a frontend panel-incapable.
|
`src/lua_bindings/`. A body cannot make a frontend panel-incapable.
|
||||||
|
|
||||||
**The implementation must ENUMERATE the body-reachable transitions
|
**AT LEAST TWO ROUTES REACH DEDICATION, and the second was found in
|
||||||
rather than trust that list**, and report the enumeration — closing the
|
review after the first was specified — which is the evidence that
|
||||||
side window, or any other route to "no usable side slot", counts and I
|
guarding one named call site is not a design:**
|
||||||
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
|
1. **`set_params`** — the writable-field path (`window_panel.rs:888`).
|
||||||
rests on gets observed.
|
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
|
**If the enumeration turns out to be open-ended**, the fallback is to
|
||||||
**collapse the two profiles** — run all four checks always, losing the
|
**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**.
|
in its own test: the callback dedicates the side slot **mid-commit**.
|
||||||
Three assertions, and the second and third are the ones that matter:
|
Three assertions, and the second and third are the ones that matter:
|
||||||
the dedication call itself is **refused**; the side slot is **still
|
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
|
two bullets above cannot catch this — both establish their fallback
|
||||||
state *before* `commit_to` is entered, so a preflight-snapshot design
|
state *before* `commit_to` is entered, so a preflight-snapshot design
|
||||||
passes them.
|
passes them.
|
||||||
|
|
|
||||||
Loading…
Reference in New Issue