{-# 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 right now. It generates plausible sequences of Decrement and Close
-- actions, along with Contest and Fanout, each using a snapshot of some version
-- and number. UTxOs are simplified such that their identity is A-E and value is
-- just a number.
--
-- Actions and snapshots are generated "just-in-time" and result in valid, but
-- also deliberately invalid combinations of versions/numbers. Generated
-- snapshots are correctly signed and consistent in what they decommit from the
-- head.
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 Cardano.Ledger.Coin (Coin (..))
import Data.Map.Strict qualified as Map
import Data.Time.Clock.POSIX (posixSecondsToUTCTime)
import GHC.Natural (naturalFromInteger, naturalToInteger)
import Hydra.Cardano.Api (
  PaymentKey,
  SlotNo (..),
  VerificationKey,
  lovelaceToValue,
  mkTxOutDatumInline,
  modifyTxOutValue,
  selectLovelace,
  throwError,
  txOutAddress,
  txOutValue,
 )
import Hydra.Cardano.Api.Pretty (renderTxWithUTxO)
import Hydra.Chain.Direct.State (
  ChainContext (..),
  CloseTxError,
  ContestTxError,
  DecrementTxError,
  FanoutTxError,
  close,
  contest,
  decrement,
  fanout,
 )
import Hydra.Chain.Direct.Tx (
  HeadObservation (NoHeadTx),
  observeHeadTx,
 )
import Hydra.Chain.Direct.Tx qualified as Tx
import Hydra.Contract.HeadState qualified as Head
import Hydra.Ledger.Cardano (Tx, adjustUTxO)
import Hydra.Ledger.Cardano.Evaluate (evaluateTx)
import Hydra.Tx.ContestationPeriod qualified as CP
import Hydra.Tx.Crypto (MultiSignature, aggregate, sign)
import Hydra.Tx.HeadId (headIdToCurrencySymbol, mkHeadId)
import Hydra.Tx.Init (mkHeadOutput)
import Hydra.Tx.IsTx (hashUTxO, utxoFromTx)
import Hydra.Tx.Party (partyToChain)
import Hydra.Tx.ScriptRegistry (ScriptRegistry, registryUTxO)
import Hydra.Tx.Snapshot (ConfirmedSnapshot (..), Snapshot (..), SnapshotNumber (..), SnapshotVersion (..), 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 (Property, Smart (..), choose, cover, elements, forAll, frequency, ioProperty, oneof, shuffle, sublistOf, (===))
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 -> Property -> Spec
forall prop.
(HasCallStack, Testable prop) =>
String -> prop -> Spec
prop String
"generates interesting transaction traces" Property
prop_traces
  String -> (Actions Model -> Property) -> Spec
forall prop.
(HasCallStack, Testable prop) =>
String -> prop -> Spec
prop String
"all valid transactions" Actions Model -> Property
prop_runActions
  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)

prop_traces :: Property
prop_traces :: Property
prop_traces =
  Gen (Actions Model) -> (Actions Model -> Property) -> Property
forall a prop.
(Show a, Testable prop) =>
Gen a -> (a -> prop) -> Property
forAll (Gen (Actions Model)
forall a. Arbitrary a => Gen a
arbitrary :: Gen (Actions Model)) ((Actions Model -> Property) -> Property)
-> (Actions Model -> Property) -> Property
forall a b. (a -> b) -> a -> b
$ \(Actions_ [String]
_ (Smart Int
_ [Step Model]
steps)) ->
    -- FIXME: fix generators and minimums and re-enable coverage
    -- checkCoverage $
    Bool
True
      Bool -> (Bool -> Property) -> Property
forall a b. a -> (a -> b) -> b
& Double -> Bool -> String -> Bool -> 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
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
1 ([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
0.5 ([Step Model] -> Bool
fanoutWithEmptyUTxO [Step Model]
steps) String
"fanout with empty 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
1 ([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
0.5 ([Step Model] -> Bool
fanoutWithDelta [Step Model]
steps) String
"fanout with additional UTxO to distribute"
 where
  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. Map SingleUTxO a -> Bool
forall (t :: * -> *) a. Foldable t => t a -> Bool
null (ModelUTxO -> Bool) -> ModelUTxO -> Bool
forall a b. (a -> b) -> a -> b
$ ModelSnapshot -> ModelUTxO
decommitUTxO 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 :: 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
        Fanout{} -> Polarity
polarity Polarity -> Polarity -> Bool
forall a. Eq a => a -> a -> Bool
== Polarity
PosPolarity
        Action Model a
_ -> Bool
False

  fanoutWithEmptyUTxO :: [Step Model] -> Bool
fanoutWithEmptyUTxO =
    (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:Decrement :: Action Model TxResult -> ModelUTxO
utxo} ->
          Polarity
polarity Polarity -> Polarity -> Bool
forall a. Eq a => a -> a -> Bool
== Polarity
PosPolarity
            Bool -> Bool -> Bool
&& ModelUTxO -> Bool
forall a. Map SingleUTxO a -> Bool
forall (t :: * -> *) a. Foldable t => t a -> Bool
null ModelUTxO
utxo
        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
$sel:utxo:Decrement :: Action Model TxResult -> ModelUTxO
utxo :: 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. Map SingleUTxO a -> Bool
forall (t :: * -> *) a. Foldable t => t a -> Bool
null ModelUTxO
utxo)
        Action Model a
_ -> Bool
False

  fanoutWithDelta :: [Step Model] -> Bool
fanoutWithDelta =
    (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
deltaUTxO :: ModelUTxO
$sel:deltaUTxO:Decrement :: Action Model TxResult -> ModelUTxO
deltaUTxO} ->
          Polarity
polarity Polarity -> Polarity -> Bool
forall a. Eq a => a -> a -> Bool
== Polarity
PosPolarity
            Bool -> Bool -> Bool
&& Bool -> Bool
not (ModelUTxO -> Bool
forall a. Map SingleUTxO a -> Bool
forall (t :: * -> *) a. Foldable t => t a -> Bool
null ModelUTxO
deltaUTxO)
        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:Decrement :: Action Model TxResult -> ModelSnapshot
snapshot} -> ModelSnapshot
snapshot ModelSnapshot -> ModelSnapshot -> Bool
forall a. Ord a => a -> a -> Bool
> ModelSnapshot
0
      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:Decrement :: 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 =
  (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 UTxO
localState <- UTxO -> IO (IORef UTxO)
forall (m :: * -> *) a. MonadIO m => a -> m (IORef a)
newIORef UTxO
openHeadUTxO
    ReaderT (IORef UTxO) IO Property -> IORef UTxO -> IO Property
forall r (m :: * -> *) a. ReaderT r m a -> r -> m a
runReaderT (AppM Property -> ReaderT (IORef UTxO) IO Property
forall a. AppM a -> ReaderT (IORef UTxO) IO a
runAppM AppM Property
action) IORef UTxO
localState

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

data SingleUTxO = A | B | C | D | E
  deriving (Int -> SingleUTxO -> ShowS
[SingleUTxO] -> ShowS
SingleUTxO -> String
(Int -> SingleUTxO -> ShowS)
-> (SingleUTxO -> String)
-> ([SingleUTxO] -> 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 :: [SingleUTxO] -> ShowS
showList :: [SingleUTxO] -> 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 -> [SingleUTxO]
SingleUTxO -> SingleUTxO
SingleUTxO -> SingleUTxO -> [SingleUTxO]
SingleUTxO -> SingleUTxO -> SingleUTxO -> [SingleUTxO]
(SingleUTxO -> SingleUTxO)
-> (SingleUTxO -> SingleUTxO)
-> (Int -> SingleUTxO)
-> (SingleUTxO -> Int)
-> (SingleUTxO -> [SingleUTxO])
-> (SingleUTxO -> SingleUTxO -> [SingleUTxO])
-> (SingleUTxO -> SingleUTxO -> [SingleUTxO])
-> (SingleUTxO -> SingleUTxO -> SingleUTxO -> [SingleUTxO])
-> 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 -> [SingleUTxO]
enumFrom :: SingleUTxO -> [SingleUTxO]
$cenumFromThen :: SingleUTxO -> SingleUTxO -> [SingleUTxO]
enumFromThen :: SingleUTxO -> SingleUTxO -> [SingleUTxO]
$cenumFromTo :: SingleUTxO -> SingleUTxO -> [SingleUTxO]
enumFromTo :: SingleUTxO -> SingleUTxO -> [SingleUTxO]
$cenumFromThenTo :: SingleUTxO -> SingleUTxO -> SingleUTxO -> [SingleUTxO]
enumFromThenTo :: SingleUTxO -> SingleUTxO -> SingleUTxO -> [SingleUTxO]
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 -> [SingleUTxO]
shrink = SingleUTxO -> [SingleUTxO]
forall a.
(Generic a, RecursivelyShrink (Rep a), GSubterms (Rep a) a) =>
a -> [a]
genericShrink

type ModelUTxO = Map SingleUTxO Natural

data Model = Model
  { Model -> State
headState :: State
  , Model -> SnapshotVersion
currentVersion :: SnapshotVersion
  , Model -> SnapshotNumber
latestSnapshot :: SnapshotNumber
  , Model -> [Actor]
alreadyContested :: [Actor]
  , Model -> ModelUTxO
utxoInHead :: ModelUTxO
  , Model -> ModelUTxO
pendingDecommitUTxO :: 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)

-- | 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
snapshotUTxO :: ModelUTxO
  , ModelSnapshot -> ModelUTxO
decommitUTxO :: 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 = Natural -> SnapshotVersion
UnsafeSnapshotVersion Natural
0
      , $sel:number:ModelSnapshot :: SnapshotNumber
number = Natural -> SnapshotNumber
UnsafeSnapshotNumber (Natural -> SnapshotNumber) -> Natural -> SnapshotNumber
forall a b. (a -> b) -> a -> b
$ Natural -> Maybe Natural -> Natural
forall a. a -> Maybe a -> a
fromMaybe Natural
0 (Maybe Natural -> Natural) -> Maybe Natural -> Natural
forall a b. (a -> b) -> a -> b
$ Integer -> Maybe Natural
integerToNatural Integer
x
      , $sel:snapshotUTxO:ModelSnapshot :: ModelUTxO
snapshotUTxO = ModelUTxO
forall a. Monoid a => a
mempty
      , $sel:decommitUTxO:ModelSnapshot :: ModelUTxO
decommitUTxO = ModelUTxO
forall a. Monoid a => a
mempty
      }

instance Arbitrary ModelSnapshot where
  arbitrary :: Gen ModelSnapshot
arbitrary = Gen ModelSnapshot
forall a.
(Generic a, GA UnsizedOpts (Rep a),
 UniformWeight (Weights_ (Rep a))) =>
Gen a
genericArbitrary

  shrink :: ModelSnapshot -> [ModelSnapshot]
shrink = ModelSnapshot -> [ModelSnapshot]
forall a.
(Generic a, RecursivelyShrink (Rep a), GSubterms (Rep a) a) =>
a -> [a]
genericShrink

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)

initialAmount :: Natural
initialAmount :: Natural
initialAmount = Natural
10

initialModelUTxO :: ModelUTxO
initialModelUTxO :: ModelUTxO
initialModelUTxO = [Item ModelUTxO] -> ModelUTxO
forall l. IsList l => [Item l] -> l
fromList ([Item ModelUTxO] -> ModelUTxO) -> [Item ModelUTxO] -> ModelUTxO
forall a b. (a -> b) -> a -> b
$ (SingleUTxO -> (SingleUTxO, Natural))
-> [SingleUTxO] -> [(SingleUTxO, Natural)]
forall a b. (a -> b) -> [a] -> [b]
map (,Natural
initialAmount) [SingleUTxO
A, SingleUTxO
B, SingleUTxO
C, SingleUTxO
D, SingleUTxO
E]

balanceUTxOInHead :: Ord k => Map k Natural -> Map k Natural -> Map k Natural
balanceUTxOInHead :: forall k. Ord k => Map k Natural -> Map k Natural -> Map k Natural
balanceUTxOInHead Map k Natural
currentUtxoInHead Map k Natural
someUTxOToDecrement =
  Map k Natural
currentUtxoInHead Map k Natural -> Map k Natural -> Map k Natural
forall k a b. Ord k => Map k a -> Map k b -> Map k a
`Map.difference` Map k Natural
someUTxOToDecrement

instance StateModel Model where
  data Action Model a where
    Decrement :: {Action Model TxResult -> Actor
actor :: Actor, Action Model TxResult -> ModelSnapshot
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
deltaUTxO :: 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:currentVersion:Model :: SnapshotVersion
currentVersion = SnapshotVersion
0
      , $sel:latestSnapshot:Model :: SnapshotNumber
latestSnapshot = SnapshotNumber
0
      , $sel:alreadyContested:Model :: [Actor]
alreadyContested = []
      , $sel:utxoInHead:Model :: ModelUTxO
utxoInHead = ModelUTxO
initialModelUTxO
      , $sel:pendingDecommitUTxO:Model :: ModelUTxO
pendingDecommitUTxO = ModelUTxO
forall k a. Map k a
Map.empty
      }

  -- FIXME: 1.5k discards on 100 runs

  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, SnapshotVersion
$sel:currentVersion:Model :: Model -> SnapshotVersion
currentVersion :: SnapshotVersion
currentVersion, SnapshotNumber
$sel:latestSnapshot:Model :: Model -> SnapshotNumber
latestSnapshot :: SnapshotNumber
latestSnapshot, ModelUTxO
$sel:utxoInHead:Model :: Model -> ModelUTxO
utxoInHead :: ModelUTxO
utxoInHead, ModelUTxO
$sel:pendingDecommitUTxO:Model :: Model -> ModelUTxO
pendingDecommitUTxO :: ModelUTxO
pendingDecommitUTxO} =
    case State
headState of
      Open{} ->
        [(Int, Gen (Any (Action Model)))] -> Gen (Any (Action Model))
forall a. [(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
            , do
                Actor
actor <- [Actor] -> Gen Actor
forall a. [a] -> Gen a
elements [Actor]
allActors
                ModelSnapshot
snapshot <- Gen ModelSnapshot
genSnapshot
                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:Decrement :: Actor
actor :: Actor
actor, ModelSnapshot
$sel:snapshot:Decrement :: ModelSnapshot
snapshot :: ModelSnapshot
snapshot}
            )
          ]
            [(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
                    Actor
actor <- [Actor] -> Gen Actor
forall a. [a] -> Gen a
elements [Actor]
allActors
                    ModelSnapshot
snapshot <- Gen ModelSnapshot
genSnapshot
                    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:Decrement :: Actor
actor :: Actor
actor, ModelSnapshot
$sel:snapshot:Decrement :: ModelSnapshot
snapshot :: ModelSnapshot
snapshot}
                 )
               | -- We dont want to generate decrements if there is nothing in the head.
               Bool -> Bool
not (ModelUTxO -> Bool
forall a. Map SingleUTxO a -> Bool
forall (t :: * -> *) a. Foldable t => t a -> Bool
null ModelUTxO
utxoInHead)
               ]
      Closed{} ->
        [Gen (Any (Action Model))] -> Gen (Any (Action Model))
forall a. [Gen a] -> Gen a
oneof ([Gen (Any (Action Model))] -> Gen (Any (Action Model)))
-> [Gen (Any (Action Model))] -> Gen (Any (Action Model))
forall a b. (a -> b) -> a -> b
$
          [ do
              -- Fanout with the currently known model state.
              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:Decrement :: ModelUTxO
utxo = ModelUTxO
utxoInHead
                    , $sel:deltaUTxO:Decrement :: ModelUTxO
deltaUTxO = ModelUTxO
pendingDecommitUTxO
                    }
          ]
            [Gen (Any (Action Model))]
