Merge pull request #343 from fiddlerwoaroof/adr009/derived

feat(incremental): the Derived trait, Eager and the differential harness (improvise-t8ow)

Cargo.lock

@@ -952,6 +952,15 @@ dependencies = [
  "improvise-formula",
 ]
 
+[[package]]
+name = "improvise-incremental"
+version = "0.1.0"
+dependencies = [
+ "improvise-core",
+ "improvise-io",
+ "proptest",
+]
+
 [[package]]
 name = "improvise-io"
 version = "0.1.0-rc2"

Cargo.toml

@@ -1,5 +1,5 @@
 [workspace]
-members = [".", "crates/improvise-formula", "crates/improvise-core", "crates/improvise-protocol", "crates/improvise-io", "crates/improvise-command", "crates/improvise-wasm-client", "crates/improvise-ws-server", "crates/improvise-worker-server", "crates/gp-tree", "crates/improvise-gp", "crates/numtower", "crates/zset"]
+members = [".", "crates/improvise-formula", "crates/improvise-core", "crates/improvise-protocol", "crates/improvise-io", "crates/improvise-command", "crates/improvise-wasm-client", "crates/improvise-ws-server", "crates/improvise-worker-server", "crates/gp-tree", "crates/improvise-gp", "crates/numtower", "crates/zset", "crates/improvise-incremental"]
 
 [package]
 name = "improvise"

context/code/improvise-incremental.md

