{-# 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 Interruptable
--   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.
-- This sequence can be copy/pasted and reused directly as a test against either the `Model` or the implementation
-- as exemplified by the following sample:
--
-- @@
--  it "runs actions against actual nodes" $ do
--    let Actions act =
--          Actions
--            [ Var 1
--                := Seed
--                  { seedKeys =
--                      [ (HydraSigningKey (SignKeyEd25519DSIGN "00000000000000000000000000000000000000000000000000000000000000003b6a27bcceb6a42d62a3a8d02a6f0d73653215771de243a63ac048a18b59da29"),
--                                          "0100000008030606080507030707000607020508050000020207070508040800")
--                      , (HydraSigningKey (SignKeyEd25519DSIGN "2e00000000000000000000000000000000000000000000000000000000000000264a0707979e0d6691f74b055429b5f318d39c2883bb509310b67424252e9ef2"),
--                                          "0106010101070600040403010600080805020003040508030307080706060608")
--                      , (HydraSigningKey (SignKeyEd25519DSIGN "ed785af0fb0000000000000000000000000000000000000000000000000000001c02babf6d3d51b725db8b72043823d66634b39db74836b1494bdb647073d566"),
--                                          "0000070304040705060101030802010105080806050605070104030603010503")
--                      ]
--                  }
--            , Var 2 := Command{Model.party = Party{vkey = HydraVerificationKey (VerKeyEd25519DSIGN "3b6a27bcceb6a42d62a3a8d02a6f0d73653215771de243a63ac048a18b59da29")},
--                               command = Init{contestationPeriod = -6.413670805613}}
--            , Var 3 := Command{Model.party = Party{vkey = HydraVerificationKey (VerKeyEd25519DSIGN "264a0707979e0d6691f74b055429b5f318d39c2883bb509310b67424252e9ef2")},
--                               command = Commit{Input.utxo = [("0106010101070600040403010600080805020003040508030307080706060608", fromList [(AdaAssetId, 18470954)])]}}
--            , Var 4 := Command{Model.party = Party{vkey = HydraVerificationKey (VerKeyEd25519DSIGN "1c02babf6d3d51b725db8b72043823d66634b39db74836b1494bdb647073d566")},
--                               command = Commit{Input.utxo = [("0000070304040705060101030802010105080806050605070104030603010503", fromList [(AdaAssetId, 19691416)])]}}
--            , Var 5 := Command{Model.party = Party{vkey = HydraVerificationKey (VerKeyEd25519DSIGN "3b6a27bcceb6a42d62a3a8d02a6f0d73653215771de243a63ac048a18b59da29")},
--                               command = Commit{Input.utxo = [("0100000008030606080507030707000607020508050000020207070508040800", fromList [(AdaAssetId, 7003529)])]}}
--            , Var 6
--                := Command
--                  { Model.party = Party{vkey = HydraVerificationKey (VerKeyEd25519DSIGN "3b6a27bcceb6a42d62a3a8d02a6f0d73653215771de243a63ac048a18b59da29")}
--                  , command =
--                      NewTx
--                        { Input.transaction =
--                            Payment
--                              { from = "0100000008030606080507030707000607020508050000020207070508040800"
--                              , to = "0106010101070600040403010600080805020003040508030307080706060608"
--                              , value = fromList [(AdaAssetId, 7003529)]
--                              }
--                        }
--                  }
--            ]
--        -- env and model state are unused in perform
--        env = []
--
--        dummyState :: WorldState (IOSim s)
--        dummyState = WorldState{hydraParties = mempty, hydraState = Start}
--
--        loop [] = pure ()
--        loop ((Var{} := a) : as) = do
--          void $ perform dummyState a (lookUpVar env)
--          loop as
--        tr =
--          runSimTrace $
--            evalStateT
--              (loop act)
--              (Nodes mempty traceInIOSim)
--        traceDump = printTrace (Proxy :: Proxy Tx) tr
--    print traceDump
--    True `shouldBe` True
-- @@
module Hydra.ModelSpec where

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

import Cardano.Api.UTxO qualified as UTxO
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 GHC.IO (unsafePerformIO)
import Hydra.API.ClientInput (ClientInput (..))
import Hydra.API.ServerOutput (ServerOutput (..))
import Hydra.BehaviorSpec (TestHydraClient (..), dummySimulatedChainNetwork)
import Hydra.Logging.Messages (HydraLog)
import Hydra.Model (
  Action (ObserveConfirmedTx, ObserveHeadIsOpen, Wait),
  GlobalState (..),
  Nodes (Nodes, nodes),
  OffChainState (..),
  RunMonad,
  RunState (..),
  WorldState (..),
  genInit,
  genPayment,
  genSeed,
  runMonad,
  toRealUTxO,
  toTxOuts,
 )
import Hydra.Model qualified as Model
import Hydra.Model.Payment qualified as Payment
import Hydra.Tx.Party (Party (..), deriveParty)
import System.IO.Temp (writeSystemTempFile)
import Test.Hydra.Tx.Fixture (testNetworkId)
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', monitor, run)
import Test.QuickCheck.Property ((===))
import Test.QuickCheck.StateModel (
  ActionWithPolarity (..),
  Actions,
  Annotated (..),
  Step ((:=)),
  precondition,
  runActions,
  stateAfter,
  pattern Actions,
 )
import Test.Util (printTrace, traceInIOSim)

spec :: Spec
spec :: Spec
spec = do
  -- 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
  String -> Property -> Spec
forall prop.
(HasCallStack, Testable prop) =>
String -> prop -> Spec
prop String
"model should not generate 0 Ada UTxO" (Property -> Spec) -> Property -> Spec
forall a b. (a -> b) -> a -> b
$ Int -> (Actions WorldState -> Bool) -> Property
forall prop. Testable prop => Int -> prop -> Property
withMaxSuccess Int
10000 Actions WorldState -> Bool
prop_doesNotGenerate0AdaUTxO
  String -> Property -> Spec
forall prop.
(HasCallStack, Testable prop) =>
String -> prop -> Spec
prop String
"model generates consistent traces" (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
prop_generateTraces
  String -> (Actions WorldState -> Property) -> Spec
forall prop.
(HasCallStack, Testable prop) =>
String -> prop -> Spec
prop String
"implementation respects model" Actions WorldState -> Property
prop_HydraModel
  String -> Property -> Spec
forall prop.
(HasCallStack, Testable prop) =>
String -> prop -> Spec
prop String
"check conflict-free liveness" Property
prop_checkConflictFreeLiveness
  String -> Property -> Spec
forall prop.
(HasCallStack, Testable prop) =>
String -> prop -> Spec
prop String
"check head opens if all participants commit" Property
prop_checkHeadOpensIfAllPartiesCommit
  String -> Property -> Spec
forall prop.
(HasCallStack, Testable prop) =>
String -> prop -> Spec
prop String
"fanout contains whole confirmed UTxO" Property
prop_fanoutContainsWholeConfirmedUTxO
  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 -> Property -> Spec
forall prop.
(HasCallStack, Testable prop) =>
String -> prop -> Spec
prop String
"parties contest to wrong closed snapshot" Property
prop_partyContestsToWrongClosedSnapshot

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))

