-- | 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 MultiParamTypeClasses      #-}
{-# LANGUAGE NumericUnderscores         #-}
{-# LANGUAGE OverloadedStrings          #-}
{-# LANGUAGE PatternSynonyms            #-}
{-# LANGUAGE PolyKinds                  #-}
{-# LANGUAGE QuantifiedConstraints      #-}
{-# LANGUAGE RankNTypes                 #-}
{-# LANGUAGE ScopedTypeVariables        #-}
{-# LANGUAGE TemplateHaskell            #-}
{-# LANGUAGE TupleSections              #-}
{-# LANGUAGE TypeApplications           #-}
{-# LANGUAGE TypeFamilies               #-}
{-# LANGUAGE UndecidableInstances       #-}
{-# OPTIONS_GHC -Wno-redundant-constraints -fno-warn-name-shadowing #-}

module Plutus.Contract.Test.ContractModel.Internal
    ( -- * Contract models
      --
      -- $contractModel
      ContractModel(..)
    , HasActions(..)
      -- ** Model state
    , ModelState(..)
    , contractState
    , currentSlot
    , balanceChanges
    , balanceChange
    , minted
    , lockedValue
    , symIsZero
    , GetModelState(..)
    , getContractState
    , askModelState
    , askContractState
    , viewModelState
    , viewContractState
    , SymToken
    , symAssetClassValue
    -- ** The Spec monad
    --
    -- $specMonad
    , Spec(..)
    , wait
    , waitUntil
    , mint
    , burn
    , deposit
    , withdraw
    , transfer
    , modifyContractState
    , createToken
    , assertSpec
    , ($=)
    , ($~)
    , SpecificationEmulatorTrace
    , registerToken
    , delay
    -- * Test scenarios
    --
    -- $dynamicLogic
    , DL
    , action
    , waitUntilDL
    , anyAction
    , anyActions
    , anyActions_

    -- ** Failures
    --
    -- $dynamicLogic_errors
    , DL.assert
    , assertModel
    , stopping
    , weight
    , monitor

    -- * Properties
    --
    -- $runningProperties
    , Actions(..)
    , Act(..)
    , pattern Actions
    , actionsFromList
    -- ** Wallet contract handles
    --
    -- $walletHandles
    , SchemaConstraints
    , ContractInstanceSpec(..)
    , SomeContractInstanceKey(..)
    , StartContract(..)
    , HandleFun
    -- ** Model properties
    , propSanityCheckModel
    , propSanityCheckAssertions
    , propSanityCheckReactive
    -- ** Coverage checking options
    , CoverageOptions
    , defaultCoverageOptions
    , endpointCoverageReq
    , checkCoverage
    , coverageIndex
    , quickCheckWithCoverage
    , quickCheckWithCoverageAndResult
    -- ** Emulator properties
    , propRunActions_
    , propRunActions
    , propRunActionsWithOptions
    , defaultCheckOptionsContractModel
    -- ** DL properties
    , forAllDL
    , forAllDL_
    -- ** Test cases
    --
    -- $testCases
    , DLTest(..)
    , TestStep(..)
    , FailedStep(..)
    , withDLTest

    -- ** Standard properties
    --
    -- $noLockedFunds
    , NoLockedFundsProof(..)
    , defaultNLFP
    , checkNoLockedFundsProof
    , checkNoLockedFundsProofFast
    , NoLockedFundsProofLight(..)
    , checkNoLockedFundsProofLight
    -- $checkNoPartiality
    , Whitelist
    , whitelistOk
    , mkWhitelist
    , errorPrefixes
    , defaultWhitelist
    , checkErrorWhitelist
    , checkErrorWhitelistWithOptions
    ) where

import Control.DeepSeq
import Control.Monad.Freer.Error (Error)
import Plutus.Trace.Effects.Assert (Assert)
import Plutus.Trace.Effects.EmulatedWalletAPI (EmulatedWalletAPI)
import Plutus.Trace.Effects.EmulatorControl (EmulatorControl)
import Plutus.Trace.Effects.RunContract (RunContract)
import Plutus.Trace.Effects.Waiting (Waiting)
import Plutus.Trace.Emulator (initialChainState, waitUntilSlot)
import Plutus.Trace.Emulator.Types (ContractHandle (..), ContractInstanceMsg (..), ContractInstanceTag,
                                    EmulatorRuntimeError (..), UserThreadMsg (..), cilMessage)

import PlutusTx.Prelude qualified as P

import Control.Foldl qualified as L
import Control.Lens
import Control.Monad.Cont
import Control.Monad.Freer (Eff, raise, run)
import Control.Monad.Freer.Extras.Log (LogMessage, LogMsg, logMessageContent)
import Control.Monad.Reader
import Control.Monad.State (MonadState, State)
import Control.Monad.State qualified as State
import Control.Monad.Writer qualified as Writer
import Data.Aeson qualified as JSON
import Data.Data
import Data.Foldable
import Data.IORef
import Data.List
import Data.Map (Map)
import Data.Map qualified as Map
import Data.Maybe
import Data.Row (Row)
import Data.Row.Records (labels')
import Data.Set (Set)
import Data.Set qualified as Set
import Data.Text qualified as Text

import Ledger.Ada qualified as Ada
import Ledger.Index
import Ledger.Slot
import Ledger.Value (AssetClass)
import Plutus.Contract (Contract, ContractError, ContractInstanceId, Endpoint, endpoint)
import Plutus.Contract.Schema (Input)
import Plutus.Contract.Test
import Plutus.Contract.Test.ContractModel.Symbolics
import Plutus.Contract.Test.Coverage
import Plutus.Trace.Effects.EmulatorControl (discardWallets)
import Plutus.Trace.Emulator as Trace (EmulatorTrace, activateContract, callEndpoint, freezeContractInstance,
                                       runEmulatorStream, waitNSlots, walletInstanceTag)
import Plutus.Trace.Emulator.Types (unContractInstanceTag)
import Plutus.V1.Ledger.Scripts
import PlutusTx.Builtins qualified as Builtins
import PlutusTx.Coverage
import PlutusTx.ErrorCodes
import Streaming qualified as S
import Test.QuickCheck.DynamicLogic.Monad qualified as DL
import Test.QuickCheck.StateModel hiding (Action, Actions (..), arbitraryAction, initialState, monitoring, nextState,
                                   pattern Actions, perform, precondition, shrinkAction, stateAfter)
import Test.QuickCheck.StateModel qualified as StateModel

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

import Wallet.Emulator.Chain hiding (_currentSlot, currentSlot)
import Wallet.Emulator.MultiAgent (EmulatorEvent, eteEvent)
import Wallet.Emulator.Stream (EmulatorErr)

import Wallet.Emulator.Folds (postMapM)
import Wallet.Emulator.Folds qualified as Folds

import Control.Monad.Freer.Reader qualified as Freer
import Control.Monad.Freer.Writer (Writer (..), runWriter, tell)
import Data.Void
import Plutus.Contract.Types (IsContract (..))
import Prettyprinter

import Data.Generics.Uniplate.Data (universeBi)

-- | Key-value map where keys and values have three indices that can vary between different elements
--   of the map. Used to store `ContractHandle`s, which are indexed over observable state, schema,
--   and error type.
data IMap (key :: i -> j -> k -> l -> *) (val :: i -> j -> k -> *) where
    IMNil  :: IMap key val
    IMCons :: (Typeable i, Typeable j, Typeable k, Typeable l) => key i j k l -> val i j k -> IMap key val -> IMap key val

-- TODO: Should this make sure we don't duplicate keys?
imAppend :: IMap key val -> IMap key val -> IMap key val
imAppend :: IMap key val -> IMap key val -> IMap key val
imAppend IMap key val
IMNil IMap key val
m           = IMap key val
m
imAppend (IMCons key i j k l
k val i j k
v IMap key val
m) IMap key val
m' = key i j k l -> val i j k -> IMap key val -> IMap key val
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 key i j k l
k val i j k
v (IMap key val -> IMap key val -> IMap key val
forall i j k l (key :: i -> j -> k -> l -> *)
       (val :: i -> j -> k -> *).
IMap key val -> IMap key val -> IMap key val
imAppend IMap key val
m IMap key val
m')

-- | Look up a value in an indexed map. First checks that the indices agree, using `cast`. Once the
--   type checker is convinced that the indices match we can check the key for equality.
imLookup :: (Typeable i, Typeable j, Typeable k, Typeable l, Typeable key, Typeable val, Eq (key i j k l)) => key i j k l -> IMap key val -> Maybe (val i j k)
imLookup :: key i j k l -> IMap key val -> Maybe (val i j k)
imLookup key i j k l
_ IMap key val
IMNil = Maybe (val i j k)
forall a. Maybe a
Nothing
imLookup key i j k l
k (IMCons key i j k l
key val i j k
val IMap key val
m) =
    case (key i j k l, val i j k) -> Maybe (key i j k l, val i j k)
forall a b. (Typeable a, Typeable b) => a -> Maybe b
cast (key i j k l
key, val i j k
val) of
        Just (key i j k l
key', val i j k
val') | key i j k l
key' key i j k l -> key i j k l -> Bool
forall a. Eq a => a -> a -> Bool
== key i j k l
k -> val i j k -> Maybe (val i j k)
forall a. a -> Maybe a
Just val i j k
val'
        Maybe (key i j k l, val i j k)
_                             -> key i j k l -> IMap key val -> Maybe (val i j k)
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, Typeable key,
 Typeable val, Eq (key i j k l)) =>
key i j k l -> IMap key val -> Maybe (val i j k)
imLookup key i j k l
k IMap key val
m

-- $walletHandles
--
-- In order to call contract endpoints using `Plutus.Trace.Emulator.callEndpoint`, a `ContractHandle`
-- is required. Contract handles are managed behind the scenes by the `propRunActions` functions,
-- based on a given a list of `ContractInstanceSpec`s, associating `ContractInstanceKey`s with `Wallet`s and
-- `Contract`s. Before testing starts, `activateContractWallet` is called for all entries in the
-- list and the mapping from `ContractInstanceKey` to `ContractHandle` is provided in the `HandleFun` argument
-- to `perform`.

-- | The constraints required on contract schemas and error types to enable calling contract
--   endpoints (`Plutus.Trace.Emulator.callEndpoint`).
type SchemaConstraints w schema err =
        ( Typeable w
        , Monoid w
        , JSON.ToJSON w
        , Typeable schema
        , ContractConstraints schema
        , Show err
        , Typeable err
        , JSON.ToJSON err
        , JSON.FromJSON err
        , JSON.ToJSON w
        , JSON.FromJSON w
        )

-- | A `ContractInstanceSpec` associates a `ContractInstanceKey` with a concrete `Wallet` and
--   `Contract`. The contract type parameters are hidden from the outside.
data ContractInstanceSpec state where
    ContractInstanceSpec :: (SchemaConstraints w schema err, Typeable params)
                  => ContractInstanceKey state w schema err params -- ^ The key used when looking up contract instance handles in `perform`
                  -> Wallet                                        -- ^ The wallet who owns the contract instance
                  -> Contract w schema err ()                      -- ^ The contract that is running in the instance
                  -> ContractInstanceSpec state

-- TODO: Here be ugly hacks to make the CrashTolerance stuff less ugly. The crash tolerance stuff can be done without this
-- but then I have to write crap myself and I'm not paid enough to suffer that much!
instance (forall w s e p. Show (ContractInstanceKey state w s e p)) => Show (ContractInstanceSpec state) where
  showsPrec :: Int -> ContractInstanceSpec state -> ShowS
showsPrec Int
p (ContractInstanceSpec ContractInstanceKey state w schema err params
key Wallet
w Contract w schema err ()
_) = Bool -> ShowS -> ShowS
showParen (Int
p Int -> Int -> Bool
forall a. Ord a => a -> a -> Bool
>= Int
11) (ShowS -> ShowS) -> ShowS -> ShowS
forall a b. (a -> b) -> a -> b
$ String -> ShowS
showString String
"ConstractInstanceSpec "
                                                                   ShowS -> ShowS -> ShowS
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Int -> ContractInstanceKey state w schema err params -> ShowS
forall a. Show a => Int -> a -> ShowS
showsPrec Int
11 ContractInstanceKey state w schema err params
key
                                                                   ShowS -> ShowS -> ShowS
forall b c a. (b -> c) -> (a -> b) -> a -> c
. String -> ShowS
showString String
" "
                                                                   ShowS -> ShowS -> ShowS
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Int -> Wallet -> ShowS
forall a. Show a => Int -> a -> ShowS
showsPrec Int
11 Wallet
w
                                                                   ShowS -> ShowS -> ShowS
forall b c a. (b -> c) -> (a -> b) -> a -> c
. String -> ShowS
showString String
" <Contract>"

instance (Typeable state, forall w s e p. Eq (ContractInstanceKey state w s e p)) => Eq (ContractInstanceSpec state) where
  ContractInstanceSpec ContractInstanceKey state w schema err params
key Wallet
w Contract w schema err ()
_ == :: ContractInstanceSpec state -> ContractInstanceSpec state -> Bool
== ContractInstanceSpec ContractInstanceKey state w schema err params
key' Wallet
w' Contract w schema err ()
_ = Wallet
w Wallet -> Wallet -> Bool
forall a. Eq a => a -> a -> Bool
== Wallet
w' Bool -> Bool -> Bool
&& ContractInstanceKey state w schema err params
-> Maybe (ContractInstanceKey state w schema err params)
forall a b. (Typeable a, Typeable b) => a -> Maybe b
cast ContractInstanceKey state w schema err params
key Maybe (ContractInstanceKey state w schema err params)
-> Maybe (ContractInstanceKey state w schema err params) -> Bool
forall a. Eq a => a -> a -> Bool
== ContractInstanceKey state w schema err params
-> Maybe (ContractInstanceKey state w schema err params)
forall a. a -> Maybe a
Just ContractInstanceKey state w schema err params
key'

data WalletContractHandle w s e = WalletContractHandle Wallet (ContractHandle w s e)

type Handles state = IMap (ContractInstanceKey state) WalletContractHandle

handlesAppend :: Handles state -> Handles state -> Handles state
handlesAppend :: Handles state -> Handles state -> Handles state
handlesAppend = Handles state -> Handles state -> Handles state
forall i j k l (key :: i -> j -> k -> l -> *)
       (val :: i -> j -> k -> *).
IMap key val -> IMap key val -> IMap key val
imAppend

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

activateWallets :: forall state. ContractModel state => (SymToken -> AssetClass) -> [StartContract state] -> EmulatorTrace (Handles state)
activateWallets :: (SymToken -> AssetClass)
-> [StartContract state] -> EmulatorTrace (Handles state)
activateWallets SymToken -> AssetClass
_ [] = Handles state -> EmulatorTrace (Handles state)
forall (m :: * -> *) a. Monad m => a -> m a
return Handles state
forall i j k l (key :: i -> j -> k -> l -> *)
       (val :: i -> j -> k -> *).
IMap key val
IMNil
activateWallets SymToken -> AssetClass
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.
ContractModel 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
     '[StartContract, RunContract, Assert, Waiting, EmulatorControl,
       EmulatedWalletAPI, LogMsg String, Error EmulatorRuntimeError]
     (ContractHandle w s e)
forall (contract :: * -> Row * -> * -> * -> *) (s :: Row *) e w a
       (effs :: [* -> *]).
(IsContract contract, ContractConstraints s, Show e, FromJSON e,
 ToJSON e, ToJSON w, Monoid w, FromJSON w,
 Member StartContract effs) =>
Wallet
-> contract w s e a
-> ContractInstanceTag
-> Eff effs (ContractHandle w s e)
activateContract Wallet
wallet ((SymToken -> AssetClass)
-> ContractInstanceKey state w s e p -> p -> Contract w s e ()
forall state w (s :: Row *) e p.
ContractModel state =>
(SymToken -> AssetClass)
-> ContractInstanceKey state w s e p -> p -> Contract w s e ()
instanceContract SymToken -> AssetClass
sa ContractInstanceKey state w s e p
key p
params) (ContractInstanceKey state w s e p -> ContractInstanceTag
forall state w (s :: Row *) e p.
(ContractModel state, SchemaConstraints w s e) =>
ContractInstanceKey state w s e p -> ContractInstanceTag
instanceTag ContractInstanceKey state w s e p
key)
    Handles state
m <- (SymToken -> AssetClass)
-> [StartContract state] -> EmulatorTrace (Handles state)
forall state.
ContractModel state =>
(SymToken -> AssetClass)
-> [StartContract state] -> EmulatorTrace (Handles state)
activateWallets SymToken -> AssetClass
sa [StartContract state]
starts
    Handles state -> EmulatorTrace (Handles state)
forall (m :: * -> *) a. Monad m => a -> m a
return (Handles state -> EmulatorTrace (Handles state))
-> Handles state -> EmulatorTrace (Handles 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) Handles state
m

-- | A function returning the `ContractHandle` corresponding to a `ContractInstanceKey`. A
--   `HandleFun` is provided to the `perform` function to enable calling contract endpoints with
--   `Plutus.Trace.Emulator.callEndpoint`.
type HandleFun state = forall w schema err params. (Typeable w, Typeable schema, Typeable err, Typeable params) => ContractInstanceKey state w schema err params -> ContractHandle w schema err

-- | The `ModelState` models the state of the blockchain. It contains,
--
--   * the contract-specific state (`contractState`)
--   * the current slot (`currentSlot`)
--   * the wallet balances (`balances`)
--   * the amount that has been minted (`minted`)
data ModelState state = ModelState
        { ModelState state -> Slot
_currentSlot    :: Slot
        , ModelState state -> Map Wallet SymValue
_balanceChanges :: Map Wallet SymValue
        , ModelState state -> SymValue
_minted         :: SymValue
        , ModelState state -> Set SymToken
_symTokens      :: Set SymToken
        , ModelState state -> [(String, Bool)]
_assertions     :: [(String, Bool)]
        , ModelState state -> Bool
_assertionsOk   :: Bool
        , ModelState state -> state
_contractState  :: state
        }
  deriving (Int -> ModelState state -> ShowS
[ModelState state] -> ShowS
ModelState state -> String
(Int -> ModelState state -> ShowS)
-> (ModelState state -> String)
-> ([ModelState state] -> ShowS)
-> Show (ModelState state)
forall state. Show state => Int -> ModelState state -> ShowS
forall state. Show state => [ModelState state] -> ShowS
forall state. Show state => ModelState state -> String
forall a.
(Int -> a -> ShowS) -> (a -> String) -> ([a] -> ShowS) -> Show a
showList :: [ModelState state] -> ShowS
$cshowList :: forall state. Show state => [ModelState state] -> ShowS
show :: ModelState state -> String
$cshow :: forall state. Show state => ModelState state -> String
showsPrec :: Int -> ModelState state -> ShowS
$cshowsPrec :: forall state. Show state => Int -> ModelState state -> ShowS
Show)

instance Functor ModelState where
  fmap :: (a -> b) -> ModelState a -> ModelState b
fmap a -> b
f ModelState a
m = ModelState a
m { _contractState :: b
_contractState = a -> b
f (ModelState a -> a
forall state. ModelState state -> state
_contractState ModelState a
m) }

dummyModelState :: state -> ModelState state
dummyModelState :: state -> ModelState state
dummyModelState state
s = Slot
-> Map Wallet SymValue
-> SymValue
-> Set SymToken
-> [(String, Bool)]
-> Bool
-> state
-> ModelState state
forall state.
Slot
-> Map Wallet SymValue
-> SymValue
-> Set SymToken
-> [(String, Bool)]
-> Bool
-> state
-> ModelState state
ModelState Slot
1 Map Wallet SymValue
forall k a. Map k a
Map.empty SymValue
forall a. Monoid a => a
mempty Set SymToken
forall a. Monoid a => a
mempty [(String, Bool)]
forall a. Monoid a => a
mempty Bool
True state
s

-- | The `Spec` monad is a state monad over the `ModelState` with reader and writer components to keep track
--   of newly created symbolic tokens. It is used exclusively by the `nextState` function to model the effects
--   of an action on the blockchain.
newtype Spec state a = Spec { Spec state a
-> WriterT
     [SymToken] (ReaderT (Var AssetKey) (State (ModelState state))) a
unSpec :: Writer.WriterT [SymToken] (ReaderT (Var AssetKey) (State (ModelState state))) a }
    deriving (a -> Spec state b -> Spec state a
(a -> b) -> Spec state a -> Spec state b
(forall a b. (a -> b) -> Spec state a -> Spec state b)
-> (forall a b. a -> Spec state b -> Spec state a)
-> Functor (Spec state)
forall a b. a -> Spec state b -> Spec state a
forall a b. (a -> b) -> Spec state a -> Spec state b
forall state a b. a -> Spec state b -> Spec state a
forall state a b. (a -> b) -> Spec state a -> Spec state b
forall (f :: * -> *).
(forall a b. (a -> b) -> f a -> f b)
-> (forall a b. a -> f b -> f a) -> Functor f
<$ :: a -> Spec state b -> Spec state a
$c<$ :: forall state a b. a -> Spec state b -> Spec state a
fmap :: (a -> b) -> Spec state a -> Spec state b
$cfmap :: forall state a b. (a -> b) -> Spec state a -> Spec state b
Functor, Functor (Spec state)
a -> Spec state a
Functor (Spec state)
-> (forall a. a -> Spec state a)
-> (forall a b.
    Spec state (a -> b) -> Spec state a -> Spec state b)
-> (forall a b c.
    (a -> b -> c) -> Spec state a -> Spec state b -> Spec state c)
-> (forall a b. Spec state a -> Spec state b -> Spec state b)
-> (forall a b. Spec state a -> Spec state b -> Spec state a)
-> Applicative (Spec state)
Spec state a -> Spec state b -> Spec state b
Spec state a -> Spec state b -> Spec state a
Spec state (a -> b) -> Spec state a -> Spec state b
(a -> b -> c) -> Spec state a -> Spec state b -> Spec state c
forall state. Functor (Spec state)
forall a. a -> Spec state a
forall state a. a -> Spec state a
forall a b. Spec state a -> Spec state b -> Spec state a
forall a b. Spec state a -> Spec state b -> Spec state b
forall a b. Spec state (a -> b) -> Spec state a -> Spec state b
forall state a b. Spec state a -> Spec state b -> Spec state a
forall state a b. Spec state a -> Spec state b -> Spec state b
forall state a b.
Spec state (a -> b) -> Spec state a -> Spec state b
forall a b c.
(a -> b -> c) -> Spec state a -> Spec state b -> Spec state c
forall state a b c.
(a -> b -> c) -> Spec state a -> Spec state b -> Spec state c
forall (f :: * -> *).
Functor f
-> (forall a. a -> f a)
-> (forall a b. f (a -> b) -> f a -> f b)
-> (forall a b c. (a -> b -> c) -> f a -> f b -> f c)
-> (forall a b. f a -> f b -> f b)
-> (forall a b. f a -> f b -> f a)
-> Applicative f
<* :: Spec state a -> Spec state b -> Spec state a
$c<* :: forall state a b. Spec state a -> Spec state b -> Spec state a
*> :: Spec state a -> Spec state b -> Spec state b
$c*> :: forall state a b. Spec state a -> Spec state b -> Spec state b
liftA2 :: (a -> b -> c) -> Spec state a -> Spec state b -> Spec state c
$cliftA2 :: forall state a b c.
(a -> b -> c) -> Spec state a -> Spec state b -> Spec state c
<*> :: Spec state (a -> b) -> Spec state a -> Spec state b
$c<*> :: forall state a b.
Spec state (a -> b) -> Spec state a -> Spec state b
pure :: a -> Spec state a
$cpure :: forall state a. a -> Spec state a
$cp1Applicative :: forall state. Functor (Spec state)
Applicative, Applicative (Spec state)
a -> Spec state a
Applicative (Spec state)
-> (forall a b.
    Spec state a -> (a -> Spec state b) -> Spec state b)
-> (forall a b. Spec state a -> Spec state b -> Spec state b)
-> (forall a. a -> Spec state a)
-> Monad (Spec state)
Spec state a -> (a -> Spec state b) -> Spec state b
Spec state a -> Spec state b -> Spec state b
forall state. Applicative (Spec state)
forall a. a -> Spec state a
forall state a. a -> Spec state a
forall a b. Spec state a -> Spec state b -> Spec state b
forall a b. Spec state a -> (a -> Spec state b) -> Spec state b
forall state a b. Spec state a -> Spec state b -> Spec state b
forall state a b.
Spec state a -> (a -> Spec state b) -> Spec state b
forall (m :: * -> *).
Applicative m
-> (forall a b. m a -> (a -> m b) -> m b)
-> (forall a b. m a -> m b -> m b)
-> (forall a. a -> m a)
-> Monad m
return :: a -> Spec state a
$creturn :: forall state a. a -> Spec state a
>> :: Spec state a -> Spec state b -> Spec state b
$c>> :: forall state a b. Spec state a -> Spec state b -> Spec state b
>>= :: Spec state a -> (a -> Spec state b) -> Spec state b
$c>>= :: forall state a b.
Spec state a -> (a -> Spec state b) -> Spec state b
$cp1Monad :: forall state. Applicative (Spec state)
Monad)

instance MonadState state (Spec state) where
    state :: (state -> (a, state)) -> Spec state a
state state -> (a, state)
f = WriterT
  [SymToken] (ReaderT (Var AssetKey) (State (ModelState state))) a
-> Spec state a
forall state a.
WriterT
  [SymToken] (ReaderT (Var AssetKey) (State (ModelState state))) a
-> Spec state a
Spec (WriterT
   [SymToken] (ReaderT (Var AssetKey) (State (ModelState state))) a
 -> Spec state a)
-> WriterT
     [SymToken] (ReaderT (Var AssetKey) (State (ModelState state))) a
-> Spec state a
forall a b. (a -> b) -> a -> b
$ (ModelState state -> (a, ModelState state))
-> WriterT
     [SymToken] (ReaderT (Var AssetKey) (State (ModelState state))) a
forall s (m :: * -> *) a. MonadState s m => (s -> (a, s)) -> m a
State.state ((ModelState state -> (a, ModelState state))
 -> WriterT
      [SymToken] (ReaderT (Var AssetKey) (State (ModelState state))) a)
-> (ModelState state -> (a, ModelState state))
-> WriterT
     [SymToken] (ReaderT (Var AssetKey) (State (ModelState state))) a
forall a b. (a -> b) -> a -> b
$ \ModelState state
s -> case state -> (a, state)
f (ModelState state -> state
forall state. ModelState state -> state
_contractState ModelState state
s) of
        (a
a, state
cs) -> (a
a, ModelState state
s { _contractState :: state
_contractState = state
cs })
    {-# INLINE state #-}

    get :: Spec state state
get = WriterT
  [SymToken]
  (ReaderT (Var AssetKey) (State (ModelState state)))
  state
-> Spec state state
forall state a.
WriterT
  [SymToken] (ReaderT (Var AssetKey) (State (ModelState state))) a
-> Spec state a
Spec (WriterT
   [SymToken]
   (ReaderT (Var AssetKey) (State (ModelState state)))
   state
 -> Spec state state)
-> WriterT
     [SymToken]
     (ReaderT (Var AssetKey) (State (ModelState state)))
     state
-> Spec state state
forall a b. (a -> b) -> a -> b
$ (ModelState state -> state)
-> WriterT
     [SymToken]
     (ReaderT (Var AssetKey) (State (ModelState state)))
     (ModelState state)
-> WriterT
     [SymToken]
     (ReaderT (Var AssetKey) (State (ModelState state)))
     state
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap ModelState state -> state
forall state. ModelState state -> state
_contractState WriterT
  [SymToken]
  (ReaderT (Var AssetKey) (State (ModelState state)))
  (ModelState state)
forall s (m :: * -> *). MonadState s m => m s
State.get
    {-# INLINE get #-}

    put :: state -> Spec state ()
put state
cs = WriterT
  [SymToken] (ReaderT (Var AssetKey) (State (ModelState state))) ()
-> Spec state ()
forall state a.
WriterT
  [SymToken] (ReaderT (Var AssetKey) (State (ModelState state))) a
-> Spec state a
Spec (WriterT
   [SymToken] (ReaderT (Var AssetKey) (State (ModelState state))) ()
 -> Spec state ())
-> WriterT
     [SymToken] (ReaderT (Var AssetKey) (State (ModelState state))) ()
-> Spec state ()
forall a b. (a -> b) -> a -> b
$ (ModelState state -> ModelState state)
-> WriterT
     [SymToken] (ReaderT (Var AssetKey) (State (ModelState state))) ()
forall s (m :: * -> *). MonadState s m => (s -> s) -> m ()
State.modify' ((ModelState state -> ModelState state)
 -> WriterT
      [SymToken] (ReaderT (Var AssetKey) (State (ModelState state))) ())
-> (ModelState state -> ModelState state)
-> WriterT
     [SymToken] (ReaderT (Var AssetKey) (State (ModelState state))) ()
forall a b. (a -> b) -> a -> b
$ \ModelState state
s -> ModelState state
s { _contractState :: state
_contractState = state
cs }
    {-# INLINE put #-}

data SomeContractInstanceKey state where
  Key :: (SchemaConstraints w s e, Typeable p) => ContractInstanceKey state w s e p -> SomeContractInstanceKey state

data StartContract state where
  StartContract :: (SchemaConstraints w s e, Typeable p) => ContractInstanceKey state w s e p -> p -> StartContract state

instance ContractModel state => Eq (SomeContractInstanceKey state) where
  Key ContractInstanceKey state w s e p
k == :: SomeContractInstanceKey state
-> SomeContractInstanceKey state -> Bool
== Key ContractInstanceKey state w s e p
k' = ContractInstanceKey state w s e p
-> Maybe (ContractInstanceKey state w s e p)
forall a. a -> Maybe a
Just ContractInstanceKey state w s e p
k Maybe (ContractInstanceKey state w s e p)
-> Maybe (ContractInstanceKey state w s e p) -> Bool
forall a. Eq a => a -> a -> Bool
== ContractInstanceKey state w s e p
-> Maybe (ContractInstanceKey state w s e p)
forall a b. (Typeable a, Typeable b) => a -> Maybe b
cast ContractInstanceKey state w s e p
k'

instance ContractModel state => Show (SomeContractInstanceKey state) where
  showsPrec :: Int -> SomeContractInstanceKey state -> ShowS
showsPrec Int
d (Key ContractInstanceKey state w s e p
k) = Int -> ContractInstanceKey state w s e p -> ShowS
forall a. Show a => Int -> a -> ShowS
showsPrec Int
d ContractInstanceKey state w s e p
k

type SpecificationEmulatorTrace a =
        Eff '[ Writer [(String, AssetClass)]
             , RunContract
             , Assert
             , Waiting
             , EmulatorControl
             , EmulatedWalletAPI
             , LogMsg String
             , Error EmulatorRuntimeError
             ] a

-- $contractModel
--
-- A contract model is a type @state@ with a `ContractModel` instance. The state type should
-- capture an abstraction of the state of the blockchain relevant to the contract (or contracts)
-- under test. During test generation and execution, the contract-specific @state@ is wrapped in the
-- `ModelState` type, which in addition to @state@ tracks common features of the blockchain, like
-- wallet balances and the current slot.

class (Eq (Action state), Show (Action state)) => HasActions state where
  getAllSymtokens :: Action state -> Set SymToken

instance {-# OVERLAPPABLE #-} (Eq (Action state), Show (Action state), Data (Action state)) => HasActions state where
  getAllSymtokens :: Action state -> Set SymToken
getAllSymtokens = [SymToken] -> Set SymToken
forall a. Ord a => [a] -> Set a
Set.fromList ([SymToken] -> Set SymToken)
-> (Action state -> [SymToken]) -> Action state -> Set SymToken
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Action state -> [SymToken]
forall from to. Biplate from to => from -> [to]
universeBi

-- | A `ContractModel` instance captures everything that is needed to generate and run tests of a
--   contract or set of contracts. It specifies among other things
--
--  * what operations are supported by the contract (`Action`),
--  * when they are valid (`precondition`),
--  * how to generate random actions (`arbitraryAction`),
--  * how the operations affect the state (`nextState`), and
--  * how to run the operations in the emulator (`perform`)

class ( Typeable state
      , Show state
      , HasActions state
      , (forall w s e p. Eq (ContractInstanceKey state w s e p))
      , (forall w s e p. Show (ContractInstanceKey state w s e p))
      ) => ContractModel state where

    -- | The type of actions that are supported by the contract. An action usually represents a single
    --   `Plutus.Trace.Emulator.callEndpoint` or a transfer of tokens, but it can be anything
    --   that can be interpreted in the `EmulatorTrace` monad.
    data Action state

    -- | To be able to call a contract endpoint from a wallet a `ContractHandle` is required. These
    --   are managed by the test framework and all the user needs to do is provide this contract
    --   instance key type representing the different contract instances that a test needs to work
    --   with, and when creating a property (see `propRunActions_`) provide a list of contract
    --   instance keys together with their wallets and contracts (a `ContractInstanceSpec`).
    --   Contract instance keys are indexed by the observable state, schema, and error type of the
    --   contract and should be defined as a GADT. For example, a handle type for a contract with
    --   one seller and multiple buyers could look like this.
    --
    --   >  data ContractInstanceKey MyModel w s e where
    --   >      Buyer  :: Wallet -> ContractInstanceKey MyModel MyObsState MySchema MyError MyParams
    --   >      Seller :: ContractInstanceKey MyModel MyObsState MySchema MyError MyParams
    data ContractInstanceKey state :: * -> Row * -> * -> * -> *

    -- | Get the wallet that the contract running at a specific `ContractInstanceKey` should run
    -- in
    instanceWallet :: ContractInstanceKey state w s e p -> Wallet

    -- | The 'ContractInstanceTag' of an instance key for a wallet. Defaults to 'walletInstanceTag'.
    --   You must override this if you have multiple instances per wallet.
    instanceTag :: forall w s e p. SchemaConstraints w s e => ContractInstanceKey state w s e p -> ContractInstanceTag
    instanceTag = Wallet -> ContractInstanceTag
walletInstanceTag (Wallet -> ContractInstanceTag)
-> (ContractInstanceKey state w s e p -> Wallet)
-> ContractInstanceKey state w s e p
-> ContractInstanceTag
forall b c a. (b -> c) -> (a -> b) -> a -> c
. ContractInstanceKey state w s e p -> Wallet
forall state w (s :: Row *) e p.
ContractModel state =>
ContractInstanceKey state w s e p -> Wallet
instanceWallet

    -- | Given the current model state, provide a QuickCheck generator for a random next action.
    --   This is used in the `Arbitrary` instance for `Actions`s as well as by `anyAction` and
    --   `anyActions`.
    arbitraryAction :: ModelState state -> Gen (Action state)

    -- | The probability that we will generate a `WaitUntil` in a given state
    waitProbability :: ModelState state -> Double
    waitProbability ModelState state
_ = Double
0.1

    -- | Control the distribution of how long `WaitUntil` waits
    arbitraryWaitInterval :: ModelState state -> Gen Slot
    arbitraryWaitInterval ModelState state
s = Integer -> Slot
Slot (Integer -> Slot) -> Gen Integer -> Gen Slot
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> (Integer, Integer) -> Gen Integer
forall a. Random a => (a, a) -> Gen a
choose (Integer
1,Integer -> Integer -> Integer
forall a. Ord a => a -> a -> a
max Integer
10 ([Integer] -> Integer
forall a. [a] -> a
head [ Integer
5Integer -> Integer -> Integer
forall a. Num a => a -> a -> a
*(Integer
kInteger -> Integer -> Integer
forall a. Num a => a -> a -> a
-Integer
1) | Integer
k <- [Integer
0..], Integer
2Integer -> Integer -> Integer
forall a b. (Num a, Integral b) => a -> b -> a
^Integer
k Integer -> Integer -> Bool
forall a. Ord a => a -> a -> Bool
> Integer
n]))
      where
        Slot Integer
n = ModelState state -> Slot
forall state. ModelState state -> Slot
_currentSlot ModelState state
s

    -- | The initial state, before any actions have been performed.
    initialState :: state

    -- | The initial handles
    initialInstances :: [StartContract state]

    -- | The `precondition` function decides if a given action is valid in a given state. Typically
    --   actions generated by `arbitraryAction` will satisfy the precondition, but if they don't
    --   they will be discarded and another action will be generated. More importantly, the
    --   preconditions are used when shrinking (see `shrinkAction`) to ensure that shrunk test cases
    --   still make sense.
    --
    --   If an explicit `action` in a `DL` scenario violates the precondition an error is raised.
    precondition :: ModelState state -> Action state -> Bool
    precondition ModelState state
_ Action state
_ = Bool
True

    -- | `nextReactiveState` is run every time the model `wait`s for a slot to be reached. This
    --   can be used to model reactive components of off-chain code.
    nextReactiveState :: Slot -> Spec state ()
    nextReactiveState Slot
_ = () -> Spec state ()
forall (m :: * -> *) a. Monad m => a -> m a
return ()

    -- | This is where the model logic is defined. Given an action, `nextState` specifies the
    --   effects running that action has on the model state. It runs in the `Spec` monad, which is a
    --   state monad over the `ModelState`.
    nextState :: Action state -> Spec state ()

    -- | Start new contract instances
    startInstances :: ModelState state
                   -> Action state
                   -> [StartContract state]
    startInstances ModelState state
_ Action state
_ = []

    -- | Map a `ContractInstanceKey` `k` to the `Contract` that is started when we start
    -- `k` in a given `ModelState` with a given semantics of `SymToken`s
    instanceContract :: (SymToken -> AssetClass)
                     -> ContractInstanceKey state w s e p
                     -> p
                     -> Contract w s e ()

    -- | While `nextState` models the behaviour of the actions, `perform` contains the code for
    --   running the actions in the emulator (see "Plutus.Trace.Emulator"). It gets access to the
    --   wallet contract handles, the current model state, and the action to be performed.
    perform :: HandleFun state  -- ^ Function from `ContractInstanceKey` to `ContractHandle`
            -> (SymToken -> AssetClass) -- ^ Map from symbolic tokens (that may appear in actions or the state)
                                        -- to assset class of actual blockchain token
            -> ModelState state -- ^ The model state before peforming the action
            -> Action state     -- ^ The action to perform
            -> SpecificationEmulatorTrace ()

    -- | When a test involving random sequences of actions fails, the framework tries to find a
    --   minimal failing test case by shrinking the original failure. Action sequences are shrunk by
    --   removing individual actions, or by replacing an action by one of the (simpler) actions
    --   returned by `shrinkAction`.
    --
    --   See `Test.QuickCheck.shrink` for more information on shrinking.
    shrinkAction :: ModelState state -> Action state -> [Action state]
    shrinkAction ModelState state
_ Action state
_ = []

    -- | The `monitoring` function allows you to collect statistics of your testing using QuickCheck
    --   functions like `Test.QuickCheck.label`, `Test.QuickCheck.collect`,
    --   `Test.QuickCheck.classify`, and `Test.QuickCheck.tabulate`. This function is called by
    --   `propRunActions` (and friends) for any actions in the given `Actions`.
    --
    --   Statistics on which actions are executed are always collected.
    monitoring :: (ModelState state, ModelState state)  -- ^ Model state before and after the action
               -> Action state                          -- ^ The action that was performed
               -> Property -> Property
    monitoring (ModelState state, ModelState state)
_ Action state
_ = Property -> Property
forall a. a -> a
id

    -- | In some scenarios it's useful to have actions that are never generated randomly, but only
    --   used explicitly in `DL` scenario `action`s. To avoid these actions matching an `anyAction`
    --   when shrinking, they can be marked `restricted`.
    restricted :: Action state -> Bool
    restricted Action state
_ = Bool
False

-- | Lens for the contract-specific part of the model state.
--
--   `Spec` monad update functions: `$=` and `$~`.
makeLensesFor [("_contractState",  "contractState")]   'ModelState
makeLensesFor [("_currentSlot",    "currentSlotL")]    'ModelState
makeLensesFor [("_lastSlot",       "lastSlotL")]       'ModelState
makeLensesFor [("_balanceChanges", "balanceChangesL")] 'ModelState
makeLensesFor [("_minted",         "mintedL")]         'ModelState
makeLensesFor [("_tokenNameIndex", "tokenNameIndex")]  'ModelState
makeLensesFor [("_assertions", "assertions")]          'ModelState
makeLensesFor [("_assertionsOk", "assertionsOk")]      'ModelState
makeLensesFor [("_symTokens", "symTokens")]            'ModelState

-- | Get the current slot.
--
--   `Spec` monad update functions: `wait` and `waitUntil`.
currentSlot :: Getter (ModelState state) Slot
currentSlot :: (Slot -> f Slot) -> ModelState state -> f (ModelState state)
currentSlot = (Slot -> f Slot) -> ModelState state -> f (ModelState state)
forall state. Lens' (ModelState state) Slot
currentSlotL

-- | Get the current wallet balance changes. These are delta balances, so they start out at zero and
--   can be negative. The absolute balances used by the emulator can be set in the `CheckOptions`
--   argument to `propRunActionsWithOptions`.
--
--   `Spec` monad update functions: `withdraw`, `deposit`, `transfer`.
balanceChanges :: Getter (ModelState state) (Map Wallet SymValue)
balanceChanges :: (Map Wallet SymValue -> f (Map Wallet SymValue))
-> ModelState state -> f (ModelState state)
balanceChanges = (Map Wallet SymValue -> f (Map Wallet SymValue))
-> ModelState state -> f (ModelState state)
forall state. Lens' (ModelState state) (Map Wallet SymValue)
balanceChangesL

-- | Get the current balance change for a wallet. This is the delta balance, so it starts out at zero and
--   can be negative. The absolute balance used by the emulator can be set in the `CheckOptions`
--   argument to `propRunActionsWithOptions`.
--
--   `Spec` monad update functions: `withdraw`, `deposit`, `transfer`.
balanceChange :: Wallet -> Getter (ModelState state) SymValue
balanceChange :: Wallet -> Getter (ModelState state) SymValue
balanceChange Wallet
w = (Map Wallet SymValue -> f (Map Wallet SymValue))
-> ModelState state -> f (ModelState state)
forall state. Lens' (ModelState state) (Map Wallet SymValue)
balanceChangesL ((Map Wallet SymValue -> f (Map Wallet SymValue))
 -> ModelState state -> f (ModelState state))
-> ((SymValue -> f SymValue)
    -> Map Wallet SymValue -> f (Map Wallet SymValue))
-> (SymValue -> f SymValue)
-> ModelState state
-> f (ModelState state)
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Index (Map Wallet SymValue)
-> Lens'
     (Map Wallet SymValue) (Maybe (IxValue (Map Wallet SymValue)))
forall m. At m => Index m -> Lens' m (Maybe (IxValue m))
at Index (Map Wallet SymValue)
Wallet
w ((Maybe SymValue -> f (Maybe SymValue))
 -> Map Wallet SymValue -> f (Map Wallet SymValue))
-> ((SymValue -> f SymValue)
    -> Maybe SymValue -> f (Maybe SymValue))
-> (SymValue -> f SymValue)
-> Map Wallet SymValue
-> f (Map Wallet SymValue)
forall b c a. (b -> c) -> (a -> b) -> a -> c
. SymValue -> Iso' (Maybe SymValue) SymValue
forall a. Eq a => a -> Iso' (Maybe a) a
non SymValue
forall a. Monoid a => a
mempty

-- | Get the amount of tokens minted so far. This is used to compute `lockedValue`.
--
--   `Spec` monad update functions: `mint` and `burn`.
minted :: Getter (ModelState state) SymValue
minted :: (SymValue -> f SymValue)
-> ModelState state -> f (ModelState state)
minted = (SymValue -> f SymValue)
-> ModelState state -> f (ModelState state)
forall state. Lens' (ModelState state) SymValue
mintedL

-- | How much value is currently locked by contracts. This computed by subtracting the wallet
--   `balances` from the `minted` value.
lockedValue :: ModelState s -> SymValue
lockedValue :: ModelState s -> SymValue
lockedValue ModelState s
s = ModelState s
s ModelState s
-> Getting SymValue (ModelState s) SymValue -> SymValue
forall s a. s -> Getting a s a -> a
^. Getting SymValue (ModelState s) SymValue
forall state. Getter (ModelState state) SymValue
minted SymValue -> SymValue -> SymValue
forall a. Semigroup a => a -> a -> a
<> SymValue -> SymValue
inv (Map Wallet SymValue -> SymValue
forall (t :: * -> *) m. (Foldable t, Monoid m) => t m -> m
fold (Map Wallet SymValue -> SymValue)
-> Map Wallet SymValue -> SymValue
forall a b. (a -> b) -> a -> b
$ ModelState s
s ModelState s
-> Getting
     (Map Wallet SymValue) (ModelState s) (Map Wallet SymValue)
-> Map Wallet SymValue
forall s a. s -> Getting a s a -> a
^. Getting (Map Wallet SymValue) (ModelState s) (Map Wallet SymValue)
forall state. Getter (ModelState state) (Map Wallet SymValue)
balanceChanges)

-- | Monads with read access to the model state: the `Spec` monad used in `nextState`, and the `DL`
--   monad used to construct test scenarios.
class Monad m => GetModelState m where
    -- | The contract state type of the monad. For both `Spec` and `DL` this is simply the @state@
    --   parameter of the respective monad.
    type StateType m :: *

    -- | Get the current model state.
    getModelState :: m (ModelState (StateType m))

-- | Get the contract state part of the model state.
getContractState :: GetModelState m => m (StateType m)
getContractState :: m (StateType m)
getContractState = ModelState (StateType m) -> StateType m
forall state. ModelState state -> state
_contractState (ModelState (StateType m) -> StateType m)
-> m (ModelState (StateType m)) -> m (StateType m)
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> m (ModelState (StateType m))
forall (m :: * -> *).
GetModelState m =>
m (ModelState (StateType m))
getModelState

-- | Get a component of the model state.
askModelState :: GetModelState m => (ModelState (StateType m) -> a) -> m a
askModelState :: (ModelState (StateType m) -> a) -> m a
askModelState ModelState (StateType m) -> a
f = ModelState (StateType m) -> a
f (ModelState (StateType m) -> a)
-> m (ModelState (StateType m)) -> m a
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> m (ModelState (StateType m))
forall (m :: * -> *).
GetModelState m =>
m (ModelState (StateType m))
getModelState

-- | Get a component of the contract state.
askContractState :: GetModelState m => (StateType m -> a) -> m a
askContractState :: (StateType m -> a) -> m a
askContractState StateType m -> a
f = (ModelState (StateType m) -> a) -> m a
forall (m :: * -> *) a.
GetModelState m =>
(ModelState (StateType m) -> a) -> m a
askModelState (StateType m -> a
f (StateType m -> a)
-> (ModelState (StateType m) -> StateType m)
-> ModelState (StateType m)
-> a
forall b c a. (b -> c) -> (a -> b) -> a -> c
. ModelState (StateType m) -> StateType m
forall state. ModelState state -> state
_contractState)

-- | Get a component of the model state using a lens.
viewModelState :: GetModelState m => Getting a (ModelState (StateType m)) a -> m a
viewModelState :: Getting a (ModelState (StateType m)) a -> m a
viewModelState Getting a (ModelState (StateType m)) a
l = (ModelState (StateType m) -> a) -> m a
forall (m :: * -> *) a.
GetModelState m =>
(ModelState (StateType m) -> a) -> m a
askModelState (ModelState (StateType m)
-> Getting a (ModelState (StateType m)) a -> a
forall s a. s -> Getting a s a -> a
^. Getting a (ModelState (StateType m)) a
l)

-- | Get a component of the contract state using a lens.
viewContractState :: GetModelState m => Getting a (StateType m) a -> m a
viewContractState :: Getting a (StateType m) a -> m a
viewContractState Getting a (StateType m) a
l = Getting a (ModelState (StateType m)) a -> m a
forall (m :: * -> *) a.
GetModelState m =>
Getting a (ModelState (StateType m)) a -> m a
viewModelState ((StateType m -> Const a (StateType m))
-> ModelState (StateType m) -> Const a (ModelState (StateType m))
forall state state.
Lens (ModelState state) (ModelState state) state state
contractState ((StateType m -> Const a (StateType m))
 -> ModelState (StateType m) -> Const a (ModelState (StateType m)))
-> Getting a (StateType m) a
-> Getting a (ModelState (StateType m)) a
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Getting a (StateType m) a
l)

-- $specMonad
--
-- The `Spec` monad is used in the `nextState` function to specify how the model state is affected
-- by each action.
--
-- Note that the model state does not track the absolute `balances` of each wallet, only how the
-- balance changes over the execution of a contract. Thus, token transfers (using `transfer`,
-- `deposit` or `withdraw`) always succeed in the model, but might fail when running the
-- contract in the emulator, causing test failures. The simplest way to deal with this is
-- to make sure that each wallet has enough starting funds to cover any scenario encountered during
-- testing. The starting funds can be provided in the `CheckOptions` argument to
-- `propRunActionsWithOptions`.
-- Another option is to model the starting funds of each contract in the contract state and check
-- that enough funds are available before performing a transfer.

runSpec :: Spec state ()
        -> Var AssetKey
        -> ModelState state
        -> ModelState state
runSpec :: Spec state ()
-> Var AssetKey -> ModelState state -> ModelState state
runSpec (Spec WriterT
  [SymToken] (ReaderT (Var AssetKey) (State (ModelState state))) ()
spec) Var AssetKey
v ModelState state
s = (State (ModelState state) ()
 -> ModelState state -> ModelState state)
-> ModelState state
-> State (ModelState state) ()
-> ModelState state
forall a b c. (a -> b -> c) -> b -> a -> c
flip State (ModelState state) () -> ModelState state -> ModelState state
forall s a. State s a -> s -> s
State.execState ModelState state
s (State (ModelState state) () -> ModelState state)
-> State (ModelState state) () -> ModelState state
forall a b. (a -> b) -> a -> b
$ do
  [SymToken]
w <- ReaderT (Var AssetKey) (State (ModelState state)) [SymToken]
-> Var AssetKey -> State (ModelState state) [SymToken]
forall r (m :: * -> *) a. ReaderT r m a -> r -> m a
runReaderT (((), [SymToken]) -> [SymToken]
forall a b. (a, b) -> b
snd (((), [SymToken]) -> [SymToken])
-> ReaderT
     (Var AssetKey) (State (ModelState state)) ((), [SymToken])
-> ReaderT (Var AssetKey) (State (ModelState state)) [SymToken]
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> WriterT
  [SymToken] (ReaderT (Var AssetKey) (State (ModelState state))) ()
-> ReaderT
     (Var AssetKey) (State (ModelState state)) ((), [SymToken])
forall w (m :: * -> *) a. WriterT w m a -> m (a, w)
Writer.runWriterT WriterT
  [SymToken] (ReaderT (Var AssetKey) (State (ModelState state))) ()
spec) Var AssetKey
v
  (Set SymToken -> Identity (Set SymToken))
-> ModelState state -> Identity (ModelState state)
forall state. Lens' (ModelState state) (Set SymToken)
symTokens ((Set SymToken -> Identity (Set SymToken))
 -> ModelState state -> Identity (ModelState state))
-> (Set SymToken -> Set SymToken) -> State (ModelState state) ()
forall s (m :: * -> *) a b.
MonadState s m =>
ASetter s s a b -> (a -> b) -> m ()
%= ([SymToken] -> Set SymToken
forall a. Ord a => [a] -> Set a
Set.fromList [SymToken]
w Set SymToken -> Set SymToken -> Set SymToken
forall a. Semigroup a => a -> a -> a
<>)

-- | Check if a given action creates new symbolic tokens in a given `ModelState`
createsTokens :: ContractModel state
              => ModelState state
              -> Action state
              -> Bool
createsTokens :: ModelState state -> Action state -> Bool
createsTokens ModelState state
s Action state
a = ([] [SymToken] -> [SymToken] -> Bool
forall a. Eq a => a -> a -> Bool
/=) ([SymToken] -> Bool) -> [SymToken] -> Bool
forall a b. (a -> b) -> a -> b
$ State (ModelState state) [SymToken]
-> ModelState state -> [SymToken]
forall s a. State s a -> s -> a
State.evalState (ReaderT (Var AssetKey) (State (ModelState state)) [SymToken]
-> Var AssetKey -> State (ModelState state) [SymToken]
forall r (m :: * -> *) a. ReaderT r m a -> r -> m a
runReaderT (((), [SymToken]) -> [SymToken]
forall a b. (a, b) -> b
snd (((), [SymToken]) -> [SymToken])
-> ReaderT
     (Var AssetKey) (State (ModelState state)) ((), [SymToken])
-> ReaderT (Var AssetKey) (State (ModelState state)) [SymToken]
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> WriterT
  [SymToken] (ReaderT (Var AssetKey) (State (ModelState state))) ()
-> ReaderT
     (Var AssetKey) (State (ModelState state)) ((), [SymToken])
forall w (m :: * -> *) a. WriterT w m a -> m (a, w)
Writer.runWriterT (Spec state ()
-> WriterT
     [SymToken] (ReaderT (Var AssetKey) (State (ModelState state))) ()
forall state a.
Spec state a
-> WriterT
     [SymToken] (ReaderT (Var AssetKey) (State (ModelState state))) a
unSpec (Action state -> Spec state ()
forall state. ContractModel state => Action state -> Spec state ()
nextState Action state
a))) (Int -> Var AssetKey
forall a. Int -> Var a
Var Int
0)) ModelState state
s

-- | Modify a field in the `ModelState`
modState :: forall state a. Setter' (ModelState state) a -> (a -> a) -> Spec state ()
modState :: Setter' (ModelState state) a -> (a -> a) -> Spec state ()
modState Setter' (ModelState state) a
l a -> a
f = WriterT
  [SymToken] (ReaderT (Var AssetKey) (State (ModelState state))) ()
-> Spec state ()
forall state a.
WriterT
  [SymToken] (ReaderT (Var AssetKey) (State (ModelState state))) a
-> Spec state a
Spec (WriterT
   [SymToken] (ReaderT (Var AssetKey) (State (ModelState state))) ()
 -> Spec state ())
-> WriterT
     [SymToken] (ReaderT (Var AssetKey) (State (ModelState state))) ()
-> Spec state ()
forall a b. (a -> b) -> a -> b
$ (ModelState state -> ModelState state)
-> WriterT
     [SymToken] (ReaderT (Var AssetKey) (State (ModelState state))) ()
forall s (m :: * -> *). MonadState s m => (s -> s) -> m ()
State.modify ((ModelState state -> ModelState state)
 -> WriterT
      [SymToken] (ReaderT (Var AssetKey) (State (ModelState state))) ())
-> (ModelState state -> ModelState state)
-> WriterT
     [SymToken] (ReaderT (Var AssetKey) (State (ModelState state))) ()
forall a b. (a -> b) -> a -> b
$ ASetter (ModelState state) (ModelState state) a a
-> (a -> a) -> ModelState state -> ModelState state
forall s t a b. ASetter s t a b -> (a -> b) -> s -> t
over ASetter (ModelState state) (ModelState state) a a
Setter' (ModelState state) a
l a -> a
f

-- | Wait the given number of slots. Updates the `currentSlot` of the model state.
wait :: ContractModel state => Integer -> Spec state ()
wait :: Integer -> Spec state ()
wait Integer
0 = () -> Spec state ()
forall (m :: * -> *) a. Monad m => a -> m a
return ()
wait Integer
n = do
  Slot Integer
now <- Getting Slot (ModelState (StateType (Spec state))) Slot
-> Spec state Slot
forall (m :: * -> *) a.
GetModelState m =>
Getting a (ModelState (StateType m)) a -> m a
viewModelState Getting Slot (ModelState (StateType (Spec state))) Slot
forall state. Getter (ModelState state) Slot
currentSlot
  Slot -> Spec state ()
forall state. ContractModel state => Slot -> Spec state ()
nextReactiveState (Integer -> Slot
Slot (Integer -> Slot) -> Integer -> Slot
forall a b. (a -> b) -> a -> b
$ Integer
now Integer -> Integer -> Integer
forall a. Num a => a -> a -> a
+ Integer
n)
  Setter' (ModelState state) Slot -> (Slot -> Slot) -> Spec state ()
forall state a.
Setter' (ModelState state) a -> (a -> a) -> Spec state ()
modState forall state. Lens' (ModelState state) Slot
Setter' (ModelState state) Slot
currentSlotL (Slot -> Slot -> Slot
forall a b. a -> b -> a
const (Integer -> Slot
Slot (Integer -> Slot) -> Integer -> Slot
forall a b. (a -> b) -> a -> b
$ Integer
now Integer -> Integer -> Integer
forall a. Num a => a -> a -> a
+ Integer
n))

-- | Wait until the given slot. Has no effect if `currentSlot` is greater than the given slot.
waitUntil :: ContractModel state => Slot -> Spec state ()
waitUntil :: Slot -> Spec state ()
waitUntil (Slot Integer
n) = do
  Slot Integer
now <- Getting Slot (ModelState (StateType (Spec state))) Slot
-> Spec state Slot
forall (m :: * -> *) a.
GetModelState m =>
Getting a (ModelState (StateType m)) a -> m a
viewModelState Getting Slot (ModelState (StateType (Spec state))) Slot
forall state. Getter (ModelState state) Slot
currentSlot
  Bool -> Spec state () -> Spec state ()
forall (f :: * -> *). Applicative f => Bool -> f () -> f ()
when (Integer
now Integer -> Integer -> Bool
forall a. Ord a => a -> a -> Bool
< Integer
n) (Spec state () -> Spec state ()) -> Spec state () -> Spec state ()
forall a b. (a -> b) -> a -> b
$ do
    Integer -> Spec state ()
forall state. ContractModel state => Integer -> Spec state ()
wait (Integer
n Integer -> Integer -> Integer
forall a. Num a => a -> a -> a
- Integer
now)

-- | Mint tokens. Minted tokens start out as `lockedValue` (i.e. owned by the contract) and can be
--   transferred to wallets using `deposit`.
mint :: SymValueLike v => v -> Spec state ()
mint :: v -> Spec state ()
mint v
v = Setter' (ModelState state) SymValue
-> (SymValue -> SymValue) -> Spec state ()
forall state a.
Setter' (ModelState state) a -> (a -> a) -> Spec state ()
modState forall state. Lens' (ModelState state) SymValue
Setter' (ModelState state) SymValue
mintedL (SymValue -> SymValue -> SymValue
forall a. Semigroup a => a -> a -> a
<> v -> SymValue
forall v. SymValueLike v => v -> SymValue
toSymValue v
v)

-- | Burn tokens. Equivalent to @`mint` . `inv`@.
burn :: SymValueLike v => v -> Spec state ()
burn :: v -> Spec state ()
burn = SymValue -> Spec state ()
forall v state. SymValueLike v => v -> Spec state ()
mint (SymValue -> Spec state ())
-> (v -> SymValue) -> v -> Spec state ()
forall b c a. (b -> c) -> (a -> b) -> a -> c
. SymValue -> SymValue
inv (SymValue -> SymValue) -> (v -> SymValue) -> v -> SymValue
forall b c a. (b -> c) -> (a -> b) -> a -> c
. v -> SymValue
forall v. SymValueLike v => v -> SymValue
toSymValue

-- | Add tokens to the `balanceChange` of a wallet. The added tokens are subtracted from the
--   `lockedValue` of tokens held by contracts.
deposit :: SymValueLike v => Wallet -> v -> Spec state ()
deposit :: Wallet -> v -> Spec state ()
deposit Wallet
w v
val = Setter' (ModelState state) (Maybe SymValue)
-> (Maybe SymValue -> Maybe SymValue) -> Spec state ()
forall state a.
Setter' (ModelState state) a -> (a -> a) -> Spec state ()
modState ((Map Wallet SymValue -> f (Map Wallet SymValue))
-> ModelState state -> f (ModelState state)
forall state. Lens' (ModelState state) (Map Wallet SymValue)
balanceChangesL ((Map Wallet SymValue -> f (Map Wallet SymValue))
 -> ModelState state -> f (ModelState state))
-> ((Maybe SymValue -> f (Maybe SymValue))
    -> Map Wallet SymValue -> f (Map Wallet SymValue))
-> (Maybe SymValue -> f (Maybe SymValue))
-> ModelState state
-> f (ModelState state)
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Index (Map Wallet SymValue)
-> Lens'
     (Map Wallet SymValue) (Maybe (IxValue (Map Wallet SymValue)))
forall m. At m => Index m -> Lens' m (Maybe (IxValue m))
at Index (Map Wallet SymValue)
Wallet
w) (SymValue -> Maybe SymValue
forall a. a -> Maybe a
Just (SymValue -> Maybe SymValue)
-> (Maybe SymValue -> SymValue) -> Maybe SymValue -> Maybe SymValue
forall b c a. (b -> c) -> (a -> b) -> a -> c
. SymValue -> (SymValue -> SymValue) -> Maybe SymValue -> SymValue
forall b a. b -> (a -> b) -> Maybe a -> b
maybe (v -> SymValue
forall v. SymValueLike v => v -> SymValue
toSymValue v
val) (SymValue -> SymValue -> SymValue
forall a. Semigroup a => a -> a -> a
<> v -> SymValue
forall v. SymValueLike v => v -> SymValue
toSymValue v
val))

-- | Withdraw tokens from a wallet. The withdrawn tokens are added to the `lockedValue` of tokens
--   held by contracts.
withdraw :: SymValueLike v => Wallet -> v -> Spec state ()
withdraw :: Wallet -> v -> Spec state ()
withdraw Wallet
w v
val = Wallet -> SymValue -> Spec state ()
forall v state. SymValueLike v => Wallet -> v -> Spec state ()
deposit Wallet
w (SymValue -> SymValue
inv (SymValue -> SymValue) -> (v -> SymValue) -> v -> SymValue
forall b c a. (b -> c) -> (a -> b) -> a -> c
. v -> SymValue
forall v. SymValueLike v => v -> SymValue
toSymValue (v -> SymValue) -> v -> SymValue
forall a b. (a -> b) -> a -> b
$ v
val)

-- | Transfer tokens between wallets, updating their `balances`.
transfer :: SymValueLike v
         => Wallet  -- ^ Transfer from this wallet
         -> Wallet  -- ^ to this wallet
         -> v   -- ^ this many tokens
         -> Spec state ()
transfer :: Wallet -> Wallet -> v -> Spec state ()
transfer Wallet
fromW Wallet
toW v
val = Wallet -> v -> Spec state ()
forall v state. SymValueLike v => Wallet -> v -> Spec state ()
withdraw Wallet
fromW v
val Spec state () -> Spec state () -> Spec state ()
forall (m :: * -> *) a b. Monad m => m a -> m b -> m b
>> Wallet -> v -> Spec state ()
forall v state. SymValueLike v => Wallet -> v -> Spec state ()
deposit Wallet
toW v
val

-- | Assert that a particular predicate holds at a point in the specification
assertSpec :: String -> Bool -> Spec state ()
assertSpec :: String -> Bool -> Spec state ()
assertSpec String
s Bool
b = do
  Setter' (ModelState state) [(String, Bool)]
-> ([(String, Bool)] -> [(String, Bool)]) -> Spec state ()
forall state a.
Setter' (ModelState state) a -> (a -> a) -> Spec state ()
modState forall state. Lens' (ModelState state) [(String, Bool)]
Setter' (ModelState state) [(String, Bool)]
assertions ((String
s, Bool
b)(String, Bool) -> [(String, Bool)] -> [(String, Bool)]
forall a. a -> [a] -> [a]
:)
  Setter' (ModelState state) Bool -> (Bool -> Bool) -> Spec state ()
forall state a.
Setter' (ModelState state) a -> (a -> a) -> Spec state ()
modState forall state. Lens' (ModelState state) Bool
Setter' (ModelState state) Bool
assertionsOk (Bool -> Bool -> Bool
&&Bool
b)

-- | Modify the contract state.
modifyContractState :: (state -> state) -> Spec state ()
modifyContractState :: (state -> state) -> Spec state ()
modifyContractState state -> state
f = Setter' (ModelState state) state
-> (state -> state) -> Spec state ()
forall state a.
Setter' (ModelState state) a -> (a -> a) -> Spec state ()
modState forall state state.
Lens (ModelState state) (ModelState state) state state
Setter' (ModelState state) state
contractState state -> state
f

-- | Set a specific field of the contract state.
($=) :: Setter' state a -> a -> Spec state ()
$= :: Setter' state a -> a -> Spec state ()
($=) = Setter' state a -> a -> Spec state ()
forall s (m :: * -> *) a b.
MonadState s m =>
ASetter s s a b -> b -> m ()
(.=)

-- | Modify a specific field of the contract state.
($~) :: Setter' state a -> (a -> a) -> Spec state ()
$~ :: Setter' state a -> (a -> a) -> Spec state ()
($~) = Setter' state a -> (a -> a) -> Spec state ()
forall s (m :: * -> *) a b.
MonadState s m =>
ASetter s s a b -> (a -> b) -> m ()
(%=)

-- | Create a new symbolic token in `nextState` - must have a
-- corresponding `registerToken` call in `perform`
createToken :: String -> Spec state SymToken
createToken :: String -> Spec state SymToken
createToken String
key = WriterT
  [SymToken]
  (ReaderT (Var AssetKey) (State (ModelState state)))
  SymToken
-> Spec state SymToken
forall state a.
WriterT
  [SymToken] (ReaderT (Var AssetKey) (State (ModelState state))) a
-> Spec state a
Spec (WriterT
   [SymToken]
   (ReaderT (Var AssetKey) (State (ModelState state)))
   SymToken
 -> Spec state SymToken)
-> WriterT
     [SymToken]
     (ReaderT (Var AssetKey) (State (ModelState state)))
     SymToken
-> Spec state SymToken
forall a b. (a -> b) -> a -> b
$ do
  Var AssetKey
var <- WriterT
  [SymToken]
  (ReaderT (Var AssetKey) (State (ModelState state)))
  (Var AssetKey)
forall r (m :: * -> *). MonadReader r m => m r
ask
  [SymToken]
-> WriterT
     [SymToken] (ReaderT (Var AssetKey) (State (ModelState state))) ()
forall w (m :: * -> *). MonadWriter w m => w -> m ()
Writer.tell [Var AssetKey -> String -> SymToken
SymToken Var AssetKey
var String
key]
  SymToken
-> WriterT
     [SymToken]
     (ReaderT (Var AssetKey) (State (ModelState state)))
     SymToken
forall (f :: * -> *) a. Applicative f => a -> f a
pure (SymToken
 -> WriterT
      [SymToken]
      (ReaderT (Var AssetKey) (State (ModelState state)))
      SymToken)
-> SymToken
-> WriterT
     [SymToken]
     (ReaderT (Var AssetKey) (State (ModelState state)))
     SymToken
forall a b. (a -> b) -> a -> b
$ Var AssetKey -> String -> SymToken
SymToken Var AssetKey
var String
key

-- | Register the real token corresponding to a symbolic token created
-- in `createToken`.
registerToken :: String -> AssetClass -> SpecificationEmulatorTrace ()
registerToken :: String -> AssetClass -> SpecificationEmulatorTrace ()
registerToken String
s AssetClass
ac = [(String, AssetClass)] -> SpecificationEmulatorTrace ()
forall w (effs :: [* -> *]).
Member (Writer w) effs =>
w -> Eff effs ()
tell [(String
s, AssetClass
ac)]

-- | `delay n` delays emulator execution by `n` slots
delay :: Integer -> SpecificationEmulatorTrace ()
delay :: Integer -> SpecificationEmulatorTrace ()
delay = Eff
  '[Writer [(String, AssetClass)], RunContract, Assert, Waiting,
    EmulatorControl, EmulatedWalletAPI, LogMsg String,
    Error EmulatorRuntimeError]
  Slot
-> SpecificationEmulatorTrace ()
forall (f :: * -> *) a. Functor f => f a -> f ()
void (Eff
   '[Writer [(String, AssetClass)], RunContract, Assert, Waiting,
     EmulatorControl, EmulatedWalletAPI, LogMsg String,
     Error EmulatorRuntimeError]
   Slot
 -> SpecificationEmulatorTrace ())
-> (Integer
    -> Eff
         '[Writer [(String, AssetClass)], RunContract, Assert, Waiting,
           EmulatorControl, EmulatedWalletAPI, LogMsg String,
           Error EmulatorRuntimeError]
         Slot)
-> Integer
-> SpecificationEmulatorTrace ()
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Natural
-> Eff
     '[Writer [(String, AssetClass)], RunContract, Assert, Waiting,
       EmulatorControl, EmulatedWalletAPI, LogMsg String,
       Error EmulatorRuntimeError]
     Slot
forall (effs :: [* -> *]).
Member Waiting effs =>
Natural -> Eff effs Slot
Trace.waitNSlots (Natural
 -> Eff
      '[Writer [(String, AssetClass)], RunContract, Assert, Waiting,
        EmulatorControl, EmulatedWalletAPI, LogMsg String,
        Error EmulatorRuntimeError]
      Slot)
-> (Integer -> Natural)
-> Integer
-> Eff
     '[Writer [(String, AssetClass)], RunContract, Assert, Waiting,
       EmulatorControl, EmulatedWalletAPI, LogMsg String,
       Error EmulatorRuntimeError]
     Slot
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Integer -> Natural
forall a. Num a => Integer -> a
fromInteger

instance GetModelState (Spec state) where
    type StateType (Spec state) = state
    getModelState :: Spec state (ModelState (StateType (Spec state)))
getModelState = WriterT
  [SymToken]
  (ReaderT (Var AssetKey) (State (ModelState state)))
  (ModelState state)
-> Spec state (ModelState state)
forall state a.
WriterT
  [SymToken] (ReaderT (Var AssetKey) (State (ModelState state))) a
-> Spec state a
Spec WriterT
  [SymToken]
  (ReaderT (Var AssetKey) (State (ModelState state)))
  (ModelState state)
forall s (m :: * -> *). MonadState s m => m s
State.get

handle :: ContractModel s => Handles s -> HandleFun s
handle :: Handles s -> HandleFun s
handle Handles s
handles ContractInstanceKey s w schema err params
key =
    case ContractInstanceKey s w schema err params
-> Handles s -> Maybe (WalletContractHandle w schema err)
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, Typeable key,
 Typeable val, Eq (key i j k l)) =>
key i j k l -> IMap key val -> Maybe (val i j k)
imLookup ContractInstanceKey s w schema err params
key Handles s
handles of
        Just (WalletContractHandle Wallet
_ ContractHandle w schema err
h) -> ContractHandle w schema err
h
        Maybe (WalletContractHandle w schema err)
Nothing                         -> String -> ContractHandle w schema err
forall a. HasCallStack => String -> a
error (String -> ContractHandle w schema err)
-> String -> ContractHandle w schema err
forall a b. (a -> b) -> a -> b
$ String
"handle: No handle for " String -> ShowS
forall a. [a] -> [a] -> [a]
++ ContractInstanceKey s w schema err params -> String
forall a. Show a => a -> String
show ContractInstanceKey s w schema err params
key

type AssetMap = Map AssetKey (Map String AssetClass)

-- | The `EmulatorTrace` monad does not let you get the result of a computation out, but the way
--   "Test.QuickCheck.Monadic" is set up requires you to provide a function @m Property -> Property@.
--   This means that we can't use `EmulatorTrace` as the action monad in the `StateModel`. Instead
--   we use a state monad that builds up an `EmulatorTrace` computation to be executed at the end
--   (by `finalChecks`). We also need access to the contract handles, so what we are building is a
--   function from the handles to an emulator trace computation returning potentially updated
--   handles.

-- TODO: Refactor this(!)
type EmulatorMonad = State.StateT AssetMap EmulatorTrace
newtype EmulatorAction state = EmulatorAction { EmulatorAction state
-> Handles state -> EmulatorMonad (Handles state)
runEmulatorAction :: Handles state -> EmulatorMonad (Handles state) }

instance Semigroup (EmulatorAction state) where
    EmulatorAction Handles state -> EmulatorMonad (Handles state)
f <> :: EmulatorAction state
-> EmulatorAction state -> EmulatorAction state
<> EmulatorAction Handles state -> EmulatorMonad (Handles state)
g = (Handles state -> EmulatorMonad (Handles state))
-> EmulatorAction state
forall state.
(Handles state -> EmulatorMonad (Handles state))
-> EmulatorAction state
EmulatorAction (Handles state -> EmulatorMonad (Handles state)
f (Handles state -> EmulatorMonad (Handles state))
-> (Handles state -> EmulatorMonad (Handles state))
-> Handles state
-> EmulatorMonad (Handles state)
forall (m :: * -> *) a b c.
Monad m =>
(a -> m b) -> (b -> m c) -> a -> m c
>=> Handles state -> EmulatorMonad (Handles state)
g)

instance Monoid (EmulatorAction state) where
    mempty :: EmulatorAction state
mempty  = (Handles state -> EmulatorMonad (Handles state))
-> EmulatorAction state
forall state.
(Handles state -> EmulatorMonad (Handles state))
-> EmulatorAction state
EmulatorAction Handles state -> EmulatorMonad (Handles state)
forall (f :: * -> *) a. Applicative f => a -> f a
pure
    mappend :: EmulatorAction state
-> EmulatorAction state -> EmulatorAction state
mappend = EmulatorAction state
-> EmulatorAction state -> EmulatorAction state
forall a. Semigroup a => a -> a -> a
(<>)

type ContractMonad state = State.State (ContractMonadState state)

data ContractMonadState state = ContractMonadState { ContractMonadState state -> EmulatorAction state
_cmsEmulatorAction    :: (EmulatorAction state)
                                                   , ContractMonadState state -> [SomeContractInstanceKey state]
_cmsContractInstances :: [SomeContractInstanceKey state]
                                                   , ContractMonadState state -> AssetKey
_cmsNextVarIdx        :: AssetKey }

makeLenses ''ContractMonadState

instance Semigroup (ContractMonadState state) where
    ContractMonadState EmulatorAction state
f [SomeContractInstanceKey state]
xs AssetKey
idx <> :: ContractMonadState state
-> ContractMonadState state -> ContractMonadState state
<> ContractMonadState EmulatorAction state
g [SomeContractInstanceKey state]
ys AssetKey
idx' = EmulatorAction state
-> [SomeContractInstanceKey state]
-> AssetKey
-> ContractMonadState state
forall state.
EmulatorAction state
-> [SomeContractInstanceKey state]
-> AssetKey
-> ContractMonadState state
ContractMonadState (EmulatorAction state
f EmulatorAction state
-> EmulatorAction state -> EmulatorAction state
forall a. Semigroup a => a -> a -> a
<> EmulatorAction state
g) ([SomeContractInstanceKey state]
xs [SomeContractInstanceKey state]
-> [SomeContractInstanceKey state]
-> [SomeContractInstanceKey state]
forall a. Semigroup a => a -> a -> a
<> [SomeContractInstanceKey state]
ys) (AssetKey -> AssetKey -> AssetKey
forall a. Ord a => a -> a -> a
max AssetKey
idx AssetKey
idx')

instance Monoid (ContractMonadState state) where
    mempty :: ContractMonadState state
mempty = EmulatorAction state
-> [SomeContractInstanceKey state]
-> AssetKey
-> ContractMonadState state
forall state.
EmulatorAction state
-> [SomeContractInstanceKey state]
-> AssetKey
-> ContractMonadState state
ContractMonadState EmulatorAction state
forall a. Monoid a => a
mempty [SomeContractInstanceKey state]
forall a. Monoid a => a
mempty AssetKey
0

runEmulator_ :: (Handles state -> EmulatorMonad ()) -> ContractMonad state ()
runEmulator_ :: (Handles state -> EmulatorMonad ()) -> ContractMonad state ()
runEmulator_ Handles state -> EmulatorMonad ()
a = (EmulatorAction state -> Identity (EmulatorAction state))
-> ContractMonadState state -> Identity (ContractMonadState state)
forall state.
Lens' (ContractMonadState state) (EmulatorAction state)
cmsEmulatorAction ((EmulatorAction state -> Identity (EmulatorAction state))
 -> ContractMonadState state -> Identity (ContractMonadState state))
-> (EmulatorAction state -> EmulatorAction state)
-> ContractMonad state ()
forall s (m :: * -> *) a b.
MonadState s m =>
ASetter s s a b -> (a -> b) -> m ()
%= (EmulatorAction state
-> EmulatorAction state -> EmulatorAction state
forall a. Semigroup a => a -> a -> a
<> (Handles state -> EmulatorMonad (Handles state))
-> EmulatorAction state
forall state.
(Handles state -> EmulatorMonad (Handles state))
-> EmulatorAction state
EmulatorAction (\ Handles state
h -> Handles state
h Handles state -> EmulatorMonad () -> EmulatorMonad (Handles state)
forall (f :: * -> *) a b. Functor f => a -> f b -> f a
<$ Handles state -> EmulatorMonad ()
a Handles state
h))

runEmulator :: (Handles state -> EmulatorMonad (Handles state)) -> ContractMonad state ()
runEmulator :: (Handles state -> EmulatorMonad (Handles state))
-> ContractMonad state ()
runEmulator Handles state -> EmulatorMonad (Handles state)
a = (EmulatorAction state -> Identity (EmulatorAction state))
-> ContractMonadState state -> Identity (ContractMonadState state)
forall state.
Lens' (ContractMonadState state) (EmulatorAction state)
cmsEmulatorAction ((EmulatorAction state -> Identity (EmulatorAction state))
 -> ContractMonadState state -> Identity (ContractMonadState state))
-> (EmulatorAction state -> EmulatorAction state)
-> ContractMonad state ()
forall s (m :: * -> *) a b.
MonadState s m =>
ASetter s s a b -> (a -> b) -> m ()
%= (EmulatorAction state
-> EmulatorAction state -> EmulatorAction state
forall a. Semigroup a => a -> a -> a
<> (Handles state -> EmulatorMonad (Handles state))
-> EmulatorAction state
forall state.
(Handles state -> EmulatorMonad (Handles state))
-> EmulatorAction state
EmulatorAction (\ Handles state
h -> Handles state -> EmulatorMonad (Handles state)
a Handles state
h))

addInstances :: [StartContract state] -> ContractMonad state ()
addInstances :: [StartContract state] -> ContractMonad state ()
addInstances [StartContract state]
starts = ([SomeContractInstanceKey state]
 -> Identity [SomeContractInstanceKey state])
-> ContractMonadState state -> Identity (ContractMonadState state)
forall state.
Lens' (ContractMonadState state) [SomeContractInstanceKey state]
cmsContractInstances (([SomeContractInstanceKey state]
  -> Identity [SomeContractInstanceKey state])
 -> ContractMonadState state -> Identity (ContractMonadState state))
-> [SomeContractInstanceKey state] -> ContractMonad state ()
forall s (m :: * -> *) a.
(MonadState s m, Semigroup a) =>
ASetter' s a -> a -> m ()
<>= [ContractInstanceKey state w s e p -> SomeContractInstanceKey state
forall w (s :: Row *) e p state.
(SchemaConstraints w s e, Typeable p) =>
ContractInstanceKey state w s e p -> SomeContractInstanceKey state
Key ContractInstanceKey state w s e p
key | StartContract ContractInstanceKey state w s e p
key p
_ <- [StartContract state]
starts]

setHandles :: EmulatorMonad (Handles state) -> ContractMonad state ()
setHandles :: EmulatorMonad (Handles state) -> ContractMonad state ()
setHandles EmulatorMonad (Handles state)
a = (EmulatorAction state -> Identity (EmulatorAction state))
-> ContractMonadState state -> Identity (ContractMonadState state)
forall state.
Lens' (ContractMonadState state) (EmulatorAction state)
cmsEmulatorAction ((EmulatorAction state -> Identity (EmulatorAction state))
 -> ContractMonadState state -> Identity (ContractMonadState state))
-> (EmulatorAction state -> EmulatorAction state)
-> ContractMonad state ()
forall s (m :: * -> *) a b.
MonadState s m =>
ASetter s s a b -> (a -> b) -> m ()
%= (EmulatorAction state
-> EmulatorAction state -> EmulatorAction state
forall a. Semigroup a => a -> a -> a
<> (Handles state -> EmulatorMonad (Handles state))
-> EmulatorAction state
forall state.
(Handles state -> EmulatorMonad (Handles state))
-> EmulatorAction state
EmulatorAction (EmulatorMonad (Handles state)
-> Handles state -> EmulatorMonad (Handles state)
forall a b. a -> b -> a
const EmulatorMonad (Handles state)
a))

makeVariable :: ContractMonad state AssetKey
makeVariable :: ContractMonad state AssetKey
makeVariable = do
  AssetKey
i <- Getting AssetKey (ContractMonadState state) AssetKey
-> ContractMonad state AssetKey
forall s (m :: * -> *) a. MonadState s m => Getting a s a -> m a
use Getting AssetKey (ContractMonadState state) AssetKey
forall state. Lens' (ContractMonadState state) AssetKey
cmsNextVarIdx
  (AssetKey -> Identity AssetKey)
-> ContractMonadState state -> Identity (ContractMonadState state)
forall state. Lens' (ContractMonadState state) AssetKey
cmsNextVarIdx ((AssetKey -> Identity AssetKey)
 -> ContractMonadState state -> Identity (ContractMonadState state))
-> AssetKey -> StateT (ContractMonadState state) Identity ()
forall s (m :: * -> *) a.
(MonadState s m, Num a) =>
ASetter' s a -> a -> m ()
+= AssetKey
1
  AssetKey -> ContractMonad state AssetKey
forall (f :: * -> *) a. Applicative f => a -> f a
pure AssetKey
i

contractAction :: ContractModel state => ModelState state -> Action state -> StateModel.Action (ModelState state) AssetKey
contractAction :: ModelState state
-> Action state -> Action (ModelState state) AssetKey
contractAction ModelState state
s Action state
a = Bool -> Action state -> Action (ModelState state) AssetKey
forall state.
Bool -> Action state -> Action (ModelState state) AssetKey
ContractAction (ModelState state -> Action state -> Bool
forall state.
ContractModel state =>
ModelState state -> Action state -> Bool
createsTokens ModelState state
s Action state
a) Action state
a

instance ContractModel state => Show (StateModel.Action (ModelState state) a) where
    showsPrec :: Int -> Action (ModelState state) a -> ShowS
showsPrec Int
p (ContractAction _ a) = Int -> Action state -> ShowS
forall a. Show a => Int -> a -> ShowS
showsPrec Int
p Action state
a
    showsPrec Int
p (WaitUntil n)        = Bool -> ShowS -> ShowS
showParen (Int
p Int -> Int -> Bool
forall a. Ord a => a -> a -> Bool
>= Int
11) (ShowS -> ShowS) -> ShowS -> ShowS
forall a b. (a -> b) -> a -> b
$ String -> ShowS
showString String
"WaitUntil " ShowS -> ShowS -> ShowS
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Int -> Slot -> ShowS
forall a. Show a => Int -> a -> ShowS
showsPrec Int
11 Slot
n
    showsPrec Int
p (Unilateral w)       = Bool -> ShowS -> ShowS
showParen (Int
p Int -> Int -> Bool
forall a. Ord a => a -> a -> Bool
>= Int
11) (ShowS -> ShowS) -> ShowS -> ShowS
forall a b. (a -> b) -> a -> b
$ String -> ShowS
showString String
"Unilateral " ShowS -> ShowS -> ShowS
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Int -> Wallet -> ShowS
forall a. Show a => Int -> a -> ShowS
showsPrec Int
11 Wallet
w

deriving instance ContractModel state => Eq (StateModel.Action (ModelState state) a)

instance ContractModel state => StateModel (ModelState state) where

    data Action (ModelState state) a where
        ContractAction :: Bool -> Action state -> StateModel.Action (ModelState state) AssetKey
        Unilateral :: Wallet -> StateModel.Action (ModelState state) ()
          -- ^ This action disables all wallets other than the given wallet, by freezing their
          --   contract instances and removing their private keys from the emulator state. This can
          --   be used to check that a wallet can *unilaterally* achieve a desired outcome, without
          --   the help of other wallets.
        WaitUntil :: Slot -> StateModel.Action (ModelState state) ()

    type ActionMonad (ModelState state) = ContractMonad state

    arbitraryAction :: ModelState state -> Gen (Any (Action (ModelState state)))
arbitraryAction ModelState state
s =
        -- TODO: do we need some way to control the distribution
        -- between actions and waits here?
        [(Int, Gen (Any (Action (ModelState state))))]
-> Gen (Any (Action (ModelState state)))
forall a. [(Int, Gen a)] -> Gen a
frequency [(Double -> Int
forall a b. (RealFrac a, Integral b) => a -> b
floor (Double -> Int) -> Double -> Int
forall a b. (a -> b) -> a -> b
$ Double
100.0Double -> Double -> Double
forall a. Num a => a -> a -> a
*(Double
1.0Double -> Double -> Double
forall a. Num a => a -> a -> a
-ModelState state -> Double
forall state. ContractModel state => ModelState state -> Double
waitProbability ModelState state
s), do Action state
a <- ModelState state -> Gen (Action state)
forall state.
ContractModel state =>
ModelState state -> Gen (Action state)
arbitraryAction ModelState state
s
                                                              Any (Action (ModelState state))
-> Gen (Any (Action (ModelState state)))
forall (m :: * -> *) a. Monad m => a -> m a
return (Action (ModelState state) AssetKey
-> Any (Action (ModelState state))
forall a (f :: * -> *).
(Show a, Typeable a, Eq (f a)) =>
f a -> Any f
Some (Bool -> Action state -> Action (ModelState state) AssetKey
forall state.
Bool -> Action state -> Action (ModelState state) AssetKey
ContractAction (ModelState state -> Action state -> Bool
forall state.
ContractModel state =>
ModelState state -> Action state -> Bool
createsTokens ModelState state
s Action state
a) Action state
a)))
                  ,(Double -> Int
forall a b. (RealFrac a, Integral b) => a -> b
floor (Double -> Int) -> Double -> Int
forall a b. (a -> b) -> a -> b
$ Double
100.0Double -> Double -> Double
forall a. Num a => a -> a -> a
*ModelState state -> Double
forall state. ContractModel state => ModelState state -> Double
waitProbability ModelState state
s, Action (ModelState state) () -> Any (Action (ModelState state))
forall a (f :: * -> *).
(Show a, Typeable a, Eq (f a)) =>
f a -> Any f
Some (Action (ModelState state) () -> Any (Action (ModelState state)))
-> (Slot -> Action (ModelState state) ())
-> Slot
-> Any (Action (ModelState state))
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Slot -> Action (ModelState state) ()
forall state. Slot -> Action (ModelState state) ()
WaitUntil (Slot -> Action (ModelState state) ())
-> (Slot -> Slot) -> Slot -> Action (ModelState state) ()
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Slot -> Slot
step (Slot -> Any (Action (ModelState state)))
-> Gen Slot -> Gen (Any (Action (ModelState state)))
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> ModelState state -> Gen Slot
forall state. ContractModel state => ModelState state -> Gen Slot
arbitraryWaitInterval ModelState state
s)]
        where
            slot :: Slot
slot = ModelState state
s ModelState state -> Getting Slot (ModelState state) Slot -> Slot
forall s a. s -> Getting a s a -> a
^. Getting Slot (ModelState state) Slot
forall state. Getter (ModelState state) Slot
currentSlot
            step :: Slot -> Slot
step Slot
n = Slot
slot Slot -> Slot -> Slot
forall a. Num a => a -> a -> a
+ Slot
n

    shrinkAction :: ModelState state
-> Action (ModelState state) a -> [Any (Action (ModelState state))]
shrinkAction ModelState state
s (ContractAction _ a) =
      [ Action (ModelState state) () -> Any (Action (ModelState state))
forall a (f :: * -> *).
(Show a, Typeable a, Eq (f a)) =>
f a -> Any f
Some (Slot -> Action (ModelState state) ()
forall state. Slot -> Action (ModelState state) ()
WaitUntil (Integer -> Slot
Slot Integer
n')) | let Slot Integer
n = Spec state ()
-> Var AssetKey -> ModelState state -> ModelState state
forall state.
Spec state ()
-> Var AssetKey -> ModelState state -> ModelState state
runSpec (Action state -> Spec state ()
forall state. ContractModel state => Action state -> Spec state ()
nextState Action state
a) (Int -> Var AssetKey
forall a. Int -> Var a
Var Int
0) ModelState state
s ModelState state -> Getting Slot (ModelState state) Slot -> Slot
forall s a. s -> Getting a s a -> a
^. Getting Slot (ModelState state) Slot
forall state. Getter (ModelState state) Slot
currentSlot
                                   , Integer
n' <- Integer
n Integer -> [Integer] -> [Integer]
forall a. a -> [a] -> [a]
: Integer -> [Integer]
forall a. Arbitrary a => a -> [a]
shrink Integer
n
                                   , Integer -> Slot
Slot Integer
n' Slot -> Slot -> Bool
forall a. Ord a => a -> a -> Bool
> ModelState state
s ModelState state -> Getting Slot (ModelState state) Slot -> Slot
forall s a. s -> Getting a s a -> a
^. Getting Slot (ModelState state) Slot
forall state. Getter (ModelState state) Slot
currentSlot ] [Any (Action (ModelState state))]
-> [Any (Action (ModelState state))]
-> [Any (Action (ModelState state))]
forall a. [a] -> [a] -> [a]
++
      [ Action (ModelState state) AssetKey
-> Any (Action (ModelState state))
forall a (f :: * -> *).
(Show a, Typeable a, Eq (f a)) =>
f a -> Any f
Some (ModelState state
-> Action state -> Action (ModelState state) AssetKey
forall state.
ContractModel state =>
ModelState state
-> Action state -> Action (ModelState state) AssetKey
contractAction ModelState state
s Action state
a') | Action state
a' <- ModelState state -> Action state -> [Action state]
forall state.
ContractModel state =>
ModelState state -> Action state -> [Action state]
shrinkAction ModelState state
s Action state
a ]
    shrinkAction ModelState state
s (WaitUntil (Slot n))        =
      [ Action (ModelState state) () -> Any (Action (ModelState state))
forall a (f :: * -> *).
(Show a, Typeable a, Eq (f a)) =>
f a -> Any f
Some (Slot -> Action (ModelState state) ()
forall state. Slot -> Action (ModelState state) ()
WaitUntil (Integer -> Slot
Slot Integer
n')) | Integer
n' <- Integer -> [Integer]
forall a. Arbitrary a => a -> [a]
shrink Integer
n, Integer -> Slot
Slot Integer
n' Slot -> Slot -> Bool
forall a. Ord a => a -> a -> Bool
> ModelState state
s ModelState state -> Getting Slot (ModelState state) Slot -> Slot
forall s a. s -> Getting a s a -> a
^. Getting Slot (ModelState state) Slot
forall state. Getter (ModelState state) Slot
currentSlot ]
    shrinkAction ModelState state
_ Action (ModelState state) a
_                    = []

    initialState :: ModelState state
initialState = ModelState :: forall state.
Slot
-> Map Wallet SymValue
-> SymValue
-> Set SymToken
-> [(String, Bool)]
-> Bool
-> state
-> ModelState state
ModelState { _currentSlot :: Slot
_currentSlot      = Slot
1
                              , _balanceChanges :: Map Wallet SymValue
_balanceChanges   = Map Wallet SymValue
forall k a. Map k a
Map.empty
                              , _minted :: SymValue
_minted           = SymValue
forall a. Monoid a => a
mempty
                              , _assertions :: [(String, Bool)]
_assertions       = [(String, Bool)]
forall a. Monoid a => a
mempty
                              , _assertionsOk :: Bool
_assertionsOk     = Bool
True
                              , _symTokens :: Set SymToken
_symTokens        = Set SymToken
forall a. Monoid a => a
mempty
                              , _contractState :: state
_contractState    = state
forall state. ContractModel state => state
initialState
                              }

    nextState :: ModelState state
-> Action (ModelState state) a -> Var a -> ModelState state
nextState ModelState state
s (ContractAction _ cmd) Var a
v = Spec state ()
-> Var AssetKey -> ModelState state -> ModelState state
forall state.
Spec state ()
-> Var AssetKey -> ModelState state -> ModelState state
runSpec (Action state -> Spec state ()
forall state. ContractModel state => Action state -> Spec state ()
nextState Action state
cmd) Var a
Var AssetKey
v ModelState state
s
    nextState ModelState state
s (WaitUntil n) Var a
_          = Spec state ()
-> Var AssetKey -> ModelState state -> ModelState state
forall state.
Spec state ()
-> Var AssetKey -> ModelState state -> ModelState state
runSpec (() () -> Spec state () -> Spec state ()
forall (f :: * -> *) a b. Functor f => a -> f b -> f a
<$ Slot -> Spec state ()
forall state. ContractModel state => Slot -> Spec state ()
waitUntil Slot
n) (String -> Var AssetKey
forall a. HasCallStack => String -> a
error String
"unreachable") ModelState state
s
    nextState ModelState state
s Unilateral{} Var a
_           = ModelState state
s

    -- Note that the order of the preconditions in this case matter - we want to run
    -- `getAllSymtokens` last because its likely to be stricter than the user precondition
    -- and so if the user relies on the lazyness of the Gen monad by using the precondition
    -- to avoid duplicate checks in the precondition and generator we don't screw that up.
    precondition :: ModelState state -> Action (ModelState state) a -> Bool
precondition ModelState state
s (ContractAction _ cmd) = ModelState state
s ModelState state -> Getting Bool (ModelState state) Bool -> Bool
forall s a. s -> Getting a s a -> a
^. Getting Bool (ModelState state) Bool
forall state. Lens' (ModelState state) Bool
assertionsOk
                                          Bool -> Bool -> Bool
&& ModelState state -> Action state -> Bool
forall state.
ContractModel state =>
ModelState state -> Action state -> Bool
precondition ModelState state
s Action state
cmd
                                          Bool -> Bool -> Bool
&& Action state -> Set SymToken
forall state. HasActions state => Action state -> Set SymToken
getAllSymtokens Action state
cmd Set SymToken -> Set SymToken -> Bool
forall a. Ord a => Set a -> Set a -> Bool
`Set.isSubsetOf` (ModelState state
s ModelState state
-> Getting (Set SymToken) (ModelState state) (Set SymToken)
-> Set SymToken
forall s a. s -> Getting a s a -> a
^. Getting (Set SymToken) (ModelState state) (Set SymToken)
forall state. Lens' (ModelState state) (Set SymToken)
symTokens)
    precondition ModelState state
s (WaitUntil n)          = Slot
n Slot -> Slot -> Bool
forall a. Ord a => a -> a -> Bool
> ModelState state
s ModelState state -> Getting Slot (ModelState state) Slot -> Slot
forall s a. s -> Getting a s a -> a
^. Getting Slot (ModelState state) Slot
forall state. Getter (ModelState state) Slot
currentSlot
    precondition ModelState state
_ Action (ModelState state) a
_                      = Bool
True

    perform :: ModelState state
-> Action (ModelState state) a
-> LookUp
-> ActionMonad (ModelState state) a
perform ModelState state
s (ContractAction _ cmd) LookUp
envOuter = do
      let newKeys :: [StartContract state]
newKeys = ModelState state -> Action state -> [StartContract state]
forall state.
ContractModel state =>
ModelState state -> Action state -> [StartContract state]
startInstances ModelState state
s Action state
cmd
      [StartContract state] -> ContractMonad state ()
forall state. [StartContract state] -> ContractMonad state ()
addInstances [StartContract state]
newKeys
      AssetKey
v <- ContractMonad state AssetKey
forall state. ContractMonad state AssetKey
makeVariable
      (Handles state -> EmulatorMonad (Handles state))
-> ContractMonad state ()
forall state.
(Handles state -> EmulatorMonad (Handles state))
-> ContractMonad state ()
runEmulator ((Handles state -> EmulatorMonad (Handles state))
 -> ContractMonad state ())
-> (Handles state -> EmulatorMonad (Handles state))
-> ContractMonad state ()
forall a b. (a -> b) -> a -> b
$ \ Handles state
h -> do
        Map AssetKey (Map String AssetClass)
envInner <- StateT
  (Map AssetKey (Map String AssetClass))
  EmulatorTrace
  (Map AssetKey (Map String AssetClass))
forall s (m :: * -> *). MonadState s m => m s
State.get
        let lookup :: SymToken -> AssetClass
lookup (SymToken Var AssetKey
outerVar String
idx) = case String -> Map String AssetClass -> Maybe AssetClass
forall k a. Ord k => k -> Map k a -> Maybe a
Map.lookup String
idx (Map String AssetClass -> Maybe AssetClass)
-> Map String AssetClass -> Maybe AssetClass
forall a b. (a -> b) -> a -> b
$ Maybe (Map String AssetClass) -> Map String AssetClass
forall (t :: * -> *) m. (Foldable t, Monoid m) => t m -> m
fold (AssetKey
-> Map AssetKey (Map String AssetClass)
-> Maybe (Map String AssetClass)
forall k a. Ord k => k -> Map k a -> Maybe a
Map.lookup (Var AssetKey -> AssetKey
LookUp
envOuter Var AssetKey
outerVar) Map AssetKey (Map String AssetClass)
envInner) of
              Just AssetClass
tok -> AssetClass
tok
              Maybe AssetClass
Nothing  -> String -> AssetClass
forall a. HasCallStack => String -> a
error (String -> AssetClass) -> String -> AssetClass
forall a b. (a -> b) -> a -> b
$ String
"Missing registerToken call for token: " String -> ShowS
forall a. [a] -> [a] -> [a]
++ ShowS
forall a. Show a => a -> String
show String
idx
        Handles state
newHandles <- Eff
  '[StartContract, RunContract, Assert, Waiting, EmulatorControl,
    EmulatedWalletAPI, LogMsg String, Error EmulatorRuntimeError]
  (Handles state)
-> EmulatorMonad (Handles state)
forall (t :: (* -> *) -> * -> *) (m :: * -> *) a.
(MonadTrans t, Monad m) =>
m a -> t m a
lift (Eff
   '[StartContract, RunContract, Assert, Waiting, EmulatorControl,
     EmulatedWalletAPI, LogMsg String, Error EmulatorRuntimeError]
   (Handles state)
 -> EmulatorMonad (Handles state))
-> Eff
     '[StartContract, RunContract, Assert, Waiting, EmulatorControl,
       EmulatedWalletAPI, LogMsg String, Error EmulatorRuntimeError]
     (Handles state)
-> EmulatorMonad (Handles state)
forall a b. (a -> b) -> a -> b
$ (SymToken -> AssetClass)
-> [StartContract state]
-> Eff
     '[StartContract, RunContract, Assert, Waiting, EmulatorControl,
       EmulatedWalletAPI, LogMsg String, Error EmulatorRuntimeError]
     (Handles state)
forall state.
ContractModel state =>
(SymToken -> AssetClass)
-> [StartContract state] -> EmulatorTrace (Handles state)
activateWallets SymToken -> AssetClass
lookup [StartContract state]
newKeys
        let h' :: Handles state
h' = Handles state -> Handles state -> Handles state
forall state. Handles state -> Handles state -> Handles state
handlesAppend Handles state
newHandles Handles state
h
        (()
_, [(String, AssetClass)]
result) <- Eff
  '[StartContract, RunContract, Assert, Waiting, EmulatorControl,
    EmulatedWalletAPI, LogMsg String, Error EmulatorRuntimeError]
  ((), [(String, AssetClass)])
-> StateT
     (Map AssetKey (Map String AssetClass))
     EmulatorTrace
     ((), [(String, AssetClass)])
forall (t :: (* -> *) -> * -> *) (m :: * -> *) a.
(MonadTrans t, Monad m) =>
m a -> t m a
lift (Eff
   '[StartContract, RunContract, Assert, Waiting, EmulatorControl,
     EmulatedWalletAPI, LogMsg String, Error EmulatorRuntimeError]
   ((), [(String, AssetClass)])
 -> StateT
      (Map AssetKey (Map String AssetClass))
      EmulatorTrace
      ((), [(String, AssetClass)]))
-> (SpecificationEmulatorTrace ()
    -> Eff
         '[StartContract, RunContract, Assert, Waiting, EmulatorControl,
           EmulatedWalletAPI, LogMsg String, Error EmulatorRuntimeError]
         ((), [(String, AssetClass)]))
-> SpecificationEmulatorTrace ()
-> StateT
     (Map AssetKey (Map String AssetClass))
     EmulatorTrace
     ((), [(String, AssetClass)])
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Eff
  '[RunContract, Assert, Waiting, EmulatorControl, EmulatedWalletAPI,
    LogMsg String, Error EmulatorRuntimeError]
  ((), [(String, AssetClass)])
-> Eff
     '[StartContract, RunContract, Assert, Waiting, EmulatorControl,
       EmulatedWalletAPI, LogMsg String, Error EmulatorRuntimeError]
     ((), [(String, AssetClass)])
forall (effs :: [* -> *]) a (e :: * -> *).
Eff effs a -> Eff (e : effs) a
raise (Eff
   '[RunContract, Assert, Waiting, EmulatorControl, EmulatedWalletAPI,
     LogMsg String, Error EmulatorRuntimeError]
   ((), [(String, AssetClass)])
 -> Eff
      '[StartContract, RunContract, Assert, Waiting, EmulatorControl,
        EmulatedWalletAPI, LogMsg String, Error EmulatorRuntimeError]
      ((), [(String, AssetClass)]))
-> (SpecificationEmulatorTrace ()
    -> Eff
         '[RunContract, Assert, Waiting, EmulatorControl, EmulatedWalletAPI,
           LogMsg String, Error EmulatorRuntimeError]
         ((), [(String, AssetClass)]))
-> SpecificationEmulatorTrace ()
-> Eff
     '[StartContract, RunContract, Assert, Waiting, EmulatorControl,
       EmulatedWalletAPI, LogMsg String, Error EmulatorRuntimeError]
     ((), [(String, AssetClass)])
forall b c a. (b -> c) -> (a -> b) -> a -> c
. SpecificationEmulatorTrace ()
-> Eff
     '[RunContract, Assert, Waiting, EmulatorControl, EmulatedWalletAPI,
       LogMsg String, Error EmulatorRuntimeError]
     ((), [(String, AssetClass)])
forall w (effs :: [* -> *]) a.
Monoid w =>
Eff (Writer w : effs) a -> Eff effs (a, w)
runWriter (SpecificationEmulatorTrace ()
 -> StateT
      (Map AssetKey (Map String AssetClass))
      EmulatorTrace
      ((), [(String, AssetClass)]))
-> SpecificationEmulatorTrace ()
-> StateT
     (Map AssetKey (Map String AssetClass))
     EmulatorTrace
     ((), [(String, AssetClass)])
forall a b. (a -> b) -> a -> b
$ HandleFun state
-> (SymToken -> AssetClass)
-> ModelState state
-> Action state
-> SpecificationEmulatorTrace ()
forall state.
ContractModel state =>
HandleFun state
-> (SymToken -> AssetClass)
-> ModelState state
-> Action state
-> SpecificationEmulatorTrace ()
perform (Handles state -> HandleFun state
forall s. ContractModel s => Handles s -> HandleFun s
handle Handles state
h') SymToken -> AssetClass
lookup ModelState state
s Action state
cmd
        -- Ensure that each call to `createToken` in the spec corresponds to a call to
        -- `registerToken` during execution
        Bool -> EmulatorMonad () -> EmulatorMonad ()
forall (f :: * -> *). Applicative f => Bool -> f () -> f ()
when (Set String -> Int
forall a. Set a -> Int
Set.size ([String] -> Set String
forall a. Ord a => [a] -> Set a
Set.fromList ([String] -> Set String)
-> ([(String, AssetClass)] -> [String])
-> [(String, AssetClass)]
-> Set String
forall b c a. (b -> c) -> (a -> b) -> a -> c
. ((String, AssetClass) -> String)
-> [(String, AssetClass)] -> [String]
forall a b. (a -> b) -> [a] -> [b]
map (String, AssetClass) -> String
forall a b. (a, b) -> a
fst ([(String, AssetClass)] -> Set String)
-> [(String, AssetClass)] -> Set String
forall a b. (a -> b) -> a -> b
$ [(String, AssetClass)]
result) Int -> Int -> Bool
forall a. Eq a => a -> a -> Bool
/= [(String, AssetClass)] -> Int
forall (t :: * -> *) a. Foldable t => t a -> Int
length [(String, AssetClass)]
result) (EmulatorMonad () -> EmulatorMonad ())
-> EmulatorMonad () -> EmulatorMonad ()
forall a b. (a -> b) -> a -> b
$ do
          String -> EmulatorMonad ()
forall a. HasCallStack => String -> a
error (String -> EmulatorMonad ()) -> String -> EmulatorMonad ()
forall a b. (a -> b) -> a -> b
$ String
"Non-unique registered token in call to perform with tokens: " String -> ShowS
forall a. [a] -> [a] -> [a]
++ [(String, AssetClass)] -> String
forall a. Show a => a -> String
show [(String, AssetClass)]
result
        (Map AssetKey (Map String AssetClass)
 -> Map AssetKey (Map String AssetClass))
-> EmulatorMonad ()
forall s (m :: * -> *). MonadState s m => (s -> s) -> m ()
State.modify (AssetKey
-> Map String AssetClass
-> Map AssetKey (Map String AssetClass)
-> Map AssetKey (Map String AssetClass)
forall k a. Ord k => k -> a -> Map k a -> Map k a
Map.insert AssetKey
v ([(String, AssetClass)] -> Map String AssetClass
forall k a. Ord k => [(k, a)] -> Map k a
Map.fromList [(String, AssetClass)]
result))
        Handles state -> EmulatorMonad (Handles state)
forall (m :: * -> *) a. Monad m => a -> m a
return Handles state
h'
      AssetKey -> ContractMonad state AssetKey
forall (m :: * -> *) a. Monad m => a -> m a
return AssetKey
v
    perform ModelState state
_ (Unilateral w) LookUp
_env = (Handles state -> EmulatorMonad ()) -> ContractMonad state ()
forall state.
(Handles state -> EmulatorMonad ()) -> ContractMonad state ()
runEmulator_ ((Handles state -> EmulatorMonad ()) -> ContractMonad state ())
-> (Handles state -> EmulatorMonad ()) -> ContractMonad state ()
forall a b. (a -> b) -> a -> b
$ \ Handles state
h -> Eff
  '[StartContract, RunContract, Assert, Waiting, EmulatorControl,
    EmulatedWalletAPI, LogMsg String, Error EmulatorRuntimeError]
  ()
-> EmulatorMonad ()
forall (t :: (* -> *) -> * -> *) (m :: * -> *) a.
(MonadTrans t, Monad m) =>
m a -> t m a
lift (Eff
   '[StartContract, RunContract, Assert, Waiting, EmulatorControl,
     EmulatedWalletAPI, LogMsg String, Error EmulatorRuntimeError]
   ()
 -> EmulatorMonad ())
