plutus-contract-0.1.0.0
Safe HaskellNone
LanguageHaskell2010

Plutus.Contract.Test.ContractModel

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

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

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

arbitraryWaitInterval :: ModelState state -> Gen Slot Source #

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

perform Source #

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.

monitoring Source #

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

Defined in Plutus.Contract.Test.ContractModel.CrashTolerance

Associated Types

data Action (WithCrashTolerance state) Source #

data ContractInstanceKey (WithCrashTolerance state) :: Type -> Row Type -> Type -> Type -> Type Source #

Methods

instanceWallet :: 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 #

waitProbability :: ModelState (WithCrashTolerance state) -> Double Source #

arbitraryWaitInterval :: ModelState (WithCrashTolerance state) -> Gen Slot Source #

initialState :: WithCrashTolerance state Source #

initialInstances :: [StartContract (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

Defined in Plutus.Contract.Test.ContractModel.Internal

ContractModel state => HasActions (WithCrashTolerance state) Source # 
Instance details

Defined in Plutus.Contract.Test.ContractModel.CrashTolerance

Model state

data ModelState state Source #

The ModelState models the state of the blockchain. It contains,

Instances

Instances details
Functor ModelState Source # 
Instance details

Defined in Plutus.Contract.Test.ContractModel.Internal

Methods

fmap :: (a -> b) -> ModelState a -> ModelState b Source #

(<$) :: a -> ModelState b -> ModelState a Source #

Show state => Show (ModelState state) Source # 
Instance details

Defined in Plutus.Contract.Test.ContractModel.Internal

Methods

showsPrec :: Int -> ModelState state -> ShowS Source #

show :: ModelState state -> String Source #

showList :: [ModelState state] -> ShowS Source #

ContractModel s => DynLogicModel (ModelState s) Source # 
Instance details

Defined in Plutus.Contract.Test.ContractModel.Internal

ContractModel state => StateModel (ModelState state) Source # 
Instance details

Defined in Plutus.Contract.Test.ContractModel.Internal

Associated Types

data Action (ModelState state) a Source #

type ActionMonad (ModelState state) :: Type -> Type Source #

Methods

actionName :: 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 #

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

Defined in Plutus.Contract.Test.ContractModel.Internal

Associated Types

type StateType (DL state) Source #

Methods

getModelState :: DL state (ModelState (StateType (DL state))) Source #

ContractModel state => Eq (Action (ModelState state) a) Source # 
Instance details

Defined in Plutus.Contract.Test.ContractModel.Internal

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

Defined in Plutus.Contract.Test.ContractModel.Internal

Methods

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

Defined in Plutus.Contract.Test.ContractModel.Internal

type ActionMonad (ModelState state)
data Action (ModelState state) a Source # 
Instance details

Defined in Plutus.Contract.Test.ContractModel.Internal

data Action (ModelState state) a where
type StateType (DL state) Source # 
Instance details

Defined in Plutus.Contract.Test.ContractModel.Internal

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 $~.

currentSlot :: Getter (ModelState state) Slot Source #

Get the current slot.

Spec monad update functions: wait and waitUntil.

balanceChanges :: Getter (ModelState state) (Map Wallet SymValue) Source #

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.

balanceChange :: Wallet -> Getter (ModelState state) SymValue Source #

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.

minted :: Getter (ModelState state) SymValue Source #

Get the amount of tokens minted so far. This is used to compute lockedValue.

Spec monad update functions: mint and burn.

lockedValue :: ModelState s -> SymValue Source #

How much value is currently locked by contracts. This computed by subtracting the wallet balances from the minted value.

symIsZero :: SymValue -> Bool Source #

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

Defined in Plutus.Contract.Test.ContractModel.Internal

Associated Types

type StateType (Spec state) Source #

Methods

getModelState :: Spec state (ModelState (StateType (Spec state))) Source #

GetModelState (DL state) Source # 
Instance details

Defined in Plutus.Contract.Test.ContractModel.Internal

Associated Types

type StateType (DL state) Source #

Methods

getModelState :: 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
Eq SymToken Source # 
Instance details

Defined in Plutus.Contract.Test.ContractModel.Symbolics

Data SymToken Source # 
Instance details

Defined in Plutus.Contract.Test.ContractModel.Symbolics

Methods

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

toConstr :: SymToken -> Constr Source #

dataTypeOf :: SymToken -> DataType 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 #

Ord SymToken Source # 
Instance details

Defined in Plutus.Contract.Test.ContractModel.Symbolics

Show SymToken Source # 
Instance details

Defined in Plutus.Contract.Test.ContractModel.Symbolics

TokenLike SymToken Source # 
Instance details

Defined in Plutus.Contract.Test.ContractModel.Symbolics

symAssetClassValue :: TokenLike t => t -> Integer -> SymValue Source #

Convert a token and an amount to a SymValue

The Spec monad

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

Instances

Instances details
MonadState state (Spec state) Source # 
Instance details

Defined in Plutus.Contract.Test.ContractModel.Internal

Methods

get :: Spec state state Source #

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

state :: (state -> (a, state)) -> Spec state a Source #

Monad (Spec state) Source # 
Instance details

Defined in Plutus.Contract.Test.ContractModel.Internal

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

Defined in Plutus.Contract.Test.ContractModel.Internal

Methods

fmap :: (a -> b) -> Spec state a -> Spec state b Source #

(<$) :: a -> Spec state b -> Spec state a Source #

Applicative (Spec state) Source # 
Instance details

Defined in Plutus.Contract.Test.ContractModel.Internal

Methods

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

Defined in Plutus.Contract.Test.ContractModel.Internal

Associated Types

type StateType (Spec state) Source #

Methods

getModelState :: Spec state (ModelState (StateType (Spec state))) Source #

type StateType (Spec state) Source # 
Instance details

Defined in Plutus.Contract.Test.ContractModel.Internal

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.

transfer Source #

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.

Helper functions for writing perform functions

registerToken :: String -> AssetClass -> SpecificationEmulatorTrace () Source #

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

delay :: Integer -> SpecificationEmulatorTrace () Source #

`delay n` delays emulator execution by n slots

Test scenarios

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

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

Random generation

forAllQ :: Quantifiable q => q -> DL s (Quantifies q) Source #

Generate a random value using the given Quantification (or list/tuple of quantifications). Generated values will only shrink to smaller values that could also have been generated.

data Quantification a Source #

A Quantification over a type a is a generator that can be used with forAllQ to generate random values in DL scenarios. In addition to a QuickCheck generator a Quantification contains a shrinking strategy that ensures that shrunk values stay in the range of the generator.

Instances

Instances details
(Eq a, Show a, Typeable a) => Quantifiable (Quantification a) 
Instance details

Defined in Test.QuickCheck.DynamicLogic.Quantify

Associated Types

type Quantifies (Quantification a) Source #

type Quantifies (Quantification a) 
Instance details

Defined in Test.QuickCheck.DynamicLogic.Quantify

shrinkQ :: Quantification a -> a -> [a] Source #

arbitraryQ :: Arbitrary a => Quantification a Source #

Pack up an Arbitrary instance as a Quantification. Treats all values as being in range.

exactlyQ :: Eq a => a -> Quantification a Source #

Generates exactly the given value. Does not shrink.

elementsQ :: Eq a => [a] -> Quantification a Source #

Pick a random value from a list. Treated as an empty choice if the list is empty:

forAllQ (elementsQ []) == empty

oneofQ :: [Quantification a] -> Quantification a Source #

Choose from a list of quantifications. Same as frequencyQ with all weights the same (and > 0).

frequencyQ :: [(Int, Quantification a)] -> Quantification a Source #

Choose from a weighted list of quantifications. Treated as an empty choice if no quantification has weight > 0.

mapQ :: (a -> b, b -> a) -> Quantification a -> Quantification b Source #

Quantification is not a Functor, since it also keeps track of the range of the generators. However, if you have two functions to :: a -> b from :: b -> a satisfying from . to = id you can go from a quantification over a to one over b. Note that the from function need only be defined on the image of to.

whereQ :: Quantification a -> (a -> Bool) -> Quantification a Source #

Restrict the range of a quantification.

chooseQ :: (Arbitrary a, Random a, Ord a) => (a, a) -> Quantification a Source #

Generate a random value in a given range (inclusive).

class (Eq (Quantifies q), Show (Quantifies q), Typeable (Quantifies q)) => Quantifiable q where Source #

Generalization of Quantifications, which lets you treat lists and tuples of quantifications as quantifications. For instance,

  ...
  (die1, die2) <- forAllQ (chooseQ (1, 6), chooseQ (1, 6))
  ...

Associated Types

type Quantifies q Source #

The type of values quantified over.

Quantifies (Quantification a) = a

Methods

quantify :: q -> Quantification (Quantifies q) Source #

Computing the actual Quantification.

Instances

Instances details
Quantifiable a => Quantifiable [a] 
Instance details

Defined in Test.QuickCheck.DynamicLogic.Quantify

Associated Types

type Quantifies [a] Source #

Methods

quantify :: [a] -> Quantification (Quantifies [a]) Source #

(Eq a, Show a, Typeable a) => Quantifiable (Quantification a) 
Instance details

Defined in Test.QuickCheck.DynamicLogic.Quantify

Associated Types

type Quantifies (Quantification a) Source #

(Quantifiable a, Quantifiable b) => Quantifiable (a, b) 
Instance details

Defined in Test.QuickCheck.DynamicLogic.Quantify

Associated Types

type Quantifies (a, b) Source #

Methods

quantify :: (a, b) -> Quantification (Quantifies (a, b)) Source #

(Quantifiable a, Quantifiable b, Quantifiable c) => Quantifiable (a, b, c) 
Instance details

Defined in Test.QuickCheck.DynamicLogic.Quantify

Associated Types

type Quantifies (a, b, c) Source #

Methods

quantify :: (a, b, c) -> Quantification (Quantifies (a, b, c)) Source #

(Quantifiable a, Quantifiable b, Quantifiable c, Quantifiable d) => Quantifiable (a, b, c, d) 
Instance details

Defined in Test.QuickCheck.DynamicLogic.Quantify

Associated Types

type Quantifies (a, b, c, d) Source #

Methods

quantify :: (a, b, c, d) -> Quantification (Quantifies (a, b, c, d)) Source #

(Quantifiable a, Quantifiable b, Quantifiable c, Quantifiable d, Quantifiable e) => Quantifiable (a, b, c, d, e) 
Instance details

Defined in Test.QuickCheck.DynamicLogic.Quantify

Associated Types

type Quantifies (a, b, c, d, e) Source #

Methods

quantify :: (a, b, c, d, e) -> Quantification (Quantifies (a, b, c, d, e)) Source #

Properties

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

Defined in Plutus.Contract.Test.ContractModel.Internal

Methods

showsPrec :: Int -> Actions state -> ShowS Source #

show :: Actions state -> String Source #

showList :: [Actions state] -> ShowS Source #

ContractModel s => Arbitrary (Actions s) Source # 
Instance details

Defined in Plutus.Contract.Test.ContractModel.Internal

data Act s Source #

Constructors

Bind 

Fields

NoBind 

Fields

ActWaitUntil (Var ()) Slot 

Instances

Instances details
ContractModel s => Eq (Act s) Source # 
Instance details

Defined in Plutus.Contract.Test.ContractModel.Internal

Methods

(==) :: Act s -> Act s -> Bool Source #

(/=) :: Act s -> Act s -> Bool Source #

ContractModel state => Show (Act state) Source # 
Instance details

Defined in Plutus.Contract.Test.ContractModel.Internal

Methods

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

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

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

Defined in Plutus.Contract.Test.ContractModel.Internal

(forall w (s :: Row Type) e p. Show (ContractInstanceKey state w s e p)) => Show (ContractInstanceSpec state) Source # 
Instance details

Defined in Plutus.Contract.Test.ContractModel.Internal

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

data CoverageOptions Source #

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.

defaultCoverageOptions :: CoverageOptions Source #

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

propRunActions_ Source #

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

propRunActions Source #

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

propRunActionsWithOptions Source #

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

defaultCheckOptionsContractModel :: CheckOptions Source #

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.

Test cases

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

Defined in Plutus.Contract.Test.ContractModel.Internal

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

Defined in Plutus.Contract.Test.ContractModel.Internal

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.

withDLTest 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

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 

Fields

  • nlfpMainStrategy :: 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 -> SymValue

    An initial amount of overhead value that may be lost - e.g. setup fees for scripts that can't be recovered.

  • nlfpErrorMargin :: ModelState model -> SymValue

    The total amount of margin for error in the value collected by the WalletStrategy compared to the MainStrategy. This is useful if your contract contains rounding code that makes the order of operations have a small but predictable effect on the value collected by different wallets.

defaultNLFP :: NoLockedFundsProof model Source #

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

checkNoLockedFundsProof :: ContractModel model => CheckOptions -> NoLockedFundsProof model -> Property Source #

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 

Fields

data Whitelist Source #

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

whitelistOk :: Whitelist -> Bool Source #

Check that a whitelist does not accept any partial functions

checkErrorWhitelist :: ContractModel m => Whitelist -> Actions m -> Property Source #

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

checkErrorWhitelistWithOptions :: forall m. ContractModel m => CheckOptions -> CoverageOptions -> Whitelist -> Actions m -> Property Source #

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