Summary

TLA+ spec + jstest for SERVER-121988: between view-resolution kickbacks (especially across getMore boundaries), a drop+recreate flips the view definition and the second-pass query silently returns no matches. Production correctness for sharded analytical workloads. Prior PR declined; spec-first re-attempt.

Files

• src/mongo/tla_plus/Catalog/OWNERS.yml → 10gen/server-query-execution
• src/mongo/tla_plus/Catalog/ViewResolutionGetMore/ViewResolutionGetMore.tla (281 lines) — 3 actors (mongos resolver / catalog mutator / consumer getMore), 6 actions (OpenCursor, GetMore, CloseCursor, DropView, RecreateView, SwapView), AllowViewMutationMidCommand toggle, invariants SingleViewDefinitionPerCommand + NoSilentEmptyBatchAfterOk.
• MCViewResolutionGetMore.tla / .cfg (green) + _Bug.cfg
• OWNERS.yml + README.md (254 words)
• jstests/aggregation/lookup_view_drop_recreate_getMore.js (293 lines) — 8 cases ($lookup × {drop, drop+recreate same backing, swap to backing_b, view→collection swap}

  + same 4 for $graphLookup). Batch size pinned at 5, 200 source docs guarantee multiple getMore boundaries.

TLC verdicts

• Green (AllowViewMutationMidCommand=FALSE): 125 distinct states, no error.
• Bug (=TRUE): Invariant SingleViewDefinitionPerCommand is violated at depth 5 — OpenCursor → DropView → GetMore returns batchEmpty.