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

-- | Unit tests of the the protocol logic in 'HeadLogic'. These are very fine
-- grained and specific to individual steps in the protocol. More high-level of
-- the protocol logic, especially between multiple parties can be found in
-- 'Hydra.BehaviorSpec'.
module Hydra.HeadLogicSpec where

import Hydra.Prelude
import Test.Hydra.Prelude

import Cardano.Api.UTxO qualified as UTxO
import Cardano.Ledger.Api (bodyTxL, inputsTxBodyL)
import Control.Lens ((.~))
import Data.List qualified as List
import Data.Map (notMember)
import Data.Set qualified as Set
import Hydra.API.ServerOutput (DecommitInvalidReason (..), ServerOutput (..))
import Hydra.Cardano.Api (fromLedgerTx, genTxIn, mkVkAddress, toLedgerTx, txOutValue, unSlotNo, pattern TxValidityUpperBound)
import Hydra.Chain (
  ChainEvent (..),
  OnChainTx (..),
  PostChainTx (CollectComTx, ContestTx),
 )
import Hydra.Chain.ChainState (ChainSlot (..), IsChainState)
import Hydra.Chain.Direct.State ()
import Hydra.HeadLogic (
  ClosedState (..),
  CoordinatedHeadState (..),
  Effect (..),
  HeadState (..),
  IdleState (..),
  InitialState (..),
  Input (..),
  LogicError (..),
  OpenState (..),
  Outcome (..),
  RequirementFailure (..),
  TTL,
  WaitReason (..),
  aggregateState,
  cause,
  defaultTTL,
  update,
 )
import Hydra.HeadLogic.State (SeenSnapshot (..), getHeadParameters)
import Hydra.Ledger (Ledger (..), ValidationError (..))
import Hydra.Ledger.Cardano (cardanoLedger, mkRangedTx)
import Hydra.Ledger.Simple (SimpleChainState (..), SimpleTx (..), aValidTx, simpleLedger, utxoRef, utxoRefs)
import Hydra.Network.Message (Connectivity, Message (..), NetworkEvent (..))
import Hydra.Options (defaultContestationPeriod)
import Hydra.Prelude qualified as Prelude
import Hydra.Tx.Crypto (generateSigningKey, sign)
import Hydra.Tx.Crypto qualified as Crypto
import Hydra.Tx.Environment (Environment (..))
import Hydra.Tx.HeadParameters (HeadParameters (..))
import Hydra.Tx.IsTx (IsTx (..))
import Hydra.Tx.Party (Party (..))
import Hydra.Tx.Snapshot (ConfirmedSnapshot (..), Snapshot (..), SnapshotNumber, SnapshotVersion, getSnapshot)
import Test.Hydra.Node.Fixture qualified as Fixture
import Test.Hydra.Tx.Fixture (alice, aliceSk, bob, bobSk, carol, carolSk, deriveOnChainId, testHeadId, testHeadSeed)
import Test.Hydra.Tx.Gen (genKeyPair, genOutput)
import Test.QuickCheck (Property, counterexample, elements, forAll, oneof, shuffle, suchThat)
import Test.QuickCheck.Monadic (assert, monadicIO, pick, run)

spec :: Spec
spec :: Spec
spec =
  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]
        bobEnv :: Environment
bobEnv =
          Environment
            { $sel:party:Environment :: Party
party = Party
bob
            , $sel:signingKey:Environment :: SigningKey HydraKey
signingKey = SigningKey HydraKey
bobSk
            , $sel:otherParties:Environment :: [Party]
otherParties = [Party
alice, Party
carol]
            , $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
            }
        aliceEnv :: Environment
aliceEnv =
          Environment
            { $sel:party:Environment :: Party
party = Party
alice
            , $sel:signingKey:Environment :: SigningKey HydraKey
signingKey = SigningKey HydraKey
aliceSk
            , $sel:otherParties:Environment :: [Party]
otherParties = [Party
bob, Party
carol]
            , $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
            }

    String -> Spec -> Spec
forall a. HasCallStack => String -> SpecWith a -> SpecWith a
describe String
"Coordinated Head Protocol" (Spec -> Spec) -> Spec -> Spec
forall a b. (a -> b) -> a -> b
$ do
      let ledger :: Ledger SimpleTx
ledger = Ledger SimpleTx
simpleLedger

      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 :: [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 UTxOType SimpleTx
forall a. Monoid a => a
mempty
              , $sel:seenSnapshot:CoordinatedHeadState :: SeenSnapshot SimpleTx
seenSnapshot = SeenSnapshot SimpleTx
forall tx. SeenSnapshot tx
NoSeenSnapshot
              , $sel:decommitTx:CoordinatedHeadState :: Maybe SimpleTx
decommitTx = Maybe SimpleTx
forall a. Maybe a
Nothing
              , $sel:version:CoordinatedHeadState :: SnapshotVersion
version = SnapshotVersion
0
              }

      String -> IO () -> SpecWith (Arg (IO ()))
forall a.
(HasCallStack, Example a) =>
String -> a -> SpecWith (Arg a)
it String
"reports if a requested tx is expired" (IO () -> SpecWith (Arg (IO ())))
-> IO () -> SpecWith (Arg (IO ()))
forall a b. (a -> b) -> a -> b
$ do
        let inputs :: UTxOType SimpleTx
inputs = SimpleId -> UTxOType SimpleTx
utxoRef SimpleId
1
            tx :: SimpleTx
tx = SimpleId -> UTxOType SimpleTx -> UTxOType SimpleTx -> SimpleTx
SimpleTx SimpleId
2 Set SimpleTxOut
UTxOType SimpleTx
inputs Set SimpleTxOut
UTxOType SimpleTx
forall a. Monoid a => a
mempty
            ttl :: Natural
ttl = Natural
0
            reqTx :: Input SimpleTx
reqTx = Natural -> NetworkEvent (Message SimpleTx) -> Input SimpleTx
forall tx. Natural -> NetworkEvent (Message tx) -> Input tx
NetworkInput Natural
ttl (NetworkEvent (Message SimpleTx) -> Input SimpleTx)
-> NetworkEvent (Message SimpleTx) -> Input SimpleTx
forall a b. (a -> b) -> a -> b
$ ReceivedMessage{$sel:sender:ConnectivityEvent :: Party
sender = Party
alice, $sel:msg:ConnectivityEvent :: Message SimpleTx
msg = SimpleTx -> Message SimpleTx
forall tx. tx -> Message tx
ReqTx SimpleTx
tx}
            s0 :: HeadState SimpleTx
s0 = [Party] -> HeadState SimpleTx
inOpenState [Party]
threeParties

        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
ledger HeadState SimpleTx
s0 Input SimpleTx
reqTx Outcome SimpleTx -> (Effect SimpleTx -> Bool) -> IO ()
forall tx.
(HasCallStack, IsChainState tx) =>
Outcome tx -> (Effect tx -> Bool) -> IO ()
`hasEffectSatisfying` \case
          ClientEffect TxInvalid{SimpleTx
transaction :: SimpleTx
$sel:transaction:PeerConnected :: forall tx. ServerOutput tx -> tx
transaction} -> SimpleTx
transaction SimpleTx -> SimpleTx -> Bool
forall a. Eq a => a -> a -> Bool
== SimpleTx
tx
          Effect SimpleTx
_ -> Bool
False

      String -> IO () -> SpecWith (Arg (IO ()))
forall a.
(HasCallStack, Example a) =>
String -> a -> SpecWith (Arg a)
it String
"waits if a requested tx is not (yet) applicable" (IO () -> SpecWith (Arg (IO ())))
-> IO () -> SpecWith (Arg (IO ()))
forall a b. (a -> b) -> a -> b
$ do
        let reqTx :: Input SimpleTx
reqTx = 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 -> Message SimpleTx) -> SimpleTx -> Message SimpleTx
forall a b. (a -> b) -> a -> b
$ SimpleId -> UTxOType SimpleTx -> UTxOType SimpleTx -> SimpleTx
SimpleTx SimpleId
2 Set SimpleTxOut
UTxOType SimpleTx
inputs Set SimpleTxOut
UTxOType SimpleTx
forall a. Monoid a => a
mempty
            inputs :: UTxOType SimpleTx
inputs = SimpleId -> UTxOType SimpleTx
utxoRef SimpleId
1
            s0 :: HeadState SimpleTx
s0 = [Party] -> HeadState SimpleTx
inOpenState [Party]
threeParties

        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
ledger HeadState SimpleTx
s0 Input SimpleTx
reqTx
          Outcome SimpleTx -> WaitReason SimpleTx -> IO ()
forall tx.
(HasCallStack, IsChainState tx) =>
Outcome tx -> WaitReason tx -> IO ()
`assertWait` ValidationError -> WaitReason SimpleTx
forall tx. ValidationError -> WaitReason tx
WaitOnNotApplicableTx (Text -> ValidationError
ValidationError Text
"cannot apply transaction")

      String -> IO () -> SpecWith (Arg (IO ()))
forall a.
(HasCallStack, Example a) =>
String -> a -> SpecWith (Arg a)
it String
"confirms snapshot given it receives AckSn from all parties" (IO () -> SpecWith (Arg (IO ())))
-> IO () -> SpecWith (Arg (IO ()))
forall a b. (a -> b) -> a -> b
$ do
        let reqSn :: Input tx
reqSn = Message tx -> Input tx
forall tx. Message tx -> Input tx
receiveMessage (Message tx -> Input tx) -> Message tx -> Input tx
forall a b. (a -> b) -> a -> b
$ SnapshotVersion
-> SnapshotNumber -> [TxIdType tx] -> Maybe tx -> Message tx
forall tx.
SnapshotVersion
-> SnapshotNumber -> [TxIdType tx] -> Maybe tx -> Message tx
ReqSn SnapshotVersion
0 SnapshotNumber
1 [] Maybe tx
forall a. Maybe a
Nothing
            snapshot1 :: Snapshot SimpleTx
snapshot1 = HeadId
-> SnapshotVersion
-> SnapshotNumber
-> [TxIdType SimpleTx]
-> UTxOType SimpleTx
-> Maybe (UTxOType SimpleTx)
-> Snapshot SimpleTx
forall tx.
HeadId
-> SnapshotVersion
-> SnapshotNumber
-> [TxIdType tx]
-> 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
            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
        HeadState SimpleTx
