From 4da3a3432bf504f247ee212185175e39aa8e61eb Mon Sep 17 00:00:00 2001 From: Levi Neuwirth Date: Wed, 12 Aug 2026 10:37:24 +0200 Subject: [PATCH] docs: P2 implemented --- framing revision 11 retracts revision 10's claim Revision 10 argued a route-classification transcript satisfied P2 because a route 'names its local effect'. The wheel falsifies it: a wheel route carries a delta, and whether that becomes a viewport update, a panel event, a terminal event or nothing at all depends on State. The route names the family; only running the body names the effect. Retracted rather than quietly amended, since it was an argument this document made and review overturned. Co-Authored-By: Claude Opus 5 Claude-Session: https://claude.ai/code/session_016bqGA6s9tTUFzYpbeW3tai --- docs/active-work.md | 43 +++++++++++++++++--- docs/gui-stage1-input-framing.md | 69 +++++++++++++++++++++++++------- 2 files changed, 92 insertions(+), 20 deletions(-) diff --git a/docs/active-work.md b/docs/active-work.md index 0f00ab4..80962b3 100644 --- a/docs/active-work.md +++ b/docs/active-work.md @@ -260,12 +260,13 @@ waits for a signal that is not coming. Stage 0 merge, #236). **`githubsucks/gui-stage1-pre` is the authoritative tip** — the ref, not a SHA. Recover with `git fetch githubsucks && git checkout gui-stage1-pre`. -- **Framing `docs/gui-stage1-input-framing.md`, revision 10, APPROVED** +- **Framing `docs/gui-stage1-input-framing.md`, revision 11, APPROVED** after **eight rejected revisions**. Revision 9 is the approved design; - **revision 10 changes none of it** and records one scope correction - found against this implementation (below). It is Stage 1's framing for - **all** slices and governs the later branches; only Stage 0 was framed - by the arc document itself. + revision 10 recorded a scope correction found against this + implementation and **also argued P2 was satisfied by classification + alone, which review overturned — revision 11 retracts it**. It is + Stage 1's framing for **all** slices and governs the later branches; + only Stage 0 was framed by the arc document itself. - **Scope of THIS branch: 1-pre only — the input seam. No behaviour change.** `App::window_event` was **655 lines** and is now **33**: one `route_event` call and one arm per route. Nothing below it could be @@ -274,7 +275,37 @@ waits for a signal that is not coming. - **IMPLEMENTED in four commits, one per event family**, so each lands with its own witnesses and mutations rather than as one 600-line diff: `014110f` lifecycle (close / modifiers / resize), `7f0f9db` - redraw, `0705564` keyboard, `e955645` the four pointer arms. + redraw, `0705564` keyboard, `e955645` the four pointer arms. Review + round 1 added `f976dc1`, the P2 effect harness. +- **P2 HAS TWO HARNESSES, and the second was review round 1's blocker.** + The routing harness answers *where did this event go*; `EffectHarness` + answers *what did it do*. Classification alone could not satisfy P2 — + **a wheel route carries a delta, and whether that becomes a viewport + update, a panel event, a terminal event or nothing depends on + `State`.** The effect harness drives a real `AttachClient` over a + `socketpair` (real handshake, outbox, writer thread and encoder, so + the transcript is the wire), a real windowless `State`, and + `App::dispatch_window_event`. +- **`App::dispatch_window_event` is what made P2 reachable.** Left inside + `window_event`, the dispatch would force the harness to re-implement + it, and a harness that re-implements what it tests witnesses its own + copy. `window_event` is now **four lines**, so **P3 shrinks from a + 33-line match to a single `if`**. +- **Steps are delimited by a non-coalesceable sentinel key, not a + sleep** — otherwise "this step sent nothing" is undecidable without + waiting, and a fixed-duration wait against a writer thread is exactly + the core-count assumption behind PR #235's CI red. +- **The effect rows never skip**: a missing wgpu adapter is an assertion + failure. M21 confirms all **nine** effect rows fail loudly while the + **thirteen** GPU-free routing rows stay green. +- **Three manufactured absences, all found by running the rows**, and + each the same shape: the harness withheld something production + supplies, then witnessed its own omission. `resumed` sets the frontend + id and session version before any geometry flush (the resize row); + the fixture document was two lines and could not scroll; a headless + `State` has no attached buffer, so `scroll_by_lines` returned `None`. + A fourth was a vacuous assertion — `.all(|e| matches!(..))` over an + empty transcript is true — caught by the outbound-blind mutation. - **The shape.** Deciding is `route_event(&WindowEvent) -> Route`, a free function composing one decision function per family (`route_lifecycle`, `route_keyboard` + `route_key_action`, diff --git a/docs/gui-stage1-input-framing.md b/docs/gui-stage1-input-framing.md index 6791261..45f48d7 100644 --- a/docs/gui-stage1-input-framing.md +++ b/docs/gui-stage1-input-framing.md @@ -1,10 +1,11 @@ # GUI arc, Stage 1 — input foundation (framing) -**Status: revision 10 — APPROVED.** Revisions 1–8 rejected; revision 9 -is the approved design and **revision 10 changes none of it** — it -records one scope correction found against the 1-pre implementation -(§6, "Revision 10"). **Q#S1-8, Q#S1-9 and Q#S1-10 are RULED.** -**1-pre is IMPLEMENTED**; 1a onward may begin from this document. +**Status: revision 11 — APPROVED.** Revisions 1–8 rejected; revision 9 +is the approved design. Revision 10 recorded a scope correction found +against the 1-pre implementation and **also made a claim about P2 that +review overturned; revision 11 retracts it and P2 is implemented as +written** (§6). **Q#S1-8, Q#S1-9 and Q#S1-10 are RULED.** **1-pre is +IMPLEMENTED**; 1a onward may begin from this document. **Verification base:** checked in the `gui-arc-stage0` worktree at `a994f37`, whose tree for these files is what `f8ad3e7` merged. @@ -121,7 +122,9 @@ P3 remains an accepted structural exception: not headlessly testable. **Revision 10 — one finding against the implementation, not the design.** The 1-pre seam is built and the table above holds, with one -scope correction that could not be seen from the design. +scope correction that could not be seen from the design. *(Revision 10 +also argued P2 was satisfied by classification alone. It is not — see +revision 11 at the end of this section.)* **P1 has a SECOND structural exception, and it is winit's rather than this seam's.** `KeyEvent` carries a `pub(crate) platform_specific` @@ -147,15 +150,53 @@ blanket one: body with `let _ = (event_loop, event);` — a GUI that responds to no input at all — leaves **all 256 `pmacs-gpu` tests green**, not merely the 13 routing rows. That is the exception's true extent: no headless - test anywhere in the crate observes the delegation. + test anywhere in the crate observes the delegation. *(Revision 11 + shrinks what the exception covers: `window_event` is now four lines, + so the unwitnessed residue is one `if` rather than a 33-line match.)* -**P2's harness records ROUTES, and that is the mechanism rather than a -narrowing.** A route names its local effect — `Exit`, `Redraw`, -`Resize { width, height }`, `Modifiers(state)` — so one transcript -covers both halves of P2's contract. The transcript row is deliberately -the **sole** owner of P2 (the per-variant rows call `route_event` -directly), which is what keeps "record outbound only" failing exactly -one row instead of every row. +**Revision 11 — P2 IS IMPLEMENTED AS WRITTEN. Revision 10's argument +here was wrong and is retracted.** + +Revision 10 claimed a route-classification transcript covered both +halves of P2 because a route "names its local effect". **The wheel +falsifies that.** A wheel route carries a delta; whether that delta +becomes a viewport update, a panel event, a terminal event or nothing at +all depends on `State`. The route names the *family*, and only running +the body names the *effect* — so classification could not have +satisfied P2, and arguing that it did was a narrowing wearing the +costume of a mechanism. + +P2 now has a second harness beside the routing one: + +- **`EffectHarness` drives production end to end** — a real + `AttachClient` over a `socketpair` (real handshake, outbox, writer + thread, encoder, so the transcript is the wire), a real windowless + `State`, and `App::dispatch_window_event`. +- **`App::dispatch_window_event` is what made this reachable.** Left + inside `window_event`, the dispatch would force a harness to + re-implement it, and a harness that re-implements what it tests + witnesses its own copy. **P3 therefore narrows from a 33-line match to + a single `if`**: `window_event` is now `call dispatch, exit if it + asks`. +- **Local effects are read where they land**: exit from the returned + `EventOutcome`, redraw from a test-only `render_calls`, resize from + the surface config, modifiers from `App`, scroll from `scroll_top`. +- **Steps are delimited by a non-coalesceable sentinel key, not a + sleep** — "this step sent nothing" is otherwise undecidable without + waiting, and a fixed-duration wait against a writer thread is the + core-count assumption of PR #235's CI red. +- **The rows never skip.** A missing wgpu adapter is an assertion + failure; mutation M21 confirms all nine effect rows fail loudly while + the thirteen GPU-free routing rows stay green. + +`M22` (blind to outbound) and `M23` (blind to local) fail rows in both +directions, which is P2's contract executable rather than asserted. + +The routing rows stay, and the division of labour is deliberate: the +routing harness answers *where did this event go*, the effect harness +answers *what did it do*. The transcript row remains the routing +harness's sole P2-recording owner, which keeps its own mutation +surgical. **One design consequence worth carrying into 1a.** The keyboard arm was the second caller of `event_loop.exit()` — the idle-Escape local quit —