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

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

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

import Cardano.Api.UTxO (UTxO)
import Cardano.Api.UTxO qualified as UTxO
import Data.List ((\\))
import Data.Map.Strict qualified as Map
import Data.Time.Clock.POSIX (posixSecondsToUTCTime)
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 (Confidence (..), Property, Smart (..), Testable, checkCoverage, checkCoverageWith, cover, elements, frequency, ioProperty, 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 -> (ModelUTxO -> ModelUTxO -> Property) -> Spec
forall prop.
(HasCallStack, Testable prop) =>
String -> prop -> Spec
prop String
"realWorldModelUTxO preserves addition" ((ModelUTxO -> ModelUTxO -> Property) -> Spec)
-> (ModelUTxO -> ModelUTxO -> Property) -> Spec
forall a b. (a -> b) -> a -> b
$ \ModelUTxO
u1 ModelUTxO
u2 ->
    ModelUTxO -> UTxO
realWorldModelUTxO (ModelUTxO
u1 ModelUTxO -> ModelUTxO -> ModelUTxO
forall a. Semigroup a => a -> a -> a
<> ModelUTxO
u2) UTxO -> UTxO -> Property
forall a. (Eq a, Show a) => a -> a -> Property
=== (ModelUTxO -> UTxO
realWorldModelUTxO ModelUTxO
u1 UTxO -> UTxO -> UTxO
forall a. Semigroup a => a -> a -> a
<> ModelUTxO -> UTxO
realWorldModelUTxO ModelUTxO
u2)
  String -> (Actions Model -> Property) -> Spec
forall prop.
(HasCallStack, Testable prop) =>
String -> prop -> Spec
prop String
"generates interesting transaction traces" ((Actions Model -> Property) -> Spec)
-> (Actions Model -> Property) -> Spec
forall a b. (a -> b) -> a -> b
$ \Actions Model
actions ->
    Property -> Property
forall prop. Testable prop => prop -> Property
checkCoverage (Property -> Property) -> Property -> Property
forall a b. (a -> b) -> a -> b
$ Actions Model -> Bool -> Property
forall p. Testable p => Actions Model -> p -> Property
coversInterestingActions Actions Model
actions Bool
True
  String -> Property -> Spec
forall prop.
(HasCallStack, Testable prop) =>
String -> prop -> Spec
prop String
"all valid transactions" (Property -> Spec) -> Property -> Spec
forall a b. (a -> b) -> a -> b
$
    -- NOTE: Using lower confidence to improve performance. In case of an error,
    -- check coverage numbers and also the distribution in above test (which is
    -- way faster).
    Confidence -> (Actions Model -> Property) -> Property
forall prop. Testable prop => Confidence -> prop -> Property
checkCoverageWith
      Confidence{certainty :: Integer
certainty = Integer
100, tolerance :: Double
tolerance = Double
0.8}
      Actions Model -> Property
prop_runActions

coversInterestingActions :: Testable p => Actions Model -> p -> Property
coversInterestingActions :: forall p. Testable p => Actions Model -> p -> Property
coversInterestingActions (Actions_ [String]
_ (Smart Int
_ [Step Model]
steps)) p
p =
  p
p
    p -> (p -> Property) -> Property
forall a b. a -> (a -> b) -> b
& Double -> Bool -> String -> p -> Property
forall prop.
Testable prop =>
Double -> Bool -> String -> prop -> Property
cover Double
1 ([Step Model] -> Bool
forall a. [a] -> Bool
forall (t :: * -> *) a. Foldable t => t a -> Bool
null [Step Model]
steps) String
"empty"
    Property -> (Property -> Property) -> Property
forall a b. a -> (a -> b) -> b
& Double -> Bool -> String -> Property -> Property
forall prop.
Testable prop =>
Double -> Bool -> String -> prop -> Property
cover Double
50 ([Step Model] -> Bool
hasSomeSnapshots [Step Model]
steps) String
"has some snapshots"
    Property -> (Property -> Property) -> Property
forall a b. a -> (a -> b) -> b
& Double -> Bool -> String -> Property -> Property
forall prop.
Testable prop =>
Double -> Bool -> String -> prop -> Property
cover Double
5 ([Step Model] -> Bool
hasDecrement [Step Model]
steps) String
"has decrements"
    Property -> (Property -> Property) -> Property
forall a b. a -> (a -> b) -> b
& Double -> Bool -> String -> Property -> Property
forall prop.
Testable prop =>
Double -> Bool -> String -> prop -> Property
cover Double
0.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
10 ([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
10 ([Step Model] -> Bool
fanoutWithSomeUTxO [Step Model]
steps) String
"fanout with some UTxO"
    Property -> (Property -> Property) -> Property
forall a b. a -> (a -> b) -> b
& Double -> Bool -> String -> Property -> Property
forall prop.
Testable prop =>
Double -> Bool -> String -> prop -> Property
cover Double
10 ([Step Model] -> Bool
fanoutWithDelta [Step Model]
steps) String
"fanout with additional UTxO to distribute"
 where
  hasSomeSnapshots :: [Step Model] -> Bool
hasSomeSnapshots =
    (Step Model -> Bool) -> [Step Model] -> Bool
forall (t :: * -> *) a. Foldable t => (a -> Bool) -> t a -> Bool
any ((Step Model -> Bool) -> [Step Model] -> Bool)
-> (Step Model -> Bool) -> [Step Model] -> Bool
forall a b. (a -> b) -> a -> b
$
      \(Var a
_ := ActionWithPolarity{Action Model a
polarAction :: Action Model a
polarAction :: forall state a. ActionWithPolarity state a -> Action state a
polarAction, Polarity
polarity :: Polarity
polarity :: forall state a. ActionWithPolarity state a -> Polarity
polarity}) -> case Action Model a
polarAction of
        NewSnapshot{} ->
          Polarity
polarity Polarity -> Polarity -> Bool
forall a. Eq a => a -> a -> Bool
== Polarity
PosPolarity
        Action Model a
_ -> Bool
False

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

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

  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:NewSnapshot :: 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. [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:NewSnapshot :: 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. [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:NewSnapshot :: 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. [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:NewSnapshot :: Action Model TxResult -> ModelSnapshot
snapshot} -> ModelSnapshot
snapshot ModelSnapshot -> ModelSnapshot -> Bool
forall a. Ord a => a -> a -> Bool
> ModelSnapshot
0
      Action Model a
_ -> Bool
False

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

prop_runActions :: Actions Model -> Property
prop_runActions :: Actions Model -> Property
prop_runActions Actions Model
actions =
  Actions Model -> Property -> Property
forall p. Testable p => Actions Model -> p -> Property
coversInterestingActions Actions Model
actions
    (Property -> Property)
-> (PropertyM AppM () -> Property) -> PropertyM AppM () -> Property
forall b c a. (b -> c) -> (a -> b) -> a -> c
. (AppM Property -> Property) -> PropertyM AppM () -> Property
forall a (m :: * -> *).
(Testable a, Monad m) =>
(m Property -> Property) -> PropertyM m a -> Property
monadic AppM Property -> Property
runAppMProperty
    (PropertyM AppM () -> Property) -> PropertyM AppM () -> Property
forall a b. (a -> b) -> a -> b
$ do
      -- print actions
      PropertyM AppM (Annotated Model, Env AppM) -> PropertyM AppM ()
forall (f :: * -> *) a. Functor f => f a -> f ()
void (Actions Model -> PropertyM AppM (Annotated Model, Env AppM)
forall state (m :: * -> *) e.
(StateModel state, RunModel state m, e ~ Error state,
 forall a. IsPerformResult e a) =>
Actions state -> PropertyM m (Annotated state, Env m)
runActions Actions Model
actions)
 where
  runAppMProperty :: AppM Property -> Property
  runAppMProperty :: AppM Property -> Property
runAppMProperty AppM Property
action = IO Property -> Property
forall prop. Testable prop => IO prop -> Property
ioProperty (IO Property -> Property) -> IO Property -> Property
forall a b. (a -> b) -> a -> b
$ do
    IORef 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
ModelUTxO -> ShowS
SingleUTxO -> String
(Int -> SingleUTxO -> ShowS)
-> (SingleUTxO -> String)
-> (ModelUTxO -> ShowS)
-> Show SingleUTxO
forall a.
(Int -> a -> ShowS) -> (a -> String) -> ([a] -> ShowS) -> Show a
$cshowsPrec :: Int -> SingleUTxO -> ShowS
showsPrec :: Int -> SingleUTxO -> ShowS
$cshow :: SingleUTxO -> String
show :: SingleUTxO -> String
$cshowList :: ModelUTxO -> ShowS
showList :: ModelUTxO -> ShowS
Show, SingleUTxO -> SingleUTxO -> Bool
(SingleUTxO -> SingleUTxO -> Bool)
-> (SingleUTxO -> SingleUTxO -> Bool) -> Eq SingleUTxO
forall a. (a -> a -> Bool) -> (a -> a -> Bool) -> Eq a
$c== :: SingleUTxO -> SingleUTxO -> Bool
== :: SingleUTxO -> SingleUTxO -> Bool
$c/= :: SingleUTxO -> SingleUTxO -> Bool
/= :: SingleUTxO -> SingleUTxO -> Bool
Eq, Eq SingleUTxO
Eq SingleUTxO =>
(SingleUTxO -> SingleUTxO -> Ordering)
-> (SingleUTxO -> SingleUTxO -> Bool)
-> (SingleUTxO -> SingleUTxO -> Bool)
-> (SingleUTxO -> SingleUTxO -> Bool)
-> (SingleUTxO -> SingleUTxO -> Bool)
-> (SingleUTxO -> SingleUTxO -> SingleUTxO)
-> (SingleUTxO -> SingleUTxO -> SingleUTxO)
-> Ord SingleUTxO
SingleUTxO -> SingleUTxO -> Bool
SingleUTxO -> SingleUTxO -> Ordering
SingleUTxO -> SingleUTxO -> SingleUTxO
forall a.
Eq a =>
(a -> a -> Ordering)
-> (a -> a -> Bool)
-> (a -> a -> Bool)
-> (a -> a -> Bool)
-> (a -> a -> Bool)
-> (a -> a -> a)
-> (a -> a -> a)
-> Ord a
$ccompare :: SingleUTxO -> SingleUTxO -> Ordering
compare :: SingleUTxO -> SingleUTxO -> Ordering
$c< :: SingleUTxO -> SingleUTxO -> Bool
< :: SingleUTxO -> SingleUTxO -> Bool
$c<= :: SingleUTxO -> SingleUTxO -> Bool
<= :: SingleUTxO -> SingleUTxO -> Bool
$c> :: SingleUTxO -> SingleUTxO -> Bool
> :: SingleUTxO -> SingleUTxO -> Bool
$c>= :: SingleUTxO -> SingleUTxO -> Bool
>= :: SingleUTxO -> SingleUTxO -> Bool
$cmax :: SingleUTxO -> SingleUTxO -> SingleUTxO
max :: SingleUTxO -> SingleUTxO -> SingleUTxO
$cmin :: SingleUTxO -> SingleUTxO -> SingleUTxO
min :: SingleUTxO -> SingleUTxO -> SingleUTxO
Ord, Int -> SingleUTxO
SingleUTxO -> Int
SingleUTxO -> ModelUTxO
SingleUTxO -> SingleUTxO
SingleUTxO -> SingleUTxO -> ModelUTxO
SingleUTxO -> SingleUTxO -> SingleUTxO -> ModelUTxO
(SingleUTxO -> SingleUTxO)
-> (SingleUTxO -> SingleUTxO)
-> (Int -> SingleUTxO)
-> (SingleUTxO -> Int)
-> (SingleUTxO -> ModelUTxO)
-> (SingleUTxO -> SingleUTxO -> ModelUTxO)
-> (SingleUTxO -> SingleUTxO -> ModelUTxO)
-> (SingleUTxO -> SingleUTxO -> SingleUTxO -> ModelUTxO)
-> Enum SingleUTxO
forall a.
(a -> a)
-> (a -> a)
-> (Int -> a)
-> (a -> Int)
-> (a -> [a])
-> (a -> a -> [a])
-> (a -> a -> [a])
-> (a -> a -> a -> [a])
-> Enum a
$csucc :: SingleUTxO -> SingleUTxO
succ :: SingleUTxO -> SingleUTxO
$cpred :: SingleUTxO -> SingleUTxO
pred :: SingleUTxO -> SingleUTxO
$ctoEnum :: Int -> SingleUTxO
toEnum :: Int -> SingleUTxO
$cfromEnum :: SingleUTxO -> Int
fromEnum :: SingleUTxO -> Int
$cenumFrom :: SingleUTxO -> ModelUTxO
enumFrom :: SingleUTxO -> ModelUTxO
$cenumFromThen :: SingleUTxO -> SingleUTxO -> ModelUTxO
enumFromThen :: SingleUTxO -> SingleUTxO -> ModelUTxO
$cenumFromTo :: SingleUTxO -> SingleUTxO -> ModelUTxO
enumFromTo :: SingleUTxO -> SingleUTxO -> ModelUTxO
$cenumFromThenTo :: SingleUTxO -> SingleUTxO -> SingleUTxO -> ModelUTxO
enumFromThenTo :: SingleUTxO -> SingleUTxO -> SingleUTxO -> ModelUTxO
Enum, (forall x. SingleUTxO -> Rep SingleUTxO x)
-> (forall x. Rep SingleUTxO x -> SingleUTxO) -> Generic SingleUTxO
forall x. Rep SingleUTxO x -> SingleUTxO
forall x. SingleUTxO -> Rep SingleUTxO x
forall a.
(forall x. a -> Rep a x) -> (forall x. Rep a x -> a) -> Generic a
$cfrom :: forall x. SingleUTxO -> Rep SingleUTxO x
from :: forall x. SingleUTxO -> Rep SingleUTxO x
$cto :: forall x. Rep SingleUTxO x -> SingleUTxO
to :: forall x. Rep SingleUTxO x -> SingleUTxO
Generic)

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

type ModelUTxO = [SingleUTxO]

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

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

latestSnapshot :: [ModelSnapshot] -> Maybe ModelSnapshot
latestSnapshot :: [ModelSnapshot] -> Maybe ModelSnapshot
latestSnapshot = \case
  [] -> Maybe ModelSnapshot
forall a. Maybe a
Nothing
  (ModelSnapshot
s : [ModelSnapshot]
_) -> ModelSnapshot -> Maybe ModelSnapshot
forall a. a -> Maybe a
Just ModelSnapshot
s

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

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

instance StateModel Model where
  data Action Model a where
    NewSnapshot :: {Action Model () -> ModelSnapshot
newSnapshot :: ModelSnapshot} -> Action Model ()
    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:knownSnapshots:Model :: [ModelSnapshot]
knownSnapshots = []
      , $sel:currentVersion:Model :: SnapshotVersion
currentVersion = SnapshotVersion
0
      , $sel:closedSnapshotNumber:Model :: SnapshotNumber
closedSnapshotNumber = SnapshotNumber
0
      , $sel:alreadyContested:Model :: [Actor]
alreadyContested = []
      , $sel:utxoInHead:Model :: ModelUTxO
utxoInHead = [Item ModelUTxO] -> ModelUTxO
forall l. IsList l => [Item l] -> l
fromList [Item ModelUTxO
SingleUTxO
A, Item ModelUTxO
SingleUTxO
B, Item ModelUTxO
SingleUTxO
C]
      , $sel:pendingDecommit:Model :: ModelUTxO
pendingDecommit = ModelUTxO
forall a. Monoid a => a
mempty
      }

  arbitraryAction :: VarContext -> Model -> Gen (Any (Action Model))
  arbitraryAction :: VarContext -> Model -> Gen (Any (Action Model))
arbitraryAction VarContext
_lookup Model{State
$sel:headState:Model :: Model -> State
headState :: State
headState, [ModelSnapshot]
$sel:knownSnapshots:Model :: Model -> [ModelSnapshot]
knownSnapshots :: [ModelSnapshot]
knownSnapshots, SnapshotVersion
$sel:currentVersion:Model :: Model -> SnapshotVersion
currentVersion :: SnapshotVersion
currentVersion, ModelUTxO
$sel:utxoInHead:Model :: Model -> ModelUTxO
utxoInHead :: ModelUTxO
utxoInHead, ModelUTxO
$sel:pendingDecommit:Model :: Model -> ModelUTxO
pendingDecommit :: ModelUTxO
pendingDecommit} =
    case State
headState of
      Open{} ->
        [(Int, Gen (Any (Action Model)))] -> Gen (Any (Action Model))
forall a. HasCallStack => [(Int, Gen a)] -> Gen a
frequency ([(Int, Gen (Any (Action Model)))] -> Gen (Any (Action Model)))
-> [(Int, Gen (Any (Action Model)))] -> Gen (Any (Action Model))
forall a b. (a -> b) -> a -> b
$
          [(Int
3, Action Model () -> Any (Action Model)
forall a (f :: * -> *). (Typeable a, Eq (f a)) => f a -> Any f
Some (Action Model () -> Any (Action Model))
-> (ModelSnapshot -> Action Model ())
-> ModelSnapshot
-> Any (Action Model)
forall b c a. (b -> c) -> (a -> b) -> a -> c
. ModelSnapshot -> Action Model ()
NewSnapshot (ModelSnapshot -> Any (Action Model))
-> Gen ModelSnapshot -> Gen (Any (Action Model))
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> Gen ModelSnapshot
genSnapshot)]
            [(Int, Gen (Any (Action Model)))]
-> [(Int, Gen (Any (Action Model)))]
-> [(Int, Gen (Any (Action Model)))]
forall a. Semigroup a => a -> a -> a
<> [ ( Int
3
                 , do
                    Actor
actor <- [Actor] -> Gen Actor
forall a. HasCallStack => [a] -> Gen a
elements [Actor]
allActors
                    ModelSnapshot
snapshot <- [ModelSnapshot] -> Gen ModelSnapshot
forall a. HasCallStack => [a] -> Gen a
elements [ModelSnapshot]
knownSnapshots
                    Any (Action Model) -> Gen (Any (Action Model))
forall a. a -> Gen a
forall (f :: * -> *) a. Applicative f => a -> f a
pure (Any (Action Model) -> Gen (Any (Action Model)))
-> Any (Action Model) -> Gen (Any (Action Model))
forall a b. (a -> b) -> a -> b
$ Action Model TxResult -> Any (Action Model)
forall a (f :: * -> *). (Typeable a, Eq (f a)) => f a -> Any f
Some Decrement{Actor
$sel:actor:NewSnapshot :: Actor
actor :: Actor
actor, ModelSnapshot
$sel:snapshot:NewSnapshot :: ModelSnapshot
snapshot :: ModelSnapshot
snapshot}
                 )
               | Bool -> Bool
not ([ModelSnapshot] -> Bool
forall a. [a] -> Bool
forall (t :: * -> *) a. Foldable t => t a -> Bool
null [ModelSnapshot]
knownSnapshots) -- XXX: DRY this check
               ]
            [(Int, Gen (Any (Action Model)))]
-> [(Int, Gen (Any (Action Model)))]
-> [(Int, Gen (Any (Action Model)))]
forall a. Semigroup a => a -> a -> a
<> [ ( Int
1
                 , do
                    Actor
actor <- [Actor] -> Gen Actor
forall a. HasCallStack => [a] -> Gen a
elements [Actor]
allActors
                    ModelSnapshot
snapshot <- [ModelSnapshot] -> Gen ModelSnapshot
forall a. HasCallStack => [a] -> Gen a
elements [ModelSnapshot]
knownSnapshots
                    Any (Action Model) -> Gen (Any (Action Model))
forall a. a -> Gen a
forall (f :: * -> *) a. Applicative f => a -> f a
pure (Any (Action Model) -> Gen (Any (Action Model)))
-> Any (Action Model) -> Gen (Any (Action Model))
forall a b. (a -> b) -> a -> b
$ Action Model TxResult -> Any (Action Model)
forall a (f :: * -> *). (Typeable a, Eq (f a)) => f a -> Any f
Some (Action Model TxResult -> Any (Action Model))
-> Action Model TxResult -> Any (Action Model)
forall a b. (a -> b) -> a -> b
$ Close{Actor
$sel:actor:NewSnapshot :: Actor
actor :: Actor
actor, $sel:snapshot:NewSnapshot :: ModelSnapshot
snapshot = ModelSnapshot
snapshot}
                 )
               | Bool -> Bool
not ([ModelSnapshot] -> Bool
forall a. [a] -> Bool
forall (t :: * -> *) a. Foldable t => t a -> Bool
null [ModelSnapshot]
knownSnapshots)
               ]
      Closed{} ->
        [(Int, Gen (Any (Action Model)))] -> Gen (Any (Action Model))
forall a. HasCallStack => [(Int, Gen a)] -> Gen a
frequency ([(Int, Gen (Any (Action Model)))] -> Gen (Any (Action Model)))
-> [(Int, Gen (Any (Action Model)))] -> Gen (Any (Action Model))
forall a b. (a -> b) -> a -> b
$
          ( Int
1
          , 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:NewSnapshot :: ModelUTxO
utxo = ModelUTxO
utxoInHead
                    , $sel:deltaUTxO:NewSnapshot :: ModelUTxO
deltaUTxO = ModelUTxO
pendingDecommit
                    }
          )
            (Int, Gen (Any (Action Model)))
-> [(Int, Gen (Any (Action Model)))]
-> [(Int, Gen (Any (Action Model)))]
forall a. a -> [a] -> [a]
: [ ( Int
10
                , do
                    Actor
actor <- [Actor] -> Gen Actor
forall a. HasCallStack => [a] -> Gen a
elements [Actor]
allActors
                    ModelSnapshot
snapshot <- [ModelSnapshot] -> Gen ModelSnapshot
forall a. HasCallStack => [a] -> Gen a
elements [ModelSnapshot]
knownSnapshots
                    Any (Action Model) -> Gen (Any (Action Model))
forall a. a -> Gen a
forall (f :: * -> *) a. Applicative f => a -> f a
pure (Any (Action Model) -> Gen (Any (Action Model)))
-> Any (Action Model) -> Gen (Any (Action Model))
forall a b. (a -> b) -> a -> b
$ Action Model TxResult -> Any (Action Model)
forall a (f :: * -> *). (Typeable a, Eq (f a)) => f a -> Any f
Some Contest{Actor
$sel:actor:NewSnapshot :: Actor
actor :: Actor
actor, ModelSnapshot
$sel:snapshot:NewSnapshot :: ModelSnapshot
snapshot :: ModelSnapshot
snapshot}
                )
              | Bool -> Bool
not ([ModelSnapshot] -> Bool
forall a. [a] -> Bool
forall (t :: * -> *) a. Foldable t => t a -> Bool
null [ModelSnapshot]
knownSnapshots)
              ]
      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
      -- Only decommit if not already pending
      ModelUTxO
toDecommit <-
        if ModelUTxO -> Bool
forall a. [a] -> Bool
forall (t :: * -> *) a. Foldable t => t a -> Bool
null ModelUTxO
pendingDecommit
          then ModelUTxO -> Gen ModelUTxO
forall a. [a] -> Gen [a]
sublistOf ModelUTxO
utxoInHead
          else ModelUTxO -> Gen ModelUTxO
forall a. a -> Gen a
forall (f :: * -> *) a. Applicative f => a -> f a
pure ModelUTxO
pendingDecommit
      ModelUTxO
inHead <- ModelUTxO -> Gen ModelUTxO
forall a. [a] -> Gen [a]
shuffle (ModelUTxO -> Gen ModelUTxO) -> ModelUTxO -> Gen ModelUTxO
forall a b. (a -> b) -> a -> b
$ ModelUTxO
utxoInHead ModelUTxO -> ModelUTxO -> ModelUTxO
forall a. Eq a => [a] -> [a] -> [a]
\\ ModelUTxO
toDecommit
      let validSnapshot :: ModelSnapshot
validSnapshot =
            ModelSnapshot
              { $sel:version:ModelSnapshot :: SnapshotVersion
version = SnapshotVersion
currentVersion
              , $sel:number:ModelSnapshot :: SnapshotNumber
number = [ModelSnapshot] -> SnapshotNumber
latestSnapshotNumber [ModelSnapshot]
knownSnapshots SnapshotNumber -> SnapshotNumber -> SnapshotNumber
forall a. Num a => a -> a -> a
+ SnapshotNumber
1
              , ModelUTxO
$sel:inHead:ModelSnapshot :: ModelUTxO
inHead :: ModelUTxO
inHead
              , ModelUTxO
$sel:toDecommit:ModelSnapshot :: ModelUTxO
toDecommit :: ModelUTxO
toDecommit
              }
      ModelSnapshot -> Gen ModelSnapshot
forall a. a -> Gen a
forall (f :: * -> *) a. Applicative f => a -> f a
pure ModelSnapshot
validSnapshot

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

  -- 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, [ModelSnapshot]
$sel:knownSnapshots:Model :: Model -> [ModelSnapshot]
knownSnapshots :: [ModelSnapshot]
knownSnapshots, SnapshotVersion
$sel:currentVersion:Model :: Model -> SnapshotVersion
currentVersion :: SnapshotVersion
currentVersion} = \case
    Action Model a
R:ActionModela a
Stop -> Bool
False
    NewSnapshot{} -> Bool
False
    -- Only filter non-matching states as we are not interested in these kind of
    -- verification failures.
    Decrement{ModelSnapshot
$sel:snapshot:NewSnapshot :: Action Model TxResult -> ModelSnapshot
snapshot :: ModelSnapshot
snapshot} ->
      State
headState State -> State -> Bool
forall a. Eq a => a -> a -> Bool
== State
Open
        Bool -> Bool -> Bool
&& ModelSnapshot
snapshot ModelSnapshot -> [ModelSnapshot] -> Bool
forall (f :: * -> *) a.
(Foldable f, DisallowElem f, Eq a) =>
a -> f a -> Bool
`elem` [ModelSnapshot]
knownSnapshots
        Bool -> Bool -> Bool
&& ModelSnapshot
snapshot.version SnapshotVersion -> SnapshotVersion -> Bool
forall a. Eq a => a -> a -> Bool
/= SnapshotVersion
currentVersion
    Close{ModelSnapshot
$sel:snapshot:NewSnapshot :: Action Model TxResult -> ModelSnapshot
snapshot :: ModelSnapshot
snapshot} ->
      State
headState State -> State -> Bool
forall a. Eq a => a -> a -> Bool
== State
Open
        Bool -> Bool -> Bool
&& ModelSnapshot
snapshot ModelSnapshot -> [ModelSnapshot] -> Bool
forall (f :: * -> *) a.
(Foldable f, DisallowElem f, Eq a) =>
a -> f a -> Bool
`elem` [ModelSnapshot]
knownSnapshots
        Bool -> Bool -> Bool
&& ( 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])
           )
    Contest{ModelSnapshot
$sel:snapshot:NewSnapshot :: Action Model TxResult -> ModelSnapshot
snapshot :: ModelSnapshot
snapshot} ->
      State
