improvise/context/code/improvise-incremental.md

improvise-incremental: the reasoning

crates/improvise-incremental began as 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 backend is checked with, and, from step 4 (improvise-u2le), the first backend that keeps state, Incremental (section "Step 4" below). The step 2 sections describe the trait and the oracle; they predate the backend. The decisions are the ADR's (context/adr/009-incremental-evaluation.md). 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
Incremental	the backend of step 4: maintained groups and occupancy; formulas and Sum/Avg still go to the model (later steps change that)

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 joined the trait in improvise-bw4p.3 (section "Step 4 groundwork"). 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, except the two zeros: they differ, since a drawn -0.00 is not 0.00 and eager's Min and Max return the sign they were given. Clause 8 has its own tests for the sign of a zero sum.
7. The zset dependency arrived with step 3, as the cell delta (below).

Step 3: the cell delta (improvise-5r8c)

delta.rs holds DeltaValue, CellDelta = ZSet<(CellKey, DeltaValue)>, cell_delta and moved_records. improvise-command's apply_effects reads them for the record tier and the dirty flag (context/code/command.md). Evidence: context/test-evidence/improvise-incremental.md. These are the readings taken, where ADR 009 clause 3 leaves a choice.

1. DataStore logs, improvise-incremental builds the Z-set. The ADR says the store "emits a ZSet", but core never depends on zset (clause 2). DataStore::record_changes turns on a Vec<CellChange> log (None while off, so an unwatched store keeps nothing), drain_changes empties it and cell_delta folds it. The log lives in the store, not in Model::set_cell, so every route that writes a cell is seen, including RemoveCategory's sweep.
2. DeltaValue canonicalises on construction: every NaN becomes f64::NAN, -0.0 becomes +0.0, and the order is total_cmp on the result, with numbers before text before errors. The inner value is private, so a non-canonical one cannot be built. Equality is the order's Equal, so == and Ord agree.
3. CellKey is Ord by derivation: the sorted coordinate pairs, compared as strings. Clause 3 calls this "the natural order of ids", which ADR 007's id form will change; the derive then moves with the key type.
4. The record tier is the set of records a consolidated batch delta names. A cell written and written back inside one batch cancels, as the old XOR did.
5. The dirty flag needs two inputs the ADR does not name. Besides a non-empty delta and the formula set, document_config stays (an AddItem writes no cell and the existing test requires it dirty) and the saved order joins, which no delta carries: DataStore::reorders counts SortData, and any logged insertion or removal dirties too, because a clear-then-set of one value nets to zero yet moves the cell to the end of the store (a same-item rename).
6. document_generation and the wire are untouched, and Eager and the Derived trait are not used: no backend consumes the delta yet. The differential for this step is the delta against the store it describes (the_cell_delta_of_an_edit_is_...), since there is nothing to compare with Eager.

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>.

Step 4 groundwork: what a view draws (improvise-bw4p.3, improvise-bw4p.4)

The subset probes above cannot see a drawn cell on a view with four or more None categories (it drops more than MAX_DROPPED coordinates of a stored key), and the trait could not be asked about hidden items, totals or occupancy. Both are closed. These are the readings taken.

