{-# LANGUAGE DuplicateRecordFields #-}
{-# OPTIONS_GHC -Wno-unused-do-bind #-}

module Hydra.HeadLogicSnapshotSpec where

import Hydra.Prelude hiding (label)
import Test.Hydra.Prelude

import Data.List qualified as List
import Data.Map.Strict qualified as Map
import Hydra.HeadLogic (
  CoordinatedHeadState (..),
  Effect (..),
  HeadState (..),
  OpenState (OpenState),
  SeenSnapshot (..),
  coordinatedHeadState,
  isLeader,
  update,
 )
import Hydra.HeadLogicSpec (getState, hasEffect, hasEffectSatisfying, hasNoEffectSatisfying, inOpenState, inOpenState', receiveMessage, receiveMessageFrom, runHeadLogic, step)
import Hydra.Ledger.Simple (SimpleTx (..), aValidTx, simpleLedger, utxoRef)
import Hydra.Network.Message (Message (..))
import Hydra.Options (defaultContestationPeriod)
import Hydra.Tx.Crypto (sign)
import Hydra.Tx.Environment (Environment (..))
import Hydra.Tx.HeadParameters (HeadParameters (..))
import Hydra.Tx.IsTx (txId)
import Hydra.Tx.Party (deriveParty)
import Hydra.Tx.Snapshot (ConfirmedSnapshot (..), Snapshot (..), getSnapshot)
import Test.Hydra.Tx.Fixture (
  alice,
  aliceSk,
  bob,
  bobSk,
  carol,
  carolSk,
  deriveOnChainId,
  testHeadId,
 )
import Test.QuickCheck (Property, counterexample, forAll, oneof, (==>))
import Test.QuickCheck.Monadic (monadicST, pick)

spec :: Spec
spec :: Spec
spec = do
  Spec -> Spec
forall a. SpecWith a -> SpecWith a
parallel (Spec -> Spec) -> Spec -> Spec
forall a b. (a -> b) -> a -> b
$ do
    let threeParties :: [Party]
threeParties = [Party
alice, Party
bob, Party
carol]
        u0 :: Set SimpleTxOut
u0 = Set SimpleTxOut
forall a. Monoid a => a
mempty
        envFor :: SigningKey HydraKey -> Environment
envFor SigningKey HydraKey
signingKey =
          let party :: Party
party = SigningKey HydraKey -> Party
deriveParty SigningKey HydraKey
signingKey
              otherParties :: [Party]
otherParties = Party -> [Party] -> [Party]
forall a. Eq a => a -> [a] -> [a]
List.delete Party
party [Party]
threeParties
           in Environment
                { Party
party :: Party
$sel:party:Environment :: Party
party
                , SigningKey HydraKey
signingKey :: SigningKey HydraKey
$sel:signingKey:Environment :: SigningKey HydraKey
signingKey
                , [Party]
otherParties :: [Party]
$sel:otherParties:Environment :: [Party]
otherParties
                , $sel:contestationPeriod:Environment :: ContestationPeriod
contestationPeriod = ContestationPeriod
defaultContestationPeriod
                , $sel:participants:Environment :: [OnChainId]
participants = Party -> OnChainId
deriveOnChainId (Party -> OnChainId) -> [Party] -> [OnChainId]
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> [Party]
threeParties
                }

    let coordinatedHeadState :: CoordinatedHeadState SimpleTx
coordinatedHeadState =
          CoordinatedHeadState
            { $sel:localUTxO:CoordinatedHeadState :: UTxOType SimpleTx
localUTxO = Set SimpleTxOut
UTxOType SimpleTx
u0
            , $sel:allTxs:CoordinatedHeadState :: Map (TxIdType SimpleTx) SimpleTx
allTxs = Map SimpleId SimpleTx
Map (TxIdType SimpleTx) SimpleTx
forall a. Monoid a => a
mempty
            , $sel:localTxs:CoordinatedHeadState :: [SimpleTx]
localTxs = [SimpleTx]
forall a. Monoid a => a
mempty
            , $sel:confirmedSnapshot:CoordinatedHeadState :: ConfirmedSnapshot SimpleTx
confirmedSnapshot = HeadId -> UTxOType SimpleTx -> ConfirmedSnapshot SimpleTx
forall tx. HeadId -> UTxOType tx -> ConfirmedSnapshot tx
InitialSnapshot HeadId
testHeadId Set SimpleTxOut
UTxOType SimpleTx
u0
            , $sel:seenSnapshot:CoordinatedHeadState :: SeenSnapshot SimpleTx
seenSnapshot = SeenSnapshot SimpleTx
forall tx. SeenSnapshot tx
NoSeenSnapshot
            , $sel:pendingDeposits:CoordinatedHeadState :: Map (TxIdType SimpleTx) (UTxOType SimpleTx)
pendingDeposits = Map SimpleId (Set SimpleTxOut)
Map (TxIdType SimpleTx) (UTxOType SimpleTx)
forall a. Monoid a => a
mempty
            , $sel:decommitTx:CoordinatedHeadState :: Maybe SimpleTx
decommitTx = Maybe SimpleTx
forall a. Maybe a
Nothing
            , $sel:version:CoordinatedHeadState :: SnapshotVersion
version = SnapshotVersion
0
            }
    let sendReqSn :: Effect tx -> Bool
sendReqSn = \case
          NetworkEffect ReqSn{} -> Bool
True
          Effect tx
_ -> Bool
False
    let snapshot1 :: Snapshot SimpleTx
snapshot1 = HeadId
-> SnapshotVersion
-> SnapshotNumber
-> [SimpleTx]
-> UTxOType SimpleTx
-> Maybe (UTxOType SimpleTx)
-> Maybe (UTxOType SimpleTx)
-> Snapshot SimpleTx
forall tx.
HeadId
-> SnapshotVersion
-> SnapshotNumber
-> [tx]
-> UTxOType tx
-> Maybe (UTxOType tx)
-> Maybe (UTxOType tx)
-> Snapshot tx
Snapshot HeadId
testHeadId SnapshotVersion
0 SnapshotNumber
1 [] UTxOType SimpleTx
forall a. Monoid a => a
mempty Maybe (UTxOType SimpleTx)
forall a. Maybe a
Nothing Maybe (UTxOType SimpleTx)
forall a. Maybe a
Nothing

    let ackFrom :: SigningKey HydraKey -> Party -> Input SimpleTx
ackFrom SigningKey HydraKey
sk Party
vk = Party -> Message SimpleTx -> Input SimpleTx
forall tx. Party -> Message tx -> Input tx
receiveMessageFrom Party
vk (Message SimpleTx -> Input SimpleTx)
-> Message SimpleTx -> Input SimpleTx
forall a b. (a -> b) -> a -> b
$ Signature (Snapshot SimpleTx) -> SnapshotNumber -> Message SimpleTx
forall tx. Signature (Snapshot tx) -> SnapshotNumber -> Message tx
AckSn (SigningKey HydraKey
-> Snapshot SimpleTx -> Signature (Snapshot SimpleTx)
forall a.
SignableRepresentation a =>
SigningKey HydraKey -> a -> Signature a
sign SigningKey HydraKey
sk Snapshot SimpleTx
snapshot1) SnapshotNumber
1

    String -> Spec -> Spec
forall a. HasCallStack => String -> SpecWith a -> SpecWith a
describe String
"Generic Snapshot property" (Spec -> Spec) -> Spec -> Spec
forall a b. (a -> b) -> a -> b
$ do
      String -> Property -> Spec
forall prop.
(HasCallStack, Testable prop) =>
String -> prop -> Spec
prop String
"there's always a leader for every snapshot number" Property
prop_thereIsAlwaysALeader

    String -> Spec -> Spec
forall a. HasCallStack => String -> SpecWith a -> SpecWith a
describe String
"On ReqTx" (Spec -> Spec) -> Spec -> Spec
forall a b. (a -> b) -> a -> b
$ do
      String -> (ConfirmedSnapshot SimpleTx -> Property) -> Spec
forall prop.
(HasCallStack, Testable prop) =>
String -> prop -> Spec
prop String
"always emit ReqSn given head has 1 member" ConfirmedSnapshot SimpleTx -> Property
prop_singleMemberHeadAlwaysSnapshotOnReqTx

      String -> IO () -> SpecWith (Arg (IO ()))
forall a.
(HasCallStack, Example a) =>
String -> a -> SpecWith (Arg a)
it String
"sends ReqSn when leader and no snapshot in flight" (IO () -> SpecWith (Arg (IO ())))
-> IO () -> SpecWith (Arg (IO ()))
forall a b. (a -> b) -> a -> b
$ do
        let tx :: SimpleTx
tx = SimpleId -> SimpleTx
aValidTx SimpleId
1
            outcome :: Outcome SimpleTx
outcome = Environment
-> Ledger SimpleTx
-> HeadState SimpleTx
-> Input SimpleTx
-> Outcome SimpleTx
forall tx.
IsChainState tx =>
Environment -> Ledger tx -> HeadState tx -> Input tx -> Outcome tx
update (SigningKey HydraKey -> Environment
envFor SigningKey HydraKey
aliceSk) Ledger SimpleTx
simpleLedger ([Party] -> CoordinatedHeadState SimpleTx -> HeadState SimpleTx
inOpenState' [Party
alice, Party
bob] CoordinatedHeadState SimpleTx
coordinatedHeadState) (Input SimpleTx -> Outcome SimpleTx)
-> Input SimpleTx -> Outcome SimpleTx
forall a b. (a -> b) -> a -> b
$ Message SimpleTx -> Input SimpleTx
forall tx. Message tx -> Input tx
receiveMessage (Message SimpleTx -> Input SimpleTx)
-> Message SimpleTx -> Input SimpleTx
forall a b. (a -> b) -> a -> b
$ SimpleTx -> Message SimpleTx
forall tx. tx -> Message tx
ReqTx SimpleTx
tx

        Outcome SimpleTx
outcome
          Outcome SimpleTx -> Effect SimpleTx -> IO ()
forall tx.
(HasCallStack, IsChainState tx) =>
Outcome tx -> Effect tx -> IO ()
`hasEffect` Message SimpleTx -> Effect SimpleTx
forall tx. Message tx -> Effect tx
NetworkEffect (SnapshotVersion
-> SnapshotNumber
-> [TxIdType SimpleTx]
-> Maybe SimpleTx
-> Maybe (UTxOType SimpleTx)
-> Message SimpleTx
forall tx.
SnapshotVersion
-> SnapshotNumber
-> [TxIdType tx]
-> Maybe tx
-> Maybe (UTxOType tx)
-> Message tx
ReqSn SnapshotVersion
0 SnapshotNumber
1 [SimpleTx -> TxIdType SimpleTx
forall tx. IsTx tx => tx -> TxIdType tx
txId SimpleTx
tx] Maybe SimpleTx
forall a. Maybe a
Nothing Maybe (Set SimpleTxOut)
Maybe (UTxOType SimpleTx)
forall a. Maybe a
Nothing)

      String -> IO () -> SpecWith (Arg (IO ()))
forall a.
(HasCallStack, Example a) =>
String -> a -> SpecWith (Arg a)
it String
"does NOT send ReqSn when we are NOT the leader even if no snapshot in flight" (IO () -> SpecWith (Arg (IO ())))
-> IO () -> SpecWith (Arg (IO ()))
forall a b. (a -> b) -> a -> b
$ do
        let tx :: SimpleTx
tx = SimpleId -> SimpleTx
aValidTx SimpleId
1
            st :: CoordinatedHeadState SimpleTx
st = CoordinatedHeadState SimpleTx
coordinatedHeadState{localTxs = [tx]}
            outcome :: Outcome SimpleTx
outcome = Environment
-> Ledger SimpleTx
-> HeadState SimpleTx
-> Input SimpleTx
-> Outcome SimpleTx
forall tx.
IsChainState tx =>
Environment -> Ledger tx -> HeadState tx -> Input tx -> Outcome tx
update (SigningKey HydraKey -> Environment
envFor SigningKey HydraKey
bobSk) Ledger SimpleTx
simpleLedger ([Party] -> CoordinatedHeadState SimpleTx -> HeadState SimpleTx
inOpenState' [Party
alice, Party
bob] CoordinatedHeadState SimpleTx
st) (Input SimpleTx -> Outcome SimpleTx)
-> Input SimpleTx -> Outcome SimpleTx
forall a b. (a -> b) -> a -> b
$ Party -> Message SimpleTx -> Input SimpleTx
forall tx. Party -> Message tx -> Input tx
receiveMessageFrom Party
bob (Message SimpleTx -> Input SimpleTx)
-> Message SimpleTx -> Input SimpleTx
forall a b. (a -> b) -> a -> b
$ SimpleTx -> Message SimpleTx
forall tx. tx -> Message tx
ReqTx SimpleTx
tx

        Outcome SimpleTx
outcome Outcome SimpleTx -> (Effect SimpleTx -> Bool) -> IO ()
forall tx.
(HasCallStack, IsChainState tx) =>
Outcome tx -> (Effect tx -> Bool) -> IO ()
`hasNoEffectSatisfying` Effect SimpleTx -> Bool
forall {tx}. Effect tx -> Bool
sendReqSn

      String -> IO () -> SpecWith (Arg (IO ()))
forall a.
(HasCallStack, Example a) =>
String -> a -> SpecWith (Arg a)
it String
"does NOT send ReqSn when we are the leader but snapshot in flight" (IO () -> SpecWith (Arg (IO ())))
-> IO () -> SpecWith (Arg (IO ()))
forall a b. (a -> b) -> a -> b
$ do
        let tx :: SimpleTx
tx = SimpleId -> SimpleTx
aValidTx SimpleId
1
            sn1 :: Snapshot SimpleTx
sn1 = HeadId
-> SnapshotVersion
-> SnapshotNumber
-> [SimpleTx]
-> UTxOType SimpleTx
-> Maybe (UTxOType SimpleTx)
-> Maybe (UTxOType SimpleTx)
-> Snapshot SimpleTx
forall tx.
HeadId
-> SnapshotVersion
-> SnapshotNumber
-> [tx]
-> UTxOType tx
-> Maybe (UTxOType tx)
-> Maybe (UTxOType tx)
-> Snapshot tx
Snapshot HeadId
testHeadId SnapshotVersion
1 SnapshotNumber
1 [] Set SimpleTxOut
UTxOType SimpleTx
u0 Maybe (Set SimpleTxOut)
Maybe (UTxOType SimpleTx)
forall a. Maybe a
Nothing Maybe (Set SimpleTxOut)
Maybe (UTxOType SimpleTx)
forall a. Maybe a
Nothing :: Snapshot SimpleTx
            st :: CoordinatedHeadState SimpleTx
st = CoordinatedHeadState SimpleTx
coordinatedHeadState{seenSnapshot = SeenSnapshot sn1 mempty}
            outcome :: Outcome SimpleTx
outcome = Environment
-> Ledger SimpleTx
-> HeadState SimpleTx
-> Input SimpleTx
-> Outcome SimpleTx
forall tx.
IsChainState tx =>
Environment -> Ledger tx -> HeadState tx -> Input tx -> Outcome tx
update (SigningKey HydraKey -> Environment
envFor SigningKey HydraKey
aliceSk) Ledger SimpleTx
simpleLedger ([Party] -> CoordinatedHeadState SimpleTx -> HeadState SimpleTx
inOpenState' [Party
alice, Party
bob] CoordinatedHeadState SimpleTx
st) (Input SimpleTx -> Outcome SimpleTx)
-> Input SimpleTx -> Outcome SimpleTx
forall a b. (a -> b) -> a -> b
$ Message SimpleTx -> Input SimpleTx
forall tx. Message tx -> Input tx
receiveMessage (Message SimpleTx -> Input SimpleTx)
-> Message SimpleTx -> Input SimpleTx
forall a b. (a -> b) -> a -> b
$ SimpleTx -> Message SimpleTx
forall tx. tx -> Message tx
ReqTx SimpleTx
tx

        Outcome SimpleTx
