{-# LANGUAGE DuplicateRecordFields #-}
{-# LANGUAGE RankNTypes #-}
{-# LANGUAGE ScopedTypeVariables #-}

-- | Model-Based testing of Hydra Head protocol implementation.
--
-- * Troubleshooting
--
-- ** Deadlocks
--
-- One of the most annoying problems one can face with those very high level properties involving multithreading and a lot
-- of complex moving parts is when the test execution deadlocks. Here is a short guide on what one can do to troubleshoort
-- this kind of issue:
--
-- * **Check generators**: `suchThat` combinator from QuickCheck is useful when one wants to refine another `Gen`erator's behaviour
--   but it can lead to deadlock if the filtering leads to no value being generated. Avoid it.
--
-- * **Dump nodes' logs**: In case of a "normal" failure of the tests, the logs from the nodes are dumped. However, if the test does
--   not even complete then no logs are produced because they are kept in memory. In this case. replacing `traceInIOSim` with
--   `traceInIOSim <> traceDebug` will ensure the logs are dumped on the `stderr`. It could be a good idea to store them in a file
--   as they can be quite large.
--
-- * **Use** `Debug.Trace.trace` liberally: Because getting a proper stack trace is hard in Haskell, esp. in pure code, sprinkling
--   `trace` statements at key points might help understand what's going on and zoom in on the culprits
--
-- * **Dump IOSim trace**: In case the deadlock (or race condition) is caused by having two or more concurrent threads competing
--   to access a resource, dumping the trace of IOSim's runtime scheduleer execution can help. io-sim generate its trace lazily which
--   means that even when it deadlocks, one can capture at least a significant prefix of the trace and dump it to `stderr`. One can
--   `map (\ t -> trace (ppEvents t) t) . traceEvents` over the `SimTrace` returned by `runSimTrace` to get some pretty-printed
--   output similar to:
--
--   @@
--   Time 380.1s - ThreadId [4]  node-94455e3e - EventThrow AsyncCancelled
--   Time 380.1s - ThreadId [4]  node-94455e3e - EventMask MaskedInterruptible
--   Time 380.1s - ThreadId [4]  node-94455e3e - EventMask MaskedInterruptible
--   Time 380.1s - ThreadId [4]  node-94455e3e - EventDeschedule Interruptible
--   Time 380.1s - ThreadId [4]  node-94455e3e - EventTxCommitted [Labelled (TVarId 25) (Just "async-ThreadId [4]")] [] Nothing
--   Time 380.1s - ThreadId []   main          - EventTxWakeup [Labelled (TVarId 25) (Just "async-ThreadId [4]")]
--   Time 380.1s - ThreadId [4]  node-94455e3e - EventUnblocked [ThreadId []]
--   Time 380.1s - ThreadId [4]  node-94455e3e - EventDeschedule Yield
--   Time 380.1s - ThreadId []   main          - EventTxCommitted [] [] Nothing
--   Time 380.1s - ThreadId []   main          - EventUnblocked []
--   Time 380.1s - ThreadId []   main          - EventDeschedule Yield
--   Time 380.1s - ThreadId [4]  node-94455e3e - EventThreadFinished
--   Time 380.1s - ThreadId [4]  node-94455e3e - EventDeschedule Terminated
--   Time 380.1s - ThreadId []   main          - EventThreadFinished
--   @@
--
-- ** Recording trace failures
--
-- When a property fails it will dump the sequence of actions leading to the
-- failure:
--
-- @@
--   do action $ Seed {seedKeys = [("8bbc9f32e4faff669ed1561025f243649f1332902aa79ad7e6e6bbae663f332d",CardanoSigningKey {signingKey = "0400020803030302070808060405040001050408070401040604000005010603"})], seedContestationPeriod = 46s, seedDepositDeadline = 50s, toCommit = fromList [(Party {vkey = "b4ea494b4bda6281899727bf4cfef5cdeba8fb3fec4edebc408aa72dfd6ad4f0"},[(CardanoSigningKey {signingKey = "0400020803030302070808060405040001050408070401040604000005010603"},valueFromList [(AdaAssetId,54862683)])])]}
--      var2 <- action $ Init (Party {vkey = "b4ea494b4bda6281899727bf4cfef5cdeba8fb3fec4edebc408aa72dfd6ad4f0"})
--      action $ Commit {headIdVar = var2, party = Party {vkey = "b4ea494b4bda6281899727bf4cfef5cdeba8fb3fec4edebc408aa72dfd6ad4f0"}, utxoToCommit = [(CardanoSigningKey {signingKey = "0400020803030302070808060405040001050408070401040604000005010603"},valueFromList [(AdaAssetId,54862683)])]}
--      action $ Decommit {party = Party {vkey = "b4ea494b4bda6281899727bf4cfef5cdeba8fb3fec4edebc408aa72dfd6ad4f0"}, decommitTx = Payment { from = CardanoSigningKey {signingKey = "0400020803030302070808060405040001050408070401040604000005010603"}, to = CardanoSigningKey {signingKey = "0702050602000101050108060302010707060007020308080801060700030306"}, value = valueFromList [(AdaAssetId,54862683)] }}
--      action $ Deposit {headIdVar = var2, utxoToDeposit = [(CardanoSigningKey {signingKey = "0400020803030302070808060405040001050408070401040604000005010603"},valueFromList [(AdaAssetId,54862683)])], deadline = 1864-06-06 08:24:08.669152896211 UTC}
--      pure ()
-- @@
--
-- Which can be turned into a unit test after resolving most of the imports.
-- Common pitfalls are incorrect show instances (e.g. the UTCTime in deadline
-- above). Should the variables not be bound correctly, double check
-- HasVariables instances. A working example of the above output would be:
--
-- @@
--   it "troubleshoot" . withMaxSuccess 1 . flip forAllDL propHydraModel $ do
--     action $ Seed{seedKeys = [("8bbc9f32e4faff669ed1561025f243649f1332902aa79ad7e6e6bbae663f332d", CardanoSigningKey{signingKey = "0400020803030302070808060405040001050408070401040604000005010603"})], seedContestationPeriod = UnsafeContestationPeriod 46, seedDepositDeadline = UnsafeDepositDeadline 50, toCommit = fromList [(Party{vkey = "b4ea494b4bda6281899727bf4cfef5cdeba8fb3fec4edebc408aa72dfd6ad4f0"}, [(CardanoSigningKey{signingKey = "0400020803030302070808060405040001050408070401040604000005010603"}, valueFromList [(AdaAssetId, 54862683)])])]}
--     var2 <- action $ Init (Party{vkey = "b4ea494b4bda6281899727bf4cfef5cdeba8fb3fec4edebc408aa72dfd6ad4f0"})
--     action $ Commit{headIdVar = var2, party = Party{vkey = "b4ea494b4bda6281899727bf4cfef5cdeba8fb3fec4edebc408aa72dfd6ad4f0"}, utxoToCommit = [(CardanoSigningKey{signingKey = "0400020803030302070808060405040001050408070401040604000005010603"}, valueFromList [(AdaAssetId, 54862683)])]}
--     action $ Decommit{party = Party{vkey = "b4ea494b4bda6281899727bf4cfef5cdeba8fb3fec4edebc408aa72dfd6ad4f0"}, decommitTx = Payment{from = CardanoSigningKey{signingKey = "0400020803030302070808060405040001050408070401040604000005010603"}, to = CardanoSigningKey{signingKey = "0702050602000101050108060302010707060007020308080801060700030306"}, value = valueFromList [(AdaAssetId, 54862683)]}}
--     action $ Deposit{headIdVar = var2, utxoToDeposit = [(CardanoSigningKey{signingKey = "0400020803030302070808060405040001050408070401040604000005010603"}, valueFromList [(AdaAssetId, 54862683)])], deadline = read "1864-06-06 08:24:08.669152896211 UTC"}
--     pure ()
-- @@
module Hydra.ModelSpec where

import Hydra.Cardano.Api
import Hydra.Prelude
import Test.Hydra.Prelude hiding (after)

import Control.Concurrent.Class.MonadSTM (newTVarIO)
import Control.Monad.Class.MonadTimer ()
import Control.Monad.IOSim (Failure (FailureException), IOSim, runSimTrace, traceResult)
import Data.Map ((!))
import Data.Map qualified as Map
import Data.Set qualified as Set
import Data.Typeable (cast)
import Hydra.BehaviorSpec (TestHydraClient (..), dummySimulatedChainNetwork)
import Hydra.Logging.Messages (HydraLog)
import Hydra.Model (
  Action (..),
  GlobalState (..),
  Nodes (Nodes, nodes),
  OffChainState (..),
  RunMonad,
  RunState (..),
  WorldState (..),
  genInit,
  genPayment,
  genSeed,
  headUTxO,
  runMonad,
  toRealUTxO,
  toTxOuts,
 )
import Hydra.Model qualified as Model
import Hydra.Model.Payment (Payment (..))
import Hydra.Model.Payment qualified as Payment
import Hydra.Tx.Party (Party (..), deriveParty)
import System.IO.Temp (writeSystemTempFile)
import System.IO.Unsafe (unsafePerformIO)
import Test.HUnit.Lang (formatFailureReason)
import Test.QuickCheck (Property, Testable, counterexample, forAllShrink, property, withMaxSuccess, within)
import Test.QuickCheck.DynamicLogic (
  DL,
  Quantification,
  action,
  anyActions_,
  forAllDL,
  forAllNonVariableQ,
  forAllQ,
  getModelStateDL,
  whereQ,
  withGenQ,
 )
import Test.QuickCheck.Gen.Unsafe (Capture (Capture), capture)
import Test.QuickCheck.Monadic (PropertyM, assert, monadic', run, stop)
import Test.QuickCheck.Property ((===))
import Test.QuickCheck.StateModel (
  ActionWithPolarity (..),
  Actions,
  Annotated (..),
  Step ((:=)),
  precondition,
  runActions,
  pattern Actions,
 )
import Test.Util (printTrace, traceInIOSim)

spec :: Spec
spec :: Spec
spec = do
  String -> Spec -> Spec
forall a. HasCallStack => String -> SpecWith a -> SpecWith a
context String
"modeling" (Spec -> Spec) -> Spec -> Spec
forall a b. (a -> b) -> a -> b
$ do
    String -> Property -> Spec
forall prop.
(HasCallStack, Testable prop) =>
String -> prop -> Spec
prop String
"not generate actions with 0 Ada" (Property -> Spec) -> Property -> Spec
forall a b. (a -> b) -> a -> b
$ Int -> (Actions WorldState -> Property) -> Property
forall prop. Testable prop => Int -> prop -> Property
withMaxSuccess Int
10000 Actions WorldState -> Property
propDoesNotGenerate0AdaUTxO
    String
-> ([(CardanoSigningKey, Value)]
    -> [(CardanoSigningKey, Value)] -> Property)
-> Spec
forall prop.
(HasCallStack, Testable prop) =>
String -> prop -> Spec
prop String
"toRealUTxO is distributive" (([(CardanoSigningKey, Value)]
  -> [(CardanoSigningKey, Value)] -> Property)
 -> Spec)
-> ([(CardanoSigningKey, Value)]
    -> [(CardanoSigningKey, Value)] -> Property)
-> Spec
forall a b. (a -> b) -> a -> b
$ ([(CardanoSigningKey, Value)] -> UTxO' (TxOut CtxUTxO Era))
-> [(CardanoSigningKey, Value)]
-> [(CardanoSigningKey, Value)]
-> Property
forall b a.
(Show b, Eq b, Semigroup a, Semigroup b) =>
(a -> b) -> a -> a -> Property
propIsDistributive [(CardanoSigningKey, Value)] -> UTxO' (TxOut CtxUTxO Era)
UTxOType Payment -> UTxOType Tx
toRealUTxO
    String
-> ([(CardanoSigningKey, Value)]
    -> [(CardanoSigningKey, Value)] -> Property)
-> Spec
forall prop.
(HasCallStack, Testable prop) =>
String -> prop -> Spec
prop String
"toTxOuts is distributive" (([(CardanoSigningKey, Value)]
  -> [(CardanoSigningKey, Value)] -> Property)
 -> Spec)
-> ([(CardanoSigningKey, Value)]
    -> [(CardanoSigningKey, Value)] -> Property)
-> Spec
forall a b. (a -> b) -> a -> b
$ ([(CardanoSigningKey, Value)] -> [TxOut CtxUTxO Era])
-> [(CardanoSigningKey, Value)]
-> [(CardanoSigningKey, Value)]
-> Property
forall b a.
(Show b, Eq b, Semigroup a, Semigroup b) =>
(a -> b) -> a -> a -> Property
propIsDistributive [(CardanoSigningKey, Value)] -> [TxOut CtxUTxO Era]
toTxOuts
  String -> (Actions WorldState -> Property) -> Spec
forall prop.
(HasCallStack, Testable prop) =>
String -> prop -> Spec
prop String
"check model" Actions WorldState -> Property
propHydraModel
  String -> Property -> Spec
forall prop.
(HasCallStack, Testable prop) =>
String -> prop -> Spec
prop String
"check model balances" Property
propCheckModelBalances
  String -> Spec -> Spec
forall a. HasCallStack => String -> SpecWith a -> SpecWith a
context String
"logic" (Spec -> Spec) -> Spec -> Spec
forall a b. (a -> b) -> a -> b
$ do
    String -> Property -> Spec
forall prop.
(HasCallStack, Testable prop) =>
String -> prop -> Spec
prop String
"check conflict-free liveness" (Property -> Spec) -> Property -> Spec
forall a b. (a -> b) -> a -> b
$ DL WorldState () -> Property
propDL DL WorldState ()
conflictFreeLiveness
    String -> Property -> Spec
forall prop.
(HasCallStack, Testable prop) =>
String -> prop -> Spec
prop String
"check head opens if all participants commit" (Property -> Spec) -> Property -> Spec
forall a b. (a -> b) -> a -> b
$ DL WorldState () -> Property
propDL DL WorldState ()
headOpensIfAllPartiesCommit
    String -> Property -> Spec
forall prop.
(HasCallStack, Testable prop) =>
String -> prop -> Spec
prop String
"fanout contains whole confirmed UTxO" (Property -> Spec) -> Property -> Spec
forall a b. (a -> b) -> a -> b
$ DL WorldState () -> Property
propDL DL WorldState ()
fanoutContainsWholeConfirmedUTxO
    String -> Property -> Spec
forall prop.
(HasCallStack, Testable prop) =>
String -> prop -> Spec
prop String
"parties contest to wrong closed snapshot" (Property -> Spec) -> Property -> Spec
forall a b. (a -> b) -> a -> b
$ DL WorldState () -> Property
propDL DL WorldState ()
partyContestsToWrongClosedSnapshot

propDL :: DL WorldState () -> Property
propDL :: DL WorldState () -> Property
propDL DL WorldState ()
d = DL WorldState () -> (Actions WorldState -> Property) -> Property
forall s a.
(DynLogicModel s, Testable a) =>
DL s () -> (Actions s -> a) -> Property
forAllDL DL WorldState ()
d Actions WorldState -> Property
propHydraModel

propHydraModel :: Actions WorldState -> Property
propHydraModel :: Actions WorldState -> Property
propHydraModel Actions WorldState
actions =
  (forall s. PropertyM (RunMonad (IOSim s)) ()) -> Property
forall a.
Testable a =>
(forall s. PropertyM (RunMonad (IOSim s)) a) -> Property
runIOSimProp ((forall s. PropertyM (RunMonad (IOSim s)) ()) -> Property)
-> (forall s. PropertyM (RunMonad (IOSim s)) ()) -> Property
forall a b. (a -> b) -> a -> b
$ do
    (Annotated WorldState, Env (RunMonad (IOSim s)))
_ <- Actions WorldState
-> PropertyM
     (RunMonad (IOSim s))
     (Annotated WorldState, Env (RunMonad (IOSim s)))
forall state (m :: * -> *) e.
(StateModel state, RunModel state m, e ~ Error state,
 forall a. IsPerformResult e a) =>
Actions state -> PropertyM m (Annotated state, Env m)
runActions Actions WorldState
actions
    Bool -> PropertyM (RunMonad (IOSim s)) ()
forall (m :: * -> *). Monad m => Bool -> PropertyM m ()
assert Bool
True

-- XXX: This is very similar to propHydraModel, where the assertion is
-- basically a post condition!?
propCheckModelBalances :: Property
propCheckModelBalances :: Property
propCheckModelBalances =
  Int -> Property -> Property
forall prop. Testable prop => Int -> prop -> Property
within Int
30000000 (Property -> Property) -> Property -> Property
forall a b. (a -> b) -> a -> b
$
    Gen (Actions WorldState)
-> (Actions WorldState -> [Actions WorldState])
-> (Actions WorldState -> Property)
-> Property
forall a prop.
(Show a, Testable prop) =>
Gen a -> (a -> [a]) -> (a -> prop) -> Property
forAllShrink Gen (Actions WorldState)
forall a. Arbitrary a => Gen a
arbitrary Actions WorldState -> [Actions WorldState]
forall a. Arbitrary a => a -> [a]
shrink ((Actions WorldState -> Property) -> Property)
-> (Actions WorldState -> Property) -> Property
forall a b. (a -> b) -> a -> b
$ \Actions WorldState
actions ->
      (forall s. PropertyM (RunMonad (IOSim s)) ()) -> Property
forall a.
Testable a =>
(forall s. PropertyM (RunMonad (IOSim s)) a) -> Property
runIOSimProp ((forall s. PropertyM (RunMonad (IOSim s)) ()) -> Property)
-> (forall s. PropertyM (RunMonad (IOSim s)) ()) -> Property
forall a b. (a -> b) -> a -> b
$ do
        (Annotated WorldState
metadata, Env (RunMonad (IOSim s))
_symEnv) <- Actions WorldState
-> PropertyM
     (RunMonad (IOSim s))
     (Annotated WorldState, Env (RunMonad (IOSim s)))
forall state (m :: * -> *) e.
(StateModel state, RunModel state m, e ~ Error state,
 forall a. IsPerformResult e a) =>
Actions state -> PropertyM m (Annotated state, Env m)
runActions Actions WorldState
actions
        let WorldState{[(SigningKey HydraKey, CardanoSigningKey)]
hydraParties :: [(SigningKey HydraKey, CardanoSigningKey)]
$sel:hydraParties:WorldState :: WorldState -> [(SigningKey HydraKey, CardanoSigningKey)]
hydraParties, GlobalState
hydraState :: GlobalState
$sel:hydraState:WorldState :: WorldState -> GlobalState
hydraState} = Annotated WorldState -> WorldState
forall state. Annotated state -> state
underlyingState Annotated WorldState
metadata
        -- XXX: This wait time is arbitrary and corresponds to 3 "blocks" from
        -- the underlying simulated chain which produces a block every 20s. It
        -- should be enough to ensure all nodes' threads terminate their actions
        -- and those gets picked up by the chain
        RunMonad (IOSim s) () -> PropertyM (RunMonad (IOSim s)) ()
forall (m :: * -> *) a. Monad m => m a -> PropertyM m a
run (RunMonad (IOSim s) () -> PropertyM (RunMonad (IOSim s)) ())
-> RunMonad (IOSim s) () -> PropertyM (RunMonad (IOSim s)) ()
forall a b. (a -> b) -> a -> b
$ IOSim s () -> RunMonad (IOSim s) ()
forall (m :: * -> *) a. Monad m => m a -> RunMonad m a
forall (t :: (* -> *) -> * -> *) (m :: * -> *) a.
(MonadTrans t, Monad m) =>
m a -> t m a
lift IOSim s ()
forall (m :: * -> *). MonadDelay m => m ()
waitForAMinute
        let parties :: Set Party
parties = [Party] -> Set Party
forall a. Ord a => [a] -> Set a
Set.fromList ([Party] -> Set Party) -> [Party] -> Set Party
forall a b. (a -> b) -> a -> b
$ SigningKey HydraKey -> Party
deriveParty (SigningKey HydraKey -> Party)
-> ((SigningKey HydraKey, CardanoSigningKey)
    -> SigningKey HydraKey)
-> (SigningKey HydraKey, CardanoSigningKey)
-> Party
forall b c a. (b -> c) -> (a -> b) -> a -> c
. (SigningKey HydraKey, CardanoSigningKey) -> SigningKey HydraKey
forall a b. (a, b) -> a
fst ((SigningKey HydraKey, CardanoSigningKey) -> Party)
-> [(SigningKey HydraKey, CardanoSigningKey)] -> [Party]
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> [(SigningKey HydraKey, CardanoSigningKey)]
hydraParties
        Map Party (TestHydraClient Tx (IOSim s))
nodes <- RunMonad (IOSim s) (Map Party (TestHydraClient Tx (IOSim s)))
-> PropertyM
     (RunMonad (IOSim s)) (Map Party (TestHydraClient Tx (IOSim s)))
forall (m :: * -> *) a. Monad m => m a -> PropertyM m a
run (RunMonad (IOSim s) (Map Party (TestHydraClient Tx (IOSim s)))
 -> PropertyM
      (RunMonad (IOSim s)) (Map Party (TestHydraClient Tx (IOSim s))))
-> RunMonad (IOSim s) (Map Party (TestHydraClient Tx (IOSim s)))
-> PropertyM
     (RunMonad (IOSim s)) (Map Party (TestHydraClient Tx (IOSim s)))
forall a b. (a -> b) -> a -> b
$ (Nodes (IOSim s) -> Map Party (TestHydraClient Tx (IOSim s)))
-> RunMonad (IOSim s) (Map Party (TestHydraClient Tx (IOSim s)))
forall s (m :: * -> *) a. MonadState s m => (s -> a) -> m a
gets Nodes (IOSim s) -> Map Party (TestHydraClient Tx (IOSim s))
forall (m :: * -> *). Nodes m -> Map Party (TestHydraClient Tx m)
nodes
        Bool -> PropertyM (RunMonad (IOSim s)) ()
forall (m :: * -> *). Monad m => Bool -> PropertyM m ()
assert (Set Party
parties Set Party -> Set Party -> Bool
forall a. Eq a => a -> a -> Bool
== Map Party (TestHydraClient Tx (IOSim s)) -> Set Party
forall k a. Map k a -> Set k
Map.keysSet Map Party (TestHydraClient Tx (IOSim s))
nodes)
        Set Party
-> (Party -> PropertyM (RunMonad (IOSim s)) ())
-> PropertyM (RunMonad (IOSim s)) ()
forall (t :: * -> *) (m :: * -> *) a b.
(Foldable t, Monad m) =>
t a -> (a -> m b) -> m ()
forM_ Set Party
parties ((Party -> PropertyM (RunMonad (IOSim s)) ())
 -> PropertyM (RunMonad (IOSim s)) ())
-> (Party -> PropertyM (RunMonad (IOSim s)) ())
-> PropertyM (RunMonad (IOSim s)) ()
forall a b. (a -> b) -> a -> b
$ \Party
p -> do
          RunMonad (IOSim s) () -> PropertyM (RunMonad (IOSim s)) ()
forall (m :: * -> *) a. Monad m => m a -> PropertyM m a
run (RunMonad (IOSim s) () -> PropertyM (RunMonad (IOSim s)) ())
-> RunMonad (IOSim s) () -> PropertyM (RunMonad (IOSim s)) ()
forall a b. (a -> b) -> a -> b
$ IOSim s () -> RunMonad (IOSim s) ()
forall (m :: * -> *) a. Monad m => m a -> RunMonad m a
forall (t :: (* -> *) -> * -> *) (m :: * -> *) a.
(MonadTrans t, Monad m) =>
m a -> t m a
lift (IOSim s () -> RunMonad (IOSim s) ())
-> IOSim s () -> RunMonad (IOSim s) ()
forall a b. (a -> b) -> a -> b
$ DiffTime -> IOSim s ()
forall (m :: * -> *). MonadDelay m => DiffTime -> m ()
threadDelay DiffTime
1
          GlobalState
-> Map Party (TestHydraClient Tx (IOSim s))
-> Party
-> PropertyM (RunMonad (IOSim s)) ()
forall s.
GlobalState
-> Map Party (TestHydraClient Tx (IOSim s))
-> Party
-> PropertyM (RunMonad (IOSim s)) ()
assertBalancesInOpenHeadAreConsistent GlobalState
hydraState Map Party (TestHydraClient Tx (IOSim s))
nodes Party
p
 where
  waitForAMinute :: MonadDelay m => m ()
  waitForAMinute :: forall (m :: * -> *). MonadDelay m => m ()
waitForAMinute = DiffTime -> m ()
forall (m :: * -> *). MonadDelay m => DiffTime -> m ()
threadDelay DiffTime
60

assertBalancesInOpenHeadAreConsistent ::
  GlobalState ->
  Map Party (TestHydraClient Tx (IOSim s)) ->
  Party ->
  PropertyM (RunMonad (IOSim s)) ()
assertBalancesInOpenHeadAreConsistent :: forall s.
GlobalState
-> Map Party (TestHydraClient Tx (IOSim s))
-> Party
-> PropertyM (RunMonad (IOSim s)) ()
assertBalancesInOpenHeadAreConsistent GlobalState
world Map Party (TestHydraClient Tx (IOSim s))
nodes Party
p = do
  Bool -> PropertyM (RunMonad (IOSim s)) ()
forall (m :: * -> *). Monad m => Bool -> PropertyM m ()
assert (Key (Map Party (TestHydraClient Tx (IOSim s)))
Party
p Key (Map Party (TestHydraClient Tx (IOSim s)))
-> Map Party (TestHydraClient Tx (IOSim s)) -> Bool
forall t. StaticMap t => Key t -> t -> Bool
`member` Map Party (TestHydraClient Tx (IOSim s))
nodes)
  let node :: TestHydraClient Tx (IOSim s)
node = Map Party (TestHydraClient Tx (IOSim s))
nodes Map Party (TestHydraClient Tx (IOSim s))
-> Party -> TestHydraClient Tx (IOSim s)
forall k a. Ord k => Map k a -> k -> a
! Party
p
  case GlobalState
world of
    Open{$sel:offChainState:Start :: GlobalState -> OffChainState
offChainState = OffChainState{UTxOType Payment
confirmedUTxO :: UTxOType Payment
$sel:confirmedUTxO:OffChainState :: OffChainState -> UTxOType Payment
confirmedUTxO}} -> do
      UTxO' (TxOut CtxUTxO Era)
utxo <- RunMonad (IOSim s) (UTxO' (TxOut CtxUTxO Era))
-> PropertyM (RunMonad (IOSim s)) (UTxO' (TxOut CtxUTxO Era))
forall (m :: * -> *) a. Monad m => m a -> PropertyM m a
run (RunMonad (IOSim s) (UTxO' (TxOut CtxUTxO Era))
 -> PropertyM (RunMonad (IOSim s)) (UTxO' (TxOut CtxUTxO Era)))
-> RunMonad (IOSim s) (UTxO' (TxOut CtxUTxO Era))
-> PropertyM (RunMonad (IOSim s)) (UTxO' (TxOut CtxUTxO Era))
forall a b. (a -> b) -> a -> b
$ IOSim s (UTxO' (TxOut CtxUTxO Era))
-> RunMonad (IOSim s) (UTxO' (TxOut CtxUTxO Era))
forall (m :: * -> *) a. Monad m => m a -> RunMonad m a
forall (t :: (* -> *) -> * -> *) (m :: * -> *) a.
(MonadTrans t, Monad m) =>
m a -> t m a
lift (IOSim s (UTxO' (TxOut CtxUTxO Era))
 -> RunMonad (IOSim s) (UTxO' (TxOut CtxUTxO Era)))
-> IOSim s (UTxO' (TxOut CtxUTxO Era))
-> RunMonad (IOSim s) (UTxO' (TxOut CtxUTxO Era))
forall a b. (a -> b) -> a -> b
$ TestHydraClient Tx (IOSim s) -> IOSim s (UTxOType Tx)
forall tx (m :: * -> *).
(IsTx tx, MonadDelay m) =>
TestHydraClient tx m -> m (UTxOType tx)
headUTxO TestHydraClient Tx (IOSim s)
node
      let sorted :: [TxOut ctx] -> [TxOut ctx]
sorted = (TxOut ctx -> (AddressInEra, Lovelace))
-> [TxOut ctx] -> [TxOut ctx]
forall b a. Ord b => (a -> b) -> [a] -> [a]
sortOn (\TxOut ctx
o -> (TxOut ctx -> AddressInEra
forall ctx. TxOut ctx -> AddressInEra
txOutAddress TxOut ctx
o, Value -> Lovelace
selectLovelace (TxOut ctx -> Value
forall ctx. TxOut ctx -> Value
txOutValue TxOut ctx
o)))
      let expected :: [TxOut CtxUTxO Era]
expected = [TxOut CtxUTxO Era] -> [TxOut CtxUTxO Era]
forall {ctx}. [TxOut ctx] -> [TxOut ctx]
sorted ([(CardanoSigningKey, Value)] -> [TxOut CtxUTxO Era]
toTxOuts [(CardanoSigningKey, Value)]
UTxOType Payment
confirmedUTxO)
      let actual :: [TxOut CtxUTxO Era]
actual = [TxOut CtxUTxO Era] -> [TxOut CtxUTxO Era]
forall {ctx}. [TxOut ctx] -> [TxOut ctx]
sorted (UTxO' (TxOut CtxUTxO Era) -> [TxOut CtxUTxO Era]
forall a. UTxO' a -> [a]
forall (t :: * -> *) a. Foldable t => t a -> [a]
toList UTxO' (TxOut CtxUTxO Era)
utxo)
      Property -> PropertyM (RunMonad (IOSim s)) ()
forall prop (m :: * -> *) a.
(Testable prop, Monad m) =>
prop -> PropertyM m a
stop (Property -> PropertyM (RunMonad (IOSim s)) ())
-> Property -> PropertyM (RunMonad (IOSim s)) ()
forall a b. (a -> b) -> a -> b
$
        [TxOut CtxUTxO Era]
expected [TxOut CtxUTxO Era] -> [TxOut CtxUTxO Era] -> Property
forall a. (Eq a, Show a) => a -> a -> Property
=== [TxOut CtxUTxO Era]
actual
          Property -> (Property -> Property) -> Property
forall a b. a -> (a -> b) -> b
& String -> Property -> Property
forall prop. Testable prop => String -> prop -> Property
counterexample (String
"actual: \n  " String -> String -> String
forall a. Semigroup a => a -> a -> a
<> String -> [String] -> String
forall a. [a] -> [[a]] -> [a]
intercalate String
"\n  " ((TxOut CtxUTxO Era -> String) -> [TxOut CtxUTxO Era] -> [String]
forall a b. (a -> b) -> [a] -> [b]
map TxOut CtxUTxO Era -> String
forall {ctx}. TxOut ctx -> String
renderTxOut [TxOut CtxUTxO Era]
actual))
          Property -> (Property -> Property) -> Property
forall a b. a -> (a -> b) -> b
& String -> Property -> Property
forall prop. Testable prop => String -> prop -> Property
counterexample (String
"expected: \n  " String -> String -> String
forall a. Semigroup a => a -> a -> a
<> String -> [String] -> String
forall a. [a] -> [[a]] -> [a]
intercalate String
"\n  " ((TxOut CtxUTxO Era -> String) -> [TxOut CtxUTxO Era] -> [String]
forall a b. (a -> b) -> [a] -> [b]
map TxOut CtxUTxO Era -> String
forall {ctx}. TxOut ctx -> String
renderTxOut [TxOut CtxUTxO Era]
expected))
          Property -> (Property -> Property) -> Property
forall a b. a -> (a -> b) -> b
& String -> Property -> Property
forall prop. Testable prop => String -> prop -> Property
counterexample (String
"Incorrect balance for party " String -> String -> String
forall a. Semigroup a => a -> a -> a
<> Party -> String
forall b a. (Show a, IsString b) => a -> b
show Party
p)
    GlobalState
_ -> do
      () -> PropertyM (RunMonad (IOSim s)) ()
forall a. a -> PropertyM (RunMonad (IOSim s)) a
forall (f :: * -> *) a. Applicative f => a -> f a
pure ()
 where
  renderTxOut :: TxOut ctx -> String
renderTxOut TxOut ctx
o =
    Text -> String
forall a. ToString a => a -> String
toString (Text -> String) -> Text -> String
forall a b. (a -> b) -> a -> b
$
      AddressInEra -> Text
forall addr. SerialiseAddress addr => addr -> Text
serialiseAddress (TxOut ctx -> AddressInEra
forall ctx. TxOut ctx -> AddressInEra
txOutAddress TxOut ctx
o) Text -> Text -> Text
forall a. Semigroup a => a -> a -> a
<> Text
": " Text -> Text -> Text
forall a. Semigroup a => a -> a -> a
<> Value -> Text
renderValue (TxOut ctx -> Value
forall ctx. TxOut ctx -> Value
txOutValue TxOut ctx
o)

propIsDistributive :: (Show b, Eq b, Semigroup a, Semigroup b) => (a -> b) -> a -> a -> Property
propIsDistributive :: forall b a.
(Show b, Eq b, Semigroup a, Semigroup b) =>
(a -> b) -> a -> a -> Property
propIsDistributive a -> b
f a
x a
y =
  a -> b
f a
x b -> b -> b
forall a. Semigroup a => a -> a -> a
<> a -> b
f a
y b -> b -> Property
forall a. (Eq a, Show a) => a -> a -> Property
=== a -> b
f (a
x a -> a -> a
forall a. Semigroup a => a -> a -> a
<> a
y)
    Property -> (Property -> Property) -> Property
forall a b. a -> (a -> b) -> b
& String -> Property -> Property
forall prop. Testable prop => String -> prop -> Property
counterexample (String
"f (x <> y)   " String -> String -> String
forall a. Semigroup a => a -> a -> a
<> b -> String
forall b a. (Show a, IsString b) => a -> b
show (a -> b
f (a
x a -> a -> a
forall a. Semigroup a => a -> a -> a
<> a
y)))
    Property -> (Property -> Property) -> Property
forall a b. a -> (a -> b) -> b
& String -> Property -> Property
forall prop. Testable prop => String -> prop -> Property
counterexample (String
"f x <> f y: " String -> String -> String
forall a. Semigroup a => a -> a -> a
<> b -> String
forall b a. (Show a, IsString b) => a -> b
show (a -> b
f a
x b -> b -> b
forall a. Semigroup a => a -> a -> a
<> a -> b
f a
y))

-- | Expect to see contestations when trying to close with
-- an old snapshot
partyContestsToWrongClosedSnapshot :: DL WorldState ()
partyContestsToWrongClosedSnapshot :: DL WorldState ()
partyContestsToWrongClosedSnapshot = do
  DL WorldState ()
headOpensIfAllPartiesCommit
  DL WorldState WorldState
forall s. DL s s
getModelStateDL DL WorldState WorldState
-> (WorldState -> DL WorldState ()) -> DL WorldState ()
forall a b.
DL WorldState a -> (a -> DL WorldState b) -> DL WorldState b
forall (m :: * -> *) a b. Monad m => m a -> (a -> m b) -> m b
>>= \case
    st :: WorldState
st@WorldState{$sel:hydraState:WorldState :: WorldState -> GlobalState
hydraState = Open{}} -> do
      (Party
party, Payment
payment) <- Quantification (Party, Payment) -> DL WorldState (Party, Payment)
forall a s.
QuantifyConstraints (HasNoVariables a) =>
Quantification a -> DL s a
forAllNonVariableQ (WorldState -> Quantification (Party, Payment)
nonConflictingTx WorldState
st)
      Var Payment
tx <- Action WorldState Payment -> DL WorldState (Var Payment)
forall a s.
(Typeable a, Eq (Action s a), Show (Action s a)) =>
Action s a -> DL s (Var a)
action (Action WorldState Payment -> DL WorldState (Var Payment))
-> Action WorldState Payment -> DL WorldState (Var Payment)
forall a b. (a -> b) -> a -> b
$ Party -> Payment -> Action WorldState Payment
Model.NewTx Party
party Payment
payment
      Action WorldState () -> DL WorldState ()
eventually (Var Payment -> Action WorldState ()
ObserveConfirmedTx Var Payment
tx)
      Action WorldState () -> DL WorldState ()
forall a. Typeable a => Action WorldState a -> DL WorldState ()
action_ (Action WorldState () -> DL WorldState ())
-> Action WorldState () -> DL WorldState ()
forall a b. (a -> b) -> a -> b
$ Party -> Action WorldState ()
Model.CloseWithInitialSnapshot Party
party
      DL WorldState (Var (UTxO' (TxOut CtxUTxO Era))) -> DL WorldState ()
forall (f :: * -> *) a. Functor f => f a -> f ()
void (DL WorldState (Var (UTxO' (TxOut CtxUTxO Era)))
 -> DL WorldState ())
-> DL WorldState (Var (UTxO' (TxOut CtxUTxO Era)))
-> DL WorldState ()
forall a b. (a -> b) -> a -> b
$ Action WorldState (UTxO' (TxOut CtxUTxO Era))
-> DL WorldState (Var (UTxO' (TxOut CtxUTxO Era)))
forall a s.
(Typeable a, Eq (Action s a), Show (Action s a)) =>
Action s a -> DL s (Var a)
action (Action WorldState (UTxO' (TxOut CtxUTxO Era))
 -> DL WorldState (Var (UTxO' (TxOut CtxUTxO Era))))
-> Action WorldState (UTxO' (TxOut CtxUTxO Era))
-> DL WorldState (Var (UTxO' (TxOut CtxUTxO Era)))
forall a b. (a -> b) -> a -> b
$ Party -> Action WorldState (UTxO' (TxOut CtxUTxO Era))
Model.Fanout Party
party
    WorldState
_ -> () -> DL WorldState ()
forall a. a -> DL WorldState a
forall (f :: * -> *) a. Applicative f => a -> f a
pure ()
  Action WorldState () -> DL WorldState ()
forall a. Typeable a => Action WorldState a -> DL WorldState ()
action_ Action WorldState ()
Model.StopTheWorld

-- | Given any random walk of the model, if the Head is open a NewTx getting
-- confirmed must be part of the UTxO after finalization.
fanoutContainsWholeConfirmedUTxO :: DL WorldState ()
fanoutContainsWholeConfirmedUTxO :: DL WorldState ()
fanoutContainsWholeConfirmedUTxO = do
  DL WorldState ()
forall s. DL s ()
anyActions_
  DL WorldState WorldState
forall s. DL s s
getModelStateDL DL WorldState WorldState
-> (WorldState -> DL WorldState ()) -> DL WorldState ()
forall a b.
DL WorldState a -> (a -> DL WorldState b) -> DL WorldState b
forall (m :: * -> *) a b. Monad m => m a -> (a -> m b) -> m b
>>= \case
    st :: WorldState
st@WorldState{$sel:hydraState:WorldState :: WorldState -> GlobalState
hydraState = Open{}} -> do
      (Party
party, Payment
payment) <- Quantification (Party, Payment) -> DL WorldState (Party, Payment)
forall a s.
QuantifyConstraints (HasNoVariables a) =>
Quantification a -> DL s a
forAllNonVariableQ (WorldState -> Quantification (Party, Payment)
nonConflictingTx WorldState
st)
      Var Payment
tx <- Action WorldState Payment -> DL WorldState (Var Payment)
forall a s.
(Typeable a, Eq (Action s a), Show (Action s a)) =>
Action s a -> DL s (Var a)
action (Action WorldState Payment -> DL WorldState (Var Payment))
-> Action WorldState Payment -> DL WorldState (Var Payment)
forall a b. (a -> b) -> a -> b
$ Party -> Payment -> Action WorldState Payment
Model.NewTx Party
party Payment
payment
      Action WorldState () -> DL WorldState ()
eventually (Var Payment -> Action WorldState ()
ObserveConfirmedTx Var Payment
tx)
      Action WorldState () -> DL WorldState ()
forall a. Typeable a => Action WorldState a -> DL WorldState ()
action_ (Action WorldState () -> DL WorldState ())
-> Action WorldState () -> DL WorldState ()
forall a b. (a -> b) -> a -> b
$ Party -> Action WorldState ()
Model.Close Party
party
      -- NOTE: The check is actually in the Model postcondition for 'Fanout'
      DL WorldState (Var (UTxO' (TxOut CtxUTxO Era))) -> DL WorldState ()
forall (f :: * -> *) a. Functor f => f a -> f ()
void (DL WorldState (Var (UTxO' (TxOut CtxUTxO Era)))
 -> DL WorldState ())
-> DL WorldState (Var (UTxO' (TxOut CtxUTxO Era)))
-> DL WorldState ()
forall a b. (a -> b) -> a -> b
$ Action WorldState (UTxO' (TxOut CtxUTxO Era))
-> DL WorldState (Var (UTxO' (TxOut CtxUTxO Era)))
forall a s.
(Typeable a, Eq (Action s a), Show (Action s a)) =>
Action s a -> DL s (Var a)
action (Action WorldState (UTxO' (TxOut CtxUTxO Era))
 -> DL WorldState (Var (UTxO' (TxOut CtxUTxO Era))))
-> Action WorldState (UTxO' (TxOut CtxUTxO Era))
-> DL WorldState (Var (UTxO' (TxOut CtxUTxO Era)))
forall a b. (a -> b) -> a -> b
$ Party -> Action WorldState (UTxO' (TxOut CtxUTxO Era))
Model.Fanout Party
party
    WorldState
_ -> () -> DL WorldState ()
forall a. a -> DL WorldState a
forall (f :: * -> *) a. Applicative f => a -> f a
pure ()
  Action WorldState () -> DL WorldState ()
forall a. Typeable a => Action WorldState a -> DL WorldState ()
action_ Action WorldState ()
Model.StopTheWorld

nonConflictingTx :: WorldState -> Quantification (Party, Payment.Payment)
nonConflictingTx :: WorldState -> Quantification (Party, Payment)
nonConflictingTx WorldState
st =
  Gen (Party, Payment)
-> ((Party, Payment) -> Bool)
-> ((Party, Payment) -> [(Party, Payment)])
-> Quantification (Party, Payment)
forall a. Gen a -> (a -> Bool) -> (a -> [a]) -> Quantification a
withGenQ (WorldState -> Gen (Party, Payment)
genPayment WorldState
st) (Bool -> (Party, Payment) -> Bool
forall a b. a -> b -> a
const Bool
True) ([(Party, Payment)] -> (Party, Payment) -> [(Party, Payment)]
forall a b. a -> b -> a
const [])
    Quantification (Party, Payment)
-> ((Party, Payment) -> Bool) -> Quantification (Party, Payment)
forall a. Quantification a -> (a -> Bool) -> Quantification a
`whereQ` \(Party
party, Payment
tx) -> WorldState -> Action WorldState Payment -> Bool
forall state a. StateModel state => state -> Action state a -> Bool
forall a. WorldState -> Action WorldState a -> Bool
precondition WorldState
st (Party -> Payment -> Action WorldState Payment
Model.NewTx Party
party Payment
tx)

headOpensIfAllPartiesCommit :: DL WorldState ()
headOpensIfAllPartiesCommit :: DL WorldState ()
headOpensIfAllPartiesCommit = do
  DL WorldState ()
seedTheWorld
  DL WorldState ()
initHead
  DL WorldState ()
everybodyCommit
  Action WorldState () -> DL WorldState ()
forall a. Typeable a => Action WorldState a -> DL WorldState ()
eventually' Action WorldState ()
ObserveHeadIsOpen
 where
  eventually' :: Action WorldState a -> DL WorldState ()
eventually' Action WorldState a
a = Action WorldState () -> DL WorldState (Var ())
forall a s.
(Typeable a, Eq (Action s a), Show (Action s a)) =>
Action s a -> DL s (Var a)
action (DiffTime -> Action WorldState ()
Wait DiffTime
1000) DL WorldState (Var ()) -> DL WorldState () -> DL WorldState ()
forall a b. DL WorldState a -> DL WorldState b -> DL WorldState b
forall (m :: * -> *) a b. Monad m => m a -> m b -> m b
>> Action WorldState a -> DL WorldState ()
forall a. Typeable a => Action WorldState a -> DL WorldState ()
action_ Action WorldState a
a

  seedTheWorld :: DL WorldState ()
seedTheWorld = Quantification (Action WorldState ())
-> DL WorldState (Action WorldState ())
forall a s.
QuantifyConstraints (HasNoVariables a) =>
Quantification a -> DL s a
forAllNonVariableQ (Gen (Action WorldState ())
-> (Action WorldState () -> Bool)
-> (Action WorldState () -> [Action WorldState ()])
-> Quantification (Action WorldState ())
forall a. Gen a -> (a -> Bool) -> (a -> [a]) -> Quantification a
withGenQ Gen (Action WorldState ())
genSeed (Bool -> Action WorldState () -> Bool
forall a b. a -> b -> a
const Bool
True) ([Action WorldState ()]
-> Action WorldState () -> [Action WorldState ()]
forall a b. a -> b -> a
const [])) DL WorldState (Action WorldState ())
-> (Action WorldState () -> DL WorldState ()) -> DL WorldState ()
forall a b.
DL WorldState a -> (a -> DL WorldState b) -> DL WorldState b
forall (m :: * -> *) a b. Monad m => m a -> (a -> m b) -> m b
>>= Action WorldState () -> DL WorldState ()
forall a. Typeable a => Action WorldState a -> DL WorldState ()
action_

  initHead :: DL WorldState ()
initHead = do
    WorldState{[(SigningKey HydraKey, CardanoSigningKey)]
$sel:hydraParties:WorldState :: WorldState -> [(SigningKey HydraKey, CardanoSigningKey)]
hydraParties :: [(SigningKey HydraKey, CardanoSigningKey)]
hydraParties} <- DL WorldState WorldState
forall s. DL s s
getModelStateDL
    Quantification (Action WorldState HeadId)
-> DL
     WorldState (Quantifies (Quantification (Action WorldState HeadId)))
forall q s. Quantifiable q => q -> DL s (Quantifies q)
forAllQ (Gen (Action WorldState HeadId)
-> (Action WorldState HeadId -> Bool)
-> (Action WorldState HeadId -> [Action WorldState HeadId])
-> Quantification (Action WorldState HeadId)
forall a. Gen a -> (a -> Bool) -> (a -> [a]) -> Quantification a
withGenQ ([(SigningKey HydraKey, CardanoSigningKey)]
-> Gen (Action WorldState HeadId)
forall b.
[(SigningKey HydraKey, b)] -> Gen (Action WorldState HeadId)
genInit [(SigningKey HydraKey, CardanoSigningKey)]
hydraParties) (Bool -> Action WorldState HeadId -> Bool
forall a b. a -> b -> a
const Bool
True) ([Action WorldState HeadId]
-> Action WorldState HeadId -> [Action WorldState HeadId]
forall a b. a -> b -> a
const [])) DL WorldState (Action WorldState HeadId)
-> (Action WorldState HeadId -> DL WorldState ())
-> DL WorldState ()
forall a b.
DL WorldState a -> (a -> DL WorldState b) -> DL WorldState b
forall (m :: * -> *) a b. Monad m => m a -> (a -> m b) -> m b
>>= Action WorldState HeadId -> DL WorldState ()
forall a. Typeable a => Action WorldState a -> DL WorldState ()
action_

  everybodyCommit :: DL WorldState ()
everybodyCommit = do
    WorldState{[(SigningKey HydraKey, CardanoSigningKey)]
$sel:hydraParties:WorldState :: WorldState -> [(SigningKey HydraKey, CardanoSigningKey)]
hydraParties :: [(SigningKey HydraKey, CardanoSigningKey)]
hydraParties, GlobalState
$sel:hydraState:WorldState :: WorldState -> GlobalState
hydraState :: GlobalState
hydraState} <- DL WorldState WorldState
forall s. DL s s
getModelStateDL
    case GlobalState
hydraState of
      Initial{Var HeadId
headIdVar :: Var HeadId
$sel:headIdVar:Start :: GlobalState -> Var HeadId
headIdVar, Uncommitted
pendingCommits :: Uncommitted
$sel:pendingCommits:Start :: GlobalState -> Uncommitted
pendingCommits} ->
        [(SigningKey HydraKey, CardanoSigningKey)]
-> ((SigningKey HydraKey, CardanoSigningKey) -> DL WorldState ())
-> DL WorldState ()
forall (t :: * -> *) (m :: * -> *) a b.
(Foldable t, Monad m) =>
t a -> (a -> m b) -> m ()
forM_ [(SigningKey HydraKey, CardanoSigningKey)]
hydraParties (((SigningKey HydraKey, CardanoSigningKey) -> DL WorldState ())
 -> DL WorldState ())
-> ((SigningKey HydraKey, CardanoSigningKey) -> DL WorldState ())
-> DL WorldState ()
forall a b. (a -> b) -> a -> b
$ \(SigningKey HydraKey, CardanoSigningKey)
p -> do
          let party :: Party
party = SigningKey HydraKey -> Party
deriveParty ((SigningKey HydraKey, CardanoSigningKey) -> SigningKey HydraKey
forall a b. (a, b) -> a
fst (SigningKey HydraKey, CardanoSigningKey)
p)
          case Party
-> Map Party [(CardanoSigningKey, Value)]
-> Maybe [(CardanoSigningKey, Value)]
forall k a. Ord k => k -> Map k a -> Maybe a
Map.lookup Party
party Map Party [(CardanoSigningKey, Value)]
Uncommitted
pendingCommits of
            Maybe [(CardanoSigningKey, Value)]
Nothing -> () -> DL WorldState ()
forall a. a -> DL WorldState a
forall (f :: * -> *) a. Applicative f => a -> f a
pure ()
            Just [(CardanoSigningKey, Value)]
utxo ->
              DL WorldState (Var ()) -> DL WorldState ()
forall (f :: * -> *) a. Functor f => f a -> f ()
void (DL WorldState (Var ()) -> DL WorldState ())
-> DL WorldState (Var ()) -> DL WorldState ()
forall a b. (a -> b) -> a -> b
$ Action WorldState () -> DL WorldState (Var ())
forall a s.
(Typeable a, Eq (Action s a), Show (Action s a)) =>
Action s a -> DL s (Var a)
action (Action WorldState () -> DL WorldState (Var ()))
-> Action WorldState () -> DL WorldState (Var ())
forall a b. (a -> b) -> a -> b
$ Var HeadId -> Party -> UTxOType Payment -> Action WorldState ()
Model.Commit Var HeadId
headIdVar Party
party [(CardanoSigningKey, Value)]
UTxOType Payment
utxo
      GlobalState
_ -> () -> DL WorldState ()
forall a. a -> DL WorldState a
forall (f :: * -> *) a. Applicative f => a -> f a
pure ()

-- • Conflict-Free Liveness (Head):
--
-- In presence of a network adversary, a conflict-free execution satisfies the following condition:
-- For any transaction tx input via (new,tx), tx ∈ T i∈[n] Ci eventually holds.
--
-- TODO: make the network adversarial => make the model runner interleave/delay network messages
conflictFreeLiveness :: DL WorldState ()
conflictFreeLiveness :: DL WorldState ()
conflictFreeLiveness = do
  DL WorldState ()
forall s. DL s ()
anyActions_
  DL WorldState WorldState
forall s. DL s s
getModelStateDL DL WorldState WorldState
-> (WorldState -> DL WorldState ()) -> DL WorldState ()
forall a b.
DL WorldState a -> (a -> DL WorldState b) -> DL WorldState b
forall (m :: * -> *) a b. Monad m => m a -> (a -> m b) -> m b
>>= \case
    st :: WorldState
st@WorldState{$sel:hydraState:WorldState :: WorldState -> GlobalState
hydraState = Open{}} -> do
      (Party
party, Payment
payment) <- Quantification (Party, Payment) -> DL WorldState (Party, Payment)
forall a s.
QuantifyConstraints (HasNoVariables a) =>
Quantification a -> DL s a
forAllNonVariableQ (WorldState -> Quantification (Party, Payment)
nonConflictingTx WorldState
st)
      Var Payment
tx <- Action WorldState Payment -> DL WorldState (Var Payment)
forall a s.
(Typeable a, Eq (Action s a), Show (Action s a)) =>
Action s a -> DL s (Var a)
action (Action WorldState Payment -> DL WorldState (Var Payment))
-> Action WorldState Payment -> DL WorldState (Var Payment)
forall a b. (a -> b) -> a -> b
$ Party -> Payment -> Action WorldState Payment
Model.NewTx Party
party Payment
payment
      Action WorldState () -> DL WorldState ()
eventually (Var Payment -> Action WorldState ()
ObserveConfirmedTx Var Payment
tx)
    WorldState
_ -> () -> DL WorldState ()
forall a. a -> DL WorldState a
forall (f :: * -> *) a. Applicative f => a -> f a
pure ()
  Action WorldState () -> DL WorldState ()
forall a. Typeable a => Action WorldState a -> DL WorldState ()
action_ Action WorldState ()
Model.StopTheWorld

-- There cannot be a UTxO with no ADAs
-- See https://github.com/input-output-hk/cardano-ledger/blob/master/doc/explanations/min-utxo-mary.rst
propDoesNotGenerate0AdaUTxO :: Actions WorldState -> Property
propDoesNotGenerate0AdaUTxO :: Actions WorldState -> Property
propDoesNotGenerate0AdaUTxO (Actions [Step WorldState]
actions) =
  Bool -> Property
forall prop. Testable prop => prop -> Property
property (Bool -> Property) -> Bool -> Property
forall a b. (a -> b) -> a -> b
$ Bool -> Bool
not ((Step WorldState -> Bool) -> [Step WorldState] -> Bool
forall (t :: * -> *) a. Foldable t => (a -> Bool) -> t a -> Bool
any Step WorldState -> Bool
contains0AdaUTxO [Step WorldState]
actions)
 where
  contains0AdaUTxO :: Step WorldState -> Bool
  contains0AdaUTxO :: Step WorldState -> Bool
contains0AdaUTxO = \case
    Var a
_anyVar := (ActionWithPolarity (Model.Commit Var HeadId
_ Party
_anyParty UTxOType Payment
utxos) Polarity
_) -> ((CardanoSigningKey, Value) -> Bool)
-> [(CardanoSigningKey, Value)] -> Bool
forall (t :: * -> *) a. Foldable t => (a -> Bool) -> t a -> Bool
any (CardanoSigningKey, Value) -> Bool
forall {a}. (a, Value) -> Bool
contains0Ada [(CardanoSigningKey, Value)]
UTxOType Payment
utxos
    Var a
_anyVar := (ActionWithPolarity (Model.NewTx Party
_anyParty Payment.Payment{Value
value :: Value
$sel:value:Payment :: Payment -> Value
value}) Polarity
_) -> Value
value Value -> Value -> Bool
forall a. Eq a => a -> a -> Bool
== Lovelace -> Value
lovelaceToValue Lovelace
0
    Step WorldState
_anyOtherStep -> Bool
False
  contains0Ada :: (a, Value) -> Bool
contains0Ada = (Value -> Value -> Bool
forall a. Eq a => a -> a -> Bool
== Lovelace -> Value
lovelaceToValue Lovelace
0) (Value -> Bool) -> ((a, Value) -> Value) -> (a, Value) -> Bool
forall b c a. (b -> c) -> (a -> b) -> a -> c
. (a, Value) -> Value
forall a b. (a, b) -> b
snd

-- * Utilities

-- | Specialised runner similar to <monadicST https://hackage.haskell.org/package/QuickCheck-2.14.3/docs/Test-QuickCheck-Monadic.html#v:monadicST>.
runIOSimProp :: Testable a => (forall s. PropertyM (RunMonad (IOSim s)) a) -> Property
runIOSimProp :: forall a.
Testable a =>
(forall s. PropertyM (RunMonad (IOSim s)) a) -> Property
runIOSimProp forall s. PropertyM (RunMonad (IOSim s)) a
p = Gen Property -> Property
forall prop. Testable prop => prop -> Property
property ((forall s. Gen (RunMonad (IOSim s) Property)) -> Gen Property
forall a.
Testable a =>
(forall s. Gen (RunMonad (IOSim s) a)) -> Gen Property
runRunMonadIOSimGen (PropertyM (RunMonad (IOSim s)) a
-> Gen (RunMonad (IOSim s) Property)
forall a (m :: * -> *).
(Testable a, Monad m) =>
PropertyM m a -> Gen (m Property)
monadic' PropertyM (RunMonad (IOSim s)) a
forall s. PropertyM (RunMonad (IOSim s)) a
p))

-- | Similar to <runSTGen https://hackage.haskell.org/package/QuickCheck-2.14.3/docs/Test-QuickCheck-Monadic.html#v:runSTGen>
--
-- It returns `Property` rather than `Gen a`, what allows to enhance the logging
-- in case of failures.
runRunMonadIOSimGen ::
  forall a.
  Testable a =>
  (forall s. Gen (RunMonad (IOSim s) a)) ->
  Gen Property
runRunMonadIOSimGen :: forall a.
Testable a =>
(forall s. Gen (RunMonad (IOSim s) a)) -> Gen Property
runRunMonadIOSimGen forall s. Gen (RunMonad (IOSim s) a)
f = do
  Capture forall a. Gen a -> a
eval <- Gen Capture
capture
  let tr :: SimTrace a
tr = (forall s. IOSim s a) -> SimTrace a
forall a. (forall s. IOSim s a) -> SimTrace a
runSimTrace ((Gen (RunMonad (IOSim s) a) -> RunMonad (IOSim s) a) -> IOSim s a
forall s.
(Gen (RunMonad (IOSim s) a) -> RunMonad (IOSim s) a) -> IOSim s a
sim Gen (RunMonad (IOSim s) a) -> RunMonad (IOSim s) a
forall a. Gen a -> a
eval)
  Property -> Gen Property
forall a. a -> Gen a
forall (m :: * -> *) a. Monad m => a -> m a
return (Property -> Gen Property) -> Property -> Gen Property
forall a b. (a -> b) -> a -> b
$
    SimTrace a -> Property -> Property
forall {prop} {a}. Testable prop => SimTrace a -> prop -> Property
logsOnError SimTrace a
tr (Property -> Property) -> Property -> Property
forall a b. (a -> b) -> a -> b
$
      case Bool -> SimTrace a -> Either Failure a
forall a. Bool -> SimTrace a -> Either Failure a
traceResult Bool
False SimTrace a
tr of
        Right a
a -> a -> Property
forall prop. Testable prop => prop -> Property
property a
a
        Left (FailureException (SomeException e
ex)) ->
          case e -> Maybe HUnitFailure
forall a b. (Typeable a, Typeable b) => a -> Maybe b
cast e
ex of
            Just (HUnitFailure Maybe SrcLoc
loc FailureReason
reason) ->
              Bool
False
                Bool -> (Bool -> Property) -> Property
forall a b. a -> (a -> b) -> b
& String -> Bool -> Property
forall prop. Testable prop => String -> prop -> Property
counterexample (FailureReason -> String
formatFailureReason FailureReason
reason)
                Property -> (Property -> Property) -> Property
forall a b. a -> (a -> b) -> b
& String -> Property -> Property
forall prop. Testable prop => String -> prop -> Property
counterexample (String
"Location: " String -> String -> String
forall a. Semigroup a => a -> a -> a
<> String -> (SrcLoc -> String) -> Maybe SrcLoc -> String
forall b a. b -> (a -> b) -> Maybe a -> b
maybe String
"unknown" SrcLoc -> String
prettySrcLoc Maybe SrcLoc
loc)
            Maybe HUnitFailure
Nothing -> String -> Bool -> Property
forall prop. Testable prop => String -> prop -> Property
counterexample (e -> String
forall b a. (Show a, IsString b) => a -> b
show e
ex) Bool
False
        Left Failure
ex ->
          String -> Bool -> Property
forall prop. Testable prop => String -> prop -> Property
counterexample (Failure -> String
forall b a. (Show a, IsString b) => a -> b
show Failure
ex) Bool
False
 where
  logsOnError :: SimTrace a -> prop -> Property
logsOnError SimTrace a
tr =
    -- NOTE: Store trace dump in file when showing the counterexample. Behavior of
    -- this during shrinking is not 100% confirmed, show the trace directly if you
    -- want to be sure:
    --
    -- counterexample $ toString traceDump
    String -> prop -> Property
forall prop. Testable prop => String -> prop -> Property
counterexample (String -> prop -> Property)
-> (IO String -> String) -> IO String -> prop -> Property
forall b c a. (b -> c) -> (a -> b) -> a -> c
. IO String -> String
forall a. IO a -> a
unsafePerformIO (IO String -> prop -> Property) -> IO String -> prop -> Property
forall a b. (a -> b) -> a -> b
$ do
      String
fn <- String -> String -> IO String
writeSystemTempFile String
"io-sim-trace" (String -> IO String) -> String -> IO String
forall a b. (a -> b) -> a -> b
$ Text -> String
forall a. ToString a => a -> String
toString Text
traceDump
      String -> IO String
forall a. a -> IO a
forall (f :: * -> *) a. Applicative f => a -> f a
pure (String -> IO String) -> String -> IO String
forall a b. (a -> b) -> a -> b
$ String
"IOSim trace stored in: " String -> String -> String
forall a. Semigroup a => a -> a -> a
<> String -> String
forall a. ToString a => a -> String
toString String
fn
   where
    traceDump :: Text
traceDump = Proxy (HydraLog Tx) -> SimTrace a -> Text
forall log a.
(Typeable log, ToJSON log) =>
Proxy log -> SimTrace a -> Text
printTrace (Proxy (HydraLog Tx)
forall {k} (t :: k). Proxy t
Proxy :: Proxy (HydraLog Tx)) SimTrace a
tr

  sim ::
    forall s.
    (Gen (RunMonad (IOSim s) a) -> RunMonad (IOSim s) a) ->
    IOSim s a
  sim :: forall s.
(Gen (RunMonad (IOSim s) a) -> RunMonad (IOSim s) a) -> IOSim s a
sim Gen (RunMonad (IOSim s) a) -> RunMonad (IOSim s) a
eval = do
    TVar s (Nodes (IOSim s))
v <-
      Nodes (IOSim s) -> IOSim s (TVar (IOSim s) (Nodes (IOSim s)))
forall a. a -> IOSim s (TVar (IOSim s) a)
forall (m :: * -> *) a. MonadSTM m => a -> m (TVar m a)
newTVarIO
        Nodes
          { $sel:nodes:Nodes :: Map Party (TestHydraClient Tx (IOSim s))
nodes = Map Party (TestHydraClient Tx (IOSim s))
forall a. Monoid a => a
mempty
          , $sel:logger:Nodes :: Tracer (IOSim s) (HydraLog Tx)
logger = Tracer (IOSim s) (HydraLog Tx)
forall a s. Typeable a => Tracer (IOSim s) a
traceInIOSim
          , $sel:threads:Nodes :: [Async (IOSim s) ()]
threads = [Async (IOSim s) ()]
[Async s ()]
forall a. Monoid a => a
mempty
          , $sel:chain:Nodes :: SimulatedChainNetwork Tx (IOSim s)
chain = SimulatedChainNetwork Tx (IOSim s)
forall tx (m :: * -> *). SimulatedChainNetwork tx m
dummySimulatedChainNetwork
          }
    ReaderT (RunState (IOSim s)) (IOSim s) a
-> RunState (IOSim s) -> IOSim s a
forall r (m :: * -> *) a. ReaderT r m a -> r -> m a
runReaderT (RunMonad (IOSim s) a -> ReaderT (RunState (IOSim s)) (IOSim s) a
forall (m :: * -> *) a. RunMonad m a -> ReaderT (RunState m) m a
runMonad (Gen (RunMonad (IOSim s) a) -> RunMonad (IOSim s) a
eval Gen (RunMonad (IOSim s) a)
forall s. Gen (RunMonad (IOSim s) a)
f)) (TVar (IOSim s) (Nodes (IOSim s)) -> RunState (IOSim s)
forall (m :: * -> *). TVar m (Nodes m) -> RunState m
RunState TVar (IOSim s) (Nodes (IOSim s))
TVar s (Nodes (IOSim s))
v)

eventually :: Action WorldState () -> DL WorldState ()
eventually :: Action WorldState () -> DL WorldState ()
eventually Action WorldState ()
a = Action WorldState () -> DL WorldState ()
forall a. Typeable a => Action WorldState a -> DL WorldState ()
action_ (DiffTime -> Action WorldState ()
Wait DiffTime
10) DL WorldState () -> DL WorldState () -> DL WorldState ()
forall a b. DL WorldState a -> DL WorldState b -> DL WorldState b
forall (m :: * -> *) a b. Monad m => m a -> m b -> m b
>> Action WorldState () -> DL WorldState ()
forall a. Typeable a => Action WorldState a -> DL WorldState ()
action_ Action WorldState ()
a

action_ :: Typeable a => Action WorldState a -> DL WorldState ()
action_ :: forall a. Typeable a => Action WorldState a -> DL WorldState ()
action_ = DL WorldState (Var a) -> DL WorldState ()
forall (f :: * -> *) a. Functor f => f a -> f ()
void (DL WorldState (Var a) -> DL WorldState ())
-> (Action WorldState a -> DL WorldState (Var a))
-> Action WorldState a
-> DL WorldState ()
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Action WorldState a -> DL WorldState (Var a)
forall a s.
(Typeable a, Eq (Action s a), Show (Action s a)) =>
Action s a -> DL s (Var a)
action