1. Reading is how a view reads. The aggregation (Aggregation::of its None categories) and the hidden (category, item) pairs of View::hidden_items. covers(cat, item) is the predicate GridLayout::evaluator passes as its covers. It is a value, not a closure, so a probe can name it and a divergence can print it. A fold over a group or a spanned category leaves hidden members out; a read of a key naming neither does not (a hidden East still counts in {Product=A} when Region is None), while an occupancy count always leaves them out. The count follows the drawn items, not the value; Eager mirrors production in both.
2. Three methods join the trait: covered(key, reading) is Model::evaluate_covering; total(key, over, reading) is evaluate_spanning, a column total as ONE fold over the visible items of the omitted categories; occupancy(partial, reading) is ADR 009 clause 7's count by axis item: the stored cells matching partial, none of whose coordinates is hidden, where a coordinate naming a group matches every stored member of that group (a collapsed group is a remap, so the Coastal line of two visible members counts 2). A key naming a formula target has no stored cells and is not asked. "Has a value" (what prune_empty asks) is covered(..).is_some(), already probed.
3. drawn_probes(model, views, none_cats) asks what each view draws, built from the view's own GridLayout (pruned as production builds it): for every drawn cell the three subset questions plus Covered and Occupancy; for every column its column_key occupancy and, where GridLayout::draws_totals (the condition grid_body also reads), a Total over the row categories; for every row the occupancy of its cell key less the column coordinates. Lines carry the page coordinates, as a cell's key does, so a page is its own slice. A records view is skipped: its keys are synthetic _Index/_Dim coordinates naming no stored cell and it has no totals, while its stored keys are the subset probes' business. A view whose None categories differ from the oracle's is skipped, since Eager recomputes its formulas under one set (a backend keeping a cache per aggregation class is therefore not exercised on the others). differential_in(model, views, ..) adds them at every step; differential is that with no views. A view is a View, not a document, because the model holds none.
4. sub_partials is polynomial: it enumerates the sets of at most MAX_DROPPED dropped indices, not the 2^n masks. The probe set is unchanged for every key length (a test compares it with the old walk up to 12 coordinates, and counts it at 64). MAX_DROPPED stays: it bounds the subset probes, and the drawn probes carry the cells that drop more.
5. The hidden fixture is a workbook the corpus now includes (hidden): no shipped demo hides an item, so a backend wrong about hidden items would have passed the direct Eager-against-evaluator comparison as well.
6. Probe is Hash + Eq, so Asked deduplicates on the probe itself (Aggregation gained Hash in core for it).

Step 4: the incremental backend (improvise-u2le)

Incremental (incremental.rs) is the first Derived that keeps state. It owns a Model (the store) and Shapes (shapes.rs, the groups). Maintained::apply applies the edit to the model, drains the store's change log into a CellDelta and feeds the delta to every shape. A read asks a group, never the store, for what step 4 owns. The rest of this section is the readings taken where clause 4 and clause 7 leave a choice; evidence is in context/test-evidence/improvise-incremental.md.

1. A shape is a set of category names, not a None list. Clause 4 says "a group is the cell key minus the None categories". The trait is asked about keys of any category set (the harness drops up to three coordinates of a stored key), so the unit is the set a key names: a Shape maps the projection of a stored cell onto those categories to a Group, and a cell lands in it only if it has all of them. A view's None list is one of these sets. Clause 7's "one circuit serves every shape key with the same None list" holds trivially, since the sets are shared by every reader.

2. A shape is built on its first read, by one pass over the store, and fed every delta after. Clause 7 makes a new key's first build a sliced job under ADR 008's job runner. That runner does not exist, so the pass is synchronous and counted (Meter::builds, built_cells). Nothing evicts a shape. Shapes holds its map in a RefCell because Derived reads take &self; the cell is private to shapes.rs and no reference to it leaves a method.

3. A group is a count, a count of numbers and a multiset (group.rs). One update touches one map entry (O(log d)); the count and the multiset serve every function, so SetMeasureAgg rebuilds nothing. A read of several groups (a collapsed group, a total) folds their union without merging them: fold_groups sums the counts and takes the smallest of the groups' minima, the largest of their maxima, or the one value they share.

4. Eager's rules are reproduced, not improved (superseded for NaN and zeros by "Eager's math, fixed" below). An all-numbers group reduces; any other group is unanimous or Error("mixed"), so Count of a group holding text is that text. Min and Max skip NaN and are +inf/-inf over only NaN, as fold(INFINITY, f64::min) is. The multiset orders by the delta's total order, with NaN last, so the skip is a step past one key. A group holding a NaN and a non-number is mixed, because NaN is not equal to itself in CellValue's == and is a distinct key here.

5. Sum and Avg stay with the store until step 6. Their eager result depends on the order the cells are added in (insertion order in the store, not CellKey order, whatever clause 3 says), so a group cannot reproduce it without keeping that order. The backend routes a read whose measure aggregation is Sum or Avg to Model::evaluate_covering and evaluate_spanning, which is eager's own path. Step 6 replaces both sides with ExactSum. Because Sum is the default, the corpus reaches the groups only once a SetMeasureAgg edit has changed a measure; the differential tests apply those on purpose.

