docs(adr): ADR 009 incremental evaluation (proposed) (improvise-felo.4)

An in-house DBSP core as a problem-agnostic crate, plugged in behind a trait in improvise-core, with the eager evaluator kept as the oracle. Adds examples/retraction_drift.rs, which measures f64 retraction drift against the eager fold and the exact decimal sum. Co-Authored-By: Claude Opus 5.5 (1M context) <noreply@anthropic.com> Claude-Session: https://claude.ai/code/session_01VdfEGXA7aJ6ftMsCc9PJze
2026-09-24 20:14:37 -07:00
parent 57d385e155
commit 322875b30a
3 changed files with 804 additions and 0 deletions
@@ -0,0 +1,612 @@
 # ADR 009 — Incremental evaluation: an in-house DBSP core, plugged in behind a trait
 **Status:** proposed. Only the user accepts an ADR. The numbered questions at the end
 are theirs to answer on the PR. ·
 **Ticket:** improvise-felo.4 ·
 **Decision from:** the user, 2026-09-25 (below) ·
 **Builds on:** ADR 001 (the record tiers), ADR 003 (live-backed models) ·
 **Relates to:** ADR 005 (exact decimals, improvise-l2b8, no file yet), ADR 008 (the
 virtualized grid, PR #308, which is revised to assume this ADR) ·
 **Governed by:** `context/design-principles.md` §3 and §5
 **Numbering.** ADR 005 and 006 are claimed by improvise-l2b8 and improvise-ilvl and have
 no file yet. 007 is merged, and 008 is PR #308. 009 is the next free number. No bead and
 no open PR claimed it when this was written.
 **Citations.** Every `file:line` below is at `gh/main` `57d385e1`. Line numbers are
 dated, so re-derive them before citing this document elsewhere. "ADR 008 clause N" means
 revision 2 of `context/adr/008-virtualized-grid.md` on PR #308.
 ## The decision this ADR writes down
 The user pointed at a teaching implementation of the DBSP paper,
 [brurucy/dbsp-from-scratch](https://github.com/brurucy/dbsp-from-scratch/blob/master/dbsp_paper_walkthrough_implementation.ipynb),
 as a way to evaluate formulas so that data can stream. The notebook builds, in order:
 - abelian groups;
 - streams, with `Delay` (z⁻¹), `Differentiate` and `Integrate`;
 - Z-sets, which are maps from element to an integer weight;
 - lifted and doubly-lifted joins, and a delta join that keeps less state;
 - `distinct` through the `H` function over an integrated state;
 - recursion by nested streams, shown on graph reachability.
 The user then decided:
 > "I think doing our own implementation of the core of dbsp as a crate we can plugin is
 > probably dieal [sic] here. Write the ADR and Update ADR 008 to assume the decisions in
 > that one"
 >
 > — the user, 2026-09-25, recorded on improvise-felo.4
 So the choice between Feldera's crate and our own is already made (see Alternatives for
 what was checked). This ADR says what "the core of dbsp" is for improvise, where it
 plugs in, and what it may not change.
 ## Context
 ### Evaluation today is a from-scratch fold, rerun after every batch
 - **Every batch recomputes every formula cell.** `App::apply_effects`
  (`crates/improvise-command/src/ui/app.rs:989`) ends in `rebuild_layout` (`:880-891`).
  That calls `Model::recompute_formulas` (`crates/improvise-core/src/model/types.rs:971-1030`).
  It clears `formula_cache`, rebuilds the stem set from every stored cell (`:986-997`),
  and iterates `stem × formula` to a fixed point bounded by `MAX_EVAL_DEPTH = 16`
  (`:699`, `:1001-1022`). A cursor move and a cell write pay the same.
 - **Raw aggregation scans the matching cells on every read.** `evaluate_unfolded`
  (`types.rs:837-845`) folds `DataStore::matching_values` through
  `aggregate_cell_values` (`:30-42`). `fold_stored` (`:918-930`) does the same for a
  collapsed group, through `spanned_values` (`crates/improvise-core/src/model/cell.rs:445`).
 - **`formula_cache` holds one aggregation shape at a time.** It is keyed by cell and
  computed for one `none_cats` list. A session on another view with a different None
  axis gets a *cloned model* recomputed for its own list (`rederived_for`,
  `crates/improvise-command/src/ui/project.rs:195-210`).
 - **A formula total with an aggregate inside walks a cross product.** `contexts_of`
  (`types.rs:905-916`) calls `Expansion::members` (`:201-213`), which materializes every
  combination of the spanned categories' items. ADR 008 clause 5 names this as the one
  O(grid) path left in totals.
 - **Two of the record tiers are observed by scanning the store.** `record_fingerprints`
  (`app.rs:254-264`) hashes every cell before and after a cell-writing batch, and
  `document_content` (`app.rs:165-178`) does the same for the dirty flag. Both are
  O(cells) per batch, whatever the batch wrote.
 ### What an incremental evaluator must not change
 These rules come from the repo map and `context/code/core.md`. Each one is a place an
 incremental evaluator could quietly disagree with the eager one.
 - **Gotcha 7, text unanimity.** `aggregate_cell_values` checks the all-numeric branch
  first. Otherwise one distinct value is that value, and anything else is
  `Error("mixed")`. `Count` of a lone number is `1`, not the number.
 - **Gotcha 9 and core.md §3, circularity.** A cell still moving after 16 passes is
  written as `Error("circular")` (improvise-7iww). **A chain that needs all sixteen
  passes is also reported circular**, because the fixed point can only confirm
  convergence with a pass that changes nothing. The direct evaluator agrees because its
  recursion depth is the same 16 (`types.rs:705-714`).
 - **Gotcha 17, one epsilon.** `FLOAT_EQ_EPSILON = 1e-10` (`types.rs:14`) is shared by
  `=`, `!=` and the div/0 guard, in both evaluators.
 - **Gotcha 18, ordering is correctness.** A `HashSet` index is for lookup, never for
  iteration. `SUM` and `AVG` drifted in the last bits when the store was walked in hash
  order (improvise-shyt), because f64 addition is not associative.
 - **Gotcha 40, the tiers are observed.** A write that lands the value already there
  bumps nothing. The record set is collected into a *set*, so a rewritten record counts
  once.
 ## Decision
 **A new, problem-agnostic workspace crate implements the DBSP core. improvise-core
 defines a trait for the derived state it reads. Today's evaluator is one implementation
 of that trait, and a circuit built on the new crate is the other. Both stay in the tree,
 and a differential test holds them equal.** Eleven clauses.
 ### 1. The crate: `zset` (name is question 1)
 Like `gp-tree`, it knows nothing about improvise. It has **no dependencies** beyond
 `std`, so it is wasm32-clean by construction.
 **What it contains:**
 - **`ZSet<K>`**: a map from `K: Ord + Clone` to a non-zero `i64` weight, with `add`,
  `neg` and `zero`. It forms an abelian group, and its laws are property-tested as the
  notebook's first cell does: commutativity, associativity, identity and inverse.
  Weights use checked arithmetic, so an overflow is a panic, not a wrap. A weight that
  reaches zero is removed, so equal Z-sets are equal as maps.
 - **A synchronous `Circuit`.** Operators are wired once, and `step` takes one input
  delta per source and returns one output delta per sink. There is one clock, one
  thread, and no scheduler.
 - **Stream operators:** `delay` (z⁻¹), `integrate` (I) and `differentiate` (D), with
  I∘D = D∘I = id tested as a property.
 - **Linear operators, which are their own incremental form:** `map`, `filter` and
  `flat_map`.
 - **`index_by(key)`.** It turns a `ZSet<V>` into an indexed Z-set `K → ZSet<V>`, which
  is the input shape for grouping and joins.
 - **`join_indexed`.** The bilinear delta join: Δ(a ⋈ b) = Δa ⋈ Δb + I(a)₋₁ ⋈ Δb +
  Δa ⋈ I(b)₋₁, over integrated indexes. It is needed for one purpose, clause 5's
  cross-stem references.
 - **`distinct`.** It is `H` over the integrated input, as in the notebook. The output
  delta is non-empty exactly when an element's total weight crosses zero.
 - **`aggregate(group, Aggregator)`.** Its output delta retracts the group's old value
  and inserts its new one. The trait has two kinds of implementation:
  - **linear:** `Count`, and `Sum<G>` for any `G: AbelianGroup`. The state is one value
    per group, and each delta element costs O(1).
  - **integrated:** the aggregator keeps the group's integrated multiset,
    `BTreeMap<V, i64>`, and reads its answer off it. `Min` and `Max` are the first and
    last keys. Unanimity (clause 4) is "exactly one distinct key". Each delta element
    costs O(log d), where d is the number of distinct values in the group.
 **What it leaves out, deliberately:**
 - **Nested streams and least-fixed-point recursion** (the notebook's
  `LiftedLiftedJoin`, `DeltaLiftedDeltaLiftedDistinct` and `IncrementalGraphReachability`).
  improvise's circular semantics are not a least fixed point (clause 6).
 - **Timestamps beyond one clock, lattices, and out-of-order input.** improvise applies
  batches in one total order (ADR 001, "There is already a total order").
 - **Persistence, spilling to disk, and threads.** State lives in memory, and a browser
  worker has one thread.
 - **A query language or planner.** Circuits are wired by hand in the seam crate
  (clause 2).
 **The weight type is `i64`.** Integer weights make `ZSet` an exact group, so
 consolidation and retraction never drift. The drift problem is in the *values* being
 summed, not in the weights (clause 8).
 ### 2. The plug: a trait in improvise-core, and a seam crate that implements it
 **improvise-core gains a trait for the derived state its evaluator reads.** The working
 name is `Derived`. It replaces the two places where eager evaluation folds the store:
 - the formula result at a key, which is `formula_cache` today (`types.rs:370`);
 - the raw fold of the cells matching a partial key under an aggregation, which is
  `aggregate_cell_values(matching_values(..))` today (`types.rs:844`, `:1191`).
 It has one mutation, `apply(&mut self, delta: &CellDelta)`, plus a rebuild for the
 changes that are not cell deltas (clause 7).
 **The formula evaluator stays one.** `eval_expr` and `eval_expr_cached` keep their code
 and read through the trait. The circuit decides *which* formula cells to re-evaluate
 and supplies their inputs, and the existing per-cell evaluator computes the value.
 Formulas are never compiled into operators. A compiled `IF`/`POW`/`WHERE` would be a
 second implementation of evaluation, which design-principles §5 calls the defect
 itself. It is also the reason ADR 008 revision 1 gave for rejecting incremental totals.
 **Two implementations:**
 - **`Eager`** is today's code moved behind the trait, with no behaviour change: `apply`
  records the delta, and the post-batch refresh is `recompute_formulas`.
 - **`Incremental`** lives in a seam crate, working name `improvise-incremental`, which
  depends on `zset` and `improvise-core`. This is the `gp-tree`/`improvise-gp` shape:
  improvise-core never depends on `zset`, and it can be built and tested eager-only
  (question 2).
 **Why keep both.** `Eager` is the oracle for the differential test. It is also the
 backend a query-only source keeps (clause 10). The differential test is a property test
 in the seam crate. It generates documents with groups, collapse, hidden items, formulas
 (including `WHERE`, aggregates inside formulas, chains and cycles), page filters, text
 cells and non-finite numbers, applies the same random edit sequence to both backends,
 and compares every drawn cell, every column total and every occupancy count.
 ### 3. The input: a cell write is a retraction plus an insertion
 **The input stream is the *cell delta*: a `ZSet<(CellKey, CellValue)>` with weights
 ±1.** `DataStore::set` and `DataStore::remove` (`cell.rs:286`, `:325`) are the only
 places a cell changes, so the delta is emitted there:
 - a new cell is `+(k, v)`;
 - an overwrite of `v₀` with `v₁` is `−(k, v₀) + (k, v₁)`;
 - a removal is `−(k, v₀)`.
 An overwrite with an equal value consolidates to the empty Z-set. The circuit steps once
 per model effect, as ADR 008 clause 3 requires: the frame observation reads occupancy
 inside the effect loop (`app.rs:1073-1084`).
 **This lines up with ADR 001's record tier with no extra rule.** The records a batch
 moved are the `record_of` (`crates/improvise-core/src/model/record.rs:14`) of the keys
 in the batch's consolidated delta. So:
 - a write of the value already there moves nothing, which is gotcha 40's rule;
 - a record gained, lost or rewritten is named once, because a Z-set is already a set of
  keys.
 `bump_changed_records` can then read the delta instead of diffing two
 `record_fingerprints` scans (`app.rs:254-264`). The tier is still *observed*: the delta
 comes from the mutation sites, not from an `EffectKind`. The same holds for the content
 half of the dirty flag, where a non-empty delta means dirty. `layout_version` is
 unchanged, because it observes `view_shape` and not cells.
 **`CellKey` gains `Ord`.** It is a sorted `Vec<(String, String)>`
 (`cell.rs:10-11`), so deriving `Ord` is sound. `CellValue` holds an `f64` and is only
 `PartialEq` (`cell.rs:116`), so multiset keys use a wrapper ordered by
 `f64::total_cmp`. Clause 4 says where that differs from `==`.
 ### 4. Aggregates: linear where they can be, an integrated multiset where they cannot
 **The group** is the cell key with the view's `none_cats` removed. That is the partial
 key `evaluate_unfolded` folds over. There is one aggregation circuit per distinct
 `none_cats` list, shared by every view that has that list. That replaces
 `rederived_for`'s model clone (`project.rs:195-210`). **The aggregator** for a group
 comes from its `_Measure` coordinate through `measure_agg`, as `agg_for` does
 (`types.rs:717-722`).
 **What each group keeps:**
 | answer | state per group | cost per delta element | exact on f64? |
 |---|---|---|---|
 | `Count` | count of values, count of numbers | O(1) | yes (integers) |
 | `Sum` | running sum | O(1) | **no** (clause 8) |
 | `Avg` | derived: `Sum / Count` | O(1) | no, through `Sum` |
 | `Min`, `Max` | multiset of the numbers | O(log d) | yes (order-free) |
 | unanimity and `mixed` | multiset of all values | O(log d) | yes (order-free) |
 Reading a group reproduces `aggregate_cell_values`'s branch order:
 - if the count of numbers equals the count of values, the numeric answer;
 - else if the value multiset has exactly one distinct key, that value;
 - else `Error("mixed")`.
 The empty group is absent. The formula-level `eval_agg` (`types.rs:55-87`) reads the
 same state with its own emptiness rule, `0` for `Sum` and `Count`, at read time.
 **Memory.** Summed over all groups, the multisets hold at most one entry per stored
 cell. So the state for one `none_cats` list is O(cells), on the order of the store it
 summarizes. **Estimate, not measured:** a `BTreeMap` entry of about 40–60 bytes plus the
 key's size gives a few megabytes at the 190k cells ADR 008 measured. Only the measures
 whose `measure_agg` is `Min`, `Max`, or that hold text, need the multisets. A
 `Sum`-only document keeps one number per group.
 **`total_cmp` is not `==`, and the differential test must say so.** `NaN != NaN`, so
 today two NaNs in one group read as `mixed`, and `f64::min` skips a NaN. A multiset keyed
 by `total_cmp` would call two NaNs one value and would order NaN at an end. The test
 generates non-finite values (core.md §16), and the aggregator matches eager
 behaviour explicitly rather than inheriting `total_cmp`'s.
 ### 5. Formulas: the circuit finds what moved, and the evaluator recomputes it
 **Stems are a `distinct`.** Today's stem set (`types.rs:986-997`) is every stored key
 with the target category and each `none_cats` entry removed. That is
 `distinct(map(project))` over the cell delta. A stem enters when its first cell arrives
 and leaves when its last cell goes.
 **A formula cell is re-evaluated when one of its inputs moved.** The inputs of formula
 `T` at stem `s` are:
 - for each `Ref(R)`, the group `s.with(cat(R), R)`. `cat(R)` is resolved once per
  formula set through `find_item_category`, including its `_Measure` fallback for
  formula targets (`types.rs:725-740`). Whether `R` is derived (`formula_for`) is also
  decided per formula set, so a ref to another formula becomes an edge between formula
  nodes, and a ref to raw data becomes an edge from an aggregate group.
 - for an `Agg` with no filter, the group at `s` itself, because `eval_agg` pools over
  `context.without(target_category)`.
 - for an `Agg` whose inner `WHERE` names `Cat = Item`, the group at
  `s.with(Cat, Item)`. That is a different stem, so a delta at `Cat = Item` reaches
  every stem that differs only in `Cat`. **This is the one join**: stems indexed by
  "stem minus `Cat`", joined with the aggregate's output delta.
 The affected `(stem, formula)` pairs are consolidated, ordered topologically over the
 **formula graph**, and handed to the existing evaluator. Its cached path already reads
 refs through `formula_cache` and falls back to raw aggregation (`types.rs:1066-1086`).
 With the trait, both reads go to the maintained state.
 **A formula's own `WHERE`** is decided per cell, as today. A cell whose coordinate does
 not match falls back to raw aggregation (`types.rs:1047-1055`), so its input is its own
 group and nothing else.
 **An aggregate over an expression replaces `Expansion::members`.** `SUM(expr)` pools
 `expr` evaluated at each member record (`agg_values`, `types.rs:89-139`). Incrementally,
 that is `map(record ↦ expr at record)`, then `index_by(base key)`, then `Sum`. The
 member records never have to be listed. **The boundary:** the map is sound only when
 `expr` reads the record's own cells. An inner expression that reads another record, or
 holds a nested aggregate, stays on the eager path for that formula, and the
 differential test pins the boundary. Until `Sum` is exact, this path carries clause 8's
 caveat. ADR 008 clause 5 adopts the same boundary.
 ### 6. Circular references: DBSP's recursion is not our semantics
 DBSP handles recursion by computing a **least fixed point**: nested streams iterate a
 monotone operator, and `distinct` keeps the lattice finite, so reachability converges.
 improvise has no such guarantee:
 - `A = B + 1` with `B = A + 1` has no fixed point at all;
 - `X = X + 1` over a stored `X = 10` climbs forever;
 - the required answer is `Error("circular")`, not a limit or a non-terminating step.
 So the crate has no recursion operator, and circularity is decided *outside* it:
 - **The formula graph** (target → the targets its refs name) is rebuilt when the formula
  set changes, and its strongly connected components are found (Tarjan). Formulas
  outside every cycle are evaluated in topological order, each exactly once per step.
 - **A formula in a cycle, a self-loop included, has its affected cells evaluated by
  today's bounded fixed point, restricted to that component.** A formula-level cycle is
  not always circular at every cell. `A = IF(x, B, 1)` with `B = A` converges wherever
  `x` is false. The per-cell fixed point is the only thing that gets those cells right,
  and reusing it keeps `Error("circular")` exactly as it is.
 - **The depth bound is part of the semantics today.** An acyclic chain that needs all
  sixteen passes is reported circular by both eager evaluators (core.md §3). A
  topological evaluator would compute it correctly, and so would disagree with eager.
  Question 4 asks whether to reproduce the bound. The recommendation is to reproduce
  it, by carrying each formula's topological depth, so the differential test compares
  like with like. Changing the rule would be its own decision, for both backends at
  once.
 ### 7. What is not a cell delta rebuilds, once
 Some changes alter the circuit's *shape*, not its input:
 - the formula set: add, remove or replace;
 - `measure_agg`;
 - category and item structure: add or remove a category, remove an item, and group
  membership;
 - a view's axes, hidden items and collapsed groups, which change `view_shape`;
 - a document swap, `document_generation`.
 Each rebuilds only the affected operators, from the integrated base Z-set. That costs
 O(cells), once per change, and is never repeated per keypress. **The trigger is the same
 observation the tiers use**: a `view_shape` diff (`app.rs:40-72`) rebuilds that view's
 operators, the same diff that bumps `layout_version`. So there is one signal and not two.
 **A page selection is not a rebuild.** The group key includes the page categories, so
 `[` and `]` read another slice of state that already exists. The held-key path stays
 O(visible) (improvise-748f's constraint). The slices cost nothing extra, because the
 state is still bounded by the stored cells, however many pages there are (question 7).
 ### 8. Floating point: retraction drifts, and exactness is ADR 005's
 f64 addition is not associative, so a sum maintained by `+v` and `−v` is not the sum
 the eager fold computes. **Measured**, not asserted:
 `cargo run --release -p improvise-core --example retraction_drift`
 (`crates/improvise-core/examples/retraction_drift.rs`, added by this PR). It was run on
 an Apple M4 Max, with seeds 1 and 2. The example keeps a running sum through N
 retract-and-insert cycles. It compares the sum against the eager fold,
 `evaluate_aggregated_f64`, and against the exact decimal sum, taken as an integer count
 of 10⁻⁵ units rounded to f64 once. Values are signed two-place decimals spread over 3 or
 9 decades.
 | store | magnitudes | after 1M cycles: naive vs eager | ≥ `FLOAT_EQ_EPSILON`? | eager vs exact |
 |---|---|---|---|---|
 | 1,000 cells | 3 decades | 6.4e-11 – 1.3e-10 (35–140 ulp) | in 1 of 2 seeds | ≤ 7.3e-12 |
 | 18,000 cells | 3 decades | 1.7e-9 – 2.3e-9 (57–80 ulp) | yes | 1.5e-10 – 2.6e-10 |
 | 18,000 cells | 9 decades | 2.3e-5 – 3.2e-4 (3–42 ulp) | yes | 2.4e-4 – 2.5e-4 |
 A fourth case holds 1e17, then adds 1,000 cells of 0.01, then retracts the 1e17. The
 naive running sum reads **0.00**, and the eager fold and the exact sum both read
 **10.00** (at `,.2`). The small values were absorbed and never came back.
 A Neumaier-compensated running sum recovers that case exactly. In the random cases it
 stays about as close to the exact sum as eager does, **but it is never bit-equal to
 eager**, because eager folds in store order and is itself inexact.
 Four conclusions follow:
 - **Bit-equality between an incremental and an eager f64 `Sum` is not attainable** by
  any running-sum technique. The differential test can compare `Count`, `Min`, `Max`,
  unanimity and occupancy bit for bit today, because they are order-free. It can compare
  `Sum` and `Avg` only with a tolerance.
 - **The gap reaches the epsilon.** In most 18k-cell cases the incremental sum and the
  eager sum differ by more than `FLOAT_EQ_EPSILON`. So `IF(SUM(..) = x, ..)` can answer
  differently on the two paths. That is a behaviour difference, not a display one.
 - **This is already a bug in eager, which the measurement found in passing.** The eager
  18k-cell sum is 1.5e-10 to 5.8e-10 from the exact decimal sum, so `=` against a
  decimal a user typed can already be wrong today. That supports ADR 005 on its own
  merits, and it is recorded here for improvise-l2b8.
 - **Exact decimals dissolve both problems.** Under ADR 005, `Sum` is a true
  `AbelianGroup`, retraction is exact, the order of folding stops mattering (gotcha 18's
  whole class), and the differential test is bit-exact everywhere.
 **So ADR 005 is a prerequisite for the maintained `Sum`/`Avg` on the displayed path, but
 not for the rest of this ADR** (question 3). Occupancy, `Count`, `Min`, `Max`,
 unanimity, stems and invalidation can all land before it. Until ADR 005 lands, a `Sum`
 or `Avg` the grid displays, including a column total that holds one, is read from the
 eager fold. The maintained sum runs only inside the differential test, under a stated
 tolerance. If the user wants maintained sums before ADR 005, the fallback is a
 compensated sum that re-folds a group from its values when cancellation is detected.
 The measurement above is the evidence for and against that fallback.
 ### 9. What ADR 008 gets from it
 ADR 008 (revision 2, PR #308) assumes these, under the shared names below.
 - **Occupancy** (ADR 008 clause 3). For each view, there is a count per row tuple and
  per column tuple of cells that hold a value. Stored cells pass the view's filter, with
  hidden items dropped, and a collapsed group's members map to the group's tuple.
  Formula cells count at their stems, which is today's `formula_cache` stem set. A tuple
  is on the axis iff its count is above zero. **This ADR does not settle ADR 008
  question 1 (both cases: fold rows with a formula column, and `Exact`).** Today those
  cells are values with no stored cell under them. The stem definition drops them, and
  if the user rules otherwise, those views fall back to a non-occupancy path. Occupancy
  is integer and order-free, so it does not wait for ADR 005.
 - **The occupancy delta** (ADR 008 clause 8). `distinct` over occupancy emits a
  non-empty delta exactly when a tuple enters or leaves an axis. A reframe is a
  non-empty occupancy delta. The two-arm asymmetry of the frame observation (gotcha 24,
  improvise-mcq4) is unchanged, but each arm costs O(delta) instead of a rebuilt grid
  per view.
 - **Column totals** (ADR 008 clause 5). A column total is the formula evaluated over
  the pooled fold (`GridEval::column_total`, `crates/improvise-core/src/view/layout.rs:976-980`),
  not a sum of row values. So the circuit keeps a per-(column tuple, raw measure)
  aggregate, and the formula layer re-evaluates only the columns whose inputs moved,
  through clause 2's trait. `Expansion::members` is replaced by clause 5. Totals that
  hold a `Sum` or `Avg` wait for ADR 005 (clause 8).
 - **What ADR 008 therefore stops asking.** Its question 6 (totals: query and memoize,
  or maintain) is struck there as decided by the user through this ADR. Its questions 1
  and 2 stay open there.
 - **What it does not get.** Column widths depend on formatted text, which is
  display-only (gotcha 8), so they are not maintained here. They stay ADR 008 question 2.
 ### 10. ADR 003's live sources are delta streams, when they can be
 A live source that can report its changes, by polling and diffing, by triggers, or by a
 change feed, produces a cell delta. That is the same input `DataStore` produces, and the
 circuit cannot tell them apart. That is the "data can stream" half of the user's
 prompt.
 **A source that can only answer aggregate queries stays on `Eager`,** with ADR 003's
 pushdown. There is a tension: ADR 003 wants data larger than memory, and every
 integrated operator here keeps state proportional to its input (clause 4). So the
 backend is chosen per document, which is what "pluggable" buys (question 8). A
 read-only live source also sidesteps ADR 001's record tier, as ADR 003 already notes.
 ### 11. Constraints
 - **wasm32.** `zset` has no dependencies. The seam crate adds only `zset` and
  `improvise-core`. If improvise-command selects the backend, both join the browser
  bundle, so they join the `wasm` CI job's per-crate list in the same PR that adds
  them. Check with `cargo tree --edges normal`, per crate (repo map, "Wasm").
 - **Two seconds per test binary.** The crate's laws and its "incremental equals
  from-scratch" properties run at the default 256 cases over small inputs. The
  differential test lives in the seam crate's own binary, so its cost is visible on its
  own. Its document sizes are bounded by the strategy, never by raising or lowering the
  case count (design-principles §7).
 - **Ordering determinism (gotcha 18).** A `ZSet` iterates in `K`'s `Ord` order, never
  in hash order. A hash index is allowed for lookup only. Output deltas are
  consolidated and sorted before they leave an operator. Nothing in the circuit decides
  a display order: record order stays `DataStore`'s (`live_records`, `cell.rs:366`).
  The determinism test builds **two** circuits independently from the same history and
  compares them. One circuit compared with itself proves nothing (improvise-hzjo's
  vacuity).
 - **ADR 001 clause 4, rollback.** A refused frame is put back by `App::restore`
  (`app.rs:647`). The backend's state is part of the snapshot. Undoing by applying the
  inverse delta is exact for integer weights and order-free aggregators, but not for an
  f64 `Sum`, so the snapshot is kept until clause 8's prerequisite lands (question 9).
 - **ADR 006, replay (improvise-ilvl).** A circuit is a deterministic function of the
  delta sequence, so replaying commands reproduces its state.
 ## Alternatives considered
 **Feldera's `dbsp` crate.** What was verified on 2026-09-24:
 - The latest release is 0.354.0, a 4.8 MB compressed tarball, MIT OR Apache-2.0,
  requiring Rust 1.96.1.
 - It has 67 direct normal dependencies, none optional, and two features
  (`backend-mode`, `default`). tokio, mimalloc, nix, zstd, libc and core_affinity are
  all required.
 - `cargo tree -e normal` resolves about 455 crates natively and 421 for
  `wasm32-unknown-unknown`. For comparison, improvise-core's whole normal tree for wasm32
  is 25 crates, and improvise-command's is 68.
 - `cargo check` succeeds natively. **`cargo check --target wasm32-unknown-unknown`
  fails**: `mio` (tokio's) reports 48 errors.
 What was **not** verified: whether anything past `mio` would also fail. The build stops
 at the first failure, so that is estimated, not measured. It is likely, because
 mimalloc's sys crate and zstd build C code, and `libsqlite3-sys` already fails under this
 repo's nix cc-wrapper (gotcha 41). Even if it built, it is a multi-threaded,
 storage-backed query engine where improvise needs a single-threaded operator library.
 The user's decision already excludes it. This records why that decision loses nothing.
 **Keep eager evaluation and memoize.** improvise-swre proposes keying `grid_of` on the
 existing tiers, so an unchanged grid costs nothing. That is worth doing under either
 backend. But every write still recomputes every formula and rescans the store, and a
 second view with a different None axis still clones the model. It removes the cost of
 *not* changing and leaves the cost of changing at O(cells).
 **An ad-hoc incremental cache.** Track dirty stems by hand: invalidate the groups a
 write touches, and recompute them. It is cheaper to start. But each derived fact, such
 as a group aggregate, occupancy, a column total, a stem or a cross-stem `WHERE`, needs
 its own invalidation rule. Each rule is a second description of evaluation, free to
 disagree with the first. The Z-set algebra gives **one** rule, linearity and
 bilinearity, whose laws can be property-tested once in the crate. That is the same
 argument as design-principles §5's "a derivation done twice is the defect".
 **Compile formulas into operators.** This is the fully DBSP-shaped answer. It is
 rejected in clause 2, because it would be a second evaluator.
 ## Consequences and migration
 **Order.** Each step is its own ticket and PR, with gates green, and none switches the
 displayed path until the differential test holds.
 1. **The `zset` crate**, with its group laws, operator properties and determinism
   test. Nothing in improvise uses it yet.
 2. **The `Derived` trait, with `Eager` behind it.** No behaviour change, and the
   existing suite is the evidence. `CellKey` gains `Ord`.
 3. **The cell delta from `DataStore`.** `bump_changed_records` and the content half of
   the dirty flag move onto it. That removes two O(cells) scans per cell-writing batch.
   The existing tier tests are the evidence.
 4. **`Incremental`, for the order-free parts**: stems, `Count`, `Min`, `Max`,
   unanimity, occupancy and the occupancy delta, under the differential test. **ADR 008
   clauses 3 and 8 (pruning and the frame observation) depend on this step.**
 5. **`Sum` and `Avg`, and column totals, after ADR 005** (or on question 3's fallback).
   **ADR 008 clause 5 depends on this step.**
 6. **Formulas**: the formula graph, topological re-evaluation, the component fixed
   point, and the aggregate-over-expression map that replaces `Expansion::members`.
 7. **Live sources as delta streams**, when ADR 003's source trait exists.
 **Tickets.** improvise-felo.4 is this ADR. The steps above are not yet filed, which is
 question 10. improvise-swre stays independent and is useful under either backend.
 improvise-l2b8 (ADR 005) gains a dependant, and a measured argument, from clause 8.
 **Good.**
 - A write costs O(delta) plus the formula cells it reaches, not O(cells).
 - The store scans behind the record tier and the dirty flag disappear.
 - Per-view model clones for a different None axis disappear.
 - ADR 008 gets occupancy, the occupancy delta and column totals without a second
  evaluator.
 - Live sources that can report changes plug in without touching the evaluator.
 **Bad.**
 - Two backends, kept equal by a differential test that must itself be kept honest.
 - Integrated state is O(cells) in memory, per distinct None axis, in addition to the
  store.
 - `Sum` and `Avg` cannot be maintained on the displayed path until ADR 005 lands, and
  the measurement says so.
 - Circularity is decided in two layers: the formula graph's components and the
  per-cell bound.
 - The browser bundle grows by two small crates.
 ## Open questions
 Each question has a recommendation. The user's answers will be folded in under "What
 the user decided", as ADRs 004 and 007 did.
 1. **The crate's name.** `zset`, `dbsp-core`, or `improvise-dbsp`?
   *Recommendation:* `zset`. It is problem-agnostic, like `gp-tree`, so it should not
   carry improvise's name. `dbsp-core` invites confusion with Feldera's `dbsp`.
 2. **Where `Incremental` lives.** In a seam crate (`improvise-incremental`, depending on
   `zset` and `improvise-core`), or inside improvise-core?
   *Recommendation:* a seam crate. improvise-core then never depends on `zset`, and
   `Eager` stays buildable and testable alone. It is the `gp-tree`/`improvise-gp` shape.
 3. **Floating point.** Should ADR 005 (exact decimals) be a prerequisite for maintaining
   `Sum` and `Avg` on the displayed path, with the eager fold kept for them until then?
   Or should a compensated f64 sum, re-folded on detected cancellation, ship first with
   a tolerance in the differential test?
   *Recommendation:* ADR 005 as the prerequisite. The measured drift reaches
   `FLOAT_EQ_EPSILON`, so `=` could answer differently on the two paths. No f64 technique
   makes the differential test bit-exact. Everything else in this ADR lands without it.
 4. **The sixteen-pass bound.** An acyclic chain needing all sixteen passes is reported
   `circular` today (core.md §3). Should `Incremental` reproduce that?
   *Recommendation:* reproduce it, so the two backends are comparable. If the bound is to
   change, change it in both backends at once, as its own decision.
 5. **Formula cycles.** Should formulas in a cycle of the formula graph be evaluated by
   today's bounded fixed point, restricted to their component, rather than by any
   operator in the crate?
   *Recommendation:* yes. It keeps `Error("circular")` exactly as it is, including the
   cells a guarded cycle leaves convergent. The crate needs no recursion operator.
 6. **Keep `Eager` permanently?** Once `Incremental` is the default, should `Eager` stay?
   *Recommendation:* yes, permanently. It is the differential test's oracle and the
   backend for ADR 003's query-only sources. Deleting it would delete the test.
 7. **Page selection as a slice.** Should the group key include the page categories, so
   switching page reads existing state, rather than rebuilding the view's operators per
   page change?
   *Recommendation:* the slice. The state stays bounded by the stored cells, and the
   held-key path (`[`/`]`) stays O(visible). ADR 008 revision 2 assumes this.
 8. **Live sources.** Should `Incremental` serve only sources that can emit change deltas,
   with query-only sources kept on `Eager` and ADR 003's pushdown?
   *Recommendation:* yes, chosen per document. Integrated state is proportional to the
   source, which contradicts ADR 003's larger-than-memory goal for exactly the sources
   that cannot report their changes anyway.
 9. **Rollback.** For ADR 001 clause 4, should the backend's state be snapshotted with
   the `App`, or undone by applying the inverse delta?
   *Recommendation:* snapshot until ADR 005 lands, then the inverse delta. The inverse
   is exact only when every aggregator is.
 10. **Ticket structure.** Should improvise-felo.4 become the epic for clause-order steps
    1–7, with one child bead per step, and ADR 008's dependent steps linked as blocked by
    steps 4 and 5?
    *Recommendation:* yes. The user's decision is recorded on felo.4, and the steps are
    how it is met.
@@ -0,0 +1,191 @@
 //! How far a SUM maintained by insert/retract deltas drifts from the eager fold,
 //! in f64. ADR 009 (improvise-felo.4), "Floating point".
 use improvise_core::format::format_f64;
 use improvise_core::model::cell::{CellKey, CellValue};
 use improvise_core::model::types::{Aggregation, Model};
 const MEASURE: &str = "_Measure";
 /// SplitMix64: seeded, so a run is reproducible and a second seed is a new sample.
 struct Rng(u64);
 impl Rng {
    fn next(&mut self) -> u64 {
        self.0 = self.0.wrapping_add(0x9E37_79B9_7F4A_7C15);
        let mut z = self.0;
        z = (z ^ (z >> 30)).wrapping_mul(0xBF58_476D_1CE4_E5B9);
        z = (z ^ (z >> 27)).wrapping_mul(0x94D0_49BB_1331_11EB);
        z ^ (z >> 31)
    }
    fn below(&mut self, n: u64) -> u64 {
        self.next() % n
    }
 }
 /// A user-entered decimal as an exact count of 1e-5 units, its magnitude spread
 /// over `decades` decades. The f64 the store holds is `typed(units)`.
 fn decimal(rng: &mut Rng, decades: u32) -> i64 {
    let scale = 10i64.pow(rng.below(u64::from(decades)) as u32);
    let cents = rng.below(100_000) as i64;
    let sign = if rng.below(4) == 0 { -1 } else { 1 };
    sign * cents * scale
 }
 fn typed(units: i64) -> f64 {
    units as f64 / 1e5
 }
 /// The exact decimal sum, rounded to f64 once: what ADR 005's arithmetic would show.
 fn exact(units: &[i64]) -> f64 {
    units.iter().map(|&u| i128::from(u)).sum::<i128>() as f64 / 1e5
 }
 fn key(row: usize) -> CellKey {
    CellKey::new(vec![
        ("Row".to_string(), format!("r{row}")),
        (MEASURE.to_string(), "Amount".to_string()),
    ])
 }
 /// `cells` rows of one measure; the eager SUM is the one the grid draws.
 fn document(rng: &mut Rng, cells: usize, decades: u32) -> (Model, Vec<i64>) {
    let mut m = Model::new("drift");
    m.add_category("Row").expect("under the limit");
    let values: Vec<i64> = (0..cells).map(|_| decimal(rng, decades)).collect();
    for (row, v) in values.iter().enumerate() {
        m.category_mut("Row")
            .expect("just added")
            .add_item(format!("r{row}"));
        m.set_cell(key(row), CellValue::Number(typed(*v)));
    }
    (m, values)
 }
 fn eager(m: &Model) -> f64 {
    let total = CellKey::new(vec![(MEASURE.to_string(), "Amount".to_string())]);
    m.evaluate_aggregated_f64(&total, Aggregation::OverHidden)
 }
 /// Neumaier's compensated running sum: the cheap mitigation, measured beside the naive one.
 #[derive(Default)]
 struct Compensated {
    sum: f64,
    carry: f64,
 }
 impl Compensated {
    fn add(&mut self, x: f64) {
        let t = self.sum + x;
        self.carry += match self.sum.abs() >= x.abs() {
            true => (self.sum - t) + x,
            false => (x - t) + self.sum,
        };
        self.sum = t;
    }
    fn value(&self) -> f64 {
        self.sum + self.carry
    }
 }
 fn ulps(a: f64, b: f64) -> u64 {
    (a.to_bits() as i64).abs_diff(b.to_bits() as i64)
 }
 /// Each running sum against the eager fold (the differential oracle) and against the
 /// exact decimal sum. `flip`: the gap reaches `FLOAT_EQ_EPSILON`, so `=` can answer differently.
 fn report(label: &str, cycles: usize, exact: f64, eager: f64, naive: f64, comp: f64) {
    let shown = |v: f64| format_f64(v, true, 2);
    println!(
        "{label:<22} {cycles:>8} {:>10.2e} {:>6} {:>10.2e} {:>6} {:>5} {:>10.2e} {:>10.2e} {:>10.2e}",
        (naive - eager).abs(),
        ulps(naive, eager),
        (comp - eager).abs(),
        ulps(comp, eager),
        (naive - eager).abs() >= 1e-10,
        (eager - exact).abs(),
        (naive - exact).abs(),
        (comp - exact).abs(),
    );
    if shown(naive) != shown(eager) || shown(eager) != shown(exact) {
        println!(
            "  shown at ,.2: naive {} eager {} exact {}",
            shown(naive),
            shown(eager),
            shown(exact)
        );
    }
 }
 /// Each cycle retracts one live value and inserts a fresh one at the same key.
 fn random_updates(seed: u64, cells: usize, decades: u32, checkpoints: &[usize]) {
    let mut rng = Rng(seed);
    let (mut m, mut values) = document(&mut rng, cells, decades);
    let mut naive = eager(&m);
    let mut comp = Compensated::default();
    comp.add(naive);
    let mut done = 0;
    for &at in checkpoints {
        while done < at {
            let row = rng.below(cells as u64) as usize;
            let new = decimal(&mut rng, decades);
            naive = naive - typed(values[row]) + typed(new);
            comp.add(-typed(values[row]));
            comp.add(typed(new));
            values[row] = new;
            m.set_cell(key(row), CellValue::Number(typed(new)));
            done += 1;
        }
        let label = format!("{cells} cells, {decades} dec");
        report(&label, at, exact(&values), eager(&m), naive, comp.value());
    }
 }
 /// A large value arrives, small ones accumulate under it, then it is retracted.
 fn absorbed_by_a_large_value() {
    let mut m = Model::new("absorb");
    m.add_category("Row").expect("under the limit");
    m.category_mut("Row").expect("just added").add_item("r0");
    let mut naive = 0.0;
    let mut comp = Compensated::default();
    m.set_cell(key(0), CellValue::Number(1e17));
    naive += 1e17;
    comp.add(1e17);
    for row in 1..=1000 {
        m.category_mut("Row")
            .expect("just added")
            .add_item(format!("r{row}"));
        m.set_cell(key(row), CellValue::Number(0.01));
        naive += 0.01;
        comp.add(0.01);
    }
    m.clear_cell(&key(0));
    naive -= 1e17;
    comp.add(-1e17);
    report("1e17, 1000 x 0.01, -1e17", 1001, 10.0, eager(&m), naive, comp.value());
 }
 fn main() {
    println!(
        "{:<22} {:>8} {:>10} {:>6} {:>10} {:>6} {:>5} {:>10} {:>10} {:>10}",
        "case",
        "cycles",
        "naive-eag",
        "ulp",
        "comp-eag",
        "ulp",
        "flip",
        "eag-exact",
        "nai-exact",
        "cmp-exact"
    );
    let checkpoints = [1_000, 10_000, 100_000, 1_000_000];
    for seed in [1, 2] {
        random_updates(seed, 1_000, 3, &checkpoints);
        random_updates(seed, 18_000, 3, &checkpoints);
        random_updates(seed, 18_000, 9, &checkpoints);
    }
    absorbed_by_a_large_value();
 }
@@ -46,6 +46,7 @@ const SECTIONS = [
      ["context/adr/003-live-backed-models.md", "adr/003-live-backed-models", "ADR 003 — Live-backed models"],
      ["context/adr/004-faces-and-themes.md", "adr/004-faces-and-themes", "ADR 004 — Faces"],
      ["context/adr/007-stable-identities.md", "adr/007-stable-identities", "ADR 007 — Stable identities"],
      ["context/adr/009-incremental-evaluation.md", "adr/009-incremental-evaluation", "ADR 009 — Incremental evaluation (proposed)"],
    ],
  },
  {