prop_partyContestsToWrongClosedSnapshot :: Property
prop_partyContestsToWrongClosedSnapshot :: Property
prop_partyContestsToWrongClosedSnapshot =
  DL WorldState () -> (Actions WorldState -> Property) -> Property
forall s a.
(DynLogicModel s, Testable a) =>
DL s () -> (Actions s -> a) -> Property
forAllDL DL WorldState ()
partyContestsToWrongClosedSnapshot Actions WorldState -> Property
prop_HydraModel

-- | 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 ()
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 ()
action_ Action WorldState ()
Model.StopTheWorld

prop_fanoutContainsWholeConfirmedUTxO :: Property
prop_fanoutContainsWholeConfirmedUTxO :: Property
prop_fanoutContainsWholeConfirmedUTxO =
  DL WorldState () -> (Actions WorldState -> Property) -> Property
forall s a.
(DynLogicModel s, Testable a) =>
DL s () -> (Actions s -> a) -> Property
forAllDL DL WorldState ()
fanoutContainsWholeConfirmedUTxO Actions WorldState -> Property
prop_HydraModel

-- | 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 ()
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 ()
action_ Action WorldState ()
Model.StopTheWorld

prop_checkHeadOpensIfAllPartiesCommit :: Property
prop_checkHeadOpensIfAllPartiesCommit :: Property
prop_checkHeadOpensIfAllPartiesCommit =
  Int -> Property -> Property