6. Formulas stay with the model until step 5. A key a formula owns is read through the model, and apply calls Model::recompute_formulas, as Eager does. Step 5 replaces the call.

7. A fold is the union of its members' groups. fold.rs is Model::group_expansion read off the public model: the cross product of the covered members of every group the key names and every covered item of every category in over that it omits. Under OverHidden the members are groups of one shape (the base's categories plus the spans'). Under Exact the cells admitted are exactly the member keys, so the read is a lookup per member and a throwaway Group. A total therefore reads one group per covered row, not one per stored cell, but still one per row: clause 7's maintained totals with a subtracted hidden overlay are not built (see "Not built").

8. Occupancy counts by inclusion and exclusion. occupancy(partial) is the cells under partial, where a coordinate naming a group matches each of its members' items, with no hidden coordinate. For each way of choosing a member per group coordinate the count is the group's cell count, less the cells holding a hidden item of a category the key leaves free, by inclusion and exclusion over those categories: N(P) - sum N(P + h) + .... The cost is the product of the hidden items per free category, a group read each. A key naming a hidden item itself is zero.

9. The meter counts operations. Meter is updates (group updates a delta caused), reads (groups a read looked at), builds and built_cells. tests/measure.rs fixes one table at two sizes and asserts the counts: an overwrite costs two updates per shape whatever the table holds, and a read of a group of 36 or 72 cells costs one group. Eager's cost for the same read is matching_values().len(), which the test prints beside it. This is the local fixture the brief asked for; ADR 009 step 4 says "measured at ADR 008's fixture", which needs ADR 008 (unapproved) and is deferred.

10. Min and Max keep the sign of a zero. The multiset calls -0.0 and +0.0 one value (clause 3), so a group also counts its negative zeros from the raw change log, as step 6's sums are fed. Eager's f64::min and f64::max leave the sign of a tie between the two zeros to the platform and the order (fmin on ARM returns -0.0; x86 may not). The backend reproduces the part that does not depend on either: all zeros negative gives -0.0, all positive gives +0.0. With both, Min is -0.0 and Max is +0.0; eager now returns the same (see "Eager's math, fixed").

Not built in step 4

• Maintained totals (clause 7): a total reads one group per covered row.
• Eviction of shapes, and the build as a sliced job.
• Sum, Avg (step 6) and formulas (step 5) are eager's, behind the same trait.
• The ADR 008 fixture measurement.

Step 5: formulas (improvise-shbc)

Incremental calls recompute_formulas only for the documents item 2 calls wide. Otherwise it keeps the formula cache itself (Model::formula_cell, set_formula_cell, clear_formula_cells and the now-public evaluate_formula_cell, the small additions to improvise-core) and decides which cells of it to evaluate again; the evaluator that computes each value is core's own. The ADR (clauses 5 and 6) is followed in outline, and the places it is not are the reason for this section.