-> Eff
     '[StartContract, RunContract, Assert, Waiting, EmulatorControl,
       EmulatedWalletAPI, LogMsg String, Error EmulatorRuntimeError]
     ()
-> EmulatorMonad ()
forall a b. (a -> b) -> a -> b
$ do
      let insts :: [ContractInstanceId]
insts = Wallet -> Handles state -> [ContractInstanceId]
forall state. Wallet -> Handles state -> [ContractInstanceId]
instancesForOtherWallets Wallet
w Handles state
h
      (ContractInstanceId
 -> Eff
      '[StartContract, RunContract, Assert, Waiting, EmulatorControl,
        EmulatedWalletAPI, LogMsg String, Error EmulatorRuntimeError]
      ())
-> [ContractInstanceId]
-> Eff
     '[StartContract, RunContract, Assert, Waiting, EmulatorControl,
       EmulatedWalletAPI, LogMsg String, Error EmulatorRuntimeError]
     ()
forall (t :: * -> *) (m :: * -> *) a b.
(Foldable t, Monad m) =>
(a -> m b) -> t a -> m ()
mapM_ ContractInstanceId
-> Eff
     '[StartContract, RunContract, Assert, Waiting, EmulatorControl,
       EmulatedWalletAPI, LogMsg String, Error EmulatorRuntimeError]
     ()
