docs: the reseq probe's readings, and the invariants resequencing changes

Co-Authored-By: Claude Sonnet 4.6 <noreply@anthropic.com>

docs/claude/probe-readings.md

@@ -586,6 +586,53 @@ Two lines of the self-check output are assertions in disguise:
   it afterwards.
 - `[keys] a: armed 0->1 | space: paused 0->1 | t: trigger panel: 0->1 | … | editable focused: 'm' refused=1` (stderr, `UDPSCOPE_PROBE_KEYS_MS`) — **every `X->Y` pair must differ** and **`refused` must be 1**. The refusal is the whole reason the controller is in the bubble phase: every bare-letter accel is also a character, so an accel that fires while a `GtkEditable` has focus makes the window entry unusable. A pair reading `0->0` is an action whose dispatch does not reach the handler a click reaches. Note the format is `<key>: <widget-description>: <before>-><after>` — the name passed to `before_after()` includes the widget's description, so `t: trigger panel: 0->1` is the correct form (not `t: trigger panel 0->1` without the colon before the values).
 - `[color] '<name>' at row R slot S: trace=#RRGGBB chip_agrees=1 (want 1)`, then `[color] override: trace=#123456 chip_agrees=1`, `[color] session: entries=1 rgb=#123456` and `[color] default: trace=#RRGGBB chip_agrees=1` (stderr, `UDPSCOPE_PROBE_COLOR_MS`) — **all three `chip_agrees` must be 1**, the override line's `trace` must be `#123456`, the session line must read `entries=1 rgb=#123456`, and the default line's `trace` must be back to the first line's. Run it with `UDPSCOPE_ENABLE_ALL_MS` ahead of it, or there is no bound trace and the probe prints `no bound trace to recolour` instead of asserting anything; on the standard mock the first line reads `'sine' at row 0 slot 0: trace=#4FA3FF`. Two things make this an assertion rather than a tautology. The colours are read out of **`plot::Plot::trace().color`** — what the renderer will stroke, reached through `Row::plot` *after* `relayout_areas()`, since a new colour is a new figure — and out of the chip's own `<span foreground="…">` markup, not by asking `RowSet::signal_color()` twice, which would pass against a chip that never reached the trace. And the override is `#123456`, deliberately in no palette slot: an override equal to the entry it replaces passes against an implementation that ignores overrides entirely. The session leg round-trips `collect_layout()` → `save_layout()` → `load_layout()` on a temp path and deletes it, because a probe must not leave a colour in the real session file for a later run to inherit.
