{-# LANGUAGE OverloadedRecordDot #-}
{-# OPTIONS_GHC -Wno-ambiguous-fields #-}

-- | Stateful model-based testing of the transactions created by the "Direct"
-- chain modules.
--
-- The model is focusing on transitions between Open and Closed states of the
-- head.
--
-- Given an initial UTxO, the model generates a plausible sequence of snapshots
-- that an honest node would approve. That is, the total balance of UTxO remains
-- constant and utxoToDecommit is only allowed to clear if the version is
-- incremented. Consequently, also all snapshots are correctly signed (we don't
-- test handling of adverarial signatures). UTxOs are simplified such that they
-- are A-E items, where each maps to an arbitrary real UTxO.
--
-- From this sequence of valid snapshots, possible Decrement and Close actions
-- are generated, along with occasional Contest and consequential Fanout.
module Hydra.Chain.Direct.TxTraceSpec where

import Hydra.Prelude hiding (Any, State, label, show)
import Test.Hydra.Prelude

import Cardano.Api.UTxO (UTxO)
import Cardano.Api.UTxO qualified as UTxO
import Data.List (nub, (\\))
import Data.Map.Strict qualified as Map
import Data.Time.Clock.POSIX (posixSecondsToUTCTime)
import Hydra.Cardano.Api (
  PaymentKey,
  SlotNo (..),
  TxId,
  VerificationKey,
  getTxBody,
  getTxId,
  lovelaceToValue,
  mkTxOutDatumInline,
  modifyTxOutValue,
  selectLovelace,
  throwError,
  txOutAddress,
  txOutValue,
  txSpendingUTxO,
 )
import Hydra.Cardano.Api.Pretty (renderTxWithUTxO)
import Hydra.Chain.Direct.State (ChainContext (..), CloseTxError, ContestTxError, DecrementTxError, FanoutTxError, IncrementTxError (..), close, contest, decrement, fanout, increment)
import Hydra.Contract.HeadState qualified as Head
import Hydra.Ledger.Cardano (Tx, adjustUTxO)
import Hydra.Ledger.Cardano.Evaluate (evaluateTx)
import Hydra.Tx (CommitBlueprintTx (..))
import Hydra.Tx.ContestationPeriod qualified as CP
import Hydra.Tx.Crypto (MultiSignature, aggregate, sign)
import Hydra.Tx.Deposit (depositTx)
import Hydra.Tx.HeadId (headIdToCurrencySymbol, mkHeadId)
import Hydra.Tx.Init (mkHeadOutput)
import Hydra.Tx.IsTx (hashUTxO, utxoFromTx)
import Hydra.Tx.Observe (HeadObservation (NoHeadTx), observeHeadTx)
import Hydra.Tx.Observe qualified as Tx
import Hydra.Tx.Party (partyToChain)
import Hydra.Tx.ScriptRegistry (ScriptRegistry, registryUTxO)
import Hydra.Tx.Snapshot (ConfirmedSnapshot (..), Snapshot (..), SnapshotNumber (..), SnapshotVersion (..), getSnapshot, number)
import PlutusTx.Builtins (toBuiltin)
import Test.Hydra.Tx.Fixture (alice, bob, carol, testNetworkId)
import Test.Hydra.Tx.Fixture qualified as Fixture
import Test.Hydra.Tx.Gen (
  genForParty,
  genScriptRegistry,
  genTxOut,
  genUTxO1,
  genVerificationKey,
 )
import Test.Hydra.Tx.Mutation (addParticipationTokens)
import Test.QuickCheck (Confidence (..), Property, Smart (..), Testable, checkCoverage, checkCoverageWith, cover, elements, frequency, ioProperty, (===))
import Test.QuickCheck.Monadic (monadic)
import Test.QuickCheck.StateModel (
  ActionWithPolarity (..),
  Actions (..),
  Any (..),
  HasVariables (getAllVariables),
  Polarity (..),
  PostconditionM,
  Realized,
  RunModel (..),
  StateModel (..),
  Step ((:=)),
  Var,
  VarContext,
  counterexamplePost,
  runActions,
 )
import Text.Show (Show (..))

spec :: Spec
spec :: Spec
spec = do
  String -> (ModelUTxO -> ModelUTxO -> Property) -> Spec
forall prop.
(HasCallStack, Testable prop) =>
String -> prop -> Spec
prop String
"realWorldModelUTxO preserves addition" ((ModelUTxO -> ModelUTxO -> Property) -> Spec)
-> (ModelUTxO -> ModelUTxO -> Property) -> Spec
forall a b. (a -> b) -> a -> b
$ \ModelUTxO
u1 ModelUTxO
u2 ->
    ModelUTxO -> UTxO
realWorldModelUTxO (ModelUTxO
u1 ModelUTxO -> ModelUTxO -> ModelUTxO
forall a. Semigroup a => a -> a -> a
<> ModelUTxO
u2) UTxO -> UTxO -> Property
forall a. (Eq a, Show a) => a -> a -> Property
=== (ModelUTxO -> UTxO
realWorldModelUTxO ModelUTxO
u1 UTxO -> UTxO -> UTxO
forall a. Semigroup a => a -> a -> a
<> ModelUTxO -> UTxO
realWorldModelUTxO ModelUTxO
u2)
  String -> (Actions Model -> Property) -> Spec
forall prop.
(HasCallStack, Testable prop) =>
String -> prop -> Spec
prop String
"generates interesting transaction traces" ((Actions Model -> Property) -> Spec)
-> (Actions Model -> Property) -> Spec
forall a b. (a -> b) -> a -> b
$ \Actions Model
actions ->
    Property -> Property
forall prop. Testable prop => prop -> Property
checkCoverage (Property -> Property) -> Property -> Property
forall a b. (a -> b) -> a -> b
$ Actions Model -> Bool -> Property
forall p. Testable p => Actions Model -> p -> Property
coversInterestingActions Actions Model
actions Bool
True
  String -> Property -> Spec
forall prop.
(HasCallStack, Testable prop) =>
String -> prop -> Spec
prop String
"all valid transactions" (Property -> Spec) -> Property -> Spec
forall a b. (a -> b) -> a -> b
$
    -- NOTE: Using lower confidence to improve performance. In case of an error,
    -- check coverage numbers and also the distribution in above test (which is
    -- way faster).
    Confidence -> (Actions Model -> Property) -> Property
forall prop. Testable prop => Confidence -> prop -> Property
checkCoverageWith
      Confidence{certainty :: Integer
certainty = Integer
100, tolerance :: Double
tolerance = Double
0.8}
      Actions Model -> Property
prop_runActions

coversInterestingActions :: Testable p => Actions Model -> p -> Property
coversInterestingActions :: forall p. Testable p => Actions Model -> p -> Property
coversInterestingActions (Actions_ [String]
_ (Smart Int
_ [Step Model]
steps)) p
p =
  p
p
    p -> (p -> Property) -> Property
forall a b. a -> (a -> b) -> b
& Double -> Bool -> String -> p -> Property
forall prop.
Testable prop =>
Double -> Bool -> String -> prop -> Property
cover Double
1 ([Step Model] -> Bool
forall a. [a] -> Bool
forall (t :: * -> *) a. Foldable t => t a -> Bool
null [Step Model]
steps) String
"empty"
    Property -> (Property -> Property) -> Property
forall a b. a -> (a -> b) -> b
& Double -> Bool -> String -> Property -> Property
forall prop.
Testable prop =>
Double -> Bool -> String -> prop -> Property
cover Double
50 ([Step Model] -> Bool
hasSomeSnapshots [Step Model]
steps) String
"has some snapshots"
    Property -> (Property -> Property) -> Property
forall a b. a -> (a -> b) -> b
& Double -> Bool -> String -> Property -> Property
forall prop.
Testable prop =>
Double -> Bool -> String -> prop -> Property
cover Double
5 ([Step Model] -> Bool
hasDeposit [Step Model]
steps) String
"has deposits"
    Property -> (Property -> Property) -> Property
forall a b. a -> (a -> b) -> b
& Double -> Bool -> String -> Property -> Property
forall prop.
Testable prop =>
Double -> Bool -> String -> prop -> Property
cover Double
5 ([Step Model] -> Bool
hasIncrement [Step Model]
steps) String
"has increments"
    Property -> (Property -> Property) -> Property
forall a b. a -> (a -> b) -> b
& Double -> Bool -> String -> Property -> Property
forall prop.
Testable prop =>
Double -> Bool -> String -> prop -> Property
cover Double
5 ([Step Model] -> Bool
hasDecrement [Step Model]
steps) String
"has decrements"
    Property -> (Property -> Property) -> Property
forall a b. a -> (a -> b) -> b
& Double -> Bool -> String -> Property -> Property
forall prop.
Testable prop =>
Double -> Bool -> String -> prop -> Property
cover Double
0.05 ([Step Model] -> Int
countContests [Step Model]
steps Int -> Int -> Bool
forall a. Ord a => a -> a -> Bool
>= Int
2) String
"has multiple contests"
    Property -> (Property -> Property) -> Property
forall a b. a -> (a -> b) -> b
& Double -> Bool -> String -> Property -> Property
forall prop.
Testable prop =>
Double -> Bool -> String -> prop -> Property
cover Double
5 ([Step Model] -> Bool
closeNonInitial [Step Model]
steps) String
"close with non initial snapshots"
    Property -> (Property -> Property) -> Property
forall a b. a -> (a -> b) -> b
& Double -> Bool -> String -> Property -> Property
forall prop.
Testable prop =>
Double -> Bool -> String -> prop -> Property
cover Double
10 ([Step Model] -> Bool
hasFanout [Step Model]
steps) String
"reach fanout"
    Property -> (Property -> Property) -> Property
forall a b. a -> (a -> b) -> b
& Double -> Bool -> String -> Property -> Property
forall prop.
Testable prop =>
Double -> Bool -> String -> prop -> Property
cover Double
10 ([Step Model] -> Bool
fanoutWithSomeUTxO [Step Model]
steps) String
"fanout with some UTxO"
    Property -> (Property -> Property) -> Property
forall a b. a -> (a -> b) -> b
& Double -> Bool -> String -> Property -> Property
forall prop.
Testable prop =>
Double -> Bool -> String -> prop -> Property
cover Double
10 ([Step Model] -> Bool
fanoutWithCommitOrDecommitDelta [Step Model]
steps) String
"fanout with additional de/commit UTxO to distribute"
 where
  hasSomeSnapshots :: [Step Model] -> Bool
hasSomeSnapshots =
    (Step Model -> Bool) -> [Step Model] -> Bool
forall (t :: * -> *) a. Foldable t => (a -> Bool) -> t a -> Bool
any ((Step Model -> Bool) -> [Step Model] -> Bool)
-> (Step Model -> Bool) -> [Step Model] -> Bool
forall a b. (a -> b) -> a -> b
$
      \(Var a
_ := ActionWithPolarity{Action Model a
polarAction :: Action Model a
polarAction :: forall state a. ActionWithPolarity state a -> Action state a
polarAction, Polarity
polarity :: Polarity
polarity :: forall state a. ActionWithPolarity state a -> Polarity
polarity}) -> case Action Model a
polarAction of
        NewSnapshot{} ->
          Polarity
polarity Polarity -> Polarity -> Bool
forall a. Eq a => a -> a -> Bool
== Polarity
PosPolarity
        Action Model a
_ -> Bool
False

  hasUTxOToCommit :: ModelSnapshot -> Bool
hasUTxOToCommit ModelSnapshot
snapshot = Bool -> Bool
not (Bool -> Bool) -> (ModelUTxO -> Bool) -> ModelUTxO -> Bool
forall b c a. (b -> c) -> (a -> b) -> a -> c
. ModelUTxO -> Bool
forall a. [a] -> Bool
forall (t :: * -> *) a. Foldable t => t a -> Bool
null (ModelUTxO -> Bool) -> ModelUTxO -> Bool
forall a b. (a -> b) -> a -> b
$ ModelSnapshot -> ModelUTxO
toCommit ModelSnapshot
snapshot
  hasUTxOToDecommit :: ModelSnapshot -> Bool
hasUTxOToDecommit ModelSnapshot
snapshot = Bool -> Bool
not (Bool -> Bool) -> (ModelUTxO -> Bool) -> ModelUTxO -> Bool
forall b c a. (b -> c) -> (a -> b) -> a -> c
. ModelUTxO -> Bool
forall a. [a] -> Bool
forall (t :: * -> *) a. Foldable t => t a -> Bool
null (ModelUTxO -> Bool) -> ModelUTxO -> Bool
forall a b. (a -> b) -> a -> b
$ ModelSnapshot -> ModelUTxO
toDecommit ModelSnapshot
snapshot

  hasFanout :: [Step Model] -> Bool
hasFanout =
    (Step Model -> Bool) -> [Step Model] -> Bool
forall (t :: * -> *) a. Foldable t => (a -> Bool) -> t a -> Bool
any ((Step Model -> Bool) -> [Step Model] -> Bool)
-> (Step Model -> Bool) -> [Step Model] -> Bool
forall a b. (a -> b) -> a -> b
$
      \(Var a
_ := ActionWithPolarity{Action Model a
polarAction :: forall state a. ActionWithPolarity state a -> Action state a
polarAction :: Action Model a
polarAction, Polarity
polarity :: forall state a. ActionWithPolarity state a -> Polarity
polarity :: Polarity
polarity}) -> case Action Model a
polarAction of
        Fanout{} -> Polarity
polarity Polarity -> Polarity -> Bool
forall a. Eq a => a -> a -> Bool
== Polarity
PosPolarity
        Action Model a
_ -> Bool
False

  fanoutWithSomeUTxO :: [Step Model] -> Bool
fanoutWithSomeUTxO =
    (Step Model -> Bool) -> [Step Model] -> Bool
forall (t :: * -> *) a. Foldable t => (a -> Bool) -> t a -> Bool
any ((Step Model -> Bool) -> [Step Model] -> Bool)
-> (Step Model -> Bool) -> [Step Model] -> Bool
forall a b. (a -> b) -> a -> b
$
      \(Var a
_ := ActionWithPolarity{Action Model a
polarAction :: forall state a. ActionWithPolarity state a -> Action state a
polarAction :: Action Model a
polarAction, Polarity
polarity :: forall state a. ActionWithPolarity state a -> Polarity
polarity :: Polarity
polarity}) -> case Action Model a
polarAction of
        Fanout{ModelUTxO
utxo :: ModelUTxO
$sel:utxo:NewSnapshot :: Action Model TxResult -> ModelUTxO
utxo} ->
          Polarity
polarity Polarity -> Polarity -> Bool
forall a. Eq a => a -> a -> Bool
== Polarity
PosPolarity
            Bool -> Bool -> Bool
&& Bool -> Bool
not (ModelUTxO -> Bool
forall a. [a] -> Bool
forall (t :: * -> *) a. Foldable t => t a -> Bool
null ModelUTxO
utxo)
        Action Model a
_ -> Bool
False

  fanoutWithCommitOrDecommitDelta :: [Step Model] -> Bool
fanoutWithCommitOrDecommitDelta =
    (Step Model -> Bool) -> [Step Model] -> Bool
forall (t :: * -> *) a. Foldable t => (a -> Bool) -> t a -> Bool
any ((Step Model -> Bool) -> [Step Model] -> Bool)
-> (Step Model -> Bool) -> [Step Model] -> Bool
forall a b. (a -> b) -> a -> b
$
      \(Var a
_ := ActionWithPolarity{Action Model a
polarAction :: forall state a. ActionWithPolarity state a -> Action state a
polarAction :: Action Model a
polarAction, Polarity
polarity :: forall state a. ActionWithPolarity state a -> Polarity
polarity :: Polarity
polarity}) -> case Action Model a
polarAction of
        Fanout{ModelUTxO
alphaUTxO :: ModelUTxO
$sel:alphaUTxO:NewSnapshot :: Action Model TxResult -> ModelUTxO
alphaUTxO, ModelUTxO
omegaUTxO :: ModelUTxO
$sel:omegaUTxO:NewSnapshot :: Action Model TxResult -> ModelUTxO
omegaUTxO} ->
          Polarity
polarity Polarity -> Polarity -> Bool
forall a. Eq a => a -> a -> Bool
== Polarity
PosPolarity
            Bool -> Bool -> Bool
&& (Bool -> Bool
not (ModelUTxO -> Bool
forall a. [a] -> Bool
forall (t :: * -> *) a. Foldable t => t a -> Bool
null ModelUTxO
alphaUTxO) Bool -> Bool -> Bool
|| Bool -> Bool
not (ModelUTxO -> Bool
forall a. [a] -> Bool
forall (t :: * -> *) a. Foldable t => t a -> Bool
null ModelUTxO
omegaUTxO))
        Action Model a
_ -> Bool
False

  countContests :: [Step Model] -> Int
countContests =
    [Step Model] -> Int
forall a. [a] -> Int
forall (t :: * -> *) a. Foldable t => t a -> Int
length
      ([Step Model] -> Int)
-> ([Step Model] -> [Step Model]) -> [Step Model] -> Int
forall b c a. (b -> c) -> (a -> b) -> a -> c
. (Step Model -> Bool) -> [Step Model] -> [Step Model]
forall a. (a -> Bool) -> [a] -> [a]
filter
        ( \(Var a
_ := ActionWithPolarity{Action Model a
polarAction :: forall state a. ActionWithPolarity state a -> Action state a
polarAction :: Action Model a
polarAction, Polarity
polarity :: forall state a. ActionWithPolarity state a -> Polarity
polarity :: Polarity
polarity}) -> case Action Model a
polarAction of
            Contest{} -> Polarity
polarity Polarity -> Polarity -> Bool
forall a. Eq a => a -> a -> Bool
== Polarity
PosPolarity
            Action Model a
_ -> Bool
False
        )

  closeNonInitial :: [Step Model] -> Bool
closeNonInitial =
    (Step Model -> Bool) -> [Step Model] -> Bool
forall (t :: * -> *) a. Foldable t => (a -> Bool) -> t a -> Bool
any ((Step Model -> Bool) -> [Step Model] -> Bool)
-> (Step Model -> Bool) -> [Step Model] -> Bool
forall a b. (a -> b) -> a -> b
$ \(Var a
_ := ActionWithPolarity{Action Model a
polarAction :: forall state a. ActionWithPolarity state a -> Action state a
polarAction :: Action Model a
polarAction}) -> case Action Model a
polarAction of
      Close{ModelSnapshot
snapshot :: ModelSnapshot
$sel:snapshot:NewSnapshot :: Action Model TxResult -> ModelSnapshot
snapshot} -> ModelSnapshot
snapshot ModelSnapshot -> ModelSnapshot -> Bool
forall a. Ord a => a -> a -> Bool
> ModelSnapshot
0
      Action Model a
_ -> Bool
False

  hasDeposit :: [Step Model] -> Bool
hasDeposit =
    (Step Model -> Bool) -> [Step Model] -> Bool
forall (t :: * -> *) a. Foldable t => (a -> Bool) -> t a -> Bool
all ((Step Model -> Bool) -> [Step Model] -> Bool)
-> (Step Model -> Bool) -> [Step Model] -> Bool
forall a b. (a -> b) -> a -> b
$
      \(Var a
_ := ActionWithPolarity{Action Model a
polarAction :: forall state a. ActionWithPolarity state a -> Action state a
polarAction :: Action Model a
polarAction, Polarity
polarity :: forall state a. ActionWithPolarity state a -> Polarity
polarity :: Polarity
polarity}) -> case Action Model a
polarAction of
        Deposit{} ->
          Polarity
polarity Polarity -> Polarity -> Bool
forall a. Eq a => a -> a -> Bool
== Polarity
PosPolarity
        Action Model a
_ -> Bool
False
  hasIncrement :: [Step Model] -> Bool
hasIncrement =
    (Step Model -> Bool) -> [Step Model] -> Bool
forall (t :: * -> *) a. Foldable t => (a -> Bool) -> t a -> Bool
all ((Step Model -> Bool) -> [Step Model] -> Bool)
-> (Step Model -> Bool) -> [Step Model] -> Bool
forall a b. (a -> b) -> a -> b
$
      \(Var a
_ := ActionWithPolarity{Action Model a
polarAction :: forall state a. ActionWithPolarity state a -> Action state a
polarAction :: Action Model a
polarAction, Polarity
polarity :: forall state a. ActionWithPolarity state a -> Polarity
polarity :: Polarity
polarity}) -> case Action Model a
polarAction of
        Increment{ModelSnapshot
$sel:snapshot:NewSnapshot :: Action Model TxResult -> ModelSnapshot
snapshot :: ModelSnapshot
snapshot} ->
          Polarity
polarity Polarity -> Polarity -> Bool
forall a. Eq a => a -> a -> Bool
== Polarity
PosPolarity
            Bool -> Bool -> Bool
&& ModelSnapshot -> Bool
hasUTxOToCommit ModelSnapshot
snapshot
        Action Model a
_ -> Bool
False
  hasDecrement :: [Step Model] -> Bool
hasDecrement =
    (Step Model -> Bool) -> [Step Model] -> Bool
forall (t :: * -> *) a. Foldable t => (a -> Bool) -> t a -> Bool
all ((Step Model -> Bool) -> [Step Model] -> Bool)
-> (Step Model -> Bool) -> [Step Model] -> Bool
forall a b. (a -> b) -> a -> b
$
      \(Var a
_ := ActionWithPolarity{Action Model a
polarAction :: forall state a. ActionWithPolarity state a -> Action state a
polarAction :: Action Model a
polarAction, Polarity
polarity :: forall state a. ActionWithPolarity state a -> Polarity
polarity :: Polarity
polarity}) -> case Action Model a
polarAction of
        Decrement{ModelSnapshot
$sel:snapshot:NewSnapshot :: Action Model TxResult -> ModelSnapshot
snapshot :: ModelSnapshot
snapshot} ->
          Polarity
polarity Polarity -> Polarity -> Bool
forall a. Eq a => a -> a -> Bool
== Polarity
PosPolarity
            Bool -> Bool -> Bool
&& ModelSnapshot -> Bool
hasUTxOToDecommit ModelSnapshot
snapshot
        Action Model a
_ -> Bool
False

prop_runActions :: Actions Model -> Property
prop_runActions :: Actions Model -> Property
prop_runActions Actions Model
actions =
  Actions Model -> Property -> Property
forall p. Testable p => Actions Model -> p -> Property
coversInterestingActions Actions Model
actions
    (Property -> Property)
-> (PropertyM AppM () -> Property) -> PropertyM AppM () -> Property
forall b c a. (b -> c) -> (a -> b) -> a -> c
. (AppM Property -> Property) -> PropertyM AppM () -> Property
forall a (m :: * -> *).
(Testable a, Monad m) =>
(m Property -> Property) -> PropertyM m a -> Property
monadic AppM Property -> Property
runAppMProperty
    (PropertyM AppM () -> Property) -> PropertyM AppM () -> Property
forall a b. (a -> b) -> a -> b
$ do
      -- print actions
      PropertyM AppM (Annotated Model, Env AppM) -> PropertyM AppM ()
forall (f :: * -> *) a. Functor f => f a -> f ()
void (Actions Model -> PropertyM AppM (Annotated Model, Env AppM)
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 Model
actions)
 where
  runAppMProperty :: AppM Property -> Property
  runAppMProperty :: AppM Property -> Property
runAppMProperty AppM Property
action = IO Property -> Property
forall prop. Testable prop => IO prop -> Property
ioProperty (IO Property -> Property) -> IO Property -> Property
forall a b. (a -> b) -> a -> b
$ do
    IORef (Maybe TxId, UTxO)
localState <- (Maybe TxId, UTxO) -> IO (IORef (Maybe TxId, UTxO))
forall (m :: * -> *) a. MonadIO m => a -> m (IORef a)
newIORef (Maybe TxId
forall a. Maybe a
Nothing, UTxO
openHeadUTxO)
    ReaderT (IORef (Maybe TxId, UTxO)) IO Property
-> IORef (Maybe TxId, UTxO) -> IO Property
forall r (m :: * -> *) a. ReaderT r m a -> r -> m a
runReaderT (AppM Property -> ReaderT (IORef (Maybe TxId, UTxO)) IO Property
forall a. AppM a -> ReaderT (IORef (Maybe TxId, UTxO)) IO a
runAppM AppM Property
action) IORef (Maybe TxId, UTxO)
localState

-- * ============================== MODEL WORLD ==========================

data SingleUTxO = A | B | C | D | E | F | G | H | I
  deriving (Int -> SingleUTxO -> ShowS
ModelUTxO -> ShowS
SingleUTxO -> String
(Int -> SingleUTxO -> ShowS)
-> (SingleUTxO -> String)
-> (ModelUTxO -> ShowS)
-> Show SingleUTxO
forall a.
(Int -> a -> ShowS) -> (a -> String) -> ([a] -> ShowS) -> Show a
$cshowsPrec :: Int -> SingleUTxO -> ShowS
showsPrec :: Int -> SingleUTxO -> ShowS
$cshow :: SingleUTxO -> String
show :: SingleUTxO -> String
$cshowList :: ModelUTxO -> ShowS
showList :: ModelUTxO -> ShowS
Show, SingleUTxO -> SingleUTxO -> Bool
(SingleUTxO -> SingleUTxO -> Bool)
-> (SingleUTxO -> SingleUTxO -> Bool) -> Eq SingleUTxO
forall a. (a -> a -> Bool) -> (a -> a -> Bool) -> Eq a
$c== :: SingleUTxO -> SingleUTxO -> Bool
== :: SingleUTxO -> SingleUTxO -> Bool
$c/= :: SingleUTxO -> SingleUTxO -> Bool
/= :: SingleUTxO -> SingleUTxO -> Bool
Eq, Eq SingleUTxO
Eq SingleUTxO =>
(SingleUTxO -> SingleUTxO -> Ordering)
-> (SingleUTxO -> SingleUTxO -> Bool)
-> (SingleUTxO -> SingleUTxO -> Bool)
-> (SingleUTxO -> SingleUTxO -> Bool)
-> (SingleUTxO -> SingleUTxO -> Bool)
-> (SingleUTxO -> SingleUTxO -> SingleUTxO)
-> (SingleUTxO -> SingleUTxO -> SingleUTxO)
-> Ord SingleUTxO
SingleUTxO -> SingleUTxO -> Bool
SingleUTxO -> SingleUTxO -> Ordering
SingleUTxO -> SingleUTxO -> SingleUTxO
forall a.
Eq a =>
(a -> a -> Ordering)
-> (a -> a -> Bool)
-> (a -> a -> Bool)
-> (a -> a -> Bool)
-> (a -> a -> Bool)
-> (a -> a -> a)
-> (a -> a -> a)
-> Ord a
$ccompare :: SingleUTxO -> SingleUTxO -> Ordering
compare :: SingleUTxO -> SingleUTxO -> Ordering
$c< :: SingleUTxO -> SingleUTxO -> Bool
< :: SingleUTxO -> SingleUTxO -> Bool
$c<= :: SingleUTxO -> SingleUTxO -> Bool
<= :: SingleUTxO -> SingleUTxO -> Bool
$c> :: SingleUTxO -> SingleUTxO -> Bool
> :: SingleUTxO -> SingleUTxO -> Bool
$c>= :: SingleUTxO -> SingleUTxO -> Bool
>= :: SingleUTxO -> SingleUTxO -> Bool
$cmax :: SingleUTxO -> SingleUTxO -> SingleUTxO
max :: SingleUTxO -> SingleUTxO -> SingleUTxO
$cmin :: SingleUTxO -> SingleUTxO -> SingleUTxO
min :: SingleUTxO -> SingleUTxO -> SingleUTxO
Ord, Int -> SingleUTxO
SingleUTxO -> Int
SingleUTxO -> ModelUTxO
SingleUTxO -> SingleUTxO
SingleUTxO -> SingleUTxO -> ModelUTxO
SingleUTxO -> SingleUTxO -> SingleUTxO -> ModelUTxO
(SingleUTxO -> SingleUTxO)
-> (SingleUTxO -> SingleUTxO)
-> (Int -> SingleUTxO)
-> (SingleUTxO -> Int)
-> (SingleUTxO -> ModelUTxO)
-> (SingleUTxO -> SingleUTxO -> ModelUTxO)
-> (SingleUTxO -> SingleUTxO -> ModelUTxO)
-> (SingleUTxO -> SingleUTxO -> SingleUTxO -> ModelUTxO)
-> Enum SingleUTxO
forall a.
(a -> a)
-> (a -> a)
-> (Int -> a)
-> (a -> Int)
-> (a -> [a])
-> (a -> a -> [a])
-> (a -> a -> [a])
-> (a -> a -> a -> [a])
-> Enum a
$csucc :: SingleUTxO -> SingleUTxO
succ :: SingleUTxO -> SingleUTxO
$cpred :: SingleUTxO -> SingleUTxO
pred :: SingleUTxO -> SingleUTxO
$ctoEnum :: Int -> SingleUTxO
toEnum :: Int -> SingleUTxO
$cfromEnum :: SingleUTxO -> Int
fromEnum :: SingleUTxO -> Int
$cenumFrom :: SingleUTxO -> ModelUTxO
enumFrom :: SingleUTxO -> ModelUTxO
$cenumFromThen :: SingleUTxO -> SingleUTxO -> ModelUTxO
enumFromThen :: SingleUTxO -> SingleUTxO -> ModelUTxO
$cenumFromTo :: SingleUTxO -> SingleUTxO -> ModelUTxO
enumFromTo :: SingleUTxO -> SingleUTxO -> ModelUTxO
$cenumFromThenTo :: SingleUTxO -> SingleUTxO -> SingleUTxO -> ModelUTxO
enumFromThenTo :: SingleUTxO -> SingleUTxO -> SingleUTxO -> ModelUTxO
Enum, (forall x. SingleUTxO -> Rep SingleUTxO x)
-> (forall x. Rep SingleUTxO x -> SingleUTxO) -> Generic SingleUTxO
forall x. Rep SingleUTxO x -> SingleUTxO
forall x. SingleUTxO -> Rep SingleUTxO x
forall a.
(forall x. a -> Rep a x) -> (forall x. Rep a x -> a) -> Generic a
$cfrom :: forall x. SingleUTxO -> Rep SingleUTxO x
from :: forall x. SingleUTxO -> Rep SingleUTxO x
$cto :: forall x. Rep SingleUTxO x -> SingleUTxO
to :: forall x. Rep SingleUTxO x -> SingleUTxO
Generic)

instance Arbitrary SingleUTxO where
  arbitrary :: Gen SingleUTxO
arbitrary = Gen SingleUTxO
forall a.
(Generic a, GA UnsizedOpts (Rep a),
 UniformWeight (Weights_ (Rep a))) =>
Gen a
genericArbitrary
  shrink :: SingleUTxO -> ModelUTxO
shrink = SingleUTxO -> ModelUTxO
forall a.
(Generic a, RecursivelyShrink (Rep a), GSubterms (Rep a) a) =>
a -> [a]
genericShrink

type ModelUTxO = [SingleUTxO]

data Model = Model
  { Model -> State
headState :: State
  , Model -> [ModelSnapshot]
knownSnapshots :: [ModelSnapshot]
  -- ^ List of off-chain snapshots, from most recent to oldest.
  , Model -> SnapshotVersion
currentVersion :: SnapshotVersion
  , Model -> SnapshotNumber
currentSnapshotNumber :: SnapshotNumber
  , Model -> SnapshotNumber
closedSnapshotNumber :: SnapshotNumber
  , Model -> [Actor]
alreadyContested :: [Actor]
  , Model -> ModelUTxO
utxoInHead :: ModelUTxO
  , Model -> ModelUTxO
pendingDeposit :: ModelUTxO
  , -- XXX: This is used in two ways, to track pending decommits for generating
    -- snapshots and to remember the pending (delta) utxo during close/fanout
    Model -> ModelUTxO
pendingDecommit :: ModelUTxO
  }
  deriving (Int -> Model -> ShowS
[Model] -> ShowS
Model -> String
(Int -> Model -> ShowS)
-> (Model -> String) -> ([Model] -> ShowS) -> Show Model
forall a.
(Int -> a -> ShowS) -> (a -> String) -> ([a] -> ShowS) -> Show a
$cshowsPrec :: Int -> Model -> ShowS
showsPrec :: Int -> Model -> ShowS
$cshow :: Model -> String
show :: Model -> String
$cshowList :: [Model] -> ShowS
showList :: [Model] -> ShowS
Show)

latestSnapshotNumber :: [ModelSnapshot] -> SnapshotNumber
latestSnapshotNumber :: [ModelSnapshot] -> SnapshotNumber
latestSnapshotNumber = \case
  (ModelSnapshot
s : [ModelSnapshot]
_) -> ModelSnapshot
s.number
  [ModelSnapshot]
_ -> SnapshotNumber
0

-- | Model of a real snapshot which contains a 'SnapshotNumber` but also our
-- simplified form of 'UTxO'.
data ModelSnapshot = ModelSnapshot
  { ModelSnapshot -> SnapshotVersion
version :: SnapshotVersion
  , ModelSnapshot -> SnapshotNumber
number :: SnapshotNumber
  , ModelSnapshot -> ModelUTxO
inHead :: ModelUTxO
  , ModelSnapshot -> ModelUTxO
toCommit :: ModelUTxO
  , ModelSnapshot -> ModelUTxO
toDecommit :: ModelUTxO
  }
  deriving (Int -> ModelSnapshot -> ShowS
[ModelSnapshot] -> ShowS
ModelSnapshot -> String
(Int -> ModelSnapshot -> ShowS)
-> (ModelSnapshot -> String)
-> ([ModelSnapshot] -> ShowS)
-> Show ModelSnapshot
forall a.
(Int -> a -> ShowS) -> (a -> String) -> ([a] -> ShowS) -> Show a
$cshowsPrec :: Int -> ModelSnapshot -> ShowS
showsPrec :: Int -> ModelSnapshot -> ShowS
$cshow :: ModelSnapshot -> String
show :: ModelSnapshot -> String
$cshowList :: [ModelSnapshot] -> ShowS
showList :: [ModelSnapshot] -> ShowS
Show, ModelSnapshot -> ModelSnapshot -> Bool
(ModelSnapshot -> ModelSnapshot -> Bool)
-> (ModelSnapshot -> ModelSnapshot -> Bool) -> Eq ModelSnapshot
forall a. (a -> a -> Bool) -> (a -> a -> Bool) -> Eq a
$c== :: ModelSnapshot -> ModelSnapshot -> Bool
== :: ModelSnapshot -> ModelSnapshot -> Bool
$c/= :: ModelSnapshot -> ModelSnapshot -> Bool
/= :: ModelSnapshot -> ModelSnapshot -> Bool
Eq, Eq ModelSnapshot
Eq ModelSnapshot =>
(ModelSnapshot -> ModelSnapshot -> Ordering)
-> (ModelSnapshot -> ModelSnapshot -> Bool)
-> (ModelSnapshot -> ModelSnapshot -> Bool)
-> (ModelSnapshot -> ModelSnapshot -> Bool)
-> (ModelSnapshot -> ModelSnapshot -> Bool)
-> (ModelSnapshot -> ModelSnapshot -> ModelSnapshot)
-> (ModelSnapshot -> ModelSnapshot -> ModelSnapshot)
-> Ord ModelSnapshot
ModelSnapshot -> ModelSnapshot -> Bool
ModelSnapshot -> ModelSnapshot -> Ordering
ModelSnapshot -> ModelSnapshot -> ModelSnapshot
forall a.
Eq a =>
(a -> a -> Ordering)
-> (a -> a -> Bool)
-> (a -> a -> Bool)
-> (a -> a -> Bool)
-> (a -> a -> Bool)
-> (a -> a -> a)
-> (a -> a -> a)
-> Ord a
$ccompare :: ModelSnapshot -> ModelSnapshot -> Ordering
compare :: ModelSnapshot -> ModelSnapshot -> Ordering
$c< :: ModelSnapshot -> ModelSnapshot -> Bool
< :: ModelSnapshot -> ModelSnapshot -> Bool
$c<= :: ModelSnapshot -> ModelSnapshot -> Bool
<= :: ModelSnapshot -> ModelSnapshot -> Bool
$c> :: ModelSnapshot -> ModelSnapshot -> Bool
> :: ModelSnapshot -> ModelSnapshot -> Bool
$c>= :: ModelSnapshot -> ModelSnapshot -> Bool
>= :: ModelSnapshot -> ModelSnapshot -> Bool
$cmax :: ModelSnapshot -> ModelSnapshot -> ModelSnapshot
max :: ModelSnapshot -> ModelSnapshot -> ModelSnapshot
$cmin :: ModelSnapshot -> ModelSnapshot -> ModelSnapshot
min :: ModelSnapshot -> ModelSnapshot -> ModelSnapshot
Ord, (forall x. ModelSnapshot -> Rep ModelSnapshot x)
-> (forall x. Rep ModelSnapshot x -> ModelSnapshot)
-> Generic ModelSnapshot
forall x. Rep ModelSnapshot x -> ModelSnapshot
forall x. ModelSnapshot -> Rep ModelSnapshot x
forall a.
(forall x. a -> Rep a x) -> (forall x. Rep a x -> a) -> Generic a
$cfrom :: forall x. ModelSnapshot -> Rep ModelSnapshot x
from :: forall x. ModelSnapshot -> Rep ModelSnapshot x
$cto :: forall x. Rep ModelSnapshot x -> ModelSnapshot
to :: forall x. Rep ModelSnapshot x -> ModelSnapshot
Generic)

instance Num ModelSnapshot where
  ModelSnapshot
_ + :: ModelSnapshot -> ModelSnapshot -> ModelSnapshot
+ ModelSnapshot
_ = Text -> ModelSnapshot
forall a t. (HasCallStack, IsText t) => t -> a
error Text
"undefined"
  ModelSnapshot
_ - :: ModelSnapshot -> ModelSnapshot -> ModelSnapshot
- ModelSnapshot
_ = Text -> ModelSnapshot
forall a t. (HasCallStack, IsText t) => t -> a
error Text
"undefined"
  ModelSnapshot
_ * :: ModelSnapshot -> ModelSnapshot -> ModelSnapshot
* ModelSnapshot
_ = Text -> ModelSnapshot
forall a t. (HasCallStack, IsText t) => t -> a
error Text
"undefined"
  abs :: ModelSnapshot -> ModelSnapshot
abs ModelSnapshot
_ = Text -> ModelSnapshot
forall a t. (HasCallStack, IsText t) => t -> a
error Text
"undefined"
  signum :: ModelSnapshot -> ModelSnapshot
signum ModelSnapshot
_ = Text -> ModelSnapshot
forall a t. (HasCallStack, IsText t) => t -> a
error Text
"undefined"
  fromInteger :: Integer -> ModelSnapshot
fromInteger Integer
x =
    ModelSnapshot
      { $sel:version:ModelSnapshot :: SnapshotVersion
version = Nat -> SnapshotVersion
UnsafeSnapshotVersion Nat
0
      , $sel:number:ModelSnapshot :: SnapshotNumber
number = Nat -> SnapshotNumber
UnsafeSnapshotNumber (Nat -> SnapshotNumber) -> Nat -> SnapshotNumber
forall a b. (a -> b) -> a -> b
$ Nat -> Maybe Nat -> Nat
forall a. a -> Maybe a -> a
fromMaybe Nat
0 (Maybe Nat -> Nat) -> Maybe Nat -> Nat
forall a b. (a -> b) -> a -> b
$ Integer -> Maybe Nat
integerToNatural Integer
x
      , $sel:inHead:ModelSnapshot :: ModelUTxO
inHead = ModelUTxO
forall a. Monoid a => a
mempty
      , $sel:toCommit:ModelSnapshot :: ModelUTxO
toCommit = ModelUTxO
forall a. Monoid a => a
mempty
      , $sel:toDecommit:ModelSnapshot :: ModelUTxO
toDecommit = ModelUTxO
forall a. Monoid a => a
mempty
      }

data State
  = Open
  | Closed
  | Final
  deriving (Int -> State -> ShowS
[State] -> ShowS
State -> String
(Int -> State -> ShowS)
-> (State -> String) -> ([State] -> ShowS) -> Show State
forall a.
(Int -> a -> ShowS) -> (a -> String) -> ([a] -> ShowS) -> Show a
$cshowsPrec :: Int -> State -> ShowS
showsPrec :: Int -> State -> ShowS
$cshow :: State -> String
show :: State -> String
$cshowList :: [State] -> ShowS
showList :: [State] -> ShowS
Show, State -> State -> Bool
(State -> State -> Bool) -> (State -> State -> Bool) -> Eq State
forall a. (a -> a -> Bool) -> (a -> a -> Bool) -> Eq a
$c== :: State -> State -> Bool
== :: State -> State -> Bool
$c/= :: State -> State -> Bool
/= :: State -> State -> Bool
Eq)

data Actor = Alice | Bob | Carol
  deriving (Int -> Actor -> ShowS
[Actor] -> ShowS
Actor -> String
(Int -> Actor -> ShowS)
-> (Actor -> String) -> ([Actor] -> ShowS) -> Show Actor
forall a.
(Int -> a -> ShowS) -> (a -> String) -> ([a] -> ShowS) -> Show a
$cshowsPrec :: Int -> Actor -> ShowS
showsPrec :: Int -> Actor -> ShowS
$cshow :: Actor -> String
show :: Actor -> String
$cshowList :: [Actor] -> ShowS
showList :: [Actor] -> ShowS
Show, Actor -> Actor -> Bool
(Actor -> Actor -> Bool) -> (Actor -> Actor -> Bool) -> Eq Actor
forall a. (a -> a -> Bool) -> (a -> a -> Bool) -> Eq a
$c== :: Actor -> Actor -> Bool
== :: Actor -> Actor -> Bool
$c/= :: Actor -> Actor -> Bool
/= :: Actor -> Actor -> Bool
Eq)

-- | Result of constructing and performing a transaction. Notably there are
-- three stages to this which can fail: construction, validation, and
-- observation. Results from all stages are needed to express post-conditions.
data TxResult = TxResult
  { TxResult -> Either String Tx
constructedTx :: Either String Tx
  , TxResult -> UTxO
spendableUTxO :: UTxO
  , TxResult -> Maybe String
validationError :: Maybe String
  , TxResult -> HeadObservation
observation :: HeadObservation
  }
  deriving (TxResult -> TxResult -> Bool
(TxResult -> TxResult -> Bool)
-> (TxResult -> TxResult -> Bool) -> Eq TxResult
forall a. (a -> a -> Bool) -> (a -> a -> Bool) -> Eq a
$c== :: TxResult -> TxResult -> Bool
== :: TxResult -> TxResult -> Bool
$c/= :: TxResult -> TxResult -> Bool
/= :: TxResult -> TxResult -> Bool
Eq, Int -> TxResult -> ShowS
[TxResult] -> ShowS
TxResult -> String
(Int -> TxResult -> ShowS)
-> (TxResult -> String) -> ([TxResult] -> ShowS) -> Show TxResult
forall a.
(Int -> a -> ShowS) -> (a -> String) -> ([a] -> ShowS) -> Show a
$cshowsPrec :: Int -> TxResult -> ShowS
showsPrec :: Int -> TxResult -> ShowS
$cshow :: TxResult -> String
show :: TxResult -> String
$cshowList :: [TxResult] -> ShowS
showList :: [TxResult] -> ShowS
Show)

instance StateModel Model where
  data Action Model a where
    NewSnapshot :: {Action Model () -> ModelSnapshot
newSnapshot :: ModelSnapshot} -> Action Model ()
    Deposit :: {Action Model TxResult -> ModelUTxO
utxoToDeposit :: ModelUTxO} -> Action Model TxResult
    Increment :: {Action Model TxResult -> Actor
actor :: Actor, Action Model TxResult -> ModelSnapshot
snapshot :: ModelSnapshot} -> Action Model TxResult
    Decrement :: {actor :: Actor, snapshot :: ModelSnapshot} -> Action Model TxResult
    Close :: {actor :: Actor, snapshot :: ModelSnapshot} -> Action Model TxResult
    Contest :: {actor :: Actor, snapshot :: ModelSnapshot} -> Action Model TxResult
    Fanout :: {Action Model TxResult -> ModelUTxO
utxo :: ModelUTxO, Action Model TxResult -> ModelUTxO
alphaUTxO :: ModelUTxO, Action Model TxResult -> ModelUTxO
omegaUTxO :: ModelUTxO} -> Action Model TxResult
    -- \| Helper action to identify the terminal state 'Final' and shorten
    -- traces using the 'precondition'.
    Stop :: Action Model ()

  initialState :: Model
initialState =
    Model
      { $sel:headState:Model :: State
headState = State
Open
      , $sel:knownSnapshots:Model :: [ModelSnapshot]
knownSnapshots = []
      , $sel:currentVersion:Model :: SnapshotVersion
currentVersion = SnapshotVersion
0
      , $sel:currentSnapshotNumber:Model :: SnapshotNumber
currentSnapshotNumber = SnapshotNumber
0
      , $sel:closedSnapshotNumber:Model :: SnapshotNumber
closedSnapshotNumber = SnapshotNumber
0
      , $sel:alreadyContested:Model :: [Actor]
alreadyContested = []
      , $sel:utxoInHead:Model :: ModelUTxO
utxoInHead = [Item ModelUTxO] -> ModelUTxO
forall l. IsList l => [Item l] -> l
fromList [Item ModelUTxO
SingleUTxO
A, Item ModelUTxO
SingleUTxO
B, Item ModelUTxO
SingleUTxO
C]
      , $sel:pendingDeposit:Model :: ModelUTxO
pendingDeposit = ModelUTxO
forall a. Monoid a => a
mempty
      , $sel:pendingDecommit:Model :: ModelUTxO
pendingDecommit = ModelUTxO
forall a. Monoid a => a
mempty
      }

  arbitraryAction :: VarContext -> Model -> Gen (Any (Action Model))
  arbitraryAction :: VarContext -> Model -> Gen (Any (Action Model))
arbitraryAction VarContext
_lookup Model{State
$sel:headState:Model :: Model -> State
headState :: State
headState, SnapshotNumber
$sel:currentSnapshotNumber:Model :: Model -> SnapshotNumber
currentSnapshotNumber :: SnapshotNumber
currentSnapshotNumber, [ModelSnapshot]
$sel:knownSnapshots:Model :: Model -> [ModelSnapshot]
knownSnapshots :: [ModelSnapshot]
knownSnapshots, SnapshotVersion
$sel:currentVersion:Model :: Model -> SnapshotVersion
currentVersion :: SnapshotVersion
currentVersion, ModelUTxO
$sel:utxoInHead:Model :: Model -> ModelUTxO
utxoInHead :: ModelUTxO
utxoInHead, ModelUTxO
$sel:pendingDeposit:Model :: Model -> ModelUTxO
pendingDeposit :: ModelUTxO
pendingDeposit, ModelUTxO
$sel:pendingDecommit:Model :: Model -> ModelUTxO
pendingDecommit :: ModelUTxO
pendingDecommit} =
    case State
headState of
      Open{} ->
        [(Int, Gen (Any (Action Model)))] -> Gen (Any (Action Model))
forall a. HasCallStack => [(Int, Gen a)] -> Gen a
frequency ([(Int, Gen (Any (Action Model)))] -> Gen (Any (Action Model)))
-> [(Int, Gen (Any (Action Model)))] -> Gen (Any (Action Model))
forall a b. (a -> b) -> a -> b
$
          [(Int
1, Action Model () -> Any (Action Model)
forall a (f :: * -> *). (Typeable a, Eq (f a)) => f a -> Any f
Some (Action Model () -> Any (Action Model))
-> (ModelSnapshot -> Action Model ())
-> ModelSnapshot
-> Any (Action Model)
forall b c a. (b -> c) -> (a -> b) -> a -> c
. ModelSnapshot -> Action Model ()
NewSnapshot (ModelSnapshot -> Any (Action Model))
-> Gen ModelSnapshot -> Gen (Any (Action Model))
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> Gen ModelSnapshot
genSnapshot)]
            [(Int, Gen (Any (Action Model)))]
-> [(Int, Gen (Any (Action Model)))]
-> [(Int, Gen (Any (Action Model)))]
forall a. Semigroup a => a -> a -> a
<> [ ( Int
2
                 , do
                     Actor
actor <- [Actor] -> Gen Actor
forall a. HasCallStack => [a] -> Gen a
elements [Actor]
allActors
                     ModelSnapshot
snapshot <- [ModelSnapshot] -> Gen ModelSnapshot
forall a. HasCallStack => [a] -> Gen a
elements [ModelSnapshot]
knownSnapshots
                     Any (Action Model) -> Gen (Any (Action Model))
forall a. a -> Gen a
forall (f :: * -> *) a. Applicative f => a -> f a
pure (Any (Action Model) -> Gen (Any (Action Model)))
-> Any (Action Model) -> Gen (Any (Action Model))
forall a b. (a -> b) -> a -> b
$ Action Model TxResult -> Any (Action Model)
forall a (f :: * -> *). (Typeable a, Eq (f a)) => f a -> Any f
Some Increment{Actor
$sel:actor:NewSnapshot :: Actor
actor :: Actor
actor, ModelSnapshot
$sel:snapshot:NewSnapshot :: ModelSnapshot
snapshot :: ModelSnapshot
snapshot}
                 )
               | Bool -> Bool
not ([ModelSnapshot] -> Bool
forall a. [a] -> Bool
forall (t :: * -> *) a. Foldable t => t a -> Bool
null [ModelSnapshot]
knownSnapshots) -- XXX: DRY this check
               ]
            [(Int, Gen (Any (Action Model)))]
-> [(Int, Gen (Any (Action Model)))]
-> [(Int, Gen (Any (Action Model)))]
forall a. Semigroup a => a -> a -> a
<> [ ( Int
5
                 , do
                     Actor
actor <- [Actor] -> Gen Actor
forall a. HasCallStack => [a] -> Gen a
elements [Actor]
allActors
                     ModelSnapshot
snapshot <- [ModelSnapshot] -> Gen ModelSnapshot
forall a. HasCallStack => [a] -> Gen a
elements [ModelSnapshot]
knownSnapshots
                     Any (Action Model) -> Gen (Any (Action Model))
forall a. a -> Gen a
forall (f :: * -> *) a. Applicative f => a -> f a
pure (Any (Action Model) -> Gen (Any (Action Model)))
-> Any (Action Model) -> Gen (Any (Action Model))
forall a b. (a -> b) -> a -> b
$ Action Model TxResult -> Any (Action Model)
forall a (f :: * -> *). (Typeable a, Eq (f a)) => f a -> Any f
Some Decrement{Actor
$sel:actor:NewSnapshot :: Actor
actor :: Actor
actor, ModelSnapshot
$sel:snapshot:NewSnapshot :: ModelSnapshot
snapshot :: ModelSnapshot
snapshot}
                 )
               | Bool -> Bool
not ([ModelSnapshot] -> Bool
forall a. [a] -> Bool
forall (t :: * -> *) a. Foldable t => t a -> Bool
null [ModelSnapshot]
knownSnapshots) -- XXX: DRY this check
               ]
            [(Int, Gen (Any (Action Model)))]
-> [(Int, Gen (Any (Action Model)))]
-> [(Int, Gen (Any (Action Model)))]
forall a. Semigroup a => a -> a -> a
<> [
                 ( Int
1
                 , do
                     ModelUTxO
toCommit <- Gen ModelUTxO
forall a. Arbitrary a => Gen a
arbitrary
                     Any (Action Model) -> Gen (Any (Action Model))
forall a. a -> Gen a
forall (f :: * -> *) a. Applicative f => a -> f a
pure (Any (Action Model) -> Gen (Any (Action Model)))
-> Any (Action Model) -> Gen (Any (Action Model))
forall a b. (a -> b) -> a -> b
$ Action Model TxResult -> Any (Action Model)
forall a (f :: * -> *). (Typeable a, Eq (f a)) => f a -> Any f
Some Deposit{$sel:utxoToDeposit:NewSnapshot :: ModelUTxO
utxoToDeposit = Int -> ModelUTxO -> ModelUTxO
forall a. Int -> [a] -> [a]
take Int
1 (ModelUTxO -> ModelUTxO) -> ModelUTxO -> ModelUTxO
forall a b. (a -> b) -> a -> b
$ ModelUTxO -> ModelUTxO
forall a. Eq a => [a] -> [a]
nub (ModelUTxO -> ModelUTxO) -> ModelUTxO -> ModelUTxO
forall a b. (a -> b) -> a -> b
$ (SingleUTxO -> Bool) -> ModelUTxO -> ModelUTxO
forall a. (a -> Bool) -> [a] -> [a]
filter (SingleUTxO -> ModelUTxO -> Bool
forall (f :: * -> *) a.
(Foldable f, DisallowElem f, Eq a) =>
a -> f a -> Bool
`notElem` ModelUTxO
utxoInHead) ModelUTxO
toCommit}
                 )
               ]
            [(Int, Gen (Any (Action Model)))]
-> [(Int, Gen (Any (Action Model)))]
-> [(Int, Gen (Any (Action Model)))]
forall a. Semigroup a => a -> a -> a
<> [ ( Int
5
                 , do
                     Actor
actor <- [Actor] -> Gen Actor
forall a. HasCallStack => [a] -> Gen a
elements [Actor]
allActors
                     ModelSnapshot
snapshot <- [ModelSnapshot] -> Gen ModelSnapshot
forall a. HasCallStack => [a] -> Gen a
elements [ModelSnapshot]
knownSnapshots
                     Any (Action Model) -> Gen (Any (Action Model))
forall a. a -> Gen a
forall (f :: * -> *) a. Applicative f => a -> f a
pure (Any (Action Model) -> Gen (Any (Action Model)))
-> Any (Action Model) -> Gen (Any (Action Model))
forall a b. (a -> b) -> a -> b
$ Action Model TxResult -> Any (Action Model)
forall a (f :: * -> *). (Typeable a, Eq (f a)) => f a -> Any f
Some (Action Model TxResult -> Any (Action Model))
-> Action Model TxResult -> Any (Action Model)
forall a b. (a -> b) -> a -> b
$ Close{Actor
$sel:actor:NewSnapshot :: Actor
actor :: Actor
actor, $sel:snapshot:NewSnapshot :: ModelSnapshot
snapshot = ModelSnapshot
snapshot}
                 )
               | Bool -> Bool
not ([ModelSnapshot] -> Bool
forall a. [a] -> Bool
forall (t :: * -> *) a. Foldable t => t a -> Bool
null [ModelSnapshot]
knownSnapshots)
               ]
            [(Int, Gen (Any (Action Model)))]
-> [(Int, Gen (Any (Action Model)))]
-> [(Int, Gen (Any (Action Model)))]
forall a. Semigroup a => a -> a -> a
<> [
                 ( Int
5
                 , do
                     Actor
actor <- [Actor] -> Gen Actor
forall a. HasCallStack => [a] -> Gen a
elements [Actor]
allActors
                     ModelSnapshot
snapshot <- Gen ModelSnapshot
genCloseWithDecrement
                     Any (Action Model) -> Gen (Any (Action Model))
forall a. a -> Gen a
forall (f :: * -> *) a. Applicative f => a -> f a
pure (Any (Action Model) -> Gen (Any (Action Model)))
-> Any (Action Model) -> Gen (Any (Action Model))
forall a b. (a -> b) -> a -> b
$ Action Model TxResult -> Any (Action Model)
forall a (f :: * -> *). (Typeable a, Eq (f a)) => f a -> Any f
Some (Action Model TxResult -> Any (Action Model))
-> Action Model TxResult -> Any (Action Model)
forall a b. (a -> b) -> a -> b
$ Close{Actor
$sel:actor:NewSnapshot :: Actor
actor :: Actor
actor, $sel:snapshot:NewSnapshot :: ModelSnapshot
snapshot = ModelSnapshot
snapshot}
                 )
               ]
      Closed{} ->
        [(Int, Gen (Any (Action Model)))] -> Gen (Any (Action Model))
forall a. HasCallStack => [(Int, Gen a)] -> Gen a
frequency ([(Int, Gen (Any (Action Model)))] -> Gen (Any (Action Model)))
-> [(Int, Gen (Any (Action Model)))] -> Gen (Any (Action Model))
forall a b. (a -> b) -> a -> b
$
          ( Int
5
          , do
              -- Fanout with the currently known model state.
              ModelUTxO
omegaUTxO <- [(Int, Gen ModelUTxO)] -> Gen ModelUTxO
forall a. HasCallStack => [(Int, Gen a)] -> Gen a
frequency [(Int
1, ModelUTxO -> Gen ModelUTxO
forall a. a -> Gen a
forall (f :: * -> *) a. Applicative f => a -> f a
pure ModelUTxO
pendingDecommit), (Int
1, ModelUTxO -> Gen ModelUTxO
forall a. a -> Gen a
forall (f :: * -> *) a. Applicative f => a -> f a
pure ModelUTxO
forall a. Monoid a => a
mempty), (Int
5, Gen ModelUTxO
forall a. Arbitrary a => Gen a
arbitrary)]
              SingleUTxO
alphaUTxO' <- [(Int, Gen SingleUTxO)] -> Gen SingleUTxO
forall a. HasCallStack => [(Int, Gen a)] -> Gen a
frequency [(Int
1, if ModelUTxO -> Bool
forall a. [a] -> Bool
forall (t :: * -> *) a. Foldable t => t a -> Bool
null ModelUTxO
pendingDeposit then Gen SingleUTxO
forall a. Arbitrary a => Gen a
arbitrary else ModelUTxO -> Gen SingleUTxO
forall a. HasCallStack => [a] -> Gen a
elements ModelUTxO
pendingDeposit), (Int
1, Gen SingleUTxO
forall a. Arbitrary a => Gen a
arbitrary)]
              Any (Action Model) -> Gen (Any (Action Model))
forall a. a -> Gen a
forall (f :: * -> *) a. Applicative f => a -> f a
pure (Any (Action Model) -> Gen (Any (Action Model)))
-> Any (Action Model) -> Gen (Any (Action Model))
forall a b. (a -> b) -> a -> b
$
                Action Model TxResult -> Any (Action Model)
forall a (f :: * -> *). (Typeable a, Eq (f a)) => f a -> Any f
Some (Action Model TxResult -> Any (Action Model))
-> Action Model TxResult -> Any (Action Model)
forall a b. (a -> b) -> a -> b
$
                  Fanout
                    { $sel:utxo:NewSnapshot :: ModelUTxO
utxo = ModelUTxO
utxoInHead
                    , $sel:alphaUTxO:NewSnapshot :: ModelUTxO
alphaUTxO = [SingleUTxO
alphaUTxO']
                    , ModelUTxO
$sel:omegaUTxO:NewSnapshot :: ModelUTxO
omegaUTxO :: ModelUTxO
omegaUTxO
                    }
          )
            (Int, Gen (Any (Action Model)))
-> [(Int, Gen (Any (Action Model)))]
-> [(Int, Gen (Any (Action Model)))]
forall a. a -> [a] -> [a]
: [ ( Int
5
                , do
                    Actor
actor <- [Actor] -> Gen Actor
forall a. HasCallStack => [a] -> Gen a
elements [Actor]
allActors
                    ModelSnapshot
snapshot <- [ModelSnapshot] -> Gen ModelSnapshot
forall a. HasCallStack => [a] -> Gen a
elements [ModelSnapshot]
knownSnapshots
                    Any (Action Model) -> Gen (Any (Action Model))
forall a. a -> Gen a
forall (f :: * -> *) a. Applicative f => a -> f a
pure (Any (Action Model) -> Gen (Any (Action Model)))
-> Any (Action Model) -> Gen (Any (Action Model))
forall a b. (a -> b) -> a -> b
$ Action Model TxResult -> Any (Action Model)
forall a (f :: * -> *). (Typeable a, Eq (f a)) => f a -> Any f
Some Contest{Actor
$sel:actor:NewSnapshot :: Actor
actor :: Actor
actor, ModelSnapshot
$sel:snapshot:NewSnapshot :: ModelSnapshot
snapshot :: ModelSnapshot
snapshot}
                )
              | Bool -> Bool
not ([ModelSnapshot] -> Bool
forall a. [a] -> Bool
forall (t :: * -> *) a. Foldable t => t a -> Bool
null [ModelSnapshot]
knownSnapshots)
              ]
              [(Int, Gen (Any (Action Model)))]
-> [(Int, Gen (Any (Action Model)))]
-> [(Int, Gen (Any (Action Model)))]
forall a. Semigroup a => a -> a -> a
<> [
                   ( Int
5
                   , do
                       Actor
actor <- [Actor] -> Gen Actor
forall a. HasCallStack => [a] -> Gen a
elements [Actor]
allActors
                       ModelSnapshot
snapshot <- Gen ModelSnapshot
genContest
                       Any (Action Model) -> Gen (Any (Action Model))
forall a. a -> Gen a
forall (f :: * -> *) a. Applicative f => a -> f a
pure (Any (Action Model) -> Gen (Any (Action Model)))
-> Any (Action Model) -> Gen (Any (Action Model))
forall a b. (a -> b) -> a -> b
$ Action Model TxResult -> Any (Action Model)
forall a (f :: * -> *). (Typeable a, Eq (f a)) => f a -> Any f
Some (Action Model TxResult -> Any (Action Model))
-> Action Model TxResult -> Any (Action Model)
forall a b. (a -> b) -> a -> b
$ Contest{Actor
$sel:actor:NewSnapshot :: Actor
actor :: Actor
actor, ModelSnapshot
$sel:snapshot:NewSnapshot :: ModelSnapshot
snapshot :: ModelSnapshot
snapshot}
                   )
                 ]
      State
Final -> Any (Action Model) -> Gen (Any (Action Model))
forall a. a -> Gen a
forall (f :: * -> *) a. Applicative f => a -> f a
pure (Any (Action Model) -> Gen (Any (Action Model)))
-> Any (Action Model) -> Gen (Any (Action Model))
forall a b. (a -> b) -> a -> b
$ Action Model () -> Any (Action Model)
forall a (f :: * -> *). (Typeable a, Eq (f a)) => f a -> Any f
Some Action Model ()
Stop
   where
    genContest :: Gen ModelSnapshot
genContest = do
      ModelSnapshot -> Gen ModelSnapshot
forall a. a -> Gen a
forall (f :: * -> *) a. Applicative f => a -> f a
pure
        ModelSnapshot
          { $sel:version:ModelSnapshot :: SnapshotVersion
version = SnapshotVersion
currentVersion
          , $sel:number:ModelSnapshot :: SnapshotNumber
number = [ModelSnapshot] -> SnapshotNumber
latestSnapshotNumber [ModelSnapshot]
knownSnapshots SnapshotNumber -> SnapshotNumber -> SnapshotNumber
forall a. Num a => a -> a -> a
+ SnapshotNumber
1
          , $sel:inHead:ModelSnapshot :: ModelUTxO
inHead = [(Int, Gen ModelUTxO)] -> Gen ModelUTxO
forall a. HasCallStack => [(Int, Gen a)] -> Gen a
frequency [(Int
1, ModelUTxO -> Gen ModelUTxO
forall a. a -> Gen a
forall (f :: * -> *) a. Applicative f => a -> f a
pure ModelUTxO
utxoInHead), (Int
3, ModelUTxO -> Gen ModelUTxO
forall a. a -> Gen a
forall (f :: * -> *) a. Applicative f => a -> f a
pure ModelUTxO
forall a. Monoid a => a
mempty)] Gen ModelUTxO -> Int -> ModelUTxO
forall a. Gen a -> Int -> a
`generateWith` Int
42
          , $sel:toCommit:ModelSnapshot :: ModelUTxO
toCommit = ModelUTxO
forall a. Monoid a => a
mempty
          , $sel:toDecommit:ModelSnapshot :: ModelUTxO
toDecommit = ModelUTxO
forall a. Monoid a => a
mempty
          }
    genCloseWithDecrement :: Gen ModelSnapshot
genCloseWithDecrement = do
      ModelSnapshot -> Gen ModelSnapshot
forall a. a -> Gen a
forall (f :: * -> *) a. Applicative f => a -> f a
pure
        ModelSnapshot
          { $sel:version:ModelSnapshot :: SnapshotVersion
version = SnapshotVersion
currentVersion SnapshotVersion -> SnapshotVersion -> SnapshotVersion
forall a. Num a => a -> a -> a
+ SnapshotVersion
1
          , $sel:number:ModelSnapshot :: SnapshotNumber
number = [ModelSnapshot] -> SnapshotNumber
latestSnapshotNumber [ModelSnapshot]
knownSnapshots SnapshotNumber -> SnapshotNumber -> SnapshotNumber
forall a. Num a => a -> a -> a
+ SnapshotNumber
1
          , $sel:inHead:ModelSnapshot :: ModelUTxO
inHead = ModelUTxO
utxoInHead
          , $sel:toCommit:ModelSnapshot :: ModelUTxO
toCommit = ModelUTxO
forall a. Monoid a => a
mempty
          , $sel:toDecommit:ModelSnapshot :: ModelUTxO
toDecommit = ModelUTxO
forall a. Monoid a => a
mempty
          }

    genSnapshot :: Gen ModelSnapshot
genSnapshot = do
      let defaultSnapshot :: ModelSnapshot
defaultSnapshot =
            ModelSnapshot
              { $sel:version:ModelSnapshot :: SnapshotVersion
version = SnapshotVersion
currentVersion
              , $sel:number:ModelSnapshot :: SnapshotNumber
number = [ModelSnapshot] -> SnapshotNumber
latestSnapshotNumber [ModelSnapshot]
knownSnapshots SnapshotNumber -> SnapshotNumber -> SnapshotNumber
forall a. Num a => a -> a -> a
+ SnapshotNumber
1
              , $sel:inHead:ModelSnapshot :: ModelUTxO
inHead = [(Int, Gen ModelUTxO)] -> Gen ModelUTxO
forall a. HasCallStack => [(Int, Gen a)] -> Gen a
frequency [(Int
1, ModelUTxO -> Gen ModelUTxO
forall a. a -> Gen a
forall (f :: * -> *) a. Applicative f => a -> f a
pure ModelUTxO
utxoInHead), (Int
3, ModelUTxO -> Gen ModelUTxO
forall a. a -> Gen a
forall (f :: * -> *) a. Applicative f => a -> f a
pure ModelUTxO
forall a. Monoid a => a
mempty)] Gen ModelUTxO -> Int -> ModelUTxO
forall a. Gen a -> Int -> a
`generateWith` Int
42
              , $sel:toCommit:ModelSnapshot :: ModelUTxO
toCommit = ModelUTxO
forall a. Monoid a => a
mempty
              , $sel:toDecommit:ModelSnapshot :: ModelUTxO
toDecommit = ModelUTxO
forall a. Monoid a => a
mempty
              }
      [(Int, Gen ModelSnapshot)] -> Gen ModelSnapshot
forall a. HasCallStack => [(Int, Gen a)] -> Gen a
frequency
        [ (Int
3, ModelSnapshot -> Gen ModelSnapshot
forall a. a -> Gen a
forall (f :: * -> *) a. Applicative f => a -> f a
pure ModelSnapshot
defaultSnapshot)
        , (Int
3, ModelSnapshot -> Gen ModelSnapshot
forall a. a -> Gen a
forall (f :: * -> *) a. Applicative f => a -> f a
pure (ModelSnapshot -> Gen ModelSnapshot)
-> ModelSnapshot -> Gen ModelSnapshot
forall a b. (a -> b) -> a -> b
$ ModelSnapshot
defaultSnapshot{version = currentVersion + 1, toCommit = nub $ filter (`notElem` utxoInHead) pendingDeposit})
        , if SnapshotNumber
currentSnapshotNumber SnapshotNumber -> SnapshotNumber -> Bool
forall a. Ord a => a -> a -> Bool
> SnapshotNumber
0
            then
              ( Int
3
              , do
                  let toDecommit' :: ModelUTxO
toDecommit' = Int -> ModelUTxO -> ModelUTxO
forall a. Int -> [a] -> [a]
take Int
1 ModelUTxO
utxoInHead
                  case ModelUTxO
toDecommit' of
                    [] -> ModelSnapshot -> Gen ModelSnapshot
forall a. a -> Gen a
forall (f :: * -> *) a. Applicative f => a -> f a
pure ModelSnapshot
defaultSnapshot
                    ModelUTxO
_ -> ModelSnapshot -> Gen ModelSnapshot
forall a. a -> Gen a
forall (f :: * -> *) a. Applicative f => a -> f a
pure (ModelSnapshot -> Gen ModelSnapshot)
-> ModelSnapshot -> Gen ModelSnapshot
forall a b. (a -> b) -> a -> b
$ ModelSnapshot
defaultSnapshot{version = currentVersion + 1, toDecommit = toDecommit'}
              )
            else (Int
3, ModelSnapshot -> Gen ModelSnapshot
forall a. a -> Gen a
forall (f :: * -> *) a. Applicative f => a -> f a
pure ModelSnapshot
defaultSnapshot)
        ]

  -- Determine actions we want to perform and expect to work. If this is False,
  -- validFailingAction is checked too.
  precondition :: Model -> Action Model a -> Bool
  precondition :: forall a. Model -> Action Model a -> Bool
precondition Model{State
$sel:headState:Model :: Model -> State
headState :: State
headState, [ModelSnapshot]
$sel:knownSnapshots:Model :: Model -> [ModelSnapshot]
knownSnapshots :: [ModelSnapshot]
knownSnapshots, SnapshotNumber
$sel:currentSnapshotNumber:Model :: Model -> SnapshotNumber
currentSnapshotNumber :: SnapshotNumber
currentSnapshotNumber, SnapshotNumber
$sel:closedSnapshotNumber:Model :: Model -> SnapshotNumber
closedSnapshotNumber :: SnapshotNumber
closedSnapshotNumber, [Actor]
$sel:alreadyContested:Model :: Model -> [Actor]
alreadyContested :: [Actor]
alreadyContested, SnapshotVersion
$sel:currentVersion:Model :: Model -> SnapshotVersion
currentVersion :: SnapshotVersion
currentVersion, ModelUTxO
$sel:pendingDeposit:Model :: Model -> ModelUTxO
pendingDeposit :: ModelUTxO
pendingDeposit, ModelUTxO
$sel:pendingDecommit:Model :: Model -> ModelUTxO
pendingDecommit :: ModelUTxO
pendingDecommit} = \case
    Action Model a
R:ActionModela a
Stop -> State
headState State -> State -> Bool
forall a. Eq a => a -> a -> Bool
/= State
Final
    NewSnapshot{ModelSnapshot
$sel:newSnapshot:NewSnapshot :: Action Model () -> ModelSnapshot
newSnapshot :: ModelSnapshot
newSnapshot} ->
      (ModelSnapshot
newSnapshot.version SnapshotVersion -> SnapshotVersion -> Bool
forall a. Eq a => a -> a -> Bool
== SnapshotVersion
currentVersion Bool -> Bool -> Bool
|| ModelSnapshot
newSnapshot.version SnapshotVersion -> SnapshotVersion -> Bool
forall a. Eq a => a -> a -> Bool
== SnapshotVersion
currentVersion SnapshotVersion -> SnapshotVersion -> SnapshotVersion
forall a. Num a => a -> a -> a
+ SnapshotVersion
1)
        Bool -> Bool -> Bool
&& ModelSnapshot
newSnapshot.number SnapshotNumber -> SnapshotNumber -> Bool
forall a. Ord a => a -> a -> Bool
> [ModelSnapshot] -> SnapshotNumber
latestSnapshotNumber [ModelSnapshot]
knownSnapshots
    Deposit{ModelUTxO
$sel:utxoToDeposit:NewSnapshot :: Action Model TxResult -> ModelUTxO
utxoToDeposit :: ModelUTxO
utxoToDeposit} ->
      State
headState State -> State -> Bool
forall a. Eq a => a -> a -> Bool
== State
Open
        Bool -> Bool -> Bool
&& ModelUTxO
utxoToDeposit ModelUTxO -> ModelUTxO -> Bool
forall a. Eq a => a -> a -> Bool
/= ModelUTxO
forall a. Monoid a => a
mempty
        Bool -> Bool -> Bool
&& SnapshotNumber
currentSnapshotNumber SnapshotNumber -> SnapshotNumber -> Bool
forall a. Ord a => a -> a -> Bool
> SnapshotNumber
0
    Increment{ModelSnapshot
$sel:snapshot:NewSnapshot :: Action Model TxResult -> ModelSnapshot
snapshot :: ModelSnapshot
snapshot} ->
      State
headState State -> State -> Bool
forall a. Eq a => a -> a -> Bool
== State
Open
        Bool -> Bool -> Bool
&& ModelSnapshot
snapshot ModelSnapshot -> [ModelSnapshot] -> Bool
forall (f :: * -> *) a.
(Foldable f, DisallowElem f, Eq a) =>
a -> f a -> Bool
`elem` [ModelSnapshot]
knownSnapshots
        Bool -> Bool -> Bool
&& ModelUTxO
pendingDeposit ModelUTxO -> ModelUTxO -> Bool
forall a. Eq a => a -> a -> Bool
/= ModelUTxO
forall a. Monoid a => a
mempty
        Bool -> Bool -> Bool
&& ModelSnapshot
snapshot.toCommit ModelUTxO -> ModelUTxO -> Bool
forall a. Eq a => a -> a -> Bool
== ModelUTxO
pendingDeposit
        Bool -> Bool -> Bool
&& ModelSnapshot
snapshot.version SnapshotVersion -> SnapshotVersion -> Bool
forall a. Eq a => a -> a -> Bool
== SnapshotVersion
currentVersion
        Bool -> Bool -> Bool
&& SnapshotNumber
currentSnapshotNumber SnapshotNumber -> SnapshotNumber -> Bool
forall a. Ord a => a -> a -> Bool
> SnapshotNumber
0
    Decrement{ModelSnapshot
$sel:snapshot:NewSnapshot :: Action Model TxResult -> ModelSnapshot
snapshot :: ModelSnapshot
snapshot} ->
      State
headState State -> State -> Bool
forall a. Eq a => a -> a -> Bool
== State
Open
        Bool -> Bool -> Bool
&& ModelSnapshot
snapshot ModelSnapshot -> [ModelSnapshot] -> Bool
forall (f :: * -> *) a.
(Foldable f, DisallowElem f, Eq a) =>
a -> f a -> Bool
`elem` [ModelSnapshot]
knownSnapshots
        Bool -> Bool -> Bool
&& ModelSnapshot
snapshot.version SnapshotVersion -> SnapshotVersion -> Bool
forall a. Eq a => a -> a -> Bool
== SnapshotVersion
currentVersion
        Bool -> Bool -> Bool
&& ModelUTxO
pendingDecommit ModelUTxO -> ModelUTxO -> Bool
forall a. Eq a => a -> a -> Bool
/= ModelUTxO
forall a. Monoid a => a
mempty
        Bool -> Bool -> Bool
&& ModelSnapshot
snapshot.toDecommit ModelUTxO -> ModelUTxO -> Bool
forall a. Eq a => a -> a -> Bool
== ModelUTxO
pendingDecommit
        Bool -> Bool -> Bool
&& SnapshotNumber
currentSnapshotNumber SnapshotNumber -> SnapshotNumber -> Bool
forall a. Ord a => a -> a -> Bool
> SnapshotNumber
0
    Close{ModelSnapshot
$sel:snapshot:NewSnapshot :: Action Model TxResult -> ModelSnapshot
snapshot :: ModelSnapshot
snapshot} ->
      State
headState State -> State -> Bool
forall a. Eq a => a -> a -> Bool
== State
Open
        Bool -> Bool -> Bool
&& ModelSnapshot
snapshot ModelSnapshot -> [ModelSnapshot] -> Bool
forall (f :: * -> *) a.
(Foldable f, DisallowElem f, Eq a) =>
a -> f a -> Bool
`elem` [ModelSnapshot]
knownSnapshots
        Bool -> Bool -> Bool
&& (ModelUTxO
pendingDeposit ModelUTxO -> ModelUTxO -> Bool
forall a. Eq a => a -> a -> Bool
== ModelSnapshot
snapshot.toCommit Bool -> Bool -> Bool
&& ModelUTxO
pendingDecommit ModelUTxO -> ModelUTxO -> Bool
forall a. Eq a => a -> a -> Bool
== ModelSnapshot
snapshot.toDecommit)
        Bool -> Bool -> Bool
&& (if ModelSnapshot
snapshot.version SnapshotVersion -> SnapshotVersion -> Bool
forall a. Eq a => a -> a -> Bool
== SnapshotVersion
currentVersion then ModelSnapshot
snapshot.toCommit ModelUTxO -> ModelUTxO -> Bool
forall a. Eq a => a -> a -> Bool
== ModelUTxO
forall a. Monoid a => a
mempty Bool -> Bool -> Bool
&& ModelSnapshot
snapshot.toDecommit ModelUTxO -> ModelUTxO -> Bool
forall a. Eq a => a -> a -> Bool
== ModelUTxO
forall a. Monoid a => a
mempty else ModelSnapshot
snapshot.toCommit ModelUTxO -> ModelUTxO -> Bool
forall a. Eq a => a -> a -> Bool
/= ModelUTxO
forall a. Monoid a => a
mempty Bool -> Bool -> Bool
|| ModelSnapshot
snapshot.toDecommit ModelUTxO -> ModelUTxO -> Bool
forall a. Eq a => a -> a -> Bool
/= ModelUTxO
forall a. Monoid a => a
mempty)
        Bool -> Bool -> Bool
&& ( if ModelSnapshot
snapshot.number SnapshotNumber -> SnapshotNumber -> Bool
forall a. Eq a => a -> a -> Bool
== SnapshotNumber
0
               then ModelSnapshot
snapshot.inHead ModelUTxO -> ModelUTxO -> Bool
forall a. Eq a => a -> a -> Bool
== ModelUTxO
initialUTxOInHead
               else
                 ModelSnapshot
snapshot.version SnapshotVersion -> [SnapshotVersion] -> Bool
forall (f :: * -> *) a.
(Foldable f, DisallowElem f, Eq a) =>
a -> f a -> Bool
`elem` (SnapshotVersion
currentVersion SnapshotVersion -> [SnapshotVersion] -> [SnapshotVersion]
forall a. a -> [a] -> [a]
: [SnapshotVersion
currentVersion SnapshotVersion -> SnapshotVersion -> SnapshotVersion
forall a. Num a => a -> a -> a
- SnapshotVersion
1 | SnapshotVersion
currentVersion SnapshotVersion -> SnapshotVersion -> Bool
forall a. Ord a => a -> a -> Bool
> SnapshotVersion
0])
           )
     where
      Model{$sel:utxoInHead:Model :: Model -> ModelUTxO
utxoInHead = ModelUTxO
initialUTxOInHead} = Model
forall state. StateModel state => state
initialState
    Contest{Actor
$sel:actor:NewSnapshot :: Action Model TxResult -> Actor
actor :: Actor
actor, ModelSnapshot
$sel:snapshot:NewSnapshot :: Action Model TxResult -> ModelSnapshot
snapshot :: ModelSnapshot
snapshot} ->
      State
headState State -> State -> Bool
forall a. Eq a => a -> a -> Bool
== State
Closed
        Bool -> Bool -> Bool
&& ((ModelSnapshot
snapshot.version SnapshotVersion -> SnapshotVersion -> Bool
forall a. Eq a => a -> a -> Bool
== SnapshotVersion
currentVersion) Bool -> Bool -> Bool
&& (ModelSnapshot
snapshot.toCommit ModelUTxO -> ModelUTxO -> Bool
forall a. Eq a => a -> a -> Bool
== ModelUTxO
forall a. Monoid a => a
mempty Bool -> Bool -> Bool
&& ModelSnapshot
snapshot.toDecommit ModelUTxO -> ModelUTxO -> Bool
forall a. Eq a => a -> a -> Bool
== ModelUTxO
forall a. Monoid a => a
mempty))
        Bool -> Bool -> Bool
&& ModelSnapshot
snapshot.number SnapshotNumber -> SnapshotNumber -> Bool
forall a. Ord a => a -> a -> Bool
> SnapshotNumber
closedSnapshotNumber
        Bool -> Bool -> Bool
&& ModelSnapshot
snapshot.number SnapshotNumber -> SnapshotNumber -> Bool
forall a. Ord a => a -> a -> Bool
> SnapshotNumber
currentSnapshotNumber
        Bool -> Bool -> Bool
&& Actor
actor Actor -> [Actor] -> Bool
forall (f :: * -> *) a.
(Foldable f, DisallowElem f, Eq a) =>
a -> f a -> Bool
`notElem` [Actor]
alreadyContested
    Fanout{ModelUTxO
$sel:alphaUTxO:NewSnapshot :: Action Model TxResult -> ModelUTxO
alphaUTxO :: ModelUTxO
alphaUTxO, ModelUTxO
$sel:omegaUTxO:NewSnapshot :: Action Model TxResult -> ModelUTxO
omegaUTxO :: ModelUTxO
omegaUTxO} ->
      (ModelUTxO
alphaUTxO ModelUTxO -> ModelUTxO -> Bool
forall a. Eq a => a -> a -> Bool
== ModelUTxO
forall a. Monoid a => a
mempty Bool -> Bool -> Bool
|| ModelUTxO
omegaUTxO ModelUTxO -> ModelUTxO -> Bool
forall a. Eq a => a -> a -> Bool
== ModelUTxO
forall a. Monoid a => a
mempty)
        Bool -> Bool -> Bool
&& State
headState State -> State -> Bool
forall a. Eq a => a -> a -> Bool
== State
Closed

  -- Determine actions we want to perform and want to see failing. If this is
  -- False, the action is discarded (e.g. it's invalid or we don't want to see
  -- it tried to perform).
  validFailingAction :: Model -> Action Model a -> Bool
  validFailingAction :: forall a. Model -> Action Model a -> Bool
validFailingAction Model{State
$sel:headState:Model :: Model -> State
headState :: State
headState, SnapshotNumber
$sel:currentSnapshotNumber:Model :: Model -> SnapshotNumber
currentSnapshotNumber :: SnapshotNumber
currentSnapshotNumber, SnapshotNumber
$sel:closedSnapshotNumber:Model :: Model -> SnapshotNumber
closedSnapshotNumber :: SnapshotNumber
closedSnapshotNumber, [Actor]
$sel:alreadyContested:Model :: Model -> [Actor]
alreadyContested :: [Actor]
alreadyContested, [ModelSnapshot]
$sel:knownSnapshots:Model :: Model -> [ModelSnapshot]
knownSnapshots :: [ModelSnapshot]
knownSnapshots, SnapshotVersion
$sel:currentVersion:Model :: Model -> SnapshotVersion
currentVersion :: SnapshotVersion
currentVersion, ModelUTxO
$sel:pendingDeposit:Model :: Model -> ModelUTxO
pendingDeposit :: ModelUTxO
pendingDeposit, ModelUTxO
$sel:pendingDecommit:Model :: Model -> ModelUTxO
pendingDecommit :: ModelUTxO
pendingDecommit} = \case
    Action Model a
R:ActionModela a
Stop -> Bool
False
    NewSnapshot{} -> Bool
False
    Deposit{ModelUTxO
$sel:utxoToDeposit:NewSnapshot :: Action Model TxResult -> ModelUTxO
utxoToDeposit :: ModelUTxO
utxoToDeposit} ->
      State
headState State -> State -> Bool
forall a. Eq a => a -> a -> Bool
== State
Open
        Bool -> Bool -> Bool
&& ModelUTxO
utxoToDeposit ModelUTxO -> ModelUTxO -> Bool
forall a. Eq a => a -> a -> Bool
/= ModelUTxO
forall a. Monoid a => a
mempty
        Bool -> Bool -> Bool
&& ModelUTxO
pendingDeposit ModelUTxO -> ModelUTxO -> Bool
forall a. Eq a => a -> a -> Bool
== ModelUTxO
forall a. Monoid a => a
mempty
        Bool -> Bool -> Bool
&& ModelUTxO
pendingDecommit ModelUTxO -> ModelUTxO -> Bool
forall a. Eq a => a -> a -> Bool
/= ModelUTxO
forall a. Monoid a => a
mempty
        Bool -> Bool -> Bool
&& SnapshotNumber
currentSnapshotNumber SnapshotNumber -> SnapshotNumber -> Bool
forall a. Ord a => a -> a -> Bool
> SnapshotNumber
0
    Increment{ModelSnapshot
$sel:snapshot:NewSnapshot :: Action Model TxResult -> ModelSnapshot
snapshot :: ModelSnapshot
snapshot} ->
      State
headState State -> State -> Bool
forall a. Eq a => a -> a -> Bool
== State
Open
        Bool -> Bool -> Bool
&& ModelSnapshot
snapshot ModelSnapshot -> [ModelSnapshot] -> Bool
forall (f :: * -> *) a.
(Foldable f, DisallowElem f, Eq a) =>
a -> f a -> Bool
`elem` [ModelSnapshot]
knownSnapshots
        Bool -> Bool -> Bool
&& ModelUTxO
pendingDeposit ModelUTxO -> ModelUTxO -> Bool
forall a. Eq a => a -> a -> Bool
/= ModelUTxO
forall a. Monoid a => a
mempty
        Bool -> Bool -> Bool
&& ModelSnapshot
snapshot.toCommit ModelUTxO -> ModelUTxO -> Bool
forall a. Eq a => a -> a -> Bool
== ModelUTxO
pendingDeposit
        Bool -> Bool -> Bool
&& SnapshotNumber
currentSnapshotNumber SnapshotNumber -> SnapshotNumber -> Bool
forall a. Ord a => a -> a -> Bool
> SnapshotNumber
0
    -- Only filter non-matching states as we are not interested in these kind of
    -- verification failures.
    Decrement{ModelSnapshot
$sel:snapshot:NewSnapshot :: Action Model TxResult -> ModelSnapshot
snapshot :: ModelSnapshot
snapshot} ->
      State
headState State -> State -> Bool
forall a. Eq a => a -> a -> Bool
== State
Open
        Bool -> Bool -> Bool
&& ModelSnapshot
snapshot ModelSnapshot -> [ModelSnapshot] -> Bool
forall (f :: * -> *) a.
(Foldable f, DisallowElem f, Eq a) =>
a -> f a -> Bool
`elem` [ModelSnapshot]
knownSnapshots
        Bool -> Bool -> Bool
&& ModelSnapshot
snapshot.version SnapshotVersion -> SnapshotVersion -> Bool
forall a. Eq a => a -> a -> Bool
== SnapshotVersion
currentVersion
        Bool -> Bool -> Bool
&& Bool -> Bool
not (ModelUTxO -> Bool
forall a. [a] -> Bool
forall (t :: * -> *) a. Foldable t => t a -> Bool
null ModelSnapshot
snapshot.toDecommit)
        Bool -> Bool -> Bool
&& ModelSnapshot
snapshot.toDecommit ModelUTxO -> ModelUTxO -> Bool
forall a. Eq a => a -> a -> Bool
== ModelUTxO
pendingDecommit
        Bool -> Bool -> Bool
&& SnapshotNumber
currentSnapshotNumber SnapshotNumber -> SnapshotNumber -> Bool
forall a. Ord a => a -> a -> Bool
> SnapshotNumber
0
    Close{ModelSnapshot
$sel:snapshot:NewSnapshot :: Action Model TxResult -> ModelSnapshot
snapshot :: ModelSnapshot
snapshot} ->
      State
headState State -> State -> Bool
forall a. Eq a => a -> a -> Bool
== State
Open
        Bool -> Bool -> Bool
&& ModelSnapshot
snapshot ModelSnapshot -> [ModelSnapshot] -> Bool
forall (f :: * -> *) a.
(Foldable f, DisallowElem f, Eq a) =>
a -> f a -> Bool
`elem` [ModelSnapshot]
knownSnapshots
        Bool -> Bool -> Bool
&& (ModelUTxO
pendingDeposit ModelUTxO -> ModelUTxO -> Bool
forall a. Eq a => a -> a -> Bool
== ModelSnapshot
snapshot.toCommit Bool -> Bool -> Bool
&& ModelUTxO
pendingDecommit ModelUTxO -> ModelUTxO -> Bool
forall a. Eq a => a -> a -> Bool
== ModelSnapshot
snapshot.toDecommit)
        Bool -> Bool -> Bool
&& (if ModelSnapshot
snapshot.version SnapshotVersion -> SnapshotVersion -> Bool
forall a. Eq a => a -> a -> Bool
== SnapshotVersion
currentVersion then ModelSnapshot
snapshot.toCommit ModelUTxO -> ModelUTxO -> Bool
forall a. Eq a => a -> a -> Bool
== ModelUTxO
forall a. Monoid a => a
mempty Bool -> Bool -> Bool
&& ModelSnapshot
snapshot.toDecommit ModelUTxO -> ModelUTxO -> Bool
forall a. Eq a => a -> a -> Bool
== ModelUTxO
forall a. Monoid a => a
mempty else ModelSnapshot
snapshot.toCommit ModelUTxO -> ModelUTxO -> Bool
forall a. Eq a => a -> a -> Bool
/= ModelUTxO
forall a. Monoid a => a
mempty Bool -> Bool -> Bool
|| ModelSnapshot
snapshot.toDecommit ModelUTxO -> ModelUTxO -> Bool
forall a. Eq a => a -> a -> Bool
/= ModelUTxO
forall a. Monoid a => a
mempty)
        Bool -> Bool -> Bool
&& ( if ModelSnapshot
snapshot.number SnapshotNumber -> SnapshotNumber -> Bool
forall a. Eq a => a -> a -> Bool
== SnapshotNumber
0
               then ModelSnapshot
snapshot.inHead ModelUTxO -> ModelUTxO -> Bool
forall a. Eq a => a -> a -> Bool
== ModelUTxO
initialUTxOInHead
               else
                 ModelSnapshot
snapshot.version SnapshotVersion -> [SnapshotVersion] -> Bool
forall (f :: * -> *) a.
(Foldable f, DisallowElem f, Eq a) =>
a -> f a -> Bool
`elem` (SnapshotVersion
currentVersion SnapshotVersion -> [SnapshotVersion] -> [SnapshotVersion]
forall a. a -> [a] -> [a]
: [SnapshotVersion
currentVersion SnapshotVersion -> SnapshotVersion -> SnapshotVersion
forall a. Num a => a -> a -> a
- SnapshotVersion
1 | SnapshotVersion
currentVersion SnapshotVersion -> SnapshotVersion -> Bool
forall a. Ord a => a -> a -> Bool
> SnapshotVersion
0])
           )
     where
      Model{$sel:utxoInHead:Model :: Model -> ModelUTxO
utxoInHead = ModelUTxO
initialUTxOInHead} = Model
forall state. StateModel state => state
initialState
    Contest{Actor
$sel:actor:NewSnapshot :: Action Model TxResult -> Actor
actor :: Actor
actor, ModelSnapshot
$sel:snapshot:NewSnapshot :: Action Model TxResult -> ModelSnapshot
snapshot :: ModelSnapshot
snapshot} ->
      State
headState State -> State -> Bool
forall a. Eq a => a -> a -> Bool
== State
Closed
        Bool -> Bool -> Bool
&& ((ModelSnapshot
snapshot.version SnapshotVersion -> SnapshotVersion -> Bool
forall a. Eq a => a -> a -> Bool
== SnapshotVersion
currentVersion) Bool -> Bool -> Bool
&& (ModelSnapshot
snapshot.toCommit ModelUTxO -> ModelUTxO -> Bool
forall a. Eq a => a -> a -> Bool
== ModelUTxO
forall a. Monoid a => a
mempty Bool -> Bool -> Bool
&& ModelSnapshot
snapshot.toDecommit ModelUTxO -> ModelUTxO -> Bool
forall a. Eq a => a -> a -> Bool
== ModelUTxO
forall a. Monoid a => a
mempty))
        Bool -> Bool -> Bool
&& ModelSnapshot
snapshot.number SnapshotNumber -> SnapshotNumber -> Bool
forall a. Ord a => a -> a -> Bool
> SnapshotNumber
closedSnapshotNumber
        Bool -> Bool -> Bool
&& ModelSnapshot
snapshot.number SnapshotNumber -> SnapshotNumber -> Bool
forall a. Ord a => a -> a -> Bool
> SnapshotNumber
currentSnapshotNumber
        Bool -> Bool -> Bool
&& Actor
actor Actor -> [Actor] -> Bool
forall (f :: * -> *) a.
(Foldable f, DisallowElem f, Eq a) =>
a -> f a -> Bool
`notElem` [Actor]
alreadyContested
    Fanout{} ->
      State
headState State -> State -> Bool
forall a. Eq a => a -> a -> Bool
== State
Closed

  nextState :: Model -> Action Model a -> Var a -> Model
  nextState :: forall a. Model -> Action Model a -> Var a -> Model
nextState m :: Model
m@Model{} Action Model a
t Var a
_result =
    case Action Model a
t of
      Action Model a
R:ActionModela a
Stop -> Model
m
      NewSnapshot{ModelSnapshot
$sel:newSnapshot:NewSnapshot :: Action Model () -> ModelSnapshot
newSnapshot :: ModelSnapshot
newSnapshot} ->
        Model
m
          { knownSnapshots = nub $ newSnapshot : m.knownSnapshots
          , pendingDecommit = newSnapshot.toDecommit
          , currentSnapshotNumber = newSnapshot.number
          }
      Deposit{ModelUTxO
$sel:utxoToDeposit:NewSnapshot :: Action Model TxResult -> ModelUTxO
utxoToDeposit :: ModelUTxO
utxoToDeposit} ->
        Model
m
          { headState = Open
          , pendingDeposit = utxoToDeposit
          }
      Increment{ModelSnapshot
$sel:snapshot:NewSnapshot :: Action Model TxResult -> ModelSnapshot
snapshot :: ModelSnapshot
snapshot} ->
        Model
m
          { headState = Open
          , currentVersion = snapshot.version
          , utxoInHead = m.utxoInHead <> snapshot.toCommit
          , pendingDeposit = mempty
          , currentSnapshotNumber = snapshot.number
          }
      Decrement{ModelSnapshot
$sel:snapshot:NewSnapshot :: Action Model TxResult -> ModelSnapshot
snapshot :: ModelSnapshot
snapshot} ->
        Model
m
          { headState = Open
          , currentVersion = snapshot.version
          , utxoInHead = m.utxoInHead \\ snapshot.toDecommit
          , pendingDecommit = mempty
          , currentSnapshotNumber = snapshot.number
          }
      Close{ModelSnapshot
$sel:snapshot:NewSnapshot :: Action Model TxResult -> ModelSnapshot
snapshot :: ModelSnapshot
snapshot} ->
        Model
m
          { headState = Closed
          , currentVersion = snapshot.version
          , closedSnapshotNumber = snapshot.number
          , currentSnapshotNumber = snapshot.number
          , alreadyContested = []
          }
      Contest{Actor
$sel:actor:NewSnapshot :: Action Model TxResult -> Actor
actor :: Actor
actor, ModelSnapshot
$sel:snapshot:NewSnapshot :: Action Model TxResult -> ModelSnapshot
snapshot :: ModelSnapshot
snapshot} ->
        Model
m
          { headState = Closed
          , alreadyContested = actor : alreadyContested m
          , currentSnapshotNumber = snapshot.number
          }
      Fanout{} -> Model
m{headState = Final}

instance HasVariables Model where
  getAllVariables :: Model -> Set (Any Var)
getAllVariables = Model -> Set (Any Var)
forall a. Monoid a => a
mempty

instance HasVariables (Action Model a) where
  getAllVariables :: Action Model a -> Set (Any Var)
getAllVariables = Action Model a -> Set (Any Var)
forall a. Monoid a => a
mempty

deriving instance Eq (Action Model a)
deriving instance Show (Action Model a)

-- * ============================== REAL WORLD ==========================

-- | Application monad to perform model actions. Currently it only keeps a
-- 'UTxO' which is updated whenever transactions are valid in 'performTx'.
newtype AppM a = AppM {forall a. AppM a -> ReaderT (IORef (Maybe TxId, UTxO)) IO a
runAppM :: ReaderT (IORef (Maybe TxId, UTxO)) IO a}
  deriving newtype ((forall a b. (a -> b) -> AppM a -> AppM b)
-> (forall a b. a -> AppM b -> AppM a) -> Functor AppM
forall a b. a -> AppM b -> AppM a
forall a b. (a -> b) -> AppM a -> AppM b
forall (f :: * -> *).
(forall a b. (a -> b) -> f a -> f b)
-> (forall a b. a -> f b -> f a) -> Functor f
$cfmap :: forall a b. (a -> b) -> AppM a -> AppM b
fmap :: forall a b. (a -> b) -> AppM a -> AppM b
$c<$ :: forall a b. a -> AppM b -> AppM a
<$ :: forall a b. a -> AppM b -> AppM a
Functor, Functor AppM
Functor AppM =>
(forall a. a -> AppM a)
-> (forall a b. AppM (a -> b) -> AppM a -> AppM b)
-> (forall a b c. (a -> b -> c) -> AppM a -> AppM b -> AppM c)
-> (forall a b. AppM a -> AppM b -> AppM b)
-> (forall a b. AppM a -> AppM b -> AppM a)
-> Applicative AppM
forall a. a -> AppM a
forall a b. AppM a -> AppM b -> AppM a
forall a b. AppM a -> AppM b -> AppM b
forall a b. AppM (a -> b) -> AppM a -> AppM b
forall a b c. (a -> b -> c) -> AppM a -> AppM b -> AppM c
forall (f :: * -> *).
Functor f =>
(forall a. a -> f a)
-> (forall a b. f (a -> b) -> f a -> f b)
-> (forall a b c. (a -> b -> c) -> f a -> f b -> f c)
-> (forall a b. f a -> f b -> f b)
-> (forall a b. f a -> f b -> f a)
-> Applicative f
$cpure :: forall a. a -> AppM a
pure :: forall a. a -> AppM a
$c<*> :: forall a b. AppM (a -> b) -> AppM a -> AppM b
<*> :: forall a b. AppM (a -> b) -> AppM a -> AppM b
$cliftA2 :: forall a b c. (a -> b -> c) -> AppM a -> AppM b -> AppM c
liftA2 :: forall a b c. (a -> b -> c) -> AppM a -> AppM b -> AppM c
$c*> :: forall a b. AppM a -> AppM b -> AppM b
*> :: forall a b. AppM a -> AppM b -> AppM b
$c<* :: forall a b. AppM a -> AppM b -> AppM a
<* :: forall a b. AppM a -> AppM b -> AppM a
Applicative, Applicative AppM
Applicative AppM =>
(forall a b. AppM a -> (a -> AppM b) -> AppM b)
-> (forall a b. AppM a -> AppM b -> AppM b)
-> (forall a. a -> AppM a)
-> Monad AppM
forall a. a -> AppM a
forall a b. AppM a -> AppM b -> AppM b
forall a b. AppM a -> (a -> AppM b) -> AppM b
forall (m :: * -> *).
Applicative m =>
(forall a b. m a -> (a -> m b) -> m b)
-> (forall a b. m a -> m b -> m b)
-> (forall a. a -> m a)
-> Monad m
$c>>= :: forall a b. AppM a -> (a -> AppM b) -> AppM b
>>= :: forall a b. AppM a -> (a -> AppM b) -> AppM b
$c>> :: forall a b. AppM a -> AppM b -> AppM b
>> :: forall a b. AppM a -> AppM b -> AppM b
$creturn :: forall a. a -> AppM a
return :: forall a. a -> AppM a
Monad, Monad AppM
Monad AppM => (forall a. IO a -> AppM a) -> MonadIO AppM
forall a. IO a -> AppM a
forall (m :: * -> *).
Monad m =>
(forall a. IO a -> m a) -> MonadIO m
$cliftIO :: forall a. IO a -> AppM a
liftIO :: forall a. IO a -> AppM a
MonadIO, Monad AppM
Monad AppM => (forall a. String -> AppM a) -> MonadFail AppM
forall a. String -> AppM a
forall (m :: * -> *).
Monad m =>
(forall a. String -> m a) -> MonadFail m
$cfail :: forall a. String -> AppM a
fail :: forall a. String -> AppM a
MonadFail, Monad AppM
Monad AppM =>
(forall e a. Exception e => e -> AppM a)
-> (forall a b c.
    AppM a -> (a -> AppM b) -> (a -> AppM c) -> AppM c)
-> (forall a b c. AppM a -> AppM b -> AppM c -> AppM c)
-> (forall a b. AppM a -> AppM b -> AppM a)
-> MonadThrow AppM
forall e a. Exception e => e -> AppM a
forall a b. AppM a -> AppM b -> AppM a
forall a b c. AppM a -> AppM b -> AppM c -> AppM c
forall a b c. AppM a -> (a -> AppM b) -> (a -> AppM c) -> AppM c
forall (m :: * -> *).
Monad m =>
(forall e a. Exception e => e -> m a)
-> (forall a b c. m a -> (a -> m b) -> (a -> m c) -> m c)
-> (forall a b c. m a -> m b -> m c -> m c)
-> (forall a b. m a -> m b -> m a)
-> MonadThrow m
$cthrowIO :: forall e a. Exception e => e -> AppM a
throwIO :: forall e a. Exception e => e -> AppM a
$cbracket :: forall a b c. AppM a -> (a -> AppM b) -> (a -> AppM c) -> AppM c
bracket :: forall a b c. AppM a -> (a -> AppM b) -> (a -> AppM c) -> AppM c
$cbracket_ :: forall a b c. AppM a -> AppM b -> AppM c -> AppM c
bracket_ :: forall a b c. AppM a -> AppM b -> AppM c -> AppM c
$cfinally :: forall a b. AppM a -> AppM b -> AppM a
finally :: forall a b. AppM a -> AppM b -> AppM a
MonadThrow)

instance MonadReader (Maybe TxId, UTxO) AppM where
  ask :: AppM (Maybe TxId, UTxO)
ask = ReaderT (IORef (Maybe TxId, UTxO)) IO (Maybe TxId, UTxO)
-> AppM (Maybe TxId, UTxO)
forall a. ReaderT (IORef (Maybe TxId, UTxO)) IO a -> AppM a
AppM (ReaderT (IORef (Maybe TxId, UTxO)) IO (Maybe TxId, UTxO)
 -> AppM (Maybe TxId, UTxO))
-> ReaderT (IORef (Maybe TxId, UTxO)) IO (Maybe TxId, UTxO)
-> AppM (Maybe TxId, UTxO)
forall a b. (a -> b) -> a -> b
$ ReaderT (IORef (Maybe TxId, UTxO)) IO (IORef (Maybe TxId, UTxO))
forall r (m :: * -> *). MonadReader r m => m r
ask ReaderT (IORef (Maybe TxId, UTxO)) IO (IORef (Maybe TxId, UTxO))
-> (IORef (Maybe TxId, UTxO)
    -> ReaderT (IORef (Maybe TxId, UTxO)) IO (Maybe TxId, UTxO))
-> ReaderT (IORef (Maybe TxId, UTxO)) IO (Maybe TxId, UTxO)
forall a b.
ReaderT (IORef (Maybe TxId, UTxO)) IO a
-> (a -> ReaderT (IORef (Maybe TxId, UTxO)) IO b)
-> ReaderT (IORef (Maybe TxId, UTxO)) IO b
forall (m :: * -> *) a b. Monad m => m a -> (a -> m b) -> m b
>>= IO (Maybe TxId, UTxO)
-> ReaderT (IORef (Maybe TxId, UTxO)) IO (Maybe TxId, UTxO)
forall a. IO a -> ReaderT (IORef (Maybe TxId, UTxO)) IO a
forall (m :: * -> *) a. MonadIO m => IO a -> m a
liftIO (IO (Maybe TxId, UTxO)
 -> ReaderT (IORef (Maybe TxId, UTxO)) IO (Maybe TxId, UTxO))
-> (IORef (Maybe TxId, UTxO) -> IO (Maybe TxId, UTxO))
-> IORef (Maybe TxId, UTxO)
-> ReaderT (IORef (Maybe TxId, UTxO)) IO (Maybe TxId, UTxO)
forall b c a. (b -> c) -> (a -> b) -> a -> c
. IORef (Maybe TxId, UTxO) -> IO (Maybe TxId, UTxO)
forall (m :: * -> *) a. MonadIO m => IORef a -> m a
readIORef

  local :: forall a.
((Maybe TxId, UTxO) -> (Maybe TxId, UTxO)) -> AppM a -> AppM a
local (Maybe TxId, UTxO) -> (Maybe TxId, UTxO)
f AppM a
action = do
    (Maybe TxId, UTxO)
txidAndutxo <- AppM (Maybe TxId, UTxO)
forall r (m :: * -> *). MonadReader r m => m r
ask
    IORef (Maybe TxId, UTxO)
r <- (Maybe TxId, UTxO) -> AppM (IORef (Maybe TxId, UTxO))
forall (m :: * -> *) a. MonadIO m => a -> m (IORef a)
newIORef ((Maybe TxId, UTxO) -> (Maybe TxId, UTxO)
f (Maybe TxId, UTxO)
txidAndutxo)
    ReaderT (IORef (Maybe TxId, UTxO)) IO a -> AppM a
forall a. ReaderT (IORef (Maybe TxId, UTxO)) IO a -> AppM a
AppM (ReaderT (IORef (Maybe TxId, UTxO)) IO a -> AppM a)
-> ReaderT (IORef (Maybe TxId, UTxO)) IO a -> AppM a
forall a b. (a -> b) -> a -> b
$ (IORef (Maybe TxId, UTxO) -> IORef (Maybe TxId, UTxO))
-> ReaderT (IORef (Maybe TxId, UTxO)) IO a
-> ReaderT (IORef (Maybe TxId, UTxO)) IO a
forall a.
(IORef (Maybe TxId, UTxO) -> IORef (Maybe TxId, UTxO))
-> ReaderT (IORef (Maybe TxId, UTxO)) IO a
-> ReaderT (IORef (Maybe TxId, UTxO)) IO a
forall r (m :: * -> *) a. MonadReader r m => (r -> r) -> m a -> m a
local (IORef (Maybe TxId, UTxO)
-> IORef (Maybe TxId, UTxO) -> IORef (Maybe TxId, UTxO)
forall a b. a -> b -> a
const IORef (Maybe TxId, UTxO)
r) (ReaderT (IORef (Maybe TxId, UTxO)) IO a
 -> ReaderT (IORef (Maybe TxId, UTxO)) IO a)
-> ReaderT (IORef (Maybe TxId, UTxO)) IO a
-> ReaderT (IORef (Maybe TxId, UTxO)) IO a
forall a b. (a -> b) -> a -> b
$ AppM a -> ReaderT (IORef (Maybe TxId, UTxO)) IO a
forall a. AppM a -> ReaderT (IORef (Maybe TxId, UTxO)) IO a
runAppM AppM a
action

instance MonadState (Maybe TxId, UTxO) AppM where
  get :: AppM (Maybe TxId, UTxO)
get = AppM (Maybe TxId, UTxO)
forall r (m :: * -> *). MonadReader r m => m r
ask
  put :: (Maybe TxId, UTxO) -> AppM ()
put (Maybe TxId, UTxO)
utxo = ReaderT (IORef (Maybe TxId, UTxO)) IO () -> AppM ()
forall a. ReaderT (IORef (Maybe TxId, UTxO)) IO a -> AppM a
AppM (ReaderT (IORef (Maybe TxId, UTxO)) IO () -> AppM ())
-> ReaderT (IORef (Maybe TxId, UTxO)) IO () -> AppM ()
forall a b. (a -> b) -> a -> b
$ ReaderT (IORef (Maybe TxId, UTxO)) IO (IORef (Maybe TxId, UTxO))
forall r (m :: * -> *). MonadReader r m => m r
ask ReaderT (IORef (Maybe TxId, UTxO)) IO (IORef (Maybe TxId, UTxO))
-> (IORef (Maybe TxId, UTxO)
    -> ReaderT (IORef (Maybe TxId, UTxO)) IO ())
-> ReaderT (IORef (Maybe TxId, UTxO)) IO ()
forall a b.
ReaderT (IORef (Maybe TxId, UTxO)) IO a
-> (a -> ReaderT (IORef (Maybe TxId, UTxO)) IO b)
-> ReaderT (IORef (Maybe TxId, UTxO)) IO b
forall (m :: * -> *) a b. Monad m => m a -> (a -> m b) -> m b
>>= IO () -> ReaderT (IORef (Maybe TxId, UTxO)) IO ()
forall a. IO a -> ReaderT (IORef (Maybe TxId, UTxO)) IO a
forall (m :: * -> *) a. MonadIO m => IO a -> m a
liftIO (IO () -> ReaderT (IORef (Maybe TxId, UTxO)) IO ())
-> (IORef (Maybe TxId, UTxO) -> IO ())
-> IORef (Maybe TxId, UTxO)
-> ReaderT (IORef (Maybe TxId, UTxO)) IO ()
forall b c a. (b -> c) -> (a -> b) -> a -> c
. (IORef (Maybe TxId, UTxO) -> (Maybe TxId, UTxO) -> IO ())
-> (Maybe TxId, UTxO) -> IORef (Maybe TxId, UTxO) -> IO ()
forall a b c. (a -> b -> c) -> b -> a -> c
flip IORef (Maybe TxId, UTxO) -> (Maybe TxId, UTxO) -> IO ()
forall (m :: * -> *) a. MonadIO m => IORef a -> a -> m ()
writeIORef (Maybe TxId, UTxO)
utxo

type instance Realized AppM a = a

-- XXX: Most of the heavy-lifting here is similar to what
-- quickcheck-contractmodel does. We could consider using that package and
-- define a corresponding RunModel using our tx construction / evaluation hooks
-- only.
instance RunModel Model AppM where
  perform :: forall a.
Typeable a =>
Model
-> Action Model a
-> LookUp AppM
-> AppM (PerformResult (Error Model) (Realized AppM a))
perform Model{SnapshotVersion
$sel:currentVersion:Model :: Model -> SnapshotVersion
currentVersion :: SnapshotVersion
currentVersion} Action Model a
action LookUp AppM
_lookupVar = do
    case Action Model a
action of
      deposit :: Action Model a
deposit@Deposit{ModelUTxO
$sel:utxoToDeposit:NewSnapshot :: Action Model TxResult -> ModelUTxO
utxoToDeposit :: ModelUTxO
utxoToDeposit} -> do
        Either String Tx
tx <- Action Model a -> ModelUTxO -> AppM (Either String Tx)
forall a. Action Model a -> ModelUTxO -> AppM (Either String Tx)
newDepositTx Action Model a
deposit ModelUTxO
utxoToDeposit
        Action Model a -> Either String Tx -> AppM TxResult
forall err a.
Show err =>
Action Model a -> Either err Tx -> AppM TxResult
performTx Action Model a
deposit Either String Tx
tx
      i :: Action Model a
i@Increment{Actor
$sel:actor:NewSnapshot :: Action Model TxResult -> Actor
actor :: Actor
actor, ModelSnapshot
$sel:snapshot:NewSnapshot :: Action Model TxResult -> ModelSnapshot
snapshot :: ModelSnapshot
snapshot} -> do
        Either IncrementTxError Tx
tx <- Actor -> ConfirmedSnapshot Tx -> AppM (Either IncrementTxError Tx)
newIncrementTx Actor
actor (ModelSnapshot -> ConfirmedSnapshot Tx
confirmedSnapshot ModelSnapshot
snapshot)
        Action Model a -> Either IncrementTxError Tx -> AppM TxResult
forall err a.
Show err =>
Action Model a -> Either err Tx -> AppM TxResult
performTx Action Model a
i Either IncrementTxError Tx
tx
      d :: Action Model a
d@Decrement{Actor
$sel:actor:NewSnapshot :: Action Model TxResult -> Actor
actor :: Actor
actor, ModelSnapshot
$sel:snapshot:NewSnapshot :: Action Model TxResult -> ModelSnapshot
snapshot :: ModelSnapshot
snapshot} -> do
        Either DecrementTxError Tx
tx <- Actor -> ConfirmedSnapshot Tx -> AppM (Either DecrementTxError Tx)
newDecrementTx Actor
actor (ModelSnapshot -> ConfirmedSnapshot Tx
confirmedSnapshot ModelSnapshot
snapshot)
        Action Model a -> Either DecrementTxError Tx -> AppM TxResult
forall err a.
Show err =>
Action Model a -> Either err Tx -> AppM TxResult
performTx Action Model a
d Either DecrementTxError Tx
tx
      c :: Action Model a
c@Close{Actor
$sel:actor:NewSnapshot :: Action Model TxResult -> Actor
actor :: Actor
actor, ModelSnapshot
$sel:snapshot:NewSnapshot :: Action Model TxResult -> ModelSnapshot
snapshot :: ModelSnapshot
snapshot} -> do
        Either CloseTxError Tx
tx <- Actor
-> SnapshotVersion
-> ConfirmedSnapshot Tx
-> AppM (Either CloseTxError Tx)
newCloseTx Actor
actor SnapshotVersion
currentVersion (ModelSnapshot -> ConfirmedSnapshot Tx
confirmedSnapshot ModelSnapshot
snapshot)
        Action Model a -> Either CloseTxError Tx -> AppM TxResult
forall err a.
Show err =>
Action Model a -> Either err Tx -> AppM TxResult
performTx Action Model a
c Either CloseTxError Tx
tx
      c :: Action Model a
c@Contest{Actor
$sel:actor:NewSnapshot :: Action Model TxResult -> Actor
actor :: Actor
actor, ModelSnapshot
$sel:snapshot:NewSnapshot :: Action Model TxResult -> ModelSnapshot
snapshot :: ModelSnapshot
snapshot} -> do
        Either ContestTxError Tx
tx <- Actor
-> SnapshotVersion
-> ConfirmedSnapshot Tx
-> AppM (Either ContestTxError Tx)
newContestTx Actor
actor SnapshotVersion
currentVersion (ModelSnapshot -> ConfirmedSnapshot Tx
confirmedSnapshot ModelSnapshot
snapshot)
        Action Model a -> Either ContestTxError Tx -> AppM TxResult
forall err a.
Show err =>
Action Model a -> Either err Tx -> AppM TxResult
performTx Action Model a
c Either ContestTxError Tx
tx
      f :: Action Model a
f@Fanout{ModelUTxO
$sel:utxo:NewSnapshot :: Action Model TxResult -> ModelUTxO
utxo :: ModelUTxO
utxo, ModelUTxO
$sel:alphaUTxO:NewSnapshot :: Action Model TxResult -> ModelUTxO
alphaUTxO :: ModelUTxO
alphaUTxO, ModelUTxO
$sel:omegaUTxO:NewSnapshot :: Action Model TxResult -> ModelUTxO
omegaUTxO :: ModelUTxO
omegaUTxO} -> do
        Either FanoutTxError Tx
tx <- Actor
-> ModelUTxO
-> ModelUTxO
-> ModelUTxO
-> AppM (Either FanoutTxError Tx)
newFanoutTx Actor
Alice ModelUTxO
utxo ModelUTxO
alphaUTxO ModelUTxO
omegaUTxO
        Action Model a -> Either FanoutTxError Tx -> AppM TxResult
forall err a.
Show err =>
Action Model a -> Either err Tx -> AppM TxResult
performTx Action Model a
f Either FanoutTxError Tx
tx
      NewSnapshot{} -> () -> AppM ()
forall a. a -> AppM a
forall (f :: * -> *) a. Applicative f => a -> f a
pure ()
      Action Model a
R:ActionModela a
Stop -> () -> AppM ()
forall a. a -> AppM a
forall (f :: * -> *) a. Applicative f => a -> f a
pure ()

  postcondition :: forall a.
(Model, Model)
-> Action Model a
-> LookUp AppM
-> Realized AppM a
-> PostconditionM AppM Bool
postcondition (Model
modelBefore, Model
modelAfter) Action Model a
action LookUp AppM
_lookup Realized AppM a
result = PostconditionM' AppM () -> PostconditionM AppM Bool
forall (m :: * -> *).
Monad m =>
PostconditionM' m () -> PostconditionM m Bool
runPostconditionM' (PostconditionM' AppM () -> PostconditionM AppM Bool)
-> PostconditionM' AppM () -> PostconditionM AppM Bool
forall a b. (a -> b) -> a -> b
$ do
    String -> PostconditionM' AppM ()
forall (m :: * -> *). Monad m => String -> PostconditionM' m ()
counterexample' (Model -> String
forall a. Show a => a -> String
show Model
modelBefore)
    String -> PostconditionM' AppM ()
forall (m :: * -> *). Monad m => String -> PostconditionM' m ()
counterexample' (Action Model a -> String
forall a. Show a => a -> String
show Action Model a
action)
    case Action Model a
action of
      Deposit{} -> TxResult
-> (HeadObservation -> PostconditionM' AppM ())
-> PostconditionM' AppM ()
forall (m :: * -> *) a.
Monad m =>
TxResult
-> (HeadObservation -> PostconditionM' m a) -> PostconditionM' m a
expectValid Realized AppM a
TxResult
result ((HeadObservation -> PostconditionM' AppM ())
 -> PostconditionM' AppM ())
-> (HeadObservation -> PostconditionM' AppM ())
-> PostconditionM' AppM ()
forall a b. (a -> b) -> a -> b
$ \case
        Tx.Deposit{} -> () -> PostconditionM' AppM ()
forall a. a -> PostconditionM' AppM a
forall (f :: * -> *) a. Applicative f => a -> f a
pure ()
        HeadObservation
_ -> String -> PostconditionM' AppM ()
forall a. String -> PostconditionM' AppM a
forall (m :: * -> *) a. MonadFail m => String -> m a
fail String
"Expected Deposit"
      Increment{} -> TxResult
-> (HeadObservation -> PostconditionM' AppM ())
-> PostconditionM' AppM ()
forall (m :: * -> *) a.
Monad m =>
TxResult
-> (HeadObservation -> PostconditionM' m a) -> PostconditionM' m a
expectValid Realized AppM a
TxResult
result ((HeadObservation -> PostconditionM' AppM ())
 -> PostconditionM' AppM ())
-> (HeadObservation -> PostconditionM' AppM ())
-> PostconditionM' AppM ()
forall a b. (a -> b) -> a -> b
$ \case
        Tx.Increment{} -> () -> PostconditionM' AppM ()
forall a. a -> PostconditionM' AppM a
forall (f :: * -> *) a. Applicative f => a -> f a
pure ()
        HeadObservation
_ -> String -> PostconditionM' AppM ()
forall a. String -> PostconditionM' AppM a
forall (m :: * -> *) a. MonadFail m => String -> m a
fail String
"Expected Increment"
      Decrement{} -> TxResult
-> (HeadObservation -> PostconditionM' AppM ())
-> PostconditionM' AppM ()
forall (m :: * -> *) a.
Monad m =>
TxResult
-> (HeadObservation -> PostconditionM' m a) -> PostconditionM' m a
expectValid Realized AppM a
TxResult
result ((HeadObservation -> PostconditionM' AppM ())
 -> PostconditionM' AppM ())
-> (HeadObservation -> PostconditionM' AppM ())
-> PostconditionM' AppM ()
forall a b. (a -> b) -> a -> b
$ \case
        Tx.Decrement{} -> () -> PostconditionM' AppM ()
forall a. a -> PostconditionM' AppM a
forall (f :: * -> *) a. Applicative f => a -> f a
pure ()
        HeadObservation
_ -> String -> PostconditionM' AppM ()
forall a. String -> PostconditionM' AppM a
forall (m :: * -> *) a. MonadFail m => String -> m a
fail String
"Expected Decrement"
      Close{} -> TxResult
-> (HeadObservation -> PostconditionM' AppM ())
-> PostconditionM' AppM ()
forall (m :: * -> *) a.
Monad m =>
TxResult
-> (HeadObservation -> PostconditionM' m a) -> PostconditionM' m a
expectValid Realized AppM a
TxResult
result ((HeadObservation -> PostconditionM' AppM ())
 -> PostconditionM' AppM ())
-> (HeadObservation -> PostconditionM' AppM ())
-> PostconditionM' AppM ()
forall a b. (a -> b) -> a -> b
$ \case
        Tx.Close{} -> () -> PostconditionM' AppM ()
forall a. a -> PostconditionM' AppM a
forall (f :: * -> *) a. Applicative f => a -> f a
pure ()
        HeadObservation
_ -> String -> PostconditionM' AppM ()
forall a. String -> PostconditionM' AppM a
forall (m :: * -> *) a. MonadFail m => String -> m a
fail String
"Expected Close"
      Contest{} -> TxResult
-> (HeadObservation -> PostconditionM' AppM ())
-> PostconditionM' AppM ()
forall (m :: * -> *) a.
Monad m =>
TxResult
-> (HeadObservation -> PostconditionM' m a) -> PostconditionM' m a
expectValid Realized AppM a
TxResult
result ((HeadObservation -> PostconditionM' AppM ())
 -> PostconditionM' AppM ())
-> (HeadObservation -> PostconditionM' AppM ())
-> PostconditionM' AppM ()
forall a b. (a -> b) -> a -> b
$ \case
        Tx.Contest Tx.ContestObservation{[PubKeyHash]
contesters :: [PubKeyHash]
$sel:contesters:ContestObservation :: ContestObservation -> [PubKeyHash]
contesters} -> do
          String -> PostconditionM' AppM ()
forall (m :: * -> *). Monad m => String -> PostconditionM' m ()
counterexample' (String -> PostconditionM' AppM ())
-> String -> PostconditionM' AppM ()
forall a b. (a -> b) -> a -> b
$ String
"Wrong contesters: expected " String -> ShowS
forall a. Semigroup a => a -> a -> a
<> [Actor] -> String
forall a. Show a => a -> String
show (Model -> [Actor]
alreadyContested Model
modelAfter) String -> ShowS
forall a. Semigroup a => a -> a -> a
<> String
", got " String -> ShowS
forall a. Semigroup a => a -> a -> a
<> [PubKeyHash] -> String
forall a. Show a => a -> String
show [PubKeyHash]
contesters
          Bool -> PostconditionM' AppM ()
forall (f :: * -> *). Alternative f => Bool -> f ()
guard (Bool -> PostconditionM' AppM ())
-> Bool -> PostconditionM' AppM ()
forall a b. (a -> b) -> a -> b
$ [PubKeyHash] -> Int
forall a. [a] -> Int
forall (t :: * -> *) a. Foldable t => t a -> Int
length [PubKeyHash]
contesters Int -> Int -> Bool
forall a. Eq a => a -> a -> Bool
== [Actor] -> Int
forall a. [a] -> Int
forall (t :: * -> *) a. Foldable t => t a -> Int
length (Model -> [Actor]
alreadyContested Model
modelAfter)
        HeadObservation
_ -> String -> PostconditionM' AppM ()
forall a. String -> PostconditionM' AppM a
forall (m :: * -> *) a. MonadFail m => String -> m a
fail String
"Expected Contest"
      Fanout{ModelUTxO
$sel:utxo:NewSnapshot :: Action Model TxResult -> ModelUTxO
utxo :: ModelUTxO
utxo, ModelUTxO
$sel:omegaUTxO:NewSnapshot :: Action Model TxResult -> ModelUTxO
omegaUTxO :: ModelUTxO
omegaUTxO} -> do
        case Realized AppM a
result of
          TxResult{$sel:constructedTx:TxResult :: TxResult -> Either String Tx
constructedTx = Left String
err} -> String -> PostconditionM' AppM ()
forall a. String -> PostconditionM' AppM a
forall (m :: * -> *) a. MonadFail m => String -> m a
fail (String -> PostconditionM' AppM ())
-> String -> PostconditionM' AppM ()
forall a b. (a -> b) -> a -> b
$ String
"Failed to construct transaction: " String -> ShowS
forall a. Semigroup a => a -> a -> a
<> String
err
          TxResult{$sel:constructedTx:TxResult :: TxResult -> Either String Tx
constructedTx = Right Tx
tx} -> do
            -- NOTE: Sort `[TxOut]` by the address and values. We want to make
            -- sure that the fanout outputs match what we had in the open Head
            -- exactly.
            let sorted :: UTxO' (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))) ([TxOut ctx] -> [TxOut ctx])
-> (UTxO' (TxOut ctx) -> [TxOut ctx])
-> UTxO' (TxOut ctx)
-> [TxOut ctx]
forall b c a. (b -> c) -> (a -> b) -> a -> c
. UTxO' (TxOut ctx) -> [TxOut ctx]
forall a. UTxO' a -> [a]
forall (t :: * -> *) a. Foldable t => t a -> [a]
toList
            let fannedOut :: UTxOType Tx
fannedOut = Tx -> UTxOType Tx
forall tx. IsTx tx => tx -> UTxOType tx
utxoFromTx Tx
tx
            Bool -> PostconditionM' AppM ()
forall (f :: * -> *). Alternative f => Bool -> f ()
guard (Bool -> PostconditionM' AppM ())
-> Bool -> PostconditionM' AppM ()
forall a b. (a -> b) -> a -> b
$ UTxO -> [TxOut CtxUTxO Era]
forall {ctx}. UTxO' (TxOut ctx) -> [TxOut ctx]
sorted UTxO
UTxOType Tx
fannedOut [TxOut CtxUTxO Era] -> [TxOut CtxUTxO Era] -> Bool
forall a. Eq a => a -> a -> Bool
== UTxO -> [TxOut CtxUTxO Era]
forall {ctx}. UTxO' (TxOut ctx) -> [TxOut ctx]
sorted (ModelUTxO -> UTxO
realWorldModelUTxO ModelUTxO
utxo UTxO -> UTxO -> UTxO
forall a. Semigroup a => a -> a -> a
<> ModelUTxO -> UTxO
realWorldModelUTxO ModelUTxO
omegaUTxO)

        TxResult
-> (HeadObservation -> PostconditionM' AppM ())
-> PostconditionM' AppM ()
forall (m :: * -> *) a.
Monad m =>
TxResult
-> (HeadObservation -> PostconditionM' m a) -> PostconditionM' m a
expectValid Realized AppM a
TxResult
result ((HeadObservation -> PostconditionM' AppM ())
 -> PostconditionM' AppM ())
-> (HeadObservation -> PostconditionM' AppM ())
-> PostconditionM' AppM ()
forall a b. (a -> b) -> a -> b
$ \case
          Tx.Fanout{} -> () -> PostconditionM' AppM ()
forall a. a -> PostconditionM' AppM a
forall (f :: * -> *) a. Applicative f => a -> f a
pure ()
          HeadObservation
_ -> String -> PostconditionM' AppM ()
forall a. String -> PostconditionM' AppM a
forall (m :: * -> *) a. MonadFail m => String -> m a
fail String
"Expected Fanout"
      NewSnapshot{} -> () -> PostconditionM' AppM ()
forall a. a -> PostconditionM' AppM a
forall (f :: * -> *) a. Applicative f => a -> f a
pure ()
      Action Model a
R:ActionModela a
Stop -> () -> PostconditionM' AppM ()
forall a. a -> PostconditionM' AppM a
forall (f :: * -> *) a. Applicative f => a -> f a
pure ()

  postconditionOnFailure :: forall a.
(Model, Model)
-> Action Model a
-> LookUp AppM
-> Either (Error Model) (Realized AppM a)
-> PostconditionM AppM Bool
postconditionOnFailure (Model
modelBefore, Model
_modelAfter) Action Model a
action LookUp AppM
_lookup Either (Error Model) (Realized AppM a)
result = PostconditionM' AppM () -> PostconditionM AppM Bool
forall (m :: * -> *).
Monad m =>
PostconditionM' m () -> PostconditionM m Bool
runPostconditionM' (PostconditionM' AppM () -> PostconditionM AppM Bool)
-> PostconditionM' AppM () -> PostconditionM AppM Bool
forall a b. (a -> b) -> a -> b
$ do
    String -> PostconditionM' AppM ()
forall (m :: * -> *). Monad m => String -> PostconditionM' m ()
counterexample' (Model -> String
forall a. Show a => a -> String
show Model
modelBefore)
    String -> PostconditionM' AppM ()
forall (m :: * -> *). Monad m => String -> PostconditionM' m ()
counterexample' (Action Model a -> String
forall a. Show a => a -> String
show Action Model a
action)
    case Action Model a
action of
      Deposit{} -> (Void -> PostconditionM' AppM ())
-> (TxResult -> PostconditionM' AppM ())
-> Either Void TxResult
-> PostconditionM' AppM ()
forall a c b. (a -> c) -> (b -> c) -> Either a b -> c
either (PostconditionM' AppM () -> Void -> PostconditionM' AppM ()
forall a b. a -> b -> a
const PostconditionM' AppM ()
forall (m :: * -> *). Monad m => PostconditionM' m ()
fulfilled) TxResult -> PostconditionM' AppM ()
forall (m :: * -> *). Monad m => TxResult -> PostconditionM' m ()
expectInvalid Either Void TxResult
Either (Error Model) (Realized AppM a)
result
      Increment{} -> (Void -> PostconditionM' AppM ())
-> (TxResult -> PostconditionM' AppM ())
-> Either Void TxResult
-> PostconditionM' AppM ()
forall a c b. (a -> c) -> (b -> c) -> Either a b -> c
either (PostconditionM' AppM () -> Void -> PostconditionM' AppM ()
forall a b. a -> b -> a
const PostconditionM' AppM ()
forall (m :: * -> *). Monad m => PostconditionM' m ()
fulfilled) TxResult -> PostconditionM' AppM ()
forall (m :: * -> *). Monad m => TxResult -> PostconditionM' m ()
expectInvalid Either Void TxResult
Either (Error Model) (Realized AppM a)
result
      Decrement{} -> (Void -> PostconditionM' AppM ())
-> (TxResult -> PostconditionM' AppM ())
-> Either Void TxResult
-> PostconditionM' AppM ()
forall a c b. (a -> c) -> (b -> c) -> Either a b -> c
either (PostconditionM' AppM () -> Void -> PostconditionM' AppM ()
forall a b. a -> b -> a
const PostconditionM' AppM ()
forall (m :: * -> *). Monad m => PostconditionM' m ()
fulfilled) TxResult -> PostconditionM' AppM ()
forall (m :: * -> *). Monad m => TxResult -> PostconditionM' m ()
expectInvalid Either Void TxResult
Either (Error Model) (Realized AppM a)
result
      Close{} -> (Void -> PostconditionM' AppM ())
-> (TxResult -> PostconditionM' AppM ())
-> Either Void TxResult
-> PostconditionM' AppM ()
forall a c b. (a -> c) -> (b -> c) -> Either a b -> c
either (PostconditionM' AppM () -> Void -> PostconditionM' AppM ()
forall a b. a -> b -> a
const PostconditionM' AppM ()
forall (m :: * -> *). Monad m => PostconditionM' m ()
fulfilled) TxResult -> PostconditionM' AppM ()
forall (m :: * -> *). Monad m => TxResult -> PostconditionM' m ()
expectInvalid Either Void TxResult
Either (Error Model) (Realized AppM a)
result
      Contest{} -> (Void -> PostconditionM' AppM ())
-> (TxResult -> PostconditionM' AppM ())
-> Either Void TxResult
-> PostconditionM' AppM ()
forall a c b. (a -> c) -> (b -> c) -> Either a b -> c
either (PostconditionM' AppM () -> Void -> PostconditionM' AppM ()
forall a b. a -> b -> a
const PostconditionM' AppM ()
forall (m :: * -> *). Monad m => PostconditionM' m ()
fulfilled) TxResult -> PostconditionM' AppM ()
forall (m :: * -> *). Monad m => TxResult -> PostconditionM' m ()
expectInvalid Either Void TxResult
Either (Error Model) (Realized AppM a)
result
      Fanout{} -> (Void -> PostconditionM' AppM ())
-> (TxResult -> PostconditionM' AppM ())
-> Either Void TxResult
-> PostconditionM' AppM ()
forall a c b. (a -> c) -> (b -> c) -> Either a b -> c
either (PostconditionM' AppM () -> Void -> PostconditionM' AppM ()
forall a b. a -> b -> a
const PostconditionM' AppM ()
forall (m :: * -> *). Monad m => PostconditionM' m ()
fulfilled) TxResult -> PostconditionM' AppM ()
forall (m :: * -> *). Monad m => TxResult -> PostconditionM' m ()
expectInvalid Either Void TxResult
Either (Error Model) (Realized AppM a)
result
      Action Model a
_ -> () -> PostconditionM' AppM ()
forall a. a -> PostconditionM' AppM a
forall (f :: * -> *) a. Applicative f => a -> f a
pure ()

-- | Perform a transaction by evaluating and observing it. This updates the
-- 'UTxO' in the 'AppM' if a transaction is valid and produces a 'TxResult' that
-- can be used to assert expected success / failure.
performTx :: Show err => Action Model a -> Either err Tx -> AppM TxResult
performTx :: forall err a.
Show err =>
Action Model a -> Either err Tx -> AppM TxResult
performTx Action Model a
action Either err Tx
result =
  case Either err Tx
result of
    Left err
err -> do
      (Maybe TxId
_, UTxO
utxo) <- AppM (Maybe TxId, UTxO)
forall s (m :: * -> *). MonadState s m => m s
get
      TxResult -> AppM TxResult
forall a. a -> AppM a
forall (f :: * -> *) a. Applicative f => a -> f a
pure
        TxResult
          { $sel:constructedTx:TxResult :: Either String Tx
constructedTx = String -> Either String Tx
forall a b. a -> Either a b
Left (String -> Either String Tx) -> String -> Either String Tx
forall a b. (a -> b) -> a -> b
$ err -> String
forall a. Show a => a -> String
show err
err
          , $sel:spendableUTxO:TxResult :: UTxO
spendableUTxO = UTxO
utxo
          , $sel:validationError:TxResult :: Maybe String
validationError = Maybe String
forall a. Maybe a
Nothing
          , $sel:observation:TxResult :: HeadObservation
observation = HeadObservation
NoHeadTx
          }
    Right Tx
tx -> do
      (Maybe TxId
depositTxId, UTxO
utxo) <- AppM (Maybe TxId, UTxO)
forall s (m :: * -> *). MonadState s m => m s
get
      let validationError :: Maybe String
validationError = Tx -> UTxO -> Maybe String
getValidationError Tx
tx UTxO
utxo
      Bool -> AppM () -> AppM ()
forall (f :: * -> *). Applicative f => Bool -> f () -> f ()
when (Maybe String -> Bool
forall a. Maybe a -> Bool
isNothing Maybe String
validationError) (AppM () -> AppM ()) -> AppM () -> AppM ()
forall a b. (a -> b) -> a -> b
$ do
        let adjusted :: (Maybe TxId, UTxO)
adjusted =
              case Action Model a
action of
                Deposit{} -> (TxId -> Maybe TxId
forall a. a -> Maybe a
Just (TxId -> Maybe TxId) -> (Tx -> TxId) -> Tx -> Maybe TxId
forall b c a. (b -> c) -> (a -> b) -> a -> c
. TxBody Era -> TxId
forall era. TxBody era -> TxId
getTxId (TxBody Era -> TxId) -> (Tx -> TxBody Era) -> Tx -> TxId
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Tx -> TxBody Era
forall era. Tx era -> TxBody era
getTxBody (Tx -> Maybe TxId) -> Tx -> Maybe TxId
forall a b. (a -> b) -> a -> b
$ Tx
tx, Tx -> UTxO -> UTxO
adjustUTxO Tx
tx UTxO
utxo)
                Action Model a
_ -> (Maybe TxId
depositTxId, Tx -> UTxO -> UTxO
adjustUTxO Tx
tx UTxO
utxo)
        (Maybe TxId, UTxO) -> AppM ()
forall s (m :: * -> *). MonadState s m => s -> m ()
put (Maybe TxId, UTxO)
adjusted
      let observation :: HeadObservation
observation = NetworkId -> UTxO -> Tx -> HeadObservation
observeHeadTx NetworkId
Fixture.testNetworkId UTxO
utxo Tx
tx
      TxResult -> AppM TxResult
forall a. a -> AppM a
forall (f :: * -> *) a. Applicative f => a -> f a
pure
        TxResult
          { $sel:constructedTx:TxResult :: Either String Tx
constructedTx = Tx -> Either String Tx
forall a b. b -> Either a b
Right Tx
tx
          , $sel:spendableUTxO:TxResult :: UTxO
spendableUTxO = UTxO
utxo
          , Maybe String
$sel:validationError:TxResult :: Maybe String
validationError :: Maybe String
validationError
          , HeadObservation
$sel:observation:TxResult :: HeadObservation
observation :: HeadObservation
observation
          }

getValidationError :: Tx -> UTxO -> Maybe String
getValidationError :: Tx -> UTxO -> Maybe String
getValidationError Tx
tx UTxO
utxo =
  case Tx -> UTxO -> Either EvaluationError EvaluationReport
evaluateTx Tx
tx UTxO
utxo of
    Left EvaluationError
err ->
      String -> Maybe String
forall a. a -> Maybe a
Just (String -> Maybe String) -> String -> Maybe String
forall a b. (a -> b) -> a -> b
$ EvaluationError -> String
forall a. Show a => a -> String
show EvaluationError
err
    Right EvaluationReport
redeemerReport
      | (Either ScriptExecutionError ExecutionUnits -> Bool)
-> [Either ScriptExecutionError ExecutionUnits] -> Bool
forall (t :: * -> *) a. Foldable t => (a -> Bool) -> t a -> Bool
any Either ScriptExecutionError ExecutionUnits -> Bool
forall a b. Either a b -> Bool
isLeft (EvaluationReport -> [Either ScriptExecutionError ExecutionUnits]
forall k a. Map k a -> [a]
Map.elems EvaluationReport
redeemerReport) ->
          String -> Maybe String
forall a. a -> Maybe a
Just (String -> Maybe String)
-> ([Text] -> String) -> [Text] -> Maybe String
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Text -> String
forall a. ToString a => a -> String
toString (Text -> String) -> ([Text] -> Text) -> [Text] -> String
forall b c a. (b -> c) -> (a -> b) -> a -> c
. [Text] -> Text
forall t. IsText t "unlines" => [t] -> t
unlines ([Text] -> Maybe String) -> [Text] -> Maybe String
forall a b. (a -> b) -> a -> b
$
            String -> Text
forall a. IsString a => String -> a
fromString
              (String -> Text) -> [String] -> [Text]
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> [ String
"Transaction evaluation failed: " String -> ShowS
forall a. Semigroup a => a -> a -> a
<> UTxO -> Tx -> String
renderTxWithUTxO UTxO
utxo Tx
tx
                  , String
"Some redeemers failed: " String -> ShowS
forall a. Semigroup a => a -> a -> a
<> EvaluationReport -> String
forall a. Show a => a -> String
show EvaluationReport
redeemerReport
                  ]
      | Bool
otherwise -> Maybe String
forall a. Maybe a
Nothing

-- * Fixtures and glue code

-- | List of all model actors corresponding to the fixtures used.
allActors :: [Actor]
allActors :: [Actor]
allActors = [Actor
Alice, Actor
Bob, Actor
Carol]

-- | Map a 'ModelUTxO' to a real-world 'UTxO'.
realWorldModelUTxO :: ModelUTxO -> UTxO
realWorldModelUTxO :: ModelUTxO -> UTxO
realWorldModelUTxO =
  (SingleUTxO -> UTxO) -> ModelUTxO -> UTxO
forall m a. Monoid m => (a -> m) -> [a] -> m
forall (t :: * -> *) m a.
(Foldable t, Monoid m) =>
(a -> m) -> t a -> m
foldMap (\SingleUTxO
a -> Gen UTxO
gen Gen UTxO -> Int -> UTxO
forall a. Gen a -> Int -> a
`generateWith` SingleUTxO -> Int
forall a. Enum a => a -> Int
fromEnum SingleUTxO
a)
 where
  gen :: Gen UTxO
gen = do
    Lovelace
lovelace <- Gen Lovelace
forall a. Arbitrary a => Gen a
arbitrary
    Gen (TxOut CtxUTxO Era) -> Gen UTxO
genUTxO1 ((Value -> Value) -> TxOut CtxUTxO Era -> TxOut CtxUTxO Era
forall era ctx.
IsMaryBasedEra era =>
(Value -> Value) -> TxOut ctx era -> TxOut ctx era
modifyTxOutValue (Value -> Value -> Value
forall a b. a -> b -> a
const (Value -> Value -> Value) -> Value -> Value -> Value
forall a b. (a -> b) -> a -> b
$ Lovelace -> Value
lovelaceToValue Lovelace
lovelace) (TxOut CtxUTxO Era -> TxOut CtxUTxO Era)
-> Gen (TxOut CtxUTxO Era) -> Gen (TxOut CtxUTxO Era)
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> Gen (TxOut CtxUTxO Era)
forall ctx. Gen (TxOut ctx)
genTxOut)

-- | A correctly signed snapshot. Given a snapshot number a snapshot signed by
-- all participants (alice, bob and carol) with some UTxO contained is produced.
signedSnapshot :: ModelSnapshot -> (Snapshot Tx, MultiSignature (Snapshot Tx))
signedSnapshot :: ModelSnapshot -> (Snapshot Tx, MultiSignature (Snapshot Tx))
signedSnapshot ModelSnapshot
ms =
  (Snapshot Tx
snapshot, MultiSignature (Snapshot Tx)
signatures)
 where
  snapshot :: Snapshot Tx
snapshot =
    Snapshot
      { $sel:headId:Snapshot :: HeadId
headId = PolicyId -> HeadId
mkHeadId PolicyId
Fixture.testPolicyId
      , $sel:version:Snapshot :: SnapshotVersion
version = ModelSnapshot
ms.version
      , $sel:number:Snapshot :: SnapshotNumber
number = ModelSnapshot
ms.number
      , $sel:confirmed:Snapshot :: [Tx]
confirmed = []
      , UTxO
UTxOType Tx
utxo :: UTxO
$sel:utxo:Snapshot :: UTxOType Tx
utxo
      , Maybe UTxO
Maybe (UTxOType Tx)
utxoToCommit :: Maybe UTxO
$sel:utxoToCommit:Snapshot :: Maybe (UTxOType Tx)
utxoToCommit
      , Maybe UTxO
Maybe (UTxOType Tx)
utxoToDecommit :: Maybe UTxO
$sel:utxoToDecommit:Snapshot :: Maybe (UTxOType Tx)
utxoToDecommit
      }

  signatures :: MultiSignature (Snapshot Tx)
signatures = [Signature (Snapshot Tx)] -> MultiSignature (Snapshot Tx)
forall {k} (a :: k). [Signature a] -> MultiSignature a
aggregate [SigningKey HydraKey -> Snapshot Tx -> Signature (Snapshot Tx)
forall a.
SignableRepresentation a =>
SigningKey HydraKey -> a -> Signature a
sign SigningKey HydraKey
sk Snapshot Tx
snapshot | SigningKey HydraKey
sk <- [SigningKey HydraKey
Fixture.aliceSk, SigningKey HydraKey
Fixture.bobSk, SigningKey HydraKey
Fixture.carolSk]]

  utxo :: UTxO
utxo = ModelUTxO -> UTxO
realWorldModelUTxO (ModelSnapshot -> ModelUTxO
inHead ModelSnapshot
ms)

  utxoToDecommit :: Maybe UTxO
utxoToDecommit =
    let u :: UTxO
u = ModelUTxO -> UTxO
realWorldModelUTxO (ModelSnapshot -> ModelUTxO
toDecommit ModelSnapshot
ms)
     in if UTxO -> Bool
forall a. UTxO' a -> Bool
forall (t :: * -> *) a. Foldable t => t a -> Bool
null UTxO
u then Maybe UTxO
forall a. Maybe a
Nothing else UTxO -> Maybe UTxO
forall a. a -> Maybe a
Just UTxO
u

  utxoToCommit :: Maybe UTxO
utxoToCommit =
    let u :: UTxO
u = ModelUTxO -> UTxO
realWorldModelUTxO (ModelSnapshot -> ModelUTxO
toCommit ModelSnapshot
ms)
     in if UTxO -> Bool
forall a. UTxO' a -> Bool
forall (t :: * -> *) a. Foldable t => t a -> Bool
null UTxO
u then Maybe UTxO
forall a. Maybe a
Nothing else UTxO -> Maybe UTxO
forall a. a -> Maybe a
Just UTxO
u

-- | A confirmed snapshot (either initial or later confirmed), based onTxTra
-- 'signedSnapshot'.
confirmedSnapshot :: ModelSnapshot -> ConfirmedSnapshot Tx
confirmedSnapshot :: ModelSnapshot -> ConfirmedSnapshot Tx
confirmedSnapshot modelSnapshot :: ModelSnapshot
modelSnapshot@ModelSnapshot{SnapshotNumber
$sel:number:ModelSnapshot :: ModelSnapshot -> SnapshotNumber
number :: SnapshotNumber
number} =
  case SnapshotNumber
number of
    SnapshotNumber
0 ->
      InitialSnapshot
        { -- -- NOTE: The close validator would not check headId on close with
          -- initial snapshot, but we need to provide it still.
          $sel:headId:InitialSnapshot :: HeadId
headId = PolicyId -> HeadId
mkHeadId PolicyId
Fixture.testPolicyId
        , $sel:initialUTxO:InitialSnapshot :: UTxOType Tx
initialUTxO = ModelUTxO -> UTxO
realWorldModelUTxO (ModelUTxO -> UTxO) -> ModelUTxO -> UTxO
forall a b. (a -> b) -> a -> b
$ ModelSnapshot -> ModelUTxO
inHead ModelSnapshot
modelSnapshot
        }
    SnapshotNumber
_ -> ConfirmedSnapshot{Snapshot Tx
snapshot :: Snapshot Tx
$sel:snapshot:InitialSnapshot :: Snapshot Tx
snapshot, MultiSignature (Snapshot Tx)
signatures :: MultiSignature (Snapshot Tx)
$sel:signatures:InitialSnapshot :: MultiSignature (Snapshot Tx)
signatures}
     where
      (Snapshot Tx
snapshot, MultiSignature (Snapshot Tx)
signatures) = ModelSnapshot -> (Snapshot Tx, MultiSignature (Snapshot Tx))
signedSnapshot ModelSnapshot
modelSnapshot

-- | UTxO of the open head on-chain. NOTE: This uses fixtures for headId, parties, and cperiod.
openHeadUTxO :: UTxO
openHeadUTxO :: UTxO
openHeadUTxO =
  (TxIn, TxOut CtxUTxO Era) -> UTxO
forall out. (TxIn, out) -> UTxO' out
UTxO.singleton (TxIn
headTxIn, TxOut CtxUTxO Era
openHeadTxOut)
    UTxO -> UTxO -> UTxO
forall a. Semigroup a => a -> a -> a
<> ScriptRegistry -> UTxO
registryUTxO ScriptRegistry
testScriptRegistry
 where
  headTxIn :: TxIn
headTxIn = Gen TxIn
forall a. Arbitrary a => Gen a
arbitrary Gen TxIn -> Int -> TxIn
forall a. Gen a -> Int -> a
`generateWith` Int
42

  openHeadTxOut :: TxOut CtxUTxO Era
openHeadTxOut =
    NetworkId -> PolicyId -> TxOutDatum CtxUTxO -> TxOut CtxUTxO Era
forall ctx. NetworkId -> PolicyId -> TxOutDatum ctx -> TxOut ctx
mkHeadOutput NetworkId
Fixture.testNetworkId PolicyId
Fixture.testPolicyId TxOutDatum CtxUTxO
forall {ctx}. TxOutDatum ctx Era
openHeadDatum
      TxOut CtxUTxO Era
-> (TxOut CtxUTxO Era -> TxOut CtxUTxO Era) -> TxOut CtxUTxO Era
forall a b. a -> (a -> b) -> b
& [VerificationKey PaymentKey]
-> TxOut CtxUTxO Era -> TxOut CtxUTxO Era
addParticipationTokens [VerificationKey PaymentKey
alicePVk, VerificationKey PaymentKey
bobPVk, VerificationKey PaymentKey
carolPVk]
      TxOut CtxUTxO Era
-> (TxOut CtxUTxO Era -> TxOut CtxUTxO Era) -> TxOut CtxUTxO Era
forall a b. a -> (a -> b) -> b
& (Value -> Value) -> TxOut CtxUTxO Era -> TxOut CtxUTxO Era
forall era ctx.
IsMaryBasedEra era =>
(Value -> Value) -> TxOut ctx era -> TxOut ctx era
modifyTxOutValue (Value -> Value -> Value
forall a. Semigroup a => a -> a -> a
<> (TxOut CtxUTxO Era -> Value) -> UTxO -> Value
forall m a. Monoid m => (a -> m) -> UTxO' a -> m
forall (t :: * -> *) m a.
(Foldable t, Monoid m) =>
(a -> m) -> t a -> m
foldMap TxOut CtxUTxO Era -> Value
forall ctx. TxOut ctx -> Value
txOutValue UTxO
inHeadUTxO)

  openHeadDatum :: TxOutDatum ctx Era
openHeadDatum =
    State -> TxOutDatum ctx Era
forall era a ctx.
(ToScriptData a, IsBabbageBasedEra era) =>
a -> TxOutDatum ctx era
mkTxOutDatumInline (State -> TxOutDatum ctx Era) -> State -> TxOutDatum ctx Era
forall a b. (a -> b) -> a -> b
$
      OpenDatum -> State
Head.Open
        Head.OpenDatum
          { $sel:parties:OpenDatum :: [Party]
parties = Party -> Party
partyToChain (Party -> Party) -> [Party] -> [Party]
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> [Party
Fixture.alice, Party
Fixture.bob, Party
Fixture.carol]
          , $sel:utxoHash:OpenDatum :: Hash
utxoHash = ByteString -> ToBuiltin ByteString
forall a. HasToBuiltin a => a -> ToBuiltin a
toBuiltin (ByteString -> ToBuiltin ByteString)
-> ByteString -> ToBuiltin ByteString
forall a b. (a -> b) -> a -> b
$ UTxOType Tx -> ByteString
forall tx. IsTx tx => UTxOType tx -> ByteString
hashUTxO UTxO
UTxOType Tx
inHeadUTxO
          , $sel:contestationPeriod:OpenDatum :: ContestationPeriod
contestationPeriod = ContestationPeriod -> ContestationPeriod
CP.toChain ContestationPeriod
Fixture.cperiod
          , $sel:headId:OpenDatum :: CurrencySymbol
headId = HeadId -> CurrencySymbol
headIdToCurrencySymbol (HeadId -> CurrencySymbol) -> HeadId -> CurrencySymbol
forall a b. (a -> b) -> a -> b
$ PolicyId -> HeadId
mkHeadId PolicyId
Fixture.testPolicyId
          , $sel:version:OpenDatum :: Integer
version = Integer
0
          }

  inHeadUTxO :: UTxO
inHeadUTxO = ModelUTxO -> UTxO
realWorldModelUTxO (Model -> ModelUTxO
utxoInHead Model
forall state. StateModel state => state
initialState)

-- | Creates a deposit transaction using given UTxO.
newDepositTx :: Action Model a -> ModelUTxO -> AppM (Either String Tx)
newDepositTx :: forall a. Action Model a -> ModelUTxO -> AppM (Either String Tx)
newDepositTx Action Model a
_ ModelUTxO
utxoToDeposit = do
  let deadline :: UTCTime
deadline = UTCTime
Fixture.depositDeadline
  let depositUTxO :: UTxO
depositUTxO = ModelUTxO -> UTxO
realWorldModelUTxO ModelUTxO
utxoToDeposit
  let blueprint :: CommitBlueprintTx Tx
blueprint = CommitBlueprintTx{$sel:blueprintTx:CommitBlueprintTx :: Tx
blueprintTx = UTxO -> Tx
txSpendingUTxO UTxO
depositUTxO, $sel:lookupUTxO:CommitBlueprintTx :: UTxOType Tx
lookupUTxO = UTxO
UTxOType Tx
depositUTxO}
  Either String Tx -> AppM (Either String Tx)
forall a. a -> AppM a
forall (f :: * -> *) a. Applicative f => a -> f a
pure (Either String Tx -> AppM (Either String Tx))
-> Either String Tx -> AppM (Either String Tx)
forall a b. (a -> b) -> a -> b
$
    Tx -> Either String Tx
forall a b. b -> Either a b
Right (Tx -> Either String Tx) -> Tx -> Either String Tx
forall a b. (a -> b) -> a -> b
$
      NetworkId -> HeadId -> CommitBlueprintTx Tx -> UTCTime -> Tx
depositTx
        NetworkId
Fixture.testNetworkId
        (PolicyId -> HeadId
mkHeadId PolicyId
Fixture.testPolicyId)
        CommitBlueprintTx Tx
blueprint
        UTCTime
deadline

-- | Creates a increment transaction using given utxo and given snapshot.
newIncrementTx :: Actor -> ConfirmedSnapshot Tx -> AppM (Either IncrementTxError Tx)
newIncrementTx :: Actor -> ConfirmedSnapshot Tx -> AppM (Either IncrementTxError Tx)
newIncrementTx Actor
actor ConfirmedSnapshot Tx
snapshot = do
  let Snapshot{Maybe (UTxOType Tx)
$sel:utxoToCommit:Snapshot :: forall tx. Snapshot tx -> Maybe (UTxOType tx)
utxoToCommit :: Maybe (UTxOType Tx)
utxoToCommit} = ConfirmedSnapshot Tx -> Snapshot Tx
forall tx. ConfirmedSnapshot tx -> Snapshot tx
getSnapshot ConfirmedSnapshot Tx
snapshot
  case Maybe (UTxOType Tx)
utxoToCommit of
    Maybe (UTxOType Tx)
Nothing -> Either IncrementTxError Tx -> AppM (Either IncrementTxError Tx)
forall a. a -> AppM a
forall (f :: * -> *) a. Applicative f => a -> f a
pure (Either IncrementTxError Tx -> AppM (Either IncrementTxError Tx))
-> Either IncrementTxError Tx -> AppM (Either IncrementTxError Tx)
forall a b. (a -> b) -> a -> b
$ IncrementTxError -> Either IncrementTxError Tx
forall a b. a -> Either a b
Left IncrementTxError
SnapshotMissingIncrementUTxO
    Just UTxOType Tx
_ -> do
      (Maybe TxId
depositTxId, UTxO
spendableUTxO) <- AppM (Maybe TxId, UTxO)
forall s (m :: * -> *). MonadState s m => m s
get
      let slotNo :: SlotNo
slotNo = Word64 -> SlotNo
SlotNo Word64
0
      let txid :: TxId
txid = TxId -> Maybe TxId -> TxId
forall a. a -> Maybe a -> a
fromMaybe (Text -> TxId
forall a t. (HasCallStack, IsText t) => t -> a
error Text
"No deposit txid") Maybe TxId
depositTxId
      Either IncrementTxError Tx -> AppM (Either IncrementTxError Tx)
forall a. a -> AppM a
forall (f :: * -> *) a. Applicative f => a -> f a
pure (Either IncrementTxError Tx -> AppM (Either IncrementTxError Tx))
-> Either IncrementTxError Tx -> AppM (Either IncrementTxError Tx)
forall a b. (a -> b) -> a -> b
$
        ChainContext
-> UTxO
-> HeadId
-> HeadParameters
-> ConfirmedSnapshot Tx
-> TxId
-> SlotNo
-> Either IncrementTxError Tx
increment
          (Actor -> ChainContext
actorChainContext Actor
actor)
          UTxO
spendableUTxO
          (PolicyId -> HeadId
mkHeadId PolicyId
Fixture.testPolicyId)
          HeadParameters
Fixture.testHeadParameters
          ConfirmedSnapshot Tx
snapshot
          TxId
txid
          SlotNo
slotNo

-- | Creates a decrement transaction using given utxo and given snapshot.
newDecrementTx :: Actor -> ConfirmedSnapshot Tx -> AppM (Either DecrementTxError Tx)
newDecrementTx :: Actor -> ConfirmedSnapshot Tx -> AppM (Either DecrementTxError Tx)
newDecrementTx Actor
actor ConfirmedSnapshot Tx
snapshot = do
  (Maybe TxId
_, UTxO
spendableUTxO) <- AppM (Maybe TxId, UTxO)
forall s (m :: * -> *). MonadState s m => m s
get
  Either DecrementTxError Tx -> AppM (Either DecrementTxError Tx)
forall a. a -> AppM a
forall (f :: * -> *) a. Applicative f => a -> f a
pure (Either DecrementTxError Tx -> AppM (Either DecrementTxError Tx))
-> Either DecrementTxError Tx -> AppM (Either DecrementTxError Tx)
forall a b. (a -> b) -> a -> b
$
    ChainContext
-> UTxO
-> HeadId
-> HeadParameters
-> ConfirmedSnapshot Tx
-> Either DecrementTxError Tx
decrement
      (Actor -> ChainContext
actorChainContext Actor
actor)
      UTxO
spendableUTxO
      (PolicyId -> HeadId
mkHeadId PolicyId
Fixture.testPolicyId)
      HeadParameters
Fixture.testHeadParameters
      ConfirmedSnapshot Tx
snapshot

-- | Creates a transaction that closes 'openHeadUTxO' with given the snapshot.
-- NOTE: This uses fixtures for headId, parties (alice, bob, carol),
-- contestation period and also claims to close at time 0 resulting in a
-- contestation deadline of 0 + cperiod.
newCloseTx :: Actor -> SnapshotVersion -> ConfirmedSnapshot Tx -> AppM (Either CloseTxError Tx)
newCloseTx :: Actor
-> SnapshotVersion
-> ConfirmedSnapshot Tx
-> AppM (Either CloseTxError Tx)
newCloseTx Actor
actor SnapshotVersion
openVersion ConfirmedSnapshot Tx
snapshot = do
  (Maybe TxId
_, UTxO
spendableUTxO) <- AppM (Maybe TxId, UTxO)
forall s (m :: * -> *). MonadState s m => m s
get
  Either CloseTxError Tx -> AppM (Either CloseTxError Tx)
forall a. a -> AppM a
forall (f :: * -> *) a. Applicative f => a -> f a
pure (Either CloseTxError Tx -> AppM (Either CloseTxError Tx))
-> Either CloseTxError Tx -> AppM (Either CloseTxError Tx)
forall a b. (a -> b) -> a -> b
$
    ChainContext
-> UTxO
-> HeadId
-> HeadParameters
-> SnapshotVersion
-> ConfirmedSnapshot Tx
-> SlotNo
-> PointInTime
-> Either CloseTxError Tx
close
      (Actor -> ChainContext
actorChainContext Actor
actor)
      UTxO
spendableUTxO
      (PolicyId -> HeadId
mkHeadId PolicyId
Fixture.testPolicyId)
      HeadParameters
Fixture.testHeadParameters
      SnapshotVersion
openVersion
      ConfirmedSnapshot Tx
snapshot
      SlotNo
lowerBound
      PointInTime
upperBound
 where
  lowerBound :: SlotNo
lowerBound = SlotNo
0

  upperBound :: PointInTime
upperBound = (SlotNo
0, POSIXTime -> UTCTime
posixSecondsToUTCTime POSIXTime
0)

-- | Creates a contest transaction using given utxo and contesting with given
-- snapshot. NOTE: This uses fixtures for headId, contestation period and also
-- claims to contest at time 0.
newContestTx :: Actor -> SnapshotVersion -> ConfirmedSnapshot Tx -> AppM (Either ContestTxError Tx)
newContestTx :: Actor
-> SnapshotVersion
-> ConfirmedSnapshot Tx
-> AppM (Either ContestTxError Tx)
newContestTx Actor
actor SnapshotVersion
openVersion ConfirmedSnapshot Tx
snapshot = do
  (Maybe TxId
_, UTxO
spendableUTxO) <- AppM (Maybe TxId, UTxO)
forall s (m :: * -> *). MonadState s m => m s
get
  Either ContestTxError Tx -> AppM (Either ContestTxError Tx)
forall a. a -> AppM a
forall (f :: * -> *) a. Applicative f => a -> f a
pure (Either ContestTxError Tx -> AppM (Either ContestTxError Tx))
-> Either ContestTxError Tx -> AppM (Either ContestTxError Tx)
forall a b. (a -> b) -> a -> b
$
    ChainContext
-> UTxO
-> HeadId
-> ContestationPeriod
-> SnapshotVersion
-> ConfirmedSnapshot Tx
-> PointInTime
-> Either ContestTxError Tx
contest
      (Actor -> ChainContext
actorChainContext Actor
actor)
      UTxO
spendableUTxO
      (PolicyId -> HeadId
mkHeadId PolicyId
Fixture.testPolicyId)
      ContestationPeriod
Fixture.cperiod
      SnapshotVersion
openVersion
      ConfirmedSnapshot Tx
snapshot
      PointInTime
currentTime
 where
  currentTime :: PointInTime
currentTime = (SlotNo
0, POSIXTime -> UTCTime
posixSecondsToUTCTime POSIXTime
0)

-- | Creates a fanout transaction using given utxo. NOTE: This uses fixtures for
-- seedTxIn and contestation period. Consequently, the lower bound used is
-- precisely at the maximum deadline slot as if everyone contested.
newFanoutTx :: Actor -> ModelUTxO -> ModelUTxO -> ModelUTxO -> AppM (Either FanoutTxError Tx)
newFanoutTx :: Actor
-> ModelUTxO
-> ModelUTxO
-> ModelUTxO
-> AppM (Either FanoutTxError Tx)
newFanoutTx Actor
actor ModelUTxO
utxo ModelUTxO
pendingCommit ModelUTxO
pendingDecommit = do
  (Maybe TxId
_, UTxO
spendableUTxO) <- AppM (Maybe TxId, UTxO)
forall s (m :: * -> *). MonadState s m => m s
get
  Either FanoutTxError Tx -> AppM (Either FanoutTxError Tx)
forall a. a -> AppM a
forall (f :: * -> *) a. Applicative f => a -> f a
pure (Either FanoutTxError Tx -> AppM (Either FanoutTxError Tx))
-> Either FanoutTxError Tx -> AppM (Either FanoutTxError Tx)
forall a b. (a -> b) -> a -> b
$
    ChainContext
-> UTxO
-> TxIn
-> UTxO
-> Maybe UTxO
-> Maybe UTxO
-> SlotNo
-> Either FanoutTxError Tx
fanout
      (Actor -> ChainContext
actorChainContext Actor
actor)
      UTxO
spendableUTxO
      TxIn
Fixture.testSeedInput
      (ModelUTxO -> UTxO
realWorldModelUTxO ModelUTxO
utxo)
      -- Model world has no 'Maybe ModelUTxO', but real world does.
      (if ModelUTxO -> Bool
forall a. [a] -> Bool
forall (t :: * -> *) a. Foldable t => t a -> Bool
null ModelUTxO
pendingCommit then Maybe UTxO
forall a. Maybe a
Nothing else UTxO -> Maybe UTxO
forall a. a -> Maybe a
Just (UTxO -> Maybe UTxO) -> UTxO -> Maybe UTxO
forall a b. (a -> b) -> a -> b
$ ModelUTxO -> UTxO
realWorldModelUTxO ModelUTxO
pendingCommit)
      (if ModelUTxO -> Bool
forall a. [a] -> Bool
forall (t :: * -> *) a. Foldable t => t a -> Bool
null ModelUTxO
pendingDecommit then Maybe UTxO
forall a. Maybe a
Nothing else UTxO -> Maybe UTxO
forall a. a -> Maybe a
Just (UTxO -> Maybe UTxO) -> UTxO -> Maybe UTxO
forall a b. (a -> b) -> a -> b
$ ModelUTxO -> UTxO
realWorldModelUTxO ModelUTxO
pendingDecommit)
      SlotNo
deadline
 where
  CP.UnsafeContestationPeriod Nat
contestationPeriod = ContestationPeriod
Fixture.cperiod
  deadline :: SlotNo
deadline = Word64 -> SlotNo
SlotNo (Word64 -> SlotNo) -> Word64 -> SlotNo
forall a b. (a -> b) -> a -> b
$ Nat -> Word64
forall a b. (Integral a, Num b) => a -> b
fromIntegral Nat
contestationPeriod Word64 -> Word64 -> Word64
forall a. Num a => a -> a -> a
* Int -> Word64
forall a b. (Integral a, Num b) => a -> b
fromIntegral ([Actor] -> Int
forall a. [a] -> Int
forall (t :: * -> *) a. Foldable t => t a -> Int
length [Actor]
allActors)

-- | Cardano payment keys for 'alice', 'bob', and 'carol'.
alicePVk, bobPVk, carolPVk :: VerificationKey PaymentKey
alicePVk :: VerificationKey PaymentKey
alicePVk = Gen (VerificationKey PaymentKey)
genVerificationKey Gen (VerificationKey PaymentKey)
-> Party -> VerificationKey PaymentKey
forall a. Gen a -> Party -> a
`genForParty` Party
alice
bobPVk :: VerificationKey PaymentKey
bobPVk = Gen (VerificationKey PaymentKey)
genVerificationKey Gen (VerificationKey PaymentKey)
-> Party -> VerificationKey PaymentKey
forall a. Gen a -> Party -> a
`genForParty` Party
bob
carolPVk :: VerificationKey PaymentKey
carolPVk = Gen (VerificationKey PaymentKey)
genVerificationKey Gen (VerificationKey PaymentKey)
-> Party -> VerificationKey PaymentKey
forall a. Gen a -> Party -> a
`genForParty` Party
carol

-- | Fixture for the chain context of a model 'Actor' on 'testNetworkId'. Uses a generated 'ScriptRegistry'.
actorChainContext :: Actor -> ChainContext
actorChainContext :: Actor -> ChainContext
actorChainContext Actor
actor =
  ChainContext
    { $sel:networkId:ChainContext :: NetworkId
networkId = NetworkId
testNetworkId
    , $sel:ownVerificationKey:ChainContext :: VerificationKey PaymentKey
ownVerificationKey =
        case Actor
actor of
          Actor
Alice -> VerificationKey PaymentKey
alicePVk
          Actor
Bob -> VerificationKey PaymentKey
bobPVk
          Actor
Carol -> VerificationKey PaymentKey
carolPVk
    , $sel:ownParty:ChainContext :: Party
ownParty =
        case Actor
actor of
          Actor
Alice -> Party
alice
          Actor
Bob -> Party
bob
          Actor
Carol -> Party
carol
    , $sel:scriptRegistry:ChainContext :: ScriptRegistry
scriptRegistry = ScriptRegistry
testScriptRegistry
    }

testScriptRegistry :: ScriptRegistry
testScriptRegistry :: ScriptRegistry
testScriptRegistry = Gen ScriptRegistry
genScriptRegistry Gen ScriptRegistry -> Int -> ScriptRegistry
forall a. Gen a -> Int -> a
`generateWith` Int
42

-- * Helpers

-- | Run a short-cutting variant of PostconditionM which produces 'True' if it
-- reaches the end, or 'False' if 'fail' is used.
runPostconditionM' :: Monad m => PostconditionM' m () -> PostconditionM m Bool
runPostconditionM' :: forall (m :: * -> *).
Monad m =>
PostconditionM' m () -> PostconditionM m Bool
runPostconditionM' (PostconditionM' ExceptT (Maybe String) (PostconditionM m) ()
action) =
  ExceptT (Maybe String) (PostconditionM m) ()
-> PostconditionM m (Either (Maybe String) ())
forall e (m :: * -> *) a. ExceptT e m a -> m (Either e a)
runExceptT ExceptT (Maybe String) (PostconditionM m) ()
action PostconditionM m (Either (Maybe String) ())
-> (Either (Maybe String) () -> PostconditionM m Bool)
-> PostconditionM m Bool
forall a b.
PostconditionM m a
-> (a -> PostconditionM m b) -> PostconditionM m b
forall (m :: * -> *) a b. Monad m => m a -> (a -> m b) -> m b
>>= \case
    Left Maybe String
Nothing -> Bool -> PostconditionM m Bool
forall a. a -> PostconditionM m a
forall (f :: * -> *) a. Applicative f => a -> f a
pure Bool
True
    Left (Just String
err) -> String -> PostconditionM m ()
forall (m :: * -> *). Monad m => String -> PostconditionM m ()
counterexamplePost String
err PostconditionM m () -> Bool -> PostconditionM m Bool
forall (f :: * -> *) a b. Functor f => f a -> b -> f b
$> Bool
False
    Right () -> Bool -> PostconditionM m Bool
forall a. a -> PostconditionM m a
forall (f :: * -> *) a. Applicative f => a -> f a
pure Bool
True

newtype PostconditionM' m a = PostconditionM' (ExceptT (Maybe String) (PostconditionM m) a)
  deriving newtype ((forall a b.
 (a -> b) -> PostconditionM' m a -> PostconditionM' m b)
-> (forall a b. a -> PostconditionM' m b -> PostconditionM' m a)
-> Functor (PostconditionM' m)
forall a b. a -> PostconditionM' m b -> PostconditionM' m a
forall a b. (a -> b) -> PostconditionM' m a -> PostconditionM' m b
forall (m :: * -> *) a b.
Functor m =>
a -> PostconditionM' m b -> PostconditionM' m a
forall (m :: * -> *) a b.
Functor m =>
(a -> b) -> PostconditionM' m a -> PostconditionM' m b
forall (f :: * -> *).
(forall a b. (a -> b) -> f a -> f b)
-> (forall a b. a -> f b -> f a) -> Functor f
$cfmap :: forall (m :: * -> *) a b.
Functor m =>
(a -> b) -> PostconditionM' m a -> PostconditionM' m b
fmap :: forall a b. (a -> b) -> PostconditionM' m a -> PostconditionM' m b
$c<$ :: forall (m :: * -> *) a b.
Functor m =>
a -> PostconditionM' m b -> PostconditionM' m a
<$ :: forall a b. a -> PostconditionM' m b -> PostconditionM' m a
Functor, Functor (PostconditionM' m)
Functor (PostconditionM' m) =>
(forall a. a -> PostconditionM' m a)
-> (forall a b.
    PostconditionM' m (a -> b)
    -> PostconditionM' m a -> PostconditionM' m b)
-> (forall a b c.
    (a -> b -> c)
    -> PostconditionM' m a
    -> PostconditionM' m b
    -> PostconditionM' m c)
-> (forall a b.
    PostconditionM' m a -> PostconditionM' m b -> PostconditionM' m b)
-> (forall a b.
    PostconditionM' m a -> PostconditionM' m b -> PostconditionM' m a)
-> Applicative (PostconditionM' m)
forall a. a -> PostconditionM' m a
forall a b.
PostconditionM' m a -> PostconditionM' m b -> PostconditionM' m a
forall a b.
PostconditionM' m a -> PostconditionM' m b -> PostconditionM' m b
forall a b.
PostconditionM' m (a -> b)
-> PostconditionM' m a -> PostconditionM' m b
forall a b c.
(a -> b -> c)
-> PostconditionM' m a
-> PostconditionM' m b
-> PostconditionM' m c
forall (m :: * -> *). Monad m => Functor (PostconditionM' m)
forall (m :: * -> *) a. Monad m => a -> PostconditionM' m a
forall (m :: * -> *) a b.
Monad m =>
PostconditionM' m a -> PostconditionM' m b -> PostconditionM' m a
forall (m :: * -> *) a b.
Monad m =>
PostconditionM' m a -> PostconditionM' m b -> PostconditionM' m b
forall (m :: * -> *) a b.
Monad m =>
PostconditionM' m (a -> b)
-> PostconditionM' m a -> PostconditionM' m b
forall (m :: * -> *) a b c.
Monad m =>
(a -> b -> c)
-> PostconditionM' m a
-> PostconditionM' m b
-> PostconditionM' m c
forall (f :: * -> *).
Functor f =>
(forall a. a -> f a)
-> (forall a b. f (a -> b) -> f a -> f b)
-> (forall a b c. (a -> b -> c) -> f a -> f b -> f c)
-> (forall a b. f a -> f b -> f b)
-> (forall a b. f a -> f b -> f a)
-> Applicative f
$cpure :: forall (m :: * -> *) a. Monad m => a -> PostconditionM' m a
pure :: forall a. a -> PostconditionM' m a
$c<*> :: forall (m :: * -> *) a b.
Monad m =>
PostconditionM' m (a -> b)
-> PostconditionM' m a -> PostconditionM' m b
<*> :: forall a b.
PostconditionM' m (a -> b)
-> PostconditionM' m a -> PostconditionM' m b
$cliftA2 :: forall (m :: * -> *) a b c.
Monad m =>
(a -> b -> c)
-> PostconditionM' m a
-> PostconditionM' m b
-> PostconditionM' m c
liftA2 :: forall a b c.
(a -> b -> c)
-> PostconditionM' m a
-> PostconditionM' m b
-> PostconditionM' m c
$c*> :: forall (m :: * -> *) a b.
Monad m =>
PostconditionM' m a -> PostconditionM' m b -> PostconditionM' m b
*> :: forall a b.
PostconditionM' m a -> PostconditionM' m b -> PostconditionM' m b
$c<* :: forall (m :: * -> *) a b.
Monad m =>
PostconditionM' m a -> PostconditionM' m b -> PostconditionM' m a
<* :: forall a b.
PostconditionM' m a -> PostconditionM' m b -> PostconditionM' m a
Applicative, Applicative (PostconditionM' m)
Applicative (PostconditionM' m) =>
(forall a. PostconditionM' m a)
-> (forall a.
    PostconditionM' m a -> PostconditionM' m a -> PostconditionM' m a)
-> (forall a. PostconditionM' m a -> PostconditionM' m [a])
-> (forall a. PostconditionM' m a -> PostconditionM' m [a])
-> Alternative (PostconditionM' m)
forall a. PostconditionM' m a
forall a. PostconditionM' m a -> PostconditionM' m [a]
forall a.
PostconditionM' m a -> PostconditionM' m a -> PostconditionM' m a
forall (m :: * -> *). Monad m => Applicative (PostconditionM' m)
forall (m :: * -> *) a. Monad m => PostconditionM' m a
forall (m :: * -> *) a.
Monad m =>
PostconditionM' m a -> PostconditionM' m [a]
forall (m :: * -> *) a.
Monad m =>
PostconditionM' m a -> PostconditionM' m a -> PostconditionM' m a
forall (f :: * -> *).
Applicative f =>
(forall a. f a)
-> (forall a. f a -> f a -> f a)
-> (forall a. f a -> f [a])
-> (forall a. f a -> f [a])
-> Alternative f
$cempty :: forall (m :: * -> *) a. Monad m => PostconditionM' m a
empty :: forall a. PostconditionM' m a
$c<|> :: forall (m :: * -> *) a.
Monad m =>
PostconditionM' m a -> PostconditionM' m a -> PostconditionM' m a
<|> :: forall a.
PostconditionM' m a -> PostconditionM' m a -> PostconditionM' m a
$csome :: forall (m :: * -> *) a.
Monad m =>
PostconditionM' m a -> PostconditionM' m [a]
some :: forall a. PostconditionM' m a -> PostconditionM' m [a]
$cmany :: forall (m :: * -> *) a.
Monad m =>
PostconditionM' m a -> PostconditionM' m [a]
many :: forall a. PostconditionM' m a -> PostconditionM' m [a]
Alternative, Applicative (PostconditionM' m)
Applicative (PostconditionM' m) =>
(forall a b.
 PostconditionM' m a
 -> (a -> PostconditionM' m b) -> PostconditionM' m b)
-> (forall a b.
    PostconditionM' m a -> PostconditionM' m b -> PostconditionM' m b)
-> (forall a. a -> PostconditionM' m a)
-> Monad (PostconditionM' m)
forall a. a -> PostconditionM' m a
forall a b.
PostconditionM' m a -> PostconditionM' m b -> PostconditionM' m b
forall a b.
PostconditionM' m a
-> (a -> PostconditionM' m b) -> PostconditionM' m b
forall (m :: * -> *). Monad m => Applicative (PostconditionM' m)
forall (m :: * -> *) a. Monad m => a -> PostconditionM' m a
forall (m :: * -> *) a b.
Monad m =>
PostconditionM' m a -> PostconditionM' m b -> PostconditionM' m b
forall (m :: * -> *) a b.
Monad m =>
PostconditionM' m a
-> (a -> PostconditionM' m b) -> PostconditionM' m b
forall (m :: * -> *).
Applicative m =>
(forall a b. m a -> (a -> m b) -> m b)
-> (forall a b. m a -> m b -> m b)
-> (forall a. a -> m a)
-> Monad m
$c>>= :: forall (m :: * -> *) a b.
Monad m =>
PostconditionM' m a
-> (a -> PostconditionM' m b) -> PostconditionM' m b
>>= :: forall a b.
PostconditionM' m a
-> (a -> PostconditionM' m b) -> PostconditionM' m b
$c>> :: forall (m :: * -> *) a b.
Monad m =>
PostconditionM' m a -> PostconditionM' m b -> PostconditionM' m b
>> :: forall a b.
PostconditionM' m a -> PostconditionM' m b -> PostconditionM' m b
$creturn :: forall (m :: * -> *) a. Monad m => a -> PostconditionM' m a
return :: forall a. a -> PostconditionM' m a
Monad)

instance Monad m => MonadFail (PostconditionM' m) where
  fail :: forall a. String -> PostconditionM' m a
fail = ExceptT (Maybe String) (PostconditionM m) a -> PostconditionM' m a
forall (m :: * -> *) a.
ExceptT (Maybe String) (PostconditionM m) a -> PostconditionM' m a
PostconditionM' (ExceptT (Maybe String) (PostconditionM m) a
 -> PostconditionM' m a)
-> (String -> ExceptT (Maybe String) (PostconditionM m) a)
-> String
-> PostconditionM' m a
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Maybe String -> ExceptT (Maybe String) (PostconditionM m) a
forall a.
Maybe String -> ExceptT (Maybe String) (PostconditionM m) a
forall e (m :: * -> *) a. MonadError e m => e -> m a
throwError (Maybe String -> ExceptT (Maybe String) (PostconditionM m) a)
-> (String -> Maybe String)
-> String
-> ExceptT (Maybe String) (PostconditionM m) a
forall b c a. (b -> c) -> (a -> b) -> a -> c
. String -> Maybe String
forall a. a -> Maybe a
Just

-- | Short-cut a postcondition monad like 'fail', but in a successful way. This
-- is useful to not have unrelated counterexample' outputs.
fulfilled :: Monad m => PostconditionM' m ()
fulfilled :: forall (m :: * -> *). Monad m => PostconditionM' m ()
fulfilled = ExceptT (Maybe String) (PostconditionM m) ()
-> PostconditionM' m ()
forall (m :: * -> *) a.
ExceptT (Maybe String) (PostconditionM m) a -> PostconditionM' m a
PostconditionM' (ExceptT (Maybe String) (PostconditionM m) ()
 -> PostconditionM' m ())
-> ExceptT (Maybe String) (PostconditionM m) ()
-> PostconditionM' m ()
forall a b. (a -> b) -> a -> b
$ Maybe String -> ExceptT (Maybe String) (PostconditionM m) ()
forall a.
Maybe String -> ExceptT (Maybe String) (PostconditionM m) a
forall e (m :: * -> *) a. MonadError e m => e -> m a
throwError Maybe String
forall a. Maybe a
Nothing

-- | Add given message in case the postcondition fails.
counterexample' :: Monad m => String -> PostconditionM' m ()
counterexample' :: forall (m :: * -> *). Monad m => String -> PostconditionM' m ()
counterexample' String
msg = ExceptT (Maybe String) (PostconditionM m) ()
-> PostconditionM' m ()
forall (m :: * -> *) a.
ExceptT (Maybe String) (PostconditionM m) a -> PostconditionM' m a
PostconditionM' (ExceptT (Maybe String) (PostconditionM m) ()
 -> PostconditionM' m ())
-> ExceptT (Maybe String) (PostconditionM m) ()
-> PostconditionM' m ()
forall a b. (a -> b) -> a -> b
$ PostconditionM m (Either (Maybe String) ())
-> ExceptT (Maybe String) (PostconditionM m) ()
forall e (m :: * -> *) a. m (Either e a) -> ExceptT e m a
ExceptT (PostconditionM m (Either (Maybe String) ())
 -> ExceptT (Maybe String) (PostconditionM m) ())
-> PostconditionM m (Either (Maybe String) ())
-> ExceptT (Maybe String) (PostconditionM m) ()
forall a b. (a -> b) -> a -> b
$ String -> PostconditionM m ()
forall (m :: * -> *). Monad m => String -> PostconditionM m ()
counterexamplePost String
msg PostconditionM m ()
-> Either (Maybe String) ()
-> PostconditionM m (Either (Maybe String) ())
forall (f :: * -> *) a b. Functor f => f a -> b -> f b
$> () -> Either (Maybe String) ()
forall a b. b -> Either a b
Right ()

-- | Assertion helper to check whether a 'TxResult' was valid and the expected
-- 'HeadObservation' could be made. To be used in 'postcondition'.
expectValid :: Monad m => TxResult -> (HeadObservation -> PostconditionM' m a) -> PostconditionM' m a
expectValid :: forall (m :: * -> *) a.
Monad m =>
TxResult
-> (HeadObservation -> PostconditionM' m a) -> PostconditionM' m a
expectValid TxResult{$sel:validationError:TxResult :: TxResult -> Maybe String
validationError = Just String
err} HeadObservation -> PostconditionM' m a
_ = do
  String -> PostconditionM' m ()
forall (m :: * -> *). Monad m => String -> PostconditionM' m ()
counterexample' String
"Expected to pass validation"
  String -> PostconditionM' m a
forall a. String -> PostconditionM' m a
forall (m :: * -> *) a. MonadFail m => String -> m a
fail String
err
expectValid TxResult{HeadObservation
$sel:observation:TxResult :: TxResult -> HeadObservation
observation :: HeadObservation
observation, Either String Tx
$sel:constructedTx:TxResult :: TxResult -> Either String Tx
constructedTx :: Either String Tx
constructedTx, UTxO
$sel:spendableUTxO:TxResult :: TxResult -> UTxO
spendableUTxO :: UTxO
spendableUTxO} HeadObservation -> PostconditionM' m a
fn = do
  case Either String Tx
constructedTx of
    Left String
err -> String -> PostconditionM' m ()
forall (m :: * -> *). Monad m => String -> PostconditionM' m ()
counterexample' (String -> PostconditionM' m ()) -> String -> PostconditionM' m ()
forall a b. (a -> b) -> a -> b
$ String
"But construction failed with: " String -> ShowS
forall a. Semigroup a => a -> a -> a
<> String
err
    Right Tx
tx -> do
      String -> PostconditionM' m ()
forall (m :: * -> *). Monad m => String -> PostconditionM' m ()
counterexample' (String -> PostconditionM' m ()) -> String -> PostconditionM' m ()
forall a b. (a -> b) -> a -> b
$ UTxO -> Tx -> String
renderTxWithUTxO UTxO
spendableUTxO Tx
tx
  String -> PostconditionM' m ()
forall (m :: * -> *). Monad m => String -> PostconditionM' m ()
counterexample' (String -> PostconditionM' m ()) -> String -> PostconditionM' m ()
forall a b. (a -> b) -> a -> b
$ String
"Wrong observation: " String -> ShowS
forall a. Semigroup a => a -> a -> a
<> HeadObservation -> String
forall a. Show a => a -> String
show HeadObservation
observation
  HeadObservation -> PostconditionM' m a
fn HeadObservation
observation

-- | Assertion helper to check whether a 'TxResult' was invalid or construction failed.
expectInvalid :: Monad m => TxResult -> PostconditionM' m ()
expectInvalid :: forall (m :: * -> *). Monad m => TxResult -> PostconditionM' m ()
expectInvalid = \case
  TxResult{$sel:validationError:TxResult :: TxResult -> Maybe String
validationError = Maybe String
Nothing, Either String Tx
$sel:constructedTx:TxResult :: TxResult -> Either String Tx
constructedTx :: Either String Tx
constructedTx, UTxO
$sel:spendableUTxO:TxResult :: TxResult -> UTxO
spendableUTxO :: UTxO
spendableUTxO} -> do
    case Either String Tx
constructedTx of
      Left String
_ -> () -> PostconditionM' m ()
forall a. a -> PostconditionM' m a
forall (f :: * -> *) a. Applicative f => a -> f a
pure ()
      Right Tx
tx -> do
        String -> PostconditionM' m ()
forall (m :: * -> *). Monad m => String -> PostconditionM' m ()
counterexample' String
"Expected tx to fail validation"
        String -> PostconditionM' m ()
forall (m :: * -> *). Monad m => String -> PostconditionM' m ()
counterexample' (String -> PostconditionM' m ()) -> String -> PostconditionM' m ()
forall a b. (a -> b) -> a -> b
$ UTxO -> Tx -> String
renderTxWithUTxO UTxO
spendableUTxO Tx
tx
        String -> PostconditionM' m ()
forall a. String -> PostconditionM' m a
forall (m :: * -> *) a. MonadFail m => String -> m a
fail String
"But it did not fail"
  TxResult
_ -> () -> PostconditionM' m ()
forall a. a -> PostconditionM' m a
forall (f :: * -> *) a. Applicative f => a -> f a
pure ()