\* The read-conditioned substitution under the identity exemption: a layer
\* whose read the foreign write made stale, and whose write the exemption
\* elides, is observed as a contributor while durable history holds the
\* foreign write of the same value, which the content form of INV-1 states
\* (ContentCoherence). Single-path writes, the ChannelIdentity bound.
\* 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 = "channel"
  IdentityMode = "elide"
  ViewMode = "intendedRead"
WriteChoices <- SingletonWrites
INVARIANT TypeOK
INVARIANT ContentCoherence
INVARIANT ElidedUnchanged
INVARIANT CascadeTotality
INVARIANT MonotonicResolution
INVARIANT AcceptedVersusDropped