CONSTANTS
  Shards = {h, d}
  Ids = {a, b}
  N = 2

SPECIFICATION Spec
INVARIANT TypeOK
INVARIANT NoPartialShard
INVARIANT RejectedBatchWritesNothing
INVARIANT AuditOnlyCommitted
INVARIANT RetryConverges
CHECK_DEADLOCK FALSE