test: Parquet merge pipeline verification suite

[g-talbot]

Summary

End-to-end verification stack for the Parquet merge pipeline. Closes the
loop from formal spec → exhaustive model → production runtime checks →
trace-conformance proof, so a divergence between production and the
verified model surfaces as a test failure or a Datadog metric, not a
silent corruption.

Verification pyramid (single source of truth)

TLA+ specs (docs/internals/specs/tla/)
        │ mirrors
Shared invariants (quickwit-dst/src/invariants/merge_pipeline.rs)  ← single Rust module
        │ used by                          │ called by
Stateright models                Production check_invariant! sites
        │                                  │
        └────── Trace conformance test ────┘

The Stateright model and production code evaluate the same Rust
predicate functions on the same state struct. Drift impossible by
construction.

What landed

TLA+ — MergePipelineShutdown.tla
Extended from the original orderly-shutdown spec to cover crash and
restart at every transition. CompleteMerge split into UploadMergeOutput

• PublishMergeAndFeedback so a crash between upload and metastore
  replace is reachable (orphan_outputs failure mode). Multi-lifetime
  support (Restart can fire after graceful shutdown, modeling fresh
  process invocations). New invariants:

• RowsConserved (MP-4): sum of rows in published splits = total ingested rows
• LeakIsObjectStoreOnly (MP-10): orphans never become durable data
• BoundedWriteAmp (MP-5), MP1_LevelHomogeneity, NoOrphanInPlanner (MP-8), NoOrphanWhenConnected (MP-9)
• Action property RestartReSeedsAllImmature (MP-11): every Restart re-seeds correctly
• Liveness NoPersistentOrphan: orphans always eventually clear

Two TLC configs: primary (multi-lifetime, ~16K states, 1s) and chains
(deep merge chain, ~218K states, 12s). 11 invariants + 3 temporal
properties verified.

Shared invariants — quickwit-dst/src/invariants/merge_pipeline.rs
New MergePipelineState struct mirrors the TLA+ VARIABLES block
literally; used directly by the Stateright model (no parallel
definition). 9 pure-function predicates (MP-1, MP-4..MP-11) with unit
tests for passing and failing paths.

Stateright — quickwit-dst/src/models/merge_pipeline.rs
Refactored to use the shared state and predicates. Mirrors the TLA+
multi-phase merge and multi-lifetime semantics. Three configs (small,
multi_lifetime, deep_chains) all pass.

Production runtime checks — quickwit-indexing/.../metrics_pipeline/
Eight new check_invariant! call sites, all forwarding to the existing
DogStatsD recorder (pomsky.invariant.{checked,violated}{invariant=MP-X}):

• ParquetMergeExecutor — MP-1 (level homogeneity), MP-2 (≥2 inputs), MP-3 (scope), MP-4 (input rows == output rows)
• ParquetMergePlanner::new — MP-11 (post-restart re-seed completeness, the formal "fetch_immature_splits is correct" claim)

Trace conformance — parquet_merge_pipeline_trace_conformance_test.rs
Production emits a MergePipelineEvent stream at every modeled
transition (Restart, PlanMerge, UploadMergeOutput,
PublishMergeAndFeedback, DisconnectMergePlanner,
RunFinalizeAndQuit, etc.). The test replays the captured events
through the same predicates Stateright verifies. Two scenarios pass:

• Normal path: 4 splits → cascade of merges → mature output
• Crash mid-cascade: publish failure forces respawn; production re-seeds
  cleanly across the crash boundary; rows conserved end-to-end

A divergence between production and the verified model would surface
here as a predicate failure with the offending event in the panic
message.

Original verification suite (still here)
Property test, sketch integration test, crash/restart integration test,
multi-round merge integration test — unchanged.

What's deferred

• CS-3 (no compaction before threshold): the TLA+ model has it, but
  production ParquetMergePolicyConfig doesn't expose
  compaction_start_time yet. TODO in
  parquet_merge_planner::record_splits_if_necessary so the check lands
  alongside the feature.
• MP-5..MP-10 lifted to runtime: currently checked only by Stateright +
  trace test; would need a periodic background task to materialize the
  full MergePipelineState for runtime evaluation. Not added because
  the trace-conformance proof already covers them.

Coverage table (23 invariants in registry)

• 13/23 runtime-checked in production via check_invariant!
• 6/23 (MP-5..MP-10) verified by Stateright + trace conformance
• 4/23 (SS-3, SS-4, DM-4, DM-5) by construction (unfalsifiable runtime check)

Sesh-mode rule

Added a strong rule to .claude/skills/sesh-mode/SKILL.md: when a
verification check fails, never silently weaken or remove the invariant.
Almost always either (a) the implementation has a real bug, or (b) the
property is over-strong — and the failing trace is revealing the
weaker safety property the design does guarantee.

Test plan

• TLC: MergePipelineShutdown.cfg passes (~16K states, 1s); _chains.cfg passes (~218K states, 12s); 11 invariants + 3 temporal properties
• cargo nextest run -p quickwit-dst --features model-checking — 49 tests pass + 1 ignored deep_chains passes when run
• cargo nextest run -p quickwit-indexing --features metrics metrics_pipeline — 54 tests pass (52 prior + 2 new trace conformance)
• Clippy clean (-Dwarnings)
• Nightly fmt clean
• cargo doc --no-deps -p quickwit-indexing --features metrics clean
• cargo machete clean

🤖 Generated with Claude Code