\* The delayed-verdict refinement: full-stack recording, the CT-1910 repair
\* basis, and verdicts delivered over an in-flight channel instead of
\* atomically with admission. The client processes each verdict by an
\* explicit Deliver step (in submission order; in the implementation a
\* rejection's processing point is the covering fan-out frame — the
\* read-repair gate); a rejection's drop-and-cascade runs at that step, so
\* builds in the unprocessed window name decided-dead layers (doomed by the
\* dead-dependency admission rule) and builds after the drop
\* record sparse arrays (03-commit-model.md section 3.5). Brings INV-6
\* (AcceptedVersusDropped) and the CT-1927 parking window into model scope.
\* EXPECTED: all invariants HOLD.
SPECIFICATION Spec
CHECK_DEADLOCK FALSE
CONSTANTS
  Sessions = {"s1", "s2"}
  Paths = {"p1", "p2"}
  MaxTotal = 4
  DepMode = "fullstack"
  BasisMode = "confirmed"
  Values = {"v"}
  DeliveryMode = "channel"
  IdentityMode = "none"
  ViewMode = "replay"
INVARIANT TypeOK
INVARIANT ReadCoherence
INVARIANT CascadeTotality
INVARIANT MonotonicResolution
INVARIANT AcceptedVersusDropped