snapshotInProgress <- 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
ledger ([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 Input SimpleTx
forall {tx}. Input tx
reqSn
          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

        HeadState SimpleTx -> Maybe (Snapshot SimpleTx)
forall tx. HeadState tx -> Maybe (Snapshot tx)
getConfirmedSnapshot HeadState SimpleTx
snapshotInProgress Maybe (Snapshot SimpleTx) -> Maybe (Snapshot SimpleTx) -> IO ()
forall a. (HasCallStack, Show a, Eq a) => a -> a -> IO ()
`shouldBe` Snapshot SimpleTx -> Maybe (Snapshot SimpleTx)
forall a. a -> Maybe a
Just (SnapshotNumber
-> SnapshotVersion
-> [TxIdType SimpleTx]
-> UTxOType SimpleTx
-> Snapshot SimpleTx
forall tx.
Monoid (UTxOType tx) =>
SnapshotNumber
-> SnapshotVersion -> [TxIdType tx] -> UTxOType tx -> Snapshot tx
testSnapshot SnapshotNumber
0 SnapshotVersion
0 [] Set SimpleTxOut
UTxOType SimpleTx
forall a. Monoid a => a
mempty)

        HeadState SimpleTx
snapshotConfirmed <-
          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
ledger HeadState SimpleTx
snapshotInProgress (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 (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
        HeadState SimpleTx -> Maybe (Snapshot SimpleTx)
forall tx. HeadState tx -> Maybe (Snapshot tx)
getConfirmedSnapshot HeadState SimpleTx
snapshotConfirmed Maybe (Snapshot SimpleTx) -> Maybe (Snapshot SimpleTx) -> IO ()
forall a. (HasCallStack, Show a, Eq a) => a -> a -> IO ()
`shouldBe` Snapshot SimpleTx -> Maybe (Snapshot SimpleTx)
forall a. a -> Maybe a
Just Snapshot SimpleTx
snapshot1

      String -> Spec -> Spec
forall a. HasCallStack => String -> SpecWith a -> SpecWith a
describe String
"ReqSn" (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
"prunes local txs in order" (IO () -> SpecWith (Arg (IO ())))
-> IO () -> SpecWith (Arg (IO ()))
forall a b. (a -> b) -> a -> b
$ do
          -- Given a list of transactions each depending on the previous. If a
          -- prefix gets snapshotted, the suffix still stays in the local txs.
          let tx1 :: SimpleTx
tx1 = SimpleId -> UTxOType SimpleTx -> UTxOType SimpleTx -> SimpleTx
SimpleTx SimpleId
1 Set SimpleTxOut
UTxOType SimpleTx
forall a. Monoid a => a
mempty (SimpleId -> UTxOType SimpleTx
utxoRef SimpleId
2) -- No inputs, requires no specific starting state
              tx2 :: SimpleTx
tx2 = SimpleId -> UTxOType SimpleTx -> UTxOType SimpleTx -> SimpleTx
SimpleTx SimpleId
2 (SimpleId -> UTxOType SimpleTx
utxoRef SimpleId
2) (SimpleId -> UTxOType SimpleTx
utxoRef SimpleId
3)
              tx3 :: SimpleTx
tx3 = SimpleId -> UTxOType SimpleTx -> UTxOType SimpleTx -> SimpleTx
SimpleTx SimpleId
3 (SimpleId -> UTxOType SimpleTx
utxoRef SimpleId
3) (SimpleId -> UTxOType SimpleTx
utxoRef SimpleId
4)
              s0 :: HeadState SimpleTx
s0 = [Party] -> HeadState SimpleTx
inOpenState [Party]
threeParties

          -- XXX: this is hiding unxpected 'Error' outcomes
          HeadState SimpleTx
s <- 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
ledger HeadState SimpleTx
s0 (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
tx1
            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
tx2
            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
tx3
            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
$ SnapshotVersion
-> SnapshotNumber
-> [TxIdType SimpleTx]
-> Maybe SimpleTx
-> Message SimpleTx
forall tx.
SnapshotVersion
-> SnapshotNumber -> [TxIdType tx] -> Maybe tx -> Message tx
ReqSn SnapshotVersion
0 SnapshotNumber
1 [TxIdType SimpleTx
1] Maybe SimpleTx
forall a. Maybe a
Nothing
            StateT (StepState SimpleTx) IO (HeadState SimpleTx)
forall tx (m :: * -> *).
MonadState (StepState tx) m =>
m (HeadState tx)
getState

          case HeadState SimpleTx
s of
            (Open OpenState{$sel:coordinatedHeadState:OpenState :: forall tx. OpenState tx -> CoordinatedHeadState tx
coordinatedHeadState = CoordinatedHeadState{[SimpleTx]
$sel:localTxs:CoordinatedHeadState :: forall tx. CoordinatedHeadState tx -> [tx]
localTxs :: [SimpleTx]
localTxs}}) -> do
              [SimpleTx]
localTxs [SimpleTx] -> [SimpleTx] -> IO ()
forall a. (HasCallStack, Show a, Eq a) => a -> a -> IO ()
`shouldBe` [SimpleTx
tx2, SimpleTx
tx3]
            HeadState SimpleTx
_ -> String -> IO ()
forall a. String -> IO a
forall (m :: * -> *) a. MonadFail m => String -> m a
fail String
"expected Open state"

      String -> Spec -> Spec
forall a. HasCallStack => String -> SpecWith a -> SpecWith a
describe String
"Decommit" (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
"observes DecommitRequested and ReqDec in an Open state" (IO () -> SpecWith (Arg (IO ())))
-> IO () -> SpecWith (Arg (IO ()))
forall a b. (a -> b) -> a -> b
$ do
          let outputs :: UTxOType SimpleTx
outputs = SimpleId -> UTxOType SimpleTx
utxoRef SimpleId
1
              input :: Input SimpleTx
input = Message SimpleTx -> Input SimpleTx
forall tx. Message tx -> Input tx
receiveMessage ReqDec{$sel:transaction:ReqTx :: SimpleTx
transaction = SimpleId -> UTxOType SimpleTx -> UTxOType SimpleTx -> SimpleTx
SimpleTx SimpleId
1 Set SimpleTxOut
UTxOType SimpleTx
forall a. Monoid a => a
mempty Set SimpleTxOut
UTxOType SimpleTx
outputs}
              st :: HeadState SimpleTx
st = [Party] -> HeadState SimpleTx
inOpenState [Party]
threeParties

          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
ledger HeadState SimpleTx
st Input SimpleTx
input
            Outcome SimpleTx -> (Effect SimpleTx -> Bool) -> IO ()
forall tx.
(HasCallStack, IsChainState tx) =>
Outcome tx -> (Effect tx -> Bool) -> IO ()
`hasEffectSatisfying` \case
              ClientEffect DecommitRequested{HeadId
headId :: HeadId
$sel:headId:PeerConnected :: forall tx. ServerOutput tx -> HeadId
headId, UTxOType SimpleTx
utxoToDecommit :: UTxOType SimpleTx
$sel:utxoToDecommit:PeerConnected :: forall tx. ServerOutput tx -> UTxOType tx
utxoToDecommit} ->
                HeadId
headId HeadId -> HeadId -> Bool
forall a. Eq a => a -> a -> Bool
== HeadId
testHeadId Bool -> Bool -> Bool
&& Set SimpleTxOut
UTxOType SimpleTx
utxoToDecommit Set SimpleTxOut -> Set SimpleTxOut -> Bool
forall a. Eq a => a -> a -> Bool
== Set SimpleTxOut
outputs
              Effect SimpleTx
_ -> Bool
False

        String -> Property -> SpecWith (Arg Property)
forall a.
(HasCallStack, Example a) =>
String -> a -> SpecWith (Arg a)
it String
"ignores ReqDec when not in Open state" (Property -> SpecWith (Arg Property))
-> Property -> SpecWith (Arg Property)
forall a b. (a -> b) -> a -> b
$ PropertyM IO (IO ()) -> Property
forall a. Testable a => PropertyM IO a -> Property
monadicIO (PropertyM IO (IO ()) -> Property)
-> PropertyM IO (IO ()) -> Property
forall a b. (a -> b) -> a -> b
$ do
          let reqDec :: Message SimpleTx
reqDec = ReqDec{$sel:transaction:ReqTx :: SimpleTx
transaction = SimpleId -> UTxOType SimpleTx -> UTxOType SimpleTx -> SimpleTx
SimpleTx SimpleId
1 Set SimpleTxOut
UTxOType SimpleTx
forall a. Monoid a => a
mempty (SimpleId -> UTxOType SimpleTx
utxoRef SimpleId
1)}
          let input :: Input SimpleTx
input = Message SimpleTx -> Input SimpleTx
forall tx. Message tx -> Input tx
receiveMessage Message SimpleTx
reqDec
          HeadState SimpleTx
st <- Gen (HeadState SimpleTx) -> PropertyM IO (HeadState SimpleTx)
forall (m :: * -> *) a. Monad m => Gen a -> PropertyM m a
pickBlind (Gen (HeadState SimpleTx) -> PropertyM IO (HeadState SimpleTx))
-> Gen (HeadState SimpleTx) -> PropertyM IO (HeadState SimpleTx)
forall a b. (a -> b) -> a -> b
$ [HeadState SimpleTx] -> Gen (HeadState SimpleTx)
forall a. [a] -> Gen a
elements [[Party] -> HeadState SimpleTx
inInitialState [Party]
threeParties, HeadState SimpleTx
inIdleState, [Party] -> HeadState SimpleTx
inClosedState [Party]
threeParties]
          IO () -> PropertyM IO (IO ())
forall a. a -> PropertyM IO a
forall (f :: * -> *) a. Applicative f => a -> f a
pure (IO () -> PropertyM IO (IO ())) -> IO () -> PropertyM IO (IO ())
forall a b. (a -> b) -> a -> b
$
            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
ledger HeadState SimpleTx
st Input SimpleTx
input
              Outcome SimpleTx -> Outcome SimpleTx -> IO ()
forall a. (HasCallStack, Show a, Eq a) => a -> a -> IO ()
`shouldNotBe` Effect SimpleTx -> Outcome SimpleTx
forall tx. Effect tx -> Outcome tx
cause (Message SimpleTx -> Effect SimpleTx
forall tx. Message tx -> Effect tx
NetworkEffect Message SimpleTx
reqDec)

        String -> IO () -> SpecWith (Arg (IO ()))
forall a.
(HasCallStack, Example a) =>
String -> a -> SpecWith (Arg a)
it String
"reports if a requested decommit tx is expired" (IO () -> SpecWith (Arg (IO ())))
-> IO () -> SpecWith (Arg (IO ()))
forall a b. (a -> b) -> a -> b
$ do
          let inputs :: UTxOType SimpleTx
inputs = SimpleId -> UTxOType SimpleTx
utxoRef SimpleId
1
              decommitTx :: SimpleTx
decommitTx = SimpleId -> UTxOType SimpleTx -> UTxOType SimpleTx -> SimpleTx
SimpleTx SimpleId
1 Set SimpleTxOut
UTxOType SimpleTx
forall a. Monoid a => a
mempty Set SimpleTxOut
UTxOType SimpleTx
inputs
              ttl :: Natural
ttl = Natural
0
              reqDec :: Message SimpleTx
reqDec = ReqDec{$sel:transaction:ReqTx :: SimpleTx
transaction = SimpleTx
decommitTx}
              reqDecEvent :: Input SimpleTx
reqDecEvent = Natural -> NetworkEvent (Message SimpleTx) -> Input SimpleTx
forall tx. Natural -> NetworkEvent (Message tx) -> Input tx
NetworkInput Natural
ttl (NetworkEvent (Message SimpleTx) -> Input SimpleTx)
-> NetworkEvent (Message SimpleTx) -> Input SimpleTx
forall a b. (a -> b) -> a -> b
$ ReceivedMessage{$sel:sender:ConnectivityEvent :: Party
sender = Party
alice, $sel:msg:ConnectivityEvent :: Message SimpleTx
msg = Message SimpleTx
reqDec}
              decommitTxInFlight :: SimpleTx
decommitTxInFlight = SimpleId -> UTxOType SimpleTx -> UTxOType SimpleTx -> SimpleTx
SimpleTx SimpleId
2 Set SimpleTxOut
UTxOType SimpleTx
forall a. Monoid a => a
mempty (SimpleId -> UTxOType SimpleTx
utxoRef SimpleId
2)
              s0 :: HeadState SimpleTx
s0 =
                [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
                    { decommitTx = Just decommitTxInFlight
                    }
          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
ledger HeadState SimpleTx
s0 Input SimpleTx
reqDecEvent Outcome SimpleTx -> (Effect SimpleTx -> Bool) -> IO ()
forall tx.
(HasCallStack, IsChainState tx) =>
Outcome tx -> (Effect tx -> Bool) -> IO ()
`hasEffectSatisfying` \case
            ClientEffect DecommitInvalid{$sel:decommitTx:PeerConnected :: forall tx. ServerOutput tx -> tx
decommitTx = SimpleTx
invalidTx} -> SimpleTx
invalidTx SimpleTx -> SimpleTx -> Bool
forall a. Eq a => a -> a -> Bool
== SimpleTx
decommitTx
            Effect SimpleTx
_ -> Bool
False

        String -> IO () -> SpecWith (Arg (IO ()))
forall a.
(HasCallStack, Example a) =>
String -> a -> SpecWith (Arg a)
it String
"wait for second decommit when another one is in flight" (IO () -> SpecWith (Arg (IO ())))
-> IO () -> SpecWith (Arg (IO ()))
forall a b. (a -> b) -> a -> b
$
          do
            let decommitTx1 :: SimpleTx
decommitTx1 = SimpleId -> UTxOType SimpleTx -> UTxOType SimpleTx -> SimpleTx
SimpleTx SimpleId
1 Set SimpleTxOut
UTxOType SimpleTx
forall a. Monoid a => a
mempty (SimpleId -> UTxOType SimpleTx
utxoRef SimpleId
1)
                decommitTx2 :: SimpleTx
decommitTx2 = SimpleId -> UTxOType SimpleTx -> UTxOType SimpleTx -> SimpleTx
SimpleTx SimpleId
2 Set SimpleTxOut
UTxOType SimpleTx
forall a. Monoid a => a
mempty (SimpleId -> UTxOType SimpleTx
utxoRef SimpleId
2)
                s0 :: HeadState SimpleTx
s0 = [Party] -> HeadState SimpleTx
inOpenState [Party]
threeParties

            HeadState SimpleTx
s1 <- 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
aliceEnv Ledger SimpleTx
ledger HeadState SimpleTx
s0 (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
$ Party -> Message SimpleTx -> Input SimpleTx
forall tx. Party -> Message tx -> Input tx
receiveMessageFrom Party
alice ReqDec{$sel:transaction:ReqTx :: SimpleTx
transaction = SimpleTx
decommitTx1}
              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
ledger HeadState SimpleTx
s1 (Party -> Message SimpleTx -> Input SimpleTx
forall tx. Party -> Message tx -> Input tx
receiveMessageFrom Party
bob ReqDec{$sel:transaction:ReqTx :: SimpleTx
transaction = SimpleTx
decommitTx2})
              Outcome SimpleTx -> WaitReason SimpleTx -> IO ()
forall tx.
(HasCallStack, IsChainState tx) =>
Outcome tx -> WaitReason tx -> IO ()
`assertWait` WaitOnNotApplicableDecommitTx
                { $sel:notApplicableReason:WaitOnNotApplicableTx :: DecommitInvalidReason SimpleTx
notApplicableReason =
                    DecommitAlreadyInFlight
                      { $sel:otherDecommitTxId:DecommitTxInvalid :: TxIdType SimpleTx
otherDecommitTxId = SimpleTx -> TxIdType SimpleTx
forall tx. IsTx tx => tx -> TxIdType tx
txId SimpleTx
decommitTx1
                      }
                }

        String -> IO () -> SpecWith (Arg (IO ()))
forall a.
(HasCallStack, Example a) =>
String -> a -> SpecWith (Arg a)
it String
"waits if a requested decommit tx is not (yet) applicable" (IO () -> SpecWith (Arg (IO ())))
-> IO () -> SpecWith (Arg (IO ()))
forall a b. (a -> b) -> a -> b
$ do
          let decommitTx :: SimpleTx
decommitTx = SimpleTx{$sel:txSimpleId:SimpleTx :: SimpleId
txSimpleId = SimpleId
1, $sel:txInputs:SimpleTx :: UTxOType SimpleTx
txInputs = [SimpleId] -> UTxOType SimpleTx
utxoRefs [SimpleId
2], $sel:txOutputs:SimpleTx :: UTxOType SimpleTx
txOutputs = [SimpleId] -> UTxOType SimpleTx
utxoRefs [SimpleId
4]}
              s0 :: HeadState SimpleTx
s0 = [Party] -> HeadState SimpleTx
inOpenState [Party]
threeParties
              reqDecEvent :: Input SimpleTx
reqDecEvent = Message SimpleTx -> Input SimpleTx
forall tx. Message tx -> Input tx
receiveMessage ReqDec{$sel:transaction:ReqTx :: SimpleTx
transaction = SimpleTx
decommitTx}

          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
ledger HeadState SimpleTx
s0 Input SimpleTx
reqDecEvent
            Outcome SimpleTx -> WaitReason SimpleTx -> IO ()
forall tx.
(HasCallStack, IsChainState tx) =>
Outcome tx -> WaitReason tx -> IO ()
`assertWait` DecommitInvalidReason SimpleTx -> WaitReason SimpleTx
forall tx. DecommitInvalidReason tx -> WaitReason tx
WaitOnNotApplicableDecommitTx (UTxOType SimpleTx
-> ValidationError -> DecommitInvalidReason SimpleTx
forall tx.
UTxOType tx -> ValidationError -> DecommitInvalidReason tx
DecommitTxInvalid Set SimpleTxOut
UTxOType SimpleTx
forall a. Monoid a => a
mempty (Text -> ValidationError
ValidationError Text
"cannot apply transaction"))

        String -> IO () -> SpecWith (Arg (IO ()))
forall a.
(HasCallStack, Example a) =>
String -> a -> SpecWith (Arg a)
it String
"updates decommitTx on valid ReqDec" (IO () -> SpecWith (Arg (IO ())))
-> IO () -> SpecWith (Arg (IO ()))
forall a b. (a -> b) -> a -> b
$ do
          let decommitTx' :: SimpleTx
decommitTx' = SimpleId -> UTxOType SimpleTx -> UTxOType SimpleTx -> SimpleTx
SimpleTx SimpleId
1 Set SimpleTxOut
UTxOType SimpleTx
forall a. Monoid a => a
mempty (SimpleId -> UTxOType SimpleTx
utxoRef SimpleId
1)
          let reqDec :: Message SimpleTx
reqDec = ReqDec{$sel:transaction:ReqTx :: SimpleTx
transaction = SimpleTx
decommitTx'}
              reqDecEvent :: Input SimpleTx
reqDecEvent = Message SimpleTx -> Input SimpleTx
forall tx. Message tx -> Input tx
receiveMessage Message SimpleTx
reqDec
              s0 :: HeadState SimpleTx
s0 = [Party] -> HeadState SimpleTx
inOpenState [Party]
threeParties

          HeadState SimpleTx
s0 HeadState SimpleTx -> (HeadState SimpleTx -> Bool) -> IO ()
forall a. (HasCallStack, Show a) => a -> (a -> Bool) -> IO ()
`shouldSatisfy` \case
            (Open OpenState{$sel:coordinatedHeadState:OpenState :: forall tx. OpenState tx -> CoordinatedHeadState tx
coordinatedHeadState = CoordinatedHeadState{Maybe SimpleTx
$sel:decommitTx:CoordinatedHeadState :: forall tx. CoordinatedHeadState tx -> Maybe tx
decommitTx :: Maybe SimpleTx
decommitTx}}) -> Maybe SimpleTx -> Bool
forall a. Maybe a -> Bool
isNothing Maybe SimpleTx
decommitTx
            HeadState SimpleTx
_ -> Bool
False

          HeadState SimpleTx
s1 <- 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
aliceEnv Ledger SimpleTx
ledger HeadState SimpleTx
s0 (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
reqDecEvent
            StateT (StepState SimpleTx) IO (HeadState SimpleTx)
forall tx (m :: * -> *).
MonadState (StepState tx) m =>
m (HeadState tx)
getState

          HeadState SimpleTx
s1 HeadState SimpleTx -> (HeadState SimpleTx -> Bool) -> IO ()
forall a. (HasCallStack, Show a) => a -> (a -> Bool) -> IO ()
`shouldSatisfy` \case
            (Open OpenState{$sel:coordinatedHeadState:OpenState :: forall tx. OpenState tx -> CoordinatedHeadState tx
coordinatedHeadState = CoordinatedHeadState{Maybe SimpleTx
$sel:decommitTx:CoordinatedHeadState :: forall tx. CoordinatedHeadState tx -> Maybe tx
decommitTx :: Maybe SimpleTx
decommitTx}}) -> Maybe SimpleTx
decommitTx Maybe SimpleTx -> Maybe SimpleTx -> Bool
forall a. Eq a => a -> a -> Bool
== SimpleTx -> Maybe SimpleTx
forall a. a -> Maybe a
Just SimpleTx
decommitTx'
            HeadState SimpleTx
_ -> Bool
False

          -- running the 'ReqDec' again should not alter the recorded state
          HeadState SimpleTx
s2 <- 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
aliceEnv Ledger SimpleTx
ledger HeadState SimpleTx
s1 (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
reqDecEvent
            StateT (StepState SimpleTx) IO (HeadState SimpleTx)
forall tx (m :: * -> *).
MonadState (StepState tx) m =>
m (HeadState tx)
getState

          HeadState SimpleTx
s2 HeadState SimpleTx -> (HeadState SimpleTx -> Bool) -> IO ()
forall a. (HasCallStack, Show a) => a -> (a -> Bool) -> IO ()
`shouldSatisfy` \case
            (Open OpenState{$sel:coordinatedHeadState:OpenState :: forall tx. OpenState tx -> CoordinatedHeadState tx
coordinatedHeadState = CoordinatedHeadState{Maybe SimpleTx
$sel:decommitTx:CoordinatedHeadState :: forall tx. CoordinatedHeadState tx -> Maybe tx
decommitTx :: Maybe SimpleTx
decommitTx}}) -> Maybe SimpleTx
decommitTx Maybe SimpleTx -> Maybe SimpleTx -> Bool
forall a. Eq a => a -> a -> Bool
== SimpleTx -> Maybe SimpleTx
forall a. a -> Maybe a
Just SimpleTx
decommitTx'
            HeadState SimpleTx
_ -> Bool
False

        String -> IO () -> SpecWith (Arg (IO ()))
forall a.
(HasCallStack, Example a) =>
String -> a -> SpecWith (Arg a)
it String
"emits ReqSn on valid RecDec" (IO () -> SpecWith (Arg (IO ())))
-> IO () -> SpecWith (Arg (IO ()))
forall a b. (a -> b) -> a -> b
$ do
          let localUTxO :: UTxOType SimpleTx
localUTxO = [SimpleId] -> UTxOType SimpleTx
utxoRefs [SimpleId
2]
          let decommitTx' :: SimpleTx
decommitTx' = SimpleTx{$sel:txSimpleId:SimpleTx :: SimpleId
txSimpleId = SimpleId
1, $sel:txInputs:SimpleTx :: UTxOType SimpleTx
txInputs = Set SimpleTxOut
UTxOType SimpleTx
localUTxO, $sel:txOutputs:SimpleTx :: UTxOType SimpleTx
txOutputs = [SimpleId] -> UTxOType SimpleTx
utxoRefs [SimpleId
4]}
          let s0 :: HeadState SimpleTx
s0 = [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{localUTxO}

          HeadState SimpleTx
s0 HeadState SimpleTx -> (HeadState SimpleTx -> Bool) -> IO ()
forall a. (HasCallStack, Show a) => a -> (a -> Bool) -> IO ()
`shouldSatisfy` \case
            (Open OpenState{$sel:coordinatedHeadState:OpenState :: forall tx. OpenState tx -> CoordinatedHeadState tx
coordinatedHeadState = CoordinatedHeadState{Maybe SimpleTx
$sel:decommitTx:CoordinatedHeadState :: forall tx. CoordinatedHeadState tx -> Maybe tx
decommitTx :: Maybe SimpleTx
decommitTx}}) -> Maybe SimpleTx -> Bool
forall a. Maybe a -> Bool
isNothing Maybe SimpleTx
decommitTx
            HeadState SimpleTx
_ -> Bool
False

          let reqDecEvent :: Input SimpleTx
reqDecEvent = Message SimpleTx -> Input SimpleTx
forall tx. Message tx -> Input tx
receiveMessage ReqDec{$sel:transaction:ReqTx :: SimpleTx
transaction = SimpleTx
decommitTx'}

          let s1 :: Outcome SimpleTx
s1 = 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
ledger HeadState SimpleTx
s0 Input SimpleTx
reqDecEvent

          let reqSn :: Message SimpleTx
reqSn = ReqSn{$sel:snapshotVersion:ReqTx :: SnapshotVersion
snapshotVersion = SnapshotVersion
0, $sel:snapshotNumber:ReqTx :: SnapshotNumber
snapshotNumber = SnapshotNumber
1, $sel:transactionIds:ReqTx :: [TxIdType SimpleTx]
transactionIds = [], $sel:decommitTx:ReqTx :: Maybe SimpleTx
decommitTx = SimpleTx -> Maybe SimpleTx
forall a. a -> Maybe a
Just SimpleTx
decommitTx'}
          Outcome SimpleTx
s1 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 Message SimpleTx
reqSn

      String -> Spec -> Spec
forall a. HasCallStack => String -> SpecWith a -> SpecWith a
describe String
"Tracks Transaction Ids" (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
"keeps transactions in allTxs given it receives a ReqTx" (IO () -> SpecWith (Arg (IO ())))
-> IO () -> SpecWith (Arg (IO ()))
forall a b. (a -> b) -> a -> b
$ do
          let s0 :: HeadState SimpleTx
s0 = [Party] -> HeadState SimpleTx
inOpenState [Party]
threeParties
              t1 :: SimpleTx
t1 = SimpleId -> UTxOType SimpleTx -> UTxOType SimpleTx -> SimpleTx
SimpleTx SimpleId
1 Set SimpleTxOut
UTxOType SimpleTx
forall a. Monoid a => a
mempty (SimpleId -> UTxOType SimpleTx
utxoRef SimpleId
1)

          HeadState SimpleTx
sa <- 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
ledger HeadState SimpleTx
s0 (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
t1
            StateT (StepState SimpleTx) IO (HeadState SimpleTx)
forall tx (m :: * -> *).
MonadState (StepState tx) m =>
m (HeadState tx)
getState

          HeadState SimpleTx
sa HeadState SimpleTx -> (HeadState SimpleTx -> Bool) -> IO ()
forall a. (HasCallStack, Show a) => a -> (a -> Bool) -> IO ()
`shouldSatisfy` \case
            (Open OpenState{$sel:coordinatedHeadState:OpenState :: forall tx. OpenState tx -> CoordinatedHeadState tx
coordinatedHeadState = CoordinatedHeadState{Map (TxIdType SimpleTx) SimpleTx
$sel:allTxs:CoordinatedHeadState :: forall tx. CoordinatedHeadState tx -> Map (TxIdType tx) tx
allTxs :: Map (TxIdType SimpleTx) SimpleTx
allTxs}}) -> SimpleTx -> TxIdType SimpleTx
forall tx. IsTx tx => tx -> TxIdType tx
txId SimpleTx
t1 Key (Map (TxIdType SimpleTx) SimpleTx)
-> Map (TxIdType SimpleTx) SimpleTx -> Bool
forall t. StaticMap t => Key t -> t -> Bool
`member` Map (TxIdType SimpleTx) SimpleTx
allTxs
            HeadState SimpleTx
_ -> Bool
False

        String -> IO () -> SpecWith (Arg (IO ()))
forall a.
(HasCallStack, Example a) =>
String -> a -> SpecWith (Arg a)
it String
"removes transactions in allTxs given it receives a ReqSn" (IO () -> SpecWith (Arg (IO ())))
-> IO () -> SpecWith (Arg (IO ()))
forall a b. (a -> b) -> a -> b
$ do
          let s0 :: HeadState SimpleTx
s0 = [Party] -> HeadState SimpleTx
inOpenState [Party]
threeParties
              t1 :: SimpleTx
t1 = SimpleId -> UTxOType SimpleTx -> UTxOType SimpleTx -> SimpleTx
SimpleTx SimpleId
1 Set SimpleTxOut
UTxOType SimpleTx
forall a. Monoid a => a
mempty (SimpleId -> UTxOType SimpleTx
utxoRef SimpleId
1)
              reqSn :: Input SimpleTx
reqSn = 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
-> Message SimpleTx
forall tx.
SnapshotVersion
-> SnapshotNumber -> [TxIdType tx] -> Maybe tx -> Message tx
ReqSn SnapshotVersion
0 SnapshotNumber
1 [TxIdType SimpleTx
1] Maybe SimpleTx
forall a. Maybe a
Nothing

          HeadState SimpleTx
s1 <- 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
ledger HeadState SimpleTx
s0 (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
t1
            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
reqSn
            StateT (StepState SimpleTx) IO (HeadState SimpleTx)
forall tx (m :: * -> *).
MonadState (StepState tx) m =>
m (HeadState tx)
getState

          HeadState SimpleTx
s1 HeadState SimpleTx -> (HeadState SimpleTx -> Bool) -> IO ()
forall a. (HasCallStack, Show a) => a -> (a -> Bool) -> IO ()
`shouldSatisfy` \case
            (Open OpenState{$sel:coordinatedHeadState:OpenState :: forall tx. OpenState tx -> CoordinatedHeadState tx
coordinatedHeadState = CoordinatedHeadState{Map (TxIdType SimpleTx) SimpleTx
$sel:allTxs:CoordinatedHeadState :: forall tx. CoordinatedHeadState tx -> Map (TxIdType tx) tx
allTxs :: Map (TxIdType SimpleTx) SimpleTx
allTxs}}) -> SimpleTx -> TxIdType SimpleTx
forall tx. IsTx tx => tx -> TxIdType tx
txId SimpleTx
t1 SimpleId -> Map SimpleId SimpleTx -> Bool
forall k a. Ord k => k -> Map k a -> Bool
`notMember` Map SimpleId SimpleTx
Map (TxIdType SimpleTx) SimpleTx
allTxs
            HeadState SimpleTx
_ -> Bool
False

        String -> IO () -> SpecWith (Arg (IO ()))
forall a.
(HasCallStack, Example a) =>
String -> a -> SpecWith (Arg a)
it String
"removes transactions from allTxs when included in a acked snapshot even when emitting a ReqSn" (IO () -> SpecWith (Arg (IO ())))
-> IO () -> SpecWith (Arg (IO ()))
forall a b. (a -> b) -> a -> b
$ do
          let t1 :: SimpleTx
t1 = SimpleId -> UTxOType SimpleTx -> UTxOType SimpleTx -> SimpleTx
SimpleTx SimpleId
1 Set SimpleTxOut
UTxOType SimpleTx
forall a. Monoid a => a
mempty (SimpleId -> UTxOType SimpleTx
utxoRef SimpleId
1)
              pendingTransaction :: SimpleTx
pendingTransaction = SimpleId -> UTxOType SimpleTx -> UTxOType SimpleTx -> SimpleTx
SimpleTx SimpleId
2 Set SimpleTxOut
UTxOType SimpleTx
forall a. Monoid a => a
mempty (SimpleId -> UTxOType SimpleTx
utxoRef SimpleId
2)
              reqSn :: Input SimpleTx
reqSn = 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
-> Message SimpleTx
forall tx.
SnapshotVersion
-> SnapshotNumber -> [TxIdType tx] -> Maybe tx -> Message tx
ReqSn SnapshotVersion
0 SnapshotNumber
1 [TxIdType SimpleTx
1] Maybe SimpleTx
forall a. Maybe a
Nothing
              snapshot1 :: Snapshot SimpleTx
snapshot1 = SnapshotNumber
-> SnapshotVersion
-> [TxIdType SimpleTx]
-> UTxOType SimpleTx
-> Snapshot SimpleTx
forall tx.
Monoid (UTxOType tx) =>
SnapshotNumber
-> SnapshotVersion -> [TxIdType tx] -> UTxOType tx -> Snapshot tx
testSnapshot SnapshotNumber
1 SnapshotVersion
0 [TxIdType SimpleTx
1] ([SimpleId] -> UTxOType SimpleTx
utxoRefs [SimpleId
1])
              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

          HeadState SimpleTx
sa <- 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
ledger ([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 (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
t1
            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
reqSn
            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 (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
pendingTransaction

            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

          HeadState SimpleTx
sa HeadState SimpleTx -> (HeadState SimpleTx -> Bool) -> IO ()
forall a. (HasCallStack, Show a) => a -> (a -> Bool) -> IO ()
`shouldSatisfy` \case
            (Open OpenState{$sel:coordinatedHeadState:OpenState :: forall tx. OpenState tx -> CoordinatedHeadState tx
coordinatedHeadState = CoordinatedHeadState{Map (TxIdType SimpleTx) SimpleTx
$sel:allTxs:CoordinatedHeadState :: forall tx. CoordinatedHeadState tx -> Map (TxIdType tx) tx
allTxs :: Map (TxIdType SimpleTx) SimpleTx
allTxs}}) -> SimpleTx -> TxIdType SimpleTx
forall tx. IsTx tx => tx -> TxIdType tx
txId SimpleTx
t1 SimpleId -> Map SimpleId SimpleTx -> Bool
forall k a. Ord k => k -> Map k a -> Bool
`notMember` Map SimpleId SimpleTx
Map (TxIdType SimpleTx) SimpleTx
allTxs
            HeadState SimpleTx
_ -> Bool
False

      String -> IO () -> SpecWith (Arg (IO ()))
forall a.
(HasCallStack, Example a) =>
String -> a -> SpecWith (Arg a)
it String
"rejects last AckSn if one signature was from a different snapshot" (IO () -> SpecWith (Arg (IO ())))
-> IO () -> SpecWith (Arg (IO ()))
forall a b. (a -> b) -> a -> b
$ do
        let reqSn :: Input tx
reqSn = Message tx -> Input tx
forall tx. Message tx -> Input tx
receiveMessage (Message tx -> Input tx) -> Message tx -> Input tx
forall a b. (a -> b) -> a -> b
$ SnapshotVersion
-> SnapshotNumber -> [TxIdType tx] -> Maybe tx -> Message tx
forall tx.
SnapshotVersion
-> SnapshotNumber -> [TxIdType tx] -> Maybe tx -> Message tx
ReqSn SnapshotVersion
0 SnapshotNumber
1 [] Maybe tx
forall a. Maybe a
Nothing
            snapshot :: Snapshot SimpleTx
snapshot = SnapshotNumber
-> SnapshotVersion
-> [TxIdType SimpleTx]
-> UTxOType SimpleTx
-> Snapshot SimpleTx
forall tx.
Monoid (UTxOType tx) =>
SnapshotNumber
-> SnapshotVersion -> [TxIdType tx] -> UTxOType tx -> Snapshot tx
testSnapshot SnapshotNumber
1 SnapshotVersion
0 [] UTxOType SimpleTx
forall a. Monoid a => a
mempty
            snapshot' :: Snapshot SimpleTx
snapshot' = SnapshotNumber
-> SnapshotVersion
-> [TxIdType SimpleTx]
-> UTxOType SimpleTx
-> Snapshot SimpleTx
forall tx.
Monoid (UTxOType tx) =>
SnapshotNumber
-> SnapshotVersion -> [TxIdType tx] -> UTxOType tx -> Snapshot tx
testSnapshot SnapshotNumber
2 SnapshotVersion
0 [] UTxOType SimpleTx
forall a. Monoid a => a
mempty
            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
snapshot) SnapshotNumber
1
            invalidAckFrom :: SigningKey HydraKey -> Party -> Input SimpleTx
invalidAckFrom 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
snapshot') SnapshotNumber
1
        HeadState SimpleTx
waitingForLastAck <-
          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
ledger ([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 Input SimpleTx
forall {tx}. Input tx
reqSn
            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
ledger HeadState SimpleTx
waitingForLastAck (SigningKey HydraKey -> Party -> Input SimpleTx
invalidAckFrom SigningKey HydraKey
bobSk Party
bob)
          Outcome SimpleTx -> (Outcome SimpleTx -> Bool) -> IO ()
forall a. (HasCallStack, Show a) => a -> (a -> Bool) -> IO ()
`shouldSatisfy` \case
            Error (RequireFailed InvalidMultisignature{[VerificationKey HydraKey]
vkeys :: [VerificationKey HydraKey]
$sel:vkeys:ReqSnNumberInvalid :: forall tx. RequirementFailure tx -> [VerificationKey HydraKey]
vkeys}) -> [VerificationKey HydraKey]
vkeys [VerificationKey HydraKey] -> [VerificationKey HydraKey] -> Bool
forall a. Eq a => a -> a -> Bool
== [Party -> VerificationKey HydraKey
vkey Party
bob]
            Outcome SimpleTx
_ -> Bool
False

      String -> IO () -> SpecWith (Arg (IO ()))
forall a.
(HasCallStack, Example a) =>
String -> a -> SpecWith (Arg a)
it String
"rejects last AckSn if one signature was from a different key" (IO () -> SpecWith (Arg (IO ())))
-> IO () -> SpecWith (Arg (IO ()))
forall a b. (a -> b) -> a -> b
$ do
        let reqSn :: Input tx
reqSn = Message tx -> Input tx
forall tx. Message tx -> Input tx
receiveMessage (Message tx -> Input tx) -> Message tx -> Input tx
forall a b. (a -> b) -> a -> b
$ SnapshotVersion
-> SnapshotNumber -> [TxIdType tx] -> Maybe tx -> Message tx
forall tx.
SnapshotVersion
-> SnapshotNumber -> [TxIdType tx] -> Maybe tx -> Message tx
ReqSn SnapshotVersion
0 SnapshotNumber
1 [] Maybe tx
forall a. Maybe a
Nothing
            snapshot :: Snapshot SimpleTx
snapshot = SnapshotNumber
-> SnapshotVersion
-> [TxIdType SimpleTx]
-> UTxOType SimpleTx
-> Snapshot SimpleTx
forall tx.
Monoid (UTxOType tx) =>
SnapshotNumber
-> SnapshotVersion -> [TxIdType tx] -> UTxOType tx -> Snapshot tx
testSnapshot SnapshotNumber
1 SnapshotVersion
0 [] UTxOType SimpleTx
forall a. Monoid a => a
mempty
            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
snapshot) SnapshotNumber
1
        HeadState SimpleTx
waitingForLastAck <-
          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
ledger ([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 Input SimpleTx
forall {tx}. Input tx
reqSn
            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
ledger HeadState SimpleTx
waitingForLastAck (SigningKey HydraKey -> Party -> Input SimpleTx
ackFrom (ByteString -> SigningKey HydraKey
generateSigningKey ByteString
"foo") Party
bob)
          Outcome SimpleTx -> (Outcome SimpleTx -> Bool) -> IO ()
forall a. (HasCallStack, Show a) => a -> (a -> Bool) -> IO ()
`shouldSatisfy` \case
            Error (RequireFailed InvalidMultisignature{[VerificationKey HydraKey]
$sel:vkeys:ReqSnNumberInvalid :: forall tx. RequirementFailure tx -> [VerificationKey HydraKey]
vkeys :: [VerificationKey HydraKey]
vkeys}) -> [VerificationKey HydraKey]
vkeys [VerificationKey HydraKey] -> [VerificationKey HydraKey] -> Bool
forall a. Eq a => a -> a -> Bool
== [Party -> VerificationKey HydraKey
vkey Party
bob]
            Outcome SimpleTx
_ -> Bool
False

      String -> IO () -> SpecWith (Arg (IO ()))
forall a.
(HasCallStack, Example a) =>
String -> a -> SpecWith (Arg a)
it String
"rejects last AckSn if one signature was from a completely different message" (IO () -> SpecWith (Arg (IO ())))
-> IO () -> SpecWith (Arg (IO ()))
forall a b. (a -> b) -> a -> b
$ do
        let reqSn :: Input tx
reqSn = Message tx -> Input tx
forall tx. Message tx -> Input tx
receiveMessage (Message tx -> Input tx) -> Message tx -> Input tx
forall a b. (a -> b) -> a -> b
$ SnapshotVersion
-> SnapshotNumber -> [TxIdType tx] -> Maybe tx -> Message tx
forall tx.
SnapshotVersion
-> SnapshotNumber -> [TxIdType tx] -> Maybe tx -> Message tx
ReqSn SnapshotVersion
0 SnapshotNumber
1 [] Maybe tx
forall a. Maybe a
Nothing
            snapshot1 :: Snapshot SimpleTx
snapshot1 = SnapshotNumber
-> SnapshotVersion
-> [TxIdType SimpleTx]
-> UTxOType SimpleTx
-> Snapshot SimpleTx
forall tx.
Monoid (UTxOType tx) =>
SnapshotNumber
-> SnapshotVersion -> [TxIdType tx] -> UTxOType tx -> Snapshot tx
testSnapshot SnapshotNumber
1 SnapshotVersion
0 [] UTxOType SimpleTx
forall a. Monoid a => a
mempty
            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
            invalidAckFrom :: SigningKey HydraKey -> Party -> Input tx
invalidAckFrom SigningKey HydraKey
sk Party
vk =
              Party -> Message tx -> Input tx
forall tx. Party -> Message tx -> Input tx
receiveMessageFrom Party
vk (Message tx -> Input tx) -> Message tx -> Input tx
forall a b. (a -> b) -> a -> b
$
                Signature (Snapshot tx) -> SnapshotNumber -> Message tx
forall tx. Signature (Snapshot tx) -> SnapshotNumber -> Message tx
AckSn (Signature ByteString -> Signature (Snapshot tx)
forall a b. Coercible a b => a -> b
coerce (Signature ByteString -> Signature (Snapshot tx))
-> Signature ByteString -> Signature (Snapshot tx)
forall a b. (a -> b) -> a -> b
$ SigningKey HydraKey -> ByteString -> Signature ByteString
forall a.
SignableRepresentation a =>
SigningKey HydraKey -> a -> Signature a
sign SigningKey HydraKey
sk (ByteString
"foo" :: ByteString)) SnapshotNumber
1
        HeadState SimpleTx
waitingForLastAck <-
          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
ledger ([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 Input SimpleTx
forall {tx}. Input tx
reqSn
            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
forall {tx}. SigningKey HydraKey -> Party -> Input tx
invalidAckFrom SigningKey HydraKey
bobSk Party
bob)
            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
ledger HeadState SimpleTx
waitingForLastAck (SigningKey HydraKey -> Party -> Input SimpleTx
ackFrom SigningKey HydraKey
aliceSk Party
alice)
          Outcome SimpleTx -> (Outcome SimpleTx -> Bool) -> IO ()
forall a. (HasCallStack, Show a) => a -> (a -> Bool) -> IO ()
`shouldSatisfy` \case
            Error (RequireFailed InvalidMultisignature{[VerificationKey HydraKey]
$sel:vkeys:ReqSnNumberInvalid :: forall tx. RequirementFailure tx -> [VerificationKey HydraKey]
vkeys :: [VerificationKey HydraKey]
vkeys}) -> [VerificationKey HydraKey]
vkeys [VerificationKey HydraKey] -> [VerificationKey HydraKey] -> Bool
forall a. Eq a => a -> a -> Bool
== [Party -> VerificationKey HydraKey
vkey Party
bob]
            Outcome SimpleTx
_ -> Bool
False

      String -> IO () -> SpecWith (Arg (IO ()))
forall a.
(HasCallStack, Example a) =>
String -> a -> SpecWith (Arg a)
it String
"rejects last AckSn if already received signature from this party" (IO () -> SpecWith (Arg (IO ())))
-> IO () -> SpecWith (Arg (IO ()))
forall a b. (a -> b) -> a -> b
$ do
        let reqSn :: Input tx
reqSn = Message tx -> Input tx
forall tx. Message tx -> Input tx
receiveMessage (Message tx -> Input tx) -> Message tx -> Input tx
forall a b. (a -> b) -> a -> b
$ SnapshotVersion
-> SnapshotNumber -> [TxIdType tx] -> Maybe tx -> Message tx
forall tx.
SnapshotVersion
-> SnapshotNumber -> [TxIdType tx] -> Maybe tx -> Message tx
ReqSn SnapshotVersion
0 SnapshotNumber
1 [] Maybe tx
forall a. Maybe a
Nothing
            snapshot1 :: Snapshot SimpleTx
snapshot1 = SnapshotNumber
-> SnapshotVersion
-> [TxIdType SimpleTx]
-> UTxOType SimpleTx
-> Snapshot SimpleTx
forall tx.
Monoid (UTxOType tx) =>
SnapshotNumber
-> SnapshotVersion -> [TxIdType tx] -> UTxOType tx -> Snapshot tx
testSnapshot SnapshotNumber
1 SnapshotVersion
0 [] UTxOType SimpleTx
forall a. Monoid a => a
mempty
            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
        HeadState SimpleTx
waitingForAck <-
          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
ledger ([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 Input SimpleTx
forall {tx}. Input tx
reqSn
            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 (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
ledger HeadState SimpleTx
waitingForAck (SigningKey HydraKey -> Party -> Input SimpleTx
ackFrom SigningKey HydraKey
carolSk Party
carol)
          Outcome SimpleTx -> (Outcome SimpleTx -> Bool) -> IO ()
forall a. (HasCallStack, Show a) => a -> (a -> Bool) -> IO ()
`shouldSatisfy` \case
            Error (RequireFailed SnapshotAlreadySigned{Party
receivedSignature :: Party
$sel:receivedSignature:ReqSnNumberInvalid :: forall tx. RequirementFailure tx -> Party
receivedSignature}) -> Party
receivedSignature Party -> Party -> Bool
forall a. Eq a => a -> a -> Bool
== Party
carol
            Outcome SimpleTx
_ -> Bool
False

      String -> IO () -> SpecWith (Arg (IO ()))
forall a.
(HasCallStack, Example a) =>
String -> a -> SpecWith (Arg a)
it String
"rejects snapshot request with transaction not applicable to previous snapshot" (IO () -> SpecWith (Arg (IO ())))
-> IO () -> SpecWith (Arg (IO ()))
forall a b. (a -> b) -> a -> b
$ do
        let reqTx42 :: Input SimpleTx
reqTx42 = 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 (SimpleId -> UTxOType SimpleTx -> UTxOType SimpleTx -> SimpleTx
SimpleTx SimpleId
42 Set SimpleTxOut
UTxOType SimpleTx
forall a. Monoid a => a
mempty (SimpleId -> UTxOType SimpleTx
utxoRef SimpleId
1))
            reqTx1 :: Input SimpleTx
reqTx1 = 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 (SimpleId -> UTxOType SimpleTx -> UTxOType SimpleTx -> SimpleTx
SimpleTx SimpleId
1 (SimpleId -> UTxOType SimpleTx
utxoRef SimpleId
1) (SimpleId -> UTxOType SimpleTx
utxoRef SimpleId
2))
            input :: Input SimpleTx
input = 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
-> Message SimpleTx
forall tx.
SnapshotVersion
-> SnapshotNumber -> [TxIdType tx] -> Maybe tx -> Message tx
ReqSn SnapshotVersion
0 SnapshotNumber
1 [TxIdType SimpleTx
1] Maybe SimpleTx
forall a. Maybe a
Nothing
            s0 :: HeadState SimpleTx
s0 = [Party] -> HeadState SimpleTx
inOpenState [Party]
threeParties

        HeadState SimpleTx
s2 <- 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
ledger HeadState SimpleTx
s0 (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
reqTx42
          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
reqTx1
          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
ledger HeadState SimpleTx
s2 Input SimpleTx
input
          Outcome SimpleTx -> Outcome SimpleTx -> IO ()
forall a. (HasCallStack, Show a, Eq a) => a -> a -> IO ()
`shouldBe` LogicError SimpleTx -> Outcome SimpleTx
forall tx. LogicError tx -> Outcome tx
Error (RequirementFailure SimpleTx -> LogicError SimpleTx
forall tx. RequirementFailure tx -> LogicError tx
RequireFailed (SnapshotNumber
-> TxIdType SimpleTx
-> ValidationError
-> RequirementFailure SimpleTx
forall tx.
SnapshotNumber
-> TxIdType tx -> ValidationError -> RequirementFailure tx
SnapshotDoesNotApply SnapshotNumber
1 SimpleId
TxIdType SimpleTx
1 (Text -> ValidationError
ValidationError Text
"cannot apply transaction")))

      String -> IO () -> SpecWith (Arg (IO ()))
forall a.
(HasCallStack, Example a) =>
String -> a -> SpecWith (Arg a)
it String
"waits if we receive a snapshot with unseen transactions" (IO () -> SpecWith (Arg (IO ())))
-> IO () -> SpecWith (Arg (IO ()))
forall a b. (a -> b) -> a -> b
$ do
        let s0 :: HeadState SimpleTx
s0 = [Party] -> HeadState SimpleTx
inOpenState [Party]
threeParties
            reqSn :: Input SimpleTx
reqSn = 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
-> Message SimpleTx
forall tx.
SnapshotVersion
-> SnapshotNumber -> [TxIdType tx] -> Maybe tx -> Message tx
ReqSn SnapshotVersion
0 SnapshotNumber
1 [TxIdType SimpleTx
1] Maybe SimpleTx
forall a. Maybe a
Nothing
        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
ledger HeadState SimpleTx
s0 Input SimpleTx
reqSn
          Outcome SimpleTx -> WaitReason SimpleTx -> IO ()
forall tx.
(HasCallStack, IsChainState tx) =>
Outcome tx -> WaitReason tx -> IO ()
`assertWait` [TxIdType SimpleTx] -> WaitReason SimpleTx
forall tx. [TxIdType tx] -> WaitReason tx
WaitOnTxs [SimpleId
TxIdType SimpleTx
1]

      String -> IO () -> SpecWith (Arg (IO ()))
forall a.
(HasCallStack, Example a) =>
String -> a -> SpecWith (Arg a)
it String
"waits if we receive an AckSn for an unseen snapshot" (IO () -> SpecWith (Arg (IO ())))
-> IO () -> SpecWith (Arg (IO ()))
forall a b. (a -> b) -> a -> b
$ do
        let snapshot :: Snapshot SimpleTx
snapshot = SnapshotNumber
-> SnapshotVersion
-> [TxIdType SimpleTx]
-> UTxOType SimpleTx
-> Snapshot SimpleTx
forall tx.
Monoid (UTxOType tx) =>
SnapshotNumber
-> SnapshotVersion -> [TxIdType tx] -> UTxOType tx -> Snapshot tx
testSnapshot SnapshotNumber
1 SnapshotVersion
0 [] UTxOType SimpleTx
forall a. Monoid a => a
mempty
            input :: Input SimpleTx
input = 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
$ 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
aliceSk Snapshot SimpleTx
snapshot) SnapshotNumber
1
        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
ledger ([Party] -> HeadState SimpleTx
inOpenState [Party]
threeParties) Input SimpleTx
input
          Outcome SimpleTx -> WaitReason SimpleTx -> IO ()
forall tx.
(HasCallStack, IsChainState tx) =>
Outcome tx -> WaitReason tx -> IO ()
`assertWait` WaitReason SimpleTx
forall tx. WaitReason tx
WaitOnSeenSnapshot

      -- TODO: Write property tests for various future / old snapshot behavior.
      -- That way we could cover variations of snapshot numbers and state of
      -- snapshot collection.

      String -> IO () -> SpecWith (Arg (IO ()))
forall a.
(HasCallStack, Example a) =>
String -> a -> SpecWith (Arg a)
it String
"rejects if we receive a too far future snapshot" (IO () -> SpecWith (Arg (IO ())))
-> IO () -> SpecWith (Arg (IO ()))
forall a b. (a -> b) -> a -> b
$ do
        let input :: Input tx
input = Party -> Message tx -> Input tx
forall tx. Party -> Message tx -> Input tx
receiveMessageFrom Party
bob (Message tx -> Input tx) -> Message tx -> Input tx
forall a b. (a -> b) -> a -> b
$ SnapshotVersion
-> SnapshotNumber -> [TxIdType tx] -> Maybe tx -> Message tx
forall tx.
SnapshotVersion
-> SnapshotNumber -> [TxIdType tx] -> Maybe tx -> Message tx
ReqSn SnapshotVersion
0 SnapshotNumber
2 [] Maybe tx
forall a. Maybe a
Nothing
            st :: HeadState SimpleTx
st = [Party] -> HeadState SimpleTx
inOpenState [Party]
threeParties
        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
ledger HeadState SimpleTx
st Input SimpleTx
forall {tx}. Input tx
input Outcome SimpleTx -> Outcome SimpleTx -> IO ()
forall a. (HasCallStack, Show a, Eq a) => a -> a -> IO ()
`shouldBe` LogicError SimpleTx -> Outcome SimpleTx
forall tx. LogicError tx -> Outcome tx
Error (RequirementFailure SimpleTx -> LogicError SimpleTx
forall tx. RequirementFailure tx -> LogicError tx
RequireFailed (RequirementFailure SimpleTx -> LogicError SimpleTx)
-> RequirementFailure SimpleTx -> LogicError SimpleTx
forall a b. (a -> b) -> a -> b
$ SnapshotNumber -> SnapshotNumber -> RequirementFailure SimpleTx
forall tx.
SnapshotNumber -> SnapshotNumber -> RequirementFailure tx
ReqSnNumberInvalid SnapshotNumber
2 SnapshotNumber
0)

      String -> IO () -> SpecWith (Arg (IO ()))
forall a.
(HasCallStack, Example a) =>
String -> a -> SpecWith (Arg a)
it String
"waits if we receive a future snapshot while collecting signatures" (IO () -> SpecWith (Arg (IO ())))
-> IO () -> SpecWith (Arg (IO ()))
forall a b. (a -> b) -> a -> b
$ do
        let reqSn1 :: Input tx
reqSn1 = Message tx -> Input tx
forall tx. Message tx -> Input tx
receiveMessage (Message tx -> Input tx) -> Message tx -> Input tx
forall a b. (a -> b) -> a -> b
$ SnapshotVersion
-> SnapshotNumber -> [TxIdType tx] -> Maybe tx -> Message tx
forall tx.
SnapshotVersion
-> SnapshotNumber -> [TxIdType tx] -> Maybe tx -> Message tx
ReqSn SnapshotVersion
0 SnapshotNumber
1 [] Maybe tx
forall a. Maybe a
Nothing
            reqSn2 :: Input tx
reqSn2 = Party -> Message tx -> Input tx
forall tx. Party -> Message tx -> Input tx
receiveMessageFrom Party
bob (Message tx -> Input tx) -> Message tx -> Input tx
forall a b. (a -> b) -> a -> b
$ SnapshotVersion
-> SnapshotNumber -> [TxIdType tx] -> Maybe tx -> Message tx
forall tx.
SnapshotVersion
-> SnapshotNumber -> [TxIdType tx] -> Maybe tx -> Message tx
ReqSn SnapshotVersion
0 SnapshotNumber
2 [] Maybe tx
forall a. Maybe a
Nothing
        HeadState SimpleTx
st <-
          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
ledger ([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 Input SimpleTx
forall {tx}. Input tx
reqSn1
            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
ledger HeadState SimpleTx
st Input SimpleTx
forall {tx}. Input tx
reqSn2
          Outcome SimpleTx -> WaitReason SimpleTx -> IO ()
forall tx.
(HasCallStack, IsChainState tx) =>
Outcome tx -> WaitReason tx -> IO ()
`assertWait` SnapshotNumber -> WaitReason SimpleTx
forall tx. SnapshotNumber -> WaitReason tx
WaitOnSnapshotNumber SnapshotNumber
1

      String -> IO () -> SpecWith (Arg (IO ()))
forall a.
(HasCallStack, Example a) =>
String -> a -> SpecWith (Arg a)
it String
"acks signed snapshot from the constant leader" (IO () -> SpecWith (Arg (IO ())))
-> IO () -> SpecWith (Arg (IO ()))
forall a b. (a -> b) -> a -> b
$ do
        let leader :: Party
leader = Party
alice
            snapshot :: Snapshot SimpleTx
snapshot = SnapshotNumber
-> SnapshotVersion
-> [TxIdType SimpleTx]
-> UTxOType SimpleTx
-> Snapshot SimpleTx
forall tx.
Monoid (UTxOType tx) =>
SnapshotNumber
-> SnapshotVersion -> [TxIdType tx] -> UTxOType tx -> Snapshot tx
testSnapshot SnapshotNumber
1 SnapshotVersion
0 [] UTxOType SimpleTx
forall a. Monoid a => a
mempty
            input :: Input SimpleTx
input = Party -> Message SimpleTx -> Input SimpleTx
forall tx. Party -> Message tx -> Input tx
receiveMessageFrom Party
leader (Message SimpleTx -> Input SimpleTx)
-> Message SimpleTx -> Input SimpleTx
forall a b. (a -> b) -> a -> b
$ SnapshotVersion
-> SnapshotNumber
-> [TxIdType SimpleTx]
-> Maybe SimpleTx
-> Message SimpleTx
forall tx.
SnapshotVersion
-> SnapshotNumber -> [TxIdType tx] -> Maybe tx -> Message tx
ReqSn SnapshotVersion
0 (Snapshot SimpleTx -> SnapshotNumber
forall tx. Snapshot tx -> SnapshotNumber
number Snapshot SimpleTx
snapshot) [] Maybe SimpleTx
forall a. Maybe a
Nothing
            sig :: Signature (Snapshot SimpleTx)
sig = SigningKey HydraKey
-> Snapshot SimpleTx -> Signature (Snapshot SimpleTx)
forall a.
SignableRepresentation a =>
SigningKey HydraKey -> a -> Signature a
sign SigningKey HydraKey
bobSk Snapshot SimpleTx
snapshot
            st :: HeadState SimpleTx
st = [Party] -> HeadState SimpleTx
inOpenState [Party]
threeParties
            ack :: Message SimpleTx
ack = Signature (Snapshot SimpleTx) -> SnapshotNumber -> Message SimpleTx
forall tx. Signature (Snapshot tx) -> SnapshotNumber -> Message tx
AckSn Signature (Snapshot SimpleTx)
sig (Snapshot SimpleTx -> SnapshotNumber
forall tx. Snapshot tx -> SnapshotNumber
number Snapshot SimpleTx
snapshot)
        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
ledger HeadState SimpleTx
st Input SimpleTx
input 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 Message SimpleTx
ack

      String -> IO () -> SpecWith (Arg (IO ()))
forall a.
(HasCallStack, Example a) =>
String -> a -> SpecWith (Arg a)
it String
"does not ack snapshots from non-leaders" (IO () -> SpecWith (Arg (IO ())))
-> IO () -> SpecWith (Arg (IO ()))
forall a b. (a -> b) -> a -> b
$ do
        let input :: Input tx
input = Party -> Message tx -> Input tx
forall tx. Party -> Message tx -> Input tx
receiveMessageFrom Party
notTheLeader (Message tx -> Input tx) -> Message tx -> Input tx
forall a b. (a -> b) -> a -> b
$ SnapshotVersion
-> SnapshotNumber -> [TxIdType tx] -> Maybe tx -> Message tx
forall tx.
SnapshotVersion
-> SnapshotNumber -> [TxIdType tx] -> Maybe tx -> Message tx
ReqSn SnapshotVersion
0 SnapshotNumber
1 [] Maybe tx
forall a. Maybe a
Nothing
            notTheLeader :: Party
notTheLeader = Party
bob
            st :: HeadState SimpleTx
st = [Party] -> HeadState SimpleTx
inOpenState [Party]
threeParties
        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
ledger HeadState SimpleTx
st Input SimpleTx
forall {tx}. Input tx
input Outcome SimpleTx -> (Outcome SimpleTx -> Bool) -> IO ()
forall a. (HasCallStack, Show a) => a -> (a -> Bool) -> IO ()
`shouldSatisfy` \case
          Error (RequireFailed ReqSnNotLeader{$sel:requestedSn:ReqSnNumberInvalid :: forall tx. RequirementFailure tx -> SnapshotNumber
requestedSn = SnapshotNumber
1, Party
leader :: Party
$sel:leader:ReqSnNumberInvalid :: forall tx. RequirementFailure tx -> Party
leader}) -> Party
leader Party -> Party -> Bool
forall a. Eq a => a -> a -> Bool
== Party
notTheLeader
          Outcome SimpleTx
_ -> Bool
False

      String -> IO () -> SpecWith (Arg (IO ()))
forall a.
(HasCallStack, Example a) =>
String -> a -> SpecWith (Arg a)
it String
"rejects too-old snapshots" (IO () -> SpecWith (Arg (IO ())))
-> IO () -> SpecWith (Arg (IO ()))
forall a b. (a -> b) -> a -> b
$ do
        let input :: Input tx
input = Party -> Message tx -> Input tx
forall tx. Party -> Message tx -> Input tx
receiveMessageFrom Party
theLeader (Message tx -> Input tx) -> Message tx -> Input tx
forall a b. (a -> b) -> a -> b
$ SnapshotVersion
-> SnapshotNumber -> [TxIdType tx] -> Maybe tx -> Message tx
forall tx.
SnapshotVersion
-> SnapshotNumber -> [TxIdType tx] -> Maybe tx -> Message tx
ReqSn SnapshotVersion
0 SnapshotNumber
2 [] Maybe tx
forall a. Maybe a
Nothing
            theLeader :: Party
theLeader = Party
alice
            snapshot :: Snapshot SimpleTx
snapshot = SnapshotNumber
-> SnapshotVersion
-> [TxIdType SimpleTx]
-> UTxOType SimpleTx
-> Snapshot SimpleTx
forall tx.
Monoid (UTxOType tx) =>
SnapshotNumber
-> SnapshotVersion -> [TxIdType tx] -> UTxOType tx -> Snapshot tx
testSnapshot SnapshotNumber
2 SnapshotVersion
0 [] UTxOType SimpleTx
forall a. Monoid a => a
mempty
            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{confirmedSnapshot = ConfirmedSnapshot snapshot (Crypto.aggregate [])}
        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
ledger HeadState SimpleTx
st Input SimpleTx
forall {tx}. Input tx
input Outcome SimpleTx -> Outcome SimpleTx -> IO ()
forall a. (HasCallStack, Show a, Eq a) => a -> a -> IO ()
`shouldBe` LogicError SimpleTx -> Outcome SimpleTx
forall tx. LogicError tx -> Outcome tx
Error (RequirementFailure SimpleTx -> LogicError SimpleTx
forall tx. RequirementFailure tx -> LogicError tx
RequireFailed (RequirementFailure SimpleTx -> LogicError SimpleTx)
-> RequirementFailure SimpleTx -> LogicError SimpleTx
forall a b. (a -> b) -> a -> b
$ SnapshotNumber -> SnapshotNumber -> RequirementFailure SimpleTx
forall tx.
SnapshotNumber -> SnapshotNumber -> RequirementFailure tx
ReqSnNumberInvalid SnapshotNumber
2 SnapshotNumber
0)

      String -> IO () -> SpecWith (Arg (IO ()))
forall a.
(HasCallStack, Example a) =>
String -> a -> SpecWith (Arg a)
it String
"rejects too-old snapshots when collecting signatures" (IO () -> SpecWith (Arg (IO ())))
-> IO () -> SpecWith (Arg (IO ()))
forall a b. (a -> b) -> a -> b
$ do
        let input :: Input tx
input = Party -> Message tx -> Input tx
forall tx. Party -> Message tx -> Input tx
receiveMessageFrom Party
theLeader (Message tx -> Input tx) -> Message tx -> Input tx
forall a b. (a -> b) -> a -> b
$ SnapshotVersion
-> SnapshotNumber -> [TxIdType tx] -> Maybe tx -> Message tx
forall tx.
SnapshotVersion
-> SnapshotNumber -> [TxIdType tx] -> Maybe tx -> Message tx
ReqSn SnapshotVersion
0 SnapshotNumber
2 [] Maybe tx
forall a. Maybe a
Nothing
            theLeader :: Party
theLeader = Party
alice
            snapshot :: Snapshot SimpleTx
snapshot = SnapshotNumber
-> SnapshotVersion
-> [TxIdType SimpleTx]
-> UTxOType SimpleTx
-> Snapshot SimpleTx
forall tx.
Monoid (UTxOType tx) =>
SnapshotNumber
-> SnapshotVersion -> [TxIdType tx] -> UTxOType tx -> Snapshot tx
testSnapshot SnapshotNumber
2 SnapshotVersion
0 [] UTxOType SimpleTx
forall a. Monoid a => a
mempty
            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
                  { confirmedSnapshot = ConfirmedSnapshot snapshot (Crypto.aggregate [])
                  , seenSnapshot = SeenSnapshot (testSnapshot 3 0 [] mempty) mempty
                  }
        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
ledger HeadState SimpleTx
st Input SimpleTx
forall {tx}. Input tx
input Outcome SimpleTx -> Outcome SimpleTx -> IO ()
forall a. (HasCallStack, Show a, Eq a) => a -> a -> IO ()
`shouldBe` LogicError SimpleTx -> Outcome SimpleTx
forall tx. LogicError tx -> Outcome tx
Error (RequirementFailure SimpleTx -> LogicError SimpleTx
forall tx. RequirementFailure tx -> LogicError tx
RequireFailed (RequirementFailure SimpleTx -> LogicError SimpleTx)
-> RequirementFailure SimpleTx -> LogicError SimpleTx
forall a b. (a -> b) -> a -> b
$ SnapshotNumber -> SnapshotNumber -> RequirementFailure SimpleTx
forall tx.
SnapshotNumber -> SnapshotNumber -> RequirementFailure tx
ReqSnNumberInvalid SnapshotNumber
2 SnapshotNumber
3)

      String -> IO () -> SpecWith (Arg (IO ()))
forall a.
(HasCallStack, Example a) =>
String -> a -> SpecWith (Arg a)
it String
"rejects too-new snapshots from the leader" (IO () -> SpecWith (Arg (IO ())))
-> IO () -> SpecWith (Arg (IO ()))
forall a b. (a -> b) -> a -> b
$ do
        let input :: Input tx
input = Party -> Message tx -> Input tx
forall tx. Party -> Message tx -> Input tx
receiveMessageFrom Party
theLeader (Message tx -> Input tx) -> Message tx -> Input tx
forall a b. (a -> b) -> a -> b
$ SnapshotVersion
-> SnapshotNumber -> [TxIdType tx] -> Maybe tx -> Message tx
forall tx.
SnapshotVersion
-> SnapshotNumber -> [TxIdType tx] -> Maybe tx -> Message tx
ReqSn SnapshotVersion
0 SnapshotNumber
3 [] Maybe tx
forall a. Maybe a
Nothing
            theLeader :: Party
theLeader = Party
carol
            st :: HeadState SimpleTx
st = [Party] -> HeadState SimpleTx
inOpenState [Party]
threeParties
        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
ledger HeadState SimpleTx
st Input SimpleTx
forall {tx}. Input tx
input Outcome SimpleTx -> Outcome SimpleTx -> IO ()
forall a. (HasCallStack, Show a, Eq a) => a -> a -> IO ()
`shouldBe` LogicError SimpleTx -> Outcome SimpleTx
forall tx. LogicError tx -> Outcome tx
Error (RequirementFailure SimpleTx -> LogicError SimpleTx
forall tx. RequirementFailure tx -> LogicError tx
RequireFailed (RequirementFailure SimpleTx -> LogicError SimpleTx)
-> RequirementFailure SimpleTx -> LogicError SimpleTx
forall a b. (a -> b) -> a -> b
$ SnapshotNumber -> SnapshotNumber -> RequirementFailure SimpleTx
forall tx.
SnapshotNumber -> SnapshotNumber -> RequirementFailure tx
ReqSnNumberInvalid SnapshotNumber
3 SnapshotNumber
0)

      String -> IO () -> SpecWith (Arg (IO ()))
forall a.
(HasCallStack, Example a) =>
String -> a -> SpecWith (Arg a)
it String
"rejects invalid snapshots version" (IO () -> SpecWith (Arg (IO ())))
-> IO () -> SpecWith (Arg (IO ()))
forall a b. (a -> b) -> a -> b
$ do
        let validSnNumber :: SnapshotNumber
validSnNumber = SnapshotNumber
0
            invalidSnVersion :: SnapshotVersion
invalidSnVersion = SnapshotVersion
1
            input :: Input SimpleTx
input = Party -> Message SimpleTx -> Input SimpleTx
forall tx. Party -> Message tx -> Input tx
receiveMessageFrom Party
theLeader (Message SimpleTx -> Input SimpleTx)
-> Message SimpleTx -> Input SimpleTx
forall a b. (a -> b) -> a -> b
$ SnapshotVersion
-> SnapshotNumber
-> [TxIdType SimpleTx]
-> Maybe SimpleTx
-> Message SimpleTx
forall tx.
SnapshotVersion
-> SnapshotNumber -> [TxIdType tx] -> Maybe tx -> Message tx
ReqSn SnapshotVersion
invalidSnVersion SnapshotNumber
validSnNumber [] Maybe SimpleTx
forall a. Maybe a
Nothing
            theLeader :: Party
theLeader = Party
carol
            expectedSnVersion :: SnapshotVersion
expectedSnVersion = SnapshotVersion
0
            st :: HeadState SimpleTx
st = [Party] -> HeadState SimpleTx
inOpenState [Party]
threeParties
        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
ledger HeadState SimpleTx
st Input SimpleTx
input Outcome SimpleTx -> Outcome SimpleTx -> IO ()
forall a. (HasCallStack, Show a, Eq a) => a -> a -> IO ()
`shouldBe` LogicError SimpleTx -> Outcome SimpleTx
forall tx. LogicError tx -> Outcome tx
Error (RequirementFailure SimpleTx -> LogicError SimpleTx
forall tx. RequirementFailure tx -> LogicError tx
RequireFailed (RequirementFailure SimpleTx -> LogicError SimpleTx)
-> RequirementFailure SimpleTx -> LogicError SimpleTx
forall a b. (a -> b) -> a -> b
$ SnapshotVersion -> SnapshotVersion -> RequirementFailure SimpleTx
forall tx.
SnapshotVersion -> SnapshotVersion -> RequirementFailure tx
ReqSvNumberInvalid SnapshotVersion
invalidSnVersion SnapshotVersion
expectedSnVersion)

      String -> IO () -> SpecWith (Arg (IO ()))
forall a.
(HasCallStack, Example a) =>
String -> a -> SpecWith (Arg a)
it String
"rejects overlapping snapshot requests from the leader" (IO () -> SpecWith (Arg (IO ())))
-> IO () -> SpecWith (Arg (IO ()))
forall a b. (a -> b) -> a -> b
$ do
        let theLeader :: Party
theLeader = Party
alice
            nextSN :: SnapshotNumber
nextSN = SnapshotNumber
1
            firstReqTx :: Input SimpleTx
firstReqTx = 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 (SimpleId -> SimpleTx
aValidTx SimpleId
42)
            firstReqSn :: Input SimpleTx
firstReqSn = Party -> Message SimpleTx -> Input SimpleTx
forall tx. Party -> Message tx -> Input tx
receiveMessageFrom Party
theLeader (Message SimpleTx -> Input SimpleTx)
-> Message SimpleTx -> Input SimpleTx
forall a b. (a -> b) -> a -> b
$ SnapshotVersion
-> SnapshotNumber
-> [TxIdType SimpleTx]
-> Maybe SimpleTx
-> Message SimpleTx
forall tx.
SnapshotVersion
-> SnapshotNumber -> [TxIdType tx] -> Maybe tx -> Message tx
ReqSn SnapshotVersion
0 SnapshotNumber
nextSN [TxIdType SimpleTx
42] Maybe SimpleTx
forall a. Maybe a
Nothing
            secondReqTx :: Input SimpleTx
secondReqTx = 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 (SimpleId -> SimpleTx
aValidTx SimpleId
51)
            secondReqSn :: Input SimpleTx
secondReqSn = Party -> Message SimpleTx -> Input SimpleTx
forall tx. Party -> Message tx -> Input tx
receiveMessageFrom Party
theLeader (Message SimpleTx -> Input SimpleTx)
-> Message SimpleTx -> Input SimpleTx
forall a b. (a -> b) -> a -> b
$ SnapshotVersion
-> SnapshotNumber
-> [TxIdType SimpleTx]
-> Maybe SimpleTx
-> Message SimpleTx
forall tx.
SnapshotVersion
-> SnapshotNumber -> [TxIdType tx] -> Maybe tx -> Message tx
ReqSn SnapshotVersion
0 SnapshotNumber
nextSN [SimpleId
TxIdType SimpleTx
51] Maybe SimpleTx
forall a. Maybe a
Nothing

        HeadState SimpleTx
s3 <- 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
ledger ([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 Input SimpleTx
firstReqTx
          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
firstReqSn
          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
secondReqTx
          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
ledger HeadState SimpleTx
s3 Input SimpleTx
secondReqSn Outcome SimpleTx -> (Outcome SimpleTx -> Bool) -> IO ()
forall a. (HasCallStack, Show a) => a -> (a -> Bool) -> IO ()
`shouldSatisfy` \case
          Error RequireFailed{} -> Bool
True
          Outcome SimpleTx
_ -> Bool
False

      String -> IO () -> SpecWith (Arg (IO ()))
forall a.
(HasCallStack, Example a) =>
String -> a -> SpecWith (Arg a)
it String
"rejects same version snapshot requests with differring decommit txs" (IO () -> SpecWith (Arg (IO ())))
-> IO () -> SpecWith (Arg (IO ()))
forall a b. (a -> b) -> a -> b
$ do
        let decommitTx1 :: SimpleTx
decommitTx1 = SimpleId -> UTxOType SimpleTx -> UTxOType SimpleTx -> SimpleTx
SimpleTx SimpleId
1 (SimpleId -> UTxOType SimpleTx
utxoRef SimpleId
1) (SimpleId -> UTxOType SimpleTx
utxoRef SimpleId
3)
            decommitTx2 :: SimpleTx
decommitTx2 = SimpleId -> UTxOType SimpleTx -> UTxOType SimpleTx -> SimpleTx
SimpleTx SimpleId
2 (SimpleId -> UTxOType SimpleTx
utxoRef SimpleId
2) (SimpleId -> UTxOType SimpleTx
utxoRef SimpleId
4)
            activeUTxO :: UTxOType SimpleTx
activeUTxO = [SimpleId] -> UTxOType SimpleTx
utxoRefs [SimpleId
1, SimpleId
2]
            snapshot :: Snapshot SimpleTx
snapshot =
              Snapshot
                { $sel:headId:Snapshot :: HeadId
headId = HeadId
testHeadId
                , $sel:version:Snapshot :: SnapshotVersion
version = SnapshotVersion
0
                , $sel:number:Snapshot :: SnapshotNumber
number = SnapshotNumber
1
                , $sel:confirmed:Snapshot :: [TxIdType SimpleTx]
confirmed = []
                , $sel:utxo:Snapshot :: UTxOType SimpleTx
utxo = Set SimpleTxOut
UTxOType SimpleTx
activeUTxO
                , $sel:utxoToDecommit:Snapshot :: Maybe (UTxOType SimpleTx)
utxoToDecommit = UTxOType SimpleTx -> Maybe (UTxOType SimpleTx)
forall a. a -> Maybe a
Just (UTxOType SimpleTx -> Maybe (UTxOType SimpleTx))
-> UTxOType SimpleTx -> Maybe (UTxOType SimpleTx)
forall a b. (a -> b) -> a -> b
$ [SimpleId] -> UTxOType SimpleTx
utxoRefs [SimpleId
3]
                }
            s0 :: HeadState SimpleTx
s0 =
              [Party] -> CoordinatedHeadState SimpleTx -> HeadState SimpleTx
inOpenState'
                [Party]
threeParties
                CoordinatedHeadState SimpleTx
coordinatedHeadState
                  { confirmedSnapshot = ConfirmedSnapshot snapshot (Crypto.aggregate [])
                  , seenSnapshot = LastSeenSnapshot 1
                  , localUTxO = activeUTxO
                  }
            reqSn0 :: Input SimpleTx
reqSn0 = Party -> Message SimpleTx -> Input SimpleTx
forall tx. Party -> Message tx -> Input tx
receiveMessageFrom Party
alice (Message SimpleTx -> Input SimpleTx)
-> Message SimpleTx -> Input SimpleTx
forall a b. (a -> b) -> a -> b
$ SnapshotVersion
-> SnapshotNumber
-> [TxIdType SimpleTx]
-> Maybe SimpleTx
-> Message SimpleTx
forall tx.
SnapshotVersion
-> SnapshotNumber -> [TxIdType tx] -> Maybe tx -> Message tx
ReqSn SnapshotVersion
0 SnapshotNumber
1 [] (SimpleTx -> Maybe SimpleTx
forall a. a -> Maybe a
Just SimpleTx
decommitTx1)
            reqSn1 :: Input SimpleTx
reqSn1 = 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
$ SnapshotVersion
-> SnapshotNumber
-> [TxIdType SimpleTx]
-> Maybe SimpleTx
-> Message SimpleTx
forall tx.
SnapshotVersion
-> SnapshotNumber -> [TxIdType tx] -> Maybe tx -> Message tx
ReqSn SnapshotVersion
0 SnapshotNumber
2 [] (SimpleTx -> Maybe SimpleTx
forall a. a -> Maybe a
Just SimpleTx
decommitTx2)

        Outcome SimpleTx
outcome <- Environment
-> Ledger SimpleTx
-> HeadState SimpleTx
-> StateT (StepState SimpleTx) IO (Outcome SimpleTx)
-> IO (Outcome SimpleTx)
forall (m :: * -> *) tx a.
Monad m =>
Environment
-> Ledger tx -> HeadState tx -> StateT (StepState tx) m a -> m a
runHeadLogic Environment
bobEnv Ledger SimpleTx
ledger HeadState SimpleTx
s0 (StateT (StepState SimpleTx) IO (Outcome SimpleTx)
 -> IO (Outcome SimpleTx))
-> StateT (StepState SimpleTx) IO (Outcome SimpleTx)
-> IO (Outcome 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
reqSn0
          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
reqSn1
        Outcome SimpleTx
outcome Outcome SimpleTx -> (Outcome SimpleTx -> Bool) -> IO ()
forall a. (HasCallStack, Show a) => a -> (a -> Bool) -> IO ()
`shouldSatisfy` \case
          Error RequireFailed{RequirementFailure SimpleTx
requirementFailure :: RequirementFailure SimpleTx
$sel:requirementFailure:UnhandledInput :: forall tx. LogicError tx -> RequirementFailure tx
requirementFailure} | RequirementFailure SimpleTx
requirementFailure RequirementFailure SimpleTx -> RequirementFailure SimpleTx -> Bool
forall a. Eq a => a -> a -> Bool
== RequirementFailure SimpleTx
forall tx. RequirementFailure tx
ReqSnDecommitNotSettled -> Bool
True
          Outcome SimpleTx
_ -> Bool
False

      String -> IO () -> SpecWith (Arg (IO ()))
forall a.
(HasCallStack, Example a) =>
String -> a -> SpecWith (Arg a)
it String
"ignores in-flight ReqTx when closed" (IO () -> SpecWith (Arg (IO ())))
-> IO () -> SpecWith (Arg (IO ()))
forall a b. (a -> b) -> a -> b
$ do
        let s0 :: HeadState SimpleTx
s0 = [Party] -> HeadState SimpleTx
inClosedState [Party]
threeParties
            input :: Input SimpleTx
input = 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 (SimpleId -> SimpleTx
aValidTx SimpleId
42)
        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
ledger HeadState SimpleTx
s0 Input SimpleTx
input Outcome SimpleTx -> Outcome SimpleTx -> IO ()
forall a. (HasCallStack, Show a, Eq a) => a -> a -> IO ()
`shouldBe` LogicError SimpleTx -> Outcome SimpleTx
forall tx. LogicError tx -> Outcome tx
Error (Input SimpleTx -> HeadState SimpleTx -> LogicError SimpleTx
forall tx. Input tx -> HeadState tx -> LogicError tx
UnhandledInput Input SimpleTx
input HeadState SimpleTx
s0)

      String -> IO () -> SpecWith (Arg (IO ()))
forall a.
(HasCallStack, Example a) =>
String -> a -> SpecWith (Arg a)
it String
"ignores in-flight ReqDec when closed" (IO () -> SpecWith (Arg (IO ())))
-> IO () -> SpecWith (Arg (IO ()))
forall a b. (a -> b) -> a -> b
$ do
        let s0 :: HeadState SimpleTx
s0 = [Party] -> HeadState SimpleTx
inClosedState [Party]
threeParties
            input :: Input SimpleTx
input = 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
$ ReqDec{$sel:transaction:ReqTx :: SimpleTx
transaction = SimpleId -> SimpleTx
aValidTx SimpleId
42}
        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
ledger HeadState SimpleTx
s0 Input SimpleTx
input Outcome SimpleTx -> Outcome SimpleTx -> IO ()
forall a. (HasCallStack, Show a, Eq a) => a -> a -> IO ()
`shouldBe` LogicError SimpleTx -> Outcome SimpleTx
forall tx. LogicError tx -> Outcome tx
Error (Input SimpleTx -> HeadState SimpleTx -> LogicError SimpleTx
forall tx. Input tx -> HeadState tx -> LogicError tx
UnhandledInput Input SimpleTx
input HeadState SimpleTx
s0)

      String -> IO () -> SpecWith (Arg (IO ()))
forall a.
(HasCallStack, Example a) =>
String -> a -> SpecWith (Arg a)
it String
"everyone does collect on last commit after collect com" (IO () -> SpecWith (Arg (IO ())))
-> IO () -> SpecWith (Arg (IO ()))
forall a b. (a -> b) -> a -> b
$ do
        let aliceCommit :: OnChainTx SimpleTx
aliceCommit = HeadId -> Party -> UTxOType SimpleTx -> OnChainTx SimpleTx
forall tx. HeadId -> Party -> UTxOType tx -> OnChainTx tx
OnCommitTx HeadId
testHeadId Party
alice (SimpleId -> UTxOType SimpleTx
utxoRef SimpleId
1)
            bobCommit :: OnChainTx SimpleTx
bobCommit = HeadId -> Party -> UTxOType SimpleTx -> OnChainTx SimpleTx
forall tx. HeadId -> Party -> UTxOType tx -> OnChainTx tx
OnCommitTx HeadId
testHeadId Party
bob (SimpleId -> UTxOType SimpleTx
utxoRef SimpleId
2)
            carolCommit :: OnChainTx SimpleTx
carolCommit = HeadId -> Party -> UTxOType SimpleTx -> OnChainTx SimpleTx
forall tx. HeadId -> Party -> UTxOType tx -> OnChainTx tx
OnCommitTx HeadId
testHeadId Party
carol (SimpleId -> UTxOType SimpleTx
utxoRef SimpleId
3)
        HeadState SimpleTx
waitingForLastCommit <-
          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
ledger ([Party] -> HeadState SimpleTx
inInitialState [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 (Natural -> OnChainTx SimpleTx -> Input SimpleTx
observeTxAtSlot Natural
1 OnChainTx SimpleTx
aliceCommit)
            Input SimpleTx -> StateT (StepState SimpleTx) IO (Outcome SimpleTx)
forall tx (m :: * -> *).
(MonadState (StepState tx) m, IsChainState tx) =>
Input tx -> m (Outcome tx)
step (Natural -> OnChainTx SimpleTx -> Input SimpleTx
observeTxAtSlot Natural
2 OnChainTx SimpleTx
bobCommit)
            StateT (StepState SimpleTx) IO (HeadState SimpleTx)
forall tx (m :: * -> *).
MonadState (StepState tx) m =>
m (HeadState tx)
getState

        -- Bob is not the last party, but still does post a collect
        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
ledger HeadState SimpleTx
waitingForLastCommit (Natural -> OnChainTx SimpleTx -> Input SimpleTx
observeTxAtSlot Natural
3 OnChainTx SimpleTx
carolCommit)
          Outcome SimpleTx -> (Effect SimpleTx -> Bool) -> IO ()
forall tx.
(HasCallStack, IsChainState tx) =>
Outcome tx -> (Effect tx -> Bool) -> IO ()
`hasEffectSatisfying` \case
            OnChainEffect{$sel:postChainTx:ClientEffect :: forall tx. Effect tx -> PostChainTx tx
postChainTx = CollectComTx{}} -> Bool
True
            Effect SimpleTx
_ -> Bool
False

      String -> IO () -> SpecWith (Arg (IO ()))
forall a.
(HasCallStack, Example a) =>
String -> a -> SpecWith (Arg a)
it String
"cannot observe abort after collect com" (IO () -> SpecWith (Arg (IO ())))
-> IO () -> SpecWith (Arg (IO ()))
forall a b. (a -> b) -> a -> b
$ do
        HeadState SimpleTx
afterCollectCom <-
          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
ledger ([Party] -> HeadState SimpleTx
inInitialState [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 (OnChainTx SimpleTx -> Input SimpleTx
observeTx (OnChainTx SimpleTx -> Input SimpleTx)
-> OnChainTx SimpleTx -> Input SimpleTx
forall a b. (a -> b) -> a -> b
$ HeadId -> OnChainTx SimpleTx
forall tx. HeadId -> OnChainTx tx
OnCollectComTx HeadId
testHeadId)
            StateT (StepState SimpleTx) IO (HeadState SimpleTx)
forall tx (m :: * -> *).
MonadState (StepState tx) m =>
m (HeadState tx)
getState

        let unhandledInput :: Input SimpleTx
unhandledInput = OnChainTx SimpleTx -> Input SimpleTx
observeTx OnAbortTx{$sel:headId:OnInitTx :: HeadId
headId = HeadId
testHeadId}
        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
ledger HeadState SimpleTx
afterCollectCom Input SimpleTx
unhandledInput
          Outcome SimpleTx -> Outcome SimpleTx -> IO ()
forall a. (HasCallStack, Show a, Eq a) => a -> a -> IO ()
`shouldBe` LogicError SimpleTx -> Outcome SimpleTx
forall tx. LogicError tx -> Outcome tx
Error (Input SimpleTx -> HeadState SimpleTx -> LogicError SimpleTx
forall tx. Input tx -> HeadState tx -> LogicError tx
UnhandledInput Input SimpleTx
unhandledInput HeadState SimpleTx
afterCollectCom)

      String -> IO () -> SpecWith (Arg (IO ()))
forall a.
(HasCallStack, Example a) =>
String -> a -> SpecWith (Arg a)
it String
"cannot observe collect com after abort" (IO () -> SpecWith (Arg (IO ())))
-> IO () -> SpecWith (Arg (IO ()))
forall a b. (a -> b) -> a -> b
$ do
        HeadState SimpleTx
afterAbort <-
          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
ledger ([Party] -> HeadState SimpleTx
inInitialState [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 (OnChainTx SimpleTx -> Input SimpleTx
observeTx OnAbortTx{$sel:headId:OnInitTx :: HeadId
headId = HeadId
testHeadId})
            StateT (StepState SimpleTx) IO (HeadState SimpleTx)
forall tx (m :: * -> *).
MonadState (StepState tx) m =>
m (HeadState tx)
getState

        let unhandledInput :: Input SimpleTx
unhandledInput = OnChainTx SimpleTx -> Input SimpleTx
observeTx (HeadId -> OnChainTx SimpleTx
forall tx. HeadId -> OnChainTx tx
OnCollectComTx HeadId
testHeadId)
        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
ledger HeadState SimpleTx
afterAbort Input SimpleTx
unhandledInput
          Outcome SimpleTx -> Outcome SimpleTx -> IO ()
forall a. (HasCallStack, Show a, Eq a) => a -> a -> IO ()
`shouldBe` LogicError SimpleTx -> Outcome SimpleTx
forall tx. LogicError tx -> Outcome tx
Error (Input SimpleTx -> HeadState SimpleTx -> LogicError SimpleTx
forall tx. Input tx -> HeadState tx -> LogicError tx
UnhandledInput Input SimpleTx
unhandledInput HeadState SimpleTx
afterAbort)

      String -> IO () -> SpecWith (Arg (IO ()))
forall a.
(HasCallStack, Example a) =>
String -> a -> SpecWith (Arg a)
it String
"notifies user on head closing and when passing the contestation deadline" (IO () -> SpecWith (Arg (IO ())))
-> IO () -> SpecWith (Arg (IO ()))
forall a b. (a -> b) -> a -> b
$ do
        let s0 :: HeadState SimpleTx
s0 = [Party] -> HeadState SimpleTx
inOpenState [Party]
threeParties
            snapshotNumber :: SnapshotNumber
snapshotNumber = SnapshotNumber
0
            contestationDeadline :: UTCTime
contestationDeadline = Gen UTCTime
forall a. Arbitrary a => Gen a
arbitrary Gen UTCTime -> Int -> UTCTime
forall a. Gen a -> Int -> a
`generateWith` Int
42
            observeCloseTx :: Input SimpleTx
observeCloseTx =
              OnChainTx SimpleTx -> Input SimpleTx
observeTx
                OnCloseTx
                  { $sel:headId:OnInitTx :: HeadId
headId = HeadId
testHeadId
                  , SnapshotNumber
snapshotNumber :: SnapshotNumber
$sel:snapshotNumber:OnInitTx :: SnapshotNumber
snapshotNumber
                  , UTCTime
contestationDeadline :: UTCTime
$sel:contestationDeadline:OnInitTx :: UTCTime
contestationDeadline
                  }
            clientEffect :: Effect SimpleTx
clientEffect = ServerOutput SimpleTx -> Effect SimpleTx
forall tx. ServerOutput tx -> Effect tx
ClientEffect HeadIsClosed{$sel:headId:PeerConnected :: HeadId
headId = HeadId
testHeadId, SnapshotNumber
snapshotNumber :: SnapshotNumber
$sel:snapshotNumber:PeerConnected :: SnapshotNumber
snapshotNumber, UTCTime
contestationDeadline :: UTCTime
$sel:contestationDeadline:PeerConnected :: UTCTime
contestationDeadline}
        Environment
-> Ledger SimpleTx
-> HeadState SimpleTx
-> StateT (StepState SimpleTx) IO ()
-> IO ()
forall (m :: * -> *) tx a.
Monad m =>
Environment
-> Ledger tx -> HeadState tx -> StateT (StepState tx) m a -> m a
runHeadLogic Environment
bobEnv Ledger SimpleTx
ledger HeadState SimpleTx
s0 (StateT (StepState SimpleTx) IO () -> IO ())
-> StateT (StepState SimpleTx) IO () -> IO ()
forall a b. (a -> b) -> a -> b
$ do
          Outcome SimpleTx
outcome1 <- 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
observeCloseTx
          IO () -> StateT (StepState SimpleTx) IO ()
forall (m :: * -> *) a.
Monad m =>
m a -> StateT (StepState SimpleTx) m a
forall (t :: (* -> *) -> * -> *) (m :: * -> *) a.
(MonadTrans t, Monad m) =>
m a -> t m a
lift (IO () -> StateT (StepState SimpleTx) IO ())
-> IO () -> StateT (StepState SimpleTx) IO ()
forall a b. (a -> b) -> a -> b
$ do
            Outcome SimpleTx
outcome1 Outcome SimpleTx -> Effect SimpleTx -> IO ()
forall tx.
(HasCallStack, IsChainState tx) =>
Outcome tx -> Effect tx -> IO ()
`hasEffect` Effect SimpleTx
clientEffect
            Outcome SimpleTx
outcome1
              Outcome SimpleTx -> (Effect SimpleTx -> Bool) -> IO ()
forall tx.
(HasCallStack, IsChainState tx) =>
Outcome tx -> (Effect tx -> Bool) -> IO ()
`hasNoEffectSatisfying` \case
                ClientEffect (ReadyToFanout HeadId
_) -> Bool
True
                Effect SimpleTx
_ -> Bool
False

          let oneSecondsPastDeadline :: UTCTime
oneSecondsPastDeadline = NominalDiffTime -> UTCTime -> UTCTime
addUTCTime NominalDiffTime
1 UTCTime
contestationDeadline
              someChainSlot :: ChainSlot
someChainSlot = Gen ChainSlot
forall a. Arbitrary a => Gen a
arbitrary Gen ChainSlot -> Int -> ChainSlot
forall a. Gen a -> Int -> a
`generateWith` Int
42
              stepTimePastDeadline :: Input SimpleTx
stepTimePastDeadline = ChainEvent SimpleTx -> Input SimpleTx
forall tx. ChainEvent tx -> Input tx
ChainInput (ChainEvent SimpleTx -> Input SimpleTx)
-> ChainEvent SimpleTx -> Input SimpleTx
forall a b. (a -> b) -> a -> b
$ UTCTime -> ChainSlot -> ChainEvent SimpleTx
forall tx. UTCTime -> ChainSlot -> ChainEvent tx
Tick UTCTime
oneSecondsPastDeadline ChainSlot
someChainSlot
          Outcome SimpleTx
outcome2 <- 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
stepTimePastDeadline
          IO () -> StateT (StepState SimpleTx) IO ()
forall (m :: * -> *) a.
Monad m =>
m a -> StateT (StepState SimpleTx) m a
forall (t :: (* -> *) -> * -> *) (m :: * -> *) a.
(MonadTrans t, Monad m) =>
m a -> t m a
lift (IO () -> StateT (StepState SimpleTx) IO ())
-> IO () -> StateT (StepState SimpleTx) IO ()
forall a b. (a -> b) -> a -> b
$ Outcome SimpleTx
outcome2 Outcome SimpleTx -> Effect SimpleTx -> IO ()
forall tx.
(HasCallStack, IsChainState tx) =>
Outcome tx -> Effect tx -> IO ()
`hasEffect` ServerOutput SimpleTx -> Effect SimpleTx
forall tx. ServerOutput tx -> Effect tx
ClientEffect (HeadId -> ServerOutput SimpleTx
forall tx. HeadId -> ServerOutput tx
ReadyToFanout HeadId
testHeadId)

      String -> IO () -> SpecWith (Arg (IO ()))
forall a.
(HasCallStack, Example a) =>
String -> a -> SpecWith (Arg a)
it String
"contests when detecting close with old snapshot" (IO () -> SpecWith (Arg (IO ())))
-> IO () -> SpecWith (Arg (IO ()))
forall a b. (a -> b) -> a -> b
$ do
        let snapshotVersion :: SnapshotVersion
snapshotVersion = SnapshotVersion
0
            snapshot :: Snapshot SimpleTx
snapshot = SnapshotNumber
-> SnapshotVersion
-> [TxIdType SimpleTx]
-> UTxOType SimpleTx
-> Snapshot SimpleTx
forall tx.
Monoid (UTxOType tx) =>
SnapshotNumber
-> SnapshotVersion -> [TxIdType tx] -> UTxOType tx -> Snapshot tx
testSnapshot SnapshotNumber
2 SnapshotVersion
snapshotVersion [] Set SimpleTxOut
UTxOType SimpleTx
forall a. Monoid a => a
mempty
            latestConfirmedSnapshot :: ConfirmedSnapshot SimpleTx
latestConfirmedSnapshot = Snapshot SimpleTx
-> MultiSignature (Snapshot SimpleTx) -> ConfirmedSnapshot SimpleTx
forall tx.
Snapshot tx -> MultiSignature (Snapshot tx) -> ConfirmedSnapshot tx
ConfirmedSnapshot Snapshot SimpleTx
snapshot ([Signature (Snapshot SimpleTx)]
-> MultiSignature (Snapshot SimpleTx)
forall {k} (a :: k). [Signature a] -> MultiSignature a
Crypto.aggregate [])
            s0 :: HeadState SimpleTx
s0 =
              [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{confirmedSnapshot = latestConfirmedSnapshot}
            deadline :: UTCTime
deadline = Gen UTCTime
forall a. Arbitrary a => Gen a
arbitrary Gen UTCTime -> Int -> UTCTime
forall a. Gen a -> Int -> a
`generateWith` Int
42
            params :: HeadParameters
params = HeadParameters -> Maybe HeadParameters -> HeadParameters
forall a. a -> Maybe a -> a
fromMaybe (ContestationPeriod -> [Party] -> HeadParameters
HeadParameters ContestationPeriod
defaultContestationPeriod [Party]
threeParties) (HeadState SimpleTx -> Maybe HeadParameters
forall tx. HeadState tx -> Maybe HeadParameters
getHeadParameters HeadState SimpleTx
s0)
        Environment
-> Ledger SimpleTx
-> HeadState SimpleTx
-> StateT (StepState SimpleTx) IO ()
-> IO ()
forall (m :: * -> *) tx a.
Monad m =>
Environment
-> Ledger tx -> HeadState tx -> StateT (StepState tx) m a -> m a
runHeadLogic Environment
bobEnv Ledger SimpleTx
ledger HeadState SimpleTx
s0 (StateT (StepState SimpleTx) IO () -> IO ())
-> StateT (StepState SimpleTx) IO () -> IO ()
forall a b. (a -> b) -> a -> b
$ do
          Outcome SimpleTx
o1 <- 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
$ OnChainTx SimpleTx -> Input SimpleTx
observeTx (HeadId -> SnapshotNumber -> UTCTime -> OnChainTx SimpleTx
forall tx. HeadId -> SnapshotNumber -> UTCTime -> OnChainTx tx
OnCloseTx HeadId
testHeadId SnapshotNumber
0 UTCTime
deadline)
          IO () -> StateT (StepState SimpleTx) IO ()
forall (m :: * -> *) a.
Monad m =>
m a -> StateT (StepState SimpleTx) m a
forall (t :: (* -> *) -> * -> *) (m :: * -> *) a.
(MonadTrans t, Monad m) =>
m a -> t m a
lift (IO () -> StateT (StepState SimpleTx) IO ())
-> IO () -> StateT (StepState SimpleTx) IO ()
forall a b. (a -> b) -> a -> b
$ Outcome SimpleTx
o1 Outcome SimpleTx -> Effect SimpleTx -> IO ()
forall tx.
(HasCallStack, IsChainState tx) =>
Outcome tx -> Effect tx -> IO ()
`hasEffect` PostChainTx SimpleTx -> Effect SimpleTx
chainEffect (HeadId
-> HeadParameters
-> SnapshotVersion
-> ConfirmedSnapshot SimpleTx
-> PostChainTx SimpleTx
forall tx.
HeadId
-> HeadParameters
-> SnapshotVersion
-> ConfirmedSnapshot tx
-> PostChainTx tx
ContestTx HeadId
testHeadId HeadParameters
params SnapshotVersion
snapshotVersion ConfirmedSnapshot SimpleTx
latestConfirmedSnapshot)
          HeadState SimpleTx
s1 <- StateT (StepState SimpleTx) IO (HeadState SimpleTx)
forall tx (m :: * -> *).
MonadState (StepState tx) m =>
m (HeadState tx)
getState
          IO () -> StateT (StepState SimpleTx) IO ()
forall (m :: * -> *) a.
Monad m =>
m a -> StateT (StepState SimpleTx) m a
forall (t :: (* -> *) -> * -> *) (m :: * -> *) a.
(MonadTrans t, Monad m) =>
m a -> t m a
lift (IO () -> StateT (StepState SimpleTx) IO ())
-> IO () -> StateT (StepState SimpleTx) IO ()
forall a b. (a -> b) -> a -> b
$
            HeadState SimpleTx
s1 HeadState SimpleTx -> (HeadState SimpleTx -> Bool) -> IO ()
forall a. (HasCallStack, Show a) => a -> (a -> Bool) -> IO ()
`shouldSatisfy` \case
              Closed ClosedState{} -> Bool
True
              HeadState SimpleTx
_ -> Bool
False

      String -> IO () -> SpecWith (Arg (IO ()))
forall a.
(HasCallStack, Example a) =>
String -> a -> SpecWith (Arg a)
it String
"re-contests when detecting contest with old snapshot" (IO () -> SpecWith (Arg (IO ())))
-> IO () -> SpecWith (Arg (IO ()))
forall a b. (a -> b) -> a -> b
$ do
        let snapshotVersion :: SnapshotVersion
snapshotVersion = SnapshotVersion
0
            snapshot2 :: Snapshot SimpleTx
snapshot2 = SnapshotNumber
-> SnapshotVersion
-> [TxIdType SimpleTx]
-> UTxOType SimpleTx
-> Snapshot SimpleTx
forall tx.
Monoid (UTxOType tx) =>
SnapshotNumber
-> SnapshotVersion -> [TxIdType tx] -> UTxOType tx -> Snapshot tx
testSnapshot SnapshotNumber
2 SnapshotVersion
snapshotVersion [] Set SimpleTxOut
UTxOType SimpleTx
forall a. Monoid a => a
mempty
            latestConfirmedSnapshot :: ConfirmedSnapshot SimpleTx
latestConfirmedSnapshot = Snapshot SimpleTx
-> MultiSignature (Snapshot SimpleTx) -> ConfirmedSnapshot SimpleTx
forall tx.
Snapshot tx -> MultiSignature (Snapshot tx) -> ConfirmedSnapshot tx
ConfirmedSnapshot Snapshot SimpleTx
snapshot2 ([Signature (Snapshot SimpleTx)]
-> MultiSignature (Snapshot SimpleTx)
forall {k} (a :: k). [Signature a] -> MultiSignature a
Crypto.aggregate [])
            s0 :: HeadState SimpleTx
s0 = [Party] -> ConfirmedSnapshot SimpleTx -> HeadState SimpleTx
inClosedState' [Party]
threeParties ConfirmedSnapshot SimpleTx
latestConfirmedSnapshot
            deadline :: UTCTime
deadline = Gen UTCTime
forall a. Arbitrary a => Gen a
arbitrary Gen UTCTime -> Int -> UTCTime
forall a. Gen a -> Int -> a
`generateWith` Int
42
            params :: HeadParameters
params = HeadParameters -> Maybe HeadParameters -> HeadParameters
forall a. a -> Maybe a -> a
fromMaybe (ContestationPeriod -> [Party] -> HeadParameters
HeadParameters ContestationPeriod
defaultContestationPeriod [Party]
threeParties) (HeadState SimpleTx -> Maybe HeadParameters
forall tx. HeadState tx -> Maybe HeadParameters
getHeadParameters HeadState SimpleTx
s0)
        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
ledger HeadState SimpleTx
s0 (OnChainTx SimpleTx -> Input SimpleTx
observeTx (OnChainTx SimpleTx -> Input SimpleTx)
-> OnChainTx SimpleTx -> Input SimpleTx
forall a b. (a -> b) -> a -> b
$ HeadId -> SnapshotNumber -> UTCTime -> OnChainTx SimpleTx
forall tx. HeadId -> SnapshotNumber -> UTCTime -> OnChainTx tx
OnContestTx HeadId
testHeadId SnapshotNumber
1 UTCTime
deadline)
          Outcome SimpleTx -> Effect SimpleTx -> IO ()
forall tx.
(HasCallStack, IsChainState tx) =>
Outcome tx -> Effect tx -> IO ()
`hasEffect` PostChainTx SimpleTx -> Effect SimpleTx
chainEffect (HeadId
-> HeadParameters
-> SnapshotVersion
-> ConfirmedSnapshot SimpleTx
-> PostChainTx SimpleTx
forall tx.
HeadId
-> HeadParameters
-> SnapshotVersion
-> ConfirmedSnapshot tx
-> PostChainTx tx
ContestTx HeadId
testHeadId HeadParameters
params SnapshotVersion
snapshotVersion ConfirmedSnapshot SimpleTx
latestConfirmedSnapshot)

      String -> Property -> SpecWith (Arg Property)
forall a.
(HasCallStack, Example a) =>
String -> a -> SpecWith (Arg a)
it String
"ignores unrelated initTx" Property
prop_ignoresUnrelatedOnInitTx

      String
-> ((Natural, Connectivity, HeadState SimpleTx) -> IO ()) -> Spec
forall prop.
(HasCallStack, Testable prop) =>
String -> prop -> Spec
prop String
"connectivity messages passthrough without affecting the current state" (((Natural, Connectivity, HeadState SimpleTx) -> IO ()) -> Spec)
-> ((Natural, Connectivity, HeadState SimpleTx) -> IO ()) -> Spec
forall a b. (a -> b) -> a -> b
$
        \(Natural
ttl, Connectivity
connectivityMessage, HeadState SimpleTx
headState) -> do
          let input :: Input SimpleTx
input = Natural -> Connectivity -> Input SimpleTx
connectivityChanged Natural
ttl Connectivity
connectivityMessage
          let 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
bobEnv Ledger SimpleTx
ledger HeadState SimpleTx
headState Input SimpleTx
input
          Outcome SimpleTx -> [StateChanged SimpleTx]
forall tx. Outcome tx -> [StateChanged tx]
stateChanges Outcome SimpleTx
outcome [StateChanged SimpleTx] -> [StateChanged SimpleTx] -> IO ()
forall a. (HasCallStack, Show a, Eq a) => a -> a -> IO ()
`shouldBe` []
          Outcome SimpleTx
outcome Outcome SimpleTx -> (Effect SimpleTx -> Bool) -> IO ()
forall tx.
(HasCallStack, IsChainState tx) =>
Outcome tx -> (Effect tx -> Bool) -> IO ()
`hasEffectSatisfying` \case ClientEffect{} -> Bool
True; Effect SimpleTx
_ -> Bool
False

      String -> (HeadId -> IO ()) -> Spec
forall prop.
(HasCallStack, Testable prop) =>
String -> prop -> Spec
prop String
"ignores abortTx of another head" ((HeadId -> IO ()) -> Spec) -> (HeadId -> IO ()) -> Spec
forall a b. (a -> b) -> a -> b
$ \HeadId
otherHeadId -> do
        let abortOtherHead :: Input SimpleTx
abortOtherHead = OnChainTx SimpleTx -> Input SimpleTx
observeTx (OnChainTx SimpleTx -> Input SimpleTx)
-> OnChainTx SimpleTx -> Input SimpleTx
forall a b. (a -> b) -> a -> b
$ OnAbortTx{$sel:headId:OnInitTx :: HeadId
headId = HeadId
otherHeadId}
        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
ledger ([Party] -> HeadState SimpleTx
inInitialState [Party]
threeParties) Input SimpleTx
abortOtherHead
          Outcome SimpleTx -> Outcome SimpleTx -> IO ()
forall a. (HasCallStack, Show a, Eq a) => a -> a -> IO ()
`shouldBe` LogicError SimpleTx -> Outcome SimpleTx
forall tx. LogicError tx -> Outcome tx
Error (NotOurHead{$sel:ourHeadId:UnhandledInput :: HeadId
ourHeadId = HeadId
testHeadId, HeadId
otherHeadId :: HeadId
$sel:otherHeadId:UnhandledInput :: HeadId
otherHeadId})

      String -> (HeadId -> IO ()) -> Spec
forall prop.
(HasCallStack, Testable prop) =>
String -> prop -> Spec
prop String
"ignores collectComTx of another head" ((HeadId -> IO ()) -> Spec) -> (HeadId -> IO ()) -> Spec
forall a b. (a -> b) -> a -> b
$ \HeadId
otherHeadId -> do
        let collectOtherHead :: Input SimpleTx
collectOtherHead = OnChainTx SimpleTx -> Input SimpleTx
observeTx (OnChainTx SimpleTx -> Input SimpleTx)
-> OnChainTx SimpleTx -> Input SimpleTx
forall a b. (a -> b) -> a -> b
$ OnCollectComTx{$sel:headId:OnInitTx :: HeadId
headId = HeadId
otherHeadId}
        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
ledger ([Party] -> HeadState SimpleTx
inInitialState [Party]
threeParties) Input SimpleTx
collectOtherHead
          Outcome SimpleTx -> Outcome SimpleTx -> IO ()
forall a. (HasCallStack, Show a, Eq a) => a -> a -> IO ()
`shouldBe` LogicError SimpleTx -> Outcome SimpleTx
forall tx. LogicError tx -> Outcome tx
Error (NotOurHead{$sel:ourHeadId:UnhandledInput :: HeadId
ourHeadId = HeadId
testHeadId, HeadId
$sel:otherHeadId:UnhandledInput :: HeadId
otherHeadId :: HeadId
otherHeadId})

      String -> (HeadId -> IO ()) -> Spec
forall prop.
(HasCallStack, Testable prop) =>
String -> prop -> Spec
prop String
"ignores decrementTx of another head" ((HeadId -> IO ()) -> Spec) -> (HeadId -> IO ()) -> Spec
forall a b. (a -> b) -> a -> b
$ \HeadId
otherHeadId -> do
        let decrementOtherHead :: Input SimpleTx
decrementOtherHead = OnChainTx SimpleTx -> Input SimpleTx
observeTx (OnChainTx SimpleTx -> Input SimpleTx)
-> OnChainTx SimpleTx -> Input SimpleTx
forall a b. (a -> b) -> a -> b
$ OnDecrementTx{$sel:headId:OnInitTx :: HeadId
headId = HeadId
otherHeadId, $sel:newVersion:OnInitTx :: SnapshotVersion
newVersion = SnapshotVersion
1, $sel:distributedOutputs:OnInitTx :: [TxOutType SimpleTx]
distributedOutputs = [SimpleTxOut]
[TxOutType SimpleTx]
forall a. Monoid a => a
mempty}
        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
ledger ([Party] -> HeadState SimpleTx
inOpenState [Party]
threeParties) Input SimpleTx
decrementOtherHead
          Outcome SimpleTx -> Outcome SimpleTx -> IO ()
forall a. (HasCallStack, Show a, Eq a) => a -> a -> IO ()
`shouldBe` LogicError SimpleTx -> Outcome SimpleTx
forall tx. LogicError tx -> Outcome tx
Error (NotOurHead{$sel:ourHeadId:UnhandledInput :: HeadId
ourHeadId = HeadId
testHeadId, HeadId
$sel:otherHeadId:UnhandledInput :: HeadId
otherHeadId :: HeadId
otherHeadId})

      String -> (HeadId -> SnapshotNumber -> UTCTime -> IO ()) -> Spec
forall prop.
(HasCallStack, Testable prop) =>
String -> prop -> Spec
prop String
"ignores closeTx of another head" ((HeadId -> SnapshotNumber -> UTCTime -> IO ()) -> Spec)
-> (HeadId -> SnapshotNumber -> UTCTime -> IO ()) -> Spec
forall a b. (a -> b) -> a -> b
$ \HeadId
otherHeadId SnapshotNumber
snapshotNumber UTCTime
contestationDeadline -> do
        let openState :: HeadState SimpleTx
openState = [Party] -> HeadState SimpleTx
inOpenState [Party]
threeParties
        let closeOtherHead :: Input SimpleTx
closeOtherHead = OnChainTx SimpleTx -> Input SimpleTx
observeTx (OnChainTx SimpleTx -> Input SimpleTx)
-> OnChainTx SimpleTx -> Input SimpleTx
forall a b. (a -> b) -> a -> b
$ OnCloseTx{$sel:headId:OnInitTx :: HeadId
headId = HeadId
otherHeadId, SnapshotNumber
$sel:snapshotNumber:OnInitTx :: SnapshotNumber
snapshotNumber :: SnapshotNumber
snapshotNumber, UTCTime
$sel:contestationDeadline:OnInitTx :: UTCTime
contestationDeadline :: UTCTime
contestationDeadline}
        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
ledger HeadState SimpleTx
openState Input SimpleTx
closeOtherHead
          Outcome SimpleTx -> Outcome SimpleTx -> IO ()
forall a. (HasCallStack, Show a, Eq a) => a -> a -> IO ()
`shouldBe` LogicError SimpleTx -> Outcome SimpleTx
forall tx. LogicError tx -> Outcome tx
Error (NotOurHead{$sel:ourHeadId:UnhandledInput :: HeadId
ourHeadId = HeadId
testHeadId, HeadId
$sel:otherHeadId:UnhandledInput :: HeadId
otherHeadId :: HeadId
otherHeadId})

      String -> (HeadId -> SnapshotNumber -> UTCTime -> IO ()) -> Spec
forall prop.
(HasCallStack, Testable prop) =>
String -> prop -> Spec
prop String
"ignores contestTx of another head" ((HeadId -> SnapshotNumber -> UTCTime -> IO ()) -> Spec)
-> (HeadId -> SnapshotNumber -> UTCTime -> IO ()) -> Spec
forall a b. (a -> b) -> a -> b
$ \HeadId
otherHeadId SnapshotNumber
snapshotNumber UTCTime
contestationDeadline -> do
        let contestOtherHead :: Input SimpleTx
contestOtherHead = OnChainTx SimpleTx -> Input SimpleTx
observeTx (OnChainTx SimpleTx -> Input SimpleTx)
-> OnChainTx SimpleTx -> Input SimpleTx
forall a b. (a -> b) -> a -> b
$ OnContestTx{$sel:headId:OnInitTx :: HeadId
headId = HeadId
otherHeadId, SnapshotNumber
$sel:snapshotNumber:OnInitTx :: SnapshotNumber
snapshotNumber :: SnapshotNumber
snapshotNumber, UTCTime
$sel:contestationDeadline:OnInitTx :: UTCTime
contestationDeadline :: UTCTime
contestationDeadline}
        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
ledger ([Party] -> HeadState SimpleTx
inClosedState [Party]
threeParties) Input SimpleTx
contestOtherHead
          Outcome SimpleTx -> Outcome SimpleTx -> IO ()
forall a. (HasCallStack, Show a, Eq a) => a -> a -> IO ()
`shouldBe` LogicError SimpleTx -> Outcome SimpleTx
forall tx. LogicError tx -> Outcome tx
Error (NotOurHead{$sel:ourHeadId:UnhandledInput :: HeadId
ourHeadId = HeadId
testHeadId, HeadId
$sel:otherHeadId:UnhandledInput :: HeadId
otherHeadId :: HeadId
otherHeadId})

      String -> (HeadId -> IO ()) -> Spec
forall prop.
(HasCallStack, Testable prop) =>
String -> prop -> Spec
prop String
"ignores fanoutTx of another head" ((HeadId -> IO ()) -> Spec) -> (HeadId -> IO ()) -> Spec
forall a b. (a -> b) -> a -> b
$ \HeadId
otherHeadId -> do
        let collectOtherHead :: Input SimpleTx
collectOtherHead = OnChainTx SimpleTx -> Input SimpleTx
observeTx (OnChainTx SimpleTx -> Input SimpleTx)
-> OnChainTx SimpleTx -> Input SimpleTx
forall a b. (a -> b) -> a -> b
$ OnFanoutTx{$sel:headId:OnInitTx :: HeadId
headId = HeadId
otherHeadId}
        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
ledger ([Party] -> HeadState SimpleTx
inClosedState [Party]
threeParties) Input SimpleTx
collectOtherHead
          Outcome SimpleTx -> Outcome SimpleTx -> IO ()
forall a. (HasCallStack, Show a, Eq a) => a -> a -> IO ()
`shouldBe` LogicError SimpleTx -> Outcome SimpleTx
forall tx. LogicError tx -> Outcome tx
Error (NotOurHead{$sel:ourHeadId:UnhandledInput :: HeadId
ourHeadId = HeadId
testHeadId, HeadId
$sel:otherHeadId:UnhandledInput :: HeadId
otherHeadId :: HeadId
otherHeadId})

    String -> Spec -> Spec
forall a. HasCallStack => String -> SpecWith a -> SpecWith a
describe String
"Coordinated Head Protocol using real Tx" (Spec -> Spec) -> Spec -> Spec
forall a b. (a -> b) -> a -> b
$
      String -> (SlotNo -> Property) -> Spec
forall prop.
(HasCallStack, Testable prop) =>
String -> prop -> Spec
prop String
"any tx with expiring upper validity range gets pruned" ((SlotNo -> Property) -> Spec) -> (SlotNo -> Property) -> Spec
forall a b. (a -> b) -> a -> b
$ \SlotNo
slotNo -> PropertyM IO () -> Property
forall a. Testable a => PropertyM IO a -> Property
monadicIO (PropertyM IO () -> Property) -> PropertyM IO () -> Property
forall a b. (a -> b) -> a -> b
$ do
        ((TxIn, TxOut CtxUTxO)
utxo, Tx
expiringTransaction) <- Gen ((TxIn, TxOut CtxUTxO), Tx)
-> PropertyM IO ((TxIn, TxOut CtxUTxO), Tx)
forall (m :: * -> *) a. (Monad m, Show a) => Gen a -> PropertyM m a
pick (Gen ((TxIn, TxOut CtxUTxO), Tx)
 -> PropertyM IO ((TxIn, TxOut CtxUTxO), Tx))
-> Gen ((TxIn, TxOut CtxUTxO), Tx)
-> PropertyM IO ((TxIn, TxOut CtxUTxO), Tx)
forall a b. (a -> b) -> a -> b
$ do
          (VerificationKey PaymentKey
vk, SigningKey PaymentKey
sk) <- Gen (VerificationKey PaymentKey, SigningKey PaymentKey)
genKeyPair
          TxOut CtxUTxO
txOut <- VerificationKey PaymentKey -> Gen (TxOut CtxUTxO)
forall ctx. VerificationKey PaymentKey -> Gen (TxOut ctx)
genOutput VerificationKey PaymentKey
vk
          (TxIn, TxOut CtxUTxO)
utxo <- (,TxOut CtxUTxO
txOut) (TxIn -> (TxIn, TxOut CtxUTxO))
-> Gen TxIn -> Gen (TxIn, TxOut CtxUTxO)
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> Gen TxIn
genTxIn
          (TxIn, TxOut CtxUTxO)
-> (AddressInEra, Value)
-> SigningKey PaymentKey
-> (Maybe TxValidityLowerBound, Maybe TxValidityUpperBound)
-> Either TxBodyError Tx
mkRangedTx
            (TxIn, TxOut CtxUTxO)
utxo
            (NetworkId -> VerificationKey PaymentKey -> AddressInEra
forall era.
IsShelleyBasedEra era =>
NetworkId -> VerificationKey PaymentKey -> AddressInEra era
mkVkAddress NetworkId
Fixture.testNetworkId VerificationKey PaymentKey
vk, TxOut CtxUTxO -> Value
forall ctx. TxOut ctx -> Value
txOutValue TxOut CtxUTxO
txOut)
            SigningKey PaymentKey
sk
            (Maybe TxValidityLowerBound
forall a. Maybe a
Nothing, TxValidityUpperBound -> Maybe TxValidityUpperBound
forall a. a -> Maybe a
Just (TxValidityUpperBound -> Maybe TxValidityUpperBound)
-> TxValidityUpperBound -> Maybe TxValidityUpperBound
forall a b. (a -> b) -> a -> b
$ SlotNo -> TxValidityUpperBound
TxValidityUpperBound SlotNo
slotNo)
            Either TxBodyError Tx
-> (Either TxBodyError Tx -> Gen ((TxIn, TxOut CtxUTxO), Tx))
-> Gen ((TxIn, TxOut CtxUTxO), Tx)
forall a b. a -> (a -> b) -> b
& \case
              Left TxBodyError
_ -> Text -> Gen ((TxIn, TxOut CtxUTxO), Tx)
forall a t. (HasCallStack, IsText t) => t -> a
Prelude.error Text
"cannot generate expired tx"
              Right Tx
tx -> ((TxIn, TxOut CtxUTxO), Tx) -> Gen ((TxIn, TxOut CtxUTxO), Tx)
forall a. a -> Gen a
forall (f :: * -> *) a. Applicative f => a -> f a
pure ((TxIn, TxOut CtxUTxO)
utxo, Tx
tx)
        let ledger :: Ledger Tx
ledger = Globals -> LedgerEnv (ShelleyLedgerEra Era) -> Ledger Tx
cardanoLedger Globals
Fixture.defaultGlobals LedgerEnv (ShelleyLedgerEra Era)
Fixture.defaultLedgerEnv
            st0 :: HeadState Tx
st0 =
              OpenState Tx -> HeadState Tx
forall tx. OpenState tx -> HeadState tx
Open
                OpenState
                  { $sel:parameters:OpenState :: HeadParameters
parameters = ContestationPeriod -> [Party] -> HeadParameters
HeadParameters ContestationPeriod
defaultContestationPeriod [Party]
threeParties
                  , $sel:coordinatedHeadState:OpenState :: CoordinatedHeadState Tx
coordinatedHeadState =
                      CoordinatedHeadState
                        { $sel:localUTxO:CoordinatedHeadState :: UTxOType Tx
localUTxO = (TxIn, TxOut CtxUTxO) -> UTxO' (TxOut CtxUTxO)
forall out. (TxIn, out) -> UTxO' out
UTxO.singleton (TxIn, TxOut CtxUTxO)
utxo
                        , $sel:allTxs:CoordinatedHeadState :: Map (TxIdType Tx) Tx
allTxs = Map TxId Tx
Map (TxIdType Tx) Tx
forall a. Monoid a => a
mempty
                        , $sel:localTxs:CoordinatedHeadState :: [Tx]
localTxs = [Tx
expiringTransaction]
                        , $sel:confirmedSnapshot:CoordinatedHeadState :: ConfirmedSnapshot Tx
confirmedSnapshot = HeadId -> UTxOType Tx -> ConfirmedSnapshot Tx
forall tx. HeadId -> UTxOType tx -> ConfirmedSnapshot tx
InitialSnapshot HeadId
testHeadId (UTxOType Tx -> ConfirmedSnapshot Tx)
-> UTxOType Tx -> ConfirmedSnapshot Tx
forall a b. (a -> b) -> a -> b
$ (TxIn, TxOut CtxUTxO) -> UTxO' (TxOut CtxUTxO)
forall out. (TxIn, out) -> UTxO' out
UTxO.singleton (TxIn, TxOut CtxUTxO)
utxo
                        , $sel:seenSnapshot:CoordinatedHeadState :: SeenSnapshot Tx
seenSnapshot = SeenSnapshot Tx
forall tx. SeenSnapshot tx
NoSeenSnapshot
                        , $sel:decommitTx:CoordinatedHeadState :: Maybe Tx
decommitTx = Maybe Tx
forall a. Maybe a
Nothing
                        , $sel:version:CoordinatedHeadState :: SnapshotVersion
version = SnapshotVersion
0
                        }
                  , $sel:chainState:OpenState :: ChainStateType Tx
chainState = Text -> ChainStateAt
forall a t. (HasCallStack, IsText t) => t -> a
Prelude.error Text
"should not be used"
                  , $sel:headId:OpenState :: HeadId
headId = HeadId
testHeadId
                  , $sel:headSeed:OpenState :: HeadSeed
headSeed = HeadSeed
testHeadSeed
                  , $sel:currentSlot:OpenState :: ChainSlot
currentSlot = Natural -> ChainSlot
ChainSlot (Natural -> ChainSlot)
-> (SlotNo -> Natural) -> SlotNo -> ChainSlot
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Word64 -> Natural
forall a b. (Integral a, Num b) => a -> b
fromIntegral (Word64 -> Natural) -> (SlotNo -> Word64) -> SlotNo -> Natural
forall b c a. (b -> c) -> (a -> b) -> a -> c
. SlotNo -> Word64
unSlotNo (SlotNo -> ChainSlot) -> SlotNo -> ChainSlot
forall a b. (a -> b) -> a -> b
$ SlotNo
slotNo SlotNo -> SlotNo -> SlotNo
forall a. Num a => a -> a -> a
+ SlotNo
1
                  }

        HeadState Tx
st <-
          IO (HeadState Tx) -> PropertyM IO (HeadState Tx)
forall (m :: * -> *) a. Monad m => m a -> PropertyM m a
run (IO (HeadState Tx) -> PropertyM IO (HeadState Tx))
-> IO (HeadState Tx) -> PropertyM IO (HeadState Tx)
forall a b. (a -> b) -> a -> b
$
            Environment
-> Ledger Tx
-> HeadState Tx
-> StateT (StepState Tx) IO (HeadState Tx)
-> IO (HeadState Tx)
forall (m :: * -> *) tx a.
Monad m =>
Environment
-> Ledger tx -> HeadState tx -> StateT (StepState tx) m a -> m a
runHeadLogic Environment
bobEnv Ledger Tx
ledger HeadState Tx
st0 (StateT (StepState Tx) IO (HeadState Tx) -> IO (HeadState Tx))
-> StateT (StepState Tx) IO (HeadState Tx) -> IO (HeadState Tx)
forall a b. (a -> b) -> a -> b
$ do
              Input Tx -> StateT (StepState Tx) IO (Outcome Tx)
forall tx (m :: * -> *).
(MonadState (StepState tx) m, IsChainState tx) =>
Input tx -> m (Outcome tx)
step (Message Tx -> Input Tx
forall tx. Message tx -> Input tx
receiveMessage (Message Tx -> Input Tx) -> Message Tx -> Input Tx
forall a b. (a -> b) -> a -> b
$ SnapshotVersion
-> SnapshotNumber -> [TxIdType Tx] -> Maybe Tx -> Message Tx
forall tx.
SnapshotVersion
-> SnapshotNumber -> [TxIdType tx] -> Maybe tx -> Message tx
ReqSn SnapshotVersion
0 SnapshotNumber
1 [] Maybe Tx
forall a. Maybe a
Nothing)
              StateT (StepState Tx) IO (HeadState Tx)
forall tx (m :: * -> *).
MonadState (StepState tx) m =>
m (HeadState tx)
getState

        Bool -> PropertyM IO ()
forall (m :: * -> *). Monad m => Bool -> PropertyM m ()
assert (Bool -> PropertyM IO ()) -> Bool -> PropertyM IO ()
forall a b. (a -> b) -> a -> b
$ case HeadState Tx
st of
          Open
            OpenState
              { $sel:coordinatedHeadState:OpenState :: forall tx. OpenState tx -> CoordinatedHeadState tx
coordinatedHeadState =
                CoordinatedHeadState{[Tx]
$sel:localTxs:CoordinatedHeadState :: forall tx. CoordinatedHeadState tx -> [tx]
localTxs :: [Tx]
localTxs}
              } -> [Tx] -> Bool
forall a. [a] -> Bool
forall (t :: * -> *) a. Foldable t => t a -> Bool
null [Tx]
localTxs
          HeadState Tx
_ -> Bool
False

    String -> (Tx -> IO ()) -> Spec
forall prop.
(HasCallStack, Testable prop) =>
String -> prop -> Spec
prop String
"empty inputs in decommit tx are prevented" ((Tx -> IO ()) -> Spec) -> (Tx -> IO ()) -> Spec
forall a b. (a -> b) -> a -> b
$ \Tx
tx -> do
      let ledger :: Ledger Tx
ledger = Globals -> LedgerEnv (ShelleyLedgerEra Era) -> Ledger Tx
cardanoLedger Globals
Fixture.defaultGlobals LedgerEnv (ShelleyLedgerEra Era)
Fixture.defaultLedgerEnv
      let st :: HeadState Tx
st =
            OpenState Tx -> HeadState Tx
forall tx. OpenState tx -> HeadState tx
Open
              OpenState
                { $sel:parameters:OpenState :: HeadParameters
parameters = ContestationPeriod -> [Party] -> HeadParameters
HeadParameters ContestationPeriod
defaultContestationPeriod [Party]
threeParties
                , $sel:coordinatedHeadState:OpenState :: CoordinatedHeadState Tx
coordinatedHeadState =
                    CoordinatedHeadState
                      { $sel:localUTxO:CoordinatedHeadState :: UTxOType Tx
localUTxO = UTxOType Tx
forall a. Monoid a => a
mempty
                      , $sel:allTxs:CoordinatedHeadState :: Map (TxIdType Tx) Tx
allTxs = Map (TxIdType Tx) Tx
forall a. Monoid a => a
mempty
                      , $sel:localTxs:CoordinatedHeadState :: [Tx]
localTxs = []
                      , $sel:confirmedSnapshot:CoordinatedHeadState :: ConfirmedSnapshot Tx
confirmedSnapshot = HeadId -> UTxOType Tx -> ConfirmedSnapshot Tx
forall tx. HeadId -> UTxOType tx -> ConfirmedSnapshot tx
InitialSnapshot HeadId
testHeadId UTxOType Tx
forall a. Monoid a => a
mempty
                      , $sel:seenSnapshot:CoordinatedHeadState :: SeenSnapshot Tx
seenSnapshot = SeenSnapshot Tx
forall tx. SeenSnapshot tx
NoSeenSnapshot
                      , $sel:decommitTx:CoordinatedHeadState :: Maybe Tx
decommitTx = Maybe Tx
forall a. Maybe a
Nothing
                      , $sel:version:CoordinatedHeadState :: SnapshotVersion
version = SnapshotVersion
0
                      }
                , $sel:chainState:OpenState :: ChainStateType Tx
chainState = Text -> ChainStateType Tx
forall a t. (HasCallStack, IsText t) => t -> a
Prelude.error Text
"should not be used"
                , $sel:headId:OpenState :: HeadId
headId = HeadId
testHeadId
                , $sel:headSeed:OpenState :: HeadSeed
headSeed = HeadSeed
testHeadSeed
                , $sel:currentSlot:OpenState :: ChainSlot
currentSlot = Natural -> ChainSlot
ChainSlot Natural
1
                }

      let tx' :: Tx
tx' = Tx (ShelleyLedgerEra Era) -> Tx
forall era.
IsShelleyBasedEra era =>
Tx (ShelleyLedgerEra era) -> Tx era
fromLedgerTx (Tx -> Tx (ShelleyLedgerEra Era)
forall era. Tx era -> Tx (ShelleyLedgerEra era)
toLedgerTx Tx
tx Tx (ShelleyLedgerEra Era)
-> (Tx (ShelleyLedgerEra Era) -> AlonzoTx StandardConway)
-> AlonzoTx StandardConway
forall a b. a -> (a -> b) -> b
& (TxBody (ShelleyLedgerEra Era)
 -> Identity (TxBody (ShelleyLedgerEra Era)))
-> Tx (ShelleyLedgerEra Era)
-> Identity (Tx (ShelleyLedgerEra Era))
(TxBody (ShelleyLedgerEra Era)
 -> Identity (TxBody (ShelleyLedgerEra Era)))
-> Tx (ShelleyLedgerEra Era) -> Identity (AlonzoTx StandardConway)
forall era. EraTx era => Lens' (Tx era) (TxBody era)
Lens' (Tx (ShelleyLedgerEra Era)) (TxBody (ShelleyLedgerEra Era))
bodyTxL ((TxBody (ShelleyLedgerEra Era)
  -> Identity (TxBody (ShelleyLedgerEra Era)))
 -> Tx (ShelleyLedgerEra Era) -> Identity (AlonzoTx StandardConway))
-> ((Set (TxIn (EraCrypto StandardConway))
     -> Identity (Set (TxIn (EraCrypto StandardConway))))
    -> TxBody (ShelleyLedgerEra Era)
    -> Identity (TxBody (ShelleyLedgerEra Era)))
-> (Set (TxIn (EraCrypto StandardConway))
    -> Identity (Set (TxIn (EraCrypto StandardConway))))
-> Tx (ShelleyLedgerEra Era)
-> Identity (AlonzoTx StandardConway)
forall b c a. (b -> c) -> (a -> b) -> a -> c
. (Set (TxIn (EraCrypto StandardConway))
 -> Identity (Set (TxIn (EraCrypto StandardConway))))
-> TxBody (ShelleyLedgerEra Era)
-> Identity (TxBody (ShelleyLedgerEra Era))
(Set (TxIn (EraCrypto StandardConway))
 -> Identity (Set (TxIn (EraCrypto StandardConway))))
-> TxBody StandardConway -> Identity (TxBody StandardConway)
forall era.
EraTxBody era =>
Lens' (TxBody era) (Set (TxIn (EraCrypto era)))
Lens'
  (TxBody StandardConway) (Set (TxIn (EraCrypto StandardConway)))
inputsTxBodyL ((Set (TxIn (EraCrypto StandardConway))
  -> Identity (Set (TxIn (EraCrypto StandardConway))))
 -> Tx (ShelleyLedgerEra Era) -> Identity (AlonzoTx StandardConway))
-> Set (TxIn (EraCrypto StandardConway))
-> Tx (ShelleyLedgerEra Era)
-> AlonzoTx StandardConway
forall s t a b. ASetter s t a b -> b -> s -> t
.~ Set (TxIn (EraCrypto StandardConway))
forall a. Monoid a => a
mempty)
      let input :: Input Tx
input = Message Tx -> Input Tx
forall tx. Message tx -> Input tx
receiveMessage (Message Tx -> Input Tx) -> Message Tx -> Input Tx
forall a b. (a -> b) -> a -> b
$ ReqDec{$sel:transaction:ReqTx :: Tx
transaction = Tx
tx'}
      Environment -> Ledger Tx -> HeadState Tx -> Input Tx -> Outcome Tx
forall tx.
IsChainState tx =>
Environment -> Ledger tx -> HeadState tx -> Input tx -> Outcome tx
update Environment
bobEnv Ledger Tx
ledger HeadState Tx
st Input Tx
input Outcome Tx -> (Outcome Tx -> Bool) -> IO ()
forall a. (HasCallStack, Show a) => a -> (a -> Bool) -> IO ()
`shouldSatisfy` \case
        Wait WaitOnNotApplicableDecommitTx{$sel:notApplicableReason:WaitOnNotApplicableTx :: forall tx. WaitReason tx -> DecommitInvalidReason tx
notApplicableReason = DecommitTxInvalid{}} [StateChanged Tx]
_ -> Bool
True
        Outcome Tx
_ -> Bool
False

-- * Properties

prop_ignoresUnrelatedOnInitTx :: Property
prop_ignoresUnrelatedOnInitTx :: Property
prop_ignoresUnrelatedOnInitTx =
  Gen Environment -> (Environment -> Property) -> Property
forall a prop.
(Show a, Testable prop) =>
Gen a -> (a -> prop) -> Property
forAll Gen Environment
forall a. Arbitrary a => Gen a
arbitrary ((Environment -> Property) -> Property)
-> (Environment -> Property) -> Property
forall a b. (a -> b) -> a -> b
$ \Environment
env ->
    Gen (OnChainTx SimpleTx)
-> (OnChainTx SimpleTx -> Property) -> Property
forall a prop.
(Show a, Testable prop) =>
Gen a -> (a -> prop) -> Property
forAll (Environment -> Gen (OnChainTx SimpleTx)
forall {tx}. Environment -> Gen (OnChainTx tx)
genUnrelatedInit Environment
env) ((OnChainTx SimpleTx -> Property) -> Property)
-> (OnChainTx SimpleTx -> Property) -> Property
forall a b. (a -> b) -> a -> b
$ \OnChainTx SimpleTx
unrelatedInit -> do
      let 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
env Ledger SimpleTx
simpleLedger HeadState SimpleTx
inIdleState (OnChainTx SimpleTx -> Input SimpleTx
observeTx OnChainTx SimpleTx
unrelatedInit)
      String -> IO () -> Property
forall prop. Testable prop => String -> prop -> Property
counterexample (String
"Outcome: " String -> String -> String
forall a. Semigroup a => a -> a -> a
<> Outcome SimpleTx -> String
forall b a. (Show a, IsString b) => a -> b
show Outcome SimpleTx
outcome) (IO () -> Property) -> IO () -> Property
forall a b. (a -> b) -> a -> b
$
        Outcome SimpleTx
outcome
          Outcome SimpleTx -> (Effect SimpleTx -> Bool) -> IO ()
forall tx.
(HasCallStack, IsChainState tx) =>
Outcome tx -> (Effect tx -> Bool) -> IO ()
`hasEffectSatisfying` \case
            ClientEffect IgnoredHeadInitializing{} -> Bool
True
            Effect SimpleTx
_ -> Bool
False
 where
  genUnrelatedInit :: Environment -> Gen (OnChainTx tx)
genUnrelatedInit Environment
env =
    [Gen (OnChainTx tx)] -> Gen (OnChainTx tx)
forall a. [Gen a] -> Gen a
oneof
      [ Environment -> Gen (OnChainTx tx)
forall {tx}. Environment -> Gen (OnChainTx tx)
genOnInitWithDifferentContestationPeriod Environment
env
      , Environment -> Gen (OnChainTx tx)
forall {tx}. Environment -> Gen (OnChainTx tx)
genOnInitWithoutParty Environment
env
      , Environment -> Gen (OnChainTx tx)
forall {tx}. Environment -> Gen (OnChainTx tx)
genOnInitWithoutOnChainId Environment
env
      ]

  genOnInitWithDifferentContestationPeriod :: Environment -> Gen (OnChainTx tx)
genOnInitWithDifferentContestationPeriod Environment{Party
$sel:party:Environment :: Environment -> Party
party :: Party
party, ContestationPeriod
$sel:contestationPeriod:Environment :: Environment -> ContestationPeriod
contestationPeriod :: ContestationPeriod
contestationPeriod, [OnChainId]
$sel:participants:Environment :: Environment -> [OnChainId]
participants :: [OnChainId]
participants} = do
    HeadId
headId <- Gen HeadId
forall a. Arbitrary a => Gen a
arbitrary
    HeadSeed
headSeed <- Gen HeadSeed
forall a. Arbitrary a => Gen a
arbitrary
    ContestationPeriod
cp <- Gen ContestationPeriod
forall a. Arbitrary a => Gen a
arbitrary Gen ContestationPeriod
-> (ContestationPeriod -> Bool) -> Gen ContestationPeriod
forall a. Gen a -> (a -> Bool) -> Gen a
`suchThat` (ContestationPeriod -> ContestationPeriod -> Bool
forall a. Eq a => a -> a -> Bool
/= ContestationPeriod
contestationPeriod)
    [Party]
parties <- [Party] -> Gen [Party]
forall a. [a] -> Gen [a]
shuffle ([Party] -> Gen [Party]) -> Gen [Party] -> Gen [Party]
forall (m :: * -> *) a b. Monad m => (a -> m b) -> m a -> m b
=<< (Gen [Party]
forall a. Arbitrary a => Gen a
arbitrary Gen [Party] -> ([Party] -> [Party]) -> Gen [Party]
forall (f :: * -> *) a b. Functor f => f a -> (a -> b) -> f b
<&> (Party
party :))
    OnChainTx tx -> Gen (OnChainTx tx)
forall a. a -> Gen a
forall (f :: * -> *) a. Applicative f => a -> f a
pure
      OnInitTx
        { HeadId
$sel:headId:OnInitTx :: HeadId
headId :: HeadId
headId
        , HeadSeed
headSeed :: HeadSeed
$sel:headSeed:OnInitTx :: HeadSeed
headSeed
        , $sel:headParameters:OnInitTx :: HeadParameters
headParameters = HeadParameters{$sel:contestationPeriod:HeadParameters :: ContestationPeriod
contestationPeriod = ContestationPeriod
cp, [Party]
parties :: [Party]
$sel:parties:HeadParameters :: [Party]
parties}
        , [OnChainId]
participants :: [OnChainId]
$sel:participants:OnInitTx :: [OnChainId]
participants
        }

  genOnInitWithoutParty :: Environment -> Gen (OnChainTx tx)
genOnInitWithoutParty Environment{Party
$sel:party:Environment :: Environment -> Party
party :: Party
party, [Party]
$sel:otherParties:Environment :: Environment -> [Party]
otherParties :: [Party]
otherParties, ContestationPeriod
$sel:contestationPeriod:Environment :: Environment -> ContestationPeriod
contestationPeriod :: ContestationPeriod
contestationPeriod, [OnChainId]
$sel:participants:Environment :: Environment -> [OnChainId]
participants :: [OnChainId]
participants} = do
    HeadId
headId <- Gen HeadId
forall a. Arbitrary a => Gen a
arbitrary
    HeadSeed
headSeed <- Gen HeadSeed
forall a. Arbitrary a => Gen a
arbitrary
    [Party]
allParties <- [Party] -> Gen [Party]
forall a. [a] -> Gen [a]
shuffle (Party
party Party -> [Party] -> [Party]
forall a. a -> [a] -> [a]
: [Party]
otherParties)
    Party
toRemove <- [Party] -> Gen Party
forall a. [a] -> Gen a
elements [Party]
allParties
    let differentParties :: [Party]
differentParties = Party -> [Party] -> [Party]
forall a. Eq a => a -> [a] -> [a]
List.delete Party
toRemove [Party]
allParties
    OnChainTx tx -> Gen (OnChainTx tx)
forall a. a -> Gen a
forall (f :: * -> *) a. Applicative f => a -> f a
pure
      OnInitTx
        { HeadId
$sel:headId:OnInitTx :: HeadId
headId :: HeadId
headId
        , HeadSeed
$sel:headSeed:OnInitTx :: HeadSeed
headSeed :: HeadSeed
headSeed
        , $sel:headParameters:OnInitTx :: HeadParameters
headParameters = HeadParameters{ContestationPeriod
$sel:contestationPeriod:HeadParameters :: ContestationPeriod
contestationPeriod :: ContestationPeriod
contestationPeriod, $sel:parties:HeadParameters :: [Party]
parties = [Party]
differentParties}
        , [OnChainId]
$sel:participants:OnInitTx :: [OnChainId]
participants :: [OnChainId]
participants
        }

  genOnInitWithoutOnChainId :: Environment -> Gen (OnChainTx tx)
genOnInitWithoutOnChainId Environment{Party
$sel:party:Environment :: Environment -> Party
party :: Party
party, [Party]
$sel:otherParties:Environment :: Environment -> [Party]
otherParties :: [Party]
otherParties, ContestationPeriod
$sel:contestationPeriod:Environment :: Environment -> ContestationPeriod
contestationPeriod :: ContestationPeriod
contestationPeriod, [OnChainId]
$sel:participants:Environment :: Environment -> [OnChainId]
participants :: [OnChainId]
participants} = do
    HeadId
headId <- Gen HeadId
forall a. Arbitrary a => Gen a
arbitrary
    HeadSeed
headSeed <- Gen HeadSeed
forall a. Arbitrary a => Gen a
arbitrary
    [OnChainId]
differentParticipants <- case [OnChainId]
participants of
      [] -> (OnChainId -> [OnChainId] -> [OnChainId]
forall a. a -> [a] -> [a]
: []) (OnChainId -> [OnChainId]) -> Gen OnChainId -> Gen [OnChainId]
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> Gen OnChainId
forall a. Arbitrary a => Gen a
arbitrary
      [OnChainId]
ps -> do
        OnChainId
toRemove <- [OnChainId] -> Gen OnChainId
forall a. [a] -> Gen a
elements [OnChainId]
participants
        [OnChainId] -> Gen [OnChainId]
forall a. a -> Gen a
forall (f :: * -> *) a. Applicative f => a -> f a
pure ([OnChainId] -> Gen [OnChainId]) -> [OnChainId] -> Gen [OnChainId]
forall a b. (a -> b) -> a -> b
$ OnChainId -> [OnChainId] -> [OnChainId]
forall a. Eq a => a -> [a] -> [a]
List.delete OnChainId
toRemove [OnChainId]
ps
    OnChainTx tx -> Gen (OnChainTx tx)
forall a. a -> Gen a
forall (f :: * -> *) a. Applicative f => a -> f a
pure
      OnInitTx
        { HeadId
$sel:headId:OnInitTx :: HeadId
headId :: HeadId
headId
        , HeadSeed
$sel:headSeed:OnInitTx :: HeadSeed
headSeed :: HeadSeed
headSeed
        , $sel:headParameters:OnInitTx :: HeadParameters
headParameters = HeadParameters{ContestationPeriod
$sel:contestationPeriod:HeadParameters :: ContestationPeriod
contestationPeriod :: ContestationPeriod
contestationPeriod, $sel:parties:HeadParameters :: [Party]
parties = Party
party Party -> [Party] -> [Party]
forall a. a -> [a] -> [a]
: [Party]
otherParties}
        , $sel:participants:OnInitTx :: [OnChainId]
participants = [OnChainId]
differentParticipants
        }

-- * Utilities

-- | Create a network input about a received protocol message with 'defaultTTL'
-- and 'alice' as the sender.
receiveMessage :: Message tx -> Input tx
receiveMessage :: forall tx. Message tx -> Input tx
receiveMessage = Party -> Message tx -> Input tx
forall tx. Party -> Message tx -> Input tx
receiveMessageFrom Party
alice

-- | Create a network input about a received protocol message with 'defaultTTL'
-- from given sender.
receiveMessageFrom :: Party -> Message tx -> Input tx
receiveMessageFrom :: forall tx. Party -> Message tx -> Input tx
receiveMessageFrom Party
sender Message tx
msg =
  Natural -> NetworkEvent (Message tx) -> Input tx
forall tx. Natural -> NetworkEvent (Message tx) -> Input tx
NetworkInput Natural
defaultTTL (NetworkEvent (Message tx) -> Input tx)
-> NetworkEvent (Message tx) -> Input tx
forall a b. (a -> b) -> a -> b
$ ReceivedMessage{Party
$sel:sender:ConnectivityEvent :: Party
sender :: Party
sender, Message tx
$sel:msg:ConnectivityEvent :: Message tx
msg :: Message tx
msg}

-- | Create a chain effect with fixed chain state and slot.
chainEffect :: PostChainTx SimpleTx -> Effect SimpleTx
chainEffect :: PostChainTx SimpleTx -> Effect SimpleTx
chainEffect PostChainTx SimpleTx
postChainTx =
  OnChainEffect
    { PostChainTx SimpleTx
$sel:postChainTx:ClientEffect :: PostChainTx SimpleTx
postChainTx :: PostChainTx SimpleTx
postChainTx
    }

-- | Create an observation chain input with chain state at given slot.
observeTxAtSlot :: Natural -> OnChainTx SimpleTx -> Input SimpleTx
observeTxAtSlot :: Natural -> OnChainTx SimpleTx -> Input SimpleTx
observeTxAtSlot Natural
slot OnChainTx SimpleTx
observedTx =
  ChainInput
    { $sel:chainEvent:ClientInput :: ChainEvent SimpleTx
chainEvent =
        Observation
          { OnChainTx SimpleTx
observedTx :: OnChainTx SimpleTx
$sel:observedTx:Observation :: OnChainTx SimpleTx
observedTx
          , $sel:newChainState:Observation :: ChainStateType SimpleTx
newChainState = SimpleChainState{$sel:slot:SimpleChainState :: ChainSlot
slot = Natural -> ChainSlot
ChainSlot Natural
slot}
          }
    }

-- | Create an observation chain input with fixed chain state and slot.
observeTx :: OnChainTx SimpleTx -> Input SimpleTx
observeTx :: OnChainTx SimpleTx -> Input SimpleTx
observeTx = Natural -> OnChainTx SimpleTx -> Input SimpleTx
observeTxAtSlot Natural
0

connectivityChanged :: TTL -> Connectivity -> Input SimpleTx
connectivityChanged :: Natural -> Connectivity -> Input SimpleTx
connectivityChanged Natural
ttl Connectivity
connectivityMessage =
  NetworkInput
    { Natural
ttl :: Natural
$sel:ttl:ClientInput :: Natural
ttl
    , $sel:networkEvent:ClientInput :: NetworkEvent (Message SimpleTx)
networkEvent = Connectivity -> NetworkEvent (Message SimpleTx)
forall msg. Connectivity -> NetworkEvent msg
ConnectivityEvent Connectivity
connectivityMessage
    }

inIdleState :: HeadState SimpleTx
inIdleState :: HeadState SimpleTx
inIdleState =
  IdleState SimpleTx -> HeadState SimpleTx
forall tx. IdleState tx -> HeadState tx
Idle IdleState{$sel:chainState:IdleState :: ChainStateType SimpleTx
chainState = SimpleChainState{$sel:slot:SimpleChainState :: ChainSlot
slot = Natural -> ChainSlot
ChainSlot Natural
0}}

-- XXX: This is always called with threeParties and simpleLedger
inInitialState :: [Party] -> HeadState SimpleTx
inInitialState :: [Party] -> HeadState SimpleTx
inInitialState [Party]
parties =
  InitialState SimpleTx -> HeadState SimpleTx
forall tx. InitialState tx -> HeadState tx
Initial
    InitialState
      { HeadParameters
parameters :: HeadParameters
$sel:parameters:InitialState :: HeadParameters
parameters
      , $sel:pendingCommits:InitialState :: PendingCommits
pendingCommits = [Party] -> PendingCommits
forall a. Ord a => [a] -> Set a
Set.fromList [Party]
parties
      , $sel:committed:InitialState :: Committed SimpleTx
committed = Map Party (Set SimpleTxOut)
Committed SimpleTx
forall a. Monoid a => a
mempty
      , $sel:chainState:InitialState :: ChainStateType SimpleTx
chainState = SimpleChainState{$sel:slot:SimpleChainState :: ChainSlot
slot = Natural -> ChainSlot
ChainSlot Natural
0}
      , $sel:headId:InitialState :: HeadId
headId = HeadId
testHeadId
      , $sel:headSeed:InitialState :: HeadSeed
headSeed = HeadSeed
testHeadSeed
      }
 where
  parameters :: HeadParameters
parameters = ContestationPeriod -> [Party] -> HeadParameters
HeadParameters ContestationPeriod
defaultContestationPeriod [Party]
parties

-- XXX: This is always called with threeParties and simpleLedger
inOpenState ::
  [Party] ->
  HeadState SimpleTx
inOpenState :: [Party] -> HeadState SimpleTx
inOpenState [Party]
parties =
  [Party] -> CoordinatedHeadState SimpleTx -> HeadState SimpleTx
inOpenState' [Party]
parties (CoordinatedHeadState SimpleTx -> HeadState SimpleTx)
-> CoordinatedHeadState SimpleTx -> HeadState SimpleTx
forall a b. (a -> b) -> a -> b
$
    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
      , ConfirmedSnapshot SimpleTx
$sel:confirmedSnapshot:CoordinatedHeadState :: ConfirmedSnapshot SimpleTx
confirmedSnapshot :: ConfirmedSnapshot SimpleTx
confirmedSnapshot
      , $sel:seenSnapshot:CoordinatedHeadState :: SeenSnapshot SimpleTx
seenSnapshot = SeenSnapshot SimpleTx
forall tx. SeenSnapshot tx
NoSeenSnapshot
      , $sel:decommitTx:CoordinatedHeadState :: Maybe SimpleTx
decommitTx = Maybe SimpleTx
forall a. Maybe a
Nothing
      , $sel:version:CoordinatedHeadState :: SnapshotVersion
version = SnapshotVersion
0
      }
 where
  u0 :: Set SimpleTxOut
u0 = Set SimpleTxOut
forall a. Monoid a => a
mempty
  confirmedSnapshot :: ConfirmedSnapshot SimpleTx
confirmedSnapshot = HeadId -> UTxOType SimpleTx -> ConfirmedSnapshot SimpleTx
forall tx. HeadId -> UTxOType tx -> ConfirmedSnapshot tx
InitialSnapshot HeadId
testHeadId Set SimpleTxOut
UTxOType SimpleTx
u0

inOpenState' ::
  [Party] ->
  CoordinatedHeadState SimpleTx ->
  HeadState SimpleTx
inOpenState' :: [Party] -> CoordinatedHeadState SimpleTx -> HeadState SimpleTx
inOpenState' [Party]
parties CoordinatedHeadState SimpleTx
coordinatedHeadState =
  OpenState SimpleTx -> HeadState SimpleTx
forall tx. OpenState tx -> HeadState tx
Open
    OpenState
      { HeadParameters
$sel:parameters:OpenState :: HeadParameters
parameters :: HeadParameters
parameters
      , CoordinatedHeadState SimpleTx
$sel:coordinatedHeadState:OpenState :: CoordinatedHeadState SimpleTx
coordinatedHeadState :: CoordinatedHeadState SimpleTx
coordinatedHeadState
      , $sel:chainState:OpenState :: ChainStateType SimpleTx
chainState = SimpleChainState{$sel:slot:SimpleChainState :: ChainSlot
slot = ChainSlot
chainSlot}
      , $sel:headId:OpenState :: HeadId
headId = HeadId
testHeadId
      , $sel:headSeed:OpenState :: HeadSeed
headSeed = HeadSeed
testHeadSeed
      , $sel:currentSlot:OpenState :: ChainSlot
currentSlot = ChainSlot
chainSlot
      }
 where
  parameters :: HeadParameters
parameters = ContestationPeriod -> [Party] -> HeadParameters
HeadParameters ContestationPeriod
defaultContestationPeriod [Party]
parties

  chainSlot :: ChainSlot
chainSlot = Natural -> ChainSlot
ChainSlot Natural
0

-- XXX: This is always called with 'threeParties'
inClosedState :: [Party] -> HeadState SimpleTx
inClosedState :: [Party] -> HeadState SimpleTx
inClosedState [Party]
parties = [Party] -> ConfirmedSnapshot SimpleTx -> HeadState SimpleTx
inClosedState' [Party]
parties ConfirmedSnapshot SimpleTx
snapshot0
 where
  snapshot0 :: ConfirmedSnapshot SimpleTx
snapshot0 = HeadId -> UTxOType SimpleTx -> ConfirmedSnapshot SimpleTx
forall tx. HeadId -> UTxOType tx -> ConfirmedSnapshot tx
InitialSnapshot HeadId
testHeadId Set SimpleTxOut
UTxOType SimpleTx
u0
  u0 :: Set SimpleTxOut
u0 = Set SimpleTxOut
forall a. Monoid a => a
mempty

inClosedState' :: [Party] -> ConfirmedSnapshot SimpleTx -> HeadState SimpleTx
inClosedState' :: [Party] -> ConfirmedSnapshot SimpleTx -> HeadState SimpleTx
inClosedState' [Party]
parties ConfirmedSnapshot SimpleTx
confirmedSnapshot =
  ClosedState SimpleTx -> HeadState SimpleTx
forall tx. ClosedState tx -> HeadState tx
Closed
    ClosedState
      { HeadParameters
parameters :: HeadParameters
$sel:parameters:ClosedState :: HeadParameters
parameters
      , ConfirmedSnapshot SimpleTx
confirmedSnapshot :: ConfirmedSnapshot SimpleTx
$sel:confirmedSnapshot:ClosedState :: ConfirmedSnapshot SimpleTx
confirmedSnapshot
      , UTCTime
contestationDeadline :: UTCTime
$sel:contestationDeadline:ClosedState :: UTCTime
contestationDeadline
      , $sel:readyToFanoutSent:ClosedState :: Bool
readyToFanoutSent = Bool
False
      , $sel:chainState:ClosedState :: ChainStateType SimpleTx
chainState = SimpleChainState{$sel:slot:SimpleChainState :: ChainSlot
slot = Natural -> ChainSlot
ChainSlot Natural
0}
      , $sel:headId:ClosedState :: HeadId
headId = HeadId
testHeadId
      , $sel:headSeed:ClosedState :: HeadSeed
headSeed = HeadSeed
testHeadSeed
      , $sel:version:ClosedState :: SnapshotVersion
version = SnapshotVersion
0
      }
 where
  parameters :: HeadParameters
parameters = ContestationPeriod -> [Party] -> HeadParameters
HeadParameters ContestationPeriod
defaultContestationPeriod [Party]
parties

  contestationDeadline :: UTCTime
contestationDeadline = Gen UTCTime
forall a. Arbitrary a => Gen a
arbitrary Gen UTCTime -> Int -> UTCTime
forall a. Gen a -> Int -> a
`generateWith` Int
42

getConfirmedSnapshot :: HeadState tx -> Maybe (Snapshot tx)
getConfirmedSnapshot :: forall tx. HeadState tx -> Maybe (Snapshot tx)
getConfirmedSnapshot = \case
  Open OpenState{$sel:coordinatedHeadState:OpenState :: forall tx. OpenState tx -> CoordinatedHeadState tx
coordinatedHeadState = CoordinatedHeadState{ConfirmedSnapshot tx
$sel:confirmedSnapshot:CoordinatedHeadState :: forall tx. CoordinatedHeadState tx -> ConfirmedSnapshot tx
confirmedSnapshot :: ConfirmedSnapshot tx
confirmedSnapshot}} ->
    Snapshot tx -> Maybe (Snapshot tx)
forall a. a -> Maybe a
Just (ConfirmedSnapshot tx -> Snapshot tx
forall tx. ConfirmedSnapshot tx -> Snapshot tx
getSnapshot ConfirmedSnapshot tx
confirmedSnapshot)
  HeadState tx
_ ->
    Maybe (Snapshot tx)
forall a. Maybe a
Nothing

data StepState tx = StepState
  { forall tx. StepState tx -> HeadState tx
headState :: HeadState tx
  , forall tx. StepState tx -> Environment
env :: Environment
  , forall tx. StepState tx -> Ledger tx
ledger :: Ledger tx
  }

runHeadLogic ::
  Monad m =>
  Environment ->
  Ledger tx ->
  HeadState tx ->
  StateT (StepState tx) m a ->
  m a
runHeadLogic :: forall (m :: * -> *) tx a.
Monad m =>
Environment
-> Ledger tx -> HeadState tx -> StateT (StepState tx) m a -> m a
runHeadLogic Environment
env Ledger tx
ledger HeadState tx
headState = (StateT (StepState tx) m a -> StepState tx -> m a
forall (m :: * -> *) s a. Monad m => StateT s m a -> s -> m a
`evalStateT` StepState{Environment
$sel:env:StepState :: Environment
env :: Environment
env, Ledger tx
$sel:ledger:StepState :: Ledger tx
ledger :: Ledger tx
ledger, HeadState tx
$sel:headState:StepState :: HeadState tx
headState :: HeadState tx
headState})

-- | Retrieves the latest 'HeadState' from within 'runHeadLogic'.
getState :: MonadState (StepState tx) m => m (HeadState tx)
getState :: forall tx (m :: * -> *).
MonadState (StepState tx) m =>
m (HeadState tx)
getState = StepState tx -> HeadState tx
forall tx. StepState tx -> HeadState tx
headState (StepState tx -> HeadState tx)
-> m (StepState tx) -> m (HeadState tx)
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> m (StepState tx)
forall s (m :: * -> *). MonadState s m => m s
get

-- | Calls 'update' and 'aggregate' to drive the 'runHeadLogic' monad forward.
step ::
  (MonadState (StepState tx) m, IsChainState tx) =>
  Input tx ->
  m (Outcome tx)
step :: forall tx (m :: * -> *).
(MonadState (StepState tx) m, IsChainState tx) =>
Input tx -> m (Outcome tx)
step Input tx
input = do
  StepState{HeadState tx
$sel:headState:StepState :: forall tx. StepState tx -> HeadState tx
headState :: HeadState tx
headState, Environment
$sel:env:StepState :: forall tx. StepState tx -> Environment
env :: Environment
env, Ledger tx
$sel:ledger:StepState :: forall tx. StepState tx -> Ledger tx
ledger :: Ledger tx
ledger} <- m (StepState tx)
forall s (m :: * -> *). MonadState s m => m s
get
  let outcome :: Outcome tx
outcome = Environment -> Ledger tx -> HeadState tx -> Input tx -> Outcome tx
forall tx.
IsChainState tx =>
Environment -> Ledger tx -> HeadState tx -> Input tx -> Outcome tx
update Environment
env Ledger tx
ledger HeadState tx
headState Input tx
input
  let headState' :: HeadState tx
headState' = HeadState tx -> Outcome tx -> HeadState tx
forall tx.
IsChainState tx =>
HeadState tx -> Outcome tx -> HeadState tx
aggregateState HeadState tx
headState Outcome tx
outcome
  StepState tx -> m ()
forall s (m :: * -> *). MonadState s m => s -> m ()
put StepState{Environment
$sel:env:StepState :: Environment
env :: Environment
env, Ledger tx
$sel:ledger:StepState :: Ledger tx
ledger :: Ledger tx
ledger, $sel:headState:StepState :: HeadState tx
headState = HeadState tx
headState'}
  Outcome tx -> m (Outcome tx)
forall a. a -> m a
forall (f :: * -> *) a. Applicative f => a -> f a
pure Outcome tx
outcome

hasEffect :: (HasCallStack, IsChainState tx) => Outcome tx -> Effect tx -> IO ()
hasEffect :: forall tx.
(HasCallStack, IsChainState tx) =>
Outcome tx -> Effect tx -> IO ()
hasEffect Outcome tx
outcome Effect tx
effect = Outcome tx -> (Effect tx -> Bool) -> IO ()
forall tx.
(HasCallStack, IsChainState tx) =>
Outcome tx -> (Effect tx -> Bool) -> IO ()
hasEffectSatisfying Outcome tx
outcome (Effect tx -> Effect tx -> Bool
forall a. Eq a => a -> a -> Bool
== Effect tx
effect)

assertWait :: (HasCallStack, IsChainState tx) => Outcome tx -> WaitReason tx -> IO ()
assertWait :: forall tx.
(HasCallStack, IsChainState tx) =>
Outcome tx -> WaitReason tx -> IO ()
assertWait Outcome tx
outcome WaitReason tx
waitReason =
  case Outcome tx
outcome of
    Wait{WaitReason tx
reason :: WaitReason tx
$sel:reason:Continue :: forall tx. Outcome tx -> WaitReason tx
reason} -> WaitReason tx
reason WaitReason tx -> WaitReason tx -> IO ()
forall a. (HasCallStack, Show a, Eq a) => a -> a -> IO ()
`shouldBe` WaitReason tx
waitReason
    Outcome tx
_ -> String -> IO ()
forall (m :: * -> *) a.
(HasCallStack, MonadThrow m) =>
String -> m a
failure (String -> IO ()) -> String -> IO ()
forall a b. (a -> b) -> a -> b
$ String
"Expected a wait, but got: " String -> String -> String
forall a. Semigroup a => a -> a -> a
<> Outcome tx -> String
forall b a. (Show a, IsString b) => a -> b
show Outcome tx
outcome

hasEffectSatisfying :: (HasCallStack, IsChainState tx) => Outcome tx -> (Effect tx -> Bool) -> IO ()
hasEffectSatisfying :: forall tx.
(HasCallStack, IsChainState tx) =>
Outcome tx -> (Effect tx -> Bool) -> IO ()
hasEffectSatisfying Outcome tx
outcome Effect tx -> Bool
predicate =
  case Outcome tx
outcome of
    Wait{} -> String -> IO ()
forall (m :: * -> *) a.
(HasCallStack, MonadThrow m) =>
String -> m a
failure String
"Expected an effect, but got Wait outcome"
    Error{} -> String -> IO ()
forall (m :: * -> *) a.
(HasCallStack, MonadThrow m) =>
String -> m a
failure String
"Expected an effect, but got Error outcome"
    Continue{[Effect tx]
effects :: [Effect tx]
$sel:effects:Continue :: forall tx. Outcome tx -> [Effect tx]
effects} ->
      Bool -> IO () -> IO ()
forall (f :: * -> *). Applicative f => Bool -> f () -> f ()
unless ((Effect tx -> Bool) -> [Effect tx] -> Bool
forall (t :: * -> *) a. Foldable t => (a -> Bool) -> t a -> Bool
any Effect tx -> Bool
predicate [Effect tx]
effects) (IO () -> IO ()) -> IO () -> IO ()
forall a b. (a -> b) -> a -> b
$
        String -> IO ()
forall (m :: * -> *) a.
(HasCallStack, MonadThrow m) =>
String -> m a
failure (String -> IO ()) -> String -> IO ()
forall a b. (a -> b) -> a -> b
$
          String
"Expected an effect satisfying the predicate, but got: " String -> String -> String
forall a. Semigroup a => a -> a -> a
<> [Effect tx] -> String
forall b a. (Show a, IsString b) => a -> b
show [Effect tx]
effects

hasNoEffectSatisfying :: (HasCallStack, IsChainState tx) => Outcome tx -> (Effect tx -> Bool) -> IO ()
hasNoEffectSatisfying :: forall tx.
(HasCallStack, IsChainState tx) =>
Outcome tx -> (Effect tx -> Bool) -> IO ()
hasNoEffectSatisfying Outcome tx
outcome Effect tx -> Bool
predicate =
  case Outcome tx
outcome of
    Wait{} -> String -> IO ()
forall (m :: * -> *) a.
(HasCallStack, MonadThrow m) =>
String -> m a
failure String
"Expected an effect, but got Wait outcome"
    Error{} -> String -> IO ()
forall (m :: * -> *) a.
(HasCallStack, MonadThrow m) =>
String -> m a
failure String
"Expected an effect, but got Error outcome"
    Continue{[Effect tx]
$sel:effects:Continue :: forall tx. Outcome tx -> [Effect tx]
effects :: [Effect tx]
effects} ->
      Bool -> IO () -> IO ()
forall (f :: * -> *). Applicative f => Bool -> f () -> f ()
when ((Effect tx -> Bool) -> [Effect tx] -> Bool
forall (t :: * -> *) a. Foldable t => (a -> Bool) -> t a -> Bool
any Effect tx -> Bool
predicate [Effect tx]
effects) (IO () -> IO ()) -> IO () -> IO ()
forall a b. (a -> b) -> a -> b
$
        String -> IO ()
forall (m :: * -> *) a.
(HasCallStack, MonadThrow m) =>
String -> m a
failure (String -> IO ()) -> String -> IO ()
forall a b. (a -> b) -> a -> b
$
          String
"Expected no effect satisfying the predicate, but got: " String -> String -> String
forall a. Semigroup a => a -> a -> a
<> [Effect tx] -> String
forall b a. (Show a, IsString b) => a -> b
show [Effect tx]
effects

testSnapshot ::
  Monoid (UTxOType tx) =>
  SnapshotNumber ->
  SnapshotVersion ->
  [TxIdType tx] ->
  UTxOType tx ->
  Snapshot tx
testSnapshot :: forall tx.
Monoid (UTxOType tx) =>
SnapshotNumber
-> SnapshotVersion -> [TxIdType tx] -> UTxOType tx -> Snapshot tx
testSnapshot SnapshotNumber
number SnapshotVersion
version [TxIdType tx]
confirmed UTxOType tx
utxo =
  Snapshot
    { $sel:headId:Snapshot :: HeadId
headId = HeadId
testHeadId
    , SnapshotVersion
$sel:version:Snapshot :: SnapshotVersion
version :: SnapshotVersion
version
    , SnapshotNumber
$sel:number:Snapshot :: SnapshotNumber
number :: SnapshotNumber
number
    , [TxIdType tx]
$sel:confirmed:Snapshot :: [TxIdType tx]
confirmed :: [TxIdType tx]
confirmed
    , UTxOType tx
$sel:utxo:Snapshot :: UTxOType tx
utxo :: UTxOType tx
utxo
    , $sel:utxoToDecommit:Snapshot :: Maybe (UTxOType tx)
utxoToDecommit = Maybe (UTxOType tx)
forall a. Monoid a => a
mempty
    }