forall (effs :: [* -> *]).
Member EmulatorControl effs =>
ContractInstanceId -> Eff effs ()
freezeContractInstance [ContractInstanceId]
insts
      (Wallet -> Bool)
-> Eff
     '[StartContract, RunContract, Assert, Waiting, EmulatorControl,
       EmulatedWalletAPI, LogMsg String, Error EmulatorRuntimeError]
     ()
forall (effs :: [* -> *]).
Member EmulatorControl effs =>
(Wallet -> Bool) -> Eff effs ()
discardWallets (Wallet
w Wallet -> Wallet -> Bool
forall a. Eq a => a -> a -> Bool
/=)
    perform ModelState state
_ (WaitUntil slot) LookUp
_ = (Handles state -> EmulatorMonad ()) -> ContractMonad state ()
forall state.
(Handles state -> EmulatorMonad ()) -> ContractMonad state ()
runEmulator_ ((Handles state -> EmulatorMonad ()) -> ContractMonad state ())
-> (Handles state -> EmulatorMonad ()) -> ContractMonad state ()
forall a b. (a -> b) -> a -> b
$ \ Handles state
_ -> Eff
  '[StartContract, RunContract, Assert, Waiting, EmulatorControl,
    EmulatedWalletAPI, LogMsg String, Error EmulatorRuntimeError]
  ()
