docs(framing): revise panel replay contract after review

Make the three-state panel-pointer result a pre-effect disposition and
replace the competing latch matrices with one complete lifecycle table.
Accepted tails now require a live gesture, accepted release replay and
record-driven termination are mutually exclusive, and the witnesses
cover stale tails plus immediate and later duplicate completion.

Place projection-raised release delivery at the enforceable daemon
boundary after semantic rendering returns and before its messages are
written. Keep the arm invariant as a backstop behind pointer, detach,
and frame-order witnesses.

Split horizontal-wheel ground truth by terminal reporting/local and
document targets. Record the missing document-panel effect explicitly
under GUI Stage 1b B1--B3, update that framing's surface scope, and
synchronize the active-work checkpoint.
This commit is contained in:
Levi Neuwirth 2026-08-20 20:50:21 +02:00
parent cda078fa91
commit 1fc3af63de
No known key found for this signature in database
3 changed files with 174 additions and 111 deletions

View File

@ -281,13 +281,15 @@ from #171 and #215 — the correction the 1b lane missed, honoured here.
**`githubsucks/panel-pointer-replay` is the authoritative tip** (the **`githubsucks/panel-pointer-replay` is the authoritative tip** (the
ref, not a SHA). Recover with ref, not a SHA). Recover with
`git fetch githubsucks && git checkout panel-pointer-replay`. `git fetch githubsucks && git checkout panel-pointer-replay`.
- **No PR yet. Checkpoint: framing revision 15 AWAITING APPROVAL - **No PR yet. Checkpoint: §5a framing revision 16 and its GUI Stage
(revision 14 was reviewed and had four blocking gaps, all answered); 1b revision-13 ownership amendment AWAITING APPROVAL (revision 15
was reviewed, corrected and folded into this branch);
IMPLEMENTATION STILL PAUSED, now on approval rather than on a IMPLEMENTATION STILL PAUSED, now on approval rather than on a
blocker.** §5a's replay contract is approved at revision 12; revision blocker.** §5a's **pre-merge** replay contract was approved at
13 ruled Q#BP-R3 and blocked the lane on a protocol-bearing mapping revision 12; revisions 14–16 are the post-merge amendment now under
generation; **that block is DISCHARGED** — the slice merged as #242 review. Revision 13 ruled Q#BP-R3 and blocked the lane on a
(`47b5463`). protocol-bearing mapping generation; **that block is DISCHARGED** —
the slice merged as #242 (`47b5463`).
- **MERGED main into this branch** at `b758c2e` rather than rebasing: - **MERGED main into this branch** at `b758c2e` rather than rebasing:
the lane's 12 commits include 10 framing revisions over the same the lane's 12 commits include 10 framing revisions over the same
800–1000 line doc regions, so a rebase meant twelve rounds of 800–1000 line doc regions, so a rebase meant twelve rounds of
@ -314,14 +316,22 @@ from #171 and #215 — the correction the 1b lane missed, honoured here.
§5b and this lane gave `dispatch_semantic_panel_pointer`'s `bool` §5b and this lane gave `dispatch_semantic_panel_pointer`'s `bool`
different meanings — accepted-as-a-gesture versus consumed-here. A different meanings — accepted-as-a-gesture versus consumed-here. A
mode-line press therefore **arms the latch** on this branch today. mode-line press therefore **arms the latch** on this branch today.
**Q#BP-R4** rules a three-state `PanelPointerOutcome`, with an **Q#BP-R4** rules a three-state `PanelPointerOutcome`, classified
asymmetric latch rule: arm only on `Accepted` + `Down(Left)`, **before** target effects. Only an `Accepted` `Down(Left)` arms;
consume on any `Up(Left)` that was not `Refused`. left `Drag`/`Up` require a live record; an accepted `Up` performs
- **Revision 14 also carries** the rows §5b's split table assigned ordinary replay once, a consumed/chrome `Up` performs the recorded
here, a **pending-release slot** for the cancellation record §5b completion once, and a refused `Up` preserves the record.
leaves nowhere to wait, the **four transitions** that strand a live - **Revision 16 carries** the rows §5b's split table assigned here, a
gesture once effects attach, and a **re-measurement obligation**: **pending-release slot** for the cancellation record §5b leaves
every production anchor in §5a has moved, evidenced in the revision. nowhere to wait, and the **four transitions** that strand a live
gesture once effects attach. Drain order is executable: before the
next panel-pointer effect; before detach teardown; and, for a
projection-raised cancellation, after `render_frame` returns but
before any returned message is written. Ground truth is re-measured
at `2c0d3ff`. Document-panel horizontal scrolling is a named deferral
to GUI Stage 1b B1–B3; a horizontal tick whose terminal precedence
selects child reporting already emits SGR, and the local terminal
branch has no horizontal viewport effect.
- **THE BLOCKER, and why the earlier acceptance failed.** A - **THE BLOCKER, and why the earlier acceptance failed.** A
`PanelPointer` names a cell; nothing on the wire says which inverse `PanelPointer` names a cell; nothing on the wire says which inverse
mapping the frontend saw, so the daemon inverts against whatever is mapping the frontend saw, so the daemon inverts against whatever is
@ -387,32 +397,26 @@ from #171 and #215 — the correction the 1b lane missed, honoured here.
**controller identity** catches the shared-path mutation, since **controller identity** catches the shared-path mutation, since
`apply_terminal_gesture` claims at `src/editor.rs:3571` before local `apply_terminal_gesture` claims at `src/editor.rs:3571` before local
handling and activation alone claims nothing. handling and activation alone claims nothing.
- **Why this lane exists.** `PanelPointer` **replays nothing**: - **Why this lane exists, re-measured at `2c0d3ff`.** The branch now
`dispatch_semantic_panel_pointer` (`src/editor.rs:2674`) validates, replays document selection, terminal mouse reporting and vertical
focuses, returns. A panel wheel is dead on both axes and so is every wheels; the remaining acceptance-48 effect is **listview row
gesture past focus. **GUI arc 1b is BLOCKED on this lane and rebases selection**. Q#BP-R4 and §5b's inherited rows still need
onto its merge commit.** implementation: pre-effect disposition/latch ordering, fixed-domain
gesture tails, exact-once termination, cancellation effects and the
pending-release drains. **GUI arc 1b is BLOCKED on this lane and
rebases onto its merge commit.**
- **No new framing document.** Acceptance 48 is already ruled in - **No new framing document.** Acceptance 48 is already ruled in
`docs/bottom-panel-framing.md`; §5a adds ground truth to it. `docs/bottom-panel-framing.md`; §5a adds ground truth to it.
- **The measurement's headline: AC48 is HALF implemented**, and nothing - **Current clause split.** DONE: click/focus and terminal activation;
had written the halves down separately. focused-only auto-scroll with passive `view_top` preserved; lossless
- **DONE:** click-to-focus and the terminal activation rule and coalesced event delivery; panel document selection; terminal
(`src/editor.rs:2701` and its `activates`); the focused-only child reporting/local selection; vertical document and terminal
auto-scroll clamp with passive `view_top` preserved (`:2568`–`:2571`, which wheel effects. MISSING here: listview row selection and the
already cites parent 48); the coalescing rules — `Move`/`Drag` lifecycle/cancellation effects above. Horizontal wheel is split:
tails coalesce, press/release/context/wheel lossless child-reporting terminal ticks already emit codes 66/67; the local
(`pmacs-gpu/src/attach.rs:374`). terminal branch is deliberately inert; document-panel `view_left`
- **MISSING:** listview row selection, panel selection, terminal is explicitly GUI Stage 1b B1–B3's effect, matching the production
mouse reporting, wheel replay. comment in `src/editor.rs:2999`–`:3003`.
- **The replay is mostly WIRING; both mechanisms exist.**
`apply_terminal_gesture` (`src/editor.rs:3525`) is *"the one terminal
pointer path, shared by both frontend kinds"* and already drives
child reporting, selection and scrollback — a panel terminal needs
the same call, with `side_window_for` + `TerminalViewKey` +
`panel_grid_size` (which the dispatcher already fetches).
`scroll_window` (`:3845`) is window-scoped, cursor carry included.
**A wheel-only bridge is the wrong shape** — the shared path takes
every kind at once.
- **The scoping hazard.** `set_cursor_byte` (`src/editor_core.rs:1216`), - **The scoping hazard.** `set_cursor_byte` (`src/editor_core.rs:1216`),
`begin_selection` (`:4691`) and `clear_selection` are `begin_selection` (`:4691`) and `clear_selection` are
**active-window scoped**; used naively they would move the **active-window scoped**; used naively they would move the

