Conversation
Cherry-pick of e49af0f from archive-bugfix/act-val-count-from-focus. `val_count` opened with `reset()`, so it counted the values below the zipper's root whatever the focus was and was right only at the root; `ZipperValues::val_count` counts at and below the focus. Verified against the model: the class goes from 1416 hits on 5000 ACT inputs at seed 7 to 0, and agreement rises 3581 -> 4733. The crate-mode run is untouched, as it must be. This also unmasks 52 inputs that now diverge on `to_next_step`. They are not a regression: `val_count` was wrong at nearly every focus, so the classifier attributed those lines to it, and the only behaviour this commit changes is `val_count`, which `to_next_step` does not call. They are an ACT iteration defect that was hidden and is now visible, and are left unclassified deliberately. The upstream commit's own test conflicted with the ACT tests master has since gained; both sets are kept. Co-Authored-By: Claude Opus 5 (1M context) <noreply@anthropic.com>
Cherry-pick of 0ef62ff from archive-bugfix/act-sibling-off-trie-focus. `to_sibling` worked off the node stack, which holds only real nodes, so a focus one byte off the trie had no frame and the method answered `None`. That starved `to_next_step`, which moves by it, and whole subtrees went unvisited. This is the fix for what the previous commit unmasked. On 5000 ACT inputs at seed 7 the 52 `to_next_step` divergences go to 0, and with them the ACT hits of the sibling-after-iteration class (50 -> 0) and the to_next_val class (123 -> 0), which were the same starvation seen through other operations. Agreement goes 4733 -> 4956, and 3581 -> 4956 against the baseline before either ACT fix. Crate mode is untouched. The upstream commit's test conflicted with the test added by the previous commit, and the conflict boundary fell inside that test; both are kept and the truncated one closed. Co-Authored-By: Claude Opus 5 (1M context) <noreply@anthropic.com>
…byte
Cherry-pick of f75fce1 from archive-bugfix/subtract-drops-value: the
missing else arm in `ByteNode::psubtract_abstract`.
Verified: both corpus reproducers for the class
(subtract_into-drops-value-under-source-path{,-2}.bin) go from failing
to agreeing, the class goes 1 -> 0 on 20000 crate inputs at seed 7,
agreement rises 19738 -> 19739, and no other class moves.
The class is not empty afterwards. Seed 12 keeps one hit, on which the
model returns Identity with the subtrie intact and the crate returns
None having dropped it -- the same shape but a subtrie discarded rather
than a value, and present identically before this commit, so it is a
residual rather than a regression. Saved as
lean/corpus/subtract_into-drops-subtrie-residual.bin.
Co-Authored-By: Claude Opus 5 (1M context) <noreply@anthropic.com>
Cherry-pick of 4453b07 from archive-bugfix/graft-child-maps: both documented symptoms plus the third inconsistency, and op 54 comes out of quarantine in the harness and the model. Verified: graft_masked_branches creating the focus goes from 177 hits on 20000 crate inputs at seed 7 to 0, and agreement rises 19739 -> 19894. Other classes move up -- join_into 24 -> 36, finding 8 20 -> 29, status 18 -> 19, dangling 11 -> 12 -- because op 54 now executes where it used to be skipped on both sides, so every input that reaches it runs more operations and has more chances to hit a bug that was already there. Total known hits fall 261 -> 106 and nothing new appears. The upstream commit also deleted its own KNOWN entries from differential.py; those are dropped from this cherry-pick, since letting a fix retire the entry that measures it makes the verification circular. Its harness.rs and Fuzz.lean hunks conflicted with the skip-reason vocabulary and were reapplied in terms of it. Co-Authored-By: Claude Opus 5 (1M context) <noreply@anthropic.com>
…source Cherry-pick of 4c793d0 from archive-bugfix/join-into-empty-dst. The tiny-ref-node arm of `pjoin_dyn` swapped its operands with an un-inverted mask, so the destination was replaced by the source; also the merge_guts identity and the integer `pjoin` setting both identity bits when the values are equal. Verified: the class goes from 36 hits on 20000 crate inputs at seed 7 to 0 and agreement rises 19894 -> 19950. The finding 8 status class falls 29 -> 8 with it, which the identity-bit half of this commit accounts for. Total known hits 106 -> 50, nothing new. The upstream commit's differential.py hunk, which retired its own KNOWN entry, is dropped for the same reason as the previous commit. Co-Authored-By: Claude Opus 5 (1M context) <noreply@anthropic.com>
Cherry-pick of 5197435 from archive-bugfix/meet-drops-dangling-paths: EmptyNode pmeet, the sentinel ptr-eq shortcut, the pmeet_generic COUNTER_IDENT claim and the dense CoFree pmeet. Three existing tests encoded the old behaviour and are changed to the spec's. Verified: all three corpus reproducers for the class (meet_into-keeps-dangling-child, -only-child, meet_k_path_into-keeps- dangling) go from failing to agreeing, the class falls from 12 hits on 20000 crate inputs at seed 7 to 2, and agreement rises 19950 -> 19960. The two that remain are the residual the branch documented: a dangling path deep inside an Arc shared by both operands still survives the ptr-eq shortcut, which returns early without inspecting the subtrie. One is saved as lean/corpus/meet_into-keeps-dangling-residual-arc-shared.bin; it first diverges under subtract_into rather than meet_into, the same shortcut seen through the other operation. Co-Authored-By: Claude Opus 5 (1M context) <noreply@anthropic.com>
Cherry-pick of 94b4043 from archive-bugfix/value-bias-by-node-layout: five swapped-orientation sites in trie_node/line_list_node/ dense_byte_node, and join_k_path_into's fold made ascending to match `PathMap.dropHead`. Verified: all four corpus reproducers (join_into, join_k_path_into, meet_2, meet_into) go from failing to agreeing, the class falls from 10 hits to 0 on 20000 crate inputs and 2 to 0 on 5000 ACT inputs at seed 7, and agreement rises 19960 -> 19975 and 4957 -> 4959. The finding 8 class falls 20 -> 16 and the dangling class 2 -> 1 with it. Three hunks conflicted with the join_into commit applied earlier. The two tiny-ref dispatch arms keep that commit's form, which fixes the same orientation and also reports the identity mask. The third is a real overlap: it takes this commit's operand order, since the join is left-biased and `a` must be on the left, while keeping the join_into commit's identity reporting, reading COUNTER_IDENT where it read SELF_IDENT because swapping the operands swaps what the bits refer to. Co-Authored-By: Claude Opus 5 (1M context) <noreply@anthropic.com>
The whole remaining ACT residual -- 293 hits over 36000 inputs, and nothing else -- sat in the `ascend_until_wz` bucket, whose note says finding 9, a *write* zipper corrupted at a node boundary. It is not that. In all 30 sampled the write zipper's fields are identical on both sides and only the read zipper moved: the ACT zipper reports a shorter ascent than the model, one byte short in 18 of 22 and two in the rest. The entry keys on the bare substring `ascend_until`, so it claimed them. The giveaway was the asymmetry: 293 hits in ACT mode and 0 in crate mode, for a defect in a write zipper that both modes share. `read_zipper_only` tags a divergence whose write-zipper fields agree, in `--act` mode only, where the read zipper is the ArenaCompactTree one; the new entry is tested before the write-zipper one. The ACT residual moves to it in full, and `ascend_until_wz` now fires nowhere. Crate agreement is unchanged. That also settles archive-bugfix/ascend-until-write-zipper, which retired this entry and which I had held back for still appearing to fire: its claim was right, and what remained was this misattribution. Co-Authored-By: Claude Opus 5 (1M context) <noreply@anthropic.com>
…e focus
`ascend_to_branch`, behind `ascend_until` and `ascend_until_branch`, first
ascends the non-existent tail of the path (`ascend_invalid`) and then has to
decide whether the real ancestor it lands on is already a stop. It read that
off the *node* instead of off the focus, and only looked for a value:
match &self.cur_node {
Node::Line(line) => if need_value && line.value.is_some() { return }
Node::Branch(node) => if need_value && node.value.is_some() { return }
}
A line node stores a run of bytes and carries its value at the *end* of that
run, so `line.value` says nothing about a focus that sits partway into the
line -- and a focus left mid-line is exactly what `ascend_invalid` produces
when the path walked off the trie in the middle of a line. The ascent then
stopped there and reported a value stop at a position that has no value, short
of the real stop further up:
paths: [1,2,3,4], [5] focus [1,2,9], one byte off the trie
ascend_until() -> ACT 1 ([1,2], no value, one child), model 3 (the root)
The other half is the case the match never considered at all: a branch is a
stop too. When the deepest real ancestor is a branch node with more than one
child, the model stops there, while the loop below fell straight through and
popped the frame, running one byte past it:
paths: [5,2], [5,6] focus [5,9]
ascend_until_branch() -> ACT 2 (the root), model 1 ([5])
Both conditions now come off the focus, through `is_val` and `child_count`,
which handle a mid-line focus correctly -- a line's interior has exactly one
child and no value -- and match what the loop below applies to every other
position it ascends past.
This was the only remaining ACT-mode divergence class. ACT differential runs,
maxlen 300, the harness's `act: ascend_until_short` entry untouched:
seed 7, 5000 inputs: 4959/5000 agree, 41 known -> 5000/5000, 0 known
seed 0, 4000 inputs: 3964/4000 agree, 36 known -> 4000/4000, 0 known
seed 10, 4000 inputs: 3964/4000 agree, 36 known -> 4000/4000, 0 known
seed 12, 4000 inputs: 3971/4000 agree, 29 known -> 4000/4000, 0 known
seed 21, 20000 inputs (after only): 20000/20000 agree, 0 known, 0 new
No new divergence class is unmasked, and crate mode is unchanged:
20000 inputs, seed 7, 19975/20000 agree, 25 known, 0 new, before and after.
`cargo test --release` and `cargo test --release --features
arena_compact,random` pass.
Regression test: `act_zipper_ascend_until_from_an_off_trie_focus`, both
operations at four roots against the `PathMap` read zipper, over off-trie foci
below a value-terminated line, below a branch, and below a branching value.
Fails before this change (1 vs 3 on the first case, 2 vs 1 on the branch one).
Co-Authored-By: Claude Opus 5 (1M context) <noreply@anthropic.com>
Finding 8 ("AlgebraicStatus::Identity is not returned when nothing changed")
still fired on `restrict` for 8 of 20k seed-7 inputs. Two defects in the dense
node's restrict, both in `src/dense_byte_node.rs`:
- `ByteNode::prestrict` seeded its identity flag with
`self.mask == mm && other.mask == mm` (line 2488, `mm = self.mask &
other.mask`). Restrict is non-commutative: only `self`'s branches can be
dropped, so the result is an identity of `self` exactly when `self.mask ==
mm`. Requiring `other.mask == mm` as well meant that any source with a branch
the destination did not have forced `Element`, even though the destination was
returned untouched. The flag is now seeded with `self.mask == mm` alone.
- `prestrict_abstract` (the dense-against-list/tiny path, line 580) walks
`self`'s entries. When `other` has no value at a byte, `self`'s value at that
byte is dropped -- the empty path does not validate -- but the identity flag
was only cleared by the onward link's own result. A co-free holding both a
value and an onward link that restricted to an identity therefore reported
`Identity`, and the caller kept `self` unchanged, so the value that should have
been dropped stayed in the map. This one is a wrong answer, not just an
imprecise status. The flag is now also cleared when the dropped co-free
carries a value.
Differential, before -> after, 0 new divergences throughout and no other class
moved (`status_imprecise` and `meet_keeps_dangling` counts are unchanged):
seed 7, 20k: 19975 -> 19982 agree; finding-8 restrict key 8 -> 1
seed 0, 10k: 9987 -> 9992 agree; finding-8 restrict key 6 -> 1
seed 10, 10k: 9989 -> 9992 agree; finding-8 restrict key 4 -> 1
seed 12, 10k: 9988 -> 9993 agree; finding-8 restrict key 5 -> 0
ACT, seed 7, 5k: 4959 -> 4959 agree, identical bucket table
The residual restrict hits are a different defect: `restrict` against a
destination that holds an empty child node materialised by an earlier
`meet_into` keeps the dangling branch the spec drops -- the `meet_keeps_dangling`
family, not an identity-mask problem.
cargo test --release: 909 passed. cargo test --release --features
arena_compact,random: 1044 passed.
Tests: write_zipper_restrict_wider_source_is_identity,
write_zipper_restrict_drops_value_beside_kept_child.
Co-Authored-By: Claude Opus 5 (1M context) <noreply@anthropic.com>
Cherry-pick of a subagent's 24ccaaf, plus the one model line it has to land with. `impl DistributiveLattice for u64` and `for u16` in src/ring.rs answered a subtraction of unequal values with `Element(*self)` -- the right value under the wrong constructor. The node algebra propagates identity *masks*, not values, so a single `Element` below a node forced the whole node, and with it `subtract_into`, to report `Element` for a byte- identical trie. `impl DistributiveLattice for bool` in the same file already returned `Identity(SELF_IDENT)`; the integer instances were the outliers. `u64Ops` in lean/PathMapModel/Basic.lean is a transcription of that instance, not an independent claim -- its own docstring says it "reproduces it exactly rather than assuming a real lattice", and SPEC_WARTS.md records it as "copied from `impl Lattice for u64`". So it follows the crate here: `psub` returns `.identity true false`. The wart SPEC_WARTS.md actually flags is that `pjoin`/`pmeet` are left-biased projections, which is untouched. Changing the crate without this line leaves the model asserting the behaviour of a version that no longer exists, and the two must move together. Verified, with the KNOWN table unmodified throughout: crate seed 0, 10000 9992 -> 10000/10000, 0 known crate seed 7, 10000 9992 -> 9999/10000, 1 known crate seed 10, 10000 9992 -> 9999/10000, 1 known crate seed 12, 10000 9993 -> 10000/10000, 0 known ACT seed 0 and 7, 5000 5000/5000, 0 known 0 new divergences in every run. The one hit left at seeds 7 and 10 is a different defect: `restrict` against a destination holding an empty node materialised by an earlier `meet_into` keeps a dangling branch the spec drops. That belongs to the empty-node-materialisation family, not to this identity-mask class. Tests: 911 and 1047 pass, 0 failed. Co-Authored-By: Claude Opus 5 (1M context) <noreply@anthropic.com>
A zipper's focus is allowed to sit on a path that does not exist: `descend_to`
an absent path puts it there and `path_exists()` reports false, and the API is
specified to keep answering from there. The siblings of such a focus are still
well defined, because they come from the parent's `child_mask`, not from the
focus itself.
The `ZipperMoving` default `to_prev_sibling_byte` computed that correctly and
then asserted something that is not true of it. On the arm where `prev_bit`
finds no previous sibling, the method puts the focus back exactly where it
started and returns `None` -- and then asserted `self.path_exists()` on the
restored focus (src/zipper.rs:457). Restoring a focus cannot make it exist, so
for every off-trie focus that assert fired. Every write zipper takes this
default impl (`WriteZipperCore` defines no sibling methods of its own), so in a
debug build `WriteZipper::to_prev_sibling_byte` panicked instead of returning
`None`. The minimal case is an empty map:
let mut wz = map.write_zipper();
wz.descend_to(&[0u8]); // off-trie; the root's child mask is empty
wz.to_prev_sibling_byte(); // panicked; must be None
The answer itself was always right. `toPrevSiblingByte` in the Lean model
returns `(none, z)` in exactly this situation, which is what the code produces,
and the release build -- where the assert is compiled out -- already agreed with
the model on all of these inputs. So the defect is the assertion's invariant,
not the computation: the only thing that holds on the restore arm is that the
focus is put back unchanged, including whether it exists. That is what is
asserted now, against the existence recorded before the ascent.
`to_next_sibling_byte` never panicked, because its matching arm carried no
assert at all; its answer was already correct. It gets the same check for
symmetry, and it holds. The `Some` arms of both keep the original
`path_exists()` assert, which is sound: that byte came out of the parent's
`child_mask`, so the sibling landed on does exist.
Measured with lean/differential.py, 4000 random inputs per seed, DEBUG build.
The class is `[prev_sibling_missing]`; the KNOWN table is untouched.
seed before after
7 3246/4000, 238 prev_sibling 3460/4000, 0
10 3202/4000, 248 prev_sibling 3432/4000, 0
12 3191/4000, 219 prev_sibling 3394/4000, 0
`new divergences` stays 0 on all three. Comparing per-input outcomes, every
input whose classification changed was previously `prev_sibling_missing`;
nothing that agreed before stopped agreeing. Most of them now agree outright
(214/230/203), and the remainder (24/17/15) run past the panic and reach
`[remove_unmasked_dangling]`, plus one input each on seeds 10 and 12 that
reaches `[status_imprecise]`. Those are pre-existing defects the panic was
hiding, not new ones.
RELEASE is unchanged, as expected for an assert-only defect: 20000 inputs,
seed 7, 19975/20000 agree, 25 known, 0 new, before and after.
cargo test --release, cargo test --release --features arena_compact,random and
cargo test (debug) all pass.
Co-Authored-By: Claude Opus 5 (1M context) <noreply@anthropic.com>
…ches
`WriteZipperCore::remove_unmasked_branches` (src/write_zipper.rs:2315)
descends through an onward link by calling `node_get_child_mut` on the
focus node, and falls back to filtering the focus node's own branches
when that returns `None`.
But a dangling path is stored as an onward link to the empty-node
sentinel, and `get_child_mut` deliberately declines to hand out an empty
child (src/line_list_node.rs:495 and :506; the same convention is
documented at src/write_zipper.rs:1603 for `graft_masked_branches`). So
a focus sitting at -- or below -- a dangling stub never descended, and
the stub's own key was handed to the focus node as if it were one of
that node's branches.
That breaks the invariant `LineListNode::node_remove_unmasked_branches`
relies on, "the calling code should have descended through this node if
that key specifies an onward link", and its
`debug_assert!(!self.is_child_ptr::<N>())` at src/line_list_node.rs:1964
and :1971 fired. In release the assertions compile away and
`remove_subtries(false, false, ..)` happens to be the right answer, so
this only showed up in debug builds.
Fix: recognise the dangling stub at the zipper before the descent and do
nothing. Nothing lives below a stub, so there are no branches to filter,
and the dangling path itself must survive -- which is what
`removeUnmaskedBranches` in lean/PathMapModel/Write.lean specifies, since
`z.childMask` at a dangling focus is empty. The node-level assertions
are left exactly as they were.
Instrumenting the call site over 1500 seed-7 inputs shows the new guard
taking 333 hits and `node_get_child_mut` always consuming the whole
`node_key`, so the single-level check covers every case the fuzzer
reaches.
Measurements, `lean/differential.py --random 4000 --maxlen 300`, DEBUG:
seed agree before -> after [remove_unmasked_dangling] new divergences
7 3246 -> 3734 513 -> 0 0 -> 0
10 3202 -> 3720 548 -> 0 0 -> 0
12 3191 -> 3752 588 -> 0 0 -> 0
The class is gone. It was masking two pre-existing classes, which grow
because those inputs now run past the abort instead of stopping at it:
[prev_sibling_missing] 239/249/220 -> 263/277/244 and
[status_imprecise] 3-4 -> 3-4 (+1 on seed 12). No new class appeared and
no input newly FAILed.
RELEASE, --random 20000 --seed 7: 19975/20000 agree, 25 known, 0 new --
unchanged from baseline, as expected.
`cargo test`, `cargo test --release` and
`cargo test --release --features arena_compact,random` all pass.
Co-Authored-By: Claude Opus 5 (1M context) <noreply@anthropic.com>
`ZipperWriting::restrict` keeps a path of the destination only when the source carries a value at some non-empty prefix of it (`validatedBy` / `restrictBelowRoot` in lean/PathMapModel/PathMap.lean). That applies to a dangling path -- one that exists but leads to no value -- exactly as it does to a valued one: an unvalidated dangling path is dropped. `ByteNode::prestrict_abstract` (src/dense_byte_node.rs:580, the dense-against- list/tiny/bridge path) walks `self`'s entries and rebuilds the node. For a byte where `other` has a path but no value, it kept whatever the onward link restricted to and cleared `is_identity` for the value it had to drop. A co-free with *neither* a value nor an onward link -- the dense representation of a dangling path, which `meet_into` materialises when it empties a branch -- fell through both of those: it was correctly left out of the rebuilt node, but nothing cleared `is_identity`. When every other byte restricted to an identity the node therefore returned `Identity(SELF_IDENT)`, and `WriteZipper::restrict` (src/write_zipper.rs:2230) responded by keeping `self` untouched -- with the dangling branch still in it. So this is a wrong answer, not only an imprecise status: both the kept path and the reported `Identity` were wrong, and the status follows from the content. The fix is the missing `else` arm: no onward link and no value means nothing of that byte reaches the result, which is a modification. The sibling paths were already right -- `Cf::prestrict` sends a dangling co-free to `None` via its `_` arm, `EmptyNode::prestrict_dyn` returns `None`, and `restrict_slot_contents` reaches that through `prestrict_dyn` -- so the dense/abstract walk was the only one on the wrong side of the asymmetry. A dangling path that *is* validated is still kept, as the model keeps it. Differential (release, --maxlen 300 --max-fails 0), before -> after, with 0 new divergences throughout: seed 7, 10000: 9999 -> 10000 agree (1 known -> 0) seed 10, 10000: 9999 -> 10000 agree (1 known -> 0) seed 0, 10000: 10000 -> 10000 seed 3, 10000: 10000 -> 10000 seed 11, 10000: 10000 -> 10000 seed 12, 10000: 10000 -> 10000 seed 99, 10000: 10000 -> 10000 ACT seed 0/7/12, 5000 each: 5000/5000 -> 5000/5000 Debug build (assertions on, 4000 inputs each): seed 7: 4000 -> 4000 seed 12: 4000 -> 4000 seed 10: 3999 -> 4000 (the same bug, hit once) The `[status_imprecise]` residual on seeds 1 and 2 did not move: seed 1 still has 1 hit and seed 2 still has 2, all `subtract_into`/`meet_into` status-only with every state field equal. lean/corpus/*.bin still agree 2/2. Tests: `write_zipper_restrict_drops_dangling_branch` covers the dense node with an unvalidated dangling co-free, the validated dangling co-free that must stay, and the shrunk differential reproducer spelled out as a program. It fails on the parent commit with `left: Identity, right: Element`. cargo test --release: 914 + 5 + 10 passed. cargo test --release --features arena_compact,random: 1050 + 5 + 19 passed. cargo test: 914 + 5 + 10 passed. Co-Authored-By: Claude Opus 5 (1M context) <noreply@anthropic.com> Claude-Session: https://claude.ai/code/session_019R2H8fnco29asY2v3TPbtF
Cherry-pick of a subagent's 194887a. A LineListNode may hold a value and an onward child under the *same* key -- that is how a path which both ends in a value and continues into a subtrie is stored. Emptying the child without pruning leaves the link in place, and the slot then carries nothing at all: there is nothing below an empty link, and the path it stands at is already there because of the value beside it. `remove_subtries` creates these routinely. Both algebras correctly *drop* such a slot, and both wrongly reported the drop as a change. `psubtract_dyn` saw `(None, Identity)` from `subtract_from_slot_contents`, fell through to the generic arm and returned `Element`; `pmeet_dyn_oriented` put the slot in `self_payloads`, where `EmptyNode::pmeet_dyn` answered `None` with a zero mask and `pmeet_generic` ANDed the combined mask to zero. No mask constant was wrong -- the identity bit was dropped by a slot that should not have been in the computation at all. A new `slot_is_shadowed_dangling` predicate (empty onward link AND a key equal to the other slot's) keeps subtract's identity and leaves the slot out of meet's payloads. The key comparison is exact: an empty link under a key of its own really does take a path away, and `Element` is right there. Verified, KNOWN table unmodified: seed 1, 10000 9999 -> 10000/10000 seed 2, 10000 9998 -> 10000/10000 seeds 0,3,7,10,11,12,99 10000/10000, unchanged Seed 2 needed both halves: its two hits were a subtract_into status case and a meet_into one, the same root cause in sibling paths. Conflicted with the restrict fix, which appended tests at the same point in write_zipper.rs; both test blocks are kept. Co-Authored-By: Claude Opus 5 (1M context) <noreply@anthropic.com> Claude-Session: https://claude.ai/code/session_019R2H8fnco29asY2v3TPbtF
The port of lean/PathMapModel/ to Rust was written against a tree where the
harness was examples/common/harness.rs and the model was its own cargo example
target. Both are gone: the harness is the `differential` crate now, so the
model lands in differential/src/reference/ with differential/src/bin/reference.rs
as its trace front end, next to pathmap_trace and act_trace.
The move costs one invariant and buys it back. "The model shares no code with
the implementation" used to be a fact about the build -- examples/reference/ did
not depend on `pathmap` at all -- and `differential` does depend on it, so a
stray `use pathmap::utils::ByteMask` would now compile and the differential would
start agreeing for the wrong reason. So it is asserted instead:
`reference::tests::model_does_not_touch_the_crate` reads the model's own source
and fails if any of it names the crate. `reference` is also not glob re-exported
from lib.rs, because it defines its own `PathMap`, `run` and `hex_path`.
The Lean model moved slightly while this was shelved, and the model follows it
rather than the other way round -- it is the reference being validated against:
* `u64Ops.psub` returns `Identity(SELF_IDENT)`, not `Element(*self)`, when the
values differ: subtracting a value that is not there leaves the destination
alone and says so.
* every `skip` renders as `skip:<reason>`. The seven reasons are transcribed
from Fuzz.lean rather than imported from harness.rs -- those are the crate
side's strings, and a second transcription that shares a constant with the
thing it is checking is not a second transcription.
* `restricting` tests the empty-focus guard before the ACT guard, and
`meet_k_path_into` splits `meetKPathUnspecified` into its two disjuncts, so
the skip names which rule fired. Both were invisible while every skip
rendered as a bare `skip`.
* op 54 `graft_child_maps` is no longer quarantined, so the model runs it:
the source's own child submaps, one single-byte mask each. This is the one
op the archived model had never executed, its `graft_child_maps` having been
written and then skipped in the same commit.
* `Zip::to_next_sibling_byte` carries the current model's account of the read
zipper root escape -- a live bug, skipped at the root -- not the archive's
"FIXED, no longer skipped".
`differential.py --model` comes back with it (it was removed in ceaaa30 when the
port was staged separately), including the rule that the KNOWN table does not
apply in that mode: it is a list of crate defects and the crate is not involved,
so every divergence is new. PATHMAP_REFERENCE overrides the binary search the
same way PATHMAP_TRACE does.
Co-Authored-By: Claude Opus 5 (1M context) <noreply@anthropic.com>
Claude-Session: https://claude.ai/code/session_019R2H8fnco29asY2v3TPbtF
Two front ends over the revived model, both reusing the existing op tables by
module path -- the model side `reference::fuzz::run`, the crate side
`harness::run` / `act::run_act` -- so there is still no fourth transcription.
`bin/in_process.rs` is the archived comparator, brought forward. It runs both
on the same bytes and compares the traces in memory: no subprocesses, no pipes,
no hex on stdin, no Python. The reason it was shelved is gone. It was written
against a crate that panicked on roughly one random input in eight, and it
deliberately does not `catch_unwind`, because catching a panic out of the middle
of a trie mutation drops half-updated refcounted nodes while the stack unwinds
and corrupts the heap. So a run used to end within a handful of inputs. The
panicking findings have since been fixed; the design is unchanged, there is
simply nothing left to end the run. The panic hook stays, and if a panic
reappears it stops and names the input, which is the right outcome.
Two deliberate changes from the archive:
* the random source now draws lengths uniformly from `[8, maxlen)`, which is
what `RandomInputs.get` in differential.py does. The archive drew from
`[8, 8+maxlen)`, so a divergence rate measured here was not comparable with
one measured there, which is the whole reason to have both.
* `--act` runs the ArenaCompactTree read source, so the in-process fuzzer
covers the same two configurations differential.py does.
It does not classify. The `KNOWN` table of tolerated crate defects lives in
lean/differential.py and there is exactly one of it, so `--save DIR` writes the
diverging inputs out and `./lean/differential.py DIR/*` does the triage -- which
also re-checks each one against the Lean oracle rather than against this
binary's own model. The run's own summary buckets by first differing *op*,
which needs no taxonomy.
`bin/afl_differential.rs` is the same comparison under AFL++, behind the `afl`
feature so a plain `cargo build -p differential` neither needs the dependency nor
builds the target. Uniform random bytes are the right shape for measuring a rate
and the wrong shape for finding: the residual divergence classes sit between 1 in
30,000 and 1 in 2,250,000, and a blind sampler pays full price for every one.
AFL keeps what reached new edges and mutates that. The wire format suits it --
every operand is a byte reduced mod a small number at the point of use, there is
no checksum and no whole-input length prefix, so a truncated input is a valid
shorter program and a byte flip lands on an op selector rather than being
rejected by a parser.
AFL also disposes of the unwind-safety question rather than working around it:
each input runs in a child forked from the fork server and `afl::fuzz!` aborts
instead of unwinding, so corruption cannot outlive the input that caused it.
That is the property the subprocess design bought, at a fraction of the cost.
`in_process --emit-corpus DIR` writes the seed corpus from the same generator.
Co-Authored-By: Claude Opus 5 (1M context) <noreply@anthropic.com>
Claude-Session: https://claude.ai/code/session_019R2H8fnco29asY2v3TPbtF
A divergence that first shows up in `MAP0`/`MAP1`/`ROOT0`/`ROOT1` has no step number, so reading the op name out of the second token printed the whole trie dump as the bucket label. Those lines carry their name in the *first* token instead, which is what "the step number parses as a number" distinguishes. Cosmetic: it only affects this binary's own per-op tally, not what it flags. The defect breakdown is still `./lean/differential.py`'s. Co-Authored-By: Claude Opus 5 (1M context) <noreply@anthropic.com> Claude-Session: https://claude.ai/code/session_019R2H8fnco29asY2v3TPbtF
The revived in-process fuzzer turned up three divergences in 9,000,000 inputs that `differential.py`'s KNOWN table does not match. All three are the `meet_keeps_dangling` defect -- the crate keeps a valueless path an algebraic op should have dropped -- and the Lean and Rust models agree byte for byte on all three, so nothing about the models is in question. Two of them are invisible to `classify()` for a structural reason worth a corpus entry. Its DANGLING-KEPT rule keys on `child_count` or `val_count` moving on the differing *trace* line; here every one of the run's 69 steps agrees exactly, and the extra path appears only in the final `MAP0` dump, which has no such fields. So the defect is real, known, and reported as new. This is the smaller of the two, shrunk from 250 bytes to 65 by lean/shrink.py. The third stops being unclassifiable once shrunk -- the reduced input's diff is narrow enough for the existing rule -- so it needs no entry. `./lean/differential.py lean/corpus/*.bin` now exits non-zero, which the README explains: it means one entry is unclassified, not that the crate regressed. No CI job runs that glob. Co-Authored-By: Claude Opus 5 (1M context) <noreply@anthropic.com> Claude-Session: https://claude.ai/code/session_019R2H8fnco29asY2v3TPbtF
The first real run saved 0 crashes and 18 hangs, and all 18 hangs replay through `in_process` as genuine divergences. Nothing was wrong with the target: AFL decides "crashed" by reaping the child and reading its signal, and when /proc/sys/kernel/core_pattern is a pipe -- apport here, systemd-coredump elsewhere, a distro default either way -- the kernel hands the corpse to that helper first and AFL's wait times out instead. It warns about this at startup, and AFL_I_DONT_CARE_ABOUT_MISSING_CRASHES=1 silences the refusal to start without changing the outcome. So the docs now say to sweep `hangs/` as well as `crashes/`, and give the tell for a *genuine* timeout -- an infinite loop in the crate, which would be a finding in its own right: it is the input in `hangs/` that `in_process` does not flag. The root-only fix is recorded next to it. Co-Authored-By: Claude Opus 5 (1M context) <noreply@anthropic.com> Claude-Session: https://claude.ai/code/session_019R2H8fnco29asY2v3TPbtF
`to_next_sibling_byte` and `to_prev_sibling_byte` were skipped on both sides whenever the target zipper sat at its own root, because the native `ReadZipperCore` override guarded on `prefix_buf.len() == 0` -- the *absolute* path length -- and so walked out of the root of a zipper rooted at a non-empty path (FINDINGS.md Adam-Vandervorst#3). The override now guards on the zipper's own root. Directly: over read zippers rooted at `[]`, `[0]`, `[0,0]`, a non-existent `[0,0,1]`, an existing `[0,0,3]` and an absent `[9]`, and over write zippers at the same roots, both moves return `None` at the root and leave `origin_path()` untouched. That is what the model already specified, so the guard now only creates a blind spot. Lifted on all three sides at once and A/B'd against the same sweeps with the guard in place: 20M inputs at maxlen 120, 20M at 300, 8M at 600, and 8M each at 300/600 in ACT mode -- 56M in all -- reproduce the baseline divergence report byte for byte, and no trace anywhere carries `ESCAPED-ROOT`. Identity is the expected outcome rather than a coincidence: at the root the operation moves neither side, so lifting it changes no downstream state. `differential.py --model` stays at zero in both modes, and the Lean model against the crate reports no new divergence over 500k inputs. Co-Authored-By: Claude Opus 5 (1M context) <noreply@anthropic.com> Claude-Session: https://claude.ai/code/session_019R2H8fnco29asY2v3TPbtF
`insert_prefix("")` was skipped on both sides because `make_parents_in(b"",
node)` discarded the node rather than doing nothing, destroying the subtrie
below the focus and still returning `true` (FINDINGS.md Adam-Vandervorst#4).
That was fixed upstream -- not by this effort -- and the fix carries its own
regression test, `write_zipper_insert_prefix_empty_is_identity`. Directly:
over seven trie shapes (empty, root value only, a single line, branchy, wide,
one with a dangling path, one built by grafting so the node boundaries fall
elsewhere), at the map root and at a non-root focus, `insert_prefix(&[])`
leaves the trie byte for byte unchanged in all fourteen. The return value
needed no special case either: `false` in exactly the shapes where the focus
has nothing below it, which is what `Zip.insertPrefix` already specified.
Same A/B as the previous commit -- 20M inputs at maxlen 120, 20M at 300, 8M at
600, 8M each at 300/600 in ACT mode -- reproduces the baseline divergence
report byte for byte. As with the root case this is the expected outcome
rather than luck: an identity operation changes no downstream state, so the
programs either side of the lift are the same programs.
`differential.py --model` stays at zero in both modes; the Lean model against
the crate reports no new divergence over 500k inputs.
Co-Authored-By: Claude Opus 5 (1M context) <noreply@anthropic.com>
Claude-Session: https://claude.ai/code/session_019R2H8fnco29asY2v3TPbtF
`restrict` was one of five return values masked to `?` whenever the write zipper's focus had nothing below it. The reason was FINDINGS.md Adam-Vandervorst#8: those returns branch on `get_focus().is_none()`, which is false at a location where `create_path` or `remove_val` happened to leave an empty node materialised and true at one that only ever carried a value. The model cannot see the difference, so the status was not compared there. It is compared now. Unmasked, over 20M inputs at maxlen 120, 20M at 300 and 8M at 600, the divergence report is byte for byte the one the mask produced -- no `restrict` line differs anywhere. The mask is not a branch that never runs: tracing 1500 inputs, 824 of 947 `restrict` calls hit it, so this is on the order of 30M statuses compared rather than skipped. (ACT mode is unaffected: `restrict` is `skip:act` there, so the ACT sweeps say nothing about it.) The other four stay, and the same experiment is why: unmasked, `remove_branches`, `join_map_into` and `take_map` each diverge on roughly one input in eight, immediately. Whatever decides `restrict`'s status, it is not the materialisation bit that decides theirs. This is evidence that the leak does not reach `restrict`, not a proof that it cannot; the commit is deliberately separate so it can be reverted alone if a counterexample turns up. `differential.py --model` stays at zero in both modes; the Lean model against the crate reports no new divergence over 500k inputs. Co-Authored-By: Claude Opus 5 (1M context) <noreply@anthropic.com> Claude-Session: https://claude.ai/code/session_019R2H8fnco29asY2v3TPbtF
`join_k_path_into` (for k > 0) had its return masked to `?` whenever the
collapse left the focus with no children. The stated reason was another
`AbstractNodeRef` leak: an empty node coming back as `Some(...)` from
`into_option()` for some representations, so `true` would be reported for a
collapse that produced nothing.
The sweep does not bear that out. Unmasked, over 20M inputs at maxlen 120,
20M at 300, 8M at 600, and 8M each at 300/600 in ACT mode -- 56M in all -- the
divergence report is byte for byte the one the mask produced; no
`join_k_path_into` line differs anywhere. The mask is not a branch that never
runs: tracing 1500 inputs, 678 of 1003 calls hit it.
`k = 0` is untouched and stays `skip:k0`. That one is a live bug, not a
suspicion: `join_k_path_into(0)` still destroys the subtrie at HEAD -- on
`{[] = 0, [0] = 0, [0,0] = 0, [1,0] = 0}` it returns `true` and leaves
`{[] = 0, [0] = 0}`, which is `zipper_bug_repros drop_head_zero` reproducing
exactly as FINDINGS.md Adam-Vandervorst#5 describes it.
As with `restrict`, this is evidence that the leak does not reach this return,
not a proof that it cannot, and it is a separate commit so it can be reverted
alone.
`differential.py --model` stays at zero in both modes; the Lean model against
the crate reports no new divergence over 500k inputs.
Co-Authored-By: Claude Opus 5 (1M context) <noreply@anthropic.com>
Claude-Session: https://claude.ai/code/session_019R2H8fnco29asY2v3TPbtF
`skip:quarantined` meant "this op is disabled outright", and the only op it ever applied to was 54, `graft_child_maps`. That was un-quarantined when its bug was fixed, and the token went with it -- but the constant stayed defined in all three op tables, the reason stayed listed in all three doc blocks, and the README still described a rule the fuzzer cannot fire. No call site remains on any side: `skipQuarantined` in `Fuzz.lean`, `SKIP_QUARANTINED` in `harness.rs` and the `#[allow(dead_code)]` one in `reference/fuzz.rs` are each referenced exactly once, by their own definition. The Rust one had to be marked dead to compile at all, which is the compiler saying the same thing. A skip vocabulary is a contract between three transcriptions, so a token in it that nothing can emit is not harmless: it invites the next reader to keep a suppression alive by analogy with one that is already gone. Removed from all three, and from the README's table. No behaviour changes -- the token appears in no trace before or after -- so the sweeps are untouched by construction. Co-Authored-By: Claude Opus 5 (1M context) <noreply@anthropic.com> Claude-Session: https://claude.ai/code/session_019R2H8fnco29asY2v3TPbtF
The four commits that lifted a suppression each A/B'd it over five sweeps -- 20M inputs at maxlen 120, 20M at 300 and 8M at 600 in crate mode, plus 8M each at 300 and 600 in ACT mode. That is 64M, and three of the notes say 56M: I added the five figures up wrong and the mistake was copied from the first commit message into the next two and into the README. The sweeps themselves are unchanged; only the arithmetic describing them was wrong, and it understated rather than overstated. `restrict`'s figure of 48M was already right -- it is `skip:act`, so the two ACT sweeps say nothing about it and its evidence is the crate-mode 48M alone. While here, the note about how much the two lifted masks actually exercised is made concrete rather than impressionistic: at the measured hit rates (824 of 947 `restrict` calls and 678 of 1003 `join_k_path_into` calls over 1500 traced inputs) the sweeps compared on the order of 26M and 29M returns that used to be reported as `?`. Co-Authored-By: Claude Opus 5 (1M context) <noreply@anthropic.com> Claude-Session: https://claude.ai/code/session_019R2H8fnco29asY2v3TPbtF
…ment `emit_repro` still wrote `// graft_child_maps: quarantined by the harness (FINDINGS Adam-Vandervorst#15)` for op 54 after the harness had started running it, so a repro for any input that reaches op 54 silently did not reproduce the trace -- the drift the module header warns about. The emitted code now does what `do_graft_child_maps` does: build one map per masked child of the source and graft them. Checked by compiling the generated repros and comparing the maps they print against the trace's MAP0/MAP1. Of 600 random inputs (seed 7, maxlen 300), 236 reach a live graft_child_maps. Before: 220 reproduce, 16 do not. After: 233 reproduce. The other 3 are a separate drift, still present: the repro calls `prune_path`/`prune_ascend` off the map root and `restricting` on an empty focus, where the harness skips them. With those guarded the same way as well, all 236 reproduce. Co-Authored-By: Claude Opus 5 (1M context) <noreply@anthropic.com> Claude-Session: https://claude.ai/code/session_019R2H8fnco29asY2v3TPbtF
The harness has compared `insert_prefix("")` since the skip was lifted
(FINDINGS Adam-Vandervorst#4, fixed upstream), but `emit_repro` still wrote a "skipped by
the harness" comment in its place. It emits the call now, spelled
`&[0u8; 0]` because `insert_prefix` is generic over the prefix and a bare
`&[]` has no element type to infer.
The empty prefix is the identity, so the old comment changed no final
maps; this is about the repro saying what the harness does. Checked by
compiling the repros for 600 random inputs (seed 7), which contain 33
empty-prefix calls: they build, and the match count against the trace's
MAP0/MAP1 is unchanged.
Co-Authored-By: Claude Opus 5 (1M context) <noreply@anthropic.com>
Claude-Session: https://claude.ai/code/session_019R2H8fnco29asY2v3TPbtF
…r tiny node
Root cause: `ByteNode::psubtract_abstract` (src/dense_byte_node.rs), used when a
DenseByteNode/CellByteNode is subtracted by a LineListNode or TinyRefNode. For
a key byte the other node reaches, a slot of `self` holding only a dangling
path -- an empty onward link, or a CoFree with neither link nor value, as left
behind by meet_2/restrict/graft_child_maps coming to nothing -- produces an
empty CoFree that is (rightly) not carried into the new node. But
`is_identity` was left set, so the op reported `Identity(SELF_IDENT)`,
`subtract_into` kept the original node, and the dangling path survived where
the spec (`PathMap.sub`: a location `b` reaches survives only on the way to a
surviving value) drops it. Now dropping a slot always clears `is_identity`.
A shadowed dangling link (value + empty link at one key) still keeps its
CoFree via the value and stays an identity.
This accounts for 1245 of the 1250 corpus inputs of the class (all with
subtract_into as the first differing op), plus the 3 unclassified inputs.
In-process campaigns, classified against Lean, before -> after:
seed 101 maxlen 120 10M: meet_keeps_dangling 42 -> 0, status_imprecise 18 -> 17,
sibling_after_iteration 7 -> 7, value_bias 1 -> 1
seed 102 maxlen 300 20M: meet_keeps_dangling 677 -> 2, status_imprecise 196 -> 157,
sibling_after_iteration 41 -> 41, new 1 -> 0
seed 103 maxlen 600 5M: meet_keeps_dangling 531 -> 1, status_imprecise 103 -> 73,
sibling_after_iteration 27 -> 27, value_bias 2 -> 2, new 2 -> 0
--act seed 104 maxlen 300 5M: 3 value_bias -> 3 value_bias
--act seed 105 maxlen 600 3M: 2 value_bias -> 2 value_bias
Co-Authored-By: Claude Opus 5 (1M context) <noreply@anthropic.com>
Claude-Session: https://claude.ai/code/session_019R2H8fnco29asY2v3TPbtF
…rd link
Root cause: `pmeet_generic_internal` (src/trie_node.rs). When a lookup in
`other` for one of `self`'s keys consumes part of the key and lands on an
onward link, the rest of the key is looked up in that child. If the child is
the empty node -- a dangling path in `other` -- nothing is found and
`node_key_overlap` on the empty node is 0, so the key was answered
`COUNTER_IDENT`: "the result equals `other` here". It does not: the meet
drops the dangling path. The typical shape is a LineListNode meeting a
DenseByteNode destination with a dangling child (the dense side enumerates
the list's payloads with `swapped`), where the dangling byte's sibling is an
Arc shared by both operands, so every other key also reports an identity and
the whole meet came back `Identity`, keeping the dangling child. An empty
`other_node` can only be reached through such a link, so it now never claims
`COUNTER_IDENT`.
These are the last 3 of the 1250 corpus inputs (meet_into first differing).
In-process campaigns, classified against Lean, before this commit -> after
(original base in brackets):
seed 101 maxlen 120 10M: meet_keeps_dangling 0 -> 0 [42], status_imprecise 17 -> 17 [18],
sibling_after_iteration 7 -> 7, value_bias 1 -> 1
seed 102 maxlen 300 20M: meet_keeps_dangling 2 -> 0 [677], status_imprecise 157 -> 157 [196],
sibling_after_iteration 41 -> 41, new 0 -> 0 [1]
seed 103 maxlen 600 5M: meet_keeps_dangling 1 -> 0 [531], status_imprecise 73 -> 73 [103],
sibling_after_iteration 27 -> 27, value_bias 2 -> 2, new 0 -> 0 [2]
--act seed 104 maxlen 300 5M: 3 value_bias, unchanged
--act seed 105 maxlen 600 3M: 2 value_bias, unchanged
Co-Authored-By: Claude Opus 5 (1M context) <noreply@anthropic.com>
Claude-Session: https://claude.ai/code/session_019R2H8fnco29asY2v3TPbtF
Reverts 7171655 ("Drop dangling paths from meet results") and 97ae27f ("Don't claim COUNTER_IDENT for a meet key that runs into an empty onward link"). Both made the crate follow the Lean model's rule that dangling paths never survive a meet. That rule is the model's own: on master `EmptyNode::pmeet_dyn` answers `Identity`, and master's tests assert it outright ("Should have had its value removed, but the path should remain"), which 7171655 had rewritten. Master's meet intersects locations -- a dangling path survives when the other side has that path too -- and prunes nothing. The drop was also not even consistent: a meet with a clone kept the dangling path through the pointer-equality shortcut while a meet with an independent copy dropped it. With the revert both keep it and report Identity, as on master. 053a186 (subtract dropping a dangling path the source reaches) stays: on master that already happens for list/list and dense/dense subtracts, and only the dense-against-list case kept the path. Co-Authored-By: Claude Opus 5 (1M context) <noreply@anthropic.com> Claude-Session: https://claude.ai/code/session_019R2H8fnco29asY2v3TPbtF
…angling paths
The model's meet kept only the locations leading to a surviving value, so no
dangling path survived a meet. Upstream intends otherwise: master's
`map_meet_dangling_branching_factor_test1` keeps a dangling path met against a
value ("value removed, but the path should remain") and checks both operand
orders. The rule is now:
prune = false a path exists in the result exactly when it exists in both
operands; a value exists exactly where both hold one, as the
meet of the two. meet(a, a) = a, dangling paths included.
prune = true the same values, and only the locations leading to one of
them: every dangling path is dropped, including one both
operands had.
In both, the focus -- the root of the met subtrie -- is never removed.
`meet_2` and `PathMap::meet`, which take no `prune`, are the first form. So
meet({[0,0]:-}, {[0,1]:-}) is {[0]:-}, and {} with prune.
Encoded as `PathMap.meet` / `PathMap.meetPruned` (with `dropDangling`) in the
Lean model and transcribed into the Rust reference model; `meet_into` and
`meet_k_path_into` choose between them on `prune` and no longer prune above the
focus. Meet's `prune` has an exact meaning now, so ops 38 and 46 use the
decoded flag instead of forcing false, in Fuzz.lean, harness.rs, the reference
op table and the repro generator. The Spec laws gain `meetIdem`,
`meetPrunedIdem` and `meetCommOnPaths`, guarded in Check.lean and check.rs; the
doc that meet is "not idempotent on locations" is gone.
The Lean and Rust models agree on 1,300,000 crate-mode and 500,000 ACT-mode
inputs (maxlen 120/300/600). The crate does not yet follow the rule.
Co-Authored-By: Claude Opus 5 (1M context) <noreply@anthropic.com>
Claude-Session: https://claude.ai/code/session_019R2H8fnco29asY2v3TPbtF
`prune = true` is relaxed: a meet may skip a node shared with the source rather than walk it for dangling paths, so a dangling path inside a shared node may survive. The result lies between `meetPruned` and `meet` -- the same values, and locations between the two -- but is no longer exact, so ops 38 and 46 go back to forcing `prune = false` in Fuzz.lean, harness.rs, the reference op table and the repro generator. The model keeps `meetPruned` as the most pruned result, documented as the lower bound. Co-Authored-By: Claude Opus 5 (1M context) <noreply@anthropic.com> Claude-Session: https://claude.ai/code/session_019R2H8fnco29asY2v3TPbtF
`write_zipper_meet_into_dangling_paths` states the rule the models now encode:
with `prune = false` a path exists in the result exactly when it exists in both
operands and a value exactly where both hold one, so meet({[0,0]:-}, {[0,1]:-})
is {[0]:-} and a meet with an equal trie -- a clone or an independent copy --
reports Identity and changes nothing; with `prune = true` every dangling path is
dropped except that nodes shared with the source may be skipped; the focus is
never removed; and the result does not depend on the node types of the two
sides.
It fails today, first on meet({[0,0]:-}, {[0,1]:-}), which the crate answers with
{} as master does. Committed failing on request, ahead of the crate fix.
Co-Authored-By: Claude Opus 5 (1M context) <noreply@anthropic.com>
Claude-Session: https://claude.ai/code/session_019R2H8fnco29asY2v3TPbtF
`prune_path_internal(false)` does not move the zipper, but to find where pruning stops it walks the node stack up, popping `focus_stack` and `prefix_idx`, and it left them there. When the focus sat in a child node -- after a `graft` at the zipper's root, for instance -- the stack then described an ancestor while `prefix_buf` still named the focus, so the next write through the focus went to the wrong node. `get_val_or_set_mut` caught it by panicking on the value it had just set (`src/write_zipper.rs:1429`); other writes went astray silently. It now walks the stack back down towards the focus with `descend_to_internal`, as far as nodes still exist. Present on master (f477a91) as well, through `prune_path` directly and through `meet_into(.., true)`, which calls it. Found by fuzzing meets with the prune flag: map1 {[1,0,0,0,0]:0}, a write zipper at [0,0] grafts the read zipper at [1], descends one byte, meets with prune, then writes a value. Regression test `write_zipper_write_after_prune_path_below_a_graft` checks the resulting trie for both routes and fails without the fix. Fuzzing with the prune flag passed through to the crate: without the fix each of three 300k runs (maxlen 120/300/600) stops on this panic; with it all three complete with no panic. The suites pass apart from `write_zipper_meet_into_dangling_paths`, which is committed failing ahead of the meet fix. Co-Authored-By: Claude Opus 5 (1M context) <noreply@anthropic.com> Claude-Session: https://claude.ai/code/session_019R2H8fnco29asY2v3TPbtF
Root cause: `CoFree::pmeet` (src/dense_byte_node.rs) returned `None` when
neither the onward nodes nor the values of two co-frees met to anything,
and `ByteNode::pmeet` then cleared the byte from the result mask. Under the
meet rule a location exists in the result exactly when it exists in both
operands, so the byte must survive as a dangling co-free. A co-free whose
onward link is an empty node is dangling too, and was treated as holding a
node, which made the identity masks wrong for it. The slim-pointer dispatch
of `pmeet_dyn` also answered `None` for an empty node, where
`EmptyNode::pmeet_dyn` answers an identity of the empty side.
Fix: two co-frees always meet to at least the bare location; a dangling side
(no value, no non-empty onward node) is an identity; otherwise each part is
met and the identity mask is taken part by part, a part that meets to
nothing being equal to the side that had nothing there.
`map_meet_after_join_test` asserted master's rule (a meet of maps with no
common value is empty); the maps share the first bytes of their paths, so
the result now holds those as dangling paths and no value.
Crate vs reference model, prune = false, 1M inputs, first differing op
(before -> after):
seed 101 / maxlen 120: meet_into 2985 -> 2671, meet_2 1181 -> 1156,
meet_k_path_into 642 -> 644
seed 102 / maxlen 300: meet_into 7606 -> 6960, meet_2 3484 -> 3427,
meet_k_path_into 1449 -> 1453
seed 103 / maxlen 600: meet_into 13755 -> 12777, meet_2 6838 -> 6728,
meet_k_path_into 2503 -> 2504
Most remaining meet divergences go through list nodes (next commit).
Co-Authored-By: Claude Opus 5 (1M context) <noreply@anthropic.com>
Claude-Session: https://claude.ai/code/session_019R2H8fnco29asY2v3TPbtF
…hs below it Root cause: `WriteZipperCore::meet_into` (src/write_zipper.rs) called `prune_path()` whenever the node meet left nothing below the focus and `prune` was set, and removed the focus value with `remove_val(prune)`; both can remove the focus and its ancestors, which the meet rule forbids. `meet_k_path_into` did the same through `remove_branches(prune)`. And `prune = true` did not drop dangling paths: it only differed from `prune = false` in removing the focus. Fix: the value step removes with `prune = false`, and nothing left below the focus grafts `None` without pruning, so only what is below the focus and the focus value change. With `prune`, the meet result is passed through `node_drop_dangling` (src/trie_node.rs, with `drop_dangling` for dense and list nodes), which rebuilds the result keeping only the locations on the way to a value, and skips a node pointer-equal to the source's node at the same location (the relaxation the rule allows), so meeting a clone stays cheap. `meet_k_path_into` drops the dangling paths of the met map the same way before grafting it, and never prunes the focus. `write_zipper_meet_into_test4`, test 3, asserted master's behaviour: a pruned meet of dangling paths kept the one both sides had and reported `Element`. Under the rule `prune` drops it too, leaving nothing below the focus (`None`) and the focus itself in place. Added test 4 for the same meet without prune. `prune = true` is not fuzzed. prune = false divergences are unchanged by this commit (seed 101/120: 4543, 102/300: 11963, 103/600: 22167 at 1M inputs). Co-Authored-By: Claude Opus 5 (1M context) <noreply@anthropic.com> Claude-Session: https://claude.ai/code/session_019R2H8fnco29asY2v3TPbtF
… have
Root cause: the list-node meet (`pmeet_generic` / `pmeet_generic_internal`
in src/trie_node.rs, used by `LineListNode::pmeet_dyn_oriented` for list
nodes and, swapped, for dense nodes met against list nodes) produced a result
entry only where the other node had a payload at a slot's full key, or a
value where the slot had an empty link. So, against the rule that a location
exists in the result exactly when it exists in both operands:
- a slot whose key the other side only has a prefix of was dropped, losing
that prefix: meet({[0,0]}, {[0,1]}) gave {} instead of {[0]};
- a slot whose onward nodes met to nothing was dropped instead of left as a
dangling path at its key;
- a value slot met against a location without a value was dropped;
- and because a dense node met against a list node is computed by the list
node, the dense side's result depended on the list node's walk, so a dense
destination met with a list source dropped a dangling path other layouts
keep, and its `SELF_IDENT` relied on `COUNTER_IDENT` from an exhaustiveness
test (`node_get_payloads`) that did not account for dangling paths.
Fix: `meet_list_slot` locates each slot's key in the other node through its
onward links, and contributes the slot's payload, a met value or onward
node, or a dangling path along the deepest prefix of the key the other side
has. Dangling contributions made redundant by the other slot are dropped so
the node stays valid. `SELF_IDENT` is decided per slot and is exact.
`COUNTER_IDENT` is only claimed when the list node computes a meet for a
dense node (`swapped`), where it becomes the dense node's `SELF_IDENT`; it
holds when each slot's contribution covers the other side along and below
the key and `meet_other_within_slots` finds nothing else in the other node
(no other branch off the keys, no value on them except under a value slot).
`pmeet_generic*` and the `node_get_payloads` methods it was the only user of
are removed, with the helpers that became unused. (The identity-mask fixes
to `node_get_payloads` on branch worktree-agent-a769033384de53103, 9639511
and f1b1460, are not needed and were not cherry-picked.)
Crate vs reference model, prune = false, first differing op in meet_into /
meet_2 / meet_k_path_into (base 3c868e1 at 1M -> this commit):
seed 101 / maxlen 120: 2985 / 1181 / 642 -> 0 / 0 / 0 (1M and 5M)
seed 102 / maxlen 300: 7606 / 3484 / 1449 -> 0 / 0 / 0 (1M and 5M)
seed 103 / maxlen 600: 13755 / 6838 / 2503 -> 0 / 0 / 0 (1M and 5M)
Fresh seeds 9001/120, 9002/300, 9003/600: 2986 / 1137 / 617,
7461 / 3481 / 1440, 13893 / 6867 / 2582 at 1M -> 0 / 0 / 0 at 5M.
ACT mode, 1M: seed 501/300 1698 meet_k_path_into divergences -> 0 in total;
seed 502/600 3065 -> 0 (one `dump` value-bias divergence remains, as on base).
The residue is to_prev_sibling_byte, subtract_into, and join_k_path_into value
bias (MAP0), none downstream of a meet.
meet benches (median, before -> after): superdense_meet 32000 252.9 -> 216.6 µs,
sparse_meet 1600 76.87 -> 63.02 µs, binary_meet 1600 373.8 -> 354.7 µs; no
bench slower by more than ~6%.
Co-Authored-By: Claude Opus 5 (1M context) <noreply@anthropic.com>
Claude-Session: https://claude.ai/code/session_019R2H8fnco29asY2v3TPbtF
Every candidate input went to one fixed path, lean/.shrink.bin, and $TMPDIR was ignored, so shrinks run concurrently overwrote each other's candidates. Eight parallel shrinks of value-bias inputs gave an IndexError on a garbled trace, "input does not diverge" for an input that does, and a "minimal" input that no longer diverged. The temp file is now per process under tempfile.gettempdir(); the same eight shrink correctly in parallel, to 39-70 bytes each. Co-Authored-By: Claude Opus 5 (1M context) <noreply@anthropic.com> Claude-Session: https://claude.ai/code/session_019R2H8fnco29asY2v3TPbtF
LineListNode::drop_head_dyn, in the case where both keys outlive the
dropped bytes, shortens the keys and swaps the two slots when the
shortened keys come out in the opposite order (e.g. [0,0,0] and [1,0]
dropping 1 byte give [0,0] and [0]). It then called factor_prefix,
which always merged slot 0 on the left. After the swap slot 0 holds the
payload from the lexicographically *later* k-path, so on a u64 collision
its value won, while the spec (Zip.joinKPathInto / PathMap.dropHead)
folds the stripped subtries in ascending k-path order and keeps the
first value. Whether the swap happens depends on how the subtrie is
split across nodes, hence the layout dependence.
factor_prefix now takes `slot1_first`; drop_head_dyn passes whether it
reordered the slots, and merge_guts runs with slot 1 as the left
operand in that case. The Identity branch also now honours
COUNTER_IDENT instead of assuming SELF_IDENT.
Reproducer (join_k_path_into(2) on {[3,0,0,0]:173, [0]:0, [3,1,0,0]:0,
[3,1,0,1,2]:82, [0,0,2]:196, [0,0,3,1]:38}) gave [0,0]=0, spec 173;
added as a regression test.
Numbers (in_process, crate vs Rust reference, classified via Lean):
- 8 shrunk fuzzer inputs: 0/3 crate + 0/5 ACT agree before, 3/3 + 5/5 after
- value_bias_by_node_layout before -> after:
crate s301 10M ml120 0->0, s302 10M ml300 1->0, s303 5M ml600 2->0,
ACT s304 3M ml300 2->0, s305 3M ml600 3->0
- fresh seeds before -> after: crate s411 20M ml300 1->0,
s412 20M ml600 7->0, ACT s413 10M ml300 8->0, s414 10M ml600 9->0
- sibling_after_iteration / status_imprecise unchanged
(4/1, 22/3, 35/5, s411 46/12, s412 131/27)
Co-Authored-By: Claude Opus 5 (1M context) <noreply@anthropic.com>
Claude-Session: https://claude.ai/code/session_019R2H8fnco29asY2v3TPbtF
…-node sibling
A location holding both a value and a child is stored in a LineListNode as two
slots with the same key. `get_sibling_of_child`, stepping backwards, took the
onward child only from the slot whose byte it matched first -- the value slot,
in that layout -- so `to_prev_sibling_byte` landed on the location without its
node: `child_count` reported 0 and nothing below could be reached. From
{[2]:0, [2,0]:0, [2,1]:0}, a read zipper at the off-trie [3] stepped to [2]
with child_count 0 and `descend_first_byte` returning None. The branch is from
e659a96 ("Fixing prev_sibling bugs"). It now looks for the child in both slots
holding the sibling's key.
This was the `sibling_after_iteration` class: all 117 inputs of it from two
fresh fuzz runs (30M inputs) first diverged at to_prev_sibling_byte, and all
117 agree now. Fresh seeds after the fix: crate 711/300 20M, 712/600 10M,
713/120 10M and ACT 714/600 5M show no sibling divergence and no panic; the
only remaining class is status_imprecise (3 and 15).
Regression test `read_zipper_prev_sibling_onto_a_value_and_child_location`
fails without the fix.
Co-Authored-By: Claude Opus 5 (1M context) <noreply@anthropic.com>
Claude-Session: https://claude.ai/code/session_019R2H8fnco29asY2v3TPbtF
Four ops in the Rust program emitted by `pathmap_trace --repro` did not match what the harness runs: - prune_path / prune_ascend (30, 31): the harness skips them unless the write zipper is at the map root; the repro always called them. - restricting (41): the harness skips it when either focus has no children; the repro always called it. - meet_2 (55): the harness takes the second source as a clone of the read zipper moved down `p`; the repro opened a fresh zipper on map1 instead, which has no history and is at a different place. - to_next_get_val (52): the repro called `to_next_val`. With these changes, compiled repros for 1335 random inputs (seed 55, all ops) end with the same MAP0/MAP1 as the trace. Co-Authored-By: Claude Opus 5 (1M context) <noreply@anthropic.com> Claude-Session: https://claude.ai/code/session_019R2H8fnco29asY2v3TPbtF
…value A byte node location can hold a value together with an empty onward link. The link carries nothing, because the value already holds the location. `CoFree::psubtract` leaves such a link out of the subtraction, but `combine_algebraic_results` then saw a link that was there go away and turned the value's `Identity` into `Element`. So `subtract_into` reported a change for a destination it had not changed. A value of the destination surviving the subtraction now keeps the result `Identity`. This was the `status_imprecise` class, the last divergence class between the crate and the model. All 38 saved inputs from 35M fuzz inputs (seeds 801-803) were `subtract_into` returning Element for Identity, and all 38 agree now. Fresh seeds after the fix: 901/300 20M, 902/600 10M, 903/1000 5M, ACT 904/600 5M, and 905/300 10M with debug assertions: 0 divergences, 0 panics. The regression test builds the layout with join_into, insert_prefix, meet_into and join_into, checks that the empty link is there, and fails without the fix. Co-Authored-By: Claude Opus 5 (1M context) <noreply@anthropic.com> Claude-Session: https://claude.ai/code/session_019R2H8fnco29asY2v3TPbtF
…t reach The differential harness only runs what the Lean model specifies, so much of the crate went unfuzzed: paths outside the 4-letter alphabet and 5-byte limit, value types other than u64, prune = true, most PathMap methods, every zipper kind but the plain read and write zippers, catamorphisms and anamorphisms, and .paths serialization. `differential/src/crash.rs` is a second op table over that surface with no model behind it: an input fails only by panicking (debug assertions included), crashing on a signal, or hanging. Calls with a documented panic are made to meet their precondition (KNOWN_PRECONDITIONS), and known failures -- val_count stubs, TrieRef forks at missing paths, k == 0, to_next_k_path without descend_first_k_path, meet_k_path_into on an empty focus -- are steered around unless --include-known (KNOWN_FAILURES). Front ends: - `crash_fuzz`: random or file inputs over -j threads. A watchdog reports hangs and abandons the stuck thread, a signal handler attributes segfaults and aborts to their input, and --keep-going supervises worker processes and groups failures by site. CRASH_TRACE=1 and CRASH_BACKTRACE=1 are for replaying one input. - `afl_crash`: the same table under AFL. - `crash_shrink.py`: shrinks an input keeping its failure site. Input generation moves from `in_process` to `differential::source` so both in-process front ends share it. A 50k-input survey with debug assertions and overflow checks found 27 failure sites, including undefined behaviour reachable from safe code. Co-Authored-By: Claude Opus 5 (1M context) <noreply@anthropic.com> Claude-Session: https://claude.ai/code/session_019R2H8fnco29asY2v3TPbtF
CRASH_FINDINGS.md lists the 29 failure sites from two 50k-input surveys (debug assertions and release) and a 10k-input all_dense_nodes survey: what each one is, how often it was hit, the public call that reaches it, and either a minimal Rust reproducer or a (seed, index) input to replay. Three are undefined behaviour reachable from safe code (ZipperHeadOwned exclusive paths, as_dense_unchecked in PathMap::join, heap corruption after ZipperHead writes); the rest are panics, failed debug assertions and hangs, plus the known failures the table steers around. crash_repros compiles the eight minimal reproducers, one selectable case each. Co-Authored-By: Claude Opus 5 (1M context) <noreply@anthropic.com> Claude-Session: https://claude.ai/code/session_019R2H8fnco29asY2v3TPbtF
imlvts
force-pushed
the
fuzz-fixes-v2
branch
from
September 17, 2026 10:25
07dac74 to
10a6332
Compare
imlvts
changed the title
imlvts
marked this pull request as draft
September 19, 2026 08:04
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.
This makes PathMap consistent with the spec across as many test cases as I could run.
This includes
meetrule change.