-> [Gen (Any (Action Model))] -> [Gen (Any (Action Model))]
forall a. Semigroup a => a -> a -> a
<> [ do
                  Actor
actor <- [Actor] -> Gen Actor
forall a. [a] -> Gen a
elements [Actor]
allActors
                  ModelSnapshot
snapshot <- Gen ModelSnapshot
genSnapshot
                  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:Decrement :: Actor
actor :: Actor
actor, ModelSnapshot
$sel:snapshot:Decrement :: 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
    genSnapshot :: Gen ModelSnapshot
genSnapshot = do
      ModelUTxO
someUTxOToDecrement <- ModelUTxO -> Gen ModelUTxO
reduceValues (ModelUTxO -> Gen ModelUTxO) -> Gen ModelUTxO -> Gen ModelUTxO
forall (m :: * -> *) a b. Monad m => (a -> m b) -> m a -> m b
=<< ModelUTxO -> Gen ModelUTxO
genSubModelOf ModelUTxO
utxoInHead
      let filteredSomeUTxOToDecrement :: ModelUTxO
filteredSomeUTxOToDecrement = (Natural -> Bool) -> ModelUTxO -> ModelUTxO
forall a k. (a -> Bool) -> Map k a -> Map k a
Map.filter (Natural -> Natural -> Bool
forall a. Ord a => a -> a -> Bool
> Natural
0) ModelUTxO
someUTxOToDecrement
      let balancedUTxOInHead :: ModelUTxO
balancedUTxOInHead = ModelUTxO -> ModelUTxO -> ModelUTxO
forall k. Ord k => Map k Natural -> Map k Natural -> Map k Natural
balanceUTxOInHead ModelUTxO
utxoInHead ModelUTxO
filteredSomeUTxOToDecrement

      SnapshotVersion
version <- [SnapshotVersion] -> Gen SnapshotVersion
forall a. [a] -> Gen a
elements ([SnapshotVersion] -> Gen SnapshotVersion)
-> [SnapshotVersion] -> Gen SnapshotVersion
forall a b. (a -> b) -> a -> b
$ 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] [SnapshotVersion] -> [SnapshotVersion] -> [SnapshotVersion]
forall a. Semigroup a => a -> a -> a
<> [SnapshotVersion
currentVersion SnapshotVersion -> SnapshotVersion -> SnapshotVersion
forall a. Num a => a -> a -> a
+ SnapshotVersion
1]
      let validSnapshot :: ModelSnapshot