-> EmulatorMonad ()
forall (t :: (* -> *) -> * -> *) (m :: * -> *) a.
(MonadTrans t, Monad m) =>
m a -> t m a
lift (Eff
   '[StartContract, RunContract, Assert, Waiting, EmulatorControl,
     EmulatedWalletAPI, LogMsg String, Error EmulatorRuntimeError]
   ()
 -> EmulatorMonad ())
-> (Eff
      '[StartContract, RunContract, Assert, Waiting, EmulatorControl,
        EmulatedWalletAPI, LogMsg String, Error EmulatorRuntimeError]
      Slot
    -> Eff
         '[StartContract, RunContract, Assert, Waiting, EmulatorControl,
           EmulatedWalletAPI, LogMsg String, Error EmulatorRuntimeError]
         ())
-> Eff
     '[StartContract, RunContract, Assert, Waiting, EmulatorControl,
       EmulatedWalletAPI, LogMsg String, Error EmulatorRuntimeError]
     Slot
-> EmulatorMonad ()
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Eff
  '[StartContract, RunContract, Assert, Waiting, EmulatorControl,
    EmulatedWalletAPI, LogMsg String, Error EmulatorRuntimeError]
  Slot
-> Eff
     '[StartContract, RunContract, Assert, Waiting, EmulatorControl,
       EmulatedWalletAPI, LogMsg String, Error EmulatorRuntimeError]
     ()