forall prop. Testable prop => Int -> prop -> Property
within Int
50000000 (Property -> Property) -> Property -> Property
forall a b. (a -> b) -> a -> b
$
    DL WorldState () -> (Actions WorldState -> Property) -> Property
forall s a.
(DynLogicModel s, Testable a) =>
DL s () -> (Actions s -> a) -> Property
forAllDL DL WorldState ()
headOpensIfAllPartiesCommit Actions WorldState -> Property
prop_HydraModel

headOpensIfAllPartiesCommit :: DL WorldState ()
headOpensIfAllPartiesCommit :: DL WorldState ()
headOpensIfAllPartiesCommit = do
  DL WorldState ()
seedTheWorld
  DL WorldState ()
initHead
  DL WorldState ()
everybodyCommit
  Action WorldState () -> DL WorldState ()
eventually' Action WorldState ()
ObserveHeadIsOpen
 where
  eventually' :: Action WorldState () -> DL WorldState ()
eventually' Action WorldState ()
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 () -> DL WorldState ()
action_ Action WorldState ()
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 ()
action_

  initHead :: DL WorldState ()
initHead = do
    WorldState{[(SigningKey HydraKey, CardanoSigningKey)]
hydraParties :: [(SigningKey HydraKey, CardanoSigningKey)]
$sel:hydraParties:WorldState :: WorldState -> [(SigningKey HydraKey, CardanoSigningKey)]
hydraParties} <- DL WorldState WorldState
forall s. DL s s
getModelStateDL
    Quantification (Action WorldState ())
-> DL
     WorldState (Quantifies (Quantification (Action WorldState ())))
