docs(framing): bottom-panel revision 12 --- the passive precondition, and two assertions that are not interchangeable

Answers review of revision 11. Still framing only; no implementation.

**"FOCUS UNCHANGED" IS VACUOUS IF THE PANEL IS ALREADY FOCUSED.** With
the terminal side window active, the below-activation mutation calls
`focus_window` on the window that is ALREADY active --- nothing
changes, and the row stays green against the exact bug it exists to
catch. I added the assertion in revision 11 and did not give it a state
in which it could fail.

Leg 2 now starts passive, and says so as assertions rather than setup:
the primary document window is active, the terminal side window is
distinct from it and passive, and the terminal controller identity is
captured as a baseline. Asserted rather than arranged, because each is
the kind of detail a later edit changes silently, and each failure mode
is a witness that passes while proving nothing.

**AND THE TWO ASSERTIONS ARE NOT INTERCHANGEABLE**, which revision 11's
prose blurred by naming them together as though either would do:

  consume check below activation
      -> `focus_window` runs, the panel takes focus, and NOTHING
         scrolls, so every movement assertion still passes
      -> caught by FOCUS, and focus alone

  terminal branch calls `apply_terminal_gesture`
      -> `claims_control` is `!matches!(kind, Move)` (`:3555`), so a
         wheel CLAIMS THE PANEL'S CONTROLLER at `:3571`, before any
         local handling at `:3575`; the chrome coordinate then fails
         the reporting bounds check and drops into the local branch,
         which may also move scrollback
      -> caught by CONTROLLER IDENTITY, plus scrollback when it moves

Activation alone claims nothing --- `focus_window` and
`claim_terminal_controller` are separate acts --- so a row asserting
only controller identity misses the ordering bug entirely, and one
asserting only focus misses a replay that quietly claims the terminal.

Gates: all nine green under `env -u TMPDIR`, log 20260814T144513Z.

Co-Authored-By: Claude Opus 5 <noreply@anthropic.com>
Claude-Session: https://claude.ai/code/session_016bqGA6s9tTUFzYpbeW3tai
This commit is contained in:
Levi Neuwirth 2026-08-14 16:49:54 +02:00
parent 112fcf593f
commit 78e5bec2d4
No known key found for this signature in database
2 changed files with 59 additions and 15 deletions

View File

@ -281,7 +281,7 @@ 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 11 (§5a) AWAITING APPROVAL; - **No PR yet. Checkpoint: framing revision 12 (§5a) AWAITING APPROVAL;
NO IMPLEMENTATION WRITTEN.** Commit one was the ground-truth NO IMPLEMENTATION WRITTEN.** Commit one was the ground-truth
re-measurement; 6 added the four replay edges; **7 answers review of re-measurement; 6 added the four replay edges; **7 answers review of
6; **8 answers review of 7** — R-c is target × gesture-ORIGIN 6; **8 answers review of 7** — R-c is target × gesture-ORIGIN
@ -317,9 +317,17 @@ from #171 and #215 — the correction the 1b lane missed, honoured here.
and `active_frontend` at `:2699` ahead of any replay decision — a and `active_frontend` at `:2699` ahead of any replay decision — a
consume check below that would change focus while scrolling nothing consume check below that would change focus while scrolling nothing
and claiming no controller. Four-step order, consumption at step 3; and claiming no controller. Four-step order, consumption at step 3;
the witness now asserts **focus and controller identity unchanged**, the witness now asserts **focus and controller identity unchanged**.
which is what catches the consume-below-activation mutation, since **Revision 12** makes that setup discriminating: leg 2 must **start
that mutation moves nothing. PASSIVE** — primary document window active, terminal side window
distinct and passive, controller baseline captured — because "focus
unchanged" is vacuous if the panel is already focused, and the
below-activation mutation would then call `focus_window` on the
already-active window and pass. The two assertions are **not
interchangeable**: **focus** catches the ordering mutation;
**controller identity** catches the shared-path mutation, since
`apply_terminal_gesture` claims at `src/editor.rs:3571` before local
handling and activation alone claims nothing.
- **Why this lane exists.** `PanelPointer` **replays nothing**: - **Why this lane exists.** `PanelPointer` **replays nothing**:
`dispatch_semantic_panel_pointer` (`src/editor.rs:2674`) validates, `dispatch_semantic_panel_pointer` (`src/editor.rs:2674`) validates,
focuses, returns. A panel wheel is dead on both axes and so is every focuses, returns. A panel wheel is dead on both axes and so is every

