\* The identity-commit acceptance (03-commit-model.md section 3.6.1) over
\* the shipped shape: full-stack recording, the CT-1910 repair basis, and
\* atomic delivery. Two values let a commit re-write what a foreign commit
\* already stored; such a commit refused for staleness is proved an
\* identity against the stored content and the content at its reader's
\* basis, then accepted with every write elided. Coherence is checked in
\* its content form, since an elided layer is observed by its own session
\* as a contributor while durable history holds the foreign write that
\* carried the same value (see ReadCoherence's comment in the module).
\* EXPECTED: all invariants HOLD.
SPECIFICATION Spec
CHECK_DEADLOCK FALSE
CONSTANTS
  Sessions = {"s1", "s2"}
  Paths = {"p1", "p2"}
  Values = {"a", "b"}
  MaxTotal = 4
  DepMode = "fullstack"
  BasisMode = "confirmed"
  DeliveryMode = "atomic"
  IdentityMode = "elide"
  ViewMode = "replay"
INVARIANT TypeOK
INVARIANT ContentCoherence
INVARIANT ElidedUnchanged
INVARIANT CascadeTotality
INVARIANT MonotonicResolution