forall q s. Quantifiable q => q -> DL s (Quantifies q)
forAllQ (Gen (Action WorldState ())
-> (Action WorldState () -> Bool)
-> (Action WorldState () -> [Action WorldState ()])
-> Quantification (Action WorldState ())
forall a. Gen a -> (a -> Bool) -> (a -> [a]) -> Quantification a
withGenQ ([(SigningKey HydraKey, CardanoSigningKey)]
-> Gen (Action WorldState ())
forall b. [(SigningKey HydraKey, b)] -> Gen (Action WorldState ())
genInit [(SigningKey HydraKey, CardanoSigningKey)]
hydraParties) (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 ()
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{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 [(CardanoSigningKey, Value)])
-> DL WorldState ()
forall (f :: * -> *) a. Functor f => f a -> f ()
void (DL WorldState (Var [(CardanoSigningKey, Value)])
 -> DL WorldState ())
-> DL WorldState (Var [(CardanoSigningKey, Value)])
-> DL WorldState ()
forall a b. (a -> b) -> a -> b
$ Action WorldState (UTxOType Payment)
-> DL WorldState (Var (UTxOType Payment))
forall a s.
(Typeable a, Eq (Action s a), Show (Action s a)) =>
Action s a -> DL s (Var a)
action (Action WorldState (UTxOType Payment)
 -> DL WorldState (Var (UTxOType Payment)))
-> Action WorldState (UTxOType Payment)
-> DL WorldState (Var (UTxOType Payment))
forall a b. (a -> b) -> a -> b
$ Party -> UTxOType Payment -> Action WorldState (UTxOType Payment)
Model.Commit 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 ()

prop_checkConflictFreeLiveness :: Property
prop_checkConflictFreeLiveness :: Property
prop_checkConflictFreeLiveness =
  Int -> Property -> Property
forall prop. Testable prop => Int -> prop -> Property
within Int
50000000 (Property -> Property) -> Property -> Property
forall a b. (a -> b) -> a -> b
$
    DL WorldState () -> (Actions WorldState -> Property) -> Property
forall s a.
(DynLogicModel s, Testable a) =>
DL s () -> (Actions s -> a) -> Property
forAllDL DL WorldState ()
conflictFreeLiveness Actions WorldState -> Property
prop_HydraModel

prop_HydraModel :: Actions WorldState -> Property
prop_HydraModel :: Actions WorldState -> Property
prop_HydraModel 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

-- • 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 ()
action_ Action WorldState ()
Model.StopTheWorld

prop_generateTraces :: Actions WorldState -> Property
prop_generateTraces :: Actions WorldState -> Property
prop_generateTraces Actions WorldState
actions =
  let Metadata VarContext
_vars WorldState
st = Actions WorldState -> Annotated WorldState
forall state. StateModel state => Actions state -> Annotated state
stateAfter Actions WorldState
actions
   in case Actions WorldState
actions of
        Actions [] -> Bool -> Property
forall prop. Testable prop => prop -> Property
property Bool
True
        Actions [Step WorldState]
_ ->
          WorldState -> GlobalState
hydraState WorldState
st GlobalState -> GlobalState -> Bool
forall a. Eq a => a -> a -> Bool
/= GlobalState
Start
            Bool -> (Bool -> Property) -> Property
forall a b. a -> (a -> b) -> b
& String -> Bool -> Property
forall prop. Testable prop => String -> prop -> Property
counterexample (String
"state: " String -> String -> String
forall a. Semigroup a => a -> a -> a
<> WorldState -> String
forall b a. (Show a, IsString b) => a -> b
show WorldState
st)

prop_doesNotGenerate0AdaUTxO :: Actions WorldState -> Bool
prop_doesNotGenerate0AdaUTxO :: Actions WorldState -> Bool
prop_doesNotGenerate0AdaUTxO (Actions [Step WorldState]
actions) =
  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 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

prop_checkModel :: Property
prop_checkModel :: Property
prop_checkModel =
  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)]
$sel:hydraParties:WorldState :: WorldState -> [(SigningKey HydraKey, CardanoSigningKey)]
hydraParties :: [(SigningKey HydraKey, CardanoSigningKey)]
hydraParties, GlobalState
$sel:hydraState:WorldState :: WorldState -> GlobalState
hydraState :: 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
          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
  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
$ TestHydraClient Tx (IOSim s) -> RunMonad (IOSim s) (UTxOType Tx)
forall {t :: (* -> *) -> * -> *} {m :: * -> *} {tx}.
(MonadTrans t, Monad m) =>
TestHydraClient tx m -> t m (UTxOType tx)
getUTxO TestHydraClient Tx (IOSim s)
node
      let expectedBalance :: Map Text Value
expectedBalance =
            (Value -> Value -> Value) -> [(Text, Value)] -> Map Text Value
forall k a. Ord k => (a -> a -> a) -> [(k, a)] -> Map k a
Map.fromListWith
              Value -> Value -> Value
