feat(panel): the wheel exemption, exhaustion, and mapped coalescing

Three rows that share a shape: each is a gate this slice owns whose
downstream EFFECT belongs to the rebased replay lane.

G10b --- ordering, and a carve-out. `panel_mapping_is_current` now takes
the event kind. Zero is refused FIRST, then coordinate-free wheels skip
the freshness comparison. The order is the row: run the carve-out first
and a sender emitting zeroed wheels faces no check at all, which is an
inbound opt-out through the exempt path. The exemption exists because a
tick changes `view_top` and so advances the key --- the next tick already
queued behind it echoes the previous generation, and without the
carve-out the panel scrolls once per frame and appears dead. It returns
before the read, so a wheel does not advance the key either; advancing
would make a wheel invalidate the press after it.

The framing's carve-out-to-the-carve-out, re-imposing the check for
CHILD-REPORTED terminal wheels where SGR carries row and column, is
replay's. Whether a wheel is forwarded is decided by the reporting mode,
and no panel pointer coordinate is consumed on this base at all.

G11a --- exhaustion fails CLOSED. `saturating_add` froze the key at the
ceiling while the mapping kept moving underneath it: the stale-gesture
hole the key exists to close, with the check still appearing to pass.
Now `checked_add`, and overflow publishes `Absent`, clears input
authority, and latches for the session.

G13a/G13b --- `PanelPointerMapped` fell through `coalesce_kind` to
`None`, so pixel-rate mapped motion was lossless and filled the bounded
outbox. Two tags of its own; tail-replacement takes the whole event, so
coordinate and generation advance together and a collapsed run can never
pair a new coordinate with a stale one. Press, release and every wheel
kind stay lossless.

Mutation results, including two that changed the design:

  - exemption before the nonzero check -> G10b(zero) alone
  - no wheel exemption -> G10b(exemption) alone
  - saturating instead of checked add -> G11a alone
  - no exhaustion latch -> G11a, but only AFTER the row was extended.
    The first version of G11a did not bite: the latch had no proven
    job, because the overflow path already returns before storing the
    ceiling snapshot, so the next read re-takes the changed arm anyway.
    Measured, the two are ALTERNATIVES --- either alone keeps the band
    down; only removing both resurrects it. The latch is kept as the
    primary because it has a job the ordering does not: `peek` now
    honours it, so the peek and the authoritative read agree that an
    exhausted session has no key rather than reporting the ceiling.
    The source comment says this, rather than the "second half" claim
    it made before the measurement.
  - mapped variants untagged / one tag for all kinds / sharing the
    legacy tags -> the mapped coalescing row alone, three times

Witness-shape note: the two G10b rows call the predicate directly, and
say why. A wheel has no dispatcher-visible effect on this base --- a
document panel focuses on `Down` only --- so asserting focus for a wheel
would prove nothing. Each row carries a press leg, which does have an
effect, to show the predicate is wired into the production arm.

Verified: `cargo fmt --check`; `cargo clippy --workspace --all-targets
-- -D warnings`; `cargo test --lib` (1959); `cargo test -p pmacs-gpu
--bins` (275); both `bottom_panel_stage2b_*` suites (39); `git diff
--check`. `composition_overhead_under_ten_percent` red once during this
work and green in isolation --- a second occurrence of a signature the
lane ledger already carries, now recorded there.

Co-Authored-By: Claude Opus 5 (1M context) <noreply@anthropic.com>
Claude-Session: https://claude.ai/code/session_016bqGA6s9tTUFzYpbeW3tai
This commit is contained in:
Levi Neuwirth 2026-08-15 22:56:42 +02:00
parent 8c5ca10698
commit a8a996c446
No known key found for this signature in database
4 changed files with 519 additions and 13 deletions

View File

@ -461,6 +461,10 @@ from #171 and #215.
live-process race under sweep load. Isolated rerun green. **Not in live-process race under sweep load. Isolated rerun green. **Not in
the registry under any id**, so it is a new signature, owed like the registry under any id**, so it is a new signature, owed like
the two above. the two above.
- **`composition_overhead_under_ten_percent`, a SECOND time**
(2026-08-15, plain `cargo test --lib`, not a gate step). Isolated
rerun green. Same budget as the occurrence above, now seen in two
different selectors on one branch in one day.
- **Three consecutive full-gate runs, three DIFFERENT unrelated - **Three consecutive full-gate runs, three DIFFERENT unrelated
failures** (composition budget in `04-lib-crdt`, then composition failures** (composition budget in `04-lib-crdt`, then composition
again in `10-sweep-crdt`, then this in `08-sweep`), against a diff again in `10-sweep-crdt`, then this in `08-sweep`), against a diff

