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>
Collaborator
|
The question is, do we want A. a model that is agnostic about dangling paths? Or B. one that has a strong opinion that dangling paths should not exist? Both start by defining correctness only as a set of values at paths. But they diverge on the details of what they model. It appears this PR implements B. |
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.
The model includes a proof for
PathMap<V>being a lattice and commutativity forPathMap<()>.The proofs are in
lean/PrunedModel/Lattice.lean,join_assoc,meet_assoc,join_idem, etc. for concrete types, section below, starting withunit_join_assoc.