validSnapshot =
            ModelSnapshot
              { SnapshotVersion
$sel:version:ModelSnapshot :: SnapshotVersion
version :: SnapshotVersion
version
              , $sel:number:ModelSnapshot :: SnapshotNumber
number = SnapshotNumber
latestSnapshot
              , $sel:snapshotUTxO:ModelSnapshot :: ModelUTxO
snapshotUTxO = ModelUTxO
balancedUTxOInHead
              , $sel:decommitUTxO:ModelSnapshot :: ModelUTxO
decommitUTxO = ModelUTxO
filteredSomeUTxOToDecrement
              }
      [Gen ModelSnapshot] -> Gen ModelSnapshot
forall a. [Gen a] -> Gen a
oneof
        [ -- valid
          ModelSnapshot -> Gen ModelSnapshot
forall a. a -> Gen a
forall (f :: * -> *) a. Applicative f => a -> f a
pure ModelSnapshot
validSnapshot
        , -- unbalanced
          ModelSnapshot -> Gen ModelSnapshot
forall a. a -> Gen a
forall (f :: * -> *) a. Applicative f => a -> f a
pure ModelSnapshot
validSnapshot{snapshotUTxO = utxoInHead}
        , do
            -- old
            let number' :: SnapshotNumber
number' = if SnapshotNumber
latestSnapshot SnapshotNumber -> SnapshotNumber -> Bool
forall a. Eq a => a -> a -> Bool
== SnapshotNumber
0 then SnapshotNumber
0 else SnapshotNumber
latestSnapshot SnapshotNumber -> SnapshotNumber -> SnapshotNumber
forall a. Num a => a -> a -> a
- SnapshotNumber
1
            ModelSnapshot -> Gen ModelSnapshot
forall a. a -> Gen a
forall (f :: * -> *) a. Applicative f => a -> f a
pure (ModelSnapshot
validSnapshot :: ModelSnapshot){number = number'}
        , -- new
          ModelSnapshot -> Gen ModelSnapshot
forall a. a -> Gen a
forall (f :: * -> *) a. Applicative f => a -> f a
pure (ModelSnapshot
validSnapshot :: ModelSnapshot){number = latestSnapshot + 1}
        , do
            -- shuffled
            ModelUTxO
someUTxOToDecrement' <- ModelUTxO -> Gen ModelUTxO
shuffleValues ModelUTxO
filteredSomeUTxOToDecrement
            ModelSnapshot -> Gen ModelSnapshot
forall a. a -> Gen a
forall (f :: * -> *) a. Applicative f => a -> f a
pure ModelSnapshot
validSnapshot{decommitUTxO = someUTxOToDecrement'}
        , do
            -- more in head
            ModelUTxO
utxoInHead' <- ModelUTxO -> Gen ModelUTxO
increaseValues ModelUTxO
utxoInHead
            ModelSnapshot -> Gen ModelSnapshot
forall a. a -> Gen a
forall (f :: * -> *) a. Applicative f => a -> f a
pure ModelSnapshot
validSnapshot{snapshotUTxO = utxoInHead'}
        , do
            -- more in decommit
            ModelUTxO
someUTxOToDecrement' <- ModelUTxO -> Gen ModelUTxO
increaseValues (ModelUTxO -> Gen ModelUTxO) -> Gen ModelUTxO -> Gen ModelUTxO
forall (m :: * -> *) a b. Monad m => (a -> m b) -> m a -> m b
=<< ModelUTxO -> Gen ModelUTxO
genSubModelOf ModelUTxO
utxoInHead
            let balancedUTxOInHead' :: ModelUTxO
balancedUTxOInHead' = ModelUTxO -> ModelUTxO -> ModelUTxO
forall k. Ord k => Map k Natural -> Map k Natural -> Map k Natural
balanceUTxOInHead ModelUTxO
utxoInHead ModelUTxO
someUTxOToDecrement'
            ModelSnapshot -> Gen ModelSnapshot
forall a. a -> Gen a
forall (f :: * -> *) a. Applicative f => a -> f a
pure
              ModelSnapshot
validSnapshot
                { snapshotUTxO = balancedUTxOInHead'
                , decommitUTxO = someUTxOToDecrement'
                }
        , -- decommit all
          ModelSnapshot -> Gen ModelSnapshot
forall a. a -> Gen a
forall (f :: * -> *) a. Applicative f => a -> f a
pure ModelSnapshot
validSnapshot{snapshotUTxO = mempty, decommitUTxO = utxoInHead}
        , Gen ModelSnapshot
forall a. Arbitrary a => Gen a
arbitrary
        ]

    genSubModelOf :: ModelUTxO -> Gen ModelUTxO
    genSubModelOf :: ModelUTxO -> Gen ModelUTxO
genSubModelOf ModelUTxO
model = do
      [(SingleUTxO, Natural)]
subset <- [(SingleUTxO, Natural)] -> Gen [(SingleUTxO, Natural)]
forall a. [a] -> Gen [a]
sublistOf (ModelUTxO -> [(SingleUTxO, Natural)]
forall k a. Map k a -> [(k, a)]
Map.toList ModelUTxO
model)
      ModelUTxO -> Gen ModelUTxO
forall a. a -> Gen a
forall (m :: * -> *) a. Monad m => a -> m a
return (ModelUTxO -> Gen ModelUTxO) -> ModelUTxO -> Gen ModelUTxO
forall a b. (a -> b) -> a -> b
$ [(SingleUTxO, Natural)] -> ModelUTxO
forall k a. Ord k => [(k, a)] -> Map k a
Map.fromList [(SingleUTxO, Natural)]
subset

    reduceValues :: ModelUTxO -> Gen ModelUTxO
    reduceValues :: ModelUTxO -> Gen ModelUTxO
reduceValues = (SingleUTxO -> Natural -> Gen Natural)
-> ModelUTxO -> Gen ModelUTxO
forall (t :: * -> *) k a b.
Applicative t =>
(k -> a -> t b) -> Map k a -> t (Map k b)
Map.traverseWithKey SingleUTxO -> Natural -> Gen Natural
reduceValue
     where
      reduceValue :: SingleUTxO -> Natural -> Gen Natural
      reduceValue :: SingleUTxO -> Natural -> Gen Natural
reduceValue SingleUTxO
_ Natural
n = do
        let n' :: Integer
n' = Natural -> Integer
naturalToInteger Natural
n
        Integer
reduction <- (Integer, Integer) -> Gen Integer
forall a. Random a => (a, a) -> Gen a
choose (Integer
0, Integer
n')
        let reduced :: Integer
reduced = if Integer
n' Integer -> Integer -> Bool
forall a. Ord a => a -> a -> Bool
< Integer
reduction then Integer
0 else Integer
n' Integer -> Integer -> Integer
forall a. Num a => a -> a -> a
- Integer
reduction
        Natural -> Gen Natural
forall a. a -> Gen a
forall (m :: * -> *) a. Monad m => a -> m a
return (Integer -> Natural
naturalFromInteger Integer
reduced)

    increaseValues :: ModelUTxO -> Gen ModelUTxO
    increaseValues :: ModelUTxO -> Gen ModelUTxO
increaseValues = (SingleUTxO -> Natural -> Gen Natural)
-> ModelUTxO -> Gen ModelUTxO
forall (t :: * -> *) k a b.
Applicative t =>
(k -> a -> t b) -> Map k a -> t (Map k b)
Map.traverseWithKey (\SingleUTxO
_ Natural
n -> Natural -> Gen Natural
forall a. a -> Gen a
forall (f :: * -> *) a. Applicative f => a -> f a
pure (Natural
n Natural -> Natural -> Natural
forall a. Num a => a -> a -> a
+ Integer -> Natural
naturalFromInteger Integer
1))

    shuffleValues :: ModelUTxO -> Gen ModelUTxO
    shuffleValues :: ModelUTxO -> Gen ModelUTxO
shuffleValues ModelUTxO
utxo = do
      let x :: [SingleUTxO]
x = ModelUTxO -> [SingleUTxO]
forall k a. Map k a -> [k]
Map.keys ModelUTxO
utxo
      let y :: [Natural]
y = ModelUTxO -> [Natural]
forall k a. Map k a -> [a]
Map.elems ModelUTxO
utxo
      [SingleUTxO]
x' <- [SingleUTxO] -> Gen [SingleUTxO]
forall a. [a] -> Gen [a]
shuffle [SingleUTxO]
x
      let shuffledUTxO :: ModelUTxO
shuffledUTxO = [(SingleUTxO, Natural)] -> ModelUTxO
forall k a. Ord k => [(k, a)] -> Map k a
Map.fromList ([(SingleUTxO, Natural)] -> ModelUTxO)
-> [(SingleUTxO, Natural)] -> ModelUTxO
forall a b. (a -> b) -> a -> b
$ [SingleUTxO] -> [Natural] -> [(SingleUTxO, Natural)]
forall a b. [a] -> [b] -> [(a, b)]
zip [SingleUTxO]
x' [Natural]
y
      ModelUTxO -> Gen ModelUTxO
forall a. a -> Gen a
forall (f :: * -> *) a. Applicative f => a -> f a
pure ModelUTxO
shuffledUTxO

  -- 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, SnapshotNumber
$sel:latestSnapshot:Model :: Model -> SnapshotNumber
latestSnapshot :: SnapshotNumber
latestSnapshot, [Actor]
$sel:alreadyContested:Model :: Model -> [Actor]
alreadyContested :: [Actor]
alreadyContested, ModelUTxO
$sel:utxoInHead:Model :: Model -> ModelUTxO
utxoInHead :: ModelUTxO
utxoInHead, ModelUTxO
$sel:pendingDecommitUTxO:Model :: Model -> ModelUTxO
pendingDecommitUTxO :: ModelUTxO
pendingDecommitUTxO, SnapshotVersion
$sel:currentVersion:Model :: Model -> SnapshotVersion
currentVersion :: SnapshotVersion
currentVersion} = \case
    Action Model a
R:ActionModela a
Stop -> State
headState State -> State -> Bool
forall a. Eq a => a -> a -> Bool
/= State
Final
    Decrement{ModelSnapshot
$sel:snapshot:Decrement :: 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.version SnapshotVersion -> SnapshotVersion -> Bool
forall a. Eq a => a -> a -> Bool
== SnapshotVersion
currentVersion
        -- you are decrementing from existing utxo in the head
        Bool -> Bool -> Bool
&& (SingleUTxO -> Bool) -> [SingleUTxO] -> Bool
forall (t :: * -> *) a. Foldable t => (a -> Bool) -> t a -> Bool
all (SingleUTxO -> [SingleUTxO] -> Bool
forall (f :: * -> *) a.
(Foldable f, DisallowElem f, Eq a) =>
a -> f a -> Bool
`elem` ModelUTxO -> [SingleUTxO]
forall k a. Map k a -> [k]
Map.keys ModelUTxO
utxoInHead) (ModelUTxO -> [SingleUTxO]
forall k a. Map k a -> [k]
Map.keys (ModelSnapshot -> ModelUTxO
decommitUTxO ModelSnapshot
snapshot) [SingleUTxO] -> [SingleUTxO] -> [SingleUTxO]
forall a. Semigroup a => a -> a -> a
<> ModelUTxO -> [SingleUTxO]
forall k a. Map k a -> [k]
Map.keys (ModelSnapshot -> ModelUTxO
snapshotUTxO ModelSnapshot
snapshot))
        -- your tx is balanced with the utxo in the head
        Bool -> Bool -> Bool
&& ModelUTxO -> Natural
forall a (f :: * -> *). (Foldable f, Num a) => f a -> a
sum (ModelSnapshot -> ModelUTxO
decommitUTxO ModelSnapshot
snapshot) Natural -> Natural -> Natural
forall a. Num a => a -> a -> a
+ ModelUTxO -> Natural
forall a (f :: * -> *). (Foldable f, Num a) => f a -> a
sum (ModelSnapshot -> ModelUTxO
snapshotUTxO ModelSnapshot
snapshot) Natural -> Natural -> Bool
forall a. Eq a => a -> a -> Bool
== ModelUTxO -> Natural
forall a (f :: * -> *). (Foldable f, Num a) => f a -> a
sum ModelUTxO
utxoInHead
        Bool -> Bool -> Bool
&& (Bool -> Bool
not (Bool -> Bool) -> (ModelUTxO -> Bool) -> ModelUTxO -> Bool
forall b c a. (b -> c) -> (a -> b) -> a -> c
. ModelUTxO -> Bool
forall a. Map SingleUTxO a -> Bool
forall (t :: * -> *) a. Foldable t => t a -> Bool
null (ModelUTxO -> Bool) -> ModelUTxO -> Bool
forall a b. (a -> b) -> a -> b
$ ModelSnapshot -> ModelUTxO
decommitUTxO ModelSnapshot
snapshot)
    Close{ModelSnapshot
$sel:snapshot:Decrement :: Action Model TxResult -> ModelSnapshot
snapshot :: ModelSnapshot
snapshot} ->
      State
headState State -> State -> Bool
forall a. Eq a => a -> a -> Bool
== State
Open
        Bool -> Bool -> Bool
&& ( if ModelSnapshot
snapshot.number SnapshotNumber -> SnapshotNumber -> Bool
forall a. Eq a => a -> a -> Bool
== SnapshotNumber
0
              then ModelSnapshot -> ModelUTxO
snapshotUTxO ModelSnapshot
snapshot ModelUTxO -> ModelUTxO -> Bool
forall a. Eq a => a -> a -> Bool
== ModelUTxO
initialUTxOInHead
              else
                ModelSnapshot
snapshot.number SnapshotNumber -> SnapshotNumber -> Bool
forall a. Ord a => a -> a -> Bool
>= SnapshotNumber
latestSnapshot
                  Bool -> Bool -> Bool
&& 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])
           )
        -- you are decrementing from existing utxo in the head
        Bool -> Bool -> Bool
&& (SingleUTxO -> Bool) -> [SingleUTxO] -> Bool
forall (t :: * -> *) a. Foldable t => (a -> Bool) -> t a -> Bool
all (SingleUTxO -> [SingleUTxO] -> Bool
forall (f :: * -> *) a.
(Foldable f, DisallowElem f, Eq a) =>
a -> f a -> Bool
`elem` ModelUTxO -> [SingleUTxO]
forall k a. Map k a -> [k]
Map.keys ModelUTxO
utxoInHead) (ModelUTxO -> [SingleUTxO]
forall k a. Map k a -> [k]
Map.keys (ModelSnapshot -> ModelUTxO
decommitUTxO ModelSnapshot
snapshot) [SingleUTxO] -> [SingleUTxO] -> [SingleUTxO]
forall a. Semigroup a => a -> a -> a
<> ModelUTxO -> [SingleUTxO]
forall k a. Map k a -> [k]
Map.keys (ModelSnapshot -> ModelUTxO
snapshotUTxO ModelSnapshot
snapshot))
        -- your tx is balanced with the utxo in the head
        Bool -> Bool -> Bool
&& ModelUTxO -> Natural
forall a (f :: * -> *). (Foldable f, Num a) => f a -> a
sum (ModelSnapshot -> ModelUTxO
decommitUTxO ModelSnapshot
snapshot) Natural -> Natural -> Natural
forall a. Num a => a -> a -> a
+ ModelUTxO -> Natural
forall a (f :: * -> *). (Foldable f, Num a) => f a -> a
sum (ModelSnapshot -> ModelUTxO
snapshotUTxO ModelSnapshot
snapshot) Natural -> Natural -> Bool
forall a. Eq a => a -> a -> Bool
== ModelUTxO -> Natural
forall a (f :: * -> *). (Foldable f, Num a) => f a -> a
sum ModelUTxO
utxoInHead
     where
      Model{$sel:utxoInHead:Model :: Model -> ModelUTxO
utxoInHead = ModelUTxO
initialUTxOInHead} = Model
forall state. StateModel state => state
initialState
    Contest{Actor
$sel:actor:Decrement :: Action Model TxResult -> Actor
actor :: Actor
actor, ModelSnapshot
$sel:snapshot:Decrement :: Action Model TxResult -> ModelSnapshot
snapshot :: ModelSnapshot
snapshot} ->
      State
headState State -> State -> Bool
forall a. Eq a => a -> a -> Bool
== State
Closed
        Bool -> Bool -> Bool
&& Actor
actor Actor -> [Actor] -> Bool
forall (f :: * -> *) a.
(Foldable f, DisallowElem f, Eq a) =>
a -> f a -> Bool
`notElem` [Actor]
alreadyContested
        Bool -> Bool -> Bool
&& 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])
        Bool -> Bool -> Bool
