Repository navigation
Conversation
subtree_has_difference() searches the shared part of both tries depth first, keeping the branch points that still have unvisited children. When a subtree was exhausted it climbed back with lhs.ascend_until_branch(), which stops at the nearest branch, not the nearest *pending* one. With a fully explored branch in between, it re-searched that branch, popped the pending entry, and never visited the pending child, so a surviving value there was missed and the subtree reported empty. The re-search can also repeat forever: a 1M-case algebraic fuzz sweep with nested SubtractZippers hung with every job inside SubtractZipper::new -> refresh -> ascend_until_branch. Record the depth of each pending branch and ascend exactly that far. Found by the algebraic fuzzer's subtract_zipper route: b - a where a is dangling-only structure and b is a plus one value. Co-Authored-By: Claude Opus 5.5 <noreply@anthropic.com>
A clone is an independent zipper at the same focus, cached state included. This also lets a SubtractZipper be the input of another one, since its ZipperMoving impl requires Clone inputs: (a - b) - c without materialising a - b. Co-Authored-By: Claude Opus 5.5 <noreply@anthropic.com>
The two existing fuzzers ask whether the answer is right -- the Lean model in
lean/ is the oracle -- or whether anything crashes. This one asks whether it
matters which way you compute it.
pathmap implements each algebraic operation several times over: eagerly on whole
maps, in place through a write zipper, 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 separate
implementations with separate pruning, grafting and value-combining logic, so
they can check each other without anyone writing down what the answer should be.
Each case is one expression over four generated tries, evaluated by every route
that applies to its shape, with every answer required to match. laws.rs is the
other half: pairs of expressions that must agree whatever the operands, which is
what catches a mistake every route shares -- including one in the baseline the
routes are compared against.
No oracle, no Lean build, no child process: about 55k cases/sec in process.
Six defects on master, each reproduced without the fuzzer in alg_bug_repros:
1. join_into drops the source's root value when the destination is empty.
2. meet_2 drops root values outright.
3. PathMap::join and PathMap::meet take the right operand's value at a shared
path when the operands' nodes are laid out differently. u64's pjoin is
left-biased and pmeet is Identity(SELF_IDENT), so the left value must win.
Every zipper route gets this right, which is why it surfaces as failing
laws rather than as one route disagreeing with the others.
4. join loses a value across shared structure: with b a clone of a plus one
value, a|b drops it and b|a keeps it. A join is a least upper bound, so no
ordering may lose a path. Needs the operands to share allocations --
rebuilding b's entries into a fresh map hides it.
5. merkleize panics on a trie holding only dangling paths. Not algebraic; it
fires while the operands are still being written.
6. Debug-assertions only, and the mechanism behind 4: join's "empty result"
path is reachable from nodes that are not empty.
algebraic::KNOWN maps every signature onto one of those and decides exit status
only; counts always print, so a known defect firing ten times more often is
still visible. Verified clean at 2M cases in release and 2M with debug
assertions enabled.
Two notes for whoever extends this. u64's value semantics are not set
semantics, so several textbook identities hold on path presence but not on
values; laws.rs lists the ones deliberately absent and why. And the recognisers
that decide which route applies were both wrong at first in ways that looked
exactly like crate defects -- the n-ary forms fold symmetric difference left, and
a DNF clause is an unordered bitmask that cannot represent `b & a` -- so they are
pinned by tests. When a route disagrees with the rest, suspect the route first.
differential now builds pathmap with the zipper_alg feature. ALGEBRAIC_FUZZING.md
has the full write-up.
Co-Authored-By: Claude Opus 5 <noreply@anthropic.com>
…ng repro
Four pieces of work on top of the initial fuzzer, all of which came out of one
discovery: the value type it was using cannot support the questions being asked
of it.
**u64's Lattice impl is not a lattice.** pjoin is left_biased_pjoin and pmeet is
Identity(SELF_IDENT), so both return the left operand, a | b == a & b for every
pair, and in a lattice that would force a == b -- the impl effectively asserts
1 == 2. Two consequences, both limits on the harness rather than on the crate:
neither operation can return AlgebraicResult::Element, so the code that stores a
genuinely combined value was never reached; and several laws had to be weakened or
omitted, which looked like facts about the algebra and were facts about u64.
bin/alg_lattice_check prints the evidence, for u64, bool, a bitmask and
max/min-on-a-total-order. The last of those is the useful one: it is a perfectly
lawful distributive lattice and still answers "never" to whether any operation
produces Element, because max(a, b) and min(a, b) are always one of the operands.
Being a lawful lattice is not sufficient; only the bitmask family reaches that
code, because a | b is a new value.
**So the harness is generic over the value type and runs every case three times.**
Signatures carry the type, and every run ends with the comparison.
* bits -- a 64-bit set under |, & and & !, empty collapsing to bottom. The same
construction pathmap::utils already uses for [u64; 4] and ByteMask, at a
narrower width. Defined in differential rather than in pathmap, because a
value type from outside the crate is what a real caller has.
* unit -- PathMap<()>, the set case, also lawful. Its pjoin and pmeet return
Identity(SELF_IDENT | COUNTER_IDENT) on *every* combination, where the others
do so only for equal values, which saturates the "either operand will do" path
the node code uses to keep sharing -- the machinery two of the findings are
about. Nothing in zipper_algebra.rs tests () at all.
* u64 -- kept, because it is what callers use and it reaches Identity-heavy
paths the lawful types do not.
Five findings are u64-only artefacts; nothing is lawful-type-only, so u64 was
masking nothing. Counts collapse rather than vanish for the rest -- join
associativity fails 3131 times under u64 and 12 under bits -- because under a
commutative join, picking the wrong operand is invisible except where one operand
already contains the other. Every residue shrinks to a lost value, not a
misplaced one. values:model drops from 1258 to 2.
Three of the four identities that only a lawful type can check hold. The fourth,
subtract-over-join, fires under unit, and is a lost value rather than a bad
identity.
**Three further corrections, each now pinned by a test:**
* model.rs no longer restates the value algebra; it delegates to
pjoin/pmeet/psubtract through the Option<V> impls in ring, so a disagreement
with a route is always about where a value ends up.
* The OverlayZipper join strategy declines for a value type whose join creates
values, instead of answering wrongly: its mapping returns a *reference*, so it
has nowhere to put a value it would create.
* Strategy tables are the same length for every value type, so route k means the
same thing under each. Shortening one silently renumbered the rest and made
the per-type comparison compare different things.
**The exit-status gate was broken** once signatures gained the value-type prefix:
is_fatal matched class names against the start of the whole signature, so every
class fell through to not-fatal and runs with new findings were passing. It parses
the class field now. Two findings were sitting unreported behind it.
**alg_bug_repros covers every cause in KNOWN.** The dangling-path class had none,
and is the largest; case 7 adds it. Its explanation was also backwards: the
lockstep traversals in zipper_algebra DISCARD dangling structure and the whole-map
and write-zipper forms PRESERVE it, not the other way round. Corrected in four
places and pinned, since going stale quietly is how it was wrong to begin with.
**Documented soundness limit.** A run that catches panics aborts with heap
corruption, reproducibly, and it tracks the number of panics caught rather than
the build profile, thread count or value type -- a run that catches none is clean.
Every panic caught fired mid-mutation inside pathmap's node code, and unwinding
out of a half-updated node leaves a trie that is not safe to drop. This harness's
problem, not a defect: the crash fuzzer runs one input per process. Not fixed,
because the fix is a design change; until then the first panic in a run is the end
of its trustworthy output.
Verified clean at 1M cases, corpus replays clean in both profiles, 14 harness
tests, 1043 lib tests, no warnings. Nothing outside differential/ is touched.
Co-Authored-By: Claude Opus 5 <noreply@anthropic.com>
Two whole-expression routes, appended after the existing ones so no route number or KNOWN signature moves: - subtract_zipper: every `-` through the lazy SubtractZipper, materialised by walking it; other operators through the baseline, so a divergence points at SubtractZipper or at what consumes its output. - subtract_zipper_nested: nested SubtractZippers, one reading from another, as the left input (`x - y - z ...`) or the right one (`x - (y - z)`). A new test checks that every whole-expression route applies to some random case; the first version of the nested route, plain-operand chains only, applied to none in 2000. KNOWN: the subtract_zipper route's divergences trace to existing causes. Its subtraction agrees with PathMap::subtract on every path and value, dangling paths included; the different node layout is what the baseline join then trips on (u64 bias, and the dangling-only join loss whose debug assert fires). Also re-keys the panic sites master moved: line_list_node.rs 1745->1785, 2669->2732, 2720->2783; dense_byte_node.rs 2080->2088. Found one SubtractZipper defect, fixed in the survival-search commit below this one. Without that fix, a 1M-case sweep hangs, with jobs stuck in the survival search. With it: 1M release (seed 2) and 1M debug-assert (seed 3) cases, nothing outside KNOWN, about 70s each. Co-Authored-By: Claude Opus 5.5 <noreply@anthropic.com>
imlvts
force-pushed
the
alg-fuzzer
branch
2 times, most recently
from
October 23, 2026 22:53
236441a to
5195266
Compare
New alg-fuzz job, after the tests, on PRs, pushes to master and manual runs: - the harness gate (cargo test -p differential --test algebraic); - a release sweep and a debug-assertions sweep, 1M cases each with a fixed seed by default (alg_fuzz_cases / alg_fuzz_seed inputs on manual runs), failing on any signature missing from algebraic::KNOWN; - each sweep under `timeout`, since a hang is a finding too; - a step summary per sweep (verdict plus the per-value-type table, and the command to reproduce) and the saved inputs as the alg-fuzz-out artifact. The debug build repeats target-cpu=native in RUSTFLAGS (it replaces .cargo/config.toml's flags and gxhash needs it) and uses its own target dir. The bench job now also waits for this gate. Checked with actionlint, and by running each step's script locally under `bash -eo pipefail`: passing sweeps, an unexpected finding (exit 1), and a timeout (exit 124 with an error annotation) all report as intended. Co-Authored-By: Claude Opus 5.5 <noreply@anthropic.com>
A non-unwinding panic (a debug-mode unsafe-precondition check, a panic in a destructor during unwinding) aborts the process, so it can never become a finding, and the quiet hook used to swallow its message: CI saw only "thread caused non-unwinding panic. aborting." Print the message, the site, a backtrace and the current input as hex, so the abort names its reproducer. The first one it caught: under Rust 1.99 with debug assertions, gxhash 3.5.0's get_partial_unsafe reads 16 bytes past short inputs, and std's _mm_loadu_si128 now checks copy_nonoverlapping, so merkleize aborts when the over-read overlaps a stack local. Layout dependent, so per binary and thread. Co-Authored-By: Claude Opus 5.5 <noreply@anthropic.com>
Each job draws its own input stream, so --jobs "$(nproc)" made the inputs depend on the runner: a 192-core runner fuzzed cases no 64-core machine ever ran, and its findings did not reproduce elsewhere. A fixed 64 runs the same inputs everywhere (oversubscribed on smaller machines), and the reproduce command in the summary is exact. Co-Authored-By: Claude Opus 5.5 <noreply@anthropic.com>
gxhash 3.5.0 hashes inputs shorter than 16 bytes with a 16-byte _mm_loadu_si128 that reads past their end. Since Rust 1.99 that intrinsic is a checked copy_nonoverlapping, so with debug assertions merkleize could abort with "unsafe precondition(s) violated" (the CI debug-assert sweep did, on Rust 1.99.1). Upstream: ogxd/gxhash#111, still open; 3.5.0 is the latest release. Pin to 390c3e5 (ogxd/gxhash#118), which does that load with inline assembly and is otherwise 3.5.0. Not main: that is gxhash 4.0, and gxhash only keeps hash values stable within a major version. Checked: - hash values identical to 3.5.0: gxhash128, gxhash64 and GxHasher over every length 0-200 at every alignment, four seeds (12864 cases); - Rust 1.99.1 with debug assertions: both captured aborting inputs replay clean, and 1M-case sweeps at 192 and 64 jobs finish with nothing unexpected; - cargo test on 1.99.1 (release, arena_compact+random, debug lib) and on the local nightly: all pass. Co-Authored-By: Claude Opus 5.5 <noreply@anthropic.com>
This file contains hidden or bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
Sign up for free
to join this conversation on GitHub.
Already have an account?
Sign in to comment
Add this suggestion to a batch that can be applied as a single commit.This suggestion is invalid because no changes were made to the code.Suggestions cannot be applied while the pull request is closed.Suggestions cannot be applied while viewing a subset of changes.Only one suggestion per line can be applied in a batch.Add this suggestion to a batch that can be applied as a single commit.Applying suggestions on deleted lines is not supported.You must change the existing code in this line in order to create a valid suggestion.Outdated suggestions cannot be applied.This suggestion has been applied or marked resolved.Suggestions cannot be applied from pending reviews.Suggestions cannot be applied on multi-line comments.Suggestions cannot be applied while the pull request is queued to merge.Suggestion cannot be applied right now. Please check back later.
This implements a fuzzer for algebraic ops.
There are multiple ways in PathMap to compute the same expression. We test that those different ways compute the same result.
All the ways to compute the same expression are written down in differential/src/algebraic/routes.rs
Here's the list of exercised APIs:
PathMap::join,WriteZipper::join_into,join_map_into,join_into_take,zipper_join,OverlayZipper(u64 only)PathMap::meet,WriteZipper::meet_into,WriteZipper::meet_2,zipper_meetPathMap::subtract,WriteZipper::subtract_into,zipper_subtractzipper_sym_diff,jointhenmeetthensubtractPathMap::restrict,WriteZipper::restrictAs an additional option, differential/src/algebraic/model.rs implements a "model" implementation of the algebraic ops, using pairwise operation. It gives an additional validation for the operations.
The boolean/lattice laws which should hold for the algebraic expressions are written down in differential/src/algebraic/laws.rs
All of that gets driven by differential/src/bin/alg_fuzz.rs
Latest gxhash (3.5.0) is broken on Rust 1.99 in release with debug info. This broke merkleize in CI/fuzzing.
I updated the dependency to a newer version pinned to a commit.