headState State -> State -> Bool
forall a. Eq a => a -> a -> Bool
== State
Closed
        Bool -> Bool -> Bool
&& ModelSnapshot
snapshot ModelSnapshot -> [ModelSnapshot] -> Bool
forall (f :: * -> *) a.
(Foldable f, DisallowElem f, Eq a) =>
a -> f a -> Bool
`elem` [ModelSnapshot]
knownSnapshots
    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
      NewSnapshot{ModelSnapshot
$sel:newSnapshot:NewSnapshot :: Action Model () -> ModelSnapshot
newSnapshot :: ModelSnapshot
newSnapshot} ->
        Model
m
          { knownSnapshots = newSnapshot : m.knownSnapshots
          , pendingDecommit = newSnapshot.toDecommit
          }
      Decrement{ModelSnapshot
$sel:snapshot:NewSnapshot :: Action Model TxResult -> ModelSnapshot
snapshot :: ModelSnapshot
snapshot} ->
        Model
m
          { headState = Open
          , currentVersion = m.currentVersion + 1
          , utxoInHead = m.utxoInHead \\ snapshot.toDecommit
          , pendingDecommit = mempty
          }
      Close{ModelSnapshot
$sel:snapshot:NewSnapshot :: Action Model TxResult -> ModelSnapshot
snapshot :: ModelSnapshot
snapshot} ->
        Model
