plutus-contract-0.1.0.0

Plutus.Contract.Test.ContractModel.Internal

Description

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 (Actions) 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.

Synopsis

# Contract models

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 (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 Source #

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)

Minimal complete definition

Associated Types

data Action state Source #

The type of actions that are supported by the contract. An action usually represents a single callEndpoint or a transfer of tokens, but it can be anything that can be interpreted in the EmulatorTrace monad.

data ContractInstanceKey state :: * -> Row * -> * -> * -> * Source #

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

Methods

instanceWallet :: ContractInstanceKey state w s e p -> Wallet Source #

Get the wallet that the contract running at a specific ContractInstanceKey should run in

instanceTag :: forall w s e p. SchemaConstraints w s e => ContractInstanceKey state w s e p -> ContractInstanceTag Source #

The ContractInstanceTag of an instance key for a wallet. Defaults to walletInstanceTag. You must override this if you have multiple instances per wallet.

arbitraryAction :: ModelState state -> Gen (Action state) Source #

Given the current model state, provide a QuickCheck generator for a random next action. This is used in the Arbitrary instance for Actionss as well as by anyAction and anyActions.

waitProbability :: ModelState state -> Double Source #

The probability that we will generate a WaitUntil in a given state

Control the distribution of how long WaitUntil waits

initialState :: state Source #

The initial state, before any actions have been performed.

initialInstances :: [StartContract state] Source #

The initial handles

precondition :: ModelState state -> Action state -> Bool Source #

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.

nextReactiveState :: Slot -> Spec state () Source #

nextReactiveState is run every time the model waits for a slot to be reached. This can be used to model reactive components of off-chain code.

nextState :: Action state -> Spec state () Source #

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.

startInstances :: ModelState state -> Action state -> [StartContract state] Source #

Start new contract instances

instanceContract :: (SymToken -> AssetClass) -> ContractInstanceKey state w s e p -> p -> Contract w s e () Source #

Map a ContractInstanceKey k to the Contract that is started when we start k in a given ModelState with a given semantics of SymTokens

Arguments

 :: 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 ()

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.

shrinkAction :: ModelState state -> Action state -> [Action state] Source #

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 shrink for more information on shrinking.

Arguments

 :: (ModelState state, ModelState state) Model state before and after the action -> Action state The action that was performed -> Property -> Property

The monitoring function allows you to collect statistics of your testing using QuickCheck functions like label, collect, classify, and 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.

restricted :: Action state -> Bool Source #

In some scenarios it's useful to have actions that are never generated randomly, but only used explicitly in DL scenario actions. To avoid these actions matching an anyAction when shrinking, they can be marked restricted.

#### Instances

Instances details
 (Typeable state, Show (ContractInstanceSpec state), Eq (ContractInstanceSpec state), CrashTolerance state) => ContractModel (WithCrashTolerance state) Source # Instance details Associated Typesdata Action (WithCrashTolerance state) Source #data ContractInstanceKey (WithCrashTolerance state) :: Type -> Row Type -> Type -> Type -> Type Source # MethodsinstanceWallet :: forall w (s :: Row Type) e p. ContractInstanceKey (WithCrashTolerance state) w s e p -> Wallet Source #instanceTag :: forall w (s :: Row Type) e p. SchemaConstraints w s e => ContractInstanceKey (WithCrashTolerance state) w s e p -> ContractInstanceTag Source #arbitraryAction :: ModelState (WithCrashTolerance state) -> Gen (Action (WithCrashTolerance state)) Source #precondition :: ModelState (WithCrashTolerance state) -> Action (WithCrashTolerance state) -> Bool Source #nextReactiveState :: Slot -> Spec (WithCrashTolerance state) () Source #nextState :: Action (WithCrashTolerance state) -> Spec (WithCrashTolerance state) () Source #startInstances :: ModelState (WithCrashTolerance state) -> Action (WithCrashTolerance state) -> [StartContract (WithCrashTolerance state)] Source #instanceContract :: forall w (s :: Row Type) e p. (SymToken -> AssetClass) -> ContractInstanceKey (WithCrashTolerance state) w s e p -> p -> Contract w s e () Source #perform :: HandleFun (WithCrashTolerance state) -> (SymToken -> AssetClass) -> ModelState (WithCrashTolerance state) -> Action (WithCrashTolerance state) -> SpecificationEmulatorTrace () Source #shrinkAction :: ModelState (WithCrashTolerance state) -> Action (WithCrashTolerance state) -> [Action (WithCrashTolerance state)] Source #monitoring :: (ModelState (WithCrashTolerance state), ModelState (WithCrashTolerance state)) -> Action (WithCrashTolerance state) -> Property -> Property Source #restricted :: Action (WithCrashTolerance state) -> Bool Source #