@@ -0,0 +1,91 @@
+# `improvise-incremental`: the reasoning
+
+`crates/improvise-incremental` is ADR 009 step 2 (improvise-t8ow, epic improvise-bw4p): the
+plug. It holds the `Derived` trait, `Eager` (today's evaluator behind it) and the
+differential harness every later backend is checked with. There is no incremental backend
+here, the evaluator is untouched and no existing crate changed. The decisions are the ADR's
+(`context/adr/009-incremental-evaluation.md`, clause 2). The evidence for each test is in
+`context/test-evidence/improvise-incremental.md`.
+
+## The shape
+
+| item | what it is |
+|---|---|
+| `Derived` | the two things the evaluator reads: `value(key, agg)` and `raw_fold(partial)` |
+| `Eager` | an owned `Model` plus its None categories; every answer is a call into `Model` |
+| `Maintained` | a `Derived` that is told each `Edit`; `Eager` is one |
+| `Edit` | one model mutation as data (set, clear, add or remove a formula, set a measure's aggregation) |
+| `probes`, `Probe` | every question worth asking of a model, and a way to put it to any backend |
+| `differential` | runs one edit sequence on a candidate and on `Eager`, comparing every probe at every step |
+| `Divergence`, `Report` | what a failure names (step, probe, both answers) and what a pass compared |
+
+## Interpretations
+
+Clause 2 names the trait and says what it carries ("the formula result at a key, and the raw
+fold of the cells that match a partial key") and nothing else. These are the readings taken.
+
+1. **`Derived` lives in this crate, not in improvise-core.** The ADR says improvise-core
+   "gains a trait". Putting it there changes an existing crate's source, which the brief for
+   this step ruled out, and the brief was ambiguous about it. This departs from the accepted
+   ADR's text, so it is flagged to the user and not decided here: improvise-bw4p.2 moves it
+   (one file and a `pub use`, since the trait names only core types). While it sits
+   downstream, core cannot read through it, which is the clause's point.
+2. **Two methods, the minimum.** `value(key, agg)` is the formula result at a key, or the cell
+   as stored or folded; `raw_fold(partial)` is the fold of matching stored cells. `agg` is
+   `Aggregation`, the evaluator's own type. Hidden-item `covers`, totals and occupancy are not
+   in the trait, so the differential cannot probe them, and a hidden item (view state) cannot
+   be exercised at all. The ADR's differential compares "every drawn cell, total and occupancy
+   count"; improvise-bw4p.3 adds them. A group is exercised: a stored key with one coordinate
+   replaced by its item's group is a probe.
+3. **`raw_fold` is never a formula, and `Eager` enforces it.** For a partial naming a formula
+   target `Eager::raw_fold` is `None`; otherwise it is `evaluate_aggregated(partial, OverHidden)`,
+   because the evaluator's own raw fold (`aggregate_raw`, `aggregate_cell_values`) is private to
+   core. Calling it through the public path is exact for any partial that names no formula
+   target. improvise-bw4p.2 exposes the raw fold from core so `Eager` stops going round.
+4. **`Eager` recomputes formulas after every edit.** Production does it in `rebuild_layout`
+   (`Model::recompute_formulas(none_cats)`), and an over-hidden read of a formula cell reads
+   the cache it fills. So `Eager` carries the None categories of the view it stands for and
+   recomputes under them after each edit, as a layout rebuild does.
+5. **`Edit` is the vocabulary of the harness, not of the wire.** Five variants, each one
+   public `Model` call. A later step adds variants for what it maintains (an item added, a
+   category removed); the harness does not care which. An `Edit` fault reaches both sides of a
+   differential alike, so it is pinned only where a direct `Eager` test reads the result:
+   `ClearCell`, `AddFormula` and `RemoveFormula`, and `SetMeasureAgg` through the fold tests.
+   `SetCell` is read by nearly every test.
+6. **Values agree by float rules with every NaN one value** (`same_value`), the rule clause 3
+   states for cell deltas. Signed zero compares equal, so a later `ExactSum` cannot be told
+   from eager's sum by the sign of a zero here; clause 8 has its own property test for that.
+7. **No `zset` dependency yet.** Nothing in this step uses a Z-set. It arrives with the first
+   backend, as the cell delta of step 3.
+
+## What the harness checks
+
+`differential(model, none_cats, candidate, edits)` builds `Eager` over a clone of the model,
+applies each edit to both, and after step 0 and after every edit asks both every probe. The
+probe set **accumulates**: probes from the model at every earlier step stay asked, so a backend
+that goes on answering for a removed formula diverges. A pass returns a `Report` of how many
+states and answers were compared.
+
+`probes(model)` takes the base keys (each stored key, and each with one coordinate replaced by
+its item's group), every sub-partial of a base key dropping at most `MAX_DROPPED = 3`
+coordinates plus the empty key, and each formula's target over each of those. Each key is asked
+as an exact value, an over-hidden value and a raw fold. A fold dropping more than three
+coordinates from a stored key is not asked about. `edit_probes`
+adds the key an edit names, so a cleared cell is asked about after it is gone. A divergence
+reads `divergence at step N: <probe>: eager <a> != candidate <b>`.
+
+**A limit, stated plainly (improvise-bw4p.4).** The probe set is every stored key's
+sub-partials, not the keys a view draws. A view with four or more categories on None draws a cell
+that drops four or more coordinates of a stored key, and the harness checks none of those cells:
+a rival wrong only at `{C0=a, _Measure=Revenue}` over a five-category model passes. Neither
+shipped demo reaches the limit, so the corpus does not show it. Raising `MAX_DROPPED` is not the
+answer, because `sub_partials` walks all 2^n subsets of a key whatever the limit is (93ms at 20
+categories and 225ms at 22 in a debug build, per call). The fix is to probe the keys each view
+draws, with steps 3 and 4; until then a candidate on such a view is under-checked.
+
+The corpus the tests use is `examples/demo.improv` and `web/demo.improv`, loaded through
+`improvise_io::persistence::load`, and hand-built models (formulas, text, mixed values, a group).
+`eager_matches_the_evaluator_on_the_shipped_documents` takes every view's None categories; the
+differential runs take the first per document, and the largest document only its first four
+edits, to keep the binary under two seconds in a debug build. A proptest (256 cases) runs random
+edit sequences against a candidate that rebuilds an `Eager` from scratch on each edit.

context/test-evidence/improvise-incremental.md

@@ -0,0 +1,194 @@
+# Test evidence: `improvise-incremental`
+
+What each test guards, which rival it was run against, and where that rival failed. The
+reasoning is in `context/code/improvise-incremental.md`; the decisions are ADR 009 clause 2's.
+
+**How the rivals are kept.** The `the_harness_catches_*` tests run `differential` on a
+`Rival`, an `Eager` told every edit and wrong in one way, and assert the step at which the
+harness reports the divergence. They run on every build, so each rival is watched failing on
+every run and not once by hand.
+
+**Injected in the source.** Eighteen faults were put into `src/eager.rs`, `src/harness.rs`
+and `src/edit.rs` one at a time, each run against the whole suite and each reverted and
+followed by a full rerun. The failing tests, by name (a fault no test names survived, and
+none did):
+- `Eager::value` ignores its `Aggregation`: `eager_follows_an_edit_to_the_cell_a_fold_reads`,
+  `eager_matches_the_evaluator_on_the_shipped_documents`, `eager_raw_fold_is_never_a_formula`,
+  `eager_value_reads_a_formula_exactly_and_folded`,
+  `the_harness_catches_a_backend_that_ignores_the_aggregation`,
+  `the_harness_catches_a_wrong_folded_formula_value`;
+- `Eager::raw_fold` reads `Exact`: `eager_raw_fold_sums_by_default`,
+  `eager_raw_fold_follows_the_measures_aggregation`, `eager_raw_fold_of_text_is_unanimous_or_mixed`,
+  `eager_numbers_among_text_are_mixed`, `eager_follows_an_edit_to_the_cell_a_fold_reads`,
+  `eager_matches_the_evaluator_on_the_shipped_documents`,
+  `the_harness_catches_a_raw_fold_that_returns_a_formula`;
+- `Eager::raw_fold` returns a formula's value: `eager_raw_fold_is_never_a_formula`,
+  `eager_matches_the_evaluator_on_the_shipped_documents`,
+  `the_harness_catches_a_raw_fold_that_returns_a_formula`;
+- `Eager::apply` does not recompute formulas: `eager_follows_an_edit_to_the_cell_a_fold_reads`,
+  `a_maintained_eager_equals_a_fresh_one_over_random_edit_sequences`;
+- the harness compares only the first edit: `the_harness_catches_a_backend_that_ignores_a_clear`,
+  `…_ignores_the_measure_aggregation`, `…_goes_stale_after_two_edits`,
+  `the_harness_catches_a_backend_that_keeps_answering_for_a_removed_formula`;
+- the harness never reports a divergence: all nine `the_harness_catches_*` tests;
+- `same_value` always true: `same_value_follows_the_float_rules_and_is_exact_elsewhere` and four
+  `the_harness_catches_*` tests;
+- `same_value` NaN unequal, signed zero by bits, any two text equal: each fails
+  `same_value_follows_the_float_rules_and_is_exact_elsewhere` and nothing else;
+- `probes` omit formula cells: `probes_cover_folds_formulas_measures_and_groups` and four
+  `the_harness_catches_*` tests;
+- `probes` drop at most one coordinate: `probes_cover_folds_formulas_measures_and_groups`,
+  `the_harness_catches_a_fault_that_only_shows_after_two_coordinates_are_dropped`;
+- `probes` omit raw folds: `probes_cover_folds_formulas_measures_and_groups`,
+  `an_edit_names_its_key_as_two_value_probes_and_a_fold`,
+  `the_harness_catches_a_raw_fold_that_returns_a_formula`;
+- `probes` omit group keys: `probes_cover_folds_formulas_measures_and_groups`,
+  `the_harness_catches_a_wrong_group_fold`;
+- the probe history is forgotten between steps: `…_goes_stale_after_two_edits`,
+  `…_ignores_a_clear`, `the_harness_catches_a_backend_that_keeps_answering_for_a_removed_formula`;
+- `edit_probes` names nothing: `an_edit_names_its_key_as_two_value_probes_and_a_fold`;
+- `Edit::AddFormula` as a no-op: `eager_add_and_remove_formula_change_what_a_key_reads`;
+- `Edit::ClearCell` applied as `SetCell(0.0)`, which both sides of a differential share and so
+  only a direct `Eager` test can see: `eager_clear_cell_leaves_the_key_absent`.
+
+## eager_raw_fold_sums_by_default
+
+Hand-computed: Revenue under Product A is 10 + 5 = 15. Fails on the `raw_fold`-reads-`Exact`
+rival (a partial key names no stored cell, so the answer is `None`).
+
+## eager_raw_fold_follows_the_measures_aggregation
+
+After `measure_agg[Revenue] = Max` the same fold is 10, and Cost, unchanged, still sums to 6.
+A fold that always sums fails on the first; one that always takes the maximum fails on the second.
+
+## eager_raw_fold_of_text_is_unanimous_or_mixed
+
+Note under A is two equal texts and reads as that text; under B it is two different texts and
+reads `Error("mixed")`. A fold that drops text, which the evaluator used to do (gotcha 7),
+returns `None` for both.
+
+## eager_numbers_among_text_are_mixed
+
+A text among numbers is `Error("mixed")`, not the sum of the numbers.
+
+## eager_value_reads_a_formula_exactly_and_folded
+
+`Profit = Revenue - Cost` reads 6 at East/A exactly, and 9 at Product A with Region over
+hidden: (10 + 5) - (4 + 2), the fold taken before the subtraction. Fails on the
+`value`-ignores-`Aggregation` rival.
+
+## eager_follows_an_edit_to_the_cell_a_fold_reads
+
+After East/A Revenue becomes 20 the fold is 25 and the folded Profit 19. The Profit half is
+what fails when `apply` forgets to recompute formulas: the folded cache is then stale.
+
+## eager_matches_the_evaluator_on_the_shipped_documents
+
+Both shipped documents, every view's None categories, and the hand model: every probe of
+`Eager` equals a direct `evaluate_aggregated` on a model recomputed under the same None
+categories, and the probe set is non-empty. Fails on both aggregation rivals.
+
+## eager_agrees_with_itself_over_every_corpus_edit_sequence
+
+`differential` over a generated edit sequence on each corpus model returns a `Report` with
+`edits + 1` steps and a non-zero probe count. The count assertion is what a harness that
+compared nothing would fail; the step count is what one that stopped early would fail.
+## the_harness_passes_a_backend_that_is_right
+
+The control for the `catches` tests: `Eager` as the candidate over the hand-built edits is a
+pass, so a harness that rejects everything is seen.
+
+## the_harness_catches_a_backend_that_ignores_the_aggregation
+
+A candidate that reads every `value` as `Exact` diverges at step 0, first at the full-key
+formula cell `{East, A, Profit}` over hidden (eager `None`, candidate `6`).
+
+## the_harness_catches_a_backend_that_ignores_the_measure_aggregation
+
+A candidate that drops `SetMeasureAgg` diverges at step 2, the edit that sets it, on a Revenue key.
+
+## the_harness_catches_a_backend_that_goes_stale_after_two_edits
+
+A candidate that stops applying edits after the second diverges at step 3, on a Revenue key.
+A prefix of steps cannot see a backend that goes wrong late.
+
+## the_harness_catches_a_backend_that_ignores_a_clear
+
+A candidate that keeps a cleared cell diverges at step 3 and the message names it.
+
+## the_harness_catches_a_wrong_folded_formula_value
+
+Review of PR 343 (Codex P1): a rival wrong only at `value({Product=A, _Measure=Profit}, OverHidden)`,
+the Profit cell a view with Region on None draws, passed 128 probes, because formula cells were
+built over full keys only. Now the divergence is at step 0 on exactly that probe, eager `9`,
+candidate `-999`.
+
+## the_harness_catches_a_backend_that_keeps_answering_for_a_removed_formula
+
+Review of PR 343: probes were rebuilt from the post-edit model, so a candidate that ignores
+`RemoveFormula` was never asked about Profit again. Probes now accumulate over every step. The
+divergence is at the last step, on a Profit key, eager `None`, candidate `Some`.
+
+## the_harness_catches_a_fault_that_only_shows_after_two_coordinates_are_dropped
+
+Review of PR 343 (Copilot): only one-coordinate partials and the empty key were probed. A rival
+wrong only at `{_Measure=Revenue}` now diverges at step 0 on `Value({_Measure=Revenue}, Exact)`.
+The bound is `MAX_DROPPED = 3` coordinates; a fold dropping more is not asked about.
+
+## the_harness_catches_a_raw_fold_that_returns_a_formula
+
+Review of PR 343 (Copilot): `raw_fold` is documented never to be a formula. A rival whose
+`raw_fold` is `value(partial, OverHidden)` diverges at step 0 on a `RawFold` of a Profit partial
+(eager `None`, candidate `Some`). It could not be seen while `Eager` itself returned the formula.
+
+## the_harness_catches_a_wrong_group_fold
+
+A group name stands in for an item in the probe keys. A rival wrong only at
+`{Region=Coastal, Product=A, _Measure=Revenue}` diverges at step 0, eager `15`, candidate `-999`.
+
+## eager_folds_a_group_it_is_asked_about
+
+The group fold in the grouped model is East + West = 15 exactly, so the rival test above has a
+true answer to differ from.
+
+## eager_raw_fold_is_never_a_formula
+
+At `{Product=A, _Measure=Profit}` the folded value is `9` and the raw fold is `None`. Fails on the
+fault that lets `raw_fold` read the formula cache.
+
+## eager_add_and_remove_formula_change_what_a_key_reads
+
+Review of PR 343: `Edit::AddFormula` as a no-op left all 25 tests green, because an `Edit` fault
+reaches both sides of a differential alike. `Double = Revenue * 2` reads `None` before the edit
+and `20` at East/A after it, and `None` again after `RemoveFormula`. Fails on `AddFormula` as a
+no-op.
+
+## eager_clear_cell_leaves_the_key_absent
+
+After `ClearCell` the key reads `None` and the model holds no cell. A `ClearCell` applied as
+`SetCell(0.0)` hits both sides of a differential identically, so only this direct test fails.
+
+## same_value_follows_the_float_rules_and_is_exact_elsewhere
+
+NaN equals NaN, `-0.0` equals `0.0`, `1.0` differs from `1.0000000000000002`, texts and errors
+compare exactly, and `None` equals only `None`. Each of three one-line faults in `same_value`
+(NaN unequal, signed zero by bits, any two texts equal) survived the whole suite until this test
+existed.
+
+## probes_cover_folds_formulas_measures_and_groups
+
+`probes` includes a raw fold, a full key, a folded formula cell under both aggregations, the
+two-dropped key `{_Measure=Revenue}`, the empty key and a group key. Review of PR 343 showed
+`probes` omitting formula cells, `_Measure` keys or raw folds left every test green.
+
+## an_edit_names_its_key_as_two_value_probes_and_a_fold
+
+`edit_probes` of a `ClearCell` names the cleared key three ways, and of an edit naming no key
+names nothing.
+
+## a_maintained_eager_equals_a_fresh_one_over_random_edit_sequences
+
+Clause 2 asks for a property test over a random edit sequence. A proptest (256 cases, up to four
+edits of five kinds over the hand-built model) runs `differential` with a candidate that rebuilds
+an `Eager` from scratch on every edit. It fails on the `Eager::apply`-skips-recompute fault, which
+is the property: maintaining in place equals building afresh.

crates/improvise-incremental/Cargo.toml

@@ -0,0 +1,15 @@
+[package]
+name = "improvise-incremental"
+version = "0.1.0"
+edition = "2024"
+license = "Apache-2.0"
+description = "The seam between improvise-core and the incremental circuit: the Derived trait, the Eager oracle and the differential harness (ADR 009 clause 2)."
+
+# ADR 009 clause 2: depends on improvise-core, never the other way round. The
+# `zset` edge arrives with the first backend that uses it (step 3), not before.
+[dependencies]
+improvise-core = { path = "../improvise-core" }
+
+[dev-dependencies]
+improvise-io = { path = "../improvise-io" }
+proptest = "1"

crates/improvise-incremental/src/eager.rs

@@ -0,0 +1,46 @@
+//! Today's evaluator behind the trait. Temporary (ADR 009 clause 2).
+
+use crate::{Derived, Edit, Maintained};
+use improvise_core::model::cell::{CellKey, CellValue};
+use improvise_core::model::{Aggregation, Model};
+
+/// A model plus the None categories its formulas were last recomputed under.
+/// It adds no logic: every answer is a call into `Model`.
+#[derive(Debug, Clone)]
+pub struct Eager {
+    model: Model,
+    none_cats: Vec<String>,
+}
+
+impl Eager {
+    pub fn new(mut model: Model, none_cats: Vec<String>) -> Self {
+        model.recompute_formulas(&none_cats);
+        Eager { model, none_cats }
+    }
+
+    pub fn model(&self) -> &Model {
+        &self.model
+    }
+}
+
+impl Derived for Eager {
+    fn value(&self, key: &CellKey, agg: Aggregation) -> Option<CellValue> {
+        self.model.evaluate_aggregated(key, agg)
+    }
+
+    fn raw_fold(&self, partial: &CellKey) -> Option<CellValue> {
+        match self.model.formula_for(partial) {
+            Some(_) => None,
+            None => self
+                .model
+                .evaluate_aggregated(partial, Aggregation::OverHidden),
+        }
+    }
+}
+
+impl Maintained for Eager {
+    fn apply(&mut self, edit: &Edit) {
+        edit.apply(&mut self.model);
+        self.model.recompute_formulas(&self.none_cats);
+    }
+}

crates/improvise-incremental/src/edit.rs

@@ -0,0 +1,46 @@
+//! One mutation of a model, as data, so a sequence can be replayed on two backends.
+
+use improvise_core::formula::ast::{AggFunc, Formula};
+use improvise_core::model::Model;
+use improvise_core::model::cell::{CellKey, CellValue};
+
+#[derive(Debug, Clone)]
+pub enum Edit {
+    SetCell(CellKey, CellValue),
+    ClearCell(CellKey),
+    AddFormula(Formula),
+    RemoveFormula {
+        target: String,
+        target_category: String,
+    },
+    SetMeasureAgg {
+        measure: String,
+        func: AggFunc,
+    },
+}
+
+impl Edit {
+    /// The one place an edit becomes a call on the model.
+    pub fn apply(&self, model: &mut Model) {
+        match self {
+            Edit::SetCell(key, value) => model.set_cell(key.clone(), value.clone()),
+            Edit::ClearCell(key) => model.clear_cell(key),
+            Edit::AddFormula(formula) => model.add_formula(formula.clone()),
+            Edit::RemoveFormula {
+                target,
+                target_category,
+            } => model.remove_formula(target, target_category),
+            Edit::SetMeasureAgg { measure, func } => {
+                model.measure_agg.insert(measure.clone(), func.clone());
+            }
+        }
+    }
+
+    /// The key an edit names, if it names one: always probed after it.
+    pub fn key(&self) -> Option<&CellKey> {
+        match self {
+            Edit::SetCell(key, _) | Edit::ClearCell(key) => Some(key),
+            _ => None,
+        }
+    }
+}

crates/improvise-incremental/src/harness.rs

@@ -0,0 +1,195 @@
+//! The differential harness: one edit sequence, two backends, every probe after every step.
+
+use crate::{Derived, Eager, Edit};
+use improvise_core::model::cell::{CellKey, CellValue};
+use improvise_core::model::{Aggregation, Model};
+use std::collections::HashSet;
+use std::fmt;
+
+/// A backend that holds state of its own and is told each edit.
+pub trait Maintained: Derived {
+    fn apply(&mut self, edit: &Edit);
+}
+
+/// One question put to both backends.
+#[derive(Debug, Clone, PartialEq)]
+pub enum Probe {
+    Value(CellKey, Aggregation),
+    RawFold(CellKey),
+}
+
+impl Probe {
+    pub fn ask(&self, backend: &dyn Derived) -> Option<CellValue> {
+        match self {
+            Probe::Value(key, agg) => backend.value(key, *agg),
+            Probe::RawFold(partial) => backend.raw_fold(partial),
+        }
+    }
+}
+
+#[derive(Debug, Clone, PartialEq)]
+pub struct Divergence {
+    /// 0 is the model as built, `n` the state after edit `n`.
+    pub step: usize,
+    pub probe: Probe,
+    pub eager: Option<CellValue>,
+    pub candidate: Option<CellValue>,
+}
+
+impl fmt::Display for Divergence {
+    fn fmt(&self, f: &mut fmt::Formatter<'_>) -> fmt::Result {
+        write!(
+            f,
+            "divergence at step {}: {:?}: eager {:?} != candidate {:?}",
+            self.step, self.probe, self.eager, self.candidate
+        )
+    }
+}
+
+/// How many states and how many answers were compared: a run that compared
+/// nothing must be visible as such.
+#[derive(Debug, Clone, Copy, PartialEq, Eq)]
+pub struct Report {
+    pub steps: usize,
+    pub probes: usize,
+}
+
+/// Values agree when equal by float rules with every NaN one value, so a NaN
+/// answer is not a divergence from itself.
+pub fn same_value(a: &Option<CellValue>, b: &Option<CellValue>) -> bool {
+    match (a, b) {
+        (Some(CellValue::Number(x)), Some(CellValue::Number(y))) => {
+            x == y || (x.is_nan() && y.is_nan())
+        }
+        _ => a == b,
+    }
+}
+
+/// The most coordinates a probed partial key drops from a stored key; the
+/// empty key is probed as well. A fold dropping more is not asked about.
+pub const MAX_DROPPED: usize = 3;
+
+/// The questions asked of a backend, once each, in the order first added.
+#[derive(Default)]
+struct Asked {
+    seen: HashSet<(CellKey, u8)>,
+    order: Vec<Probe>,
+}
+
+impl Asked {
+    fn extend(&mut self, probes: impl IntoIterator<Item = Probe>) {
+        for p in probes {
+            let tag = match &p {
+                Probe::Value(k, Aggregation::Exact) => (k.clone(), 0),
+                Probe::Value(k, Aggregation::OverHidden) => (k.clone(), 1),
+                Probe::RawFold(k) => (k.clone(), 2),
+            };
+            if self.seen.insert(tag) {
+                self.order.push(p);
+            }
+        }
+    }
+}
+
+fn all_three(key: CellKey) -> [Probe; 3] {
+    [
+        Probe::Value(key.clone(), Aggregation::Exact),
+        Probe::Value(key.clone(), Aggregation::OverHidden),
+        Probe::RawFold(key),
+    ]
+}
+
+/// Every key `key` keeps after dropping at most `MAX_DROPPED` coordinates.
+fn sub_partials(key: &CellKey) -> impl Iterator<Item = CellKey> + '_ {
+    let n = key.0.len();
+    (0..1u64 << n)
+        .filter(|mask| mask.count_ones() as usize <= MAX_DROPPED)
+        .map(move |mask| {
+            let kept = (0..n)
+                .filter(|i| mask >> i & 1 == 0)
+                .map(|i| key.0[i].clone());
+            CellKey::new(kept.collect())
+        })
+}
+
+/// Every question worth asking of `model`; the bound and the key set are
+/// in `context/code/improvise-incremental.md`.
+pub fn probes(model: &Model) -> Vec<Probe> {
+    let stored: Vec<CellKey> = model.data.iter_cells().map(|(k, _)| k).collect();
+    let grouped = stored.iter().flat_map(|k| {
+        k.0.iter().filter_map(|(cat, item)| {
+            let group = model.category(cat)?.items.get(item)?.group.clone()?;
+            Some(k.clone().with(cat, group))
+        })
+    });
+    let base: Vec<CellKey> = stored.iter().cloned().chain(grouped).collect();
+    let partials = base
+        .iter()
+        .flat_map(sub_partials)
+        .chain(std::iter::once(CellKey::new(vec![])));
+    let mut asked = Asked::default();
+    for key in partials {
+        let formula_cells = model
+            .formulas()
+            .iter()
+            .map(|f| key.clone().with(&f.target_category, &f.target))
+            .collect::<Vec<_>>();
+        asked.extend(all_three(key));
+        asked.extend(formula_cells.into_iter().flat_map(all_three));
+    }
+    asked.order
+}
+
+/// What an edit names: its key, asked all three ways, after the edit.
+pub fn edit_probes(edit: &Edit) -> Vec<Probe> {
+    edit.key()
+        .cloned()
+        .into_iter()
+        .flat_map(all_three)
+        .collect()
+}
+
+fn compare(
+    step: usize,
+    eager: &Eager,
+    candidate: &dyn Derived,
+    asked: &Asked,
+) -> Result<usize, Divergence> {
+    for probe in &asked.order {
+        let (want, got) = (probe.ask(eager), probe.ask(candidate));
+        if !same_value(&want, &got) {
+            return Err(Divergence {
+                step,
+                probe: probe.clone(),
+                eager: want,
+                candidate: got,
+            });
+        }
+    }
+    Ok(asked.order.len())
+}
+
+/// Runs `edits` on `candidate` and on `Eager`, comparing every probe ever
+/// asked (so a removed formula stays asked about) at each step. `candidate` is built from `model` with the same `none_cats`.
+pub fn differential<C: Maintained>(
+    model: &Model,
+    none_cats: &[String],
+    mut candidate: C,
+    edits: &[Edit],
+) -> Result<Report, Divergence> {
+    let mut eager = Eager::new(model.clone(), none_cats.to_vec());
+    let mut asked = Asked::default();
+    asked.extend(probes(eager.model()));
+    let mut probes_run = compare(0, &eager, &candidate, &asked)?;
+    for (n, edit) in edits.iter().enumerate() {
+        eager.apply(edit);
+        candidate.apply(edit);
+        asked.extend(probes(eager.model()));
+        asked.extend(edit_probes(edit));
+        probes_run += compare(n + 1, &eager, &candidate, &asked)?;
+    }
+    Ok(Report {
+        steps: edits.len() + 1,
+        probes: probes_run,
+    })
+}

crates/improvise-incremental/src/lib.rs

@@ -0,0 +1,27 @@
+//! The plug: what the evaluator reads, and the oracle that answers it today.
+//! Reasoning: `context/code/improvise-incremental.md`.
+
+mod eager;
+mod edit;
+mod harness;
+
+pub use eager::Eager;
+pub use edit::Edit;
+pub use harness::{
+    Divergence, MAX_DROPPED, Maintained, Probe, Report, differential, edit_probes, probes,
+    same_value,
+};
+
+use improvise_core::model::Aggregation;
+use improvise_core::model::cell::{CellKey, CellValue};
+
+/// The two things the evaluator reads (ADR 009 clause 2).
+pub trait Derived {
+    /// The value at `key`: the formula result when a formula owns it, else the
+    /// cell as stored or folded over what `agg` hides. `Model::evaluate_aggregated`.
+    fn value(&self, key: &CellKey, agg: Aggregation) -> Option<CellValue>;
+
+    /// The raw fold of the stored cells that match `partial`, by the measure's
+    /// aggregation. Never a formula: `None` for a partial naming a formula target.
+    fn raw_fold(&self, partial: &CellKey) -> Option<CellValue>;
+}

crates/improvise-incremental/tests/oracle.rs

@@ -0,0 +1,633 @@
+//! `Eager` against the evaluator, and the harness against wrong backends.
+//! Evidence: `context/test-evidence/improvise-incremental.md`.
+
+use improvise_core::formula::ast::AggFunc;
+use improvise_core::formula::parse_formula;
+use improvise_core::model::cell::{CellKey, CellValue};
+use improvise_core::model::{Aggregation, Model};
+use improvise_core::view::Axis;
+use improvise_incremental::{
+    Derived, Divergence, Eager, Edit, Maintained, Probe, differential, probes, same_value,
+};
+use proptest::prelude::*;
+use std::path::Path;
+
+fn key(region: &str, product: &str, measure: &str) -> CellKey {
+    CellKey::new(vec![
+        ("Region".into(), region.into()),
+        ("Product".into(), product.into()),
+        ("_Measure".into(), measure.into()),
+    ])
+}
+
+fn partial(product: &str, measure: &str) -> CellKey {
+    CellKey::new(vec![
+        ("Product".into(), product.into()),
+        ("_Measure".into(), measure.into()),
+    ])
+}
+
+fn num(n: f64) -> Option<CellValue> {
+    Some(CellValue::Number(n))
+}
+
+fn text(s: &str) -> Option<CellValue> {
+    Some(CellValue::Text(s.into()))
+}
+
+fn mixed() -> Option<CellValue> {
+    Some(CellValue::Error("mixed".into()))
+}
+
+/// Region is the None category. Revenue and Cost are numbers; Note is text,
+/// unanimous under A and conflicting under B.
+fn hand_model() -> Model {
+    let mut m = Model::new("hand");
+    for (cat, items) in [("Region", ["East", "West"]), ("Product", ["A", "B"])] {
+        m.add_category(cat).unwrap();
+        for item in items {
+            m.category_mut(cat).unwrap().add_item(item);
+        }
+    }
+    for measure in ["Revenue", "Cost", "Note"] {
+        m.category_mut("_Measure").unwrap().add_item(measure);
+    }
+    let rows = [
+        ("East", "A", 10.0, 4.0, "n", "n"),
+        ("West", "A", 5.0, 2.0, "n", "n"),
+        ("East", "B", 7.0, 3.0, "x", "x"),
+        ("West", "B", 1.0, 1.0, "y", "y"),
+    ];
+    for (r, p, rev, cost, note, _) in rows {
+        m.set_cell(key(r, p, "Revenue"), CellValue::Number(rev));
+        m.set_cell(key(r, p, "Cost"), CellValue::Number(cost));
+        m.set_cell(key(r, p, "Note"), CellValue::Text(note.into()));
+    }
+    m.add_formula(parse_formula("Profit = Revenue - Cost", "_Measure").unwrap());
+    m
+}
+
+fn hand_eager() -> Eager {
+    Eager::new(hand_model(), vec!["Region".into()])
+}
+
+fn hand_edits() -> Vec<Edit> {
+    vec![
+        Edit::SetCell(key("East", "A", "Revenue"), CellValue::Number(20.0)),
+        Edit::SetMeasureAgg {
+            measure: "Revenue".into(),
+            func: AggFunc::Max,
+        },
+        Edit::ClearCell(key("West", "A", "Revenue")),
+        Edit::SetCell(key("West", "B", "Revenue"), CellValue::Text("oops".into())),
+        Edit::AddFormula(parse_formula("Double = Revenue * 2", "_Measure").unwrap()),
+        Edit::RemoveFormula {
+            target: "Profit".into(),
+            target_category: "_Measure".into(),
+        },
+    ]
+}
+
+#[test]
+fn eager_raw_fold_sums_by_default() {
+    assert_eq!(hand_eager().raw_fold(&partial("A", "Revenue")), num(15.0));
+}
+
+#[test]
+fn eager_raw_fold_follows_the_measures_aggregation() {
+    let mut eager = hand_eager();
+    eager.apply(&Edit::SetMeasureAgg {
+        measure: "Revenue".into(),
+        func: AggFunc::Max,
+    });
+    assert_eq!(eager.raw_fold(&partial("A", "Revenue")), num(10.0));
+    assert_eq!(eager.raw_fold(&partial("A", "Cost")), num(6.0));
+}
+
+#[test]
+fn eager_raw_fold_of_text_is_unanimous_or_mixed() {
+    let eager = hand_eager();
+    assert_eq!(eager.raw_fold(&partial("A", "Note")), text("n"));
+    assert_eq!(eager.raw_fold(&partial("B", "Note")), mixed());
+}
+
+#[test]
+fn eager_value_reads_a_formula_exactly_and_folded() {
+    let eager = hand_eager();
+    assert_eq!(
+        eager.value(&key("East", "A", "Profit"), Aggregation::Exact),
+        num(6.0)
+    );
+    assert_eq!(
+        eager.value(&partial("A", "Profit"), Aggregation::OverHidden),
+        num(9.0)
+    );
+}
+
+#[test]
+fn eager_follows_an_edit_to_the_cell_a_fold_reads() {
+    let mut eager = hand_eager();
+    eager.apply(&Edit::SetCell(
+        key("East", "A", "Revenue"),
+        CellValue::Number(20.0),
+    ));
+    assert_eq!(eager.raw_fold(&partial("A", "Revenue")), num(25.0));
+    assert_eq!(
+        eager.value(&partial("A", "Profit"), Aggregation::OverHidden),
+        num(19.0)
+    );
+}
+
+#[test]
+fn eager_numbers_among_text_are_mixed() {
+    let mut eager = hand_eager();
+    eager.apply(&Edit::SetCell(
+        key("West", "B", "Revenue"),
+        CellValue::Text("oops".into()),
+    ));
+    assert_eq!(eager.raw_fold(&partial("B", "Revenue")), mixed());
+}
+
+fn corpus() -> Vec<(String, Model, Vec<String>)> {
+    let root = Path::new(env!("CARGO_MANIFEST_DIR")).join("../..");
+    let mut out = Vec::new();
+    for file in ["examples/demo.improv", "web/demo.improv"] {
+        let wb = improvise_io::persistence::load(&root.join(file)).unwrap();
+        let mut seen: Vec<Vec<String>> = Vec::new();
+        for (name, view) in &wb.views {
+            let none: Vec<String> = view
+                .categories_on(Axis::None)
+                .into_iter()
+                .map(String::from)
+                .collect();
+            if !seen.contains(&none) {
+                seen.push(none.clone());
+                out.push((format!("{file}:{name}"), wb.model.clone(), none));
+            }
+        }
+    }
+    out.push(("hand".into(), hand_model(), vec!["Region".into()]));
+    out
+}
+
+/// Edits built from the model's own first cell: overwrite, text, clear, a new
+/// record, a new aggregation, and the first formula removed then restored.
+fn edits_for(model: &Model) -> Vec<Edit> {
+    let Some((first, _)) = model.data.iter_cells().next() else {
+        return vec![];
+    };
+    let (last_cat, _) = first.0.last().unwrap().clone();
+    let measure = first.get("_Measure").map(String::from);
+    let fresh = first.clone().with(last_cat, "Zz-new");
+    let mut edits = vec![
+        Edit::SetCell(first.clone(), CellValue::Number(7.5)),
+        Edit::SetCell(first.clone(), CellValue::Text("t".into())),
+        Edit::SetCell(fresh.clone(), CellValue::Number(3.0)),
+        Edit::ClearCell(first),
+    ];
+    edits.extend(measure.map(|m| Edit::SetMeasureAgg {
+        measure: m,
+        func: AggFunc::Max,
+    }));
+    if let Some(f) = model.formulas().first() {
+        edits.push(Edit::RemoveFormula {
+            target: f.target.clone(),
+            target_category: f.target_category.clone(),
+        });
+        edits.push(Edit::AddFormula(f.clone()));
+    }
+    edits.push(Edit::ClearCell(fresh));
+    edits
+}
+
+#[test]
+fn eager_matches_the_evaluator_on_the_shipped_documents() {
+    for (name, model, none) in corpus() {
+        let eager = Eager::new(model.clone(), none.clone());
+        let mut direct = model.clone();
+        direct.recompute_formulas(&none);
+        let asked = probes(eager.model());
+        assert!(!asked.is_empty(), "{name}: no probes");
+        for probe in asked {
+            let want = match &probe {
+                Probe::Value(k, a) => direct.evaluate_aggregated(k, *a),
+                Probe::RawFold(k) if direct.formula_for(k).is_some() => None,
+                Probe::RawFold(k) => direct.evaluate_aggregated(k, Aggregation::OverHidden),
+            };
+            assert_eq!(probe.ask(&eager), want, "{name}: {probe:?}");
+        }
+    }
+}
+
+#[test]
+fn eager_agrees_with_itself_over_every_corpus_edit_sequence() {
+    let mut files_done: Vec<String> = Vec::new();
+    for (name, model, none) in corpus() {
+        let file = name.split(':').next().unwrap().to_string();
+        if files_done.contains(&file) {
+            continue;
+        }
+        files_done.push(file);
+        let mut edits = edits_for(&model);
+        // Probes grow with the cells squared-ish, and a debug build pays for it.
+        if model.data.iter_cells().count() > 40 {
+            edits.truncate(4);
+        }
+        let report = differential(
+            &model,
+            &none,
+            Eager::new(model.clone(), none.clone()),
+            &edits,
+        )
+        .unwrap_or_else(|d| panic!("{name}: {d}"));
+        assert_eq!(report.steps, edits.len() + 1, "{name}");
+        assert!(report.probes > 0, "{name}");
+    }
+}
+
+fn grouped_model() -> Model {
+    let mut m = Model::new("grouped");
+    m.add_category("Region").unwrap();
+    m.add_category("Product").unwrap();
+    m.category_mut("Region")
+        .unwrap()
+        .add_group(improvise_core::model::category::Group::new("Coastal"));
+    let region = m.category_mut("Region").unwrap();
+    region.add_item_in_group("East", "Coastal");
+    region.add_item_in_group("West", "Coastal");
+    region.add_item("Inland");
+    m.category_mut("Product").unwrap().add_item("A");
+    m.category_mut("_Measure").unwrap().add_item("Revenue");
+    for (r, v) in [("East", 10.0), ("West", 5.0), ("Inland", 2.0)] {
+        m.set_cell(key(r, "A", "Revenue"), CellValue::Number(v));
+    }
+    m
+}
+
+fn coastal() -> CellKey {
+    key("Coastal", "A", "Revenue")
+}
+
+/// A wrong backend: an `Eager` told every edit, answering one thing wrongly.
+#[derive(Clone, Copy)]
+enum Fault {
+    IgnoresAggregation,
+    IgnoresMeasureAggregation,
+    GoesStaleAfterTwoEdits,
+    IgnoresClear,
+    WrongFoldedFormula,
+    IgnoresRemoveFormula,
+    WrongWhenTwoAreDropped,
+    RawFoldReturnsFormula,
+    WrongOnAGroup,
+}
+
+struct Rival {
+    inner: Eager,
+    fault: Fault,
+    seen: usize,
+}
+
+impl Rival {
+    fn over(inner: Eager, fault: Fault) -> Self {
+        Rival {
+            inner,
+            fault,
+            seen: 0,
+        }
+    }
+
+    fn of(fault: Fault) -> Self {
+        Self::over(hand_eager(), fault)
+    }
+}
+
+impl Derived for Rival {
+    fn value(&self, k: &CellKey, agg: Aggregation) -> Option<CellValue> {
+        let wrong = match self.fault {
+            Fault::WrongFoldedFormula => {
+                *k == partial("A", "Profit") && agg == Aggregation::OverHidden
+            }
+            Fault::WrongWhenTwoAreDropped => *k == only_revenue(),
+            Fault::WrongOnAGroup => *k == coastal() && agg == Aggregation::Exact,
+            _ => false,
+        };
+        match (wrong, self.fault) {
+            (true, _) => num(-999.0),
+            (_, Fault::IgnoresAggregation) => self.inner.value(k, Aggregation::Exact),
+            _ => self.inner.value(k, agg),
+        }
+    }
+
+    fn raw_fold(&self, p: &CellKey) -> Option<CellValue> {
+        match self.fault {
+            Fault::WrongWhenTwoAreDropped if *p == only_revenue() => num(-999.0),
+            Fault::RawFoldReturnsFormula => self.inner.value(p, Aggregation::OverHidden),
+            _ => self.inner.raw_fold(p),
+        }
+    }
+}
+
+impl Maintained for Rival {
+    fn apply(&mut self, edit: &Edit) {
+        self.seen += 1;
+        let skip = match (self.fault, edit) {
+            (Fault::IgnoresMeasureAggregation, Edit::SetMeasureAgg { .. }) => true,
+            (Fault::GoesStaleAfterTwoEdits, _) => self.seen > 2,
+            (Fault::IgnoresClear, Edit::ClearCell(_)) => true,
+            (Fault::IgnoresRemoveFormula, Edit::RemoveFormula { .. }) => true,
+            _ => false,
+        };
+        if !skip {
+            self.inner.apply(edit);
+        }
+    }
+}
+
+fn only_revenue() -> CellKey {
+    CellKey::new(vec![("_Measure".into(), "Revenue".into())])
+}
+
+fn measure_of(probe: &Probe) -> Option<&str> {
+    match probe {
+        Probe::Value(k, _) | Probe::RawFold(k) => k.get("_Measure"),
+    }
+}
+
+fn run_rival(fault: Fault) -> Result<improvise_incremental::Report, Divergence> {
+    differential(
+        &hand_model(),
+        &["Region".to_string()],
+        Rival::of(fault),
+        &hand_edits(),
+    )
+}
+
+#[test]
+fn the_harness_passes_a_backend_that_is_right() {
+    let report = differential(
+        &hand_model(),
+        &["Region".to_string()],
+        hand_eager(),
+        &hand_edits(),
+    )
+    .unwrap();
+    assert_eq!(report.steps, hand_edits().len() + 1);
+}
+
+#[test]
+fn the_harness_catches_a_backend_that_ignores_the_aggregation() {
+    let d = run_rival(Fault::IgnoresAggregation).unwrap_err();
+    assert_eq!(d.step, 0);
+    assert_eq!(
+        d.probe,
+        Probe::Value(key("East", "A", "Profit"), Aggregation::OverHidden)
+    );
+    assert_eq!((d.eager, d.candidate), (None, num(6.0)));
+}
+
+#[test]
+fn the_harness_catches_a_backend_that_ignores_the_measure_aggregation() {
+    let d = run_rival(Fault::IgnoresMeasureAggregation).unwrap_err();
+    assert_eq!(d.step, 2, "{d}");
+    assert_eq!(measure_of(&d.probe), Some("Revenue"), "{d}");
+}
+
+#[test]
+fn the_harness_catches_a_backend_that_goes_stale_after_two_edits() {
+    let d = run_rival(Fault::GoesStaleAfterTwoEdits).unwrap_err();
+    assert_eq!(d.step, 3, "{d}");
+    assert_eq!(measure_of(&d.probe), Some("Revenue"), "{d}");
+}
+
+#[test]
+fn the_harness_catches_a_backend_that_ignores_a_clear() {
+    let d = run_rival(Fault::IgnoresClear).unwrap_err();
+    assert_eq!(d.step, 3, "{d}");
+    assert_eq!(measure_of(&d.probe), Some("Revenue"), "{d}");
+    assert!(d.to_string().starts_with("divergence at step 3:"), "{d}");
+}
+
+#[test]
+fn the_harness_catches_a_wrong_folded_formula_value() {
+    let d = run_rival(Fault::WrongFoldedFormula).unwrap_err();
+    assert_eq!(d.step, 0);
+    assert_eq!(
+        d.probe,
+        Probe::Value(partial("A", "Profit"), Aggregation::OverHidden)
+    );
+    assert_eq!((d.eager, d.candidate), (num(9.0), num(-999.0)));
+}
+
+#[test]
+fn the_harness_catches_a_backend_that_keeps_answering_for_a_removed_formula() {
+    let d = run_rival(Fault::IgnoresRemoveFormula).unwrap_err();
+    assert_eq!(d.step, hand_edits().len(), "{d}");
+    assert_eq!(measure_of(&d.probe), Some("Profit"), "{d}");
+    assert!(d.eager.is_none() && d.candidate.is_some(), "{d}");
+}
+
+#[test]
+fn the_harness_catches_a_fault_that_only_shows_after_two_coordinates_are_dropped() {
+    let d = run_rival(Fault::WrongWhenTwoAreDropped).unwrap_err();
+    assert_eq!(d.step, 0);
+    assert_eq!(d.probe, Probe::Value(only_revenue(), Aggregation::Exact));
+    assert_eq!(d.candidate, num(-999.0));
+}
+
+#[test]
+fn the_harness_catches_a_raw_fold_that_returns_a_formula() {
+    let d = run_rival(Fault::RawFoldReturnsFormula).unwrap_err();
+    assert_eq!(d.step, 0);
+    assert!(matches!(d.probe, Probe::RawFold(_)), "{d}");
+    assert_eq!(measure_of(&d.probe), Some("Profit"), "{d}");
+    assert!(d.eager.is_none() && d.candidate.is_some(), "{d}");
+}
+
+#[test]
+fn the_harness_catches_a_wrong_group_fold() {
+    let eager = Eager::new(grouped_model(), vec![]);
+    let d = differential(
+        &grouped_model(),
+        &[],
+        Rival::over(eager, Fault::WrongOnAGroup),
+        &[],
+    )
+    .unwrap_err();
+    assert_eq!(d.probe, Probe::Value(coastal(), Aggregation::Exact));
+    assert_eq!((d.eager, d.candidate), (num(15.0), num(-999.0)));
+}
+
+#[test]
+fn eager_folds_a_group_it_is_asked_about() {
+    let eager = Eager::new(grouped_model(), vec![]);
+    assert_eq!(eager.value(&coastal(), Aggregation::Exact), num(15.0));
+}
+
+#[test]
+fn eager_raw_fold_is_never_a_formula() {
+    let eager = hand_eager();
+    assert_eq!(
+        eager.value(&partial("A", "Profit"), Aggregation::OverHidden),
+        num(9.0)
+    );
+    assert_eq!(eager.raw_fold(&partial("A", "Profit")), None);
+}
+
+#[test]
+fn eager_add_and_remove_formula_change_what_a_key_reads() {
+    let mut eager = hand_eager();
+    let k = key("East", "A", "Double");
+    assert_eq!(eager.value(&k, Aggregation::Exact), None);
+    eager.apply(&Edit::AddFormula(
+        parse_formula("Double = Revenue * 2", "_Measure").unwrap(),
+    ));
+    assert_eq!(eager.value(&k, Aggregation::Exact), num(20.0));
+    eager.apply(&Edit::RemoveFormula {
+        target: "Double".into(),
+        target_category: "_Measure".into(),
+    });
+    assert_eq!(eager.value(&k, Aggregation::Exact), None);
+}
+
+#[test]
+fn eager_clear_cell_leaves_the_key_absent() {
+    let mut eager = hand_eager();
+    let k = key("East", "A", "Revenue");
+    eager.apply(&Edit::ClearCell(k.clone()));
+    assert_eq!(eager.value(&k, Aggregation::Exact), None);
+    assert_eq!(eager.model().get_cell(&k), None);
+}
+
+#[test]
+fn same_value_follows_the_float_rules_and_is_exact_elsewhere() {
+    let n = |x: f64| num(x);
+    assert!(same_value(&n(f64::NAN), &n(f64::NAN)));
+    assert!(same_value(&n(-0.0), &n(0.0)));
+    assert!(!same_value(&n(1.0), &n(1.000_000_000_000_000_2)));
+    assert!(!same_value(&n(1.0), &n(f64::NAN)));
+    assert!(same_value(&text("a"), &text("a")));
+    assert!(!same_value(&text("a"), &text("b")));
+    let err = |s: &str| Some(CellValue::Error(s.into()));
+    assert!(same_value(&err("mixed"), &err("mixed")));
+    assert!(!same_value(&err("mixed"), &err("circular")));
+    assert!(!same_value(&None, &n(0.0)));
+    assert!(same_value(&None, &None));
+}
+
+#[test]
+fn probes_cover_folds_formulas_measures_and_groups() {
+    let hand = probes(&hand_model());
+    let has = |p: Probe| hand.contains(&p);
+    assert!(has(Probe::RawFold(partial("A", "Revenue"))));
+    assert!(has(Probe::Value(
+        key("East", "A", "Revenue"),
+        Aggregation::Exact
+    )));
+    assert!(has(Probe::Value(
+        partial("A", "Profit"),
+        Aggregation::Exact
+    )));
+    assert!(has(Probe::Value(
+        partial("A", "Profit"),
+        Aggregation::OverHidden
+    )));
+    assert!(has(Probe::Value(only_revenue(), Aggregation::OverHidden)));
+    assert!(has(Probe::RawFold(CellKey::new(vec![]))));
+    let grouped = probes(&grouped_model());
+    assert!(grouped.contains(&Probe::Value(coastal(), Aggregation::Exact)));
+}
+
+#[test]
+fn an_edit_names_its_key_as_two_value_probes_and_a_fold() {
+    let k = key("East", "A", "Revenue");
+    let asked = improvise_incremental::edit_probes(&Edit::ClearCell(k.clone()));
+    assert!(asked.contains(&Probe::Value(k.clone(), Aggregation::Exact)));
+    assert!(asked.contains(&Probe::Value(k.clone(), Aggregation::OverHidden)));
+    assert!(asked.contains(&Probe::RawFold(k)));
+    let none = improvise_incremental::edit_probes(&Edit::SetMeasureAgg {
+        measure: "Revenue".into(),
+        func: AggFunc::Max,
+    });
+    assert!(none.is_empty());
+}
+
+/// An `Eager` rebuilt from scratch on every edit: maintaining one in place
+/// must give the same answers as building it afresh.
+struct Fresh {
+    model: Model,
+    none: Vec<String>,
+    eager: Eager,
+}
+
+impl Derived for Fresh {
+    fn value(&self, k: &CellKey, agg: Aggregation) -> Option<CellValue> {
+        self.eager.value(k, agg)
+    }
+
+    fn raw_fold(&self, p: &CellKey) -> Option<CellValue> {
+        self.eager.raw_fold(p)
+    }
+}
+
+impl Maintained for Fresh {
+    fn apply(&mut self, edit: &Edit) {
+        edit.apply(&mut self.model);
+        self.eager = Eager::new(self.model.clone(), self.none.clone());
+    }
+}
+
+fn any_key() -> impl Strategy<Value = CellKey> {
+    (
+        prop::sample::select(vec!["East", "West"]),
+        prop::sample::select(vec!["A", "B"]),
+        prop::sample::select(vec!["Revenue", "Cost", "Note"]),
+    )
+        .prop_map(|(r, p, m)| key(r, p, m))
+}
+
+fn any_value() -> impl Strategy<Value = CellValue> {
+    prop_oneof![
+        (-4i32..5).prop_map(|n| CellValue::Number(f64::from(n))),
+        Just(CellValue::Number(-0.0)),
+        prop::sample::select(vec!["n", "x"]).prop_map(|t| CellValue::Text(t.into())),
+    ]
+}
+
+fn any_edit() -> impl Strategy<Value = Edit> {
+    prop_oneof![
+        (any_key(), any_value()).prop_map(|(k, v)| Edit::SetCell(k, v)),
+        any_key().prop_map(Edit::ClearCell),
+        prop::sample::select(vec!["Profit = Revenue - Cost", "Double = Revenue * 2"])
+            .prop_map(|raw| Edit::AddFormula(parse_formula(raw, "_Measure").unwrap())),
+        prop::sample::select(vec!["Profit", "Double"]).prop_map(|t| Edit::RemoveFormula {
+            target: t.into(),
+            target_category: "_Measure".into(),
+        }),
+        (
+            prop::sample::select(vec!["Revenue", "Cost"]),
+            prop::sample::select(vec![AggFunc::Sum, AggFunc::Max, AggFunc::Min, AggFunc::Avg]),
+        )
+            .prop_map(|(m, func)| Edit::SetMeasureAgg {
+                measure: m.into(),
+                func,
+            }),
+    ]
+}
+
+proptest! {
+    #[test]
+    fn a_maintained_eager_equals_a_fresh_one_over_random_edit_sequences(
+        edits in prop::collection::vec(any_edit(), 0..4)
+    ) {
+        let model = hand_model();
+        let none = vec!["Region".to_string()];
+        let fresh = Fresh {
+            model: model.clone(),
+            none: none.clone(),
+            eager: Eager::new(model.clone(), none.clone()),
+        };
+        let run = differential(&model, &none, fresh, &edits);
+        prop_assert!(run.is_ok(), "{}", run.unwrap_err());
+    }
+}

nix/ci.nix

@@ -50,6 +50,8 @@
     "numtower"
     # ADR 009 clause 1: std-only; nothing depends on it yet.
     "zset"
+    # ADR 009 clause 2: the Derived trait, Eager and the differential harness.
+    "improvise-incremental"
   ];
   pFlags = crates: lib.concatMapStringsSep " " (c: "-p ${c}") crates;
 

scripts/build-doc-site.mjs

@@ -69,6 +69,7 @@ const SECTIONS = [
       ["context/code/gp.md", "code/gp", "gp-tree and improvise-gp"],
       ["context/code/numtower.md", "code/numtower", "numtower, the numeric tower"],
       ["context/code/zset.md", "code/zset", "zset, the Z-set group"],
+      ["context/code/improvise-incremental.md", "code/improvise-incremental", "improvise-incremental, the plug"],
       ["context/code/kb-tool.md", "code/kb-tool", "The kb tool"],
       ["context/code/tooling.md", "code/tooling", "The repository's own checkers"],
     ],
@@ -89,6 +90,7 @@ const SECTIONS = [
       ["context/test-evidence/gp.md", "test-evidence/gp", "gp-tree and improvise-gp"],
       ["context/test-evidence/numtower.md", "test-evidence/numtower", "numtower"],
       ["context/test-evidence/zset.md", "test-evidence/zset", "zset"],
+      ["context/test-evidence/improvise-incremental.md", "test-evidence/improvise-incremental", "improvise-incremental"],
       ["context/test-evidence/tooling.md", "test-evidence/tooling", "The repository's own gates"],
       ["context/test-evidence/layout-cost.md", "test-evidence/layout-cost", "Layout and keypress cost"],
       ["context/test-evidence/scale-bisect.md", "test-evidence/scale-bisect", "Scale bisect"],