improvise/context/test-evidence/improvise-incremental.md

Test evidence: improvise-incremental

What each test guards, which rival it was run against, and where that rival failed. The reasoning is in context/code/improvise-incremental.md; the decisions are ADR 009 clause 2's.

How the rivals are kept. The the_harness_catches_* tests run differential on a Rival, an Eager told every edit and wrong in one way, and assert the step at which the harness reports the divergence. They run on every build, so each rival is watched failing on every run and not once by hand.

Injected in the source. Eighteen faults were put into src/eager.rs, src/harness.rs and src/edit.rs one at a time, each run against the whole suite and each reverted and followed by a full rerun. The failing tests, by name (a fault no test names survived, and none did):

• Eager::value ignores its Aggregation: eager_follows_an_edit_to_the_cell_a_fold_reads, eager_matches_the_evaluator_on_the_shipped_documents, eager_raw_fold_is_never_a_formula, eager_value_reads_a_formula_exactly_and_folded, the_harness_catches_a_backend_that_ignores_the_aggregation, the_harness_catches_a_wrong_folded_formula_value;
• Eager::raw_fold reads Exact: eager_raw_fold_sums_by_default, eager_raw_fold_follows_the_measures_aggregation, eager_raw_fold_of_text_is_unanimous_or_mixed, eager_numbers_among_text_are_mixed, eager_follows_an_edit_to_the_cell_a_fold_reads, eager_matches_the_evaluator_on_the_shipped_documents, the_harness_catches_a_raw_fold_that_returns_a_formula;
• Eager::raw_fold returns a formula's value: eager_raw_fold_is_never_a_formula, eager_matches_the_evaluator_on_the_shipped_documents, the_harness_catches_a_raw_fold_that_returns_a_formula;
• Eager::apply does not recompute formulas: eager_follows_an_edit_to_the_cell_a_fold_reads, a_maintained_eager_equals_a_fresh_one_over_random_edit_sequences;
• the harness compares only the first edit: the_harness_catches_a_backend_that_ignores_a_clear, …_ignores_the_measure_aggregation, …_goes_stale_after_two_edits, the_harness_catches_a_backend_that_keeps_answering_for_a_removed_formula;
• the harness never reports a divergence: all nine the_harness_catches_* tests;
• same_value always true: same_value_follows_the_float_rules_and_is_exact_elsewhere and four the_harness_catches_* tests;
• same_value NaN unequal, signed zero by bits, any two text equal: each fails same_value_follows_the_float_rules_and_is_exact_elsewhere and nothing else;
• probes omit formula cells: probes_cover_folds_formulas_measures_and_groups and four the_harness_catches_* tests;
• probes drop at most one coordinate: probes_cover_folds_formulas_measures_and_groups, the_harness_catches_a_fault_that_only_shows_after_two_coordinates_are_dropped;
• probes omit raw folds: probes_cover_folds_formulas_measures_and_groups, an_edit_names_its_key_as_two_value_probes_and_a_fold, the_harness_catches_a_raw_fold_that_returns_a_formula;
• probes omit group keys: probes_cover_folds_formulas_measures_and_groups, the_harness_catches_a_wrong_group_fold;
• the probe history is forgotten between steps: …_goes_stale_after_two_edits, …_ignores_a_clear, the_harness_catches_a_backend_that_keeps_answering_for_a_removed_formula;
• edit_probes names nothing: an_edit_names_its_key_as_two_value_probes_and_a_fold;
• Edit::AddFormula as a no-op: eager_add_and_remove_formula_change_what_a_key_reads;
• Edit::ClearCell applied as SetCell(0.0), which both sides of a differential share and so only a direct Eager test can see: eager_clear_cell_leaves_the_key_absent.

eager_raw_fold_sums_by_default

Hand-computed: Revenue under Product A is 10 + 5 = 15. Fails on the raw_fold-reads-Exact rival (a partial key names no stored cell, so the answer is None).

eager_raw_fold_follows_the_measures_aggregation

After measure_agg[Revenue] = Max the same fold is 10, and Cost, unchanged, still sums to 6. A fold that always sums fails on the first; one that always takes the maximum fails on the second.

eager_raw_fold_of_text_is_unanimous_or_mixed

Note under A is two equal texts and reads as that text; under B it is two different texts and reads Error("mixed"). A fold that drops text, which the evaluator used to do (gotcha 7), returns None for both.

eager_numbers_among_text_are_mixed

A text among numbers is Error("mixed"), not the sum of the numbers.

eager_value_reads_a_formula_exactly_and_folded

Profit = Revenue - Cost reads 6 at East/A exactly, and 9 at Product A with Region over hidden: (10 + 5) - (4 + 2), the fold taken before the subtraction. Fails on the value-ignores-Aggregation rival.

eager_follows_an_edit_to_the_cell_a_fold_reads

After East/A Revenue becomes 20 the fold is 25 and the folded Profit 19. The Profit half is what fails when apply forgets to recompute formulas: the folded cache is then stale.

eager_matches_the_evaluator_on_the_shipped_documents

Both shipped documents, every view's None categories, and the hand model: every probe of Eager equals a direct evaluate_aggregated on a model recomputed under the same None categories, and the probe set is non-empty. Fails on both aggregation rivals.

eager_agrees_with_itself_over_every_corpus_edit_sequence

differential over a generated edit sequence on each corpus model returns a Report with edits + 1 steps and a non-zero probe count. The count assertion is what a harness that compared nothing would fail; the step count is what one that stopped early would fail.

the_harness_passes_a_backend_that_is_right

The control for the catches tests: Eager as the candidate over the hand-built edits is a pass, so a harness that rejects everything is seen.