&& ModelSnapshot
snapshot.number SnapshotNumber -> SnapshotNumber -> Bool
forall a. Ord a => a -> a -> Bool
> SnapshotNumber
latestSnapshot
        -- you are decrementing from existing utxo in the head
        Bool -> Bool -> Bool
&& (SingleUTxO -> Bool) -> [SingleUTxO] -> Bool
forall (t :: * -> *) a. Foldable t => (a -> Bool) -> t a -> Bool
all (SingleUTxO -> [SingleUTxO] -> Bool
forall (f :: * -> *) a.
(Foldable f, DisallowElem f, Eq a) =>
a -> f a -> Bool
`elem` ModelUTxO -> [SingleUTxO]
forall k a. Map k a -> [k]
Map.keys ModelUTxO
utxoInHead) (ModelUTxO -> [SingleUTxO]
forall k a. Map k a -> [k]
Map.keys (ModelSnapshot -> ModelUTxO
decommitUTxO ModelSnapshot
snapshot) [SingleUTxO] -> [SingleUTxO] -> [SingleUTxO]
forall a. Semigroup a => a -> a -> a
<> ModelUTxO -> [SingleUTxO]
forall k a. Map k a -> [k]
Map.keys (ModelSnapshot -> ModelUTxO
snapshotUTxO ModelSnapshot
snapshot))
        -- your tx is balanced with the utxo in the head
        Bool -> Bool -> Bool
