From ba48ae6153c0f90adf240f1f607624e691817dec Mon Sep 17 00:00:00 2001 From: Levi Neuwirth Date: Thu, 20 Aug 2026 23:12:06 +0200 Subject: [PATCH] test(panel): P2's focus assertion was blocked by assertion order, not by the type Answers review of 557ea6d. Capturing the outcome and asserting it LAST makes the focus assertion reachable: removing the buffer check accepts the press, an accepted press activates the panel before it replays, and the row now fails on focus --- WindowId(3) against WindowId(2). I had recorded this as a limit of the type boundary, claiming no mutation could reach the effect assertions because the daemon applies only on Accepted and the disposition gives Refused no target. That was wrong. The obstacle was that the row asserted the refusal BEFORE dispatch and aborted there. Ordering, not architecture. The classification is still checked, at the end, so the row cannot go vacuous if it ever stops testing a refusal. Controller and byte assertions stay documented as defence in depth, and now for an accurate reason: the mutation that reaches them routes through a document buffer, which touches neither. Also replaces failure text that still described an out-of-range anchor, which this fixture stopped using when its refusal lever became a foreign buffer. Co-Authored-By: Claude Opus 5 (1M context) Claude-Session: https://claude.ai/code/session_016bqGA6s9tTUFzYpbeW3tai --- docs/active-work.md | 14 ++++++++---- src/daemon.rs | 52 ++++++++++++++++++++++++++++----------------- 2 files changed, 42 insertions(+), 24 deletions(-) diff --git a/docs/active-work.md b/docs/active-work.md index f8cfc9d..2a87a12 100644 --- a/docs/active-work.md +++ b/docs/active-work.md @@ -318,10 +318,16 @@ from #171 and #215 — the correction the 1b lane missed, honoured here. for a gesture that never began, so the record IS the artifact. Manufacturing an effect assertion for them would not distinguish their mutations. - **P2 is a third case**: its falsifiable claim is the - classification; its focus, controller and byte assertions are - defence in depth, because the precondition asserting `Refused` - fires first under the only mutation that would reach them. + **P2 is a third case**: its FOCUS assertion is witnessed — + removing the buffer check accepts the press, which activates the + panel before replaying — and its classification is checked LAST so + the row still fails if it stops testing a refusal. Only its + controller and byte assertions are defence in depth, because that + mutation routes through a document buffer and touches neither. An + earlier version asserted the refusal first, which aborted the row + before dispatch and made every effect assertion unreachable; I + recorded that ordering limit as a limit of the type boundary, and + it was not one. - **Every fixture asserts its own precondition** (the disposition is `Accepted`, or is `Refused`) because four rows in these rounds passed vacuously: cells that were out of grid, or that clamped to diff --git a/src/daemon.rs b/src/daemon.rs index 20a843a..776c032 100644 --- a/src/daemon.rs +++ b/src/daemon.rs @@ -8520,15 +8520,18 @@ mod tests { /// P2, effect half — a REFUSED press reaches no target at all. /// - /// **What is falsifiable here is the CLASSIFICATION.** Removing the - /// buffer check makes this press `Accepted`, and the row fails. The - /// focus, controller and byte assertions cannot fail under that - /// same mutation, because the precondition asserting `Refused` - /// fires first — and no other mutation reaches them, since the - /// daemon calls `apply_panel_pointer` only on `Accepted` and the - /// disposition enum gives `Refused` no target to apply. They are - /// **defence in depth against a future refactor**, kept and - /// labelled rather than presented as witnessed coverage. + /// **The FOCUS assertion is witnessed.** Removing the buffer check + /// makes this press `Accepted`; it then activates the panel before + /// replaying, and the focus assertion fails. An earlier version + /// asserted the refusal BEFORE dispatch, which aborted the row + /// first and made every effect assertion unreachable — a limit of + /// ordering that I mistook for a limit of the type boundary. The + /// classification is now checked LAST, so it still catches a row + /// that has stopped testing a refusal. + /// + /// The controller and byte assertions remain **defence in depth**: + /// the mutation that reaches them routes through a document buffer, + /// which touches neither. /// /// §5b's four `g5_substrate_a_refused_*` rows read the latch and the /// cancellation count; none of them reads the target. A refusal that @@ -8573,14 +8576,14 @@ mod tests { .terminal_manager .borrow() .controller_view_for_frontend(fid); - assert_eq!( - editor - .classify_panel_pointer(fid, foreign_buffer, in_content, press) - .outcome(), - crate::editor::PanelPointerOutcome::Refused, - "fixture: this press really is refused --- asserted, because \ - every effect assertion below is vacuous if it is not" - ); + // CAPTURED, not asserted yet. Asserting the refusal here aborted + // the row before dispatch, so the effect assertions below could + // never fail under the one mutation that reaches them. The + // precondition still runs --- at the END --- so the row cannot go + // vacuous either. + let observed_outcome = editor + .classify_panel_pointer(fid, foreign_buffer, in_content, press) + .outcome(); send_panel( &mut editor, @@ -8602,9 +8605,10 @@ mod tests { assert_eq!( editor.core.borrow().views[&fid].active, focused_before, - "and it must not FOCUS the panel: a misclassified press - focuses before its out-of-range anchor fails, so byte and \ - latch assertions alone stay green while focus has moved" + "and it must not FOCUS the panel: an accepted press \ + activates BEFORE it replays, so a misclassified one moves \ + focus to the panel whatever its replay then does with a \ + buffer that is not the one on screen" ); assert_eq!( editor @@ -8614,6 +8618,14 @@ mod tests { controller_before, "and it must not claim the terminal CONTROLLER" ); + assert_eq!( + observed_outcome, + crate::editor::PanelPointerOutcome::Refused, + "and the press really was refused --- checked LAST so that a \ + mutation which accepts it is caught by the effects above \ + rather than aborting the row here, while still failing if \ + this row ever stops testing a refusal at all" + ); assert!( !editor .terminal_manager