View File

@ -7,7 +7,21 @@ 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 11 — 2026-08-14, AWAITING APPROVAL.** Answers review of 10. **Revision 12 — 2026-08-14, AWAITING APPROVAL.** Answers review of 11,
whose witness had a **vacuous precondition**.
"Focus unchanged" proves nothing if the terminal panel is **already
focused**: the below-activation mutation then calls `focus_window` on
the already-active side window, nothing changes, and the row passes.
Leg 2 must **start passive**, and assert it — primary document window
active, terminal side window distinct and passive, controller baseline
captured. The prose is also narrowed: **focus** catches the
below-activation ordering mutation; **controller identity** catches the
shared-path mutation, since `apply_terminal_gesture` claims the
controller at `src/editor.rs:3571` before local handling. Activation
alone claims nothing, so the two assertions are not interchangeable.
**Previously, revision 11 — SUPERSEDED.** Answered review of 10.
**The terminal-chrome wheel must be consumed BEFORE ACTIVATION**, not **The terminal-chrome wheel must be consumed BEFORE ACTIVATION**, not
merely before `apply_terminal_gesture`. `activates` is merely before `apply_terminal_gesture`. `activates` is
@ -2300,18 +2314,40 @@ the two outcomes are separated by nothing but the buffer kind:
no document scroll, **and the focused window and terminal controller no document scroll, **and the focused window and terminal controller
identity are unchanged**. identity are unchanged**.
Two mutations, biting different halves: ##### Leg 2 must START PASSIVE, or "focus unchanged" is vacuous
| mutation | must fail | **A focus assertion proves nothing if the panel already has focus.**
|---|---| With the terminal side window active, moving the consume check below
| the terminal branch calls `apply_terminal_gesture` | the chrome coordinate fails its reporting bounds check, drops into the local branch, and the row catches the **accidental local scrollback** revision 8's clamp would have shipped deliberately | activation calls `focus_window` on **the window that is already
| the consume check sits **below** the activation block | nothing scrolls, so bytes/scrollback/document all still pass — **only the focus and controller assertions catch it** | active** — nothing changes, and the row stays green against the very
mutation it exists to catch.
**The second mutation is why the focus and controller assertions are **Preconditions, asserted before the wheel, not merely arranged:**
load-bearing.** Without them the row is green against an
implementation that steals focus on every chrome wheel over a - the **primary document window is active**;
terminal — the half-state is invisible to any assertion about - the **terminal side window is distinct from it and PASSIVE**;
movement, because nothing moves either way. - the **terminal controller identity is captured as a baseline**.
Asserted rather than assumed, because each is exactly the kind of setup
detail a later edit silently changes — and each failure mode is a
witness that passes while proving nothing.
**With that setup the two mutations separate cleanly, and each is
caught by a DIFFERENT assertion:**
| mutation | what it does | caught by |
|---|---|---|
| the consume check sits **below** the activation block | `focus_window` runs and the panel takes focus; nothing scrolls, so every movement assertion still passes | **focus** — and focus alone |
| the terminal branch calls `apply_terminal_gesture` | `claims_control` is `!matches!(kind, Move)` (`src/editor.rs:3555`), so a wheel **claims the panel's controller at `:3571`, before any local handling** at `:3575`; the chrome coordinate then fails the reporting bounds check and drops into the local branch, which may also move scrollback | **controller identity** — plus scrollback when it moves |
**The two assertions are not interchangeable**, which revision 11's
prose blurred by naming them together. **Focus catches the ordering
mutation; controller identity catches the shared-path mutation.**
Activation alone does not claim a controller — `focus_window` and
`claim_terminal_controller` are separate acts — so a row asserting only
controller identity would miss the below-activation ordering bug
entirely, and one asserting only focus would miss a replay that quietly
claims the terminal.
Doing it in one frontend across a replacement is what makes it a Doing it in one frontend across a replacement is what makes it a
control rather than two unrelated observations: the geometry, the control rather than two unrelated observations: the geometry, the