&& ModelUTxO -> Natural
forall a (f :: * -> *). (Foldable f, Num a) => f a -> a
sum (ModelSnapshot -> ModelUTxO
decommitUTxO ModelSnapshot
snapshot) Natural -> Natural -> Natural
forall a. Num a => a -> a -> a
+ ModelUTxO -> Natural
forall a (f :: * -> *). (Foldable f, Num a) => f a -> a
sum (ModelSnapshot -> ModelUTxO
snapshotUTxO ModelSnapshot
snapshot) Natural -> Natural -> Bool
forall a. Eq a => a -> a -> Bool
== ModelUTxO -> Natural
forall a (f :: * -> *). (Foldable f, Num a) => f a -> a
sum ModelUTxO
utxoInHead
    Fanout{ModelUTxO
$sel:utxo:Decrement :: Action Model TxResult -> ModelUTxO
utxo :: ModelUTxO
utxo, ModelUTxO
$sel:deltaUTxO:Decrement :: Action Model TxResult -> ModelUTxO
deltaUTxO :: ModelUTxO
deltaUTxO} ->
      State
headState State -> State -> Bool
forall a. Eq a => a -> a -> Bool
== State
Closed
        Bool -> Bool -> Bool
&& ModelUTxO
utxo ModelUTxO -> ModelUTxO -> Bool
forall a. Eq a => a -> a -> Bool
== ModelUTxO
utxoInHead
        Bool -> Bool -> Bool
