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 <noreply@anthropic.com> Claude-Session: https://claude.ai/code/session_016bqGA6s9tTUFzYpbeW3tai
This commit is contained in:
parent
f976dc1042
commit
4da3a3432b
|
|
@ -260,12 +260,13 @@ waits for a signal that is not coming.
|
||||||
Stage 0 merge, #236). **`githubsucks/gui-stage1-pre` is the
|
Stage 0 merge, #236). **`githubsucks/gui-stage1-pre` is the
|
||||||
authoritative tip** — the ref, not a SHA. Recover with
|
authoritative tip** — the ref, not a SHA. Recover with
|
||||||
`git fetch githubsucks && git checkout gui-stage1-pre`.
|
`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;
|
after **eight rejected revisions**. Revision 9 is the approved design;
|
||||||
**revision 10 changes none of it** and records one scope correction
|
revision 10 recorded a scope correction found against this
|
||||||
found against this implementation (below). It is Stage 1's framing for
|
implementation and **also argued P2 was satisfied by classification
|
||||||
**all** slices and governs the later branches; only Stage 0 was framed
|
alone, which review overturned — revision 11 retracts it**. It is
|
||||||
by the arc document itself.
|
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
|
- **Scope of THIS branch: 1-pre only — the input seam. No behaviour
|
||||||
change.** `App::window_event` was **655 lines** and is now **33**: one
|
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
|
`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
|
- **IMPLEMENTED in four commits, one per event family**, so each lands
|
||||||
with its own witnesses and mutations rather than as one 600-line
|
with its own witnesses and mutations rather than as one 600-line
|
||||||
diff: `014110f` lifecycle (close / modifiers / resize), `7f0f9db`
|
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
|
- **The shape.** Deciding is `route_event(&WindowEvent) -> Route`, a
|
||||||
free function composing one decision function per family
|
free function composing one decision function per family
|
||||||
(`route_lifecycle`, `route_keyboard` + `route_key_action`,
|
(`route_lifecycle`, `route_keyboard` + `route_key_action`,
|
||||||
|
|
|
||||||
|
|
@ -1,10 +1,11 @@
|
||||||
# GUI arc, Stage 1 — input foundation (framing)
|
# GUI arc, Stage 1 — input foundation (framing)
|
||||||
|
|
||||||
**Status: revision 10 — APPROVED.** Revisions 1–8 rejected; revision 9
|
**Status: revision 11 — APPROVED.** Revisions 1–8 rejected; revision 9
|
||||||
is the approved design and **revision 10 changes none of it** — it
|
is the approved design. Revision 10 recorded a scope correction found
|
||||||
records one scope correction found against the 1-pre implementation
|
against the 1-pre implementation and **also made a claim about P2 that
|
||||||
(§6, "Revision 10"). **Q#S1-8, Q#S1-9 and Q#S1-10 are RULED.**
|
review overturned; revision 11 retracts it and P2 is implemented as
|
||||||
**1-pre is IMPLEMENTED**; 1a onward may begin from this document.
|
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
|
**Verification base:** checked in the `gui-arc-stage0` worktree at
|
||||||
`a994f37`, whose tree for these files is what `f8ad3e7` merged.
|
`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
|
**Revision 10 — one finding against the implementation, not the
|
||||||
design.** The 1-pre seam is built and the table above holds, with one
|
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
|
**P1 has a SECOND structural exception, and it is winit's rather than
|
||||||
this seam's.** `KeyEvent` carries a `pub(crate) platform_specific`
|
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
|
body with `let _ = (event_loop, event);` — a GUI that responds to no
|
||||||
input at all — leaves **all 256 `pmacs-gpu` tests green**, not merely
|
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
|
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
|
**Revision 11 — P2 IS IMPLEMENTED AS WRITTEN. Revision 10's argument
|
||||||
narrowing.** A route names its local effect — `Exit`, `Redraw`,
|
here was wrong and is retracted.**
|
||||||
`Resize { width, height }`, `Modifiers(state)` — so one transcript
|
|
||||||
covers both halves of P2's contract. The transcript row is deliberately
|
Revision 10 claimed a route-classification transcript covered both
|
||||||
the **sole** owner of P2 (the per-variant rows call `route_event`
|
halves of P2 because a route "names its local effect". **The wheel
|
||||||
directly), which is what keeps "record outbound only" failing exactly
|
falsifies that.** A wheel route carries a delta; whether that delta
|
||||||
one row instead of every row.
|
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
|
**One design consequence worth carrying into 1a.** The keyboard arm was
|
||||||
the second caller of `event_loop.exit()` — the idle-Escape local quit —
|
the second caller of `event_loop.exit()` — the idle-Escape local quit —
|
||||||
|
|
|
||||||
Loading…
Reference in New Issue