the_harness_catches_a_backend_that_ignores_the_aggregation

A candidate that reads every value as Exact diverges at step 0, first at the full-key formula cell {East, A, Profit} over hidden (eager None, candidate 6).

the_harness_catches_a_backend_that_ignores_the_measure_aggregation

A candidate that drops SetMeasureAgg diverges at step 2, the edit that sets it, on a Revenue key.

the_harness_catches_a_backend_that_goes_stale_after_two_edits

A candidate that stops applying edits after the second diverges at step 3, on a Revenue key. A prefix of steps cannot see a backend that goes wrong late.

the_harness_catches_a_backend_that_ignores_a_clear

A candidate that keeps a cleared cell diverges at step 3 and the message names it.

the_harness_catches_a_wrong_folded_formula_value

Review of PR 343 (Codex P1): a rival wrong only at value({Product=A, _Measure=Profit}, OverHidden), the Profit cell a view with Region on None draws, passed 128 probes, because formula cells were built over full keys only. Now the divergence is at step 0 on exactly that probe, eager 9, candidate -999.

the_harness_catches_a_backend_that_keeps_answering_for_a_removed_formula

Review of PR 343: probes were rebuilt from the post-edit model, so a candidate that ignores RemoveFormula was never asked about Profit again. Probes now accumulate over every step. The divergence is at the last step, on a Profit key, eager None, candidate Some.

the_harness_catches_a_fault_that_only_shows_after_two_coordinates_are_dropped

Review of PR 343 (Copilot): only one-coordinate partials and the empty key were probed. A rival wrong only at {_Measure=Revenue} now diverges at step 0 on Value({_Measure=Revenue}, Exact). The bound is MAX_DROPPED = 3 coordinates; a fold dropping more is not asked about.

the_harness_catches_a_raw_fold_that_returns_a_formula

Review of PR 343 (Copilot): raw_fold is documented never to be a formula. A rival whose raw_fold is value(partial, OverHidden) diverges at step 0 on a RawFold of a Profit partial (eager None, candidate Some). It could not be seen while Eager itself returned the formula.

the_harness_catches_a_wrong_group_fold

A group name stands in for an item in the probe keys. A rival wrong only at {Region=Coastal, Product=A, _Measure=Revenue} diverges at step 0, eager 15, candidate -999.

eager_folds_a_group_it_is_asked_about

The group fold in the grouped model is East + West = 15 exactly, so the rival test above has a true answer to differ from.

eager_raw_fold_is_never_a_formula

At {Product=A, _Measure=Profit} the folded value is 9 and the raw fold is None. Fails on the fault that lets raw_fold read the formula cache.

eager_add_and_remove_formula_change_what_a_key_reads

Review of PR 343: Edit::AddFormula as a no-op left all 25 tests green, because an Edit fault reaches both sides of a differential alike. Double = Revenue * 2 reads None before the edit and 20 at East/A after it, and None again after RemoveFormula. Fails on AddFormula as a no-op.

eager_clear_cell_leaves_the_key_absent

After ClearCell the key reads None and the model holds no cell. A ClearCell applied as SetCell(0.0) hits both sides of a differential identically, so only this direct test fails.

same_value_follows_the_float_rules_and_is_exact_elsewhere

NaN equals NaN, -0.0 equals 0.0, 1.0 differs from 1.0000000000000002, texts and errors compare exactly, and None equals only None. Each of three one-line faults in same_value (NaN unequal, signed zero by bits, any two texts equal) survived the whole suite until this test existed.

probes_cover_folds_formulas_measures_and_groups

probes includes a raw fold, a full key, a folded formula cell under both aggregations, the two-dropped key {_Measure=Revenue}, the empty key and a group key. Review of PR 343 showed probes omitting formula cells, _Measure keys or raw folds left every test green.

an_edit_names_its_key_as_two_value_probes_and_a_fold

edit_probes of a ClearCell names the cleared key three ways, and of an edit naming no key names nothing.

a_maintained_eager_equals_a_fresh_one_over_random_edit_sequences

Clause 2 asks for a property test over a random edit sequence. A proptest (256 cases, up to four edits of five kinds over the hand-built model) runs differential with a candidate that rebuilds an Eager from scratch on every edit. It fails on the Eager::apply-skips-recompute fault, which is the property: maintaining in place equals building afresh.

delta::tests::overwriting_a_value_with_one_that_compares_equal_is_the_zero_delta

Every pair of NaN spellings (positive, negative, two payloads), 0.0 over -0.0 and back, and equal text each give the zero delta. Faults: DeltaValue::new not mapping NaN to the canonical one, and not mapping -0.0 to +0.0; each fails this test and two others.

delta::tests::numbers_order_by_total_cmp_with_the_canonical_nan_last

Comparing by bits instead of f64::total_cmp passes every equality test, since the values are canonical, and fails only here, where negatives must sort below positives.

delta::tests::values_that_differ_by_the_float_rules_stay_different

Guards the other direction: a cmp returning Equal across variants (0 against "0") fails this and the totality test. A weight of +1 for the old value fails four tests.

the_cell_delta_of_an_edit_is_the_store_after_minus_the_store_before

The differential for step 3. A proptest (256 cases, up to 12 edits drawn from sets, clears, both zeros and three NaN spellings) checks that the delta DataStore logs for an edit equals the store as a Z-set after it minus the store before. No Derived backend exists yet, so this is the harness's step-3 form: the delta against the store it describes.

the_harness_checks_a_cell_a_view_draws_that_drops_four_coordinates

