\* The reconnect before client-declared holdings: a resumed session's
\* catch-up is diffed against the SERVER's memory of what it delivered.
\* With one lost push (the OW61 client-absorb class) or a wiped replica,
\* the lost document is remembered as delivered and never re-sent.
\* EXPECTED: ReconnectConverges VIOLATED — kept as the regression witness
\* for the schema-doc quarantine residual (verification-coverage.md OW61).
SPECIFICATION Spec
CHECK_DEADLOCK FALSE
CONSTANTS
  Docs = {"d1", "d2"}
  MaxWrites = 3
  MaxLoss = 1
  AllowReset = TRUE
  Mode = "memory"
INVARIANT TypeOK
INVARIANT ReconnectConverges