-- | 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 (chainStateToChainIndex, chainStateToContractModelChainState)
import Cardano.Node.Emulator.Internal.Node (ChainEvent (TxnValidation))
import Cardano.Node.Emulator.Internal.Node.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 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 (SlotNo (..))
import Cardano.Api qualified as CardanoAPI
import Cardano.Api.Shelley (ProtocolParameters)
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 (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.ContractModel.Internal (ContractModelResult)
import Test.QuickCheck.ContractModel.Internal.Model (annotatedStateAfter)
import Test.QuickCheck.ContractModel.ThreatModel (ThreatModel, assertThreatModel)
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 Ledger.Value.CardanoAPI (lovelaceValueOf)
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
                => (forall t. HasSymbolicRep t => Symbolic t -> t)
                -> [StartContract state]
                -> EmulatorTraceWithInstances state ()
activateWallets :: (forall t. HasSymbolicRep t => Symbolic t -> t)
-> [StartContract state] -> EmulatorTraceWithInstances state ()
activateWallets forall t. HasSymbolicRep t => Symbolic t -> t
_ [] = () -> EmulatorTraceWithInstances state ()
forall (m :: * -> *) a. Monad m => a -> m a
return ()
activateWallets forall t. HasSymbolicRep t => Symbolic t -> t
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 ((forall t. HasSymbolicRep t => Symbolic t -> t)
-> ContractInstanceKey state w s e p -> p -> Contract w s e ()
forall state w (s :: Row *) e p.
ContractInstanceModel state =>
(forall t. HasSymbolicRep t => Symbolic t -> t)
-> ContractInstanceKey state w s e p -> p -> Contract w s e ()
instanceContract forall t. HasSymbolicRep t => Symbolic t -> t
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)
    (forall t. HasSymbolicRep t => Symbolic t -> t)
-> [StartContract state] -> EmulatorTraceWithInstances state ()
forall state.
ContractInstanceModel state =>
(forall t. HasSymbolicRep t => Symbolic t -> t)
-> [StartContract state] -> EmulatorTraceWithInstances state ()
activateWallets forall t. HasSymbolicRep t => Symbolic t -> t
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)
-> (forall t. HasSymbolicRep t => Symbolic t -> t)
-> RunMonad (EmulatorTraceWithInstances state) ()
perform ModelState (WithInstances state)
si (UnderlyingAction a) forall t. HasSymbolicRep t => Symbolic t -> t
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
$ (forall t. HasSymbolicRep t => Symbolic t -> t)
-> [StartContract state]
-> Eff (State (Handles state) : EmulatorEffects) ()
forall state.
ContractInstanceModel state =>
(forall t. HasSymbolicRep t => Symbolic t -> t)
-> [StartContract state] -> EmulatorTraceWithInstances state ()
activateWallets forall t. HasSymbolicRep t => Symbolic t -> t
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
-> (forall t. HasSymbolicRep t => Symbolic t -> t)
-> RunMonad (SpecificationEmulatorTrace state) ()
forall state (m :: * -> *).
RunModel state m =>
ModelState state
-> Action state
-> (forall t. HasSymbolicRep t => Symbolic t -> t)
-> RunMonad m ()
perform @_ @(SpecificationEmulatorTrace state) ModelState state
s Action state
a forall t. HasSymbolicRep t => Symbolic t -> t
symEnv
  perform ModelState (WithInstances state)
