Conversation
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>
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
1 participant
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.
No description provided.