View File

@ -379,6 +379,28 @@ fn coalesce_kind(event: &FrontendEvent) -> Option<u8> {
kind: MouseKind::Drag(_), kind: MouseKind::Drag(_),
.. ..
} => Some(7), } => Some(7),
// §5b G13a — the v25 mapped family needs its OWN tags. Falling
// through to `None` would make pixel-rate mapped motion lossless
// and fill the bounded queue, which is `OUTBOX_MAX` events of
// hover before the socket closes.
//
// Tail-replacement takes the whole newer event, so the surviving
// event carries the latest coordinate AND the latest
// `mapping_generation` together — a collapsed run can never pair
// a new coordinate with a stale generation.
//
// Distinct from the legacy tags 6/7 rather than shared with
// them. A session negotiates one family and never mixes the two,
// so sharing would buy nothing and would let a family confusion
// collapse silently instead of showing up as two queued events.
FrontendEvent::PanelPointerMapped {
kind: MouseKind::Move,
..
} => Some(8),
FrontendEvent::PanelPointerMapped {
kind: MouseKind::Drag(_),
..
} => Some(9),
_ => None, _ => None,
} }
} }
@ -1482,6 +1504,115 @@ mod tests {
} }
} }
fn fe_panel_mapped(kind: MouseKind, row: u32, col: u32, generation: u64) -> FrontendEvent {
FrontendEvent::PanelPointerMapped {
frontend_id: FrontendId(1),
buffer_id: BufferId::from_raw(1),
coord: CellCoord::new(row, col),
kind,
mods: Modifiers::NONE,
geometry_epoch: 1,
panel_epoch: 1,
mapping_generation: generation,
}
}
/// §5b G13a/G13b — the mapped family keeps the legacy family's
/// coalescing contract: `Move` and `Drag` collapse to the latest
/// coordinate AND generation together; press, release and every
/// wheel kind stay lossless and ordered.
#[test]
fn mapped_panel_motion_coalesces_carrying_its_latest_generation() {
let mut ob = Outbox::new();
ob.enqueue(fe_panel_mapped(MouseKind::Down(MouseButton::Left), 0, 0, 4));
ob.enqueue(fe_panel_mapped(MouseKind::Drag(MouseButton::Left), 0, 1, 4));
ob.enqueue(fe_panel_mapped(MouseKind::Drag(MouseButton::Left), 0, 2, 5));
ob.enqueue(fe_panel_mapped(MouseKind::Drag(MouseButton::Left), 0, 3, 6));
ob.enqueue(fe_panel_mapped(MouseKind::Up(MouseButton::Left), 0, 3, 6));
assert_eq!(
ob.queue.len(),
3,
"the drag run collapsed to one; without a tag of its own the \
mapped family is lossless and this is five"
);
// The whole event is replaced, so coordinate and generation
// advance TOGETHER. A tag that replaced only the coordinate
// would leave generation 4 on a cell measured under 6, which the
// daemon then refuses as stale.
assert!(
matches!(
&ob.queue[1],
FrontendEvent::PanelPointerMapped {
kind: MouseKind::Drag(MouseButton::Left),
coord: CellCoord { row: 0, col: 3 },
mapping_generation: 6,
..
}
),
"surviving drag: {:?}",
&ob.queue[1]
);
// G13b — wheel ticks carry scroll DISTANCE. Two ticks in one
// generation must both survive the queue, or the panel scrolls
// once and stops.
let mut wheel = Outbox::new();
wheel.enqueue(fe_panel_mapped(MouseKind::ScrollUp, 1, 1, 7));
wheel.enqueue(fe_panel_mapped(MouseKind::ScrollUp, 1, 1, 7));
wheel.enqueue(fe_panel_mapped(MouseKind::ScrollDown, 1, 1, 7));
wheel.enqueue(fe_panel_mapped(MouseKind::ScrollLeft, 1, 1, 7));
wheel.enqueue(fe_panel_mapped(MouseKind::ScrollRight, 1, 1, 7));
assert_eq!(wheel.queue.len(), 5, "every wheel kind stays lossless");
// Repeated presses are what the daemon reads as a multi-click,
// and a right press is the context gesture.
let mut presses = Outbox::new();
presses.enqueue(fe_panel_mapped(MouseKind::Down(MouseButton::Left), 2, 2, 8));
presses.enqueue(fe_panel_mapped(MouseKind::Down(MouseButton::Left), 2, 2, 8));
presses.enqueue(fe_panel_mapped(
MouseKind::Down(MouseButton::Right),
2,
2,
8,
));
assert_eq!(presses.queue.len(), 3, "presses stay lossless");
// Motion does not collapse ACROSS an intervening lossless event.
let mut mixed = Outbox::new();
mixed.enqueue(fe_panel_mapped(MouseKind::Move, 3, 1, 9));
mixed.enqueue(fe_panel_mapped(MouseKind::Move, 3, 2, 9));
assert_eq!(mixed.queue.len(), 1);
mixed.enqueue(fe_panel_mapped(MouseKind::ScrollDown, 3, 2, 9));
mixed.enqueue(fe_panel_mapped(MouseKind::Move, 3, 3, 9));
assert_eq!(
mixed.queue.len(),
3,
"the wheel tick between them must not be jumped"
);
// And Move does not fold into a Drag tail: they are separate
// gestures, and one tag for both would turn a hover into part of
// a selection.
let mut kinds = Outbox::new();
kinds.enqueue(fe_panel_mapped(MouseKind::Drag(MouseButton::Left), 4, 1, 9));
kinds.enqueue(fe_panel_mapped(MouseKind::Move, 4, 2, 9));
assert_eq!(kinds.queue.len(), 2);
// The two FAMILIES do not coalesce into each other either.
let mut families = Outbox::new();
families.enqueue(FrontendEvent::PanelPointer {
frontend_id: FrontendId(1),
buffer_id: BufferId::from_raw(1),
coord: CellCoord::new(5, 1),
kind: MouseKind::Move,
mods: Modifiers::NONE,
geometry_epoch: 1,
panel_epoch: 1,
});
families.enqueue(fe_panel_mapped(MouseKind::Move, 5, 2, 9));
assert_eq!(families.queue.len(), 2);
}
/// Acceptance 34: terminal move/drag runs coalesce to the latest /// Acceptance 34: terminal move/drag runs coalesce to the latest
/// cell, while press, release, and wheel stay lossless and ordered. /// cell, while press, release, and wheel stay lossless and ordered.
#[test] #[test]