class (Eq (Action state), Show (Action state)) => HasActions state where Source #

#### Instances

Instances details
 (Eq (Action state), Show (Action state), Data (Action state)) => HasActions state Source # Instance details MethodsgetAllSymtokens :: Action state -> Set SymToken Source # ContractModel state => HasActions (WithCrashTolerance state) Source # Instance details Methods

## Model state

data ModelState state Source #

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)

Constructors

 ModelState Fields_currentSlot :: Slot _balanceChanges :: Map Wallet SymValue _minted :: SymValue _symTokens :: Set SymToken _assertions :: [(String, Bool)] _assertionsOk :: Bool _contractState :: state

#### Instances

Instances details
 Source # Instance details Methodsfmap :: (a -> b) -> ModelState a -> ModelState b Source #(<$) :: a -> ModelState b -> ModelState a Source # Show state => Show (ModelState state) Source # Instance details MethodsshowsPrec :: Int -> ModelState state -> ShowS Source #show :: ModelState state -> String Source #showList :: [ModelState state] -> ShowS Source # Source # Instance details Methodsrestricted :: Action (ModelState s) a -> Bool Source # ContractModel state => StateModel (ModelState state) Source # Instance details Associated Typesdata Action (ModelState state) a Source #type ActionMonad (ModelState state) :: Type -> Type Source # MethodsactionName :: Action (ModelState state) a -> String Source #arbitraryAction :: ModelState state -> Gen (Any (Action (ModelState state))) Source #shrinkAction :: (Typeable a, Show a) => ModelState state -> Action (ModelState state) a -> [Any (Action (ModelState state))] Source #nextState :: ModelState state -> Action (ModelState state) a -> Var a -> ModelState state Source #precondition :: ModelState state -> Action (ModelState state) a -> Bool Source #perform :: ModelState state -> Action (ModelState state) a -> LookUp -> ActionMonad (ModelState state) a Source #postcondition :: ModelState state -> Action (ModelState state) a -> LookUp -> a -> Bool Source #monitoring :: (ModelState state, ModelState state) -> Action (ModelState state) a -> LookUp -> a -> Property -> Property Source # GetModelState (DL state) Source # Instance details Associated Typestype StateType (DL state) Source # MethodsgetModelState :: DL state (ModelState (StateType (DL state))) Source # ContractModel state => Eq (Action (ModelState state) a) Source # Instance details Methods(==) :: Action (ModelState state) a -> Action (ModelState state) a -> Bool Source #(/=) :: Action (ModelState state) a -> Action (ModelState state) a -> Bool Source # ContractModel state => Show (Action (ModelState state) a) Source # Instance details MethodsshowsPrec :: Int -> Action (ModelState state) a -> ShowS Source #show :: Action (ModelState state) a -> String Source #showList :: [Action (ModelState state) a] -> ShowS Source # type ActionMonad (ModelState state) Source # Instance details type ActionMonad (ModelState state) data Action (ModelState state) a Source # Instance details data Action (ModelState state) a whereContractAction :: forall state. Bool -> Action state -> Action (ModelState state) AssetKeyUnilateral :: forall state. Wallet -> Action (ModelState state) ()WaitUntil :: forall state. Slot -> Action (ModelState state) () type StateType (DL state) Source # Instance details type StateType (DL state) = state contractState :: forall state state. Lens (ModelState state) (ModelState state) state state Source # Lens for the contract-specific part of the model state. Spec monad update functions: $= and $~. Get the current slot. Spec monad update functions: wait and waitUntil. 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. 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. Get the amount of tokens minted so far. This is used to compute lockedValue. Spec monad update functions: mint and burn. How much value is currently locked by contracts. This computed by subtracting the wallet balances from the minted value. Check if a symbolic value is zero class Monad m => GetModelState m where Source # Monads with read access to the model state: the Spec monad used in nextState, and the DL monad used to construct test scenarios. Associated Types type StateType m :: * Source # The contract state type of the monad. For both Spec and DL this is simply the state parameter of the respective monad. Methods getModelState :: m (ModelState (StateType m)) Source # Get the current model state. #### Instances Instances details  GetModelState (Spec state) Source # Instance details Associated Typestype StateType (Spec state) Source # MethodsgetModelState :: Spec state (ModelState (StateType (Spec state))) Source # GetModelState (DL state) Source # Instance details Associated Typestype StateType (DL state) Source # MethodsgetModelState :: DL state (ModelState (StateType (DL state))) Source # getContractState :: GetModelState m => m (StateType m) Source # Get the contract state part of the model state. askModelState :: GetModelState m => (ModelState (StateType m) -> a) -> m a Source # Get a component of the model state. askContractState :: GetModelState m => (StateType m -> a) -> m a Source # Get a component of the contract state. viewModelState :: GetModelState m => Getting a (ModelState (StateType m)) a -> m a Source # Get a component of the model state using a lens. viewContractState :: GetModelState m => Getting a (StateType m) a -> m a Source # Get a component of the contract state using a lens. data SymToken Source # A symbolic token is a token that exists only during ContractModel generation time #### Instances Instances details  Source # Instance details Methods Source # Instance details Methodsgfoldl :: (forall d b. Data d => c (d -> b) -> d -> c b) -> (forall g. g -> c g) -> SymToken -> c SymToken Source #gunfold :: (forall b r. Data b => c (b -> r) -> c r) -> (forall r. r -> c r) -> Constr -> c SymToken Source #dataCast1 :: Typeable t => (forall d. Data d => c (t d)) -> Maybe (c SymToken) Source #dataCast2 :: Typeable t => (forall d e. (Data d, Data e) => c (t d e)) -> Maybe (c SymToken) Source #gmapT :: (forall b. Data b => b -> b) -> SymToken -> SymToken Source #gmapQl :: (r -> r' -> r) -> r -> (forall d. Data d => d -> r') -> SymToken -> r Source #gmapQr :: forall r r'. (r' -> r -> r) -> r -> (forall d. Data d => d -> r') -> SymToken -> r Source #gmapQ :: (forall d. Data d => d -> u) -> SymToken -> [u] Source #gmapQi :: Int -> (forall d. Data d => d -> u) -> SymToken -> u Source #gmapM :: Monad m => (forall d. Data d => d -> m d) -> SymToken -> m SymToken Source #gmapMp :: MonadPlus m => (forall d. Data d => d -> m d) -> SymToken -> m SymToken Source #gmapMo :: MonadPlus m => (forall d. Data d => d -> m d) -> SymToken -> m SymToken Source # Source # Instance details Methods Source # Instance details MethodsshowList :: [SymToken] -> ShowS Source # Source # Instance details Methods symAssetClassValue :: TokenLike t => t -> Integer -> SymValue Source # Convert a token and an amount to a SymValue ## The Spec monad 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. newtype Spec state a Source # 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. Constructors  Spec FieldsunSpec :: WriterT [SymToken] (ReaderT (Var AssetKey) (State (ModelState state))) a #### Instances Instances details  MonadState state (Spec state) Source # Instance details Methodsget :: Spec state state Source #put :: state -> Spec state () Source #state :: (state -> (a, state)) -> Spec state a Source # Monad (Spec state) Source # Instance details Methods(>>=) :: Spec state a -> (a -> Spec state b) -> Spec state b Source #(>>) :: Spec state a -> Spec state b -> Spec state b Source #return :: a -> Spec state a Source # Functor (Spec state) Source # Instance details Methodsfmap :: (a -> b) -> Spec state a -> Spec state b Source #(<$) :: a -> Spec state b -> Spec state a Source # Applicative (Spec state) Source # Instance details Methodspure :: a -> Spec state a Source #(<*>) :: Spec state (a -> b) -> Spec state a -> Spec state b Source #liftA2 :: (a -> b -> c) -> Spec state a -> Spec state b -> Spec state c Source #(*>) :: Spec state a -> Spec state b -> Spec state b Source #(<*) :: Spec state a -> Spec state b -> Spec state a Source # GetModelState (Spec state) Source # Instance details Associated Typestype StateType (Spec state) Source # MethodsgetModelState :: Spec state (ModelState (StateType (Spec state))) Source # type StateType (Spec state) Source # Instance details type StateType (Spec state) = state

