Implement liveness and safety property tests.

- 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.

.stack-to-nix.cache

@@ -22,3 +22,4 @@ https://github.com/input-output-hk/cardano-prelude 3ac22a2fda11ca7131a011a9ea48f
 https://github.com/input-output-hk/cardano-ledger-specs c006b101b699b7b54a96d077fdbad07005b8da77 byron/semantics/executable-spec 1m2xs2z9bq83k65l2hx41zbj1akyl83cdlxhdxssd8nbmb723qar small-steps small-steps.nix
 https://github.com/input-output-hk/cardano-ledger-specs c006b101b699b7b54a96d077fdbad07005b8da77 byron/ledger/executable-spec 1m2xs2z9bq83k65l2hx41zbj1akyl83cdlxhdxssd8nbmb723qar cs-ledger cs-ledger.nix
 https://github.com/input-output-hk/cardano-base 0fcb3a306e96ce36fca75d62792c55ab1de871ea slotting 0fbcf3iim4fh8m647ilw02ybbxiqna3zpny0w7rlqjgd4skfqvjr cardano-slotting cardano-slotting.nix
+https://github.com/nomeata/haskell-successors 6f9f60eb3232b83cbffdc46301054c85983cf207 . 03jbs0730nyjhi01wqgmn6848pklvnzja7dv4nlhs1s6zb43gznx successors successors.nix

executable-spec/decentralized-updates.cabal

@@ -33,9 +33,10 @@ library
                      , Cardano.Ledger.Update.Ideation
                      , Cardano.Ledger.Update.Approval
                      , Cardano.Ledger.Update.Activation
-                     -- Proposals state
+                     -- State
                      , Cardano.Ledger.Update.ProposalState
                      , Cardano.Ledger.Update.ProposalsState
+                     , Cardano.Ledger.Update.Activation.State
                      -- Environment constraints
                      , Cardano.Ledger.Update.Env.TracksSlotTime
                      , Cardano.Ledger.Update.Env.HasStakeDistribution
@@ -58,6 +59,7 @@ library
                      -- Needed for 'Cardano.Ledger.Assert' only. We might want
                      -- to put this module on our test section.
                      , monad-validate
+                     , Unique
                      -- Needed for 'Cardano.Ledger.Debug' only.
                      , mtl
   default-language:    Haskell2010
@@ -85,15 +87,26 @@ test-suite ledger-rules-test
                      , Test.Cardano.Ledger.Update.UnitTests.Approval
                      , Test.Cardano.Ledger.Update.UnitTests.Activation
                      , Test.Cardano.Ledger.Update.UnitTests.Common
+                     -- Property tests
+                     , Test.Cardano.Ledger.Update.Properties
+                     , Test.Cardano.Ledger.Update.Properties.UpdateSUT
+                     , Test.Cardano.Ledger.Update.Properties.SimpleScenario
+                     , Test.Cardano.Ledger.Update.Properties.Liveness
+                     , Test.Cardano.Ledger.Update.Properties.StateChangeValidity
+                     , Test.Cardano.Ledger.Update.Events
+                     , Test.Cardano.Ledger.Update.Properties.Examples
                      -- Test case specification
                      , Test.Cardano.Ledger.UpdateSpec
                      , Test.Cardano.Ledger.Update.TestCase
                      , Test.Cardano.Ledger.Update.Interface
                      -- Unit testing
                      , Util.TestCase
                      -- Property testing
-                     , Properties
-                     , SUTTest
+                     , SystemUnderTest
+                     , Trace
+                     , Trace.Scenario
+                     , Trace.Generation
+                     , Trace.PropertyTesting
   default-language:    Haskell2010
   build-depends:       base
                      , containers
@@ -104,6 +117,7 @@ test-suite ledger-rules-test
                      , pretty-simple
                      , text
                      , random
+                     , successors
                      -- Cardano specific imports
                      , cardano-slotting
                      , decentralized-updates
@@ -117,6 +131,7 @@ test-suite ledger-rules-test
                        --
                        -- The 4 megabytes stack bound and 150 megabytes heap bound were
                        -- determined ad-hoc.
+                       --
                        "-with-rtsopts=-K1m -M150m"
                        -threaded
                        -rtsopts