forall (f :: * -> *) a. Functor f => f a -> f ()
void (Eff
   '[StartContract, RunContract, Assert, Waiting, EmulatorControl,
     EmulatedWalletAPI, LogMsg String, Error EmulatorRuntimeError]
   Slot
 -> EmulatorMonad ())
-> Eff
     '[StartContract, RunContract, Assert, Waiting, EmulatorControl,
       EmulatedWalletAPI, LogMsg String, Error EmulatorRuntimeError]
     Slot
-> EmulatorMonad ()
forall a b. (a -> b) -> a -> b
$ Slot
-> Eff
     '[StartContract, RunContract, Assert, Waiting, EmulatorControl,
       EmulatedWalletAPI, LogMsg String, Error EmulatorRuntimeError]
     Slot
forall (effs :: [* -> *]).
Member Waiting effs =>
Slot -> Eff effs Slot
waitUntilSlot Slot
slot

    postcondition :: ModelState state
-> Action (ModelState state) a -> LookUp -> a -> Bool
postcondition ModelState state
_s Action (ModelState state) a
_cmd LookUp
_env a
_res = Bool
True

    monitoring :: (ModelState state, ModelState state)
-> Action (ModelState state) a
-> LookUp
-> a
-> Property
-> Property
monitoring (ModelState state
s0, ModelState state
s1) (ContractAction _ cmd) LookUp
_env a
_res = (ModelState state, ModelState state)
-> Action state -> Property -> Property
forall state.
ContractModel state =>
(ModelState state, ModelState state)
-> Action state -> Property -> Property
monitoring (ModelState state
s0, ModelState state
s1) Action state
cmd
    monitoring (ModelState state
s0, ModelState state
_) (WaitUntil n@(Slot _n)) LookUp
_ a
_                 =
      String -> [String] -> Property -> Property
forall prop.
Testable prop =>
String -> [String] -> prop -> Property
tabulate String
"Wait interval" (Integer -> Integer -> [String]
forall t. (Show t, Integral t) => t -> t -> [String]
bucket Integer
10 Integer
diff) (Property -> Property)
-> (Property -> Property) -> Property -> Property
forall b c a. (b -> c) -> (a -> b) -> a -> c
.
      String -> [String] -> Property -> Property
forall prop.
Testable prop =>
String -> [String] -> prop -> Property
tabulate String
"Wait until" (Integer -> Integer -> [String]
forall t. (Show t, Integral t) => t -> t -> [String]
bucket Integer
10 Integer
_n)
      where Slot Integer
diff = Slot
n Slot -> Slot -> Slot
forall a. Num a => a -> a -> a
- ModelState state
s0 ModelState state -> Getting Slot (ModelState state) Slot -> Slot
forall s a. s -> Getting a s a -> a
^. Getting Slot (ModelState state) Slot
forall state. Getter (ModelState state) Slot
currentSlot
            bucket :: t -> t -> [String]
bucket t
size t
n | t
n t -> t -> Bool
forall a. Ord a => a -> a -> Bool
< t
size = [ String
"<" String -> ShowS
forall a. [a] -> [a] -> [a]
++ t -> String
forall a. Show a => a -> String
show t
size ]
                          | t
size t -> t -> Bool
forall a. Ord a => a -> a -> Bool
<= t
n
                          , t
n t -> t -> Bool
forall a. Ord a => a -> a -> Bool
< t
sizet -> t -> t
forall a. Num a => a -> a -> a
*t
10 = [t -> t -> String
forall a. (Integral a, Show a) => a -> a -> String
bucketIn t
size t
n]
                          | Bool
otherwise = t -> t -> [String]
bucket (t
sizet -> t -> t
forall a. Num a => a -> a -> a
*t
10) t
n
            bucketIn :: a -> a -> String
bucketIn a
size a
n =
              let b :: a
b = a
n a -> a -> a
forall a. Integral a => a -> a -> a
`div` a
size in
              a -> String
forall a. Show a => a -> String
show (a
ba -> a -> a
forall a. Num a => a -> a -> a
*a
size) String -> ShowS
forall a. [a] -> [a] -> [a]
++ String
"-" String -> ShowS
forall a. [a] -> [a] -> [a]
++ a -> String
forall a. Show a => a -> String
show (a
ba -> a -> a
forall a. Num a => a -> a -> a
*a
sizea -> a -> a
forall a. Num a => a -> a -> a
+(a
size a -> a -> a
forall a. Num a => a -> a -> a
- a
1))
    monitoring (ModelState state, ModelState state)
_ Action (ModelState state) a
_ LookUp
_ a
_ = Property -> Property
forall a. a -> a
id

-- We present a simplified view of test sequences, and DL test cases, so
-- that users do not need to see the variables bound to results.

-- $testCases
--
-- Failing `DL` tests can be rechecked using `withDLTest`. The easiest way to do this is to copy and
-- paste the `DLTest` printed on failure into a source file. For instance, suppose
-- @prop_Finish@ from the `forAllDL` example fails with @`BadPrecondition` ...@. You could copy this
-- into your source file and define the property
--
-- @
-- failedTest :: `DLTest` AuctionState
-- failedTest = `BadPrecondition` ...
--
-- checkFailed :: Property
-- checkFailed = `withMaxSuccess` 1 $ `withDLTest` finishAuction prop_Auction failedTest
-- @
--
-- Now the failing test can be rerun to check if changes code or model has fixed the problem.

-- | A `Actions` is a list of intelligent and sophisticated `Action`s.

-- We include a list of rejected action names.
data Actions s = Actions_ [String] (Smart [Act s])

