docs(evidence): the improvise-incremental entries use ### so --check-evidence reads them (improvise-bw4p.3)

Co-Authored-By: Claude Sonnet 5.5 <noreply@anthropic.com>
Claude-Session: https://claude.ai/code/session_01VdfEGXA7aJ6ftMsCc9PJze
This commit is contained in:
Claude (dbsp-probes)
2026-10-10 12:07:34 -07:00
committed by Edward Langley
parent ce138bf740
commit d83a4b8330
+32 -32
View File
@@ -51,142 +51,142 @@ none did):
- `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
### 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
### 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
### 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
### 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
### 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
### 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
### 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
### 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_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
### 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
### 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
### 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
### 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
### 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
### 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
### 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
### 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
### 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
### 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
### 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
### 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
### 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
### 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_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
### 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
### 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
@@ -216,37 +216,37 @@ both zeros and three NaN spellings) checks that the delta `DataStore` logs for a
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
### 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.
## probing_a_key_of_twenty_six_coordinates_is_not_exponential
### probing_a_key_of_twenty_six_coordinates_is_not_exponential
The old `sub_partials` walked all 2^n masks (93ms at 20 categories, 225ms at 22). With the mask
walk put back, 26 coordinates take 807ms against a 250ms bound; the combination walk takes
under 70ms. The probe set is unchanged for keys of up to 3 coordinates over any bound.
## the_harness_catches_a_fold_that_covers_a_hidden_item
### 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
### 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
### the_harness_catches_a_total_that_does_not_span_its_rows
A rival answering `covered` for a column key (so the aggregate over its rows, not one fold over
the pooled rows) is told apart from `total`: with no None category the first has no cell.
## the_harness_catches_an_occupancy_that_counts_a_hidden_item
### 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