\* Three friends, messages live two ticks, at most three held on the device.
CONSTANTS
  Peers = {a, b, c}
  TTL = 2
  MaxMsgs = 3
  None = None

INIT Init
NEXT Next

INVARIANTS
  TypeOK
  FocusNotInSight
  SomeoneToWalkToward
  Ephemeral
  TapOnlyForDM

CHECK_DEADLOCK FALSE