improvise-bw4p.4. Six categories, four on None, a rival wrong only at {C0=a, _Measure=Revenue}. Before the drawn probes the differential passed it (is_err failed); the cell drops four coordinates of a stored key and MAX_DROPPED is three. Now the first divergence is the drawn cell's exact value. Fault: drawn_probes skipping every view fails this and five more.

harness::tests::sub_partials_are_the_keys_the_old_mask_walk_gave

The subset walk no longer enumerates 2^n masks. For every key of up to 12 coordinates its keys equal the old mask walk's as sorted sets, so only the order changed. Fault: dropping at most two coordinates instead of three fails this and the next test. No wall clock is read.

harness::tests::sub_partials_of_sixty_four_coordinates_number_the_choices_of_at_most_three

At 64 coordinates the old 1u64 << n cannot run, so only the combination walk answers; its count must be the sum of C(64, k) for k up to 3, 43745. This replaces a 250ms timing bound (removed: a debug-build wall clock fails on a slow runner and the old walk passes in release).

the_harness_catches_a_fold_that_covers_a_hidden_item

improvise-bw4p.3. East hidden, Coastal collapsed: the drawn Coastal/A is 5, not 15. A rival whose covered reads with no hidden items diverges there. Fault in Eager::covered (covers everything) fails this and eager_matches_the_evaluator_on_the_shipped_documents, which now includes the hidden document, because no shipped demo hides an item.

the_harness_catches_a_total_that_counts_a_hidden_item

A rival total reading with no hidden items diverges at a column total. The same fault in Eager::total fails this, the next test and the shipped-documents comparison.

the_harness_catches_a_total_that_does_not_span_its_rows

Nothing is hidden and Margin is Revenue / Cost, so only the span can separate the rival: the pooled total of {_Measure=Margin} over the rows is 15 / 6 for eager and None for a backend answering covered at a column key. The first version used the hidden fixture and failed through the hidden East instead; it passed once nothing was hidden. Fault: Eager::total ignoring hidden items does not fail this test, as it must not.

the_harness_catches_an_occupancy_that_counts_a_hidden_item

A rival counting stored cells with no hidden filter diverges at a drawn cell's or line's occupancy. Eager::occupancy ignoring the hidden items fails this and the shipped-documents comparison, whose count is taken independently from iter_cells and matches_partial.

a_collapsed_groups_occupancy_counts_its_visible_members