executable-spec/src/Cardano/Ledger/Assert.hs

@@ -1,55 +1,78 @@
 {-# LANGUAGE CPP #-}
 {-# LANGUAGE OverloadedStrings #-}
+{-# LANGUAGE FlexibleContexts #-}
 
 module Cardano.Ledger.Assert
   ( assert
+  , assertAndReturn
+  , runAssertion
+  , Assertion
+  , pass
+  , failBecause
   -- * Comparison assertions
   , (<!)
   , (<=!)
   , (==!)
+  , (/=!)
   , (>!)
   , (>=!)
   -- ** LHS is maybe
   , (?<!)
   , (?<=!)
   , (?==!)
+  , (?/=!)
   , (?>!)
   , (?>=!)
   -- ** RHS is maybe
   , (<?!)
   , (<=?!)
   , (==?!)
+  , (/=?!)
   , (>?!)
   , (>=?!)
   -- ** Both sides are maybe
   , (?<?!)
   , (?<=?!)
   , (?==?!)
+  , (?/=?!)
   , (?>?!)
   , (?>=?!)
+    -- ** Logical operators
+  , (||!)
   -- * Comparison with maybe values
   , (?<)
   , (?<=)
   , (?==)
+  , (?/=)
   , (?>)
   , (?>=)
   -- * Assertions on containers
   , holdsForAllElementsIn
   , doesNotContain
   , doesNotContainKey
   , doesNotContainMaybeKey
+  -- ** Assertions on lists
+  , allUnique
+  -- * Quantifications
+  , forall
+  , exists
   -- * Show utilities
   , cShow
   , orElseShow
+#if PRETTY_PRINT
+  , prettyShow
+#endif
+  , showErrors
   )
 where
 
 import           GHC.Stack (HasCallStack)
-
-import           Control.Monad.Validate (Validate, dispute, runValidate)
+import           Control.Monad.Validate (Validate, dispute, runValidate, mapErrors)
 import           Data.Map.Strict (Map)
 import qualified Data.Map.Strict as  Map
 import           Data.Foldable (traverse_)
+import           Data.List.Unique (repeated)
+import           Data.List (intercalate)
 
 #if PRETTY_PRINT
 import qualified Text.Pretty.Simple as Pretty
@@ -60,14 +83,24 @@ import qualified Data.Text.Lazy as Text.Lazy
 assert :: HasCallStack => Assertion -> a -> a
 assert assertion a =
 #if ENABLE_ASSERTIONS
-  case runValidate assertion of
-    Left msg -> error $ unlines
+  case runAssertion assertion of
+    Just msg -> error $ unlines
                       $ "Failed assertions" : fmap Text.Lazy.unpack msg
-    Right _  -> a
+    Nothing -> a
 #else
   a
 #endif
 
+
+-- | Check the assertion. If it succeeds return 'Nothing', if it fails return
+-- the error.
+runAssertion :: Assertion -> Maybe [Text.Lazy.Text]
+runAssertion = either Just (const Nothing) . runValidate
+
+assertAndReturn
+  :: HasCallStack => (a -> Assertion) -> a -> a
+assertAndReturn p x = assert (p x) x
+
 failBecause :: Text.Lazy.Text -> Assertion
 failBecause = dispute . pure
 
@@ -76,72 +109,92 @@ pass = pure ()
 
 type Assertion = Validate [Text.Lazy.Text] ()
 
-(<!), (<=!), (==!), (>!), (>=!) :: (Show a, Ord a) => a -> a -> Assertion
-(<!)  = assertOrder LessThan
-(<=!) = assertOrder LessEqualThan
-(==!) = assertOrder Equal
-(>!)  = assertOrder GreaterThan
-(>=!) = assertOrder GreaterEqualThan
+(==!), (/=!) :: (Show a, Eq a) => a -> a -> Assertion
+(<!), (<=!), (>!), (>=!) :: (Show a, Ord a) => a -> a -> Assertion
+(<!)  = assertRelation (<)  " is not less than "
+(<=!) = assertRelation (<=) " is not less or equal than "
+(==!) = assertRelation (==) " is not equal to "
+(/=!) = assertRelation (/=) " is equal to "
+(>!)  = assertRelation (>)  " is not greater than"
+(>=!) = assertRelation (>=) " is not greater or equal than"
+infix 4 <!, <=!, ==!, /=!, >!, >=!
 
-(?<!), (?<=!), (?==!), (?>!), (?>=!)
+(?==!), (?/=!)
+  :: (Show a, Eq a) => Maybe a -> a -> Assertion
+(?<!), (?<=!), (?>!), (?>=!)
   :: (Show a, Ord a) => Maybe a -> a -> Assertion
 ma ?<! b  = maybe pass (<!  b) ma
 ma ?<=! b = maybe pass (<=! b) ma
 ma ?==! b = maybe pass (==! b) ma
+ma ?/=! b = maybe pass (/=! b) ma
 ma ?>! b  = maybe pass (>!  b) ma
 ma ?>=! b = maybe pass (>=!  b) ma
+infix 4 ?<!, ?<=!, ?==!, ?/=!, ?>!, ?>=!
 
-(<?!), (<=?!), (==?!), (>?!), (>=?!)
+(==?!), (/=?!)
+  :: (Show a, Eq a) => a -> Maybe a -> Assertion
+(<?!), (<=?!), (>?!), (>=?!)
   :: (Show a, Ord a) => a -> Maybe a -> Assertion
 a <?!  mb = maybe pass (a <! ) mb
 a <=?! mb = maybe pass (a <=!) mb
 a ==?! mb = maybe pass (a ==!) mb
+a /=?! mb = maybe pass (a /=!) mb
 a >?!  mb = maybe pass (a >! ) mb
 a >=?! mb = maybe pass (a >=!) mb
+infix 4 <?!, <=?!, ==?!, /=?!, >?!, >=?!
 
-(?<?!), (?<=?!), (?==?!), (?>?!), (?>=?!)
+(?==?!), (?/=?!)
+  :: (Show a, Eq a) => Maybe a -> Maybe a -> Assertion
+(?<?!), (?<=?!), (?>?!), (?>=?!)
   :: (Show a, Ord a) => Maybe a -> Maybe a -> Assertion
 ma ?<?!  mb = maybe pass (ma ?<! ) mb
 ma ?<=?! mb = maybe pass (ma ?<=!) mb
 ma ?==?! mb = maybe pass (ma ?==!) mb
+ma ?/=?! mb = maybe pass (ma ?/=!) mb
 ma ?>?!  mb = maybe pass (ma ?>! ) mb
 ma ?>=?! mb = maybe pass (ma ?>=!) mb
+infix 4 ?<?!, ?<=?!, ?==?!, ?/=?!, ?>?!, ?>=?!
 
-(?<), (?<=), (?==), (?>), (?>=)
+(?==), (?/=)
+  :: Eq a => Maybe a -> a -> Bool
+(?<), (?<=), (?>), (?>=)
   :: Ord a => Maybe a -> a -> Bool
 ma ?< b  = maybe True (<  b) ma
 ma ?<= b = maybe True (<= b) ma
 ma ?== b = maybe True (== b) ma
+ma ?/= b = maybe True (/= b) ma
 ma ?> b  = maybe True (>  b) ma
 ma ?>= b = maybe True (>  b) ma
+infix 4 ?<, ?<=, ?==, ?/=, ?>, ?>=
+
+assertRelation :: (Show a) => (a -> a -> Bool) -> Text.Lazy.Text -> a -> a -> Assertion
+assertRelation rel relationDoesNotHoldText x y
+  | x `rel` y = pass
+  | otherwise = failBecause $  cShow x
+                            <> relationDoesNotHoldText
+                            <> cShow y
+
+--------------------------------------------------------------------------------
+-- Logical operators
+--------------------------------------------------------------------------------
 
-data CompareBy
-  = LessThan
-  | LessEqualThan
-  | Equal
-  | GreaterThan
-  | GreaterEqualThan
-
-assertOrder :: (Show a, Ord a) => CompareBy -> a -> a -> Assertion
-assertOrder ordering a b
-  | compareBy ordering a b = pass
-  | otherwise              = failBecause $  cShow a
-                                         <> orderRelationDoesNotHold ordering
-                                         <> cShow b
-
-compareBy :: Ord a => CompareBy -> a -> a -> Bool
-compareBy LessThan         = (<)
-compareBy LessEqualThan    = (<=)
-compareBy Equal            = (==)
-compareBy GreaterThan      = (>)
-compareBy GreaterEqualThan = (>)
-
-orderRelationDoesNotHold :: CompareBy -> Text.Lazy.Text
-orderRelationDoesNotHold LessThan         = " is not less than "
-orderRelationDoesNotHold LessEqualThan    = " is not less or equal than "
-orderRelationDoesNotHold Equal            = " is not equal to "
-orderRelationDoesNotHold GreaterThan      = " is not greater than"
-orderRelationDoesNotHold GreaterEqualThan = " is not greater or equal than"
+(||!) :: Assertion -> Assertion -> Assertion
+a0 ||! a1 =
+  case runValidate a0 of
+    Right _    -> pass
+    Left errs0 ->
+      case runValidate a1 of
+        Right _    -> pass
+        Left errs1 ->
+          -- TODO: we might want to use a data structure like a tree to give
+          -- some structure to the errors.
+          dispute $ "No term satisfies the assertion: "
+                  : fmap (Text.Lazy.cons '\t') (errs0 ++ errs1)
+infixr 2 ||!
+
+--------------------------------------------------------------------------------
+-- Custom show functions
+--------------------------------------------------------------------------------
 
 -- | Customized show. It can show pretty formatted data structures, or not
 -- depending on the PRETTY_PRINT_ASSERTIONS compile time flag.
@@ -153,10 +206,23 @@ cShow =
   Text.Lazy.pack . show
 #endif
 
+#if PRETTY_PRINT
+prettyShow :: Show a => a -> String
+prettyShow = Text.Lazy.unpack . Pretty.pShow
+#endif
+
+-- | Convert the errors to a string. Each error will be separated by a newline.
+showErrors :: [Text.Lazy.Text] -> String
+showErrors = intercalate "\n" . fmap Text.Lazy.unpack
+
 orElseShow :: Bool -> Text.Lazy.Text -> Assertion
 orElseShow False reason = failBecause reason
 orElseShow True  _      = pass
 
+--------------------------------------------------------------------------------
+-- Operations on collections
+--------------------------------------------------------------------------------
+
 doesNotContain
   :: (Eq a, Show a, Foldable f) => f a -> a -> Assertion
 doesNotContain xs a
@@ -178,7 +244,43 @@ holdsForAllElementsIn
 holdsForAllElementsIn p fa =
   traverse_ (p `holdsFor`) fa
 
+allUnique :: (Show a, Ord a) => [a] -> Assertion
+allUnique xs =
+  case repeated xs of
+    [] -> pass
+    ys -> failBecause $  "The list should contain unique elements,"
+                      <> " however these elements are repeated: "
+                      <> cShow ys
+
 holdsFor :: Show a => (a -> Bool) -> a -> Assertion
 holdsFor p a
   | p a       = pass
   | otherwise = failBecause $ "Predicate does not hold for " <> cShow a
+
+--------------------------------------------------------------------------------
+-- Quantifications
+--------------------------------------------------------------------------------
+
+forall :: (Foldable t, Show a) => t a -> (a -> Assertion) -> Assertion
+forall domain term = traverse_ checkTerm domain
+  where
+    checkTerm x
+      = mapErrors ((("forall: element does not satisfy the assertion: \n" <> cShow x) :)
+                  . fmap (Text.Lazy.cons '\t')
+                  )
+      $ term x
+
+data Any e = Found | Errors [e]
+
+exists :: (Foldable t) => t a -> (a -> Assertion) -> Assertion
+exists domain term = do
+  case foldl elementSatisfies (Errors []) domain of
+    Found     -> pass
+    Errors xs -> dispute $ "exists: No element satisfies the given assertion \n":
+                           (reverse $ fmap (Text.Lazy.cons '\t') xs)
+  where
+    elementSatisfies Found       _ = Found
+    elementSatisfies (Errors es) x =
+      case runValidate (term x) of
+        Right _   -> Found
+        Left errs -> Errors (errs ++ es) -- TODO: use a structure with constant concatenation to accumulate errors.