&& ModelUTxO
deltaUTxO ModelUTxO -> ModelUTxO -> Bool
forall a. Eq a => a -> a -> Bool
== ModelUTxO
pendingDecommitUTxO

  -- 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, ModelUTxO
$sel:utxoInHead:Model :: Model -> ModelUTxO
utxoInHead :: ModelUTxO
utxoInHead, SnapshotVersion
$sel:currentVersion:Model :: Model -> SnapshotVersion
currentVersion :: SnapshotVersion
currentVersion} = \case
    Action Model a
R:ActionModela a
Stop -> Bool
False
    -- Only filter non-matching states as we are not interested in these kind of
    -- verification failures.
    Decrement{ModelSnapshot
$sel:snapshot:Decrement :: 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.version SnapshotVersion -> SnapshotVersion -> Bool
forall a. Eq a => a -> a -> Bool
/= SnapshotVersion
currentVersion
        -- Ignore unbalanced decrements.
        -- TODO: make them fail gracefully and test this?
        Bool -> Bool -> Bool
&& ModelUTxO -> Natural
forall a (f :: * -> *). (Foldable f, Num a) => f a -> a
sum (ModelSnapshot -> ModelUTxO
decommitUTxO ModelSnapshot
snapshot) Natural -> Natural -> Natural
forall a. Num a => a -> a -> a
+ ModelUTxO -> Natural
forall a (f :: * -> *). (Foldable f, Num a) => f a -> a
sum (ModelSnapshot -> ModelUTxO
snapshotUTxO ModelSnapshot
snapshot) Natural -> Natural -> Bool
forall a. Eq a => a -> a -> Bool
== ModelUTxO -> Natural
forall a (f :: * -> *). (Foldable f, Num a) => f a -> a
sum ModelUTxO
utxoInHead
        -- Ignore decrements that work with non existing utxo in the head
        Bool -> Bool -> Bool
&& (SingleUTxO -> Bool) -> [SingleUTxO] -> Bool
forall (t :: * -> *) a. Foldable t => (a -> Bool) -> t a -> Bool
all (SingleUTxO -> [SingleUTxO] -> Bool
forall (f :: * -> *) a.
(Foldable f, DisallowElem f, Eq a) =>
a -> f a -> Bool
`elem` ModelUTxO -> [SingleUTxO]
forall k a. Map k a -> [k]
Map.keys ModelUTxO
utxoInHead) (ModelUTxO -> [SingleUTxO]
forall k a. Map k a -> [k]
Map.keys (ModelSnapshot -> ModelUTxO
decommitUTxO ModelSnapshot
snapshot) [SingleUTxO] -> [SingleUTxO] -> [SingleUTxO]
forall a. Semigroup a => a -> a -> a
<> ModelUTxO -> [SingleUTxO]
forall k a. Map k a -> [k]
Map.keys (ModelSnapshot -> ModelUTxO
snapshotUTxO ModelSnapshot
snapshot))
        -- Ignore decrement without something to decommit
        Bool -> Bool -> Bool
&& (Bool -> Bool
not (Bool -> Bool) -> (ModelUTxO -> Bool) -> ModelUTxO -> Bool
forall b c a. (b -> c) -> (a -> b) -> a -> c
. ModelUTxO -> Bool
forall a. Map SingleUTxO a -> Bool
forall (t :: * -> *) a. Foldable t => t a -> Bool
null (ModelUTxO -> Bool) -> ModelUTxO -> Bool
forall a b. (a -> b) -> a -> b
$ ModelSnapshot -> ModelUTxO
decommitUTxO ModelSnapshot
snapshot)
    Close{ModelSnapshot
$sel:snapshot:Decrement :: 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.number SnapshotNumber -> SnapshotNumber -> Bool
forall a. Eq a => a -> a -> Bool
== SnapshotNumber
0
              Bool -> Bool -> Bool
|| 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])
           )
        -- Ignore unbalanced close.
        -- TODO: make them fail gracefully and test this?
        Bool -> Bool -> Bool
&& ModelUTxO -> Natural
forall a (f :: * -> *). (Foldable f, Num a) => f a -> a
sum (ModelSnapshot -> ModelUTxO
decommitUTxO ModelSnapshot
snapshot) Natural -> Natural -> Natural
forall a. Num a => a -> a -> a
+ ModelUTxO -> Natural
forall a (f :: * -> *). (Foldable f, Num a) => f a -> a
sum (ModelSnapshot -> ModelUTxO
snapshotUTxO ModelSnapshot
snapshot) Natural -> Natural -> Bool
forall a. Eq a => a -> a -> Bool
== ModelUTxO -> Natural
forall a (f :: * -> *). (Foldable f, Num a) => f a -> a
sum ModelUTxO
utxoInHead
        -- Ignore close that work with non existing utxo in the head
        Bool -> Bool -> Bool
&& (SingleUTxO -> Bool) -> [SingleUTxO] -> Bool
forall (t :: * -> *) a. Foldable t => (a -> Bool) -> t a -> Bool
all (SingleUTxO -> [SingleUTxO] -> Bool
forall (f :: * -> *) a.
(Foldable f, DisallowElem f, Eq a) =>
a -> f a -> Bool
`elem` ModelUTxO -> [SingleUTxO]
forall k a. Map k a -> [k]
Map.keys ModelUTxO
utxoInHead) (ModelUTxO -> [SingleUTxO]
forall k a. Map k a -> [k]
Map.keys (ModelSnapshot -> ModelUTxO
decommitUTxO ModelSnapshot
snapshot) [SingleUTxO] -> [SingleUTxO] -> [SingleUTxO]
forall a. Semigroup a => a -> a -> a
<> ModelUTxO -> [SingleUTxO]
forall k a. Map k a -> [k]
Map.keys (ModelSnapshot -> ModelUTxO
snapshotUTxO ModelSnapshot
snapshot))
    Contest{ModelSnapshot
$sel:snapshot:Decrement :: Action Model TxResult -> ModelSnapshot
snapshot :: ModelSnapshot
snapshot} ->
      State