_ (Unilateral w) forall t. HasSymbolicRep t => Symbolic t -> t
_ = 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)
-> (forall t. HasSymbolicRep t => Symbolic t -> t)
-> SymIndex
-> Property
-> Property
monitoring (ModelState (WithInstances state)
s, ModelState (WithInstances state)
s') (UnderlyingAction a) = (ModelState state, ModelState state)
-> Action state
-> (forall t. HasSymbolicRep t => Symbolic t -> t)
-> SymIndex
-> Property
-> Property
forall state (m :: * -> *).
RunModel state m =>
(ModelState state, ModelState state)
-> Action state
-> (forall t. HasSymbolicRep t => Symbolic t -> t)
-> SymIndex
-> 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{} = \ forall t. HasSymbolicRep t => Symbolic t -> t
_ SymIndex
_ -> 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 Member EmulatorControl effs => HasChainIndex (Eff effs) where
  getChainIndex :: Eff effs ChainIndex
getChainIndex = do
    NetworkId
nid <- Params -> NetworkId
pNetworkId (Params -> NetworkId) -> Eff effs Params -> Eff effs NetworkId
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> Eff effs Params
forall (effs :: [* -> *]).
Member EmulatorControl effs =>
Eff effs Params
EmulatorControl.getParams
    NetworkId -> ChainState -> ChainIndex
chainStateToChainIndex NetworkId
nid (ChainState -> ChainIndex)
-> Eff effs ChainState -> Eff effs ChainIndex
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> Eff effs ChainState
forall (effs :: [* -> *]).
Member EmulatorControl effs =>
Eff effs ChainState
EmulatorControl.chainState
  getChainState :: Eff effs ChainState
getChainState = ChainState -> ChainState
chainStateToContractModelChainState (ChainState -> ChainState)
-> Eff effs ChainState -> Eff effs ChainState
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> Eff effs ChainState
forall (effs :: [* -> *]).
Member EmulatorControl effs =>
Eff effs ChainState
EmulatorControl.chainState

-- | `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 (HasChainIndex (Eff effs), 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 HasSymbolics (Action s) => HasSymbolics (Action (WithInstances s)) where
  getAllSymbolics :: Action (WithInstances s) -> SymCollectionIndex
getAllSymbolics (UnderlyingAction a) = Action s -> SymCollectionIndex
forall a. HasSymbolics a => a -> SymCollectionIndex
getAllSymbolics Action s
a
  getAllSymbolics Unilateral{}         = SymCollectionIndex
forall a. Monoid a => a
mempty

deriving via StateModel.HasNoVariables Wallet instance StateModel.HasVariables Wallet

instance forall s. ContractModel s => ContractModel (WithInstances s) where
  data Action (WithInstances s) = UnderlyingAction (Action s)
                                | Unilateral Wallet
                                deriving (forall x.
 Action (WithInstances s) -> Rep (Action (WithInstances s)) x)
-> (forall x.
    Rep (Action (WithInstances s)) x -> Action (WithInstances s))
-> Generic (Action (WithInstances s))
forall x.
Rep (Action (WithInstances s)) x -> Action (WithInstances s)
forall x.
Action (WithInstances s) -> Rep (Action (WithInstances s)) x
forall a.
(forall x. a -> Rep a x) -> (forall x. Rep a x -> a) -> Generic a
forall s x.
Rep (Action (WithInstances s)) x -> Action (WithInstances s)
forall s x.
Action (WithInstances s) -> Rep (Action (WithInstances s)) x
$cto :: forall s x.
Rep (Action (WithInstances s)) x -> Action (WithInstances s)
$cfrom :: forall s x.
Action (WithInstances s) -> Rep (Action (WithInstances s)) x
Generic
  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
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)

balanceChangePredicate :: ProtocolParameters -> ContractModelResult state -> Property
balanceChangePredicate :: ProtocolParameters -> ContractModelResult state -> Property
balanceChangePredicate ProtocolParameters
ps ContractModelResult state
result =
  let 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
  in BalanceChangeOptions -> ContractModelResult 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 state
result

threatModelPredicate :: ThreatModel a -> ProtocolParameters -> ContractModelResult state -> Property
threatModelPredicate :: ThreatModel a
-> ProtocolParameters -> ContractModelResult state -> Property
threatModelPredicate ThreatModel a
m ProtocolParameters
ps ContractModelResult state
result = ThreatModel a
-> ProtocolParameters -> ContractModelResult state -> Property
forall a state.
ThreatModel a
-> ProtocolParameters -> ContractModelResult state -> Property
assertThreatModel ThreatModel a
m ProtocolParameters
ps ContractModelResult state
result

-- | Check a threat model on all transactions produced by the given actions.
checkThreatModel ::
    CheckableContractModel state
    => ThreatModel a
    -> Actions (WithInstances state)                 -- ^ The actions to run
    -> Property
checkThreatModel :: ThreatModel a -> Actions (WithInstances state) -> Property
checkThreatModel = CheckOptions
-> CoverageOptions
-> ThreatModel a
-> Actions (WithInstances state)
-> Property
forall state a.
CheckableContractModel state =>
CheckOptions
-> CoverageOptions
-> ThreatModel a
-> Actions (WithInstances state)
-> Property
checkThreatModelWithOptions CheckOptions
defaultCheckOptionsContractModel CoverageOptions
defaultCoverageOptions

-- | Check a threat model on all transactions produced by the given actions.
checkThreatModelWithOptions ::
    CheckableContractModel state
    => CheckOptions                                  -- ^ Emulator options
    -> CoverageOptions                               -- ^ Coverage options
    -> ThreatModel a
    -> Actions (WithInstances state)                 -- ^ The actions to run
    -> Property
checkThreatModelWithOptions :: CheckOptions
-> CoverageOptions
-> ThreatModel a
-> Actions (WithInstances state)
-> Property
checkThreatModelWithOptions CheckOptions
opts CoverageOptions
covopts ThreatModel a
m Actions (WithInstances state)
actions =
  CheckOptions
-> CoverageOptions
-> (ModelState (WithInstances state) -> TracePredicate)
-> (ProtocolParameters
    -> ContractModelResult (WithInstances state) -> Property)
-> Actions (WithInstances state)
-> Property
forall state.
CheckableContractModel state =>
CheckOptions
-> CoverageOptions
-> (ModelState (WithInstances state) -> TracePredicate)
-> (ProtocolParameters
    -> ContractModelResult (WithInstances state) -> Property)
-> Actions (WithInstances state)
-> Property
propRunActionsWithOptions CheckOptions
opts CoverageOptions
covopts (\ ModelState (WithInstances state)
_ -> Bool -> TracePredicate
forall (f :: * -> *) a. Applicative f => a -> f a
pure Bool
True) (ThreatModel a
-> ProtocolParameters
-> ContractModelResult (WithInstances state)
-> Property
forall a state.
ThreatModel a
-> ProtocolParameters -> ContractModelResult state -> Property
threatModelPredicate ThreatModel a
m) 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. 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)
-> (ProtocolParameters
    -> ContractModelResult (WithInstances state) -> Property)
-> Actions (WithInstances state)
-> Property
forall state.
CheckableContractModel state =>
(ModelState (WithInstances state) -> TracePredicate)
-> (ProtocolParameters
    -> ContractModelResult (WithInstances state) -> Property)
-> Actions (WithInstances state)
-> Property
propRunActions (\ ModelState (WithInstances state)
_ -> Bool -> TracePredicate
forall (f :: * -> *) a. Applicative f => a -> f a
pure Bool
True) ProtocolParameters
-> ContractModelResult (WithInstances state) -> Property
forall state.
ProtocolParameters -> ContractModelResult state -> Property
balanceChangePredicate 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
    -> (ProtocolParameters -> ContractModelResult (WithInstances state) -> Property) -- ^ Predicate to run on the contract model
    -> Actions (WithInstances state)                        -- ^ The actions to run
    -> Property
propRunActions :: (ModelState (WithInstances state) -> TracePredicate)
-> (ProtocolParameters
    -> ContractModelResult (WithInstances state) -> Property)
-> Actions (WithInstances state)
-> Property
propRunActions = CheckOptions
-> CoverageOptions
-> (ModelState (WithInstances state) -> TracePredicate)
-> (ProtocolParameters
    -> ContractModelResult (WithInstances state) -> Property)
-> Actions (WithInstances state)
-> Property
forall state.
CheckableContractModel state =>
CheckOptions
-> CoverageOptions
-> (ModelState (WithInstances state) -> TracePredicate)
-> (ProtocolParameters
    -> ContractModelResult (WithInstances state) -> Property)
-> 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
    -> (ProtocolParameters -> ContractModelResult (WithInstances state) -> Property) -- ^ Predicate to run on the contract model
    -> Actions (WithInstances state)                        -- ^ The actions to run
    -> Property
propRunActionsWithOptions :: CheckOptions
-> CoverageOptions
-> (ModelState (WithInstances state) -> TracePredicate)
-> (ProtocolParameters
    -> ContractModelResult (WithInstances state) -> Property)
-> Actions (WithInstances state)
-> Property
propRunActionsWithOptions CheckOptions
opts CoverageOptions
copts ModelState (WithInstances state) -> TracePredicate
predicate ProtocolParameters
-> ContractModelResult (WithInstances state) -> Property
contractmodelPredicate 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

        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
$ (forall t. HasSymbolicRep t => Symbolic t -> t)
-> [StartContract state]
-> Eff (State (Handles state) : EmulatorEffects) ()
forall state.
ContractInstanceModel state =>
(forall t. HasSymbolicRep t => Symbolic t -> t)
-> [StartContract state] -> EmulatorTraceWithInstances state ()
activateWallets (\ Symbolic t
_ -> [Char] -> t
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
$ ProtocolParameters
-> ContractModelResult (WithInstances state) -> Property
contractmodelPredicate ProtocolParameters
ps 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, SymIndex) -> Property)
-> Eff
     (State (Handles state) : EmulatorEffects) (Property, SymIndex)
-> Eff (State (Handles state) : EmulatorEffects) Property
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap (Property, SymIndex) -> Property
forall a b. (a, b) -> a
fst
                              (Eff (State (Handles state) : EmulatorEffects) (Property, SymIndex)
 -> Eff (State (Handles state) : EmulatorEffects) Property)
-> (RunMonad (EmulatorTraceWithInstances state) Property
    -> Eff
         (State (Handles state) : EmulatorEffects) (Property, SymIndex))
-> RunMonad (EmulatorTraceWithInstances state) Property
-> Eff (State (Handles state) : EmulatorEffects) Property
forall b c a. (b -> c) -> (a -> b) -> a -> c
. WriterT SymIndex (EmulatorTraceWithInstances state) Property
-> Eff
     (State (Handles state) : EmulatorEffects) (Property, SymIndex)
forall w (m :: * -> *) a. WriterT w m a -> m (a, w)
runWriterT
                              (WriterT SymIndex (EmulatorTraceWithInstances state) Property
 -> Eff
      (State (Handles state) : EmulatorEffects) (Property, SymIndex))
-> (RunMonad (EmulatorTraceWithInstances state) Property
    -> WriterT SymIndex (EmulatorTraceWithInstances state) Property)
-> RunMonad (EmulatorTraceWithInstances state) Property
-> Eff
     (State (Handles state) : EmulatorEffects) (Property, SymIndex)
forall b c a. (b -> c) -> (a -> b) -> a -> c
. RunMonad (EmulatorTraceWithInstances state) Property
-> WriterT SymIndex (EmulatorTraceWithInstances state) Property
forall (m :: * -> *) a. RunMonad m a -> WriterT SymIndex 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)
-> (ProtocolParameters
    -> ContractModelResult (WithInstances model) -> Property)
-> Actions (WithInstances model)
-> Property
forall state.
CheckableContractModel state =>
CheckOptions
-> CoverageOptions
-> (ModelState (WithInstances state) -> TracePredicate)
-> (ProtocolParameters
    -> ContractModelResult (WithInstances state) -> Property)
-> 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) ProtocolParameters
-> ContractModelResult (WithInstances model) -> Property
forall state.
ProtocolParameters -> ContractModelResult state -> Property
balanceChangePredicate

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) ->
    let ans0 :: Annotated (ModelState (WithInstances model))
ans0 = (Actions (WithInstances model)
-> Annotated (ModelState (WithInstances model))
forall state.
ContractModel state =>
Actions state -> Annotated (ModelState state)
annotatedStateAfter (Actions (WithInstances model)
 -> Annotated (ModelState (WithInstances model)))
-> Actions (WithInstances model)
-> Annotated (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) in
    Annotated (ModelState (WithInstances model))
-> DL (WithInstances model) ()
-> (Actions (WithInstances model) -> Property)
-> Property
forall state p.
(ContractModel state, Testable p) =>
Annotated (ModelState state)
-> DL state () -> (Actions state -> p) -> Property
forAllUniqueDL Annotated (ModelState (WithInstances model))
ans0 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))
                            [ Annotated (ModelState (WithInstances model))
-> ModelState (WithInstances model)
-> [Act (WithInstances model)]
-> Wallet
-> SymValue
-> Property
walletProp Annotated (ModelState (WithInstances model))
ans0 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
        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 :: Annotated (ModelState (WithInstances model))
-> ModelState (WithInstances model)
-> [Act (WithInstances model)]
-> Wallet
-> SymValue
-> Property
walletProp Annotated (ModelState (WithInstances model))
ans0 ModelState (WithInstances model)
s0 [Act (WithInstances model)]
as Wallet
w SymValue
bal =
          Annotated (ModelState (WithInstances model))
-> DL (WithInstances model) ()
-> (Actions (ModelState (WithInstances model)) -> Property)
-> Property
forall s a.
(DynLogicModel s, Testable a) =>
Annotated s -> DL s () -> (Actions s -> a) -> Property
DL.forAllUniqueDL Annotated (ModelState (WithInstances model))
ans0 (Action (ModelState (WithInstances model)) SymIndex
-> DL (ModelState (WithInstances model)) (Var SymIndex)
forall a s.
(Typeable a, Eq (Action s a), Show (Action s a)) =>
Action s a -> DL s (Var a)
DL.action (Bool
-> Action (WithInstances model)
-> Action (ModelState (WithInstances model)) SymIndex
forall state.
Bool -> Action state -> Action (ModelState state) SymIndex
ContractAction Bool
False (Action (WithInstances model)
 -> Action (ModelState (WithInstances model)) SymIndex)
-> Action (WithInstances model)
-> Action (ModelState (WithInstances model)) SymIndex
forall a b. (a -> b) -> a -> b
$ Wallet -> Action (WithInstances model)
forall s. Wallet -> Action (WithInstances s)
Unilateral Wallet
w) DL (ModelState (WithInstances model)) (Var SymIndex)
-> 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 SymIndex -> Action s -> Act s)
-> [Var SymIndex] -> [Action s] -> [Act s]
forall a b c. (a -> b -> c) -> [a] -> [b] -> [c]
zipWith Var SymIndex -> Action s -> Act s
forall s. Var SymIndex -> Action s -> Act s
NoBind (Int -> Var SymIndex
forall a. Int -> Var a
StateModel.mkVar (Int -> Var SymIndex) -> [Int] -> [Var SymIndex]
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> [Int
0..])

-- 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) ->
    Annotated (ModelState (WithInstances model))
-> DL (WithInstances model) ()
-> (Actions (WithInstances model) -> Property)
-> Property
forall state p.
(ContractModel state, Testable p) =>
Annotated (ModelState state)
-> DL state () -> (Actions state -> p) -> Property
forAllUniqueDL (Actions (WithInstances model)
-> Annotated (ModelState (WithInstances model))
forall state.
ContractModel state =>
Actions state -> Annotated (ModelState state)
annotatedStateAfter (Actions (WithInstances model)
 -> Annotated (ModelState (WithInstances model)))
-> Actions (WithInstances model)
-> Annotated (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
    run :: Actions (WithInstances model) -> Property
run = CheckOptions
-> CoverageOptions
-> (ModelState (WithInstances model) -> TracePredicate)
-> (ProtocolParameters
    -> ContractModelResult (WithInstances model) -> Property)
-> Actions (WithInstances model)
-> Property
forall state.
CheckableContractModel state =>
CheckOptions
-> CoverageOptions
-> (ModelState (WithInstances state) -> TracePredicate)
-> (ProtocolParameters
    -> ContractModelResult (WithInstances state) -> Property)
-> 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)
                                    ProtocolParameters
-> ContractModelResult (WithInstances model) -> Property
forall state.
ProtocolParameters -> ContractModelResult state -> Property
balanceChangePredicate

-- | A whitelist entry tells you what final log entry prefixes
-- are acceptable for a given error
newtype 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)
-> (ProtocolParameters
    -> ContractModelResult (WithInstances m) -> Property)
-> Actions (WithInstances m)
-> Property
forall state.
CheckableContractModel state =>
CheckOptions
-> CoverageOptions
-> (ModelState (WithInstances state) -> TracePredicate)
-> (ProtocolParameters
    -> ContractModelResult (WithInstances state) -> Property)
-> Actions (WithInstances state)
-> Property
propRunActionsWithOptions CheckOptions
opts CoverageOptions
copts (TracePredicate -> ModelState (WithInstances m) -> TracePredicate
forall a b. a -> b -> a
const TracePredicate
check) ProtocolParameters
-> ContractModelResult (WithInstances m) -> Property
forall state.
ProtocolParameters -> ContractModelResult state -> Property
balanceChangePredicate
  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 = (CardanoTx -> ValidationError -> Bool) -> TracePredicate
assertFailedTransaction (\ CardanoTx
_ 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 | TxnValidation (Index.FailPhase1 CardanoTx
_ (ScriptFailure ScriptError
f)) <- [ChainEvent]
events ]