1. A stem is the unit, because eager's cache is per stem. Stems (formulas.rs) holds, per target category, how many stored cells give each stem (a cell minus that category and the None categories, as recompute_formulas derives them), and which stems at least one category gives (live). Counts come from the raw store changes, one net count per stem per category per batch, so an overwrite never makes a stem vanish and reappear. A stem that appears is evaluated; one that goes has its cells removed.
2. A stem's cells are evaluated from nothing. recompute_formulas clears the cache and runs fixed-point passes over every stem together. When no formula reads another stem's cache the stems are independent, so running the same passes on one stem from an empty cache gives exactly what the whole run gives for it, including circular for a cell still moving after sixteen passes. That is why a dirty stem is cleared first (passes-start-warm shows what a warm start changes). Where they are not independent (Stems::is_wide: two target categories, or a name in another category that is not None) the backend falls back to recompute_formulas for the whole cache, so those documents are exact and not incremental.
3. Which stems a change reaches is a superset, read off the formulas. For formula f, Reads is the set of names in its expression and in the formulas those names target, and the categories that puts in play (its target's, every name's, every WHERE's and IS's). A stored cell can change what f evaluates to at stem s only if it agrees with s everywhere outside those categories. Readers indexes each live stem by what is left of it outside them, per category set, so a changed cell finds its stems by looking up its own projection on each set: no scan of the stems. This is clause 5's input rule made coarser, once for every shape of formula: it re-evaluates a stem for a cell of an item the formula never names (a change to a Note cell evaluates the stems Profit has). It cannot miss one, which is what the aggregate over an expression needs, since the cells it reads are chosen at run time by the records.
4. The aggregate-over-expression pipeline (clause 5, items 1 to 3) is not built. A dirty stem evaluates its formulas whole, so SUM(Revenue * Price) is re-folded over its records when any cell under the stem changes, not adjusted for the one record. That needs the evaluator to accept a maintained aggregate in place of folding, which is a change to core's evaluator and to the order its records are visited in (insertion order, not CellKey order). It is a bead.
5. Dependency order is an optimisation and is checked against the plain passes (the NaN and zero differences below are gone: "Eager's math, fixed"). Order is the formulas' dependency graph by name. When it has no cycle and there are fewer formulas than passes, one evaluation per cell in dependency order reaches the fixed point eager's passes reach (a chain of fifteen links needs fifteen passes and a sixteenth to see no change). It is the same fixed point, because Eager's convergence test compares by bits ("Eager's math, fixed"). Evaluation::Plain always runs the passes; tests/ordering.rs compares the two after every edit, zero signs included, and tests/formulas.rs compares both with eager.
6. A formula edit rebuilds the stems. Adding, removing or replacing a formula (the fingerprint of the formula list moves) rebuilds the stems from the store by one pass, clears the cache and evaluates every stem, because a formula has a cell at each. Clause 5 wants a formula delta; the index is not maintained across a formula edit. Meter::rebuilds counts it.
7. A new aggregation dirties the stems it can reach. measure_agg is not a cell, so no change reaches the readers. A fold under a None category takes its aggregation from the _Measure coordinate of the key, which for a formula targeting another category comes from the stem and from no name the formula reads, so every live stem carrying that measure is dirtied (Stems::carrying). Where a formula names the measure (it targets _Measure) reads_name dirties every stem.
8. A write of the same bits changes nothing; a write of -0.0 over 0.0 does. The cell delta treats the two as one value (clause 3), but a formula may not (Units ^ -1 is inf and -inf), so the formula side reads the raw change log, not the canonical delta.

Not built in step 5

• The aggregate-over-expression pipeline and the per-record order key (item 4).
• Stems that survive a formula edit (item 6), and name-level selectivity within a stem (item 3).
• Incremental cache for documents with formulas in more than one target category, or a name in a non-None category other than the formula's own (item 2): they use the whole recompute.
• Strongly connected components as a maintained structure: Order is rebuilt with the stems, which is O(formulas) on a formula edit, and cycles are found by depth-first search, not Tarjan's.

Step 6: Sum, Avg and totals through an exact sum (improvise-hrjz)

ADR 009 clause 8, in both backends. Sum and Avg stop being the one reading that went to the store: a group now holds a numtower::ExactSum beside its counts and multiset, and Reduce (was OrderFree) has all five functions. Step 4's delegation, and its sentence in section 5 of that step, are gone; formula-owned keys still go to the model, whose cache step 5 maintains.