outcome Outcome SimpleTx -> (Effect SimpleTx -> Bool) -> IO ()
forall tx.
(HasCallStack, IsChainState tx) =>
Outcome tx -> (Effect tx -> Bool) -> IO ()
`hasNoEffectSatisfying` Effect SimpleTx -> Bool
forall {tx}. Effect tx -> Bool
sendReqSn

      String -> IO () -> SpecWith (Arg (IO ()))
forall a.
(HasCallStack, Example a) =>
String -> a -> SpecWith (Arg a)
it String
"updates seenSnapshot state when sending ReqSn" (IO () -> SpecWith (Arg (IO ())))
-> IO () -> SpecWith (Arg (IO ()))
forall a b. (a -> b) -> a -> b
$ do
        let tx :: SimpleTx
tx = SimpleId -> SimpleTx
aValidTx SimpleId
1
            st :: HeadState SimpleTx
st = [Party] -> CoordinatedHeadState SimpleTx -> HeadState SimpleTx
inOpenState' [Party]
threeParties CoordinatedHeadState SimpleTx
coordinatedHeadState
            st' :: HeadState SimpleTx
st' =
              [Party] -> CoordinatedHeadState SimpleTx -> HeadState SimpleTx
inOpenState' [Party]
threeParties (CoordinatedHeadState SimpleTx -> HeadState SimpleTx)
-> CoordinatedHeadState SimpleTx -> HeadState SimpleTx
forall a b. (a -> b) -> a -> b
$
                CoordinatedHeadState SimpleTx