{-# COMPLETE Actions #-}
pattern Actions :: [Act s] -> Actions s
pattern $bActions :: [Act s] -> Actions s
$mActions :: forall r s. Actions s -> ([Act s] -> r) -> (Void# -> r) -> r
Actions as <- Actions_ _ (Smart _ as) where
  Actions [Act s]
as = [String] -> Smart [Act s] -> Actions s
forall s. [String] -> Smart [Act s] -> Actions s
Actions_ [] (Int -> [Act s] -> Smart [Act s]
forall a. Int -> a -> Smart a
Smart Int
0 [Act s]
as)

data Act s = Bind {Act s -> Var AssetKey
varOf :: Var AssetKey, Act s -> Action s
actionOf :: Action s }
           | NoBind {varOf :: Var AssetKey, actionOf :: Action s}
           | ActWaitUntil (Var ()) Slot

deriving instance ContractModel s => Eq (Act s)

isBind :: Act s -> Bool
isBind :: Act s -> Bool
isBind Bind{} = Bool
True
isBind Act s
_      = Bool
False

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 AssetKey -> Action s -> Act s)
-> [Var AssetKey] -> [Action s] -> [Act s]
forall a b c. (a -> b -> c) -> [a] -> [b] -> [c]
zipWith Var AssetKey -> Action s -> Act s
forall s. Var AssetKey -> Action s -> Act s
NoBind (Int -> Var AssetKey
forall a. Int -> Var a
Var (Int -> Var AssetKey) -> [Int] -> [Var AssetKey]
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> [Int
0..])

varNumOf :: Act s -> Int
varNumOf :: Act s -> Int
varNumOf (ActWaitUntil (Var Int
i) Slot
_) = Int
i
varNumOf Act s
act | Var Int
i <- Act s -> Var AssetKey
forall s. Act s -> Var AssetKey
varOf Act s
act = Int
i

instance ContractModel state => Show (Act state) where
  showsPrec :: Int -> Act state -> ShowS
showsPrec Int
d (Bind (Var Int
i) Action state
a)   = Bool -> ShowS -> ShowS
showParen (Int
d Int -> Int -> Bool
forall a. Ord a => a -> a -> Bool
>= Int
11) (ShowS -> ShowS) -> ShowS -> ShowS
forall a b. (a -> b) -> a -> b
$ String -> ShowS
showString (String
"tok" String -> ShowS
forall a. [a] -> [a] -> [a]
++ Int -> String
forall a. Show a => a -> String
show Int
i String -> ShowS
forall a. [a] -> [a] -> [a]
++ String
" := ") ShowS -> ShowS -> ShowS
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Int -> Action state -> ShowS
forall a. Show a => Int -> a -> ShowS
showsPrec Int
0 Action state
a
  showsPrec Int
d (ActWaitUntil Var ()
_ Slot
n) = Bool -> ShowS -> ShowS
showParen (Int
d Int -> Int -> Bool
forall a. Ord a => a -> a -> Bool
>= Int
11) (ShowS -> ShowS) -> ShowS -> ShowS
forall a b. (a -> b) -> a -> b
$ String -> ShowS
showString (String
"WaitUntil ") ShowS -> ShowS -> ShowS
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Int -> Slot -> ShowS
forall a. Show a => Int -> a -> ShowS
showsPrec Int
11 Slot
n
  showsPrec Int
d (NoBind Var AssetKey
_ Action state
a)       = Int -> Action state -> ShowS
forall a. Show a => Int -> a -> ShowS
showsPrec Int
d Action state
a

instance ContractModel state => Show (Actions state) where
  showsPrec :: Int -> Actions state -> ShowS
showsPrec Int
d (Actions [Act state]
as)
    | Int
dInt -> Int -> Bool
forall a. Ord a => a -> a -> Bool
>Int
10      = (String
"("String -> ShowS
forall a. [a] -> [a] -> [a]
++)ShowS -> ShowS -> ShowS
forall b c a. (b -> c) -> (a -> b) -> a -> c
.Int -> Actions state -> ShowS
forall a. Show a => Int -> a -> ShowS
showsPrec Int
0 ([Act state] -> Actions state
forall s. [Act s] -> Actions s
Actions [Act state]
as)ShowS -> ShowS -> ShowS
forall b c a. (b -> c) -> (a -> b) -> a -> c
.(String
")"String -> ShowS
forall a. [a] -> [a] -> [a]
++)
    | [Act state] -> Bool
forall (t :: * -> *) a. Foldable t => t a -> Bool
null [Act state]
as   = (String
"Actions []"String -> ShowS
forall a. [a] -> [a] -> [a]
++)
    | Bool
otherwise = (String
"Actions \n [" String -> ShowS
forall a. [a] -> [a] -> [a]
++) ShowS -> ShowS -> ShowS
forall b c a. (b -> c) -> (a -> b) -> a -> c
.
                  (ShowS -> ShowS -> ShowS) -> ShowS -> [ShowS] -> ShowS
forall (t :: * -> *) a b.
Foldable t =>
(a -> b -> b) -> b -> t a -> b
foldr ShowS -> ShowS -> ShowS
forall b c a. (b -> c) -> (a -> b) -> a -> c
(.) (Int -> Act state -> ShowS
forall a. Show a => Int -> a -> ShowS
showsPrec Int
0 ([Act state] -> Act state
forall a. [a] -> a
last [Act state]
as) ShowS -> ShowS -> ShowS
forall b c a. (b -> c) -> (a -> b) -> a -> c
. (String
"]"String -> ShowS
forall a. [a] -> [a] -> [a]
++))
                    [Int -> Act state -> ShowS
forall a. Show a => Int -> a -> ShowS
showsPrec Int
0 Act state
a ShowS -> ShowS -> ShowS
forall b c a. (b -> c) -> (a -> b) -> a -> c
. (String
",\n  "String -> ShowS
forall a. [a] -> [a] -> [a]
++) | Act state
a <- [Act state] -> [Act state]
forall a. [a] -> [a]
init [Act state]
as]

instance ContractModel s => Arbitrary (Actions s) where
  arbitrary :: Gen (Actions s)
arbitrary = Actions (ModelState s) -> Actions s
forall s. Actions (ModelState s) -> Actions s
fromStateModelActions (Actions (ModelState s) -> Actions s)
-> Gen (Actions (ModelState s)) -> Gen (Actions s)
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> Gen (Actions (ModelState s))
forall a. Arbitrary a => Gen a
arbitrary
  shrink :: Actions s -> [Actions s]
shrink = (Actions (ModelState s) -> Actions s)
-> [Actions (ModelState s)] -> [Actions s]
forall a b. (a -> b) -> [a] -> [b]
map Actions (ModelState s) -> Actions s
forall s. Actions (ModelState s) -> Actions s
fromStateModelActions ([Actions (ModelState s)] -> [Actions s])
-> (Actions s -> [Actions (ModelState s)])
-> Actions s
-> [Actions s]
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Actions (ModelState s) -> [Actions (ModelState s)]
forall a. Arbitrary a => a -> [a]
shrink (Actions (ModelState s) -> [Actions (ModelState s)])
-> (Actions s -> Actions (ModelState s))
-> Actions s
-> [Actions (ModelState s)]
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Actions s -> Actions (ModelState s)
forall state.
ContractModel state =>
Actions state -> Actions (ModelState state)
toStateModelActions

toStateModelActions :: ContractModel state =>
                        Actions state -> StateModel.Actions (ModelState state)
toStateModelActions :: Actions state -> Actions (ModelState state)
toStateModelActions (Actions_ [String]
rs (Smart Int
k [Act state]
s)) =
  [String]
-> Smart [Step (ModelState state)] -> Actions (ModelState state)
forall state. [String] -> Smart [Step state] -> Actions state
StateModel.Actions_ [String]
rs (Int -> [Step (ModelState state)] -> Smart [Step (ModelState state)]
forall a. Int -> a -> Smart a
Smart Int
k ([Step (ModelState state)] -> Smart [Step (ModelState state)])
-> [Step (ModelState state)] -> Smart [Step (ModelState state)]
forall a b. (a -> b) -> a -> b
$ (Act state -> Step (ModelState state))
-> [Act state] -> [Step (ModelState state)]
forall a b. (a -> b) -> [a] -> [b]
map Act state -> Step (ModelState state)
forall state.
ContractModel state =>
Act state -> Step (ModelState state)
mkStep [Act state]
s)
    where mkStep :: Act state -> Step (ModelState state)
mkStep (ActWaitUntil Var ()
v Slot
n) = Var ()
v Var () -> Action (ModelState state) () -> Step (ModelState state)
forall a state.
(Show a, Typeable a, Eq (Action state a),
 Typeable (Action state a), Show (Action state a)) =>
Var a -> Action state a -> Step state
:= Slot -> Action (ModelState state) ()
forall state. Slot -> Action (ModelState state) ()
WaitUntil Slot
n
          mkStep Act state
act                = Act state -> Var AssetKey
forall s. Act s -> Var AssetKey
varOf Act state
act Var AssetKey
-> Action (ModelState state) AssetKey -> Step (ModelState state)
forall a state.
(Show a, Typeable a, Eq (Action state a),
 Typeable (Action state a), Show (Action state a)) =>
Var a -> Action state a -> Step state
:= Bool -> Action state -> Action (ModelState state) AssetKey
forall state.
Bool -> Action state -> Action (ModelState state) AssetKey
ContractAction (Act state -> Bool
forall s. Act s -> Bool
isBind Act state
act) (Act state -> Action state
forall s. Act s -> Action s
actionOf Act state
act)

fromStateModelActions :: StateModel.Actions (ModelState s) -> Actions s
fromStateModelActions :: Actions (ModelState s) -> Actions s
fromStateModelActions (StateModel.Actions_ [String]
rs (Smart Int
k [Step (ModelState s)]
s)) =
  [String] -> Smart [Act s] -> Actions s
forall s. [String] -> Smart [Act s] -> Actions s
Actions_ [String]
rs (Int -> [Act s] -> Smart [Act s]
forall a. Int -> a -> Smart a
Smart Int
k ([Maybe (Act s)] -> [Act s]
forall a. [Maybe a] -> [a]
catMaybes ([Maybe (Act s)] -> [Act s]) -> [Maybe (Act s)] -> [Act s]
forall a b. (a -> b) -> a -> b
$ (Step (ModelState s) -> Maybe (Act s))
-> [Step (ModelState s)] -> [Maybe (Act s)]
forall a b. (a -> b) -> [a] -> [b]
map Step (ModelState s) -> Maybe (Act s)
forall s. Step (ModelState s) -> Maybe (Act s)
mkAct [Step (ModelState s)]
s))
  where
    mkAct :: Step (ModelState s) -> Maybe (Act s)
    mkAct :: Step (ModelState s) -> Maybe (Act s)
mkAct (Var Int
i := ContractAction b act) = Act s -> Maybe (Act s)
forall a. a -> Maybe a
Just (Act s -> Maybe (Act s)) -> Act s -> Maybe (Act s)
forall a b. (a -> b) -> a -> b
$ if Bool
b then Var AssetKey -> Action s -> Act s
forall s. Var AssetKey -> Action s -> Act s
Bind (Int -> Var AssetKey
forall a. Int -> Var a
Var Int
i) Action s
act else Var AssetKey -> Action s -> Act s
forall s. Var AssetKey -> Action s -> Act s
NoBind (Int -> Var AssetKey
forall a. Int -> Var a
Var Int
i) Action s
act
    mkAct (Var a
v     := WaitUntil n)          = Act s -> Maybe (Act s)
forall a. a -> Maybe a
Just (Act s -> Maybe (Act s)) -> Act s -> Maybe (Act s)
forall a b. (a -> b) -> a -> b
$ Var () -> Slot -> Act s
forall s. Var () -> Slot -> Act s
ActWaitUntil Var a
Var ()
v Slot
n
    mkAct (Var a
_     := Unilateral{})         = Maybe (Act s)
forall a. Maybe a
Nothing

-- | An instance of a `DL` scenario generated by `forAllDL`. It is turned into a `Actions` before
--   being passed to the property argument of `forAllDL`, but in case of a failure the generated
--   `DLTest` is printed. This test can then be rerun using `withDLTest`.
data DLTest state =
    BadPrecondition [TestStep state] [FailedStep state] state
        -- ^ An explicit `action` failed its precondition (@[Action](#v:Action)@), or an assertion failed (`Assert`).
        --   There is a list of `FailedStep`s because there may be multiple branches
        --   (`Control.Applicative.<|>`) in the scenario that fail. Contains the contract state at
        --   the point of failure.
  | Looping         [TestStep state]
        -- ^ Test case generation from the `DL` scenario failed to terminate. See `stopping` for
        --   more information.
  | Stuck           [TestStep state] state
        -- ^ There are no possible next steps in the scenario. Corresponds to a call to
        --  `Control.Applicative.empty`. Contains the contract state at the point where the scenario
        --  got stuck.
  | DLScript        [TestStep state]
        -- ^ A successfully generated test case.

-- | This type captures the two different kinds of `BadPrecondition`s that can occur.
data FailedStep state = Action (Act state)
                        -- ^ A call to `action` that does not satisfy its `precondition`.
                      | Assert String
                        -- ^ A call to `DL.assert` or `assertModel` failed, or a `fail` in the `DL`
                        --   monad. Stores the string argument of the corresponding call.

deriving instance ContractModel s => Show (FailedStep s)
instance ContractModel s => Eq (FailedStep s) where
  Assert String
s == :: FailedStep s -> FailedStep s -> Bool
== Assert String
s'                                   = String
s String -> String -> Bool
forall a. Eq a => a -> a -> Bool
== String
s'
  Action (ActWaitUntil Var ()
_ Slot
n) == Action (ActWaitUntil Var ()
_ Slot
n') = Slot
n Slot -> Slot -> Bool
forall a. Eq a => a -> a -> Bool
== Slot
n'
  Action Act s
a == Action Act s
a'                                   = Act s -> Action s
forall s. Act s -> Action s
actionOf Act s
a Action s -> Action s -> Bool
forall a. Eq a => a -> a -> Bool
== Act s -> Action s
forall s. Act s -> Action s
actionOf Act s
a'
  FailedStep s
_ == FailedStep s
_                                                  = Bool
False

instance ContractModel s => Show (DLTest s) where
    show :: DLTest s -> String
show (BadPrecondition [TestStep s]
as [FailedStep s]
bads s
s) =
        [String] -> String
unlines ([String] -> String) -> [String] -> String
forall a b. (a -> b) -> a -> b
$ [String
"BadPrecondition"] [String] -> [String] -> [String]
forall a. [a] -> [a] -> [a]
++
                  [String] -> [String]
bracket ((TestStep s -> String) -> [TestStep s] -> [String]
forall a b. (a -> b) -> [a] -> [b]
map TestStep s -> String
forall a. Show a => a -> String
show [TestStep s]
as) [String] -> [String] -> [String]
forall a. [a] -> [a] -> [a]
++
                  [String
"  " String -> ShowS
forall a. [a] -> [a] -> [a]
++ [FailedStep s] -> String
forall a. Show a => a -> String
show ([FailedStep s] -> [FailedStep s]
forall a. Eq a => [a] -> [a]
nub [FailedStep s]
bads)] [String] -> [String] -> [String]
forall a. [a] -> [a] -> [a]
++
                  [String
"  " String -> ShowS
forall a. [a] -> [a] -> [a]
++ Int -> s -> ShowS
forall a. Show a => Int -> a -> ShowS
showsPrec Int
11 s
s String
""]
    show (Looping [TestStep s]
as) =
        [String] -> String
unlines ([String] -> String) -> [String] -> String
forall a b. (a -> b) -> a -> b
$ [String
"Looping"] [String] -> [String] -> [String]
forall a. [a] -> [a] -> [a]
++ [String] -> [String]
bracket ((TestStep s -> String) -> [TestStep s] -> [String]
forall a b. (a -> b) -> [a] -> [b]
map TestStep s -> String
forall a. Show a => a -> String
show [TestStep s]
as)
    show (Stuck [TestStep s]
as s
s) =
        [String] -> String
unlines ([String] -> String) -> [String] -> String
forall a b. (a -> b) -> a -> b
$ [String
"Stuck"] [String] -> [String] -> [String]
forall a. [a] -> [a] -> [a]
++ [String] -> [String]
bracket ((TestStep s -> String) -> [TestStep s] -> [String]
forall a b. (a -> b) -> [a] -> [b]
map TestStep s -> String
forall a. Show a => a -> String
show [TestStep s]
as) [String] -> [String] -> [String]
forall a. [a] -> [a] -> [a]
++ [String
"  " String -> ShowS
forall a. [a] -> [a] -> [a]
++ Int -> s -> ShowS
forall a. Show a => Int -> a -> ShowS
showsPrec Int
11 s
s String
""]
    show (DLScript [TestStep s]
as) =
        [String] -> String
unlines ([String] -> String) -> [String] -> String
forall a b. (a -> b) -> a -> b
$ [String
"DLScript"] [String] -> [String] -> [String]
forall a. [a] -> [a] -> [a]
++ [String] -> [String]
bracket ((TestStep s -> String) -> [TestStep s] -> [String]
forall a b. (a -> b) -> [a] -> [b]
map TestStep s -> String
forall a. Show a => a -> String
show [TestStep s]
as)

bracket :: [String] -> [String]
bracket :: [String] -> [String]
bracket []  = [String
"  []"]
bracket [String
s] = [String
"  [" String -> ShowS
forall a. [a] -> [a] -> [a]
++ String
s String -> ShowS
forall a. [a] -> [a] -> [a]
++ String
"]"]
bracket (String
first:[String]
rest) = [String
"  ["String -> ShowS
forall a. [a] -> [a] -> [a]
++String
firstString -> ShowS
forall a. [a] -> [a] -> [a]
++String
", "] [String] -> [String] -> [String]
forall a. [a] -> [a] -> [a]
++
                       ShowS -> [String] -> [String]
forall a b. (a -> b) -> [a] -> [b]
map ((String
"   "String -> ShowS
forall a. [a] -> [a] -> [a]
++)ShowS -> ShowS -> ShowS
forall b c a. (b -> c) -> (a -> b) -> a -> c
.(String -> ShowS
forall a. [a] -> [a] -> [a]
++String
", ")) ([String] -> [String]
forall a. [a] -> [a]
init [String]
rest) [String] -> [String] -> [String]
forall a. [a] -> [a] -> [a]
++
                       [String
"   " String -> ShowS
forall a. [a] -> [a] -> [a]
++ [String] -> String
forall a. [a] -> a
last [String]
rest String -> ShowS
forall a. [a] -> [a] -> [a]
++ String
"]"]

-- | One step of a test case. Either an `Action` (`Do`) or a value generated by a `DL.forAllQ`
--   (`Witness`). When a `DLTest` is turned into a `Actions` to be executed the witnesses are
--   stripped away.
data TestStep s = Do (Act s)
                | forall a. (Eq a, Show a, Typeable a) => Witness a

instance ContractModel s => Show (TestStep s) where
  show :: TestStep s -> String
show (Do Act s
act)    = String
"Do $ "String -> ShowS
forall a. [a] -> [a] -> [a]
++Act s -> String
forall a. Show a => a -> String
show Act s
act
  show (Witness a
a) = String
"Witness ("String -> ShowS
forall a. [a] -> [a] -> [a]
++a -> String
forall a. Show a => a -> String
show a
aString -> ShowS
forall a. [a] -> [a] -> [a]
++String
" :: "String -> ShowS
forall a. [a] -> [a] -> [a]
++TypeRep -> String
forall a. Show a => a -> String
show (a -> TypeRep
forall a. Typeable a => a -> TypeRep
typeOf a
a)String -> ShowS
forall a. [a] -> [a] -> [a]
++String
")"

toDLTest :: ContractModel state =>
              DLTest state -> DL.DynLogicTest (ModelState state)
toDLTest :: DLTest state -> DynLogicTest (ModelState state)
toDLTest (BadPrecondition [TestStep state]
steps [FailedStep state]
acts state
s) =
  [TestStep (ModelState state)]
-> [Any (Action (ModelState state))]
-> ModelState state
-> DynLogicTest (ModelState state)
forall s. [TestStep s] -> [Any (Action s)] -> s -> DynLogicTest s
DL.BadPrecondition ([TestStep state] -> [TestStep (ModelState state)]
forall state.
ContractModel state =>
[TestStep state] -> [TestStep (ModelState state)]
toDLTestSteps [TestStep state]
steps) ((FailedStep state -> Any (Action (ModelState state)))
-> [FailedStep state] -> [Any (Action (ModelState state))]
forall a b. (a -> b) -> [a] -> [b]
map FailedStep state -> Any (Action (ModelState state))
forall state.
ContractModel state =>
FailedStep state -> Any (Action (ModelState state))
conv [FailedStep state]
acts) (state -> ModelState state
forall state. state -> ModelState state
dummyModelState state
s)
    where
        conv :: FailedStep state -> Any (Action (ModelState state))
conv (Action (ActWaitUntil Var ()
_ Slot
n)) = Action (ModelState state) () -> Any (Action (ModelState state))
forall a (f :: * -> *).
(Show a, Typeable a, Eq (f a)) =>
f a -> Any f
Some (Slot -> Action (ModelState state) ()
forall state. Slot -> Action (ModelState state) ()
WaitUntil Slot
n)
        conv (Action Act state
a)                  = Action (ModelState state) AssetKey
-> Any (Action (ModelState state))
forall a (f :: * -> *).
(Show a, Typeable a, Eq (f a)) =>
f a -> Any f
Some (Bool -> Action state -> Action (ModelState state) AssetKey
forall state.
Bool -> Action state -> Action (ModelState state) AssetKey
ContractAction (Act state -> Bool
forall s. Act s -> Bool
isBind Act state
a) (Act state -> Action state
forall s. Act s -> Action s
actionOf Act state
a))
        conv (Assert String
e)                  = String -> Any (Action (ModelState state))
forall (f :: * -> *). String -> Any f
Error String
e
toDLTest (Looping [TestStep state]
steps) =
  [TestStep (ModelState state)] -> DynLogicTest (ModelState state)
forall s. [TestStep s] -> DynLogicTest s
DL.Looping ([TestStep state] -> [TestStep (ModelState state)]
forall state.
ContractModel state =>
[TestStep state] -> [TestStep (ModelState state)]
toDLTestSteps [TestStep state]
steps)
toDLTest (Stuck [TestStep state]
steps state
s) =
  [TestStep (ModelState state)]
-> ModelState state -> DynLogicTest (ModelState state)
forall s. [TestStep s] -> s -> DynLogicTest s
DL.Stuck ([TestStep state] -> [TestStep (ModelState state)]
forall state.
ContractModel state =>
[TestStep state] -> [TestStep (ModelState state)]
toDLTestSteps [TestStep state]
steps) (state -> ModelState state
forall state. state -> ModelState state
dummyModelState state
s)
toDLTest (DLScript [TestStep state]
steps) =
  [TestStep (ModelState state)] -> DynLogicTest (ModelState state)
forall s. [TestStep s] -> DynLogicTest s
DL.DLScript ([TestStep state] -> [TestStep (ModelState state)]
forall state.
ContractModel state =>
[TestStep state] -> [TestStep (ModelState state)]
toDLTestSteps [TestStep state]
steps)

toDLTestSteps :: ContractModel state =>
                   [TestStep state] -> [DL.TestStep (ModelState state)]
toDLTestSteps :: [TestStep state] -> [TestStep (ModelState state)]
toDLTestSteps [TestStep state]
steps = (TestStep state -> TestStep (ModelState state))
-> [TestStep state] -> [TestStep (ModelState state)]
forall a b. (a -> b) -> [a] -> [b]
map TestStep state -> TestStep (ModelState state)
forall state.
ContractModel state =>
TestStep state -> TestStep (ModelState state)
toDLTestStep [TestStep state]
steps

toDLTestStep :: ContractModel state =>
                  TestStep state -> DL.TestStep (ModelState state)
toDLTestStep :: TestStep state -> TestStep (ModelState state)
toDLTestStep (Do (ActWaitUntil Var ()
v Slot
n)) = Step (ModelState state) -> TestStep (ModelState state)
forall s. Step s -> TestStep s
DL.Do (Step (ModelState state) -> TestStep (ModelState state))
-> Step (ModelState state) -> TestStep (ModelState state)
forall a b. (a -> b) -> a -> b
$ Var ()
v Var () -> Action (ModelState state) () -> Step (ModelState state)
forall a state.
(Show a, Typeable a, Eq (Action state a),
 Typeable (Action state a), Show (Action state a)) =>
Var a -> Action state a -> Step state
StateModel.:= Slot -> Action (ModelState state) ()
forall state. Slot -> Action (ModelState state) ()
WaitUntil Slot
n
toDLTestStep (Do Act state
act)                = Step (ModelState state) -> TestStep (ModelState state)
forall s. Step s -> TestStep s
DL.Do (Step (ModelState state) -> TestStep (ModelState state))
-> Step (ModelState state) -> TestStep (ModelState state)
forall a b. (a -> b) -> a -> b
$ Act state -> Var AssetKey
forall s. Act s -> Var AssetKey
varOf Act state
act Var AssetKey
-> Action (ModelState state) AssetKey -> Step (ModelState state)
forall a state.
(Show a, Typeable a, Eq (Action state a),
 Typeable (Action state a), Show (Action state a)) =>
Var a -> Action state a -> Step state
StateModel.:= Bool -> Action state -> Action (ModelState state) AssetKey
forall state.
Bool -> Action state -> Action (ModelState state) AssetKey
ContractAction (Act state -> Bool
forall s. Act s -> Bool
isBind Act state
act) (Act state -> Action state
forall s. Act s -> Action s
actionOf Act state
act)
toDLTestStep (Witness a
a)             = a -> TestStep (ModelState state)
forall s a. (Eq a, Show a, Typeable a) => a -> TestStep s
DL.Witness a
a

fromDLTest :: forall s. DL.DynLogicTest (ModelState s) -> DLTest s
fromDLTest :: DynLogicTest (ModelState s) -> DLTest s
fromDLTest (DL.BadPrecondition [TestStep (ModelState s)]
steps [Any (Action (ModelState s))]
acts ModelState s
s) =
  [TestStep s] -> [FailedStep s] -> s -> DLTest s
forall state.
[TestStep state] -> [FailedStep state] -> state -> DLTest state
BadPrecondition ([TestStep (ModelState s)] -> [TestStep s]
forall state. [TestStep (ModelState state)] -> [TestStep state]
fromDLTestSteps [TestStep (ModelState s)]
steps) ((Any (Action (ModelState s)) -> [FailedStep s])
-> [Any (Action (ModelState s))] -> [FailedStep s]
forall (t :: * -> *) a b. Foldable t => (a -> [b]) -> t a -> [b]
concatMap Any (Action (ModelState s)) -> [FailedStep s]
conv [Any (Action (ModelState s))]
acts) (ModelState s -> s
forall state. ModelState state -> state
_contractState ModelState s
s)
  where conv :: Any (StateModel.Action (ModelState s)) -> [FailedStep s]
        conv :: Any (Action (ModelState s)) -> [FailedStep s]
conv (Some (ContractAction _ act)) = [Act s -> FailedStep s
forall state. Act state -> FailedStep state
Action (Act s -> FailedStep s) -> Act s -> FailedStep s
forall a b. (a -> b) -> a -> b
$ Var AssetKey -> Action s -> Act s
forall s. Var AssetKey -> Action s -> Act s
NoBind (Int -> Var AssetKey
forall a. Int -> Var a
Var Int
0) Action s
act]
        conv (Some (WaitUntil n))          = [Act s -> FailedStep s
forall state. Act state -> FailedStep state
Action (Act s -> FailedStep s) -> Act s -> FailedStep s
forall a b. (a -> b) -> a -> b
$ Var () -> Slot -> Act s
forall s. Var () -> Slot -> Act s
ActWaitUntil (Int -> Var ()
forall a. Int -> Var a
Var Int
0) Slot
n]
        conv (Some Unilateral{})           = []
        conv (Error String
e)                     = [String -> FailedStep s
forall state. String -> FailedStep state
Assert String
e]
fromDLTest (DL.Looping [TestStep (ModelState s)]
steps) =
  [TestStep s] -> DLTest s
forall state. [TestStep state] -> DLTest state
Looping ([TestStep (ModelState s)] -> [TestStep s]
forall state. [TestStep (ModelState state)] -> [TestStep state]
fromDLTestSteps [TestStep (ModelState s)]
steps)
fromDLTest (DL.Stuck [TestStep (ModelState s)]
steps ModelState s
s) =
  [TestStep s] -> s -> DLTest s
forall state. [TestStep state] -> state -> DLTest state
Stuck ([TestStep (ModelState s)] -> [TestStep s]
forall state. [TestStep (ModelState state)] -> [TestStep state]
fromDLTestSteps [TestStep (ModelState s)]
steps) (ModelState s -> s
forall state. ModelState state -> state
_contractState ModelState s
s)
fromDLTest (DL.DLScript [TestStep (ModelState s)]
steps) =
  [TestStep s] -> DLTest s
forall state. [TestStep state] -> DLTest state
DLScript ([TestStep (ModelState s)] -> [TestStep s]
forall state. [TestStep (ModelState state)] -> [TestStep state]
fromDLTestSteps [TestStep (ModelState s)]
steps)

fromDLTestSteps :: [DL.TestStep (ModelState state)] -> [TestStep state]
fromDLTestSteps :: [TestStep (ModelState state)] -> [TestStep state]
fromDLTestSteps [TestStep (ModelState state)]
steps = (TestStep (ModelState state) -> [TestStep state])
-> [TestStep (ModelState state)] -> [TestStep state]
forall (t :: * -> *) a b. Foldable t => (a -> [b]) -> t a -> [b]
concatMap TestStep (ModelState state) -> [TestStep state]
forall state. TestStep (ModelState state) -> [TestStep state]
fromDLTestStep [TestStep (ModelState state)]
steps

fromDLTestStep :: DL.TestStep (ModelState state) -> [TestStep state]
fromDLTestStep :: TestStep (ModelState state) -> [TestStep state]
fromDLTestStep (DL.Do (Var a
v := ContractAction b act)) = [Act state -> TestStep state
forall s. Act s -> TestStep s
Do (Act state -> TestStep state) -> Act state -> TestStep state
forall a b. (a -> b) -> a -> b
$ if Bool
b then Var AssetKey -> Action state -> Act state
forall s. Var AssetKey -> Action s -> Act s
Bind Var a
Var AssetKey
v Action state
act else Var AssetKey -> Action state -> Act state
forall s. Var AssetKey -> Action s -> Act s
NoBind Var a
Var AssetKey
v Action state
act]
fromDLTestStep (DL.Do (Var a
v := WaitUntil n))          = [Act state -> TestStep state
forall s. Act s -> TestStep s
Do (Act state -> TestStep state) -> Act state -> TestStep state
forall a b. (a -> b) -> a -> b
$ Var () -> Slot -> Act state
forall s. Var () -> Slot -> Act s
ActWaitUntil Var a
Var ()
v Slot
n]
fromDLTestStep (DL.Do (Var a
_ := Unilateral{}))         = []
fromDLTestStep (DL.Witness a
a)                      = [a -> TestStep state
forall s a. (Eq a, Show a, Typeable a) => a -> TestStep s
Witness a
a]

-- | Run a specific `DLTest`. Typically this test comes from a failed run of `forAllDL`
--   applied to the given `DL` scenario and property. Useful to check if a particular problem has
--   been fixed after updating the code or the model.
withDLTest :: (ContractModel state, Testable prop)
           => DL state ()              -- ^ The `DL` scenario
           -> (Actions state -> prop)   -- ^ The property. Typically a call to `propRunActions_`
           -> DLTest state             -- ^ The specific test case to run
           -> Property
withDLTest :: DL state () -> (Actions state -> prop) -> DLTest state -> Property
withDLTest DL state ()
dl Actions state -> prop
prop DLTest state
test = DL state ()
-> (Actions (ModelState state) -> prop)
-> DynLogicTest (ModelState state)
-> Property
forall s a.
(DynLogicModel s, Testable a) =>
DL s () -> (Actions s -> a) -> DynLogicTest s -> Property
DL.withDLTest DL state ()
dl (Actions state -> prop
prop (Actions state -> prop)
-> (Actions (ModelState state) -> Actions state)
-> Actions (ModelState state)
-> prop
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Actions (ModelState state) -> Actions state
forall s. Actions (ModelState s) -> Actions s
fromStateModelActions) (DLTest state -> DynLogicTest (ModelState state)
forall state.
ContractModel state =>
DLTest state -> DynLogicTest (ModelState state)
toDLTest DLTest state
test)

-- $dynamicLogic
--
-- Test scenarios are described in the `DL` monad (based on dynamic logic) which lets you freely mix
-- random sequences of actions (`anyAction`, `anyActions_`, `anyActions`) with specific
-- actions (`action`). It also supports checking properties of the model state (`DL.assert`,
-- `assertModel`), and random generation (`DL.forAllQ`).
--
-- For instance, a unit test for a simple auction contract might look something like this:
--
-- @
--  unitTest :: `DL` AuctionState ()
--  unitTest = do
--      `action` $ Bid w1 100
--      `action` $ Bid w2 150
--      `action` $ Wait endSlot
--      `action` $ Collect
-- @
--
--  and could easily be extended with some randomly generated values
--
-- @
--  unitTest :: `DL` AuctionState ()
--  unitTest = do
--      bid <- `forAllQ` $ `chooseQ` (1, 100)
--      `action` $ Bid w1 bid
--      `action` $ Bid w2 (bid + 50)
--      `action` $ Wait endSlot
--      `action` $ Collect
-- @
--
-- More interesting scenarios can be constructed by mixing random and fixed sequences. The following
-- checks that you can always finish an auction after which point there are no funds locked by the
-- contract:
--
-- @
-- finishAuction :: `DL` AuctionState ()
-- finishAuction = do
--   `anyActions_`
--   `action` $ Wait endSlot
--   `action` $ Collect
--   `assertModel` "Funds are locked!" (`Ledger.Value.isZero` . `lockedValue`)
-- @
--
-- `DL` scenarios are turned into QuickCheck properties using `forAllDL`.

-- $dynamicLogic_errors
--
-- In addition to failing the check that the emulator run matches the model, there are a few other
-- ways that test scenarios can fail:
--
-- * an explicit `action` does not satisfy its `precondition`
-- * a failed `DL.assert` or `assertModel`, or a monad `fail`
-- * an `Control.Applicative.empty` set of `Control.Applicative.Alternative`s
-- * the scenario fails to terminate (see `stopping`)
--
-- All of these occur at test case generation time, and thus do not directly say anything about the
-- contract implementation. However, together with the check that the model agrees with the emulator
-- they indirectly imply properties of the implementation. An advantage of this is that `DL` test
-- scenarios can be checked without running the contract through the emulator, which is much much
-- faster. For instance,
--
-- @
-- prop_FinishModel = `forAllDL` finishAuction $ const True
-- @
--
-- would check that the model does not think there will be any locked funds after the auction is
-- finished. Once this property passes, one can run the slower property that also checks that the
-- emulator agrees.

-- | The monad for writing test scenarios. It supports non-deterministic choice through
--   `Control.Applicative.Alternative`, failure with `MonadFail`, and access to the model state
--   through `GetModelState`. It is lazy, so scenarios can be potentially infinite, although the
--   probability of termination needs to be high enough that concrete test cases are always finite.
--   See `stopping` for more information on termination.
type DL state = DL.DL (ModelState state)

-- | Generate a specific action. Fails if the action's `precondition` is not satisfied.
action :: ContractModel state => Action state -> DL state ()
action :: Action state -> DL state ()
action Action state
cmd = do
  ModelState state
s <- DL (ModelState state) (ModelState state)
forall (m :: * -> *).
GetModelState m =>
m (ModelState (StateType m))
getModelState
  Action (ModelState state) AssetKey -> DL state ()
forall a s.
(Show a, Typeable a, Eq (Action s a)) =>
Action s a -> DL s ()
DL.action (ModelState state
-> Action state -> Action (ModelState state) AssetKey
forall state.
ContractModel state =>
ModelState state
-> Action state -> Action (ModelState state) AssetKey
contractAction ModelState state
s Action state
cmd)

-- | Generate a specific action. Fails if the action's `precondition` is not satisfied.
waitUntilDL :: ContractModel state => Slot -> DL state ()
waitUntilDL :: Slot -> DL state ()
waitUntilDL = Action (ModelState state) () -> DL state ()
forall a s.
(Show a, Typeable a, Eq (Action s a)) =>
Action s a -> DL s ()
DL.action (Action (ModelState state) () -> DL state ())
-> (Slot -> Action (ModelState state) ()) -> Slot -> DL state ()
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Slot -> Action (ModelState state) ()
forall state. Slot -> Action (ModelState state) ()
WaitUntil

-- | Generate a random action using `arbitraryAction`. The generated action is guaranteed to satisfy
--   its `precondition`. Fails with `Stuck` if no action satisfying the precondition can be found
--   after 100 attempts.
anyAction :: DL state ()
anyAction :: DL state ()
anyAction = DL state ()
forall s. DL s ()
DL.anyAction

-- | Generate a sequence of random actions using `arbitraryAction`. All actions satisfy their
--   `precondition`s. The argument is the expected number of actions in the sequence chosen from a
--   geometric distribution, unless in the `stopping` stage, in which case as few actions as
--   possible are generated.
anyActions :: Int -> DL state ()
anyActions :: Int -> DL state ()
anyActions = Int -> DL state ()
forall s. Int -> DL s ()
DL.anyActions

-- | Generate a sequence of random actions using `arbitraryAction`. All actions satisfy their
--   `precondition`s. Actions are generated until the `stopping` stage is reached.
anyActions_ :: DL state ()
anyActions_ :: DL state ()
anyActions_ = DL state ()
forall s. DL s ()
DL.anyActions_

-- | Test case generation from `DL` scenarios have a target length of the action sequence to be
--   generated that is based on the QuickCheck size parameter (see `sized`). However, given that
--   scenarios can contain explicit `action`s it might not be possible to stop the scenario once the
--   target length has been reached.
--
--   Instead, once the target number of actions have been reached, generation goes into the
--   /stopping/ phase. In this phase branches starting with `stopping` are preferred, if possible.
--   Conversely, before the stopping phase, branches starting with `stopping`
--   are avoided unless there are no other possible choices.
--
--   For example, here is the definition of `anyActions_`:
--
-- @
-- `anyActions_` = `stopping` `Control.Applicative.<|>` (`anyAction` >> `anyActions_`)
-- @
--
--   The effect of this definition is that the second branch will be taken until the desired number
--   of actions have been generated, at which point the `stopping` branch will be taken and
--   generation stops (or continues with whatever comes after the `anyActions_` call).
--
--   Now, it might not be possible, or too hard, to find a way to terminate a scenario. For
--   instance, this scenario has no finite test cases:
--
-- @
-- looping = `anyAction` >> looping
-- @
--
--   To prevent test case generation from looping, if a scenario has not terminated after generating
--   @2 * n + 20@ actions, where @n@ is when the stopping phase kicks in, generation fails with a
--   `Looping` error.
stopping :: DL state ()
stopping :: DL state ()
stopping = DL state ()
forall s. DL s ()
DL.stopping

-- | By default, `Control.Applicative.Alternative` choice (`Control.Applicative.<|>`) picks among
--   the next actions with equal probability. So, for instance, this code chooses between the actions
--   @a@, @b@ and @c@, with a probability @1/3@ of choosing each:
--
-- @
-- unbiasedChoice a b c = `action` a `Control.Applicative.<|>` `action` b `Control.Applicative.<|>` `action` c
-- @
--
--   To change this you can use `weight`, which multiplies the
--   relative probability of picking a branch by the given number.
--
--   For instance, the following scenario picks the action @a@ with probability @2/3@ and the action
--   @b@ with probability @1/3@:
--
-- @
-- biasedChoice a b = `weight` 2 (`action` a) `Control.Applicative.<|>` `weight` (`action` b)
-- @
--
--   Calls to `weight` need to appear at the top-level after a choice, preceding any actions
--   (`action`/`anyAction`) or random generation (`forAllQ`), or they will have no effect.
weight :: Double -> DL state ()
weight :: Double -> DL state ()
weight = Double -> DL state ()
forall s. Double -> DL s ()
DL.weight

-- | The `monitor` function allows you to collect statistics of your testing using QuickCheck
--   functions like `Test.QuickCheck.label`, `Test.QuickCheck.collect`, `Test.QuickCheck.classify`,
--   and `Test.QuickCheck.tabulate`. See also the `monitoring` method of `ContractModel` which is
--   called for all actions in a test case (regardless of whether they are generated by an explicit
--   `action` or an `anyAction`).
monitor :: (Property -> Property) -> DL state ()
monitor :: (Property -> Property) -> DL state ()
monitor = (Property -> Property) -> DL state ()
forall s. (Property -> Property) -> DL s ()
DL.monitorDL

-- | Fail unless the given predicate holds of the model state.
--
--   Equivalent to
--
-- @
-- assertModel msg p = do
--   s <- `getModelState`
--   `DL.assert` msg (p s)
-- @
assertModel :: String -> (ModelState state -> Bool) -> DL state ()
assertModel :: String -> (ModelState state -> Bool) -> DL state ()
assertModel = String -> (ModelState state -> Bool) -> DL state ()
forall s. String -> (s -> Bool) -> DL s ()
DL.assertModel

-- | Turn a `DL` scenario into a QuickCheck property. Generates a random `Actions` matching the
--   scenario and feeds it to the given property. The property can be a full property running the
--   emulator and checking the results, defined using `propRunActions_`, `propRunActions`, or
--   `propRunActionsWithOptions`. Assuming a model for an auction contract and `DL` scenario that
--   checks that you can always complete the auction, you can write:
--
-- @
-- finishAuction :: `DL` AuctionState ()
-- prop_Auction  = `propRunActions_` handles
--   where handles = ...
-- prop_Finish = `forAllDL` finishAuction prop_Auction
-- @
--
--   However, there is also value in a property that does not run the emulator at all:
--
-- @
-- prop_FinishModel = `forAllDL` finishAuction $ const True
-- @
--
--   This will check all the assertions and other failure conditions of the `DL` scenario very
--   quickly. Once this property passes a large number of tests, you can run the full property
--   checking that the model agrees with reality.
forAllDL :: (ContractModel state, Testable p) => DL state () -> (Actions state -> p) -> Property
forAllDL :: DL state () -> (Actions state -> p) -> Property
forAllDL DL state ()
dl Actions state -> p
prop = (DLTest state -> DynLogicTest (ModelState state))
-> (DynLogicTest (ModelState state) -> DLTest state)
-> (Actions (ModelState state) -> Actions state)
-> DL state ()
-> (Actions state -> p)
-> Property
forall s a rep srep.
(DynLogicModel s, Testable a, Show rep) =>
(rep -> DynLogicTest s)
-> (DynLogicTest s -> rep)
-> (Actions s -> srep)
-> DL s ()
-> (srep -> a)
-> Property
DL.forAllMappedDL DLTest state -> DynLogicTest (ModelState state)
forall state.
ContractModel state =>
DLTest state -> DynLogicTest (ModelState state)
toDLTest DynLogicTest (ModelState state) -> DLTest state
forall s. DynLogicTest (ModelState s) -> DLTest s
fromDLTest Actions (ModelState state) -> Actions state
forall s. Actions (ModelState s) -> Actions s
fromStateModelActions DL state ()
dl Actions state -> p
prop

forAllDL_ :: (ContractModel state, Testable p) => DL state () -> (Actions state -> p) -> Property
forAllDL_ :: DL state () -> (Actions state -> p) -> Property
forAllDL_ DL state ()
dl Actions state -> p
prop = (DLTest state -> DynLogicTest (ModelState state))
-> (DynLogicTest (ModelState state) -> DLTest state)
-> (Actions (ModelState state) -> Actions state)
-> DL state ()
-> (Actions state -> p)
-> Property
forall s a rep srep.
(DynLogicModel s, Testable a, Show rep) =>
(rep -> DynLogicTest s)
-> (DynLogicTest s -> rep)
-> (Actions s -> srep)
-> DL s ()
-> (srep -> a)
-> Property
DL.forAllMappedDL_ DLTest state -> DynLogicTest (ModelState state)
forall state.
ContractModel state =>
DLTest state -> DynLogicTest (ModelState state)
toDLTest DynLogicTest (ModelState state) -> DLTest state
forall s. DynLogicTest (ModelState s) -> DLTest s
fromDLTest Actions (ModelState state) -> Actions state
forall s. Actions (ModelState s) -> Actions s
fromStateModelActions DL state ()
dl Actions state -> p
prop

forAllUniqueDL :: (ContractModel state, Testable p) => Int -> ModelState state -> DL state () -> (Actions state -> p) -> Property
forAllUniqueDL :: Int
-> ModelState state
-> DL state ()
-> (Actions state -> p)
-> Property
forAllUniqueDL Int
nextVar ModelState state
state DL state ()
dl Actions state -> p
prop = Int
-> ModelState state
-> DL state ()
-> (Actions (ModelState state) -> p)
-> Property
forall s a.
(DynLogicModel s, Testable a) =>
Int -> s -> DL s () -> (Actions s -> a) -> Property
DL.forAllUniqueDL Int
nextVar ModelState state
state DL state ()
dl (Actions state -> p
prop (Actions state -> p)
-> (Actions (ModelState state) -> Actions state)
-> Actions (ModelState state)
-> p
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Actions (ModelState state) -> Actions state
forall s. Actions (ModelState s) -> Actions s
fromStateModelActions)

instance ContractModel s => DL.DynLogicModel (ModelState s) where
    restricted :: Action (ModelState s) a -> Bool
restricted (ContractAction _ act) = Action s -> Bool
forall state. ContractModel state => Action state -> Bool
restricted Action s
act
    restricted WaitUntil{}            = Bool
False
    restricted Unilateral{}           = Bool
True

instance GetModelState (DL state) where
    type StateType (DL state) = state
    getModelState :: DL state (ModelState (StateType (DL state)))
getModelState = DL state (ModelState (StateType (DL state)))
forall s. DL s s
DL.getModelStateDL

-- $quantify
--
-- `DL` scenarios support random generation using `DL.forAllQ`. This does not take a normal
-- QuickCheck `Gen` generator, but a `DL.Quantification`, which aside from a generator also keeps
-- track of which values can be generated. This means test cases coming from scenarios containing
-- `DL.forAll` can be prevented from shrinking to something that could not have been generated in
-- the first place.


-- $runningProperties
--
-- Once you have a `ContractModel` and some `DL` scenarios you need to turn these into QuickCheck
-- properties that can be run by `quickCheck`. The functions `propRunActions_`, `propRunActions`, and
-- `propRunActionsWithOptions` take a sequence of actions (a `Actions`), runs it through the
-- blockchain emulator ("Plutus.Trace.Emulator") and checks that the model and the emulator agree
-- on who owns what tokens at the end.
--
-- To generate a `Actions` you can use the `Arbitrary` instance, which generates a random sequence of
-- actions using `arbitraryAction`, or you can use `forAllDL` to generate a `Actions` from a `DL`
-- scenario.

-- | 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 -> String -> Double
_endpointCoverageReq :: ContractInstanceTag -> String -> Double
                                       , CoverageOptions -> CoverageIndex
_coverageIndex       :: CoverageIndex
                                       , CoverageOptions -> Maybe (IORef CoverageReport)
_coverageIORef       :: Maybe (IORef CoverageReport)
                                       }

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 -> String -> Double)
-> CoverageIndex
-> Maybe (IORef CoverageReport)
-> CoverageOptions
CoverageOptions { _checkCoverage :: Bool
_checkCoverage = Bool
False
                                         , _endpointCoverageReq :: ContractInstanceTag -> String -> Double
_endpointCoverageReq = \ ContractInstanceTag
_ String
_ -> Double
0
                                         , _coverageIndex :: CoverageIndex
_coverageIndex = CoverageIndex
forall a. Monoid a => a
mempty
                                         , _coverageIORef :: Maybe (IORef CoverageReport)
_coverageIORef = Maybe (IORef CoverageReport)
forall a. Maybe a
Nothing }

-- | 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 CoverageReport))
     CoverageOptions
     (Maybe (IORef CoverageReport))
