Settle the mode by observing the grid, not at each composition site

ChatGPT Codex's P1 on #98: switch_view_at composes
[SwitchView(target), ChangeMode(Normal)], and changed_mode settled that
against the grid the client STILL HOLDS -- the outgoing view's. Records ->
pivot emitted RecordsNormal and pivot -> records emitted Normal, which is
the cross-view drift this PR exists to close, by a second door.

The hand-back predicted this as follow-up 3 and called it unreachable
because R is a stranding decline in the browser. That is right about the
TOGGLE route and wrong about this one: records-ness is auto-detected from
the axes (gotcha 1), so a view switch changes it with nothing in the batch
saying "records". One door was enumerated and there were two.

So the remedy is general rather than a patch to switch_view_at.
changed_mode is DELETED; every site emits the plain AppMode::Normal; and
ClientState::fold settles after every fold against the grid it HOLDS.
Route-independent, so no enumeration of composition sites is load-bearing
any more -- the same shape the repo already prefers in cursor_epoch over
matching on CycleAxis, document_generation over matching on LoadModel, and
the dirty flag over a table of command variants.

improvise_protocol::settled_mode is the one rule and all three ends call
it: ClientState::fold, ClientSession::fold (the server's mirror, so the two
cannot diverge in a field nobody currently reads today) and
App::settle_normal_mode. App::normal_mode is gone -- it was that
function's host-side duplicate, and my change orphaned it.

Bidirectional coverage drives a real Host: a session connected to a
records-mode host, the pair folded locally and sent as a
ClientFrame::Commands, every reply delivered in arrival order. The
composed ChangeMode carries the STALE answer deliberately, because
composing the friendly value would let the records -> pivot direction pass
under the fault. Both directions fail with settle_mode no-opped, each
proved separately since the loop stops at the first.

Evidence, the injections and why the first fix's unreachability argument
was too narrow: context/test-evidence/clients.md, context/code/protocol.md.

