{-# 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), Outcome, SeenSnapshot (..), coordinatedHeadState, isLeader, mkSeenSnapshot, update)
import Hydra.HeadLogicSpec (StepState, getState, hasEffect, hasEffectSatisfying, hasNoEffectSatisfying, inOpenState, inOpenState', nowFromSlot, receiveMessage, receiveMessageFrom, runHeadLogic, step)
import Hydra.Ledger.Simple (SimpleTx (..), simpleLedger)
import Hydra.Network.Message (Message (..))
import Hydra.Node.Environment (Environment (..))
import Hydra.Node.State (ChainPointTime (..), NodeState (..))
import Hydra.Options (defaultContestationPeriod, defaultDepositActivation, defaultDepositPeriod, defaultUnsyncedPeriod)
import Hydra.Tx.Accumulator qualified as Accumulator
import Hydra.Tx.Crypto (sign)
import Hydra.Tx.HeadParameters (HeadParameters (..))
import Hydra.Tx.IsTx (IsTx, UTxOType, txId)
import Hydra.Tx.Party (Party, deriveParty)
import Hydra.Tx.Snapshot (ConfirmedSnapshot (..), Snapshot (..), SnapshotNumber, SnapshotVersion, getSnapshot)
import Test.Hydra.Ledger.Simple (aValidTx, utxoRef)
import Test.Hydra.Tx.Fixture (
  alice,
  aliceSk,
  bob,
  bobSk,
  carol,
  carolSk,
  deriveOnChainId,
  testHeadId,
 )
import Test.QuickCheck (Property, counterexample, forAll, oneof, (==>))
import Test.QuickCheck.Monadic (monadicIO, pick, run)

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 :: Secret (SigningKey HydraKey) -> Environment
envFor Secret (SigningKey HydraKey)
signingKey =
          let party :: Party
party = Secret (SigningKey HydraKey) -> Party
deriveParty Secret (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
                , Secret (SigningKey HydraKey)
signingKey :: Secret (SigningKey HydraKey)
$sel:signingKey:Environment :: Secret (SigningKey HydraKey)
signingKey
                , [Party]
otherParties :: [Party]
$sel:otherParties:Environment :: [Party]
otherParties
                , $sel:contestationPeriod:Environment :: ContestationPeriod
contestationPeriod = ContestationPeriod
defaultContestationPeriod
                , $sel:depositPeriod:Environment :: DepositPeriod
depositPeriod = DepositPeriod
defaultDepositPeriod
                , $sel:depositActivation:Environment :: DepositPeriod
depositActivation = DepositPeriod
defaultDepositActivation
                , $sel:unsyncedPeriod:Environment :: UnsyncedPeriod
unsyncedPeriod = UnsyncedPeriod
defaultUnsyncedPeriod
                , $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
                , $sel:configuredPeers:Environment :: Text
configuredPeers = Text
""
                }

    let coordinatedHeadState :: CoordinatedHeadState SimpleTx
coordinatedHeadState =
          CoordinatedHeadState
            { $sel:localUTxO:CoordinatedHeadState :: UTxOType SimpleTx
localUTxO = UTxOType SimpleTx
forall a. Monoid a => a
mempty
            , $sel:allTxs:CoordinatedHeadState :: Map (TxIdType SimpleTx) SimpleTx
allTxs = Map (TxIdType SimpleTx) SimpleTx
forall a. Monoid a => a
mempty
            , $sel:localTxs:CoordinatedHeadState :: Seq SimpleTx
localTxs = Seq SimpleTx
forall a. Monoid a => a
mempty
            , $sel:confirmedSnapshot:CoordinatedHeadState :: ConfirmedSnapshot SimpleTx
confirmedSnapshot = HeadId -> ConfirmedSnapshot SimpleTx
forall tx. HeadId -> ConfirmedSnapshot tx
InitialSnapshot HeadId
testHeadId
            , $sel:seenSnapshot:CoordinatedHeadState :: SeenSnapshot SimpleTx
seenSnapshot = SeenSnapshot SimpleTx
forall tx. SeenSnapshot tx
NoSeenSnapshot
            , $sel:currentDepositTxId:CoordinatedHeadState :: Maybe (TxIdType SimpleTx)
currentDepositTxId = Maybe (TxIdType SimpleTx)
forall a. Maybe a
Nothing
            , $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 :: forall tx. Effect tx -> Bool
sendReqSn = \case
          NetworkEffect ReqSn{} -> Bool
True
          Effect tx
_ -> Bool
False
    let snapshot1 :: Snapshot SimpleTx
snapshot1 = SnapshotNumber
-> SnapshotVersion
-> [SimpleTx]
-> UTxOType SimpleTx
-> Snapshot SimpleTx
forall tx.
IsTx tx =>
SnapshotNumber
-> SnapshotVersion -> [tx] -> UTxOType tx -> Snapshot tx
testSnapshot SnapshotNumber
1 SnapshotVersion
0 [] UTxOType SimpleTx
forall a. Monoid a => a
mempty

    let ackFrom :: Secret (SigningKey HydraKey) -> Party -> Input SimpleTx
ackFrom Secret (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 (Secret (SigningKey HydraKey)
-> Snapshot SimpleTx -> Signature (Snapshot SimpleTx)
forall a.
SignableRepresentation a =>
Secret (SigningKey HydraKey) -> a -> Signature a
sign Secret (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
"SeenSnapshot" (Spec -> Spec) -> Spec -> Spec
forall a b. (a -> b) -> a -> b
$ do
      String -> IO () -> SpecWith (Arg (IO ()))
forall a.
(HasCallStack, Example a) =>
String -> a -> SpecWith (Arg a)
it String
"forcing to WHNF does not compute the signable bytes" (IO () -> SpecWith (Arg (IO ())))
-> IO () -> SpecWith (Arg (IO ()))
forall a b. (a -> b) -> a -> b
$ do
        -- State hydration folds every historical NodeState to WHNF; a strict
        -- signableBytes field would recompute one accumulator commitment per
        -- replayed SnapshotRequested event. This throws if the field ever
        -- loses its laziness annotation.
        let poisoned :: Snapshot SimpleTx
poisoned =
              (SnapshotNumber
-> SnapshotVersion
-> [SimpleTx]
-> UTxOType SimpleTx
-> Snapshot SimpleTx
forall tx.
IsTx tx =>
SnapshotNumber
-> SnapshotVersion -> [tx] -> UTxOType tx -> Snapshot tx
testSnapshot SnapshotNumber
1 SnapshotVersion
0 [] Set SimpleTxOut
UTxOType SimpleTx
forall a. Monoid a => a
mempty :: Snapshot SimpleTx)
                { accumulator = error "signableBytes forced during WHNF"
                }
        Snapshot SimpleTx
-> Map Party (Signature (Snapshot SimpleTx))
-> SeenSnapshot SimpleTx
forall tx.
IsTx tx =>
Snapshot tx
-> Map Party (Signature (Snapshot tx)) -> SeenSnapshot tx
mkSeenSnapshot Snapshot SimpleTx
poisoned Map Party (Signature (Snapshot SimpleTx))
forall a. Monoid a => a
mempty SeenSnapshot SimpleTx -> IO () -> IO ()
forall a b. a -> b -> b
`seq` forall (f :: * -> *) a. Applicative f => a -> f a
pure @IO ()

    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 = Integer -> SimpleTx
aValidTx Integer
1
            s0 :: NodeState SimpleTx
s0 = [Party] -> CoordinatedHeadState SimpleTx -> NodeState SimpleTx
inOpenState' [Party
alice, Party
bob] CoordinatedHeadState SimpleTx
coordinatedHeadState
        UTCTime
now <- ChainSlot -> IO UTCTime
forall (m :: * -> *).
(MonadFail m, MonadTime m) =>
ChainSlot -> m UTCTime
nowFromSlot (ChainPointTime -> ChainSlot
currentSlot (ChainPointTime -> ChainSlot)
-> (NodeState SimpleTx -> ChainPointTime)
-> NodeState SimpleTx
-> ChainSlot
forall b c a. (b -> c) -> (a -> b) -> a -> c
. NodeState SimpleTx -> ChainPointTime
forall tx. NodeState tx -> ChainPointTime
chainPointTime (NodeState SimpleTx -> ChainSlot)
-> NodeState SimpleTx -> ChainSlot
forall a b. (a -> b) -> a -> b
$ NodeState SimpleTx
s0)
        let outcome :: Outcome SimpleTx
outcome = Environment
-> Ledger SimpleTx
-> UTCTime
-> NodeState SimpleTx
-> Input SimpleTx
-> Outcome SimpleTx
forall tx.
IsChainState tx =>
Environment
-> Ledger tx -> UTCTime -> NodeState tx -> Input tx -> Outcome tx
update (Secret (SigningKey HydraKey) -> Environment
envFor Secret (SigningKey HydraKey)
aliceSk) Ledger SimpleTx
simpleLedger UTCTime
now NodeState SimpleTx
s0 (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 (TxIdType SimpleTx)
-> Message SimpleTx
forall tx.
SnapshotVersion
-> SnapshotNumber
-> [TxIdType tx]
-> Maybe tx
-> Maybe (TxIdType 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 Integer
Maybe (TxIdType 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 = Integer -> SimpleTx
aValidTx Integer
1
            st :: CoordinatedHeadState SimpleTx
st = CoordinatedHeadState SimpleTx
coordinatedHeadState{localTxs = pure tx}
            s0 :: NodeState SimpleTx
s0 = [Party] -> CoordinatedHeadState SimpleTx -> NodeState SimpleTx
inOpenState' [Party
alice, Party
bob] CoordinatedHeadState SimpleTx
st
        UTCTime
now <- ChainSlot -> IO UTCTime
forall (m :: * -> *).
(MonadFail m, MonadTime m) =>
ChainSlot -> m UTCTime
nowFromSlot (ChainPointTime -> ChainSlot
currentSlot (ChainPointTime -> ChainSlot)
-> (NodeState SimpleTx -> ChainPointTime)
-> NodeState SimpleTx
-> ChainSlot
forall b c a. (b -> c) -> (a -> b) -> a -> c
. NodeState SimpleTx -> ChainPointTime
forall tx. NodeState tx -> ChainPointTime
chainPointTime (NodeState SimpleTx -> ChainSlot)
-> NodeState SimpleTx -> ChainSlot
forall a b. (a -> b) -> a -> b
$ NodeState SimpleTx
s0)
        let outcome :: Outcome SimpleTx
outcome = Environment
-> Ledger SimpleTx
-> UTCTime
-> NodeState SimpleTx
-> Input SimpleTx
-> Outcome SimpleTx
forall tx.
IsChainState tx =>
Environment
-> Ledger tx -> UTCTime -> NodeState tx -> Input tx -> Outcome tx
update (Secret (SigningKey HydraKey) -> Environment
envFor Secret (SigningKey HydraKey)
bobSk) Ledger SimpleTx
simpleLedger UTCTime
now NodeState SimpleTx
s0 (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 = Integer -> SimpleTx
aValidTx Integer
1
            sn1 :: Snapshot SimpleTx
sn1 = SnapshotNumber
-> SnapshotVersion
-> [SimpleTx]
-> UTxOType SimpleTx
-> Snapshot SimpleTx
forall tx.
IsTx tx =>
SnapshotNumber
-> SnapshotVersion -> [tx] -> UTxOType tx -> Snapshot tx
testSnapshot SnapshotNumber
1 SnapshotVersion
1 [] Set SimpleTxOut
UTxOType SimpleTx
u0 :: Snapshot SimpleTx
            st :: CoordinatedHeadState SimpleTx
st = CoordinatedHeadState SimpleTx
coordinatedHeadState{seenSnapshot = mkSeenSnapshot sn1 mempty}
            s0 :: NodeState SimpleTx
s0 = [Party] -> CoordinatedHeadState SimpleTx -> NodeState SimpleTx
inOpenState' [Party
alice, Party
bob] CoordinatedHeadState SimpleTx
st
        UTCTime
now <- ChainSlot -> IO UTCTime
forall (m :: * -> *).
(MonadFail m, MonadTime m) =>
ChainSlot -> m UTCTime
nowFromSlot (ChainPointTime -> ChainSlot
currentSlot (ChainPointTime -> ChainSlot)
-> (NodeState SimpleTx -> ChainPointTime)
-> NodeState SimpleTx
-> ChainSlot
forall b c a. (b -> c) -> (a -> b) -> a -> c
. NodeState SimpleTx -> ChainPointTime
forall tx. NodeState tx -> ChainPointTime
chainPointTime (NodeState SimpleTx -> ChainSlot)
-> NodeState SimpleTx -> ChainSlot
forall a b. (a -> b) -> a -> b
$ NodeState SimpleTx
s0)
        let outcome :: Outcome SimpleTx
outcome = Environment
-> Ledger SimpleTx
-> UTCTime
-> NodeState SimpleTx
-> Input SimpleTx
-> Outcome SimpleTx
forall tx.
IsChainState tx =>
Environment
-> Ledger tx -> UTCTime -> NodeState tx -> Input tx -> Outcome tx
update (Secret (SigningKey HydraKey) -> Environment
envFor Secret (SigningKey HydraKey)
aliceSk) Ledger SimpleTx
simpleLedger UTCTime
now NodeState SimpleTx
s0 (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 = Integer -> SimpleTx
aValidTx Integer
1
            st :: NodeState SimpleTx
st = [Party] -> CoordinatedHeadState SimpleTx -> NodeState SimpleTx
inOpenState' [Party]
threeParties CoordinatedHeadState SimpleTx
coordinatedHeadState
            st' :: NodeState SimpleTx
st' =
              [Party] -> CoordinatedHeadState SimpleTx -> NodeState SimpleTx
inOpenState' [Party]
threeParties (CoordinatedHeadState SimpleTx -> NodeState SimpleTx)
-> CoordinatedHeadState SimpleTx -> NodeState SimpleTx
forall a b. (a -> b) -> a -> b
$
                CoordinatedHeadState SimpleTx
coordinatedHeadState
                  { localTxs = pure tx
                  , allTxs = Map.singleton (txId tx) tx
                  , localUTxO = u0 <> utxoRef (txId tx)
                  , seenSnapshot = RequestedSnapshot{lastSeen = 0, requested = 1}
                  }

        NodeState SimpleTx
actualState <- Environment
-> Ledger SimpleTx
-> NodeState SimpleTx
-> StateT (StepState SimpleTx) IO (NodeState SimpleTx)
-> IO (NodeState SimpleTx)
forall (m :: * -> *) tx a.
Monad m =>
Environment
-> Ledger tx -> NodeState tx -> StateT (StepState tx) m a -> m a
runHeadLogic (Secret (SigningKey HydraKey) -> Environment
envFor Secret (SigningKey HydraKey)
aliceSk) Ledger SimpleTx
simpleLedger NodeState SimpleTx
st (StateT (StepState SimpleTx) IO (NodeState SimpleTx)
 -> IO (NodeState SimpleTx))
-> StateT (StepState SimpleTx) IO (NodeState SimpleTx)
-> IO (NodeState 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, MonadTime m) =>
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 (NodeState SimpleTx)
forall tx (m :: * -> *).
MonadState (StepState tx) m =>
m (NodeState tx)
getState
        NodeState SimpleTx
actualState NodeState SimpleTx -> NodeState SimpleTx -> IO ()
forall a. (HasCallStack, Show a, Eq a) => a -> a -> IO ()
`shouldBe` NodeState 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 = Secret (SigningKey HydraKey) -> Environment
envFor Secret (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
        NodeState SimpleTx
headState <- Environment
-> Ledger SimpleTx
-> NodeState SimpleTx
-> StateT (StepState SimpleTx) IO (NodeState SimpleTx)
-> IO (NodeState SimpleTx)
forall (m :: * -> *) tx a.
Monad m =>
Environment
-> Ledger tx -> NodeState tx -> StateT (StepState tx) m a -> m a
runHeadLogic Environment
bobEnv Ledger SimpleTx
simpleLedger ([Party] -> NodeState SimpleTx
inOpenState [Party]
threeParties) (StateT (StepState SimpleTx) IO (NodeState SimpleTx)
 -> IO (NodeState SimpleTx))
-> StateT (StepState SimpleTx) IO (NodeState SimpleTx)
-> IO (NodeState 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, MonadTime m) =>
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 (TxIdType SimpleTx)
-> Message SimpleTx
forall tx.
SnapshotVersion
-> SnapshotNumber
-> [TxIdType tx]
-> Maybe tx
-> Maybe (TxIdType tx)
-> Message tx
ReqSn SnapshotVersion
0 SnapshotNumber
1 [] Maybe SimpleTx
forall a. Maybe a
Nothing Maybe (TxIdType SimpleTx)
forall a. Maybe a
Nothing)
          Input SimpleTx -> StateT (StepState SimpleTx) IO (Outcome SimpleTx)
forall tx (m :: * -> *).
(MonadState (StepState tx) m, IsChainState tx, MonadTime m) =>
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
$ Integer -> SimpleTx
aValidTx Integer
1)
          Input SimpleTx -> StateT (StepState SimpleTx) IO (Outcome SimpleTx)
forall tx (m :: * -> *).
(MonadState (StepState tx) m, IsChainState tx, MonadTime m) =>
Input tx -> m (Outcome tx)
step (Secret (SigningKey HydraKey) -> Party -> Input SimpleTx
ackFrom Secret (SigningKey HydraKey)
carolSk Party
carol)
          Input SimpleTx -> StateT (StepState SimpleTx) IO (Outcome SimpleTx)
forall tx (m :: * -> *).
(MonadState (StepState tx) m, IsChainState tx, MonadTime m) =>
Input tx -> m (Outcome tx)
step (Secret (SigningKey HydraKey) -> Party -> Input SimpleTx
ackFrom Secret (SigningKey HydraKey)
aliceSk Party
alice)
          StateT (StepState SimpleTx) IO (NodeState SimpleTx)
forall tx (m :: * -> *).
MonadState (StepState tx) m =>
m (NodeState tx)
getState

        UTCTime
now <- ChainSlot -> IO UTCTime
forall (m :: * -> *).
(MonadFail m, MonadTime m) =>
ChainSlot -> m UTCTime
nowFromSlot (ChainPointTime -> ChainSlot
currentSlot (ChainPointTime -> ChainSlot)
-> (NodeState SimpleTx -> ChainPointTime)
-> NodeState SimpleTx
-> ChainSlot
forall b c a. (b -> c) -> (a -> b) -> a -> c
. NodeState SimpleTx -> ChainPointTime
forall tx. NodeState tx -> ChainPointTime
chainPointTime (NodeState SimpleTx -> ChainSlot)
-> NodeState SimpleTx -> ChainSlot
forall a b. (a -> b) -> a -> b
$ NodeState SimpleTx
headState)
        Environment
-> Ledger SimpleTx
-> UTCTime
-> NodeState SimpleTx
-> Input SimpleTx
-> Outcome SimpleTx
forall tx.
IsChainState tx =>
Environment
-> Ledger tx -> UTCTime -> NodeState tx -> Input tx -> Outcome tx
update Environment
bobEnv Ledger SimpleTx
simpleLedger UTCTime
now NodeState SimpleTx
headState (Secret (SigningKey HydraKey) -> Party -> Input SimpleTx
ackFrom Secret (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
        NodeState SimpleTx
headState <- Environment
-> Ledger SimpleTx
-> NodeState SimpleTx
-> StateT (StepState SimpleTx) IO (NodeState SimpleTx)
-> IO (NodeState SimpleTx)
forall (m :: * -> *) tx a.
Monad m =>
Environment
-> Ledger tx -> NodeState tx -> StateT (StepState tx) m a -> m a
runHeadLogic Environment
bobEnv Ledger SimpleTx
simpleLedger ([Party] -> NodeState SimpleTx
inOpenState [Party]
threeParties) (StateT (StepState SimpleTx) IO (NodeState SimpleTx)
 -> IO (NodeState SimpleTx))
-> StateT (StepState SimpleTx) IO (NodeState SimpleTx)
-> IO (NodeState 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, MonadTime m) =>
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 (TxIdType SimpleTx)
-> Message SimpleTx
forall tx.
SnapshotVersion
-> SnapshotNumber
-> [TxIdType tx]
-> Maybe tx
-> Maybe (TxIdType tx)
-> Message tx
ReqSn SnapshotVersion
0 SnapshotNumber
1 [] Maybe SimpleTx
forall a. Maybe a
Nothing Maybe (TxIdType SimpleTx)
forall a. Maybe a
Nothing)
          Input SimpleTx -> StateT (StepState SimpleTx) IO (Outcome SimpleTx)
forall tx (m :: * -> *).
(MonadState (StepState tx) m, IsChainState tx, MonadTime m) =>
Input tx -> m (Outcome tx)
step (Secret (SigningKey HydraKey) -> Party -> Input SimpleTx
ackFrom Secret (SigningKey HydraKey)
carolSk Party
carol)
          Input SimpleTx -> StateT (StepState SimpleTx) IO (Outcome SimpleTx)
forall tx (m :: * -> *).
(MonadState (StepState tx) m, IsChainState tx, MonadTime m) =>
Input tx -> m (Outcome tx)
step (Secret (SigningKey HydraKey) -> Party -> Input SimpleTx
ackFrom Secret (SigningKey HydraKey)
aliceSk Party
alice)
          StateT (StepState SimpleTx) IO (NodeState SimpleTx)
forall tx (m :: * -> *).
MonadState (StepState tx) m =>
m (NodeState tx)
getState

        UTCTime
now <- ChainSlot -> IO UTCTime
forall (m :: * -> *).
(MonadFail m, MonadTime m) =>
ChainSlot -> m UTCTime
nowFromSlot (ChainPointTime -> ChainSlot
currentSlot (ChainPointTime -> ChainSlot)
-> (NodeState SimpleTx -> ChainPointTime)
-> NodeState SimpleTx
-> ChainSlot
forall b c a. (b -> c) -> (a -> b) -> a -> c
. NodeState SimpleTx -> ChainPointTime
forall tx. NodeState tx -> ChainPointTime
chainPointTime (NodeState SimpleTx -> ChainSlot)
-> NodeState SimpleTx -> ChainSlot
forall a b. (a -> b) -> a -> b
$ NodeState SimpleTx
headState)
        Environment
-> Ledger SimpleTx
-> UTCTime
-> NodeState SimpleTx
-> Input SimpleTx
-> Outcome SimpleTx
forall tx.
IsChainState tx =>
Environment
-> Ledger tx -> UTCTime -> NodeState tx -> Input tx -> Outcome tx
update Environment
bobEnv Ledger SimpleTx
simpleLedger UTCTime
now NodeState SimpleTx
headState (Secret (SigningKey HydraKey) -> Party -> Input SimpleTx
ackFrom Secret (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 = Secret (SigningKey HydraKey) -> Environment
envFor Secret (SigningKey HydraKey)
carolSk

        let initiateSigningASnapshot :: (MonadState (StepState SimpleTx) m, MonadTime m) => Party -> m (Outcome SimpleTx)
            initiateSigningASnapshot :: forall (m :: * -> *).
(MonadState (StepState SimpleTx) m, MonadTime m) =>
Party -> m (Outcome SimpleTx)
initiateSigningASnapshot Party
actor =
              Input SimpleTx -> m (Outcome SimpleTx)
forall tx (m :: * -> *).
(MonadState (StepState tx) m, IsChainState tx, MonadTime m) =>
Input tx -> m (Outcome tx)
step (Party -> Message SimpleTx -> Input SimpleTx
forall tx. Party -> Message tx -> Input tx
receiveMessageFrom Party
actor (Message SimpleTx -> Input SimpleTx)
-> Message SimpleTx -> Input SimpleTx
forall a b. (a -> b) -> a -> b
$ SnapshotVersion
-> SnapshotNumber
-> [TxIdType SimpleTx]
-> Maybe SimpleTx
-> Maybe (TxIdType SimpleTx)
-> Message SimpleTx
forall tx.
SnapshotVersion
-> SnapshotNumber
-> [TxIdType tx]
-> Maybe tx
-> Maybe (TxIdType tx)
-> Message tx
ReqSn SnapshotVersion
0 SnapshotNumber
1 [] Maybe SimpleTx
forall a. Maybe a
Nothing Maybe Integer
Maybe (TxIdType SimpleTx)
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, MonadTime m) =>
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
$ Integer -> SimpleTx
aValidTx Integer
1)

        NodeState SimpleTx
headState <- Environment
-> Ledger SimpleTx
-> NodeState SimpleTx
-> StateT (StepState SimpleTx) IO (NodeState SimpleTx)
-> IO (NodeState SimpleTx)
forall (m :: * -> *) tx a.
Monad m =>
Environment
-> Ledger tx -> NodeState tx -> StateT (StepState tx) m a -> m a
runHeadLogic Environment
notLeaderEnv Ledger SimpleTx
simpleLedger ([Party] -> NodeState SimpleTx
inOpenState [Party]
threeParties) (StateT (StepState SimpleTx) IO (NodeState SimpleTx)
 -> IO (NodeState SimpleTx))
-> StateT (StepState SimpleTx) IO (NodeState SimpleTx)
-> IO (NodeState SimpleTx)
forall a b. (a -> b) -> a -> b
$ do
          Party -> StateT (StepState SimpleTx) IO (Outcome SimpleTx)
forall (m :: * -> *).
(MonadState (StepState SimpleTx) m, MonadTime m) =>
Party -> m (Outcome SimpleTx)
initiateSigningASnapshot Party
alice
          Input SimpleTx -> StateT (StepState SimpleTx) IO (Outcome SimpleTx)
forall tx (m :: * -> *).
(MonadState (StepState tx) m, IsChainState tx, MonadTime m) =>
Input tx -> m (Outcome tx)
step (Secret (SigningKey HydraKey) -> Party -> Input SimpleTx
ackFrom Secret (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, MonadTime m) =>
Input tx -> m (Outcome tx)
step (Secret (SigningKey HydraKey) -> Party -> Input SimpleTx
ackFrom Secret (SigningKey HydraKey)
aliceSk Party
alice)
          StateT (StepState SimpleTx) IO (NodeState SimpleTx)
forall tx (m :: * -> *).
MonadState (StepState tx) m =>
m (NodeState tx)
getState

        UTCTime
now <- ChainSlot -> IO UTCTime
forall (m :: * -> *).
(MonadFail m, MonadTime m) =>
ChainSlot -> m UTCTime
nowFromSlot (ChainPointTime -> ChainSlot
currentSlot (ChainPointTime -> ChainSlot)
-> (NodeState SimpleTx -> ChainPointTime)
-> NodeState SimpleTx
-> ChainSlot
forall b c a. (b -> c) -> (a -> b) -> a -> c
. NodeState SimpleTx -> ChainPointTime
forall tx. NodeState tx -> ChainPointTime
chainPointTime (NodeState SimpleTx -> ChainSlot)
-> NodeState SimpleTx -> ChainSlot
forall a b. (a -> b) -> a -> b
$ NodeState SimpleTx
headState)
        let everybodyAcknowledged :: Outcome SimpleTx
everybodyAcknowledged = Environment
-> Ledger SimpleTx
-> UTCTime
-> NodeState SimpleTx
-> Input SimpleTx
-> Outcome SimpleTx
forall tx.
IsChainState tx =>
Environment
-> Ledger tx -> UTCTime -> NodeState tx -> Input tx -> Outcome tx
update Environment
notLeaderEnv Ledger SimpleTx
simpleLedger UTCTime
now NodeState SimpleTx
headState (Input SimpleTx -> Outcome SimpleTx)
-> Input SimpleTx -> Outcome SimpleTx
forall a b. (a -> b) -> a -> b
$ Secret (SigningKey HydraKey) -> Party -> Input SimpleTx
ackFrom Secret (SigningKey HydraKey)
bobSk Party
bob
        Outcome SimpleTx
everybodyAcknowledged 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
        NodeState SimpleTx
nodeState <- Environment
-> Ledger SimpleTx
-> NodeState SimpleTx
-> StateT (StepState SimpleTx) IO (NodeState SimpleTx)
-> IO (NodeState SimpleTx)
forall (m :: * -> *) tx a.
Monad m =>
Environment
-> Ledger tx -> NodeState tx -> StateT (StepState tx) m a -> m a
runHeadLogic Environment
bobEnv Ledger SimpleTx
simpleLedger ([Party] -> NodeState SimpleTx
inOpenState [Party]
threeParties) (StateT (StepState SimpleTx) IO (NodeState SimpleTx)
 -> IO (NodeState SimpleTx))
-> StateT (StepState SimpleTx) IO (NodeState SimpleTx)
-> IO (NodeState 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, MonadTime m) =>
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 (TxIdType SimpleTx)
-> Message SimpleTx
forall tx.
SnapshotVersion
-> SnapshotNumber
-> [TxIdType tx]
-> Maybe tx
-> Maybe (TxIdType tx)
-> Message tx
ReqSn SnapshotVersion
0 SnapshotNumber
1 [] Maybe SimpleTx
forall a. Maybe a
Nothing Maybe (TxIdType SimpleTx)
forall a. Maybe a
Nothing)
          Input SimpleTx -> StateT (StepState SimpleTx) IO (Outcome SimpleTx)
forall tx (m :: * -> *).
(MonadState (StepState tx) m, IsChainState tx, MonadTime m) =>
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
$ Integer -> SimpleTx
aValidTx Integer
1)
          Input SimpleTx -> StateT (StepState SimpleTx) IO (Outcome SimpleTx)
forall tx (m :: * -> *).
(MonadState (StepState tx) m, IsChainState tx, MonadTime m) =>
Input tx -> m (Outcome tx)
step (Secret (SigningKey HydraKey) -> Party -> Input SimpleTx
ackFrom Secret (SigningKey HydraKey)
carolSk Party
carol)
          Input SimpleTx -> StateT (StepState SimpleTx) IO (Outcome SimpleTx)
forall tx (m :: * -> *).
(MonadState (StepState tx) m, IsChainState tx, MonadTime m) =>
Input tx -> m (Outcome tx)
step (Secret (SigningKey HydraKey) -> Party -> Input SimpleTx
ackFrom Secret (SigningKey HydraKey)
aliceSk Party
alice)
          Input SimpleTx -> StateT (StepState SimpleTx) IO (Outcome SimpleTx)
forall tx (m :: * -> *).
(MonadState (StepState tx) m, IsChainState tx, MonadTime m) =>
Input tx -> m (Outcome tx)
step (Secret (SigningKey HydraKey) -> Party -> Input SimpleTx
ackFrom Secret (SigningKey HydraKey)
bobSk Party
bob)
          StateT (StepState SimpleTx) IO (NodeState SimpleTx)
forall tx (m :: * -> *).
MonadState (StepState tx) m =>
m (NodeState tx)
getState

        case NodeState SimpleTx -> HeadState SimpleTx
forall tx. NodeState tx -> HeadState tx
headState NodeState SimpleTx
nodeState 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 = PropertyM IO Property -> Property
forall a. Testable a => PropertyM IO a -> Property
monadicIO (PropertyM IO Property -> Property)
-> PropertyM IO Property -> Property
forall a b. (a -> b) -> a -> b
$ do
  (SeenSnapshot SimpleTx
seenSnapshot, SnapshotVersion
version) <-
    Gen (SeenSnapshot SimpleTx, SnapshotVersion)
-> PropertyM IO (SeenSnapshot SimpleTx, SnapshotVersion)
forall (m :: * -> *) a. (Monad m, Show a) => Gen a -> PropertyM m a
pick (Gen (SeenSnapshot SimpleTx, SnapshotVersion)
 -> PropertyM IO (SeenSnapshot SimpleTx, SnapshotVersion))
-> Gen (SeenSnapshot SimpleTx, SnapshotVersion)
-> PropertyM IO (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 = Integer -> SnapshotVersion
forall a. Num a => Integer -> a
fromInteger (SnapshotNumber -> Integer
forall a. Integral a => a -> Integer
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 IO SimpleTx
forall (m :: * -> *) a. (Monad m, Show a) => Gen a -> PropertyM m a
pick (Gen SimpleTx -> PropertyM IO SimpleTx)
-> Gen SimpleTx -> PropertyM IO SimpleTx
forall a b. (a -> b) -> a -> b
$ Integer -> SimpleTx
aValidTx (Integer -> SimpleTx) -> Gen Integer -> Gen SimpleTx
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> Gen Integer
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 :: Secret (SigningKey HydraKey)
signingKey = Secret (SigningKey HydraKey)
aliceSk
            , $sel:otherParties:Environment :: [Party]
otherParties = []
            , $sel:contestationPeriod:Environment :: ContestationPeriod
contestationPeriod = ContestationPeriod
defaultContestationPeriod
            , $sel:depositPeriod:Environment :: DepositPeriod
depositPeriod = DepositPeriod
defaultDepositPeriod
            , $sel:depositActivation:Environment :: DepositPeriod
depositActivation = DepositPeriod
defaultDepositActivation
            , $sel:unsyncedPeriod:Environment :: UnsyncedPeriod
unsyncedPeriod = UnsyncedPeriod
defaultUnsyncedPeriod
            , $sel:participants:Environment :: [OnChainId]
participants = [Party -> OnChainId
deriveOnChainId Party
party]
            , $sel:configuredPeers:Environment :: Text
configuredPeers = Text
""
            }
    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 Integer SimpleTx
Map (TxIdType SimpleTx) SimpleTx
forall a. Monoid a => a
mempty
        , $sel:localTxs:CoordinatedHeadState :: Seq SimpleTx
localTxs = Seq SimpleTx
forall a. Monoid a => a
mempty
        , $sel:confirmedSnapshot:CoordinatedHeadState :: ConfirmedSnapshot SimpleTx
confirmedSnapshot = ConfirmedSnapshot SimpleTx
sn
        , SeenSnapshot SimpleTx
$sel:seenSnapshot:CoordinatedHeadState :: SeenSnapshot SimpleTx
seenSnapshot :: SeenSnapshot SimpleTx
seenSnapshot
        , $sel:currentDepositTxId:CoordinatedHeadState :: Maybe (TxIdType SimpleTx)
currentDepositTxId = Maybe Integer
Maybe (TxIdType SimpleTx)
forall a. Maybe a
Nothing
        , $sel:decommitTx:CoordinatedHeadState :: Maybe SimpleTx
decommitTx = Maybe SimpleTx
forall a. Maybe a
Nothing
        , SnapshotVersion
$sel:version:CoordinatedHeadState :: SnapshotVersion
version :: SnapshotVersion
version
        }
    s0 :: NodeState SimpleTx
s0 = [Party] -> CoordinatedHeadState SimpleTx -> NodeState SimpleTx
inOpenState' [Party
alice] CoordinatedHeadState SimpleTx
st
  UTCTime
now <- IO UTCTime -> PropertyM IO UTCTime
forall (m :: * -> *) a. Monad m => m a -> PropertyM m a
run (IO UTCTime -> PropertyM IO UTCTime)
-> IO UTCTime -> PropertyM IO UTCTime
forall a b. (a -> b) -> a -> b
$ ChainSlot -> IO UTCTime
forall (m :: * -> *).
(MonadFail m, MonadTime m) =>
ChainSlot -> m UTCTime
nowFromSlot (ChainPointTime -> ChainSlot
currentSlot (ChainPointTime -> ChainSlot)
-> (NodeState SimpleTx -> ChainPointTime)
-> NodeState SimpleTx
-> ChainSlot
forall b c a. (b -> c) -> (a -> b) -> a -> c
. NodeState SimpleTx -> ChainPointTime
forall tx. NodeState tx -> ChainPointTime
chainPointTime (NodeState SimpleTx -> ChainSlot)
-> NodeState SimpleTx -> ChainSlot
forall a b. (a -> b) -> a -> b
$ NodeState SimpleTx
s0)
  let outcome :: Outcome SimpleTx
outcome = Environment
-> Ledger SimpleTx
-> UTCTime
-> NodeState SimpleTx
-> Input SimpleTx
-> Outcome SimpleTx
forall tx.
IsChainState tx =>
Environment
-> Ledger tx -> UTCTime -> NodeState tx -> Input tx -> Outcome tx
update Environment
aliceEnv Ledger SimpleTx
simpleLedger UTCTime
now NodeState SimpleTx
s0 (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. IsTx 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 IO Property
forall a. a -> PropertyM IO a
forall (f :: * -> *) a. Applicative f => a -> f a
pure (Property -> PropertyM IO Property)
-> Property -> PropertyM IO 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 (TxIdType SimpleTx)
-> Message SimpleTx
forall tx.
SnapshotVersion
-> SnapshotNumber
-> [TxIdType tx]
-> Maybe tx
-> Maybe (TxIdType 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 Integer
Maybe (TxIdType 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

testSnapshot ::
  forall tx.
  IsTx tx =>
  SnapshotNumber ->
  SnapshotVersion ->
  [tx] ->
  UTxOType tx ->
  Snapshot tx
testSnapshot :: forall tx.
IsTx tx =>
SnapshotNumber
-> SnapshotVersion -> [tx] -> UTxOType tx -> Snapshot tx
testSnapshot SnapshotNumber
number SnapshotVersion
version [tx]
confirmed UTxOType tx
utxo =
  let accumulator :: HydraAccumulator
accumulator = UTxOType tx -> HydraAccumulator
forall tx. IsTx tx => UTxOType tx -> HydraAccumulator
Accumulator.buildFromUTxO UTxOType tx
utxo
   in Snapshot
        { $sel:headId:Snapshot :: HeadId
headId = HeadId
testHeadId
        , SnapshotVersion
version :: SnapshotVersion
$sel:version:Snapshot :: SnapshotVersion
version
        , SnapshotNumber
$sel:number:Snapshot :: SnapshotNumber
number :: SnapshotNumber
number
        , [tx]
confirmed :: [tx]
$sel:confirmed:Snapshot :: [tx]
confirmed
        , UTxOType tx
utxo :: UTxOType tx
$sel:utxo:Snapshot :: UTxOType tx
utxo
        , $sel:utxoToCommit:Snapshot :: Maybe (UTxOType tx)
utxoToCommit = Maybe (UTxOType tx)
forall a. Monoid a => a
mempty
        , $sel:utxoToDecommit:Snapshot :: Maybe (UTxOType tx)
utxoToDecommit = Maybe (UTxOType tx)
forall a. Monoid a => a
mempty
        , $sel:depositTxId:Snapshot :: Maybe (TxIdType tx)
depositTxId = Maybe (TxIdType tx)
forall a. Maybe a
Nothing
        , HydraAccumulator
$sel:accumulator:Snapshot :: HydraAccumulator
accumulator :: HydraAccumulator
accumulator
        }