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)

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)

Lens for the contract-specific part of the model state.

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

Monads with read access to the model state: the Spec monad used in nextState, and the DL monad used to construct test scenarios.

Get a component of the model state using a lens.

Get a component of the contract state using a lens.

A symbolic token is a token that exists only during ContractModel generation time

Using a semantics function for symbolic tokens, convert a SymValue to a Value

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.

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

Burn tokens. Equivalent to mint . inv.

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

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

Transfer tokens between wallets, updating their balances.

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

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

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

`delay n` delays emulator execution by n slots

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.

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.

Generate a sequence of random actions using arbitraryAction. All actions satisfy their preconditions. Actions may be generated until the stopping stage is reached; the expected length is size/2.

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.

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

forAllQ (elementsQ []) == empty

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

Fail if the boolean is False.

Equivalent to

assert msg b = unless b (fail msg)

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 n = stopping <|> pure ()
                       <|> (weight (fromIntegral n) >> anyAction >> anyActions n)

The effect of this definition is that the second or third 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.

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.

Sometimes test case generation should depend on QuickCheck's size parameter. This can be accessed using getSize. For example, anyActions_ is defined by

anyActions_ = do n <- getSize
                 anyActions (n div 2 + 1)

so that we generate a random number of actions, but on average half the size (which is about the same as the average random positive integer, or length of a list).

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

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

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

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

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

Sanity check a ContractModel. Ensures that nextReactiveState is idempotent.

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.

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

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

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

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

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.

Strategy to recover all funds from the contract in any reachable state.

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.

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

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.

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.

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

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.

Perform a light-weight check to find egregious double satisfaction vulnerabilities in contracts.

A counterexample to this property consists of three transactions. * The first transaction is a valid transaction from the trace generated by the contract model. * The second transaction, generated by redirecting a non-datum pubkey output from a non-signer to a signer in the first transaction, fails to validate. This demonstrates that funds can't simply be stolen. * The third transaction goes through and manages to steal funds by altering the first transaction. It is generated by adding another script input (with the same value as the non-signer non-stealable pubkey output) and adding a datum to the non-signer non-stealable pubkey output, and giving the extra value from the new script input to a signer.

Perform a light-weight check to find egregious double satisfaction vulnerabilities in contracts, with options.

Representable types of kind *. This class is derivable in GHC with the DeriveGeneric flag on.

A Generic instance must satisfy the following laws:

from . to ≡ id
to . from ≡ id