docs(adr): ADR 009 follows the document per model effect; answer the joint review (improvise-felo.4)

- clause 7: the operator shape and the formula-set fingerprint are re-read after each
  model effect inside the loop. Formula edits are an explicit input, and a document
  swap rebuilds everything. Stated in the same words as ADR 008 revision 3.
- clause 3: a delta key's identity is bit identity, matching hash_value. The dirty
  flag keeps a formula fingerprint, so formula edits still persist.
- clause 5: the stem rule for a formula with a top-level WHERE.
- clause 11 and question 9: rollback is a snapshot, with its second O(cells) clone
  stated. The inverse delta is not a rewind.
- migration: formulas become step 5, and Sum/Avg and column totals step 6.
- the drift example's values are five-place, not two-place. Clause 7 and question 7
  are worded as recommendations.

Co-Authored-By: Claude Opus 5.5 (1M context) <noreply@anthropic.com>
Claude-Session: https://claude.ai/code/session_01VdfEGXA7aJ6ftMsCc9PJze

context/adr/009-incremental-evaluation.md

@@ -15,7 +15,7 @@ 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.
+revision 3 of `context/adr/008-virtualized-grid.md` on PR #308.
 
 ## The decision this ADR writes down
 
@@ -64,10 +64,15 @@ plugs in, and what it may not change.
   (`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.
+- **Two observations scan the store.** `record_fingerprints` (`app.rs:254-264`) hashes
+  every cell before and after a cell-writing batch. `document_content`
+  (`app.rs:165-180`) hashes every cell and every formula for the dirty flag, and it is
+  re-read after **each** `CellData` effect (`app.rs:1039-1045`). So the first is O(cells)
+  per batch and the second O(cells) per effect, whatever was written.
+- **Every mutating frame from a client already clones the document.**
+  `Host::mutating_frame` takes `App::snapshot` before applying anything (`host.rs:162`,
+  `app.rs:627-629`), for ADR 001 clause 4. That is O(cells) per frame on the network
+  path, whatever this ADR does.
 
 ### What an incremental evaluator must not change
 
@@ -158,8 +163,8 @@ name is `Derived`. It replaces the two places where eager evaluation folds the s
 - 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).
+It takes two inputs, both applied after each model effect (clause 7): the cell delta,
+and the formula delta. It also has a rebuild, for an operator shape that moved.
 
 **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
@@ -198,6 +203,25 @@ An overwrite with an equal value consolidates to the empty Z-set. The circuit st
 per model effect, as ADR 008 clause 3 requires: the frame observation reads occupancy
 inside the effect loop (`app.rs:1073-1084`).
 
+**A delta key's identity is bit identity, the same identity the record tier uses
+today.** Two `(CellKey, CellValue)` pairs are one element exactly when their keys are
+equal and their values are equal *by bits*: `Number` by `f64::to_bits`, `Text` and
+`Error` by their strings. That is `hash_value` (`app.rs:233-250`), which
+`record_fingerprints` already hashes. So the cell delta reproduces today's tier
+exactly:
+
+- overwriting `0.0` with `-0.0` is a non-empty delta and bumps the record, as it does
+  today;
+- overwriting a NaN with a NaN of the same bits is empty and bumps nothing, as today.
+
+It is **not** `CellValue`'s derived `PartialEq`, under which `-0.0 == 0.0` and
+`NaN != NaN`. `recompute_formulas` uses that one for its "did this cell move" test
+(`types.rs:1010`), and it stays there. The ordering behind a multiset (clause 4) is
+`f64::total_cmp`, whose equality *is* bit equality for every finite and non-finite
+value. So the delta identity and the multiset ordering agree, and neither is
+`PartialEq`. Step 3's tests pin both cases: signed zero, and a repeated same-bits
+NaN.
+
 **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:
@@ -208,9 +232,19 @@ in the batch's consolidated delta. So:
 
 `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.
+comes from the mutation sites, not from an `EffectKind`. `layout_version` is unchanged,
+because it observes `view_shape` and not cells.
+
+**The dirty flag's content half does not move onto the cell delta alone.**
+`document_content` (`app.rs:165-180`) hashes the formulas as well as the cells, and it
+is re-read after every `CellData` effect (`app.rs:1039-1045`). `AddFormula`,
+`RemoveFormula` and `ReplaceFormula` are `CellData` effects (`effect.rs:230`, `:247`,
+`:268`) that emit no cell delta. The worker persists on this flag (gotcha 45). So "a
+non-empty cell delta means dirty" would never save a formula edit in the browser. The
+content half becomes: **a non-empty cell delta, or a moved formula-set fingerprint**.
+The fingerprint is the one clause 7 already reads after each model effect, so nothing
+new is observed. Its cost is O(formulas), where `document_content` is O(cells) per
+`CellData` effect.
 
 **`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
@@ -252,11 +286,13 @@ key's size gives a few megabytes at the 190k cells ADR 008 measured. Only the me
 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.
+**The multiset's identity is clause 3's bit identity, and eager's *reading* is not.** A
+multiset keyed by `total_cmp` holds the values the store holds, by bits, and that is
+correct for the state. But eager *reads* a group through `PartialEq` and `f64::min`:
+`NaN != NaN`, so two NaNs in one group read as `mixed` today, `-0.0` and `0.0` read as
+one value, and `f64::min` skips a NaN. So the aggregator's *read* reproduces eager's
+rules explicitly and does not inherit `total_cmp`'s. The differential test generates
+signed zeros and non-finite values (core.md §16) to pin it.
 
 ### 5. Formulas: the circuit finds what moved, and the evaluator recomputes it
 
@@ -265,6 +301,21 @@ 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.
 
+**The stem rule: a formula cell exists at a stem only where its value would be cached
+today.** `recompute_formulas` caches a formula cell only when the cached evaluator
+returns a value (`types.rs:1010-1014`). For a formula with a top-level `WHERE`, a stem
+whose coordinate fails the filter falls back to `aggregate_raw` (`types.rs:1047-1055`),
+which is absent when no raw data lies at the target key. So:
+
+- **a formula counts at a stem only where its top-level `WHERE` (if any) matches the
+  stem's coordinate, or where raw data exists at stem + target.**
+
+This is a coordinate predicate plus one count lookup, never an evaluation. It is the
+rule ADR 008 clause 3's occupancy uses for formula cells, and it keeps today's pruning.
+The review of ADR 008 found the case that needs it: `Double = Revenue * 2 WHERE
+Region = East` with data only at West is pruned today, and a rule that counted every
+stem would have kept the column.
+
 **A formula cell is re-evaluated when one of its inputs moved.** The inputs of formula
 `T` at stem `s` are:
 
@@ -326,26 +377,51 @@ So the crate has no recursion operator, and circularity is decided *outside* it:
   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
+### 7. The circuit follows the document per model effect
 
-Some changes alter the circuit's *shape*, not its input:
+Some changes alter what the circuit computes, not only its input. They are observed
+**inside** `apply_effects`, after **every** `EffectKind::Model(_)` effect: the same
+position as the frame and dirty observations (`app.rs:1036-1084`). They are not the
+post-loop `view_shape` diff that bumps `layout_version` (`app.rs:1102`, `:1116-1124`).
+That diff comes too late, and it cannot see most of these changes. ADR 008 states this
+clause in the same words.
 
-- 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`.
+- **Operator shape, per view.** The operator shape is `view_shape` (`app.rs:40-72`),
+  plus the group membership of every drawn item, collapsed or not, plus
+  `measure_agg`. `view_shape` itself is not widened, so what bumps `layout_version` is
+  unchanged. A view whose operator shape moved has its operators rebuilt from the
+  integrated base Z-set **before the next effect's cell delta is applied**.
+- **The formula set is an input, not a rebuild.** After each model effect the host
+  compares a fingerprint of the formula set, over (`raw`, `target`,
+  `target_category`), with its previous read. If it moved, the formula delta (−the old
+  formulas, +the new ones) is fed to the circuit as an explicit input. The formula
+  layer then re-derives the formula graph (clause 6) and re-evaluates the affected
+  targets at their stems. This is observed, not declared by effect type, as the tiers
+  are. It is what catches a `ReplaceFormula` that keeps its target, which moves no
+  `view_shape`.
+- **A document swap rebuilds every circuit** from the new store. `install_workbook`
+  bumps `document_generation`, and the same after-each-effect read sees it.
 
-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.
+Re-reading the operator shape costs O(items) per view per model effect, and the formula
+fingerprint O(formulas). Neither grows with the cells or the grid. A rebuild costs
+O(cells), once per actual reshape. The same `view_shape` function is therefore read at
+two moments: by the circuit after each effect, and by `layout_version` after the loop.
+They answer different questions, and neither replaces the other.
 
-**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).
+**The worked case is gotcha 43's frame, `[AddItem(East), SetCell(East)]`.** `AddItem`
+moves the operator shape, so the view is rebuilt with East in its sequences. Only then
+does `SetCell`'s delta arrive, at operators that already know East. So the in-loop
+`CellData` frame observation reads occupancy for the new shape. The `LayoutGeometry`
+arm (`app.rs:1062-1071`) reads the frame immediately after each geometry effect, and it
+reads a rebuilt occupancy for the same reason.
+
+**Recommended: a page selection is not a rebuild (question 7).** Under the recommended
+answer, 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. Filter coordinates still filter; only page
+coordinates key the slice. If the user answers the other way, a page change is an
+operator-shape change like any other.
 
 ### 8. Floating point: retraction drifts, and exactness is ADR 005's
 
