M3: the implication test, and the row closes #14
Reference in New Issue
Block a user
Delete Branch "m3-partial-implication"
Deleting a branch is permanent. Although the deleted branch may continue to exist for a short time before it actually gets removed, it CANNOT be undone in most cases. Continue?
Step 5 of
docs/M3_INDEX_TYPES_DESIGN_REVIEW.md's order, and the lastitem in M3's row. A partial index was maintained and enforced
unique,and every read scanned -- correct, but the speedup the option exists for
was never earned.
tests/spec/indexes/goes 42/42 to 48/48.The test
A partial index may answer a query that cannot match a document its
filter left out. One-sided by construction: a
falsecosts a scan, atruehas to be right, because too few documents is the one failureworse than having no index at all.
Route one -- the query pins a value. Run the real matcher against a
stand-in document holding that value at the path, rather than
reimplementing eight operators against a comparison that would then have
two definitions. Sound because every operator
check_partial_filteradmits is existential -- "some value at this path satisfies it" -- so a
document with more values at the path satisfies it at least as easily,
and every document the query matches has the pinned value among its
values there. Settles
$eq,$in,$type,$existsand the boundstogether.
Two shapes break that argument and are refused rather than approximated,
each with its own row in the test table:
{a: [1, 2]}matches{a: [[1, 2], 3]}, whosevalues at
ado not include 1 or 2 -- only one level is expanded, sothe real document's value set is not a superset of the stand-in's.
{a: null}also matches a document with noa,which has no values at the path rather than more of them. The
stand-in alone would report
{a: {$exists: true}}as implied, so anempty document is tested too and both have to agree.
Route two -- bounds. The only route needing neither side to name a
document:
{a: {$gt: 5}}implies{a: {$gt: 0}}. Inclusivity is whereit is decided --
$gte: 0admits the endpoint$gt: 0excludes.$oron the filter's side is implied by one implied branch: sufficient,not necessary, since a query can imply a disjunction without implying a
disjunct.
Soundness is against this server's matcher, not mongod's
Both halves of the question run the same code:
query.matches_bytesdecides the index's contents in
build_entriesand re-filters everycandidate the plan yields. Where this server's comparison differs from
mongod's -- PLAN §6 records that the comparison operators are not
type-bracketed -- both halves are wrong together, which is a matching bug
and not a lost document.
What each gate can and cannot see
Measured with two mutations, and the answer is not symmetric:
query_implies_filterforced topartial.jsontruefalse(the behaviour this replaces)No client can observe that an index was used, only that an answer went
missing, and this server has no
explain. So the corpus guards soundnessand the unit test on
plan()is the only thing that sees the featurework at all. Both numbers are in PLAN §6 and the corpus README so the
next change here knows which gate is load-bearing for which direction.
Corpus
Six cases added, each pairing a query that implies the filter with one
that does not and touches the same field: a query leaving the filter's
field out, an
$instraddling the filter, a query for null against an$existsfilter, equalities inside and outside a range filter, a sort apartial index could serve, and a unique partial index read.
partial.json24 -> 30 cases.Verification
tests/spec/indexes/48/0,operators/125/0,positional/51/0,aggregate/70/0crash-fuzzgreenFour mutations were run against the new unit table as well -- the whole
test forced true, the lower-bound comparison dropped, the null guard
dropped, the array guard dropped -- and each reddens it.
M3's row is closed. Next milestone is M4, sessions and transactions.
Step 5, the last of `docs/M3_INDEX_TYPES_DESIGN_REVIEW.md`'s order and the last item in M3's row. A partial index was maintained and enforced `unique`, and every read scanned -- correct, but the speedup the option exists for was never earned. The test is one-sided by construction: a `false` costs a scan, a `true` has to be right, because returning too few documents is the one failure worse than having no index at all. Two routes, and a filter conjunct is implied if either answers yes: **Route one, the query pins a value.** Run the *real matcher* against a stand-in document holding that value at the path, rather than reimplementing eight operators against a comparison that would then have two definitions. Sound because every operator `check_partial_filter` admits is existential -- "some value at this path satisfies it" -- so a document with more values at the path satisfies it at least as easily, and every document the query matches has the pinned value among its values there. Covers `$eq`, `$in`, `$type`, `$exists` and the bounds in one stroke. Two shapes break that argument and are refused rather than approximated, and both have a row in the test table: - an **array** value. `{a: [1, 2]}` matches `{a: [[1, 2], 3]}`, whose values at `a` do not include 1 or 2 -- only one level is expanded, so the real document's value set is not a superset of the stand-in's. - a **null** value. `{a: null}` also matches a document with no `a`, which has no values at the path rather than more of them. The stand-in alone would report `{a: {$exists: true}}` as implied, so an empty document is tested too and both have to agree. This is the rule the previous commit's null fix made necessary and possible in the same breath. **Route two, bounds.** The only route needing neither side to name a document: `{a: {$gt: 5}}` implies `{a: {$gt: 0}}`. Inclusivity is where it is decided -- `$gte: 0` admits the endpoint that `$gt: 0` excludes. Soundness is judged against *this server's* matcher, not mongod's. Both halves of the question run the same code: `query.matches_bytes` decides the index's contents in `build_entries` and re-filters every candidate the plan yields. Where this server's comparison differs from mongod's (PLAN §6: the comparison operators are not type-bracketed) both halves are wrong together, which is a matching bug and not a lost document. `$or` on the filter's side is implied by one implied branch: sufficient, not necessary, since a query can imply a disjunction without implying a disjunct. **What each gate can and cannot see, measured with two mutations.** With `query_implies_filter` forced to `true`, `partial.json` goes 23/7 and every failure reads "expected N, got N-1" -- the exact shape of the bug. With it forced to `false` -- the behaviour this commit replaces -- the corpus is 30/30, because no client can observe *that* an index was used, only that an answer went missing. So the corpus guards soundness and the unit test on `plan()` is the only thing that sees the feature work at all; both are needed and the commit says which does which. Six corpus cases added, each pairing a query that implies the filter with one that does not and touches the same field: a query leaving the filter's field out, an `$in` straddling the filter, a query for null against an `$exists` filter, equalities inside and outside a range filter, a sort a partial index could serve, and a unique partial index read. `partial.json` 24 -> 30 cases, `tests/spec/indexes/` 42 -> 48. Verified: 257/257 unit tests in ReleaseFast and ReleaseSafe, 88/88 fuzz, all four corpora 0 fail, pinned scorecard unchanged at 228/63/196, the full e2e matrix and crash-fuzz green.