Sweep every span query, mutating ones included - #134
Merged
Conversation
TestSpanAndArrayQueriesAgree reached 5 of the 20 structures offering a span query. It now reaches all 19 with a pure one, and a second sweep covers the 13 whose span query also changes the structure. The mutating half needed a different shape. Agreeing on every answer is only half of it: two paths can return the same value at every step and leave the structure holding different things, and a filter that answers correctly while holding the wrong thing does not fail at the seam -- it fails later, somewhere else, for no visible reason. Each pair is driven step for step through its own instance and then compared through its payload, the same oracle the equivalence sweep uses. Two mutators answer with the structure itself, so there is no value to compare and the state is the whole check. InvertibleBloomLookupTable needs the fixed-width helper, since it refuses a key of any other length. Both sweeps are checked against rosters derived from the span surface, split by whether the method mutates. A structure that gains a span query fails these until it is covered. Co-Authored-By: Claude Opus 5 <noreply@anthropic.com> Claude-Session: https://claude.ai/code/session_01JH2NRDbhF5bwAsTAP7znb9
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
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.
TestSpanAndArrayQueriesAgreereached 5 of the 20 structures offering a span query. It now reaches all 19 with a pure one, and a second sweep covers the 13 whose span query also changes the structure.Two properties, not one
The mutating half needed a different shape. Agreeing on every answer is only half of it: two paths can return the same value at every step and leave the structure holding different things. A filter that answers correctly while holding the wrong thing doesn't fail at the seam — it fails later, somewhere else, for no visible reason.
So each pair in
TestSpanAndArrayMutatingQueriesAgreeis driven step for step through its own instance, comparing the answer at every key, and then compared through its payload — the same oracle the equivalence sweep uses.Two mutators (
InvertibleBloomLookupTable.Remove,SublimeCountMinSketch.Remove) answer with the structure itself, so there is no value to compare and the state is the whole check. The table also needs the fixed-width helper, since it refuses a key of any other length.Rosters
Both sweeps check against rosters derived from the library's span surface, split by whether the method mutates:
WithPureSpanQueries— 19 structures (Test,Count,TryGetValue)WithMutatingSpanQueries— 13 (TestAndAdd,TestAndRemove,Remove)A structure that gains a span query fails these until it is covered.
Verification
Five probes, each with the build exit checked:
InvertibleBloomLookupTable.Remove's array path applying twice → killed withleft different states. This is the one that matters: a fluent mutator has no answer to compare, so nothing but the state check could see it.BloomFilter.TestAndAdd's array path negating its result → killed withanswered differently for key 0. The mirror case: identical state, wrong answer.InfiniFilterfrom the mutating roster → killed, namedHeavyKeeperfrom the pure roster → killed, namedClean
dotnet build -c Release -warnaserror, exit 0 unpiped. 907 tests passing, up 1.A comment I had to correct
I first annotated
PrivateCountMinSketchandDpswSketchas drawing noise per query, which would mean their two overloads need only agree in distribution. That's wrong, and the tests passing is what exposed it: the noise is drawn once at construction and lives in the counters — which is precisely what stops repeated queries from averaging it away. A query is an ordinary read, and the two overloads must return the identicaldouble. The comment now says that.