1. ExactSum already signs a zero total (numtower/src/sum.rs, PR #348, written for step 8's last test): -0.0 only if every finite addend is -0.0, +0.0 for any other zero, an exact cancellation included. An earlier version of this step wrote that rule as a wrapper, FloatSum; it was dropped when gh/main brought the same rule into ExactSum, and the tests of the rule are that PR's tests/zero_sign.rs. One difference from the wrapper: an empty sum reads +0.0, where Sum for f64 starts at -0.0. Core's SUM over no rows therefore changes from -0.0 to +0.0 (a formula SUM whose WHERE matches nothing); a_formula_sum_over_nothing_is_positive_zero, in core, pins it.
2. Core sums through it. apply_agg (Sum, Avg) and the formula-level SUM in eval_agg call exact_sum, so Eager is exact, and so is every reading of the model, with no flag: the user visible change clause 8 names (displayed sums change in their last bits) is this commit. improvise-core gains the numtower dependency; both of the new edges are in Cargo.nix and the harness lock.
3. A group's sum is fed from the raw changes, not the cell delta. The delta calls -0.0 and +0.0 one value (clause 3), so an overwrite of 0.0 by -0.0 is no delta at all, yet it moves the sign of a zero sum. Shape::apply takes the delta for counts and the multiset and the change log for sums, skipping only a change that left the same bits. The ADR's two clauses 3 and 8 are consistent only because the sum reads the store's values and not the delta's. The cost is a second walk of the batch per shape.
4. Totals and collapsed groups absorb. A read of several groups (total, a collapsed group, a hidden member left out) adds their accumulators with absorb and reads once, so a total is the same bits whatever the grouping and whatever the order of the rows. The clause 7 hidden overlay (subtracting the hidden cells from a kept total) is still not built; a total is a union of member groups, not a kept total less an overlay.
5. Avg is the exact total over the cell count, rounded once (ExactSum::mean). The first version divided a rounded sum, which rounds twice and overflows with the sum: Avg([MAX, MAX]) was inf and a correctly rounded mean differs from the twice-rounded one for about 2% of random multisets. Both backends now use mean, so this is a second user-visible numeric change beside the sums: a displayed average can differ in its last bit, and a mean whose sum would overflow is finite. numtower/tests/mean.rs checks it against exact rationals.
6. What a group costs. An ExactSum is 70 limbs of i64 and a few counters, about 650 bytes (size_of), in every group of every shape, whether or not the measure is summed. Clause 8 accepts 568 bytes "per summed group"; here the shape does not know which measure its groups serve, so a shape at cell granularity (a read of a full key) pays it for each cell. Sparing groups that are never summed, or holding the sum only above one cell, is the improvement; it is a bead.
7. The drift test is 20,000 overwrites, not a million. ADR 009 measured 1.7e-9 at 18,000 cells after a million cycles. tests/exact.rs runs 20,000 overwrites of a 1,000-cell group with values chosen so an f64 sum drifts, and asserts the two backends equal each other and a sum built afresh to the bit. The count is what a test binary can afford; the property it pins is independent of it.

Not built in step 6

• The hidden overlay and kept totals (clause 7).
• A group that does not pay for a sum it never reads (item 6).

Eager's math, fixed (user ruling 2026-10-10)

"Don't reproduce math bugs you might find in the Eager mode." Every place the earlier steps matched Eager's arithmetic "as eager does" was reviewed. The items below supersede the sentences in steps 4 and 5 that say otherwise (step 4 items 4 and 10, step 5 item 5). Each is a user-visible numeric change.

1. Min and Max of both zeros is -0.0 and +0.0, whatever the order or the platform. Core's fold used f64::min and f64::max, whose tie between the zeros is left to the platform; it now orders by total_cmp over the non-NaN values. Incremental already returned this. (improvise-bw4p.20)
2. Min and Max over only NaN are NaN, where they were +inf and -inf (the seed of the old fold leaking out). NaN among numbers is still skipped.
3. A NaN formula result is a value, not a cycle. The fixed point compared cached cells with !=, so a cell that settled on NaN never settled and became circular, dragging the cells that read it. It now compares with model::types::settled: numbers by bits, every NaN one value. A cell that really oscillates is still circular after sixteen passes. mark_nan_circular is gone.
4. A zero's sign is a change. settled compares by bits, so 0.0 becoming -0.0 between passes moves the cell, and eager's fixed point and dependency order's agree. Dependency order is the unique fixed point of an acyclic set under bit equality, up to NaN payload and sign (settled merges NaNs): each cell is a function of the final values it reads. So the holds_a_zero fallback is dropped and Ordered needs no extra precondition.
5. Empty SUM is +0.0 (step 6), listed here for completeness.
6. Cycles over zeros and NaN. A cycle that only flips a zero's sign (X = -X, X = X * -1, IF(X < 1, -X, X), A = -B with B = A over zeros) used to settle, because -0.0 == 0.0; it is now circular, as the same cycle over nonzero data always was. A cycle fed a NaN (A = A + 1, or A = A with A NaN) used to be circular and now settles on NaN.
7. Min and Max skip NaN while Sum and Avg propagate it. Kept: it is IEEE's minimumNumber and maximumNumber for the extremes and ordinary addition for the sums, and consistent with ADR 005. Whether a spreadsheet user expects one rule for both is a product question (bead text in the hand-back).

Left alone, with the reasoning

• Count of a group that holds text returns the text (the unanimity branch of aggregate_cell_values), not the number of cells. That is probably not what a user wants, but it is a decision about what a Count measure means for non-numbers, not an arithmetic error, so it is filed rather than changed.
• The division and equality epsilon (FLOAT_EQ_EPSILON, 1e-10) is shared and deliberate (gotcha 17).
• A group holding NaN beside text is mixed: NaN is a number and text is not, so no unanimity exists.
• Avg and Sum are already exact and correctly rounded (step 6).
• Overflow of the exact sum to infinity follows ExactSum::value (round to nearest, so an overflowing total is infinite): correct IEEE behaviour.

Step 7: live sources (improvise-rnak)

ADR 009 clause 2 names two kinds of live source: one that reports its changes, which feeds cell deltas like DataStore, and one that answers aggregate queries but reports none, which implements the derived value by pushdown. The core half of both is in context/code/source.md (CellSource, Model::over). The brief ordered this half after the evaluator hook; the hook came first because a source that reports changes still has its formulas evaluated over it. User ruling 2026-10-10: formulas are computed in RAM from the source's folds, never pushed down; Derived stays in this crate.

Change-reporting (Incremental::over)

1. ChangeSource is CellSource plus drain_changes(&self), and a source's cells are those as of the last drain. A shape is built lazily, by a pass over the source, at its first read. If a source showed a write before reporting it, a shape built in between would hold the write and the next drain would add it again. So the contract is that nothing is visible until it is drained, which is what a database does inside a read transaction and what DataStore does already (its log is drained in the step that made the edit). &self because a live source is shared with the model that reads it and changes behind it by interior mutability of its own.
2. Incremental::over(model, feed, none_cats) takes a SharedFeed, the alias core exports (a generic Arc<S> could not take it: S is Sized). The model is put over the feed (Model::over), which drops the cells it came with, so none is left for get_cell, persistence or the harness to read. Its categories, formulas and aggregations are the definition; the source holds the data. Shapes and stems are built from the feed as it stands.
3. sync() drains and maintains; apply_changes(&[CellChange]) maintains changes the source already reflects, for a source whose changes reach the backend by another route (a trigger table, a channel). Maintained::apply on a fed backend takes definition edits (a formula, an aggregation) and drains: a cell edit is the source's to make, and apply refuses it with an assert! in every build (a release build lost it silently when only Model::set_cell's debug_assert stood in the way). A feed has one drainer: a drain is destructive, so two backends over one feed split its changes (context/code/source.md, ChangeSource).
4. Freshness is the source's. ADR 003 left "polled, triggered, or stale until refreshed" open: sync is the poll, and when it is called is the host's decision. Nothing here schedules it.
5. What a change costs is what it costs for the owned store: two group updates and two exact-sum updates per maintained shape, no pass over the source (the_cost_of_a_reported_change_... counts the rows the source serves for snapshots: zero after the build). Formulas are evaluated at the stems the change reaches, as in step 5.
6. Three routes into the store were routed through the source: Shape::of (the build) reads cells(&[]), Stems::build reads keys(&[]), and Incremental::read reads value_at. Eager::occupancy reads keys(&[]) too, so an Eager over a source would answer it.

