M3: the implication test, and the row closes #14

Merged
dev merged 2 commits from m3-partial-implication into main 2026-08-11 06:56:41 +00:00
3 changed files with 68 additions and 6 deletions
Showing only changes of commit 35c1e6537c - Show all commits

33
PLAN.md
View File

@@ -467,7 +467,7 @@ answers, and the trade is only acceptable because the lie is removed first.
| M1 | **Cursors + wire polish** | getMore / killCursors / batchSize; server-side cursor state with idle timeout; sessions plumbing (lsid accepted) as drivers send it; hello advertisement updates; **`moreToCome` on requests** (see the bug below); command-monitoring assertions in the spec runner | crud spec suite green; e2e green | | M1 | **Cursors + wire polish** | getMore / killCursors / batchSize; server-side cursor state with idle timeout; sessions plumbing (lsid accepted) as drivers send it; hello advertisement updates; **`moreToCome` on requests** (see the bug below); command-monitoring assertions in the spec runner | crud spec suite green; e2e green |
| M2 | **The `aggregate` command surface** | `$out` and `$merge` (7 of the 13 failures), and refusing every pipeline construct the engine does not implement instead of answering `0` (amendment A6). The other 6 failures are blocked on M2.5, M4 and M8 — see `docs/M2_DESIGN_REVIEW.md` §7 | `aggregate-*.json`: 0 fail among the 7 reachable cases | | M2 | **The `aggregate` command surface** | `$out` and `$merge` (7 of the 13 failures), and refusing every pipeline construct the engine does not implement instead of answering `0` (amendment A6). The other 6 failures are blocked on M2.5, M4 and M8 — see `docs/M2_DESIGN_REVIEW.md` §7 | `aggregate-*.json`: 0 fail among the 7 reachable cases |
| M2.5 | **The aggregation engine** | expression evaluator, per-stage document iterator, the accumulators, `$unwind`; `$lookup`/`$facet` explicitly out of the first cut (amendment A6) | a purpose-built stage corpus, every expectation measured against mongod | | M2.5 | **The aggregation engine** | expression evaluator, per-stage document iterator, the accumulators, `$unwind`; `$lookup`/`$facet` explicitly out of the first cut (amendment A6) | a purpose-built stage corpus, every expectation measured against mongod |
| M3 | **Update operators + index types** | `distinct` (**done**); positional paths refused rather than destructive (**done**); `$`/`$[]`/`$[<ident>]` + `arrayFilters` (**done**); $setOnInsert, $addToSet, $mul, $min/$max, $pop, $pullAll, $currentDate + `$push`'s modifiers (**done**); pipeline-style updates (**done**); partial indexes (**done**); hashed indexes (**done**); then the implication test that lets a partial index serve a read | `tests/spec/positional/` 0 fail (51), `tests/spec/operators/` 0 fail (125) and `tests/spec/indexes/` 0 fail (42), all recorded from mongod — **green**; the named gate could not see any of the three, see below; remaining crud coverage; e2e3/e2e4 green | | M3 | **Update operators + index types** | `distinct` (**done**); positional paths refused rather than destructive (**done**); `$`/`$[]`/`$[<ident>]` + `arrayFilters` (**done**); $setOnInsert, $addToSet, $mul, $min/$max, $pop, $pullAll, $currentDate + `$push`'s modifiers (**done**); pipeline-style updates (**done**); partial indexes (**done**); hashed indexes (**done**); the implication test that lets a partial index serve a read (**done**) — **the row is closed** | `tests/spec/positional/` 0 fail (51), `tests/spec/operators/` 0 fail (125) and `tests/spec/indexes/` 0 fail (48), all recorded from mongod — **green**; the named gate could not see any of the three, see below; remaining crud coverage; e2e3/e2e4 green |
| M4 | **Sessions + transactions** | logical sessions, snapshot isolation on the mmap engine, write concern at commit | sessions + transactions spec suites green | | M4 | **Sessions + transactions** | logical sessions, snapshot isolation on the mmap engine, write concern at commit | sessions + transactions spec suites green |
| M5 | **Change streams** | change feed + resume tokens (likely log-seq based), getMore integration | change-streams spec suite green | | M5 | **Change streams** | change feed + resume tokens (likely log-seq based), getMore integration | change-streams spec suite green |
| M6 | **Admin/ops commands** | dbStats, collStats, serverStatus, ping, buildInfo, listDatabases filters, dropDatabase durability (log it) | mongosh UX smoke; e2e green | | M6 | **Admin/ops commands** | dbStats, collStats, serverStatus, ping, buildInfo, listDatabases filters, dropDatabase durability (log it) | mongosh UX smoke; e2e green |
@@ -1151,6 +1151,7 @@ has to be its own commit with its own re-recorded scorecard.
to read from a partial index**: it holds a subset, so answering a query from to read from a partial index**: it holds a subset, so answering a query from
it is only correct when the query implies the filter, and that implication it is only correct when the query implies the filter, and that implication
test is the last step of the row. Too few documents is worse than no index. test is the last step of the row. Too few documents is worse than no index.
(That step has since landed; see the implication entry below.)
**Hashed indexes landed**; `hashed.json` is 18/18, so `tests/spec/indexes/` **Hashed indexes landed**; `hashed.json` is 18/18, so `tests/spec/indexes/`
is 42/42. A hashed component stores a tag byte and a 64-bit hash of the is 42/42. A hashed component stores a tag byte and a 64-bit hash of the
@@ -1181,7 +1182,8 @@ has to be its own commit with its own re-recorded scorecard.
cannot tell apart from a plain subdocument — so the check walks the path cannot tell apart from a plain subdocument — so the check walks the path
rather than counting what it yields. rather than counting what it yields.
**`tests/spec/indexes/` is the gate**, recorded red at 3/39 across 42 cases. **`tests/spec/indexes/` is the gate**, recorded red at 3/39 across 42 cases
and since grown to 48 by the implication work.
A case there is a *sequence* -- create, insert, read, list -- because an A case there is a *sequence* -- create, insert, read, list -- because an
index outlives a `deleteMany` and every case is about which indexes exist. index outlives a `deleteMany` and every case is about which indexes exist.
Recording it corrected two of the review's own guesses: `$in` in a partial Recording it corrected two of the review's own guesses: `$in` in a partial
@@ -1195,6 +1197,33 @@ has to be its own commit with its own re-recorded scorecard.
exists the safe rule is to maintain the index and never read from it. Too exists the safe rule is to maintain the index and never read from it. Too
few documents is the one failure worse than no index at all. few documents is the one failure worse than no index at all.
- **The implication test closes M3's row, and the two gates see opposite
halves of it.** A partial index may answer a query that cannot match a
document its filter left out. Two routes: the query pins a value at the
filter's path and the *real matcher* is run against a stand-in document
holding it (sound because every operator the partial grammar admits is
existential, so more values at a path can only satisfy it more easily), or
the query's bounds are at least as tight as the filter's. An array value and
a null value are refused rather than approximated — `{a: [1, 2]}` matches
`{a: [[1, 2], 3]}`, whose values at `a` do not include 1 or 2, and
`{a: null}` matches a document with no `a` at all, which has no values there
rather than more of them.
Soundness is judged against **this server's** matcher, not mongod's:
`query.matches_bytes` decides the index's contents in `build_entries` and
re-filters every candidate. Where this server's comparison differs from
mongod's — the type-bracketing item below — both halves are wrong together,
which is a matching bug and not a lost document.
Measured with two mutations, and worth keeping because the answer is not
symmetric. Forcing the test to `true` takes `partial.json` to 23/7 and every
failure reads "expected N, got N-1" — the exact shape of the bug. Forcing it
to `false`, which is the behaviour it replaced, leaves the corpus **30/30**:
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 can see the feature work at all. A read path with no
`explain` has no third option.
- **What the index corpus caught that was not about indexes: `{a: null}` did - **What the index corpus caught that was not about indexes: `{a: null}` did
not match a missing field.** `find({a: null})` has to match a document with not match a missing field.** `find({a: null})` has to match a document with
no `a` as well as one holding an explicit null. This server matched only the no `a` as well as one holding an explicit null. This server matched only the

