Test Genesis State Machine with quickcheck-dynamic

[geo2a]

Fixes #1149

"no changelog", as the changes only affect the ouroboros-consensus-diffusion:consensus-test package.

In this PR, we refactor the Test.Consensus.GSM modules, which contain the tests for the Genesis State Machine component, to use a different state machine testing framework. Specifically, we are switching the tests from quickcheck-state-machine to quickcheck-dynamic. The main motivation for the switch is being able to run the Genesis State Machine in IOSim in order to benefit from IOSims ability to manipulate the passage of time and this speed-up the tests.

While the current GSM tests do run in IOSim, this is only possible due to vendoring a copy of quickcheck-state-machine that allows using IOSim, which we would like to avoid long-term.

Specifically, this PR:

• adds QD-based tests
• groups definition used in both QSM and QD tests

Below, I describe some aspects of the switch that I consider worth highlighting, hopefully making the review more manageable.

Differences from quickcheck-state-machine tests

While I've tried to replicate the existing quickcheck-state-machine-based tests as closely as possible, there are some unavoidable differences between the test suites stemming from how the quickcheck-dynamic library is structured and implemented.

Different distributions of command sequences

While the user can specify the logic to generate individual commands, both quickcheck-dynamic and quickcheck-state-machine have internal hard-coded logic to generate sequences of commands:

quickcheck-dynamic	quickcheck-state-machine
generateActionsWithOptions	generateCommandsState

Here are the partial tests reports, which show that QSM produces more uniform distribution of commands:

quickcheck-dynamic                     |             quickcheck-state-machine
                                       |
GSM (at most 1 peer):  OK (0.19s)      |             GSM (at most 1 peer):  OK (0.42s)
  +++ OK, passed 1000 tests.           |               +++ OK, passed 1000 tests.
                                       |
  Actions (24732 in total):            |               Commands (7336 in total):
  33.232% +TimePasses                  |               13.63% NewCandidate
  14.257% +ReadMarker                  |               13.63% StartIdling
  14.152% +ReadGsmState                |               13.63% TimePasses
  13.404% +ModifyCandidate             |               13.56% ReadMarker
  12.187% +StartIdling                 |               13.54% ReadGsmState
   6.740% +NewCandidate                |               13.41% ModifyCandidate
   3.324% +Disconnect                  |               10.17% Disconnect
   2.705% +ExtendSelection             |                8.42% ExtendSelection
                                       |
  Notables (2312 in total):            |               Notables (3347 in total):
  17.82% FellBehindN                   |               20.50% FellBehindN
  17.08% PreSyncingToSyncingN          |               19.30% PreSyncingToSyncingN
  16.09% <none>                        |               13.92% TooOldN
  11.98% TooOldN                       |               13.65% CaughtUpN
  10.86% CaughtUpN                     |                9.68% FlickerN
   9.34% SyncingToPreSyncingN          |                9.47% SyncingToPreSyncingN
   9.26% BigDurN                       |                9.20% BigDurN
   7.53% FlickerN                      |                4.27% <none>
   0.04% NotThrashingN                 |

Similarly, for 5 peers:

`quickcheck-dynamic`                   |             `quickcheck-state-machine`
                                       |
GSM (at most 5 peers): OK (0.25s)      |             GSM (at most 5 peers): OK (0.53s)
  +++ OK, passed 1000 tests.           |               +++ OK, passed 1000 tests.
                                       |
  Actions (26337 in total):            |               Commands (7314 in total):
  29.157% +TimePasses                  |               13.67% NewCandidate
  16.190% +StartIdling                 |               13.67% TimePasses
  15.643% +NewCandidate                |               13.65% StartIdling
  11.098% +ReadGsmState                |               13.29% ReadGsmState
  11.072% +ReadMarker                  |               13.28% ReadMarker
  10.024% +ModifyCandidate             |               13.04% ModifyCandidate
   4.291% +ExtendSelection             |               10.39% ExtendSelection
   2.525% +Disconnect                  |                9.01% Disconnect
                                       |
  Notables (2102 in total):            |               Notables (2788 in total):
  27.26% PreSyncingToSyncingN          |               31.17% PreSyncingToSyncingN
  21.93% SyncingToPreSyncingN          |               24.82% SyncingToPreSyncingN
  16.60% FellBehindN                   |               21.34% FellBehindN
  14.65% <none>                        |                6.85% BigDurN
   5.99% TooOldN                       |                6.71% TooOldN
   5.95% BigDurN                       |                6.56% CaughtUpN
   5.80% CaughtUpN                     |                1.94% FlickerN
   1.81% FlickerN                      |                0.61% <none>

QD also generates significantly more commands than QSM, probably due to longer defaults length for command sequences.

The glue code of quickcheck-dymamic is essentially pure and thus allows to use IOSim

The type of quickcheck-state-machine's runCommands function constraints the underlying monad to IO:

runCommands :: (MonadMask m, MonadIO m)
            => ...
            -> PropertyM m (History cmd resp, model Concrete, Reason)

