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