Co-Authored-By: Claude Opus 5 (1M context) <noreply@anthropic.com>
Claude-Session: https://claude.ai/code/session_01FC2jVn8Au7E9JPkw6bwXXH
This commit is contained in:
Edward Langley
2026-09-21 10:44:17 -07:00
parent 49c6af1978
commit 81fe546594
8 changed files with 263 additions and 76 deletions
+39 -4
View File
@@ -875,10 +875,45 @@ Like `GridUpdate::Extent` it **frames nothing**, so `apply` does not re-fit and
its position in a batch is not load-bearing: it describes what kind of grid the
frames describe, not any position in one.
The client's own settling has **one home**, `resolve::changed_mode`, which every
composition site that can emit `AppMode::Normal` goes through — including
`entered`, which is how a bound `enter-mode normal` reaches it. The three
decision points now ask `state.grid.records`. What that buys concretely: the
**The settling is observed, never composed — and the first version of this fix
got that wrong.** It settled at each *composition site*, in `resolve::changed_mode`,
against the grid the client held **at the moment it resolved the key**. ChatGPT
Codex found the hole on PR #98: `switch_view_at` composes
`[SwitchView(target), ChangeMode(Normal)]`, so the settling read the **outgoing**
view's grid and records → pivot emitted `RecordsNormal` while pivot → records
emitted `Normal`. The drift the fix existed to close, by a second door.
The unreachability argument the first version leaned on covered the *toggle*
route only — `R` is a `stranding` decline in the browser — and records-ness is
auto-detected from the axes (gotcha 1), so a **view switch** changes it with
nothing in the batch saying "records". `doctrine(an_unreachability_claim_is_only_as_wide_as_the_routes_enumerated)`.
So `changed_mode` is **deleted**, every site emits the plain `AppMode::Normal`,
and `ClientState::fold` settles after every fold against the grid it **holds**:
`self.view.mode = settled_mode(&self.view.mode, self.grid.records)`. That is
route-independent — it needs no enumeration of composition sites, which is the
part nothing checks — and it is the same shape the repo already prefers
elsewhere: `cursor_epoch` over matching on `CycleAxis` (gotcha 24),
`document_generation` over matching on `LoadModel` (gotcha 39), the dirty flag
over a table of command variants (gotcha 45).
`settled_mode` is the **one rule**, in `improvise-protocol`, and all three ends
call it: `ClientState::fold`, `ClientSession::fold` (the server's mirror, so the
two cannot diverge in a field nobody currently reads) and
`App::settle_normal_mode`. `App::normal_mode` is gone — it was that function's
host-side duplicate. It settles the `Normal` pair and **nothing else**:
`Editing`/`RecordsEditing` pass through untouched, which is exactly why a
records decision asks the grid and never the mode.
There remains a **window, and it is inherent**: between the local optimistic
fold of a `SwitchView` and the arrival of the target view's projection, the
client holds the outgoing grid and cannot know the target's records-ness. The
mode settles the moment the projection lands. No design removes that window —
read-time derivation has exactly the same exposure, since it would read the same
stale grid — so the honest statement is that the mode settles *when the grid
does*, on both ends.
The three decision points ask `state.grid.records`. What that buys concretely: the
commit at a records cell **declines** rather than composing
`typed_cell_command` against a grid whose columns are
`[coords…, +cat, measures…, +]` (gotcha 1), which was a wrong write and strictly
+67 -15
View File
@@ -2493,21 +2493,73 @@ test fails on `a records commit this client cannot compose was composed anyway`.
`App::settle_normal_mode` settles **both** `Normal` and `RecordsNormal` against
the layout, so a `RecordsNormal` over an ordinary grid becomes `Normal`. The
first version of `resolve::changed_mode` mapped only `Normal → RecordsNormal`,
which left the mirror-image drift live: `Esc` out of `RecordsEditing` resolves
through `entered` to `enter-mode records-normal`, and a grid that had stopped
being a records grid would leave the client on `RecordsNormal` while its host
settled `Normal`. Found in review of this branch rather than by a test.
first version of the client's settling mapped only `Normal → RecordsNormal`,
which left the mirror-image drift live. Found in review of this branch.
The test now aims at `improvise_protocol::settled_mode`, which is the **one**
rule all three ends call — `ClientState::fold`, `ClientSession::fold` and
`App::settle_normal_mode`.
**Fault injected**: the `(Normal | RecordsNormal, false)` arm narrowed to
`(Normal, false)`. The case `records=false, asked RecordsNormal` fails. The
fourth row and the `AppMode::Help` case are the negative arms — without them a
helper that answered `RecordsNormal` always, or one that answered `Normal`
always, would pass.
`(Normal, false)`. The case `records=false, holding RecordsNormal` fails. The
fourth row and the pass-through cases are the negative arms — without them a
rule that answered `RecordsNormal` always, or `Normal` always, would pass, and
the pass-through loop is what pins that `Editing`/`RecordsEditing` are **not**
settled (the reason a records decision asks the grid and never the mode).
Residual, stated rather than guarded: the host settles **after** the batch and
the client settles at **composition** time, so a batch that itself changes
records-ness and then ends in `Normal` would still disagree. No client in this
workspace composes one — `R` is a `stranding` decline in the browser — and
closing it needs the settling to move behind the fold, which `reduce_view` (a
function of `ViewState` alone, gotcha 32) cannot do today.
### switching_between_a_records_view_and_a_pivot_view_settles_both_ways
**The P1 ChatGPT Codex found on PR #98, and the more useful half is why the
first fix missed it.** That fix settled the mode at each *composition site*
(`resolve::changed_mode`), against the grid the client held when it resolved the
key. `switch_view_at` composes `[SwitchView(target), ChangeMode(Normal)]`, so it
settled against the **outgoing** view: records → pivot emitted `RecordsNormal`
and pivot → records emitted `Normal`, recreating the very drift the PR closed.
The hand-back had *predicted* this as follow-up 3 and concluded it was
unreachable **because `R` is a `stranding` decline in the browser**. That
reasoning is right about the toggle route and wrong about this one: records-ness
is auto-detected from the axes (gotcha 1), so a **view switch** changes it with
nothing in the batch saying "records". One door was enumerated and there were
two — `doctrine(an_unreachability_claim_is_only_as_wide_as_the_routes_enumerated)`.
Codex had flagged the same path on PR #91, where the host side was fixed and the
client side was not, so it was tracking one defect across three PRs.
The remedy is general rather than a patch to `switch_view_at`: `changed_mode` is
deleted, every site emits the plain `AppMode::Normal`, and `ClientState::fold`
settles after **every** fold against the grid it holds. Route-independent, so no
enumeration of composition sites is load-bearing any more.
**The fixture drives the real path**: a `Host` in records mode, a session
connected (which opens the document's *default* view, gotcha 29 — the first
draft asserted the opposite and failed its own precondition), the composed pair
folded locally and sent as a `ClientFrame::Commands`, and every reply frame
delivered in arrival order. `deliver` takes the whole reply rather than a
hand-picked projection.
**The composed `ChangeMode` carries the STALE answer deliberately** —
`settled_mode(&Normal, client.grid.records)` off the outgoing grid — because
that is what `switch_view_at` really emitted, and composing the friendly value
instead would make the records → pivot direction pass under the fault.
**Fault injected**: `ClientState::settle_mode` reduced to a no-op. Both
directions fail, each proved separately because the loop stops at the first:
- pivot → records: `_Records: the client settled against the view it LEFT`,
`Normal` against `RecordsNormal`.
- records → pivot, reached by relaxing the first iteration's expectation under
the same injection: `Default: the client settled against the view it LEFT`,
`RecordsNormal` against `Normal`.
Records-ness and the mode are asserted as **two separate facts** rather than one
derived from the other — a first version computed the records precondition from
the mode expectation, so relaxing the mode silently relaxed the precondition too
and the test failed for the wrong reason.
### the_mode_a_switch_lands_in_is_the_one_a_host_on_that_view_holds
The lockstep half of the entry above: it asserts the host itself answers
**differently** per view (`Normal` on the pivot, `RecordsNormal` on the records
view). Without it, "the client settles to X" is a claim about the client alone —
a host that answered `Normal` everywhere would make the switch test's
expectations arbitrary rather than lockstep.
+4 -15
View File
@@ -604,24 +604,13 @@ impl App {
self.cursor_epoch
}
/// What `AppMode::Normal` means on the grid this app is on: a records layout
/// has its own. Observed, never carried — `context/code/command.md`.
pub fn normal_mode(&self) -> AppMode {
match self.layout.is_records_mode() {
true => AppMode::RecordsNormal,
false => AppMode::Normal,
}
}
/// `Normal` and `RecordsNormal` are one mode over two layouts, so the mode a
/// batch ENDS in must match the grid it ends on (improvise-sihr).
fn settle_normal_mode(&mut self) {
if matches!(
self.view_state.mode,
AppMode::Normal | AppMode::RecordsNormal
) {
self.view_state.mode = self.normal_mode();
}
// The same rule a client settles by, so the two ends cannot drift
// (improvise-e5pf) — `context/code/protocol.md`.
self.view_state.mode =
improvise_protocol::settled_mode(&self.view_state.mode, self.layout.is_records_mode());
}
/// Which views the last batch actually reshaped. **Empty means "not known"**,
@@ -712,6 +712,9 @@ impl ClientSession {
/// same function the client runs. Private: [`Sessions::apply`] is the door.
fn fold(&mut self, cmd: &Command) {
reduce_view(&mut self.view, cmd);
// The mirror settles exactly as the client does, against the grid this
// session was last projected (improvise-e5pf).
self.view.mode = improvise_protocol::settled_mode(&self.view.mode, self.grid.records);
}
/// The server's mirror of this client's view slice.
+9
View File
@@ -4,6 +4,7 @@
use crate::{
BasisCache, CategoryTreeCache, Command, DocumentCache, FormulaCache, GridCache, Projection,
Rejection, Snapshot, TileBarCache, ViewListCache, ViewState, WidgetCache, reduce_view,
settled_mode,
};
use serde::Serialize;
@@ -52,6 +53,7 @@ impl ClientState {
for projection in &snapshot.seed {
self.apply_projection(projection);
}
self.settle_mode();
self.revision += 1;
}
@@ -62,9 +64,16 @@ impl ClientState {
Command::Project(projection) => self.apply_projection(projection),
other => reduce_view(&mut self.view, other),
}
self.settle_mode();
self.revision += 1;
}
/// Settle the `Normal` pair against the grid this client **holds**, after
/// every fold. Observed, never composed — `context/code/clients.md`.
fn settle_mode(&mut self) {
self.view.mode = settled_mode(&self.view.mode, self.grid.records);
}
/// The widget dispatch: a projection names the widget it is addressed to.
/// The `CategoryTreeCache`/`TileBarCache` overlap is deliberate (gotcha 32).
fn apply_projection(&mut self, projection: &Projection) {
+12
View File
@@ -170,6 +170,18 @@ pub enum AppMode {
},
}
/// `Normal` and `RecordsNormal` are one mode over two layouts, so the mode an
/// end holds must answer for the grid it holds — `context/code/protocol.md`.
pub fn settled_mode(mode: &AppMode, records: bool) -> AppMode {
// The pair and nothing else: `Editing`/`RecordsEditing` are NOT settled,
// which is why a records decision asks the grid and never the mode.
match (mode, records) {
(AppMode::Normal | AppMode::RecordsNormal, true) => AppMode::RecordsNormal,
(AppMode::Normal | AppMode::RecordsNormal, false) => AppMode::Normal,
(other, _) => other.clone(),
}
}
impl AppMode {
/// The mode a keymap's `enter-mode <name>` argument names. **Not every
/// variant is nameable** — `context/code/protocol.md` §1 says which and why.
+28 -42
View File
@@ -290,7 +290,7 @@ fn composed(
let mode = AppMode::from_name(args.first()?)?;
// `declined` answers this first, and both halves hold the rule:
// no path opens a room this client cannot commit.
stranding(&mode).is_none().then(|| entered(state, mode))
stranding(&mode).is_none().then(|| entered(mode))
}
// ── panels ───────────────────────────────────────────────────
@@ -312,13 +312,10 @@ fn composed(
panel,
open: !closing,
},
changed_mode(
state,
match closing {
true => AppMode::Normal,
false => panel.mode(),
},
),
Command::ChangeMode(match closing {
true => AppMode::Normal,
false => panel.mode(),
}),
])
}
@@ -377,7 +374,7 @@ fn composed(
Some(vec![
model(state, ModelCommand::CreateView(name.clone()))?,
Command::SwitchView(name),
changed_mode(state, AppMode::Normal),
Command::ChangeMode(AppMode::Normal),
])
}
"delete-view-at-cursor" => delete_view_at_cursor(state),
@@ -459,28 +456,17 @@ fn stranding(mode: &AppMode) -> Option<&'static str> {
}
/// `EnterMode::execute`: clear the incoming mode's minibuffer, then change.
fn entered(state: &ClientState, mode: AppMode) -> Vec<Command> {
fn entered(mode: AppMode) -> Vec<Command> {
let mut commands = Vec::new();
if let Some(mb) = mode.minibuffer() {
commands.push(write_buffer(&mb.buffer_key, String::new()));
}
commands.push(changed_mode(state, mode));
// Plain `Normal`: which member of the pair it settles to is the grid's, and
// `ClientState::fold` answers that — improvise-e5pf, `context/code/clients.md`.
commands.push(Command::ChangeMode(mode));
commands
}
/// `AppMode::Normal` settled against the GRID, the way `App::settle_normal_mode`
/// settles it against the layout (improvise-e5pf). The **one** home.
fn changed_mode(state: &ClientState, mode: AppMode) -> Command {
// BOTH directions, because `settle_normal_mode` settles both: a
// `RecordsNormal` over an ordinary grid is the mirror-image drift.
let settled = match (mode, state.grid.records) {
(AppMode::Normal | AppMode::RecordsNormal, true) => AppMode::RecordsNormal,
(AppMode::Normal | AppMode::RecordsNormal, false) => AppMode::Normal,
(other, _) => other,
};
Command::ChangeMode(settled)
}
// ── the grid cursor ─────────────────────────────────────────────────────
/// A mirror of `navigation.rs`'s `MoveKind`, spelled again because that crate
@@ -714,7 +700,7 @@ fn commit(state: &ClientState, edit_mode: AppMode, advance: Advance) -> Option<V
basis: state.basis.claim([record_at_cursor(state)?])?,
cmd: typed_cell_command(id, &text)?,
}];
commands.push(changed_mode(state, AppMode::Normal));
commands.push(Command::ChangeMode(AppMode::Normal));
commands.extend(advanced(state, edit_mode, advance)?);
Some(commands)
}
@@ -730,7 +716,7 @@ fn create_column(
) -> Option<Vec<Command>> {
// `exit_mode_for`: the tidy-up goes FIRST, where an aborting
// `AddCategory` cannot reach it (gotcha 21).
let mut commands = vec![changed_mode(state, AppMode::Normal)];
let mut commands = vec![Command::ChangeMode(AppMode::Normal)];
let name = text.trim();
if !name.is_empty() {
commands.push(model(
@@ -989,7 +975,7 @@ fn switch_view_at(state: &ClientState, index: usize) -> Option<Vec<Command>> {
let summary = state.views.views.get(index)?;
Some(vec![
Command::SwitchView(summary.name.clone()),
changed_mode(state, AppMode::Normal),
Command::ChangeMode(AppMode::Normal),
])
}
@@ -2497,32 +2483,32 @@ mod tests {
);
}
/// `changed_mode` mirrors `settle_normal_mode`, which settles BOTH members
/// `settled_mode` mirrors `settle_normal_mode`, which settles BOTH members
/// of the pair. See `context/test-evidence/clients.md`.
#[test]
fn the_normal_pair_is_settled_in_both_directions() {
for (records, asked, expected) in [
for (records, held, expected) in [
(true, AppMode::Normal, AppMode::RecordsNormal),
(true, AppMode::RecordsNormal, AppMode::RecordsNormal),
(false, AppMode::RecordsNormal, AppMode::Normal),
(false, AppMode::Normal, AppMode::Normal),
] {
let mut state = client_on(record_cell());
crate::WidgetCache::apply(&mut state.grid, &GridUpdate::Records(records));
assert_eq!(
changed_mode(&state, asked.clone()),
Command::ChangeMode(expected),
"records={records}, asked {asked:?}"
crate::settled_mode(&held, records),
expected,
"records={records}, holding {held:?}"
);
}
// And a mode that is neither passes through untouched, or the helper is
// a records-mode filter rather than a settling.
let mut state = client_on(record_cell());
crate::WidgetCache::apply(&mut state.grid, &GridUpdate::Records(true));
assert_eq!(
changed_mode(&state, AppMode::Help),
Command::ChangeMode(AppMode::Help)
);
// Everything else passes through, or this is a records-mode filter and
// not a settling — `Editing` is the one that must NOT move.
for other in [
AppMode::Help,
AppMode::editing(),
AppMode::records_editing(),
] {
assert_eq!(crate::settled_mode(&other, true), other);
assert_eq!(crate::settled_mode(&other, false), other);
}
}
/// Records mode is the fork this client does not have (gotcha 1), so its
@@ -1148,6 +1148,107 @@ fn leaving_a_panel_in_records_mode_lands_where_the_host_lands() {
}
}
/// Deliver everything the host said to this session, in arrival order — the
/// whole reply, never a hand-picked projection.
fn deliver(
frames: Vec<improvise_command::ui::host::Addressed>,
session: improvise_command::ui::project::SessionId,
client: &mut ClientState,
) {
for addressed in frames.into_iter().filter(|a| a.to == session) {
match addressed.msg {
improvise_protocol::ServerFrame::Snapshot(snapshot) => client.bootstrap(*snapshot),
improvise_protocol::ServerFrame::Commands(cmds) => {
for cmd in &cmds {
client.fold(cmd);
}
}
improvise_protocol::ServerFrame::Rejected(_) => {}
}
}
}
/// improvise-e5pf, the route the first fix missed: a **view switch** changes
/// records-ness. See `context/test-evidence/clients.md`.
#[test]
fn switching_between_a_records_view_and_a_pivot_view_settles_both_ways() {
let (host_app, _) = records_pair();
let records_view = host_app.view_name().to_string();
let mut host = improvise_command::ui::host::Host::new(host_app);
let (session, welcome) = host.connect(8, 8);
let mut client = ClientState {
window: (8, 8),
..ClientState::default()
};
deliver(vec![welcome], session, &mut client);
// A fresh session opens the DOCUMENT's default view, not the host's
// (gotcha 29), so the client starts on the pivot and the host on records.
assert!(
!client.grid.records,
"precondition: the client opens on a pivot"
);
assert_eq!(format!("{:?}", client.view.mode), "Normal");
// Two separate facts, so a broken mode cannot be masked by a precondition
// derived from the same expectation — `context/test-evidence/clients.md`.
for (target, records, expected) in [
(records_view.as_str(), true, "RecordsNormal"),
("Default", false, "Normal"),
] {
// The WORST a composition site can do, and what `switch_view_at` really
// did: settle against the grid the client still holds — the outgoing one.
let stale = improvise_protocol::settled_mode(&AppMode::Normal, client.grid.records);
let composed = vec![
improvise_protocol::Command::SwitchView(target.to_string()),
improvise_protocol::Command::ChangeMode(stale),
];
for cmd in &composed {
client.fold(cmd);
}
deliver(
host.handle(session, ClientFrame::Commands(composed)),
session,
&mut client,
);
assert_eq!(
client.view.active_view, target,
"the client must really be on {target}, or nothing below separates the two"
);
assert_eq!(
client.grid.records, records,
"{target}: the projection must really change records-ness"
);
assert_eq!(
format!("{:?}", client.view.mode),
expected,
"{target}: the client settled against the view it LEFT"
);
}
}
/// The host standing on each of those views holds the same mode the client
/// does. See `context/test-evidence/clients.md`.
#[test]
fn the_mode_a_switch_lands_in_is_the_one_a_host_on_that_view_holds() {
let (mut app, _) = records_pair();
let records_view = app.view_name().to_string();
let mut held = Vec::new();
for target in ["Default", &records_view] {
app.switch_to_view(target);
app.apply_effects(vec![]);
held.push(format!("{:?}", app.view_state.mode));
}
assert_eq!(
held,
vec!["Normal".to_string(), "RecordsNormal".to_string()],
"the host itself must answer differently per view, or the client has \
nothing to agree with"
);
}
/// improvise-e5pf: the commit declines off the GRID, so a client whose mode has
/// drifted still declines. See `context/test-evidence/clients.md`.
#[test]