coordinatedHeadState
                  { localTxs = [tx]
                  , allTxs = Map.singleton (txId tx) tx
                  , localUTxO = u0 <> utxoRef (txId tx)
                  , seenSnapshot = RequestedSnapshot{lastSeen = 0, requested = 1}
                  }

        HeadState SimpleTx
actualState <- Environment
-> Ledger SimpleTx
-> HeadState SimpleTx
-> StateT (StepState SimpleTx) IO (HeadState SimpleTx)
-> IO (HeadState SimpleTx)
forall (m :: * -> *) tx a.
Monad m =>
Environment
-> Ledger tx -> HeadState tx -> StateT (StepState tx) m a -> m a
runHeadLogic (SigningKey HydraKey -> Environment
envFor SigningKey HydraKey
aliceSk) Ledger SimpleTx
simpleLedger HeadState SimpleTx
st (StateT (StepState SimpleTx) IO (HeadState SimpleTx)
 -> IO (HeadState SimpleTx))
-> StateT (StepState SimpleTx) IO (HeadState SimpleTx)
-> IO (HeadState SimpleTx)
forall a b. (a -> b) -> a -> b
$ do
          Input SimpleTx -> StateT (StepState SimpleTx) IO (Outcome SimpleTx)
forall tx (m :: * -> *).
(MonadState (StepState tx) m, IsChainState tx) =>
Input tx -> m (Outcome tx)
step (Input SimpleTx
 -> StateT (StepState SimpleTx) IO (Outcome SimpleTx))
-> Input SimpleTx
-> StateT (StepState SimpleTx) IO (Outcome SimpleTx)
forall a b. (a -> b) -> a -> b
$ Message SimpleTx -> Input SimpleTx
forall tx. Message tx -> Input tx
receiveMessage (Message SimpleTx -> Input SimpleTx)
-> Message SimpleTx -> Input SimpleTx
forall a b. (a -> b) -> a -> b
$ SimpleTx -> Message SimpleTx
forall tx. tx -> Message tx
ReqTx SimpleTx
tx
          StateT (StepState SimpleTx) IO (HeadState SimpleTx)
