diff --git a/context/code/protocol.md b/context/code/protocol.md index f967ee30..c55e1a8b 100644 --- a/context/code/protocol.md +++ b/context/code/protocol.md @@ -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 diff --git a/context/test-evidence/clients.md b/context/test-evidence/clients.md index 11a18ab8..6b087874 100644 --- a/context/test-evidence/clients.md +++ b/context/test-evidence/clients.md @@ -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. diff --git a/crates/improvise-command/src/ui/app.rs b/crates/improvise-command/src/ui/app.rs index 9dd1f127..c556dfa0 100644 --- a/crates/improvise-command/src/ui/app.rs +++ b/crates/improvise-command/src/ui/app.rs @@ -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"**, diff --git a/crates/improvise-command/src/ui/project.rs b/crates/improvise-command/src/ui/project.rs index f9cf5c2d..3acd0663 100644 --- a/crates/improvise-command/src/ui/project.rs +++ b/crates/improvise-command/src/ui/project.rs @@ -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. diff --git a/crates/improvise-protocol/src/client.rs b/crates/improvise-protocol/src/client.rs index ff7763b3..fd09185b 100644 --- a/crates/improvise-protocol/src/client.rs +++ b/crates/improvise-protocol/src/client.rs @@ -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) { diff --git a/crates/improvise-protocol/src/lib.rs b/crates/improvise-protocol/src/lib.rs index d58bbc33..31fc74ab 100644 --- a/crates/improvise-protocol/src/lib.rs +++ b/crates/improvise-protocol/src/lib.rs @@ -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 ` argument names. **Not every /// variant is nameable** — `context/code/protocol.md` §1 says which and why. diff --git a/crates/improvise-protocol/src/resolve.rs b/crates/improvise-protocol/src/resolve.rs index 2945debe..035db148 100644 --- a/crates/improvise-protocol/src/resolve.rs +++ b/crates/improvise-protocol/src/resolve.rs @@ -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 { +fn entered(mode: AppMode) -> Vec { 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 Option> { // `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> { 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 diff --git a/crates/improvise-wasm-client/tests/lockstep.rs b/crates/improvise-wasm-client/tests/lockstep.rs index 6c3b778f..fd8737fc 100644 --- a/crates/improvise-wasm-client/tests/lockstep.rs +++ b/crates/improvise-wasm-client/tests/lockstep.rs @@ -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, + 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]