@@ -356,8 +432,10 @@ the eager fold computes. **Measured**, not asserted:
 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.
+of 10⁻⁵ units rounded to f64 once. Each value is a signed whole number of 10⁻⁵ units:
+up to 99,999 units, times a power of ten spread over 3 or 9 decades. So the smallest
+values carry five decimal places, not the two a user usually types. Two-place input
+would absorb differently, and it was **not** measured.
 
 | store | magnitudes | after 1M cycles: naive vs eager | ≥ `FLOAT_EQ_EPSILON`? | eager vs exact |
 |---|---|---|---|---|
@@ -403,12 +481,15 @@ 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.
+ADR 008 (revision 3, 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
+  Formula cells count by clause 5's stem rule, which is when today's `formula_cache`
+  holds a value: a top-level `WHERE` must match, or raw data must exist at the target.
+  The operators are rebuilt per clause 7, so a batch that reshapes and then writes feeds
+  its write to the new shape. Page coordinates key a slice, subject to question 7. 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
@@ -463,9 +544,20 @@ read-only live source also sidesteps ADR 001's record tier, as ADR 003 already n
   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).
+  (`app.rs:647`). **Recommended (question 9): the backend's state joins the snapshot.**
+  Applying the inverse delta is **not** a rollback, even with exact aggregators. It
+  restores integrated values, but `step(d)` then `step(−d)` still advances the circuit
+  and changes the history that `delay` and `differentiate` hold. So the next step after
+  a "rewind" can differ from the next step after nothing happened. A real rewind would
+  have to restore every stateful operator, with a test of observational equivalence
+  across all of them. This ADR does not propose one.
+
+  **The snapshot costs a second O(cells) clone per mutating frame.**
+  `Host::mutating_frame` already clones the workbook on every mutating frame
+  (`host.rs:162`, `app.rs:627-629`), and the integrated state is of the same order. So
+  on the network path a write is not O(delta): it is O(cells) for the snapshot today,
+  and roughly twice that with the circuit in it. The keyboard path (`apply_effects`
+  without a `Host`) takes no snapshot and keeps the O(delta) cost.
 - **ADR 006, replay (improvise-ilvl).** A circuit is a deterministic function of the
   delta sequence, so replaying commands reproduces its state.
 