View File

@ -1088,9 +1088,29 @@ fn peer_uses_mapped_panel_family(session_registry: &SessionRegistry, source: Fro
/// changing** — a foreign edit, a fold, a reload, none of which moves /// changing** — a foreign edit, a fold, a reload, none of which moves
/// an epoch. /// an epoch.
/// ///
/// **Zero is refused outright.** It is what a default-constructed or /// **Zero is refused outright, and BEFORE the wheel exemption.** Zero is
/// half-initialised sender produces, so accepting it would let a peer /// what a default-constructed or half-initialised sender produces, so
/// opt out of the check by sending nothing. /// accepting it would let a peer opt out of the check by sending
/// nothing. Ordering the exemption first would reopen that opt-out
/// through the exempt path: a sender emitting zeroed wheels would face
/// no check at all (G10b).
///
/// **Coordinate-free wheels are then EXEMPT from the freshness
/// comparison.** A wheel tick changes `view_top`, which advances the
/// key; the next tick already queued behind it echoes the previous
/// generation and would be refused, so the panel would scroll exactly
/// once per frame and appear dead. The exemption is safe because the
/// coordinate is not what a wheel means — the tick is. It returns
/// before the read, so a wheel does not advance the key either;
/// advancing would make the wheel invalidate the press after it.
///
/// The carve-out the framing states for **child-reported** terminal
/// wheels, where SGR does carry row and column, is
/// `panel-pointer-replay`'s. Whether a wheel is forwarded to a child is
/// decided by the reporting mode, and no panel pointer coordinate is
/// consumed on this base at all — `dispatch_semantic_panel_pointer`
/// bounds-checks and routes focus. Re-imposing the check belongs in the
/// branch that introduces the forwarding it protects.
/// ///
/// Read through the SAME accessor projection stamps with, so "what the /// Read through the SAME accessor projection stamps with, so "what the
/// frontend was shown" and "what the daemon checks" cannot drift. /// frontend was shown" and "what the daemon checks" cannot drift.
@ -1098,11 +1118,22 @@ fn panel_mapping_is_current(
editor: &EditorState, editor: &EditorState,
semantic_states: &mut HashMap<FrontendId, crate::semantic_render::SemanticRenderState>, semantic_states: &mut HashMap<FrontendId, crate::semantic_render::SemanticRenderState>,
source: FrontendId, source: FrontendId,
kind: pmacs_protocol::MouseKind,
echoed: u64, echoed: u64,
) -> bool { ) -> bool {
// ORDER IS LOAD-BEARING: nonzero first, exemption second.
if echoed == 0 { if echoed == 0 {
return false; return false;
} }
if matches!(
kind,
pmacs_protocol::MouseKind::ScrollUp
| pmacs_protocol::MouseKind::ScrollDown
| pmacs_protocol::MouseKind::ScrollLeft
| pmacs_protocol::MouseKind::ScrollRight
) {
return true;
}
let snapshot = editor.panel_mapping_snapshot(source); let snapshot = editor.panel_mapping_snapshot(source);
semantic_states semantic_states
.get_mut(&source) .get_mut(&source)
@ -2602,6 +2633,7 @@ fn handle_dispatcher_event(
editor, editor,
semantic_states, semantic_states,
source, source,
kind,
mapping_generation, mapping_generation,
) )
{ {
@ -6438,6 +6470,22 @@ mod tests {
) )
} }
/// An edit this frontend did NOT make: the case `view_top` cannot
/// catch, because nothing about the frontend's own state moves.
fn foreign_edit(
editor: &crate::editor::EditorState,
buffer_id: crate::buffer::BufferId,
text: &[u8],
) {
let core = editor.core.borrow();
let registry = core.registry.clone();
let mut reg = registry.borrow_mut();
reg.get_mut(buffer_id)
.expect("the panel's buffer")
.set_generated_contents(text)
.expect("a generated-contents write is a plain content change");
}
/// The mapping generation this session's producer most recently /// The mapping generation this session's producer most recently
/// stamped, which a mapped gesture must echo. /// stamped, which a mapped gesture must echo.
fn stamped_generation( fn stamped_generation(
@ -6733,6 +6781,276 @@ mod tests {
); );
} }
/// §5b G10b — **zero is refused BEFORE the wheel exemption**.
///
/// The ordering is the row. Zero is what a sender that never
/// initialised the field produces; the exemption is a liveness
/// carve-out for coordinate-free wheels. Run the carve-out first and
/// a zeroed wheel faces no check at all — an inbound opt-out through
/// the exempt path.
///
/// The predicate is called directly because a wheel has **no
/// dispatcher-visible effect on this base**: a document panel
/// focuses on `Down` only, and no panel pointer coordinate is
/// consumed anywhere, so an accepted wheel and a refused one are
/// indistinguishable downstream. Asserting focus for a wheel would
/// be a witness that proves nothing. The end-to-end leg below uses a
/// press, which does have an effect, so the predicate is shown to be
/// wired into the production arm rather than merely correct in
/// isolation.
#[test]
fn g10b_generation_zero_is_refused_before_the_wheel_exemption_applies() {
use pmacs_protocol::{MouseButton, MouseKind};
let fid = FrontendId(774);
let (mut editor, mut semantic_states, mut render, _document, panel, epochs) =
panel_session_at(PROTOCOL_VERSION, fid);
let buffer_id = editor.core.borrow().windows[&panel].buffer_id;
let generation = stamped_generation(&semantic_states, fid);
// The exempt kind with an INVALID generation: refused.
assert!(
!panel_mapping_is_current(&editor, &mut semantic_states, fid, MouseKind::ScrollDown, 0),
"a zeroed wheel is refused: the exemption must not run first"
);
// A non-exempt kind with the same zero: also refused, so the
// above is the zero and not the kind.
assert!(!panel_mapping_is_current(
&editor,
&mut semantic_states,
fid,
MouseKind::Down(MouseButton::Left),
0
));
// POSITIVE CONTROL — the same wheel with a real generation
// passes, so the refusal is not a dead predicate.
assert!(
panel_mapping_is_current(
&editor,
&mut semantic_states,
fid,
MouseKind::ScrollDown,
generation
),
"a wheel with a real generation passes"
);
// And the predicate is WIRED: a press is the kind whose
// acceptance is visible, so it carries the end-to-end leg.
let baseline = editor.core.borrow().views[&fid].active;
assert_ne!(
baseline, panel,
"fixture: the panel must NOT already be focused, or the \
refusal below is indistinguishable from acceptance"
);
dispatch_panel_event(
&mut editor,
fid,
PROTOCOL_VERSION,
&mut semantic_states,
&mut render,
mapped_pointer(fid, epochs, buffer_id, 0),
);
assert_eq!(
editor.core.borrow().views[&fid].active,
baseline,
"a zeroed press never reaches the focus path"
);
dispatch_panel_event(
&mut editor,
fid,
PROTOCOL_VERSION,
&mut semantic_states,
&mut render,
mapped_pointer(fid, epochs, buffer_id, generation),
);
assert_eq!(
editor.core.borrow().views[&fid].active,
panel,
"and a real one does"
);
}
/// §5b G10b — a coordinate-free wheel is EXEMPT from the freshness
/// comparison, so a second queued tick is not refused.
///
/// Only the GATE is proven here. The framing's G12 — that both ticks
/// apply their scrolls — is `panel-pointer-replay`'s, because no
/// panel wheel moves a view on this base. What this pins is that the
/// second tick is not refused, which is the half that would
/// otherwise make G12 unreachable.
///
/// The exemption must also NOT advance the key. Returning early
/// before the read is what gives that; advancing on a wheel would
/// make the wheel invalidate the press that follows it.
#[test]
fn g10b_a_stale_generation_on_a_wheel_is_exempt_but_fatal_on_a_press() {
use pmacs_protocol::{MouseButton, MouseKind};
let fid = FrontendId(775);
let (editor, mut semantic_states, _render, _document, panel, _epochs) =
panel_session_at(PROTOCOL_VERSION, fid);
let buffer_id = editor.core.borrow().windows[&panel].buffer_id;
let stale = stamped_generation(&semantic_states, fid);
// Move the mapping, so `stale` now names a mapping that is gone —
// exactly the state the first of two queued ticks leaves behind.
foreign_edit(&editor, buffer_id, b"moved\n");
// The wheel FIRST, while the key has not yet been re-read: the
// exempt path must neither compare nor advance.
let before = semantic_states[&fid]
.panel_mapping_generation_peek()
.expect("a stamped key");
assert!(
panel_mapping_is_current(
&editor,
&mut semantic_states,
fid,
MouseKind::ScrollDown,
stale
),
"the second queued tick still lands — without the exemption \
the first tick advances the key and the panel scrolls once \
and dies"
);
assert_eq!(
semantic_states[&fid].panel_mapping_generation_peek(),
Some(before),
"and the exempt path does not advance the key: a wheel that \
advanced it would invalidate the press that follows"
);
// NEGATIVE CONTROL — a press echoing the SAME stale value is
// refused, so the acceptance above is the exemption and not a
// check that never fires.
assert!(
!panel_mapping_is_current(
&editor,
&mut semantic_states,
fid,
MouseKind::Down(MouseButton::Left),
stale
),
"a press against a stale mapping is refused"
);
// Every coordinate-free wheel kind is exempt, not just the two
// vertical ones.
for kind in [
MouseKind::ScrollUp,
MouseKind::ScrollDown,
MouseKind::ScrollLeft,
MouseKind::ScrollRight,
] {
assert!(
panel_mapping_is_current(&editor, &mut semantic_states, fid, kind, stale),
"{kind:?} is coordinate-free and exempt"
);
}
}
/// §5b G11a — **exhaustion fails CLOSED and does not leave a zombie
/// band**.
///
/// Three obligations, and each has its own failure: publish
/// `Absent`, clear input authority, and LATCH so the next frame
/// cannot resurrect the band.
#[test]
fn g11a_generation_exhaustion_publishes_absent_and_latches_for_the_session() {
let fid = FrontendId(776);
let (mut editor, mut semantic_states, mut render, _document, panel, epochs) =
panel_session_at(PROTOCOL_VERSION, fid);
let buffer_id = editor.core.borrow().windows[&panel].buffer_id;
// Precondition: a live band, and a gesture the exhaustion must
// not silently strand.
assert!(
matches!(
semantic_states[&fid].last_panel_payload_for_test(),
Some(pmacs_protocol::PanelFramePayload::PresentMapped { .. })
),
"fixture: the band is live and mapped"
);
// Park the key one below the ceiling against the CURRENT
// snapshot, so the next mapping change is the advance that
// overflows. Seeding the snapshot too keeps the "unchanged" arm
// from firing instead.
let snapshot = editor
.panel_mapping_snapshot(fid)
.expect("a presentable mapping");
semantic_states
.get_mut(&fid)
.expect("projection")
.seed_panel_mapping_generation_for_test(snapshot, u64::MAX);
foreign_edit(&editor, buffer_id, b"one edit too many\n");
let messages = semantic_states
.get_mut(&fid)
.expect("projection")
.render_frame(&editor);
assert!(
messages.iter().any(|msg| matches!(
msg,
InstanceMessage::PanelFrame(pmacs_protocol::PanelFramePayload::Absent)
)),
"the band is published Absent: refusing input alone leaves a \
stale panel painted and permanently inert"
);
assert!(
semantic_states[&fid].panel_declaration().is_none(),
"and input authority is cleared with it"
);
assert!(
semantic_states[&fid].panel_mapping_generation_exhausted(),
"and the session latches"
);
assert_eq!(
semantic_states[&fid].panel_mapping_generation_peek(),
None,
"an exhausted session reports NO key: the stored pair still \
holds the ceiling it stopped at, and naming it would \
describe a key no frame carries and no gesture may echo"
);
// The NEXT frame must not resurrect the band. Without the latch
// the snapshot is unchanged, the "unchanged" arm returns the
// frozen ceiling, and a `PresentMapped` ships with a key that can
// no longer distinguish anything.
let next = semantic_states
.get_mut(&fid)
.expect("projection")
.render_frame(&editor);
assert!(
!next.iter().any(|msg| matches!(
msg,
InstanceMessage::PanelFrame(
pmacs_protocol::PanelFramePayload::PresentMapped { .. }
)
)),
"no zombie band on the following frame"
);
// And inbound stays refused for the rest of the session.
let baseline = editor.core.borrow().views[&fid].active;
assert_ne!(baseline, panel, "fixture: the panel is not focused");
for echoed in [1, u64::MAX] {
dispatch_panel_event(
&mut editor,
fid,
PROTOCOL_VERSION,
&mut semantic_states,
&mut render,
mapped_pointer(fid, epochs, buffer_id, echoed),
);
assert_eq!(
editor.core.borrow().views[&fid].active,
baseline,
"an exhausted session accepts no gesture, whatever it echoes"
);
}
}
/// §5b G5a — the key advancing RAISES cancellation, without waiting /// §5b G5a — the key advancing RAISES cancellation, without waiting
/// for another pointer event. /// for another pointer event.
/// ///
@ -6763,15 +7081,7 @@ mod tests {
// A FOREIGN edit — nothing this frontend did, and no further // A FOREIGN edit — nothing this frontend did, and no further
// pointer event. The key moves on the next read. // pointer event. The key moves on the next read.
{ foreign_edit(&editor, buffer_id, b"moved\n");
let core = editor.core.borrow();
let registry = core.registry.clone();
let mut reg = registry.borrow_mut();
reg.get_mut(buffer_id)
.expect("panel buffer")
.set_generated_contents(b"moved\n")
.expect("a plain content change");
}
let snapshot = editor.panel_mapping_snapshot(fid); let snapshot = editor.panel_mapping_snapshot(fid);
let state = semantic_states.get_mut(&fid).expect("projection"); let state = semantic_states.get_mut(&fid).expect("projection");
let advanced = state.panel_mapping_generation(snapshot); let advanced = state.panel_mapping_generation(snapshot);

View File

@ -429,6 +429,16 @@ pub struct SemanticRenderState {
/// `generation` starts at 0 meaning "never established"; the first /// `generation` starts at 0 meaning "never established"; the first
/// real mapping takes 1, because zero is invalid on the wire. /// real mapping takes 1, because zero is invalid on the wire.
panel_mapping: Option<(crate::editor::PanelMappingSnapshot, u64)>, panel_mapping: Option<(crate::editor::PanelMappingSnapshot, u64)>,
/// §5b G11a — set once the mapping generation cannot advance, and
/// never cleared for the session.
///
/// Exhaustion fails **closed**: no key means no authority, so the
/// band is published `Absent` and every inbound panel event is
/// refused. The latch is what makes that permanent. Without it the
/// next projection finds an UNCHANGED snapshot, takes the
/// "unchanged" arm, and hands back the frozen ceiling — resurrecting
/// the band with a key that can no longer distinguish anything.
panel_mapping_exhausted: bool,
/// §5b G5 — the panel gesture this frontend has an ACCEPTED `Down` /// §5b G5 — the panel gesture this frontend has an ACCEPTED `Down`
/// for, if any. /// for, if any.
/// ///
@ -661,6 +671,7 @@ impl SemanticRenderState {
// frame from shipping a redundant authoritative `Absent`. // frame from shipping a redundant authoritative `Absent`.
last_panel_payload: Some(PanelFramePayload::Absent), last_panel_payload: Some(PanelFramePayload::Absent),
panel_mapping: None, panel_mapping: None,
panel_mapping_exhausted: false,
accepted_gesture: None, accepted_gesture: None,
panel_gesture_cancellations: 0, panel_gesture_cancellations: 0,
panel_epoch_used: 0, panel_epoch_used: 0,
@ -772,6 +783,9 @@ impl SemanticRenderState {
&mut self, &mut self,
snapshot: Option<crate::editor::PanelMappingSnapshot>, snapshot: Option<crate::editor::PanelMappingSnapshot>,
) -> Option<u64> { ) -> Option<u64> {
if self.panel_mapping_exhausted {
return None;
}
let snapshot = snapshot?; let snapshot = snapshot?;
// Matched by value, not by reference: the changed arm CANCELS, // Matched by value, not by reference: the changed arm CANCELS,
// and cancelling needs `&mut self`. // and cancelling needs `&mut self`.
@ -792,7 +806,30 @@ impl SemanticRenderState {
// physical `Up`, the producer clears its latch and the // physical `Up`, the producer clears its latch and the
// cancelling event never arrives. // cancelling event never arrives.
self.cancel_accepted_gesture(); self.cancel_accepted_gesture();
generation.saturating_add(1) let Some(next) = generation.checked_add(1) else {
// §5b G11a — fail CLOSED, and return BEFORE the
// store below. A saturating add would freeze the key
// at the ceiling while the mapping kept moving
// underneath it, which is precisely the stale-gesture
// hole the key exists to close, with the check still
// looking like it passes.
//
// Returning BEFORE the store below is a second,
// redundant guard against the same zombie band:
// recording `(snapshot, MAX)` here would make the
// next read take the unchanged arm and hand back the
// ceiling. Measured, the two are ALTERNATIVES —
// either alone keeps the band down, and only
// removing both resurrects it. The latch is kept as
// the primary because it has a job the ordering
// does not: it is what makes `peek` and the
// authoritative read agree that this session has no
// key, rather than reporting the ceiling it stopped
// at.
self.panel_mapping_exhausted = true;
return None;
};
next
} }
// First establishment takes 1, never 0: zero is the wire's // First establishment takes 1, never 0: zero is the wire's
// "uninitialised" value and is refused on sight. // "uninitialised" value and is refused on sight.
@ -802,10 +839,34 @@ impl SemanticRenderState {
Some(next) Some(next)
} }
/// §5b G11a — whether this session's key is exhausted.
#[must_use]
pub fn panel_mapping_generation_exhausted(&self) -> bool {
self.panel_mapping_exhausted
}
/// Place the key one advance below the ceiling, so exhaustion is
/// reachable in a test without 2^64 mutations.
#[doc(hidden)]
pub fn seed_panel_mapping_generation_for_test(
&mut self,
snapshot: crate::editor::PanelMappingSnapshot,
generation: u64,
) {
self.panel_mapping = Some((snapshot, generation));
}
/// The current key without advancing it, for assertions and for /// The current key without advancing it, for assertions and for
/// callers that must not have a side effect. /// callers that must not have a side effect.
///
/// `None` once exhausted, matching the authoritative read. The
/// stored pair still holds the ceiling it stopped at, and reporting
/// that would name a key no frame carries and no gesture may echo.
#[must_use] #[must_use]
pub fn panel_mapping_generation_peek(&self) -> Option<u64> { pub fn panel_mapping_generation_peek(&self) -> Option<u64> {
if self.panel_mapping_exhausted {
return None;
}
self.panel_mapping self.panel_mapping
.as_ref() .as_ref()
.map(|(_, generation)| *generation) .map(|(_, generation)| *generation)