View File

@ -1,5 +1,13 @@
# Bottom panel — framing (window placement + side windows) # Bottom panel — framing (window placement + side windows)
**Revision 16 — 2026-08-20, AWAITING APPROVAL.** Revision 16 closes
review of 15: Q#BP-R4 is one pre-effect disposition/gesture-lifecycle
table; projection-raised releases drain after `render_frame` returns
and before its messages are written; horizontal-wheel ground truth is
split by target/domain and the missing document effect is explicitly
owned by GUI Stage 1b; superseded current-state text is removed from
this section and the active-work ledger.
**Revision 4 — pre-implementation, DRAFT after review round 3 plus landed-state **Revision 4 — pre-implementation, DRAFT after review round 3 plus landed-state
audit. Ground truth: canonical `main` @ `ddaa80d` (documentation landing #152; audit. Ground truth: canonical `main` @ `ddaa80d` (documentation landing #152;
runtime @ `0dd16a5`, GPU initial target / #148 after folding Stage 2 / #149), runtime @ `0dd16a5`, GPU initial target / #148 after folding Stage 2 / #149),
@ -7,7 +15,7 @@ protocol v20, 2026-07-24. Amended by the pre-implementation dependency
verification in §0.6: the folding dependency is cleared, and one geometry verification in §0.6: the folding dependency is cleared, and one geometry
caller-census error is corrected.** caller-census error is corrected.**
**Revision 13 — 2026-08-14, AWAITING APPROVAL. Q#BP-R3 is OVERRULED: **Previously, revision 13 — 2026-08-14. Q#BP-R3 was OVERRULED:
the lane BLOCKS on a protocol-bearing cell-mapping generation (new the lane BLOCKS on a protocol-bearing cell-mapping generation (new
§5b).** Revision 12 accepted current-state hit semantics on three §5b).** Revision 12 accepted current-state hit semantics on three
bounds, and all three were wrong — a **foreign** edit moves the mapping bounds, and all three were wrong — a **foreign** edit moves the mapping
@ -1970,13 +1978,22 @@ cannot preserve the old panel-focused attach leak.
## 5a. Acceptance 48 — ground truth, RE-MEASURED at `2c0d3ff` (2026-08-20) ## 5a. Acceptance 48 — ground truth, RE-MEASURED at `2c0d3ff` (2026-08-20)
**Status: revision 15 — AWAITING APPROVAL.** Revision 13 ruled Q#BP-R3 **Status: revision 16 — AWAITING APPROVAL.** Revision 13 ruled Q#BP-R3
and **blocked** this lane on a protocol-bearing mapping generation. and **blocked** this lane on a protocol-bearing mapping generation.
That slice was framed as §5b, approved at revision 16, and **merged as That slice was framed as §5b, approved at revision 16, and **merged as
#242 (`47b5463`)**, so **revision 13's block is DISCHARGED** and its #242 (`47b5463`)**, so **revision 13's block is DISCHARGED** and its
ruling stands as history rather than as a gate. Revision 14 answered ruling stands as history rather than as a gate. Revision 14 answered
what the lane inherits from a substrate that changed underneath it. what the lane inherits from a substrate that changed underneath it.
**Revision 16 closes review of 15.** It replaces the two competing
Q#BP-R4 matrices with one pre-effect disposition/lifecycle table;
names the projection drain at the only enforceable seam — after
`render_frame` returns and before its messages are written; splits
horizontal-wheel ground truth by target and gesture domain; records
GUI Stage 1b as the owner of document-panel horizontal scrolling; and
removes revision 14's now-false remeasurement obligation from the live
section and ledger.
**Revision 15 answers review of 14, and four of its five changes are **Revision 15 answers review of 14, and four of its five changes are
corrections rather than additions:** corrections rather than additions:**
@ -1995,7 +2012,8 @@ corrections rather than additions:**
- **The ground truth was knowingly false and is now RE-MEASURED**, at - **The ground truth was knowingly false and is now RE-MEASURED**, at
`2c0d3ff`, rather than deferred to implementation. Two clauses the `2c0d3ff`, rather than deferred to implementation. Two clauses the
old table called MISSING are DONE, and a third — the horizontal old table called MISSING are DONE, and a third — the horizontal
wheel — turns out to be an unruled gap. wheel — exposed an ownership gap that revision 16 now splits and
assigns explicitly.
- **"This lane MOVES the grade" was wrong.** Step 5/GPU is floored - **"This lane MOVES the grade" was wrong.** Step 5/GPU is floored
`Partial` by 5(a) IME and step 8 is already `Works`; no journey cell `Partial` by 5(a) IME and step 8 is already `Works`; no journey cell
moves. The draft had read this section's own MISSING column as if it moves. The draft had read this section's own MISSING column as if it
@ -2024,19 +2042,24 @@ kept below as history; **this table is the current one**:
| move/drag tails coalesce; press/release/context/wheel lossless and ordered | **DONE** | `coalesce_kind` (`pmacs-gpu/src/attach.rs:338`) | | move/drag tails coalesce; press/release/context/wheel lossless and ordered | **DONE** | `coalesce_kind` (`pmacs-gpu/src/attach.rs:338`) |
| **panel selection** | **DONE — was MISSING** | `replay_panel_document_gesture` (`src/editor.rs:2914`), called at `:2903`: `Down`/`Drag`/`Up(Left)`, shift-extend, double-click word select, right-press | | **panel selection** | **DONE — was MISSING** | `replay_panel_document_gesture` (`src/editor.rs:2914`), called at `:2903`: `Down`/`Drag`/`Up(Left)`, shift-extend, double-click word select, right-press |
| **terminal mouse reporting** | **DONE — was MISSING** | `apply_terminal_gesture` called at `src/editor.rs:2899`, viewport `content_rows` | | **terminal mouse reporting** | **DONE — was MISSING** | `apply_terminal_gesture` called at `src/editor.rs:2899`, viewport `content_rows` |
| **wheel moves the panel's viewport** | **VERTICAL DONE — was MISSING** | `ScrollUp`/`ScrollDown` → `scroll_window` (`src/editor.rs:2925`) | | **vertical wheel moves the panel's viewport** | **DONE — was MISSING** | document `ScrollUp`/`ScrollDown` → `scroll_window` (`src/editor.rs:2925`); reporting and local terminal paths share `apply_terminal_gesture` |
| **horizontal wheel** | **INERT, AND UNRULED** | `ScrollLeft`/`ScrollRight` fall into the catch-all no-op arm (`src/editor.rs:3004`) **with no comment and no ruling** — the old table's "dead on both axes" became half-true without anyone deciding the other half | | **horizontal wheel, terminal precedence selects child reporting** | **RECEIVER DONE; PRODUCER AWAITS GUI 1b** | `apply_terminal_gesture` reaches `encode_mouse`, whose `ScrollLeft`/`ScrollRight` codes are 66/67 (`src/terminal/input.rs:130`–`:131`) |
| **horizontal wheel, terminal precedence selects local handling** | **RULED INERT** | Shift, reporting-off or a scrolled-back view can select the local branch; terminal scrollback is vertical and there is no local horizontal viewport, so the shared path deliberately has no `ScrollLeft`/`ScrollRight` arm |
| **horizontal wheel, document panel** | **NAMED DEFERRAL: GUI Stage 1b B1–B3** | `ScrollLeft`/`ScrollRight` are claimed and dropped at `src/editor.rs:3004`; the comment at `:2999`–`:3003` already assigns horizontal panel scrolling to 1b, whose framing now explicitly includes the panel-document surface |
| **listview row selection** | **MISSING** | — no listview handling on the replay path; Q#BP-R1 ruled the semantics (single click selects only), and nothing implements them | | **listview row selection** | **MISSING** | — no listview handling on the replay path; Q#BP-R1 ruled the semantics (single click selects only), and nothing implements them |
| without disturbing the document mirror | **the constraint on all of the above** | — | | without disturbing the document mirror | **the constraint on all of the above** | — |
**Two findings the re-measurement produced**, neither of which a **Two findings the re-measurement produced**, neither of which a
line-number patch would have surfaced: line-number patch would have surfaced:
- **The horizontal wheel is an unruled gap, not a deferral.** It sits - **"Horizontal wheel" was not one verdict.** A tick for which terminal
in a catch-all arm beside `Move` and the non-left buttons, so it precedence selects child reporting already sends the horizontal SGR
reads as deliberate and is not. **Revision 14 does not rule it** — code; the local terminal branch has no horizontal viewport to move;
it names it, because inventing a ruling inside a re-measurement is only a document panel lacks an effect. That last leg is a **named
how an unexamined default becomes a decision. deferral to GUI Stage 1b B1–B3**,
not an unexplained catch-all: 1b owns horizontal tick production,
sign, per-surface residuals and the window-targeted `view_left`
effect. The panel-replay lane remains 1b's prerequisite.
- **Two of the four "MISSING" effects are DONE on this branch.** The - **Two of the four "MISSING" effects are DONE on this branch.** The
section had been telling every reader that replay does nothing while section had been telling every reader that replay does nothing while
the branch it describes had implemented most of it. the branch it describes had implemented most of it.
@ -2694,7 +2717,7 @@ R-d's orphan is distinct from R-b's: **R-b's arrives from a passive
panel, R-d's from a replaced or re-declared one**, and an panel, R-d's from a replaced or re-declared one**, and an
implementation can fix either alone. implementation can fix either alone.
### Revision 14 — what §5b changed underneath this lane ### Revisions 14–16 — what §5b changed underneath this lane
#### Q#BP-R4 — what does `dispatch_semantic_panel_pointer`'s answer MEAN? **RULED: a three-state outcome, not a bool** #### Q#BP-R4 — what does `dispatch_semantic_panel_pointer`'s answer MEAN? **RULED: a three-state outcome, not a bool**
@ -2722,30 +2745,49 @@ fixed, re-entering by merge rather than by edit.
| **a three-state outcome** | **RULED** | | **a three-state outcome** | **RULED** |
```rust ```rust
/// What the dispatcher did with a panel gesture. /// How an authenticated panel event relates to the authoritative
/// panel surface, decided BEFORE any target effect.
pub enum PanelPointerOutcome { pub enum PanelPointerOutcome {
/// Neither this panel's nor well-formed: no grid, out of grid, no /// Not addressable as this panel: no grid, out of grid, no side
/// side window, or a buffer that is not the one shown there. /// window, or a buffer that is not the one shown there.
Refused, Refused,
/// This panel's, and handled HERE deliberately --- the chrome /// This panel owns the cell/event, but it is deliberately not a
/// swallows of Q#BP-R2 and R-c. Not a content gesture. /// content gesture --- the chrome claims of Q#BP-R2 and R-c.
Consumed, Consumed,
/// Reached the target as a content gesture. /// A content gesture for the resolved target.
Accepted, Accepted,
} }
``` ```
**The latch rule, and it is NOT "arm and consume on `Accepted`".** The **The outcome is a DISPOSITION, not proof that an effect already ran.**
two halves are asymmetric, because a release ends a gesture wherever It is decided before replay. The current function combines validation,
the pointer happens to be: classification and mutation, but that ordering cannot implement §5b's
stale-tail rule: an `Up` or `Drag` with no accepted `Down` has already
reached the child/selection before the daemon consults the latch. The
implementation may split the function into classify/apply helpers or
use an equivalent single wrapper, but these two facts are fixed:
- **ARM** only on `Accepted` **and** `Down(Left)`. A chrome press 1. the editor remains the **only** authority that derives
begins nothing. `Refused`/`Consumed`/`Accepted`; the daemon never re-derives chrome,
- **TERMINATE** on any `Up(Left)` that was **not `Refused`** — so target kind or content bounds;
`Accepted` **or** `Consumed`. A **`Refused`** release is different in 2. disposition and the live-gesture check both complete **before** a
kind: out-of-grid or wrong-buffer means the daemon cannot tell the left `Drag`/`Up` target effect.
event is even about this gesture, and §5b already pinned that it must
not consume. **One transition table is authoritative:**
| event | `Refused` | `Consumed` | `Accepted` |
|---|---|---|---|
| `Down(Left)` | no effect; do not arm | no target effect; do not arm | apply the content press, then arm **from the effect result** so target/domain/encoding and `reached_child` describe what actually happened |
| `Drag(Left)` | no effect; retain any live record | no target effect; retain any live record | no live record → inert; live record → continue in the **recorded domain**, update its last valid content cell |
| `Up(Left)` | no effect; retain any live record for a later authoritative cancellation | no live record → inert; live record → deliver the **recorded completion** at its last valid content cell, then take it | no live record → inert; live record → apply the ordinary in-content completion **once**, then take it; do **not** also run recorded completion |
| every other kind | no effect; no latch change | no target effect; no latch change | apply its one-shot content effect; never arm or consume the left-gesture latch |
This is the required asymmetry. A chrome press begins nothing. A
chrome release can end a live gesture, but a refused release cannot be
known to concern it. An accepted release already performs the ordinary
target effect; a consumed release has not, so it terminates from the
record. A stale `Drag`/`Up` with no accepted `Down` is inert rather than
sending a child tail or changing selection.
**"TERMINATE", not "consume", and the distinction is the whole of **"TERMINATE", not "consume", and the distinction is the whole of
review finding 1.** An earlier draft of this ruling said consume, and review finding 1.** An earlier draft of this ruling said consume, and
@ -2760,42 +2802,42 @@ anything. A latch that empties while the child stays pressed is
*exactly* the failure the draft claimed to prevent, now invisible *exactly* the failure the draft claimed to prevent, now invisible
because the bookkeeping looks right. because the bookkeeping looks right.
**RULED: a non-`Refused` `Up(Left)` must produce the target's **RULED: a live gesture plus non-`Refused` `Up(Left)` must produce the
completion effect, and the row asserts the EFFECT, not the latch.** target's completion effect exactly once, and the row asserts the
EFFECT, not the latch.**
| target | required completion effect | | target | required completion effect |
|---|---| |---|---|
| terminal panel, child reporting on | the **release is reported to the child** — the same report an in-content `Up` produces, at the gesture's last content cell per R-c2 | | terminal panel, child reporting on | the **release is reported to the child in the recorded encoding** — an accepted content `Up` uses its accepted cell; a consumed/chrome `Up` uses the gesture's last content cell per R-c2 |
| terminal panel, child reporting off | the **local terminal selection completes** — the selection the drag built is finalised, not abandoned | | terminal panel, child reporting off | the **local terminal selection completes** — the selection the drag built is finalised, not abandoned |
| document panel | the document gesture completes at the last content cell; an empty selection is cleared **without moving point** (the effect §5b's split table already assigns here) | | document panel | the document gesture completes at the last content cell; an empty selection is cleared **without moving point** (the effect §5b's split table already assigns here) |
**And exactly once.** A completion delivered here must not be delivered **And exactly once.** An accepted `Up` must not replay normally and
again by a later cancellation of the same gesture, which is reachable then also run the record-driven completion. Any completion must take
because the four stranding transitions below can fire afterwards. the record, so a later cancellation of the same gesture — reachable
through the four stranding transitions below — cannot repeat it.
| # | mutation | must bite | | # | mutation | must bite |
|---|---|---| |---|---|---|
| P1 | chrome press returns `Accepted` | a chrome `Down(Left)` does not arm | | P1 | chrome press returns `Accepted` | a chrome `Down(Left)` does not arm |
| P2 | `Refused` treated as `Accepted` | §5b's four `g5_substrate_a_refused_*` rows | | P2 | `Refused` treated as `Accepted` | §5b's four `g5_substrate_a_refused_*` rows plus their no-target-effect assertions |
| P3 | chrome `Up` empties the latch but delivers **no** completion | the child-release / selection-completion row — **the latch-only assertion must NOT satisfy this** | | P3 | chrome `Up` empties the latch but delivers **no** completion | the child-release / selection-completion row — **the latch-only assertion must NOT satisfy this** |
| P4 | `Refused` release delivers a completion | a refused release leaves both the latch and the child untouched | | P4 | `Refused` release delivers a completion | a refused release leaves both the latch and the child untouched |
| P5 | completion delivered, then a later cancellation delivers another | the no-duplicate-release row | | P5 | an accepted content `Up` replays normally **and** invokes record-driven completion | the exact child stream contains one release, not two |
| P6 | completion delivered, then a later cancellation delivers another | the no-duplicate-release row |
| P7 | an accepted `Up` with no live record reaches the target | the stale-release row: no child bytes and no local/document selection mutation |
| P8 | an accepted `Drag` with no live record reaches the target | the orphan-drag row: no child bytes and no cursor/selection mutation |
**P3 is written against the earlier draft's own weakness.** A row that **P3 is written against the earlier draft's own weakness.** A row that
asserts only `has_accepted_gesture() == false` passes while the child asserts only `has_accepted_gesture() == false` passes while the child
receives nothing, so the row must read the child's reported bytes or receives nothing, so the row must read the child's reported bytes or
the terminal's selection state. the terminal's selection state.
**That asymmetry is what earns the third state.** Under it, all three **That asymmetry is what earns the third state.** `Refused` preserves a
outcomes are behaviourally distinct at the latch, so each is live gesture, `Consumed` owns the surface but runs only a recorded
falsifiable: completion, and `Accepted` reaches content. Each is behaviourally
distinct at the effect/lifecycle seam, and the single matrix above is
| # | mutation | must bite | the witness contract.
|---|---|---|
| P1 | chrome press returns `Accepted` | a chrome `Down(Left)` does not arm |
| P2 | `Refused` treated as `Accepted` | §5b's four `g5_substrate_a_refused_*` rows |
| P3 | `Consumed` treated as `Refused` for `Up` | a chrome `Up(Left)` consumes a live gesture |
| P4 | consume gated on `Accepted` alone | the same chrome-release row as P3, from the other side |
**R-c2 does not discharge P3.** The producer normalizes a release that **R-c2 does not discharge P3.** The producer normalizes a release that
lands on chrome back to the last content cell, so a conforming lands on chrome back to the last content cell, so a conforming
@ -2869,9 +2911,15 @@ effect too late.
2. **before detach teardown**, so a frontend that goes away does not 2. **before detach teardown**, so a frontend that goes away does not
take an owed release with it — detach is one of the four stranding take an owed release with it — detach is one of the four stranding
transitions below, and it is the one with no later opportunity; transitions below, and it is the one with no later opportunity;
3. **before the frontend's next frame is produced**, so a cancellation 3. **after semantic projection returns and before any message it
raised during projection cannot be overtaken by the frame that returned is filtered or written.** Mapping cancellation is
caused it. discovered *inside* `SemanticRenderState::render_frame`, while the
successor `PresentMapped` is being constructed, so "before that
frame is produced" is impossible. The enforceable daemon seam is
immediately after `sem.render_frame(editor)` returns
(`src/daemon.rs:1428`–`:1430`) and before `for msg in &messages`
(`:1591`). The pending termination drains there, so the successor
frame cannot overtake the release its new mapping required.
| # | mutation | must bite | | # | mutation | must bite |
|---|---|---| |---|---|---|
@ -2879,7 +2927,8 @@ effect too late.
| Q2 | park it but never drain | the same row, from the delivery side | | Q2 | park it but never drain | the same row, from the delivery side |
| Q3 | drain **after** `dispatch_semantic_panel_pointer` instead of before | the **old-release-before-new-press ordering row** — assert the child's byte stream carries the release ahead of the press, not merely that both arrive | | Q3 | drain **after** `dispatch_semantic_panel_pointer` instead of before | the **old-release-before-new-press ordering row** — assert the child's byte stream carries the release ahead of the press, not merely that both arrive |
| Q4 | skip the drain on detach | the detach row: an owed release is delivered before teardown | | Q4 | skip the drain on detach | the detach row: an owed release is delivered before teardown |
| Q5 | allow arming over a pending release | the invariant witness — kept, now as a **backstop** behind the ordering rows rather than as the guarantee | | Q5 | enter the returned-message write loop before draining a projection-raised release | the daemon-order witness records the termination effect before the first successor-frame write |
| Q6 | allow arming over a pending release | the invariant witness — kept, now as a **backstop** behind the ordering rows rather than as the guarantee |
#### Four transitions strand a live gesture, and they become defects HERE #### Four transitions strand a live gesture, and they become defects HERE
@ -2899,23 +2948,13 @@ motion. The daemon side has the same shape and needs the same
independently discriminating legs rather than one shared "resets independently discriminating legs rather than one shared "resets
something" assertion. something" assertion.
#### The ground truth must be RE-MEASURED, and this is evidenced #### Re-measurement closed in revision 16
This section's heading says `72da24a`. **Every production anchor in it The authoritative clause table is now the `2c0d3ff` table at the start
has moved**, measured at `b758c2e`: of §5a. The `72da24a` table is retained only under its explicit
**Superseded** heading. Revision 14's line-movement inventory did its
| §5a claims | actually | job by forcing a clause-by-clause scout; it is no longer a live
|---|---| implementation obligation.
| `dispatch_semantic_panel_pointer` at `src/editor.rs:2674` | `:2809` |
| `apply_terminal_gesture` at `src/editor.rs:3525` | `:3875` |
| `scroll_window` at `src/editor.rs:3845` | `:4195` |
| `Absent` clears the latch at `pmacs-gpu/src/main.rs:6909` | `:7206` |
**The clause table itself is NOT assumed to have survived.** §5b
rewrote the dispatcher this lane measured, so each DONE/MISSING verdict
is owed a re-measurement before implementation, not a line-number
patch. A table that is right about *what* is missing and wrong about
*where* is the kind of record that gets trusted and then misleads.
#### Coherence impact (`COHERENCE.md` §20) #### Coherence impact (`COHERENCE.md` §20)
@ -2926,11 +2965,12 @@ patch. A table that is right about *what* is missing and wrong about
inferred from this section's own MISSING column: inferred from this section's own MISSING column:
- **Step 5 / GPU is `Partial`, and stays `Partial`.** It is floored - **Step 5 / GPU is `Partial`, and stays `Partial`.** It is floored
by **5(a)** — no IME, no `set_ime_allowed`, so composed and CJK by **5(a)** — no IME, no `set_ime_allowed`, so composed and CJK
input is impossible (`COHERENCE.md:462`). Completing 5(c) inside a input is impossible (`COHERENCE.md:468`). Completing 5(c) inside a
panel cannot lift a cell held down by a different clause. That is panel cannot lift a cell held down by a different clause. That is
§2a's aggregation rule working as designed. §2a's aggregation rule working as designed.
- **Step 8 is already `Works` on all three columns.** There is no - **Step 8 is already `Works` on all three columns**
grade left to move; 8(b) is hardened, not opened. (`COHERENCE.md:471`). There is no grade left to move; 8(b) is
hardened, not opened.
- The draft's error was reading §5a's MISSING column as if it were - The draft's error was reading §5a's MISSING column as if it were
the scorecard. **A section-local gap list is not a journey grade**, the scorecard. **A section-local gap list is not a journey grade**,
and the one place that decides grades is `COHERENCE.md`. and the one place that decides grades is `COHERENCE.md`.
@ -2941,7 +2981,7 @@ patch. A table that is right about *what* is missing and wrong about
- **Background work: none started**, and no existing attribution - **Background work: none started**, and no existing attribution
changes. changes.
#### What revision 14 does NOT do #### What revisions 14–16 do NOT reopen
It does not re-open Q#BP-R1 (single click selects only), Q#BP-R2 (a It does not re-open Q#BP-R1 (single click selects only), Q#BP-R2 (a
terminal panel's chrome wheel is consumed, not clamped), or R-a/R-b/ terminal panel's chrome wheel is consumed, not clamped), or R-a/R-b/