m
          { headState = Closed
          , closedSnapshotNumber = snapshot.number
          , alreadyContested = []
          , utxoInHead = snapshot.inHead
          , pendingDecommit = if currentVersion == snapshot.version then toDecommit snapshot else mempty
          }
      Contest{Actor
$sel:actor:NewSnapshot :: Action Model TxResult -> Actor
actor :: Actor
actor, ModelSnapshot
$sel:snapshot:NewSnapshot :: Action Model TxResult -> ModelSnapshot
snapshot :: ModelSnapshot
snapshot} ->
        Model
m
          { headState = Closed
          , closedSnapshotNumber = snapshot.number
          , alreadyContested = actor : alreadyContested m
          , utxoInHead = snapshot.inHead
          , pendingDecommit = if currentVersion == snapshot.version then toDecommit snapshot else mempty
          }
      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

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

  postcondition :: forall a.
(Model, Model)
-> Action Model a
-> LookUp AppM
-> Realized AppM a
-> PostconditionM AppM Bool
postcondition (Model
modelBefore, Model
modelAfter) Action Model a
action LookUp AppM
_lookup Realized AppM a
result = PostconditionM' AppM () -> PostconditionM AppM Bool
forall (m :: * -> *).
Monad m =>
PostconditionM' m () -> PostconditionM m Bool
runPostconditionM' (PostconditionM' AppM () -> PostconditionM AppM Bool)
-> PostconditionM' AppM () -> PostconditionM AppM Bool
forall a b. (a -> b) -> a -> b
$ do
    String -> PostconditionM' AppM ()