+- `[reseq-probe] reseq=N late=N stale=N holes=N hole_slots=N backfilled=N open_holes=N bands=N
+  bands_repaired=N nan_slots=N scanned=N trigger_in_hole=D` (stderr, `UDPSCOPE_PROBE_RESEQ_MS`) —
+  the resequencing path's mid-run state; the measured readings and the per-case command are in
+  [verification.md](verification.md). Six things to read carefully:
+
+  1. **`backfilled` and `hole_slots` are not comparable directly.** `hole_slots` counts
+     *time-ring* slots once per hole; `backfilled` counts *value-ring* slots repaired and
+     therefore sums over every non-math channel. On a stream with 4 non-math channels they
+     stand a factor of 4 apart. `hole_slots=4200 backfilled=16800` in the `late` case is
+     healthy, not an error; `backfilled` below `4 × hole_slots` would mean some channels
+     went unrepaired.
+
+  2. **`nan_slots=0` beside a large `holes` is healthy, not a contradiction.** A hole is
+     retired from the table only when its slots age out of the ring
+     (`ScopeModel::forget_holes_before()`), *never* on repair. So the `late` case reads
+     `holes=42 nan_slots=0`: every hole was fully repaired, and all 42 entries stay in the
+     table with no placeholder left in the data. What *would* be a defect is `nan_slots > 0`
+     with `bands_repaired == bands`, which would mean a band claimed data was recovered while
+     placeholders remained. The discriminator is `bands_repaired`, not `holes`.
+
+  3. **`bands` is the visible spans, `open_holes` the whole table.** `bands` counts what the
+     plot is actually shading in the visible window; `open_holes` counts every live hole entry
+     whether or not it is in view. `bands` below `open_holes` is normal — in the `mixed` case
+     `open_holes=43` against `bands=42` because the 43rd hole has scrolled out of the visible
+     window and `build_invalid_spans()` drops it. `bands` *above* `open_holes` would name a
+     stale span left on a plot after its hole was retired.
+
+  4. **`bands_repaired` is the faint tier.** A hole whose late packets have all arrived is
+     still drawn, in `Style::invalid_repaired_fill` rather than `Style::invalid_fill`, so the
+     display distinguishes "there is no data here" from "there was none when this window was
+     first drawn". The three states are: solid while the hole still lacks packets, faint once
+     `Hole::repaired()` is true, absent once the slots age out and `forget_holes_before()`
+     drops it. `bands_repaired == bands` with `nan_slots=0` is the fully recovered reading;
+     `bands_repaired=0` with a non-zero `backfilled` would mean the repair never reached the
+     display.
+
+  5. **`trigger_in_hole` must be 0, always.** A `1` means the trigger engine was fed a
+     reserved span's samples. The engine is specifically not fed them; a NaN comparison is
+     false anyway, but the real reason is that feeding them would advance the hold-off clock
+     across time nothing was sampled in.
+
+  6. **The discriminator for whether a reservation sized the hole right is the exit dump's
+     per-channel `stored=` line, not `frames=`.** `frames` counts delivered packets and is
+     blind to the slots a reservation pushed on their behalf. `stored` reflects what the ring
+     actually holds, so a reservation that mismeasured the hole shows up there and nowhere
+     else.
+
 - `[zoomkeys] ctrl+plus x=[..]->[..] y_held=1 | alt+plus y=[..]->[..] x_held=1` (stderr, `UDPSCOPE_PROBE_ZOOMKEYS_MS`) — **both `_held` must be 1 and both zooms must still happen.** Run it inside a pinned state, where a frame cannot re-frame the other axis for its own reasons: `UDPSCOPE_PROBE_PAUSE_MS=1500 UDPSCOPE_PROBE_ZOOMKEYS_MS=2200`. A `_held=0` is the modifier not reaching the plotter's controller; an unchanged range on the *zoomed* axis is the opposite failure, the key doing nothing. Ctrl restricts to x and Alt to y; Ctrl+Alt zooms neither (no special case needed — neither flag alone fires).
 - `status bar: glance=[● live · 1.09 MS/s · 2 s window] max_glance_chars=53 detail_fields=11 popover_rebuilds=0` (exit dump) — **`max_glance_chars` must stay small** (under about 60) and **`popover_rebuilds` must be 0**. The status row is directly above the plot, so this is the "layout must not depend on content" rule read from the bar's own side: the state field is one word from a fixed set (`connecting`, `live`, `paused`, `armed`, `capturing`, `event held`, `disarmed` — a word added to it must be **no wider than the widest already there**, which is what let `connecting` join at ten characters beside `event held`; the dead-port glance reads `max_glance_chars=51` against a live run's 54), the rate field is `%.3g` (so `10 kS/s`, never `10.0 kS/s`), and the two fields a *state* adds are both elapsed times — trigger mode's `last event … ago` and a pause's `for <elapsed>` — which step units rather than growing digits (`format_elapsed()`). A **paused** glance is not in the dump at all: it is read by `[pause-probe]`'s `glance=` field, since the dump's own line is taken live. `detail_fields` is the popover's label count, a literal, so adding a label without thinking about layout shows up here. The glance rate format matters: `%.3g` drops the trailing zero that a `%.4g` or a fixed-precision format would keep — a rate that reads differently in the dump and in the help page is a format disagreement, and `14-status.txt`'s example must match it.