This is needed, because quickcheck-state-machine uses TChans internally to orchestrate the interaction between the model and the system-under-test. This in particular makes it impossible to run the system-under-test in IOSim and motivated us to vendor a copy of QSM with the types adapted to permit IOSim.

In quickcheck-dymamic, commands are called actions, and run using the
runActions function, whose type gives the user much more freedom:

runActions
  :: forall state m e
   . ( StateModel state
     , RunModel state m
     , e ~ Error state m
     , forall a. IsPerformResult e a
     )
  => Actions state
  -> PropertyM m (Annotated state, Env)

class (forall a. Show (Action state a), Monad m) => RunModel state m where
  ...

I.e. the user needs to instantiate the RunModel class, where the library only requires m to be a Monad. The implementation of runActions itself is essentially pure and only uses the facilities of Test.Quickcheck.Monadic to invoke the underlying monadic code of the system-under-test.

Slightly different test setup routine

While quickcheck-state-machine represents state machines as records of functions, and thus gives a lot of flexibility to the user in terms pasteurisation, quickcheck-dynamic is not as flexible, as it uses type classes.

Specifically, I was having a hard time to emulate the pattern of parameterising the state machine with a Context that exists in the current QSM test (see here, for example). The Context data type contains parameters that are generated with quickcheck and are fixed over the execution of one property test, i.e. they are static from the state machine's point of view.

quickcheck-dynamic does not provide a way to supply static information to the state machine out of the box, thus not allowing to configure the initial state according to some external static parameter and presenting us with an instance of the classic configuration problem. I've tried several ways to solve this particular instance, but the turned out to be using reflection as suggested by @nfrisby. Specifically, I've taken inspiration from this blogpost by John Wiegley, where he uses reflection to provide configuration to quickcheck generators --- this is almost exactly what we want here!

The essence of the solution is to constrain the StateModel instance with an constraint provided by reflection. This way, we get to use have the reflected parameters in the initialState method:

instance Reflection.Reifies params StaticParams => QD.StateModel (Model params) where
  ...

  initialState = initModel params
    where params = Reflection.reflect (Proxy @params)

initModel :: StaticParams -> Model params

We would then create a value of StaticParams in the property definition:

prop_sequential_iosim :: Maybe UpstreamPeer -> LedgerStateJudgement -> QC.Fun (Set.Set UpstreamPeer) Bool -> QC.Property
prop_sequential_iosim pUpstreamPeerBound pInitialJudgement (QC.Fun _ pIsHaaSatisfied) =
    Reflection.reify (StaticParams{ pUpstreamPeerBound
                                  , pInitialJudgement
                                  , pIsHaaSatisfied
                                  }) $ \(Proxy :: Proxy params) ->
     -- NOTE: the actions have to be generated with an explicit call, as
     -- 'generator' relies on reflection for access to the parameters
     QC.forAll QC.arbitrary $ \actions ->
       runIOSimProp $ prop_sequential_iosim1 @_ @params actions

The only tricky thing here is to explicitly invoke the generator for actions, so that the reified value of StaticParams is in scope.

Next steps

Once the reviewers are happy with the changes, we should:

• remove the tests based on quickcheck-state-machine
• remove our copy of quickcheck-state-machien that allows IOSim
• restructure the GSM tests modules accordingly, i.e. move the QD module one level up and rename it to GSMTests

Independently:

• we need to make a Hackage release of quickcheck-dynamic, as this PR relies on the version from master which is not yet released
• once the release is uploaded, we will be able to remove the s-r-p

[geo2a]

This module needs to be moved, as quickcheck-dynamic also has Test.QuickCheck.Extras.

[amesgen]

This looks great!

---

Thanks a lot for the thorough attention to labelling! One further observation: we set the minimum command length to 20 for QSM; for QD, I get this distribution:

        # of actions (1000 in total):
        41.5% "0 - 9"
        19.4% "10 - 19"
        12.2% "20 - 29"
         7.6% "30 - 39"
         6.0% "40 - 49"
         3.1% "50 - 59"
         3.0% "100 - 199"
         2.9% "60 - 69"
         2.2% "70 - 79"
         1.1% "80 - 89"
         0.8% "90 - 99"
         0.2% "200 - 299"

This still seems completely fine, especially as the chosen value of 20 for QSM was ad-hoc either way.

---

The PR description can be updated in two aspects:

• The way of using reflection changed as of Test Genesis State Machine with quickcheck-dynamic #1413 (comment).
• The new release of quickcheck-dynamic seems to have happened already.

---

Apart from that, I think we can now proceed as described in the PR description and remove the vendored QSM code and the QSM GSM test.

[jasagredo]

I think the failing reference must now point to https://developers.cardano.org/docs/get-started/cardano-node/installing-cardano-node

[geo2a]

I've fixed the link, thanks @jasagredo!

[geo2a]

Blocked on update of quickcheck-lockstep to use quickcheck-dynamic 4.0.0, see this Slack thread.