forall (m :: * -> *). Monad m => String -> PostconditionM' m ()
counterexample' (Model -> String
forall a. Show a => a -> String
show Model
modelBefore)
    String -> PostconditionM' AppM ()
forall (m :: * -> *). Monad m => String -> PostconditionM' m ()
counterexample' (Action Model a -> String
forall a. Show a => a -> String
show Action Model a
action)
    case Action Model a
action of
      Decrement{} -> TxResult
-> (HeadObservation -> PostconditionM' AppM ())
-> PostconditionM' AppM ()
forall (m :: * -> *) a.
Monad m =>
TxResult
-> (HeadObservation -> PostconditionM' m a) -> PostconditionM' m a
expectValid Realized AppM a
TxResult
result ((HeadObservation -> PostconditionM' AppM ())
 -> PostconditionM' AppM ())
-> (HeadObservation -> PostconditionM' AppM ())
-> PostconditionM' AppM ()
forall a b. (a -> b) -> a -> b
$ \case
        Tx.Decrement{} -> () -> PostconditionM' AppM ()
forall a. a -> PostconditionM' AppM a
forall (f :: * -> *) a. Applicative f => a -> f a
pure ()
        HeadObservation
_ -> String -> PostconditionM' AppM ()
forall a. String -> PostconditionM' AppM a
forall (m :: * -> *) a. MonadFail m => String -> m a
fail String
"Expected Decrement"
      Close{} -> TxResult
-> (HeadObservation -> PostconditionM' AppM ())
-> PostconditionM' AppM ()
forall (m :: * -> *) a.
Monad m =>
TxResult
-> (HeadObservation -> PostconditionM' m a) -> PostconditionM' m a
expectValid Realized AppM a
TxResult
result ((HeadObservation -> PostconditionM' AppM ())
 -> PostconditionM' AppM ())
-> (HeadObservation -> PostconditionM' AppM ())
-> PostconditionM' AppM ()
forall a b. (a -> b) -> a -> b
$ \case
        Tx.Close{} -> () -> PostconditionM' AppM ()
forall a. a -> PostconditionM' AppM a
forall (f :: * -> *) a. Applicative f => a -> f a
pure ()
        HeadObservation
_ -> String -> PostconditionM' AppM ()
forall a. String -> PostconditionM' AppM a
forall (m :: * -> *) a. MonadFail m => String -> m a
fail String
"Expected Close"
      Contest{} -> TxResult
-> (HeadObservation -> PostconditionM' AppM ())
-> PostconditionM' AppM ()
forall (m :: * -> *) a.
Monad m =>
TxResult
-> (HeadObservation -> PostconditionM' m a) -> PostconditionM' m a
expectValid Realized AppM a
TxResult
result ((HeadObservation -> PostconditionM' AppM ())
 -> PostconditionM' AppM ())
-> (HeadObservation -> PostconditionM' AppM ())
-> PostconditionM' AppM ()
forall a b. (a -> b) -> a -> b
$ \case
        Tx.Contest Tx.ContestObservation{[PubKeyHash]
contesters :: [PubKeyHash]
$sel:contesters:ContestObservation :: ContestObservation -> [PubKeyHash]
contesters} -> do
          String -> PostconditionM' AppM ()
forall (m :: * -> *). Monad m => String -> PostconditionM' m ()
counterexample' (String -> PostconditionM' AppM ())
-> String -> PostconditionM' AppM ()
forall a b. (a -> b) -> a -> b
$ String
"Wrong contesters: expected " String -> ShowS
forall a. Semigroup a => a -> a -> a
<> [Actor] -> String
forall a. Show a => a -> String
show (Model -> [Actor]
alreadyContested Model
modelAfter) String -> ShowS
forall a. Semigroup a => a -> a -> a
<> String
", got " String -> ShowS
forall a. Semigroup a => a -> a -> a
<> [PubKeyHash] -> String
forall a. Show a => a -> String
show [PubKeyHash]
contesters
          Bool -> PostconditionM' AppM ()
forall (f :: * -> *). Alternative f => Bool -> f ()
guard (Bool -> PostconditionM' AppM ())
-> Bool -> PostconditionM' AppM ()
forall a b. (a -> b) -> a -> b
$ [PubKeyHash] -> Int
forall a. [a] -> Int
forall (t :: * -> *) a. Foldable t => t a -> Int
length [PubKeyHash]
contesters Int -> Int -> Bool
forall a. Eq a => a -> a -> Bool
== [Actor] -> Int
forall a. [a] -> Int
forall (t :: * -> *) a. Foldable t => t a -> Int
length (Model -> [Actor]
alreadyContested Model
modelAfter)
        HeadObservation
_ -> String -> PostconditionM' AppM ()
forall a. String -> PostconditionM' AppM a
forall (m :: * -> *) a. MonadFail m => String -> m a
fail String
"Expected Contest"
      Fanout{ModelUTxO
$sel:utxo:NewSnapshot :: Action Model TxResult -> ModelUTxO
utxo :: ModelUTxO
utxo, ModelUTxO
$sel:deltaUTxO:NewSnapshot :: 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, Lovelace))
-> [TxOut ctx] -> [TxOut ctx]
forall b a. Ord b => (a -> b) -> [a] -> [a]
sortOn (\TxOut ctx
o -> (TxOut ctx -> AddressInEra
forall ctx. TxOut ctx -> AddressInEra
txOutAddress TxOut ctx
o, Value -> Lovelace
selectLovelace (TxOut ctx -> Value
forall ctx. TxOut ctx -> Value
txOutValue TxOut ctx
o))) ([TxOut ctx] -> [TxOut ctx])
-> (UTxO' (TxOut ctx) -> [TxOut ctx])
-> UTxO' (TxOut ctx)
-> [TxOut ctx]
forall b c a. (b -> c) -> (a -> b) -> a -> c
. UTxO' (TxOut ctx) -> [TxOut ctx]
forall a. UTxO' a -> [a]
forall (t :: * -> *) a. Foldable t => t a -> [a]
toList
            let fannedOut :: UTxOType Tx
fannedOut = Tx -> UTxOType Tx
forall tx. IsTx tx => tx -> UTxOType tx
utxoFromTx Tx
tx
            Bool -> PostconditionM' AppM ()
forall (f :: * -> *). Alternative f => Bool -> f ()
guard (Bool -> PostconditionM' AppM ())
-> Bool -> PostconditionM' AppM ()
forall a b. (a -> b) -> a -> b
$ UTxO -> [TxOut CtxUTxO Era]
forall {ctx}. UTxO' (TxOut ctx) -> [TxOut ctx]
sorted UTxO
UTxOType Tx
fannedOut [TxOut CtxUTxO Era] -> [TxOut CtxUTxO Era] -> Bool
forall a. Eq a => a -> a -> Bool
== UTxO -> [TxOut CtxUTxO Era]
forall {ctx}. UTxO' (TxOut ctx) -> [TxOut ctx]
sorted (ModelUTxO -> UTxO
realWorldModelUTxO ModelUTxO
utxo UTxO -> UTxO -> UTxO
forall a. Semigroup a => a -> a -> a
<> ModelUTxO -> UTxO
realWorldModelUTxO ModelUTxO
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]

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

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

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

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

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

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

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

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

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

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

-- | Creates a 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
pendingDecommit = 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. [a] -> Bool
forall (t :: * -> *) a. Foldable t => t a -> Bool
null ModelUTxO
pendingDecommit then Maybe UTxO
forall a. Maybe a
Nothing else UTxO -> Maybe UTxO
forall a. a -> Maybe a
Just (UTxO -> Maybe UTxO) -> UTxO -> Maybe UTxO
forall a b. (a -> b) -> a -> b
$ ModelUTxO -> UTxO
realWorldModelUTxO ModelUTxO
pendingDecommit)
      SlotNo
deadline
 where
  CP.UnsafeContestationPeriod Nat
contestationPeriod = ContestationPeriod
Fixture.cperiod
  deadline :: SlotNo
deadline = Word64 -> SlotNo
SlotNo (Word64 -> SlotNo) -> Word64 -> SlotNo
forall a b. (a -> b) -> a -> b
$ Nat -> Word64
forall a b. (Integral a, Num b) => a -> b
fromIntegral Nat
contestationPeriod Word64 -> Word64 -> Word64
forall a. Num a => a -> a -> a
* Int -> Word64
forall a b. (Integral a, Num b) => a -> b
fromIntegral ([Actor] -> Int
forall a. [a] -> Int
forall (t :: * -> *) a. Foldable t => t a -> Int
length [Actor]
allActors)

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

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

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

-- * Helpers

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

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

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

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

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

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

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

-- | Generate sometimes a value with given generator, but 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. HasCallStack => [(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)]