10f63cdef9
Co-Authored-By: Claude Sonnet 5.5 <noreply@anthropic.com> Claude-Session: https://claude.ai/code/session_01VdfEGXA7aJ6ftMsCc9PJze
715 lines
40 KiB
Markdown
715 lines
40 KiB
Markdown
# 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_infinite_over_nothing_else` and eight differentials;
|
|
- `Max` takes the first key: `group::tests::min_and_max_skip_nan_and_are_infinite_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_infinite_over_nothing_else
|
|
|
|
NaN is skipped by `Min` and `Max`, a group of only NaN gives `+inf` and `-inf` 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;
|
|
- NaN is not marked circular: `a_formula_cell_holding_nan_is_circular_and_the_cells_that_read_it_keep_the_nan_they_read`;
|
|
- 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_circular_and_the_cells_that_read_it_keep_the_nan_they_read
|
|
|
|
NaN is not equal to itself, so eager's passes never see it settle. Fails when the ordered path leaves it.
|
|
|
|
### 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
|
|
|
|
The reviewer's second repro, a Product-targeted `SUM(F0 WHERE Region = East)`. It already agreed on this
|
|
fixture and stays as the second shape of the same hazard.
|
|
|
|
### ordered_evaluation_keeps_the_zero_eager_settles_on
|
|
|
|
A stored `0.0` at `F1`, then `F3 = F1`, `F4 = F3 ^ -1`, then `F1 = -0`: eager settles on `F3 = 0.0` and `F4 = inf`
|
|
because it calls `-0.0` equal to the `0.0` it first read; the first ordered evaluation gave `-inf`. Fails
|
|
(only `Ordered`) when a stem with a zero is not re-evaluated by the passes. 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`,
|
|
`a_million_overwrites_in_a_thousand_cell_group_do_not_drift`;
|
|
- eager's `Avg` adds in order: `an_average_is_the_exact_sum_over_the_count`;
|
|
- 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_sum_over_the_count` 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.
|
|
|
|
### an_average_is_the_exact_sum_over_the_count
|
|
|
|
Five values whose sum `f64` addition misses; both backends give the exact sum rounded once, then divided.
|
|
|
|
### 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.
|
|
|
|
### a_million_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.
|