-- | This module provides a framework for testing Plutus contracts built on "Test.QuickCheck". The
--   testing is model based, so to test a contract you define a type modelling the state of the
--   contract (or set of contracts) and provide an instance of the `ContractModel` class. This
--   instance specifies what operations (`Action`s) the contract supports, how they interact with
--   the model state, and how to execute them in the blockchain emulator ("Plutus.Trace.Emulator").
--   Tests are evaluated by running sequences of actions (random or user-specified) in the emulator
--   and comparing the state of the blockchain to the model state at the end.
--
--   Test cases are written in the `DL` monad, which supports mixing fixed sequences of actions with
--   random actions, making it easy to write properties like
--   /it is always possible to get all funds out of the contract/.

{-# LANGUAGE AllowAmbiguousTypes        #-}
{-# LANGUAGE ConstraintKinds            #-}
{-# LANGUAGE DataKinds                  #-}
{-# LANGUAGE DeriveDataTypeable         #-}
{-# LANGUAGE DerivingVia                #-}
{-# LANGUAGE FlexibleContexts           #-}
{-# LANGUAGE FlexibleInstances          #-}
{-# LANGUAGE GADTs                      #-}
{-# LANGUAGE GeneralizedNewtypeDeriving #-}
{-# LANGUAGE ImportQualifiedPost        #-}
{-# LANGUAGE MultiParamTypeClasses      #-}
{-# LANGUAGE NumericUnderscores         #-}
{-# LANGUAGE OverloadedStrings          #-}
{-# LANGUAGE PatternSynonyms            #-}
{-# LANGUAGE PolyKinds                  #-}
{-# LANGUAGE QuantifiedConstraints      #-}
{-# LANGUAGE RankNTypes                 #-}
{-# LANGUAGE ScopedTypeVariables        #-}
{-# LANGUAGE TemplateHaskell            #-}
{-# LANGUAGE TupleSections              #-}
{-# LANGUAGE TypeApplications           #-}
{-# LANGUAGE TypeFamilies               #-}
{-# LANGUAGE TypeOperators              #-}
{-# LANGUAGE UndecidableInstances       #-}
{-# LANGUAGE ViewPatterns               #-}
{-# OPTIONS_GHC -Wno-redundant-constraints -fno-warn-name-shadowing -Wno-orphans #-}

module Plutus.Contract.Test.ContractModel.Internal
  ( module Internal
  , module Plutus.Contract.Test.ContractModel.Internal
  ) where

import Cardano.Node.Emulator.Chain
import Cardano.Node.Emulator.Params
import Control.DeepSeq
import Control.Monad.Freer.Reader (Reader, ask, runReader)
import Control.Monad.Freer.State (State, get, modify, runState)
import Control.Monad.Writer as Writer (WriterT (..), runWriterT)
import Ledger.Blockchain
import Ledger.Tx
import Plutus.Trace.Effects.Waiting (Waiting)
import Plutus.Trace.Emulator (initialChainState, waitUntilSlot)
import Plutus.Trace.Emulator.Types (ContractHandle (..), ContractInstanceTag, UserThreadMsg (..))

import Control.Lens
import Control.Monad.Cont
import Control.Monad.Freer (Eff, Member, raise)
import Data.Data
import Data.IORef
import Data.List as List
import Data.Map qualified as Map
import Data.Maybe
import Data.Set (Set)
import Data.Set qualified as Set
import Data.Text qualified as Text
import GHC.Generics

import Cardano.Api (AssetId, SlotNo (..))
import Cardano.Api qualified as CardanoAPI
import Cardano.Crypto.Hash.Class qualified as Crypto
import Cardano.Node.Emulator.Params ()
import Ledger.Ada qualified as Ada
import Ledger.Address
import Ledger.Index as Index
import Ledger.Scripts
import Ledger.Slot
import Plutus.Contract (ContractInstanceId)
import Plutus.Contract.Test hiding (not)
import Plutus.Trace.Effects.EmulatorControl (discardWallets)
import Plutus.Trace.Emulator as Trace (BaseEmulatorEffects, EmulatorEffects, EmulatorTrace, activateContract,
                                       freezeContractInstance, waitNSlots)
import Plutus.V1.Ledger.Crypto
import PlutusTx.Builtins qualified as Builtins
import PlutusTx.Coverage hiding (_coverageIndex)
import PlutusTx.ErrorCodes
import Test.QuickCheck.DynamicLogic qualified as DL
import Test.QuickCheck.StateModel (Realized)
import Test.QuickCheck.StateModel qualified as StateModel

import Test.QuickCheck hiding (ShrinkState, checkCoverage, getSize, (.&&.), (.||.))
import Test.QuickCheck qualified as QC
import Test.QuickCheck.ContractModel as CM
import Test.QuickCheck.Monadic (PropertyM, monadic)
import Test.QuickCheck.Monadic qualified as QC

import Wallet.Emulator.MultiAgent (eteEvent)

import Plutus.Trace.Effects.EmulatorControl qualified as EmulatorControl
import Prettyprinter

import Plutus.Contract.Test.ContractModel.Internal.ContractInstance as Internal

-- Drops StartContract from EmulatorEffects
type SpecificationEmulatorTrace s =
  Eff ( Reader (Handles s)
     ': BaseEmulatorEffects
      )

type EmulatorTraceWithInstances s =
  Eff ( State (Handles s)
     ': EmulatorEffects
      )

type CheckableContractModel state =
  ( RunModel state (SpecificationEmulatorTrace state)
  , ContractInstanceModel state )

contractHandle :: (ContractInstanceModel state, Typeable w, Typeable schema, Typeable err, Typeable params)
       => ContractInstanceKey state w schema err params
       -> RunMonad (SpecificationEmulatorTrace state) (ContractHandle w schema err)
contractHandle :: ContractInstanceKey state w schema err params
-> RunMonad
     (SpecificationEmulatorTrace state) (ContractHandle w schema err)
contractHandle ContractInstanceKey state w schema err params
key = do
  IMap (ContractInstanceKey state) WalletContractHandle
handles <- Eff
  (Reader (IMap (ContractInstanceKey state) WalletContractHandle)
     : BaseEmulatorEffects)
  (IMap (ContractInstanceKey state) WalletContractHandle)
-> RunMonad
     (SpecificationEmulatorTrace state)
     (IMap (ContractInstanceKey state) WalletContractHandle)
forall (t :: (* -> *) -> * -> *) (m :: * -> *) a.
(MonadTrans t, Monad m) =>
m a -> t m a
lift Eff
  (Reader (IMap (ContractInstanceKey state) WalletContractHandle)
     : BaseEmulatorEffects)
  (IMap (ContractInstanceKey state) WalletContractHandle)
forall r (effs :: [* -> *]). Member (Reader r) effs => Eff effs r
ask
  case ContractInstanceKey state w schema err params
-> IMap (ContractInstanceKey state) WalletContractHandle
-> Maybe (WalletContractHandle w schema err)
forall i1 j1 k1 l1 (i2 :: i1) (j2 :: j1) (k2 :: k1) (l2 :: l1)
       (key :: i1 -> j1 -> k1 -> l1 -> *) (val :: i1 -> j1 -> k1 -> *).
(Typeable i2, Typeable j2, Typeable k2, Typeable l2, Typeable key,
 Typeable val, Eq (key i2 j2 k2 l2)) =>
key i2 j2 k2 l2 -> IMap key val -> Maybe (val i2 j2 k2)
imLookup ContractInstanceKey state w schema err params
key IMap (ContractInstanceKey state) WalletContractHandle
handles of
    Just (WalletContractHandle Wallet
_ ContractHandle w schema err
h) -> ContractHandle w schema err
-> RunMonad
     (SpecificationEmulatorTrace state) (ContractHandle w schema err)
forall (f :: * -> *) a. Applicative f => a -> f a
pure ContractHandle w schema err
h
    Maybe (WalletContractHandle w schema err)
Nothing                         -> [Char]
-> RunMonad
     (SpecificationEmulatorTrace state) (ContractHandle w schema err)
forall a. HasCallStack => [Char] -> a
error ([Char]
 -> RunMonad
      (SpecificationEmulatorTrace state) (ContractHandle w schema err))
-> [Char]
-> RunMonad
     (SpecificationEmulatorTrace state) (ContractHandle w schema err)
forall a b. (a -> b) -> a -> b
$ [Char]
"contractHandle: No handle for " [Char] -> [Char] -> [Char]
forall a. [a] -> [a] -> [a]
++ ContractInstanceKey state w schema err params -> [Char]
forall a. Show a => a -> [Char]
show ContractInstanceKey state w schema err params
key

activateWallets :: ContractInstanceModel state
                => (SymToken -> AssetId)
                -> [StartContract state]
                -> EmulatorTraceWithInstances state ()
activateWallets :: (SymToken -> AssetId)
-> [StartContract state] -> EmulatorTraceWithInstances state ()
activateWallets SymToken -> AssetId
_ [] = () -> EmulatorTraceWithInstances state ()
forall (m :: * -> *) a. Monad m => a -> m a
return ()
activateWallets SymToken -> AssetId
sa (StartContract ContractInstanceKey state w s e p
key p
params : [StartContract state]
starts) = do
    let wallet :: Wallet
wallet = ContractInstanceKey state w s e p -> Wallet
forall state w (s :: Row *) e p.
ContractInstanceModel state =>
ContractInstanceKey state w s e p -> Wallet
instanceWallet ContractInstanceKey state w s e p
key
    ContractHandle w s e
h <- Wallet
-> Contract w s e ()
-> ContractInstanceTag
-> Eff
     (State (Handles state) : EmulatorEffects) (ContractHandle w s e)
forall (contract :: * -> Row * -> * -> * -> *) (s :: Row *) e w a
       (effs :: [* -> *]).
(IsContract contract, ContractConstraints s, Show e, FromJSON e,
 ToJSON e, ToJSON w, Monoid w, FromJSON w,
 Member StartContract effs) =>
Wallet
-> contract w s e a
-> ContractInstanceTag
-> Eff effs (ContractHandle w s e)
activateContract Wallet
wallet ((SymToken -> AssetId)
-> ContractInstanceKey state w s e p -> p -> Contract w s e ()
forall state w (s :: Row *) e p.
ContractInstanceModel state =>
(SymToken -> AssetId)
-> ContractInstanceKey state w s e p -> p -> Contract w s e ()
instanceContract SymToken -> AssetId
sa ContractInstanceKey state w s e p
key p
params) (ContractInstanceKey state w s e p -> ContractInstanceTag
forall state w (s :: Row *) e p.
(ContractInstanceModel state, SchemaConstraints w s e) =>
ContractInstanceKey state w s e p -> ContractInstanceTag
instanceTag ContractInstanceKey state w s e p
key)
    (Handles state -> Handles state)
-> EmulatorTraceWithInstances state ()
forall s (effs :: [* -> *]).
Member (State s) effs =>
(s -> s) -> Eff effs ()
modify ((Handles state -> Handles state)
 -> EmulatorTraceWithInstances state ())
-> (Handles state -> Handles state)
-> EmulatorTraceWithInstances state ()
forall a b. (a -> b) -> a -> b
$ ContractInstanceKey state w s e p
-> WalletContractHandle w s e -> Handles state -> Handles state
forall i j k l (i :: i) (j :: j) (k :: k) (l :: l)
       (key :: i -> j -> k -> l -> *) (val :: i -> j -> k -> *).
(Typeable i, Typeable j, Typeable k, Typeable l) =>
key i j k l -> val i j k -> IMap key val -> IMap key val
IMCons ContractInstanceKey state w s e p
key (Wallet -> ContractHandle w s e -> WalletContractHandle w s e
forall w (s :: Row *) e.
Wallet -> ContractHandle w s e -> WalletContractHandle w s e
WalletContractHandle Wallet
wallet ContractHandle w s e
h)
    (SymToken -> AssetId)
-> [StartContract state] -> EmulatorTraceWithInstances state ()
forall state.
ContractInstanceModel state =>
(SymToken -> AssetId)
-> [StartContract state] -> EmulatorTraceWithInstances state ()
activateWallets SymToken -> AssetId
sa [StartContract state]
starts

-- | Used to freeze other wallets when checking a `NoLockedFundsProof`.
instancesForOtherWallets :: Wallet -> Handles state -> [ContractInstanceId]
instancesForOtherWallets :: Wallet -> Handles state -> [ContractInstanceId]
instancesForOtherWallets Wallet
_ Handles state
IMNil = []
instancesForOtherWallets Wallet
w (IMCons ContractInstanceKey state i j k l
_ (WalletContractHandle Wallet
w' ContractHandle i j k
h) Handles state
m)
  | Wallet
w Wallet -> Wallet -> Bool
forall a. Eq a => a -> a -> Bool
/= Wallet
w'   = ContractHandle i j k -> ContractInstanceId
forall w (s :: Row *) e. ContractHandle w s e -> ContractInstanceId
chInstanceId ContractHandle i j k
h ContractInstanceId -> [ContractInstanceId] -> [ContractInstanceId]
forall a. a -> [a] -> [a]
: Wallet -> Handles state -> [ContractInstanceId]
forall state. Wallet -> Handles state -> [ContractInstanceId]
instancesForOtherWallets Wallet
w Handles state
m
  | Bool
otherwise = Wallet -> Handles state -> [ContractInstanceId]
forall state. Wallet -> Handles state -> [ContractInstanceId]
instancesForOtherWallets Wallet
w Handles state
m

newtype WithInstances s = WithInstances { WithInstances s -> s
withoutInstances :: s }
  deriving (WithInstances s -> WithInstances s -> Bool
(WithInstances s -> WithInstances s -> Bool)
-> (WithInstances s -> WithInstances s -> Bool)
-> Eq (WithInstances s)
forall s. Eq s => WithInstances s -> WithInstances s -> Bool
forall a. (a -> a -> Bool) -> (a -> a -> Bool) -> Eq a
/= :: WithInstances s -> WithInstances s -> Bool
$c/= :: forall s. Eq s => WithInstances s -> WithInstances s -> Bool
== :: WithInstances s -> WithInstances s -> Bool
$c== :: forall s. Eq s => WithInstances s -> WithInstances s -> Bool
Eq, (forall x. WithInstances s -> Rep (WithInstances s) x)
-> (forall x. Rep (WithInstances s) x -> WithInstances s)
-> Generic (WithInstances s)
forall x. Rep (WithInstances s) x -> WithInstances s
forall x. WithInstances s -> Rep (WithInstances s) x
forall a.
(forall x. a -> Rep a x) -> (forall x. Rep a x -> a) -> Generic a
forall s x. Rep (WithInstances s) x -> WithInstances s
forall s x. WithInstances s -> Rep (WithInstances s) x
$cto :: forall s x. Rep (WithInstances s) x -> WithInstances s
$cfrom :: forall s x. WithInstances s -> Rep (WithInstances s) x
Generic)
  deriving newtype (Int -> WithInstances s -> [Char] -> [Char]
[WithInstances s] -> [Char] -> [Char]
WithInstances s -> [Char]
(Int -> WithInstances s -> [Char] -> [Char])
-> (WithInstances s -> [Char])
-> ([WithInstances s] -> [Char] -> [Char])
-> Show (WithInstances s)
forall s. Show s => Int -> WithInstances s -> [Char] -> [Char]
forall s. Show s => [WithInstances s] -> [Char] -> [Char]
forall s. Show s => WithInstances s -> [Char]
forall a.
(Int -> a -> [Char] -> [Char])
-> (a -> [Char]) -> ([a] -> [Char] -> [Char]) -> Show a
showList :: [WithInstances s] -> [Char] -> [Char]
$cshowList :: forall s. Show s => [WithInstances s] -> [Char] -> [Char]
show :: WithInstances s -> [Char]
$cshow :: forall s. Show s => WithInstances s -> [Char]
showsPrec :: Int -> WithInstances s -> [Char] -> [Char]
$cshowsPrec :: forall s. Show s => Int -> WithInstances s -> [Char] -> [Char]
Show)

instance CheckableContractModel state =>
         RunModel (WithInstances state) (EmulatorTraceWithInstances state) where
  perform :: ModelState (WithInstances state)
-> Action (WithInstances state)
-> (SymToken -> AssetId)
-> RunMonad (EmulatorTraceWithInstances state) ()
perform ModelState (WithInstances state)
si (UnderlyingAction a) SymToken -> AssetId
symEnv = do
    let s :: ModelState state
s = WithInstances state -> state
forall s. WithInstances s -> s
withoutInstances (WithInstances state -> state)
-> ModelState (WithInstances state) -> ModelState state
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> ModelState (WithInstances state)
si
    Eff (State (Handles state) : EmulatorEffects) ()
-> RunMonad (EmulatorTraceWithInstances state) ()
forall (t :: (* -> *) -> * -> *) (m :: * -> *) a.
(MonadTrans t, Monad m) =>
m a -> t m a
lift (Eff (State (Handles state) : EmulatorEffects) ()
 -> RunMonad (EmulatorTraceWithInstances state) ())
-> Eff (State (Handles state) : EmulatorEffects) ()
-> RunMonad (EmulatorTraceWithInstances state) ()
forall a b. (a -> b) -> a -> b
$ (SymToken -> AssetId)
-> [StartContract state]
-> Eff (State (Handles state) : EmulatorEffects) ()
forall state.
ContractInstanceModel state =>
(SymToken -> AssetId)
-> [StartContract state] -> EmulatorTraceWithInstances state ()
activateWallets SymToken -> AssetId
symEnv ([StartContract state]
 -> Eff (State (Handles state) : EmulatorEffects) ())
-> [StartContract state]
-> Eff (State (Handles state) : EmulatorEffects) ()
forall a b. (a -> b) -> a -> b
$ ModelState state -> Action state -> [StartContract state]
forall state.
ContractInstanceModel state =>
ModelState state -> Action state -> [StartContract state]
startInstances ModelState state
s Action state
a
    (forall a1.
 SpecificationEmulatorTrace state a1
 -> EmulatorTraceWithInstances state a1)
-> RunMonad (SpecificationEmulatorTrace state) ()
-> RunMonad (EmulatorTraceWithInstances state) ()
forall (m :: * -> *) (n :: * -> *) a.
(forall a1. m a1 -> n a1) -> RunMonad m a -> RunMonad n a
liftRunMonad forall a1.
SpecificationEmulatorTrace state a1
-> EmulatorTraceWithInstances state a1
forall s a.
SpecificationEmulatorTrace s a -> EmulatorTraceWithInstances s a
liftSpecificationTrace (RunMonad (SpecificationEmulatorTrace state) ()
 -> RunMonad (EmulatorTraceWithInstances state) ())
-> RunMonad (SpecificationEmulatorTrace state) ()
-> RunMonad (EmulatorTraceWithInstances state) ()
forall a b. (a -> b) -> a -> b
$ ModelState state
-> Action state
-> (SymToken -> AssetId)
-> RunMonad (SpecificationEmulatorTrace state) ()
forall state (m :: * -> *).
RunModel state m =>
ModelState state
-> Action state -> (SymToken -> AssetId) -> RunMonad m ()
perform @_ @(SpecificationEmulatorTrace state) ModelState state
s Action state
a SymToken -> AssetId
symEnv
  perform ModelState (WithInstances state)
_ (Unilateral w) SymToken -> AssetId
_ = do
    Handles state
h <- Eff (State (Handles state) : EmulatorEffects) (Handles state)
-> RunMonad (EmulatorTraceWithInstances state) (Handles state)
forall (t :: (* -> *) -> * -> *) (m :: * -> *) a.
(MonadTrans t, Monad m) =>
m a -> t m a
lift (Eff (State (Handles state) : EmulatorEffects) (Handles state)
 -> RunMonad (EmulatorTraceWithInstances state) (Handles state))
-> Eff (State (Handles state) : EmulatorEffects) (Handles state)
-> RunMonad (EmulatorTraceWithInstances state) (Handles state)
forall a b. (a -> b) -> a -> b
$ forall (effs :: [* -> *]).
Member (State (Handles state)) effs =>
Eff effs (Handles state)
forall s (effs :: [* -> *]). Member (State s) effs => Eff effs s
get @(Handles state)
    let insts :: [ContractInstanceId]
insts = Wallet -> Handles state -> [ContractInstanceId]
forall state. Wallet -> Handles state -> [ContractInstanceId]
instancesForOtherWallets Wallet
w Handles state
h
    Eff (State (Handles state) : EmulatorEffects) ()
-> RunMonad (EmulatorTraceWithInstances state) ()
forall (t :: (* -> *) -> * -> *) (m :: * -> *) a.
(MonadTrans t, Monad m) =>
m a -> t m a
lift (Eff (State (Handles state) : EmulatorEffects) ()
 -> RunMonad (EmulatorTraceWithInstances state) ())
-> Eff (State (Handles state) : EmulatorEffects) ()
-> RunMonad (EmulatorTraceWithInstances state) ()
forall a b. (a -> b) -> a -> b
$ (ContractInstanceId
 -> Eff (State (Handles state) : EmulatorEffects) ())
-> [ContractInstanceId]
-> Eff (State (Handles state) : EmulatorEffects) ()
forall (t :: * -> *) (m :: * -> *) a b.
(Foldable t, Monad m) =>
(a -> m b) -> t a -> m ()
mapM_ ContractInstanceId
-> Eff (State (Handles state) : EmulatorEffects) ()
forall (effs :: [* -> *]).
Member EmulatorControl effs =>
ContractInstanceId -> Eff effs ()
freezeContractInstance [ContractInstanceId]
insts
    Eff (State (Handles state) : EmulatorEffects) ()
-> RunMonad (EmulatorTraceWithInstances state) ()
forall (t :: (* -> *) -> * -> *) (m :: * -> *) a.
(MonadTrans t, Monad m) =>
m a -> t m a
lift (Eff (State (Handles state) : EmulatorEffects) ()
 -> RunMonad (EmulatorTraceWithInstances state) ())
-> Eff (State (Handles state) : EmulatorEffects) ()
-> RunMonad (EmulatorTraceWithInstances state) ()
forall a b. (a -> b) -> a -> b
$ (Wallet -> Bool)
-> Eff (State (Handles state) : EmulatorEffects) ()
forall (effs :: [* -> *]).
Member EmulatorControl effs =>
(Wallet -> Bool) -> Eff effs ()
discardWallets (Wallet
w Wallet -> Wallet -> Bool
forall a. Eq a => a -> a -> Bool
/=)
  monitoring :: (ModelState (WithInstances state),
 ModelState (WithInstances state))
-> Action (WithInstances state)
-> (SymToken -> AssetId)
-> Map [Char] AssetId
-> Property
-> Property
monitoring (ModelState (WithInstances state)
s, ModelState (WithInstances state)
s') (UnderlyingAction a) = (ModelState state, ModelState state)
-> Action state
-> (SymToken -> AssetId)
-> Map [Char] AssetId
-> Property
-> Property
forall state (m :: * -> *).
RunModel state m =>
(ModelState state, ModelState state)
-> Action state
-> (SymToken -> AssetId)
-> Map [Char] AssetId
-> Property
-> Property
monitoring @_ @(SpecificationEmulatorTrace state)
                                                       (WithInstances state -> state
forall s. WithInstances s -> s
withoutInstances (WithInstances state -> state)
-> ModelState (WithInstances state) -> ModelState state
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> ModelState (WithInstances state)
s, WithInstances state -> state
forall s. WithInstances s -> s
withoutInstances (WithInstances state -> state)
-> ModelState (WithInstances state) -> ModelState state
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> ModelState (WithInstances state)
s') Action state
a
  monitoring (ModelState (WithInstances state),
 ModelState (WithInstances state))
_ Unilateral{} = \ SymToken -> AssetId
_ Map [Char] AssetId
_ -> Property -> Property
forall a. a -> a
id

liftSpecificationTrace :: SpecificationEmulatorTrace s a -> EmulatorTraceWithInstances s a
liftSpecificationTrace :: SpecificationEmulatorTrace s a -> EmulatorTraceWithInstances s a
liftSpecificationTrace SpecificationEmulatorTrace s a
m = do
  Handles s
s <- Eff (State (Handles s) : EmulatorEffects) (Handles s)
forall s (effs :: [* -> *]). Member (State s) effs => Eff effs s
get
  Eff EmulatorEffects a -> EmulatorTraceWithInstances s a
forall (effs :: [* -> *]) a (e :: * -> *).
Eff effs a -> Eff (e : effs) a
raise (Eff EmulatorEffects a -> EmulatorTraceWithInstances s a)
-> (Eff BaseEmulatorEffects a -> Eff EmulatorEffects a)
-> Eff BaseEmulatorEffects a
-> EmulatorTraceWithInstances s a
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Eff BaseEmulatorEffects a -> Eff EmulatorEffects a
forall (effs :: [* -> *]) a (e :: * -> *).
Eff effs a -> Eff (e : effs) a
raise (Eff BaseEmulatorEffects a -> EmulatorTraceWithInstances s a)
-> Eff BaseEmulatorEffects a -> EmulatorTraceWithInstances s a
forall a b. (a -> b) -> a -> b
$ Handles s
-> SpecificationEmulatorTrace s a -> Eff BaseEmulatorEffects a
forall r (effs :: [* -> *]) a.
r -> Eff (Reader r : effs) a -> Eff effs a
runReader Handles s
s SpecificationEmulatorTrace s a
m

instance HasChainIndex (EmulatorTraceWithInstances state) where
  getChainIndex :: EmulatorTraceWithInstances state ChainIndex
getChainIndex = do
    NetworkId
nid <- Params -> NetworkId
pNetworkId (Params -> NetworkId)
-> Eff (State (Handles state) : EmulatorEffects) Params
-> Eff (State (Handles state) : EmulatorEffects) NetworkId
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> Eff (State (Handles state) : EmulatorEffects) Params
forall (effs :: [* -> *]).
Member EmulatorControl effs =>
Eff effs Params
EmulatorControl.getParams
    NetworkId -> ChainState -> ChainIndex
chainStateToChainIndex NetworkId
nid (ChainState -> ChainIndex)
-> Eff (State (Handles state) : EmulatorEffects) ChainState
-> EmulatorTraceWithInstances state ChainIndex
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> Eff (State (Handles state) : EmulatorEffects) ChainState
forall (effs :: [* -> *]).
Member EmulatorControl effs =>
Eff effs ChainState
EmulatorControl.chainState
    -- Note, we don't store the genesis transaction in the index but put it in the before state
    -- instead to avoid showing that as a balance change in the models.
    where chainStateToChainIndex :: NetworkId -> ChainState -> ChainIndex
chainStateToChainIndex NetworkId
nid ChainState
cs =
            ChainIndex :: ChainState -> ChainState -> [TxInState] -> NetworkId -> ChainIndex
ChainIndex { before :: ChainState
before = ChainState
beforeState
                       , after :: ChainState
after  = ChainState :: SlotNo -> UTxO Era -> ChainState
CM.ChainState
                                    { slot :: SlotNo
slot = Integer -> SlotNo
forall a. Num a => Integer -> a
fromInteger (Integer -> SlotNo) -> (Slot -> Integer) -> Slot -> SlotNo
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Slot -> Integer
forall a. Integral a => a -> Integer
toInteger (Slot -> SlotNo) -> Slot -> SlotNo
forall a b. (a -> b) -> a -> b
$ ChainState -> Slot
_chainCurrentSlot ChainState
cs
                                    , utxo :: UTxO Era
utxo = UtxoIndex -> UTxO Era
makeUTxOs (UtxoIndex -> UTxO Era) -> UtxoIndex -> UTxO Era
forall a b. (a -> b) -> a -> b
$ Blockchain -> UtxoIndex
Index.initialise (ChainState -> Blockchain
_chainNewestFirst ChainState
cs)
                                    }
                       -- The Backwards order
                       , transactions :: [TxInState]
transactions = ([TxInState], ChainState) -> [TxInState]
forall a b. (a, b) -> a
fst (([TxInState], ChainState) -> [TxInState])
-> ([TxInState], ChainState) -> [TxInState]
forall a b. (a -> b) -> a -> b
$ ([OnChainTx]
 -> ([TxInState], ChainState) -> ([TxInState], ChainState))
-> ([TxInState], ChainState)
-> Blockchain
-> ([TxInState], ChainState)
forall (t :: * -> *) a b.
Foldable t =>
(a -> b -> b) -> b -> t a -> b
foldr [OnChainTx]
-> ([TxInState], ChainState) -> ([TxInState], ChainState)
addBlock ([], ChainState
beforeState)
                                                             ( Blockchain -> Blockchain
forall a. [a] -> [a]
reverse
                                                             (Blockchain -> Blockchain)
-> (ChainState -> Blockchain) -> ChainState -> Blockchain
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Int -> Blockchain -> Blockchain
forall a. Int -> [a] -> [a]
drop Int
1
                                                             (Blockchain -> Blockchain)
-> (ChainState -> Blockchain) -> ChainState -> Blockchain
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Blockchain -> Blockchain
forall a. [a] -> [a]
reverse
                                                             (Blockchain -> Blockchain)
-> (ChainState -> Blockchain) -> ChainState -> Blockchain
forall b c a. (b -> c) -> (a -> b) -> a -> c
. ChainState -> Blockchain
_chainNewestFirst
                                                             (ChainState -> Blockchain) -> ChainState -> Blockchain
forall a b. (a -> b) -> a -> b
$ ChainState
cs)
                       , networkId :: NetworkId
networkId = NetworkId
nid
                       }
            where beforeState :: ChainState
beforeState = ChainState :: SlotNo -> UTxO Era -> ChainState
CM.ChainState { slot :: SlotNo
slot = SlotNo
0
                                              , utxo :: UTxO Era
utxo = UtxoIndex -> UTxO Era
makeUTxOs
                                                     (UtxoIndex -> UTxO Era) -> UtxoIndex -> UTxO Era
forall a b. (a -> b) -> a -> b
$ Blockchain -> UtxoIndex
Index.initialise (Int -> Blockchain -> Blockchain
forall a. Int -> [a] -> [a]
take Int
1 (Blockchain -> Blockchain) -> Blockchain -> Blockchain
forall a b. (a -> b) -> a -> b
$ Blockchain -> Blockchain
forall a. [a] -> [a]
reverse (ChainState -> Blockchain
_chainNewestFirst ChainState
cs))
                                              }
                  addBlock :: [OnChainTx]
-> ([TxInState], ChainState) -> ([TxInState], ChainState)
addBlock [OnChainTx]
block ([TxInState]
txs, ChainState
state) =
                    ( [TxInState]
txs [TxInState] -> [TxInState] -> [TxInState]
forall a. [a] -> [a] -> [a]
++ [ Tx Era -> ChainState -> Bool -> TxInState
TxInState ((\(CardanoApiEmulatorEraTx Tx Era
tx) -> Tx Era
tx) (SomeCardanoApiTx -> Tx Era)
-> (OnChainTx -> SomeCardanoApiTx) -> OnChainTx -> Tx Era
forall b c a. (b -> c) -> (a -> b) -> a -> c
. CardanoTx -> SomeCardanoApiTx
_cardanoApiTx (CardanoTx -> SomeCardanoApiTx)
-> (OnChainTx -> CardanoTx) -> OnChainTx -> SomeCardanoApiTx
forall b c a. (b -> c) -> (a -> b) -> a -> c
. OnChainTx -> CardanoTx
unOnChain (OnChainTx -> Tx Era) -> OnChainTx -> Tx Era
forall a b. (a -> b) -> a -> b
$ OnChainTx
tx)
                                         ChainState
state
                                         (OnChainTx -> Bool
onChainTxIsValid OnChainTx
tx)
                             | OnChainTx
tx <- [OnChainTx]
block ]
                    , [OnChainTx] -> ChainState -> ChainState
updateState [OnChainTx]
block ChainState
state )

                  updateState :: [OnChainTx] -> CM.ChainState -> CM.ChainState
                  updateState :: [OnChainTx] -> ChainState -> ChainState
updateState [OnChainTx]
block ChainState
state =
                    ChainState :: SlotNo -> UTxO Era -> ChainState
CM.ChainState{ slot :: SlotNo
slot = ChainState -> SlotNo
slot ChainState
state SlotNo -> SlotNo -> SlotNo
forall a. Num a => a -> a -> a
+ SlotNo
1
                                 , utxo :: UTxO Era
utxo = (OnChainTx -> UTxO Era -> UTxO Era)
-> UTxO Era -> [OnChainTx] -> UTxO Era
forall (t :: * -> *) a b.
Foldable t =>
(a -> b -> b) -> b -> t a -> b
foldr OnChainTx -> UTxO Era -> UTxO Era
addTx (ChainState -> UTxO Era
utxo ChainState
state) [OnChainTx]
block
                                 }

                  addTx :: OnChainTx -> CardanoAPI.UTxO CM.Era -> CardanoAPI.UTxO CM.Era
                  addTx :: OnChainTx -> UTxO Era -> UTxO Era
addTx OnChainTx
tx (CardanoAPI.UTxO Map TxIn (TxOut CtxUTxO Era)
utxos) =
                      Map TxIn (TxOut CtxUTxO Era) -> UTxO Era
forall era. Map TxIn (TxOut CtxUTxO era) -> UTxO era
CardanoAPI.UTxO (Map TxIn (TxOut CtxUTxO Era) -> UTxO Era)
-> Map TxIn (TxOut CtxUTxO Era) -> UTxO Era
forall a b. (a -> b) -> a -> b
$ Map TxIn (TxOut CtxUTxO Era)
outputs Map TxIn (TxOut CtxUTxO Era)
-> Map TxIn (TxOut CtxUTxO Era) -> Map TxIn (TxOut CtxUTxO Era)
forall a. Semigroup a => a -> a -> a
<> Map TxIn (TxOut CtxUTxO Era)
-> Set TxIn -> Map TxIn (TxOut CtxUTxO Era)
forall k a. Ord k => Map k a -> Set k -> Map k a
Map.withoutKeys Map TxIn (TxOut CtxUTxO Era)
utxos Set TxIn
consumed
                    where
                      consumed :: Set CardanoAPI.TxIn
                      consumed :: Set TxIn
consumed = [TxIn] -> Set TxIn
forall a. Ord a => [a] -> Set a
Set.fromList ([TxIn] -> Set TxIn) -> [TxIn] -> Set TxIn
forall a b. (a -> b) -> a -> b
$ (TxIn -> TxIn) -> [TxIn] -> [TxIn]
forall a b. (a -> b) -> [a] -> [b]
map TxIn -> TxIn
mkTxIn ([TxIn] -> [TxIn]) -> [TxIn] -> [TxIn]
forall a b. (a -> b) -> a -> b
$ OnChainTx -> [TxIn]
consumableInputs OnChainTx
tx

                      CardanoAPI.UTxO Map TxIn (TxOut CtxUTxO Era)
outputs = UtxoIndex -> UTxO Era
makeUTxOs (UtxoIndex -> UTxO Era) -> UtxoIndex -> UTxO Era
forall a b. (a -> b) -> a -> b
$ Map TxOutRef TxOut -> UtxoIndex
UtxoIndex (Map TxOutRef TxOut -> UtxoIndex)
-> Map TxOutRef TxOut -> UtxoIndex
forall a b. (a -> b) -> a -> b
$ OnChainTx -> Map TxOutRef TxOut
outputsProduced OnChainTx
tx

          mkTxIn :: TxIn -> CardanoAPI.TxIn
          mkTxIn :: TxIn -> TxIn
mkTxIn = TxOutRef -> TxIn
mkRef (TxOutRef -> TxIn) -> (TxIn -> TxOutRef) -> TxIn -> TxIn
forall b c a. (b -> c) -> (a -> b) -> a -> c
. TxIn -> TxOutRef
txInRef

          makeUTxOs :: UtxoIndex -> CardanoAPI.UTxO CM.Era
          makeUTxOs :: UtxoIndex -> UTxO Era
makeUTxOs (UtxoIndex Map TxOutRef TxOut
i) = Map TxIn (TxOut CtxUTxO Era) -> UTxO Era
forall era. Map TxIn (TxOut CtxUTxO era) -> UTxO era
CardanoAPI.UTxO (Map TxIn (TxOut CtxUTxO Era) -> UTxO Era)
-> Map TxIn (TxOut CtxUTxO Era) -> UTxO Era
forall a b. (a -> b) -> a -> b
$ [(TxIn, TxOut CtxUTxO Era)] -> Map TxIn (TxOut CtxUTxO Era)
forall k a. Ord k => [(k, a)] -> Map k a
Map.fromList [ (TxOutRef -> TxIn
mkRef TxOutRef
ref, TxOut -> TxOut CtxUTxO Era
mkTxOut TxOut
utxo)
                                                                   | (TxOutRef
ref, TxOut
utxo) <- Map TxOutRef TxOut -> [(TxOutRef, TxOut)]
forall k a. Map k a -> [(k, a)]
Map.toList Map TxOutRef TxOut
i ]

          mkRef :: TxOutRef -> CardanoAPI.TxIn
          mkRef :: TxOutRef -> TxIn
mkRef (TxOutRef (TxId BuiltinByteString
bs) Integer
ix) = TxId -> TxIx -> TxIn
CardanoAPI.TxIn
                                            (Hash StandardCrypto EraIndependentTxBody -> TxId
CardanoAPI.TxId (Hash StandardCrypto EraIndependentTxBody -> TxId)
-> Hash StandardCrypto EraIndependentTxBody -> TxId
forall a b. (a -> b) -> a -> b
$ BuiltinByteString -> Hash Blake2b_256 EraIndependentTxBody
forall crypto stuff.
HashAlgorithm crypto =>
BuiltinByteString -> Hash crypto stuff
makeTheHash BuiltinByteString
bs)
                                            (Word -> TxIx
CardanoAPI.TxIx (Word -> TxIx) -> Word -> TxIx
forall a b. (a -> b) -> a -> b
$ Integer -> Word
forall a b. (Integral a, Num b) => a -> b
fromIntegral Integer
ix)

          mkTxOut :: TxOut -> CardanoAPI.TxOut CardanoAPI.CtxUTxO Era
          mkTxOut :: TxOut -> TxOut CtxUTxO Era
mkTxOut (TxOut TxOut CtxTx Era
o) = TxOut CtxTx Era -> TxOut CtxUTxO Era
forall era. TxOut CtxTx era -> TxOut CtxUTxO era
CardanoAPI.toCtxUTxOTxOut TxOut CtxTx Era
o

makeTheHash :: Crypto.HashAlgorithm crypto => Builtins.BuiltinByteString -> Crypto.Hash crypto stuff
makeTheHash :: BuiltinByteString -> Hash crypto stuff
makeTheHash BuiltinByteString
bs =
  case ByteString -> Maybe (Hash crypto stuff)
forall h a. HashAlgorithm h => ByteString -> Maybe (Hash h a)
Crypto.hashFromBytes (ByteString -> Maybe (Hash crypto stuff))
-> ByteString -> Maybe (Hash crypto stuff)
forall a b. (a -> b) -> a -> b
$ BuiltinByteString -> ByteString
forall arep a. FromBuiltin arep a => arep -> a
Builtins.fromBuiltin BuiltinByteString
bs of
    Maybe (Hash crypto stuff)
Nothing   -> [Char] -> Hash crypto stuff
forall a. HasCallStack => [Char] -> a
error [Char]
"Bad hash!"
    Just Hash crypto stuff
hash -> Hash crypto stuff
hash

-- | `delay n` delays emulator execution by `n` slots
delay :: Integer -> RunMonad (SpecificationEmulatorTrace state) ()
delay :: Integer -> RunMonad (SpecificationEmulatorTrace state) ()
delay = Eff (Reader (Handles state) : BaseEmulatorEffects) ()
-> RunMonad (SpecificationEmulatorTrace state) ()
forall (t :: (* -> *) -> * -> *) (m :: * -> *) a.
(MonadTrans t, Monad m) =>
m a -> t m a
lift (Eff (Reader (Handles state) : BaseEmulatorEffects) ()
 -> RunMonad (SpecificationEmulatorTrace state) ())
-> (Integer
    -> Eff (Reader (Handles state) : BaseEmulatorEffects) ())
-> Integer
-> RunMonad (SpecificationEmulatorTrace state) ()
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Eff (Reader (Handles state) : BaseEmulatorEffects) Slot
-> Eff (Reader (Handles state) : BaseEmulatorEffects) ()
forall (f :: * -> *) a. Functor f => f a -> f ()
void (Eff (Reader (Handles state) : BaseEmulatorEffects) Slot
 -> Eff (Reader (Handles state) : BaseEmulatorEffects) ())
-> (Integer
    -> Eff (Reader (Handles state) : BaseEmulatorEffects) Slot)
-> Integer
-> Eff (Reader (Handles state) : BaseEmulatorEffects) ()
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Natural -> Eff (Reader (Handles state) : BaseEmulatorEffects) Slot
forall (effs :: [* -> *]).
Member Waiting effs =>
Natural -> Eff effs Slot
Trace.waitNSlots (Natural
 -> Eff (Reader (Handles state) : BaseEmulatorEffects) Slot)
-> (Integer -> Natural)
-> Integer
-> Eff (Reader (Handles state) : BaseEmulatorEffects) Slot
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Integer -> Natural
forall a. Num a => Integer -> a
fromInteger

instance Member Waiting effs => IsRunnable (Eff effs) where
  awaitSlot :: SlotNo -> Eff effs ()
awaitSlot = Eff effs Slot -> Eff effs ()
forall (f :: * -> *) a. Functor f => f a -> f ()
void (Eff effs Slot -> Eff effs ())
-> (SlotNo -> Eff effs Slot) -> SlotNo -> Eff effs ()
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Slot -> Eff effs Slot
forall (effs :: [* -> *]).
Member Waiting effs =>
Slot -> Eff effs Slot
waitUntilSlot (Slot -> Eff effs Slot)
-> (SlotNo -> Slot) -> SlotNo -> Eff effs Slot
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Integer -> Slot
Slot (Integer -> Slot) -> (SlotNo -> Integer) -> SlotNo -> Slot
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Word64 -> Integer
forall a. Integral a => a -> Integer
toInteger (Word64 -> Integer) -> (SlotNo -> Word64) -> SlotNo -> Integer
forall b c a. (b -> c) -> (a -> b) -> a -> c
. SlotNo -> Word64
unSlotNo

type instance Realized (Eff effs) a = a

deriving instance Eq (Action s) => Eq (Action (WithInstances s))

instance Show (Action s) => Show (Action (WithInstances s)) where
  showsPrec :: Int -> Action (WithInstances s) -> [Char] -> [Char]
showsPrec Int
p (UnderlyingAction a) = Int -> Action s -> [Char] -> [Char]
forall a. Show a => Int -> a -> [Char] -> [Char]
showsPrec Int
p Action s
a
  showsPrec Int
p (Unilateral w)       = Bool -> ([Char] -> [Char]) -> [Char] -> [Char]
showParen (Int
p Int -> Int -> Bool
forall a. Ord a => a -> a -> Bool
> Int
10) (([Char] -> [Char]) -> [Char] -> [Char])
-> ([Char] -> [Char]) -> [Char] -> [Char]
forall a b. (a -> b) -> a -> b
$ [Char] -> [Char] -> [Char]
showString [Char]
"Unilateral " ([Char] -> [Char]) -> ([Char] -> [Char]) -> [Char] -> [Char]
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Int -> Wallet -> [Char] -> [Char]
forall a. Show a => Int -> a -> [Char] -> [Char]
showsPrec Int
11 Wallet
w

instance HasSymTokens (Action s) => HasSymTokens (Action (WithInstances s)) where
  getAllSymTokens :: Action (WithInstances s) -> Set SymToken
getAllSymTokens (UnderlyingAction a) = Action s -> Set SymToken
forall a. HasSymTokens a => a -> Set SymToken
getAllSymTokens Action s
a
  getAllSymTokens Unilateral{}         = Set SymToken
forall a. Monoid a => a
mempty

instance forall s. ContractModel s => ContractModel (WithInstances s) where
  data Action (WithInstances s) = UnderlyingAction (Action s)
                                | Unilateral Wallet
  initialState :: WithInstances s
initialState                        = s -> WithInstances s
forall s. s -> WithInstances s
WithInstances s
forall state. ContractModel state => state
initialState
  waitProbability :: ModelState (WithInstances s) -> Double
waitProbability                     = ModelState s -> Double
forall state. ContractModel state => ModelState state -> Double
waitProbability (ModelState s -> Double)
-> (ModelState (WithInstances s) -> ModelState s)
-> ModelState (WithInstances s)
-> Double
forall b c a. (b -> c) -> (a -> b) -> a -> c
. (WithInstances s -> s)
-> ModelState (WithInstances s) -> ModelState s
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap WithInstances s -> s
forall s. WithInstances s -> s
withoutInstances
  arbitraryWaitInterval :: ModelState (WithInstances s) -> Gen SlotNo
arbitraryWaitInterval               = ModelState s -> Gen SlotNo
forall state. ContractModel state => ModelState state -> Gen SlotNo
arbitraryWaitInterval (ModelState s -> Gen SlotNo)
-> (ModelState (WithInstances s) -> ModelState s)
-> ModelState (WithInstances s)
-> Gen SlotNo
forall b c a. (b -> c) -> (a -> b) -> a -> c
. (WithInstances s -> s)
-> ModelState (WithInstances s) -> ModelState s
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap WithInstances s -> s
forall s. WithInstances s -> s
withoutInstances
  actionName :: Action (WithInstances s) -> [Char]
actionName (UnderlyingAction a) = Action s -> [Char]
forall state. ContractModel state => Action state -> [Char]
actionName Action s
a
  actionName Unilateral{}         = [Char]
"Unilateral"
  arbitraryAction :: ModelState (WithInstances s) -> Gen (Action (WithInstances s))
arbitraryAction                     = (Action s -> Action (WithInstances s))
-> Gen (Action s) -> Gen (Action (WithInstances s))
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap Action s -> Action (WithInstances s)
forall s. Action s -> Action (WithInstances s)
UnderlyingAction (Gen (Action s) -> Gen (Action (WithInstances s)))
-> (ModelState (WithInstances s) -> Gen (Action s))
-> ModelState (WithInstances s)
-> Gen (Action (WithInstances s))
forall b c a. (b -> c) -> (a -> b) -> a -> c
. ModelState s -> Gen (Action s)
forall state.
ContractModel state =>
ModelState state -> Gen (Action state)
arbitraryAction (ModelState s -> Gen (Action s))
-> (ModelState (WithInstances s) -> ModelState s)
-> ModelState (WithInstances s)
-> Gen (Action s)
forall b c a. (b -> c) -> (a -> b) -> a -> c
. (WithInstances s -> s)
-> ModelState (WithInstances s) -> ModelState s
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap WithInstances s -> s
forall s. WithInstances s -> s
withoutInstances
  precondition :: ModelState (WithInstances s) -> Action (WithInstances s) -> Bool
precondition ModelState (WithInstances s)
s (UnderlyingAction a) = ModelState s -> Action s -> Bool
forall state.
ContractModel state =>
ModelState state -> Action state -> Bool
precondition (WithInstances s -> s
forall s. WithInstances s -> s
withoutInstances (WithInstances s -> s)
-> ModelState (WithInstances s) -> ModelState s
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> ModelState (WithInstances s)
s) Action s
a
  precondition ModelState (WithInstances s)
_ Unilateral{}         = Bool
True
  nextReactiveState :: SlotNo -> Spec (WithInstances s) ()
nextReactiveState SlotNo
slot              = Spec s () -> Spec (WithInstances s) ()
forall s s' a. Coercible s s' => Spec s a -> Spec s' a
coerceSpec (Spec s () -> Spec (WithInstances s) ())
-> Spec s () -> Spec (WithInstances s) ()
forall a b. (a -> b) -> a -> b
$ SlotNo -> Spec s ()
forall state. ContractModel state => SlotNo -> Spec state ()
nextReactiveState @s SlotNo
slot
  nextState :: Action (WithInstances s) -> Spec (WithInstances s) ()
nextState (UnderlyingAction a) = Spec s () -> Spec (WithInstances s) ()
forall s s' a. Coercible s s' => Spec s a -> Spec s' a
coerceSpec (Spec s () -> Spec (WithInstances s) ())
-> Spec s () -> Spec (WithInstances s) ()
forall a b. (a -> b) -> a -> b
$ Action s -> Spec s ()
forall state. ContractModel state => Action state -> Spec state ()
nextState Action s
a
  nextState Unilateral{}         = () -> Spec (WithInstances s) ()
forall (f :: * -> *) a. Applicative f => a -> f a
pure ()
  shrinkAction :: ModelState (WithInstances s)
-> Action (WithInstances s) -> [Action (WithInstances s)]
shrinkAction ModelState (WithInstances s)
s (UnderlyingAction a) = Action s -> Action (WithInstances s)
forall s. Action s -> Action (WithInstances s)
UnderlyingAction (Action s -> Action (WithInstances s))
-> [Action s] -> [Action (WithInstances s)]
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> ModelState s -> Action s -> [Action s]
forall state.
ContractModel state =>
ModelState state -> Action state -> [Action state]
shrinkAction (WithInstances s -> s
forall s. WithInstances s -> s
withoutInstances (WithInstances s -> s)
-> ModelState (WithInstances s) -> ModelState s
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> ModelState (WithInstances s)
s) Action s
a
  shrinkAction ModelState (WithInstances s)
_ Unilateral{}         = []
  restricted :: Action (WithInstances s) -> Bool
restricted (UnderlyingAction a) = Action s -> Bool
forall state. ContractModel state => Action state -> Bool
restricted Action s
a
  restricted Unilateral{}         = Bool
True

-- | Options for controlling coverage checking requirements
--
-- * `checkCoverage` tells you whether or not to run the coverage checks at all.
-- * `endpointCoverageEq instance endpointName` tells us what percentage of tests are required to include
-- a call to the endpoint `endpointName` in the contract at `instance`.
-- * `coverIndex` is the coverage index obtained from the `CompiledCodeIn` of the validator.
data CoverageOptions = CoverageOptions
  { CoverageOptions -> Bool
_checkCoverage       :: Bool
  , CoverageOptions -> ContractInstanceTag -> [Char] -> Double
_endpointCoverageReq :: ContractInstanceTag -> String -> Double
  , CoverageOptions -> CoverageIndex
_coverageIndex       :: CoverageIndex
  , CoverageOptions -> Maybe (IORef CoverageData)
_coverageIORef       :: Maybe (IORef CoverageData)
  }
makeLenses ''CoverageOptions

-- | Default coverage checking options are:
-- * not to check coverage
-- * set the requriements for every endpoint to 20% and
-- * not to cover any source locations in the validator scripts.
defaultCoverageOptions :: CoverageOptions
defaultCoverageOptions :: CoverageOptions
defaultCoverageOptions = CoverageOptions :: Bool
-> (ContractInstanceTag -> [Char] -> Double)
-> CoverageIndex
-> Maybe (IORef CoverageData)
-> CoverageOptions
CoverageOptions
  { _checkCoverage :: Bool
_checkCoverage = Bool
False
  , _endpointCoverageReq :: ContractInstanceTag -> [Char] -> Double
_endpointCoverageReq = \ ContractInstanceTag
_ [Char]
_ -> Double
0
  , _coverageIndex :: CoverageIndex
_coverageIndex = CoverageIndex
forall a. Monoid a => a
mempty
  , _coverageIORef :: Maybe (IORef CoverageData)
_coverageIORef = Maybe (IORef CoverageData)
forall a. Maybe a
Nothing }

-- | Default check options that include a large amount of Ada in the initial distributions to avoid having
-- to write `ContractModel`s that keep track of balances.
defaultCheckOptionsContractModel :: CheckOptions
defaultCheckOptionsContractModel :: CheckOptions
defaultCheckOptionsContractModel =
  let initialValue :: Value
initialValue = Integer -> Value
Ada.lovelaceValueOf Integer
100_000_000_000_000_000 in
  CheckOptions
defaultCheckOptions CheckOptions -> (CheckOptions -> CheckOptions) -> CheckOptions
forall a b. a -> (a -> b) -> b
& (EmulatorConfig -> Identity EmulatorConfig)
-> CheckOptions -> Identity CheckOptions
Lens' CheckOptions EmulatorConfig
emulatorConfig
                      ((EmulatorConfig -> Identity EmulatorConfig)
 -> CheckOptions -> Identity CheckOptions)
-> ((InitialChainState -> Identity InitialChainState)
    -> EmulatorConfig -> Identity EmulatorConfig)
-> (InitialChainState -> Identity InitialChainState)
-> CheckOptions
-> Identity CheckOptions
forall b c a. (b -> c) -> (a -> b) -> a -> c
. (InitialChainState -> Identity InitialChainState)
-> EmulatorConfig -> Identity EmulatorConfig
Lens' EmulatorConfig InitialChainState
initialChainState ((InitialChainState -> Identity InitialChainState)
 -> CheckOptions -> Identity CheckOptions)
-> InitialChainState -> CheckOptions -> CheckOptions
forall s t a b. ASetter s t a b -> b -> s -> t
.~ (Map Wallet Value -> InitialChainState
forall a b. a -> Either a b
Left (Map Wallet Value -> InitialChainState)
-> ([(Wallet, Value)] -> Map Wallet Value)
-> [(Wallet, Value)]
-> InitialChainState
forall b c a. (b -> c) -> (a -> b) -> a -> c
. [(Wallet, Value)] -> Map Wallet Value
forall k a. Ord k => [(k, a)] -> Map k a
Map.fromList ([(Wallet, Value)] -> InitialChainState)
-> [(Wallet, Value)] -> InitialChainState
forall a b. (a -> b) -> a -> b
$ [Wallet] -> [Value] -> [(Wallet, Value)]
forall a b. [a] -> [b] -> [(a, b)]
zip [Wallet]
knownWallets (Value -> [Value]
forall a. a -> [a]
repeat Value
initialValue))

-- | Run QuickCheck on a property that tracks coverage and print its coverage report.
quickCheckWithCoverage :: QC.Testable prop
                       => QC.Args
                       -> CoverageOptions
                       -> (CoverageOptions -> prop)
                       -> IO CoverageReport
quickCheckWithCoverage :: Args
-> CoverageOptions
-> (CoverageOptions -> prop)
-> IO CoverageReport
quickCheckWithCoverage Args
qcargs CoverageOptions
opts CoverageOptions -> prop
prop = (CoverageReport, Result) -> CoverageReport
forall a b. (a, b) -> a
fst ((CoverageReport, Result) -> CoverageReport)
-> IO (CoverageReport, Result) -> IO CoverageReport
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> Args
-> CoverageOptions
-> (CoverageOptions -> prop)
-> IO (CoverageReport, Result)
forall prop.
Testable prop =>
Args
-> CoverageOptions
-> (CoverageOptions -> prop)
-> IO (CoverageReport, Result)
quickCheckWithCoverageAndResult Args
qcargs CoverageOptions
opts CoverageOptions -> prop
prop

quickCheckWithCoverageAndResult :: QC.Testable prop
                                => QC.Args
                                -> CoverageOptions
                                -> (CoverageOptions -> prop)
                                -> IO (CoverageReport, Result)
quickCheckWithCoverageAndResult :: Args
-> CoverageOptions
-> (CoverageOptions -> prop)
-> IO (CoverageReport, Result)
quickCheckWithCoverageAndResult Args
qcargs CoverageOptions
copts CoverageOptions -> prop
prop = do
  CoverageOptions
copts <- case CoverageOptions
copts CoverageOptions
-> Getting
     (Maybe (IORef CoverageData))
     CoverageOptions
     (Maybe (IORef CoverageData))
-> Maybe (IORef CoverageData)
forall s a. s -> Getting a s a -> a
^. Getting
  (Maybe (IORef CoverageData))
  CoverageOptions
  (Maybe (IORef CoverageData))
Lens' CoverageOptions (Maybe (IORef CoverageData))
coverageIORef of
    Maybe (IORef CoverageData)
Nothing -> do
      IORef CoverageData
ref <- CoverageData -> IO (IORef CoverageData)
forall a. a -> IO (IORef a)
newIORef CoverageData
forall a. Monoid a => a
mempty
      CoverageOptions -> IO CoverageOptions
forall (m :: * -> *) a. Monad m => a -> m a
return (CoverageOptions -> IO CoverageOptions)
-> CoverageOptions -> IO CoverageOptions
forall a b. (a -> b) -> a -> b
$ CoverageOptions
copts { _coverageIORef :: Maybe (IORef CoverageData)
_coverageIORef = IORef CoverageData -> Maybe (IORef CoverageData)
forall a. a -> Maybe a
Just IORef CoverageData
ref }
    Maybe (IORef CoverageData)
_ -> CoverageOptions -> IO CoverageOptions
forall (m :: * -> *) a. Monad m => a -> m a
return CoverageOptions
copts
  Result
res <- Args -> prop -> IO Result
forall prop. Testable prop => Args -> prop -> IO Result
QC.quickCheckWithResult Args
qcargs (prop -> IO Result) -> prop -> IO Result
forall a b. (a -> b) -> a -> b
$ CoverageOptions -> prop
prop (CoverageOptions -> prop) -> CoverageOptions -> prop
forall a b. (a -> b) -> a -> b
$ CoverageOptions
copts { _checkCoverage :: Bool
_checkCoverage = Bool
True }
  case CoverageOptions
copts CoverageOptions
-> Getting
     (Maybe (IORef CoverageData))
     CoverageOptions
     (Maybe (IORef CoverageData))
-> Maybe (IORef CoverageData)
forall s a. s -> Getting a s a -> a
^. Getting
  (Maybe (IORef CoverageData))
  CoverageOptions
  (Maybe (IORef CoverageData))
Lens' CoverageOptions (Maybe (IORef CoverageData))
coverageIORef of
    Maybe (IORef CoverageData)
Nothing -> [Char] -> IO (CoverageReport, Result)
forall (m :: * -> *) a. MonadFail m => [Char] -> m a
fail [Char]
"Unreachable case in quickCheckWithCoverage"
    Just IORef CoverageData
ref -> do
      CoverageData
covdata <- IORef CoverageData -> IO CoverageData
forall a. IORef a -> IO a
readIORef IORef CoverageData
ref
      let report :: CoverageReport
report = CoverageIndex -> CoverageData -> CoverageReport
CoverageReport (CoverageOptions
copts CoverageOptions
-> Getting CoverageIndex CoverageOptions CoverageIndex
-> CoverageIndex
forall s a. s -> Getting a s a -> a
^. Getting CoverageIndex CoverageOptions CoverageIndex
Lens' CoverageOptions CoverageIndex
coverageIndex) CoverageData
covdata
      Bool -> IO () -> IO ()
forall (f :: * -> *). Applicative f => Bool -> f () -> f ()
when (Args -> Bool
chatty Args
qcargs) (IO () -> IO ()) -> IO () -> IO ()
forall a b. (a -> b) -> a -> b
$ [Char] -> IO ()
putStrLn ([Char] -> IO ()) -> (Doc Any -> [Char]) -> Doc Any -> IO ()
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Doc Any -> [Char]
forall a. Show a => a -> [Char]
show (Doc Any -> IO ()) -> Doc Any -> IO ()
forall a b. (a -> b) -> a -> b
$ CoverageReport -> Doc Any
forall a ann. Pretty a => a -> Doc ann
pretty CoverageReport
report
      (CoverageReport, Result) -> IO (CoverageReport, Result)
forall (m :: * -> *) a. Monad m => a -> m a
return (CoverageReport
report, Result
res)

-- | Run a `Actions` in the emulator and check that the model and the emulator agree on the final
--   wallet balance changes. Equivalent to
--
-- @
-- propRunActions_ hs actions = `propRunActions` hs (`const` `$` `pure` `True`) actions
-- @
propRunActions_ ::
    CheckableContractModel state
    => Actions (WithInstances state)                 -- ^ The actions to run
    -> Property
propRunActions_ :: Actions (WithInstances state) -> Property
propRunActions_ Actions (WithInstances state)
actions =
    (ModelState (WithInstances state) -> TracePredicate)
-> Actions (WithInstances state) -> Property
forall state.
CheckableContractModel state =>
(ModelState (WithInstances state) -> TracePredicate)
-> Actions (WithInstances state) -> Property
propRunActions (\ ModelState (WithInstances state)
_ -> Bool -> TracePredicate
forall (f :: * -> *) a. Applicative f => a -> f a
pure Bool
True) Actions (WithInstances state)
actions

-- | Run a `Actions` in the emulator and check that the model and the emulator agree on the final
--   wallet balance changes, and that the given `TracePredicate` holds at the end. Equivalent to:
--
-- @
-- propRunActions = `propRunActionsWithOptions` `defaultCheckOptionsContractModel` `defaultCoverageOptions`
-- @
propRunActions ::
    CheckableContractModel state
    => (ModelState (WithInstances state) -> TracePredicate) -- ^ Predicate to check at the end
    -> Actions (WithInstances state)                        -- ^ The actions to run
    -> Property
propRunActions :: (ModelState (WithInstances state) -> TracePredicate)
-> Actions (WithInstances state) -> Property
propRunActions = CheckOptions
-> CoverageOptions
-> (ModelState (WithInstances state) -> TracePredicate)
-> Actions (WithInstances state)
-> Property
forall state.
CheckableContractModel state =>
CheckOptions
-> CoverageOptions
-> (ModelState (WithInstances state) -> TracePredicate)
-> Actions (WithInstances state)
-> Property
propRunActionsWithOptions CheckOptions
defaultCheckOptionsContractModel CoverageOptions
defaultCoverageOptions

propRunActionsWithOptions :: forall state.
    CheckableContractModel state
    => CheckOptions                                         -- ^ Emulator options
    -> CoverageOptions                                      -- ^ Coverage options
    -> (ModelState (WithInstances state) -> TracePredicate) -- ^ Predicate to check at the end of execution
    -> Actions (WithInstances state)                        -- ^ The actions to run
    -> Property
propRunActionsWithOptions :: CheckOptions
-> CoverageOptions
-> (ModelState (WithInstances state) -> TracePredicate)
-> Actions (WithInstances state)
-> Property
propRunActionsWithOptions CheckOptions
opts CoverageOptions
copts ModelState (WithInstances state) -> TracePredicate
predicate Actions (WithInstances state)
actions =
    ModelState (WithInstances state) -> Property
forall state. ModelState state -> Property
asserts ModelState (WithInstances state)
finalState Property -> Property -> Property
forall prop1 prop2.
(Testable prop1, Testable prop2) =>
prop1 -> prop2 -> Property
QC..&&.
    (RunMonad (EmulatorTraceWithInstances state) Property -> Property)
-> PropertyM (RunMonad (EmulatorTraceWithInstances state)) Property
-> Property
forall a (m :: * -> *).
(Testable a, Monad m) =>
(m Property -> Property) -> PropertyM m a -> Property
monadic RunMonad (EmulatorTraceWithInstances state) Property -> Property
runFinalPredicate PropertyM (RunMonad (EmulatorTraceWithInstances state)) Property
monadicPredicate
    where
        finalState :: ModelState (WithInstances state)
finalState = Actions (WithInstances state) -> ModelState (WithInstances state)
forall state.
ContractModel state =>
Actions state -> ModelState state
stateAfter Actions (WithInstances state)
actions

        prettyAddr :: AddressInEra Era -> [Char]
prettyAddr AddressInEra Era
a = [Char] -> (Wallet -> [Char]) -> Maybe Wallet -> [Char]
forall b a. b -> (a -> b) -> Maybe a -> b
maybe (AddressInEra Era -> [Char]
forall a. Show a => a -> [Char]
show AddressInEra Era
a) Wallet -> [Char]
forall a. Show a => a -> [Char]
show (Maybe Wallet -> [Char]) -> Maybe Wallet -> [Char]
forall a b. (a -> b) -> a -> b
$ AddressInEra Era -> Maybe Wallet
addressToWallet AddressInEra Era
a

        monadicPredicate :: PropertyM (RunMonad (EmulatorTraceWithInstances state)) Property
        monadicPredicate :: PropertyM (RunMonad (EmulatorTraceWithInstances state)) Property
monadicPredicate = do
            ProtocolParameters
ps <- RunMonad (EmulatorTraceWithInstances state) ProtocolParameters
-> PropertyM
     (RunMonad (EmulatorTraceWithInstances state)) ProtocolParameters
forall (m :: * -> *) a. Monad m => m a -> PropertyM m a
QC.run (RunMonad (EmulatorTraceWithInstances state) ProtocolParameters
 -> PropertyM
      (RunMonad (EmulatorTraceWithInstances state)) ProtocolParameters)
-> (Eff
      (State (Handles state) : EmulatorEffects) ProtocolParameters
    -> RunMonad (EmulatorTraceWithInstances state) ProtocolParameters)
-> Eff (State (Handles state) : EmulatorEffects) ProtocolParameters
-> PropertyM
     (RunMonad (EmulatorTraceWithInstances state)) ProtocolParameters
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Eff (State (Handles state) : EmulatorEffects) ProtocolParameters
-> RunMonad (EmulatorTraceWithInstances state) ProtocolParameters
forall (t :: (* -> *) -> * -> *) (m :: * -> *) a.
(MonadTrans t, Monad m) =>
m a -> t m a
lift (Eff (State (Handles state) : EmulatorEffects) ProtocolParameters
 -> PropertyM
      (RunMonad (EmulatorTraceWithInstances state)) ProtocolParameters)
-> Eff (State (Handles state) : EmulatorEffects) ProtocolParameters
-> PropertyM
     (RunMonad (EmulatorTraceWithInstances state)) ProtocolParameters
forall a b. (a -> b) -> a -> b
$ (Params -> ProtocolParameters)
-> Eff (State (Handles state) : EmulatorEffects) Params
-> Eff (State (Handles state) : EmulatorEffects) ProtocolParameters
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap Params -> ProtocolParameters
pProtocolParams Eff (State (Handles state) : EmulatorEffects) Params
forall (effs :: [* -> *]).
Member EmulatorControl effs =>
Eff effs Params
EmulatorControl.getParams
            RunMonad (EmulatorTraceWithInstances state) ()
-> PropertyM (RunMonad (EmulatorTraceWithInstances state)) ()
forall (m :: * -> *) a. Monad m => m a -> PropertyM m a
QC.run (RunMonad (EmulatorTraceWithInstances state) ()
 -> PropertyM (RunMonad (EmulatorTraceWithInstances state)) ())
-> (Eff (State (Handles state) : EmulatorEffects) ()
    -> RunMonad (EmulatorTraceWithInstances state) ())
-> Eff (State (Handles state) : EmulatorEffects) ()
-> PropertyM (RunMonad (EmulatorTraceWithInstances state)) ()
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Eff (State (Handles state) : EmulatorEffects) ()
-> RunMonad (EmulatorTraceWithInstances state) ()
forall (t :: (* -> *) -> * -> *) (m :: * -> *) a.
(MonadTrans t, Monad m) =>
m a -> t m a
lift (Eff (State (Handles state) : EmulatorEffects) ()
 -> PropertyM (RunMonad (EmulatorTraceWithInstances state)) ())
-> Eff (State (Handles state) : EmulatorEffects) ()
-> PropertyM (RunMonad (EmulatorTraceWithInstances state)) ()
forall a b. (a -> b) -> a -> b
$ (SymToken -> AssetId)
-> [StartContract state]
-> Eff (State (Handles state) : EmulatorEffects) ()
forall state.
ContractInstanceModel state =>
(SymToken -> AssetId)
-> [StartContract state] -> EmulatorTraceWithInstances state ()
activateWallets (\ SymToken
_ -> [Char] -> AssetId
forall a. HasCallStack => [Char] -> a
error [Char]
"No SymTokens yet") [StartContract state]
forall state. ContractInstanceModel state => [StartContract state]
initialInstances
            ContractModelResult (WithInstances state)
result <- Actions (WithInstances state)
-> PropertyM
     (RunMonad (EmulatorTraceWithInstances state))
     (ContractModelResult (WithInstances state))
forall state (m :: * -> *).
(ContractModel state, RunModel state m, HasChainIndex m) =>
Actions state -> PropertyM (RunMonad m) (ContractModelResult state)
runContractModel Actions (WithInstances state)
actions
            Property
-> PropertyM (RunMonad (EmulatorTraceWithInstances state)) Property
forall (f :: * -> *) a. Applicative f => a -> f a
pure (Property
 -> PropertyM
      (RunMonad (EmulatorTraceWithInstances state)) Property)
-> Property
-> PropertyM (RunMonad (EmulatorTraceWithInstances state)) Property
forall a b. (a -> b) -> a -> b
$ BalanceChangeOptions
-> ContractModelResult (WithInstances state) -> Property
forall state.
BalanceChangeOptions -> ContractModelResult state -> Property
assertBalanceChangesMatch (Bool
-> FeeCalculation
-> ProtocolParameters
-> (AddressInEra Era -> [Char])
-> BalanceChangeOptions
BalanceChangeOptions Bool
False FeeCalculation
signerPaysFees ProtocolParameters
ps AddressInEra Era -> [Char]
prettyAddr) ContractModelResult (WithInstances state)
result

        runFinalPredicate :: RunMonad (EmulatorTraceWithInstances state) Property
                          -> Property
        runFinalPredicate :: RunMonad (EmulatorTraceWithInstances state) Property -> Property
runFinalPredicate RunMonad (EmulatorTraceWithInstances state) Property
emulatorTrace =
          let traceWithResult :: EmulatorTrace Property
              traceWithResult :: EmulatorTrace Property
traceWithResult = ((Property, Handles state) -> Property)
-> Eff EmulatorEffects (Property, Handles state)
-> EmulatorTrace Property
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap (Property, Handles state) -> Property
forall a b. (a, b) -> a
fst
                              (Eff EmulatorEffects (Property, Handles state)
 -> EmulatorTrace Property)
-> (RunMonad (EmulatorTraceWithInstances state) Property
    -> Eff EmulatorEffects (Property, Handles state))
-> RunMonad (EmulatorTraceWithInstances state) Property
-> EmulatorTrace Property
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Handles state
-> Eff (State (Handles state) : EmulatorEffects) Property
-> Eff EmulatorEffects (Property, Handles state)
forall s (effs :: [* -> *]) a.
s -> Eff (State s : effs) a -> Eff effs (a, s)
runState Handles state
forall i j k l (key :: i -> j -> k -> l -> *)
       (val :: i -> j -> k -> *).
IMap key val
IMNil
                              (Eff (State (Handles state) : EmulatorEffects) Property
 -> Eff EmulatorEffects (Property, Handles state))
-> (RunMonad (EmulatorTraceWithInstances state) Property
    -> Eff (State (Handles state) : EmulatorEffects) Property)
-> RunMonad (EmulatorTraceWithInstances state) Property
-> Eff EmulatorEffects (Property, Handles state)
forall b c a. (b -> c) -> (a -> b) -> a -> c
. ((Property, [([Char], AssetId)]) -> Property)
-> Eff
     (State (Handles state) : EmulatorEffects)
     (Property, [([Char], AssetId)])
-> Eff (State (Handles state) : EmulatorEffects) Property
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap (Property, [([Char], AssetId)]) -> Property
forall a b. (a, b) -> a
fst
                              (Eff
   (State (Handles state) : EmulatorEffects)
   (Property, [([Char], AssetId)])
 -> Eff (State (Handles state) : EmulatorEffects) Property)
-> (RunMonad (EmulatorTraceWithInstances state) Property
    -> Eff
         (State (Handles state) : EmulatorEffects)
         (Property, [([Char], AssetId)]))
-> RunMonad (EmulatorTraceWithInstances state) Property
-> Eff (State (Handles state) : EmulatorEffects) Property
forall b c a. (b -> c) -> (a -> b) -> a -> c
. WriterT
  [([Char], AssetId)] (EmulatorTraceWithInstances state) Property
-> Eff
     (State (Handles state) : EmulatorEffects)
     (Property, [([Char], AssetId)])
forall w (m :: * -> *) a. WriterT w m a -> m (a, w)
runWriterT
                              (WriterT
   [([Char], AssetId)] (EmulatorTraceWithInstances state) Property
 -> Eff
      (State (Handles state) : EmulatorEffects)
      (Property, [([Char], AssetId)]))
-> (RunMonad (EmulatorTraceWithInstances state) Property
    -> WriterT
         [([Char], AssetId)] (EmulatorTraceWithInstances state) Property)
-> RunMonad (EmulatorTraceWithInstances state) Property
-> Eff
     (State (Handles state) : EmulatorEffects)
     (Property, [([Char], AssetId)])
forall b c a. (b -> c) -> (a -> b) -> a -> c
. RunMonad (EmulatorTraceWithInstances state) Property
-> WriterT
     [([Char], AssetId)] (EmulatorTraceWithInstances state) Property
forall (m :: * -> *) a.
RunMonad m a -> WriterT [([Char], AssetId)] m a
unRunMonad
                              (RunMonad (EmulatorTraceWithInstances state) Property
 -> EmulatorTrace Property)
-> RunMonad (EmulatorTraceWithInstances state) Property
-> EmulatorTrace Property
forall a b. (a -> b) -> a -> b
$ RunMonad (EmulatorTraceWithInstances state) Property
emulatorTrace
          in PropertyM IO Property -> Property
forall a. Testable a => PropertyM IO a -> Property
QC.monadicIO (PropertyM IO Property -> Property)
-> PropertyM IO Property -> Property
forall a b. (a -> b) -> a -> b
$ CheckOptions
-> TracePredicate
-> EmulatorTrace Property
-> ([Char] -> PropertyM IO ())
-> (Bool -> PropertyM IO ())
-> (CoverageData -> PropertyM IO ())
-> PropertyM IO (Either EmulatorErr Property)
forall (m :: * -> *) a.
Monad m =>
CheckOptions
-> TracePredicate
-> EmulatorTrace a
-> ([Char] -> m ())
-> (Bool -> m ())
-> (CoverageData -> m ())
-> m (Either EmulatorErr a)
checkPredicateInner CheckOptions
opts (TracePredicate
noMainThreadCrashes TracePredicate -> TracePredicate -> TracePredicate
.&&. ModelState (WithInstances state) -> TracePredicate
predicate ModelState (WithInstances state)
finalState)
                                                EmulatorTrace Property
traceWithResult [Char] -> PropertyM IO ()
forall (m :: * -> *). Monad m => [Char] -> PropertyM m ()
debugOutput
                                                Bool -> PropertyM IO ()
forall (m :: * -> *). Monad m => Bool -> PropertyM m ()
assertResult CoverageData -> PropertyM IO ()
cover
                            PropertyM IO (Either EmulatorErr Property)
-> (Either EmulatorErr Property -> PropertyM IO Property)
-> PropertyM IO Property
forall (m :: * -> *) a b. Monad m => m a -> (a -> m b) -> m b
>>= \Either EmulatorErr Property
res -> case Either EmulatorErr Property
res of
                                  Left EmulatorErr
err   -> Property -> PropertyM IO Property
forall (m :: * -> *) a. Monad m => a -> m a
return (Property -> PropertyM IO Property)
-> Property -> PropertyM IO Property
forall a b. (a -> b) -> a -> b
$ [Char] -> Property -> Property
forall prop. Testable prop => [Char] -> prop -> Property
counterexample ([Char]
"checkPredicateInner terminated with error: " [Char] -> [Char] -> [Char]
forall a. [a] -> [a] -> [a]
++ EmulatorErr -> [Char]
forall a. Show a => a -> [Char]
show EmulatorErr
err)
                                                       (Property -> Property) -> Property -> Property
forall a b. (a -> b) -> a -> b
$ Bool -> Property
forall prop. Testable prop => prop -> Property
property Bool
False
                                  Right Property
prop -> Property -> PropertyM IO Property
forall (m :: * -> *) a. Monad m => a -> m a
return Property
prop

        cover :: CoverageData -> PropertyM IO ()
cover CoverageData
report | CoverageOptions
copts CoverageOptions -> Getting Bool CoverageOptions Bool -> Bool
forall s a. s -> Getting a s a -> a
^. Getting Bool CoverageOptions Bool
Lens' CoverageOptions Bool
checkCoverage
                     , Just IORef CoverageData
ref <- CoverageOptions
copts CoverageOptions
-> Getting
     (Maybe (IORef CoverageData))
     CoverageOptions
     (Maybe (IORef CoverageData))
-> Maybe (IORef CoverageData)
forall s a. s -> Getting a s a -> a
^. Getting
  (Maybe (IORef CoverageData))
  CoverageOptions
  (Maybe (IORef CoverageData))
Lens' CoverageOptions (Maybe (IORef CoverageData))
coverageIORef =
                       CoverageData
report CoverageData -> PropertyM IO () -> PropertyM IO ()
forall a b. NFData a => a -> b -> b
`deepseq`
                        ((Property -> Property) -> PropertyM IO ()
forall (m :: * -> *).
Monad m =>
(Property -> Property) -> PropertyM m ()
QC.monitor ((Property -> Property) -> PropertyM IO ())
-> (Property -> Property) -> PropertyM IO ()
forall a b. (a -> b) -> a -> b
$ \ Property
p -> 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 CoverageData -> (CoverageData -> CoverageData) -> IO ()
forall a. IORef a -> (a -> a) -> IO ()
modifyIORef IORef CoverageData
ref (CoverageData
reportCoverageData -> CoverageData -> CoverageData
forall a. Semigroup a => a -> a -> a
<>)
                           Property -> IO Property
forall (m :: * -> *) a. Monad m => a -> m a
return Property
p)
                     | Bool
otherwise = () -> PropertyM IO ()
forall (f :: * -> *) a. Applicative f => a -> f a
pure ()

        debugOutput :: Monad m => String -> PropertyM m ()
        debugOutput :: [Char] -> PropertyM m ()
debugOutput = (Property -> Property) -> PropertyM m ()
forall (m :: * -> *).
Monad m =>
(Property -> Property) -> PropertyM m ()
QC.monitor ((Property -> Property) -> PropertyM m ())
-> ([Char] -> Property -> Property) -> [Char] -> PropertyM m ()
forall b c a. (b -> c) -> (a -> b) -> a -> c
. [Char] -> Property -> Property
forall prop. Testable prop => [Char] -> prop -> Property
counterexample

        assertResult :: Monad m => Bool -> PropertyM m ()
        assertResult :: Bool -> PropertyM m ()
assertResult = Bool -> PropertyM m ()
forall (m :: * -> *). Monad m => Bool -> PropertyM m ()
QC.assert

        -- don't accept traces where the main thread crashes
        noMainThreadCrashes :: TracePredicate
        noMainThreadCrashes :: TracePredicate
noMainThreadCrashes = ([EmulatorTimeEvent UserThreadMsg] -> Bool) -> TracePredicate
assertUserLog (([EmulatorTimeEvent UserThreadMsg] -> Bool) -> TracePredicate)
-> ([EmulatorTimeEvent UserThreadMsg] -> Bool) -> TracePredicate
forall a b. (a -> b) -> a -> b
$ \ [EmulatorTimeEvent UserThreadMsg]
log -> [()] -> Bool
forall (t :: * -> *) a. Foldable t => t a -> Bool
null [ () | UserThreadErr EmulatorRuntimeError
_ <- Getting
  UserThreadMsg (EmulatorTimeEvent UserThreadMsg) UserThreadMsg
-> EmulatorTimeEvent UserThreadMsg -> UserThreadMsg
forall s (m :: * -> *) a. MonadReader s m => Getting a s a -> m a
view Getting
  UserThreadMsg (EmulatorTimeEvent UserThreadMsg) UserThreadMsg
forall e1 e2.
Lens (EmulatorTimeEvent e1) (EmulatorTimeEvent e2) e1 e2
eteEvent (EmulatorTimeEvent UserThreadMsg -> UserThreadMsg)
-> [EmulatorTimeEvent UserThreadMsg] -> [UserThreadMsg]
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> [EmulatorTimeEvent UserThreadMsg]
log ]

-- $noLockedFunds
-- Showing that funds can not be locked in the contract forever.

-- | A "proof" that you can always recover the funds locked by a contract. The first component is
--   a strategy that from any state of the contract can get all the funds out. The second component
--   is a strategy for each wallet that from the same state, shows how that wallet can recover the
--   same (or bigger) amount as using the first strategy, without relying on any actions being taken
--   by the other wallets.
--
--   For instance, in a two player game where each player bets some amount of funds and the winner
--   gets the pot, there needs to be a mechanism for the players to recover their bid if the other
--   player simply walks away (perhaps after realising the game is lost). If not, it won't be
--   possible to construct a `NoLockedFundsProof` that works in a state where both players need to
--   move before any funds can be collected.
data NoLockedFundsProof model = NoLockedFundsProof
  { NoLockedFundsProof model -> DL (WithInstances model) ()
nlfpMainStrategy   :: DL (WithInstances model) ()   -- TODO: wrapper for DL
    -- ^ Strategy to recover all funds from the contract in any reachable state.
  , NoLockedFundsProof model -> Wallet -> DL (WithInstances model) ()
nlfpWalletStrategy :: Wallet -> DL (WithInstances model) ()
    -- ^ A strategy for each wallet to recover as much (or more) funds as the main strategy would
    --   give them in a given state, without the assistance of any other wallet.
  , NoLockedFundsProof model
-> ModelState (WithInstances model) -> SymValue
nlfpOverhead       :: ModelState (WithInstances model) -> SymValue
    -- ^ An initial amount of overhead value that may be lost - e.g. setup fees for scripts that
    -- can't be recovered.
  , NoLockedFundsProof model
-> ModelState (WithInstances model) -> SymValue
nlfpErrorMargin    :: ModelState (WithInstances model) -> SymValue
    -- ^ The total amount of margin for error in the value collected by the WalletStrategy compared
    -- to the MainStrategy. This is useful if your contract contains rounding code that makes the order
    -- of operations have a small but predictable effect on the value collected by different wallets.
  }
data NoLockedFundsProofLight model = NoLockedFundsProofLight
  { NoLockedFundsProofLight model -> DL (WithInstances model) ()
nlfplMainStrategy :: DL (WithInstances model) () }

-- | The default skeleton of a NoLockedFundsProof - doesn't permit any overhead or error margin.
defaultNLFP :: NoLockedFundsProof model
defaultNLFP :: NoLockedFundsProof model
defaultNLFP = NoLockedFundsProof :: forall model.
DL (WithInstances model) ()
-> (Wallet -> DL (WithInstances model) ())
-> (ModelState (WithInstances model) -> SymValue)
-> (ModelState (WithInstances model) -> SymValue)
-> NoLockedFundsProof model
NoLockedFundsProof { nlfpMainStrategy :: DL (WithInstances model) ()
nlfpMainStrategy = () -> DL (WithInstances model) ()
forall (m :: * -> *) a. Monad m => a -> m a
return ()
                                 , nlfpWalletStrategy :: Wallet -> DL (WithInstances model) ()
nlfpWalletStrategy = DL (WithInstances model) ()
-> Wallet -> DL (WithInstances model) ()
forall a b. a -> b -> a
const (() -> DL (WithInstances model) ()
forall (m :: * -> *) a. Monad m => a -> m a
return ())
                                 , nlfpOverhead :: ModelState (WithInstances model) -> SymValue
nlfpOverhead = SymValue -> ModelState (WithInstances model) -> SymValue
forall a b. a -> b -> a
const SymValue
forall a. Monoid a => a
mempty
                                 , nlfpErrorMargin :: ModelState (WithInstances model) -> SymValue
nlfpErrorMargin = SymValue -> ModelState (WithInstances model) -> SymValue
forall a b. a -> b -> a
const SymValue
forall a. Monoid a => a
mempty }

-- | Check a `NoLockedFundsProof`. Each test will generate an arbitrary sequence of actions
--   (`anyActions_`) and ask the `nlfpMainStrategy` to recover all funds locked by the contract
--   after performing those actions. This results in some distribution of the contract funds to the
--   wallets, and the test then asks each `nlfpWalletStrategy` to show how to recover their
--   allotment of funds without any assistance from the other wallets (assuming the main strategy
--   did not execute). When executing wallet strategies, the off-chain instances for other wallets
--   are killed and their private keys are deleted from the emulator state.

checkNoLockedFundsProof
  :: CheckableContractModel model
  => NoLockedFundsProof model
  -> Property
checkNoLockedFundsProof :: NoLockedFundsProof model -> Property
checkNoLockedFundsProof = CheckOptions -> NoLockedFundsProof model -> Property
forall model.
CheckableContractModel model =>
CheckOptions -> NoLockedFundsProof model -> Property
checkNoLockedFundsProofWithOptions CheckOptions
defaultCheckOptionsContractModel

checkNoLockedFundsProofFast
  :: CheckableContractModel model
  => NoLockedFundsProof model
  -> Property
checkNoLockedFundsProofFast :: NoLockedFundsProof model -> Property
checkNoLockedFundsProofFast = CheckOptions -> NoLockedFundsProof model -> Property
forall model.
CheckableContractModel model =>
CheckOptions -> NoLockedFundsProof model -> Property
checkNoLockedFundsProofFastWithOptions CheckOptions
defaultCheckOptionsContractModel

checkNoLockedFundsProofWithOptions
  :: CheckableContractModel model
  => CheckOptions
  -> NoLockedFundsProof model
  -> Property
checkNoLockedFundsProofWithOptions :: CheckOptions -> NoLockedFundsProof model -> Property
checkNoLockedFundsProofWithOptions CheckOptions
options =
  (Actions (WithInstances model) -> Property)
-> NoLockedFundsProof model -> Property
forall model.
CheckableContractModel model =>
(Actions (WithInstances model) -> Property)
-> NoLockedFundsProof model -> Property
checkNoLockedFundsProof' Actions (WithInstances model) -> Property
prop
  where
    prop :: Actions (WithInstances model) -> Property
prop = CheckOptions
-> CoverageOptions
-> (ModelState (WithInstances model) -> TracePredicate)
-> Actions (WithInstances model)
-> Property
forall state.
CheckableContractModel state =>
CheckOptions
-> CoverageOptions
-> (ModelState (WithInstances state) -> TracePredicate)
-> Actions (WithInstances state)
-> Property
propRunActionsWithOptions CheckOptions
options CoverageOptions
defaultCoverageOptions (\ ModelState (WithInstances model)
_ -> (forall (effs :: [* -> *]).
 Members TestEffects effs =>
 FoldM (Eff effs) EmulatorEvent Bool)
-> TracePredicate
forall a.
(forall (effs :: [* -> *]).
 Members TestEffects effs =>
 FoldM (Eff effs) EmulatorEvent a)
-> TracePredicateF a
TracePredicate ((forall (effs :: [* -> *]).
  Members TestEffects effs =>
  FoldM (Eff effs) EmulatorEvent Bool)
 -> TracePredicate)
-> (forall (effs :: [* -> *]).
    Members TestEffects effs =>
    FoldM (Eff effs) EmulatorEvent Bool)
-> TracePredicate
forall a b. (a -> b) -> a -> b
$ Bool -> FoldM (Eff effs) EmulatorEvent Bool
forall (f :: * -> *) a. Applicative f => a -> f a
pure Bool
True)

checkNoLockedFundsProofFastWithOptions
  :: CheckableContractModel model
  => CheckOptions
  -> NoLockedFundsProof model
  -> Property
checkNoLockedFundsProofFastWithOptions :: CheckOptions -> NoLockedFundsProof model -> Property
checkNoLockedFundsProofFastWithOptions CheckOptions
_ = (Actions (WithInstances model) -> Property)
-> NoLockedFundsProof model -> Property
forall model.
CheckableContractModel model =>
(Actions (WithInstances model) -> Property)
-> NoLockedFundsProof model -> Property
checkNoLockedFundsProof' (Property -> Actions (WithInstances model) -> Property
forall a b. a -> b -> a
const (Property -> Actions (WithInstances model) -> Property)
-> Property -> Actions (WithInstances model) -> Property
forall a b. (a -> b) -> a -> b
$ Bool -> Property
forall prop. Testable prop => prop -> Property
property Bool
True)

checkNoLockedFundsProof'
  :: CheckableContractModel model
  => (Actions (WithInstances model) -> Property)
  -> NoLockedFundsProof model
  -> Property
checkNoLockedFundsProof' :: (Actions (WithInstances model) -> Property)
-> NoLockedFundsProof model -> Property
checkNoLockedFundsProof' Actions (WithInstances model) -> Property
run NoLockedFundsProof{nlfpMainStrategy :: forall model.
NoLockedFundsProof model -> DL (WithInstances model) ()
nlfpMainStrategy   = DL (WithInstances model) ()
mainStrat,
                                                nlfpWalletStrategy :: forall model.
NoLockedFundsProof model -> Wallet -> DL (WithInstances model) ()
nlfpWalletStrategy = Wallet -> DL (WithInstances model) ()
walletStrat,
                                                nlfpOverhead :: forall model.
NoLockedFundsProof model
-> ModelState (WithInstances model) -> SymValue
nlfpOverhead       = ModelState (WithInstances model) -> SymValue
overhead,
                                                nlfpErrorMargin :: forall model.
NoLockedFundsProof model
-> ModelState (WithInstances model) -> SymValue
nlfpErrorMargin    = ModelState (WithInstances model) -> SymValue
wiggle } =
    DL (WithInstances model) ()
-> (Actions (WithInstances model) -> Property) -> Property
forall state p.
(ContractModel state, Testable p) =>
DL state () -> (Actions state -> p) -> Property
forAllDL DL (WithInstances model) ()
forall state. DL state ()
anyActions_ ((Actions (WithInstances model) -> Property) -> Property)
-> (Actions (WithInstances model) -> Property) -> Property
forall a b. (a -> b) -> a -> b
$ \ (Actions [Act (WithInstances model)]
as) ->
    Int
-> ModelState (WithInstances model)
-> DL (WithInstances model) ()
-> (Actions (WithInstances model) -> Property)
-> Property
forall state p.
(ContractModel state, Testable p) =>
Int
-> ModelState state
-> DL state ()
-> (Actions state -> p)
-> Property
forAllUniqueDL ([Act (WithInstances model)] -> Int
forall s. [Act s] -> Int
nextVarIdx [Act (WithInstances model)]
as) (Actions (WithInstances model) -> ModelState (WithInstances model)
forall state.
ContractModel state =>
Actions state -> ModelState state
stateAfter (Actions (WithInstances model) -> ModelState (WithInstances model))
-> Actions (WithInstances model)
-> ModelState (WithInstances model)
forall a b. (a -> b) -> a -> b
$ [Act (WithInstances model)] -> Actions (WithInstances model)
forall s. [Act s] -> Actions s
Actions [Act (WithInstances model)]
as) DL (WithInstances model) ()
mainStrat ((Actions (WithInstances model) -> Property) -> Property)
-> (Actions (WithInstances model) -> Property) -> Property
forall a b. (a -> b) -> a -> b
$ \ (Actions [Act (WithInstances model)]
as') ->
          let s0 :: ModelState (WithInstances model)
s0 = (Actions (WithInstances model) -> ModelState (WithInstances model)
forall state.
ContractModel state =>
Actions state -> ModelState state
stateAfter (Actions (WithInstances model) -> ModelState (WithInstances model))
-> Actions (WithInstances model)
-> ModelState (WithInstances model)
forall a b. (a -> b) -> a -> b
$ [Act (WithInstances model)] -> Actions (WithInstances model)
forall s. [Act s] -> Actions s
Actions [Act (WithInstances model)]
as)
              s :: ModelState (WithInstances model)
s = Actions (WithInstances model) -> ModelState (WithInstances model)
forall state.
ContractModel state =>
Actions state -> ModelState state
stateAfter (Actions (WithInstances model) -> ModelState (WithInstances model))
-> Actions (WithInstances model)
-> ModelState (WithInstances model)
forall a b. (a -> b) -> a -> b
$ [Act (WithInstances model)] -> Actions (WithInstances model)
forall s. [Act s] -> Actions s
Actions ([Act (WithInstances model)]
as [Act (WithInstances model)]
-> [Act (WithInstances model)] -> [Act (WithInstances model)]
forall a. [a] -> [a] -> [a]
++ [Act (WithInstances model)]
as') in
            (Property -> Property -> Property)
-> Property -> [Property] -> Property
forall (t :: * -> *) b a.
Foldable t =>
(b -> a -> b) -> b -> t a -> b
foldl Property -> Property -> Property
forall prop1 prop2.
(Testable prop1, Testable prop2) =>
prop1 -> prop2 -> Property
(QC..&&.) ([Char] -> Property -> Property
forall prop. Testable prop => [Char] -> prop -> Property
counterexample [Char]
"Main run prop" (Actions (WithInstances model) -> Property
run ([Act (WithInstances model)] -> Actions (WithInstances model)
forall s. [Act s] -> Actions s
Actions ([Act (WithInstances model)] -> Actions (WithInstances model))
-> [Act (WithInstances model)] -> Actions (WithInstances model)
forall a b. (a -> b) -> a -> b
$ [Act (WithInstances model)]
as [Act (WithInstances model)]
-> [Act (WithInstances model)] -> [Act (WithInstances model)]
forall a. [a] -> [a] -> [a]
++ [Act (WithInstances model)]
as')) Property -> Property -> Property
forall prop1 prop2.
(Testable prop1, Testable prop2) =>
prop1 -> prop2 -> Property
QC..&&.
                             ([Char] -> Property -> Property
forall prop. Testable prop => [Char] -> prop -> Property
counterexample [Char]
"Main strategy" (Property -> Property)
-> (Property -> Property) -> Property -> Property
forall b c a. (b -> c) -> (a -> b) -> a -> c
. [Char] -> Property -> Property
forall prop. Testable prop => [Char] -> prop -> Property
counterexample (Actions (WithInstances model) -> [Char]
forall a. Show a => a -> [Char]
show (Actions (WithInstances model) -> [Char])
-> ([Act (WithInstances model)] -> Actions (WithInstances model))
-> [Act (WithInstances model)]
-> [Char]
forall b c a. (b -> c) -> (a -> b) -> a -> c
. [Act (WithInstances model)] -> Actions (WithInstances model)
forall s. [Act s] -> Actions s
Actions ([Act (WithInstances model)] -> [Char])
-> [Act (WithInstances model)] -> [Char]
forall a b. (a -> b) -> a -> b
$ [Act (WithInstances model)]
as [Act (WithInstances model)]
-> [Act (WithInstances model)] -> [Act (WithInstances model)]
forall a. [a] -> [a] -> [a]
++ [Act (WithInstances model)]
as') (Property -> Property) -> Property -> Property
forall a b. (a -> b) -> a -> b
$ ModelState (WithInstances model)
-> ModelState (WithInstances model) -> Property
prop ModelState (WithInstances model)
s0 ModelState (WithInstances model)
s))
                            [ ModelState (WithInstances model)
-> [Act (WithInstances model)] -> Wallet -> SymValue -> Property
walletProp ModelState (WithInstances model)
s0 [Act (WithInstances model)]
as Wallet
w SymValue
bal
                            | (AddressInEra Era
addr, SymValue
bal) <- Map (AddressInEra Era) SymValue -> [(AddressInEra Era, SymValue)]
forall k a. Map k a -> [(k, a)]
Map.toList (ModelState (WithInstances model)
s ModelState (WithInstances model)
-> Getting
     (Map (AddressInEra Era) SymValue)
     (ModelState (WithInstances model))
     (Map (AddressInEra Era) SymValue)
-> Map (AddressInEra Era) SymValue
forall s a. s -> Getting a s a -> a
^. Getting
  (Map (AddressInEra Era) SymValue)
  (ModelState (WithInstances model))
  (Map (AddressInEra Era) SymValue)
forall state.
Getter (ModelState state) (Map (AddressInEra Era) SymValue)
balanceChanges)
                            , Just Wallet
w <- [AddressInEra Era -> Maybe Wallet
addressToWallet AddressInEra Era
addr]
                            , Bool -> Bool
not (Bool -> Bool) -> Bool -> Bool
forall a b. (a -> b) -> a -> b
$ SymValue
bal SymValue -> SymValue -> Bool
`symLeq` (ModelState (WithInstances model)
s0 ModelState (WithInstances model)
-> Getting SymValue (ModelState (WithInstances model)) SymValue
-> SymValue
forall s a. s -> Getting a s a -> a
^. AddressInEra Era
-> Getter (ModelState (WithInstances model)) SymValue
forall state.
Ord (AddressInEra Era) =>
AddressInEra Era -> Getter (ModelState state) SymValue
balanceChange AddressInEra Era
addr) ]
                            -- if the main strategy leaves w with <= the starting value, then doing nothing is a good wallet strategy.
    where
        nextVarIdx :: [Act s] -> Int
nextVarIdx [Act s]
as = Int
1 Int -> Int -> Int
forall a. Num a => a -> a -> a
+ [Int] -> Int
forall (t :: * -> *) a. (Foldable t, Ord a) => t a -> a
maximum ([Int
0] [Int] -> [Int] -> [Int]
forall a. [a] -> [a] -> [a]
++ [ Int
i | Int
i <- Act s -> Int
forall s. Act s -> Int
varNumOf (Act s -> Int) -> [Act s] -> [Int]
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> [Act s]
as ])
        prop :: ModelState (WithInstances model)
-> ModelState (WithInstances model) -> Property
prop ModelState (WithInstances model)
s0 ModelState (WithInstances model)
s =
          -- TODO: check that nothing is locked by scripts
          let lockedVal :: SymValue
lockedVal = ModelState (WithInstances model) -> SymValue
forall s. ModelState s -> SymValue
lockedValue ModelState (WithInstances model)
s
          in ([Char] -> Bool -> Property
forall prop. Testable prop => [Char] -> prop -> Property
counterexample ([Char]
"Locked funds should be at most " [Char] -> [Char] -> [Char]
forall a. [a] -> [a] -> [a]
++ SymValue -> [Char]
forall a. Show a => a -> [Char]
show (ModelState (WithInstances model) -> SymValue
overhead ModelState (WithInstances model)
s0) [Char] -> [Char] -> [Char]
forall a. [a] -> [a] -> [a]
++ [Char]
", but they are\n  " [Char] -> [Char] -> [Char]
forall a. [a] -> [a] -> [a]
++ SymValue -> [Char]
forall a. Show a => a -> [Char]
show SymValue
lockedVal)
            (Bool -> Property) -> Bool -> Property
forall a b. (a -> b) -> a -> b
$ SymValue -> SymValue -> Bool
symLeq SymValue
lockedVal (ModelState (WithInstances model) -> SymValue
overhead ModelState (WithInstances model)
s0))

        walletProp :: ModelState (WithInstances model)
-> [Act (WithInstances model)] -> Wallet -> SymValue -> Property
walletProp ModelState (WithInstances model)
s0 [Act (WithInstances model)]
as Wallet
w SymValue
bal =
          Int
-> ModelState (WithInstances model)
-> DL (WithInstances model) ()
-> (Actions (ModelState (WithInstances model)) -> Property)
-> Property
forall s a.
(DynLogicModel s, Testable a) =>
Int -> s -> DL s () -> (Actions s -> a) -> Property
DL.forAllUniqueDL ([Act (WithInstances model)] -> Int
forall s. [Act s] -> Int
nextVarIdx [Act (WithInstances model)]
as) ModelState (WithInstances model)
s0 (Action (ModelState (WithInstances model)) (Map [Char] AssetId)
-> DL (WithInstances model) ()
forall a s. (Typeable a, Eq (Action s a)) => Action s a -> DL s ()
DL.action (Bool
-> Action (WithInstances model)
-> Action (ModelState (WithInstances model)) (Map [Char] AssetId)
forall state.
Bool
-> Action state -> Action (ModelState state) (Map [Char] AssetId)
ContractAction Bool
False (Action (WithInstances model)
 -> Action (ModelState (WithInstances model)) (Map [Char] AssetId))
-> Action (WithInstances model)
-> Action (ModelState (WithInstances model)) (Map [Char] AssetId)
forall a b. (a -> b) -> a -> b
$ Wallet -> Action (WithInstances model)
forall s. Wallet -> Action (WithInstances s)
Unilateral Wallet
w) DL (WithInstances model) ()
-> DL (WithInstances model) () -> DL (WithInstances model) ()
forall (m :: * -> *) a b. Monad m => m a -> m b -> m b
>> Wallet -> DL (WithInstances model) ()
walletStrat Wallet
w) ((Actions (ModelState (WithInstances model)) -> Property)
 -> Property)
-> (Actions (ModelState (WithInstances model)) -> Property)
-> Property
forall a b. (a -> b) -> a -> b
$ \ Actions (ModelState (WithInstances model))
acts ->
          let Actions [Act (WithInstances model)]
as' = Actions (ModelState (WithInstances model))
-> Actions (WithInstances model)
forall s. Actions (ModelState s) -> Actions s
fromStateModelActions Actions (ModelState (WithInstances model))
acts
              wig :: SymValue
wig = ModelState (WithInstances model) -> SymValue
wiggle ModelState (WithInstances model)
s0
              err :: [Char]
err  = [Char]
"Unilateral strategy for " [Char] -> [Char] -> [Char]
forall a. [a] -> [a] -> [a]
++ Wallet -> [Char]
forall a. Show a => a -> [Char]
show Wallet
w [Char] -> [Char] -> [Char]
forall a. [a] -> [a] -> [a]
++ [Char]
" should have gotten it at least\n" [Char] -> [Char] -> [Char]
forall a. [a] -> [a] -> [a]
++
                     [Char]
"  " [Char] -> [Char] -> [Char]
forall a. [a] -> [a] -> [a]
++ SymValue -> [Char]
forall a. Show a => a -> [Char]
show SymValue
bal [Char] -> [Char] -> [Char]
forall a. [a] -> [a] -> [a]
++ [Char]
"\n" [Char] -> [Char] -> [Char]
forall a. [a] -> [a] -> [a]
++
                     [[Char]] -> [Char]
forall (t :: * -> *) a. Foldable t => t [a] -> [a]
concat [ [Char]
"with wiggle room\n" [Char] -> [Char] -> [Char]
forall a. [a] -> [a] -> [a]
++ [Char]
"  " [Char] -> [Char] -> [Char]
forall a. [a] -> [a] -> [a]
++ SymValue -> [Char]
forall a. Show a => a -> [Char]
show SymValue
wig [Char] -> [Char] -> [Char]
forall a. [a] -> [a] -> [a]
++ [Char]
"\n"
                            | SymValue
wig SymValue -> SymValue -> Bool
forall a. Eq a => a -> a -> Bool
/= SymValue
forall a. Monoid a => a
mempty ] [Char] -> [Char] -> [Char]
forall a. [a] -> [a] -> [a]
++
                     [Char]
"but it got\n" [Char] -> [Char] -> [Char]
forall a. [a] -> [a] -> [a]
++
                     [Char]
"  " [Char] -> [Char] -> [Char]
forall a. [a] -> [a] -> [a]
++ SymValue -> [Char]
forall a. Show a => a -> [Char]
show SymValue
bal'
              bal' :: SymValue
bal' = Actions (WithInstances model) -> ModelState (WithInstances model)
forall state.
ContractModel state =>
Actions state -> ModelState state
stateAfter ([Act (WithInstances model)] -> Actions (WithInstances model)
forall s. [Act s] -> Actions s
Actions ([Act (WithInstances model)] -> Actions (WithInstances model))
-> [Act (WithInstances model)] -> Actions (WithInstances model)
forall a b. (a -> b) -> a -> b
$ [Act (WithInstances model)]
as [Act (WithInstances model)]
-> [Act (WithInstances model)] -> [Act (WithInstances model)]
forall a. [a] -> [a] -> [a]
++ [Act (WithInstances model)]
as') ModelState (WithInstances model)
-> Getting SymValue (ModelState (WithInstances model)) SymValue
-> SymValue
forall s a. s -> Getting a s a -> a
^. AddressInEra Era
-> Getter (ModelState (WithInstances model)) SymValue
forall state.
Ord (AddressInEra Era) =>
AddressInEra Era -> Getter (ModelState state) SymValue
balanceChange (Wallet -> AddressInEra Era
walletAddress Wallet
w)
              smacts :: Actions (WithInstances model)
smacts = [Act (WithInstances model)] -> Actions (WithInstances model)
forall s. [Act s] -> Actions s
Actions ([Act (WithInstances model)] -> Actions (WithInstances model))
-> [Act (WithInstances model)] -> Actions (WithInstances model)
forall a b. (a -> b) -> a -> b
$ [Act (WithInstances model)]
as [Act (WithInstances model)]
-> [Act (WithInstances model)] -> [Act (WithInstances model)]
forall a. [a] -> [a] -> [a]
++ [Act (WithInstances model)]
as' -- toStateModelActions (Actions as) <> acts
              err' :: [Char]
err' = [Char]
"The ContractModel's Unilateral behaviour for " [Char] -> [Char] -> [Char]
forall a. [a] -> [a] -> [a]
++ Wallet -> [Char]
forall a. Show a => a -> [Char]
show Wallet
w [Char] -> [Char] -> [Char]
forall a. [a] -> [a] -> [a]
++ [Char]
" does not match the actual behaviour for actions:\n"
                   [Char] -> [Char] -> [Char]
forall a. [a] -> [a] -> [a]
++ Actions (WithInstances model) -> [Char]
forall a. Show a => a -> [Char]
show Actions (WithInstances model)
smacts
          in [Char] -> Bool -> Property
forall prop. Testable prop => [Char] -> prop -> Property
counterexample [Char]
err (SymValue -> SymValue -> Bool
symLeq SymValue
bal (SymValue
bal' SymValue -> SymValue -> SymValue
forall a. Semigroup a => a -> a -> a
<> SymValue
wig))
          Property -> Property -> Property
forall prop1 prop2.
(Testable prop1, Testable prop2) =>
prop1 -> prop2 -> Property
QC..&&. [Char] -> Property -> Property
forall prop. Testable prop => [Char] -> prop -> Property
counterexample [Char]
err' (Actions (WithInstances model) -> Property
run Actions (WithInstances model)
smacts)

actionsFromList :: [Action s] -> Actions s
actionsFromList :: [Action s] -> Actions s
actionsFromList = [Act s] -> Actions s
forall s. [Act s] -> Actions s
Actions ([Act s] -> Actions s)
-> ([Action s] -> [Act s]) -> [Action s] -> Actions s
forall b c a. (b -> c) -> (a -> b) -> a -> c
. (Var (Map [Char] AssetId) -> Action s -> Act s)
-> [Var (Map [Char] AssetId)] -> [Action s] -> [Act s]
forall a b c. (a -> b -> c) -> [a] -> [b] -> [c]
zipWith Var (Map [Char] AssetId) -> Action s -> Act s
forall s. Var (Map [Char] AssetId) -> Action s -> Act s
NoBind (Int -> Var (Map [Char] AssetId)
forall a. Int -> Var a
StateModel.Var (Int -> Var (Map [Char] AssetId))
-> [Int] -> [Var (Map [Char] AssetId)]
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> [Int
0..])

varNumOf :: Act s -> Int
varNumOf :: Act s -> Int
varNumOf (ActWaitUntil (StateModel.Var Int
i) SlotNo
_) = Int
i
varNumOf Act s
act | StateModel.Var Int
i <- Act s -> Var (Map [Char] AssetId)
forall s. Act s -> Var (Map [Char] AssetId)
varOf Act s
act = Int
i

-- TODO: possibly there's a nicer way to do this...?
walletAddress :: Wallet -> CardanoAPI.AddressInEra Era
walletAddress :: Wallet -> AddressInEra Era
walletAddress Wallet
w
  | Just Hash PaymentKey
hash <- AsType (Hash PaymentKey) -> ByteString -> Maybe (Hash PaymentKey)
forall a.
SerialiseAsRawBytes a =>
AsType a -> ByteString -> Maybe a
CardanoAPI.deserialiseFromRawBytes (AsType PaymentKey -> AsType (Hash PaymentKey)
forall a. AsType a -> AsType (Hash a)
CardanoAPI.AsHash AsType PaymentKey
CardanoAPI.AsPaymentKey)
                                                    (BuiltinByteString -> ByteString
forall arep a. FromBuiltin arep a => arep -> a
Builtins.fromBuiltin BuiltinByteString
pkh) =
      Address ShelleyAddr -> AddressInEra Era
forall era.
IsShelleyBasedEra era =>
Address ShelleyAddr -> AddressInEra era
CardanoAPI.shelleyAddressInEra (Address ShelleyAddr -> AddressInEra Era)
-> Address ShelleyAddr -> AddressInEra Era
forall a b. (a -> b) -> a -> b
$
      -- TODO: this is all wrong! It needs to be some magic version of testnet
      NetworkId
-> PaymentCredential
-> StakeAddressReference
-> Address ShelleyAddr
CardanoAPI.makeShelleyAddress NetworkId
testnet
                                    (Hash PaymentKey -> PaymentCredential
CardanoAPI.PaymentCredentialByKey Hash PaymentKey
hash)
                                    StakeAddressReference
CardanoAPI.NoStakeAddress
  | Bool
otherwise = [Char] -> AddressInEra Era
forall a. HasCallStack => [Char] -> a
error ([Char] -> AddressInEra Era) -> [Char] -> AddressInEra Era
forall a b. (a -> b) -> a -> b
$ [Char]
"Bad wallet: " [Char] -> [Char] -> [Char]
forall a. [a] -> [a] -> [a]
++ Wallet -> [Char]
forall a. Show a => a -> [Char]
show Wallet
w
  where pkh :: BuiltinByteString
pkh = PubKeyHash -> BuiltinByteString
getPubKeyHash (PubKeyHash -> BuiltinByteString)
-> PubKeyHash -> BuiltinByteString
forall a b. (a -> b) -> a -> b
$ PaymentPubKeyHash -> PubKeyHash
unPaymentPubKeyHash (PaymentPubKeyHash -> PubKeyHash)
-> PaymentPubKeyHash -> PubKeyHash
forall a b. (a -> b) -> a -> b
$ Wallet -> PaymentPubKeyHash
mockWalletPaymentPubKeyHash Wallet
w

addressToWallet :: CardanoAPI.AddressInEra Era -> Maybe Wallet
addressToWallet :: AddressInEra Era -> Maybe Wallet
addressToWallet AddressInEra Era
a = AddressInEra Era -> [(AddressInEra Era, Wallet)] -> Maybe Wallet
forall a b. Eq a => a -> [(a, b)] -> Maybe b
List.lookup AddressInEra Era
a [ (Wallet -> AddressInEra Era
walletAddress Wallet
w, Wallet
w) | Wallet
w <- [Wallet]
knownWallets ]

checkNoLockedFundsProofLight
  :: CheckableContractModel model
  => NoLockedFundsProofLight model
  -> Property
checkNoLockedFundsProofLight :: NoLockedFundsProofLight model -> Property
checkNoLockedFundsProofLight NoLockedFundsProofLight{nlfplMainStrategy :: forall model.
NoLockedFundsProofLight model -> DL (WithInstances model) ()
nlfplMainStrategy = DL (WithInstances model) ()
mainStrat} =
  DL (WithInstances model) ()
-> (Actions (WithInstances model) -> Property) -> Property
forall state p.
(ContractModel state, Testable p) =>
DL state () -> (Actions state -> p) -> Property
forAllDL DL (WithInstances model) ()
forall state. DL state ()
anyActions_ ((Actions (WithInstances model) -> Property) -> Property)
-> (Actions (WithInstances model) -> Property) -> Property
forall a b. (a -> b) -> a -> b
$ \ (Actions [Act (WithInstances model)]
as) ->
    Int
-> ModelState (WithInstances model)
-> DL (WithInstances model) ()
-> (Actions (WithInstances model) -> Property)
-> Property
forall state p.
(ContractModel state, Testable p) =>
Int
-> ModelState state
-> DL state ()
-> (Actions state -> p)
-> Property
forAllUniqueDL ([Act (WithInstances model)] -> Int
forall s. [Act s] -> Int
nextVarIdx [Act (WithInstances model)]
as) (Actions (WithInstances model) -> ModelState (WithInstances model)
forall state.
ContractModel state =>
Actions state -> ModelState state
stateAfter (Actions (WithInstances model) -> ModelState (WithInstances model))
-> Actions (WithInstances model)
-> ModelState (WithInstances model)
forall a b. (a -> b) -> a -> b
$ [Act (WithInstances model)] -> Actions (WithInstances model)
forall s. [Act s] -> Actions s
Actions [Act (WithInstances model)]
as) DL (WithInstances model) ()
mainStrat ((Actions (WithInstances model) -> Property) -> Property)
-> (Actions (WithInstances model) -> Property) -> Property
forall a b. (a -> b) -> a -> b
$ \ (Actions [Act (WithInstances model)]
as') ->
      [Char] -> Property -> Property
forall prop. Testable prop => [Char] -> prop -> Property
counterexample [Char]
"Main run prop" (Actions (WithInstances model) -> Property
run (Actions (WithInstances model) -> Property)
-> Actions (WithInstances model) -> Property
forall a b. (a -> b) -> a -> b
$ [Act (WithInstances model)] -> Actions (WithInstances model)
forall s. [Act s] -> Actions s
Actions ([Act (WithInstances model)] -> Actions (WithInstances model))
-> [Act (WithInstances model)] -> Actions (WithInstances model)
forall a b. (a -> b) -> a -> b
$ [Act (WithInstances model)]
as [Act (WithInstances model)]
-> [Act (WithInstances model)] -> [Act (WithInstances model)]
forall a. [a] -> [a] -> [a]
++ [Act (WithInstances model)]
as')
  where
    nextVarIdx :: [Act s] -> Int
nextVarIdx [Act s]
as = Int
1 Int -> Int -> Int
forall a. Num a => a -> a -> a
+ [Int] -> Int
forall (t :: * -> *) a. (Foldable t, Ord a) => t a -> a
maximum ([Int
0] [Int] -> [Int] -> [Int]
forall a. [a] -> [a] -> [a]
++ [ Int
i | StateModel.Var Int
i <- Act s -> Var (Map [Char] AssetId)
forall s. Act s -> Var (Map [Char] AssetId)
varOf (Act s -> Var (Map [Char] AssetId))
-> [Act s] -> [Var (Map [Char] AssetId)]
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> [Act s]
as ])
    run :: Actions (WithInstances model) -> Property
run = CheckOptions
-> CoverageOptions
-> (ModelState (WithInstances model) -> TracePredicate)
-> Actions (WithInstances model)
-> Property
forall state.
CheckableContractModel state =>
CheckOptions
-> CoverageOptions
-> (ModelState (WithInstances state) -> TracePredicate)
-> Actions (WithInstances state)
-> Property
propRunActionsWithOptions CheckOptions
defaultCheckOptionsContractModel
                                    CoverageOptions
defaultCoverageOptions (\ ModelState (WithInstances model)
_ -> (forall (effs :: [* -> *]).
 Members TestEffects effs =>
 FoldM (Eff effs) EmulatorEvent Bool)
-> TracePredicate
forall a.
(forall (effs :: [* -> *]).
 Members TestEffects effs =>
 FoldM (Eff effs) EmulatorEvent a)
-> TracePredicateF a
TracePredicate ((forall (effs :: [* -> *]).
  Members TestEffects effs =>
  FoldM (Eff effs) EmulatorEvent Bool)
 -> TracePredicate)
-> (forall (effs :: [* -> *]).
    Members TestEffects effs =>
    FoldM (Eff effs) EmulatorEvent Bool)
-> TracePredicate
forall a b. (a -> b) -> a -> b
$ Bool -> FoldM (Eff effs) EmulatorEvent Bool
forall (f :: * -> *) a. Applicative f => a -> f a
pure Bool
True)

-- | A whitelist entry tells you what final log entry prefixes
-- are acceptable for a given error
data Whitelist = Whitelist { Whitelist -> Set Text
errorPrefixes :: Set Text.Text }

instance Semigroup Whitelist where
  Whitelist Set Text
wl <> :: Whitelist -> Whitelist -> Whitelist
<> Whitelist Set Text
wl' = Set Text -> Whitelist
Whitelist (Set Text -> Whitelist) -> Set Text -> Whitelist
forall a b. (a -> b) -> a -> b
$ Set Text
wl Set Text -> Set Text -> Set Text
forall a. Semigroup a => a -> a -> a
<> Set Text
wl'

instance Monoid Whitelist where
  mempty :: Whitelist
mempty = Whitelist
defaultWhitelist

-- | Check that the last entry in a log is accepted by a whitelist entry
isAcceptedBy :: Maybe Text.Text -> Whitelist -> Bool
isAcceptedBy :: Maybe Text -> Whitelist -> Bool
isAcceptedBy Maybe Text
Nothing Whitelist
_           = Bool
False
isAcceptedBy (Just Text
lastEntry) Whitelist
wl = (Text -> Bool) -> [Text] -> Bool
forall (t :: * -> *) a. Foldable t => (a -> Bool) -> t a -> Bool
any (Text -> Text -> Bool
`Text.isPrefixOf` Text
lastEntry) (Set Text -> [Text]
forall a. Set a -> [a]
Set.toList (Set Text -> [Text]) -> Set Text -> [Text]
forall a b. (a -> b) -> a -> b
$ Whitelist -> Set Text
errorPrefixes Whitelist
wl)

{- Note [Maintaining `whitelistOk` and `checkErrorWhitelist`]
   The intended use case of `checkErrorWhitelist` is to be able to assert that failures of
   validation only happen for reasons that the programmer intended. However, to avoid
   degenerate whitelists that accept obvious mistakes like validation failing because a
   partial function in the prelude failed we need to make sure that any whitelist used passes
   the `whitelistOk` check. This means in turn that we need to maintain `whitelistOk` when we
   introduce new failure modes or change existing failure modes in the prelude or elsewhere
   in the plutus system.
-}

-- | Check that a whitelist does not accept any partial functions
whitelistOk :: Whitelist -> Bool
whitelistOk :: Whitelist -> Bool
whitelistOk Whitelist
wl = Bool
noPreludePartials
  where
    noPreludePartials :: Bool
noPreludePartials =
      -- We specifically ignore `checkHasFailed` here because it is the failure you get when a
      -- validator that returns a boolean fails correctly.
      (BuiltinString -> Bool) -> [BuiltinString] -> Bool
forall (t :: * -> *) a. Foldable t => (a -> Bool) -> t a -> Bool
all (\BuiltinString
ec -> Bool -> Bool
Prelude.not (Bool -> Bool) -> Bool -> Bool
forall a b. (a -> b) -> a -> b
$ (Text -> Maybe Text
forall a. a -> Maybe a
Just (Text -> Maybe Text) -> Text -> Maybe Text
forall a b. (a -> b) -> a -> b
$ BuiltinString -> Text
forall arep a. FromBuiltin arep a => arep -> a
Builtins.fromBuiltin BuiltinString
ec) Maybe Text -> Whitelist -> Bool
`isAcceptedBy` Whitelist
wl)
          (Map BuiltinString [Char] -> [BuiltinString]
forall k a. Map k a -> [k]
Map.keys Map BuiltinString [Char]
allErrorCodes [BuiltinString] -> [BuiltinString] -> [BuiltinString]
forall a. Eq a => [a] -> [a] -> [a]
\\ [BuiltinString
checkHasFailedError])

mkWhitelist :: [Text.Text] -> Whitelist
mkWhitelist :: [Text] -> Whitelist
mkWhitelist [Text]
txs = Whitelist
defaultWhitelist Whitelist -> Whitelist -> Whitelist
forall a. Semigroup a => a -> a -> a
<> Set Text -> Whitelist
Whitelist ([Text] -> Set Text
forall a. Ord a => [a] -> Set a
Set.fromList [Text]
txs)

defaultWhitelist :: Whitelist
defaultWhitelist :: Whitelist
defaultWhitelist = Set Text -> Whitelist
Whitelist (Set Text -> Whitelist) -> (Text -> Set Text) -> Text -> Whitelist
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Text -> Set Text
forall a. a -> Set a
Set.singleton (Text -> Whitelist) -> Text -> Whitelist
forall a b. (a -> b) -> a -> b
$ BuiltinString -> Text
forall arep a. FromBuiltin arep a => arep -> a
Builtins.fromBuiltin BuiltinString
checkHasFailedError

-- | Check that running a contract model does not result in validation
-- failures that are not accepted by the whitelist.
checkErrorWhitelist :: CheckableContractModel m
                    => Whitelist
                    -> Actions (WithInstances m)
                    -> Property
checkErrorWhitelist :: Whitelist -> Actions (WithInstances m) -> Property
checkErrorWhitelist = CheckOptions
-> CoverageOptions
-> Whitelist
-> Actions (WithInstances m)
-> Property
forall m.
CheckableContractModel m =>
CheckOptions
-> CoverageOptions
-> Whitelist
-> Actions (WithInstances m)
-> Property
checkErrorWhitelistWithOptions CheckOptions
defaultCheckOptionsContractModel CoverageOptions
defaultCoverageOptions

-- | Check that running a contract model does not result in validation
-- failures that are not accepted by the whitelist.
checkErrorWhitelistWithOptions :: forall m.
                                  CheckableContractModel m
                               => CheckOptions
                               -> CoverageOptions
                               -> Whitelist
                               -> Actions (WithInstances m)
                               -> Property
checkErrorWhitelistWithOptions :: CheckOptions
-> CoverageOptions
-> Whitelist
-> Actions (WithInstances m)
-> Property
checkErrorWhitelistWithOptions CheckOptions
opts CoverageOptions
copts Whitelist
whitelist =
  CheckOptions
-> CoverageOptions
-> (ModelState (WithInstances m) -> TracePredicate)
-> Actions (WithInstances m)
-> Property
forall state.
CheckableContractModel state =>
CheckOptions
-> CoverageOptions
-> (ModelState (WithInstances state) -> TracePredicate)
-> Actions (WithInstances state)
-> Property
propRunActionsWithOptions CheckOptions
opts CoverageOptions
copts (TracePredicate -> ModelState (WithInstances m) -> TracePredicate
forall a b. a -> b -> a
const TracePredicate
check)
  where
    check :: TracePredicate
    check :: TracePredicate
check = TracePredicate
checkOnchain TracePredicate -> TracePredicate -> TracePredicate
.&&. (TracePredicate
assertNoFailedTransactions TracePredicate -> TracePredicate -> TracePredicate
.||. TracePredicate
checkOffchain)

    checkOnchain :: TracePredicate
    checkOnchain :: TracePredicate
checkOnchain = ([ChainEvent] -> Bool) -> TracePredicate
assertChainEvents [ChainEvent] -> Bool
checkEvents

    checkOffchain :: TracePredicate
    checkOffchain :: TracePredicate
checkOffchain = (Tx -> ValidationError -> Bool) -> TracePredicate
assertFailedTransaction (\ Tx
_ ValidationError
ve -> case ValidationError
ve of {ScriptFailure ScriptError
e -> ScriptError -> Bool
checkEvent ScriptError
e; ValidationError
_ -> Bool
False})

    checkEvent :: ScriptError -> Bool
    checkEvent :: ScriptError -> Bool
checkEvent (EvaluationError [Text]
log [Char]
msg) | [Char]
"CekEvaluationFailure" [Char] -> [Char] -> Bool
forall a. Eq a => [a] -> [a] -> Bool
`isPrefixOf` [Char]
msg = [Text] -> Maybe Text
forall a. [a] -> Maybe a
listToMaybe ([Text] -> [Text]
forall a. [a] -> [a]
reverse [Text]
log) Maybe Text -> Whitelist -> Bool
`isAcceptedBy` Whitelist
whitelist
    checkEvent (EvaluationError [Text]
_ [Char]
msg) | [Char]
"BuiltinEvaluationFailure" [Char] -> [Char] -> Bool
forall a. Eq a => [a] -> [a] -> Bool
`isPrefixOf` [Char]
msg = Bool
False
    checkEvent ScriptError
_ = Bool
False

    checkEvents :: [ChainEvent] -> Bool
    checkEvents :: [ChainEvent] -> Bool
checkEvents [ChainEvent]
events = (ScriptError -> Bool) -> [ScriptError] -> Bool
forall (t :: * -> *) a. Foldable t => (a -> Bool) -> t a -> Bool
all ScriptError -> Bool
checkEvent [ ScriptError
f | (TxnValidationFail ValidationPhase
_ TxId
_ CardanoTx
_ (ScriptFailure ScriptError
f) Value
_ [Text]
_) <- [ChainEvent]
events ]