forall tx (m :: * -> *).
MonadState (StepState tx) m =>
m (HeadState tx)
getState
        HeadState SimpleTx
actualState HeadState SimpleTx -> HeadState SimpleTx -> IO ()
forall a. (HasCallStack, Show a, Eq a) => a -> a -> IO ()
`shouldBe` HeadState SimpleTx
st'

    String -> Spec -> Spec
forall a. HasCallStack => String -> SpecWith a -> SpecWith a
describe String
"On AckSn" (Spec -> Spec) -> Spec -> Spec
forall a b. (a -> b) -> a -> b
$ do
      let bobEnv :: Environment
bobEnv = SigningKey HydraKey -> Environment
envFor SigningKey HydraKey
bobSk

      String -> IO () -> SpecWith (Arg (IO ()))
forall a.
(HasCallStack, Example a) =>
String -> a -> SpecWith (Arg a)
it String
"sends ReqSn  when leader and there are seen transactions" (IO () -> SpecWith (Arg (IO ())))
-> IO () -> SpecWith (Arg (IO ()))
forall a b. (a -> b) -> a -> b
$ do
        HeadState SimpleTx
headState <- Environment
-> Ledger SimpleTx
-> HeadState SimpleTx
-> StateT (StepState SimpleTx) IO (HeadState SimpleTx)
-> IO (HeadState SimpleTx)
forall (m :: * -> *) tx a.
Monad m =>
Environment
-> Ledger tx -> HeadState tx -> StateT (StepState tx) m a -> m a
runHeadLogic Environment
bobEnv Ledger SimpleTx
simpleLedger ([Party] -> HeadState SimpleTx
inOpenState [Party]
threeParties) (StateT (StepState SimpleTx) IO (HeadState SimpleTx)
 -> IO (HeadState SimpleTx))
-> StateT (StepState SimpleTx) IO (HeadState SimpleTx)
-> IO (HeadState SimpleTx)
forall a b. (a -> b) -> a -> b
$ do
          Input SimpleTx -> StateT (StepState SimpleTx) IO (Outcome SimpleTx)
forall tx (m :: * -> *).
(MonadState (StepState tx) m, IsChainState tx) =>
Input tx -> m (Outcome tx)
step (Message SimpleTx -> Input SimpleTx
forall tx. Message tx -> Input tx
receiveMessage (Message SimpleTx -> Input SimpleTx)
-> Message SimpleTx -> Input SimpleTx
forall a b. (a -> b) -> a -> b
$ SnapshotVersion
-> SnapshotNumber
-> [TxIdType SimpleTx]
-> Maybe SimpleTx
-> Maybe (UTxOType SimpleTx)
-> Message SimpleTx
forall tx.
SnapshotVersion
-> SnapshotNumber
-> [TxIdType tx]
-> Maybe tx
-> Maybe (UTxOType tx)
-> Message tx
ReqSn SnapshotVersion
0 SnapshotNumber
1 [] Maybe SimpleTx
forall a. Maybe a
Nothing Maybe (UTxOType SimpleTx)
forall a. Maybe a
Nothing)
          Input SimpleTx -> StateT (StepState SimpleTx) IO (Outcome SimpleTx)
forall tx (m :: * -> *).
(MonadState (StepState tx) m, IsChainState tx) =>
Input tx -> m (Outcome tx)
step (Party -> Message SimpleTx -> Input SimpleTx
forall tx. Party -> Message tx -> Input tx
receiveMessageFrom Party
carol (Message SimpleTx -> Input SimpleTx)
-> Message SimpleTx -> Input SimpleTx
forall a b. (a -> b) -> a -> b
$ SimpleTx -> Message SimpleTx
forall tx. tx -> Message tx
ReqTx (SimpleTx -> Message SimpleTx) -> SimpleTx -> Message SimpleTx
forall a b. (a -> b) -> a -> b
$ SimpleId -> SimpleTx
aValidTx SimpleId
1)
          Input SimpleTx -> StateT (StepState SimpleTx) IO (Outcome SimpleTx)
forall tx (m :: * -> *).
(MonadState (StepState tx) m, IsChainState tx) =>
Input tx -> m (Outcome tx)
step (SigningKey HydraKey -> Party -> Input SimpleTx
ackFrom SigningKey HydraKey
carolSk Party
carol)
          Input SimpleTx -> StateT (StepState SimpleTx) IO (Outcome SimpleTx)
forall tx (m :: * -> *).
(MonadState (StepState tx) m, IsChainState tx) =>
Input tx -> m (Outcome tx)
step (SigningKey HydraKey -> Party -> Input SimpleTx
ackFrom SigningKey HydraKey
aliceSk Party
alice)
          StateT (StepState SimpleTx) IO (HeadState SimpleTx)
forall tx (m :: * -> *).
MonadState (StepState tx) m =>
m (HeadState tx)
getState

        Environment
-> Ledger SimpleTx
-> HeadState SimpleTx
-> Input SimpleTx
-> Outcome SimpleTx
forall tx.
IsChainState tx =>
Environment -> Ledger tx -> HeadState tx -> Input tx -> Outcome tx
update Environment
bobEnv Ledger SimpleTx
simpleLedger HeadState SimpleTx
headState (SigningKey HydraKey -> Party -> Input SimpleTx
ackFrom SigningKey HydraKey
bobSk Party
bob)
          Outcome SimpleTx -> (Effect SimpleTx -> Bool) -> IO ()
forall tx.
(HasCallStack, IsChainState tx) =>
Outcome tx -> (Effect tx -> Bool) -> IO ()
`hasEffectSatisfying` Effect SimpleTx -> Bool
forall {tx}. Effect tx -> Bool
sendReqSn

      String -> IO () -> SpecWith (Arg (IO ()))
forall a.
(HasCallStack, Example a) =>
String -> a -> SpecWith (Arg a)
it String
"does NOT send ReqSn when we are the leader but there are NO seen transactions" (IO () -> SpecWith (Arg (IO ())))
-> IO () -> SpecWith (Arg (IO ()))
forall a b. (a -> b) -> a -> b
$ do
        HeadState SimpleTx
headState <- Environment
-> Ledger SimpleTx
-> HeadState SimpleTx
-> StateT (StepState SimpleTx) IO (HeadState SimpleTx)
-> IO (HeadState SimpleTx)
forall (m :: * -> *) tx a.
Monad m =>
Environment
-> Ledger tx -> HeadState tx -> StateT (StepState tx) m a -> m a
runHeadLogic Environment
bobEnv Ledger SimpleTx
simpleLedger ([Party] -> HeadState SimpleTx
inOpenState [Party]
threeParties) (StateT (StepState SimpleTx) IO (HeadState SimpleTx)
 -> IO (HeadState SimpleTx))