forall a. Semigroup a => a -> a -> a
(<>)
              [ (AddressInEra -> Text
unwrapAddress AddressInEra
addr, Value
value)
              | (Payment.CardanoSigningKey SigningKey PaymentKey
sk, Value
value) <- [(CardanoSigningKey, Value)]
UTxOType Payment
confirmedUTxO
              , let addr :: AddressInEra
addr = NetworkId -> VerificationKey PaymentKey -> AddressInEra
forall era.
IsShelleyBasedEra era =>
NetworkId -> VerificationKey PaymentKey -> AddressInEra era
mkVkAddress NetworkId
testNetworkId (SigningKey PaymentKey -> VerificationKey PaymentKey
forall keyrole.
(Key keyrole, HasTypeProxy keyrole) =>
SigningKey keyrole -> VerificationKey keyrole
getVerificationKey SigningKey PaymentKey
sk)
              , Value -> Maybe Lovelace
valueToLovelace Value
value Maybe Lovelace -> Maybe Lovelace -> Bool
forall a. Eq a => a -> a -> Bool
/= Lovelace -> Maybe Lovelace
forall a. a -> Maybe a
Just Lovelace
0
              ]
      let actualBalance :: Map Text Value
actualBalance =
            (Value -> Value -> Value) -> [(Text, Value)] -> Map Text Value
forall k a. Ord k => (a -> a -> a) -> [(k, a)] -> Map k a
Map.fromListWith Value -> Value -> Value
forall a. Semigroup a => a -> a -> a
(<>) ([(Text, Value)] -> Map Text Value)
-> [(Text, Value)] -> Map Text Value
forall a b. (a -> b) -> a -> b
$
              [ (AddressInEra -> Text
unwrapAddress AddressInEra
addr, Value
value)
              | (TxOut AddressInEra
addr Value
value TxOutDatum CtxUTxO
_ ReferenceScript
_) <- Map TxIn (TxOut CtxUTxO Era) -> [TxOut CtxUTxO Era]
forall k a. Map k a -> [a]
Map.elems (UTxO' (TxOut CtxUTxO Era) -> Map TxIn (TxOut CtxUTxO Era)
forall out. UTxO' out -> Map TxIn out
UTxO.toMap UTxO' (TxOut CtxUTxO Era)
utxo)
              , Value -> Maybe Lovelace
valueToLovelace Value
value Maybe Lovelace -> Maybe Lovelace -> Bool
forall a. Eq a => a -> a -> Bool
/= Lovelace -> Maybe Lovelace
forall a. a -> Maybe a
Just Lovelace
0
              ]
      (Property -> Property) -> PropertyM (RunMonad (IOSim s)) ()
forall (m :: * -> *).
Monad m =>
(Property -> Property) -> PropertyM m ()
monitor ((Property -> Property) -> PropertyM (RunMonad (IOSim s)) ())
-> (Property -> Property) -> PropertyM (RunMonad (IOSim s)) ()
forall a b. (a -> b) -> a -> b
$
        String -> Property -> Property
forall prop. Testable prop => String -> prop -> Property
counterexample (String -> Property -> Property) -> String -> Property -> Property
forall a b. (a -> b) -> a -> b
$
          Text -> String
forall a. ToString a => a -> String
toString (Text -> String) -> Text -> String
forall a b. (a -> b) -> a -> b
$
            [Text] -> Text
forall t. IsText t "unlines" => [t] -> t
unlines
              [ Text
"actualBalance = " Text -> Text -> Text
forall a. Semigroup a => a -> a -> a
<> Map Text Value -> Text
forall b a. (Show a, IsString b) => a -> b
show Map Text Value
actualBalance
              , Text
"expectedBalance = " Text -> Text -> Text
forall a. Semigroup a => a -> a -> a
<> Map Text Value -> Text
forall b a. (Show a, IsString b) => a -> b
show Map Text Value
expectedBalance
              , Text
"Difference: (" Text -> Text -> Text
forall a. Semigroup a => a -> a -> a
<> Party -> Text
forall b a. (Show a, IsString b) => a -> b
show Party
p Text -> Text -> Text
forall a. Semigroup a => a -> a -> a
<> Text
") " Text -> Text -> Text
forall a. Semigroup a => a -> a -> a
<> Map Text Value -> Text
forall b a. (Show a, IsString b) => a -> b
show (Map Text Value -> Map Text Value -> Map Text Value
forall k a b. Ord k => Map k a -> Map k b -> Map k a
Map.difference Map Text Value
actualBalance Map Text Value
expectedBalance)
              ]
      Bool -> PropertyM (RunMonad (IOSim s)) ()