-> Maybe (IORef CoverageReport)
forall s a. s -> Getting a s a -> a
^. Getting
  (Maybe (IORef CoverageReport))
  CoverageOptions
  (Maybe (IORef CoverageReport))
Lens' CoverageOptions (Maybe (IORef CoverageReport))
coverageIORef of
    Maybe (IORef CoverageReport)
Nothing -> do
      IORef CoverageReport
ref <- CoverageReport -> IO (IORef CoverageReport)
forall a. a -> IO (IORef a)
newIORef CoverageReport
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 CoverageReport)
_coverageIORef = IORef CoverageReport -> Maybe (IORef CoverageReport)
forall a. a -> Maybe a
Just IORef CoverageReport
ref }
    Maybe (IORef CoverageReport)
_ -> 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 CoverageReport))
     CoverageOptions
     (Maybe (IORef CoverageReport))
-> Maybe (IORef CoverageReport)
forall s a. s -> Getting a s a -> a
^. Getting
  (Maybe (IORef CoverageReport))
  CoverageOptions
  (Maybe (IORef CoverageReport))
Lens' CoverageOptions (Maybe (IORef CoverageReport))
coverageIORef of
    Maybe (IORef CoverageReport)
Nothing -> String -> IO (CoverageReport, Result)
forall (m :: * -> *) a. MonadFail m => String -> m a
fail String
"Unreachable case in quickCheckWithCoverage"
    Just IORef CoverageReport
ref -> do
      CoverageReport
report <- IORef CoverageReport -> IO CoverageReport
forall a. IORef a -> IO a
readIORef IORef CoverageReport
ref
      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
$ String -> IO ()
putStrLn (String -> IO ()) -> (Doc Any -> String) -> Doc Any -> IO ()
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Doc Any -> String
forall a. Show a => a -> String
show (Doc Any -> IO ()) -> Doc Any -> IO ()
forall a b. (a -> b) -> a -> b
$ CoverageIndex -> CoverageReport -> Doc Any
forall ann. CoverageIndex -> CoverageReport -> Doc ann
pprCoverageReport (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) CoverageReport
report
      (CoverageReport, Result) -> IO (CoverageReport, Result)
forall (m :: * -> *) a. Monad m => a -> m a
return (CoverageReport
report, Result
res)

finalChecks :: ContractModel state
            => CheckOptions
            -> CoverageOptions
            -> ([SomeContractInstanceKey state] -> Env {- Outer env -} -> TracePredicate)
            -> PropertyM (ContractMonad state) Env
            -> PropertyM (ContractMonad state) ()
finalChecks :: CheckOptions
-> CoverageOptions
-> ([SomeContractInstanceKey state] -> Env -> TracePredicate)
-> PropertyM (ContractMonad state) Env
-> PropertyM (ContractMonad state) ()
finalChecks CheckOptions
opts CoverageOptions
copts [SomeContractInstanceKey state] -> Env -> TracePredicate
predicate PropertyM (ContractMonad state) Env
prop = do
    Env
outerEnv <- PropertyM (ContractMonad state) Env
prop
    ContractMonadState EmulatorAction state
tr [SomeContractInstanceKey state]
keys' AssetKey
_ <- ContractMonad state (ContractMonadState state)
-> PropertyM (ContractMonad state) (ContractMonadState state)
forall (m :: * -> *) a. Monad m => m a -> PropertyM m a
QC.run ContractMonad state (ContractMonadState state)
forall s (m :: * -> *). MonadState s m => m s
State.get
    let innerAction :: EmulatorTrace AssetMap
        innerAction :: EmulatorTrace (Map AssetKey (Map String AssetClass))
innerAction = StateT
  (Map AssetKey (Map String AssetClass))
  EmulatorTrace
  (Handles state)
-> Map AssetKey (Map String AssetClass)
-> EmulatorTrace (Map AssetKey (Map String AssetClass))
forall (m :: * -> *) s a. Monad m => StateT s m a -> s -> m s
State.execStateT (EmulatorAction state
-> Handles state
-> StateT
     (Map AssetKey (Map String AssetClass))
     EmulatorTrace
     (Handles state)
forall state.
EmulatorAction state
-> Handles state -> EmulatorMonad (Handles state)
runEmulatorAction EmulatorAction state
tr Handles state
forall i j k l (key :: i -> j -> k -> l -> *)
       (val :: i -> j -> k -> *).
IMap key val
IMNil) Map AssetKey (Map String AssetClass)
forall k a. Map k a
Map.empty
        action :: Eff
  '[StartContract, RunContract, Assert, Waiting, EmulatorControl,
    EmulatedWalletAPI, LogMsg String, Error EmulatorRuntimeError]
  ()
action = do
          -- see note [The Env contract]
          Map AssetKey (Map String AssetClass)
env <- EmulatorTrace (Map AssetKey (Map String AssetClass))
innerAction
          ContractHandle
  ()
  ('R
     '[ "register-token-env"
        ':-> (EndpointValue (Map AssetKey (Map String AssetClass)),
              ActiveEndpoint)])
  ContractError
hdl <- Wallet
-> Contract
     ()
     ('R
        '[ "register-token-env"
           ':-> (EndpointValue (Map AssetKey (Map String AssetClass)),
                 ActiveEndpoint)])
     ContractError
     (Map AssetKey (Map String AssetClass))
-> ContractInstanceTag
-> Eff
     '[StartContract, RunContract, Assert, Waiting, EmulatorControl,
       EmulatedWalletAPI, LogMsg String, Error EmulatorRuntimeError]
     (ContractHandle
        ()
        ('R
           '[ "register-token-env"
              ':-> (EndpointValue (Map AssetKey (Map String AssetClass)),
                    ActiveEndpoint)])
        ContractError)
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
w1 (Contract
  ()
  EnvContractSchema
  ContractError
  (Map AssetKey (Map String AssetClass))
forall w.
Contract
  w
  EnvContractSchema
  ContractError
  (Map AssetKey (Map String AssetClass))
getEnvContract @()) ContractInstanceTag
envContractInstanceTag
          Eff
  '[StartContract, RunContract, Assert, Waiting, EmulatorControl,
    EmulatedWalletAPI, LogMsg String, Error EmulatorRuntimeError]
  ()
-> Eff
     '[StartContract, RunContract, Assert, Waiting, EmulatorControl,
       EmulatedWalletAPI, LogMsg String, Error EmulatorRuntimeError]
     ()
forall (f :: * -> *) a. Functor f => f a -> f ()
void (Eff
   '[StartContract, RunContract, Assert, Waiting, EmulatorControl,
     EmulatedWalletAPI, LogMsg String, Error EmulatorRuntimeError]
   ()
 -> Eff
      '[StartContract, RunContract, Assert, Waiting, EmulatorControl,
        EmulatedWalletAPI, LogMsg String, Error EmulatorRuntimeError]
      ())
-> Eff
     '[StartContract, RunContract, Assert, Waiting, EmulatorControl,
       EmulatedWalletAPI, LogMsg String, Error EmulatorRuntimeError]
     ()
-> Eff
     '[StartContract, RunContract, Assert, Waiting, EmulatorControl,
       EmulatedWalletAPI, LogMsg String, Error EmulatorRuntimeError]
     ()
forall a b. (a -> b) -> a -> b
$ ContractHandle
  ()
  ('R
     '[ "register-token-env"
        ':-> (EndpointValue (Map AssetKey (Map String AssetClass)),
              ActiveEndpoint)])
  ContractError
-> Map AssetKey (Map String AssetClass)
-> Eff
     '[StartContract, RunContract, Assert, Waiting, EmulatorControl,
       EmulatedWalletAPI, LogMsg String, Error EmulatorRuntimeError]
     ()
forall (l :: Symbol) ep w (s :: Row *) e (effs :: [* -> *]).
(ToJSON ep, ContractConstraints s, HasEndpoint l ep s,
 Member RunContract effs) =>
ContractHandle w s e -> ep -> Eff effs ()
callEndpoint @"register-token-env" ContractHandle
  ()
  ('R
     '[ "register-token-env"
        ':-> (EndpointValue (Map AssetKey (Map String AssetClass)),
              ActiveEndpoint)])
  ContractError
hdl Map AssetKey (Map String AssetClass)
env
        stream :: forall effs. S.Stream (S.Of (LogMessage EmulatorEvent)) (Eff effs) (Maybe EmulatorErr)
        stream :: Stream
  (Of (LogMessage EmulatorEvent)) (Eff effs) (Maybe EmulatorErr)
stream = (Maybe EmulatorErr, EmulatorState) -> Maybe EmulatorErr
forall a b. (a, b) -> a
fst ((Maybe EmulatorErr, EmulatorState) -> Maybe EmulatorErr)
-> Stream
     (Of (LogMessage EmulatorEvent))
     (Eff effs)
     (Maybe EmulatorErr, EmulatorState)
-> Stream
     (Of (LogMessage EmulatorEvent)) (Eff effs) (Maybe EmulatorErr)
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> EmulatorConfig
-> Eff
     '[StartContract, RunContract, Assert, Waiting, EmulatorControl,
       EmulatedWalletAPI, LogMsg String, Error EmulatorRuntimeError]
     ()
-> Stream
     (Of (LogMessage EmulatorEvent))
     (Eff effs)
     (Maybe EmulatorErr, EmulatorState)
forall (effs :: [* -> *]) a.
EmulatorConfig
-> EmulatorTrace a
-> Stream
     (Of (LogMessage EmulatorEvent))
     (Eff effs)
     (Maybe EmulatorErr, EmulatorState)
runEmulatorStream (CheckOptions
opts CheckOptions
-> Getting EmulatorConfig CheckOptions EmulatorConfig
-> EmulatorConfig
forall s a. s -> Getting a s a -> a
^. Getting EmulatorConfig CheckOptions EmulatorConfig
Lens' CheckOptions EmulatorConfig
emulatorConfig) Eff
  '[StartContract, RunContract, Assert, Waiting, EmulatorControl,
    EmulatedWalletAPI, LogMsg String, Error EmulatorRuntimeError]
  ()
action
        (Maybe EmulatorErr
errorResult, [EmulatorEvent]
events) = (Maybe EmulatorErr -> (Maybe EmulatorErr, [EmulatorEvent]))
-> (Eff '[] (Maybe EmulatorErr, [EmulatorEvent])
    -> (Maybe EmulatorErr, [EmulatorEvent]))
-> (Of
      (LogMessage EmulatorEvent) (Maybe EmulatorErr, [EmulatorEvent])
    -> (Maybe EmulatorErr, [EmulatorEvent]))