-> StateT (StepState SimpleTx) IO (HeadState SimpleTx)
-> IO (HeadState SimpleTx)
forall a b. (a -> b) -> a -> b
$ do
          Input SimpleTx -> StateT (StepState SimpleTx) IO (Outcome SimpleTx)
forall tx (m :: * -> *).
(MonadState (StepState tx) m, IsChainState tx) =>
Input tx -> m (Outcome tx)
step (Message SimpleTx -> Input SimpleTx
forall tx. Message tx -> Input tx
receiveMessage (Message SimpleTx -> Input SimpleTx)
-> Message SimpleTx -> Input SimpleTx
forall a b. (a -> b) -> a -> b
$ SnapshotVersion
-> SnapshotNumber
-> [TxIdType SimpleTx]
-> Maybe SimpleTx
-> Maybe (UTxOType SimpleTx)
-> Message SimpleTx
forall tx.
SnapshotVersion
-> SnapshotNumber
-> [TxIdType tx]
-> Maybe tx
-> Maybe (UTxOType tx)
-> Message tx
ReqSn SnapshotVersion
0 SnapshotNumber
1 [] Maybe SimpleTx
forall a. Maybe a
Nothing Maybe (UTxOType SimpleTx)
forall a. Maybe a
Nothing)
          Input SimpleTx -> StateT (StepState SimpleTx) IO (Outcome SimpleTx)
forall tx (m :: * -> *).
(MonadState (StepState tx) m, IsChainState tx) =>
Input tx -> m (Outcome tx)
step (SigningKey HydraKey -> Party -> Input SimpleTx
ackFrom SigningKey HydraKey
carolSk Party
carol)
          Input SimpleTx -> StateT (StepState SimpleTx) IO (Outcome SimpleTx)
forall tx (m :: * -> *).
(MonadState (StepState tx) m, IsChainState tx) =>
Input tx -> m (Outcome tx)
step (SigningKey HydraKey -> Party -> Input SimpleTx
ackFrom SigningKey HydraKey
aliceSk Party
alice)
          StateT (StepState SimpleTx) IO (HeadState SimpleTx)
forall tx (m :: * -> *).
MonadState (StepState tx) m =>
m (HeadState tx)
getState

        Environment
-> Ledger SimpleTx
-> HeadState SimpleTx
-> Input SimpleTx
-> Outcome SimpleTx
forall tx.
IsChainState tx =>
Environment -> Ledger tx -> HeadState tx -> Input tx -> Outcome tx
update Environment
bobEnv Ledger SimpleTx
simpleLedger HeadState SimpleTx
headState (SigningKey HydraKey -> Party -> Input SimpleTx
ackFrom SigningKey HydraKey
bobSk Party
bob)
          Outcome SimpleTx -> (Effect SimpleTx -> Bool) -> IO ()
forall tx.
(HasCallStack, IsChainState tx) =>
Outcome tx -> (Effect tx -> Bool) -> IO ()
`hasNoEffectSatisfying` Effect SimpleTx -> Bool
forall {tx}. Effect tx -> Bool
sendReqSn

      String -> IO () -> SpecWith (Arg (IO ()))
forall a.
(HasCallStack, Example a) =>
String -> a -> SpecWith (Arg a)
it String
"does NOT send ReqSn when we are NOT the leader but there are seen transactions" (IO () -> SpecWith (Arg (IO ())))
-> IO () -> SpecWith (Arg (IO ()))
forall a b. (a -> b) -> a -> b
$ do
        let
          notLeaderEnv :: Environment
notLeaderEnv = SigningKey HydraKey -> Environment
envFor SigningKey HydraKey
carolSk

        let initiateSigningASnapshot :: Party -> m (Outcome tx)
initiateSigningASnapshot Party
actor =
              Input tx -> m (Outcome tx)
forall tx (m :: * -> *).
(MonadState (StepState tx) m, IsChainState tx) =>
Input tx -> m (Outcome tx)
step (Party -> Message tx -> Input tx
forall tx. Party -> Message tx -> Input tx
receiveMessageFrom Party
actor (Message tx -> Input tx) -> Message tx -> Input tx
forall a b. (a -> b) -> a -> b
$ SnapshotVersion
-> SnapshotNumber
-> [TxIdType tx]
-> Maybe tx
-> Maybe (UTxOType tx)
-> Message tx
forall tx.
SnapshotVersion
-> SnapshotNumber
-> [TxIdType tx]
-> Maybe tx
-> Maybe (UTxOType tx)
-> Message tx
ReqSn SnapshotVersion
0 SnapshotNumber
1 [] Maybe tx
forall a. Maybe a
Nothing Maybe (UTxOType tx)
forall a. Maybe a
Nothing)
            newTxBeforeSnapshotAcknowledged :: StateT (StepState SimpleTx) IO (Outcome SimpleTx)
newTxBeforeSnapshotAcknowledged =
              Input SimpleTx -> StateT (StepState SimpleTx) IO (Outcome SimpleTx)
forall tx (m :: * -> *).
(MonadState (StepState tx) m, IsChainState tx) =>
Input tx -> m (Outcome tx)
step (Party -> Message SimpleTx -> Input SimpleTx
forall tx. Party -> Message tx -> Input tx
receiveMessageFrom Party
carol (Message SimpleTx -> Input SimpleTx)
-> Message SimpleTx -> Input SimpleTx
forall a b. (a -> b) -> a -> b
$ SimpleTx -> Message SimpleTx
forall tx. tx -> Message tx
ReqTx (SimpleTx -> Message SimpleTx) -> SimpleTx -> Message SimpleTx
forall a b. (a -> b) -> a -> b
$ SimpleId -> SimpleTx
aValidTx SimpleId
1)

        HeadState SimpleTx
headState <- Environment
-> Ledger SimpleTx
-> HeadState SimpleTx
-> StateT (StepState SimpleTx) IO (HeadState SimpleTx)
-> IO (HeadState SimpleTx)
forall (m :: * -> *) tx a.
Monad m =>
Environment
-> Ledger tx -> HeadState tx -> StateT (StepState tx) m a -> m a
runHeadLogic Environment
notLeaderEnv Ledger SimpleTx
simpleLedger ([Party] -> HeadState SimpleTx
inOpenState [Party]
threeParties) (StateT (StepState SimpleTx) IO (HeadState SimpleTx)
 -> IO (HeadState SimpleTx))