forall (m :: * -> *). Monad m => Bool -> PropertyM m ()
assert (Map Text Value
expectedBalance Map Text Value -> Map Text Value -> Bool
forall a. Eq a => a -> a -> Bool
== Map Text Value
actualBalance)
    GlobalState
_ -> do
      () -> PropertyM (RunMonad (IOSim s)) ()
forall a. a -> PropertyM (RunMonad (IOSim s)) a
forall (f :: * -> *) a. Applicative f => a -> f a
pure ()
 where
  getUTxO :: TestHydraClient tx m -> t m (UTxOType tx)
getUTxO TestHydraClient tx m
node = m (UTxOType tx) -> t m (UTxOType tx)
forall (m :: * -> *) a. Monad m => m a -> t m a
forall (t :: (* -> *) -> * -> *) (m :: * -> *) a.
(MonadTrans t, Monad m) =>
m a -> t m a
lift (m (UTxOType tx) -> t m (UTxOType tx))
-> m (UTxOType tx) -> t m (UTxOType tx)
forall a b. (a -> b) -> a -> b
$ do
    TestHydraClient tx m
node TestHydraClient tx m -> ClientInput tx -> m ()
forall tx (m :: * -> *).
TestHydraClient tx m -> ClientInput tx -> m ()
`send` ClientInput tx
forall tx. ClientInput tx
GetUTxO
    let loop :: m (UTxOType tx)
loop =
          TestHydraClient tx m -> m (ServerOutput tx)
forall tx (m :: * -> *).
TestHydraClient tx m -> m (ServerOutput tx)
waitForNext TestHydraClient tx m
node m (ServerOutput tx)
-> (ServerOutput tx -> m (UTxOType tx)) -> m (UTxOType tx)
forall a b. m a -> (a -> m b) -> m b
forall (m :: * -> *) a b. Monad m => m a -> (a -> m b) -> m b
>>= \case
            GetUTxOResponse HeadId
_ UTxOType tx
u -> UTxOType tx -> m (UTxOType tx)
forall a. a -> m a
forall (f :: * -> *) a. Applicative f => a -> f a
pure UTxOType tx
u
            ServerOutput tx
_ -> m (UTxOType tx)
loop
    m (UTxOType tx)
loop

--

-- * Utilities for `IOSim`

--

-- | 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)) ->
          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
  -- 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.
  logsOnError :: SimTrace a -> prop -> Property
logsOnError SimTrace a
tr =
    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)

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)

eventually :: Action WorldState () -> DL WorldState ()
eventually :: Action WorldState () -> DL WorldState ()
eventually Action WorldState ()
a = Action WorldState () -> 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 ()
action_ Action WorldState ()
a

action_ :: Action WorldState () -> DL WorldState ()
action_ :: Action WorldState () -> DL WorldState ()
action_ = DL WorldState (Var ()) -> DL WorldState ()
forall (f :: * -> *) a. Functor f => f a -> f ()
void (DL WorldState (Var ()) -> DL WorldState ())
-> (Action WorldState () -> DL WorldState (Var ()))
-> Action WorldState ()
-> DL WorldState ()
forall b c a. (b -> c) -> (a -> b) -> a -> c
. 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

unwrapAddress :: AddressInEra -> Text
unwrapAddress :: AddressInEra -> Text
unwrapAddress = \case
  ShelleyAddressInEra Address ShelleyAddr
addr -> Address ShelleyAddr -> Text
forall a. SerialiseAsBech32 a => a -> Text
serialiseToBech32 Address ShelleyAddr
addr
  ByronAddressInEra{} -> Text -> Text
forall a t. (HasCallStack, IsText t) => t -> a
error Text
"Byron."