From e15b28582227f5dcd3566ef3b5d85bf9beb1f52d Mon Sep 17 00:00:00 2001 From: "Claude (adr009-zset)" Date: Fri, 9 Oct 2026 22:57:39 -0700 Subject: [PATCH 1/8] feat(zset): the Z-set group, map, filter, distinct and the stream operators (improvise-tk51) Co-Authored-By: Claude Sonnet 5.5 Claude-Session: https://claude.ai/code/session_01VdfEGXA7aJ6ftMsCc9PJze --- Cargo.lock | 7 + Cargo.toml | 2 +- crates/zset/Cargo.toml | 14 + crates/zset/src/lib.rs | 351 +++++++++++++++++++ crates/zset/tests/properties.rs | 594 ++++++++++++++++++++++++++++++++ 5 files changed, 967 insertions(+), 1 deletion(-) create mode 100644 crates/zset/Cargo.toml create mode 100644 crates/zset/src/lib.rs create mode 100644 crates/zset/tests/properties.rs diff --git a/Cargo.lock b/Cargo.lock index 51a21dda..d09a5591 100644 --- a/Cargo.lock +++ b/Cargo.lock @@ -2725,3 +2725,10 @@ name = "zmij" version = "1.0.23" source = "registry+https://github.com/rust-lang/crates.io-index" checksum = "29666d0abbfad1e3dc4dcf6144730dd3a3ab225bbbdac83319345b1b44ccfc1b" + +[[package]] +name = "zset" +version = "0.1.0" +dependencies = [ + "proptest", +] diff --git a/Cargo.toml b/Cargo.toml index a07fe043..1f99d257 100644 --- a/Cargo.toml +++ b/Cargo.toml @@ -1,5 +1,5 @@ [workspace] -members = [".", "crates/improvise-formula", "crates/improvise-core", "crates/improvise-protocol", "crates/improvise-io", "crates/improvise-command", "crates/improvise-wasm-client", "crates/improvise-ws-server", "crates/improvise-worker-server", "crates/gp-tree", "crates/improvise-gp", "crates/numtower"] +members = [".", "crates/improvise-formula", "crates/improvise-core", "crates/improvise-protocol", "crates/improvise-io", "crates/improvise-command", "crates/improvise-wasm-client", "crates/improvise-ws-server", "crates/improvise-worker-server", "crates/gp-tree", "crates/improvise-gp", "crates/numtower", "crates/zset"] [package] name = "improvise" diff --git a/crates/zset/Cargo.toml b/crates/zset/Cargo.toml new file mode 100644 index 00000000..811333d0 --- /dev/null +++ b/crates/zset/Cargo.toml @@ -0,0 +1,14 @@ +[package] +name = "zset" +version = "0.1.0" +edition = "2024" +license = "Apache-2.0" +description = "Z-sets: finite maps from keys to non-zero integer weights, an abelian group, with the stream operators incremental evaluation needs." +keywords = ["z-set", "dbsp", "incremental", "group"] +categories = ["data-structures"] + +# ADR 009 clause 1: no dependencies beyond std, so it is wasm32-clean and serde-free. +[dependencies] + +[dev-dependencies] +proptest = "1" diff --git a/crates/zset/src/lib.rs b/crates/zset/src/lib.rs new file mode 100644 index 00000000..bb28430a --- /dev/null +++ b/crates/zset/src/lib.rs @@ -0,0 +1,351 @@ +//! Z-sets: finite maps from keys to non-zero `i64` weights, forming an abelian group +//! under pointwise addition (ADR 009 clause 1). +//! +//! Reasoning, the interpretations the ADR left open and the overflow policy are in +//! `context/code/zset.md`. Evidence for each test is in `context/test-evidence/zset.md`. + +use std::collections::BTreeMap; +use std::collections::btree_map::Entry; +use std::iter::FromIterator; +use std::ops::{Add, AddAssign, Mul, Neg, Sub, SubAssign}; + +/// A map from `K` to a non-zero `i64` weight. +/// +/// The representation is canonical: a key with weight zero is never stored, so two +/// Z-sets are `==` exactly when they assign every key the same weight. Iteration is in +/// ascending key order. +#[derive(Clone, Debug, PartialEq, Eq, Hash, PartialOrd, Ord)] +pub struct ZSet { + weights: BTreeMap, +} + +#[track_caller] +fn overflow(op: &str, a: i64, b: i64) -> ! { + panic!("zset: weight overflow in {op}: {a} and {b} do not combine within i64") +} + +fn plus(a: i64, b: i64) -> i64 { + a.checked_add(b).unwrap_or_else(|| overflow("add", a, b)) +} + +fn negated(a: i64) -> i64 { + a.checked_neg().unwrap_or_else(|| overflow("neg", a, 0)) +} + +fn times(a: i64, n: i64) -> i64 { + a.checked_mul(n).unwrap_or_else(|| overflow("scale", a, n)) +} + +impl Default for ZSet { + fn default() -> Self { + ZSet { + weights: BTreeMap::new(), + } + } +} + +impl ZSet { + /// The zero of the group: no key has a weight. + pub fn new() -> Self { + Self::default() + } + + /// One key at `weight`; a zero weight gives the zero Z-set. + pub fn singleton(key: K, weight: i64) -> Self { + let mut z = Self::new(); + z.insert(key, weight); + z + } + + /// The weight of `key`, zero if it is absent. + pub fn weight(&self, key: &K) -> i64 { + self.weights.get(key).copied().unwrap_or(0) + } + + pub fn is_zero(&self) -> bool { + self.weights.is_empty() + } + + /// The number of keys with a non-zero weight. + pub fn len(&self) -> usize { + self.weights.len() + } + + /// Keys with their weights, in ascending key order. No weight is zero. + pub fn iter(&self) -> impl Iterator { + self.weights.iter().map(|(k, w)| (k, *w)) + } + + /// Adds `weight` to `key`'s weight, dropping the key if the sum is zero. + /// + /// Panics if the sum does not fit an `i64`. + pub fn insert(&mut self, key: K, weight: i64) { + match self.weights.entry(key) { + Entry::Vacant(e) => { + if weight != 0 { + e.insert(weight); + } + } + Entry::Occupied(mut e) => { + let sum = plus(*e.get(), weight); + if sum == 0 { + e.remove(); + } else { + *e.get_mut() = sum; + } + } + } + } + + /// Maps every key through `f`; the weights of keys with one image sum. + pub fn map(&self, mut f: impl FnMut(&K) -> L) -> ZSet { + let mut out = ZSet::new(); + for (k, w) in &self.weights { + out.insert(f(k), *w); + } + out + } + + /// Keeps the keys `keep` accepts, with their weights. It looks at the key only, + /// which is what makes it linear. + pub fn filter(&self, mut keep: impl FnMut(&K) -> bool) -> Self + where + K: Clone, + { + self.weights + .iter() + .filter(|(k, _)| keep(k)) + .map(|(k, w)| (k.clone(), *w)) + .collect() + } + + /// Weight 1 for every key whose weight is positive; every other key is dropped. + pub fn distinct(&self) -> Self + where + K: Clone, + { + self.weights + .iter() + .filter(|(_, w)| **w > 0) + .map(|(k, _)| (k.clone(), 1)) + .collect() + } + + /// Every weight times `n`; zero gives the zero Z-set. + /// + /// Panics if a product does not fit an `i64`. + pub fn scale(&self, n: i64) -> Self + where + K: Clone, + { + if n == 0 { + return Self::new(); + } + let weights = self + .weights + .iter() + .map(|(k, w)| (k.clone(), times(*w, n))) + .collect(); + ZSet { weights } + } +} + +impl FromIterator<(K, i64)> for ZSet { + /// Weights of repeated keys sum. + fn from_iter>(iter: I) -> Self { + let mut z = ZSet::new(); + z.extend(iter); + z + } +} + +impl Extend<(K, i64)> for ZSet { + fn extend>(&mut self, iter: I) { + for (k, w) in iter { + self.insert(k, w); + } + } +} + +impl IntoIterator for ZSet { + type Item = (K, i64); + type IntoIter = std::collections::btree_map::IntoIter; + + fn into_iter(self) -> Self::IntoIter { + self.weights.into_iter() + } +} + +impl AddAssign for ZSet { + fn add_assign(&mut self, other: Self) { + self.extend(other); + } +} + +impl AddAssign<&ZSet> for ZSet { + fn add_assign(&mut self, other: &ZSet) { + self.extend(other.iter().map(|(k, w)| (k.clone(), w))); + } +} + +impl Add for ZSet { + type Output = ZSet; + + fn add(mut self, other: Self) -> Self { + self += other; + self + } +} + +impl Add for &ZSet { + type Output = ZSet; + + fn add(self, other: Self) -> ZSet { + let mut z = self.clone(); + z += other; + z + } +} + +impl Neg for ZSet { + type Output = ZSet; + + fn neg(self) -> Self { + let weights = self + .weights + .into_iter() + .map(|(k, w)| (k, negated(w))) + .collect(); + ZSet { weights } + } +} + +impl Neg for &ZSet { + type Output = ZSet; + + fn neg(self) -> ZSet { + self.clone().neg() + } +} + +impl Sub for ZSet { + type Output = ZSet; + + fn sub(mut self, other: Self) -> Self { + self -= other; + self + } +} + +impl Sub for &ZSet { + type Output = ZSet; + + fn sub(self, other: Self) -> ZSet { + self.clone() - other.clone() + } +} + +impl SubAssign for ZSet { + fn sub_assign(&mut self, other: Self) { + self.extend(other.into_iter().map(|(k, w)| (k, negated(w)))); + } +} + +impl Mul for &ZSet { + type Output = ZSet; + + fn mul(self, n: i64) -> ZSet { + self.scale(n) + } +} + +/// The running sums of a stream of deltas: element `i` is `d_0 + ... + d_i`. +pub fn integrate(deltas: &[ZSet]) -> Vec> { + let mut state = ZSet::new(); + deltas + .iter() + .map(|d| { + state += d; + state.clone() + }) + .collect() +} + +/// The differences of a stream of states: element 0 is `s_0` (the state before it is +/// zero), and element `i` is `s_i - s_(i-1)`. +pub fn differentiate(states: &[ZSet]) -> Vec> { + let mut previous = ZSet::new(); + states + .iter() + .map(|s| { + let d = s - &previous; + previous = s.clone(); + d + }) + .collect() +} + +#[cfg(test)] +mod tests { + use super::*; + + #[test] + fn a_zero_weight_is_never_stored() { + let z = ZSet::from_iter([("a", 2), ("a", -2), ("b", 0), ("c", 1)]); + assert_eq!(z.len(), 1); + assert_eq!(z.weight(&"a"), 0); + assert_eq!(z, ZSet::singleton("c", 1)); + assert!(ZSet::singleton("x", 0).is_zero()); + } + + #[test] + fn distinct_clamps_positive_weights_and_drops_the_rest() { + let z = ZSet::from_iter([("a", 5), ("b", -3), ("c", 1)]); + assert_eq!(z.distinct(), ZSet::from_iter([("a", 1), ("c", 1)])); + } + + #[test] + fn map_sums_colliding_images() { + let z = ZSet::from_iter([(1, 2), (2, -2), (3, 4)]); + assert_eq!(z.map(|k| k % 2), ZSet::from_iter([(0, -2), (1, 6)])); + assert!(ZSet::from_iter([(1, 2), (2, -2)]).map(|_| 0).is_zero()); + } + + #[test] + fn the_differentiate_of_a_stream_starts_from_zero() { + let s = vec![ZSet::singleton(1, 1), ZSet::singleton(2, 1)]; + let d = differentiate(&s); + assert_eq!(d[0], s[0]); + assert_eq!(d[1], ZSet::from_iter([(1, -1), (2, 1)])); + assert_eq!(integrate(&d), s); + } + + #[test] + #[should_panic(expected = "weight overflow in add")] + fn adding_past_i64_max_panics() { + let _ = ZSet::singleton(1, i64::MAX) + ZSet::singleton(1, 1); + } + + #[test] + #[should_panic(expected = "weight overflow in add")] + fn adding_past_i64_min_panics() { + let _ = ZSet::singleton(1, i64::MIN) + ZSet::singleton(1, -1); + } + + #[test] + #[should_panic(expected = "weight overflow in neg")] + fn negating_i64_min_panics() { + let _ = -ZSet::singleton(1, i64::MIN); + } + + #[test] + #[should_panic(expected = "weight overflow in scale")] + fn scaling_past_i64_panics() { + let _ = ZSet::singleton(1, i64::MAX).scale(2); + } + + #[test] + fn scaling_by_zero_never_overflows() { + assert!(ZSet::singleton(1, i64::MAX).scale(0).is_zero()); + } +} diff --git a/crates/zset/tests/properties.rs b/crates/zset/tests/properties.rs new file mode 100644 index 00000000..beaafa56 --- /dev/null +++ b/crates/zset/tests/properties.rs @@ -0,0 +1,594 @@ +//! Property tests for `zset`. Each property is a checker that takes the implementation as +//! a parameter: the property's own test runs it on `ZSet`, and a `_catches_` companion runs +//! the same checker on a rival with one injected fault and requires that the failure carry +//! the property's tag. The evidence is in `context/test-evidence/zset.md`. + +use proptest::prelude::*; +use proptest::test_runner::{TestError, TestRunner}; +use zset::{ZSet, differentiate, integrate}; + +type Pairs = Vec<(u8, i64)>; + +/// The operations under test, over a representation the implementation chooses. +trait Alg { + type Z: Clone + std::fmt::Debug; + fn from_pairs(&self, p: &[(u8, i64)]) -> Self::Z; + fn add(&self, a: &Self::Z, b: &Self::Z) -> Self::Z; + fn neg(&self, a: &Self::Z) -> Self::Z; + fn sub(&self, a: &Self::Z, b: &Self::Z) -> Self::Z; + fn scale(&self, a: &Self::Z, n: i64) -> Self::Z; + /// Images are `k % m`, so keys collide. + fn map(&self, a: &Self::Z, m: u8) -> Self::Z; + /// Keeps the keys whose `k % 3` is not `drop`. + fn filter(&self, a: &Self::Z, drop: u8) -> Self::Z; + fn distinct(&self, a: &Self::Z) -> Self::Z; + fn integrate(&self, d: &[Self::Z]) -> Vec; + fn differentiate(&self, s: &[Self::Z]) -> Vec; + /// What an iteration yields, in the order it yields it. + fn stored(&self, a: &Self::Z) -> Vec<(u8, i64)>; + /// Whether two values are the same set of weights, however each is stored. + fn same(&self, a: &Self::Z, b: &Self::Z) -> bool; + fn zero(&self) -> Self::Z { + self.from_pairs(&[]) + } +} + +struct Real; + +impl Alg for Real { + type Z = ZSet; + fn from_pairs(&self, p: &[(u8, i64)]) -> ZSet { + p.iter().copied().collect() + } + fn add(&self, a: &ZSet, b: &ZSet) -> ZSet { + a + b + } + fn neg(&self, a: &ZSet) -> ZSet { + -a + } + fn sub(&self, a: &ZSet, b: &ZSet) -> ZSet { + a - b + } + fn scale(&self, a: &ZSet, n: i64) -> ZSet { + a * n + } + fn map(&self, a: &ZSet, m: u8) -> ZSet { + a.map(|k| k % m) + } + fn filter(&self, a: &ZSet, drop: u8) -> ZSet { + a.filter(|k| k % 3 != drop) + } + fn distinct(&self, a: &ZSet) -> ZSet { + a.distinct() + } + fn integrate(&self, d: &[ZSet]) -> Vec> { + integrate(d) + } + fn differentiate(&self, s: &[ZSet]) -> Vec> { + differentiate(s) + } + fn stored(&self, a: &ZSet) -> Vec<(u8, i64)> { + a.iter().map(|(k, w)| (*k, w)).collect() + } + fn same(&self, a: &ZSet, b: &ZSet) -> bool { + a == b + } +} + +#[derive(Clone, Copy, PartialEq, Debug)] +enum Fault { + None, + KeepZero, + AddKeepsLeft, + AddClamps, + AddIntersects, + NegForgetsAKey, + SubFlipped, + ScaleAbs, + MapOverwrites, + FilterReadsWeight, + DistinctNoClamp, + InsertionOrder, + IntegrateExcludesCurrent, + DifferentiateDropsFirst, +} + +/// A second implementation over a plain vector, with at most one fault injected. +struct Model(Fault); + +type V = Vec<(u8, i64)>; + +impl Model { + fn normal(&self, v: V) -> V { + let mut out: V = Vec::new(); + for (k, w) in v { + match out.iter_mut().find(|(k2, _)| *k2 == k) { + Some(e) => e.1 += w, + None => out.push((k, w)), + } + } + if self.0 != Fault::KeepZero { + out.retain(|(_, w)| *w != 0); + } + if self.0 != Fault::InsertionOrder { + out.sort_by_key(|(k, _)| *k); + } + out + } +} + +impl Alg for Model { + type Z = V; + fn from_pairs(&self, p: &[(u8, i64)]) -> V { + self.normal(p.to_vec()) + } + fn add(&self, a: &V, b: &V) -> V { + if self.0 == Fault::AddKeepsLeft { + let mut out = a.clone(); + for (k, w) in b { + if !out.iter().any(|(k2, _)| k2 == k) { + out.push((*k, *w)); + } + } + return self.normal(out); + } + if self.0 == Fault::AddIntersects { + let both = |k: &u8, v: &V| v.iter().any(|(k2, _)| k2 == k); + let kept = a.iter().chain(b).filter(|(k, _)| both(k, a) && both(k, b)); + return self.normal(kept.copied().collect()); + } + let sum = self.normal(a.iter().chain(b).copied().collect()); + if self.0 == Fault::AddClamps { + return sum.into_iter().map(|(k, w)| (k, w.clamp(-10, 10))).collect(); + } + sum + } + fn neg(&self, a: &V) -> V { + let skip = usize::from(self.0 == Fault::NegForgetsAKey); + self.normal(a.iter().skip(skip).map(|(k, w)| (*k, -w)).collect()) + } + fn sub(&self, a: &V, b: &V) -> V { + let (x, y) = if self.0 == Fault::SubFlipped { (b, a) } else { (a, b) }; + self.add(x, &self.neg(y)) + } + fn scale(&self, a: &V, n: i64) -> V { + let n = if self.0 == Fault::ScaleAbs { n.abs() } else { n }; + self.normal(a.iter().map(|(k, w)| (*k, w * n)).collect()) + } + fn map(&self, a: &V, m: u8) -> V { + if self.0 == Fault::MapOverwrites { + let mut out: Vec<(u8, i64)> = Vec::new(); + for (k, w) in a { + out.retain(|(k2, _)| *k2 != k % m); + out.push((k % m, *w)); + } + return self.normal(out); + } + self.normal(a.iter().map(|(k, w)| (k % m, *w)).collect()) + } + fn filter(&self, a: &V, drop: u8) -> V { + let weighted = self.0 == Fault::FilterReadsWeight; + self.normal( + a.iter() + .filter(|(k, w)| k % 3 != drop && (!weighted || *w > 0)) + .copied() + .collect(), + ) + } + fn distinct(&self, a: &V) -> V { + let clamp = if self.0 == Fault::DistinctNoClamp { None } else { Some(1) }; + self.normal( + a.iter() + .filter(|(_, w)| *w > 0) + .map(|(k, w)| (*k, clamp.unwrap_or(*w))) + .collect(), + ) + } + fn integrate(&self, d: &[V]) -> Vec { + let mut state = self.zero(); + let mut out = Vec::new(); + for x in d { + if self.0 == Fault::IntegrateExcludesCurrent { + out.push(state.clone()); + state = self.add(&state, x); + } else { + state = self.add(&state, x); + out.push(state.clone()); + } + } + out + } + fn differentiate(&self, s: &[V]) -> Vec { + let mut prev = self.zero(); + let mut out = Vec::new(); + for (i, x) in s.iter().enumerate() { + let d = self.sub(x, &prev); + out.push(if i == 0 && self.0 == Fault::DifferentiateDropsFirst { self.zero() } else { d }); + prev = x.clone(); + } + out + } + fn stored(&self, a: &V) -> Vec<(u8, i64)> { + a.clone() + } + fn same(&self, a: &V, b: &V) -> bool { + let sorted = |v: &V| { + let mut v = v.clone(); + v.sort(); + v + }; + sorted(a) == sorted(b) + } +} + +fn weight() -> impl Strategy { + prop_oneof![ + 3 => -3i64..=3, + 1 => Just(0i64), + 2 => -(1i64 << 40)..=(1i64 << 40), + ] +} + +/// Keys from a small range, so colliding keys and cancelling pairs are the common case. +fn pairs() -> impl Strategy { + prop::collection::vec((0u8..6, weight()), 0..8) +} + +fn scalar() -> impl Strategy { + prop_oneof![-3i64..=3, -(1i64 << 10)..=(1i64 << 10)] +} + +fn stream() -> impl Strategy> { + prop::collection::vec(pairs(), 0..6) +} + +fn caught( + strategy: impl Strategy, + tag: &str, + check: impl Fn(&T) -> Result<(), TestCaseError>, +) { + let mut runner = TestRunner::deterministic(); + match runner.run(&strategy, |v| check(&v)) { + Err(TestError::Fail(reason, _)) => { + let message = reason.message().to_string(); + assert!(message.contains(tag), "failed, but not on {tag}: {message}"); + } + other => panic!("the rival was not caught on {tag}: {other:?}"), + } +} + +fn ok(strategy: impl Strategy, check: impl Fn(&T) -> Result<(), TestCaseError>) +where + T: std::fmt::Debug, +{ + let mut runner = TestRunner::deterministic(); + runner.run(&strategy, |v| check(&v)).unwrap(); +} + +fn associativity(x: &A, (a, b, c): &(Pairs, Pairs, Pairs)) -> Result<(), TestCaseError> { + let (a, b, c) = (x.from_pairs(a), x.from_pairs(b), x.from_pairs(c)); + let left = x.add(&x.add(&a, &b), &c); + let right = x.add(&a, &x.add(&b, &c)); + prop_assert!(x.same(&left, &right), "[associativity] {left:?} != {right:?}"); + Ok(()) +} + +fn commutativity(x: &A, (a, b): &(Pairs, Pairs)) -> Result<(), TestCaseError> { + let (a, b) = (x.from_pairs(a), x.from_pairs(b)); + let (ab, ba) = (x.add(&a, &b), x.add(&b, &a)); + prop_assert!(x.same(&ab, &ba), "[commutativity] {ab:?} != {ba:?}"); + Ok(()) +} + +fn identity(x: &A, a: &Pairs) -> Result<(), TestCaseError> { + let a = x.from_pairs(a); + let zero = x.zero(); + prop_assert!(x.same(&x.add(&a, &zero), &a), "[identity] a + 0 != a for {a:?}"); + prop_assert!(x.same(&x.add(&zero, &a), &a), "[identity] 0 + a != a for {a:?}"); + Ok(()) +} + +fn inverse(x: &A, a: &Pairs) -> Result<(), TestCaseError> { + let a = x.from_pairs(a); + let sum = x.add(&a, &x.neg(&a)); + prop_assert!(x.same(&sum, &x.zero()), "[inverse] a + (-a) = {sum:?} for {a:?}"); + let diff = x.sub(&a, &a); + prop_assert!(x.same(&diff, &x.zero()), "[inverse] a - a = {diff:?} for {a:?}"); + prop_assert!(x.same(&x.neg(&x.neg(&a)), &a), "[inverse] --a != a for {a:?}"); + Ok(()) +} + +fn subtraction(x: &A, (a, b): &(Pairs, Pairs)) -> Result<(), TestCaseError> { + let (a, b) = (x.from_pairs(a), x.from_pairs(b)); + let (d, e) = (x.sub(&a, &b), x.add(&a, &x.neg(&b))); + prop_assert!(x.same(&d, &e), "[subtraction] a - b = {d:?} but a + (-b) = {e:?}"); + Ok(()) +} + +fn canonical_zero(x: &A, (a, b, n, m): &(Pairs, Pairs, i64, u8)) -> Result<(), TestCaseError> { + let (a, b) = (x.from_pairs(a), x.from_pairs(b)); + let made = [ + a.clone(), + x.add(&a, &b), + x.add(&a, &x.neg(&a)), + x.neg(&a), + x.sub(&a, &b), + x.scale(&a, *n), + x.scale(&a, 0), + x.map(&a, *m), + x.filter(&a, 1), + x.distinct(&a), + ]; + for z in &made { + let zeros: Vec<_> = x.stored(z).into_iter().filter(|(_, w)| *w == 0).collect(); + prop_assert!(zeros.is_empty(), "[canonical-zero] stored zero weights {zeros:?} in {z:?}"); + } + Ok(()) +} + +fn canonical_equality(x: &A, (p, seed): &(Pairs, usize)) -> Result<(), TestCaseError> { + let mut shuffled = p.clone(); + if !shuffled.is_empty() { + let n = shuffled.len(); + shuffled.rotate_left(seed % n); + shuffled.reverse(); + } + let (a, b) = (x.from_pairs(p), x.from_pairs(&shuffled)); + prop_assert!(x.same(&a, &b), "[canonical-equality] {a:?} != {b:?}"); + // The same set built in two steps, with a cancelling pair spliced in. + let mut padded = p.clone(); + padded.push((9, 5)); + padded.push((9, -5)); + let c = x.from_pairs(&padded); + prop_assert!(x.same(&a, &c), "[canonical-equality] a cancelled pair changed {a:?} into {c:?}"); + Ok(()) +} + +fn scalar_multiplication( + x: &A, + (a, b, m, n): &(Pairs, Pairs, i64, i64), +) -> Result<(), TestCaseError> { + let (a, b) = (x.from_pairs(a), x.from_pairs(b)); + let (l, r) = (x.scale(&x.add(&a, &b), *n), x.add(&x.scale(&a, *n), &x.scale(&b, *n))); + prop_assert!(x.same(&l, &r), "[scale] (a+b)*n = {l:?} but a*n + b*n = {r:?}"); + // The scalar side: (m + n) * a, with m, n small enough that m + n cannot wrap. + let (l, r) = (x.scale(&a, m + n), x.add(&x.scale(&a, *m), &x.scale(&a, *n))); + prop_assert!(x.same(&l, &r), "[scale] a*(m+n) = {l:?} but a*m + a*n = {r:?}"); + prop_assert!(x.same(&x.scale(&a, -1), &x.neg(&a)), "[scale] a * -1 != -a for {a:?}"); + prop_assert!(x.same(&x.scale(&a, 1), &a), "[scale] a * 1 != a for {a:?}"); + prop_assert!(x.same(&x.scale(&a, 0), &x.zero()), "[scale] a * 0 != zero for {a:?}"); + Ok(()) +} + +fn map_homomorphism(x: &A, (a, b, m): &(Pairs, Pairs, u8)) -> Result<(), TestCaseError> { + let (a, b) = (x.from_pairs(a), x.from_pairs(b)); + let (l, r) = (x.map(&x.add(&a, &b), *m), x.add(&x.map(&a, *m), &x.map(&b, *m))); + prop_assert!(x.same(&l, &r), "[map] map(a+b) = {l:?} but map(a)+map(b) = {r:?}"); + let (l, r) = (x.map(&x.neg(&a), *m), x.neg(&x.map(&a, *m))); + prop_assert!(x.same(&l, &r), "[map] map(-a) = {l:?} but -map(a) = {r:?}"); + Ok(()) +} + +fn filter_linearity(x: &A, (a, b, d): &(Pairs, Pairs, u8)) -> Result<(), TestCaseError> { + let (a, b) = (x.from_pairs(a), x.from_pairs(b)); + let (l, r) = (x.filter(&x.add(&a, &b), *d), x.add(&x.filter(&a, *d), &x.filter(&b, *d))); + prop_assert!(x.same(&l, &r), "[filter] filter(a+b) = {l:?} but filter(a)+filter(b) = {r:?}"); + let (l, r) = (x.filter(&x.neg(&a), *d), x.neg(&x.filter(&a, *d))); + prop_assert!(x.same(&l, &r), "[filter] filter(-a) = {l:?} but -filter(a) = {r:?}"); + Ok(()) +} + +fn distinct_semantics(x: &A, a: &Pairs) -> Result<(), TestCaseError> { + let a = x.from_pairs(a); + let d = x.distinct(&a); + let expected: Vec<_> = x.stored(&a).into_iter().filter(|(_, w)| *w > 0).map(|(k, _)| (k, 1)).collect(); + prop_assert!( + x.stored(&d) == expected, + "[distinct] distinct({a:?}) = {d:?}, expected weight 1 on exactly the positive keys" + ); + prop_assert!(x.same(&x.distinct(&d), &d), "[distinct] not idempotent on {a:?}"); + Ok(()) +} + +fn iteration_order(x: &A, (p, seed): &(Pairs, usize)) -> Result<(), TestCaseError> { + let a = x.from_pairs(p); + let order = x.stored(&a); + prop_assert!( + order.windows(2).all(|w| w[0].0 < w[1].0), + "[order] iteration is not strictly ascending by key: {order:?}" + ); + let mut shuffled = p.clone(); + if !shuffled.is_empty() { + let n = shuffled.len(); + shuffled.rotate_left(seed % n); + shuffled.reverse(); + } + let again = x.stored(&x.from_pairs(&shuffled)); + prop_assert!(order == again, "[order] insertion order shows through: {order:?} vs {again:?}"); + Ok(()) +} + +fn correction(x: &A, (held, target): &(Pairs, Pairs)) -> Result<(), TestCaseError> { + let (held, target) = (x.from_pairs(held), x.from_pairs(target)); + let delta = x.sub(&target, &held); + let got = x.add(&held, &delta); + prop_assert!(x.same(&got, &target), "[correction] held + (target - held) = {got:?}, not {target:?}"); + let nothing = x.sub(&target, &target); + prop_assert!(x.same(¬hing, &x.zero()), "[correction] a correct state needs {nothing:?}"); + Ok(()) +} + +fn streams(x: &A, s: &Vec) -> Result<(), TestCaseError> { + let deltas: Vec<_> = s.iter().map(|p| x.from_pairs(p)).collect(); + let states = x.integrate(&deltas); + prop_assert!(states.len() == deltas.len(), "[stream] integrate changed the length"); + let mut running = x.zero(); + for (i, d) in deltas.iter().enumerate() { + running = x.add(&running, d); + prop_assert!(x.same(&states[i], &running), "[stream] integrate[{i}] = {:?}, not {running:?}", states[i]); + } + let back = x.differentiate(&states); + prop_assert!(back.len() == deltas.len(), "[stream] differentiate changed the length"); + for (i, d) in deltas.iter().enumerate() { + prop_assert!(x.same(&back[i], d), "[stream] differentiate(integrate(d))[{i}] = {:?}, not {d:?}", back[i]); + } + // The other direction, from arbitrary states. + let again = x.integrate(&x.differentiate(&deltas)); + for (i, d) in deltas.iter().enumerate() { + prop_assert!(x.same(&again[i], d), "[stream] integrate(differentiate(s))[{i}] = {:?}, not {d:?}", again[i]); + } + Ok(()) +} + +macro_rules! property { + ($name:ident, $catches:ident, $strategy:expr, $check:ident, $tag:literal, $($rival:ident => $test:ident),+) => { + proptest! { + #[test] + fn $name(input in $strategy) { + $check(&Real, &input)?; + } + } + + #[test] + fn $catches() { + // The same checker run on a second, correct implementation passes. + ok($strategy, |v| $check(&Model(Fault::None), v)); + } + + $( + #[test] + fn $test() { + caught($strategy, concat!("[", $tag, "]"), |v| $check(&Model(Fault::$rival), v)); + } + )+ + }; +} + +property!( + addition_is_associative, + associativity_holds_on_the_model, + (pairs(), pairs(), pairs()), + associativity, + "associativity", + AddClamps => associativity_catches_an_add_that_clamps_weights +); + +property!( + addition_is_commutative, + commutativity_holds_on_the_model, + (pairs(), pairs()), + commutativity, + "commutativity", + AddKeepsLeft => commutativity_catches_an_add_that_keeps_the_left_weight +); + +property!( + zero_is_the_identity, + identity_holds_on_the_model, + pairs(), + identity, + "identity", + AddIntersects => identity_catches_an_add_that_keeps_only_shared_keys +); + +property!( + every_set_has_an_inverse, + inverse_holds_on_the_model, + pairs(), + inverse, + "inverse", + KeepZero => inverse_catches_an_add_that_keeps_zero_weights, + NegForgetsAKey => inverse_catches_a_neg_that_forgets_a_key +); + +property!( + subtraction_is_adding_the_negation, + subtraction_holds_on_the_model, + (pairs(), pairs()), + subtraction, + "subtraction", + SubFlipped => subtraction_catches_a_flipped_sub +); + +property!( + no_zero_weight_is_ever_stored, + canonical_zero_holds_on_the_model, + (pairs(), pairs(), scalar(), 1u8..5), + canonical_zero, + "canonical-zero", + KeepZero => canonical_zero_catches_an_add_that_keeps_zero_weights +); + +property!( + equal_sets_compare_equal, + canonical_equality_holds_on_the_model, + (pairs(), any::()), + canonical_equality, + "canonical-equality", + KeepZero => canonical_equality_catches_an_add_that_keeps_zero_weights +); + +property!( + scalar_multiplication_distributes, + scale_holds_on_the_model, + (pairs(), pairs(), scalar(), scalar()), + scalar_multiplication, + "scale", + ScaleAbs => scale_catches_a_scale_that_takes_the_absolute_value, + KeepZero => scale_catches_a_scale_by_zero_that_keeps_zero_weights +); + +property!( + map_is_a_homomorphism, + map_holds_on_the_model, + (pairs(), pairs(), 1u8..5), + map_homomorphism, + "map", + MapOverwrites => map_catches_a_map_that_overwrites_colliding_keys +); + +property!( + filter_is_linear, + filter_holds_on_the_model, + (pairs(), pairs(), 0u8..3), + filter_linearity, + "filter", + FilterReadsWeight => filter_catches_a_filter_that_reads_the_weight +); + +property!( + distinct_clamps_positive_weights_to_one, + distinct_holds_on_the_model, + pairs(), + distinct_semantics, + "distinct", + DistinctNoClamp => distinct_catches_a_distinct_without_clamping +); + +property!( + iteration_is_ascending_and_independent_of_insertion_order, + order_holds_on_the_model, + (pairs(), any::()), + iteration_order, + "order", + InsertionOrder => order_catches_insertion_order_iteration +); + +property!( + held_plus_target_minus_held_is_target, + correction_holds_on_the_model, + (pairs(), pairs()), + correction, + "correction", + SubFlipped => correction_catches_a_flipped_sub +); + +property!( + integrate_and_differentiate_invert_each_other, + stream_holds_on_the_model, + stream(), + streams, + "stream", + IntegrateExcludesCurrent => stream_catches_an_integrate_that_excludes_the_current_delta, + DifferentiateDropsFirst => stream_catches_a_differentiate_that_drops_the_first_state +); From 1bb73cbe4feae3adba59e420595be35d900ea16b Mon Sep 17 00:00:00 2001 From: "Claude (adr009-zset)" Date: Fri, 9 Oct 2026 23:03:32 -0700 Subject: [PATCH 2/8] docs(zset): the reasoning, the evidence and the wasm gate entry (improvise-tk51) Registers zset in nix/ci.nix's wasmCrates and the doc site, shortens the comment runs, and fixes the clippy findings in the test crate. Co-Authored-By: Claude Sonnet 5.5 Claude-Session: https://claude.ai/code/session_01VdfEGXA7aJ6ftMsCc9PJze --- context/code/zset.md | 89 ++++++++++++ context/test-evidence/zset.md | 227 ++++++++++++++++++++++++++++++ crates/zset/src/lib.rs | 26 ++-- crates/zset/tests/properties.rs | 237 ++++++++++++++++++++++++-------- nix/ci.nix | 2 + scripts/build-doc-site.mjs | 2 + 6 files changed, 506 insertions(+), 77 deletions(-) create mode 100644 context/code/zset.md create mode 100644 context/test-evidence/zset.md diff --git a/context/code/zset.md b/context/code/zset.md new file mode 100644 index 00000000..76df1f00 --- /dev/null +++ b/context/code/zset.md @@ -0,0 +1,89 @@ +# `zset`: the reasoning + +`crates/zset` is ADR 009 step 1 (improvise-tk51, epic improvise-bw4p): the Z-set group, first +and alone. Nothing depends on it yet, so it changes no behaviour. The decisions are the +ADR's (`context/adr/009-incremental-evaluation.md`, clause 1). This file records how the +crate reads them, where the ADR left a choice open, and the evidence discipline. The +evidence for each test is in `context/test-evidence/zset.md`. + +## The shape + +| item | what it is | +|---|---| +| `ZSet` | a map from `K` to a non-zero `i64` weight; an abelian group | +| `+`, `-`, unary `-`, `* i64`, `scale` | the group operations and scalar multiplication | +| `new`, `singleton`, `insert`, `FromIterator`, `Extend` | construction; weights of equal keys sum | +| `weight`, `is_zero`, `len`, `iter`, `IntoIterator` | reads; iteration is ascending by key | +| `map`, `filter`, `distinct` | the three per-element operators | +| `integrate`, `differentiate` | the stream operators, over a slice | + +There are no dependencies: not serde (clause 9 keeps the wire form in `improvise-protocol`), +not even the workspace's own crates. The crate is wasm32-clean by construction and is in +`nix/ci.nix`'s `wasmCrates`. + +## Canonical form + +A key with weight zero is never stored. `insert` removes a key whose sum reaches zero, and +`singleton(k, 0)` is the zero Z-set. Two Z-sets are therefore `==` exactly when every key has +the same weight, so the derived `PartialEq`, `Hash` and `Ord` are the group's equality. The +clause 9 correction `target - held` relies on it: a correct state gives `==` the zero Z-set, +and `is_zero` is `len() == 0`, not a scan. + +The representation is a `BTreeMap`. Iteration order is the key order, the same in every +process and for every insertion order, which clause 3 needs (eager folds in `CellKey` order) +and which a `HashMap` would give up (`context/code/core.md`, gotcha 18's argument). + +## Interpretations + +The ADR is one paragraph on the crate, and says more about what it is for than what it is. +These are the readings this step takes. + +1. **Clause 1 lists a `Circuit` and more operators; this step builds the pure part.** The + ADR's list is `delay`, `integrate`, `differentiate`, `map`, `filter`, `flat_map`, + `index_by`, `join_indexed`, `distinct` and `aggregate`, run by a synchronous `Circuit`, + plus resumable rebuilds and a trace interface. Step 1 as ticketed is the group and the + operators that are functions of a Z-set or of a stream of them: `map`, `filter`, + `distinct`, `integrate`, `differentiate`. The rest needs the circuit (a clock, state held + between steps), or a second key type (`index_by`, `join_indexed`, `aggregate`), and is + left to the steps that use it rather than designed without a caller. `flat_map` is + `map` into several images and has no user yet either. +2. **`integrate` and `differentiate` are slice functions, not circuit nodes.** + `integrate(&[d_0, d_1, ..])` is the running sums `d_0 + .. + d_i`; `differentiate` is + its inverse, `s_0` then `s_i - s_(i-1)`. The state before the first element is zero, as in + DBSP. `delay` is not provided: over a slice it is a shift, and a circuit gives it meaning. +3. **`distinct` is not linear, and is not a group homomorphism.** It keeps weight 1 on the + keys whose weight is positive and drops every other key, negative included. That is the + set-semantics operator of DBSP. The ADR says nothing about negative weights; dropping + them is the standard reading, and the one that makes `distinct` idempotent. +4. **Operators are methods on `&self`, group operations are `std::ops` traits.** `K: Clone` + is required only where a result copies keys (`filter`, `distinct`, `scale`, the borrowed + operators); `map` and the by-value operators need only `Ord`. +5. **Overflow.** Neither clause 1 nor clause 8 states a policy for weights (clause 8 is about + `f64` sums). A weight that wraps would turn a retraction into an insertion with nothing + to show it, which is the failure the ADR's exactness argument is against. So every weight + operation uses `checked_*` and **panics** with `zset: weight overflow in `, in debug + and in release (`checked_*` does not depend on `overflow-checks`). The operations are + `add` (including `insert`, `Extend`, `FromIterator`), `neg` (so `i64::MIN` panics) and + `scale`. Scaling by zero cannot overflow and returns the zero Z-set. A panic, not a + `Result`: `Result` does not belong in the majority of the code (`AGENTS.md`), and a weight + near `i64::MAX` is a defect in the caller, not an input to recover from. The weights + clause 3 produces are small (one per cell). +6. **Stable error text.** The panic message names the operation and both operands, so a + failure in a long-running host is diagnosable from the log. + +## What the tests are + +`crates/zset/tests/properties.rs` holds one checker per property, parameterised by an `Alg` +trait. The property's test runs it on `ZSet`. A companion runs it on `Model(Fault::None)`, a +second implementation over a sorted vector, so the checker is shown not to reject a correct +implementation that is not `ZSet`. Each rival is `Model(Fault::X)`, run through the same +checker with a deterministic seed, and the failure message must carry the property's tag +(`[inverse]`, `[map]`, ..). A rival that fails for another reason does not count. The group +laws, canonical form, scalar distributivity, the `map` homomorphism, `filter` linearity, +`distinct`'s definition, iteration order, the clause 9 correction identity and the +`integrate`/`differentiate` inverses are all properties; each runs at the default 256 cases +over keys from a range of six, so collisions and cancelling pairs are the common case. +Weights come from `-3..=3`, an explicit zero, and `±2^40`, so sums of three cannot wrap. + +The overflow policy is not a property over the generators (they cannot reach it by design) +and is tested by example in `src/lib.rs`, with `should_panic(expected = ..)`. diff --git a/context/test-evidence/zset.md b/context/test-evidence/zset.md new file mode 100644 index 00000000..986647cb --- /dev/null +++ b/context/test-evidence/zset.md @@ -0,0 +1,227 @@ +# Test evidence: `zset` + +What each test guards, which rival it was run against, and where that rival failed. The +entries are keyed by exact test name, and a rename orphans its entry, which +`scripts/check-comment-runs.py --check-evidence` catches. The reasoning these tests defend +is in `context/code/zset.md`. The decisions are ADR 009 clause 1's. + +**How the rivals are kept.** Every property in `crates/zset/tests/properties.rs` is a +checker that takes the implementation as a parameter (the `Alg` trait). The property's own +test runs it on `ZSet`. A `_holds_on_the_model` test runs it on `Model(Fault::None)`, +a second, correct implementation over a sorted vector, so a checker that rejects every +implementation but `ZSet` is seen. A `_catches_` test runs the same checker +on a `Model` with one injected fault, with a deterministic seed, and asserts two things: +- the run fails; +- the failure message carries **the property's own tag**, so a rival that fails in setup, + panics, or fails some other property does not count. + +So each rival is watched failing on every run of the suite, not once by hand. + +**Injected in the source.** Eight faults were also put into `crates/zset/src/lib.rs` one at +a time, each run against the whole suite, each reverted and followed by a full rerun. The +failing tests, by name: +- `insert` stores a zero weight: `addition_is_associative`, `equal_sets_compare_equal`, + `held_plus_target_minus_held_is_target`, `integrate_and_differentiate_invert_each_other`, + `iteration_is_ascending_and_independent_of_insertion_order`, `map_is_a_homomorphism`, + `no_zero_weight_is_ever_stored`, `scalar_multiplication_distributes`; +- an `insert` that stores the sum without removing a zero one also fails + `addition_is_commutative`, `every_set_has_an_inverse` and `zero_is_the_identity`; +- `neg` skips its first key: `every_set_has_an_inverse`, `filter_is_linear`, + `map_is_a_homomorphism`, `scalar_multiplication_distributes`, + `subtraction_is_adding_the_negation`; +- `map` overwrites: `map_is_a_homomorphism`; +- `distinct` does not clamp: `distinct_clamps_positive_weights_to_one`; +- `filter` also reads the weight: `filter_is_linear`; +- `sub` flipped: `held_plus_target_minus_held_is_target`, + `integrate_and_differentiate_invert_each_other`, `subtraction_is_adding_the_negation`; +- `integrate` excludes the current delta: `integrate_and_differentiate_invert_each_other`. + +The unit tests in `src/lib.rs` (the zero-weight, `map`, `distinct` and differentiate examples +and the five overflow tests) also failed under the faults they cover. They are examples, so +they carry no entry of their own. + +**Overflow is tested by example**, not by property: the generators cannot reach it (sums of +three weights stay below 2^43). The `should_panic` tests assert the message names the +operation, so a panic from somewhere else does not pass them. + +## `crates/zset/tests/properties.rs` + +### addition_is_associative + +(a + b) + c = a + (b + c) over three independently generated sets. Tag: `[associativity]`. + +### associativity_holds_on_the_model + +The same checker on the correct second implementation. It passes; it exists to show the checker is not specific to `ZSet`. + +### associativity_catches_an_add_that_clamps_weights + +`add` clamps every result weight to +-10. A clamp is a saturating add, which is not associative: `10 + 10 + (-10)` is 0 one way and 10 the other. The weights near +-3 and +-2^40 reach it at once. + +### addition_is_commutative + +a + b = b + a. Tag: `[commutativity]`. + +### commutativity_holds_on_the_model + +The same checker on the correct second implementation. It passes; it exists to show the checker is not specific to `ZSet`. + +### commutativity_catches_an_add_that_keeps_the_left_weight + +`add` is a left-biased union: a key present on both sides keeps the left weight. It is associative, so it escaped `associativity` when first tried there (the run reported the rival not caught, which is the failure the `_catches_` shape exists to make loud), and the rival moved. It is caught here. + +### zero_is_the_identity + +a + 0 = a and 0 + a = a, with zero built by `build(&[])`, the empty iterator, not by a constructor the rival could share. Tag: `[identity]`. + +### identity_holds_on_the_model + +The same checker on the correct second implementation. It passes; it exists to show the checker is not specific to `ZSet`. + +### identity_catches_an_add_that_keeps_only_shared_keys + +`add` keeps only keys present on both sides. Then `a + 0` is empty, not `a`. The first rival tried here, an add that keeps zero weights, passes `identity` (a canonical `a` has none to keep), so it was replaced; keeping zeros is caught by `every_set_has_an_inverse` and `no_zero_weight_is_ever_stored`. + +### every_set_has_an_inverse + +a + (-a) = 0, a - a = 0 and --a = a. The sets include cancelling pairs and colliding keys. Tag: `[inverse]`. + +### inverse_holds_on_the_model + +The same checker on the correct second implementation. It passes; it exists to show the checker is not specific to `ZSet`. + +### inverse_catches_an_add_that_keeps_zero_weights + +`add` and construction leave a key with weight 0 in the map. `a + (-a)` is then a map of zeros, not the empty one, and the equality says so. + +### inverse_catches_a_neg_that_forgets_a_key + +`neg` skips the first key. `a + (-a)` keeps that key. + +### subtraction_is_adding_the_negation + +a - b = a + (-b). Tag: `[subtraction]`. + +### subtraction_holds_on_the_model + +The same checker on the correct second implementation. It passes; it exists to show the checker is not specific to `ZSet`. + +### subtraction_catches_a_flipped_sub + +`sub(a, b)` computes `b - a`. + +### no_zero_weight_is_ever_stored + +After construction, `+`, `-`, unary `-`, `scale` (including by zero), `map`, `filter` and `distinct`, no stored weight is zero. It reads what the iterator yields, so a rival that hides a zero from the equality is still seen. Tag: `[canonical-zero]`. + +### canonical_zero_holds_on_the_model + +The same checker on the correct second implementation. It passes; it exists to show the checker is not specific to `ZSet`. + +### canonical_zero_catches_an_add_that_keeps_zero_weights + +`add` and construction keep zero weights. + +### equal_sets_compare_equal + +The same pairs in another order, and with a cancelling pair spliced in, build equal sets. Tag: `[canonical-equality]`. + +### canonical_equality_holds_on_the_model + +The same checker on the correct second implementation. It passes; it exists to show the checker is not specific to `ZSet`. + +### canonical_equality_catches_an_add_that_keeps_zero_weights + +The spliced pair `(9, 5), (9, -5)` leaves a stored `(9, 0)`, so the set is no longer equal to the one without it. + +### scalar_multiplication_distributes + +(a + b) * n = a*n + b*n, a*(m + n) = a*m + a*n, a * -1 = -a, a * 1 = a, a * 0 = 0. Tag: `[scale]`. + +### scale_holds_on_the_model + +The same checker on the correct second implementation. It passes; it exists to show the checker is not specific to `ZSet`. + +### scale_catches_a_scale_that_takes_the_absolute_value + +`scale` multiplies by `|n|`. `a*(m+n)` differs from `a*m + a*n` as soon as `m` and `n` have different signs, and `a * -1` is `a`. + +### scale_catches_a_scale_by_zero_that_keeps_zero_weights + +`scale(a, 0)` keeps every key at weight 0. + +### map_is_a_homomorphism + +map(a + b) = map(a) + map(b) and map(-a) = -map(a), with images `k % m`, so keys collide (m from 1 to 4). Tag: `[map]`. + +### map_holds_on_the_model + +The same checker on the correct second implementation. It passes; it exists to show the checker is not specific to `ZSet`. + +### map_catches_a_map_that_overwrites_colliding_keys + +`map` inserts each image with `=`, so the last of several colliding keys wins instead of the weights summing. + +### filter_is_linear + +filter(a + b) = filter(a) + filter(b) and filter(-a) = -filter(a). The predicate reads the key only. Tag: `[filter]`. + +### filter_holds_on_the_model + +The same checker on the correct second implementation. It passes; it exists to show the checker is not specific to `ZSet`. + +### filter_catches_a_filter_that_reads_the_weight + +`filter` also requires a positive weight. That is not linear: a negated set loses everything, and a key whose weights cancel in `a + b` is judged on the sum. + +### distinct_clamps_positive_weights_to_one + +`distinct(a)` is exactly the keys with a positive weight, each at weight 1, in the same order; and it is idempotent. Tag: `[distinct]`. + +### distinct_holds_on_the_model + +The same checker on the correct second implementation. It passes; it exists to show the checker is not specific to `ZSet`. + +### distinct_catches_a_distinct_without_clamping + +`distinct` keeps the positive keys at their own weight. + +### iteration_is_ascending_and_independent_of_insertion_order + +Iteration is strictly ascending by key, and the same pairs inserted in another order iterate identically. Tag: `[order]`. + +### order_holds_on_the_model + +The same checker on the correct second implementation. It passes; it exists to show the checker is not specific to `ZSet`. + +### order_catches_insertion_order_iteration + +The rival stores keys in first-seen order. Its equality compares sorted copies, so every group law passes on it, and only this property sees the order. + +### held_plus_target_minus_held_is_target + +ADR 009 clause 9: `held + (target - held) = target`, and correcting a state that is already correct is the zero Z-set. Tag: `[correction]`. + +### correction_holds_on_the_model + +The same checker on the correct second implementation. It passes; it exists to show the checker is not specific to `ZSet`. + +### correction_catches_a_flipped_sub + +`sub(a, b)` computes `b - a`, so the correction applied to `held` gives `2*held - target`. + +### integrate_and_differentiate_invert_each_other + +`integrate` gives the running sums, `differentiate(integrate(d)) = d` and `integrate(differentiate(s)) = s`, element by element, including the empty stream. Tag: `[stream]`. + +### stream_holds_on_the_model + +The same checker on the correct second implementation. It passes; it exists to show the checker is not specific to `ZSet`. + +### stream_catches_an_integrate_that_excludes_the_current_delta + +Element `i` is the sum of the deltas before `i`, so the stream is shifted by one. + +### stream_catches_a_differentiate_that_drops_the_first_state + +Element 0 is zero instead of `s_0`. diff --git a/crates/zset/src/lib.rs b/crates/zset/src/lib.rs index bb28430a..38825939 100644 --- a/crates/zset/src/lib.rs +++ b/crates/zset/src/lib.rs @@ -1,19 +1,13 @@ -//! Z-sets: finite maps from keys to non-zero `i64` weights, forming an abelian group -//! under pointwise addition (ADR 009 clause 1). -//! -//! Reasoning, the interpretations the ADR left open and the overflow policy are in -//! `context/code/zset.md`. Evidence for each test is in `context/test-evidence/zset.md`. +//! Z-sets: maps from keys to non-zero `i64` weights, an abelian group (ADR 009 clause 1). +//! Reasoning and the overflow policy: `context/code/zset.md`. use std::collections::BTreeMap; use std::collections::btree_map::Entry; use std::iter::FromIterator; use std::ops::{Add, AddAssign, Mul, Neg, Sub, SubAssign}; -/// A map from `K` to a non-zero `i64` weight. -/// -/// The representation is canonical: a key with weight zero is never stored, so two -/// Z-sets are `==` exactly when they assign every key the same weight. Iteration is in -/// ascending key order. +/// A map from `K` to a non-zero `i64` weight. A zero weight is never stored, so `==` +/// is the group's equality; iteration is in ascending key order. #[derive(Clone, Debug, PartialEq, Eq, Hash, PartialOrd, Ord)] pub struct ZSet { weights: BTreeMap, @@ -66,6 +60,10 @@ impl ZSet { self.weights.is_empty() } + pub fn is_empty(&self) -> bool { + self.is_zero() + } + /// The number of keys with a non-zero weight. pub fn len(&self) -> usize { self.weights.len() @@ -76,9 +74,7 @@ impl ZSet { self.weights.iter().map(|(k, w)| (k, *w)) } - /// Adds `weight` to `key`'s weight, dropping the key if the sum is zero. - /// - /// Panics if the sum does not fit an `i64`. + /// Adds `weight` to `key`'s, dropping the key at zero. Panics on `i64` overflow. pub fn insert(&mut self, key: K, weight: i64) { match self.weights.entry(key) { Entry::Vacant(e) => { @@ -131,9 +127,7 @@ impl ZSet { .collect() } - /// Every weight times `n`; zero gives the zero Z-set. - /// - /// Panics if a product does not fit an `i64`. + /// Every weight times `n`; zero gives the zero Z-set. Panics on `i64` overflow. pub fn scale(&self, n: i64) -> Self where K: Clone, diff --git a/crates/zset/tests/properties.rs b/crates/zset/tests/properties.rs index beaafa56..25b35cfe 100644 --- a/crates/zset/tests/properties.rs +++ b/crates/zset/tests/properties.rs @@ -1,7 +1,5 @@ -//! Property tests for `zset`. Each property is a checker that takes the implementation as -//! a parameter: the property's own test runs it on `ZSet`, and a `_catches_` companion runs -//! the same checker on a rival with one injected fault and requires that the failure carry -//! the property's tag. The evidence is in `context/test-evidence/zset.md`. +//! Property checkers over an `Alg`; each runs on `ZSet`, and on rivals (`_catches_`). +//! Evidence: `context/test-evidence/zset.md`. use proptest::prelude::*; use proptest::test_runner::{TestError, TestRunner}; @@ -12,7 +10,7 @@ type Pairs = Vec<(u8, i64)>; /// The operations under test, over a representation the implementation chooses. trait Alg { type Z: Clone + std::fmt::Debug; - fn from_pairs(&self, p: &[(u8, i64)]) -> Self::Z; + fn build(&self, p: &[(u8, i64)]) -> Self::Z; fn add(&self, a: &Self::Z, b: &Self::Z) -> Self::Z; fn neg(&self, a: &Self::Z) -> Self::Z; fn sub(&self, a: &Self::Z, b: &Self::Z) -> Self::Z; @@ -29,7 +27,7 @@ trait Alg { /// Whether two values are the same set of weights, however each is stored. fn same(&self, a: &Self::Z, b: &Self::Z) -> bool; fn zero(&self) -> Self::Z { - self.from_pairs(&[]) + self.build(&[]) } } @@ -37,7 +35,7 @@ struct Real; impl Alg for Real { type Z = ZSet; - fn from_pairs(&self, p: &[(u8, i64)]) -> ZSet { + fn build(&self, p: &[(u8, i64)]) -> ZSet { p.iter().copied().collect() } fn add(&self, a: &ZSet, b: &ZSet) -> ZSet { @@ -119,7 +117,7 @@ impl Model { impl Alg for Model { type Z = V; - fn from_pairs(&self, p: &[(u8, i64)]) -> V { + fn build(&self, p: &[(u8, i64)]) -> V { self.normal(p.to_vec()) } fn add(&self, a: &V, b: &V) -> V { @@ -139,7 +137,10 @@ impl Alg for Model { } let sum = self.normal(a.iter().chain(b).copied().collect()); if self.0 == Fault::AddClamps { - return sum.into_iter().map(|(k, w)| (k, w.clamp(-10, 10))).collect(); + return sum + .into_iter() + .map(|(k, w)| (k, w.clamp(-10, 10))) + .collect(); } sum } @@ -148,11 +149,19 @@ impl Alg for Model { self.normal(a.iter().skip(skip).map(|(k, w)| (*k, -w)).collect()) } fn sub(&self, a: &V, b: &V) -> V { - let (x, y) = if self.0 == Fault::SubFlipped { (b, a) } else { (a, b) }; + let (x, y) = if self.0 == Fault::SubFlipped { + (b, a) + } else { + (a, b) + }; self.add(x, &self.neg(y)) } fn scale(&self, a: &V, n: i64) -> V { - let n = if self.0 == Fault::ScaleAbs { n.abs() } else { n }; + let n = if self.0 == Fault::ScaleAbs { + n.abs() + } else { + n + }; self.normal(a.iter().map(|(k, w)| (*k, w * n)).collect()) } fn map(&self, a: &V, m: u8) -> V { @@ -176,7 +185,11 @@ impl Alg for Model { ) } fn distinct(&self, a: &V) -> V { - let clamp = if self.0 == Fault::DistinctNoClamp { None } else { Some(1) }; + let clamp = if self.0 == Fault::DistinctNoClamp { + None + } else { + Some(1) + }; self.normal( a.iter() .filter(|(_, w)| *w > 0) @@ -203,7 +216,11 @@ impl Alg for Model { let mut out = Vec::new(); for (i, x) in s.iter().enumerate() { let d = self.sub(x, &prev); - out.push(if i == 0 && self.0 == Fault::DifferentiateDropsFirst { self.zero() } else { d }); + out.push(if i == 0 && self.0 == Fault::DifferentiateDropsFirst { + self.zero() + } else { + d + }); prev = x.clone(); } out @@ -266,47 +283,71 @@ where } fn associativity(x: &A, (a, b, c): &(Pairs, Pairs, Pairs)) -> Result<(), TestCaseError> { - let (a, b, c) = (x.from_pairs(a), x.from_pairs(b), x.from_pairs(c)); + let (a, b, c) = (x.build(a), x.build(b), x.build(c)); let left = x.add(&x.add(&a, &b), &c); let right = x.add(&a, &x.add(&b, &c)); - prop_assert!(x.same(&left, &right), "[associativity] {left:?} != {right:?}"); + prop_assert!( + x.same(&left, &right), + "[associativity] {left:?} != {right:?}" + ); Ok(()) } fn commutativity(x: &A, (a, b): &(Pairs, Pairs)) -> Result<(), TestCaseError> { - let (a, b) = (x.from_pairs(a), x.from_pairs(b)); + let (a, b) = (x.build(a), x.build(b)); let (ab, ba) = (x.add(&a, &b), x.add(&b, &a)); prop_assert!(x.same(&ab, &ba), "[commutativity] {ab:?} != {ba:?}"); Ok(()) } fn identity(x: &A, a: &Pairs) -> Result<(), TestCaseError> { - let a = x.from_pairs(a); + let a = x.build(a); let zero = x.zero(); - prop_assert!(x.same(&x.add(&a, &zero), &a), "[identity] a + 0 != a for {a:?}"); - prop_assert!(x.same(&x.add(&zero, &a), &a), "[identity] 0 + a != a for {a:?}"); + prop_assert!( + x.same(&x.add(&a, &zero), &a), + "[identity] a + 0 != a for {a:?}" + ); + prop_assert!( + x.same(&x.add(&zero, &a), &a), + "[identity] 0 + a != a for {a:?}" + ); Ok(()) } fn inverse(x: &A, a: &Pairs) -> Result<(), TestCaseError> { - let a = x.from_pairs(a); + let a = x.build(a); let sum = x.add(&a, &x.neg(&a)); - prop_assert!(x.same(&sum, &x.zero()), "[inverse] a + (-a) = {sum:?} for {a:?}"); + prop_assert!( + x.same(&sum, &x.zero()), + "[inverse] a + (-a) = {sum:?} for {a:?}" + ); let diff = x.sub(&a, &a); - prop_assert!(x.same(&diff, &x.zero()), "[inverse] a - a = {diff:?} for {a:?}"); - prop_assert!(x.same(&x.neg(&x.neg(&a)), &a), "[inverse] --a != a for {a:?}"); + prop_assert!( + x.same(&diff, &x.zero()), + "[inverse] a - a = {diff:?} for {a:?}" + ); + prop_assert!( + x.same(&x.neg(&x.neg(&a)), &a), + "[inverse] --a != a for {a:?}" + ); Ok(()) } fn subtraction(x: &A, (a, b): &(Pairs, Pairs)) -> Result<(), TestCaseError> { - let (a, b) = (x.from_pairs(a), x.from_pairs(b)); + let (a, b) = (x.build(a), x.build(b)); let (d, e) = (x.sub(&a, &b), x.add(&a, &x.neg(&b))); - prop_assert!(x.same(&d, &e), "[subtraction] a - b = {d:?} but a + (-b) = {e:?}"); + prop_assert!( + x.same(&d, &e), + "[subtraction] a - b = {d:?} but a + (-b) = {e:?}" + ); Ok(()) } -fn canonical_zero(x: &A, (a, b, n, m): &(Pairs, Pairs, i64, u8)) -> Result<(), TestCaseError> { - let (a, b) = (x.from_pairs(a), x.from_pairs(b)); +fn canonical_zero( + x: &A, + (a, b, n, m): &(Pairs, Pairs, i64, u8), +) -> Result<(), TestCaseError> { + let (a, b) = (x.build(a), x.build(b)); let made = [ a.clone(), x.add(&a, &b), @@ -321,7 +362,10 @@ fn canonical_zero(x: &A, (a, b, n, m): &(Pairs, Pairs, i64, u8)) -> Resu ]; for z in &made { let zeros: Vec<_> = x.stored(z).into_iter().filter(|(_, w)| *w == 0).collect(); - prop_assert!(zeros.is_empty(), "[canonical-zero] stored zero weights {zeros:?} in {z:?}"); + prop_assert!( + zeros.is_empty(), + "[canonical-zero] stored zero weights {zeros:?} in {z:?}" + ); } Ok(()) } @@ -333,14 +377,17 @@ fn canonical_equality(x: &A, (p, seed): &(Pairs, usize)) -> Result<(), T shuffled.rotate_left(seed % n); shuffled.reverse(); } - let (a, b) = (x.from_pairs(p), x.from_pairs(&shuffled)); + let (a, b) = (x.build(p), x.build(&shuffled)); prop_assert!(x.same(&a, &b), "[canonical-equality] {a:?} != {b:?}"); // The same set built in two steps, with a cancelling pair spliced in. let mut padded = p.clone(); padded.push((9, 5)); padded.push((9, -5)); - let c = x.from_pairs(&padded); - prop_assert!(x.same(&a, &c), "[canonical-equality] a cancelled pair changed {a:?} into {c:?}"); + let c = x.build(&padded); + prop_assert!( + x.same(&a, &c), + "[canonical-equality] a cancelled pair changed {a:?} into {c:?}" + ); Ok(()) } @@ -348,50 +395,91 @@ fn scalar_multiplication( x: &A, (a, b, m, n): &(Pairs, Pairs, i64, i64), ) -> Result<(), TestCaseError> { - let (a, b) = (x.from_pairs(a), x.from_pairs(b)); - let (l, r) = (x.scale(&x.add(&a, &b), *n), x.add(&x.scale(&a, *n), &x.scale(&b, *n))); - prop_assert!(x.same(&l, &r), "[scale] (a+b)*n = {l:?} but a*n + b*n = {r:?}"); + let (a, b) = (x.build(a), x.build(b)); + let (l, r) = ( + x.scale(&x.add(&a, &b), *n), + x.add(&x.scale(&a, *n), &x.scale(&b, *n)), + ); + prop_assert!( + x.same(&l, &r), + "[scale] (a+b)*n = {l:?} but a*n + b*n = {r:?}" + ); // The scalar side: (m + n) * a, with m, n small enough that m + n cannot wrap. - let (l, r) = (x.scale(&a, m + n), x.add(&x.scale(&a, *m), &x.scale(&a, *n))); - prop_assert!(x.same(&l, &r), "[scale] a*(m+n) = {l:?} but a*m + a*n = {r:?}"); - prop_assert!(x.same(&x.scale(&a, -1), &x.neg(&a)), "[scale] a * -1 != -a for {a:?}"); + let (l, r) = ( + x.scale(&a, m + n), + x.add(&x.scale(&a, *m), &x.scale(&a, *n)), + ); + prop_assert!( + x.same(&l, &r), + "[scale] a*(m+n) = {l:?} but a*m + a*n = {r:?}" + ); + prop_assert!( + x.same(&x.scale(&a, -1), &x.neg(&a)), + "[scale] a * -1 != -a for {a:?}" + ); prop_assert!(x.same(&x.scale(&a, 1), &a), "[scale] a * 1 != a for {a:?}"); - prop_assert!(x.same(&x.scale(&a, 0), &x.zero()), "[scale] a * 0 != zero for {a:?}"); + prop_assert!( + x.same(&x.scale(&a, 0), &x.zero()), + "[scale] a * 0 != zero for {a:?}" + ); Ok(()) } fn map_homomorphism(x: &A, (a, b, m): &(Pairs, Pairs, u8)) -> Result<(), TestCaseError> { - let (a, b) = (x.from_pairs(a), x.from_pairs(b)); - let (l, r) = (x.map(&x.add(&a, &b), *m), x.add(&x.map(&a, *m), &x.map(&b, *m))); - prop_assert!(x.same(&l, &r), "[map] map(a+b) = {l:?} but map(a)+map(b) = {r:?}"); + let (a, b) = (x.build(a), x.build(b)); + let (l, r) = ( + x.map(&x.add(&a, &b), *m), + x.add(&x.map(&a, *m), &x.map(&b, *m)), + ); + prop_assert!( + x.same(&l, &r), + "[map] map(a+b) = {l:?} but map(a)+map(b) = {r:?}" + ); let (l, r) = (x.map(&x.neg(&a), *m), x.neg(&x.map(&a, *m))); prop_assert!(x.same(&l, &r), "[map] map(-a) = {l:?} but -map(a) = {r:?}"); Ok(()) } fn filter_linearity(x: &A, (a, b, d): &(Pairs, Pairs, u8)) -> Result<(), TestCaseError> { - let (a, b) = (x.from_pairs(a), x.from_pairs(b)); - let (l, r) = (x.filter(&x.add(&a, &b), *d), x.add(&x.filter(&a, *d), &x.filter(&b, *d))); - prop_assert!(x.same(&l, &r), "[filter] filter(a+b) = {l:?} but filter(a)+filter(b) = {r:?}"); + let (a, b) = (x.build(a), x.build(b)); + let (l, r) = ( + x.filter(&x.add(&a, &b), *d), + x.add(&x.filter(&a, *d), &x.filter(&b, *d)), + ); + prop_assert!( + x.same(&l, &r), + "[filter] filter(a+b) = {l:?} but filter(a)+filter(b) = {r:?}" + ); let (l, r) = (x.filter(&x.neg(&a), *d), x.neg(&x.filter(&a, *d))); - prop_assert!(x.same(&l, &r), "[filter] filter(-a) = {l:?} but -filter(a) = {r:?}"); + prop_assert!( + x.same(&l, &r), + "[filter] filter(-a) = {l:?} but -filter(a) = {r:?}" + ); Ok(()) } fn distinct_semantics(x: &A, a: &Pairs) -> Result<(), TestCaseError> { - let a = x.from_pairs(a); + let a = x.build(a); let d = x.distinct(&a); - let expected: Vec<_> = x.stored(&a).into_iter().filter(|(_, w)| *w > 0).map(|(k, _)| (k, 1)).collect(); + let expected: Vec<_> = x + .stored(&a) + .into_iter() + .filter(|(_, w)| *w > 0) + .map(|(k, _)| (k, 1)) + .collect(); prop_assert!( x.stored(&d) == expected, "[distinct] distinct({a:?}) = {d:?}, expected weight 1 on exactly the positive keys" ); - prop_assert!(x.same(&x.distinct(&d), &d), "[distinct] not idempotent on {a:?}"); + prop_assert!( + x.same(&x.distinct(&d), &d), + "[distinct] not idempotent on {a:?}" + ); Ok(()) } fn iteration_order(x: &A, (p, seed): &(Pairs, usize)) -> Result<(), TestCaseError> { - let a = x.from_pairs(p); + let a = x.build(p); let order = x.stored(&a); prop_assert!( order.windows(2).all(|w| w[0].0 < w[1].0), @@ -403,39 +491,66 @@ fn iteration_order(x: &A, (p, seed): &(Pairs, usize)) -> Result<(), Test shuffled.rotate_left(seed % n); shuffled.reverse(); } - let again = x.stored(&x.from_pairs(&shuffled)); - prop_assert!(order == again, "[order] insertion order shows through: {order:?} vs {again:?}"); + let again = x.stored(&x.build(&shuffled)); + prop_assert!( + order == again, + "[order] insertion order shows through: {order:?} vs {again:?}" + ); Ok(()) } fn correction(x: &A, (held, target): &(Pairs, Pairs)) -> Result<(), TestCaseError> { - let (held, target) = (x.from_pairs(held), x.from_pairs(target)); + let (held, target) = (x.build(held), x.build(target)); let delta = x.sub(&target, &held); let got = x.add(&held, &delta); - prop_assert!(x.same(&got, &target), "[correction] held + (target - held) = {got:?}, not {target:?}"); + prop_assert!( + x.same(&got, &target), + "[correction] held + (target - held) = {got:?}, not {target:?}" + ); let nothing = x.sub(&target, &target); - prop_assert!(x.same(¬hing, &x.zero()), "[correction] a correct state needs {nothing:?}"); + prop_assert!( + x.same(¬hing, &x.zero()), + "[correction] a correct state needs {nothing:?}" + ); Ok(()) } -fn streams(x: &A, s: &Vec) -> Result<(), TestCaseError> { - let deltas: Vec<_> = s.iter().map(|p| x.from_pairs(p)).collect(); +fn streams(x: &A, s: &[Pairs]) -> Result<(), TestCaseError> { + let deltas: Vec<_> = s.iter().map(|p| x.build(p)).collect(); let states = x.integrate(&deltas); - prop_assert!(states.len() == deltas.len(), "[stream] integrate changed the length"); + prop_assert!( + states.len() == deltas.len(), + "[stream] integrate changed the length" + ); let mut running = x.zero(); for (i, d) in deltas.iter().enumerate() { running = x.add(&running, d); - prop_assert!(x.same(&states[i], &running), "[stream] integrate[{i}] = {:?}, not {running:?}", states[i]); + prop_assert!( + x.same(&states[i], &running), + "[stream] integrate[{i}] = {:?}, not {running:?}", + states[i] + ); } let back = x.differentiate(&states); - prop_assert!(back.len() == deltas.len(), "[stream] differentiate changed the length"); + prop_assert!( + back.len() == deltas.len(), + "[stream] differentiate changed the length" + ); for (i, d) in deltas.iter().enumerate() { - prop_assert!(x.same(&back[i], d), "[stream] differentiate(integrate(d))[{i}] = {:?}, not {d:?}", back[i]); + prop_assert!( + x.same(&back[i], d), + "[stream] differentiate(integrate(d))[{i}] = {:?}, not {d:?}", + back[i] + ); } // The other direction, from arbitrary states. let again = x.integrate(&x.differentiate(&deltas)); for (i, d) in deltas.iter().enumerate() { - prop_assert!(x.same(&again[i], d), "[stream] integrate(differentiate(s))[{i}] = {:?}, not {d:?}", again[i]); + prop_assert!( + x.same(&again[i], d), + "[stream] integrate(differentiate(s))[{i}] = {:?}, not {d:?}", + again[i] + ); } Ok(()) } diff --git a/nix/ci.nix b/nix/ci.nix index f8a56de9..3a35eb86 100644 --- a/nix/ci.nix +++ b/nix/ci.nix @@ -48,6 +48,8 @@ "improvise-gp" # ADR 005 clause 14: nothing depends on it yet, and improvise-core will. "numtower" + # ADR 009 clause 1: std-only; nothing depends on it yet. + "zset" ]; pFlags = crates: lib.concatMapStringsSep " " (c: "-p ${c}") crates; diff --git a/scripts/build-doc-site.mjs b/scripts/build-doc-site.mjs index f8489795..0ccf5cc6 100644 --- a/scripts/build-doc-site.mjs +++ b/scripts/build-doc-site.mjs @@ -68,6 +68,7 @@ const SECTIONS = [ ["context/code/cli.md", "code/cli", "The headless CLI"], ["context/code/gp.md", "code/gp", "gp-tree and improvise-gp"], ["context/code/numtower.md", "code/numtower", "numtower, the numeric tower"], + ["context/code/zset.md", "code/zset", "zset, the Z-set group"], ["context/code/kb-tool.md", "code/kb-tool", "The kb tool"], ["context/code/tooling.md", "code/tooling", "The repository's own checkers"], ], @@ -87,6 +88,7 @@ const SECTIONS = [ ["context/test-evidence/cli.md", "test-evidence/cli", "The headless CLI"], ["context/test-evidence/gp.md", "test-evidence/gp", "gp-tree and improvise-gp"], ["context/test-evidence/numtower.md", "test-evidence/numtower", "numtower"], + ["context/test-evidence/zset.md", "test-evidence/zset", "zset"], ["context/test-evidence/tooling.md", "test-evidence/tooling", "The repository's own gates"], ["context/test-evidence/layout-cost.md", "test-evidence/layout-cost", "Layout and keypress cost"], ["context/test-evidence/scale-bisect.md", "test-evidence/scale-bisect", "Scale bisect"], From 069d56bd9f15cd66561b7cb8e0ae49223c638449 Mon Sep 17 00:00:00 2001 From: "Claude (adr009-zset)" Date: Fri, 9 Oct 2026 23:40:15 -0700 Subject: [PATCH 3/8] fix(zset): a - a is zero at i64::MIN, and the partial group is stated (improvise-tk51) Answers Copilot (SubAssign negated before consulting the held weight) and Codex (checked arithmetic makes associativity order-dependent at the i64 boundary; documented as the intended policy and pinned by a test). Co-Authored-By: Claude Sonnet 5.5 Claude-Session: https://claude.ai/code/session_01VdfEGXA7aJ6ftMsCc9PJze --- context/code/zset.md | 26 +++++++++++++---- context/test-evidence/zset.md | 25 +++++++++++++++- crates/zset/src/lib.rs | 55 +++++++++++++++++++++++++++++++---- 3 files changed, 93 insertions(+), 13 deletions(-) diff --git a/context/code/zset.md b/context/code/zset.md index 76df1f00..37c78fa1 100644 --- a/context/code/zset.md +++ b/context/code/zset.md @@ -10,7 +10,7 @@ evidence for each test is in `context/test-evidence/zset.md`. | item | what it is | |---|---| -| `ZSet` | a map from `K` to a non-zero `i64` weight; an abelian group | +| `ZSet` | a map from `K` to a non-zero `i64` weight; an abelian group within `i64` (interpretation 5) | | `+`, `-`, unary `-`, `* i64`, `scale` | the group operations and scalar multiplication | | `new`, `singleton`, `insert`, `FromIterator`, `Extend` | construction; weights of equal keys sum | | `weight`, `is_zero`, `len`, `iter`, `IntoIterator` | reads; iteration is ascending by key | @@ -63,11 +63,25 @@ These are the readings this step takes. to show it, which is the failure the ADR's exactness argument is against. So every weight operation uses `checked_*` and **panics** with `zset: weight overflow in `, in debug and in release (`checked_*` does not depend on `overflow-checks`). The operations are - `add` (including `insert`, `Extend`, `FromIterator`), `neg` (so `i64::MIN` panics) and - `scale`. Scaling by zero cannot overflow and returns the zero Z-set. A panic, not a - `Result`: `Result` does not belong in the majority of the code (`AGENTS.md`), and a weight - near `i64::MAX` is a defect in the caller, not an input to recover from. The weights - clause 3 produces are small (one per cell). + `add` (including `insert`, `Extend`, `FromIterator`), `sub`, `neg` (so `i64::MIN` panics + when it has to be negated) and `scale`. Scaling by zero cannot overflow and returns the + zero Z-set. A panic, not a `Result`: `Result` does not belong in the majority of the code + (`AGENTS.md`), and a weight near `i64::MAX` is a defect in the caller, not an input to + recover from. The weights clause 3 produces are small (one per cell). + + **The group is partial, and that is the stated reading.** The ADR calls a Z-set an abelian + group. With `i64` weights and no wrapping, the laws hold wherever no weight, intermediate + ones included, leaves `i64`; outside that, an operation panics rather than return a + different value. So associativity is order-dependent at the boundary: + `(MAX + 1) + (-1)` panics where `MAX + (1 + (-1))` is `MAX`. The result is never wrong, + only sometimes refused. Wrapping arithmetic would make the type a true group (the integers + mod 2^64) and give up exactly the property the ADR argues for in clause 8, that a + retraction cancels its insertion, since a wrapped weight is a different weight. A wider + weight (`i128`) moves the boundary and does not remove it. This is the one place the crate + departs from the ADR's wording. It is a ruling for the user, not for this step + (`overflow_depends_on_the_order_of_evaluation_and_never_gives_a_wrong_value` states it). + `sub` is checked directly against the held weight, so `a - a` is zero for every `a`, `i64::MIN` + included, and only an absent key's `0 - w` can overflow (`w` is `i64::MIN`). 6. **Stable error text.** The panic message names the operation and both operands, so a failure in a long-running host is diagnosable from the log. diff --git a/context/test-evidence/zset.md b/context/test-evidence/zset.md index 986647cb..b283d1e8 100644 --- a/context/test-evidence/zset.md +++ b/context/test-evidence/zset.md @@ -38,7 +38,7 @@ failing tests, by name: The unit tests in `src/lib.rs` (the zero-weight, `map`, `distinct` and differentiate examples and the five overflow tests) also failed under the faults they cover. They are examples, so -they carry no entry of their own. +they carry no entry of their own, except the three at the end, which answer review findings. **Overflow is tested by example**, not by property: the generators cannot reach it (sums of three weights stay below 2^43). The `should_panic` tests assert the message names the @@ -225,3 +225,26 @@ Element `i` is the sum of the deltas before `i`, so the stream is shifted by one ### stream_catches_a_differentiate_that_drops_the_first_state Element 0 is zero instead of `s_0`. + +## `crates/zset/src/lib.rs` + +### tests::subtracting_a_set_from_itself_at_i64_min_is_zero + +Found by Copilot on PR #341. `SubAssign` negated every right-hand weight before consulting +the left, so `a - a` panicked for a weight of `i64::MIN`, as did `differentiate` over two +equal states. **Reproduced before the fix**: the test failed at the `sub` call with +`weight overflow in neg`. The fix subtracts a held weight with `checked_sub` and negates only +the weight of an absent key. The test also checks the borrowed operator and `differentiate`. + +### tests::subtracting_i64_min_from_nothing_panics + +The control for the one above: `0 - i64::MIN` has no `i64` value, so it must still panic. A +fix that made `a - a` pass by swallowing the overflow would fail here. + +### tests::overflow_depends_on_the_order_of_evaluation_and_never_gives_a_wrong_value + +Found by ChatGPT Codex on PR #341: checked arithmetic makes the group partial, so +`(MAX + 1) + (-1)` panics where `MAX + (1 + (-1))` is `MAX`. The behaviour is the intended +policy, not a defect, and the test states it: one order gives the exact value, the other +panics, and neither gives a different number. The argument is in `context/code/zset.md`, +interpretation 5. A wrapping implementation would fail the `catch_unwind` half. diff --git a/crates/zset/src/lib.rs b/crates/zset/src/lib.rs index 38825939..7d4a20b4 100644 --- a/crates/zset/src/lib.rs +++ b/crates/zset/src/lib.rs @@ -1,5 +1,5 @@ -//! Z-sets: maps from keys to non-zero `i64` weights, an abelian group (ADR 009 clause 1). -//! Reasoning and the overflow policy: `context/code/zset.md`. +//! Z-sets: maps from keys to non-zero `i64` weights (ADR 009 clause 1). An abelian group +//! wherever no weight leaves `i64`; past that it panics. See `context/code/zset.md`. use std::collections::BTreeMap; use std::collections::btree_map::Entry; @@ -22,6 +22,10 @@ fn plus(a: i64, b: i64) -> i64 { a.checked_add(b).unwrap_or_else(|| overflow("add", a, b)) } +fn minus(a: i64, b: i64) -> i64 { + a.checked_sub(b).unwrap_or_else(|| overflow("sub", a, b)) +} + fn negated(a: i64) -> i64 { a.checked_neg().unwrap_or_else(|| overflow("neg", a, 0)) } @@ -76,14 +80,24 @@ impl ZSet { /// Adds `weight` to `key`'s, dropping the key at zero. Panics on `i64` overflow. pub fn insert(&mut self, key: K, weight: i64) { + self.adjust(key, weight, false); + } + + fn adjust(&mut self, key: K, weight: i64, subtract: bool) { match self.weights.entry(key) { Entry::Vacant(e) => { - if weight != 0 { - e.insert(weight); + let from_zero = if subtract { negated(weight) } else { weight }; + if from_zero != 0 { + e.insert(from_zero); } } Entry::Occupied(mut e) => { - let sum = plus(*e.get(), weight); + let held = *e.get(); + let sum = if subtract { + minus(held, weight) + } else { + plus(held, weight) + }; if sum == 0 { e.remove(); } else { @@ -241,7 +255,9 @@ impl Sub for &ZSet { impl SubAssign for ZSet { fn sub_assign(&mut self, other: Self) { - self.extend(other.into_iter().map(|(k, w)| (k, negated(w)))); + for (k, w) in other { + self.adjust(k, w, true); + } } } @@ -338,6 +354,33 @@ mod tests { let _ = ZSet::singleton(1, i64::MAX).scale(2); } + #[test] + fn subtracting_a_set_from_itself_at_i64_min_is_zero() { + let a = ZSet::singleton(1, i64::MIN); + assert!(a.clone().sub(a.clone()).is_zero()); + assert!((&a - &a).is_zero()); + assert!(differentiate(&[a.clone(), a]).pop().unwrap().is_zero()); + } + + #[test] + #[should_panic(expected = "weight overflow in neg")] + fn subtracting_i64_min_from_nothing_panics() { + let _ = ZSet::::new() - ZSet::singleton(1, i64::MIN); + } + + #[test] + fn overflow_depends_on_the_order_of_evaluation_and_never_gives_a_wrong_value() { + let (max, one, minus) = ( + ZSet::singleton(1, i64::MAX), + ZSet::singleton(1, 1), + ZSet::singleton(1, -1), + ); + let right = max.clone() + (one.clone() + minus.clone()); + assert_eq!(right, max); + let left = std::panic::catch_unwind(|| (max.clone() + one.clone()) + minus.clone()); + assert!(left.is_err()); + } + #[test] fn scaling_by_zero_never_overflows() { assert!(ZSet::singleton(1, i64::MAX).scale(0).is_zero()); From 6de889a1164836863a18471f94dd8f47afa83237 Mon Sep 17 00:00:00 2001 From: "Claude (adr009-zset)" Date: Fri, 9 Oct 2026 23:57:04 -0700 Subject: [PATCH 4/8] test(zset): reach the overflow branches of sub and scale, and correct the policy's reason (improvise-tk51) Adds sub and scale(-1) overflow examples and an i128-oracle property over near-limit weights; injecting wrapping_{add,sub,mul,neg} now fails named tests. context/code/zset.md no longer claims wrapping breaks retraction. Co-Authored-By: Claude Sonnet 5.5 Claude-Session: https://claude.ai/code/session_01VdfEGXA7aJ6ftMsCc9PJze --- context/code/zset.md | 19 +++++++++++++------ context/test-evidence/zset.md | 30 ++++++++++++++++++++++++++++++ crates/zset/src/lib.rs | 18 ++++++++++++++++++ crates/zset/tests/properties.rs | 32 ++++++++++++++++++++++++++++++++ 4 files changed, 93 insertions(+), 6 deletions(-) diff --git a/context/code/zset.md b/context/code/zset.md index 37c78fa1..46461e07 100644 --- a/context/code/zset.md +++ b/context/code/zset.md @@ -74,12 +74,19 @@ These are the readings this step takes. ones included, leaves `i64`; outside that, an operation panics rather than return a different value. So associativity is order-dependent at the boundary: `(MAX + 1) + (-1)` panics where `MAX + (1 + (-1))` is `MAX`. The result is never wrong, - only sometimes refused. Wrapping arithmetic would make the type a true group (the integers - mod 2^64) and give up exactly the property the ADR argues for in clause 8, that a - retraction cancels its insertion, since a wrapped weight is a different weight. A wider - weight (`i128`) moves the boundary and does not remove it. This is the one place the crate - departs from the ADR's wording. It is a ruling for the user, not for this step - (`overflow_depends_on_the_order_of_evaluation_and_never_gives_a_wrong_value` states it). + only sometimes refused. Wrapping arithmetic would make the type a true group (the integers mod 2^64), and + `(w + x) - x == w` would still hold exactly, so a retraction does cancel its insertion + under wrapping. (An earlier version of this paragraph said otherwise; that was wrong.) What + wrapping breaks is the intermediate reads. `MAX + 1` stores `i64::MIN`, so `distinct` + drops a key whose true weight is positive and `weight()` has the wrong sign. A true weight + of 2^64 stores as 0, so the key vanishes and `is_zero`, `len` and `==` report a set that + does not exist. Those are wrong answers returned silently, which is why the crate panics + instead. A wider weight (`i128`) moves the boundary and does not remove it. The ADR's + "abelian group" wording needs amending whichever policy is chosen: checked-and-panic gives + a group only within range, wrapping gives a group whose reads can be wrong, and `i128` is + partial too. Which one is a ruling for the user, not for this step; the crate currently + panics, and + `overflow_depends_on_the_order_of_evaluation_and_never_gives_a_wrong_value` states it. `sub` is checked directly against the held weight, so `a - a` is zero for every `a`, `i64::MIN` included, and only an absent key's `0 - w` can overflow (`w` is `i64::MIN`). 6. **Stable error text.** The panic message names the operation and both operands, so a diff --git a/context/test-evidence/zset.md b/context/test-evidence/zset.md index b283d1e8..c2890257 100644 --- a/context/test-evidence/zset.md +++ b/context/test-evidence/zset.md @@ -248,3 +248,33 @@ Found by ChatGPT Codex on PR #341: checked arithmetic makes the group partial, s policy, not a defect, and the test states it: one order gives the exact value, the other panics, and neither gives a different number. The argument is in `context/code/zset.md`, interpretation 5. A wrapping implementation would fail the `catch_unwind` half. + +### tests::subtracting_past_i64_max_panics + +Found by the Opus review of PR #341: `checked_sub` in `minus` could be replaced with +`wrapping_sub` and the suite stayed green, because no example reached `sub`'s overflow +branch. **Injected**: that replacement. These two (`..._max_` and `tests::subtracting_past_i64_min_panics`) +and `near_the_limit_an_operation_is_exact_or_it_panics` failed; the rest passed. Reverted, and +the suite rerun. + +### tests::subtracting_past_i64_min_panics + +The negative-side twin of the one above; it fails under the same injection. + +### tests::scaling_i64_min_by_minus_one_panics + +`i64::MIN * -1` is the one product of a small scalar that no generator reaches. **Injected**: +`checked_mul` replaced by `wrapping_mul`. This test, `tests::scaling_past_i64_panics` and +`near_the_limit_an_operation_is_exact_or_it_panics` failed. + +## `crates/zset/tests/properties.rs`: the boundary + +### near_the_limit_an_operation_is_exact_or_it_panics + +The other properties keep weights at +-2^40 so the laws can be tested without overflow, which +left the boundary to examples. This one draws weights from `MAX-3..=MAX`, `MIN..=MIN+3` and +`-3..=3`, and compares `+`, `-`, `scale` and unary `-` on a single key with an `i128` oracle: +the result must equal the exact value when it fits `i64`, and the operation must panic when it +does not. **Injected**, one at a time, `wrapping_add`, `wrapping_sub`, `wrapping_mul` and +`wrapping_neg` in place of the checked calls: this test failed under every one, and the +example tests named above failed under the matching one. diff --git a/crates/zset/src/lib.rs b/crates/zset/src/lib.rs index 7d4a20b4..8d60c65a 100644 --- a/crates/zset/src/lib.rs +++ b/crates/zset/src/lib.rs @@ -381,6 +381,24 @@ mod tests { assert!(left.is_err()); } + #[test] + #[should_panic(expected = "weight overflow in sub")] + fn subtracting_past_i64_max_panics() { + let _ = ZSet::singleton(1, i64::MAX) - ZSet::singleton(1, -1); + } + + #[test] + #[should_panic(expected = "weight overflow in sub")] + fn subtracting_past_i64_min_panics() { + let _ = ZSet::singleton(1, i64::MIN) - ZSet::singleton(1, 1); + } + + #[test] + #[should_panic(expected = "weight overflow in scale")] + fn scaling_i64_min_by_minus_one_panics() { + let _ = ZSet::singleton(1, i64::MIN).scale(-1); + } + #[test] fn scaling_by_zero_never_overflows() { assert!(ZSet::singleton(1, i64::MAX).scale(0).is_zero()); diff --git a/crates/zset/tests/properties.rs b/crates/zset/tests/properties.rs index 25b35cfe..f921f880 100644 --- a/crates/zset/tests/properties.rs +++ b/crates/zset/tests/properties.rs @@ -707,3 +707,35 @@ property!( IntegrateExcludesCurrent => stream_catches_an_integrate_that_excludes_the_current_delta, DifferentiateDropsFirst => stream_catches_a_differentiate_that_drops_the_first_state ); + +fn near_limit() -> impl Strategy { + prop_oneof![ + (0i64..4).prop_map(|d| i64::MAX - d), + (0i64..4).prop_map(|d| i64::MIN + d), + -3i64..=3, + ] +} + +fn probe(f: &dyn Fn() -> ZSet, wide: i128, what: &str) -> Result<(), TestCaseError> { + let got = std::panic::catch_unwind(std::panic::AssertUnwindSafe(f)); + match (i64::try_from(wide).ok(), got) { + (Some(w), Ok(z)) => prop_assert_eq!(z.weight(&1), w, "{} gave the wrong weight", what), + (None, Err(_)) => {} + (Some(_), Err(_)) => prop_assert!(false, "{} panicked within range", what), + (None, Ok(z)) => prop_assert!(false, "{} returned {:?} past i64", what, z), + } + Ok(()) +} + +proptest! { + #[test] + fn near_the_limit_an_operation_is_exact_or_it_panics( + (a, b, n) in (near_limit(), near_limit(), -3i64..=3) + ) { + let (x, y) = (ZSet::singleton(1u8, a), ZSet::singleton(1u8, b)); + probe(&|| &x + &y, i128::from(a) + i128::from(b), "add")?; + probe(&|| &x - &y, i128::from(a) - i128::from(b), "sub")?; + probe(&|| x.scale(n), i128::from(a) * i128::from(n), "scale")?; + probe(&|| -&x, -i128::from(a), "neg")?; + } +} From d1665f649943b6dce82bf7e85df1d183bb96f747 Mon Sep 17 00:00:00 2001 From: "Claude (adr009-zset)" Date: Sat, 10 Oct 2026 00:04:24 -0700 Subject: [PATCH 5/8] docs(zset): drop the withdrawn premise from the overflow paragraph (improvise-tk51) Co-Authored-By: Claude Sonnet 5.5 Claude-Session: https://claude.ai/code/session_01VdfEGXA7aJ6ftMsCc9PJze --- context/code/zset.md | 8 ++++---- 1 file changed, 4 insertions(+), 4 deletions(-) diff --git a/context/code/zset.md b/context/code/zset.md index 46461e07..b3b551da 100644 --- a/context/code/zset.md +++ b/context/code/zset.md @@ -59,9 +59,8 @@ These are the readings this step takes. is required only where a result copies keys (`filter`, `distinct`, `scale`, the borrowed operators); `map` and the by-value operators need only `Ord`. 5. **Overflow.** Neither clause 1 nor clause 8 states a policy for weights (clause 8 is about - `f64` sums). A weight that wraps would turn a retraction into an insertion with nothing - to show it, which is the failure the ADR's exactness argument is against. So every weight - operation uses `checked_*` and **panics** with `zset: weight overflow in `, in debug + `f64` drift, which wrapping integers do not have). The crate currently uses `checked_*` + on every weight operation, for the reason given below, and **panics** with `zset: weight overflow in `, in debug and in release (`checked_*` does not depend on `overflow-checks`). The operations are `add` (including `insert`, `Extend`, `FromIterator`), `sub`, `neg` (so `i64::MIN` panics when it has to be negated) and `scale`. Scaling by zero cannot overflow and returns the @@ -79,7 +78,8 @@ These are the readings this step takes. under wrapping. (An earlier version of this paragraph said otherwise; that was wrong.) What wrapping breaks is the intermediate reads. `MAX + 1` stores `i64::MIN`, so `distinct` drops a key whose true weight is positive and `weight()` has the wrong sign. A true weight - of 2^64 stores as 0, so the key vanishes and `is_zero`, `len` and `==` report a set that + of 2^64 stores as 0 (by the add path; a `scale` product of 2^64 would store a zero too, which + breaks canonical form), so the key vanishes and `is_zero`, `len` and `==` report a set that does not exist. Those are wrong answers returned silently, which is why the crate panics instead. A wider weight (`i128`) moves the boundary and does not remove it. The ADR's "abelian group" wording needs amending whichever policy is chosen: checked-and-panic gives From 52453ca785f2e570063bdbe6660a53a32de63d3a Mon Sep 17 00:00:00 2001 From: "Claude (adr009-zset-amend)" Date: Sat, 10 Oct 2026 11:14:46 -0700 Subject: [PATCH 6/8] docs(adr): ADR 009 is accepted; Z-set weights are checked i64 and the group is partial (improvise-felo.4) Co-Authored-By: Claude Sonnet 5.5 Claude-Session: https://claude.ai/code/session_01VdfEGXA7aJ6ftMsCc9PJze --- context/adr/009-incremental-evaluation.md | 8 ++++++-- 1 file changed, 6 insertions(+), 2 deletions(-) diff --git a/context/adr/009-incremental-evaluation.md b/context/adr/009-incremental-evaluation.md index 68135713..f0506249 100644 --- a/context/adr/009-incremental-evaluation.md +++ b/context/adr/009-incremental-evaluation.md @@ -1,6 +1,6 @@ # ADR 009 — Incremental evaluation: an in-house DBSP core, plugged in behind a trait -**Status:** proposed. · +**Status:** accepted. · **Ticket:** improvise-felo.4 (the record of this ADR; implementation goes to its own epic) · **Relates to:** ADR 001 (the basis a write claims), ADR 002 (surrogates on the wire), @@ -29,7 +29,11 @@ mutation, it says so and names the incremental path that normally applies. A problem-agnostic workspace crate with no dependencies beyond `std` (so it is wasm32-clean and serde-free). It provides: -- `ZSet`, a map from `K: Ord` to a non-zero `i64` weight, which is an abelian group; +- `ZSet`, a map from `K: Ord` to a non-zero `i64` weight. Weight arithmetic is checked + and panics on overflow, in debug and in release. The group laws are exact wherever no + weight, intermediate ones included, leaves `i64`, so the structure is an abelian group + that is partial at the `i64` boundary. Weights are validated where deltas enter from + the wire (clause 9), so a hostile frame is rejected and never reaches the panic; - a synchronous, single-threaded `Circuit` per process, with `delay`, `integrate`, `differentiate`, `map`, `filter`, `flat_map`, `index_by`, the bilinear delta join `join_indexed`, `distinct` and `aggregate`; From b864abb125533ae5e5e791fe9e018c160525bf5f Mon Sep 17 00:00:00 2001 From: "Claude (adr009-clean)" Date: Sat, 10 Oct 2026 11:21:55 -0700 Subject: [PATCH 7/8] docs(adr): revert the ADR 009 amendment; overflow policy is an implementation detail (improvise-felo.4) Co-Authored-By: Claude Sonnet 5.5 Claude-Session: https://claude.ai/code/session_01VdfEGXA7aJ6ftMsCc9PJze --- context/adr/009-incremental-evaluation.md | 8 ++------ 1 file changed, 2 insertions(+), 6 deletions(-) diff --git a/context/adr/009-incremental-evaluation.md b/context/adr/009-incremental-evaluation.md index f0506249..68135713 100644 --- a/context/adr/009-incremental-evaluation.md +++ b/context/adr/009-incremental-evaluation.md @@ -1,6 +1,6 @@ # ADR 009 — Incremental evaluation: an in-house DBSP core, plugged in behind a trait -**Status:** accepted. · +**Status:** proposed. · **Ticket:** improvise-felo.4 (the record of this ADR; implementation goes to its own epic) · **Relates to:** ADR 001 (the basis a write claims), ADR 002 (surrogates on the wire), @@ -29,11 +29,7 @@ mutation, it says so and names the incremental path that normally applies. A problem-agnostic workspace crate with no dependencies beyond `std` (so it is wasm32-clean and serde-free). It provides: -- `ZSet`, a map from `K: Ord` to a non-zero `i64` weight. Weight arithmetic is checked - and panics on overflow, in debug and in release. The group laws are exact wherever no - weight, intermediate ones included, leaves `i64`, so the structure is an abelian group - that is partial at the `i64` boundary. Weights are validated where deltas enter from - the wire (clause 9), so a hostile frame is rejected and never reaches the panic; +- `ZSet`, a map from `K: Ord` to a non-zero `i64` weight, which is an abelian group; - a synchronous, single-threaded `Circuit` per process, with `delay`, `integrate`, `differentiate`, `map`, `filter`, `flat_map`, `index_by`, the bilinear delta join `join_indexed`, `distinct` and `aggregate`; From 0e78a97e9964d6ecdbe8a2b2c2e3abcdbcdcc274 Mon Sep 17 00:00:00 2001 From: Ed Langley Date: Sat, 10 Oct 2026 11:25:15 -0700 Subject: [PATCH 8/8] Update 009-incremental-evaluation.md --- context/adr/009-incremental-evaluation.md | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/context/adr/009-incremental-evaluation.md b/context/adr/009-incremental-evaluation.md index 68135713..1f6df927 100644 --- a/context/adr/009-incremental-evaluation.md +++ b/context/adr/009-incremental-evaluation.md @@ -1,6 +1,6 @@ # ADR 009 — Incremental evaluation: an in-house DBSP core, plugged in behind a trait -**Status:** proposed. · +**Status:** accepted. · **Ticket:** improvise-felo.4 (the record of this ADR; implementation goes to its own epic) · **Relates to:** ADR 001 (the basis a write claims), ADR 002 (surrogates on the wire),