View File

@ -1,6 +1,13 @@
# GUI arc, Stage 1 — input foundation (framing) # GUI arc, Stage 1 — input foundation (framing)
**Status: revision 12 — APPROVED.** Revision 12 is §2's ground-truth **Status: revision 13 — AWAITING APPROVAL with bottom-panel §5a
revision 16.** Revision 13 changes no previously ruled outcome. It
makes B1–B3's “per surface” scope explicit for the panel-document
surface, closing the ownership gap exposed by §5a's remeasurement:
panel replay is the prerequisite, while GUI 1b owns horizontal tick
production, residuals and the document-panel `view_left` effect.
**Previously, revision 12 — APPROVED.** Revision 12 is §2's ground-truth
re-measurement for Stage 1a and changes no ruling; it carries two re-measurement for Stage 1a and changes no ruling; it carries two
corrections to claims that were wrong at the original anchor too. corrections to claims that were wrong at the original anchor too.
@ -308,9 +315,9 @@ The crate has **exactly one** executable `event_loop.exit()`, in
| # | Contract | Witness | Mutation | | # | Contract | Witness | Mutation |
|---|---|---|---| |---|---|---|---|
| B1 | Residual per **axis and surface** | deltas discarded | share one accumulator → surface-switch jump | | B1 | Residual per **axis and surface** — primary document, panel document and minimap are distinct owners | deltas discarded | share one accumulator → primary↔panel or document↔minimap surface-switch jump |
| B2 | Wheel-right raises leftmost column; wheel-down raises top line | `x` discarded | invert a sign → that axis's row | | B2 | Wheel-right raises the leftmost column of the **document surface under the pointer**; wheel-down raises its top line. Primary-document horizontal state stays frontend-local; a panel-document tick reaches the daemon's window-targeted `view_left` path | `x` discarded; panel replay currently claims and drops document `ScrollLeft`/`ScrollRight` | invert a sign → that axis's row; omit the panel effect → primary moves while the panel remains inert |
| B3 | Clamps at content bounds; never a negative origin | no horizontal scroll to clamp | remove clamp → **at-bounds row: origin goes negative and the view blanks** | | B3 | Each document surface clamps at its own content bounds; never a negative origin, and wrap pins horizontal origin to zero | no horizontal scroll to clamp | remove a clamp → **at-bounds row: that surface's origin goes negative and the view blanks**; reuse primary bounds for a panel → unequal-width surface row fails |
| B4 | Middle-click paste uses **PRIMARY on Linux** | no middle-click path | use `CLIPBOARD` → B4 only | | B4 | Middle-click paste uses **PRIMARY on Linux** | no middle-click path | use `CLIPBOARD` → B4 only |
| B5 | I-beam over text content only | no I-beam | extend over the gutter → B5 only | | B5 | I-beam over text content only | no I-beam | extend over the gutter → B5 only |
| B6 | Wheel over the minimap scrolls the **document viewport** with **its own residual accumulator**; click/drag remains scrub | **a FULL tick already scrolls today** — minimap pixels are `Elsewhere` (`main.rs:2061`) and the wheel falls through to `scroll_by_lines` (`main.rs:3373`). What fails is **fractional accumulation**, and **residual ownership distinct from the document's**: sub-tick minimap deltas are discarded, and a **surface-switch fractional witness** (part-tick over the minimap, then over the document) must not carry residue across | share the document's accumulator → the surface-switch fractional row jumps | | B6 | Wheel over the minimap scrolls the **document viewport** with **its own residual accumulator**; click/drag remains scrub | **a FULL tick already scrolls today** — minimap pixels are `Elsewhere` (`main.rs:2061`) and the wheel falls through to `scroll_by_lines` (`main.rs:3373`). What fails is **fractional accumulation**, and **residual ownership distinct from the document's**: sub-tick minimap deltas are discarded, and a **surface-switch fractional witness** (part-tick over the minimap, then over the document) must not carry residue across | share the document's accumulator → the surface-switch fractional row jumps |
@ -322,6 +329,18 @@ blank**. The bound is *width − viewport*, saturating at zero for buffers
narrower than the viewport, and **the right-bound witness asserts the narrower than the viewport, and **the right-bound witness asserts the
final display column is still visible**. final display column is still visible**.
**Panel-replay consequence, ruled after §5a's 2026-08-20
re-measurement.** “Horizontal panel wheel” has three receiver outcomes,
not one. When terminal precedence selects child reporting it already
forwards `ScrollLeft` and `ScrollRight` as SGR codes 66/67. The local
terminal branch — selected by Shift, reporting-off or a scrolled-back
view — has no horizontal viewport and remains inert. **B1–B3 own the missing
document-panel leg**: fractional production/residuals in the GPU, the
lossless `PanelPointer` tick, and the daemon's window-targeted
`view_left` effect and clamp. This is a named deferral from panel replay,
whose source comment already assigned it here; it does not make the
prerequisite lane implement half of 1b early.
**Why B6 changed — and revision 5's reason was wrong.** Scrubbing on **Why B6 changed — and revision 5's reason was wrong.** Scrubbing on
wheel is not *impossible*: the wheel handler already reads the cached wheel is not *impossible*: the wheel handler already reads the cached
`state.pointer_pos` for surface routing (`main.rs:3337`), so an absolute `state.pointer_pos` for surface routing (`main.rs:3337`), so an absolute