-> StateT (StepState SimpleTx) IO (HeadState SimpleTx)
-> IO (HeadState SimpleTx)
forall a b. (a -> b) -> a -> b
$ do
          Party -> StateT (StepState SimpleTx) IO (Outcome SimpleTx)
forall {tx} {m :: * -> *}.
(MonadState (StepState tx) m, IsChainState tx) =>
Party -> m (Outcome tx)
initiateSigningASnapshot Party
alice
          Input SimpleTx -> StateT (StepState SimpleTx) IO (Outcome SimpleTx)
forall tx (m :: * -> *).
(MonadState (StepState tx) m, IsChainState tx) =>
Input tx -> m (Outcome tx)
step (SigningKey HydraKey -> Party -> Input SimpleTx
ackFrom SigningKey HydraKey
carolSk Party
carol)
          StateT (StepState SimpleTx) IO (Outcome SimpleTx)
newTxBeforeSnapshotAcknowledged
          Input SimpleTx -> StateT (StepState SimpleTx) IO (Outcome SimpleTx)
forall tx (m :: * -> *).
(MonadState (StepState tx) m, IsChainState tx) =>
Input tx -> m (Outcome tx)
step (SigningKey HydraKey -> Party -> Input SimpleTx
ackFrom SigningKey HydraKey
aliceSk Party
alice)
          StateT (StepState SimpleTx) IO (HeadState SimpleTx)
forall tx (m :: * -> *).
MonadState (StepState tx) m =>
m (HeadState tx)
getState

        let everybodyAcknowleged :: Outcome SimpleTx
everybodyAcknowleged = Environment
-> Ledger SimpleTx
-> HeadState SimpleTx
-> Input SimpleTx
-> Outcome SimpleTx
forall tx.
IsChainState tx =>
Environment -> Ledger tx -> HeadState tx -> Input tx -> Outcome tx
update Environment
notLeaderEnv Ledger SimpleTx
simpleLedger HeadState SimpleTx
headState (Input SimpleTx -> Outcome SimpleTx)
-> Input SimpleTx -> Outcome SimpleTx
forall a b. (a -> b) -> a -> b
$ SigningKey HydraKey -> Party -> Input SimpleTx
ackFrom SigningKey HydraKey
bobSk Party
bob
        Outcome SimpleTx
everybodyAcknowleged Outcome SimpleTx -> (Effect SimpleTx -> Bool) -> IO ()
forall tx.
(HasCallStack, IsChainState tx) =>
Outcome tx -> (Effect tx -> Bool) -> IO ()
`hasNoEffectSatisfying` Effect SimpleTx -> Bool
forall {tx}. Effect tx -> Bool
sendReqSn

      String -> IO () -> SpecWith (Arg (IO ()))
forall a.
(HasCallStack, Example a) =>
String -> a -> SpecWith (Arg a)
it String
"updates seenSnapshot state when sending ReqSn" (IO () -> SpecWith (Arg (IO ())))
-> IO () -> SpecWith (Arg (IO ()))
forall a b. (a -> b) -> a -> b
$ do
        HeadState SimpleTx
headState <- Environment
-> Ledger SimpleTx
-> HeadState SimpleTx
-> StateT (StepState SimpleTx) IO (HeadState SimpleTx)
-> IO (HeadState SimpleTx)
forall (m :: * -> *) tx a.
Monad m =>
Environment
-> Ledger tx -> HeadState tx -> StateT (StepState tx) m a -> m a
runHeadLogic Environment
bobEnv Ledger SimpleTx
simpleLedger ([Party] -> HeadState SimpleTx
inOpenState [Party]
threeParties) (StateT (StepState SimpleTx) IO (HeadState SimpleTx)
 -> IO (HeadState SimpleTx))
-> StateT (StepState SimpleTx) IO (HeadState SimpleTx)
-> IO (HeadState SimpleTx)
forall a b. (a -> b) -> a -> b
$ do
          Input SimpleTx -> StateT (StepState SimpleTx) IO (Outcome SimpleTx)
forall tx (m :: * -> *).
(MonadState (StepState tx) m, IsChainState tx) =>
Input tx -> m (Outcome tx)
step (Message SimpleTx -> Input SimpleTx
forall tx. Message tx -> Input tx
receiveMessage (Message SimpleTx -> Input SimpleTx)
-> Message SimpleTx -> Input SimpleTx
forall a b. (a -> b) -> a -> b
$ SnapshotVersion
-> SnapshotNumber
-> [TxIdType SimpleTx]
-> Maybe SimpleTx
-> Maybe (UTxOType SimpleTx)
-> Message SimpleTx
forall tx.
SnapshotVersion
-> SnapshotNumber
-> [TxIdType tx]
-> Maybe tx
-> Maybe (UTxOType tx)
-> Message tx
ReqSn SnapshotVersion
0 SnapshotNumber
1 [] Maybe SimpleTx
forall a. Maybe a
Nothing Maybe (UTxOType SimpleTx)
forall a. Maybe a
Nothing)
          Input SimpleTx -> StateT (StepState SimpleTx) IO (Outcome SimpleTx)
forall tx (m :: * -> *).
(MonadState (StepState tx) m, IsChainState tx) =>
Input tx -> m (Outcome tx)
step (Party -> Message SimpleTx -> Input SimpleTx
forall tx. Party -> Message tx -> Input tx
receiveMessageFrom Party
carol (Message SimpleTx -> Input SimpleTx)
-> Message SimpleTx -> Input SimpleTx
forall a b. (a -> b) -> a -> b
$ SimpleTx -> Message SimpleTx
forall tx. tx -> Message tx
ReqTx (SimpleTx -> Message SimpleTx) -> SimpleTx -> Message SimpleTx
forall a b. (a -> b) -> a -> b
$ SimpleId -> SimpleTx
aValidTx SimpleId
1)
          Input SimpleTx -> StateT (StepState SimpleTx) IO (Outcome SimpleTx)
forall tx (m :: * -> *).
(MonadState (StepState tx) m, IsChainState tx) =>
Input tx -> m (Outcome tx)
step (SigningKey HydraKey -> Party -> Input SimpleTx
ackFrom SigningKey HydraKey
carolSk Party
carol)
          Input SimpleTx -> StateT (StepState SimpleTx) IO (Outcome SimpleTx)
