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 <noreply@anthropic.com> Claude-Session: https://claude.ai/code/session_01VdfEGXA7aJ6ftMsCc9PJze
This commit is contained in:
committed by
Edward Langley
parent
e15b285822
commit
1bb73cbe4f
@@ -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<K: Ord>` | 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 <op>`, 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 = ..)`.
|
||||||
@@ -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 `<property>_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 `<property>_catches_<rival>` 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`.
|
||||||
+10
-16
@@ -1,19 +1,13 @@
|
|||||||
//! Z-sets: finite maps from keys to non-zero `i64` weights, forming an abelian group
|
//! Z-sets: maps from keys to non-zero `i64` weights, an abelian group (ADR 009 clause 1).
|
||||||
//! under pointwise addition (ADR 009 clause 1).
|
//! Reasoning and the overflow policy: `context/code/zset.md`.
|
||||||
//!
|
|
||||||
//! 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::BTreeMap;
|
||||||
use std::collections::btree_map::Entry;
|
use std::collections::btree_map::Entry;
|
||||||
use std::iter::FromIterator;
|
use std::iter::FromIterator;
|
||||||
use std::ops::{Add, AddAssign, Mul, Neg, Sub, SubAssign};
|
use std::ops::{Add, AddAssign, Mul, Neg, Sub, SubAssign};
|
||||||
|
|
||||||
/// A map from `K` to a non-zero `i64` weight.
|
/// 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.
|
||||||
/// 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)]
|
#[derive(Clone, Debug, PartialEq, Eq, Hash, PartialOrd, Ord)]
|
||||||
pub struct ZSet<K> {
|
pub struct ZSet<K> {
|
||||||
weights: BTreeMap<K, i64>,
|
weights: BTreeMap<K, i64>,
|
||||||
@@ -66,6 +60,10 @@ impl<K: Ord> ZSet<K> {
|
|||||||
self.weights.is_empty()
|
self.weights.is_empty()
|
||||||
}
|
}
|
||||||
|
|
||||||
|
pub fn is_empty(&self) -> bool {
|
||||||
|
self.is_zero()
|
||||||
|
}
|
||||||
|
|
||||||
/// The number of keys with a non-zero weight.
|
/// The number of keys with a non-zero weight.
|
||||||
pub fn len(&self) -> usize {
|
pub fn len(&self) -> usize {
|
||||||
self.weights.len()
|
self.weights.len()
|
||||||
@@ -76,9 +74,7 @@ impl<K: Ord> ZSet<K> {
|
|||||||
self.weights.iter().map(|(k, w)| (k, *w))
|
self.weights.iter().map(|(k, w)| (k, *w))
|
||||||
}
|
}
|
||||||
|
|
||||||
/// Adds `weight` to `key`'s weight, dropping the key if the sum is zero.
|
/// Adds `weight` to `key`'s, dropping the key at zero. Panics on `i64` overflow.
|
||||||
///
|
|
||||||
/// Panics if the sum does not fit an `i64`.
|
|
||||||
pub fn insert(&mut self, key: K, weight: i64) {
|
pub fn insert(&mut self, key: K, weight: i64) {
|
||||||
match self.weights.entry(key) {
|
match self.weights.entry(key) {
|
||||||
Entry::Vacant(e) => {
|
Entry::Vacant(e) => {
|
||||||
@@ -131,9 +127,7 @@ impl<K: Ord> ZSet<K> {
|
|||||||
.collect()
|
.collect()
|
||||||
}
|
}
|
||||||
|
|
||||||
/// Every weight times `n`; zero gives the zero Z-set.
|
/// Every weight times `n`; zero gives the zero Z-set. Panics on `i64` overflow.
|
||||||
///
|
|
||||||
/// Panics if a product does not fit an `i64`.
|
|
||||||
pub fn scale(&self, n: i64) -> Self
|
pub fn scale(&self, n: i64) -> Self
|
||||||
where
|
where
|
||||||
K: Clone,
|
K: Clone,
|
||||||
|
|||||||
+176
-61
@@ -1,7 +1,5 @@
|
|||||||
//! Property tests for `zset`. Each property is a checker that takes the implementation as
|
//! Property checkers over an `Alg`; each runs on `ZSet`, and on rivals (`_catches_`).
|
||||||
//! a parameter: the property's own test runs it on `ZSet`, and a `_catches_` companion runs
|
//! Evidence: `context/test-evidence/zset.md`.
|
||||||
//! 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::prelude::*;
|
||||||
use proptest::test_runner::{TestError, TestRunner};
|
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.
|
/// The operations under test, over a representation the implementation chooses.
|
||||||
trait Alg {
|
trait Alg {
|
||||||
type Z: Clone + std::fmt::Debug;
|
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 add(&self, a: &Self::Z, b: &Self::Z) -> Self::Z;
|
||||||
fn neg(&self, a: &Self::Z) -> Self::Z;
|
fn neg(&self, a: &Self::Z) -> Self::Z;
|
||||||
fn sub(&self, a: &Self::Z, b: &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.
|
/// Whether two values are the same set of weights, however each is stored.
|
||||||
fn same(&self, a: &Self::Z, b: &Self::Z) -> bool;
|
fn same(&self, a: &Self::Z, b: &Self::Z) -> bool;
|
||||||
fn zero(&self) -> Self::Z {
|
fn zero(&self) -> Self::Z {
|
||||||
self.from_pairs(&[])
|
self.build(&[])
|
||||||
}
|
}
|
||||||
}
|
}
|
||||||
|
|
||||||
@@ -37,7 +35,7 @@ struct Real;
|
|||||||
|
|
||||||
impl Alg for Real {
|
impl Alg for Real {
|
||||||
type Z = ZSet<u8>;
|
type Z = ZSet<u8>;
|
||||||
fn from_pairs(&self, p: &[(u8, i64)]) -> ZSet<u8> {
|
fn build(&self, p: &[(u8, i64)]) -> ZSet<u8> {
|
||||||
p.iter().copied().collect()
|
p.iter().copied().collect()
|
||||||
}
|
}
|
||||||
fn add(&self, a: &ZSet<u8>, b: &ZSet<u8>) -> ZSet<u8> {
|
fn add(&self, a: &ZSet<u8>, b: &ZSet<u8>) -> ZSet<u8> {
|
||||||
@@ -119,7 +117,7 @@ impl Model {
|
|||||||
|
|
||||||
impl Alg for Model {
|
impl Alg for Model {
|
||||||
type Z = V;
|
type Z = V;
|
||||||
fn from_pairs(&self, p: &[(u8, i64)]) -> V {
|
fn build(&self, p: &[(u8, i64)]) -> V {
|
||||||
self.normal(p.to_vec())
|
self.normal(p.to_vec())
|
||||||
}
|
}
|
||||||
fn add(&self, a: &V, b: &V) -> V {
|
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());
|
let sum = self.normal(a.iter().chain(b).copied().collect());
|
||||||
if self.0 == Fault::AddClamps {
|
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
|
sum
|
||||||
}
|
}
|
||||||
@@ -148,11 +149,19 @@ impl Alg for Model {
|
|||||||
self.normal(a.iter().skip(skip).map(|(k, w)| (*k, -w)).collect())
|
self.normal(a.iter().skip(skip).map(|(k, w)| (*k, -w)).collect())
|
||||||
}
|
}
|
||||||
fn sub(&self, a: &V, b: &V) -> V {
|
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))
|
self.add(x, &self.neg(y))
|
||||||
}
|
}
|
||||||
fn scale(&self, a: &V, n: i64) -> V {
|
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())
|
self.normal(a.iter().map(|(k, w)| (*k, w * n)).collect())
|
||||||
}
|
}
|
||||||
fn map(&self, a: &V, m: u8) -> V {
|
fn map(&self, a: &V, m: u8) -> V {
|
||||||
@@ -176,7 +185,11 @@ impl Alg for Model {
|
|||||||
)
|
)
|
||||||
}
|
}
|
||||||
fn distinct(&self, a: &V) -> V {
|
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(
|
self.normal(
|
||||||
a.iter()
|
a.iter()
|
||||||
.filter(|(_, w)| *w > 0)
|
.filter(|(_, w)| *w > 0)
|
||||||
@@ -203,7 +216,11 @@ impl Alg for Model {
|
|||||||
let mut out = Vec::new();
|
let mut out = Vec::new();
|
||||||
for (i, x) in s.iter().enumerate() {
|
for (i, x) in s.iter().enumerate() {
|
||||||
let d = self.sub(x, &prev);
|
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();
|
prev = x.clone();
|
||||||
}
|
}
|
||||||
out
|
out
|
||||||
@@ -266,47 +283,71 @@ where
|
|||||||
}
|
}
|
||||||
|
|
||||||
fn associativity<A: Alg>(x: &A, (a, b, c): &(Pairs, Pairs, Pairs)) -> Result<(), TestCaseError> {
|
fn associativity<A: Alg>(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 left = x.add(&x.add(&a, &b), &c);
|
||||||
let right = x.add(&a, &x.add(&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(())
|
Ok(())
|
||||||
}
|
}
|
||||||
|
|
||||||
fn commutativity<A: Alg>(x: &A, (a, b): &(Pairs, Pairs)) -> Result<(), TestCaseError> {
|
fn commutativity<A: Alg>(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));
|
let (ab, ba) = (x.add(&a, &b), x.add(&b, &a));
|
||||||
prop_assert!(x.same(&ab, &ba), "[commutativity] {ab:?} != {ba:?}");
|
prop_assert!(x.same(&ab, &ba), "[commutativity] {ab:?} != {ba:?}");
|
||||||
Ok(())
|
Ok(())
|
||||||
}
|
}
|
||||||
|
|
||||||
fn identity<A: Alg>(x: &A, a: &Pairs) -> Result<(), TestCaseError> {
|
fn identity<A: Alg>(x: &A, a: &Pairs) -> Result<(), TestCaseError> {
|
||||||
let a = x.from_pairs(a);
|
let a = x.build(a);
|
||||||
let zero = x.zero();
|
let zero = x.zero();
|
||||||
prop_assert!(x.same(&x.add(&a, &zero), &a), "[identity] a + 0 != a for {a:?}");
|
prop_assert!(
|
||||||
prop_assert!(x.same(&x.add(&zero, &a), &a), "[identity] 0 + a != a for {a:?}");
|
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(())
|
Ok(())
|
||||||
}
|
}
|
||||||
|
|
||||||
fn inverse<A: Alg>(x: &A, a: &Pairs) -> Result<(), TestCaseError> {
|
fn inverse<A: Alg>(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));
|
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);
|
let diff = x.sub(&a, &a);
|
||||||
prop_assert!(x.same(&diff, &x.zero()), "[inverse] a - a = {diff:?} for {a:?}");
|
prop_assert!(
|
||||||
prop_assert!(x.same(&x.neg(&x.neg(&a)), &a), "[inverse] --a != a for {a:?}");
|
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(())
|
Ok(())
|
||||||
}
|
}
|
||||||
|
|
||||||
fn subtraction<A: Alg>(x: &A, (a, b): &(Pairs, Pairs)) -> Result<(), TestCaseError> {
|
fn subtraction<A: Alg>(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)));
|
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(())
|
Ok(())
|
||||||
}
|
}
|
||||||
|
|
||||||
fn canonical_zero<A: Alg>(x: &A, (a, b, n, m): &(Pairs, Pairs, i64, u8)) -> Result<(), TestCaseError> {
|
fn canonical_zero<A: Alg>(
|
||||||
let (a, b) = (x.from_pairs(a), x.from_pairs(b));
|
x: &A,
|
||||||
|
(a, b, n, m): &(Pairs, Pairs, i64, u8),
|
||||||
|
) -> Result<(), TestCaseError> {
|
||||||
|
let (a, b) = (x.build(a), x.build(b));
|
||||||
let made = [
|
let made = [
|
||||||
a.clone(),
|
a.clone(),
|
||||||
x.add(&a, &b),
|
x.add(&a, &b),
|
||||||
@@ -321,7 +362,10 @@ fn canonical_zero<A: Alg>(x: &A, (a, b, n, m): &(Pairs, Pairs, i64, u8)) -> Resu
|
|||||||
];
|
];
|
||||||
for z in &made {
|
for z in &made {
|
||||||
let zeros: Vec<_> = x.stored(z).into_iter().filter(|(_, w)| *w == 0).collect();
|
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(())
|
Ok(())
|
||||||
}
|
}
|
||||||
@@ -333,14 +377,17 @@ fn canonical_equality<A: Alg>(x: &A, (p, seed): &(Pairs, usize)) -> Result<(), T
|
|||||||
shuffled.rotate_left(seed % n);
|
shuffled.rotate_left(seed % n);
|
||||||
shuffled.reverse();
|
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:?}");
|
prop_assert!(x.same(&a, &b), "[canonical-equality] {a:?} != {b:?}");
|
||||||
// The same set built in two steps, with a cancelling pair spliced in.
|
// The same set built in two steps, with a cancelling pair spliced in.
|
||||||
let mut padded = p.clone();
|
let mut padded = p.clone();
|
||||||
padded.push((9, 5));
|
padded.push((9, 5));
|
||||||
padded.push((9, -5));
|
padded.push((9, -5));
|
||||||
let c = x.from_pairs(&padded);
|
let c = x.build(&padded);
|
||||||
prop_assert!(x.same(&a, &c), "[canonical-equality] a cancelled pair changed {a:?} into {c:?}");
|
prop_assert!(
|
||||||
|
x.same(&a, &c),
|
||||||
|
"[canonical-equality] a cancelled pair changed {a:?} into {c:?}"
|
||||||
|
);
|
||||||
Ok(())
|
Ok(())
|
||||||
}
|
}
|
||||||
|
|
||||||
@@ -348,50 +395,91 @@ fn scalar_multiplication<A: Alg>(
|
|||||||
x: &A,
|
x: &A,
|
||||||
(a, b, m, n): &(Pairs, Pairs, i64, i64),
|
(a, b, m, n): &(Pairs, Pairs, i64, i64),
|
||||||
) -> Result<(), TestCaseError> {
|
) -> Result<(), TestCaseError> {
|
||||||
let (a, b) = (x.from_pairs(a), x.from_pairs(b));
|
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)));
|
let (l, r) = (
|
||||||
prop_assert!(x.same(&l, &r), "[scale] (a+b)*n = {l:?} but a*n + b*n = {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.
|
// 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)));
|
let (l, r) = (
|
||||||
prop_assert!(x.same(&l, &r), "[scale] a*(m+n) = {l:?} but a*m + a*n = {r:?}");
|
x.scale(&a, m + n),
|
||||||
prop_assert!(x.same(&x.scale(&a, -1), &x.neg(&a)), "[scale] a * -1 != -a for {a:?}");
|
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, 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(())
|
Ok(())
|
||||||
}
|
}
|
||||||
|
|
||||||
fn map_homomorphism<A: Alg>(x: &A, (a, b, m): &(Pairs, Pairs, u8)) -> Result<(), TestCaseError> {
|
fn map_homomorphism<A: Alg>(x: &A, (a, b, m): &(Pairs, Pairs, u8)) -> Result<(), TestCaseError> {
|
||||||
let (a, b) = (x.from_pairs(a), x.from_pairs(b));
|
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)));
|
let (l, r) = (
|
||||||
prop_assert!(x.same(&l, &r), "[map] map(a+b) = {l:?} but map(a)+map(b) = {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)));
|
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:?}");
|
prop_assert!(x.same(&l, &r), "[map] map(-a) = {l:?} but -map(a) = {r:?}");
|
||||||
Ok(())
|
Ok(())
|
||||||
}
|
}
|
||||||
|
|
||||||
fn filter_linearity<A: Alg>(x: &A, (a, b, d): &(Pairs, Pairs, u8)) -> Result<(), TestCaseError> {
|
fn filter_linearity<A: Alg>(x: &A, (a, b, d): &(Pairs, Pairs, u8)) -> Result<(), TestCaseError> {
|
||||||
let (a, b) = (x.from_pairs(a), x.from_pairs(b));
|
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)));
|
let (l, r) = (
|
||||||
prop_assert!(x.same(&l, &r), "[filter] filter(a+b) = {l:?} but filter(a)+filter(b) = {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)));
|
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(())
|
Ok(())
|
||||||
}
|
}
|
||||||
|
|
||||||
fn distinct_semantics<A: Alg>(x: &A, a: &Pairs) -> Result<(), TestCaseError> {
|
fn distinct_semantics<A: Alg>(x: &A, a: &Pairs) -> Result<(), TestCaseError> {
|
||||||
let a = x.from_pairs(a);
|
let a = x.build(a);
|
||||||
let d = x.distinct(&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!(
|
prop_assert!(
|
||||||
x.stored(&d) == expected,
|
x.stored(&d) == expected,
|
||||||
"[distinct] distinct({a:?}) = {d:?}, expected weight 1 on exactly the positive keys"
|
"[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(())
|
Ok(())
|
||||||
}
|
}
|
||||||
|
|
||||||
fn iteration_order<A: Alg>(x: &A, (p, seed): &(Pairs, usize)) -> Result<(), TestCaseError> {
|
fn iteration_order<A: Alg>(x: &A, (p, seed): &(Pairs, usize)) -> Result<(), TestCaseError> {
|
||||||
let a = x.from_pairs(p);
|
let a = x.build(p);
|
||||||
let order = x.stored(&a);
|
let order = x.stored(&a);
|
||||||
prop_assert!(
|
prop_assert!(
|
||||||
order.windows(2).all(|w| w[0].0 < w[1].0),
|
order.windows(2).all(|w| w[0].0 < w[1].0),
|
||||||
@@ -403,39 +491,66 @@ fn iteration_order<A: Alg>(x: &A, (p, seed): &(Pairs, usize)) -> Result<(), Test
|
|||||||
shuffled.rotate_left(seed % n);
|
shuffled.rotate_left(seed % n);
|
||||||
shuffled.reverse();
|
shuffled.reverse();
|
||||||
}
|
}
|
||||||
let again = x.stored(&x.from_pairs(&shuffled));
|
let again = x.stored(&x.build(&shuffled));
|
||||||
prop_assert!(order == again, "[order] insertion order shows through: {order:?} vs {again:?}");
|
prop_assert!(
|
||||||
|
order == again,
|
||||||
|
"[order] insertion order shows through: {order:?} vs {again:?}"
|
||||||
|
);
|
||||||
Ok(())
|
Ok(())
|
||||||
}
|
}
|
||||||
|
|
||||||
fn correction<A: Alg>(x: &A, (held, target): &(Pairs, Pairs)) -> Result<(), TestCaseError> {
|
fn correction<A: Alg>(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 delta = x.sub(&target, &held);
|
||||||
let got = x.add(&held, &delta);
|
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);
|
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(())
|
Ok(())
|
||||||
}
|
}
|
||||||
|
|
||||||
fn streams<A: Alg>(x: &A, s: &Vec<Pairs>) -> Result<(), TestCaseError> {
|
fn streams<A: Alg>(x: &A, s: &[Pairs]) -> Result<(), TestCaseError> {
|
||||||
let deltas: Vec<_> = s.iter().map(|p| x.from_pairs(p)).collect();
|
let deltas: Vec<_> = s.iter().map(|p| x.build(p)).collect();
|
||||||
let states = x.integrate(&deltas);
|
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();
|
let mut running = x.zero();
|
||||||
for (i, d) in deltas.iter().enumerate() {
|
for (i, d) in deltas.iter().enumerate() {
|
||||||
running = x.add(&running, d);
|
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);
|
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() {
|
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.
|
// The other direction, from arbitrary states.
|
||||||
let again = x.integrate(&x.differentiate(&deltas));
|
let again = x.integrate(&x.differentiate(&deltas));
|
||||||
for (i, d) in deltas.iter().enumerate() {
|
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(())
|
Ok(())
|
||||||
}
|
}
|
||||||
|
|||||||
@@ -48,6 +48,8 @@
|
|||||||
"improvise-gp"
|
"improvise-gp"
|
||||||
# ADR 005 clause 14: nothing depends on it yet, and improvise-core will.
|
# ADR 005 clause 14: nothing depends on it yet, and improvise-core will.
|
||||||
"numtower"
|
"numtower"
|
||||||
|
# ADR 009 clause 1: std-only; nothing depends on it yet.
|
||||||
|
"zset"
|
||||||
];
|
];
|
||||||
pFlags = crates: lib.concatMapStringsSep " " (c: "-p ${c}") crates;
|
pFlags = crates: lib.concatMapStringsSep " " (c: "-p ${c}") crates;
|
||||||
|
|
||||||
|
|||||||
@@ -68,6 +68,7 @@ const SECTIONS = [
|
|||||||
["context/code/cli.md", "code/cli", "The headless CLI"],
|
["context/code/cli.md", "code/cli", "The headless CLI"],
|
||||||
["context/code/gp.md", "code/gp", "gp-tree and improvise-gp"],
|
["context/code/gp.md", "code/gp", "gp-tree and improvise-gp"],
|
||||||
["context/code/numtower.md", "code/numtower", "numtower, the numeric tower"],
|
["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/kb-tool.md", "code/kb-tool", "The kb tool"],
|
||||||
["context/code/tooling.md", "code/tooling", "The repository's own checkers"],
|
["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/cli.md", "test-evidence/cli", "The headless CLI"],
|
||||||
["context/test-evidence/gp.md", "test-evidence/gp", "gp-tree and improvise-gp"],
|
["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/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/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/layout-cost.md", "test-evidence/layout-cost", "Layout and keypress cost"],
|
||||||
["context/test-evidence/scale-bisect.md", "test-evidence/scale-bisect", "Scale bisect"],
|
["context/test-evidence/scale-bisect.md", "test-evidence/scale-bisect", "Scale bisect"],
|
||||||
|
|||||||
Reference in New Issue
Block a user