SPECIFICATION Spec
INVARIANTS
  TypeOK
  MainWrittenOnlyByOwner
  ForkWrittenOnlyByItsUser
  NoLostUpdate
  PushIsFastForward
  RefsMatchHistory
CHECK_DEADLOCK FALSE