forall tx (m :: * -> *).
(MonadState (StepState tx) m, IsChainState tx) =>
Input tx -> m (Outcome tx)
step (SigningKey HydraKey -> Party -> Input SimpleTx
ackFrom SigningKey HydraKey
aliceSk Party
alice)
          Input SimpleTx -> StateT (StepState SimpleTx) IO (Outcome SimpleTx)
forall tx (m :: * -> *).
(MonadState (StepState tx) m, IsChainState tx) =>
Input tx -> m (Outcome tx)
step (SigningKey HydraKey -> Party -> Input SimpleTx
ackFrom SigningKey HydraKey
bobSk Party
bob)
          StateT (StepState SimpleTx) IO (HeadState SimpleTx)
forall tx (m :: * -> *).
MonadState (StepState tx) m =>
m (HeadState tx)
getState

        case HeadState SimpleTx
headState of
          Open OpenState{$sel:coordinatedHeadState:OpenState :: forall tx. OpenState tx -> CoordinatedHeadState tx
coordinatedHeadState = CoordinatedHeadState{$sel:seenSnapshot:CoordinatedHeadState :: forall tx. CoordinatedHeadState tx -> SeenSnapshot tx
seenSnapshot = SeenSnapshot SimpleTx
actualSnapshot}} ->
            SeenSnapshot SimpleTx
actualSnapshot SeenSnapshot SimpleTx -> SeenSnapshot SimpleTx -> IO ()
forall a. (HasCallStack, Show a, Eq a) => a -> a -> IO ()
`shouldBe` RequestedSnapshot{$sel:lastSeen:NoSeenSnapshot :: SnapshotNumber
lastSeen = SnapshotNumber
1, $sel:requested:NoSeenSnapshot :: SnapshotNumber
requested = SnapshotNumber
2}
          HeadState SimpleTx
other -> HasCallStack => String -> IO ()
String -> IO ()
expectationFailure (String -> IO ()) -> String -> IO ()
forall a b. (a -> b) -> a -> b
$ String
"Expected to be in open state: " String -> String -> String
forall a. Semigroup a => a -> a -> a
<> HeadState SimpleTx -> String
forall b a. (Show a, IsString b) => a -> b
show HeadState SimpleTx
other

prop_singleMemberHeadAlwaysSnapshotOnReqTx :: ConfirmedSnapshot SimpleTx -> Property
prop_singleMemberHeadAlwaysSnapshotOnReqTx :: ConfirmedSnapshot SimpleTx -> Property
prop_singleMemberHeadAlwaysSnapshotOnReqTx ConfirmedSnapshot SimpleTx
sn = (forall s. PropertyM (ST s) Property) -> Property
forall a. Testable a => (forall s. PropertyM (ST s) a) -> Property
monadicST ((forall s. PropertyM (ST s) Property) -> Property)
-> (forall s. PropertyM (ST s) Property) -> Property
forall a b. (a -> b) -> a -> b
$ do
  (SeenSnapshot SimpleTx
seenSnapshot, SnapshotVersion
version) <-
    Gen (SeenSnapshot SimpleTx, SnapshotVersion)
-> PropertyM (ST s) (SeenSnapshot SimpleTx, SnapshotVersion)
forall (m :: * -> *) a. (Monad m, Show a) => Gen a -> PropertyM m a
pick (Gen (SeenSnapshot SimpleTx, SnapshotVersion)
 -> PropertyM (ST s) (SeenSnapshot SimpleTx, SnapshotVersion))
-> Gen (SeenSnapshot SimpleTx, SnapshotVersion)
-> PropertyM (ST s) (SeenSnapshot SimpleTx, SnapshotVersion)
forall a b. (a -> b) -> a -> b
$
      [Gen (SeenSnapshot SimpleTx, SnapshotVersion)]
-> Gen (SeenSnapshot SimpleTx, SnapshotVersion)
forall a. HasCallStack => [Gen a] -> Gen a
oneof
        [ (SeenSnapshot SimpleTx, SnapshotVersion)
-> Gen (SeenSnapshot SimpleTx, SnapshotVersion)
forall a. a -> Gen a
forall (f :: * -> *) a. Applicative f => a -> f a
pure (SeenSnapshot SimpleTx
forall tx. SeenSnapshot tx
NoSeenSnapshot, SnapshotVersion
0)
        , do
            SnapshotNumber
n <- Gen SnapshotNumber
forall a. Arbitrary a => Gen a
arbitrary
            let v :: SnapshotVersion
v = SimpleId -> SnapshotVersion
forall a. Num a => SimpleId -> a
fromInteger (SnapshotNumber -> SimpleId
forall a. Integral a => a -> SimpleId
toInteger SnapshotNumber
n)
            (SeenSnapshot SimpleTx, SnapshotVersion)
-> Gen (SeenSnapshot SimpleTx, SnapshotVersion)
forall a. a -> Gen a
forall (f :: * -> *) a. Applicative f => a -> f a
pure (SnapshotNumber -> SeenSnapshot SimpleTx
forall tx. SnapshotNumber -> SeenSnapshot tx
LastSeenSnapshot SnapshotNumber
n, SnapshotVersion
v)
        ]
  SimpleTx
tx <- Gen SimpleTx -> PropertyM (ST s) SimpleTx
forall (m :: * -> *) a. (Monad m, Show a) => Gen a -> PropertyM m a
pick (Gen SimpleTx -> PropertyM (ST s) SimpleTx)
-> Gen SimpleTx -> PropertyM (ST s) SimpleTx
forall a b. (a -> b) -> a -> b
$ SimpleId -> SimpleTx
aValidTx (SimpleId -> SimpleTx) -> Gen SimpleId -> Gen SimpleTx
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> Gen SimpleId
forall a. Arbitrary a => Gen a
arbitrary
  let
    aliceEnv :: Environment
aliceEnv =
      let party :: Party
party = Party
alice
       in Environment
            { Party
$sel:party:Environment :: Party
party :: Party
party
            , $sel:signingKey:Environment :: SigningKey HydraKey
signingKey = SigningKey HydraKey
aliceSk
            , $sel:otherParties:Environment :: [Party]
otherParties = []
            , $sel:contestationPeriod:Environment :: ContestationPeriod
contestationPeriod = ContestationPeriod
defaultContestationPeriod
            , $sel:participants:Environment :: [OnChainId]
participants = [Party -> OnChainId
deriveOnChainId Party
party]
            }
    st :: CoordinatedHeadState SimpleTx
