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
With an empty path and the head's root inside a node, the walk popped a byte of the head's own path and never put it back. The next request then read past its key buffer (UB in release) or panicked. Co-Authored-By: Claude Opus 5 (1M context) <noreply@anthropic.com> Claude-Session: https://claude.ai/code/session_019R2H8fnco29asY2v3TPbtF
as_static_path_zipper asserted the zipper held no borrowed origin path, but write_zipper_at_path always does. Once buffers are prepared the path lives in prefix_buf, so drop the borrowed slice instead. Co-Authored-By: Claude Opus 5 (1M context) <noreply@anthropic.com> Claude-Session: https://claude.ai/code/session_019R2H8fnco29asY2v3TPbtF
ZipperHead read zippers own their root node, and get_trie_ref borrowed the root for the zipper's whole lifetime, which panics for an owned root. The TrieRef only needs to borrow the zipper. Co-Authored-By: Claude Opus 5 (1M context) <noreply@anthropic.com> Claude-Session: https://claude.ai/code/session_019R2H8fnco29asY2v3TPbtF
A secondary factor's root isn't a child of the node above it, so the core zipper's parent lookup unwrapped None. Ask the factor's TrieRef instead. Co-Authored-By: Claude Opus 5 (1M context) <noreply@anthropic.com> Claude-Session: https://claude.ai/code/session_019R2H8fnco29asY2v3TPbtF
val_count delegated to the core zipper, which only sees the current factor, and panicked elsewhere. Count by walking a copy of the product zipper below the focus. Co-Authored-By: Claude Opus 5 (1M context) <noreply@anthropic.com> Claude-Session: https://claude.ai/code/session_019R2H8fnco29asY2v3TPbtF
with_node_at_path joined the focus's node key and the child path in a fixed MAX_NODE_KEY_BYTES buffer, so a root path of 48 bytes or more overflowed it. Fall back to a heap buffer. Co-Authored-By: Claude Opus 5 (1M context) <noreply@anthropic.com> Claude-Session: https://claude.ai/code/session_019R2H8fnco29asY2v3TPbtF
With no root value and the zipper root at the root node, the lookup used an unset parent key and sliced out of range. The value there is just root_val. Co-Authored-By: Claude Opus 5 (1M context) <noreply@anthropic.com> Claude-Session: https://claude.ai/code/session_019R2H8fnco29asY2v3TPbtF
k = 0 is documented to return false, but with the focus in the source the method sliced the prefix past its end. Co-Authored-By: Claude Opus 5 (1M context) <noreply@anthropic.com> Claude-Session: https://claude.ai/code/session_019R2H8fnco29asY2v3TPbtF
LineListNode::pjoin_dyn's CellByteNode arm cast the other node with as_dense_unchecked, which is undefined behaviour for a cell node. Co-Authored-By: Claude Opus 5 (1M context) <noreply@anthropic.com> Claude-Session: https://claude.ai/code/session_019R2H8fnco29asY2v3TPbtF
make_cell_node called make_mut on the empty sentinel, which panics. Replace the sentinel with a new CellByteNode instead. Co-Authored-By: Claude Opus 5 (1M context) <noreply@anthropic.com> Claude-Session: https://claude.ai/code/session_019R2H8fnco29asY2v3TPbtF
With nothing below the base and no sibling, k_path_default_internal never reached its exit and spun. It also let k = 0 step sideways from the base. Stop when back at the base. Co-Authored-By: Claude Opus 5 (1M context) <noreply@anthropic.com> Claude-Session: https://claude.ai/code/session_019R2H8fnco29asY2v3TPbtF
A factor was entered below a primary path that doesn't exist, and a sibling step at depth 0 dropped the factor record although the core zipper can't leave the factor there. Later moves then saw factor roots the zipper didn't know about, and is_shared unwrapped None. Co-Authored-By: Claude Opus 5 (1M context) <noreply@anthropic.com> Claude-Session: https://claude.ai/code/session_019R2H8fnco29asY2v3TPbtF
ProductZipperG and DependentProductZipperG read focus_byte at the root, which is the primary's root path byte, and tried to ascend from there. The root has no siblings. Co-Authored-By: Claude Opus 5 (1M context) <noreply@anthropic.com> Claude-Session: https://claude.ai/code/session_019R2H8fnco29asY2v3TPbtF
Its sources may be rooted at different paths, so at the root their focus bytes differ and the debug assert failed; sibling steps then tried to move the root. Report None at the root. Co-Authored-By: Claude Opus 5 (1M context) <noreply@anthropic.com> Claude-Session: https://claude.ai/code/session_019R2H8fnco29asY2v3TPbtF
The branch meant to bring the second source down to the first one's depth descended the first source again, leaving them at different depths. Co-Authored-By: Claude Opus 5 (1M context) <noreply@anthropic.com> Claude-Session: https://claude.ai/code/session_019R2H8fnco29asY2v3TPbtF
The prefix always reported itself as existing, with one child, so a walk descended through it into a source that doesn't exist. The prefix now exists only when the source's root does. Co-Authored-By: Claude Opus 5 (1M context) <noreply@anthropic.com> Claude-Session: https://claude.ai/code/session_019R2H8fnco29asY2v3TPbtF
new_with_key_and_path_in copied the focus's node key into a fixed stack buffer, overflowing it (UB in release) when the key was longer, and truncated key + path when the two together didn't fit. Fall back to a heap buffer. Co-Authored-By: Claude Opus 5 (1M context) <noreply@anthropic.com> Claude-Session: https://claude.ai/code/session_019R2H8fnco29asY2v3TPbtF
merkleize recursed into empty child links, and the second one found the first in its memo and tried to replace it in the parent, which refuses to hand out an empty child. Empty children have nothing to share, so skip them. Co-Authored-By: Claude Opus 5 (1M context) <noreply@anthropic.com> Claude-Session: https://claude.ai/code/session_019R2H8fnco29asY2v3TPbtF
prepare_cf returned an existing link even when it was the empty sentinel, left by remove_branches, take_map or grafting nothing. A write zipper rooted there couldn't move or read. Give it a fresh node, as for a missing link. Co-Authored-By: Claude Opus 5 (1M context) <noreply@anthropic.com> Claude-Session: https://claude.ai/code/session_019R2H8fnco29asY2v3TPbtF
Co-Authored-By: Claude Opus 5 (1M context) <noreply@anthropic.com> Claude-Session: https://claude.ai/code/session_019R2H8fnco29asY2v3TPbtF
Co-Authored-By: Claude Opus 5 (1M context) <noreply@anthropic.com> Claude-Session: https://claude.ai/code/session_019R2H8fnco29asY2v3TPbtF
A head reader cloned an ancestor node, so the next exclusive writer copied it and left existing writers pointing into the old copy. Readers now own a private root holding only their own entry. Co-Authored-By: Claude Opus 5 (1M context) <noreply@anthropic.com> Claude-Session: https://claude.ai/code/session_019R2H8fnco29asY2v3TPbtF
Co-Authored-By: Claude Opus 5 (1M context) <noreply@anthropic.com> Claude-Session: https://claude.ai/code/session_019R2H8fnco29asY2v3TPbtF
Co-Authored-By: Claude Opus 5 (1M context) <noreply@anthropic.com> Claude-Session: https://claude.ai/code/session_019R2H8fnco29asY2v3TPbtF
Co-Authored-By: Claude Opus 5 (1M context) <noreply@anthropic.com> Claude-Session: https://claude.ai/code/session_019R2H8fnco29asY2v3TPbtF
Co-Authored-By: Claude Opus 5 (1M context) <noreply@anthropic.com> Claude-Session: https://claude.ai/code/session_019R2H8fnco29asY2v3TPbtF
Co-Authored-By: Claude Opus 5 (1M context) <noreply@anthropic.com> Claude-Session: https://claude.ai/code/session_019R2H8fnco29asY2v3TPbtF
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-v3
branch
from
September 17, 2026 10:25
825abec to
ee7546e
Compare
imlvts
changed the title
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 part on top of part 2 includes crash-only fuzzer, which exercises more code, but doesn't check correctness. only checks for crashes.
List of crashes