Define safety and liveness tests for the update system prototype

[dnadales]

• Change radically the test generation strategy:

  • Generate actions regardless of the SUT state. This greatly simplifies generation.
  • A trace can be elaborated from a test setup. This greatly simplifies shrinking.

• Add tests for important liveness properties:

  • SIP's are expired
  • SIP's are rejected
  • SIP's get no-quorum
  • SIP's are approved
  • Implementations are expired
  • Implementations are rejected
  • Implementations get no-quorum
  • Implementations are activated
  • Implementations are queued
  • Updates are discarded due to being expired
  • Updates are discarded due to being unsupported
  • Updates are discarded due to being obsoleted

• Make voting period duration configurable when creating a dummy update spec.

• Add forall and exists combinators to the assertions module. These the quantifiers return the element that did not satisfy the assertion on failure.

• Make assertions Testable instances (via a newtype wrapper)

• Add an assertion to endorse which makes the following precondition explicit:

  • the number of slots per-epoch must be greater than twice the number of slots after which events are stable on the chain. This ensures that the cutoff period for endorsements lies within the epoch in which the endorsement took place.

  I detected this problem due to our property tests.

• Add fixity declarations to the comparison operators of the Assert module.

• Fix error in activation phase that caused proposals to get lost and not be marked as "discarded".

• Create an Activation.State module to facilitate reasoning with operations on the activation state.

• Use ceiling instead of round when computing thresholds. This fixes a problem where if the total stake was 1 and r_a 0 then the threshold will be 0.

• Keep a history of approved implementations that moved away from the approval phase. When a proposal is revealed, we check that no proposal with the same id was approved already. This allows us to refer unambiguously to each proposal in the specification.

• Remove Ord constraints on equality assertions and simplify the implementation of equality and inequality assertions.

• Removed the Obsoleted state. Obsoleted proposal are now simply marked as unsupported.

• Ensure that a proposal can be applied only to the same id it declares to supersede.

• Define safety tests in terms of checking the event sequences and the state and trace fragments associated to those events.

• Fix error where votes could be cast after a verdict was reached.

• Fix error where proposals that could not be applied remained in the queue.

      -- If the proposal was queued it must be because it cannot __yet__ follow
      -- the current version, or there is a candidate proposal with higher or
      -- the same priority.
      ( getCurrentProtocolVersion (firstState fragment')
           <! supersedesVersion (getProtocol updateSpec)
        ||!
        exists (filter ((/= _id (getProtocol updateSpec)) . _id)
                 $ Update.candidateProtocols (firstState fragment')
               )
             (\protocol ->
                version protocol <=! version (getProtocol updateSpec)))

That test failed because there was a candidate in the queue that superseded the same version as the current version, but it superseded a different id as the current version.

• Fix error in the implementation of can follow.

 cannotFollowCurrentVersion       =
      protocolSupersedesVersion < State.getCurrentProtocolVersion st
      ||
      (protocolSupersedesVersion == State.getCurrentProtocolVersion st
      && supersedesId protocol   /= State.getCurrentProtocolId st
      )

We added the supersedesId protocol /= State.getCurrentProtocolId st check.

• Make UIState and UIError monomorphic.