headState State -> State -> Bool
forall a. Eq a => a -> a -> Bool
== State
Closed
        -- Ignore unbalanced close.
        -- TODO: make them fail gracefully and test this?
        Bool -> Bool -> Bool
&& ModelUTxO -> Natural
forall a (f :: * -> *). (Foldable f, Num a) => f a -> a
sum (ModelSnapshot -> ModelUTxO
decommitUTxO ModelSnapshot
snapshot) Natural -> Natural -> Natural
forall a. Num a => a -> a -> a
+ ModelUTxO -> Natural
forall a (f :: * -> *). (Foldable f, Num a) => f a -> a
sum (ModelSnapshot -> ModelUTxO
snapshotUTxO ModelSnapshot
snapshot) Natural -> Natural -> Bool
forall a. Eq a => a -> a -> Bool
== ModelUTxO -> Natural
forall a (f :: * -> *). (Foldable f, Num a) => f a -> a
sum ModelUTxO
utxoInHead
        -- Ignore close that work with non existing utxo in the head
        Bool -> Bool -> Bool
&& (SingleUTxO -> Bool) -> [SingleUTxO] -> Bool
forall (t :: * -> *) a. Foldable t => (a -> Bool) -> t a -> Bool
all (SingleUTxO -> [SingleUTxO] -> Bool
forall (f :: * -> *) a.
(Foldable f, DisallowElem f, Eq a) =>
a -> f a -> Bool
`elem` ModelUTxO -> [SingleUTxO]
forall k a. Map k a -> [k]
Map.keys ModelUTxO
utxoInHead) (ModelUTxO -> [SingleUTxO]
forall k a. Map k a -> [k]
Map.keys (ModelSnapshot -> ModelUTxO
decommitUTxO ModelSnapshot
snapshot) [SingleUTxO] -> [SingleUTxO] -> [SingleUTxO]
forall a. Semigroup a => a -> a -> a
<> ModelUTxO -> [SingleUTxO]
forall k a. Map k a -> [k]
Map.keys (ModelSnapshot -> ModelUTxO
snapshotUTxO ModelSnapshot
snapshot))
    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{SnapshotVersion
$sel:currentVersion:Model :: Model -> SnapshotVersion
currentVersion :: SnapshotVersion
currentVersion} Action Model a
t Var a
_result =
    case Action Model a
t of
      Action Model a
R:ActionModela a
Stop -> Model
m
      Decrement{ModelSnapshot
$sel:snapshot:Decrement :: Action Model TxResult -> ModelSnapshot
snapshot :: ModelSnapshot
snapshot} ->
        Model
m
          { headState = Open
          , currentVersion = m.currentVersion + 1
          , latestSnapshot = snapshot.number
          , utxoInHead = balanceUTxOInHead (utxoInHead m) (decommitUTxO snapshot)
          }
      Close{ModelSnapshot
$sel:snapshot:Decrement :: Action Model TxResult -> ModelSnapshot
snapshot :: ModelSnapshot
snapshot} ->
        Model
m
          { headState = Closed
          , latestSnapshot = snapshot.number
          , alreadyContested = []
          , utxoInHead = snapshotUTxO snapshot
          , pendingDecommitUTxO = if currentVersion == snapshot.version then decommitUTxO snapshot else mempty
          }
      Contest{Actor
$sel:actor:Decrement :: Action Model TxResult -> Actor
actor :: Actor
actor, ModelSnapshot
$sel:snapshot:Decrement :: Action Model TxResult -> ModelSnapshot
snapshot :: ModelSnapshot
snapshot} ->
        Model
m
          { headState = Closed
          , latestSnapshot = snapshot.number
          , alreadyContested = actor : alreadyContested m
          , utxoInHead = snapshotUTxO snapshot
          , pendingDecommitUTxO = decommitUTxO snapshot
          }
      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 UTxO) IO a
runAppM :: ReaderT (IORef 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 UTxO AppM where
  ask :: AppM UTxO
ask = ReaderT (IORef UTxO) IO UTxO -> AppM UTxO
forall a. ReaderT (IORef UTxO) IO a -> AppM a
AppM (ReaderT (IORef UTxO) IO UTxO -> AppM UTxO)
-> ReaderT (IORef UTxO) IO UTxO -> AppM UTxO
forall a b. (a -> b) -> a -> b
$ ReaderT (IORef UTxO) IO (IORef UTxO)
forall r (m :: * -> *). MonadReader r m => m r
ask ReaderT (IORef UTxO) IO (IORef UTxO)
-> (IORef UTxO -> ReaderT (IORef UTxO) IO UTxO)
-> ReaderT (IORef UTxO) IO UTxO
forall a b.
ReaderT (IORef UTxO) IO a
-> (a -> ReaderT (IORef UTxO) IO b) -> ReaderT (IORef UTxO) IO b
forall (m :: * -> *) a b. Monad m => m a -> (a -> m b) -> m b
>>= IO UTxO -> ReaderT (IORef UTxO) IO UTxO
forall a. IO a -> ReaderT (IORef UTxO) IO a
forall (m :: * -> *) a. MonadIO m => IO a -> m a
liftIO (IO UTxO -> ReaderT (IORef UTxO) IO UTxO)
-> (IORef UTxO -> IO UTxO)
-> IORef UTxO
-> ReaderT (IORef UTxO) IO UTxO
forall b c a. (b -> c) -> (a -> b) -> a -> c
. IORef UTxO -> IO UTxO
forall (m :: * -> *) a. MonadIO m => IORef a -> m a
readIORef

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

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

type instance Realized AppM a = a

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
      Decrement{Actor
$sel:actor:Decrement :: Action Model TxResult -> Actor
actor :: Actor
actor, ModelSnapshot
$sel:snapshot:Decrement :: Action Model TxResult -> ModelSnapshot
snapshot :: ModelSnapshot
snapshot} -> do
        let (Snapshot Tx
s, MultiSignature (Snapshot Tx)
signatures) = ModelSnapshot -> (Snapshot Tx, MultiSignature (Snapshot Tx))
signedSnapshot ModelSnapshot
snapshot
        Either DecrementTxError Tx
tx <- Actor -> ConfirmedSnapshot Tx -> AppM (Either DecrementTxError Tx)
newDecrementTx Actor
actor ConfirmedSnapshot{$sel:snapshot:InitialSnapshot :: Snapshot Tx
snapshot = Snapshot Tx
s, MultiSignature (Snapshot Tx)
signatures :: MultiSignature (Snapshot Tx)
$sel:signatures:InitialSnapshot :: MultiSignature (Snapshot Tx)
signatures}
        Either DecrementTxError Tx -> AppM TxResult
forall err. Show err => Either err Tx -> AppM TxResult
performTx Either DecrementTxError Tx
tx
      Close{Actor
$sel:actor:Decrement :: Action Model TxResult -> Actor
actor :: Actor
actor, ModelSnapshot
$sel:snapshot:Decrement :: 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)
        Either CloseTxError Tx -> AppM TxResult
forall err. Show err => Either err Tx -> AppM TxResult
performTx Either CloseTxError Tx
tx
      Contest{Actor
$sel:actor:Decrement :: Action Model TxResult -> Actor
actor :: Actor
actor, ModelSnapshot
$sel:snapshot:Decrement :: 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)
        Either ContestTxError Tx -> AppM TxResult
forall err. Show err => Either err Tx -> AppM TxResult
performTx Either ContestTxError Tx
tx
      Fanout{ModelUTxO
$sel:utxo:Decrement :: Action Model TxResult -> ModelUTxO
utxo :: ModelUTxO
utxo, ModelUTxO
$sel:deltaUTxO:Decrement :: Action Model TxResult -> ModelUTxO
deltaUTxO :: ModelUTxO
deltaUTxO} -> do
        Either FanoutTxError Tx
tx <- Actor -> ModelUTxO -> ModelUTxO -> AppM (Either FanoutTxError Tx)
newFanoutTx Actor
Alice ModelUTxO
utxo ModelUTxO
deltaUTxO
        Either FanoutTxError Tx -> AppM TxResult
forall err. Show err => Either err Tx -> AppM TxResult
performTx Either FanoutTxError Tx
tx
      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
      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:Decrement :: Action Model TxResult -> ModelUTxO
utxo :: ModelUTxO
utxo, ModelUTxO
$sel:deltaUTxO:Decrement :: Action Model TxResult -> ModelUTxO
deltaUTxO :: ModelUTxO
deltaUTxO} -> 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, Coin)) -> [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 -> Coin
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
            -- counterexamplePost ("Fanned out UTxO does not match: " <> renderUTxO fannedOut)
            -- counterexamplePost ("SnapshotUTxO: " <> renderUTxO (snapshotUTxO snapshot))
            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
deltaUTxO)

        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"
      Action Model a
