From 322875b30affcf751b8a43148d6d3694a026e8d3 Mon Sep 17 00:00:00 2001 From: Edward Langley Date: Thu, 24 Sep 2026 20:14:37 -0700 Subject: [PATCH] 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) Claude-Session: https://claude.ai/code/session_01VdfEGXA7aJ6ftMsCc9PJze --- context/adr/009-incremental-evaluation.md | 612 ++++++++++++++++++ .../examples/retraction_drift.rs | 191 ++++++ scripts/build-doc-site.mjs | 1 + 3 files changed, 804 insertions(+) create mode 100644 context/adr/009-incremental-evaluation.md create mode 100644 crates/improvise-core/examples/retraction_drift.rs diff --git a/context/adr/009-incremental-evaluation.md b/context/adr/009-incremental-evaluation.md new file mode 100644 index 00000000..b61fe0ad --- /dev/null +++ b/context/adr/009-incremental-evaluation.md @@ -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`**: 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` into an indexed Z-set `K → ZSet`, 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` 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`, 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. diff --git a/crates/improvise-core/examples/retraction_drift.rs b/crates/improvise-core/examples/retraction_drift.rs new file mode 100644 index 00000000..9e627378 --- /dev/null +++ b/crates/improvise-core/examples/retraction_drift.rs @@ -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::() 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) { + let mut m = Model::new("drift"); + m.add_category("Row").expect("under the limit"); + let values: Vec = (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(); +} diff --git a/scripts/build-doc-site.mjs b/scripts/build-doc-site.mjs index f9bab7b3..a2967458 100644 --- a/scripts/build-doc-site.mjs +++ b/scripts/build-doc-site.mjs @@ -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)"], ], }, {