st =
      CoordinatedHeadState
        { $sel:localUTxO:CoordinatedHeadState :: UTxOType SimpleTx
localUTxO = Set SimpleTxOut
UTxOType SimpleTx
forall a. Monoid a => a
mempty
        , $sel:allTxs:CoordinatedHeadState :: Map (TxIdType SimpleTx) SimpleTx
allTxs = Map SimpleId SimpleTx
Map (TxIdType SimpleTx) SimpleTx
forall a. Monoid a => a
mempty
        , $sel:localTxs:CoordinatedHeadState :: [SimpleTx]
localTxs = []
        , $sel:confirmedSnapshot:CoordinatedHeadState :: ConfirmedSnapshot SimpleTx
confirmedSnapshot = ConfirmedSnapshot SimpleTx
sn
        , SeenSnapshot SimpleTx
$sel:seenSnapshot:CoordinatedHeadState :: SeenSnapshot SimpleTx
seenSnapshot :: SeenSnapshot SimpleTx
seenSnapshot
        , $sel:pendingDeposits:CoordinatedHeadState :: Map (TxIdType SimpleTx) (UTxOType SimpleTx)
pendingDeposits = Map SimpleId (Set SimpleTxOut)
Map (TxIdType SimpleTx) (UTxOType SimpleTx)
forall a. Monoid a => a
mempty
        , $sel:decommitTx:CoordinatedHeadState :: Maybe SimpleTx
decommitTx = Maybe SimpleTx
forall a. Maybe a
Nothing
        , SnapshotVersion
$sel:version:CoordinatedHeadState :: SnapshotVersion
version :: SnapshotVersion
version
        }
    outcome :: Outcome SimpleTx
outcome = Environment
-> Ledger SimpleTx
-> HeadState SimpleTx
-> Input SimpleTx
-> Outcome SimpleTx
forall tx.
IsChainState tx =>
Environment -> Ledger tx -> HeadState tx -> Input tx -> Outcome tx
update Environment
aliceEnv Ledger SimpleTx
simpleLedger ([Party] -> CoordinatedHeadState SimpleTx -> HeadState SimpleTx
inOpenState' [Party
alice] CoordinatedHeadState SimpleTx
st) (Input SimpleTx -> Outcome SimpleTx)
-> Input SimpleTx -> Outcome SimpleTx
forall a b. (a -> b) -> a -> b
$ Message SimpleTx -> Input SimpleTx
forall tx. Message tx -> Input tx
receiveMessage (Message SimpleTx -> Input SimpleTx)
-> Message SimpleTx -> Input SimpleTx
forall a b. (a -> b) -> a -> b
$ SimpleTx -> Message SimpleTx
forall tx. tx -> Message tx
ReqTx SimpleTx
tx
    Snapshot{$sel:number:Snapshot :: forall tx. Snapshot tx -> SnapshotNumber
number = SnapshotNumber
confirmedSn} = ConfirmedSnapshot SimpleTx -> Snapshot SimpleTx
forall tx. ConfirmedSnapshot tx -> Snapshot tx
getSnapshot ConfirmedSnapshot SimpleTx
sn
    nextSn :: SnapshotNumber
nextSn = SnapshotNumber
confirmedSn SnapshotNumber -> SnapshotNumber -> SnapshotNumber
forall a. Num a => a -> a -> a
+ SnapshotNumber
1
  Property -> PropertyM (ST s) Property
forall a. a -> PropertyM (ST s) a
forall (f :: * -> *) a. Applicative f => a -> f a
pure (Property -> PropertyM (ST s) Property)
-> Property -> PropertyM (ST s) Property
forall a b. (a -> b) -> a -> b
$
    Outcome SimpleTx
outcome Outcome SimpleTx -> Effect SimpleTx -> IO ()
forall tx.
(HasCallStack, IsChainState tx) =>
Outcome tx -> Effect tx -> IO ()
`hasEffect` Message SimpleTx -> Effect SimpleTx
forall tx. Message tx -> Effect tx
NetworkEffect (SnapshotVersion
-> SnapshotNumber
-> [TxIdType SimpleTx]
-> Maybe SimpleTx
-> Maybe (UTxOType SimpleTx)
-> Message SimpleTx
forall tx.
SnapshotVersion
-> SnapshotNumber
-> [TxIdType tx]
-> Maybe tx
-> Maybe (UTxOType tx)
-> Message tx
ReqSn SnapshotVersion
version SnapshotNumber
nextSn [SimpleTx -> TxIdType SimpleTx
forall tx. IsTx tx => tx -> TxIdType tx
txId SimpleTx
tx] Maybe SimpleTx
forall a. Maybe a
Nothing Maybe (Set SimpleTxOut)
Maybe (UTxOType SimpleTx)
forall a. Maybe a
Nothing)
      IO () -> (IO () -> Property) -> Property
forall a b. a -> (a -> b) -> b
& String -> IO () -> Property
forall prop. Testable prop => String -> prop -> Property
counterexample (Outcome SimpleTx -> String
forall b a. (Show a, IsString b) => a -> b
show Outcome SimpleTx
outcome)

prop_thereIsAlwaysALeader :: Property
prop_thereIsAlwaysALeader :: Property
prop_thereIsAlwaysALeader =
  Gen SnapshotNumber -> (SnapshotNumber -> Property) -> Property
forall a prop.
(Show a, Testable prop) =>
Gen a -> (a -> prop) -> Property
forAll Gen SnapshotNumber
forall a. Arbitrary a => Gen a
arbitrary ((SnapshotNumber -> Property) -> Property)
-> (SnapshotNumber -> Property) -> Property
forall a b. (a -> b) -> a -> b
$ \SnapshotNumber
sn ->
    Gen HeadParameters -> (HeadParameters -> Property) -> Property
forall a prop.
(Show a, Testable prop) =>
Gen a -> (a -> prop) -> Property
forAll Gen HeadParameters
forall a. Arbitrary a => Gen a
arbitrary ((HeadParameters -> Property) -> Property)
-> (HeadParameters -> Property) -> Property
forall a b. (a -> b) -> a -> b
$ \params :: HeadParameters
params@HeadParameters{[Party]
parties :: [Party]
$sel:parties:HeadParameters :: HeadParameters -> [Party]
parties} ->
      Bool -> Bool
not ([Party] -> Bool
forall a. [a] -> Bool
forall (t :: * -> *) a. Foldable t => t a -> Bool
null [Party]
parties) Bool -> Bool -> Property
forall prop. Testable prop => Bool -> prop -> Property
==>
        (Party -> Bool) -> [Party] -> Bool
forall (t :: * -> *) a. Foldable t => (a -> Bool) -> t a -> Bool
any (\Party
p -> HeadParameters -> Party -> SnapshotNumber -> Bool
isLeader HeadParameters
params Party
p SnapshotNumber
sn) [Party]
parties