-> Stream
     (Of (LogMessage EmulatorEvent)) (Eff '[]) (Maybe EmulatorErr)
-> (Maybe EmulatorErr, [EmulatorEvent])
forall (f :: * -> *) (m :: * -> *) r b.
(Functor f, Monad m) =>
(r -> b) -> (m b -> b) -> (f b -> b) -> Stream f m r -> b
S.streamFold (,[]) Eff '[] (Maybe EmulatorErr, [EmulatorEvent])
-> (Maybe EmulatorErr, [EmulatorEvent])
forall a. Eff '[] a -> a
run (\ (LogMessage EmulatorEvent
msg S.:> (Maybe EmulatorErr, [EmulatorEvent])
es) -> ((Maybe EmulatorErr, [EmulatorEvent]) -> Maybe EmulatorErr
forall a b. (a, b) -> a
fst (Maybe EmulatorErr, [EmulatorEvent])
es, (LogMessage EmulatorEvent
msg LogMessage EmulatorEvent
-> Getting EmulatorEvent (LogMessage EmulatorEvent) EmulatorEvent
-> EmulatorEvent
forall s a. s -> Getting a s a -> a
^. Getting EmulatorEvent (LogMessage EmulatorEvent) EmulatorEvent
forall a1 a2. Lens (LogMessage a1) (LogMessage a2) a1 a2
logMessageContent) EmulatorEvent -> [EmulatorEvent] -> [EmulatorEvent]
forall a. a -> [a] -> [a]
: (Maybe EmulatorErr, [EmulatorEvent]) -> [EmulatorEvent]
forall a b. (a, b) -> b
snd (Maybe EmulatorErr, [EmulatorEvent])
es)) Stream
  (Of (LogMessage EmulatorEvent)) (Eff '[]) (Maybe EmulatorErr)
forall (effs :: [* -> *]).
Stream
  (Of (LogMessage EmulatorEvent)) (Eff effs) (Maybe EmulatorErr)
stream
    case Maybe EmulatorErr
errorResult of
      Just EmulatorErr
err -> do
        (Property -> Property) -> PropertyM (ContractMonad state) ()
forall (m :: * -> *).
Monad m =>
(Property -> Property) -> PropertyM m ()
QC.monitor ((Property -> Property) -> PropertyM (ContractMonad state) ())
-> (Property -> Property) -> PropertyM (ContractMonad state) ()
forall a b. (a -> b) -> a -> b
$ String -> Property -> Property
forall prop. Testable prop => String -> prop -> Property
counterexample (EmulatorErr -> String
forall a. Show a => a -> String
show EmulatorErr
err)
        Bool -> PropertyM (ContractMonad state) ()
forall (m :: * -> *). Monad m => Bool -> PropertyM m ()
QC.assert Bool
False
      Maybe EmulatorErr
_ -> () -> PropertyM (ContractMonad state) ()
forall (m :: * -> *) a. Monad m => a -> m a
return ()
    let cover :: CoverageReport -> PropertyM (ContractMonad state) ()
cover CoverageReport
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 CoverageReport
ref <- CoverageOptions
copts CoverageOptions
-> Getting
     (Maybe (IORef CoverageReport))
     CoverageOptions
     (Maybe (IORef CoverageReport))
-> Maybe (IORef CoverageReport)
forall s a. s -> Getting a s a -> a
^. Getting
  (Maybe (IORef CoverageReport))
  CoverageOptions
  (Maybe (IORef CoverageReport))
Lens' CoverageOptions (Maybe (IORef CoverageReport))
coverageIORef =
                       CoverageReport
report CoverageReport
-> PropertyM (ContractMonad state) ()
-> PropertyM (ContractMonad state) ()
forall a b. NFData a => a -> b -> b
`deepseq`
                        ((Property -> Property) -> PropertyM (ContractMonad state) ()
forall (m :: * -> *).
Monad m =>
(Property -> Property) -> PropertyM m ()
QC.monitor ((Property -> Property) -> PropertyM (ContractMonad state) ())
-> (Property -> Property) -> PropertyM (ContractMonad state) ()
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 CoverageReport -> (CoverageReport -> CoverageReport) -> IO ()
forall a. IORef a -> (a -> a) -> IO ()
modifyIORef IORef CoverageReport
ref (CoverageReport
reportCoverageReport -> CoverageReport -> CoverageReport
forall a. Semigroup a => a -> a -> a
<>)
                           Property -> IO Property
forall (m :: * -> *) a. Monad m => a -> m a
return Property
p)
                     | Bool
otherwise = () -> PropertyM (ContractMonad state) ()
forall (f :: * -> *) a. Applicative f => a -> f a
pure ()
    CoverageOptions
-> [SomeContractInstanceKey state]
-> [EmulatorEvent]
-> PropertyM (ContractMonad state) ()
-> PropertyM (ContractMonad state) ()
forall state a.
ContractModel state =>
CoverageOptions
-> [SomeContractInstanceKey state]
-> [EmulatorEvent]
-> PropertyM (ContractMonad state) a
-> PropertyM (ContractMonad state) a
addEndpointCoverage CoverageOptions
copts [SomeContractInstanceKey state]
keys' [EmulatorEvent]
events (PropertyM (ContractMonad state) ()
 -> PropertyM (ContractMonad state) ())
-> PropertyM (ContractMonad state) ()
-> PropertyM (ContractMonad state) ()
forall a b. (a -> b) -> a -> b
$ CheckOptions
-> TracePredicate
-> (forall (effs :: [* -> *]).
    Stream (Of (LogMessage EmulatorEvent)) (Eff effs) ())
-> (String -> PropertyM (ContractMonad state) ())
-> (Bool -> PropertyM (ContractMonad state) ())
-> (CoverageReport -> PropertyM (ContractMonad state) ())
-> PropertyM (ContractMonad state) ()
forall (m :: * -> *).
Monad m =>
CheckOptions
-> TracePredicate
-> (forall (effs :: [* -> *]).
    Stream (Of (LogMessage EmulatorEvent)) (Eff effs) ())
-> (String -> m ())
-> (Bool -> m ())
-> (CoverageReport -> m ())
-> m ()
checkPredicateInnerStream CheckOptions
opts (TracePredicate
noMainThreadCrashes TracePredicate -> TracePredicate -> TracePredicate
.&&. [SomeContractInstanceKey state] -> Env -> TracePredicate
predicate [SomeContractInstanceKey state]
keys' Env
outerEnv) (Stream
  (Of (LogMessage EmulatorEvent)) (Eff effs) (Maybe EmulatorErr)
-> Stream (Of (LogMessage EmulatorEvent)) (Eff effs) ()
forall (f :: * -> *) a. Functor f => f a -> f ()
void Stream
  (Of (LogMessage EmulatorEvent)) (Eff effs) (Maybe EmulatorErr)
forall (effs :: [* -> *]).
Stream
  (Of (LogMessage EmulatorEvent)) (Eff effs) (Maybe EmulatorErr)
stream) String -> PropertyM (ContractMonad state) ()
forall (m :: * -> *). Monad m => String -> PropertyM m ()
debugOutput Bool -> PropertyM (ContractMonad state) ()
forall (m :: * -> *). Monad m => Bool -> PropertyM m ()
assertResult CoverageReport -> PropertyM (ContractMonad state) ()
cover
    where
        debugOutput :: Monad m => String -> PropertyM m ()
        debugOutput :: String -> PropertyM m ()
debugOutput = (Property -> Property) -> PropertyM m ()
forall (m :: * -> *).
Monad m =>
(Property -> Property) -> PropertyM m ()
QC.monitor ((Property -> Property) -> PropertyM m ())
-> (String -> Property -> Property) -> String -> PropertyM m ()
forall b c a. (b -> c) -> (a -> b) -> a -> c
. IO () -> Property -> Property
forall prop. Testable prop => IO () -> prop -> Property
whenFail (IO () -> Property -> Property)
-> (String -> IO ()) -> String -> Property -> Property
forall b c a. (b -> c) -> (a -> b) -> a -> c
. String -> IO ()
putStrLn

        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 ]

-- | Check endpoint coverage
addEndpointCoverage :: ContractModel state
                    => CoverageOptions
                    -> [SomeContractInstanceKey state]
                    -> [EmulatorEvent]
                    -> PropertyM (ContractMonad state) a
                    -> PropertyM (ContractMonad state) a
addEndpointCoverage :: CoverageOptions
-> [SomeContractInstanceKey state]
-> [EmulatorEvent]
-> PropertyM (ContractMonad state) a
-> PropertyM (ContractMonad state) a
addEndpointCoverage CoverageOptions
copts [SomeContractInstanceKey state]
keys [EmulatorEvent]
es PropertyM (ContractMonad state) a
pm
  | 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 = do
    a
x <- PropertyM (ContractMonad state) a
pm
    let -- Endpoint covereage
        epsToCover :: [(ContractInstanceTag, [String])]
epsToCover = [(ContractInstanceKey state w s e p -> ContractInstanceTag
forall state w (s :: Row *) e p.
(ContractModel state, SchemaConstraints w s e) =>
ContractInstanceKey state w s e p -> ContractInstanceTag
instanceTag ContractInstanceKey state w s e p
k, ContractInstanceKey state w s e p -> [String]
forall state w (s :: Row *) e p.
SchemaConstraints w s e =>
ContractInstanceKey state w s e p -> [String]
contractInstanceEndpoints ContractInstanceKey state w s e p
k) | Key ContractInstanceKey state w s e p
k <- [SomeContractInstanceKey state]
keys]
        epsCovered :: Map ContractInstanceTag (Set String)
epsCovered = [EmulatorEvent] -> Map ContractInstanceTag (Set String)
getInvokedEndpoints [EmulatorEvent]
es
        endpointCovers :: [Property -> Property]
endpointCovers = [ Double -> Bool -> String -> Property -> Property
forall prop.
Testable prop =>
Double -> Bool -> String -> prop -> Property
QC.cover (Getting
  (ContractInstanceTag -> String -> Double)
  CoverageOptions
  (ContractInstanceTag -> String -> Double)
-> CoverageOptions -> ContractInstanceTag -> String -> Double
forall s (m :: * -> *) a. MonadReader s m => Getting a s a -> m a
view Getting
  (ContractInstanceTag -> String -> Double)
  CoverageOptions
  (ContractInstanceTag -> String -> Double)
Lens' CoverageOptions (ContractInstanceTag -> String -> Double)
endpointCoverageReq CoverageOptions
copts ContractInstanceTag
t String
e)
                                    (String
e String -> Set String -> Bool
forall (t :: * -> *) a. (Foldable t, Eq a) => a -> t a -> Bool
`elem` Maybe (Set String) -> Set String
forall (t :: * -> *) m. (Foldable t, Monoid m) => t m -> m
fold (ContractInstanceTag
-> Map ContractInstanceTag (Set String) -> Maybe (Set String)
forall k a. Ord k => k -> Map k a -> Maybe a
Map.lookup ContractInstanceTag
t Map ContractInstanceTag (Set String)
epsCovered))
                                    (Text -> String
Text.unpack (ContractInstanceTag -> Text
unContractInstanceTag ContractInstanceTag
t) String -> ShowS
forall a. [a] -> [a] -> [a]
++ String
" at endpoint " String -> ShowS
forall a. [a] -> [a] -> [a]
++ String
e)
                         | (ContractInstanceTag
t, [String]
eps) <- [(ContractInstanceTag, [String])]
epsToCover
                         , String
e <- [String]
eps ]
    [Property -> Property]
endpointCovers [Property -> Property]
-> PropertyM (ContractMonad state) ()
-> PropertyM (ContractMonad state) ()
forall a b. NFData a => a -> b -> b
`deepseq`
      ((Property -> Property) -> PropertyM (ContractMonad state) ()
forall (m :: * -> *).
Monad m =>
(Property -> Property) -> PropertyM m ()
QC.monitor ((Property -> Property) -> PropertyM (ContractMonad state) ())
-> ([Property -> Property] -> Property -> Property)
-> [Property -> Property]
-> PropertyM (ContractMonad state) ()
forall b c a. (b -> c) -> (a -> b) -> a -> c
. ((Property -> Property)
 -> (Property -> Property) -> Property -> Property)
-> (Property -> Property)
-> [Property -> Property]
-> Property
-> Property
forall (t :: * -> *) a b.
Foldable t =>
(a -> b -> b) -> b -> t a -> b
foldr (Property -> Property)
-> (Property -> Property) -> Property -> Property
forall b c a. (b -> c) -> (a -> b) -> a -> c
(.) Property -> Property
forall a. a -> a
id ([Property -> Property] -> PropertyM (ContractMonad state) ())
-> [Property -> Property] -> PropertyM (ContractMonad state) ()
forall a b. (a -> b) -> a -> b
$ [Property -> Property]
endpointCovers)
    (Property -> Property) -> PropertyM (ContractMonad state) ()
forall (m :: * -> *).
Monad m =>
(Property -> Property) -> PropertyM m ()
QC.monitor Property -> Property
forall prop. Testable prop => prop -> Property
QC.checkCoverage
    a -> PropertyM (ContractMonad state) a
forall (m :: * -> *) a. Monad m => a -> m a
return a
x
  | Bool
otherwise = PropertyM (ContractMonad state) a
pm

contractInstanceEndpoints :: forall state w s e p. SchemaConstraints w s e => ContractInstanceKey state w s e p -> [String]
contractInstanceEndpoints :: ContractInstanceKey state w s e p -> [String]
contractInstanceEndpoints ContractInstanceKey state w s e p
_ = forall s. (IsString s, Forall (Input s) Unconstrained1) => [s]
forall k (ρ :: Row k) s.
(IsString s, Forall ρ Unconstrained1) =>
[s]
labels' @(Input s)

-- | 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_ ::
    ContractModel state
    => Actions state                 -- ^ The actions to run
    -> Property
propRunActions_ :: Actions state -> Property
propRunActions_ Actions state
actions =
    (ModelState state -> TracePredicate) -> Actions state -> Property
forall state.
ContractModel state =>
(ModelState state -> TracePredicate) -> Actions state -> Property
propRunActions (\ ModelState state
_ -> Bool -> TracePredicate
forall (f :: * -> *) a. Applicative f => a -> f a
pure Bool
True) Actions state
actions

-- | 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 =
  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 (Integer -> Value
Ada.lovelaceValueOf Integer
100_000_000_000_000_000)))

-- | 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 ::
    ContractModel state
    => (ModelState state -> TracePredicate) -- ^ Predicate to check at the end
    -> Actions state                         -- ^ The actions to run
    -> Property
propRunActions :: (ModelState state -> TracePredicate) -> Actions state -> Property
propRunActions = CheckOptions
-> CoverageOptions
-> (ModelState state -> TracePredicate)
-> Actions state
-> Property
forall state.
ContractModel state =>
CheckOptions
-> CoverageOptions
-> (ModelState state -> TracePredicate)
-> Actions state
-> Property
propRunActionsWithOptions CheckOptions
defaultCheckOptionsContractModel CoverageOptions
defaultCoverageOptions

-- | Run a `Actions` in the emulator and check that the model and the emulator agree on the final
--   wallet balance changes, that no off-chain contract instance crashed, and that the given
--   `TracePredicate` holds at the end. The predicate has access to the final model state.
--
--   The `Actions` argument can be generated by a `forAllDL` from a `DL` scenario, or using the
--   `Arbitrary` instance for actions which generates random actions using `arbitraryAction`:
--
-- >>> quickCheck $ propRunActions_ handles
-- +++ OK, passed 100 tests
-- >>> quickCheck $ forAllDL dl $ propRunActions_ handles
-- +++ OK, passed 100 tests
--
--   The options argument can be used to configure the emulator--setting initial wallet balances,
--   the maximum number of slots to run for, and the log level for the emulator trace printed on
--   failing tests:
--
-- @
-- options :: `Map` `Wallet` `Value` -> `Slot` -> `Control.Monad.Freer.Extras.Log.LogLevel` -> `CheckOptions`
-- options dist slot logLevel =
--     `defaultCheckOptions` `&` `emulatorConfig` . `Plutus.Trace.Emulator.initialChainState` `.~` `Left` dist
--                         `&` `maxSlot`                            `.~` slot
--                         `&` `minLogLevel`                        `.~` logLevel
-- @
--
propRunActionsWithOptions ::
    ContractModel state
    => CheckOptions                          -- ^ Emulator options
    -> CoverageOptions                       -- ^ Coverage options
    -> (ModelState state -> TracePredicate)  -- ^ Predicate to check at the end
    -> Actions state                         -- ^ The actions to run
    -> Property
propRunActionsWithOptions :: CheckOptions
-> CoverageOptions
-> (ModelState state -> TracePredicate)
-> Actions state
-> Property
propRunActionsWithOptions CheckOptions
opts CoverageOptions
copts ModelState state -> TracePredicate
predicate Actions state
actions' =
  CheckOptions
-> CoverageOptions
-> (ModelState state -> TracePredicate)
-> Actions (ModelState state)
-> Property
forall state.
ContractModel state =>
CheckOptions
-> CoverageOptions
-> (ModelState state -> TracePredicate)
-> Actions (ModelState state)
-> Property
propRunActionsWithOptions' CheckOptions
opts CoverageOptions
copts ModelState state -> TracePredicate
predicate (Actions state -> Actions (ModelState state)
forall state.
ContractModel state =>
Actions state -> Actions (ModelState state)
toStateModelActions Actions state
actions')

initiateWallets :: ContractModel state => ContractMonad state ()
initiateWallets :: ContractMonad state ()
initiateWallets = do
  [StartContract state] -> ContractMonad state ()
forall state. [StartContract state] -> ContractMonad state ()
addInstances [StartContract state]
forall state. ContractModel state => [StartContract state]
initialInstances
  EmulatorMonad (Handles state) -> ContractMonad state ()
forall state.
EmulatorMonad (Handles state) -> ContractMonad state ()
setHandles (EmulatorMonad (Handles state) -> ContractMonad state ())
-> EmulatorMonad (Handles state) -> ContractMonad state ()
forall a b. (a -> b) -> a -> b
$ Eff
  '[StartContract, RunContract, Assert, Waiting, EmulatorControl,
    EmulatedWalletAPI, LogMsg String, Error EmulatorRuntimeError]
  (Handles state)
-> EmulatorMonad (Handles state)
forall (t :: (* -> *) -> * -> *) (m :: * -> *) a.
(MonadTrans t, Monad m) =>
m a -> t m a
lift ((SymToken -> AssetClass)
-> [StartContract state]
-> Eff
     '[StartContract, RunContract, Assert, Waiting, EmulatorControl,
       EmulatedWalletAPI, LogMsg String, Error EmulatorRuntimeError]
     (Handles state)
forall state.
ContractModel state =>
(SymToken -> AssetClass)
-> [StartContract state] -> EmulatorTrace (Handles state)
activateWallets (\ SymToken
_ -> String -> AssetClass
forall a. HasCallStack => String -> a
error String
"activateWallets: no sym tokens should have been created yet") [StartContract state]
forall state. ContractModel state => [StartContract state]
initialInstances)
  () -> ContractMonad state ()
forall (m :: * -> *) a. Monad m => a -> m a
return ()

propRunActionsWithOptions' :: forall state.
    ContractModel state
    => CheckOptions                          -- ^ Emulator options
    -> CoverageOptions                       -- ^ Coverage options
    -> (ModelState state -> TracePredicate)  -- ^ Predicate to check at the end
    -> StateModel.Actions (ModelState state) -- ^ The actions to run
    -> Property
propRunActionsWithOptions' :: CheckOptions
-> CoverageOptions
-> (ModelState state -> TracePredicate)
-> Actions (ModelState state)
-> Property
propRunActionsWithOptions' CheckOptions
opts CoverageOptions
copts ModelState state -> TracePredicate
predicate Actions (ModelState state)
actions =
    ModelState state -> Property
forall state. ModelState state -> Property
asserts ModelState state
finalState Property -> Property -> Property
forall prop1 prop2.
(Testable prop1, Testable prop2) =>
prop1 -> prop2 -> Property
QC..&&.
    ((StateT (ContractMonadState state) Identity Property -> Property)
-> PropertyM (StateT (ContractMonadState state) Identity) ()
-> Property
forall a (m :: * -> *).
(Testable a, Monad m) =>
(m Property -> Property) -> PropertyM m a -> Property
monadic ((StateT (ContractMonadState state) Identity Property
 -> ContractMonadState state -> Property)
-> ContractMonadState state
-> StateT (ContractMonadState state) Identity Property
-> Property
forall a b c. (a -> b -> c) -> b -> a -> c
flip StateT (ContractMonadState state) Identity Property
-> ContractMonadState state -> Property
forall s a. State s a -> s -> a
State.evalState ContractMonadState state
forall a. Monoid a => a
mempty) (PropertyM (StateT (ContractMonadState state) Identity) ()
 -> Property)
-> PropertyM (StateT (ContractMonadState state) Identity) ()
-> Property
forall a b. (a -> b) -> a -> b
$ CheckOptions
-> CoverageOptions
-> ([SomeContractInstanceKey state] -> Env -> TracePredicate)
-> PropertyM (StateT (ContractMonadState state) Identity) Env
-> PropertyM (StateT (ContractMonadState state) Identity) ()
forall state.
ContractModel state =>
CheckOptions
-> CoverageOptions
-> ([SomeContractInstanceKey state] -> Env -> TracePredicate)
-> PropertyM (ContractMonad state) Env
-> PropertyM (ContractMonad state) ()
finalChecks CheckOptions
opts CoverageOptions
copts [SomeContractInstanceKey state] -> Env -> TracePredicate
finalPredicate (PropertyM (StateT (ContractMonadState state) Identity) Env
 -> PropertyM (StateT (ContractMonadState state) Identity) ())
-> PropertyM (StateT (ContractMonadState state) Identity) Env
-> PropertyM (StateT (ContractMonadState state) Identity) ()
forall a b. (a -> b) -> a -> b
$ do
            StateT (ContractMonadState state) Identity ()
-> PropertyM (StateT (ContractMonadState state) Identity) ()
forall (m :: * -> *) a. Monad m => m a -> PropertyM m a
QC.run StateT (ContractMonadState state) Identity ()
forall state. ContractModel state => ContractMonad state ()
initiateWallets
            (ModelState state, Env) -> Env
forall a b. (a, b) -> b
snd ((ModelState state, Env) -> Env)
-> PropertyM
     (StateT (ContractMonadState state) Identity)
     (ModelState state, Env)
-> PropertyM (StateT (ContractMonadState state) Identity) Env
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> ModelState state
-> Actions (ModelState state)
-> PropertyM
     (ActionMonad (ModelState state)) (ModelState state, Env)
forall state.
StateModel state =>
state
-> Actions state -> PropertyM (ActionMonad state) (state, Env)
runActionsInState ModelState state
forall state. StateModel state => state
StateModel.initialState Actions (ModelState state)
actions)
    where
        finalState :: ModelState state
finalState = Actions (ModelState state) -> ModelState state
forall state. StateModel state => Actions state -> state
StateModel.stateAfter Actions (ModelState state)
actions
        finalPredicate :: [SomeContractInstanceKey state] -> Env {- Outer env -} -> TracePredicate
        finalPredicate :: [SomeContractInstanceKey state] -> Env -> TracePredicate
finalPredicate [SomeContractInstanceKey state]
keys' Env
outerEnv = ModelState state -> TracePredicate
predicate ModelState state
finalState TracePredicate -> TracePredicate -> TracePredicate
.&&. ModelState state -> Env -> TracePredicate
forall state. ModelState state -> Env -> TracePredicate
checkBalances ModelState state
finalState Env
outerEnv
                                                             TracePredicate -> TracePredicate -> TracePredicate
.&&. [SomeContractInstanceKey state] -> TracePredicate
forall state.
ContractModel state =>
[SomeContractInstanceKey state] -> TracePredicate
checkNoCrashes [SomeContractInstanceKey state]
keys'
                                                             TracePredicate -> TracePredicate -> TracePredicate
.&&. TracePredicate
checkNoOverlappingTokens
                                                             TracePredicate -> TracePredicate -> TracePredicate
.&&. ModelState state -> TracePredicate
forall state. ModelState state -> TracePredicate
checkSlot ModelState state
finalState

asserts :: ModelState state -> Property
asserts :: ModelState state -> Property
asserts ModelState state
finalState = (Property -> Property -> Property)
-> Property -> [Property] -> Property
forall (t :: * -> *) a b.
Foldable t =>
(a -> b -> b) -> b -> t a -> b
foldr Property -> Property -> Property
forall prop1 prop2.
(Testable prop1, Testable prop2) =>
prop1 -> prop2 -> Property
(QC..&&.) (Bool -> Property
forall prop. Testable prop => prop -> Property
property Bool
True) [ String -> Bool -> Property
forall prop. Testable prop => String -> prop -> Property
counterexample (String
"assertSpec failed: " String -> ShowS
forall a. [a] -> [a] -> [a]
++ String
s) Bool
b
                                                     | (String
s, Bool
b) <- ModelState state
finalState ModelState state
-> Getting [(String, Bool)] (ModelState state) [(String, Bool)]
-> [(String, Bool)]
forall s a. s -> Getting a s a -> a
^. Getting [(String, Bool)] (ModelState state) [(String, Bool)]
forall state. Lens' (ModelState state) [(String, Bool)]
assertions ]

stateAfter :: ContractModel state => Actions state -> ModelState state
stateAfter :: Actions state -> ModelState state
stateAfter Actions state
actions = Actions (ModelState state) -> ModelState state
forall state. StateModel state => Actions state -> state
StateModel.stateAfter (Actions (ModelState state) -> ModelState state)
-> Actions (ModelState state) -> ModelState state
forall a b. (a -> b) -> a -> b
$ Actions state -> Actions (ModelState state)
forall state.
ContractModel state =>
Actions state -> Actions (ModelState state)
toStateModelActions Actions state
actions

{- Note [The Env contract]

 In order to get the environment that maps symbolic variables to actual
 tokens out of the emulator we need to use a contract and the `instanceOutcome`
 fold. All this contract does is it materialises the `AssetMap` that we carry
 around inside the emulator.

 At the end of an emulator execution in which we want to check a property
 of the symbolic tokens we need to add a call to to the `