Conversation
`PathMapModel` models a trie as `List (Path × Option V)`, because `pathmap`
locations really do come in three states and `create_path` /
`remove_val(false)` produce the middle one. Modelling that state is what most
of the specification's difficulty is: `subtract` needs a separate rule for
"where the source has no node, keep self's subtree verbatim, dangling paths
included", and every algebraic operation has to say which valueless locations
survive it.
`PrunedModel` takes the other branch. It covers only the subset of the API
that cannot leave a dangling path, and in exchange drops the `Option`:
entries : List (Path × V)
A location exists iff some key has it as a prefix -- existence is derived, not
stored, so a dangling path is unrepresentable rather than merely absent. There
is no third state to specify, no prune flag to thread, and subtract is
pointwise.
The claim is correspondingly stronger. Where `PathMapModel` says what the
crate does with dangling paths, this one says these operations never make one,
so a divergence is either a wrong value or a location that leads nowhere.
`Spec.no_dangling` is the proof, in three lines, next to 30 `#guard`s that
exercise the definitions on concrete tries at elaboration time.
Shares `PathMapModel.Basic` -- Path orders, ByteMask, ValOps, AlgStatus -- which
is vocabulary rather than model; everything else is independent.
Co-Authored-By: Claude Opus 5 <noreply@anthropic.com>
Three pieces, mirroring the existing harness one for one: * `lean/PrunedModel/Fuzz.lean` + `lean/PrunedMain.lean` -- the oracle, with the same wire format and resident-server protocol. * `differential/src/pruned.rs` + `bin/pruned_trace.rs` -- the crate side. One read source, so no `ReadSource` trait and no ACT mode; `graft_child_maps`, quarantined in the other harness, is simply not in this table. * `lean/pruned_differential.py` -- the driver, which is `differential.py` with `ORACLE`, `TRACE_CANDIDATES` and `KNOWN` repointed. Nothing about *how* inputs are run is duplicated. Three restrictions define the subset. No `create_path`, whose whole purpose is a location with no value. `prune = true` everywhere, with `prune_path` and `prune_ascend` kept in the table as assertions -- the model says `0`, so a non-zero count means something in the subset leaked a dangling path for it to find. And the write zipper is rooted at the map root, because one rooted below it holds a node at its own root that survives as a location leading nowhere, which `prune_path` is documented not to rise above; off-root writing is still covered via `descend_to`. `pruned_trace --check` needs no oracle at all: it asserts the zipper invariants after every operation and, at the end, that the write target contains no dangling path -- the whole claim the subset makes. First 30 random inputs: 23 agree, and 6 of the 7 divergences are one class, reported next. Co-Authored-By: Claude Opus 5 <noreply@anthropic.com>
63 of 70 divergences are one mechanism, across seven operations: an operation whose result is empty materialises the focus anyway. Where the focus existed it leaves the chain behind, which is a missing prune; where it did not, it *creates* it -- the write path builds the node chain down to the focus before discovering it has nothing to put there, so `graft` with an empty source is accidentally `create_path`. `remove_prefix` creates the whole chain, not just the tip. The seven are exactly the operations with no `prune` parameter: `graft`, `graft_src_at`, `graft_masked_branches`, `meet_2`, `restrict`, `restricting`, `remove_prefix`. The ones that have one clean up correctly with it set, which is what this harness passes throughout, so `meet_into` and `meet_2` -- the same operation with and without a destination -- differ only in whether a caller can ask for a tidy trie. A second finding is the same mechanism one level down and worse there: `graft_masked_branches` creates a *child* for a mask bit whose branch the source lacks, so `child_mask` gains a bit for a branch holding nothing and every consumer that recurses on the mask walks into it. The remaining two shapes are already recorded against the other model (`join_into` value bias, `join_map_into` status) and are in the corpus so a regression shows up in whichever harness is run. 10 minimal reproducers, 9-47 bytes, in lean/pruned-corpus/. The driver's shape classifiers name the two new ones, so a future run can tell them from whatever is underneath. Co-Authored-By: Claude Opus 5 <noreply@anthropic.com>
The first classifier keyed on `e` alone, so an input where the crate gained both the focus and a child of it (`e0 c0` -> `e1 c1`) fell through as unclassified -- 4 of 4000, all `graft_masked_branches`, all the same mechanism as the 897 that did classify. The rule is now stated the other way round, which is what it was always about: `e` and/or `c` moved *up* while `v` and `n` did not move at all. A location appeared without a value appearing anywhere at or below the focus, so whatever the crate created or kept leads nowhere. Both halves of the finding -- the focus itself and a child of it -- land in one entry. The dump-shaped variant is renamed DANGLING-DUMP, since differential.py already uses DANGLING-KEPT for a different shape and a shared name would make the two indistinguishable in `KNOWN`. 4000 random programs on master now leave 0 unclassified. README gains a section on why there are two models at all, and the agreement table. Co-Authored-By: Claude Opus 5 <noreply@anthropic.com>
Built the pruned harness on fuzz-fixes-v3 (ee7546e) and ran the same 4000 inputs with the oracle unchanged. Neither new finding is fixed there: 974 hits, and all 8 dangling-path reproducers still diverge -- including on graft_masked_branches, which the branch does touch (3a16a57, "Fix graft_child_maps and graft_masked_branches"), so that fix addressed something else. Both classes the model *inherited* are fixed: value bias by 3dae731, and Identity-not-reported-where-nothing-changed across join_map_into, subtract_into and meet_into. That split is the argument for keeping two models rather than one. fuzz-fixes-v3 was driven by the model that reproduces dangling paths, and no amount of fuzzing against it could have reported an operation for *making* one. Two v3 columns are spec drift, not findings, and are now labelled as such: v3 changes the k-path walk (420 inputs diverge in descend_first_k_path / k_path_walk) and the integer psubtract (f8a4599 -- 45 of 600 show subtract_into reporting Identity, the opposite direction from the inherited finding). This oracle is pinned to master's reading of both. The STATUS-ONLY shape is two-directional as a result, so its KNOWN note now says to read the direction rather than the tag. Also corrects the previous commit's claim that the Identity class was only a join_map_into defect: it shows up in subtract_into and meet_into too. Co-Authored-By: Claude Opus 5 <noreply@anthropic.com>
join and meet are meant to be union and intersection. PrunedModel/Lattice.lean proves it, rather than checking it on examples as PathMapModel/Spec.lean's #guards do. The laws hold in this model and are *false* in the other one, which is the interesting part. PathMapModel.meet keeps a location only when it leads to a surviving value, so `meet a a` drops a's dangling paths: idempotence fails on exactly the states PrunedModel cannot represent. A specification that reproduces the crate's dangling-path behaviour cannot also be a lattice. Four layers: 1. `valAt_mk'` -- canonicalisation moves no lookup. This is the load-bearing lemma and the bulk of the file: dedupVals keeps the first binding per key, insertValSorted is a lookup update given a fresh key, and the insertion sort preserves lookups because dedupVals leaves keys distinct (`DistinctKeys`, proved here, is the invariant Map.lean's docstring only asserted). 2. `valAt_join` / `valAt_meet` -- each operation is pointwise on valAt. This is the step that would fail for a model storing locations separately from values, where what meet does at a path depends on what lies below it. 3. The ten laws, from `IsLatticeVals`: associativity, idempotence, empty as join's identity and meet's annihilator, both absorptions, both distributivities. Commutativity is a separate `IsCommVals`, because pathmap's integer pjoin returns Identity(SELF_IDENT) and ignores the counterpart -- `u64_not_isComm` proves join over u64 is not commutative, which is also why the value-bias class was worth fixing: with a non-commutative join, which operand lands on the left is observable. 4. `u64_isLattice` and `unit_isLattice` / `unit_isComm` discharge the hypotheses for the two instances the crate provides, plus `unitOps` in Basic.lean transcribing `impl Lattice for ()`. Over () the correspondence is exact rather than merely satisfied: Option Unit has two inhabitants, so valAt carries one bit per path and `unit_join_isSome` / `unit_meet_isSome` are that bit's || and &&. A trie over () *is* a finite set of paths. Not claimed: a Boolean algebra proper. Path is infinite, so there is no top element and no complement -- this is the lattice of finite sets of paths, a distributive lattice with a least element. The relative complement that would make it generalized Boolean is PrunedMap.sub, whose pointwise characterisation needs the DistinctKeys hypothesis and is not proved here. Statements are `Agree a b` (equal at every path) rather than `a = b`; upgrading them needs Path.lt shown to be a strict total order, which is next. Co-Authored-By: Claude Opus 5 <noreply@anthropic.com>
The laws were `Agree a b` -- equal at every path. They are now `a = b`, which is the model's own equality: `beqT`, which decides AlgebraicStatus::Identity, compares entry lists structurally. The bridge is that the canonical form is *unique*: a strictly-key-sorted association list is determined by its lookup function (`eq_of_sortedKeys_of_lookup`). Proving it needs `Path.lt` to be a strict total order, so `lt_trans` and `lt_total` join `lt_irrefl` in Basic.lean, beside the definition -- `lt_irrefl` moves there from PathMapModel/Spec.lean, where it was the only one of the three. `SortedKeys` folds distinctness into strictness, so one predicate is the whole invariant, and `canonical_mk'` shows everything the model builds satisfies it. Where the right-hand side is an operation's output there is no side condition. Where it is the bare `a` -- idempotence, the `empty` identity, both absorptions -- `a` must be canonical, and that is not a technicality: a trie whose entry list binds a key twice really is not equal to its own join, because the join keeps only the first binding. `canonical_setVal`, `canonical_removeVal`, `canonical_subtrie` and friends discharge it for anything the model constructs. The file ends with all ten laws applied at `unitOps` and at `u64Ops` with nothing left abstract, as `example`s the build checks -- twelve for `()` including both commutativity laws, ten for `UInt64` without them. 67 theorems, no `sorry`, no new axiom. Both harnesses unchanged: 5000 pruned inputs and 3000 old-harness inputs at 0 new divergences, cargo test --lib 1035. Co-Authored-By: Claude Opus 5 <noreply@anthropic.com>
…trie level
Two gaps, both found by asking where commutativity was actually restricted.
The restriction was real but invisible: `IsCommVals ops` as a hypothesis,
discharged only by `unit_isComm`, with `u64_not_isComm` ruling out `u64Ops`. But
the only place the `()` laws were *applied* was a block of anonymous `example`s,
so "join over () is commutative" was checked by the build and citable by nobody.
All twenty-two instantiations are now named theorems: twelve for `PrunedMap Unit`
including `unit_join_comm` / `unit_meet_comm`, ten for `PrunedMap UInt64`.
The second gap was rigour, not presentation. `u64_not_isComm` rules out the
*value-level* hypothesis, which is not the same claim as the trie operation being
non-commutative -- a priori the asymmetry could have been invisible once lifted.
`u64_join_not_comm` and `u64_meet_not_comm` now prove it where it is claimed:
¬ ∀ a b : PrunedMap UInt64, join u64Ops a b = join u64Ops b a
by the two single-path tries {[0] -> 1} and {[0] -> 2}, which join to themselves
in whichever order puts them on the left. Four `#guard`s run the same
counterexample through `beqT` -- the equality the model uses to decide
AlgebraicStatus::Identity -- so the claim is both proved and executed, and a
fifth shows the same two paths over `()` give the same trie, which is where the
asymmetry goes.
Co-Authored-By: Claude Opus 5 <noreply@anthropic.com>
`IsLatticeVals` is a condition on a value type, and `PrunedMap V` has join/meet
of its own, so the question is whether the structure composes.
It does not for `PrunedMap V`, and the reason is worth having written down. Five
of the ten laws hold -- both associativities, both `none` laws, meet over join --
and five fail, because the *type* has more inhabitants than the lattice has
elements. `nonCanonical = ⟨[([0],1),([0],2)]⟩` binds one key twice and `join`
keeps only the first binding, so `join a a = a` is false for it. Every failing
law is one whose right-hand side is an operand rather than another operation's
output -- precisely the laws carrying the `Canonical` side condition in
Lattice.lean §7. That side condition was never bookkeeping; it is this
obstruction, and `trieOps_not_isLattice` makes it a theorem.
Restricting to `CMap V = { t : PrunedMap V // Canonical t }` fixes it: all ten
laws, the subtype's own proof field discharging every side condition. So tries
nest, and it is `CMap V` rather than `PrunedMap V` that is the lattice object.
One law needed more than the §3 bundle. `joinDistribMeet` has a single case,
`(some a, some b, none)`, that reduces to `meet (join a b) a = a` -- absorption
with the join on the *left*. A commutative lattice gets that from the standard
axiom read backwards; pathmap's join is not commutative, so the two orientations
are different statements and only one is an axiom. Added as `IsFlipAbsorb`, with
both instances discharging it: `u64Ops` satisfies it despite being
non-commutative, because a left-biased `pjoin` makes `join x y` agree with `x`
wherever `x` has a value, which is exactly where the meet then looks. So nesting
works over `UInt64` as well as `()`, to any depth.
Co-Authored-By: Claude Opus 5 <noreply@anthropic.com>
`entries : List (Path × V)` becomes a structure with a second field, `sorted : SortedKeys entries`. Keys strictly increasing, which by `distinctKeys_of_sortedKeys` also rules out a key bound twice -- one predicate is the whole invariant, so one proof field suffices. What that buys, in order of how much it mattered: * **Every side condition goes.** The ten lattice laws were `=` only with `Canonical a` wherever the right-hand side was the bare `a` -- idempotence, the `empty` identity, both absorptions. The hypothesis existed because the old type admitted `⟨[([0],1),([0],2)]⟩`, and such a trie really is not equal to its own join. That expression is now a type error, so the hypothesis is gone from all ten laws and from the twenty-two per-instance theorems. * **`PrunedMap` becomes the lattice object.** `Nested.lean`'s `CMap` subtype existed only to exclude the junk; it is deleted, `trieOps_not_isLattice` (which was a theorem) is replaced by `trieOps_isLattice` (all ten laws), and the file drops from 230 lines to 169 while gaining a three-deep nesting example. * **`eq_of_agree` is one line.** `PrunedMap.ext`, from `eq_of_sortedKeys_of_lookup` plus proof irrelevance on the `Prop` field. Mechanically: the list-level canonicity development -- `dedupVals`, `insertValSorted`, `normVals`, `DistinctKeys`, `SortedKeys` and their twenty-odd lemmas -- moves out of `Lattice.lean`'s first and last thirds into a new `Canon.lean`, since `Map.lean` now needs it to build the proof field. No proof changed; they were already there, just on the wrong side of the file boundary. `Lattice.lean` 851 -> 496 lines. `Repr` is a hand-written instance now, the `Prop` field making `deriving` unavailable and pointless. I asked first rather than using `Std.TreeMap` as requested: TreeMap ships an `Equiv` relation precisely because `=` is too strong for it -- tree shape is not determined by contents -- so it would have removed the side conditions at the cost of the equational form. The sorted-list subtype gets both. Unchanged: 20000 pruned inputs and 3000 old-harness inputs at 0 new divergences, the same known class at the same rate, cargo test --lib 1035, zero warnings. Co-Authored-By: Claude Opus 5 <noreply@anthropic.com>
The empty-source-node exit used to `return` the node status on its own, which threw away a value the operation had already written: with no root value in the destination and only a root value in the source, the trie gained a value and the call reported Identity. That is issue Adam-Vandervorst#139, and master fixed it in PR Adam-Vandervorst#142 (276fca0) by ending both exits of join_map_into in the same `node_status.merge(val_status, true, true)`. Both models still described the early return, so they reported Identity where the crate now reports Element -- 104 of 4000 inputs on the pruned harness, which I had mislabelled as a crate defect fixed on fuzz-fixes-v3. It is the opposite: master moved and the models lagged. The non-short-circuit exit also passed `valWasNone` as merge's second flag where the crate passes `true`. Pruned harness: the Identity class drops from 104/4000 to 8/4000, the rest being genuine subtract_into/meet_into imprecision. The old harness is unchanged. Co-Authored-By: Claude Opus 5 <noreply@anthropic.com>
Both of these I got wrong on the first pass, and both are the kind of mistake that makes a findings file worse than useless. The `join_map_into` Identity class was never a crate defect. Master changed that status in PR Adam-Vandervorst#142 (276fca0, issue Adam-Vandervorst#139) -- the empty-source-node exit used to `return` the node status on its own, throwing away a value status for a value it had already written -- and both models still described the early return. So master moved and the models lagged, the opposite of what §4 claimed. `fuzz-fixes-v3` scored 0 on this not by fixing anything but by predating the PR. And `3e839e8`, which looks like the obvious candidate to pick for it, is already on master as `1e3b1c3` (PR Adam-Vandervorst#116). The KNOWN notes said "fixed on fuzz-fixes-v3" for both shared classes; only the value-bias one is. Note added: check `git log master -S<string>` before attributing anything to v3. Co-Authored-By: Claude Opus 5 <noreply@anthropic.com>
The seven operations in PRUNED_FINDINGS.md #1 and #2 are one bug in one place. `graft_internal` is the only code that learns "the result is empty", fourteen sites across nine operations hand it a `None`, and its `None` arm reads None => { self.remove_branches(false); } Flipping that `false` is not available: `meet_into` and `subtract_into` are documented to leave dangling paths when their own `prune` is false. So `graft_internal` takes the flag instead of deciding it. The three operations that own a `prune` parameter forward it -- which is how the code already reads, since each follows the call with `if prune { self.prune_path(); }` -- and the rest pass `true`, having no caller intent to honour. Three places do their own removing and need the same change: * the value step of graft/graft_src_at/graft_map. The node step cannot reclaim a location whose value is removed after it, so both halves must prune, and neither alone suffices: a focus with a value and no children is fixed only by the value step, one with children and no value only by the node step. * graft_masked_branches' own removals, and the identical pair in the ZipperWriting default implementation. * graft_masked_branches' bulk arm for masks of three bits or more, which merges through a borrow of the focus node and never reaches graft_internal. It gets a prune_path() after the merge; that is already a no-op unless the focus is a dangling tip, so it costs one node_is_empty check. 4000 random programs, seed 11, through lean/pruned_differential.py: 901 divergences in this class become 0, and agreement rises from 3005 to 3888 of 4000. cargo test --lib stays at 1030 passing. meet_2 is deliberately left alone, and PRUNED_FINDINGS.md says why: pruning it is worth 100 of the 901, but it breaks a regression test that uses meet_2 to *construct* a dangling path in a specific node representation, and it collides with the meet-is-an-intersection rule settled on fuzz-fixes-v3. The defect there is that meet_2 has no prune parameter where meet_into does -- an API decision, not a bug fix. PathMapModel moves with the crate, since it specified the old behaviour: a `tidy` helper (prune_path, which already no-ops unless the focus is a dangling tip) on graft_map, remove_prefix, restrict and restricting. Its stop depth is the zipper's root, not the map root, because prune_path_internal breaks its ascent at root_len -- getting that wrong cost 421 spurious divergences before the harness said so. `takeThenGraft` gains the proviso that there was something to take: take_map(false) at an empty focus leaves a dangling path and returns None, and graft_map of an empty map now reclaims it, so that one state is where the round-trip genuinely stops being one. Co-Authored-By: Claude Opus 5 <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> (cherry picked from commit 3dae731)
`3dae731` ("Make meet/join value bias independent of node layout") from
fuzz-fixes-v3 is the one fix this branch genuinely needed from there. Three
hunks in line_list_node.rs conflicted; the commit documents its own resolutions,
and master is newer in two of them -- `clone_as_dense` for cell nodes, and
`preserve_prune_limit` -- so those keep master's form and take only the new
`list_is_left` argument. The third takes the commit's operand order (the join
is left-biased, so `a` must be on the left) and its COUNTER_IDENT read, since
swapping the operands swaps what the bits refer to. Comments are master's
shorter ones throughout. The merge also had to restore a `}` the conflict
region ate.
Two other candidates turned out not to be fixes to pick:
* `3e839e8` already landed on master as `1e3b1c3` (PR Adam-Vandervorst#116), so cherry-picking
it yields comment churn and duplicate tests.
* the `join_map_into` Identity class was never a crate defect. Master changed
that status in PR Adam-Vandervorst#142 (276fca0, issue Adam-Vandervorst#139) and both models still described
the early `return` it replaced. Fixed in the preceding commit; the class
falls from 104 of 4000 to 8, and fuzz-fixes-v3 scored 0 on it only by
predating the PR.
Then the bigger fuzz. 200000 random programs at seed 7 through the pruned
harness: 193413 agree, 0 unclassified, 0 value bias. What is left is 5901
inputs of `meet_2`, which is deliberately not pruned, and 686 of the
subtract_into/meet_into Identity imprecision this branch does not touch.
`pruned_trace --check`, which needs no oracle, aborts on 16 of 4000 -- and on 0
once meet_2 prunes too, which independently confirms meet_2 is the only source
left. Its checker also had to stop flagging the root of an empty map, which its
own docstring already said to exempt.
The old harness, 30000 programs: 28989 agree, 0 unclassified. Its 5 residual
`remove_prefix` divergences are FINDINGS.md Adam-Vandervorst#7 -- the prune flag's in-node
effect -- made reachable by operations that now prune unconditionally, and only
off the map root. That is also why `tidy` is unconditional: guarding it on "did
the removal report a removal" is the intuitive reading and costs 302 divergences
in 8000 inputs against 5 in 30000 for not guarding, because `node_prune_limit`
reclaims within the node while reporting `false`.
cargo test --lib: 1033 passing.
Co-Authored-By: Claude Opus 5 <noreply@anthropic.com>
The class the 200000-input sweep leaves behind, reduced: a destination
{[] -> 0, [1] -> 0} and a source node {[1] -> 1}. psubtract(0, 1) keeps the
destination's 0, so the two dumps are byte-identical, and the crate still
reports Element where the model reports Identity.
Two layers. u64::psubtract returns Element(*self) where the values differ --
"here is a newly computed value", which is self's own -- rather than
Identity(SELF_IDENT), which ring.rs's own docs name as the way a
non-commutative op reports no change. And the node algebra assembles its
status as it walks without ever asking whether the node it built equals the one
it replaces, where nodeStatus decides by comparing them.
Worth stating what it costs, since the data is correct either way:
subtract_into's Identity arm returns without calling graft_internal, while the
Element arm grafts the new node over the old, so a destination shared with
another trie is copied apart for nothing.
Co-Authored-By: Claude Opus 5 <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> (cherry picked from commit f8a4599)
f8a4599 is the value level of the Identity imprecision: two lines, Element(*self) -> Identity(SELF_IDENT) in the u64 and u16 instances, plus the one Basic.lean line that has to land with them, since u64Ops is a transcription of that instance rather than an independent claim. Both models share Basic.lean, so the one line covers both. 200000 programs at seed 7: the class falls from 686 to 8 -- 6 meet_into and 2 subtract_into, 0.004%. The old harness's status_imprecise bucket empties entirely, 28989 -> 29013 agreeing of 30000, still 0 unclassified in both. cargo test --lib: 1035 passing. What remains is the node level, where the assembled node equals the one it replaces and nothing notices. That is per node type and fuzz-fixes-v3 has a commit for each; none is picked here. Co-Authored-By: Claude Opus 5 <noreply@anthropic.com>
imlvts
marked this pull request as draft
October 2, 2026 16:42
Collaborator
Collaborator
Author
|
I think we should go with your changes, I like the more straightforward model. |
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
2 participants
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.
Built on top of #154.
This has three fixes:
join_map_into's status. both models described an early return that master had already replaced withnode_status.merge(val_status, true, true)