Co-Authored-By: Claude Sonnet 5.5 <noreply@anthropic.com> Claude-Session: https://claude.ai/code/session_01VdfEGXA7aJ6ftMsCc9PJze
17 KiB
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.
Derivedlives 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 apub use, since the trait names only core types). While it sits downstream, core cannot read through it, which is the clause's point.- 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.aggisAggregation, the evaluator's own type. Hidden-itemcovers, 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. raw_foldis never a formula, andEagerenforces it. For a partial naming a formula targetEager::raw_foldisNone; otherwise it isevaluate_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 soEagerstops going round.Eagerrecomputes formulas after every edit. Production does it inrebuild_layout(Model::recompute_formulas(none_cats)), and an over-hidden read of a formula cell reads the cache it fills. SoEagercarries the None categories of the view it stands for and recomputes under them after each edit, as a layout rebuild does.Editis the vocabulary of the harness, not of the wire. Five variants, each one publicModelcall. A later step adds variants for what it maintains (an item added, a category removed); the harness does not care which. AnEditfault reaches both sides of a differential alike, so it is pinned only where a directEagertest reads the result:ClearCell,AddFormulaandRemoveFormula, andSetMeasureAggthrough the fold tests.SetCellis read by nearly every test.- 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.00is not0.00and eager'sMinandMaxreturn the sign they were given. Clause 8 has its own tests for the sign of a zero sum. - The
zsetdependency 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.
DataStorelogs,improvise-incrementalbuilds the Z-set. The ADR says the store "emits aZSet", but core never depends onzset(clause 2).DataStore::record_changesturns on aVec<CellChange>log (Nonewhile off, so an unwatched store keeps nothing),drain_changesempties it andcell_deltafolds it. The log lives in the store, not inModel::set_cell, so every route that writes a cell is seen, includingRemoveCategory's sweep.DeltaValuecanonicalises on construction: every NaN becomesf64::NAN,-0.0becomes+0.0, and the order istotal_cmpon 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'sEqual, so==andOrdagree.CellKeyisOrdby 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.- 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.
- The dirty flag needs two inputs the ADR does not name. Besides a non-empty delta and
the formula set,
document_configstays (anAddItemwrites no cell and the existing test requires it dirty) and the saved order joins, which no delta carries:DataStore::reorderscountsSortData, 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). document_generationand the wire are untouched, andEagerand theDerivedtrait 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 withEager.
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.
Readingis how a view reads. The aggregation (Aggregation::ofits None categories) and the hidden(category, item)pairs ofView::hidden_items.covers(cat, item)is the predicateGridLayout::evaluatorpasses as itscovers. 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;Eagermirrors production in both.- Three methods join the trait:
covered(key, reading)isModel::evaluate_covering;total(key, over, reading)isevaluate_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 matchingpartial, 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" (whatprune_emptyasks) iscovered(..).is_some(), already probed. drawn_probes(model, views, none_cats)asks what each view draws, built from the view's ownGridLayout(pruned as production builds it): for every drawn cell the three subset questions plusCoveredandOccupancy; for every column itscolumn_keyoccupancy and, whereGridLayout::draws_totals(the conditiongrid_bodyalso reads), aTotalover 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/_Dimcoordinates 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, sinceEagerrecomputes 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;differentialis that with no views. A view is aView, not a document, because the model holds none.sub_partialsis polynomial: it enumerates the sets of at mostMAX_DROPPEDdropped 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_DROPPEDstays: it bounds the subset probes, and the drawn probes carry the cells that drop more.- 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 directEager-against-evaluator comparison as well. ProbeisHash + Eq, soAskeddeduplicates on the probe itself (AggregationgainedHashin 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.
-
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
Shapemaps the projection of a stored cell onto those categories to aGroup, 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. -
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.Shapesholds its map in aRefCellbecauseDerivedreads take&self; the cell is private toshapes.rsand no reference to it leaves a method. -
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, soSetMeasureAggrebuilds nothing. A read of several groups (a collapsed group, a total) folds their union without merging them:fold_groupssums the counts and takes the smallest of the groups' minima, the largest of their maxima, or the one value they share. -
Eager's rules are reproduced, not improved. An all-numbers group reduces; any other group is unanimous or
Error("mixed"), soCountof a group holding text is that text.MinandMaxskip NaN and are+inf/-infover only NaN, asfold(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 inCellValue's==and is a distinct key here. -
SumandAvgstay with the store until step 6. Their eager result depends on the order the cells are added in (insertion order in the store, notCellKeyorder, whatever clause 3 says), so a group cannot reproduce it without keeping that order. The backend routes a read whose measure aggregation isSumorAvgtoModel::evaluate_coveringandevaluate_spanning, which is eager's own path. Step 6 replaces both sides withExactSum. BecauseSumis the default, the corpus reaches the groups only once aSetMeasureAggedit has changed a measure; the differential tests apply those on purpose. -
Formulas stay with the model until step 5. A key a formula owns is read through the model, and
applycallsModel::recompute_formulas, asEagerdoes. Step 5 replaces the call. -
A fold is the union of its members' groups.
fold.rsisModel::group_expansionread off the public model: the cross product of the covered members of every group the key names and every covered item of every category inoverthat it omits. UnderOverHiddenthe members are groups of one shape (the base's categories plus the spans'). UnderExactthe cells admitted are exactly the member keys, so the read is a lookup per member and a throwawayGroup. 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"). -
Occupancy counts by inclusion and exclusion.
occupancy(partial)is the cells underpartial, 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. -
The meter counts operations.
Meterisupdates(group updates a delta caused),reads(groups a read looked at),buildsandbuilt_cells.tests/measure.rsfixes 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 ismatching_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. -
MinandMaxkeep the sign of a zero. The multiset calls-0.0and+0.0one value (clause 3), so a group also counts its negative zeros from the raw change log, as step 6's sums are fed. Eager'sf64::minandf64::maxleave the sign of a tie between the two zeros to the platform and the order (fminon 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,Minis-0.0andMaxis+0.0, which is what ARM'sfmin/fmaxreturn; on other platforms eager may differ there, andtests/random.rskeeps+0.0out of its pool for that reason.
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.