wait :: ContractModel state => Integer -> Spec state () Source #

Wait the given number of slots. Updates the currentSlot of the model state.

waitUntil :: ContractModel state => Slot -> Spec state () Source #

Wait until the given slot. Has no effect if currentSlot is greater than the given slot.

mint :: SymValueLike v => v -> Spec state () Source #

Mint tokens. Minted tokens start out as lockedValue (i.e. owned by the contract) and can be transferred to wallets using deposit.

burn :: SymValueLike v => v -> Spec state () Source #

Burn tokens. Equivalent to mint . inv.

deposit :: SymValueLike v => Wallet -> v -> Spec state () Source #

Add tokens to the balanceChange of a wallet. The added tokens are subtracted from the lockedValue of tokens held by contracts.

withdraw :: SymValueLike v => Wallet -> v -> Spec state () Source #

Withdraw tokens from a wallet. The withdrawn tokens are added to the lockedValue of tokens held by contracts.

Arguments

 :: SymValueLike v => Wallet Transfer from this wallet -> Wallet to this wallet -> v this many tokens -> Spec state ()

Transfer tokens between wallets, updating their balances.

modifyContractState :: (state -> state) -> Spec state () Source #

Modify the contract state.

createToken :: String -> Spec state SymToken Source #

Create a new symbolic token in nextState - must have a corresponding registerToken call in perform

