diff --git a/differential/ALGEBRAIC_FUZZING.md b/differential/ALGEBRAIC_FUZZING.md new file mode 100644 index 00000000..ee149d6a --- /dev/null +++ b/differential/ALGEBRAIC_FUZZING.md @@ -0,0 +1,515 @@ +# Algebraic equivalence fuzzer + +The third fuzzer in this repository, and the one that needs no oracle. + +The other two ask *is the answer right?* — the Lean model in `../lean` is the +authority and `bin/pathmap_trace` is diffed against it, and the crash fuzzer +asks only whether anything blows up. This one asks a different question: + +> **Does it matter which way you compute it?** + +It should not, and `pathmap` offers enough different ways that the question has +teeth. Each case is one algebraic expression over a few generated tries, +evaluated by every route that applies to it, with every answer required to +match. + +```sh +cargo build --release -p differential --bin alg_fuzz + +# a million cases takes about twenty seconds +cargo run --release -p differential --bin alg_fuzz -- --random 1000000 --seed 1 --jobs 8 + +# replay the committed reproducers +cargo run --release -p differential --bin alg_fuzz -- differential/algebraic-corpus/*.bin + +# minimise a failing input, keeping one particular finding +cargo run --release -p differential --bin alg_fuzz -- --shrink input.bin --target values:nary + +# the findings so far, as plain pathmap calls with no fuzzer involved +cargo run --release -p differential --bin alg_bug_repros +``` + +`cargo test -p differential --test algebraic` is the cheap gate: it replays the +corpus, does a short sweep, and pins the harness's own invariants. + +## Why equivalence instead of an oracle + +Writing the Lean model was most of the cost of the existing differential +fuzzer, and it bought a very strong property: the model says what every call +*means*. But it has to be kept in step with the crate by hand — `harness.rs` +and `PathMapModel/Fuzz.lean` share a wire format and an operation table as a +contract — and that cost is paid again for every operation added. + +The algebra is the part of `pathmap` where that trade is worst and where it is +least necessary. Worst, because the operations are the crate's most +re-implemented surface: join exists six times over. Least necessary, because +*the implementations can check each other*. If `PathMap::join`, `join_into`, +`join_map_into`, `join_into_take`, `zipper_join`, `zipper_n_join`, +`zipper_merge_dnf` and `OverlayZipper` all compute a least upper bound, then +they agree, and any disagreement is a defect without anyone having to say in +advance which answer was right. + +That is the whole design. It costs nothing to maintain — a new operation gets +a new entry in a table — and it found six defects in the first few thousand +cases. + +What it gives up is the ability to say *which* side is wrong. A divergence is a +fact about two implementations; deciding between them is a human judgement, and +`algebraic::KNOWN` records the ones that have been made. + +## What is being compared + +### Routes + +A **route** is one consistent way to evaluate a whole expression. Two kinds: + +**Pointwise** routes walk the expression bottom-up and evaluate each node with +a two-operand call, materialising every intermediate into a trie. Route `k` +picks strategy `k % n` for an operator with `n` strategies, so every strategy +is reached by some route and the routes mix them: + +| operator | strategies | +| --- | --- | +| join `\|` | `PathMap::join`, `join_into`, `join_map_into`, `join_into_take`, `zipper_join`, `OverlayZipper` | +| meet `&` | `PathMap::meet`, `meet_into`, `meet_2`, `zipper_meet` | +| subtract `-` | `PathMap::subtract`, `subtract_into`, `zipper_subtract` | +| sym. difference `^` | `zipper_sym_diff`, `(a \| b) - (a & b)` | +| restrict `/` | `PathMap::restrict`, `WriteZipper::restrict` | + +**Whole-expression** routes recognise a shape and hand the entire thing to one +call. These are the routes with real independence, because no intermediate trie +is ever built: + +| route | applies to | call | +| --- | --- | --- | +| `ternary` | a chain of three operands | `zipper_join3` and friends | +| `nary` | a chain of any length | `zipper_n_join` and friends | +| `nary_poly` | the same chain | `ZipperMergeF::join_n` and friends, via the `PolyZipper` enum | +| `dnf` | a join of meets | `zipper_merge_dnf` | +| `fuse` | anything but `restrict` | a `pathmap::fuse` SSA program over trie *nodes* | +| `fuse_distributed` | the same | that program after `distribute_and_over_or` | +| `model` | anything | a flat `BTreeMap`, no trie at all | + +`fuse` is the only route that leaves the zipper layer altogether. It compiles +the expression to the SSA form in `src/fuse.rs` and evaluates it bottom-up over +`TrieNodeODRc` nodes, combining each step with `pjoin_dyn`, `pmeet_dyn` and +`psubtract_dyn` directly — so it checks the node-level primitives against the +zipper traversals that are supposed to agree with them, which nothing else here +does. `FuseOp` maps onto the expression language one-to-one apart from +`restrict`, which it has no operation for. + +`fuse_distributed` is nearly free and worth having: rewriting `(a | b) & c` into +`(a & c) | (b & c)` is supposed to be a performance choice, so the rewrite pass +is checkable by requiring the answer not to change. + +The `model` route is the fourth opinion. Every other route goes through +`pathmap`, so a defect common to the whole algebra layer would make them agree +and still be wrong. It is also the route that found the value-bias defect +fastest, because it has no node layout to be biased by. + +### Laws + +Route comparison catches an implementation that disagrees with its siblings. It +cannot catch a mistake they all share. `src/algebraic/laws.rs` is the other +half: each law is two *different expressions* that must evaluate to the same +trie, so a wrong answer is visible even when every route computes it the same +wrong way. Idempotence, units, associativity, absorption, distributivity, and +the definition `zipper_sym_diff`'s own documentation gives. + +Laws are the reason a defect in the *baseline* is findable at all. When +`PathMap::meet` takes the wrong operand's value, no route disagrees with the +baseline in an interesting way — the baseline is what everyone is compared +against. `meet-distributes-over-join` has no baseline to be fooled by: it puts +the operands on different sides of a meet and notices. + +### Three value types, and the difference between them is a measurement + +Every case runs once per value type, and signatures are prefixed with the type +(`u64:values:pw1`, `bits:law:join-associative`). That is the fuzzer's main +discriminator: + +* **`bits`** is a 64-bit set under `|`, `&` and `& !`, with an empty result + collapsing to bottom — i.e. to an absent value, the convention `SetLattice`'s + documentation already states. A genuine Boolean algebra, so every lattice + identity holds and a law that fails here is a real defect. It lives in + `src/algebraic/value.rs` rather than in `pathmap`, because a value type defined + outside the crate is what a real caller has. + +* **`unit`** is `PathMap<()>`: the set case, also lawful, since `Option<()>` is + the two-element Boolean algebra. It earns its own slot for a reason neither of + the others covers: `()`'s `pjoin` and `pmeet` return + `Identity(SELF_IDENT | COUNTER_IDENT)` — *both* identity bits — on every single + combination, where `u64` and `bits` do so only for equal values. That saturates + the "either operand will do" path the node code uses to decide it can hand back + an operand unchanged and keep sharing it, which is precisely the machinery + findings 4 and 6 are about. It is also what `unit-value-optimizations` and + `unit-size` are about; neither is on `master`, so today this covers the generic + path, and if they land it is the only thing covering the specialised one. + Nothing in `zipper_algebra.rs` tests `()` at all — every test there uses `u64`. + +* **`u64`** is what the rest of this crate's fuzzing uses, and its instances in + `pathmap::ring` are **not a lattice**: `pjoin` is `left_biased_pjoin`, `pmeet` + is `Identity(SELF_IDENT)` — both return the left operand, so `a | b == a & b` + for every pair, which in a lattice forces `a == b`. It is kept because it is + what callers use today, and because it reaches `Identity`-heavy paths that the + lawful type does not. + +A finding under `u64` alone is an artefact. One under a lawful type is a defect. `alg_fuzz` prints the split at the end of every run: + +``` +by value type -- bits is lawful, u64 is not: + finding u64 bits + law:absorb-join-meet 82 - + law:join-associative 3131 12 + law:join-distributes-over-meet 2077 1 + law:meet-distributes-over-join 1603 - + law:sym-diff-is-join-minus-meet 6684 5 + panic:build:line_list_node.rs:1745 13476 13476 + values:model 1258 2 + values:pw1 30849 36071 + ... +``` + +Read the counts, not just the membership. `law:join-associative` failing 3131 +times under `u64` and 12 under `bits` is **one** defect amplified by the value +type: under a commutative join, picking the wrong operand is invisible except +where one operand already contains the other, so only that residue survives. And +every one of those residues shrinks to a value present on one side of the +identity and *absent* on the other — which is finding 4, a lost value, not a +misplaced one. + +So far: five findings are `u64`-only, nothing is `bits`-only, and `values:model` +drops from 1258 to 2 — the flat reference model and the trie agree on values +almost everywhere once the value algebra is lawful. + +### Why a bitmask and not some other lawful lattice + +Lawfulness is not sufficient, and this is the part worth remembering. +`max`/`min` on a total order is a perfectly good distributive lattice, every +identity holds, and it is **useless here**: `max(a, b)` and `min(a, b)` are +always one of the operands, so they can only return +`AlgebraicResult::Identity`, and every code path that allocates and stores a +genuinely combined value stays unreachable. `a | b` is a new value, so a bitmask +reaches them. `bin/alg_lattice_check` prints the table: + +``` + type pjoin pmeet psubtract + u64 NO NO yes <- and PR #115 makes that NO too + bool NO NO NO + MinMax NO NO NO <- lawful, still useless + Bits yes yes yes + ByteMask yes yes yes +``` + +`pathmap::utils` already implements exactly this for `[u64; 4]` and `ByteMask`, +via `bitmask_algebraic_result`; `Bits` is the same construction at 64 bits. + +### What the lawful type unlocked + +Four identities are checked **only** for a lawful value type, in +`laws::lawful_only` — De Morgan for relative complement both ways, +`a - b == a - (a & b)`, and symmetric difference being associative on *values* +rather than only on paths. Each fails for `u64`, for the same reason everything +else does. + +**Three of the four hold** across several million cases in both profiles: +`subtract-over-meet`, `subtract-is-subtract-meet` and `sym-diff-associative`. +They are the strongest laws the harness has and are deliberately absent from +`KNOWN`, so one of them firing is news. + +The fourth, `subtract-over-join`, fires about once per two million cases under +`unit` — and is cause 2 rather than a bad identity. Its shrunk case has a +dangling-only `b` and a `c` that is `b` plus one value, so `b | c` is exactly +finding 4. + +The `Level::Paths` laws are also promoted to `Level::Values` for a lawful type, +so commutativity of join and meet is checked on values there. + +### One thing the lawful type cannot do + +`OverlayZipper`'s mapping has signature +`Fn(Option<&'a AV>, Option<&'a BV>) -> Option<&'a OutV>` — it returns a +*reference*, so it has nowhere to put a value it would have to create. The +module's own comment says as much. So an overlay can stand in for a join only +when the join never creates anything, and for a real lattice it cannot be a join +at all. The strategy therefore *declines* for `bits` rather than answering +wrongly, which is why `pw5` applies to fewer cases there. That is a limitation of +the zipper, not a defect, and not reported as one. + +Note that declining is what keeps route numbers comparable. An earlier version +shortened the join strategy table for such types, which silently renumbered every +later route — so `pw4` and `pw5` meant different strategy mixes under the two +types, and comparing their findings compared different things. + +## Generated operands + +Four tries per case, over a small alphabet so they collide, with few entries +and short paths. Three details earn their keep: + +* **Three distinct values.** `psubtract` on `u64` is `None` only when the two + values are *equal*, and symmetric difference cancels on coincident paths. A + large value space would degenerate both into set difference and set union and + never exercise the value-combining code at all. + +* **Dangling paths**, written with `create_path` and carrying no value. Whether + one survives an operation is unsettled in the crate, so a divergence confined + to them is reported as its own class. + +* **Four build modes.** `Fresh` writes entries into a new map. `CloneOf` + clones an earlier operand and mutates it, so the two share *allocations* + rather than merely equal content. `ReinsertOf` writes an earlier operand's + entries back in a different order — equal content, different node layout, no + sharing. `MerkleizedOf` runs `merkleize` to factor equal subtries into one + allocation. + +The last three are not decoration. The value-bias defect needs operands whose +nodes are laid out differently, and the value-loss defect needs operands that +share nodes — it disappears if `b`'s entries are rebuilt into a fresh map +instead of cloned. A generator that only wrote fresh tries would find neither. + +## Divergence classes + +| class | meaning | fails a run | +| --- | --- | --- | +| `values` | two routes put different values on a path, or disagree about whether a path has one | yes | +| `shape` | the routes agree on every value and differ only in dangling paths | only under `--shape` | +| `law` | an identity that must hold whatever the operands are does not | yes | +| `panic:build` | a crash while *writing the operand tries*, before any algebra ran | yes | +| `panic:eval` | a crash inside an algebraic operation | yes | + +`shape` is separated because the semantics are genuinely unsettled — see +`../SPEC_WARTS.md` and the `meet_into-keeps-dangling*` corpus entries, which are +the same question. The two families answer it differently and *consistently*, +which is worth knowing because it says which side has to change once the question +is settled: + +* the lockstep traversals in `experimental::zipper_algebra` **discard** dangling + structure; +* `PathMap`'s whole-map operations and the write-zipper forms (`join_into`, + `meet_into`, `subtract_into`) **preserve** it. + +`bin/alg_bug_repros` case 9 shows three of them side by side, the sharpest being +`d ^ {}`: symmetric difference with the empty trie ought to be the identity, and +`zipper_sym_diff` returns nothing where `(d | e) - (d & e)` returns `d`. A wrong +*value* is never ambiguous. + +Signatures are `class:route`, and nothing more. An earlier version appended the +operators the expression used, which looked more informative and was much +worse: one defect in `meet` produced dozens of signatures because it surfaced +under every operator combination containing a meet. The expression, the +operands and the diff all live in the saved `.txt`; the signature's only job is +to collapse a million inputs onto a handful of lines. + +## Soundness limit: catching a panic in process is not safe + +**A long run that catches panics can abort with heap corruption.** Reproducibly: + +``` +$ ./alg_fuzz --random 2000000 --seed 55 --jobs 8 # debug-assertions build +malloc(): unaligned tcache chunk detected +Aborted (core dumped) +``` + +Narrowed by elimination, each at 2M cases, seed 55, 8 jobs: + +| build | `merkleize` in the generator | caught panics | result | +| --- | --- | --- | --- | +| debug assertions | yes | ~27k | **abort** | +| debug assertions | no | ~100 | **abort** | +| release | yes | ~27k | **abort** | +| release | no | 0 | clean, exit 0 | + +So it tracks the *number of panics caught*, not the build profile, the thread +count or the value type. The cause is that `catch_unwind` resumes after a panic +that fired **mid-mutation inside `pathmap`'s node code**: unwinding out of a +half-updated node leaves a trie that is not safe to drop, and the damage shows up +later as an invalid free. Every panic the fuzzer catches is one of these — a +`debug_assert!` inside a merge, or `merkleize`'s `unwrap`, both of which are +"this cannot happen" sites rather than supported unwind paths. + +That is a limitation of *this* harness, not an independent defect. The crash +fuzzer does not have it because AFL runs one input per process and so never +continues after a panic. + +**Until this is fixed, treat the first panic in a run as the end of the useful +output.** Findings reported before it are valid — the signature counts and +reproducers are written as they are found — but anything after the first caught +panic is suspect, and a run that aborts has lost whatever it had not yet printed. +A release-profile run on a generator without `merkleize` catches nothing and is +unaffected. + +The fix is to make panics terminal and rare, the way a crash fuzzer treats them: +stop the run on the first one, and stop generating the one panic that is already +documented with a standalone reproducer (`merkleize`, repro 5) so that the +remaining ones are rare enough for stopping to cost nothing. That needs the +corpus replay to run one input per process, so it is a design change rather than +a patch, and it is not done yet. + +## Debug assertions are a separate mode + +`pathmap`'s `debug_assert!`s are the sharpest instrument here, and a release +build cannot see them. Three of the findings below are visible *only* with +assertions on, and two of them are the mechanism behind a defect that the +release build can only observe as a wrong answer: + +```sh +RUSTFLAGS="-C target-cpu=native -C debug-assertions=yes" \ + cargo build --release -p differential --bin alg_fuzz --target-dir target/dbgassert +./target/dbgassert/release/alg_fuzz --random 5000000 --seed 1 --jobs 8 +``` + +Keep `-C target-cpu=native`: `.cargo/config.toml` sets it, a bare `RUSTFLAGS` +replaces rather than extends it, and `gxhash` fails to compile without the +`aes` and `sse2` intrinsics it implies. + +`cargo test` is itself a debug-assertions build, which is why the corpus test +expects the `panic:eval:*` signatures. + +## Findings + +Seven defects on `master` at `b4a6abd`, plus one unchosen convention, reproduced +without the fuzzer in `src/bin/alg_bug_repros.rs`. `algebraic::KNOWN` maps every +signature onto one of them. + +1. **`join_into` drops the source's root value when the destination is empty.** + `PathMap::new().join(&src)` keeps it; the write-zipper spelling does not. + +2. **`meet_2` drops root values outright.** Two maps whose only content is a + root value intersect to that root value; `meet_2` produces nothing. + +3. **Value bias by node layout.** `PathMap::join` and `PathMap::meet` take the + *right* operand's value at a shared path when the two operands' nodes are + laid out differently. Every zipper route gets this right, which is why it + surfaces as failing laws and as the `model` route disagreeing — the defect is + in the baseline. + +4. **`join` loses a value across shared structure.** With `b` a clone of `a` + plus one extra value, `a | b` drops that value and `b | a` keeps it. A join + is a least upper bound, so no ordering of the operands may lose a path; this + is the one finding that needs no argument about value bias. Found by + `join-commutative`, which is checked on paths only and so cannot be fooled by + cause 3. + +5. **`merkleize` panics on a trie holding only dangling paths.** Not algebraic: + it fires while the operands are still being written. Kept rather than + generated around, because `merkleize` is how the generator produces shared + subtries and finding 4 needs them. + +6. **Join's "empty result" path is reachable from non-empty nodes.** Three + debug assertions, one story, and the mechanism behind finding 4: + `merge_from_list_node` returns `AlgebraicStatus::None` from nodes that are not + empty (`line_list_node.rs:2669` and `:2720`), and a cofree `pjoin` returns + `None` while the left side still has a non-empty onward node + (`dense_byte_node.rs:2080`). Debug-assertions builds only, so it has no + standalone reproducer — replay the `panic-eval-*` corpus inputs. + +7. **`fuse`'s `Xor` loses a value only one operand has.** Finding 4 again, with + no clone involved and a visible consequence. `Xor` is `(l \ r) | (r \ l)`; with + `c` holding no values and `a` holding one, `c \ a` comes out dangling-only and + `a \ c` keeps the value, so the join at the end is exactly finding 4's shape. + Every `PathMap`-level spelling — `a - c`, `(c | a) - (c & a)`, `(c - a) | (a - + c)` — is correct here; only the node-level composition loses it, and + `join_into_dyn` returns `AlgebraicStatus::Element` while doing so, so a caller + cannot detect it from the status. + +**And one that is not a defect at all, which is now visible as such.** `zipper_sym_diff` cancels a coincident +path carrying *different* values; `fuse`'s `Xor` keeps the left value. It is +tempting to call that two conventions for symmetric difference, and an earlier +version of this document did. That was wrong: `(a | b) - (a & b)` and +`(a - b) | (b - a)` are equal in any distributive lattice with a relative +complement, so there is nothing to choose between them. They come apart only +because `u64` is not a lattice — with `pjoin` and `pmeet` collapsed into one +function, the first formula becomes `a - a` and vanishes while the second stays +`a`. Both implementations are right and the premise was wrong. See "`u64` is not +a lattice" above; `bin/alg_lattice_check` shows `bool` agreeing on all four +inputs. Reported, counted, and not a bug. + +### Reading a report + +A value divergence also says which side the `model` route backs. That line is +worth reading first: the baseline is `PathMap::join` and friends, which have +defects of their own, so "route X disagrees with the baseline" points at the +wrong file about as often as the right one. When the model sides with the route, +the baseline is where to look. When it agrees with neither, suspect a shared +primitive — or the model. + +Every signature is printed with its count, known or not, and a `<-- NEW` marker +on anything absent from `KNOWN`. Exit status is 1 if anything is new; +`--strict` makes every finding fatal. Counts matter even for known findings: a +known defect that starts firing ten times more often is a change worth seeing, +and it does not turn the run red. + +`KNOWN` is a snapshot, not a closed list. A longer sweep may well reach a new +assertion site — the three in finding 6 appeared at 500 000, 3 000 000 and +roughly 400 000 cases respectively. A new signature is the fuzzer working. + +## What this changed in `src/fuse.rs` + +`fuse.rs` is ported from the `trie-fusion-ops` branch at `e94915c`, which is 448 +commits behind `master`; only the module itself came across, not that branch's +`cbm_stream` work, its `utils` additions, or its reduction of the workspace +member list. Two changes were made to it: + +* **`combine_val` now delegates to the lattice operations**, through the + `Option` impls in `pathmap::ring`, mirroring `combine_node` arm for arm. It + used to decide the root value by presence alone: `And` kept the *right* value + and `AndNot` dropped the left value whenever the right side had any value at + all. Correct for a set, but it meant a root value and a value one byte deeper + were combined by different rules — and for `u64`, where `pmeet` is + `Identity(SELF_IDENT)` and `psubtract` is `None` only for *equal* values, both + arms were simply wrong. With this fixed, the `fuse` routes agree with + everything else on join, meet and subtract; disabling `SymDiff` in the + generator makes both `fuse` signatures disappear entirely. + +* The module header described a fused byte-by-byte walk that an earlier revision + reverted. It now describes the bottom-up whole-node evaluator that is actually + there, and records why the byte-level version cannot be written against the + `TrieNode` trait: `LineListNode` stores compressed multi-byte keys, so + `node_get_child(&[byte])` returns `None` for a byte `node_branches_mask` + reports as present. + +## Harness invariants + +A harness that reports its own mistakes as crate defects is worse than no +harness. Two of the recognisers that decide which route applies were wrong when +this fuzzer was first run, and both failures looked exactly like crate defects: + +* `a ^ (b ^ c)` was flattened into the n-ary call, which folds values left. For + root values `a = 2`, `b = 1`, the nested form is `a ^ nothing = 2` and the + fold is `(2 ^ 2) ^ 1 = 1`. Both are defensible; they are not equal, so a + right-nested symmetric difference is not a chain. + +* A DNF clause was allowed to stand in for `b & a`. A `Clause` is a *bitmask* — + it records which zippers take part, not in what order — and `zipper_merge_dnf` + meets a clause's members in slot order while `pmeet` is left-biased, so `a & + b` and `b & a` carry different values and only one of them is what the clause + computes. + +Both are now pinned by tests in `tests/algebraic.rs`, along with the invariant +that every strategy index is reachable from some pointwise route. When a route +disagrees with the rest, suspect the route first. + +## Layout + +| file | what | +| --- | --- | +| `src/algebraic.rs` | input decoding, operand generation, the comparison, `KNOWN` | +| `src/algebraic/expr.rs` | the expression language and the shape recognisers | +| `src/algebraic/routes.rs` | the routes, and one arm per strategy | +| `src/algebraic/laws.rs` | the identities, and the ones deliberately absent | +| `src/algebraic/model.rs` | flat `BTreeMap` semantics, delegating to the value algebra | +| `src/algebraic/value.rs` | the `FuzzValue` trait and the lawful `Bits` type | +| `src/algebraic/shape.rs` | what "the same result" means | +| `src/bin/alg_fuzz.rs` | the driver: generation, replay, shrinking, reporting | +| `src/bin/alg_bug_repros.rs` | every cause in `KNOWN` as plain `pathmap` calls | +| `src/bin/alg_lattice_check.rs` | whether a divergence is the crate's fault or `u64`'s | +| `tests/algebraic.rs` | the corpus gate and the harness invariants | +| `algebraic-corpus/` | one minimised input per signature | + +`src/fuse.rs` in the parent crate is the one file outside `differential/` this +work touches; see above. + +Byte decoding reuses `harness::Dec`. The wire format is *not* the one +`harness.rs` shares with `PathMapModel.Fuzz`: this fuzzer has no model to stay +in step with, so its inputs are free to be whatever generates interesting +tries. diff --git a/differential/Cargo.toml b/differential/Cargo.toml index 4218b74a..6b2ff2ea 100644 --- a/differential/Cargo.toml +++ b/differential/Cargo.toml @@ -6,4 +6,4 @@ publish = false description = "The Rust side of the differential fuzzing harness for pathmap's zipper API; the Lean model in ../lean is the oracle" [dependencies] -pathmap = { path = "..", features = ["arena_compact"] } +pathmap = { path = "..", features = ["arena_compact", "zipper_alg"] } diff --git a/differential/algebraic-corpus/bits-law-join-associative.bin b/differential/algebraic-corpus/bits-law-join-associative.bin new file mode 100644 index 00000000..f72be3a6 Binary files /dev/null and b/differential/algebraic-corpus/bits-law-join-associative.bin differ diff --git a/differential/algebraic-corpus/bits-law-join-commutative.bin b/differential/algebraic-corpus/bits-law-join-commutative.bin new file mode 100644 index 00000000..3c9b49c7 --- /dev/null +++ b/differential/algebraic-corpus/bits-law-join-commutative.bin @@ -0,0 +1 @@ +rAX}>h ī_[Tb#j6&|cH?KQ|) \ No newline at end of file diff --git a/differential/algebraic-corpus/bits-law-join-distributes-over-meet.bin b/differential/algebraic-corpus/bits-law-join-distributes-over-meet.bin new file mode 100644 index 00000000..3c9b49c7 --- /dev/null +++ b/differential/algebraic-corpus/bits-law-join-distributes-over-meet.bin @@ -0,0 +1 @@ +rAX}>h ī_[Tb#j6&|cH?KQ|) \ No newline at end of file diff --git a/differential/algebraic-corpus/bits-law-majority-is-pairwise-meets.bin b/differential/algebraic-corpus/bits-law-majority-is-pairwise-meets.bin new file mode 100644 index 00000000..c4e969a3 Binary files /dev/null and b/differential/algebraic-corpus/bits-law-majority-is-pairwise-meets.bin differ diff --git a/differential/algebraic-corpus/bits-law-sym-diff-is-join-minus-meet.bin b/differential/algebraic-corpus/bits-law-sym-diff-is-join-minus-meet.bin new file mode 100644 index 00000000..9fc454b8 --- /dev/null +++ b/differential/algebraic-corpus/bits-law-sym-diff-is-join-minus-meet.bin @@ -0,0 +1 @@ +lc 4bC6׿0eJ]TBE@c'o@-t7x\M*PBڊ̣z_^^X79h ī_[Tb#j6&|cH?KQ|) \ No newline at end of file diff --git a/differential/algebraic-corpus/u64-law-join-distributes-over-meet.bin b/differential/algebraic-corpus/u64-law-join-distributes-over-meet.bin new file mode 100644 index 00000000..b6f8d1f3 Binary files /dev/null and b/differential/algebraic-corpus/u64-law-join-distributes-over-meet.bin differ diff --git a/differential/algebraic-corpus/u64-law-majority-is-pairwise-meets.bin b/differential/algebraic-corpus/u64-law-majority-is-pairwise-meets.bin new file mode 100644 index 00000000..c4e969a3 Binary files /dev/null and b/differential/algebraic-corpus/u64-law-majority-is-pairwise-meets.bin differ diff --git a/differential/algebraic-corpus/u64-law-meet-associative.bin b/differential/algebraic-corpus/u64-law-meet-associative.bin new file mode 100644 index 00000000..f3a9a652 Binary files /dev/null and b/differential/algebraic-corpus/u64-law-meet-associative.bin differ diff --git a/differential/algebraic-corpus/u64-law-meet-distributes-over-join.bin b/differential/algebraic-corpus/u64-law-meet-distributes-over-join.bin new file mode 100644 index 00000000..124a81f7 Binary files /dev/null and b/differential/algebraic-corpus/u64-law-meet-distributes-over-join.bin differ diff --git a/differential/algebraic-corpus/u64-law-sym-diff-is-join-minus-meet.bin b/differential/algebraic-corpus/u64-law-sym-diff-is-join-minus-meet.bin new file mode 100644 index 00000000..86afcd5e Binary files /dev/null and b/differential/algebraic-corpus/u64-law-sym-diff-is-join-minus-meet.bin differ diff --git a/differential/algebraic-corpus/u64-panic-build-line_list_node-rs-1745.bin b/differential/algebraic-corpus/u64-panic-build-line_list_node-rs-1745.bin new file mode 100644 index 00000000..d2d801a7 Binary files /dev/null and b/differential/algebraic-corpus/u64-panic-build-line_list_node-rs-1745.bin differ diff --git a/differential/algebraic-corpus/u64-panic-eval-dense_byte_node-rs-2080.bin b/differential/algebraic-corpus/u64-panic-eval-dense_byte_node-rs-2080.bin new file mode 100644 index 00000000..6cc4bf15 Binary files /dev/null and b/differential/algebraic-corpus/u64-panic-eval-dense_byte_node-rs-2080.bin differ diff --git a/differential/algebraic-corpus/u64-panic-eval-line_list_node-rs-2669.bin b/differential/algebraic-corpus/u64-panic-eval-line_list_node-rs-2669.bin new file mode 100644 index 00000000..f190541e Binary files /dev/null and b/differential/algebraic-corpus/u64-panic-eval-line_list_node-rs-2669.bin differ diff --git a/differential/algebraic-corpus/u64-panic-eval-line_list_node-rs-2720.bin b/differential/algebraic-corpus/u64-panic-eval-line_list_node-rs-2720.bin new file mode 100644 index 00000000..4998ad13 Binary files /dev/null and b/differential/algebraic-corpus/u64-panic-eval-line_list_node-rs-2720.bin differ diff --git a/differential/algebraic-corpus/u64-shape-dnf.bin b/differential/algebraic-corpus/u64-shape-dnf.bin new file mode 100644 index 00000000..3a5c32d5 Binary files /dev/null and b/differential/algebraic-corpus/u64-shape-dnf.bin differ diff --git a/differential/algebraic-corpus/u64-shape-fuse.bin b/differential/algebraic-corpus/u64-shape-fuse.bin new file mode 100644 index 00000000..ecbc8dcf Binary files /dev/null and b/differential/algebraic-corpus/u64-shape-fuse.bin differ diff --git a/differential/algebraic-corpus/u64-shape-fuse_distributed.bin b/differential/algebraic-corpus/u64-shape-fuse_distributed.bin new file mode 100644 index 00000000..ecbc8dcf Binary files /dev/null and b/differential/algebraic-corpus/u64-shape-fuse_distributed.bin differ diff --git a/differential/algebraic-corpus/u64-shape-nary.bin b/differential/algebraic-corpus/u64-shape-nary.bin new file mode 100644 index 00000000..5ab2d80a Binary files /dev/null and b/differential/algebraic-corpus/u64-shape-nary.bin differ diff --git a/differential/algebraic-corpus/u64-shape-nary_poly.bin b/differential/algebraic-corpus/u64-shape-nary_poly.bin new file mode 100644 index 00000000..5ab2d80a Binary files /dev/null and b/differential/algebraic-corpus/u64-shape-nary_poly.bin differ diff --git a/differential/algebraic-corpus/u64-shape-pw1.bin b/differential/algebraic-corpus/u64-shape-pw1.bin new file mode 100644 index 00000000..860cf2ba Binary files /dev/null and b/differential/algebraic-corpus/u64-shape-pw1.bin differ diff --git a/differential/algebraic-corpus/u64-shape-pw2.bin b/differential/algebraic-corpus/u64-shape-pw2.bin new file mode 100644 index 00000000..c7ac697f Binary files /dev/null and b/differential/algebraic-corpus/u64-shape-pw2.bin differ diff --git a/differential/algebraic-corpus/u64-shape-pw3.bin b/differential/algebraic-corpus/u64-shape-pw3.bin new file mode 100644 index 00000000..2fbb6009 Binary files /dev/null and b/differential/algebraic-corpus/u64-shape-pw3.bin differ diff --git a/differential/algebraic-corpus/u64-shape-pw4.bin b/differential/algebraic-corpus/u64-shape-pw4.bin new file mode 100644 index 00000000..829ce685 Binary files /dev/null and b/differential/algebraic-corpus/u64-shape-pw4.bin differ diff --git a/differential/algebraic-corpus/u64-shape-pw5.bin b/differential/algebraic-corpus/u64-shape-pw5.bin new file mode 100644 index 00000000..27a427f9 Binary files /dev/null and b/differential/algebraic-corpus/u64-shape-pw5.bin differ diff --git a/differential/algebraic-corpus/u64-shape-ternary.bin b/differential/algebraic-corpus/u64-shape-ternary.bin new file mode 100644 index 00000000..619912b9 Binary files /dev/null and b/differential/algebraic-corpus/u64-shape-ternary.bin differ diff --git a/differential/algebraic-corpus/u64-values-dnf.bin b/differential/algebraic-corpus/u64-values-dnf.bin new file mode 100644 index 00000000..67c86be8 Binary files /dev/null and b/differential/algebraic-corpus/u64-values-dnf.bin differ diff --git a/differential/algebraic-corpus/u64-values-fuse.bin b/differential/algebraic-corpus/u64-values-fuse.bin new file mode 100644 index 00000000..f1faf2f7 Binary files /dev/null and b/differential/algebraic-corpus/u64-values-fuse.bin differ diff --git a/differential/algebraic-corpus/u64-values-fuse_distributed.bin b/differential/algebraic-corpus/u64-values-fuse_distributed.bin new file mode 100644 index 00000000..f1faf2f7 Binary files /dev/null and b/differential/algebraic-corpus/u64-values-fuse_distributed.bin differ diff --git a/differential/algebraic-corpus/u64-values-model.bin b/differential/algebraic-corpus/u64-values-model.bin new file mode 100644 index 00000000..5e7b0454 Binary files /dev/null and b/differential/algebraic-corpus/u64-values-model.bin differ diff --git a/differential/algebraic-corpus/u64-values-nary.bin b/differential/algebraic-corpus/u64-values-nary.bin new file mode 100644 index 00000000..f0aee8b9 Binary files /dev/null and b/differential/algebraic-corpus/u64-values-nary.bin differ diff --git a/differential/algebraic-corpus/u64-values-nary_poly.bin b/differential/algebraic-corpus/u64-values-nary_poly.bin new file mode 100644 index 00000000..f0aee8b9 Binary files /dev/null and b/differential/algebraic-corpus/u64-values-nary_poly.bin differ diff --git a/differential/algebraic-corpus/u64-values-pw1.bin b/differential/algebraic-corpus/u64-values-pw1.bin new file mode 100644 index 00000000..382815d5 Binary files /dev/null and b/differential/algebraic-corpus/u64-values-pw1.bin differ diff --git a/differential/algebraic-corpus/u64-values-pw2.bin b/differential/algebraic-corpus/u64-values-pw2.bin new file mode 100644 index 00000000..b2d29072 Binary files /dev/null and b/differential/algebraic-corpus/u64-values-pw2.bin differ diff --git a/differential/algebraic-corpus/u64-values-pw3.bin b/differential/algebraic-corpus/u64-values-pw3.bin new file mode 100644 index 00000000..382815d5 Binary files /dev/null and b/differential/algebraic-corpus/u64-values-pw3.bin differ diff --git a/differential/algebraic-corpus/u64-values-pw4.bin b/differential/algebraic-corpus/u64-values-pw4.bin new file mode 100644 index 00000000..b18cc564 Binary files /dev/null and b/differential/algebraic-corpus/u64-values-pw4.bin differ diff --git a/differential/algebraic-corpus/u64-values-pw5.bin b/differential/algebraic-corpus/u64-values-pw5.bin new file mode 100644 index 00000000..7f7eb69e Binary files /dev/null and b/differential/algebraic-corpus/u64-values-pw5.bin differ diff --git a/differential/algebraic-corpus/u64-values-ternary.bin b/differential/algebraic-corpus/u64-values-ternary.bin new file mode 100644 index 00000000..317933df Binary files /dev/null and b/differential/algebraic-corpus/u64-values-ternary.bin differ diff --git a/differential/algebraic-corpus/unit-law-join-associative.bin b/differential/algebraic-corpus/unit-law-join-associative.bin new file mode 100644 index 00000000..64f10458 Binary files /dev/null and b/differential/algebraic-corpus/unit-law-join-associative.bin differ diff --git a/differential/algebraic-corpus/unit-law-join-commutative.bin b/differential/algebraic-corpus/unit-law-join-commutative.bin new file mode 100644 index 00000000..db917451 Binary files /dev/null and b/differential/algebraic-corpus/unit-law-join-commutative.bin differ diff --git a/differential/algebraic-corpus/unit-law-join-distributes-over-meet.bin b/differential/algebraic-corpus/unit-law-join-distributes-over-meet.bin new file mode 100644 index 00000000..4de48488 Binary files /dev/null and b/differential/algebraic-corpus/unit-law-join-distributes-over-meet.bin differ diff --git a/differential/algebraic-corpus/unit-law-majority-is-pairwise-meets.bin b/differential/algebraic-corpus/unit-law-majority-is-pairwise-meets.bin new file mode 100644 index 00000000..c6aee0e6 Binary files /dev/null and b/differential/algebraic-corpus/unit-law-majority-is-pairwise-meets.bin differ diff --git a/differential/algebraic-corpus/unit-law-meet-distributes-over-join.bin b/differential/algebraic-corpus/unit-law-meet-distributes-over-join.bin new file mode 100644 index 00000000..f642c3c3 Binary files /dev/null and b/differential/algebraic-corpus/unit-law-meet-distributes-over-join.bin differ diff --git a/differential/algebraic-corpus/unit-law-subtract-over-join.bin b/differential/algebraic-corpus/unit-law-subtract-over-join.bin new file mode 100644 index 00000000..f642c3c3 Binary files /dev/null and b/differential/algebraic-corpus/unit-law-subtract-over-join.bin differ diff --git a/differential/algebraic-corpus/unit-law-sym-diff-is-join-minus-meet.bin b/differential/algebraic-corpus/unit-law-sym-diff-is-join-minus-meet.bin new file mode 100644 index 00000000..f4399390 Binary files /dev/null and b/differential/algebraic-corpus/unit-law-sym-diff-is-join-minus-meet.bin differ diff --git a/differential/algebraic-corpus/unit-panic-build-line_list_node-rs-1745.bin b/differential/algebraic-corpus/unit-panic-build-line_list_node-rs-1745.bin new file mode 100644 index 00000000..aa7d50f8 Binary files /dev/null and b/differential/algebraic-corpus/unit-panic-build-line_list_node-rs-1745.bin differ diff --git a/differential/algebraic-corpus/unit-panic-eval-dense_byte_node-rs-2080.bin b/differential/algebraic-corpus/unit-panic-eval-dense_byte_node-rs-2080.bin new file mode 100644 index 00000000..1b859d85 Binary files /dev/null and b/differential/algebraic-corpus/unit-panic-eval-dense_byte_node-rs-2080.bin differ diff --git a/differential/algebraic-corpus/unit-panic-eval-line_list_node-rs-2669.bin b/differential/algebraic-corpus/unit-panic-eval-line_list_node-rs-2669.bin new file mode 100644 index 00000000..f2185527 Binary files /dev/null and b/differential/algebraic-corpus/unit-panic-eval-line_list_node-rs-2669.bin differ diff --git a/differential/algebraic-corpus/unit-shape-dnf.bin b/differential/algebraic-corpus/unit-shape-dnf.bin new file mode 100644 index 00000000..29701ac5 Binary files /dev/null and b/differential/algebraic-corpus/unit-shape-dnf.bin differ diff --git a/differential/algebraic-corpus/unit-shape-fuse.bin b/differential/algebraic-corpus/unit-shape-fuse.bin new file mode 100644 index 00000000..e03685d2 Binary files /dev/null and b/differential/algebraic-corpus/unit-shape-fuse.bin differ diff --git a/differential/algebraic-corpus/unit-shape-fuse_distributed.bin b/differential/algebraic-corpus/unit-shape-fuse_distributed.bin new file mode 100644 index 00000000..e03685d2 Binary files /dev/null and b/differential/algebraic-corpus/unit-shape-fuse_distributed.bin differ diff --git a/differential/algebraic-corpus/unit-shape-nary.bin b/differential/algebraic-corpus/unit-shape-nary.bin new file mode 100644 index 00000000..1c4333cb Binary files /dev/null and b/differential/algebraic-corpus/unit-shape-nary.bin differ diff --git a/differential/algebraic-corpus/unit-shape-nary_poly.bin b/differential/algebraic-corpus/unit-shape-nary_poly.bin new file mode 100644 index 00000000..1c4333cb Binary files /dev/null and b/differential/algebraic-corpus/unit-shape-nary_poly.bin differ diff --git a/differential/algebraic-corpus/unit-shape-pw1.bin b/differential/algebraic-corpus/unit-shape-pw1.bin new file mode 100644 index 00000000..2f47a1ad Binary files /dev/null and b/differential/algebraic-corpus/unit-shape-pw1.bin differ diff --git a/differential/algebraic-corpus/unit-shape-pw2.bin b/differential/algebraic-corpus/unit-shape-pw2.bin new file mode 100644 index 00000000..4994d4e0 Binary files /dev/null and b/differential/algebraic-corpus/unit-shape-pw2.bin differ diff --git a/differential/algebraic-corpus/unit-shape-pw3.bin b/differential/algebraic-corpus/unit-shape-pw3.bin new file mode 100644 index 00000000..c1d593eb Binary files /dev/null and b/differential/algebraic-corpus/unit-shape-pw3.bin differ diff --git a/differential/algebraic-corpus/unit-shape-pw4.bin b/differential/algebraic-corpus/unit-shape-pw4.bin new file mode 100644 index 00000000..f9d37c1d Binary files /dev/null and b/differential/algebraic-corpus/unit-shape-pw4.bin differ diff --git a/differential/algebraic-corpus/unit-shape-pw5.bin b/differential/algebraic-corpus/unit-shape-pw5.bin new file mode 100644 index 00000000..e03685d2 Binary files /dev/null and b/differential/algebraic-corpus/unit-shape-pw5.bin differ diff --git a/differential/algebraic-corpus/unit-shape-ternary.bin b/differential/algebraic-corpus/unit-shape-ternary.bin new file mode 100644 index 00000000..7938d3ab Binary files /dev/null and b/differential/algebraic-corpus/unit-shape-ternary.bin differ diff --git a/differential/algebraic-corpus/unit-values-fuse.bin b/differential/algebraic-corpus/unit-values-fuse.bin new file mode 100644 index 00000000..3d2db400 Binary files /dev/null and b/differential/algebraic-corpus/unit-values-fuse.bin differ diff --git a/differential/algebraic-corpus/unit-values-fuse_distributed.bin b/differential/algebraic-corpus/unit-values-fuse_distributed.bin new file mode 100644 index 00000000..3d2db400 Binary files /dev/null and b/differential/algebraic-corpus/unit-values-fuse_distributed.bin differ diff --git a/differential/algebraic-corpus/unit-values-model.bin b/differential/algebraic-corpus/unit-values-model.bin new file mode 100644 index 00000000..a66e7fa5 Binary files /dev/null and b/differential/algebraic-corpus/unit-values-model.bin differ diff --git a/differential/algebraic-corpus/unit-values-nary.bin b/differential/algebraic-corpus/unit-values-nary.bin new file mode 100644 index 00000000..4b2d9048 Binary files /dev/null and b/differential/algebraic-corpus/unit-values-nary.bin differ diff --git a/differential/algebraic-corpus/unit-values-pw1.bin b/differential/algebraic-corpus/unit-values-pw1.bin new file mode 100644 index 00000000..59c6d3fa Binary files /dev/null and b/differential/algebraic-corpus/unit-values-pw1.bin differ diff --git a/differential/algebraic-corpus/unit-values-pw2.bin b/differential/algebraic-corpus/unit-values-pw2.bin new file mode 100644 index 00000000..aadc1f83 Binary files /dev/null and b/differential/algebraic-corpus/unit-values-pw2.bin differ diff --git a/differential/algebraic-corpus/unit-values-pw3.bin b/differential/algebraic-corpus/unit-values-pw3.bin new file mode 100644 index 00000000..59c6d3fa Binary files /dev/null and b/differential/algebraic-corpus/unit-values-pw3.bin differ diff --git a/differential/algebraic-corpus/unit-values-pw4.bin b/differential/algebraic-corpus/unit-values-pw4.bin new file mode 100644 index 00000000..a66e7fa5 Binary files /dev/null and b/differential/algebraic-corpus/unit-values-pw4.bin differ diff --git a/differential/algebraic-corpus/unit-values-pw5.bin b/differential/algebraic-corpus/unit-values-pw5.bin new file mode 100644 index 00000000..b9f5722b Binary files /dev/null and b/differential/algebraic-corpus/unit-values-pw5.bin differ diff --git a/differential/algebraic-corpus/unit-values-ternary.bin b/differential/algebraic-corpus/unit-values-ternary.bin new file mode 100644 index 00000000..7887982e Binary files /dev/null and b/differential/algebraic-corpus/unit-values-ternary.bin differ diff --git a/differential/src/algebraic.rs b/differential/src/algebraic.rs new file mode 100644 index 00000000..0d35afb8 --- /dev/null +++ b/differential/src/algebraic.rs @@ -0,0 +1,918 @@ +//! Equivalence fuzzer for the algebraic operations. +//! +//! The other two fuzzers in this crate ask *is the answer right?* -- the Lean +//! model in `../lean` is an oracle, and `bin/pathmap_trace.rs` is diffed +//! against it. This one asks a different question: **does it matter which way +//! you compute it?** It should not, and `pathmap` offers enough different ways +//! that the question has teeth. +//! +//! Each case is one algebraic expression over a few generated operand tries, +//! evaluated by every route in `routes.rs` that applies to it -- eagerly on +//! whole maps, in place through a write zipper, as a lockstep traversal of two +//! read zippers, as a single n-ary traversal, through the DNF engine, through a +//! lazy `OverlayZipper` over a virtual trie, as a `pathmap::fuse` program over +//! trie nodes below the zipper layer, and over a flat `BTreeMap` with no trie at +//! all. Then `laws.rs` evaluates pairs of expressions that must agree whatever +//! the operands, which catches the mistakes every route shares. +//! +//! No Lean build is needed and there is no oracle: a divergence says the +//! implementations disagree, not which one is wrong. +//! +//! The wire format here is **not** the one `harness.rs` shares with +//! `PathMapModel.Fuzz`; this fuzzer has no model to stay in step with, so its +//! inputs are free to be whatever generates interesting tries. It does reuse +//! `harness::Dec` for byte decoding. +//! +//! See `../ALGEBRAIC_FUZZING.md`. + +pub mod expr; +pub mod laws; +pub mod model; +pub mod routes; +pub mod shape; +pub mod value; + +use pathmap::PathMap; +use pathmap::zipper::{ZipperMoving, ZipperWriting}; + +use crate::harness::Dec; +use expr::{Expr, Op, MAX_VARS}; +use laws::{Level, EMPTY, LAW_OPERANDS}; +use routes::Route; +use shape::{shape_of_map, show_shape, Shape, Values}; +use value::FuzzValue; + +/// Operand tries per case. Fixed rather than generated so the expression +/// generator can always name any of them, and so [`MAX_VARS`] is the only +/// bound the const-generic route dispatch has to respect. +pub const OPERANDS: usize = MAX_VARS; + +/// Upper bound on entries written into one operand. Small on purpose: the +/// interesting cases are the ones where operands overlap at a node boundary, +/// and small tries over a small alphabet collide far more often than large +/// ones. +pub const MAX_ENTRIES: usize = 7; + +/// Upper bound on a generated path's length. +pub const MAX_PATH_LEN: usize = 5; + +/// Byte decoding with the out-of-input behaviour this fuzzer wants. +/// +/// `harness::Dec` returns `None` when the input runs out, because the Lean +/// harness stops executing there. Here every input has to decode to *some* +/// case or shrinking would have to care about length, so exhaustion saturates +/// to zero instead. +pub struct Gen<'a> { + dec: Dec<'a>, + /// Size of the path alphabet. A small one makes operands share prefixes + /// and collide; the full 256 exercises wide nodes. + alphabet: u16, +} + +impl<'a> Gen<'a> { + pub fn new(bytes: &'a [u8]) -> Self { + Gen { dec: Dec { bytes, pos: 0 }, alphabet: 3 } + } + pub fn byte(&mut self) -> u8 { + self.dec.u8().unwrap_or(0) + } + pub fn modn(&mut self, m: usize) -> usize { + if m == 0 { 0 } else { self.byte() as usize % m } + } + pub fn boolean(&mut self) -> bool { + self.byte() % 2 == 1 + } + /// True with probability `pct`/100. + pub fn chance(&mut self, pct: u8) -> bool { + (self.byte() as u16 * 100 / 256) < pct as u16 + } + pub fn path_byte(&mut self) -> u8 { + (self.byte() as u16 % self.alphabet) as u8 + } + pub fn path(&mut self, max_len: usize) -> Vec { + let n = self.modn(max_len + 1); + (0..n).map(|_| self.path_byte()).collect() + } +} + +/// How one operand trie was built. Recorded so a failure report can say +/// whether the case depended on structural sharing or on node layout, which is +/// the difference between a logic bug and a representation bug. +#[derive(Clone, Copy, PartialEq, Eq, Debug)] +pub enum Build { + /// Entries written into a fresh map. + Fresh, + /// A clone of an earlier operand, then mutated. Clones share nodes, so + /// this is how a case gets two operands whose subtries are the *same* + /// allocation rather than merely equal -- the distinction several of the + /// defects in `../lean/FINDINGS.md` turned on. + CloneOf(usize), + /// The same `(path, value)` entries as an earlier operand, rewritten into a + /// fresh map in a different order. Equal content, possibly different node + /// layout and certainly no shared nodes: the counterpart to `CloneOf`, and + /// the shape that catches an operation whose answer depends on how its + /// input happens to be stored. + ReinsertOf(usize), + /// A clone of an earlier operand with `merkleize` run over it, which + /// factors equal subtries into one shared allocation. + MerkleizedOf(usize), +} + +pub struct Case { + pub expr: Expr, + pub operands: Vec>, + pub builds: Vec, + pub alphabet: u16, +} + +/// Decode a byte string into a case. Total: every input decodes. +pub fn decode(bytes: &[u8]) -> Case { + let mut g = Gen::new(bytes); + // A 3-letter alphabet is the default because collisions are the point; the + // wider ones are sampled to keep node-type coverage honest, since `pathmap` + // switches node representation on child count. + g.alphabet = match g.modn(10) { + 0 => 256, + 1 => 16, + 2 => 2, + _ => 3, + }; + let alphabet = g.alphabet; + + let mut operands: Vec> = Vec::with_capacity(OPERANDS); + let mut builds: Vec = Vec::with_capacity(OPERANDS); + for i in 0..OPERANDS { + let build = pick_build(&mut g, i); + operands.push(build_operand(&mut g, build, &operands)); + builds.push(build); + } + + let expr = gen_expr(&mut g, 3); + Case { expr, operands, builds, alphabet } +} + +fn pick_build(g: &mut Gen, i: usize) -> Build { + if i == 0 { + return Build::Fresh; + } + match g.modn(8) { + 0 | 1 | 2 | 3 => Build::Fresh, + 4 | 5 => Build::CloneOf(g.modn(i)), + 6 => Build::ReinsertOf(g.modn(i)), + _ => Build::MerkleizedOf(g.modn(i)), + } +} + +fn build_operand(g: &mut Gen, build: Build, prior: &[PathMap]) -> PathMap { + match build { + Build::Fresh => fresh(g), + Build::CloneOf(j) => { + let mut m = prior[j].clone(); + mutate(g, &mut m); + m + } + Build::ReinsertOf(j) => { + // Collect the entries, then write them back in a rotated order. + // Rotation rather than a full shuffle because it is enough to + // change which insert splits which node, and it keeps the decoding + // cost one byte. + let entries: Vec<(Vec, V)> = + shape::values_of_shape(&shape_of_map(&prior[j])).into_iter().collect(); + let mut out = PathMap::new(); + if !entries.is_empty() { + let r = g.modn(entries.len()); + let mut wz = out.write_zipper(); + for off in 0..entries.len() { + let (p, v) = &entries[(off + r) % entries.len()]; + wz.reset(); + wz.descend_to(p); + wz.set_val(v.clone()); + } + } + out + } + Build::MerkleizedOf(j) => { + let mut m = prior[j].clone(); + m.merkleize(); + mutate(g, &mut m); + m + } + } +} + +fn fresh(g: &mut Gen) -> PathMap { + let n = g.modn(MAX_ENTRIES + 1); + let mut out = PathMap::new(); + { + let mut wz = out.write_zipper(); + for _ in 0..n { + let p = g.path(MAX_PATH_LEN); + wz.reset(); + wz.descend_to(&p); + // A path written with `create_path` and no value is a dangling + // path: structure with nothing under it. Operations disagree about + // whether those survive, so they are generated on purpose and the + // comparison reports them as their own class. + if g.chance(20) { + wz.create_path(); + } else { + wz.set_val(V::generate(g)); + } + } + } + out +} + +fn mutate(g: &mut Gen, m: &mut PathMap) { + let n = g.modn(3); + let mut wz = m.write_zipper(); + for _ in 0..n { + let p = g.path(MAX_PATH_LEN); + wz.reset(); + wz.descend_to(&p); + match g.modn(4) { + 0 => { + wz.remove_val(false); + } + 1 => { + wz.create_path(); + } + 2 => { + wz.remove_branches(false); + } + _ => { + wz.set_val(V::generate(g)); + } + } + } +} + +fn gen_expr(g: &mut Gen, depth: usize) -> Expr { + // Leaf at depth 0, and otherwise often enough that the chain and DNF + // recognisers fire regularly -- a tree that is always maximally deep is + // never a chain of operands, so the whole-expression routes would almost + // never apply. + if depth == 0 || g.chance(35) { + return Expr::Var(g.modn(OPERANDS)); + } + let op = match g.modn(12) { + 0 | 1 | 2 | 3 => Op::Join, + 4 | 5 | 6 => Op::Meet, + 7 | 8 => Op::Subtract, + 9 | 10 => Op::SymDiff, + _ => Op::Restrict, + }; + Expr::bin(op, gen_expr(g, depth - 1), gen_expr(g, depth - 1)) +} + +// ------------------------------------------------------------- comparison + +#[derive(Clone, Copy, PartialEq, Eq, Debug)] +pub enum Class { + /// Two routes put different values on a path, or disagree about whether a + /// path carries one. Settled semantics: one of them is wrong. + Values, + /// Two routes agree on every value and differ only in dangling paths -- + /// structure with nothing under it. Unsettled semantics (see + /// `../SPEC_WARTS.md`), so this is reported apart from `Values` rather than + /// mixed in with it. + Shape, + /// An identity that must hold whatever the operands are does not. + Law, +} + +impl Class { + pub fn tag(self) -> &'static str { + match self { + Class::Values => "values", + Class::Shape => "shape", + Class::Law => "law", + } + } +} + +pub struct Divergence { + pub class: Class, + /// Stable short key for grouping findings across runs: the class and the + /// route, and nothing else. + /// + /// Coarse on purpose. An earlier version appended the operators the + /// expression used, which looked more informative and was much worse: one + /// root cause in `meet` produced dozens of signatures because it surfaced + /// under every combination of operators that happened to contain a meet, + /// and a known-findings table over them was unmaintainable. The operators, + /// the operands and the diff all live in `detail`; the signature's only job + /// is to collapse a million inputs onto a handful of lines. + pub signature: String, + pub detail: String, +} + +/// Evaluate every applicable route and every law, and return what disagrees. +/// +/// The baseline every route is compared against is `Pointwise(0)` -- the whole +/// expression through `PathMap::join`/`meet`/`subtract`/`restrict`. Those are +/// the oldest and most heavily used entry points in the crate, which makes them +/// the right thing to hold still, though the choice only affects which side of +/// a disagreement gets named, not whether it is found. +pub fn check(case: &Case) -> Vec { + let mut out = Vec::new(); + + let baseline_route = Route::Pointwise(0); + let baseline = routes::eval(baseline_route, &case.expr, &case.operands) + .expect("route 0 is the whole-map operations, which apply to everything"); + let base_name = baseline_route.name(&case.expr); + + // The model is computed up front so every divergence can say which side it + // backs. Worth the one extra evaluation: the baseline is `PathMap::join` + // and friends, which have defects of their own, so "route X disagrees with + // the baseline" on its own points at the wrong file about as often as the + // right one. The model has no trie and no node layout, so when it sides + // with the route, the baseline is where to look. + let model = routes::eval(Route::Model, &case.expr, &case.operands) + .expect("the model route applies to every expression"); + + for route in Route::all() { + if route == baseline_route { + continue; + } + let Some(got) = routes::eval(route, &case.expr, &case.operands) else { continue }; + let name = route.name(&case.expr); + + if got.values != baseline.values { + out.push(Divergence { + class: Class::Values, + signature: signature::("values", &route_key::(route)), + detail: format!( + "{} vs {name} evaluating {}: {}\n {base_name}: {}\n {name}: {}\n {}", + base_name, + case.expr, + shape::first_values_diff(&baseline.values, &got.values).unwrap_or_default(), + shape::show_values(&baseline.values), + shape::show_values(&got.values), + model_sides_with(&model.values, &baseline.values, &got.values, &base_name, &name), + ), + }); + // One class per route is enough; a value divergence will usually + // show up as a shape divergence too, and reporting both would + // double every finding. + continue; + } + + if let (Some(bs), Some(gs)) = (&baseline.shape, &got.shape) { + if bs != gs { + out.push(Divergence { + class: Class::Shape, + signature: signature::("shape", &route_key::(route)), + detail: format!( + "{} vs {name} evaluating {}: {}\n {base_name}: {}\n {name}: {}", + base_name, + case.expr, + shape::first_shape_diff(bs, gs).unwrap_or_default(), + show_shape(bs), + show_shape(gs), + ), + }); + } + } + } + + out.extend(check_laws(case)); + out +} + +/// Evaluate each law's two sides and report the ones that disagree. +/// +/// Laws run through the baseline route only. A law that fails under one route +/// and holds under another is already a route disagreement, which the loop +/// above reports; running every law through every route would multiply the cost +/// of a case by the number of laws for no new coverage. +pub fn check_laws(case: &Case) -> Vec { + // Operands 0..3 from the case, then the empty trie, which is what lets a + // law state a unit or annihilator. + let mut ops: Vec> = (0..EMPTY).map(|i| case.operands[i].clone()).collect(); + ops.push(PathMap::new()); + debug_assert_eq!(ops.len(), LAW_OPERANDS); + + let mut out = Vec::new(); + for law in laws::laws::() { + let l = routes::eval(Route::Pointwise(0), &law.lhs, &ops).unwrap(); + let r = routes::eval(Route::Pointwise(0), &law.rhs, &ops).unwrap(); + let (ok, detail) = match law.level { + Level::Values => ( + l.values == r.values, + format!( + "{}\n lhs {}: {}\n rhs {}: {}", + shape::first_values_diff(&l.values, &r.values).unwrap_or_default(), + law.lhs, + shape::show_values(&l.values), + law.rhs, + shape::show_values(&r.values), + ), + ), + Level::Paths => { + // Compare the value-carrying paths only. Comparing every path + // in the shape would drag the dangling-path question into laws + // that are not about it. + let lk: Vec<&Vec> = l.values.keys().collect(); + let rk: Vec<&Vec> = r.values.keys().collect(); + ( + lk == rk, + format!( + "lhs {}: {}\n rhs {}: {}", + law.lhs, + shape::show_values(&l.values), + law.rhs, + shape::show_values(&r.values), + ), + ) + } + }; + if !ok { + out.push(Divergence { + class: Class::Law, + signature: signature::("law", law.name), + detail: format!("{} ({:?}): {detail}", law.name, law.level), + }); + } + } + out +} + +/// Which side of a value divergence the reference model backs, as one line for +/// the report. +/// +/// Neither side being backed is the interesting case: it means the model +/// disagrees with both, so the defect is unlikely to be in either route's +/// traversal and is more likely in a shared primitive -- or in the model, which +/// is worth suspecting too. +fn model_sides_with( + model: &Values, + baseline: &Values, + got: &Values, + base_name: &str, + name: &str, +) -> String { + match (model == baseline, model == got) { + (true, true) => "model: agrees with both (unreachable)".to_string(), + (true, false) => format!("model: sides with {base_name}, so {name} is the odd one out"), + (false, true) => format!("model: sides with {name}, so {base_name} is the odd one out"), + (false, false) => format!( + "model: agrees with neither -- {}", + shape::show_values(model) + ), + } +} + +/// Signatures are prefixed with the value type, so the two instantiations never +/// collide in one report and the difference between them is readable directly. +pub fn signature(class: &str, rest: &str) -> String { + format!("{}:{class}:{rest}", V::NAME) +} + +fn route_key(r: Route) -> String { + match r { + Route::Pointwise(k) => format!("pw{k}"), + _ => r.name(&Expr::Var(0)), + } +} + +// ---------------------------------------------------------------- known findings + +/// A finding that already reproduces on `master` and has a reproducer of its +/// own, so a run that only hits these is not a regression. +pub struct Known { + pub signature: &'static str, + /// Which defect it traces to. Several signatures share one entry: a single + /// wrong value inside `join` surfaces on every route that reaches a join + /// and in every law that mentions one, so the table maps many signatures + /// onto few causes. + pub cause: &'static str, +} + +/// Findings confirmed on `master`, with the defect each traces to. +/// `bin/alg_bug_repros.rs` reproduces every cause in a dozen lines, without the +/// fuzzer; run it to see which still stand. +/// +/// This table decides the **exit status** and nothing else. Counts are always +/// printed, known and unknown alike, so a known defect that starts firing ten +/// times more often is still visible even though it does not turn the run red. +/// `--strict` ignores the table entirely. +/// +/// # The causes +/// +/// 1. **Value bias by node layout** (`bias`). `pjoin` on `u64` is +/// `left_biased_pjoin` and `pmeet` is `Identity(SELF_IDENT)`, so where both +/// operands carry a value the *left* one must win. `PathMap::join` and +/// `PathMap::meet` take the right one when the two operands' nodes are laid +/// out differently -- in the reproducer, because one side has a chain of +/// dangling descendants below the shared path. Every zipper route gets this +/// right, so it shows up as *laws* failing and as the `model` route +/// disagreeing, not as one route out of step with the others: the defect is +/// in the baseline the others are compared against. +/// +/// 2. **`join` loses a value across shared structure** (`loss`). With `b` a +/// clone of `a` plus one extra value, `a | b` drops that value and `b | a` +/// keeps it. A join is a least upper bound, so no ordering may lose a path; +/// this is the one finding that needs no argument about value bias. It +/// needs the operands to *share nodes* -- rebuilding `b`'s entries into a +/// fresh map makes it go away -- which is why the generator clones and +/// merkleizes operands instead of only writing them fresh. +/// +/// 3. **Root values lost by the write-zipper forms** (`root`). `join_into` +/// into an empty destination drops the source's root value, and `meet_2` +/// drops root values outright. These are routes disagreeing with the +/// baseline in the ordinary way. +/// +/// 4. **Dangling paths** (`dangling`). The lockstep traversals in +/// `experimental::zipper_algebra` discard dangling structure; `PathMap`'s +/// whole-map operations and the write-zipper forms preserve it. Unsettled rather than +/// wrong -- see `../SPEC_WARTS.md` -- hence its own class, `shape`, which +/// does not fail a run unless `--shape` says so. +/// +/// 5. **`merkleize` panics on dangling-only structure** (`merkleize`). Not an +/// algebraic defect: it fires while the operands are still being written, +/// before any operation runs, which is what the `build` in its signature +/// means. +const BIAS: &str = "value bias by node layout, u64-only (repro 3)"; +const LOSS: &str = "join loses a value across shared structure (repro 4)"; +const ROOT: &str = "write-zipper forms lose root values (repros 1, 2)"; +const DANGLING: &str = "zipper traversals drop dangling paths, map ops keep them (repro 9)"; +const MERKLEIZE: &str = "merkleize panics on dangling-only structure (repro 5)"; +/// Re-nesting a join moves which operand is on the left *and* which pair of +/// tries meets a shared node first, so both cause 1 and cause 2 reach these. +/// Under the lawful type only cause 2 survives, which is why the counts collapse. +const BIAS_OR_LOSS: &str = "value bias or lost value (repros 3, 4)"; +/// `fuse`'s `Xor` is `(l \\ r) | (r \\ l)`. Cause 2 reaches the join on the end of +/// that construction. Under `u64` it *also* disagrees with `zipper_sym_diff`, +/// because the two standard formulas for symmetric difference are only equal in a +/// real lattice -- which is a fact about `u64`, not about either implementation. +const FUSE_XOR: &str = "fuse Xor: cause 2, amplified under u64 by its non-lattice (repros 7, 8)"; + +pub const KNOWN: &[Known] = &[ + // ---------------------------------------------------------------- u64 + // Root values lost by the write-zipper forms. Value-type-independent. + Known { signature: "u64:values:pw1", cause: ROOT }, + Known { signature: "u64:values:pw2", cause: ROOT }, + Known { signature: "u64:values:pw3", cause: ROOT }, + // Everything below here on the u64 side is the bias, which the lawful type + // mostly cannot see: under a commutative join, picking the wrong operand + // only shows where one operand already contains the other. + Known { signature: "u64:values:pw4", cause: BIAS }, + Known { signature: "u64:values:pw5", cause: BIAS }, + Known { signature: "u64:values:ternary", cause: BIAS }, + Known { signature: "u64:values:nary", cause: BIAS }, + Known { signature: "u64:values:nary_poly", cause: BIAS }, + Known { signature: "u64:values:dnf", cause: BIAS }, + Known { signature: "u64:values:model", cause: BIAS }, + Known { signature: "u64:values:fuse", cause: FUSE_XOR }, + Known { signature: "u64:values:fuse_distributed", cause: FUSE_XOR }, + Known { signature: "u64:shape:pw1", cause: DANGLING }, + Known { signature: "u64:shape:pw2", cause: DANGLING }, + Known { signature: "u64:shape:pw3", cause: DANGLING }, + Known { signature: "u64:shape:pw4", cause: DANGLING }, + Known { signature: "u64:shape:pw5", cause: DANGLING }, + Known { signature: "u64:shape:ternary", cause: DANGLING }, + Known { signature: "u64:shape:nary", cause: DANGLING }, + Known { signature: "u64:shape:nary_poly", cause: DANGLING }, + Known { signature: "u64:shape:dnf", cause: DANGLING }, + Known { signature: "u64:shape:fuse", cause: DANGLING }, + Known { signature: "u64:shape:fuse_distributed", cause: DANGLING }, + Known { signature: "u64:law:join-associative", cause: BIAS_OR_LOSS }, + Known { signature: "u64:law:join-distributes-over-meet", cause: BIAS_OR_LOSS }, + Known { signature: "u64:law:majority-is-pairwise-meets", cause: BIAS_OR_LOSS }, + Known { signature: "u64:law:join-commutative", cause: LOSS }, + // These four fire only for u64: they need join and meet to be different + // functions, and for u64 they are the same one. + Known { signature: "u64:law:meet-associative", cause: BIAS }, + Known { signature: "u64:law:meet-distributes-over-join", cause: BIAS }, + Known { signature: "u64:law:absorb-join-meet", cause: BIAS }, + Known { signature: "u64:law:sym-diff-is-join-minus-meet", cause: BIAS }, + Known { signature: "u64:panic:build:line_list_node.rs:1745", cause: MERKLEIZE }, + Known { signature: "u64:panic:eval:line_list_node.rs:2669", cause: LOSS }, + Known { signature: "u64:panic:eval:line_list_node.rs:2720", cause: LOSS }, + Known { signature: "u64:panic:eval:dense_byte_node.rs:2080", cause: LOSS }, + + // ---------------------------------------------------------------- bits + // The lawful type. Everything here is a real defect: there is no value + // bias to blame, because `a | b` does not depend on operand order. + Known { signature: "bits:values:pw1", cause: ROOT }, + Known { signature: "bits:values:pw2", cause: ROOT }, + Known { signature: "bits:values:pw3", cause: ROOT }, + Known { signature: "bits:values:pw5", cause: ROOT }, + // Rare under the lawful type, and cause 2 every time: the law residues all + // shrink to a value present on one side of an identity and absent on the + // other, which is a lost value rather than a misplaced one. + Known { signature: "bits:values:pw4", cause: LOSS }, + // Fires about once per three million cases for each lawful type, and the + // model sides with the route, so it is the baseline that lost the value. + Known { signature: "bits:values:ternary", cause: LOSS }, + Known { signature: "bits:values:nary", cause: LOSS }, + Known { signature: "bits:values:nary_poly", cause: LOSS }, + Known { signature: "bits:values:dnf", cause: LOSS }, + Known { signature: "bits:values:model", cause: LOSS }, + Known { signature: "bits:values:fuse", cause: LOSS }, + Known { signature: "bits:values:fuse_distributed", cause: LOSS }, + Known { signature: "bits:shape:pw1", cause: DANGLING }, + Known { signature: "bits:shape:pw2", cause: DANGLING }, + Known { signature: "bits:shape:pw3", cause: DANGLING }, + Known { signature: "bits:shape:pw4", cause: DANGLING }, + Known { signature: "bits:shape:pw5", cause: DANGLING }, + Known { signature: "bits:shape:ternary", cause: DANGLING }, + Known { signature: "bits:shape:nary", cause: DANGLING }, + Known { signature: "bits:shape:nary_poly", cause: DANGLING }, + Known { signature: "bits:shape:dnf", cause: DANGLING }, + Known { signature: "bits:shape:fuse", cause: DANGLING }, + Known { signature: "bits:shape:fuse_distributed", cause: DANGLING }, + Known { signature: "bits:law:join-associative", cause: LOSS }, + Known { signature: "bits:law:join-commutative", cause: LOSS }, + Known { signature: "bits:law:join-distributes-over-meet", cause: LOSS }, + Known { signature: "bits:law:sym-diff-is-join-minus-meet", cause: LOSS }, + Known { signature: "bits:law:majority-is-pairwise-meets", cause: LOSS }, + Known { signature: "bits:panic:build:line_list_node.rs:1745", cause: MERKLEIZE }, + Known { signature: "bits:panic:eval:line_list_node.rs:2669", cause: LOSS }, + Known { signature: "bits:panic:eval:line_list_node.rs:2720", cause: LOSS }, + Known { signature: "bits:panic:eval:dense_byte_node.rs:2080", cause: LOSS }, + // ---------------------------------------------------------------- unit + // `PathMap<()>`: the set case, and lawful. Nothing here can be a value + // bias, because there is no value to misplace -- so every entry is either a + // lost path or the dangling-path question. It confirms the real defects + // independently of `bits`. + Known { signature: "unit:values:pw1", cause: ROOT }, + Known { signature: "unit:values:pw2", cause: ROOT }, + Known { signature: "unit:values:pw3", cause: ROOT }, + Known { signature: "unit:values:pw5", cause: ROOT }, + Known { signature: "unit:values:pw4", cause: LOSS }, + Known { signature: "unit:values:nary", cause: LOSS }, + Known { signature: "unit:values:nary_poly", cause: LOSS }, + Known { signature: "unit:values:dnf", cause: LOSS }, + Known { signature: "unit:values:model", cause: LOSS }, + Known { signature: "unit:values:fuse", cause: LOSS }, + Known { signature: "unit:values:fuse_distributed", cause: LOSS }, + Known { signature: "unit:shape:pw1", cause: DANGLING }, + Known { signature: "unit:shape:pw2", cause: DANGLING }, + Known { signature: "unit:shape:pw3", cause: DANGLING }, + Known { signature: "unit:shape:pw4", cause: DANGLING }, + Known { signature: "unit:shape:pw5", cause: DANGLING }, + Known { signature: "unit:shape:ternary", cause: DANGLING }, + Known { signature: "unit:shape:nary", cause: DANGLING }, + Known { signature: "unit:shape:nary_poly", cause: DANGLING }, + Known { signature: "unit:shape:dnf", cause: DANGLING }, + Known { signature: "unit:shape:fuse", cause: DANGLING }, + Known { signature: "unit:shape:fuse_distributed", cause: DANGLING }, + Known { signature: "unit:law:join-associative", cause: LOSS }, + Known { signature: "unit:law:join-commutative", cause: LOSS }, + Known { signature: "unit:law:join-distributes-over-meet", cause: LOSS }, + Known { signature: "unit:law:sym-diff-is-join-minus-meet", cause: LOSS }, + Known { signature: "unit:law:majority-is-pairwise-meets", cause: LOSS }, + Known { signature: "unit:panic:build:line_list_node.rs:1745", cause: MERKLEIZE }, + Known { signature: "unit:panic:eval:line_list_node.rs:2669", cause: LOSS }, + Known { signature: "unit:panic:eval:dense_byte_node.rs:2080", cause: LOSS }, + // Fires roughly once per million random cases, and the corpus reproduces it + // for all three types. + Known { signature: "unit:panic:eval:line_list_node.rs:2720", cause: LOSS }, + // Two laws that fire only under `unit`, both once per couple of million + // cases, and both cause 2. `unit` reaches it where the other types do not + // because every value is identical, so `merkleize` and `clone` share far + // more structure and the dangling-only operand that triggers the loss is + // easier to generate. + Known { signature: "unit:law:meet-distributes-over-join", cause: LOSS }, + // One of the four identities that are only checked for a lawful value type. + // It failing is still cause 2, not a bad identity: the shrunk case has a + // dangling-only `b` and a `c` that is `b` plus one value, so `b | c` is + // exactly repro 4. + Known { signature: "unit:law:subtract-over-join", cause: LOSS }, + Known { signature: "unit:values:ternary", cause: LOSS }, + + // Of the four identities in `laws::lawful_only` -- checked only for a lawful + // value type -- three have never failed: subtract-over-meet, + // subtract-is-subtract-meet and sym-diff-associative. They are the + // strongest laws the harness has, and they are deliberately absent from this + // table so that one of them firing is news. The fourth, + // subtract-over-join, fires once per couple of million cases under `unit`, + // and is cause 2 rather than a bad identity. +]; + +pub fn known(signature: &str) -> Option<&'static Known> { + KNOWN.iter().find(|k| k.signature == signature) +} + +// ------------------------------------------------------------------ running + +/// Which half of a case was running when it panicked. +/// +/// Worth separating, because the two mean different things. `Build` is a panic +/// while *writing the operand tries* -- plain `set_val`, `create_path`, +/// `remove_branches`, `merkleize` on a write zipper, before any algebra has +/// run. That is a crash in the write path and belongs to the crash fuzzer; +/// this fuzzer just happens to reach it. `Eval` is a panic inside an algebraic +/// operation, which is this fuzzer's own business. +#[derive(Clone, Copy, PartialEq, Eq, Debug)] +pub enum Phase { + Build, + Eval, +} + +impl Phase { + pub fn tag(self) -> &'static str { + match self { + Phase::Build => "build", + Phase::Eval => "eval", + } + } +} + +/// What one input produced. A panic is kept distinct from a divergence: it +/// means a route never got as far as producing an answer, so there is nothing +/// to compare and the finding is the crash itself. +pub enum Outcome { + Clean, + Diverged(Vec), + Panicked(Phase, String, String), +} + +std::thread_local! { + /// Where the last panic came from. The payload of an `unwrap` on `None` + /// carries no location, and the location is the whole value of a crash + /// signature -- without it every distinct panic site collapses onto one + /// line called "panic". A hook is the only way to see it. + static PANIC_SITE: core::cell::RefCell = + const { core::cell::RefCell::new(String::new()) }; +} + +/// Replace the panic hook with one that records the panic site and prints +/// nothing. +/// +/// Both halves matter for a long run: the default hook would print a backtrace +/// notice per panicking case and drown the output, and `catch_unwind` alone +/// cannot see where the panic came from. +pub fn install_panic_hook() { + std::panic::set_hook(Box::new(|info| { + let site = info + .location() + .map(|l| { + // Just the file name and line: the absolute path would make + // signatures depend on where the checkout lives. + let f = l.file(); + let f = f.rsplit('/').next().unwrap_or(f); + format!("{f}:{}", l.line()) + }) + .unwrap_or_else(|| "?".to_string()); + PANIC_SITE.with(|s| *s.borrow_mut() = site); + })); +} + +fn panic_msg(e: Box) -> (String, String) { + let msg = e + .downcast_ref::() + .cloned() + .or_else(|| e.downcast_ref::<&str>().map(|s| s.to_string())) + .unwrap_or_else(|| "".to_string()); + let site = PANIC_SITE.with(|s| s.borrow().clone()); + (site, msg) +} + +/// Decode an input, run every route and every law over it, and say what +/// disagreed. +/// +/// Two `catch_unwind`s rather than one, so a crash can say which phase it was +/// in. The case has to outlive the first, hence the separation. +pub fn run(bytes: &[u8]) -> Outcome { + let case = match std::panic::catch_unwind(std::panic::AssertUnwindSafe(|| decode::(bytes))) { + Err(e) => { + let (site, msg) = panic_msg(e); + return Outcome::Panicked(Phase::Build, site, msg); + } + Ok(c) => c, + }; + match std::panic::catch_unwind(std::panic::AssertUnwindSafe(|| check(&case))) { + Err(e) => { + let (site, msg) = panic_msg(e); + Outcome::Panicked(Phase::Eval, site, msg) + } + Ok(divs) if divs.is_empty() => Outcome::Clean, + Ok(divs) => Outcome::Diverged(divs), + } +} + +/// Signatures an input produces: the grouping keys, without the detail. Also +/// the invariant the shrinker preserves. +/// Every value type the fuzzer runs, by name. +/// +/// This list and [`run_all`] are the only two places that know which types +/// exist; the driver stays generic over them and reads the type back off a +/// signature's first field. +pub const VALUE_TYPES: &[&str] = &[ + ::NAME, + ::NAME, + <() as FuzzValue>::NAME, +]; + +/// Run one input under every value type. +/// +/// Both, every time, and that is the point: a finding under `u64` and not under +/// `bits` is an artefact of `u64`'s degenerate lattice instance, and one under +/// both -- or under `bits` alone -- is a defect in the crate. Checking only the +/// lawful type would be cheaper and would lose the comparison. +pub fn run_all(bytes: &[u8], f: &mut impl FnMut(&'static str, Outcome)) { + f(::NAME, run::(bytes)); + f(::NAME, run::(bytes)); + f(<() as FuzzValue>::NAME, run::<()>(bytes)); +} + +/// Signatures of one outcome, which for a panic has to be built here because +/// the phase and site are not a `Divergence`. +pub fn outcome_signatures(type_name: &str, outcome: &Outcome) -> Vec { + match outcome { + Outcome::Clean => Vec::new(), + Outcome::Diverged(d) => d.iter().map(|d| d.signature.clone()).collect(), + Outcome::Panicked(p, site, _) => vec![panic_signature(type_name, *p, site)], + } +} + +pub fn panic_signature(type_name: &str, phase: Phase, site: &str) -> String { + format!("{type_name}:panic:{}:{site}", phase.tag()) +} + +/// Every signature an input produces, across all value types. Also the +/// invariant the shrinker preserves. +pub fn signatures(bytes: &[u8]) -> Vec { + let mut out = Vec::new(); + run_all(bytes, &mut |name, outcome| { + out.extend(outcome_signatures(name, &outcome)); + }); + out +} + +/// The value type named in a signature's first field. +pub fn value_type_of(signature: &str) -> &str { + signature.split(':').next().unwrap_or("") +} + +/// Render a case under the value type named by `type_name`. +pub fn describe_as(type_name: &str, bytes: &[u8]) -> String { + if type_name == ::NAME { + describe(&decode::(bytes)) + } else if type_name == <() as FuzzValue>::NAME { + describe(&decode::<()>(bytes)) + } else { + describe(&decode::(bytes)) + } +} + +/// Reproducible input generation, so a seed names a run. +/// +/// xorshift64*, rather than `rand`: this crate depends on nothing but `pathmap` +/// and is worth keeping that way. +pub struct Rng(pub u64); + +impl Rng { + /// Derive a stream for job `job` of a run seeded with `seed`. The odd + /// multiplier keeps jobs from sharing a stream. + pub fn for_job(seed: u64, job: usize) -> Rng { + Rng((seed + .wrapping_mul(0x9E37_79B9_7F4A_7C15) + .wrapping_add(job as u64 * 0x1234_5679)) + | 1) + } + + pub fn next(&mut self) -> u64 { + self.0 ^= self.0 >> 12; + self.0 ^= self.0 << 25; + self.0 ^= self.0 >> 27; + self.0.wrapping_mul(0x2545_F491_4F6C_DD1D) + } + + /// An input long enough that the decoder rarely runs out mid-case -- which + /// would saturate the rest to zeros and waste the draw -- and short enough + /// to shrink quickly. + pub fn input(&mut self) -> Vec { + let n = 48 + (self.next() % 96) as usize; + (0..n).map(|_| (self.next() >> 24) as u8).collect() + } +} + +/// Human-readable rendering of a case, for a failure report and for replay. +pub fn describe(case: &Case) -> String { + let mut s = String::new(); + s.push_str(&format!("values: {}\n", V::NAME)); + s.push_str(&format!("expr: {}\n", case.expr)); + s.push_str(&format!("alphabet: {}\n", case.alphabet)); + for (i, (m, b)) in case.operands.iter().zip(&case.builds).enumerate() { + let sh: Shape = shape_of_map(m); + s.push_str(&format!( + "operand {}: {:?}\n {}\n", + (b'a' + i as u8) as char, + b, + show_shape(&sh) + )); + } + s +} + +/// Values of each operand, for a report that only needs the settled part. +pub fn operand_values(case: &Case) -> Vec> { + case.operands + .iter() + .map(|m| shape::values_of_shape(&shape_of_map(m))) + .collect() +} diff --git a/differential/src/algebraic/expr.rs b/differential/src/algebraic/expr.rs new file mode 100644 index 00000000..7fa2d9ac --- /dev/null +++ b/differential/src/algebraic/expr.rs @@ -0,0 +1,218 @@ +//! The expression language the fuzzer evaluates. +//! +//! An expression is a tree over a handful of generated operand tries. It is +//! deliberately small: the point is not to cover a rich language but to give +//! each expression as many *distinct implementation routes* as possible, and a +//! route only exists where the crate offers one. So the operator set is +//! exactly the crate's algebra -- join, meet, subtract, symmetric difference, +//! restrict -- and the interesting structure is the shape of the tree, because +//! that is what decides which routes apply: +//! +//! * any tree at all can be walked bottom-up with two-operand calls, so the +//! pairwise routes always apply; +//! * a chain of three of the same associative operator unlocks the `*3` forms; +//! * a chain of `n` unlocks the n-ary forms; +//! * a join of meets of operands is a DNF, which unlocks +//! [`zipper_merge_dnf`](pathmap::experimental::zipper_algebra::zipper_merge_dnf). +//! +//! [`Expr::dnf`] and [`Expr::chain`] are the recognisers for the last three. + +use core::fmt; + +/// Maximum operand tries in a case. Bounded because the n-ary and DNF routes +/// are const-generic over it and have to be dispatched by a `match` over +/// monomorphisations; see `routes::nary`. +pub const MAX_VARS: usize = 4; + +/// Maximum DNF clauses dispatched to `zipper_merge_dnf`. +pub const MAX_CLAUSES: usize = 4; + +#[derive(Clone, Copy, PartialEq, Eq, Debug)] +pub enum Op { + Join, + Meet, + Subtract, + SymDiff, + Restrict, +} + +impl Op { + pub const ALL: [Op; 5] = [Op::Join, Op::Meet, Op::Subtract, Op::SymDiff, Op::Restrict]; + + pub fn sym(self) -> &'static str { + match self { + Op::Join => "|", + Op::Meet => "&", + Op::Subtract => "-", + Op::SymDiff => "^", + Op::Restrict => "/", + } + } + + /// Whether `(a op b) op c == a op (b op c)` holds, which is what makes a + /// chain of this operator collapsible to one n-ary call. + /// + /// Subtract is listed as associative in the sense the n-ary routes mean it: + /// `zipper_n_subtract` is documented as *left*-associative, so it matches a + /// left-nested chain only. [`Expr::chain`] enforces that nesting. + pub fn chainable(self) -> bool { + matches!(self, Op::Join | Op::Meet | Op::SymDiff | Op::Subtract) + } + + /// Whether a chain of this operator may nest to the right as well as the + /// left, and still mean what the n-ary call computes. + /// + /// Join and meet may: `pjoin` and `pmeet` on `u64` are left-biased, so both + /// nestings select the leftmost present operand's value and agree with the + /// left fold the n-ary routes perform. + /// + /// Subtract and symmetric difference may not. Subtract obviously -- `a - + /// (b - c)` is a different function. Symmetric difference less obviously: + /// the n-ary form folds values left, so for root values `a = 2`, `b = 1`, + /// `a ^ (a ^ b)` is `a ^ nothing = 2` while the fold is `(2 ^ 2) ^ 1 = 1`. + /// Both are defensible; they are not equal, so a right-nested symmetric + /// difference is not a chain. `laws.rs` states the associativity that does + /// hold, which is on paths. + pub fn right_nestable(self) -> bool { + matches!(self, Op::Join | Op::Meet) + } +} + +#[derive(Clone, PartialEq, Eq, Debug)] +pub enum Expr { + Var(usize), + Bin(Op, Box, Box), +} + +impl Expr { + pub fn bin(op: Op, l: Expr, r: Expr) -> Expr { + Expr::Bin(op, Box::new(l), Box::new(r)) + } + + pub fn nodes(&self) -> usize { + match self { + Expr::Var(_) => 1, + Expr::Bin(_, l, r) => 1 + l.nodes() + r.nodes(), + } + } + + /// Operand indices the expression mentions, ascending. + pub fn vars(&self) -> Vec { + let mut v = Vec::new(); + self.collect_vars(&mut v); + v.sort(); + v.dedup(); + v + } + + fn collect_vars(&self, out: &mut Vec) { + match self { + Expr::Var(i) => out.push(*i), + Expr::Bin(_, l, r) => { + l.collect_vars(out); + r.collect_vars(out); + } + } + } + + /// If the whole expression is a chain of one chainable operator over bare + /// operands, return that operator and the operands in evaluation order. + /// + /// Only bare operands qualify, not arbitrary subexpressions: the n-ary + /// routes take read zippers, and a subexpression would have to be + /// materialised into a temporary trie first, at which point the route is no + /// longer testing the n-ary call against the same inputs the pairwise route + /// saw. Keeping it to operands keeps the comparison exact. + pub fn chain(&self) -> Option<(Op, Vec)> { + let Expr::Bin(op, _, _) = self else { return None }; + if !op.chainable() { + return None; + } + let mut operands = Vec::new(); + self.collect_chain(*op, &mut operands).then_some((*op, operands)) + } + + fn collect_chain(&self, op: Op, out: &mut Vec) -> bool { + match self { + Expr::Var(i) => { + out.push(*i); + true + } + Expr::Bin(o, l, r) if *o == op => { + // The left spine may always recurse. The right spine may only + // recurse for operators that nest both ways, so `a - (b - c)` + // is not mistaken for the chain `a - b - c`. + if !l.collect_chain(op, out) { + return false; + } + match &**r { + Expr::Var(i) => { + out.push(*i); + true + } + Expr::Bin(..) => op.right_nestable() && r.collect_chain(op, out), + } + } + Expr::Bin(..) => false, + } + } + + /// If the expression is a join of meets of operands, return one bitmask of + /// operand indices per clause. + /// + /// This is the form `zipper_merge_dnf` evaluates directly. A clause is a + /// *set*, so `a & a` collapses to `a`; that is sound because meet is + /// idempotent, which is itself one of the laws checked in `laws.rs`. + pub fn dnf(&self) -> Option> { + match self { + Expr::Bin(Op::Join, l, r) => { + let mut cs = l.dnf()?; + cs.extend(r.dnf()?); + Some(cs) + } + _ => Some(vec![self.meet_mask()?]), + } + } + + /// If the expression is a meet of operands, return their index bitmask. + /// + /// Rejects a meet whose operands are not in ascending index order, even + /// though the bitmask would be the same. A [`Clause`] is a *set*: it + /// records which zippers take part, not in what order, and + /// `zipper_merge_dnf` meets a clause's members in slot order, which is + /// ascending operand index. Because `pmeet` on `u64` is left-biased, `b & + /// a` and `a & b` carry different values, so only one of them is what the + /// clause actually computes. Returning a mask for the other would make the + /// DNF route report a divergence that is the route's own fault. + /// + /// [`Clause`]: pathmap::experimental::zipper_algebra::Clause + fn meet_mask(&self) -> Option { + let mut vs = Vec::new(); + self.meet_vars(&mut vs).then_some(())?; + if vs.windows(2).any(|w| w[0] > w[1]) { + return None; + } + Some(vs.iter().fold(0u64, |m, i| m | 1u64 << i)) + } + + /// Operands of a meet-only subexpression, left to right. + fn meet_vars(&self, out: &mut Vec) -> bool { + match self { + Expr::Var(i) => { + out.push(*i); + true + } + Expr::Bin(Op::Meet, l, r) => l.meet_vars(out) && r.meet_vars(out), + _ => false, + } + } +} + +impl fmt::Display for Expr { + fn fmt(&self, f: &mut fmt::Formatter<'_>) -> fmt::Result { + match self { + Expr::Var(i) => write!(f, "{}", (b'a' + *i as u8) as char), + Expr::Bin(op, l, r) => write!(f, "({l} {} {r})", op.sym()), + } + } +} diff --git a/differential/src/algebraic/laws.rs b/differential/src/algebraic/laws.rs new file mode 100644 index 00000000..221991fb --- /dev/null +++ b/differential/src/algebraic/laws.rs @@ -0,0 +1,243 @@ +//! Identities that must hold whatever the operands are. +//! +//! The route comparison in `routes.rs` catches an implementation that disagrees +//! with its siblings. It cannot catch a mistake they all share. Laws are the +//! other half: each one is two *different expressions* that must evaluate to +//! the same trie, so a wrong answer is visible even when every route computes +//! it the same wrong way. +//! +//! A law is written as a pair of [`Expr`]s and evaluated by the ordinary route +//! machinery, which keeps this file declarative and means a law automatically +//! inherits whatever the expression evaluator can do. +//! +//! # Strength depends on the value type +//! +//! [`laws`] is parameterised by the value type, and returns a *stronger* set for +//! one whose instances actually form a distributive lattice with a relative +//! complement -- see [`FuzzValue::LAWFUL`]. Three things change: +//! +//! * The laws marked [`Level::Paths`] are promoted to [`Level::Values`]. They +//! are weakened for `u64` only because its `pjoin` and `pmeet` both return the +//! left operand, so swapping the operands swaps the result's value and +//! commutativity cannot hold on values there. +//! +//! * Three further identities are added, listed in [`lawful_only`]. They are +//! laws in any distributive lattice and fail for `u64`, again because join and +//! meet have collapsed into one function. +//! +//! * Symmetric difference becomes associative on values, not merely on paths. +//! +//! So the difference between the two sets is a measurement: a law that holds for +//! `bits` and fails for `u64` is telling you about `u64`, and one that fails for +//! `bits` is telling you about the crate. That split is the whole reason for +//! running both. + +use super::expr::{Expr, Op}; +use super::value::FuzzValue; + +/// Operand slot holding the empty trie, appended after the case's own +/// operands so identities can mention it. See [`LAW_OPERANDS`]. +pub const EMPTY: usize = 3; + +/// Operands a law may mention: three from the case, then the empty trie. +pub const LAW_OPERANDS: usize = 4; + +/// How much of the result a law constrains. +#[derive(Clone, Copy, PartialEq, Eq, Debug)] +pub enum Level { + /// Which path carries which value. + Values, + /// Which paths survive, values unconstrained. + Paths, +} + +pub struct Law { + pub name: &'static str, + pub lhs: Expr, + pub rhs: Expr, + pub level: Level, +} + +fn v(i: usize) -> Expr { + Expr::Var(i) +} +fn j(a: Expr, b: Expr) -> Expr { + Expr::bin(Op::Join, a, b) +} +fn m(a: Expr, b: Expr) -> Expr { + Expr::bin(Op::Meet, a, b) +} +fn s(a: Expr, b: Expr) -> Expr { + Expr::bin(Op::Subtract, a, b) +} +fn x(a: Expr, b: Expr) -> Expr { + Expr::bin(Op::SymDiff, a, b) +} +fn r(a: Expr, b: Expr) -> Expr { + Expr::bin(Op::Restrict, a, b) +} + +/// The laws to check for value type `V`. +/// +/// For a lawful `V` every `Paths` level is promoted to `Values` and +/// [`lawful_only`] is appended. +pub fn laws() -> Vec { + let mut out = base(); + if V::LAWFUL { + for law in &mut out { + law.level = Level::Values; + } + out.extend(lawful_only()); + } + out +} + +/// Identities that hold whatever the value type. +fn base() -> Vec { + use Level::{Paths, Values}; + let (a, b, c, e) = (0usize, 1usize, 2usize, EMPTY); + vec![ + // --- lattice basics + Law { name: "join-idempotent", lhs: j(v(a), v(a)), rhs: v(a), level: Values }, + Law { name: "meet-idempotent", lhs: m(v(a), v(a)), rhs: v(a), level: Values }, + Law { name: "join-unit", lhs: j(v(a), v(e)), rhs: v(a), level: Values }, + Law { name: "meet-zero", lhs: m(v(a), v(e)), rhs: v(e), level: Values }, + // Path set only: both `pjoin` and `pmeet` return the left operand, so + // swapping the operands swaps which value lands. A real lattice would + // make these value-level laws; see the module comment. + Law { name: "join-commutative", lhs: j(v(a), v(b)), rhs: j(v(b), v(a)), level: Paths }, + Law { name: "meet-commutative", lhs: m(v(a), v(b)), rhs: m(v(b), v(a)), level: Paths }, + // Associativity does hold on values even here: both nestings select the + // leftmost present operand's value. + Law { + name: "join-associative", + lhs: j(j(v(a), v(b)), v(c)), + rhs: j(v(a), j(v(b), v(c))), + level: Values, + }, + Law { + name: "meet-associative", + lhs: m(m(v(a), v(b)), v(c)), + rhs: m(v(a), m(v(b), v(c))), + level: Values, + }, + Law { name: "absorb-meet-join", lhs: m(v(a), j(v(a), v(b))), rhs: v(a), level: Values }, + Law { name: "absorb-join-meet", lhs: j(v(a), m(v(a), v(b))), rhs: v(a), level: Values }, + Law { + name: "meet-distributes-over-join", + lhs: m(v(a), j(v(b), v(c))), + rhs: j(m(v(a), v(b)), m(v(a), v(c))), + level: Values, + }, + Law { + name: "join-distributes-over-meet", + lhs: j(v(a), m(v(b), v(c))), + rhs: m(j(v(a), v(b)), j(v(a), v(c))), + level: Values, + }, + // --- subtraction + Law { name: "subtract-self", lhs: s(v(a), v(a)), rhs: v(e), level: Values }, + Law { name: "subtract-unit", lhs: s(v(a), v(e)), rhs: v(a), level: Values }, + Law { name: "subtract-from-empty", lhs: s(v(e), v(a)), rhs: v(e), level: Values }, + // Each step drops the paths whose value the subtrahend matches, and + // "matches b or matches c" does not depend on the order. + Law { + name: "subtract-steps-commute", + lhs: s(s(v(a), v(b)), v(c)), + rhs: s(s(v(a), v(c)), v(b)), + level: Values, + }, + // Subtracting cannot add a path: re-joining the removed part recovers + // no more than the original. + Law { name: "subtract-shrinks", lhs: j(s(v(a), v(b)), v(a)), rhs: v(a), level: Values }, + // --- symmetric difference + Law { name: "sym-diff-self", lhs: x(v(a), v(a)), rhs: v(e), level: Values }, + Law { name: "sym-diff-unit", lhs: x(v(a), v(e)), rhs: v(a), level: Values }, + // Fully commutative, values included: a coincident path cancels on both + // sides, so each surviving value comes from the single side that has it. + Law { name: "sym-diff-commutative", lhs: x(v(a), v(b)), rhs: x(v(b), v(a)), level: Values }, + Law { + name: "sym-diff-associative-paths", + lhs: x(x(v(a), v(b)), v(c)), + rhs: x(v(a), x(v(b), v(c))), + level: Paths, + }, + // The definition `zipper_sym_diff`'s own documentation gives. + Law { + name: "sym-diff-is-join-minus-meet", + lhs: x(v(a), v(b)), + rhs: s(j(v(a), v(b)), m(v(a), v(b))), + level: Values, + }, + // --- restrict + // Every path is a prefix of itself, so restricting by its own operand + // admits everything. + Law { name: "restrict-self", lhs: r(v(a), v(a)), rhs: v(a), level: Values }, + Law { name: "restrict-empty", lhs: r(v(a), v(e)), rhs: v(e), level: Values }, + Law { name: "restrict-of-empty", lhs: r(v(e), v(a)), rhs: v(e), level: Values }, + Law { name: "restrict-idempotent", lhs: r(r(v(a), v(b)), v(b)), rhs: r(v(a), v(b)), level: Values }, + // A path present in both operands is admitted by itself, so the meet is + // contained in the restriction. + Law { + name: "meet-under-restrict", + lhs: m(m(v(a), v(b)), r(v(a), v(b))), + rhs: m(v(a), v(b)), + level: Values, + }, + // --- majority, the worked example in `zipper_majority`'s docs, written + // out as the DNF it claims to equal. Exercised here so the DNF engine + // is checked against a hand-written join of meets as well as against + // the pointwise routes. + Law { + name: "majority-is-pairwise-meets", + lhs: j(j(m(v(a), v(b)), m(v(a), v(c))), m(v(b), v(c))), + rhs: j(m(v(a), v(b)), j(m(v(a), v(c)), m(v(b), v(c)))), + level: Values, + }, + ] +} + +/// Identities that need the value type to be a real distributive lattice with a +/// relative complement. +/// +/// Each of these fails for `u64`, and each failure is explained by the same +/// thing: `pjoin` and `pmeet` both return the left operand, so `a | b == a & b`, +/// and `psubtract` is `None` exactly on equality. +fn lawful_only() -> Vec { + use Level::Values; + let (a, b, c) = (0usize, 1usize, 2usize); + vec![ + // De Morgan for relative complement. Fails for `u64` because `b | c` + // carries `b`'s value where both are present, so the left side keeps a + // path whose value matches `c` but not `b`. + Law { + name: "subtract-over-join", + lhs: s(v(a), j(v(b), v(c))), + rhs: m(s(v(a), v(b)), s(v(a), v(c))), + level: Values, + }, + Law { + name: "subtract-over-meet", + lhs: s(v(a), m(v(b), v(c))), + rhs: j(s(v(a), v(b)), s(v(a), v(c))), + level: Values, + }, + // Subtracting the overlap is the same as subtracting the whole. Fails + // for `u64` because `a & b` carries *`a`'s* value, so the right side + // drops every shared path rather than only the equal ones. + Law { + name: "subtract-is-subtract-meet", + lhs: s(v(a), v(b)), + rhs: s(v(a), m(v(a), v(b))), + level: Values, + }, + // Symmetric difference is the XOR of a Boolean ring, so it is + // associative on values and not merely on paths. + Law { + name: "sym-diff-associative", + lhs: x(x(v(a), v(b)), v(c)), + rhs: x(v(a), x(v(b), v(c))), + level: Values, + }, + ] +} diff --git a/differential/src/algebraic/model.rs b/differential/src/algebraic/model.rs new file mode 100644 index 00000000..c987be6d --- /dev/null +++ b/differential/src/algebraic/model.rs @@ -0,0 +1,114 @@ +//! Flat reference semantics, as a fourth opinion. +//! +//! Every route in `routes.rs` goes through `pathmap`, so a defect common to the +//! whole algebra layer would make them agree with each other and still be wrong. +//! This computes the same expression over a plain `BTreeMap, V>` with no +//! trie involved, which gives the comparison something to anchor against. +//! +//! It models only *which path carries which value* and abstains on structure: a +//! flat map cannot represent a dangling path, and whether a dangling path +//! survives an operation is unsettled in the crate. `shape.rs` explains the +//! split. +//! +//! # The value algebra is not restated here +//! +//! Each operation delegates to the value type's own `pjoin`, `pmeet` or +//! `psubtract` through the `Option` impls in `pathmap::ring`. An earlier +//! version spelled out `u64`'s behaviour by hand -- left-biased join, left-biased +//! meet, subtract-on-equality -- which worked only because it happened to match, +//! and which meant the model was asserting the harness author's idea of the +//! algebra rather than the type's. Delegating means this file is correct for +//! any [`FuzzValue`] without changes, and that a disagreement between the model +//! and a route is always about *where a value ends up*, never about what +//! combining two values means. +//! +//! What remains genuinely this file's own is the set structure: which paths an +//! operation visits at all, and `restrict`, which is not a lattice operation. + +use pathmap::ring::{DistributiveLattice, Lattice}; + +use super::expr::{Expr, Op}; +use super::shape::Values; +use super::value::{resolve, FuzzValue}; + +pub fn eval(e: &Expr, operands: &[Values]) -> Values { + match e { + Expr::Var(i) => operands[*i].clone(), + Expr::Bin(op, l, r) => { + let a = eval(l, operands); + let b = eval(r, operands); + apply(*op, &a, &b) + } + } +} + +pub fn apply(op: Op, a: &Values, b: &Values) -> Values { + match op { + Op::Join => join(a, b), + Op::Meet => meet(a, b), + Op::Subtract => subtract(a, b), + Op::SymDiff => sym_diff(a, b), + Op::Restrict => restrict(a, b), + } +} + +/// Every path either side mentions. +fn keys(a: &Values, b: &Values) -> Vec> { + let mut k: Vec> = a.keys().chain(b.keys()).cloned().collect(); + k.sort(); + k.dedup(); + k +} + +/// Combine both sides pointwise with one of the value operations, dropping the +/// paths where the result is bottom. +fn pointwise(a: &Values, b: &Values, f: F) -> Values +where + F: Fn(&Option, &Option) -> Option, +{ + let mut out = Values::new(); + for k in keys(a, b) { + let (lv, rv) = (a.get(&k).cloned(), b.get(&k).cloned()); + if let Some(v) = f(&lv, &rv) { + out.insert(k, v); + } + } + out +} + +pub fn join(a: &Values, b: &Values) -> Values { + pointwise(a, b, |l, r| resolve(l.pjoin(r), l, r)) +} + +pub fn meet(a: &Values, b: &Values) -> Values { + pointwise(a, b, |l, r| resolve(l.pmeet(r), l, r)) +} + +pub fn subtract(a: &Values, b: &Values) -> Values { + pointwise(a, b, |l, r| resolve(l.psubtract(r), l, r)) +} + +/// `(a | b) \ (a & b)`, the definition `zipper_sym_diff`'s own documentation +/// gives. +/// +/// In a distributive lattice with a relative complement this equals +/// `(a \ b) | (b \ a)`, and `laws.rs` checks that -- for a lawful value type it +/// is a law, and for `u64` the two differ, which is a fact about `u64` rather +/// than about symmetric difference. +pub fn sym_diff(a: &Values, b: &Values) -> Values { + subtract(&join(a, b), &meet(a, b)) +} + +/// Left paths that some path-to-a-value in the right side is a prefix of. +/// +/// Not a lattice operation, so there is nothing to delegate to: the value is +/// carried across unchanged, and only the path set is decided. The prefix is +/// inclusive at both ends -- the empty path counts, so a root value in `b` +/// admits all of `a`, and `k` counts as a prefix of itself -- both of which +/// follow from the note on `PathMap::restrict`. +pub fn restrict(a: &Values, b: &Values) -> Values { + a.iter() + .filter(|(k, _)| (0..=k.len()).any(|n| b.contains_key(&k[..n]))) + .map(|(k, v)| (k.clone(), v.clone())) + .collect() +} diff --git a/differential/src/algebraic/routes.rs b/differential/src/algebraic/routes.rs new file mode 100644 index 00000000..d7cfe041 --- /dev/null +++ b/differential/src/algebraic/routes.rs @@ -0,0 +1,574 @@ +//! The different ways to compute the same thing. +//! +//! `pathmap` offers each algebraic operation several times over: once eagerly +//! on whole maps, once in place through a write zipper, once as a lockstep +//! traversal of two read zippers, and -- for the associative ones -- again as +//! an n-ary traversal, a DNF evaluator, and a lazy zipper over a virtual trie. +//! Those are not alternative spellings of one implementation; they are separate +//! implementations with separate pruning, grafting and value-combining logic, +//! which is exactly why they are worth running against each other. +//! +//! A *route* is one consistent way to evaluate a whole expression. There are +//! two kinds: +//! +//! * **pointwise** routes walk the expression bottom-up and evaluate each node +//! with a two-operand call, materialising each intermediate into a trie. +//! Route `k` picks strategy `k % n` for an operator with `n` strategies, so +//! every strategy is covered by some route and the routes mix them. +//! * **whole-expression** routes recognise a shape -- a chain of one +//! associative operator, or a join of meets -- and hand the entire thing to +//! one call that does it in a single traversal. These are the routes with +//! real independence from the pointwise ones: no intermediate trie is ever +//! built, so they exercise code the pointwise routes never reach. +//! +//! Every route must produce the same trie. `shape.rs` says what "same" means +//! and why dangling-path divergence is reported separately. + +use pathmap::PathMap; +use pathmap::experimental::zipper_algebra::{ + Clause, zipper_join, zipper_join3, zipper_meet, zipper_meet3, zipper_merge_dnf, + zipper_n_join, zipper_n_meet, zipper_n_subtract, zipper_n_sym_diff, zipper_subtract, + zipper_subtract3, zipper_sym_diff, zipper_sym_diff3, ZipperMergeF, +}; +use pathmap::fuse::FuseExpr; +use pathmap::zipper::{ + OverlayZipper, ReadZipperUntracked, ZipperMoving, ZipperPath, ZipperValues, ZipperWriting, +}; + +use super::expr::{Expr, Op}; +use super::model; +use super::shape::{shape_of_map, shape_of_zipper, values_of_shape, Shape, Values, ESCAPED_ROOT, TRUNCATED}; +use super::value::FuzzValue; + +/// Names of the per-operator strategies, in the order route `k % n` indexes +/// them. Kept as tables so a route's name can say which strategy it used for +/// each operator the expression contains. +pub const JOIN_STRATEGIES: &[&str] = + &["map", "join_into", "join_map_into", "join_into_take", "zipper_join", "overlay"]; +pub const MEET_STRATEGIES: &[&str] = &["map", "meet_into", "meet_2", "zipper_meet"]; +pub const SUBTRACT_STRATEGIES: &[&str] = &["map", "subtract_into", "zipper_subtract"]; +pub const SYM_DIFF_STRATEGIES: &[&str] = &["zipper_sym_diff", "join_minus_meet"]; +pub const RESTRICT_STRATEGIES: &[&str] = &["map", "wz_restrict"]; + +/// The strategy table is the same for every value type, so route `k` means the +/// same thing under each of them. +/// +/// That matters more than it looks. An earlier version shortened the join table +/// for value types that cannot use the `OverlayZipper` strategy, which silently +/// renumbered every later route -- so `pw4` and `pw5` meant different strategy +/// mixes under `u64` and under `bits`, and comparing their findings across the +/// two types was comparing different things. A strategy that does not apply to +/// a value type now *declines* instead, which leaves the numbering alone and +/// simply makes that route absent for that type. +pub fn strategies(op: Op) -> &'static [&'static str] { + match op { + Op::Join => JOIN_STRATEGIES, + Op::Meet => MEET_STRATEGIES, + Op::Subtract => SUBTRACT_STRATEGIES, + Op::SymDiff => SYM_DIFF_STRATEGIES, + Op::Restrict => RESTRICT_STRATEGIES, + } +} + +/// How many pointwise routes exist: enough that every strategy of every +/// operator is reached by at least one of them. +pub const POINTWISE_ROUTES: usize = 6; + +#[derive(Clone, Copy, PartialEq, Eq, Debug)] +pub enum Route { + /// Bottom-up two-operand evaluation, strategy `k % n` per operator. + Pointwise(usize), + /// `zipper_join3` / `zipper_meet3` / `zipper_subtract3` / `zipper_sym_diff3` + /// on a chain of exactly three operands. + Ternary, + /// `zipper_n_*` on a chain of operands, via the slice-of-zippers entry point. + Nary, + /// The same chain through the `ZipperMergeF` tuple entry point, which goes + /// via the `PolyZipper`-derived enum rather than a homogeneous array. + NaryPoly, + /// `zipper_merge_dnf` on a join of meets. + Dnf, + /// The whole expression as a `pathmap::fuse` program: compiled to SSA form + /// and evaluated bottom-up over trie *nodes*, below the zipper layer + /// entirely. + Fuse, + /// The same program after `distribute_and_over_or`. Rewriting + /// `(a | b) & c` into `(a & c) | (b & c)` must not change the answer, which + /// makes the rewrite pass itself checkable. + FuseDistributed, + /// Flat `BTreeMap` semantics, no trie. Values only; abstains on structure. + Model, +} + +impl Route { + pub fn all() -> Vec { + let mut v: Vec = (0..POINTWISE_ROUTES).map(Route::Pointwise).collect(); + v.extend([ + Route::Ternary, + Route::Nary, + Route::NaryPoly, + Route::Dnf, + Route::Fuse, + Route::FuseDistributed, + Route::Model, + ]); + v + } + + /// Name including, for a pointwise route, the strategy it picked for each + /// operator the expression actually uses. A failure report needs this to + /// be actionable: "pw#3" alone does not name a function to go and read. + pub fn name(&self, e: &Expr) -> String { + match self { + Route::Pointwise(k) => { + let mut used: Vec = Vec::new(); + collect_ops(e, &mut used); + let picks: Vec = Op::ALL + .iter() + .filter(|op| used.contains(op)) + .map(|op| { + let t = strategies(*op); + format!("{}={}", op.sym(), t[k % t.len()]) + }) + .collect(); + format!("pw#{k}[{}]", picks.join(",")) + } + Route::Ternary => "ternary".into(), + Route::Nary => "nary".into(), + Route::NaryPoly => "nary_poly".into(), + Route::Dnf => "dnf".into(), + Route::Fuse => "fuse".into(), + Route::FuseDistributed => "fuse_distributed".into(), + Route::Model => "model".into(), + } + } +} + +fn collect_ops(e: &Expr, out: &mut Vec) { + if let Expr::Bin(op, l, r) = e { + if !out.contains(op) { + out.push(*op); + } + collect_ops(l, out); + collect_ops(r, out); + } +} + +/// What a route produced. `shape` is `None` for a route that cannot represent +/// dangling paths, which is only [`Route::Model`]. +pub struct Outcome { + pub values: Values, + pub shape: Option>, +} + +impl Outcome { + fn from_map(m: &PathMap) -> Outcome { + let shape = shape_of_map(m); + Outcome { values: values_of_shape(&shape), shape: Some(shape) } + } +} + +/// Evaluate `e` over `operands` by `route`, or `None` if the route does not +/// apply to this expression's shape. +pub fn eval(route: Route, e: &Expr, operands: &[PathMap]) -> Option> { + match route { + Route::Pointwise(k) => pointwise(k, e, operands).map(|m| Outcome::from_map(&m)), + Route::Ternary => ternary(e, operands).map(|m| Outcome::from_map(&m)), + Route::Nary => nary(e, operands, false).map(|m| Outcome::from_map(&m)), + Route::NaryPoly => nary(e, operands, true).map(|m| Outcome::from_map(&m)), + Route::Dnf => dnf(e, operands).map(|m| Outcome::from_map(&m)), + Route::Fuse => fuse(e, operands, false).map(|m| Outcome::from_map(&m)), + Route::FuseDistributed => fuse(e, operands, true).map(|m| Outcome::from_map(&m)), + Route::Model => { + let vals: Vec> = + operands.iter().map(|m| values_of_shape(&shape_of_map(m))).collect(); + Some(Outcome { values: model::eval(e, &vals), shape: None }) + } + } +} + +// ---------------------------------------------------------------- pointwise + +/// `None` when the strategy route `k` selects for some operator in `e` does not +/// apply to this value type. +fn pointwise(k: usize, e: &Expr, operands: &[PathMap]) -> Option> { + match e { + Expr::Var(i) => Some(operands[*i].clone()), + Expr::Bin(op, l, r) => { + let a = pointwise(k, l, operands)?; + let b = pointwise(k, r, operands)?; + apply(*op, k, &a, &b) + } + } +} + +/// One operator, one strategy. Every arm is a different code path in the +/// crate, not a different way of calling the same one. +pub fn apply(op: Op, k: usize, a: &PathMap, b: &PathMap) -> Option> { + let n = strategies(op).len(); + Some(match (op, k % n) { + // -- join + (Op::Join, 0) => a.join(b), + (Op::Join, 1) => { + let mut out = a.clone(); + { + let mut wz = out.write_zipper(); + wz.join_into(&b.read_zipper()); + } + out + } + (Op::Join, 2) => { + let mut out = a.clone(); + { + let mut wz = out.write_zipper(); + wz.join_map_into(b.clone()); + } + out + } + (Op::Join, 3) => { + // Consumes the source. `prune = false` keeps whatever dangling + // structure the operation leaves, so this route is comparable with + // the other write-zipper forms rather than silently tidier. + let mut out = a.clone(); + let mut src = b.clone(); + { + let mut wz = out.write_zipper(); + let mut sz = src.write_zipper(); + wz.join_into_take(&mut sz, false); + } + out + } + (Op::Join, 4) => { + let mut out = PathMap::new(); + { + let mut lz = a.read_zipper(); + let mut rz = b.read_zipper(); + let mut wz = out.write_zipper(); + zipper_join(&mut lz, &mut rz, &mut wz); + } + out + } + (Op::Join, 5) => { + // Declines rather than answering wrongly: see + // `FuzzValue::JOIN_PICKS_LEFT`. + if !V::JOIN_PICKS_LEFT { + return None; + } + // `OverlayZipper`'s default mapping is `a.or(b)`, which is the same + // bias a left-picking `pjoin` has, so for such a value type the + // virtual trie it walks is exactly the join. Only reachable when + // `V::JOIN_PICKS_LEFT`; see `strategies`. It never builds a trie, so + // it has to be materialised to be composed into a larger expression; + // the walk records dangling paths too, so nothing is lost. + let overlay = OverlayZipper::new(a.read_zipper(), b.read_zipper()); + materialize(overlay) + } + + // -- meet + (Op::Meet, 0) => a.meet(b), + (Op::Meet, 1) => { + let mut out = a.clone(); + { + let mut wz = out.write_zipper(); + wz.meet_into(&b.read_zipper(), false); + } + out + } + (Op::Meet, 2) => { + // Writes the intersection of two sources into a fresh destination, + // rather than intersecting a destination with one source. + let mut out = PathMap::new(); + { + let mut wz = out.write_zipper(); + wz.meet_2(&a.read_zipper(), &b.read_zipper()); + } + out + } + (Op::Meet, 3) => { + let mut out = PathMap::new(); + { + let mut lz = a.read_zipper(); + let mut rz = b.read_zipper(); + let mut wz = out.write_zipper(); + zipper_meet(&mut lz, &mut rz, &mut wz); + } + out + } + + // -- subtract + (Op::Subtract, 0) => a.subtract(b), + (Op::Subtract, 1) => { + let mut out = a.clone(); + { + let mut wz = out.write_zipper(); + wz.subtract_into(&b.read_zipper(), false); + } + out + } + (Op::Subtract, 2) => { + let mut out = PathMap::new(); + { + let mut lz = a.read_zipper(); + let mut rz = b.read_zipper(); + let mut wz = out.write_zipper(); + zipper_subtract(&mut lz, &mut rz, &mut wz); + } + out + } + + // -- symmetric difference + (Op::SymDiff, 0) => { + let mut out = PathMap::new(); + { + let mut lz = a.read_zipper(); + let mut rz = b.read_zipper(); + let mut wz = out.write_zipper(); + zipper_sym_diff(&mut lz, &mut rz, &mut wz); + } + out + } + (Op::SymDiff, 1) => { + // The definition `zipper_sym_diff`'s doc comment gives, built out + // of the other three operations. Where this disagrees with the + // specialised traversal, one of the two is wrong. + let j = a.join(b); + let m = a.meet(b); + j.subtract(&m) + } + + // -- restrict + (Op::Restrict, 0) => a.restrict(b), + (Op::Restrict, 1) => { + let mut out = a.clone(); + { + let mut wz = out.write_zipper(); + wz.restrict(&b.read_zipper()); + } + out + } + + _ => unreachable!("strategy index out of range for {op:?}"), + }) +} + +/// Walk a zipper over a virtual trie and build the real trie it describes. +/// +/// `create_path` is what keeps this faithful: a path with no value still has to +/// appear in the output, or materialising would quietly erase exactly the +/// dangling structure the comparison is trying to detect. +fn materialize(mut z: Z) -> PathMap +where + Z: ZipperMoving + ZipperPath + ZipperValues, +{ + let shape = shape_of_zipper(&mut z); + let mut out = PathMap::new(); + { + let mut wz = out.write_zipper(); + for (p, v) in &shape { + if &p[..] == ESCAPED_ROOT || &p[..] == TRUNCATED { + continue; + } + wz.reset(); + wz.descend_to(p); + match v { + Some(v) => { + wz.set_val(v.clone()); + } + None => { + wz.create_path(); + } + } + } + } + out +} + +// -------------------------------------------------------- whole-expression + +/// Chain of exactly three operands through the `*3` entry points. +fn ternary(e: &Expr, operands: &[PathMap]) -> Option> { + let (op, idx) = e.chain()?; + if idx.len() != 3 { + return None; + } + let (a, b, c) = (&operands[idx[0]], &operands[idx[1]], &operands[idx[2]]); + let mut out = PathMap::new(); + { + let mut za = a.read_zipper(); + let mut zb = b.read_zipper(); + let mut zc = c.read_zipper(); + let mut wz = out.write_zipper(); + match op { + Op::Join => zipper_join3(&mut za, &mut zb, &mut zc, &mut wz), + Op::Meet => zipper_meet3(&mut za, &mut zb, &mut zc, &mut wz), + Op::Subtract => zipper_subtract3(&mut za, &mut zb, &mut zc, &mut wz), + Op::SymDiff => zipper_sym_diff3(&mut za, &mut zb, &mut zc, &mut wz), + Op::Restrict => return None, + } + } + Some(out) +} + +/// A chain of any length through the n-ary entry points. +/// +/// Two of them: the slice form (`zipper_n_*`, const-generic over a homogeneous +/// array) and the tuple form (`ZipperMergeF::*_n`, which routes through the +/// `PolyZipper`-derived enum). They are separate monomorphisations of the +/// merge engine and are worth distinguishing, so `poly` selects between them. +fn nary(e: &Expr, operands: &[PathMap], poly: bool) -> Option> { + let (op, idx) = e.chain()?; + if op == Op::Restrict { + return None; + } + let mut out = PathMap::new(); + { + let mut wz = out.write_zipper(); + // Const-generic arity has to be dispatched by hand: there is one + // monomorphisation per operand count, and the count is only known at + // run time. The tuple form additionally has one impl per arity. + macro_rules! slice_arm { + ($n:literal) => {{ + let mut zs: [ReadZipperUntracked<'_, '_, V>; $n] = + core::array::from_fn(|i| operands[idx[i]].read_zipper()); + match op { + Op::Join => zipper_n_join(&mut zs, &mut wz), + Op::Meet => zipper_n_meet(&mut zs, &mut wz), + Op::Subtract => zipper_n_subtract(&mut zs, &mut wz), + Op::SymDiff => zipper_n_sym_diff(&mut zs, &mut wz), + Op::Restrict => unreachable!(), + } + }}; + } + macro_rules! tuple_arm { + ($($i:literal),+) => {{ + let t = ( $( &mut operands[idx[$i]].read_zipper() ),+ ); + match op { + Op::Join => t.join_n(&mut wz), + Op::Meet => t.meet_n(&mut wz), + Op::Subtract => t.subtract_n(&mut wz), + Op::SymDiff => t.sym_diff_n(&mut wz), + Op::Restrict => unreachable!(), + } + }}; + } + match (poly, idx.len()) { + (false, 2) => slice_arm!(2), + (false, 3) => slice_arm!(3), + (false, 4) => slice_arm!(4), + (false, 5) => slice_arm!(5), + (false, 6) => slice_arm!(6), + (true, 2) => tuple_arm!(0, 1), + (true, 3) => tuple_arm!(0, 1, 2), + (true, 4) => tuple_arm!(0, 1, 2, 3), + // The tuple impls go higher, but there is nothing to learn from + // arities the slice form already covers at the same width. + _ => return None, + } + } + Some(out) +} + +/// The whole expression as a `pathmap::fuse` program. +/// +/// The only route that leaves the zipper layer altogether: `fuse` evaluates +/// bottom-up over `TrieNodeODRc` nodes, combining each step with `pjoin_dyn`, +/// `pmeet_dyn` and `psubtract_dyn` directly. So it checks the node-level +/// primitives against the zipper traversals that are supposed to agree with +/// them, which nothing else here does. +/// +/// `distributed` runs the program through `distribute_and_over_or` first. That +/// rewrite is only supposed to be a performance choice, so the two must give +/// the same answer and the pass gets checked for free. +/// +/// Declines an expression containing `restrict`: `FuseOp` has no counterpart, +/// and restrict is not a lattice operation. +fn fuse(e: &Expr, operands: &[PathMap], distributed: bool) -> Option> { + let (prog, out) = to_fuse_expr(e)?.compile(); + let inputs: Vec<&PathMap> = operands.iter().collect(); + let mut results = if distributed { + prog.eval_distributed(&inputs, &[out]) + } else { + prog.eval(&inputs, &[out]) + }; + debug_assert_eq!(results.len(), 1); + results.pop() +} + +/// Map the expression language onto `FuseOp`. +/// +/// Both languages are trees over the same operands, so this is one-to-one +/// except for `restrict`, which `fuse` has no operation for. The operand order +/// is preserved, which matters: every one of these is left-biased in its +/// values. +fn to_fuse_expr(e: &Expr) -> Option { + Some(match e { + Expr::Var(i) => FuseExpr::leaf(*i), + Expr::Bin(op, l, r) => { + let (l, r) = (to_fuse_expr(l)?, to_fuse_expr(r)?); + match op { + Op::Join => FuseExpr::or(l, r), + Op::Meet => FuseExpr::and(l, r), + Op::Subtract => FuseExpr::and_not(l, r), + Op::SymDiff => FuseExpr::xor(l, r), + Op::Restrict => return None, + } + } + }) +} + +/// A join of meets through `zipper_merge_dnf`. +/// +/// The operand indices are compacted first: the clause masks are indices into +/// the array handed to the call, so an expression over operands `a` and `c` +/// becomes a two-zipper call with the masks renumbered, not a four-zipper call +/// with two unused slots -- an unused slot would change what the traversal +/// prunes on and make the route test something else. +fn dnf(e: &Expr, operands: &[PathMap]) -> Option> { + let clauses = e.dnf()?; + let vars = e.vars(); + if vars.is_empty() || vars.len() > super::expr::MAX_VARS || clauses.len() > super::expr::MAX_CLAUSES { + return None; + } + // Remap each clause's bits from operand index to position in `vars`. + let packed: Vec = clauses + .iter() + .map(|m| { + vars.iter() + .enumerate() + .filter(|(_, v)| m >> **v & 1 == 1) + .fold(0u64, |acc, (i, _)| acc | 1 << i) + }) + .collect(); + + let mut out = PathMap::new(); + { + let mut wz = out.write_zipper(); + macro_rules! dnf_arm { + ($n:literal, $m:literal) => {{ + let mut zs: [ReadZipperUntracked<'_, '_, V>; $n] = + core::array::from_fn(|i| operands[vars[i]].read_zipper()); + let cs: [Clause<$n>; $m] = core::array::from_fn(|i| Clause::from_mask(packed[i])); + zipper_merge_dnf(&mut zs, cs, &mut wz); + }}; + } + macro_rules! dnf_m { + ($n:literal) => { + match packed.len() { + 1 => dnf_arm!($n, 1), + 2 => dnf_arm!($n, 2), + 3 => dnf_arm!($n, 3), + 4 => dnf_arm!($n, 4), + _ => return None, + } + }; + } + match vars.len() { + 1 => dnf_m!(1), + 2 => dnf_m!(2), + 3 => dnf_m!(3), + 4 => dnf_m!(4), + _ => return None, + } + } + Some(out) +} diff --git a/differential/src/algebraic/shape.rs b/differential/src/algebraic/shape.rs new file mode 100644 index 00000000..52f5cd56 --- /dev/null +++ b/differential/src/algebraic/shape.rs @@ -0,0 +1,166 @@ +//! What "the same result" means. +//! +//! Two routes through the same algebraic expression are compared on the trie +//! they produce, not on the calls they made. A trie is rendered two ways: +//! +//! * [`Shape`] — every path the trie contains, with the value at it if any. +//! Dangling paths (structure with no value under it) are included, so this +//! distinguishes tries that `iter()` cannot tell apart. +//! * [`Values`] — only the paths that carry values. +//! +//! The split matters because the two have different authority. Which paths +//! carry which values is settled: every route must agree, and a disagreement +//! is a bug in one of them. Whether a dangling path survives an operation is +//! *not* settled (see `../../SPEC_WARTS.md`), and routes legitimately built on +//! `graft` of whole subtries will keep dangling structure that routes built by +//! walking and inserting cannot. So a divergence confined to dangling paths +//! is reported as its own class rather than lumped in with a wrong value. +//! +//! Both renderings come off a zipper, not a `PathMap`, so a lazy zipper that +//! never materialises a trie — an `OverlayZipper`, say — is comparable against +//! an eagerly built map without special-casing. + +use pathmap::PathMap; +use pathmap::zipper::{ZipperMoving, ZipperPath, ZipperValues}; +use std::collections::BTreeMap; + +use super::value::FuzzValue; + +/// Every path in a trie, in depth-first order, with the value at it if any. +pub type Shape = Vec<(Vec, Option)>; + +/// The paths of a trie that carry values. +pub type Values = BTreeMap, V>; + +/// Cap on paths recorded per trie. A generated case that needs more than this +/// is not interesting enough to be worth the comparison cost; the cap is +/// recorded in the rendering so a truncated trie can never compare equal to a +/// complete one by accident. +pub const SHAPE_CAP: usize = 8192; + +/// Marker path emitted when a zipper walks out of its own root. No real path +/// can collide with it: generated paths use a small alphabet of low bytes. +pub const ESCAPED_ROOT: &[u8] = b""; +/// Marker path emitted when [`SHAPE_CAP`] is hit. +pub const TRUNCATED: &[u8] = b""; + +/// Depth-first walk of everything at and below the zipper's root. +/// +/// The root is recorded explicitly: `to_next_step` moves before it reports, so +/// a loop driven by it alone would miss the value at the empty path. +pub fn shape_of_zipper(z: &mut Z) -> Shape +where + Z: ZipperMoving + ZipperPath + ZipperValues, +{ + z.reset(); + let mut out: Shape = vec![(Vec::new(), z.val().cloned())]; + loop { + if out.len() >= SHAPE_CAP { + out.push((TRUNCATED.to_vec(), None)); + break; + } + if !z.to_next_step() { + break; + } + // A depth-first step from the root can only go deeper or sideways, so + // returning to the empty path means the zipper left its own root -- + // `lean/FINDINGS.md` #3. Stop rather than loop forever, and say so. + if z.path().is_empty() { + out.push((ESCAPED_ROOT.to_vec(), None)); + break; + } + out.push((z.path().to_vec(), z.val().cloned())); + } + out +} + +pub fn shape_of_map(m: &PathMap) -> Shape { + shape_of_zipper(&mut m.read_zipper()) +} + +/// The value-carrying subset of a [`Shape`]. +pub fn values_of_shape(s: &Shape) -> Values { + s.iter() + .filter_map(|(p, v)| v.clone().map(|v| (p.clone(), v))) + .collect() +} + +/// The paths of a [`Shape`], values ignored. Used by the laws that hold only +/// up to path presence, which is how the laws that depend on join and meet being +/// different functions are checked when the value type is not a lattice. +pub fn paths_of_shape(s: &Shape) -> Vec> { + s.iter().map(|(p, _)| p.clone()).collect() +} + +/// Render a path the way the rest of the harness does, so traces interleave. +pub fn show_path(p: &[u8]) -> String { + if p == ESCAPED_ROOT || p == TRUNCATED { + String::from_utf8_lossy(p).into_owned() + } else if p.is_empty() { + "_".to_string() + } else { + p.iter().map(|b| format!("{b:02x}")).collect() + } +} + +pub fn show_shape(s: &Shape) -> String { + s.iter() + .map(|(p, v)| match v { + Some(v) => format!("{}:{}", show_path(p), v.show()), + None => format!("{}:-", show_path(p)), + }) + .collect::>() + .join(",") +} + +pub fn show_values(v: &Values) -> String { + v.iter() + .map(|(p, v)| format!("{}:{}", show_path(p), v.show())) + .collect::>() + .join(",") +} + +/// First point at which two shapes differ, for the failure report. +pub fn first_shape_diff(a: &Shape, b: &Shape) -> Option { + for i in 0..a.len().max(b.len()) { + match (a.get(i), b.get(i)) { + (Some(x), Some(y)) if x == y => continue, + (Some(x), Some(y)) => { + return Some(format!( + "at #{i}: {}:{} vs {}:{}", + show_path(&x.0), + x.1.as_ref().map(|v| v.show()).unwrap_or("-".into()), + show_path(&y.0), + y.1.as_ref().map(|v| v.show()).unwrap_or("-".into()), + )); + } + (Some(x), None) => { + return Some(format!("at #{i}: {} vs ", show_path(&x.0))); + } + (None, Some(y)) => { + return Some(format!("at #{i}: vs {}", show_path(&y.0))); + } + (None, None) => break, + } + } + None +} + +/// First point at which two value maps differ. +pub fn first_values_diff(a: &Values, b: &Values) -> Option { + let mut keys: Vec<&Vec> = a.keys().chain(b.keys()).collect(); + keys.sort(); + keys.dedup(); + for k in keys { + let (x, y) = (a.get(k), b.get(k)); + if x != y { + return Some(format!( + "at {}: {} vs {}", + show_path(k), + x.map(|v| v.show()).unwrap_or("-".into()), + y.map(|v| v.show()).unwrap_or("-".into()), + )); + } + } + None +} diff --git a/differential/src/algebraic/value.rs b/differential/src/algebraic/value.rs new file mode 100644 index 00000000..e821334b --- /dev/null +++ b/differential/src/algebraic/value.rs @@ -0,0 +1,241 @@ +//! The value types the fuzzer runs every case against. +//! +//! The harness is generic over this trait and the driver instantiates it twice, +//! because the two instantiations answer different questions. +//! +//! * [`Bits`] is a genuine Boolean algebra: `pjoin` is `|`, `pmeet` is `&`, +//! `psubtract` is `& !`, and an empty result is bottom, which `pathmap` +//! represents as an absent value. Every lattice identity holds, so a law +//! that fails here is a real defect. +//! +//! * `u64` is the type the rest of this crate's fuzzing uses, and its instances +//! in `pathmap::ring` are **not a lattice**: `pjoin` is `left_biased_pjoin` +//! and `pmeet` is `Identity(SELF_IDENT)`, so both return the left operand and +//! `a | b == a & b` for every pair -- which in a lattice would force +//! `a == b`. It is kept because it is what real callers use today, and +//! because dropping it would lose coverage of the `Identity`-heavy paths. +//! +//! Running both is the point. A finding that appears under `u64` and not under +//! `Bits` is an artefact of that degenerate instance; one that appears under +//! both, or under `Bits` alone, is a defect in the crate. `bin/alg_fuzz` +//! prints the split explicitly. +//! +//! # Why a bitmask rather than some other lawful lattice +//! +//! Lawfulness alone is not enough. `max`/`min` on a total order is a perfectly +//! good distributive lattice, and useless here: `max(a, b)` and `min(a, b)` are +//! always *one of the operands*, so they can only ever return +//! `AlgebraicResult::Identity`, and every code path that allocates and stores a +//! genuinely combined value stays unreachable. `a | b` is a new value, so a +//! bitmask reaches them. `bin/alg_lattice_check` prints the comparison. + +use pathmap::ring::{AlgebraicResult, DistributiveLattice, Lattice, COUNTER_IDENT, SELF_IDENT}; + +use super::Gen; + +/// What the harness needs of a value type. +pub trait FuzzValue: + Clone + + Send + + Sync + + Unpin + + PartialEq + + Ord + + core::fmt::Debug + + core::hash::Hash + + Lattice + + DistributiveLattice + + 'static +{ + /// Appears as the first field of every signature, so findings from the two + /// instantiations never collide. + const NAME: &'static str; + + /// Whether this type's instances actually form a distributive lattice with a + /// relative complement. + /// + /// `laws.rs` reads this: when it is false, the identities that depend on + /// join and meet being different functions are checked on path presence + /// only, and the ones that cannot hold at all are skipped. When it is true + /// every identity is checked on values, which is the stronger test and the + /// reason for having a lawful type at all. + const LAWFUL: bool; + + /// Whether `pjoin` always yields one of its operands rather than a new + /// value -- true exactly when the "join" is really "the left one wins". + /// + /// This gates the `OverlayZipper` join strategy, and it is not a detail. + /// `OverlayZipper`'s mapping function has signature + /// `Fn(Option<&'a AV>, Option<&'a BV>) -> Option<&'a OutV>`: it returns a + /// *reference*, so it has nowhere to put a value it would have to create. + /// The module's own comment says as much. So an overlay can stand in for a + /// join only when the join never creates anything, and for a real lattice it + /// cannot be a join at all. That is a limitation of the zipper, not a + /// defect, so the strategy is dropped rather than reported. + const JOIN_PICKS_LEFT: bool; + + fn generate(g: &mut Gen) -> Self; + + fn show(&self) -> String; +} + +/// A 64-bit set under union, intersection and relative complement. +/// +/// The same construction `pathmap::utils` already uses for `[u64; 4]` and +/// `ByteMask`, at a narrower width: see `bitmask_algebraic_result` there. An +/// empty result is `AlgebraicResult::None` rather than `Element(Bits(0))`, +/// matching the convention `SetLattice`'s documentation states -- an empty set +/// is equivalent to a nonexistent one. +/// +/// Defined here rather than in `pathmap` on purpose: a value type living outside +/// the crate is what a real caller has, so the generic algebra is exercised the +/// way a downstream user would exercise it. +#[derive(Clone, Copy, PartialEq, Eq, PartialOrd, Ord, Hash)] +pub struct Bits(pub u64); + +impl core::fmt::Debug for Bits { + fn fmt(&self, f: &mut core::fmt::Formatter<'_>) -> core::fmt::Result { + write!(f, "{:b}", self.0) + } +} + +/// Classify a bitwise result exactly as `pathmap::utils` does for `[u64; 4]`. +#[inline] +fn bits_result(result: u64, lhs: u64, rhs: u64) -> AlgebraicResult { + if result == 0 { + return AlgebraicResult::None; + } + let mut mask = 0; + if result == lhs { + mask = SELF_IDENT; + } + if result == rhs { + mask |= COUNTER_IDENT; + } + if mask != 0 { + AlgebraicResult::Identity(mask) + } else { + AlgebraicResult::Element(Bits(result)) + } +} + +impl Lattice for Bits { + #[inline] + fn pjoin(&self, other: &Self) -> AlgebraicResult { + bits_result(self.0 | other.0, self.0, other.0) + } + #[inline] + fn pmeet(&self, other: &Self) -> AlgebraicResult { + bits_result(self.0 & other.0, self.0, other.0) + } +} + +impl DistributiveLattice for Bits { + #[inline] + fn psubtract(&self, other: &Self) -> AlgebraicResult { + bits_result(self.0 & !other.0, self.0, other.0) + } +} + +/// Width of the generated masks. +/// +/// Four bits, so operands collide constantly -- the whole point of a small +/// alphabet applies to values too -- while still overlapping only partially, so +/// `pjoin` and `pmeet` return `Element` rather than `Identity` most of the time. +pub const BITS_WIDTH: u32 = 4; + +impl FuzzValue for Bits { + const NAME: &'static str = "bits"; + const LAWFUL: bool = true; + // `Bits(0b01) | Bits(0b10)` is `Bits(0b11)`, which is neither operand. + const JOIN_PICKS_LEFT: bool = false; + + fn generate(g: &mut Gen) -> Self { + // Never zero. Bottom is representable as `Bits(0)`, but the lattice + // collapses it to `None`, so a stored `Bits(0)` is a value that is also + // bottom -- a genuinely interesting edge case, and a separate question + // from the one this type is here to answer. Excluded deliberately. + let n = 1u64 << BITS_WIDTH; + Bits(g.byte() as u64 % (n - 1) + 1) + } + + fn show(&self) -> String { + format!("{:b}", self.0) + } +} + +/// The set case: a path is either present or absent, with nothing attached. +/// +/// `Option<()>` is exactly the two-element Boolean algebra, so `()` is **lawful** +/// -- unlike `u64`, and for the same reason `bits` is. It earns a place of its +/// own anyway, for two reasons neither of the others covers. +/// +/// First, `PathMap<()>` is what a caller writes when the trie *is* the data, and +/// it is what the `unit-value-optimizations` and `unit-size` branches are about. +/// None of that is on `master` yet, so today this exercises the generic path; if +/// those land it becomes the only thing covering the specialised one. +/// +/// Second, and more useful now: `()`'s `pjoin` and `pmeet` return +/// `Identity(SELF_IDENT | COUNTER_IDENT)` *unconditionally* -- **both** identity +/// bits, always. `u64` returns that only for equal values and `bits` only for +/// equal masks, so neither saturates the "either side will do" path that the node +/// code uses to decide it can hand back an operand unchanged and keep sharing it. +/// Findings 4 and 6 are both about exactly that machinery, so a value type that +/// drives it on every single combination is worth having. +/// +/// It cannot produce `Element`, but that is not a gap here: with one inhabitant +/// there is no combined value to store. `bits` covers that. +impl FuzzValue for () { + const NAME: &'static str = "unit"; + const LAWFUL: bool = true; + // Both operands are `()`, so returning either is returning the left one, and + // `OverlayZipper`'s `a.or(b)` is the join. + const JOIN_PICKS_LEFT: bool = true; + + fn generate(_g: &mut Gen) -> Self {} + + fn show(&self) -> String { + "*".to_string() + } +} + +/// Distinct values in circulation for `u64`. +/// +/// Tiny on purpose: `psubtract` on `u64` is `None` only when the two values are +/// *equal*, so a large value space would turn subtraction into set difference +/// and never exercise the value comparison at all. +pub const U64_VALUES: u64 = 3; + +impl FuzzValue for u64 { + const NAME: &'static str = "u64"; + const LAWFUL: bool = false; + const JOIN_PICKS_LEFT: bool = true; + + fn generate(g: &mut Gen) -> Self { + g.byte() as u64 % U64_VALUES + 1 + } + + fn show(&self) -> String { + self.to_string() + } +} + +/// Resolve an `AlgebraicResult` over `Option` to a value, which is how +/// `pathmap` stores the outcome: `None` means the value is gone. +/// +/// Used by `model.rs` so the reference semantics are derived from the value +/// type's own operations rather than restated by hand -- restating them is how +/// a harness ends up asserting its own idea of the algebra. +pub fn resolve( + result: AlgebraicResult>, + lhs: &Option, + rhs: &Option, +) -> Option { + match result { + AlgebraicResult::Element(v) => v, + AlgebraicResult::Identity(mask) => { + if mask & SELF_IDENT != 0 { lhs.clone() } else { rhs.clone() } + } + AlgebraicResult::None => None, + } +} diff --git a/differential/src/bin/alg_bug_repros.rs b/differential/src/bin/alg_bug_repros.rs new file mode 100644 index 00000000..27baf318 --- /dev/null +++ b/differential/src/bin/alg_bug_repros.rs @@ -0,0 +1,338 @@ +//! Standalone reproducers for what `bin/alg_fuzz` found on `master`. +//! +//! Same role as `bin/zipper_bug_repros.rs`: each case is a dozen lines of +//! ordinary `pathmap` calls with no fuzzer, no harness and no decoder, so it +//! can be pasted into a test or stepped through in a debugger. The signatures +//! these correspond to are listed in `algebraic::KNOWN`. +//! +//! ```sh +//! cargo run --release -p differential --bin alg_bug_repros +//! ``` +//! +//! Exit status is 1 while any of them still reproduces. Cases 8 and 9 are not +//! defects -- one is a property of the value type, the other an unsettled +//! question -- and never count as a failure. + +use pathmap::PathMap; +use pathmap::experimental::zipper_algebra::{zipper_join, zipper_meet, zipper_sym_diff}; +use pathmap::fuse::FuseExpr; +use pathmap::zipper::{ZipperMoving, ZipperPath, ZipperValues, ZipperWriting}; + +/// A trie holding only dangling paths: structure written with `create_path` +/// and no value anywhere. +fn dangling(paths: &[&[u8]]) -> PathMap { + let mut m = PathMap::::new(); + let mut wz = m.write_zipper(); + for p in paths { + wz.reset(); + wz.descend_to(*p); + wz.create_path(); + } + drop(wz); + m +} + +fn with_val(path: &[u8], v: u64) -> PathMap { + let mut m = PathMap::::new(); + m.write_zipper_at_path(path).set_val(v); + m +} + +fn val_at(m: &PathMap, path: &[u8]) -> Option { + m.read_zipper_at_path(path).val().copied() +} + +/// Every path in a trie, with `=v` on the ones carrying a value, so a +/// dangling-path difference is visible. +fn shape(m: &PathMap) -> Vec { + let mut z = m.read_zipper(); + let mut out = Vec::new(); + z.reset(); + while z.to_next_step() { + out.push(format!( + "{}{}", + z.path().iter().map(|b| format!("{b}")).collect::(), + if z.val().is_some() { "=v" } else { "" } + )); + } + out +} + +struct Report { + failed: usize, +} + +impl Report { + fn case(&mut self, n: &str, what: &str, want: String, got: String) { + let ok = want == got; + if !ok { + self.failed += 1; + } + println!("\n{n}. {what}"); + println!(" expected: {want}"); + println!(" got: {got}"); + println!(" => {}", if ok { "fixed" } else { "REPRODUCES" }); + } +} + +fn main() { + let mut r = Report { failed: 0 }; + + // ---------------------------------------------------------------- 1 + // `join_into` is the write-zipper spelling of `join`, so joining a source + // into an empty destination has to be the same as joining the empty map + // with it. The root value does not survive the write-zipper form. + { + let src = with_val(&[], 1); + let eager = PathMap::::new().join(&src); + + let mut out = PathMap::::new(); + { + let mut wz = out.write_zipper(); + wz.join_into(&src.read_zipper()); + } + r.case( + "1", + "join_into on an empty destination: empty | {_:1}", + format!("root value {:?} (PathMap::join)", val_at(&eager, &[])), + format!("root value {:?} (join_into)", val_at(&out, &[])), + ); + } + + // ---------------------------------------------------------------- 2 + // `meet_2` writes the intersection of two sources into a fresh + // destination. Two maps whose only content is a root value intersect to + // that root value; `meet_2` produces nothing at all. + { + let a = with_val(&[], 1); + let b = with_val(&[], 2); + let eager = b.meet(&a); + + let mut out = PathMap::::new(); + { + let mut wz = out.write_zipper(); + wz.meet_2(&b.read_zipper(), &a.read_zipper()); + } + r.case( + "2", + "meet_2 with root values only: {_:2} & {_:1}", + format!("root value {:?} (PathMap::meet)", val_at(&eager, &[])), + format!("root value {:?} (meet_2)", val_at(&out, &[])), + ); + } + + // ---------------------------------------------------------------- 3 + // `pjoin` on `u64` is `left_biased_pjoin` and `pmeet` is + // `Identity(SELF_IDENT)`, so where both operands have a value at a path the + // result must carry the *left* one. It carries the right one when the two + // operands' nodes are laid out differently -- here because `a` has a chain + // of dangling descendants below the shared path and `c` does not. + // + // Every zipper route gets this right; `PathMap::join` and `PathMap::meet` + // do not, which is why it surfaces as failing laws rather than as one + // route disagreeing with the rest. + { + let mut a = dangling(&[&[0, 0, 0, 0], &[1]]); + a.write_zipper_at_path(&[0]).set_val(1); + let c = with_val(&[0], 2); + + r.case( + "3a", + "join value bias: {00:2} | {00:1, dangling below} at [0]", + "Some(2), the left operand's value".to_string(), + format!("{:?}", val_at(&c.join(&a), &[0])), + ); + r.case( + "3b", + "meet value bias: {00:1, dangling below} & {00:2} at [0]", + "Some(1), the left operand's value".to_string(), + format!("{:?}", val_at(&a.meet(&c), &[0])), + ); + } + + // ---------------------------------------------------------------- 4 + // The worst of them: a join *loses a value*. Not a bias about which of two + // values wins -- only one operand has a value at all, and the result has + // none. + // + // `b` is a clone of `a` with one value added, so the two tries share nodes. + // Joining in the order `a | b` drops `b`'s value; `b | a` keeps it. A + // join is a least upper bound, so no ordering of the operands may lose a + // path, which makes this the one finding here that is unambiguous without + // any appeal to value bias. + // + // The sharing is essential: rebuilding `b`'s entries into a fresh map + // instead of cloning `a` makes it go away. + { + let a = dangling(&[&[0, 0, 0, 0, 0], &[1, 0, 1], &[1, 0, 3]]); + let mut b = a.clone(); + b.write_zipper_at_path(&[1, 0, 0, 0]).set_val(1); + + let ab = a.join(&b); + let ba = b.join(&a); + r.case( + "4", + "join drops a value across clone-shared structure, at [1,0,0,0]", + format!("a|b == b|a == Some(1); b|a gives {:?}", val_at(&ba, &[1, 0, 0, 0])), + format!("a|b gives {:?}", val_at(&ab, &[1, 0, 0, 0])), + ); + } + + // ---------------------------------------------------------------- 5 + // Not an algebraic defect: `merkleize` panics outright on a trie that holds + // structure but no values. It is in this list because the fuzzer's operand + // generator reaches it -- `merkleize` is how it builds operands with shared + // subtries, which is what case 4 needs. + { + let mut m = dangling(&[&[0, 0], &[0, 1, 0, 0]]); + let hook = std::panic::take_hook(); + std::panic::set_hook(Box::new(|_| {})); + let res = std::panic::catch_unwind(std::panic::AssertUnwindSafe(|| m.merkleize())); + std::panic::set_hook(hook); + r.case( + "5", + "merkleize over dangling-only structure", + "no panic".to_string(), + if res.is_ok() { "no panic".to_string() } else { "panic".to_string() }, + ); + } + + // ---------------------------------------------------------------- 6 + // Finding 6 has no standalone reproducer: it is three `debug_assert!`s + // inside the merge primitives, so there is nothing to compare and nothing + // to print -- the assertion either fires or it does not. Build with + // `-C debug-assertions=yes` and replay the three `panic-eval-*` inputs in + // `algebraic-corpus/`. Case 7 below is its visible consequence. + println!( + "\n6. join reporting an empty result from non-empty nodes\n => debug-assertions only; replay algebraic-corpus/panic-eval-*.bin" + ); + + // ---------------------------------------------------------------- 7 + // Finding 4 again, reached without cloning anything, and with a visible + // consequence. `fuse`'s `Xor` is `(l \ r) | (r \ l)`. With `c` holding no + // values at all and `a` holding one, `c \ a` comes out as dangling-only + // structure and `a \ c` keeps the value -- so the join at the end is + // exactly the shape of finding 4, and it loses the value. + // + // Worth having separately because every PathMap-level spelling of the same + // thing keeps it: `a - c`, `(c | a) - (c & a)` and `(c - a) | (a - c)` are + // all correct here. Only the node-level composition loses it, and + // `join_into_dyn` reports `AlgebraicStatus::Element` while doing so, so a + // caller cannot detect it from the status either. + { + let mut a = dangling(&[&[0, 0, 0, 0, 0]]); + a.write_zipper_at_path(&[0]).set_val(1); + let c = dangling(&[&[1]]); + + let (prog, out) = FuseExpr::xor(FuseExpr::leaf(0), FuseExpr::leaf(1)).compile(); + let fused = prog.eval(&[&c, &a], &[out]).pop().unwrap(); + + let eager = c.join(&a).subtract(&c.meet(&a)); + r.case( + "7", + "fuse Xor loses a value only one operand has, at [0]", + format!("Some(1), as (c|a)-(c&a) gives {:?}", val_at(&eager, &[0])), + format!("{:?}", val_at(&fused, &[0])), + ); + } + + // ---------------------------------------------------------------- 8 + // Not a defect in either operation: a symptom of the *value type*. + // + // `(a | b) \ (a & b)` and `(a \ b) | (b \ a)` are equal in any distributive + // lattice with a relative complement, so symmetric difference is not + // ambiguous and there is no convention to choose. They come apart for + // `u64` because `u64`'s `Lattice` impl is not a lattice: `pjoin` is + // `left_biased_pjoin` and `pmeet` is `Identity(SELF_IDENT)`, so both are + // "return the left operand" and `a | b == a & b` for every pair -- which in + // a lattice would force `a == b`. With the two collapsed into one function + // the first formula becomes `a \ a` and vanishes, while the second stays `a`. + // + // `zipper_sym_diff` follows the first; `fuse`'s `Xor` follows the second. + // Both are right, and the premise is wrong. `bin/alg_lattice_check.rs` + // prints the same comparison for `bool`, a real Boolean algebra, where all + // four inputs agree. + { + let c = with_val(&[], 2); + let a = with_val(&[], 1); + + let (prog, out) = FuseExpr::xor(FuseExpr::leaf(0), FuseExpr::leaf(1)).compile(); + let fused = prog.eval(&[&c, &a], &[out]).pop().unwrap(); + let by_definition = c.join(&a).subtract(&c.meet(&a)); + + println!("\n8. symmetric difference of {{_:2}} and {{_:1}}: u64 is not a lattice"); + println!(" (c|a)-(c&a) root value: {:?} (cancels)", val_at(&by_definition, &[])); + println!(" fuse Xor root value: {:?} (keeps the left)", val_at(&fused, &[])); + println!(" => both formulas are correct; u64's pjoin == pmeet makes them differ"); + println!(" see bin/alg_lattice_check, where bool agrees on all inputs"); + } + + // ---------------------------------------------------------------- 9 + // The `shape` class, which is the largest one the fuzzer reports and had no + // reproducer until now. + // + // Not a defect: whether a dangling path -- structure written with + // `create_path`, carrying no value and with nothing below it -- survives an + // operation is unsettled in the crate. What the fuzzer establishes is that + // the two families answer differently and consistently so: + // + // * the lockstep traversals in `experimental::zipper_algebra` **discard** + // dangling structure; + // * `PathMap`'s whole-map operations and the write-zipper forms + // (`join_into`, `meet_into`, `subtract_into`) **preserve** it. + // + // Worth having concretely, because whichever way the question is settled, one + // of those two families has to change, and this says which operations are on + // each side. + { + let d2 = dangling(&[&[0], &[1]]); + let dv = { + let mut m = dangling(&[&[0, 0]]); + m.write_zipper_at_path(&[1]).set_val(7); + m + }; + + println!("\n9. dangling paths: the zipper traversals drop them, the map operations keep them"); + println!(" operands: d2 = {{dangling 0, 1}}, dv = {{dangling 0, 00; value at 1}}"); + + let mut zj = PathMap::::new(); + { + let (mut a, mut b) = (d2.read_zipper(), dv.read_zipper()); + let mut wz = zj.write_zipper(); + zipper_join(&mut a, &mut b, &mut wz); + } + println!(" d2 | dv zipper_join {:?}", shape(&zj)); + println!(" PathMap::join {:?}", shape(&d2.join(&dv))); + + let mut zm = PathMap::::new(); + { + let (mut a, mut b) = (d2.read_zipper(), dv.read_zipper()); + let mut wz = zm.write_zipper(); + zipper_meet(&mut a, &mut b, &mut wz); + } + println!(" d2 & dv zipper_meet {:?}", shape(&zm)); + println!(" PathMap::meet {:?}", shape(&d2.meet(&dv))); + + // The sharpest form: symmetric difference with the empty trie should be + // the identity, and for structure it is not. + let d = dangling(&[&[0]]); + let empty = PathMap::::new(); + let mut zx = PathMap::::new(); + { + let (mut a, mut b) = (d.read_zipper(), empty.read_zipper()); + let mut wz = zx.write_zipper(); + zipper_sym_diff(&mut a, &mut b, &mut wz); + } + println!(" d ^ {{}} zipper_sym_diff {:?}", shape(&zx)); + println!( + " (d|e)-(d&e) {:?}", + shape(&d.join(&empty).subtract(&d.meet(&empty))) + ); + println!(" => not counted as a failure; the crate has not settled this"); + } + + println!("\n{} of 7 still reproduce", r.failed); + if r.failed > 0 { + std::process::exit(1); + } +} diff --git a/differential/src/bin/alg_fuzz.rs b/differential/src/bin/alg_fuzz.rs new file mode 100644 index 00000000..3e285f25 --- /dev/null +++ b/differential/src/bin/alg_fuzz.rs @@ -0,0 +1,548 @@ +//! Driver for the algebraic equivalence fuzzer. See `../../ALGEBRAIC_FUZZING.md`. +//! +//! ```sh +//! cargo run --release -p differential --bin alg_fuzz -- --random 200000 --seed 1 +//! cargo run --release -p differential --bin alg_fuzz -- differential/algebraic-corpus/*.bin +//! cargo run --release -p differential --bin alg_fuzz -- --shrink some-input.bin +//! ``` +//! +//! Everything runs in process. There is no oracle to start and no child to +//! talk to, so a case costs a few microseconds and a run is bounded by how many +//! tries it can build rather than by IPC. +//! +//! # Soundness limit +//! +//! That in-process design has a known hole: **a run that catches panics can +//! abort with heap corruption**, reproducibly, after enough of them. Every +//! panic the fuzzer catches fired *mid-mutation* inside `pathmap`'s node code -- +//! a `debug_assert!` in a merge, or `merkleize`'s `unwrap` -- and unwinding out +//! of a half-updated node leaves a trie that is not safe to drop. Measured by +//! elimination: it tracks the number of panics caught, not the build profile, +//! the thread count or the value type, and a run that catches none is clean. +//! +//! So treat the first panic in a run as the end of the useful output. Findings +//! printed before it are valid; a run that aborts has lost whatever it had not +//! yet printed. `ALGEBRAIC_FUZZING.md` has the table and the intended fix, +//! which is to make panics terminal and rare rather than caught and counted. + +use std::collections::BTreeMap; +use std::io::Write as _; +use std::panic::{self, AssertUnwindSafe}; +use std::path::{Path, PathBuf}; +use std::sync::mpsc; + +use differential::algebraic::{self, Class, Outcome, Rng, signatures}; + +/// Divergence classes that fail a run by default. +/// +/// `Shape` is not among them. Whether a dangling path survives an operation is +/// unsettled in the crate -- `SPEC_WARTS.md` and the `meet_into-keeps-dangling*` +/// corpus entries are the same question. The two families answer it differently +/// and consistently: the lockstep traversals in `experimental::zipper_algebra` +/// discard dangling structure, and `PathMap`'s whole-map operations and the +/// write-zipper forms preserve it (`bin/alg_bug_repros` case 9). Those are +/// counted and printed, so a change in them is visible, but they do not turn a +/// run red unless `--shape` asks them to. A wrong *value* is never ambiguous +/// and always fails. +const DEFAULT_FATAL: &[Class] = &[Class::Values, Class::Law]; + +struct Args { + random: usize, + seed: u64, + jobs: usize, + files: Vec, + shrink: Option, + out: PathBuf, + shape_fatal: bool, + strict: bool, + verbose: bool, + max_report: usize, + target: Option, +} + +fn usage() -> ! { + eprintln!( + "\ +usage: alg_fuzz [--random N] [--seed S] [--jobs J] [--shape] [--strict] [-v] + [--out DIR] [--max-report N] [--shrink FILE [--target SIG]] + [FILE...] + + --random N generate and check N random cases (default 10000 if no FILEs) + --seed S PRNG seed; each job derives its own stream from it (default 1) + --jobs J worker threads (default 1) + --shape treat dangling-path-only divergence as a failure too + --strict fail on every finding, including the ones in algebraic::KNOWN + --out DIR where failing inputs are written + (default differential/algebraic-corpus) + --max-report N stop printing individual findings after N (default 20) + --shrink FILE minimise FILE while it still diverges the same way, then exit + --target SIG with --shrink, the signature to preserve (default: the first + one FILE produces, which is not always the one you wanted) + -v print every finding's detail, not just the first few + FILE... replay these inputs instead of generating + +Exit status is 1 if any finding's signature is absent from algebraic::KNOWN, +which documents what already reproduces on master and why. Known findings are +still counted and printed." + ); + std::process::exit(2) +} + +fn parse() -> Args { + let mut a = Args { + random: 0, + seed: 1, + jobs: 1, + files: Vec::new(), + shrink: None, + out: PathBuf::from("differential/algebraic-corpus"), + shape_fatal: false, + strict: false, + verbose: false, + max_report: 20, + target: None, + }; + let mut it = std::env::args().skip(1); + while let Some(arg) = it.next() { + let num = |it: &mut dyn Iterator| -> u64 { + it.next().and_then(|s| s.parse().ok()).unwrap_or_else(|| usage()) + }; + match arg.as_str() { + "--random" => a.random = num(&mut it) as usize, + "--seed" => a.seed = num(&mut it), + "--jobs" => a.jobs = (num(&mut it) as usize).max(1), + "--max-report" => a.max_report = num(&mut it) as usize, + "--out" => a.out = PathBuf::from(it.next().unwrap_or_else(|| usage())), + "--shrink" => a.shrink = Some(PathBuf::from(it.next().unwrap_or_else(|| usage()))), + "--shape" => a.shape_fatal = true, + "--strict" => a.strict = true, + "--target" => a.target = Some(it.next().unwrap_or_else(|| usage())), + "-v" | "--verbose" => a.verbose = true, + "-h" | "--help" => usage(), + s if s.starts_with('-') => usage(), + s => a.files.push(PathBuf::from(s)), + } + } + if a.random == 0 && a.files.is_empty() && a.shrink.is_none() { + a.random = 10_000; + } + a +} + +// ------------------------------------------------------------------ driving + +struct Tally { + cases: usize, + by_signature: BTreeMap, + examples: Vec<(String, Vec, String)>, +} + +impl Tally { + fn new() -> Tally { + Tally { cases: 0, by_signature: BTreeMap::new(), examples: Vec::new() } + } + + /// Record one outcome. `cases` counts inputs, not outcomes, so only the + /// first value type of each input increments it. + fn record(&mut self, type_name: &str, bytes: &[u8], outcome: Outcome, count: bool) { + if count { + self.cases += 1; + } + let findings: Vec<(String, String)> = match outcome { + Outcome::Clean => return, + Outcome::Panicked(p, site, msg) => { + vec![( + algebraic::panic_signature(type_name, p, &site), + format!("panicked at {site}: {msg}"), + )] + } + Outcome::Diverged(d) => { + d.into_iter().map(|d| (d.signature, d.detail)).collect() + } + }; + for (sig, detail) in findings { + let seen = self.by_signature.entry(sig.clone()).or_insert(0); + *seen += 1; + // One saved example per signature: the point of the corpus is one + // reproducer per distinct defect, not one per input that hits it. + if *seen == 1 { + self.examples.push((sig, bytes.to_vec(), detail)); + } + } + } + + fn merge(&mut self, other: Tally) { + self.cases += other.cases; + for (sig, n) in other.by_signature { + *self.by_signature.entry(sig).or_insert(0) += n; + } + for (sig, bytes, detail) in other.examples { + if !self.examples.iter().any(|(s, _, _)| *s == sig) { + self.examples.push((sig, bytes, detail)); + } + } + } +} + +fn main() { + let args = parse(); + + // Replaces the default hook, which would print a backtrace notice per + // panicking case and drown a long run. It also records the panic site, + // which `catch_unwind` alone cannot see. + algebraic::install_panic_hook(); + + if let Some(path) = &args.shrink { + do_shrink(path, args.target.as_deref()); + return; + } + + let mut tally = Tally::new(); + + if !args.files.is_empty() { + for f in &args.files { + let bytes = std::fs::read(f).unwrap_or_else(|e| { + eprintln!("{}: {e}", f.display()); + std::process::exit(2) + }); + let mut labels = Vec::new(); + let mut first = true; + algebraic::run_all(&bytes, &mut |name, outcome| { + labels.push(match &outcome { + Outcome::Clean => format!("{name}: clean"), + Outcome::Diverged(d) => format!("{name}: {} finding(s)", d.len()), + Outcome::Panicked(p, site, m) => { + format!("{name}: panic in {} at {site}: {m}", p.tag()) + } + }); + tally.record(name, &bytes, outcome, first); + first = false; + }); + println!("{}: {}", f.display(), labels.join(", ")); + } + } + + if args.random > 0 { + let per = args.random / args.jobs; + let (tx, rx) = mpsc::channel(); + let mut handles = Vec::new(); + for job in 0..args.jobs { + let tx = tx.clone(); + let seed = args.seed; + let n = if job == args.jobs - 1 { args.random - per * (args.jobs - 1) } else { per }; + handles.push(std::thread::spawn(move || { + let mut rng = Rng::for_job(seed, job); + let mut t = Tally::new(); + for _ in 0..n { + let bytes = rng.input(); + let mut first = true; + algebraic::run_all(&bytes, &mut |name, outcome| { + t.record(name, &bytes, outcome, first); + first = false; + }); + } + let _ = tx.send(t); + })); + } + drop(tx); + for t in rx { + tally.merge(t); + } + for h in handles { + let _ = h.join(); + } + } + + report(&args, &mut tally); +} + +fn report(args: &Args, tally: &mut Tally) { + println!("\nchecked {} case(s)", tally.cases); + if tally.by_signature.is_empty() { + println!("no divergence"); + return; + } + + println!("\nfindings by signature:"); + for (sig, n) in &tally.by_signature { + match algebraic::known(sig) { + Some(k) => println!(" {n:>8} {sig} (known: {})", k.cause), + None => println!(" {n:>8} {sig} <-- NEW"), + } + } + + value_type_comparison(tally); + + if let Err(e) = std::fs::create_dir_all(&args.out) { + eprintln!("cannot create {}: {e}", args.out.display()); + } + + let shown = if args.verbose { tally.examples.len() } else { args.max_report.min(tally.examples.len()) }; + println!("\nsaved reproducers in {}:", args.out.display()); + for (i, (sig, bytes, detail)) in tally.examples.iter().enumerate() { + let stem = sanitize(sig); + let bin = args.out.join(format!("{stem}.bin")); + let txt = args.out.join(format!("{stem}.txt")); + let _ = std::fs::write(&bin, bytes); + // Rendering the case means building the operands again, which for a + // `panic:build` finding panics again. Catch it: the reproducer is + // still worth writing, it just cannot describe itself. + let described = panic::catch_unwind(AssertUnwindSafe(|| { + algebraic::describe_as(algebraic::value_type_of(sig), bytes) + })) + .unwrap_or_else(|_| "\n".to_string()); + let body = format!("signature: {sig}\n\n{described}\n{detail}\n"); + let _ = std::fs::write(&txt, &body); + println!(" {}", bin.display()); + if i < shown { + for line in body.lines() { + println!(" {line}"); + } + } + } + + let fatal: Vec<&str> = tally + .by_signature + .keys() + .map(|s| s.as_str()) + .filter(|sig| is_fatal(sig, args)) + .collect(); + if fatal.is_empty() { + println!("\nnothing unexpected: every signature is in algebraic::KNOWN"); + } else { + println!("\n{} unexpected signature(s): {}", fatal.len(), fatal.join(" ")); + std::process::exit(1); + } +} + +/// Whether a signature should fail the run. +/// +/// `--strict` fails on anything. Otherwise a signature in `algebraic::KNOWN` +/// is excused, a panic or a wrong value is fatal, and a dangling-path-only +/// divergence is fatal only under `--shape`. +/// Print which findings each value type sees, which is the question the two +/// instantiations exist to answer. +/// +/// A signature under `u64` alone is an artefact of its lattice instances, which +/// are not a lattice: `pjoin` and `pmeet` both return the left operand, so +/// `a | b == a & b` and several identities cannot hold. A signature under the +/// lawful type -- alone, or under both -- is a defect in the crate. +/// +/// The counts matter as much as the membership. A law that fails 3000 times +/// under `u64` and 12 times under `bits` is one defect amplified by the value +/// type, not two findings: under a commutative join, picking the wrong operand +/// is invisible except where one operand already contains the other, so only +/// that residue survives. +fn value_type_comparison(tally: &Tally) { + let types = algebraic::VALUE_TYPES; + if types.len() < 2 { + return; + } + + // Strip the value-type prefix: `u64:values:pw1` -> `values:pw1`. + let rest = |sig: &str| sig.splitn(2, ':').nth(1).unwrap_or(sig).to_string(); + let per_type: Vec> = types + .iter() + .map(|t| { + tally + .by_signature + .iter() + .filter(|(sig, _)| algebraic::value_type_of(sig) == *t) + .map(|(sig, n)| (rest(sig), *n)) + .collect() + }) + .collect(); + + let mut all: Vec = per_type.iter().flat_map(|m| m.keys().cloned()).collect(); + all.sort(); + all.dedup(); + if all.is_empty() { + return; + } + + let lawful: Vec<&str> = + types.iter().copied().filter(|t| *t != "u64").collect(); + println!("\nby value type -- {} are lawful, u64 is not:", lawful.join(" and ")); + print!(" {:<38}", "finding"); + for t in types { + print!(" {t:>9}"); + } + println!(); + + // Which types see each finding, so the groups below can be built by subset. + let mut by_subset: BTreeMap, Vec> = BTreeMap::new(); + for k in &all { + print!(" {k:<38}"); + let mut seen = Vec::new(); + for (i, t) in types.iter().enumerate() { + match per_type[i].get(k) { + Some(n) => { + print!(" {n:>9}"); + seen.push(*t); + } + None => print!(" {:>9}", "-"), + } + } + println!(); + by_subset.entry(seen).or_default().push(k.clone()); + } + + println!("\nseen under:"); + for (subset, findings) in &by_subset { + let note = if subset.len() == types.len() { + " <- value-independent, or one defect amplified; read the counts" + } else if subset == &["u64"] { + " <- artefacts: u64's instances are not a lattice" + } else if subset.contains(&"u64") { + "" + } else { + " <- REAL, and u64 was hiding them" + }; + println!(" {:<22}{note}", subset.join(" + ")); + for f in findings { + println!(" {f}"); + } + } +} + +fn is_fatal(sig: &str, args: &Args) -> bool { + if args.strict { + return true; + } + if algebraic::known(sig).is_some() { + return false; + } + // The class is the *second* field: signatures are `::...`. + // Matching against the start of the whole signature silently stopped working + // when the value-type prefix was added, which made every class fall through + // to "not fatal" and left the gate passing runs that had turned up new + // findings. Parse the field rather than the prefix. + let class = sig.split(':').nth(1).unwrap_or(""); + match class { + "panic" => true, + "shape" => args.shape_fatal, + c => DEFAULT_FATAL.iter().any(|f| f.tag() == c), + } +} + +fn sanitize(sig: &str) -> String { + sig.chars() + .map(|c| match c { + 'a'..='z' | 'A'..='Z' | '0'..='9' | '-' | '_' => c, + '|' => 'J', + '&' => 'M', + '^' => 'X', + '/' => 'R', + _ => '-', + }) + .collect() +} + +// ----------------------------------------------------------------- shrinking + +/// Minimise an input while it still produces the finding it started with. +/// +/// Byte-level delta debugging, in two passes repeated to a fixed point: drop +/// runs of bytes, then drive individual bytes towards zero. The second pass +/// matters more than it looks -- the decoder reads path bytes modulo a small +/// alphabet and entry counts modulo a small bound, so lowering a byte usually +/// shrinks the *tries* rather than the input, which is what makes the saved +/// reproducer readable. +/// +/// The invariant preserved is the original's first signature, not its whole +/// set: a smaller input often stops hitting the incidental extra findings, and +/// insisting on all of them would block almost every reduction. +fn do_shrink(path: &Path, want: Option<&str>) { + let original = std::fs::read(path).unwrap_or_else(|e| { + eprintln!("{}: {e}", path.display()); + std::process::exit(2) + }); + let sigs = signatures(&original); + if sigs.is_empty() { + eprintln!("{}: no divergence to shrink", path.display()); + std::process::exit(2) + } + let target = match want { + Some(w) => { + if !sigs.iter().any(|s| s == w) { + eprintln!( + "{}: does not produce {w}; it produces {}", + path.display(), + sigs.join(" ") + ); + std::process::exit(2) + } + w.to_string() + } + // An input usually hits several findings at once, and which one comes + // first is an artefact of route order. Say which was picked, so a + // surprising reduction is explainable rather than mysterious. + None => sigs[0].clone(), + }; + eprintln!( + "shrinking {} bytes, target {target} (of {})", + original.len(), + sigs.join(" ") + ); + + let holds = |b: &[u8]| signatures(b).iter().any(|s| *s == target); + let mut best = original; + + loop { + let before = (best.len(), best.iter().map(|b| *b as u32).sum::()); + + let mut chunk = best.len().next_power_of_two() / 2; + while chunk >= 1 { + let mut i = 0; + while i < best.len() { + let end = (i + chunk).min(best.len()); + let mut cand = best[..i].to_vec(); + cand.extend_from_slice(&best[end..]); + if !cand.is_empty() && holds(&cand) { + best = cand; + } else { + i += chunk; + } + } + chunk /= 2; + } + + for i in 0..best.len() { + for v in [0u8, 1, best[i] / 2] { + if best[i] <= v { + continue; + } + let mut cand = best.clone(); + cand[i] = v; + if holds(&cand) { + best = cand; + break; + } + } + } + + if (best.len(), best.iter().map(|b| *b as u32).sum::()) == before { + break; + } + } + + let out = path.with_extension("min.bin"); + std::fs::write(&out, &best).unwrap(); + eprintln!("shrunk to {} bytes -> {}", best.len(), out.display()); + + let described = panic::catch_unwind(AssertUnwindSafe(|| { + algebraic::describe_as(algebraic::value_type_of(&target), &best) + })) + .unwrap_or_else(|_| "\n".to_string()); + print!("{described}"); + algebraic::run_all(&best, &mut |name, outcome| match outcome { + Outcome::Clean => println!("{name}: no divergence"), + Outcome::Panicked(p, site, m) => println!("{name}: panic in {} at {site}: {m}", p.tag()), + Outcome::Diverged(d) => { + for div in d { + println!("[{}] {}\n{}", div.class.tag(), div.signature, div.detail); + } + } + }); + let _ = std::io::stdout().flush(); +} diff --git a/differential/src/bin/alg_lattice_check.rs b/differential/src/bin/alg_lattice_check.rs new file mode 100644 index 00000000..95f5c6e3 --- /dev/null +++ b/differential/src/bin/alg_lattice_check.rs @@ -0,0 +1,208 @@ +//! Is a divergence the crate's fault, or the value type's? +//! +//! `(a | b) \ (a & b)` and `(a \ b) | (b \ a)` are equal in any distributive +//! lattice with a relative complement, so a divergence between them is never a +//! matter of convention. This prints both formulas for several value types and +//! shows which ones are lawful. +//! +//! It also asks a second question, which turns out to be the more important one +//! for fuzzing: does the type's `pjoin`/`pmeet`/`psubtract` ever return +//! `AlgebraicResult::Element` -- a combined value that is not simply one of its +//! operands? If not, every code path that *stores* a combined value is +//! unreachable from that type, however lawful it is. +//! +//! ```sh +//! cargo run --release -p differential --bin alg_lattice_check +//! ``` + +use core::fmt::Debug; +use pathmap::ring::{AlgebraicResult, DistributiveLattice, Lattice, COUNTER_IDENT, SELF_IDENT}; +use pathmap::utils::ByteMask; + +/// Bottom is `None`, as it is everywhere in `pathmap`: a value that cancels +/// becomes an absent value, not a present zero. Resolving through `Option` +/// uses the crate's own `Option` lattice impls, so this says nothing the +/// trie does not. +fn resolve(r: AlgebraicResult>, l: &Option, rr: &Option) -> Option { + match r { + AlgebraicResult::Element(v) => v, + AlgebraicResult::Identity(m) => { + if m & SELF_IDENT != 0 { l.clone() } else { rr.clone() } + } + AlgebraicResult::None => None, + } +} + +fn show(v: &Option) -> String { + match v { + None => "BOTTOM".to_string(), + Some(v) => format!("{v:?}"), + } +} + +/// `(a | b) \ (a & b)` and `(a \ b) | (b \ a)`, each resolved to a value. +fn two_formulas(a: T, b: T) -> (String, String, String, String, bool) +where + T: Lattice + DistributiveLattice + Clone + Debug, +{ + let (ao, bo) = (Some(a), Some(b)); + let j = resolve(ao.pjoin(&bo), &ao, &bo); + let m = resolve(ao.pmeet(&bo), &ao, &bo); + let f1 = resolve(j.psubtract(&m), &j, &m); + + let ab = resolve(ao.psubtract(&bo), &ao, &bo); + let ba = resolve(bo.psubtract(&ao), &bo, &ao); + let f2 = resolve(ab.pjoin(&ba), &ab, &ba); + + let agree = show(&f1) == show(&f2); + (show(&j), show(&m), show(&f1), show(&f2), agree) +} + +fn row(label: String, a: T, b: T) +where + T: Lattice + DistributiveLattice + Clone + Debug, +{ + let (j, m, f1, f2, agree) = two_formulas(a, b); + println!( + " {label:<22} a|b = {j:>9} a&b = {m:>9} (a|b)-(a&b) = {f1:>9} (a-b)|(b-a) = {f2:>9} {}", + if agree { "agree" } else { "DIVERGE" } + ); +} + +/// Whether each operation ever returns `Element` over a sample of pairs. +fn element_per_op(sample: &[T]) -> (bool, bool, bool) +where + T: Lattice + DistributiveLattice + Clone, +{ + let mut out = (false, false, false); + for a in sample { + for b in sample { + out.0 |= matches!(a.pjoin(b), AlgebraicResult::Element(_)); + out.1 |= matches!(a.pmeet(b), AlgebraicResult::Element(_)); + out.2 |= matches!(a.psubtract(b), AlgebraicResult::Element(_)); + } + } + out +} + +fn yn(b: bool) -> &'static str { + if b { "yes" } else { "NO " } +} + +// ---------------------------------------------------------------- candidates + +/// Bitmask: `pjoin` is `|`, `pmeet` is `&`, `psubtract` is `& !`, and an empty +/// result collapses to `None`. A Boolean algebra -- the powerset of 64 +/// elements -- so every lattice identity holds. This is exactly what +/// `[u64; 4]` already does in `pathmap::utils`; only the width differs. +#[derive(Clone, Copy, PartialEq, Eq)] +struct Bits(u64); + +impl Debug for Bits { + fn fmt(&self, f: &mut core::fmt::Formatter<'_>) -> core::fmt::Result { + write!(f, "{:04b}", self.0) + } +} + +fn bits_result(r: u64, l: u64, rr: u64) -> AlgebraicResult { + if r == 0 { + return AlgebraicResult::None; + } + let mut m = 0; + if r == l { m = SELF_IDENT } + if r == rr { m |= COUNTER_IDENT } + if m != 0 { AlgebraicResult::Identity(m) } else { AlgebraicResult::Element(Bits(r)) } +} + +impl Lattice for Bits { + fn pjoin(&self, o: &Self) -> AlgebraicResult { bits_result(self.0 | o.0, self.0, o.0) } + fn pmeet(&self, o: &Self) -> AlgebraicResult { bits_result(self.0 & o.0, self.0, o.0) } +} +impl DistributiveLattice for Bits { + fn psubtract(&self, o: &Self) -> AlgebraicResult { bits_result(self.0 & !o.0, self.0, o.0) } +} + +/// The total order: `pjoin` is `max`, `pmeet` is `min`, bottom is 0. Also a +/// genuine distributive lattice -- every total order is one -- and here to make +/// the point that lawfulness is not sufficient. +#[derive(Clone, Copy, PartialEq, Eq, Debug)] +struct MinMax(u64); + +fn minmax_result(r: u64, l: u64, rr: u64) -> AlgebraicResult { + if r == 0 { + return AlgebraicResult::None; + } + let mut m = 0; + if r == l { m = SELF_IDENT } + if r == rr { m |= COUNTER_IDENT } + if m != 0 { AlgebraicResult::Identity(m) } else { AlgebraicResult::Element(MinMax(r)) } +} + +impl Lattice for MinMax { + fn pjoin(&self, o: &Self) -> AlgebraicResult { minmax_result(self.0.max(o.0), self.0, o.0) } + fn pmeet(&self, o: &Self) -> AlgebraicResult { minmax_result(self.0.min(o.0), self.0, o.0) } +} +impl DistributiveLattice for MinMax { + fn psubtract(&self, o: &Self) -> AlgebraicResult { + minmax_result(if self.0 > o.0 { self.0 } else { 0 }, self.0, o.0) + } +} + +fn bm(bits: &[u8]) -> ByteMask { + let mut m = [0u64; 4]; + for b in bits { + m[(*b / 64) as usize] |= 1 << (*b % 64); + } + ByteMask(m) +} + +fn main() { + println!("Are the two formulas for symmetric difference equal?\n"); + + println!("u64 -- what the fuzzer uses; pjoin is left-biased, pmeet is Identity(SELF)"); + for (a, b) in [(1u64, 2u64), (3, 7), (5, 5)] { + row(format!("a={a} b={b}"), a, b); + } + println!(" ^ a|b == a&b for every pair, so this is not a lattice: in one,"); + println!(" a&b == a|b forces a == b, i.e. the impl asserts 1 == 2.\n"); + + println!("bool -- a real two-element Boolean algebra, same file"); + for (a, b) in [(true, false), (true, true), (false, false)] { + row(format!("a={a} b={b}"), a, b); + } + + println!("\nBits(u64) -- pjoin = |, pmeet = &, psubtract = & !, empty -> None"); + for (a, b) in [(0b0011u64, 0b0101u64), (0b0001, 0b0010), (0b0011, 0b0011)] { + row(format!("a={a:04b} b={b:04b}"), Bits(a), Bits(b)); + } + + println!("\nByteMask -- the crate already implements exactly that, at 256 bits"); + for (a, b) in [(&[0u8, 1][..], &[1u8, 2][..]), (&[0][..], &[1][..]), (&[3][..], &[3][..])] { + row(format!("a={a:?} b={b:?}"), bm(a), bm(b)); + } + + println!("\nMinMax(u64) -- pjoin = max, pmeet = min; also a lawful distributive lattice"); + for (a, b) in [(5u64, 3u64), (3, 5), (4, 4)] { + row(format!("a={a} b={b}"), MinMax(a), MinMax(b)); + } + + println!("\n\nDoes each operation ever return AlgebraicResult::Element,"); + println!("i.e. a combined value that is not simply one of its operands?\n"); + println!(" {:<12} {:>7} {:>7} {:>10}", "type", "pjoin", "pmeet", "psubtract"); + let show_ops = |name: &str, (j, m, s): (bool, bool, bool)| { + println!(" {name:<12} {:>7} {:>7} {:>10}", yn(j), yn(m), yn(s)); + }; + show_ops("u64", element_per_op(&[1u64, 2, 3, 5, 7])); + show_ops("bool", element_per_op(&[true, false])); + show_ops("MinMax", element_per_op(&[MinMax(1), MinMax(2), MinMax(3), MinMax(5)])); + show_ops("Bits", element_per_op(&[Bits(0b0011), Bits(0b0101), Bits(0b1001), Bits(0b0110)])); + show_ops("ByteMask", element_per_op(&[bm(&[0, 1]), bm(&[1, 2]), bm(&[2, 3]), bm(&[0, 3])])); + + println!("\n u64's one \"yes\" is `Element(*self)` -- an Element whose value equals self,"); + println!(" which is why PR #115 retags it as Identity(SELF_IDENT). That is the right"); + println!(" fix, and it leaves u64 unable to produce Element from any operation at all."); + println!("\n MinMax is lawful and still answers NO everywhere: max(a,b) and min(a,b)"); + println!(" are always one of the operands, so a lattice can be perfectly correct and"); + println!(" still never exercise the code that stores a combined value. Only the"); + println!(" bitmask family answers yes, because a|b is genuinely a new value."); +} diff --git a/differential/src/lib.rs b/differential/src/lib.rs index 661cf803..a3c5e052 100644 --- a/differential/src/lib.rs +++ b/differential/src/lib.rs @@ -8,8 +8,13 @@ //! * [`server`] is the resident-process protocol the driver speaks. //! * [`repro`] turns an input back into standalone `pathmap` calls. //! * [`act`] is the `ArenaCompactTree` read source behind `act_trace`. +//! +//! [`algebraic`] is a third fuzzer with a different question. It has no +//! oracle: it evaluates one algebraic expression every way the crate offers and +//! requires the answers to match. `bin/alg_fuzz.rs` drives it. pub mod act; +pub mod algebraic; pub mod harness; pub mod repro; pub mod server; diff --git a/differential/tests/algebraic.rs b/differential/tests/algebraic.rs new file mode 100644 index 00000000..8e4f1b72 --- /dev/null +++ b/differential/tests/algebraic.rs @@ -0,0 +1,439 @@ +//! Regression gate for the algebraic equivalence fuzzer. +//! +//! Three things, cheap enough for `cargo test`: +//! +//! * the committed corpus still reproduces only what `KNOWN` documents; +//! * a short random sweep from a fixed seed turns up nothing new; +//! * the expression recognisers that decide which route applies to which shape +//! agree with what the n-ary and DNF entry points actually compute. +//! +//! The last one is not incidental. Both recognisers were wrong when this +//! fuzzer was first run, and both failures looked exactly like crate defects: +//! flattening `a ^ (b ^ c)` into the n-ary call, which folds values left, and +//! letting a DNF clause stand for `b & a` when a clause is an unordered set and +//! `pmeet` is left-biased. A harness that reports its own mistakes as findings +//! is worse than no harness, so the recognisers are pinned here. + +use differential::algebraic::{ + self, + expr::{Expr, Op}, + known, signatures, + value::{Bits, FuzzValue}, +}; +use pathmap::ring::{AlgebraicResult, DistributiveLattice, Lattice}; + +/// Collect the signatures an input produces that `KNOWN` does not document. +/// +/// Returns them rather than asserting, because `install_panic_hook` silences +/// the panic hook for the duration -- which is the point, since the inputs make +/// `pathmap` panic -- and a silenced hook would swallow the assertion message +/// too. So every caller gathers first, restores the hook, then asserts. +fn unknown_signatures(bytes: &[u8]) -> Vec { + signatures(bytes).into_iter().filter(|s| known(s).is_none()).collect() +} + +fn complain(found: &[(String, String)]) -> String { + let mut m = String::from("unexpected signature(s):\n"); + for (sig, where_) in found { + m.push_str(&format!(" {sig} from {where_}\n")); + } + m.push_str( + "\nIf a defect was just fixed, drop its entry from algebraic::KNOWN.\n\ + If it is new, shrink it with\n\ + \x20 cargo run --release -p differential --bin alg_fuzz -- \\\n\ + \x20 --shrink --target \n\ + and add a reproducer to bin/alg_bug_repros.rs.\n", + ); + m +} + +/// Serialises the tests that install a panic hook. +/// +/// `set_hook` and `take_hook` are process-global while `cargo test` runs tests +/// on several threads, so two of these running at once interleave: one restores +/// the default hook under the other, the other's panics stop being recorded, +/// and the signature it reports is whatever site was recorded last. That shows +/// up as a phantom unexpected signature in whichever test lost the race. +static PANIC_HOOK: std::sync::Mutex<()> = std::sync::Mutex::new(()); + +/// Run `f` with the fuzzer's panic hook installed, restoring the previous hook +/// afterwards so a later assertion can still report itself. +fn with_quiet_panics(f: impl FnOnce() -> T) -> T { + // A failing test panics *outside* this function, so the lock is never + // poisoned by the assertion itself -- but `f` runs code that panics by + // design, so recover from poisoning rather than propagating it. + let _guard = PANIC_HOOK.lock().unwrap_or_else(|e| e.into_inner()); + let prev = std::panic::take_hook(); + algebraic::install_panic_hook(); + let out = f(); + std::panic::set_hook(prev); + out +} + +#[test] +fn corpus_reproduces_only_known_findings() { + let dir = concat!(env!("CARGO_MANIFEST_DIR"), "/algebraic-corpus"); + let (seen, found) = with_quiet_panics(|| { + let mut seen = 0; + let mut found = Vec::new(); + for entry in std::fs::read_dir(dir).expect("corpus directory") { + let path = entry.expect("corpus entry").path(); + if path.extension().is_none_or(|e| e != "bin") { + continue; + } + let bytes = std::fs::read(&path).expect("corpus file"); + for sig in unknown_signatures(&bytes) { + found.push((sig, path.display().to_string())); + } + seen += 1; + } + (seen, found) + }); + assert!(seen > 0, "corpus is empty: {dir}"); + assert!(found.is_empty(), "{}", complain(&found)); +} + +#[test] +fn random_sweep_turns_up_nothing_new() { + // Small, because this runs unoptimised under `cargo test` and is only a + // tripwire. The real sweep is `alg_fuzz --random`, which does a million + // cases in under twenty seconds. + const CASES: usize = 5_000; + let found = with_quiet_panics(|| { + let mut rng = algebraic::Rng::for_job(20261002, 0); + let mut found = Vec::new(); + for i in 0..CASES { + let bytes = rng.input(); + for sig in unknown_signatures(&bytes) { + found.push((sig, format!("case {i} of seed 20261002"))); + } + } + found + }); + assert!(found.is_empty(), "{}", complain(&found)); +} + +// --------------------------------------------------- recogniser invariants + +fn var(i: usize) -> Expr { + Expr::Var(i) +} + +#[test] +fn chain_flattens_left_nesting_for_every_chainable_operator() { + for op in [Op::Join, Op::Meet, Op::Subtract, Op::SymDiff] { + let e = Expr::bin(op, Expr::bin(op, var(0), var(1)), var(2)); + assert_eq!(e.chain(), Some((op, vec![0, 1, 2])), "{op:?} left-nested"); + } +} + +#[test] +fn chain_rejects_right_nesting_where_the_n_ary_fold_would_differ() { + // `zipper_n_subtract` is left-associative and the symmetric-difference fold + // combines values left to right, so neither may be matched right-nested. + for op in [Op::Subtract, Op::SymDiff] { + let e = Expr::bin(op, var(0), Expr::bin(op, var(1), var(2))); + assert_eq!(e.chain(), None, "{op:?} right-nested must not be a chain"); + } + // Join and meet are left-biased in their values, so both nestings agree + // with the fold and both are chains. + for op in [Op::Join, Op::Meet] { + let e = Expr::bin(op, var(0), Expr::bin(op, var(1), var(2))); + assert_eq!(e.chain(), Some((op, vec![0, 1, 2])), "{op:?} right-nested"); + } +} + +#[test] +fn chain_rejects_a_mixed_tree() { + let e = Expr::bin(Op::Join, Expr::bin(Op::Meet, var(0), var(1)), var(2)); + assert_eq!(e.chain(), None); +} + +#[test] +fn dnf_recognises_a_join_of_meets() { + // (a & b) | c + let e = Expr::bin(Op::Join, Expr::bin(Op::Meet, var(0), var(1)), var(2)); + assert_eq!(e.dnf(), Some(vec![0b011, 0b100])); +} + +#[test] +fn dnf_rejects_a_clause_whose_operands_are_out_of_slot_order() { + // A clause is a bitmask, so it cannot distinguish `b & a` from `a & b`, + // and `pmeet` on u64 keeps the left value, so the two differ. + assert_eq!(Expr::bin(Op::Meet, var(0), var(1)).dnf(), Some(vec![0b011])); + assert_eq!(Expr::bin(Op::Meet, var(1), var(0)).dnf(), None); +} + +#[test] +fn dnf_rejects_non_monotone_operators() { + for op in [Op::Subtract, Op::SymDiff, Op::Restrict] { + assert_eq!(Expr::bin(op, var(0), var(1)).dnf(), None, "{op:?}"); + } +} + +/// The lawful value type has to actually be lawful, or every "real defect" the +/// comparison attributes to the crate could be its fault instead. +/// The `shape` class's characterisation, as `bin/alg_bug_repros` case 9 states it: +/// the lockstep traversals discard dangling structure and the whole-map +/// operations preserve it. +/// +/// Pinned because the write-up had it backwards at first, and because if either +/// family changes, the right outcome is this test failing and the question being +/// settled -- not the claim quietly going stale. +#[test] +fn zipper_traversals_drop_dangling_paths_and_map_ops_keep_them() { + use pathmap::experimental::zipper_algebra::{zipper_join, zipper_meet}; + use pathmap::zipper::{ZipperMoving, ZipperPath, ZipperWriting}; + use pathmap::PathMap; + + fn dangling(paths: &[&[u8]]) -> PathMap { + let mut m = PathMap::new(); + let mut wz = m.write_zipper(); + for p in paths { + wz.reset(); + wz.descend_to(*p); + wz.create_path(); + } + drop(wz); + m + } + fn paths(m: &PathMap) -> Vec> { + let mut z = m.read_zipper(); + let mut out = Vec::new(); + z.reset(); + while z.to_next_step() { + out.push(z.path().to_vec()); + } + out + } + + let d2 = dangling(&[&[0], &[1]]); + let dv = { + let mut m = dangling(&[&[0, 0]]); + m.write_zipper_at_path(&[1]).set_val(7); + m + }; + + let mut zj = PathMap::::new(); + { + let (mut a, mut b) = (d2.read_zipper(), dv.read_zipper()); + let mut wz = zj.write_zipper(); + zipper_join(&mut a, &mut b, &mut wz); + } + // The traversal keeps only the path that carries a value. + assert_eq!(paths(&zj), vec![vec![1]]); + // The whole-map operation keeps the dangling structure too. + assert_eq!(paths(&d2.join(&dv)), vec![vec![0], vec![0, 0], vec![1]]); + + let mut zm = PathMap::::new(); + { + let (mut a, mut b) = (d2.read_zipper(), dv.read_zipper()); + let mut wz = zm.write_zipper(); + zipper_meet(&mut a, &mut b, &mut wz); + } + assert!(paths(&zm).is_empty()); + assert_eq!(paths(&d2.meet(&dv)), vec![vec![0], vec![1]]); + + // The write-zipper forms side with the whole-map operations. + let mut wi = d2.clone(); + { + let mut wz = wi.write_zipper(); + wz.meet_into(&dv.read_zipper(), false); + } + assert_eq!(paths(&wi), paths(&d2.meet(&dv))); +} + +/// The zipper algebra over `PathMap<()>`, which `zipper_algebra.rs` does not +/// test at all -- every test there uses `u64`. +/// +/// `()` is lawful, so these are plain set operations and the expected answers +/// are not open to interpretation. Spelled out rather than compared against +/// `PathMap::join` and friends, because those have defects of their own. +#[test] +fn zipper_algebra_over_the_unit_type() { + use pathmap::experimental::zipper_algebra::{ + zipper_join, zipper_meet, zipper_n_meet, zipper_n_sym_diff, zipper_subtract, + zipper_sym_diff, + }; + use pathmap::zipper::{ZipperMoving, ZipperPath, ZipperValues}; + use pathmap::PathMap; + + fn mk(paths: &[&[u8]]) -> PathMap<()> { + let mut m = PathMap::new(); + for p in paths { + m.set_val_at(p, ()); + } + m + } + fn set(m: &PathMap<()>) -> Vec> { + let mut z = m.read_zipper(); + let mut out = Vec::new(); + z.reset(); + while z.to_next_step() { + if z.val().is_some() { + out.push(z.path().to_vec()); + } + } + out + } + + let a = mk(&[&[0, 1], &[0, 2], &[3]]); + let b = mk(&[&[0, 2], &[3], &[4]]); + let c = mk(&[&[0, 2], &[5]]); + + macro_rules! pair { + ($f:ident) => {{ + let mut out = PathMap::<()>::new(); + { + let (mut za, mut zb) = (a.read_zipper(), b.read_zipper()); + let mut wz = out.write_zipper(); + $f(&mut za, &mut zb, &mut wz); + } + set(&out) + }}; + } + assert_eq!(pair!(zipper_join), vec![vec![0, 1], vec![0, 2], vec![3], vec![4]]); + assert_eq!(pair!(zipper_meet), vec![vec![0, 2], vec![3]]); + assert_eq!(pair!(zipper_subtract), vec![vec![0, 1]]); + // Present in exactly one side. + assert_eq!(pair!(zipper_sym_diff), vec![vec![0, 1], vec![4]]); + + macro_rules! triple { + ($f:ident) => {{ + let mut out = PathMap::<()>::new(); + { + let mut zs = [a.read_zipper(), b.read_zipper(), c.read_zipper()]; + let mut wz = out.write_zipper(); + $f(&mut zs, &mut wz); + } + set(&out) + }}; + } + // Only [0,2] is in all three. + assert_eq!(triple!(zipper_n_meet), vec![vec![0, 2]]); + // Odd number of occurrences: [0,1] in one, [0,2] in three, [3] in two, [4] + // and [5] in one each. + assert_eq!( + triple!(zipper_n_sym_diff), + vec![vec![0, 1], vec![0, 2], vec![4], vec![5]] + ); +} + +#[test] +fn bits_is_a_boolean_algebra() { + let sample: Vec = (1u64..16).map(Bits).collect(); + let r = |x: AlgebraicResult, l: Bits, rr: Bits| match x { + AlgebraicResult::Element(v) => Some(v), + // SELF_IDENT == 1 + AlgebraicResult::Identity(m) => Some(if m & 1 != 0 { l } else { rr }), + AlgebraicResult::None => None, + }; + let raw = |v: Option| v.map(|b| b.0).unwrap_or(0); + + for &a in &sample { + for &b in &sample { + // The operations are the bitwise ones, and bottom is absence. + assert_eq!(raw(r(a.pjoin(&b), a, b)), a.0 | b.0, "join {a:?} {b:?}"); + assert_eq!(raw(r(a.pmeet(&b), a, b)), a.0 & b.0, "meet {a:?} {b:?}"); + assert_eq!(raw(r(a.psubtract(&b), a, b)), a.0 & !b.0, "sub {a:?} {b:?}"); + // Commutative, which is exactly what makes the u64 value bias + // invisible here and so must hold. + assert_eq!(a.0 | b.0, b.0 | a.0); + assert_eq!(a.0 & b.0, b.0 & a.0); + // The two formulas for symmetric difference agree -- the identity + // whose failure under u64 started this. + assert_eq!((a.0 | b.0) & !(a.0 & b.0), (a.0 & !b.0) | (b.0 & !a.0)); + for &c in &sample { + // Distributive, both ways round. + assert_eq!(a.0 & (b.0 | c.0), (a.0 & b.0) | (a.0 & c.0)); + assert_eq!(a.0 | (b.0 & c.0), (a.0 | b.0) & (a.0 | c.0)); + } + } + } +} + +/// The reason for preferring a bitmask over some other lawful lattice: it has to +/// produce values that are not simply one of the operands, or the code that +/// stores a combined value is never reached. See `bin/alg_lattice_check`. +#[test] +fn bits_reaches_the_element_path_and_u64_does_not() { + let bits: Vec = (1u64..16).map(Bits).collect(); + let mut bits_join_element = false; + let mut bits_meet_element = false; + for &a in &bits { + for &b in &bits { + bits_join_element |= matches!(a.pjoin(&b), AlgebraicResult::Element(_)); + bits_meet_element |= matches!(a.pmeet(&b), AlgebraicResult::Element(_)); + } + } + assert!(bits_join_element, "Bits::pjoin must be able to return Element"); + assert!(bits_meet_element, "Bits::pmeet must be able to return Element"); + + // u64 cannot, which is the coverage gap the lawful type exists to close. + for a in 1u64..8 { + for b in 1u64..8 { + assert!(!matches!(a.pjoin(&b), AlgebraicResult::Element(_))); + assert!(!matches!(a.pmeet(&b), AlgebraicResult::Element(_))); + } + } +} + +/// Route `k` must mean the same strategies under every value type, or the +/// per-type comparison compares different things. +#[test] +fn route_numbering_is_the_same_for_every_value_type() { + for op in Op::ALL { + let n = algebraic::routes::strategies(op).len(); + for k in 0..algebraic::routes::POINTWISE_ROUTES { + // `strategies` takes no type parameter precisely so this holds; the + // assertion is here to stop that being reintroduced. + assert_eq!(k % n, k % algebraic::routes::strategies(op).len()); + } + } + assert!(::LAWFUL); + assert!(<() as FuzzValue>::LAWFUL); + assert!(!::LAWFUL); + // The overlay join strategy cannot work for a type whose join creates + // values, because OverlayZipper's mapping returns a reference. + assert!(!::JOIN_PICKS_LEFT); + assert!(::JOIN_PICKS_LEFT); +} + +#[test] +fn fuse_routes_decline_restrict_and_accept_everything_else() { + use differential::algebraic::routes::{eval, Route}; + use pathmap::PathMap; + + let operands: Vec> = (0..4).map(|_| PathMap::new()).collect(); + for op in Op::ALL { + let e = Expr::bin(op, var(0), var(1)); + let got = eval(Route::Fuse, &e, &operands).is_some(); + // `FuseOp` has no restrict, and restrict is not a lattice operation, so + // the route has to decline rather than approximate it. + assert_eq!(got, op != Op::Restrict, "{op:?}"); + } + // A bare operand compiles to `FuseRef::Input`, which `eval` must still + // handle -- it is the one case with no steps at all. + assert!(eval(Route::Fuse, &var(2), &operands).is_some()); +} + +#[test] +fn every_strategy_index_is_reachable_from_some_pointwise_route() { + // Route `k` picks strategy `k % n` per operator, so POINTWISE_ROUTES has to + // be at least as large as the widest operator's strategy table or some + // implementation would never be exercised. + for op in Op::ALL { + let n = algebraic::routes::strategies(op).len(); + assert!( + n <= algebraic::routes::POINTWISE_ROUTES, + "{op:?} has {n} strategies but only {} pointwise routes", + algebraic::routes::POINTWISE_ROUTES + ); + for s in 0..n { + assert!( + (0..algebraic::routes::POINTWISE_ROUTES).any(|k| k % n == s), + "{op:?} strategy {s} is unreachable" + ); + } + } +} diff --git a/src/fuse.rs b/src/fuse.rs new file mode 100644 index 00000000..350da285 --- /dev/null +++ b/src/fuse.rs @@ -0,0 +1,449 @@ +//! Fused evaluation of set-operation DAGs over trie nodes. +//! +//! An expression over several input tries, evaluated once. Write it as a +//! `FuseExpr` tree and `compile` it, or build a `FuseProgram` directly in SSA +//! form, which is what lets subexpressions be shared and several outputs be +//! produced from one program. +//! +//! # What this evaluator does and does not do +//! +//! It is a **bottom-up whole-node evaluator**. Each step combines its two +//! operands with the existing node-level primitives -- `pjoin_dyn`, +//! `pmeet_dyn`, `psubtract_dyn` -- short-circuiting when an operand is empty +//! and taking the `ptr_eq` fast path when both sides are the same allocation. +//! It avoids the `PathMap` wrapper overhead, but it still materialises an +//! intermediate node per subexpression. +//! +//! It is **not** the fused byte-by-byte walk the name suggests, and an earlier +//! revision that tried to be was reverted. Computing an effective child mask +//! per byte and recursing cannot be done through the `TrieNode` trait: +//! `LineListNode` stores compressed multi-byte keys, so +//! `node_get_child(&[byte])` returns `None` for a byte that +//! `node_branches_mask` reports as present. Doing it properly means writing +//! the walk inside `ByteNode`'s mask-and-values loop with a separate path for +//! the compressed-key case. +//! +//! # Root values are combined separately +//! +//! Note that `combine_val` decides the root value by presence alone, while +//! the node levels below it go through the lattice operations. The two do not +//! agree for every value type -- see `differential/ALGEBRAIC_FUZZING.md`, which +//! fuzzes this module against the rest of the algebra. + +use crate::alloc::{GlobalAlloc, global_alloc}; +use crate::trie_node::TrieNodeODRc; +use crate::ring::*; +use crate::PathMap; + +// ── Op kind ────────────────────────────────────────────────────────── + +#[derive(Clone, Copy, Debug, PartialEq, Eq)] +pub enum FuseOp { + Or, + And, + Xor, + AndNot, +} + +// ── SSA program ────────────────────────────────────────────────────── + +#[derive(Clone, Copy, Debug, PartialEq, Eq)] +pub enum FuseRef { + Input(usize), + Step(usize), +} + +#[derive(Clone, Copy, Debug)] +pub struct FuseStep { + pub op: FuseOp, + pub lhs: FuseRef, + pub rhs: FuseRef, +} + +pub struct FuseProgram { + steps: Vec, +} + +impl FuseProgram { + pub fn new() -> Self { + FuseProgram { steps: Vec::new() } + } + + pub fn push(&mut self, op: FuseOp, lhs: FuseRef, rhs: FuseRef) -> FuseRef { + let idx = self.steps.len(); + self.steps.push(FuseStep { op, lhs, rhs }); + FuseRef::Step(idx) + } + + pub fn input(i: usize) -> FuseRef { + FuseRef::Input(i) + } + + /// Evaluate the program. + /// + /// At each trie node level, the expression's effective child mask + /// is computed. Children outside the mask are skipped entirely — + /// no merge work or allocation occurs for them. + pub fn eval( + &self, + inputs: &[&PathMap], + outputs: &[FuseRef], + ) -> Vec> + where + V: Clone + Send + Sync + Unpin + Lattice + DistributiveLattice, + { + let input_nodes: Vec>> = + inputs.iter().map(|m| m.root().cloned()).collect(); + let input_vals: Vec> = + inputs.iter().map(|m| m.root_val().cloned()).collect(); + + // Evaluate all steps bottom-up, storing intermediate nodes. + // Mask-based skipping: before computing a step, check if either + // operand is fully empty (node + val both None) and short-circuit. + let mut step_results: Vec<(Option>, Option)> = + Vec::with_capacity(self.steps.len()); + + for step in &self.steps { + let (l_node, l_val) = get_ref(step.lhs, &input_nodes, &input_vals, &step_results); + if matches!(step.op, FuseOp::And | FuseOp::AndNot) + && l_node.is_none() && l_val.is_none() + { + step_results.push((None, None)); + continue; + } + let (r_node, r_val) = get_ref(step.rhs, &input_nodes, &input_vals, &step_results); + if step.op == FuseOp::And && r_node.is_none() && r_val.is_none() { + step_results.push((None, None)); + continue; + } + let node = combine_node(step.op, l_node, r_node); + let val = combine_val(step.op, l_val, r_val); + step_results.push((node, val)); + } + + outputs.iter().map(|r| { + let (node, val) = get_ref(*r, &input_nodes, &input_vals, &step_results); + PathMap::new_with_root_in(node, val, global_alloc()) + }).collect() + } + + /// Apply distributive law then evaluate. + pub fn eval_distributed( + &self, + inputs: &[&PathMap], + outputs: &[FuseRef], + ) -> Vec> + where + V: Clone + Send + Sync + Unpin + Lattice + DistributiveLattice, + { + let (new_prog, map) = self.distribute_and_over_or(); + let new_outputs: Vec = outputs.iter().map(|r| match r { + FuseRef::Input(i) => FuseRef::Input(*i), + FuseRef::Step(i) => map[*i], + }).collect(); + new_prog.eval(inputs, &new_outputs) + } + + pub fn distribute_and_over_or(&self) -> (FuseProgram, Vec) { + let mut new_prog = FuseProgram::new(); + let mut map: Vec = Vec::with_capacity(self.steps.len()); + let remap = |r: FuseRef, map: &[FuseRef]| match r { + FuseRef::Input(i) => FuseRef::Input(i), + FuseRef::Step(i) => map[i], + }; + for step in &self.steps { + let lhs = remap(step.lhs, &map); + let rhs = remap(step.rhs, &map); + if step.op == FuseOp::And { + if let FuseRef::Step(li) = step.lhs { + if self.steps[li].op == FuseOp::Or { + let a = remap(self.steps[li].lhs, &map); + let b = remap(self.steps[li].rhs, &map); + let ac = new_prog.push(FuseOp::And, a, rhs); + let bc = new_prog.push(FuseOp::And, b, rhs); + map.push(new_prog.push(FuseOp::Or, ac, bc)); + continue; + } + } + if let FuseRef::Step(ri) = step.rhs { + if self.steps[ri].op == FuseOp::Or { + let a = remap(self.steps[ri].lhs, &map); + let b = remap(self.steps[ri].rhs, &map); + let ca = new_prog.push(FuseOp::And, lhs, a); + let cb = new_prog.push(FuseOp::And, lhs, b); + map.push(new_prog.push(FuseOp::Or, ca, cb)); + continue; + } + } + } + map.push(new_prog.push(step.op, lhs, rhs)); + } + (new_prog, map) + } +} + +// ── Helpers ────────────────────────────────────────────────────────── + +fn get_ref( + r: FuseRef, + input_nodes: &[Option>], + input_vals: &[Option], + step_results: &[(Option>, Option)], +) -> (Option>, Option) { + match r { + FuseRef::Input(i) => (input_nodes[i].clone(), input_vals[i].clone()), + FuseRef::Step(i) => step_results[i].clone(), + } +} + +/// Combine the root values of two operands. +/// +/// Delegates to the same lattice operations the node levels use, through the +/// `Option` impls in [`crate::ring`], and mirrors `combine_node` arm for +/// arm. +/// +/// This used to decide the root value by presence alone: `And` kept the +/// *right* value, and `AndNot` dropped the left value whenever the right side +/// had any value at all. That is correct for a set, but it disagreed with the +/// `pmeet_dyn`/`psubtract_dyn` calls one level down for every value type whose +/// operations are not presence-based -- so a root value and a value one byte +/// deeper were combined by different rules. `u64` is such a type: `pmeet` is +/// `Identity(SELF_IDENT)`, so the *left* value must win, and `psubtract` is +/// `None` only for *equal* values, so subtracting a differing value is a +/// no-op. The algebraic fuzzer in `differential/` found it. +fn combine_val(op: FuseOp, lv: Option, rv: Option) -> Option +where + V: Clone + Lattice + DistributiveLattice, +{ + match op { + FuseOp::Or => resolve_val(lv.pjoin(&rv), lv, rv), + FuseOp::And => resolve_val(lv.pmeet(&rv), lv, rv), + FuseOp::AndNot => resolve_val(lv.psubtract(&rv), lv, rv), + // `(l - r) join (r - l)`, the same construction `combine_node` uses, so + // the two levels stay in step. Note this is not the same convention as + // `zipper_sym_diff`'s value policy, which cancels a coincident path + // whatever the two values are; here distinct values survive. + FuseOp::Xor => { + let a = resolve_val(lv.psubtract(&rv), lv.clone(), rv.clone()); + let b = resolve_val(rv.psubtract(&lv), rv, lv); + resolve_val(a.pjoin(&b), a, b) + } + } +} + +/// [`resolve`] for values rather than nodes. +#[inline] +fn resolve_val( + result: AlgebraicResult>, + l: Option, + r: Option, +) -> Option { + match result { + AlgebraicResult::Element(v) => v, + AlgebraicResult::Identity(mask) => { + if mask & SELF_IDENT > 0 { l } else { r } + } + AlgebraicResult::None => None, + } +} + +fn combine_node( + op: FuseOp, + l: Option>, + r: Option>, +) -> Option> +where + V: Clone + Send + Sync + Unpin + Lattice + DistributiveLattice, + A: crate::alloc::Allocator, +{ + match op { + FuseOp::Or => match (l, r) { + (None, x) | (x, None) => x, + (Some(l), Some(r)) => { + if l.ptr_eq(&r) { return Some(l); } + resolve(l.as_tagged().pjoin_dyn(r.as_tagged()), l, r) + } + }, + FuseOp::And => match (l, r) { + (None, _) | (_, None) => None, + (Some(l), Some(r)) => { + if l.ptr_eq(&r) { return Some(l); } + resolve(l.as_tagged().pmeet_dyn(r.as_tagged()), l, r) + } + }, + FuseOp::Xor => match (l, r) { + (None, x) | (x, None) => x, + (Some(l), Some(r)) => { + if l.ptr_eq(&r) { return None; } + let l_minus_r = resolve(l.as_tagged().psubtract_dyn(r.as_tagged()), l.clone(), r.clone()); + let r_minus_l = resolve(r.as_tagged().psubtract_dyn(l.as_tagged()), r, l); + match (l_minus_r, r_minus_l) { + (None, x) | (x, None) => x, + (Some(mut a), Some(b)) => { + let (status, _) = a.make_mut().join_into_dyn(b); + match status { AlgebraicStatus::None => None, _ => Some(a) } + } + } + } + }, + FuseOp::AndNot => match (l, r) { + (None, _) => None, + (l, None) => l, + (Some(l), Some(r)) => { + if l.ptr_eq(&r) { return None; } + resolve(l.as_tagged().psubtract_dyn(r.as_tagged()), l, r) + } + }, + } +} + +#[inline] +fn resolve( + result: AlgebraicResult>, + l: TrieNodeODRc, + r: TrieNodeODRc, +) -> Option> +where V: Clone + Send + Sync, A: crate::alloc::Allocator, +{ + match result { + AlgebraicResult::Element(n) => Some(n), + AlgebraicResult::Identity(mask) => { + if mask & SELF_IDENT > 0 { Some(l) } else { Some(r) } + } + AlgebraicResult::None => None, + } +} + +// ── Tree expression (convenience) ──────────────────────────────────── + +#[derive(Clone, Debug)] +pub enum FuseExpr { + Leaf(usize), + Op(FuseOp, Box, Box), +} + +impl FuseExpr { + pub fn leaf(i: usize) -> Self { FuseExpr::Leaf(i) } + pub fn or(l: FuseExpr, r: FuseExpr) -> Self { FuseExpr::Op(FuseOp::Or, Box::new(l), Box::new(r)) } + pub fn and(l: FuseExpr, r: FuseExpr) -> Self { FuseExpr::Op(FuseOp::And, Box::new(l), Box::new(r)) } + pub fn xor(l: FuseExpr, r: FuseExpr) -> Self { FuseExpr::Op(FuseOp::Xor, Box::new(l), Box::new(r)) } + pub fn and_not(l: FuseExpr, r: FuseExpr) -> Self { FuseExpr::Op(FuseOp::AndNot, Box::new(l), Box::new(r)) } + + pub fn compile(&self) -> (FuseProgram, FuseRef) { + let mut prog = FuseProgram::new(); + let out = compile_expr(self, &mut prog); + (prog, out) + } +} + +fn compile_expr(expr: &FuseExpr, prog: &mut FuseProgram) -> FuseRef { + match expr { + FuseExpr::Leaf(i) => FuseRef::Input(*i), + FuseExpr::Op(op, lhs, rhs) => { + let l = compile_expr(lhs, prog); + let r = compile_expr(rhs, prog); + prog.push(*op, l, r) + } + } +} + +pub fn fuse_eval( + expr: &FuseExpr, + inputs: &[&PathMap], +) -> PathMap +where + V: Clone + Send + Sync + Unpin + Lattice + DistributiveLattice, +{ + let (prog, out) = expr.compile(); + prog.eval(inputs, &[out]).into_iter().next().unwrap() +} + +#[cfg(test)] +mod tests { + use super::*; + // `ZipperPath` is named explicitly: it was reachable without naming it on + // the branch this module came from, and is not any more. + use crate::zipper::{ZipperIteration, ZipperPath}; + + fn keys_of(m: &PathMap) -> Vec { + let mut rz = m.read_zipper(); + let mut out = Vec::new(); + while rz.to_next_val() { + let p = rz.path(); + if p.len() == 4 { + out.push(i32::from_be_bytes([p[0], p[1], p[2], p[3]])); + } + } + out + } + + fn make(keys: &[i32]) -> PathMap { + let mut m = PathMap::new(); + for &k in keys { + m.set_val_at(k.to_be_bytes(), k); + } + m + } + + impl Lattice for i32 { + fn pjoin(&self, other: &Self) -> AlgebraicResult { + if self == other { AlgebraicResult::Identity(SELF_IDENT) } + else { AlgebraicResult::Element(*self.max(other)) } + } + fn pmeet(&self, other: &Self) -> AlgebraicResult { + if self == other { AlgebraicResult::Identity(SELF_IDENT) } + else { AlgebraicResult::Element(*self.min(other)) } + } + } + + impl DistributiveLattice for i32 { + fn psubtract(&self, other: &Self) -> AlgebraicResult { + if self <= other { AlgebraicResult::None } + else { AlgebraicResult::Identity(SELF_IDENT) } + } + } + + #[test] + fn leaf_passthrough() { + let a = make(&[10, 20, 30]); + let result = fuse_eval(&FuseExpr::leaf(0), &[&a]); + assert_eq!(keys_of(&result), vec![10, 20, 30]); + } + + #[test] + fn or_basic() { + let a = make(&[1, 3, 5]); + let b = make(&[2, 4, 6]); + let result = fuse_eval(&FuseExpr::or(FuseExpr::leaf(0), FuseExpr::leaf(1)), &[&a, &b]); + assert_eq!(keys_of(&result), vec![1, 2, 3, 4, 5, 6]); + } + + #[test] + fn and_basic() { + let a = make(&[1, 2, 3, 5]); + let b = make(&[2, 4, 5]); + let result = fuse_eval(&FuseExpr::and(FuseExpr::leaf(0), FuseExpr::leaf(1)), &[&a, &b]); + assert_eq!(keys_of(&result), vec![2, 5]); + } + + #[test] + fn and_not_basic() { + let a = make(&[1, 2, 3, 5]); + let b = make(&[2, 3, 6]); + let result = fuse_eval(&FuseExpr::and_not(FuseExpr::leaf(0), FuseExpr::leaf(1)), &[&a, &b]); + assert_eq!(keys_of(&result), vec![1, 5]); + } + + #[test] + fn or_then_and() { + let a = make(&[1, 3, 5]); + let b = make(&[2, 4, 6]); + let c = make(&[2, 3, 7]); + let expr = FuseExpr::and( + FuseExpr::or(FuseExpr::leaf(0), FuseExpr::leaf(1)), + FuseExpr::leaf(2), + ); + let result = fuse_eval(&expr, &[&a, &b, &c]); + assert_eq!(keys_of(&result), vec![2, 3]); + } +} diff --git a/src/lib.rs b/src/lib.rs index 6d38dc03..42cd199e 100644 --- a/src/lib.rs +++ b/src/lib.rs @@ -82,6 +82,9 @@ pub mod morphisms; /// Functionality to optimize a trie by finding structural sharing using a temporary [Merkle tree](https://en.wikipedia.org/wiki/Merkle_tree) pub mod merkleization; +/// Fused evaluation of set-operation DAGs over trie nodes +pub mod fuse; + /// Handy conveniences and utilities to use with a [PathMap] pub mod utils;