Occupancy is keyed by axis item and a collapsed group is a remap to its visible members. The Coastal line draws two cells (West's, East being hidden) and Eager once counted 0 because it matched the group name literally. Fault: matching literally fails this test.

eager_reads_what_the_grid_evaluator_reads

Compares Eager::covered and total with GridLayout::evaluator's own cell and column_total for every drawn cell and total, so the Reading is checked against the layout's hidden items and not against the same Model call. Fault: Reading::of_view dropping every hidden item fails this and four others; before this test the shipped-documents comparison passed it.

a_page_selection_narrows_the_line_occupancy_it_is_asked_under

Lines carry the page coordinates, as a drawn cell's key does. Fault: building the row line from the row categories alone asks {Product=A} across every page and fails this test.

every_row_and_column_line_is_asked_its_occupancy

Pins the row-line probes (Inland, and the collapsed Coastal) and the column line. Fault: dropping the row lines fails this test and the pruning test.

a_pruned_view_is_asked_only_about_the_lines_it_draws

A row with no cells is asked about unpruned and not once prune_empty is set. Fault: building the layout with GridLayout::new, which does not prune, fails it.

a_records_view_is_not_asked_about

A records view draws synthetic _Index/_Dim keys that name no stored cell and has no totals; its stored keys are asked by the subset probes. Fault: not skipping it fails this test.

no_total_is_asked_where_the_grid_draws_none

GridLayout::draws_totals is the one condition grid_body and drawn_probes share. With _Measure on the rows a column mixes measures and has no total. Fault: asking totals always fails it.

a_view_under_another_none_set_is_not_asked

The oracle recomputes its formulas under one None set; a view under another is not asked, since the oracle would answer it from the wrong cache. Fault: dropping the filter fails this test.

Step 4: the incremental backend (improvise-u2le)

How the faults were injected. Twenty-two faults were put into src/group.rs, src/shapes.rs, src/fold.rs and src/incremental.rs one at a time, each run against the whole crate (cargo test -p improvise-incremental --no-fail-fast) and reverted before the next. Two survive because they change nothing observable (below); every other is named by at least one test:

• a group ignores a retraction: group::tests::a_retraction_removes_the_value_it_added, group::tests::an_emptied_group_is_absent_and_keeps_no_entries, incremental_matches_eager_on_the_shipped_documents, incremental_equals_eager_over_random_edit_sequences;
• a group never counts its numbers: a_group_read_comes_from_a_maintained_group, group::tests::min_and_max_skip_nan_and_are_nan_over_nothing_else and eight differentials;
• Max takes the first key: group::tests::min_and_max_skip_nan_and_are_nan_over_nothing_else, an_overwrite_costs_two_updates_per_shape_whatever_the_table_size and five differentials;
• Count counts one: a_collapsed_group_reads_one_group_per_member_it_covers, group::tests::*;
• unanimity ignores disagreement: group::tests::text_is_unanimous_or_mixed_across_groups, incremental_matches_eager_on_the_hand_model_under_every_aggregation;
• an Exact fold reads groups: incremental_matches_eager_on_a_group_read_without_a_view, incremental_matches_eager_on_hidden_items_and_collapsed_groups;
• a formula-owned key is served from groups: incremental_matches_eager_on_a_formula_read_under_every_aggregation;
• Sum read as Count: seven differentials, so the delegation is observed;
• occupancy counts a hidden coordinate / ignores a free hidden category / adds the hidden cells / ignores a named group: the hidden-item differentials and occupancy_with_a_hidden_item_reads_the_groups_it_subtracts (the last two of those);
• shapes are not fed after they are built: a_group_read_comes_from_a_maintained_group, an_overwrite_costs_two_updates_per_shape_whatever_the_table_size;
• a shape keeps an emptied group: a_group_whose_cells_are_all_cleared_is_no_longer_read;
• the expansion ignores covers: incremental_matches_eager_on_a_collapsed_group_with_a_hidden_member_under_every_aggregation;
• the members ignore the spans: a_collapsed_group_reads_one_group_per_member_it_covers;
• apply skips the model or leaves the formulas stale: the differentials, with and without formulas;
• the measure's aggregation is ignored: a_collapsed_group_reads_one_group_per_member_it_covers, a_group_read_comes_from_a_maintained_group;
• raw_fold answers for a formula target: incremental_matches_eager_on_a_pooled_total_of_a_ratio, incremental_matches_eager_on_the_hand_model_under_every_aggregation.

Faults that cannot be seen, and why. Group::smallest reading the first key even when it is NaN returns NaN, and f64::min(INFINITY, NaN) is INFINITY, which is the answer for a group of only NaN. A projection that keeps the cells lacking a shape's category files them under a key that names fewer categories, and a read of that shape never asks for such a key.

The fixture, and a first version that was blind. hidden_workbook draws the measure on no axis, so its cells carry no _Measure coordinate, the measure's aggregation never applies and the expansion fault above survived. hidden_counted_workbook draws the measure on the columns.

incremental_matches_eager_on_the_hand_model_under_every_aggregation

Applies Count, Min, Max, Avg, Sum to a numeric measure and to a text measure, then a text over a number and a clear. Fails on a group that ignores retractions, one that never counts numbers, Max reading the first key and unanimity that ignores disagreement.

incremental_matches_eager_on_the_shipped_documents

Both shipped documents and the hand and hidden fixtures, over edits_for. It reaches the group path only after the edit that sets a measure's aggregation, so it fails on the faults that touch the fold, not on one in the Sum path.

incremental_matches_eager_on_hidden_items_and_collapsed_groups

East is hidden and Coastal collapsed. Fails on occupancy that counts a hidden coordinate and on an Exact fold that reads groups. The measure is not drawn here, so it does not see covers.

incremental_matches_eager_on_a_collapsed_group_with_a_hidden_member_under_every_aggregation

The same workbook with the measure on the columns, so the Coastal row folds West only and the measure's aggregation applies to it. Fails on an expansion that ignores covers.

incremental_matches_eager_on_a_formula_read_under_every_aggregation

Profit is a formula target, so its key must be read by the model. Fails when the backend serves a formula-owned key from groups.

incremental_matches_eager_on_a_group_read_without_a_view

grouped_model with a NaN, a clear and every aggregation, once with no None category and once with Product. Fails on an Exact fold that reads groups.

incremental_matches_eager_on_a_cell_a_view_draws_that_drops_four_coordinates

The wide fixture under the new backend: a drawn cell that drops four coordinates of every stored key. Fails on a group that never counts numbers and on shapes not fed after the build.

incremental_matches_eager_on_a_pooled_total_of_a_ratio

The ratio fixture's formula Margin pooled over the rows. Fails when apply leaves the formulas stale and when a formula key is read as a raw fold.

incremental_equals_eager_over_random_edit_sequences

Up to six edits drawn from each fixture's own cells (an overwrite, a record in a made-up item, a clear, a new aggregation) with values from a pool that has both zeros, two NaNs, an infinity, text and an error, 256 sequences over five fixtures, probing everything each view draws. Fails on every fault listed above that a deterministic test did not already see.

a_group_read_comes_from_a_maintained_group

A Min read builds one shape and reads one group; after an overwrite the new minimum comes from the delta and the store is not scanned again. Fails on a group that never counts numbers, on shapes that are not fed after the build and on a backend that ignores the measure's aggregation.

an_overwrite_costs_two_updates_per_shape_whatever_the_table_size

At 216 and 864 cells, with one and with two shapes built, one overwrite costs a retraction and an insertion per shape and builds nothing; the two sizes cost the same. Fails on shapes that are not fed, which cost nothing, and on Max reading the first key, since the read after the write is wrong.

a_read_visits_one_group_where_eager_visits_every_cell_it_covers

A group read at two table sizes costs one group each; eager's matching_values visits the 36 and 72 cells the region covers. The counts are deterministic operations; no wall clock is read.

a_collapsed_group_reads_one_group_per_member_it_covers

Coast holds three regions, so a Count of it reads three groups and answers 108. Fails on members that ignore the spans and on a Count that counts once.

occupancy_with_a_hidden_item_reads_the_groups_it_subtracts

A line with one hidden product is its cells less the hidden product's, and reads two groups (the line and the line under that product). Fails on occupancy that ignores or adds the hidden cells.

a_group_whose_cells_are_all_cleared_is_no_longer_read

Clearing the only cell of a group removes the group, and a later read looks at none. Fails when a shape keeps the emptied group.

group::tests::a_retraction_removes_the_value_it_added

A multiset that ignores a negative weight keeps the minimum it should have lost.

group::tests::an_emptied_group_is_absent_and_keeps_no_entries

After the last retraction the group reads as absent and its map holds no zero-weight entry.

group::tests::min_and_max_skip_nan_and_are_nan_over_nothing_else

NaN is skipped by Min and Max; a group of only NaN gives NaN (it gave +inf and -inf before the Eager-math follow-up) and still counts.

group::tests::a_fold_over_several_groups_is_the_fold_of_their_union

The smallest of the minima, the largest of the maxima and the sum of the counts.

group::tests::text_is_unanimous_or_mixed_across_groups

One shared text is that text, two are mixed, a number among text is mixed, and so is a NaN.

Step 5: the formula cache (improvise-shbc)

How the faults were injected. Twenty-seven faults went into src/formulas.rs and src/incremental.rs, one at a time, each run against the whole crate and reverted before the next. A first pass left eight alive; six were a gap in the tests and were closed by the tests below, and the remaining two (born-stems-not-evaluated, target-category-not-read) cannot change an answer. What each fault was and the test that names it:

• a cell that gives a stem is not enough to evaluate it / no reader is dirtied: a_cell_edit_evaluates_the_one_stem_that_reads_it_whatever_the_table_size, every_formula_in_the_pool_is_added_edited_around_and_removed_like_eager and six others;
• a stem that no cell gives keeps its cells: a_new_record_adds_its_stem_and_a_cleared_one_takes_it_away;
• reads skip the filters' categories: a_filter_on_a_category_the_stem_has_reads_the_cells_of_other_stems;
• reads skip the formula's own target name: a_new_aggregation_for_the_measure_a_filtered_formula_falls_back_to_changes_it;
• the formula set is never wide / one target category is never wide / a name in another category is never wide: two_target_categories_read_each_others_stems_whatever_the_order_they_are_added_in, a_name_in_another_category_reads_another_stems_cell;
• every order settles in one pass / a cycle is never seen / sixteen formulas settle in one pass: formulas::tests::a_self_reference_and_a_mutual_reference_are_cyclic, formulas::tests::sixteen_formulas_leave_no_pass_to_spare, a_formula_that_keeps_moving_for_sixteen_passes_is_circular, dependency_order_and_the_plain_passes_leave_the_same_cache;
• dependencies after dependents: dependency_order_and_the_plain_passes_leave_the_same_cache and five more;
• fifteen passes / seventeen passes: a_chain_added_last_link_first_is_circular_exactly_where_eager_says;
• the passes end without marking the cells still moving, or begin from the old cache: a_chain_added_last_link_first_is_circular_exactly_where_eager_says, a_formula_that_keeps_moving_for_sixteen_passes_is_circular;
• a new aggregation dirties nothing: incremental_matches_eager_on_the_hand_model_under_every_aggregation;
• a write of the same value over a signed zero is no change: overwriting_zero_with_negative_zero_changes_what_a_formula_reads;
• a formula replaced by one of the same target is no change: a_formula_replaced_in_place_is_evaluated_afresh;
• stems keep the None categories: eleven tests, the first a_chain_added_last_link_first_is_circular_exactly_where_eager_says;
• a removed cell counts as an added one: a_new_record_adds_its_stem_and_a_cleared_one_takes_it_away;
• a wide document is evaluated by stem, a rebuild keeps the old cells, a removed last formula keeps the cache: every_formula_in_the_pool_is_added_edited_around_and_removed_like_eager, incremental_matches_eager_on_a_pooled_total_of_a_ratio.

Faults that cannot be seen, and why. Reads that skip the formulas a name targets change no answer either (only the unit test formulas::tests::what_a_formula_reads_includes_what_the_formulas_it_names_read fails): a stem is evaluated whole, so whatever the skipped formula would have added is re-evaluated because the formula itself dirties the stem. A born stem is found again by the lookup of the cell that gave it, since the cell agrees with the stem outside the target category, so skipping the extra "born means dirty" step changes nothing. The target category being in a formula's reads cannot matter either: stems are derived by removing it, so no stem has it to drop.

What the random tests found, once each, before the rules in the reasoning file existed. NaN as a formula result (eager calls it circular; a one-pass order did not), a stem containing a formula target's coordinate (stored data at a target, a second target category: the stems then read each other), and, from the fixture shrinking to one product, a filter over the stem's own category.

a_cell_edit_evaluates_the_one_stem_that_reads_it_whatever_the_table_size

At 12 and 48 products, an overwrite of one product's Revenue evaluates one stem and two formula cells (Profit, Margin) and rebuilds nothing; eager evaluates every stem for every pass. Counts are operations. Fails when no reader is dirtied.

a_formula_edit_evaluates_every_stem_once_and_rebuilds_the_index_once

A new formula has a cell at every stem, so every stem is evaluated once and the stems are rebuilt once.

a_new_record_adds_its_stem_and_a_cleared_one_takes_it_away

Records appear in and disappear from the store; their stems appear and go with their formula cells.

every_formula_in_the_pool_is_added_edited_around_and_removed_like_eager

Each of the 18 formulas (chains, a cycle, SUM over an expression, a share, filters, IS, a reciprocal, two that target Region) added, the cells around it edited and the formula removed, asking everything the view draws at every step.

a_formula_that_keeps_moving_for_sixteen_passes_is_circular

Loop = Loop + 1 with a value stored at its target never settles and is circular; without a value it settles on its first error, ref:Loop, and eager agrees with both.

a_chain_added_last_link_first_is_circular_exactly_where_eager_says

Chains of 14 to 18 formulas each referring to the one before, added last first: eager's passes make one link of progress per pass, so the longer chains are circular. Fails when the pass bound moves by one in either direction and when dependency order is not limited to fewer formulas than passes.

a_formula_replaced_in_place_is_evaluated_afresh

Profit redefined keeps its position and moves its cells; the fingerprint of the formula list includes the text.

overwriting_zero_with_negative_zero_changes_what_a_formula_reads

Units ^ -1 over a sum of zero is inf and, once both cells are -0.0, -inf. The cell delta calls the two zeros equal, so the formula side reads the raw change log.

a_filter_on_a_category_the_stem_has_reads_the_cells_of_other_stems

MAX(Revenue WHERE Product = A) at the stem of product B reads product A's cells. Fails when a filter's category is not among a formula's reads.

two_target_categories_read_each_others_stems_whatever_the_order_they_are_added_in

A formula targeting Region and one targeting _Measure, with a value stored at the second's target: the first's stems then contain the second's coordinate and read its cache. The documents fall back to the whole recompute.

a_name_in_another_category_reads_another_stems_cell

IF(Revenue > 1000, B, Revenue): at the stem of a big product it reads the cache of the stem of B, which is evaluated after it. Fails when such a formula set is not wide.

a_formula_cell_holding_nan_is_nan_and_not_circular

A NaN formula result is a value: Profit and Margin over a NaN cell read NaN under both evaluations and eager. It used to be circular in eager, because NaN is not equal to itself and never settled; the fixed point now compares with settled (follow-up, "Eager's math, fixed"). Fails when NaN is marked circular.

a_new_aggregation_for_the_measure_a_filtered_formula_falls_back_to_changes_it

A WHERE that does not match falls back to the raw group at the formula's own target, so a new aggregation for that measure changes the formula. Fails when a formula's target is not among its reads.

dependency_order_and_the_plain_passes_leave_the_same_cache

Up to four formulas drawn from the pool (cycles and Region-targeted ones among them), told to a backend that evaluates in dependency order and one that always runs eager's passes; their models, cache included, print alike. This is the test clause 6 asks for.

the_formula_fixture_matches_eager_over_random_formula_and_cell_edits

Cells written and cleared (including NaN and -0.0, a region and product the fixture lacks, and cells at formula targets), pool formulas added and removed, and new aggregations; read with Region folded and no view. Found the NaN and multiple-target cases above.

what_the_formula_fixture_draws_matches_eager_over_random_edits

The same edits, asking everything the fixture's view draws at each step.

formulas::tests::a_chain_is_ordered_dependencies_first_and_is_not_cyclic

Margin = Profit / Revenue listed before Profit: dependency order puts Profit first.

formulas::tests::a_self_reference_and_a_mutual_reference_are_cyclic

X = X + 1 and A = B + 1, B = A + 1 have no order.

formulas::tests::sixteen_formulas_leave_no_pass_to_spare

Fifteen formulas in a chain settle in one ordered pass; sixteen do not, because eager needs the sixteenth pass to see nothing move.

formulas::tests::what_a_formula_reads_includes_what_the_formulas_it_names_read

Margin names Profit, which names Cost; the reads of Margin include Cost.

the_whole_cache_recompute_of_a_wide_document_is_metered

A document with formulas in two target categories falls back to recompute_formulas; the fallback was doing the work with the meter at zero (Copilot on PR #351). It now counts Meter::recomputes, and a document with one target category counts none.

Review of PR #349: zeros, covers, speed (improvise-u2le)

same_value now tells the two zeros apart (same_value_follows_the_float_rules_and_is_exact_elsewhere asserts it), so the random suites compare zero signs; their pools hold -0.0 and no +0.0, since eager's Min/Max of both zeros is platform-defined. Injected: a sign that is always positive, Min negative only if all are, a sign fed from the delta, a retraction that adds, Max negative if any, and the fold ignoring covers; each was watched failing, by the tests below.

min_and_max_of_negative_zeros_are_negative_zero_in_both_backends

[-0.0], [-0.0, -0.0], [-0.0, NaN] and a -0.0 among nonzeros, compared as bits against eager. Fails when the sign is lost (zero-sign-always-positive) and when Min demands every zero negative.

a_positive_zero_stays_positive_and_nonzero_answers_are_untouched

[0.0] reads +0.0 for both, and Max of [-0.0, 2.0] is 2.0.

overwriting_a_zero_with_the_other_zero_moves_the_sign_of_min_and_max

0.0 to -0.0 and back: the cell delta is empty, so only the raw change log moves the sign. Fails on a sign fed from the delta, on a retraction that adds, and on an always-positive sign.

with_both_zeros_min_is_negative_and_max_is_positive_whatever_the_order

Both zeros in both orders. Fails on Max negative if any zero is.

Speed. The corpus self-comparison and the maintained-against-fresh property moved to their own binaries (tests/corpus_eager.rs, tests/maintained.rs): oracle.rs ran 2.45 to 3.04 s in loaded full runs because its two heaviest tests shared it. The tests are unchanged.

Review of PR #351: aggregation edits, zero signs (improvise-shbc)

a_new_aggregation_reaches_the_stems_of_a_formula_that_targets_another_category

R0 = East + West on Region, Time folded, SetMeasureAgg Revenue Max: eager reads 13 (the maximum of East plus the maximum of West), the first version kept 14. Fails when a new aggregation dirties only the stems of formulas that name the measure, and when Stems::carrying ignores the measure.

a_new_aggregation_reaches_a_product_targeted_filtered_sum

A Product-targeted SUM(F0 WHERE Region = East) with no None category, and SetMeasureAgg Cost Min. It agreed with eager before the fix too, so it pins the shape and not the fault.

a_new_aggregation_reaches_a_filtered_sum_on_the_fallback_path

The reviewer's shape: P0 = SUM(Revenue) WHERE Region = East on _Measure with Time as the None category, then SetMeasureAgg Revenue Max, so the fallback to the raw group at the formula's own target reads the new aggregation. Fails when a new aggregation does not reach the stems carrying the measure.

ordered_evaluation_keeps_the_zero_eager_settles_on

A stored 0.0 at F1, then F3 = F1, F4 = F3 ^ -1, then F1 = -0. Eager used to settle on F4 = inf because it called -0.0 equal to the 0.0 it first read, while the ordered evaluation gave -inf; with zero signs settled by bits both give F3 = -0.0 and F4 = -inf. Fails (only Ordered) when a stem with a zero is not re-evaluated by the passes, and in core when zeros settle equal. The ordering property's pool now holds -0, Units * -1 and -Cost, and compares after every edit, but did not find this fault alone in 1,500 cases: this test is the pin.

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

How the faults were injected. Eleven faults went into improvise-core/src/model/types.rs, src/group.rs and src/shapes.rs (ExactSum's own sign rule is PR #348's, evidenced in context/test-evidence/numtower.md), each run against the whole crate. One survived the first pass (eager-formula-sum-in-order: both backends evaluate a formula through core's one evaluator, so no difference between them can show it) and is closed by a test that reads the formula sum itself. Each fault and the tests that name it:

• eager's Sum adds in order: sums_are_exact_whatever_the_order_the_cells_were_added_in, twenty_thousand_overwrites_in_a_thousand_cell_group_do_not_drift;
• eager's Avg adds in order: an_average_is_the_exact_total_over_the_count_rounded_once;
• the formula-level SUM adds in order: a_formula_sum_over_an_expression_is_exact_in_both_backends;
• a read of several groups keeps only the first group's sum: nine differentials, among them incremental_matches_eager_on_a_collapsed_group_with_a_hidden_member_under_every_aggregation;
• Avg divides by the number of groups: an_average_is_the_exact_total_over_the_count_rounded_once and seven more;
• sums never move after the build: thirteen tests, the first a_sum_read_after_a_write_comes_from_the_delta_and_equals_a_fresh_sum;
• a retraction adds: eleven tests, among them overwriting_zero_with_negative_zero_moves_the_sign_of_a_sum;
• a build leaves the sum empty: eighteen tests, among them a_zero_total_has_the_sign_ieee_gives_the_same_addends;
• an exact fold leaves the sum empty: incremental_matches_eager_on_hidden_items_and_collapsed_groups and four more;
• an overwrite of 0.0 by -0.0 is no change to a sum: overwriting_zero_with_negative_zero_moves_the_sign_of_a_sum;
• the sum of a new cell is lost: twelve tests.

sums_are_exact_whatever_the_order_the_cells_were_added_in

1e16, 1.0, -1e16 in all six orders: f64 addition gives 0 or 1 by order, the exact sum gives 1. Both backends must give the bits of 1.0 for each. Fails on eager adding in order, which is the discrepancy clause 8 exists for: the test failed on the pre-change code with 0.

a_zero_total_has_the_sign_ieee_gives_the_same_addends

[-0.0, -0.0] is -0.0; [-0.0, 0.0], [1, -1] and [-0.0, 3, -3] are +0.0, in both backends, as bits.

overwriting_zero_with_negative_zero_moves_the_sign_of_a_sum

Two cells of 0.0 overwritten by -0.0, then one overwritten back. The cell delta calls the two zeros equal, so the move comes only from the raw change log. Fails on a sum fed from the delta.

twenty_thousand_overwrites_in_a_thousand_cell_group_do_not_drift

20,000 overwrites of a 1,000-cell group, with values that make an f64 sum drift; the maintained sum equals eager and a sum built afresh, bit for bit. The count is not a million (the ADR's measurement) because a test binary cannot afford it; the property does not depend on it.

a_formula_sum_over_an_expression_is_exact_in_both_backends

SUM(Revenue * 1) over the same three values in three orders gives 1.0. Fails on the formula-level SUM adding in order, which no comparison between the backends can see.

a_sum_read_after_a_write_comes_from_the_delta_and_equals_a_fresh_sum

After a write, a Sum read builds nothing and equals the same read of a backend built afresh.

Review of PR #353: averages, core's own tests, the meter (improvise-hrjz)

Ten faults (improvise-core and improvise-incremental run together): eager's Sum and Avg and the formula SUM adding in order, an average that divides a rounded sum, a formula SUM over nothing that is -0.0, the group's average dividing a rounded sum, a total that keeps one group's sum, sums not metered, a new cell's sum lost, sums never moving. Each was watched failing; the tests are named below. same_value compares numbers by bits since step 4, so the random suites see the sign of a zero in Sum and Avg too.

The drift test was renamed twenty_thousand_overwrites_in_a_thousand_cell_group_do_not_drift: its old name claimed fifty times what it runs.

an_average_is_the_exact_total_over_the_count_rounded_once

Five values whose sum f64 addition misses; both backends equal ExactSum::mean, which numtower/tests/mean.rs checks against exact rationals. Fails on an average that divides a rounded sum.

an_average_does_not_overflow_with_its_sum_in_either_backend

Avg([MAX, MAX]) is MAX. Fails on a rounded sum divided.

model::types::exact_sum_tests::a_sum_does_not_depend_on_the_order_of_its_addends

Core's own apply_agg: the three-addend sum is 1 in every order. Fails on eager adding in order, which the tests in improvise-incremental had been the only ones to see.

model::types::exact_sum_tests::an_average_rounds_the_exact_mean_once_and_does_not_overflow

Avg([MAX, MAX]) is MAX and Avg([0.1, 0.2, 0.3]) is the exact mean. Fails on a twice-rounded average.

model::types::exact_sum_tests::a_formula_sum_is_exact_whatever_the_order_of_the_records

SUM(Revenue * 1) over [1e16, 1, -1e16] in two orders is 1. Fails on the formula-level SUM adding in order.

model::types::exact_sum_tests::a_formula_sum_over_nothing_is_positive_zero

SUM(Revenue WHERE Region = Nowhere) is +0.0; it was -0.0 while it summed with Sum for f64. Fails on the old behaviour.

model::types::exact_sum_tests::a_stored_group_sums_exactly_and_averages_once

A measure aggregated by Sum over [1e16, 1, -1e16] is 1, and by Avg is the exact third.

the_mean_is_the_nearest_f64_to_the_exact_total_over_the_count

Up to eight finite addends, the mean against exact rationals (numtower/tests/mean.rs). Fails on an average of a rounded sum.

a_mean_whose_sum_would_overflow_is_still_finite

[MAX, MAX] has the mean MAX.

non_finite_sums_have_non_finite_means_and_zero_keeps_its_sign

Infinities and NaN read as ExactSum::value does, and a zero keeps its sign.

Eager's math, fixed (follow-up to steps 4 to 6)

Ruling (user, 2026-10-10): do not reproduce math bugs found in Eager; fix Eager. Six faults were injected into core and the groups (mixed zeros, Min over NaN, NaN never settling, zeros settling equal, and the groups' Min and Max over NaN); nan-never-settles survived the first pass because NaN produced by one evaluation always has the same bits, and is closed by a unit test of settled. Each fix has a regression test named after the bug:

• model::types::eager_math_tests::min_and_max_of_both_zeros_do_not_depend_on_their_order and with_both_zeros_min_is_negative_and_max_is_positive_whatever_the_order: a naive f64::min fold passes on ARM and fails on other platforms, so the rival is a fold that keeps the first of two zeros;
• model::types::eager_math_tests::min_and_max_over_only_nan_are_nan_not_infinite, min_and_max_over_only_nan_are_nan_in_both_backends, group::tests::min_and_max_skip_nan_and_are_nan_over_nothing_else;
• model::types::eager_math_tests::a_formula_that_settles_on_nan_is_nan_and_not_circular, a_formula_cell_holding_nan_is_nan_and_not_circular, settled_treats_every_nan_as_one_value_and_the_zeros_as_two;
• model::types::eager_math_tests::a_zero_that_changes_sign_between_passes_settles_on_the_new_sign and ordered_evaluation_keeps_the_zero_eager_settles_on (now with the sign settled by bits, no fallback);
• model::types::eager_math_tests::a_formula_that_never_settles_is_still_circular: the guard that a real oscillation is still circular. The random and differential suites compare numbers by bits and their pools hold both zeros again.

User-visible changes this evidence also covers: 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) was -0 and is now circular, as the same cycle over nonzero data always was; a cycle fed a NaN (A = A + 1, A = A with A NaN) settles on NaN instead of circular.

a_live_source_matches_eager_over_the_corpus_and_its_edits

improvise-rnak. Incremental over a LiveTable (the model's cells moved into the table, the model's own store emptied) against Eager over the shipped documents, their views and edits_for (trimmed to three edits above 40 cells, as corpus_eager does). Rivals, each failing it by name: sync drains nothing; the model not put over the feed (formulas read an empty store); a shape built from an empty store; the stems built from the model's own store.

changes_named_by_the_caller_are_maintained_as_the_drain_would

apply_changes with the changes the table reports, against Eager after each of four edits (an overwrite, a new record under an item the model lacks, a removal, a text), asking every probe of every step so far. Rivals: apply_changes ignores its changes (only this test and no other fails it); the stems from the owned store.

a_write_is_invisible_until_it_is_drained

The contract of a ChangeSource: a read after a write and before the drain sees the old value, after sync the new one, and a second sync changes nothing. Rivals: the table shows a write at once (this test alone fails it, which is why the contract has a test of its own: the differential cannot see it, since every shape it asks about was built before the write); sync drains nothing.

the_cost_of_a_reported_change_does_not_depend_on_the_size_of_the_table

One overwrite reported by the table, after the shape is built, at 216 and at 864 cells: two group updates and two sum updates, no build, equal meters, and zero snapshot rows served by the source for the change. The build itself serves exactly the table (n * n * 6 rows), so the zero is a count that could have been positive. Rival: every sync rebuilds the shapes (builds and built_cells move, and the table serves the snapshot again).

an_overwrite_by_the_same_value_moves_nothing

A table that reports an overwrite of a cell by its own value leaves the fold where it was (23). Rival: the model not over the feed fails it with the others.

a_live_source_matches_eager_over_random_formula_and_cell_edits

Fed against Eager over random formula and cell edits on the formula fixture (no views, so the binary stays under two seconds). Rivals: sync drains nothing, the model not over the feed, a shape built from an empty store and the stems from the owned store all fail it.

a_backend_can_be_built_over_the_exported_feed_alias

Review of #358: over<S>(Arc<S>) could not take the SharedFeed the same PR exports. The test builds a backend from a SharedFeed; it did not compile against the generic signature.

a_populated_model_put_over_a_feed_keeps_no_cells_of_its_own

Review of #358: Fed::new emptied the store before the call, so no test passed a populated model. This one does, asserts the owned store is empty afterwards and that every harness probe agrees with Eager. Rival: Model::over keeping the cells fails it, and only it.

a_cell_edit_on_a_fed_backend_is_refused

Maintained::apply with a SetCell panics with the backend's own message in every build. Rival: the assert removed (the test then sees the model's message, not the backend's, and fails).

a_cell_clear_on_a_fed_backend_is_refused

The same for ClearCell.

a_feed_has_one_drainer

Review of #358: two backends over one feed; one write; a.sync(); b.sync(). The first sees it, the second does not. This pins the behaviour as documented rather than as a guarantee: a drain is destructive.