assertSpec :: String -> Bool -> Spec state () Source #

Assert that a particular predicate holds at a point in the specification

($=) :: Setter' state a -> a -> Spec state () Source # Set a specific field of the contract state. ($~) :: Setter' state a -> (a -> a) -> Spec state () Source #

Modify a specific field of the contract state.

Register the real token corresponding to a symbolic token created in createToken.

delay n delays emulator execution by n slots

# Test scenarios

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 (assert, assertModel), and random generation (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!" (isZero . lockedValue)  DL scenarios are turned into QuickCheck properties using forAllDL. type DL state = DL (ModelState state) Source # The monad for writing test scenarios. It supports non-deterministic choice through 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. action :: ContractModel state => Action state -> DL state () Source # Generate a specific action. Fails if the action's precondition is not satisfied. waitUntilDL :: ContractModel state => Slot -> DL state () Source # Generate a specific action. Fails if the action's precondition is not satisfied. anyAction :: DL state () Source # 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. anyActions :: Int -> DL state () Source # Generate a sequence of random actions using arbitraryAction. All actions satisfy their preconditions. 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_ :: DL state () Source # Generate a sequence of random actions using arbitraryAction. All actions satisfy their preconditions. Actions are generated until the stopping stage is reached. ## Failures 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 assert or assertModel, or a monad fail • an empty set of Alternatives • 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.

assert :: String -> Bool -> DL s () Source #

Fail if the boolean is False.

Equivalent to

assert msg b = unless b (fail msg)


assertModel :: String -> (ModelState state -> Bool) -> DL state () Source #

Fail unless the given predicate holds of the model state.

Equivalent to

assertModel msg p = do
s <- getModelState
assert msg (p s)


stopping :: DL state () Source #

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 actions 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 <|> (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.

weight :: Double -> DL state () Source #

By default, Alternative choice (<|>) 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 <|> action b <|> 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) <|> 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.

monitor :: (Property -> Property) -> DL state () Source #

The monitor function allows you to collect statistics of your testing using QuickCheck functions like label, collect, classify, and 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).

# Properties

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.

data Actions s Source #

A Actions is a list of intelligent and sophisticated Actions.

Constructors

 Actions_ [String] (Smart [Act s])

#### Instances

Instances details
 ContractModel state => Show (Actions state) Source # Instance details MethodsshowsPrec :: Int -> Actions state -> ShowS Source #show :: Actions state -> String Source #showList :: [Actions state] -> ShowS Source # Source # Instance details Methodsshrink :: Actions s -> [Actions s] Source #

data Act s Source #

Constructors

 Bind FieldsvarOf :: Var AssetKey actionOf :: Action s NoBind FieldsvarOf :: Var AssetKey actionOf :: Action s ActWaitUntil (Var ()) Slot

#### Instances