tests/support/live.rs holds LiveTable, the scripted source (an indexed store behind a lock, with a pending list and a counter of snapshot rows) and Fed, an Incremental over one that a differential can drive: a cell edit becomes a write to the table followed by sync.

Query pushdown (Pushdown)

For a source that answers aggregate queries and reports nothing. Pushdown::new(definition, source, none_cats) puts the model over the source (Model::over) and keeps nothing else: no shapes, no change log, no stems. These are the readings taken.

1. AggregateQuery is CellSource; there are two traits, not three. The brief's AggregateQuery (fold, count) is the trait core already has: summarize is the fold, count the count. Derived stays here (user ruling) and stays a different thing: the values a view draws, which a backend builds from a source's aggregates and its own state. A source implements CellSource and a backend implements Derived.
2. Folds are queries, formula cells are computed in RAM. value, raw_fold, covered and total are the model's evaluator over Model::source(), so a fold is one summarize and the rest is arithmetic on the answers. The formula cache is the one thing Pushdown holds. That is the user's ruling (2026-10-10), and it makes the evaluator hook the only change to core's evaluation.
3. Staleness is refresh(). A stored cell or a fold is current at the moment of the read. A formula cell is the cache's value until refresh recomputes it from the source as it now stands, which costs one distinct_without per formula and the folds each formula reads. When to refresh is the host's (ADR 003's "polled, triggered, or explicitly stale"); nothing here schedules it. A delivery layer that wants notices from a pushdown-backed shape has no moved keys to name, so it marks them "correct" (ADR 009 clause 9), which is a bead (below).
4. Occupancy is one count. A group in the partial becomes a span over its own name and its members; the view's hidden pairs go as excluding. Eager::occupancy lists every key to say the same thing.
5. define(edit) takes a formula or an aggregation edit and refreshes. A cell edit is the source's: Model::set_cell refuses it in a debug build.
6. What the differential proves, and what it does not. value, raw_fold, covered and total are the same four functions for Eager and Pushdown (reads.rs; they were copies, and are shared now), so a Pushdown-against-Eager differential cannot see a mistake in them. Pushdown::members repeats Eager::group_holds in a different form (a span list against a predicate), and that repetition is compared. What the differential proves is the source's semantics: that summarize, count and distinct_without give, for every select the evaluator and the views make, the answers a DataStore gives. The evaluator over a source is proven equal to the evaluator over the owned store in improvise-core (over_tests). Nothing else is claimed.
7. A refresh wants one snapshot. refresh asks distinct_without and then folds, so a source that changes between the queries can serve them from different revisions. The passes heal what they can: a write between two folds is read again by the next pass, and the cache ends equal to the new state's values (writes_between_two_queries_of_a_refresh_are_healed_by_the_fixed_point). A stem that appears after the stem list was taken has no cell until the next refresh (a_stem_that_appears_between_the_stem_list_and_the_folds_waits_for_the_next_refresh). A real source should serve a refresh from one read transaction; nothing here can ask it to.
8. The order of the stems is part of the contract. The passes of the fixed point visit stems in the order distinct_without lists them, and a document whose stems read each other settles in as many passes as its dependency chain runs against that order, with a bound of sixteen. A chain of eighteen stems settles in one pass listed along the chain and not at all listed against it (the_order_stems_are_listed_in_decides_a_result_and_a_source_must_keep_it). No fixture before it had a result that depended on the order, and a source listing stems sorted passed everything. The first-seen order is DataStore's insertion order; a source with no order of its own must fix one.
9. What is and is not proven. The tests run against Remote (tests/support/remote.rs), a scanning in-memory table with counters, that shares no evaluator with Eager and answers queries over rows. Without a real SQL engine only the contract is proven: that a source answering these six queries as specified gives Eager's answers, and what each read costs in queries. Nothing here shows that SQLite can answer summarize exactly (an exact sum is not what its SUM returns: context/code/source.md), or what a query costs. The first real source is improvise-rucf, still deferred.

What step 7 did not predict

• The hook came before the change feed, not after (a fed backend's formulas are evaluated over the source; see context/code/source.md).
• TableSource and LiveTable found nothing in Incremental; the corpus and the random edits pass over a source on the first run. What the tests found was in the fixtures: a rival that read the owned store for the stored fallback of a filtered formula passed until a cell was stored where the WHERE fails, and a rival that forgot a group's own name as an item passed until a cell was stored under one.
• The two-second limit decided the shape of the tests more than the design did: the corpus differential over a scanning source is 2.5s untrimmed, so it follows corpus_eager's trimming, and each random test is its own binary.