| Safe Haskell | None |
|---|---|
| Language | Haskell2010 |
Test.QuickCheck.ContractModel
Synopsis
- class (Typeable state, Show state, HasActions state) => ContractModel state where
- data Action state
- arbitraryAction :: ModelState state -> Gen (Action state)
- actionName :: Action state -> String
- waitProbability :: ModelState state -> Double
- arbitraryWaitInterval :: ModelState state -> Gen SlotNo
- initialState :: state
- precondition :: ModelState state -> Action state -> Bool
- nextReactiveState :: SlotNo -> Spec state ()
- nextState :: Action state -> Spec state ()
- shrinkAction :: ModelState state -> Action state -> [Action state]
- restricted :: Action state -> Bool
- class (ContractModel state, IsRunnable m) => RunModel state m where
- perform :: ModelState state -> Action state -> (forall t. HasSymbolicRep t => Symbolic t -> t) -> RunMonad m ()
- monitoring :: (ModelState state, ModelState state) -> Action state -> (forall t. HasSymbolicRep t => Symbolic t -> t) -> SymIndex -> Property -> Property
- class (DefaultRealized m, HasChainIndex m, Monad m) => IsRunnable m where
- awaitSlot :: SlotNo -> m ()
- type DefaultRealized m = (Realized m SymIndex ~ SymIndex, Realized m () ~ ())
- newtype RunMonad m a = RunMonad {
- unRunMonad :: WriterT SymIndex m a
- data Actions s
- data Act s
- = Bind { }
- | NoBind { }
- | ActWaitUntil (Var ()) SlotNo
- | ActObservation (Var ()) String (SymbolicSemantics -> ChainState -> Bool)
- pattern Actions :: [Act s] -> Actions s
- ContractAction :: Bool -> Action state -> Action (ModelState state) SymIndex
- WaitUntil :: SlotNo -> Action (ModelState state) ()
- stateAfter :: ContractModel state => Actions state -> ModelState state
- runContractModel :: (ContractModel state, RunModel state m, HasChainIndex m) => Actions state -> PropertyM (RunMonad m) (ContractModelResult state)
- liftRunMonad :: (forall a. m a -> n a) -> RunMonad m a -> RunMonad n a
- contractState :: forall state state. Lens (ModelState state) (ModelState state) state state
- registerSymbolic :: (Monad m, HasSymbolicRep t) => String -> t -> RunMonad m ()
- registerToken :: Monad m => String -> AssetId -> RunMonad m ()
- registerTxOut :: Monad m => String -> TxOut CtxUTxO Era -> RunMonad m ()
- registerTxIn :: Monad m => String -> TxIn -> RunMonad m ()
- class HasChainIndex m where
- getChainIndex :: m ChainIndex
- getChainState :: m ChainState
- data ChainIndex = ChainIndex {
- transactions :: [TxInState]
- networkId :: NetworkId
- data ChainState = ChainState {}
- data TxInState = TxInState {
- tx :: Tx Era
- chainState :: ChainState
- accepted :: Bool
- type Era = BabbageEra
- data Symbolic t
- type SymToken = Symbolic AssetId
- type SymTxOut = Symbolic (TxOut CtxUTxO Era)
- type SymTxIn = Symbolic TxIn
- data SymValue
- symIsZero :: SymValue -> Bool
- symLeq :: SymValue -> SymValue -> Bool
- toValue :: (SymToken -> AssetId) -> SymValue -> Value
- toSymVal :: (AssetId -> Maybe SymToken) -> Value -> SymValue
- inv :: SymValue -> SymValue
- class SymValueLike v where
- toSymValue :: v -> SymValue
- class TokenLike t where
- symAssetIdValueOf :: SymValue -> t -> Quantity
- symAssetIdValue :: t -> Quantity -> SymValue
- class HasSymbolics a where
- getAllSymbolics :: a -> SymCollectionIndex
- class HasSymbolicRep t
- data BalanceChangeOptions = BalanceChangeOptions {
- observeScriptValue :: Bool
- feeCalucation :: FeeCalculation
- protocolParameters :: ProtocolParameters
- addressPrettyPrinter :: AddressInEra Era -> String
- assertBalanceChangesMatch :: BalanceChangeOptions -> ContractModelResult state -> Property
- signerPaysFees :: FeeCalculation
- asserts :: ModelState state -> Property
- module Test.QuickCheck.ContractModel.DL
- data ModelState state
- newtype Spec state a = Spec {
- unSpec :: WriterT SymCreationIndex (ReaderT (Var SymIndex) (State (ModelState state))) a
- class Monad m => GetModelState m where
- type StateType m :: *
- getModelState :: m (ModelState (StateType m))
- runSpec :: Spec state () -> Var SymIndex -> ModelState state -> ModelState state
- currentSlot :: Getter (ModelState state) SlotNo
- balanceChanges :: Getter (ModelState state) (Map (AddressInEra Era) SymValue)
- balanceChange :: Ord (AddressInEra Era) => AddressInEra Era -> Getter (ModelState state) SymValue
- minted :: Getter (ModelState state) SymValue
- lockedValue :: ModelState s -> SymValue
- getContractState :: GetModelState m => m (StateType m)
- askModelState :: GetModelState m => (ModelState (StateType m) -> a) -> m a
- askContractState :: GetModelState m => (StateType m -> a) -> m a
- viewModelState :: GetModelState m => Getting a (ModelState (StateType m)) a -> m a
- viewContractState :: GetModelState m => Getting a (StateType m) a -> m a
- createSymbolic :: forall t state. HasSymbolicRep t => String -> Spec state (Symbolic t)
- createToken :: String -> Spec state SymToken
- createTxOut :: String -> Spec state SymTxOut
- createTxIn :: String -> Spec state SymTxIn
- mint :: SymValueLike v => v -> Spec state ()
- burn :: SymValueLike v => v -> Spec state ()
- deposit :: SymValueLike v => AddressInEra Era -> v -> Spec state ()
- withdraw :: SymValueLike v => AddressInEra Era -> v -> Spec state ()
- transfer :: SymValueLike v => AddressInEra Era -> AddressInEra Era -> v -> Spec state ()
- waitUntil :: ContractModel state => SlotNo -> Spec state ()
- wait :: ContractModel state => Integer -> Spec state ()
- assertSpec :: String -> Bool -> Spec state ()
- coerceSpec :: forall s s' a. Coercible s s' => Spec s a -> Spec s' a
- fromStateModelActions :: Actions (ModelState s) -> Actions s
Documentation
class (Typeable state, Show state, HasActions state) => 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
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.
Methods
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.
actionName :: Action state -> String Source #
The name of an Action, used to report statistics.
waitProbability :: ModelState state -> Double Source #
The probability that we will generate a WaitUntil in a given state
arbitraryWaitInterval :: ModelState state -> Gen SlotNo Source #
Control the distribution of how long WaitUntil waits
initialState :: state Source #
The initial state, before any actions have been performed.
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 :: SlotNo -> 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.
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.
restricted :: Action state -> Bool Source #
class (ContractModel state, IsRunnable m) => RunModel state m where Source #
Minimal complete definition
Methods
perform :: ModelState state -> Action state -> (forall t. HasSymbolicRep t => Symbolic t -> t) -> RunMonad m () Source #
Perform an Action in some state in the Monad m. This
is the function that's used to exercise the actual stateful
implementation, usually through various side-effects as permitted
by m. It produces a value of type a, eg. some observable
output from the Action that should later be kept in the
environment through a `Var a` also passed to the nextState
function.
The Lookup parameter provides an environment to lookup `Var
a` instances from previous steps.
monitoring :: (ModelState state, ModelState state) -> Action state -> (forall t. HasSymbolicRep t => Symbolic t -> t) -> SymIndex -> Property -> Property Source #
class (DefaultRealized m, HasChainIndex m, Monad m) => IsRunnable m where Source #
Instances
| IsRunnable m => IsRunnable (RunMonad m) Source # | |
Defined in Test.QuickCheck.ContractModel.Internal | |
| (DefaultRealized m, IsRunnable m) => IsRunnable (ReaderT r m) Source # | |
Defined in Test.QuickCheck.ContractModel.Internal | |
| (DefaultRealized m, IsRunnable m) => IsRunnable (StateT s m) Source # | |
Defined in Test.QuickCheck.ContractModel.Internal | |
| (Monoid w, DefaultRealized m, IsRunnable m) => IsRunnable (WriterT w m) Source # | |
Defined in Test.QuickCheck.ContractModel.Internal | |
type DefaultRealized m = (Realized m SymIndex ~ SymIndex, Realized m () ~ ()) Source #
Constructors
| RunMonad | |
Fields
| |
Instances
Instances
| ContractModel state => Show (Actions state) Source # | |
| ContractModel s => Arbitrary (Actions s) Source # | |
Constructors
| Bind | |
| NoBind | |
| ActWaitUntil (Var ()) SlotNo | |
| ActObservation (Var ()) String (SymbolicSemantics -> ChainState -> Bool) | |
Instances
| ContractModel s => Eq (Act s) Source # | |
| ContractModel state => Show (Act state) Source # | |
ContractAction :: Bool -> Action state -> Action (ModelState state) SymIndex Source #
WaitUntil :: SlotNo -> Action (ModelState state) () Source #
stateAfter :: ContractModel state => Actions state -> ModelState state Source #
runContractModel :: (ContractModel state, RunModel state m, HasChainIndex m) => Actions state -> PropertyM (RunMonad m) (ContractModelResult state) Source #
liftRunMonad :: (forall a. m a -> n a) -> RunMonad m a -> RunMonad n a Source #
contractState :: forall state state. Lens (ModelState state) (ModelState state) state state Source #
Lens for the contract-specific part of the model state.
registerSymbolic :: (Monad m, HasSymbolicRep t) => String -> t -> RunMonad m () Source #
Chain index
class HasChainIndex m where Source #
Instances
data ChainIndex Source #
Constructors
| ChainIndex | |
Fields
| |
Instances
| Semigroup ChainIndex Source # | |
Defined in Test.QuickCheck.ContractModel.Internal.ChainIndex Methods (<>) :: ChainIndex -> ChainIndex -> ChainIndex Source # sconcat :: NonEmpty ChainIndex -> ChainIndex Source # stimes :: Integral b => b -> ChainIndex -> ChainIndex Source # | |
data ChainState Source #
Constructors
| ChainState | |
Constructors
| TxInState | |
Fields
| |
The safe interface to Symbolic
Instances
| TokenLike SymToken Source # | |
Defined in Test.QuickCheck.ContractModel.Internal.Symbolics Methods symAssetIdValueOf :: SymValue -> SymToken -> Quantity Source # symAssetIdValue :: SymToken -> Quantity -> SymValue Source # | |
| Eq (Symbolic t) Source # | |
| Ord (Symbolic t) Source # | |
Defined in Test.QuickCheck.ContractModel.Internal.Symbolics Methods compare :: Symbolic t -> Symbolic t -> Ordering Source # (<) :: Symbolic t -> Symbolic t -> Bool Source # (<=) :: Symbolic t -> Symbolic t -> Bool Source # (>) :: Symbolic t -> Symbolic t -> Bool Source # (>=) :: Symbolic t -> Symbolic t -> Bool Source # | |
| HasSymbolicRep t => Show (Symbolic t) Source # | |
| HasVariables (Symbolic t) Source # | |
Defined in Test.QuickCheck.ContractModel.Internal.Symbolics Methods getAllVariables :: Symbolic t -> Set (Any Var) | |
| HasSymbolicRep t => HasSymbolics (Symbolic t) Source # | |
Defined in Test.QuickCheck.ContractModel.Internal.Model Methods getAllSymbolics :: Symbolic t -> SymCollectionIndex Source # | |
type SymToken = Symbolic AssetId Source #
A symbolic token is a token that is only available at runtime
type SymTxOut = Symbolic (TxOut CtxUTxO Era) Source #
A SymTxOut is a `TxOut CtxUTxO Era` that is only available at runtime
A symbolic value is a combination of a real value and a value associating symbolic tokens with an amount
Instances
symLeq :: SymValue -> SymValue -> Bool Source #
Check if one symbolic value is less than or equal to another
toValue :: (SymToken -> AssetId) -> SymValue -> Value Source #
Using a semantics function for symbolic tokens, convert a SymValue to a Value
toSymVal :: (AssetId -> Maybe SymToken) -> Value -> SymValue Source #
Invert a sym token mapping to turn a Value into a SymValue, useful for error reporting
class SymValueLike v where Source #
Methods
toSymValue :: v -> SymValue Source #
Instances
| SymValueLike Value Source # | |
Defined in Test.QuickCheck.ContractModel.Internal.Symbolics Methods toSymValue :: Value -> SymValue Source # | |
| SymValueLike SymValue Source # | |
Defined in Test.QuickCheck.ContractModel.Internal.Symbolics Methods toSymValue :: SymValue -> SymValue Source # | |
class TokenLike t where Source #
Methods
symAssetIdValueOf :: SymValue -> t -> Quantity Source #
Get the value of a specific token in a SymValue
symAssetIdValue :: t -> Quantity -> SymValue Source #
Convert a token and an amount to a SymValue
Instances
| TokenLike AssetId Source # | |
Defined in Test.QuickCheck.ContractModel.Internal.Symbolics Methods symAssetIdValueOf :: SymValue -> AssetId -> Quantity Source # symAssetIdValue :: AssetId -> Quantity -> SymValue Source # | |
| TokenLike SymToken Source # | |
Defined in Test.QuickCheck.ContractModel.Internal.Symbolics Methods symAssetIdValueOf :: SymValue -> SymToken -> Quantity Source # symAssetIdValue :: SymToken -> Quantity -> SymValue Source # | |
class HasSymbolics a where Source #
Minimal complete definition
Nothing
Methods
getAllSymbolics :: a -> SymCollectionIndex Source #
default getAllSymbolics :: (Generic a, GenericHasSymbolics (Rep a)) => a -> SymCollectionIndex Source #
Instances
class HasSymbolicRep t Source #
Instances
| HasSymbolicRep TxIn Source # | |
| HasSymbolicRep AssetId Source # | |
| HasSymbolicRep (TxOut CtxUTxO Era) Source # | |
Properties
data BalanceChangeOptions Source #
Constructors
| BalanceChangeOptions | |
Fields
| |
assertBalanceChangesMatch :: BalanceChangeOptions -> ContractModelResult state -> Property Source #
asserts :: ModelState state -> Property Source #
Dynamic logic
The safe interface to Spec
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)
Instances
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 | |
Fields
| |
Instances
| MonadState state (Spec state) Source # | |
| Monad (Spec state) Source # | |
| Functor (Spec state) Source # | |
| Applicative (Spec state) Source # | |
Defined in Test.QuickCheck.ContractModel.Internal.Spec 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 # | |
Defined in Test.QuickCheck.ContractModel.Internal.Spec Methods getModelState :: Spec state (ModelState (StateType (Spec state))) Source # | |
| type StateType (Spec state) Source # | |
Defined in Test.QuickCheck.ContractModel.Internal.Spec | |
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.
Instances
| GetModelState (Spec state) Source # | |
Defined in Test.QuickCheck.ContractModel.Internal.Spec Methods getModelState :: Spec state (ModelState (StateType (Spec state))) Source # | |
| GetModelState (DL state) Source # | |
Defined in Test.QuickCheck.ContractModel.DL Methods getModelState :: DL state (ModelState (StateType (DL state))) Source # | |
runSpec :: Spec state () -> Var SymIndex -> ModelState state -> ModelState state Source #
currentSlot :: Getter (ModelState state) SlotNo Source #
Get the current slot.
Spec monad update functions: wait and waitUntil.
balanceChanges :: Getter (ModelState state) (Map (AddressInEra Era) SymValue) Source #
balanceChange :: Ord (AddressInEra Era) => AddressInEra Era -> Getter (ModelState state) SymValue Source #
minted :: Getter (ModelState state) SymValue Source #
Get the amount of tokens minted so far. This is used to compute lockedValue.
lockedValue :: ModelState s -> SymValue Source #
How much value is currently locked by contracts. This computed by subtracting the wallet
balances from the minted value.
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.
createSymbolic :: forall t state. HasSymbolicRep t => String -> Spec state (Symbolic t) Source #
createToken :: String -> Spec state SymToken Source #
Create a new symbolic token in nextState - must have a
corresponding registerToken call in perform
createTxOut :: String -> Spec state SymTxOut Source #
Create a new symbolic TxOut in nextState - must have a
corresponding registerTxOut call in perform
createTxIn :: String -> Spec state SymTxIn Source #
Create a new symbolic TxIn in nextState - must have a
corresponding registerTxIn call in perform
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.
deposit :: SymValueLike v => AddressInEra Era -> v -> Spec state () Source #
Add tokens to the balanceChange of an address. The added tokens are subtracted from the
lockedValue of tokens held by contracts.
withdraw :: SymValueLike v => AddressInEra Era -> v -> Spec state () Source #
Withdraw tokens from an address. The withdrawn tokens are added to the lockedValue of tokens
held by contracts.
Arguments
| :: SymValueLike v | |
| => AddressInEra Era | Transfer from this address |
| -> AddressInEra Era | to this address |
| -> v | this much value |
| -> Spec state () |
Transfer tokens between wallets, updating their balances.
waitUntil :: ContractModel state => SlotNo -> Spec state () Source #
Wait until the given slot. Has no effect if currentSlot is greater than the given slot.
wait :: ContractModel state => Integer -> Spec state () Source #
Wait the given number of slots. Updates the currentSlot of the model state.
assertSpec :: String -> Bool -> Spec state () Source #
Assert that a particular predicate holds at a point in the specification
Internals
fromStateModelActions :: Actions (ModelState s) -> Actions s Source #