Instances details
 ContractModel s => Eq (Act s) Source # Instance details Methods(==) :: Act s -> Act s -> Bool Source #(/=) :: Act s -> Act s -> Bool Source # ContractModel state => Show (Act state) Source # Instance details MethodsshowsPrec :: Int -> Act state -> ShowS Source #show :: Act state -> String Source #showList :: [Act state] -> ShowS Source #

pattern Actions :: [Act s] -> Actions s Source #

## Wallet contract handles

In order to call contract endpoints using callEndpoint, a ContractHandle is required. Contract handles are managed behind the scenes by the propRunActions functions, based on a given a list of ContractInstanceSpecs, associating ContractInstanceKeys with Wallets and Contracts. 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.

type SchemaConstraints w schema err = (Typeable w, Monoid w, ToJSON w, Typeable schema, ContractConstraints schema, Show err, Typeable err, ToJSON err, FromJSON err, ToJSON w, FromJSON w) Source #

The constraints required on contract schemas and error types to enable calling contract endpoints (callEndpoint).

data ContractInstanceSpec state where Source #

A ContractInstanceSpec associates a ContractInstanceKey with a concrete Wallet and Contract. The contract type parameters are hidden from the outside.

Constructors

 ContractInstanceSpec Fields:: (SchemaConstraints w schema err, Typeable params) => ContractInstanceKey state w schema err paramsThe key used when looking up contract instance handles in perform-> WalletThe wallet who owns the contract instance-> Contract w schema err ()The contract that is running in the instance-> ContractInstanceSpec state

#### Instances

Instances details
 (Typeable state, forall w (s :: Row Type) e p. Eq (ContractInstanceKey state w s e p)) => Eq (ContractInstanceSpec state) Source # Instance details Methods(==) :: ContractInstanceSpec state -> ContractInstanceSpec state -> Bool Source #(/=) :: ContractInstanceSpec state -> ContractInstanceSpec state -> Bool Source # (forall w (s :: Row Type) e p. Show (ContractInstanceKey state w s e p)) => Show (ContractInstanceSpec state) Source # Instance details MethodsshowsPrec :: Int -> ContractInstanceSpec state -> ShowS Source #show :: ContractInstanceSpec state -> String Source #showList :: [ContractInstanceSpec state] -> ShowS Source #

data SomeContractInstanceKey state where Source #

Constructors

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

#### Instances

Instances details
 ContractModel state => Eq (SomeContractInstanceKey state) Source # Instance details Methods(==) :: SomeContractInstanceKey state -> SomeContractInstanceKey state -> Bool Source #(/=) :: SomeContractInstanceKey state -> SomeContractInstanceKey state -> Bool Source # ContractModel state => Show (SomeContractInstanceKey state) Source # Instance details MethodsshowsPrec :: Int -> SomeContractInstanceKey state -> ShowS Source #show :: SomeContractInstanceKey state -> String Source #showList :: [SomeContractInstanceKey state] -> ShowS Source #

data StartContract state where Source #

Constructors

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

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

A function returning the ContractHandle corresponding to a ContractInstanceKey. A HandleFun is provided to the perform function to enable calling contract endpoints with callEndpoint.

## Model properties

propSanityCheckModel :: forall state. ContractModel state => Property Source #

Sanity check a ContractModel. Ensures that wallet balances are not always unchanged.

propSanityCheckAssertions :: forall state. ContractModel state => Actions state -> Property Source #

Sanity check a ContractModel. Ensures that all assertions in the property generation succeed.

propSanityCheckReactive :: forall state. (ContractModel state, Eq state) => Actions state -> Positive Integer -> Positive Integer -> Property Source #

Sanity check a ContractModel. Ensures that nextReactiveState is idempotent.

## Coverage checking options

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.

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.

quickCheckWithCoverage :: Testable prop => Args -> CoverageOptions -> (CoverageOptions -> prop) -> IO CoverageReport Source #

Run QuickCheck on a property that tracks coverage and print its coverage report.

## Emulator properties

Arguments

 :: ContractModel state => Actions state The actions to run -> Property

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  Arguments  :: ContractModel state => (ModelState state -> TracePredicate) Predicate to check at the end -> Actions state The actions to run -> Property 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  Arguments  :: ContractModel state => CheckOptions Emulator options -> CoverageOptions Coverage options -> (ModelState state -> TracePredicate) Predicate to check at the end -> Actions state The actions to run -> Property 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 -> LogLevel -> CheckOptions
options dist slot logLevel =
defaultCheckOptions & emulatorConfig . initialChainState .~ Left dist
& maxSlot                            .~ slot
& minLogLevel                        .~ logLevel