View File

@@ -154,7 +154,8 @@ list used for its own format change and it holds here for the same reason.
## Outcome ## Outcome
Steps 14 landed in that order. `tests/spec/indexes/` is 42/42. All five steps landed in that order, which closes M3's row.
`tests/spec/indexes/` is 48/48.
Three things this review got wrong, kept here because the point of writing it Three things this review got wrong, kept here because the point of writing it
before the code was to find out which parts would not survive contact: before the code was to find out which parts would not survive contact:
@@ -175,8 +176,22 @@ And one thing the corpus found that this review had no reason to look for:
`find({a: null})` did not match a document with no `a`, index or no index. See `find({a: null})` did not match a document with no `a`, index or no index. See
PLAN §6. PLAN §6.
Step 5, the implication test, is still open. Until it exists a partial index And one thing §4 asserted without saying how: the implication test itself. It
is maintained, enforces `unique`, and is never read from. turned out not to need a comparison of its own. Every operator
`check_partial_filter` admits is *existential* — "some value at this path
satisfies it" — so when the query pins a value, running the real matcher
against a stand-in document holding it settles `$eq`, `$in`, `$type`,
`$exists` and the bounds together. Only two shapes escape that argument (an
array value, whose elements a real document need not have; and null, which
also matches a document with no such field), and only ranges need reasoning
of their own.
The unnoticed half was the gates. A corpus recorded from mongod can see an
implication test that says *yes* too readily — the answer loses documents —
but not one that never says yes at all, because no client can observe which
index a read used. Measured: forcing the test true takes `partial.json` to
23/7; forcing it false leaves it 30/30. The unit test on `plan()` is the only
thing that sees the feature work.
## 6. Not covered ## 6. Not covered

View File

@@ -50,7 +50,7 @@ halves have since been driven green:
``` ```
hashed.json 18 pass 0 fail 0 skip hashed.json 18 pass 0 fail 0 skip
partial.json 24 pass 0 fail 0 skip partial.json 30 pass 0 fail 0 skip
``` ```
The three that passed at the start were the reads a partial index does not The three that passed at the start were the reads a partial index does not
@@ -63,6 +63,24 @@ to match a document with no `a`, and this server matched only an explicit
null — with or without an index. No other test in the repository asks, and null — with or without an index. No other test in the repository asks, and
the pinned crud+aggregate scorecard did not move when it was fixed. the pinned crud+aggregate scorecard did not move when it was fixed.
## What this corpus cannot see
Six of `partial.json`'s cases exist for the implication test — the rule that
lets a partial index answer a read — and it is worth being exact about what
they guard, because it is only half of it.
A partial index holds a subset, so reading from one the query does not imply
returns **too few** documents, and that is an answer a result comparison
catches. It was measured: forcing the implication test to always say yes takes
this file to 23 pass / 7 fail, every failure reading "expected N, got N-1".
The other direction is invisible here. Forcing it to always say *no* — the
behaviour before the test existed, where a partial index was maintained and
never read — leaves this file at **30 pass / 0 fail**. No client can observe
which index a read used, and this server has no `explain`. So the corpus
guards soundness and a unit test on `plan()` is the only thing that sees the
feature work at all.
## What recording it settled ## What recording it settled
Two of the review's own guesses were wrong, which is why it was recorded Two of the review's own guesses were wrong, which is why it was recorded