_ -> () -> 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
      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 => Either err Tx -> AppM TxResult
performTx :: forall err. Show err => Either err Tx -> AppM TxResult
performTx Either err Tx
result =
  case Either err Tx
result of
    Left err
err -> do
      UTxO
utxo <- AppM 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
      UTxO
utxo <- AppM 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
        UTxO -> AppM ()
forall s (m :: * -> *). MonadState s m => s -> m ()
put (UTxO -> AppM ()) -> UTxO -> AppM ()
forall a b. (a -> b) -> a -> b
$ Tx -> UTxO -> UTxO
adjustUTxO Tx
tx UTxO
utxo
      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]

-- | A "random" UTxO distribution for a given 'ModelSnapshot'.
generateUTxOFromModelSnapshot :: ModelSnapshot -> (UTxO, UTxO)
generateUTxOFromModelSnapshot :: ModelSnapshot -> (UTxO, UTxO)
generateUTxOFromModelSnapshot ModelSnapshot
snapshot =
  ( ModelUTxO -> UTxO
realWorldModelUTxO (ModelSnapshot -> ModelUTxO
snapshotUTxO ModelSnapshot
snapshot)
  , ModelUTxO -> UTxO
realWorldModelUTxO (ModelSnapshot -> ModelUTxO
decommitUTxO ModelSnapshot
snapshot)
  )

-- | Map a 'ModelUTxO' to a real-world 'UTxO'.
realWorldModelUTxO :: ModelUTxO -> UTxO
realWorldModelUTxO :: ModelUTxO -> UTxO
realWorldModelUTxO =
  (SingleUTxO -> Natural -> UTxO) -> ModelUTxO -> UTxO
forall m k a. Monoid m => (k -> a -> m) -> Map k a -> m
Map.foldMapWithKey
    ( \SingleUTxO
k Natural
balance ->
        Natural -> Gen UTxO
genUTxOWithBalance Natural
balance Gen UTxO -> Int -> UTxO
forall a. Gen a -> Int -> a
`generateWith` SingleUTxO -> Int
forall a. Enum a => a -> Int
fromEnum SingleUTxO
k
    )
 where
  genUTxOWithBalance :: Natural -> Gen UTxO
genUTxOWithBalance Natural
b =
    Gen (TxOut CtxUTxO Era) -> Gen UTxO
genUTxO1 ((Value -> Value) -> TxOut CtxUTxO Era -> TxOut CtxUTxO Era
forall era ctx.
(IsMaryBasedEra era, IsShelleyBasedEra 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
$ Coin -> Value
lovelaceToValue (Integer -> Coin
Coin (Integer -> Coin) -> Integer -> Coin
forall a b. (a -> b) -> a -> b
$ Natural -> Integer
naturalToInteger Natural
b)) (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
  (UTxO
utxo, UTxO
toDecommit) = ModelSnapshot -> (UTxO, UTxO)
generateUTxOFromModelSnapshot ModelSnapshot
ms
  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 :: [TxIdType Tx]
confirmed = []
      , UTxO
UTxOType Tx
utxo :: UTxO
$sel:utxo:Snapshot :: UTxOType Tx
utxo
      , $sel:utxoToDecommit:Snapshot :: Maybe (UTxOType Tx)
utxoToDecommit = UTxO -> Maybe UTxO
forall a. a -> Maybe a
Just UTxO
toDecommit
      }

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

-- | 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 = (UTxO, UTxO) -> UTxO
forall a b. (a, b) -> a
fst ((UTxO, UTxO) -> UTxO) -> (UTxO, UTxO) -> UTxO
forall a b. (a -> b) -> a -> b
$ ModelSnapshot -> (UTxO, UTxO)
generateUTxOFromModelSnapshot ModelSnapshot
modelSnapshot
        }
    SnapshotNumber
_ -> ConfirmedSnapshot{Snapshot Tx
$sel:snapshot:InitialSnapshot :: Snapshot Tx
snapshot :: Snapshot Tx
snapshot, MultiSignature (Snapshot Tx)
$sel:signatures:InitialSnapshot :: MultiSignature (Snapshot Tx)
signatures :: 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, IsShelleyBasedEra 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 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
  UTxO
spendableUTxO <- AppM 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
  UTxO
spendableUTxO <- AppM 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
  UTxO
spendableUTxO <- AppM 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 -> AppM (Either FanoutTxError Tx)
newFanoutTx :: Actor -> ModelUTxO -> ModelUTxO -> AppM (Either FanoutTxError Tx)
newFanoutTx Actor
actor ModelUTxO
utxo ModelUTxO
deltaUTxO = do
  UTxO
spendableUTxO <- AppM 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
-> 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. Map SingleUTxO a -> Bool
forall (t :: * -> *) a. Foldable t => t a -> Bool
null ModelUTxO
deltaUTxO 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
deltaUTxO)
      SlotNo
deadline
 where
  CP.UnsafeContestationPeriod Natural
contestationPeriod = ContestationPeriod
Fixture.cperiod
  deadline :: SlotNo
deadline = Word64 -> SlotNo
SlotNo (Word64 -> SlotNo) -> Word64 -> SlotNo
forall a b. (a -> b) -> a -> b
$ Natural -> Word64
forall a b. (Integral a, Num b) => a -> b
fromIntegral Natural
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.
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
    String -> PostconditionM' m ()
forall (m :: * -> *). Monad m => String -> PostconditionM' m ()
counterexample' String
"Expected tx to fail validation"
    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 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 ()

-- | Generate sometimes a value with given generator, bur more often just use
-- the given value.
orSometimes :: a -> Gen a -> Gen a
orSometimes :: forall a. a -> Gen a -> Gen a
orSometimes a
a Gen a
gen = [(Int, Gen a)] -> Gen a
forall a. [(Int, Gen a)] -> Gen a
frequency [(Int
1, a -> Gen a
forall a. a -> Gen a
forall (f :: * -> *) a. Applicative f => a -> f a
pure a
a), (Int
2, Gen a
gen)]