@@ -517,16 +609,23 @@ displayed path until the differential test holds.
    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`.
+3. **The cell delta from `DataStore`**, with clause 3's bit identity and its signed-zero
+   and NaN tests. `bump_changed_records` moves onto it. The dirty flag's content half
+   becomes "a non-empty cell delta, or a moved formula-set fingerprint" (clause 3), with
+   a test that a formula edit alone still marks the document dirty. That removes the
+   O(cells) scans per cell write. The existing tier tests are the evidence.
+4. **`Incremental`, for the order-free parts**, under the differential test: stems with
+   clause 5's stem rule, `Count`, `Min`, `Max`, unanimity, occupancy and the occupancy
+   delta, all following clause 7's per-effect operator shape. **ADR 008 clauses 3 and 8
+   (pruning and the frame observation) depend on this step.**
+5. **Formulas**: the formula graph and the formula delta (clause 7), topological
+   re-evaluation, the component fixed point (clause 6), and the aggregate-over-expression
+   map that replaces `Expansion::members` (clause 5). Formula values that depend on a
+   `Sum` or `Avg` read it from the eager fold until step 6. **ADR 008's retirement of
+   `Expansion::members` depends on this step.**
+6. **`Sum` and `Avg`, and column totals, after ADR 005** (or on question 3's
+   fallback). A column total is a formula over the pooled fold, so it needs step 5's
+   re-evaluation. **ADR 008 clause 5 (column totals) depends on this step.**
 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
@@ -535,7 +634,9 @@ improvise-l2b8 (ADR 005) gains a dependant, and a measured argument, from clause
 
 **Good.**
 
-- A write costs O(delta) plus the formula cells it reaches, not O(cells).
+- On the keyboard path, a write's *evaluation* costs O(delta) plus the formula cells it
+  reaches, not O(cells). On the network path, the ADR 001 snapshot still costs O(cells)
+  per mutating frame (see "Bad").
 - 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
@@ -551,6 +652,11 @@ improvise-l2b8 (ADR 005) gains a dependant, and a measured argument, from clause
   the measurement says so.
 - Circularity is decided in two layers: the formula graph's components and the
   per-cell bound.
+- A mutating frame from a client already clones the workbook for rollback
+  (`host.rs:162`). Snapshotting the circuit too (question 9) adds a second O(cells)
+  clone per frame. Incremental evaluation does not make the network path O(delta).
+- The operator shape is re-read after every model effect: O(items) per view, a cost the
+  post-loop `view_shape` diff paid once per batch.
 - The browser bundle grows by two small crates.
 
 ## Open questions
@@ -594,7 +700,8 @@ the user decided", as ADRs 004 and 007 did.
    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.
+   held-key path (`[`/`]`) stays O(visible). Clause 7 is written to this
+   recommendation, and ADR 008 clause 3 says it is "subject to ADR 009 question 7".
 
 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?
@@ -602,13 +709,17 @@ the user decided", as ADRs 004 and 007 did.
    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.
+9. **Rollback.** For ADR 001 clause 4, should the backend's state join the `App`
+   snapshot that `Host::mutating_frame` already takes?
+   *Recommendation:* yes, snapshot, with no later switch to the inverse delta. Applying
+   `−d` restores integrated values but not the history `delay` and `differentiate`
+   hold, so it is not a rewind even with exact aggregators (clause 11). The cost is a
+   second O(cells) clone per mutating frame, beside the workbook clone that exists
+   today. A true rewind would need its own design and an observational-equivalence test
+   over every stateful operator.
 
 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?
+    steps 4, 5 and 6?
     *Recommendation:* yes. The user's decision is recorded on felo.4, and the steps are
     how it is met.