fiddlerwoaroof/improvise
1
0
Fork 0
Code Issues Pull Requests Actions Packages Projects Releases Wiki Activity

docs(adr): ADR 009 clause 5a computes today's aggregate; bound ExactSum's weights (improvise-felo.4)

Browse Source 
- 5a: group by context (the stem projection, plus the fold/total projection),
  not by record key. The inner WHERE is a filter plus clause 5's join. There is
  an integrated per-record stage before the map, and a rule for several writes
  to one record. The order key is (context rank, record store order), so the
  pre-step-6 re-fold is bit-equal to eager at folds and totals. The first-Err
  error channel is kept.
- ExactSum splits weights into chunks of 2^30 and counts magnitude between
  carries. The example checks weight 2^33, and 20,000 weighted cases match
  exact fractions. The example prints the cost per update.
- Q3(c) states the signed-zero difference and Eager's per-read cost. Q11 is
  narrowed: drawn-item order is already in view_shape.

Co-Authored-By: Claude Opus 5.5 (1M context) <noreply@anthropic.com>
Claude-Session: https://claude.ai/code/session_01VdfEGXA7aJ6ftMsCc9PJze
This commit is contained in:
Claude (agent-felo4)
2026-09-24 22:13:53 -07:00
committed by Edward Langley
parent a2836f44f5
commit 25ebf641a9
2 changed files with 190 additions and 79 deletions
Download Patch File Download Diff File Expand all files Collapse all files
context/adr/009-incremental-evaluation.md
+149 -66
View File
@@ -351,9 +351,11 @@ key, and `FIRST` the least.
the group, and one entry per contributing record. That is the same order as
`Min`/`Max`'s multisets.
- **What moves the order.** Adding an item in the middle of the ordering category, or
reordering its items, changes every stored position. So the ordering category's
item order must be part of the operator shape (clause 7), and a change to it rebuilds
the ordered aggregators that use it. The alternative is to key by a stable item
reordering its items, changes every stored position. **Most of that is already in the
operator shape**: `view_shape` hashes each category's *drawn* items, in order
(`app.rs:47-52`), so a reorder of drawn items already rebuilds. What it does not see
is the position of a **hidden** item, which matters only if `LAST`/`FIRST` must order
values that come from hidden items. The alternative is to key by a stable item
identity (ADR 007) and look the order up at read time. That makes a reorder free, but
a read then costs O(d). This is question 11.
- **Semi-additive measures (felo.8) are aggregates of aggregates.** For example,
@@ -418,54 +420,108 @@ group and nothing else.
`SUM(Revenue * Price)` does not sum a stored measure. It computes a value **per
record**, `Revenue * Price` at that record, and pools those values across the records
of a group. Today `agg_values` (`types.rs:89-139`) lists the member records of each
context and calls the record-level evaluator on each (`member_records`, then
`eval_at`). At a fold or a column total, the contexts come from `Expansion::members`
(`types.rs:201-213`), which materializes the cross product of the spanned categories'
items. That is the one O(grid) path in totals (ADR 008 clause 5).
of a **context**. It is the one place a formula needs an expression *inside* an
operator. This clause first states exactly what today's evaluator computes, because the
incremental form must compute the same thing.
**The design.** It is a three-stage pipeline over the record stream, and each stage is
an operator from clause 1:
**What eager computes** (`eval_agg`, `types.rs:55-87`, and `agg_values`, `:89-139`):
1. **A lifted map over the per-record expression.** For each record in the cell
delta's `record_of` set, the map produces `(base key, expr at record)`. A record
whose cells changed is retracted at its old value and inserted at its new one, so
the map's output is itself a delta. `map` is linear, so this is its own incremental
form.
2. **`index_by(base key)`.** The base key is the record's key with the target category
removed, which is what `eval_agg` pools over (`types.rs:55-87`). An inner `WHERE`
(`SUM(expr WHERE Cat = Item)`) is a `filter` before the index. It is the same
rewrite `eval_agg` applies to its contexts (`types.rs:66-72`).
3. **The group aggregate** from clause 4: `Count`, `Sum`, `Min` or `Max` over the
mapped values, with `Avg` derived.
- **Contexts.** The formula cell's key is the context at a stem. At a fold or a column
total, the contexts are the members `contexts_of` lists through `Expansion::members`
(`types.rs:201-213`, `:905-916`), the cross product of the spanned categories' covered
items. That is the one O(grid) path in totals (ADR 008 clause 5).
- **An inner `WHERE` rewrites the context.** A filter `Cat = Item` *replaces* the
context's `Cat` coordinate (`c.with(&f.category, &f.item)`, `types.rs:69`, and again at
`:116`), and the distinct rewritten contexts are pooled once each. So the stem
`Region=West`, evaluating `SUM(x WHERE Region=East)`, pools **East's** records.
- **Pooling.** For each context, `partial = context.without(target_category)`
(`types.rs:97`). The context's member records are those `member_records` finds under
`partial`, in the store's record order (a record sits where its first cell sits).
The expression is evaluated at each, and the per-context value lists are concatenated
**in context order** (`types.rs:73-77`). So the order is (context rank, record store
order): expansion-major at a fold or total, and plain store order at a stem.
- **Errors.** `agg_values` collects `Result`s (`types.rs:126-136`), and so does
`eval_agg` (`:76`). So the aggregate's value is the **first** `Err` in that order,
if any member errs.
Member records never have to be listed, and no cross product is ever built. A context
in today's cross product that holds no records contributed nothing to the pool, so
pooling only the records that exist is the same answer.
**The design.** Four stages, each an operator from clause 1:
**This is not compiling formulas into operators.** The operator is the map; the
expression inside it is still evaluated by `eval_expr` at the record, exactly as
`agg_values` calls it today. The circuit decides *which* records to re-evaluate (those
the delta names), and the one evaluator computes each value. Clause 2's rule stands:
there is one evaluator.
1. **An integrated per-record stage.** A cell delta does not carry a record: when only
`Price` changes, the delta holds `−Price₀` and `+Price₁` but not the unchanged
`Revenue`, so the old mapped value cannot be computed from the delta alone. So the
first stage is `index_by(record_of)` over the cell delta, integrated. It keeps each
live record's cells, as `ZSet<(measure, value)>` per record. On each step it emits,
for every record the consolidated delta touches:
- a retraction of the record's **previous** snapshot, read from the integrated state
before the step (`I(x)₋₁`);
- an insertion of its **new** snapshot.
**Several writes to one record in one effect** consolidate before this stage (clause
3 steps once per model effect), so the record is retracted once and inserted once,
at its net state. Writes in separate effects are separate steps. A record whose
snapshot is unchanged after consolidation emits nothing.
2. **A lifted map over record snapshots.** For each snapshot, the map produces one
entry per context the record belongs to: `(context key, order key, expr at record)`.
The value is a `Result`, so an error is a mapped value like any other. `map` is linear,
so a retracted snapshot retracts exactly the entries it once produced.
- **The context key** is the record projected onto the context's shape: the target
category removed and each `none_cats` category removed, per `none_cats` list,
exactly as clause 4 defines "the group". At a fold or total, a collapsed group's
member is also mapped to its group, and each spanned category is removed. That is
the same projection occupancy uses (ADR 008 clause 3).
- **The order key** is (context rank, record store order). The context rank is the
record's position in `Expansion::members` order, and it is 0 at a stem. The record
store order is the insertion sequence of the record's first live cell. `DataStore`
does not keep one today, so this stage assigns it; `IndexMap`'s relative order is
exactly first-insertion order among live cells. `DataStore::sort_by_key`
(`cell.rs:269`, on entry into records mode) reorders the store, so it is an
operator-shape change and rebuilds this stage.
3. **An inner `WHERE` is a filter plus clause 5's join, not a filter alone.** Records
with `Cat = Item` pass the filter, and are indexed by their context key **without**
`Cat`. A stem `s` then reads the group at `s` without `Cat`, through the one join of
clause 5 (stems indexed by "stem minus `Cat`"). A filter alone would put East's
records in East's group and leave West's read empty; the join is what makes West's
stem read East's pool, as the rewrite does today.
4. **The group aggregate** from clause 4: `Count`, `Sum`, `Min` or `Max` over the
mapped `Ok` values, with `Avg` derived. **The error channel** is kept beside it: per
group, the set of erring entries, ordered by order key. The aggregate reads the
first of them if the set is non-empty, reproducing today's first-`Err`.
Member records are never listed and no cross product is built. A context in today's
cross product that holds no records contributed nothing to the pool, so pooling only
the records that exist gives the same answer.
**This is not compiling formulas into operators.** The operators are the record stage,
the map, the index and the aggregate. The expression inside the map is still evaluated
by `eval_expr` at the record, exactly as `agg_values` calls it today through `eval_at`
(`types.rs:127-134`). The circuit decides *which* records to re-evaluate (those the
delta names), and the one evaluator computes each value. Clause 2's rule stands: there
is one evaluator.
**The boundary.** The map is sound only when `expr` reads the record's own cells, so
that its value at a record changes only when that record changes. An inner expression
that reads another record, holds a nested aggregate, or refers to a formula whose value
depends on other records, is not a function of one record. That formula stays on the
eager path, and the differential test pins the boundary. ADR 008 clause 5 adopts the
same boundary.
same boundary. The regression that pins the record stage changes **one operand** of a
two-operand expression (`Price` alone, under `SUM(Revenue * Price)`) and compares with
eager.
**What stays eager until step 5, and until step 6.**
- Before step 5 (formulas), every aggregate over an expression is evaluated as today,
through `Expansion::members`.
- From step 5, the map and the index are maintained, so the cross product is gone.
`Count`, `Min` and `Max` over the mapped values are read from the maintained state,
since they are order-free and bit-exact on f64 (clause 8).
- `Sum` and `Avg` over the mapped values are **re-folded** from the group's maintained
values, in the store's record order, until step 6. That keeps them bit-equal to
eager, at a cost of O(group) per change rather than O(grid).
- From step 6 (on question 3's answer), `Sum` is maintained like any other.
**What stays eager until step 5, and what is bit-equal before step 6.**
- **Before step 5** (formulas), every aggregate over an expression is evaluated as
today, through `Expansion::members`.
- **From step 5**, the record stage, the map and the index are maintained, so the cross
product is gone. `Count`, `Min` and `Max` over the mapped values, and the error
channel, are read from the maintained state. They are order-free, or ordered by the
order key, and bit-exact on f64 (clause 8).
- **`Sum` and `Avg` over the mapped values are re-folded** from the group's maintained
values in **order-key order** until step 6. That is (context rank, record store
order), which is exactly the order eager concatenates in, so the re-fold is bit-equal
to eager at a stem, a fold and a total. It costs O(group log group) per change,
against O(grid).
- **From step 6** (on question 3's answer), `Sum` is maintained like any other. Under
question 3's recommendation (c) the order key no longer matters for `Sum`, because
the exact accumulator is order-free.
### 6. Circular references: DBSP's recursion is not our semantics
@@ -620,7 +676,15 @@ for the whole f64 range: in units of 2⁻¹⁰⁷⁴, a finite f64 is a 53-bit i
by at most 2045 bits. This is the idea behind Kulisch accumulators and Radford Neal's
xsum, and Shewchuk's expansions (behind Python's `math.fsum`) are a related technique.
Adding or retracting a value is integer addition, so the accumulator is a true abelian
group over the finite f64s. **Rounding happens once, when the value is read.** Then:
group over the finite f64s. **Rounding happens once, when the value is read.**
**The group claim needs one stated bound.** A consolidated Z-set carries weights, not
just ±1: equal mapped values consolidate, so one element can arrive with a large weight.
The accumulator therefore splits any weight into chunks of at most 2³⁰, and counts
*magnitude* between carry propagations rather than calls. Each limb then stays below
2⁶² between carries, for any `i64` weight. The first version counted calls, and review
found it silently wrong at weight 2³³: it read `−4.24e-314` where the answer is
`1.82e-304`. The example now checks that case, and it reads the exact answer. Then:
- `Sum` is the exact sum, rounded once. It is independent of order.
- `Avg` is the exact sum divided by the count, rounded once. It is correctly rounded
@@ -629,7 +693,7 @@ group over the finite f64s. **Rounding happens once, when the value is read.** T
- `Min` and `Max` are already exact.
- Non-finite values are counted (NaN, +∞, −∞), so they can be retracted too.
**Measured**, in the same example, by `ExactSum` (147 lines, including its rounding):
**Measured**, in the same example, by `ExactSum` (158 lines, including its rounding and the weight bound):
- **Maintained equals fresh, bit for bit.** At all 25 checkpoints above, an `ExactSum`
maintained through a million retract-and-insert cycles equals a fresh `ExactSum` over
@@ -639,13 +703,21 @@ group over the finite f64s. **Rounding happens once, when the value is read.** T
- **It is correct.** It was checked (not committed) against Python's `math.fsum` on
20,000 random cases. The cases include subnormals, values near the overflow bound,
and an insert-then-retract of an equal-sized noise set. There were 0 mismatches; the
1,596 cases where `fsum` overflows were checked against exact `Fraction` sums.
- **Cost, Apple M4 Max, best of 3 over 10M values:**
- about 3.2 ns per insert or retract, against about 2.3 ns for a plain f64 add in the
same loop;
- about 1.1 µs per read, which is the rounding, paid once per group read;
1,596 cases where `fsum` overflows were checked against exact `Fraction` sums. After
the weight bound, it was checked again, on 20,000 cases with weights up to 2⁴⁰
against exact `Fraction` sums: 0 mismatches. The review's own oracle run agreed.
- **Cost, Apple M4 Max, best of 3 over 10M values.** The example prints per single
update.
- This revision's three runs agreed: 2.0 ns per insert or retract, against 1.5 ns
for a plain f64 add in the same black-boxed loop, and 0.58 µs per read.
- The previous revision's run on the same machine gave 3.2 against 2.3 ns and 1.1 µs,
and the review's run gave 3.6 against 2.7 ns.
- So an update costs roughly 1.3× a plain add. A read, which is the rounding paid
once per group read, costs 0.6–1.1 µs.
- **568 bytes per group**, against 8 for an f64.
The ranges below are between runs on one kind of machine; read your own run.
The size is the real cost. A document with 100,000 `Sum` groups would hold about 57 MB
of accumulators. A sparse form that stores only the occupied span of limbs would be a
few limbs for typical data. **That is an estimate, not measured.**
@@ -686,7 +758,7 @@ operator rather than one per call site.
| `=` against a typed decimal (`FLOAT_EQ_EPSILON`) | only for sums | yes, exactly |
| typed values such as money | no | yes |
| a value's own rounding when typed (`0.1`) | no: the f64 is already inexact | yes |
| cost | 568 bytes per group, about 3.2 ns per update | bignum weight in the wasm bundle (improvise-l2b8's question 3) |
| cost | 568 bytes per group, 2.0–3.6 ns per update, 0.6–1.1 µs per read | bignum weight in the wasm bundle (improvise-l2b8's question 3) |
**So ADR 005 still matters**, for per-cell arithmetic and for typed values like money.
The accumulator covers only `SUM` and `AVG` over f64. But that is exactly the part this
@@ -837,10 +909,12 @@ displayed path until the differential test holds.
step 3) rebuilds the affected views.** **ADR 008 clauses 3 and 8 (pruning and the
frame observation) depend on this step.**
5. **Formulas**: the formula graph and the formula delta (clause 7), topological
re-evaluation, the component fixed point (clause 6), and the aggregate-over-expression
map that replaces `Expansion::members` (clause 5). Formula values that depend on a
`Sum` or `Avg` read it from the eager fold until step 6. **ADR 008's retirement of
`Expansion::members` depends on this step.**
re-evaluation, the component fixed point (clause 6), and clause 5a's pipeline that
replaces `Expansion::members`: the integrated per-record stage, the map keyed by
context and order key, the inner-`WHERE` join, and the error channel. Its tests
include a change to one operand of a two-operand expression. Formula values that
depend on a `Sum` or `Avg` are re-folded in order-key order until step 6. **ADR
008's retirement of `Expansion::members` depends on this step.**
6. **`Sum` and `Avg`, and column totals**, on question 3's answer: the exact
accumulator in both backends (recommended), or after ADR 005. A column total is a formula over the pooled fold, so it needs step 5's
re-evaluation. **ADR 008 clause 5 (column totals) depends on this step.**
@@ -906,13 +980,20 @@ the user decided", as ADRs 004 and 007 did.
**both** backends, so that incremental equals eager bit for bit.
*Recommendation:* (c), in `zset`. It is measured bit-equal after a million
retract-and-insert cycles, and exact against `math.fsum` on 20,000 cases. It costs
about 3.2 ns per update and 568 bytes per group, and it does not wait for ADR 005.
(b) is never bit-exact, and its gap reaches `FLOAT_EQ_EPSILON`. (a) remains right for
per-cell arithmetic and typed values, and it composes with (c): under ADR 005 a
decimal sum is exact on its own. The cost to accept is that today's displayed sums
change in their last bits, because they become correctly rounded, and that
`Avg`'s one rounding must be stated in step 6.
retract-and-insert cycles, and exact against an exact oracle on 20,000 cases, with
and without large weights. It does not wait for ADR 005. (b) is never bit-exact, and
its gap reaches `FLOAT_EQ_EPSILON`. (a) remains right for per-cell arithmetic and
typed values, and it composes with (c): under ADR 005 a decimal sum is exact on its
own. **The costs to accept:**
- 568 bytes per group, and 2.0–3.6 ns per update against 1.5–2.7 ns for a plain add.
- **`Eager` pays the read on every aggregate evaluation**, 0.6–1.1 µs, since it
would use the same accumulator. A whole-grid eager projection pays it once per
summed cell.
- Today's displayed sums change in their last bits, because they become correctly
rounded.
- **Signed zero:** the accumulator reads `[−0.0]` as `+0.0`, where the f64 `sum()`
that `eval_agg` uses (`types.rs:79`) gives `−0.0`.
- `Avg`'s one rounding must be stated in step 6.
4. **The sixteen-pass bound.** An acyclic chain needing all sixteen passes is reported
`circular` today (core.md §3). Should `Incremental` reproduce that?
@@ -962,10 +1043,12 @@ the user decided", as ADRs 004 and 007 did.
position, with that category's item order added to the operator shape so that a
reorder rebuilds them? Or should they key by stable item identity (ADR 007), and
look the order up at read time?
*Recommendation:* item position, with the order in the operator shape. Reads stay
O(log d), like `Min`/`Max`, and the same generic operator serves all four. An item
reorder is a rare structural edit, and clause 7 already rebuilds on those. This
extends the operator shape's `measure_agg` part to cover "and the item order of
each ordering category". ADR 008 clause 3 lists the parts as `view_shape`, group
membership and `measure_agg`. This reading changes what the `measure_agg` part
covers, not the list, so ADR 008's text and cross-references still hold.
*Recommendation:* item position. Reads stay O(log d), like `Min`/`Max`, and the
same generic operator serves all four. The order of **drawn** items is already in
`view_shape` (`app.rs:47-52`), so a reorder of drawn items already rebuilds, and
nothing new is needed for them. The one open part is **hidden** items, whose
positions `view_shape` does not hash. Recommended: `LAST`/`FIRST` order only the
values the fold covers, which are the drawn members. Then the operator shape needs
no widening at all, and ADR 008's text and cross-references hold unchanged. If the
user wants hidden items ordered too, the `measure_agg` part must also cover their
positions.
crates/improvise-core/examples/retraction_drift.rs
+41 -13
View File
@@ -96,13 +96,15 @@ impl Compensated {
const LIMB_BITS: u32 = 32;
/// Every finite f64 is `mant * 2^(shift - 1074)` with `shift <= 2045` and `mant < 2^53`.
const LIMBS: usize = 67;
/// The most weight one limb absorbs between carries: each add moves a limb by < 2^32.
const CHUNK: i64 = 1 << 30;
/// An exact sum of f64s: a signed fixed-point integer in units of 2^-1074, wide enough
/// for every finite f64, with non-finite values counted so they can be retracted too.
#[derive(Clone)]
struct ExactSum {
limbs: [i64; LIMBS],
pending: u32,
pending: u64,
nan: i64,
pos_inf: i64,
neg_inf: i64,
@@ -119,17 +121,30 @@ impl ExactSum {
}
}
/// Add `x` with `weight` +1 (insert) or -1 (retract). Exact: no rounding happens here.
/// Add `x` with any `weight` (a consolidated Z-set weight). Exact: no rounding here.
fn add(&mut self, x: f64, weight: i64) {
match (x.is_nan(), x.is_infinite()) {
(true, _) => self.nan += weight,
(false, true) if x > 0.0 => self.pos_inf += weight,
(false, true) => self.neg_inf += weight,
(false, false) => self.add_finite(x, weight),
(false, false) => {
let mut left = weight;
while left != 0 {
let chunk = left.clamp(-CHUNK, CHUNK);
self.add_finite(x, chunk);
left -= chunk;
}
}
}
}
/// Bounded so each limb stays under 2^62: `|weight| <= CHUNK` and `pending`
/// counts magnitude, not calls.
fn add_finite(&mut self, x: f64, weight: i64) {
if self.pending + weight.unsigned_abs() > CHUNK as u64 {
propagate(&mut self.limbs);
self.pending = 0;
}
let bits = x.to_bits();
let biased = ((bits >> 52) & 0x7ff) as u32;
let fraction = bits & ((1 << 52) - 1);
@@ -148,11 +163,7 @@ impl ExactSum {
let part = ((wide >> (LIMB_BITS * i as u32)) & 0xffff_ffff) as i64;
self.limbs[k + i] += sign * part;
}
self.pending += 1;
if self.pending == 1 << 30 {
propagate(&mut self.limbs);
self.pending = 0;
}
self.pending += weight.unsigned_abs();
}
/// The exact sum rounded to the nearest f64, ties to even: the one rounding.
@@ -375,12 +386,13 @@ fn cost() {
let n = 10_000_000;
let mut rng = Rng(7);
let values: Vec<f64> = (0..n).map(|_| typed(decimal(&mut rng, 9))).collect();
let plain = per_op(n, || {
let updates = 3 * n;
let plain = per_op(updates, || {
values
.iter()
.fold(0.0, |s, &v| black_box(s + v) - black_box(v) + v)
});
let exact_add = per_op(n, || {
let exact_add = per_op(updates, || {
let mut xs = ExactSum::new();
values.iter().for_each(|&v| {
xs.add(black_box(v), 1);
@@ -393,9 +405,9 @@ fn cost() {
values.iter().for_each(|&v| xs.add(v, 1));
let read = per_op(1, || xs.value());
println!();
println!("cost, {n} values, best of 3 (per op = one insert + one retract + one insert):");
println!(" plain f64 add/sub {plain:>8.2} ns per op");
println!(" exact accumulator {exact_add:>8.2} ns per op");
println!("cost, {n} values x (insert, retract, insert), best of 3, per single update:");
println!(" plain f64 add/sub {plain:>8.2} ns per update");
println!(" exact accumulator {exact_add:>8.2} ns per update");
println!(" exact read (round) {read:>8.0} ns per read");
println!(
" state per group {} bytes, against 8 for an f64",
@@ -403,6 +415,21 @@ fn cost() {
);
}
/// A consolidated Z-set weight can be large; the accumulator must stay exact at 2^33.
fn large_weight() {
let x = f64::from_bits((1u64 << 32) - 1);
let mut xs = ExactSum::new();
xs.add(x, 1 << 33);
let want = ((1u64 << 32) - 1) as f64 * 2f64.powi(33) * f64::from_bits(1);
println!();
println!(
"large weight: (2^32-1) x 2^-1074 at weight 2^33 reads {:e}, exact {:e}, equal {}",
xs.value(),
want,
xs.value().to_bits() == want.to_bits()
);
}
fn main() {
println!(
"{:<22} {:>8} {:>10} {:>6} {:>10} {:>6} {:>5} {:>10} {:>10} {:>10} {:>7} {:>10}",
@@ -426,5 +453,6 @@ fn main() {
random_updates(seed, 18_000, 9, &checkpoints);
}
absorbed_by_a_large_value();
large_weight();
cost();
}