Default check options that include a large amount of Ada in the initial distributions to avoid having to write ContractModels that keep track of balances.

## DL properties

forAllDL :: (ContractModel state, Testable p) => DL state () -> (Actions state -> p) -> Property Source #

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 Source # ## Test cases 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.

data DLTest state Source #

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.

Constructors

 BadPrecondition [TestStep state] [FailedStep state] state An explicit action failed its precondition (Action), or an assertion failed (Assert). There is a list of FailedSteps because there may be multiple branches (<|>) 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 empty. Contains the contract state at the point where the scenario got stuck. DLScript [TestStep state] A successfully generated test case.

#### Instances

Instances details
 ContractModel s => Show (DLTest s) Source # Instance details MethodsshowsPrec :: Int -> DLTest s -> ShowS Source #show :: DLTest s -> String Source #showList :: [DLTest s] -> ShowS Source #

data TestStep s Source #

One step of a test case. Either an Action (Do) or a value generated by a forAllQ (Witness). When a DLTest is turned into a Actions to be executed the witnesses are stripped away.

Constructors

 Do (Act s) forall a.(Eq a, Show a, Typeable a) => Witness a

#### Instances

Instances details
 ContractModel s => Show (TestStep s) Source # Instance details MethodsshowsPrec :: Int -> TestStep s -> ShowS Source #showList :: [TestStep s] -> ShowS Source #

data FailedStep state Source #

This type captures the two different kinds of BadPreconditions that can occur.

Constructors

 Action (Act state) A call to action that does not satisfy its precondition. Assert String A call to assert or assertModel failed, or a fail in the DL monad. Stores the string argument of the corresponding call.

#### Instances

Instances details
 ContractModel s => Eq (FailedStep s) Source # Instance details Methods(==) :: FailedStep s -> FailedStep s -> Bool Source #(/=) :: FailedStep s -> FailedStep s -> Bool Source # ContractModel s => Show (FailedStep s) Source # Instance details MethodsshowList :: [FailedStep s] -> ShowS Source #

Arguments

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

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.

## Standard properties

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

data NoLockedFundsProof model Source #

A "proof" that you can always recover the funds locked by a contract. The first component is a strategy that from any state of the contract can get all the funds out. The second component is a strategy for each wallet that from the same state, shows how that wallet can recover the same (or bigger) amount as using the first strategy, without relying on any actions being taken by the other wallets.

For instance, in a two player game where each player bets some amount of funds and the winner gets the pot, there needs to be a mechanism for the players to recover their bid if the other player simply walks away (perhaps after realising the game is lost). If not, it won't be possible to construct a NoLockedFundsProof that works in a state where both players need to move before any funds can be collected.

Constructors

 NoLockedFundsProof FieldsnlfpMainStrategy :: DL model ()Strategy to recover all funds from the contract in any reachable state.nlfpWalletStrategy :: Wallet -> DL model ()A strategy for each wallet to recover as much (or more) funds as the main strategy would give them in a given state, without the assistance of any other wallet.nlfpOverhead :: ModelState model -> SymValueAn initial amount of overhead value that may be lost - e.g. setup fees for scripts that can't be recovered.nlfpErrorMargin :: ModelState model -> SymValueThe total amount of margin for error in the value collected by the WalletStrategy compared to the MainStrategy. This is useful if your contract contains rounding code that makes the order of operations have a small but predictable effect on the value collected by different wallets.

The default skeleton of a NoLockedFundsProof - doesn't permit any overhead or error margin.

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

data NoLockedFundsProofLight model Source #

Constructors

 NoLockedFundsProofLight FieldsnlfplMainStrategy :: DL model ()

data Whitelist Source #

A whitelist entry tells you what final log entry prefixes are acceptable for a given error

#### Instances

Instances details
 Source # Instance details Methodsstimes :: Integral b => b -> Whitelist -> Whitelist Source # Source # Instance details Methodsmconcat :: [Whitelist] -> Whitelist Source #

Check that a whitelist does not accept any partial functions

Check that running a contract model does not result in validation failures that are not accepted by the whitelist.

Check that running a contract model does not result in validation failures that are not accepted by the whitelist.