Safe Haskell	None
Language	Haskell2010

Test.QuickCheck.ContractModel.Internal.Spec

Synopsis

data ModelState state = ModelState {
- _currentSlot :: SlotNo
- _balanceChanges :: Map (AddressInEra Era) SymValue
- _minted :: SymValue
- _symbolics :: SymCollectionIndex
- _assertions :: [(String, Bool)]
- _assertionsOk :: Bool
- _contractState :: state
}
newtype Spec state a = Spec {
- unSpec :: WriterT SymCreationIndex (ReaderT (Var SymIndex) (State (ModelState state))) a
}
coerceSpec :: forall s s' a. Coercible s s' => Spec s a -> Spec s' a
contractState :: forall state state. Lens (ModelState state) (ModelState state) state state
currentSlotL :: forall state. Lens' (ModelState state) SlotNo
balanceChangesL :: forall state. Lens' (ModelState state) (Map (AddressInEra Era) SymValue)
mintedL :: forall state. Lens' (ModelState state) SymValue
assertions :: forall state. Lens' (ModelState state) [(String, Bool)]
assertionsOk :: forall state. Lens' (ModelState state) Bool
symbolics :: forall state. Lens' (ModelState state) SymCollectionIndex
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
modState :: forall state a. Setter' (ModelState state) a -> (a -> a) -> Spec state ()
class Monad m => GetModelState m where
- type StateType m :: *
- getModelState :: m (ModelState (StateType m))
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
runSpec :: Spec state () -> Var SymIndex -> ModelState state -> ModelState state
symbolicsCreatedBy :: Spec state () -> Var SymIndex -> ModelState state -> SymCreationIndex
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 ()
assertSpec :: String -> Bool -> Spec state ()

Documentation

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 :: SlotNo _balanceChanges :: Map (AddressInEra Era) SymValue _minted :: SymValue _symbolics :: SymCollectionIndex _assertions :: [(String, Bool)] _assertionsOk :: Bool _contractState :: state

Instances

Instances details

Functor ModelState Source #
Instance details Defined in Test.QuickCheck.ContractModel.Internal.Spec Methods fmap :: (a -> b) -> ModelState a -> ModelState b Source # (<$) :: a -> ModelState b -> ModelState a Source #
(ContractModel state, Typeable a) => ActionLike state (Action (ModelState state) a) Source #
Instance details Defined in Test.QuickCheck.ContractModel.DL Methods action :: Action (ModelState state) a -> DL state () Source #
Show state => Show (ModelState state) Source #
Instance details Defined in Test.QuickCheck.ContractModel.Internal.Spec Methods showsPrec :: Int -> ModelState state -> ShowS Source # show :: ModelState state -> String Source # showList :: [ModelState state] -> ShowS Source #
Generic (ModelState state) Source #
Instance details Defined in Test.QuickCheck.ContractModel.Internal.Spec Associated Types type Rep (ModelState state) :: Type -> Type Source # Methods from :: ModelState state -> Rep (ModelState state) x Source # to :: Rep (ModelState state) x -> ModelState state Source #
ContractModel state => StateModel (ModelState state)
Instance details Defined in Test.QuickCheck.ContractModel.Internal.Model Associated Types data Action (ModelState state) a Methods actionName :: Action (ModelState state) a -> String arbitraryAction :: VarContext -> ModelState state -> Gen (Any (Action (ModelState state))) shrinkAction :: Typeable a => VarContext -> ModelState state -> Action (ModelState state) a -> [Any (Action (ModelState state))] initialState :: ModelState state nextState :: Typeable a => ModelState state -> Action (ModelState state) a -> Var a -> ModelState state precondition :: ModelState state -> Action (ModelState state) a -> Bool
GetModelState (DL state) Source #
Instance details Defined in Test.QuickCheck.ContractModel.DL Associated Types type StateType (DL state) Source # Methods getModelState :: DL state (ModelState (StateType (DL state))) Source #
ContractModel s => DynLogicModel (ModelState s)
Instance details Defined in Test.QuickCheck.ContractModel.DL Methods restricted :: Action (ModelState s) a -> Bool
(IsRunnable m, RunModel state m) => RunModel (ModelState state) (RunMonad m)
Instance details Defined in Test.QuickCheck.ContractModel.Internal Methods perform :: Typeable a => ModelState state -> Action (ModelState state) a -> LookUp (RunMonad m) -> RunMonad m (Realized (RunMonad m) a) postcondition :: (ModelState state, ModelState state) -> Action (ModelState state) a -> LookUp (RunMonad m) -> Realized (RunMonad m) a -> PostconditionM (RunMonad m) Bool monitoring :: (ModelState state, ModelState state) -> Action (ModelState state) a -> LookUp (RunMonad m) -> Realized (RunMonad m) a -> Property -> Property
ContractModel state => Eq (Action (ModelState state) a) Source #
Instance details Defined in Test.QuickCheck.ContractModel.Internal.Model 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 Test.QuickCheck.ContractModel.Internal.Model Methods showsPrec :: Int -> Action (ModelState state) a -> ShowS Source # show :: Action (ModelState state) a -> String Source # showList :: [Action (ModelState state) a] -> ShowS Source #
HasVariables (Action state) => HasVariables (Action (ModelState state) a)
Instance details Defined in Test.QuickCheck.ContractModel.Internal.Model Methods getAllVariables :: Action (ModelState state) a -> Set (Any Var)
type Rep (ModelState state) Source #
Instance details Defined in Test.QuickCheck.ContractModel.Internal.Spec type Rep (ModelState state) = D1 ('MetaData "ModelState" "Test.QuickCheck.ContractModel.Internal.Spec" "quickcheck-contractmodel-0.1.4.1-3bqn4RrQanG11zXTiHDaXF" 'False) (C1 ('MetaCons "ModelState" 'PrefixI 'True) ((S1 ('MetaSel ('Just "_currentSlot") 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 SlotNo) :: (S1 ('MetaSel ('Just "_balanceChanges") 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 (Map (AddressInEra Era) SymValue)) :: S1 ('MetaSel ('Just "_minted") 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 SymValue))) :: ((S1 ('MetaSel ('Just "_symbolics") 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 SymCollectionIndex) :: S1 ('MetaSel ('Just "_assertions") 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 [(String, Bool)])) :: (S1 ('MetaSel ('Just "_assertionsOk") 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 Bool) :: S1 ('MetaSel ('Just "_contractState") 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 state)))))
data Action (ModelState state) a
Instance details Defined in Test.QuickCheck.ContractModel.Internal.Model data Action (ModelState state) a where ContractAction :: forall state. Bool -> Action state -> Action (ModelState state) SymIndex Observation :: forall state. String -> (SymbolicSemantics -> ChainState -> Bool) -> Action (ModelState state) () WaitUntil :: forall state. SlotNo -> Action (ModelState state) ()
type StateType (DL state) Source #
Instance details Defined in Test.QuickCheck.ContractModel.DL type StateType (DL state) = state

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
Fields unSpec :: WriterT SymCreationIndex (ReaderT (Var SymIndex) (State (ModelState state))) a

Instances

Instances details

MonadState state (Spec state) Source #
Instance details Defined in Test.QuickCheck.ContractModel.Internal.Spec Methods get :: Spec state state put :: state -> Spec state () state :: (state -> (a, state)) -> Spec state a
Monad (Spec state) Source #
Instance details Defined in Test.QuickCheck.ContractModel.Internal.Spec 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 Test.QuickCheck.ContractModel.Internal.Spec 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 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 #
Instance details Defined in Test.QuickCheck.ContractModel.Internal.Spec 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 Test.QuickCheck.ContractModel.Internal.Spec type StateType (Spec state) = state

coerceSpec :: forall s s' a. Coercible s s' => Spec s a -> Spec s' a Source #

contractState :: forall state state. Lens (ModelState state) (ModelState state) state state Source #

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

currentSlotL :: forall state. Lens' (ModelState state) SlotNo Source #

balanceChangesL :: forall state. Lens' (ModelState state) (Map (AddressInEra Era) SymValue) Source #

mintedL :: forall state. Lens' (ModelState state) SymValue Source #

assertions :: forall state. Lens' (ModelState state) [(String, Bool)] Source #

assertionsOk :: forall state. Lens' (ModelState state) Bool Source #

symbolics :: forall state. Lens' (ModelState state) SymCollectionIndex 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 #

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 :: Ord (AddressInEra Era) => AddressInEra Era -> 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.

modState :: forall state a. Setter' (ModelState state) a -> (a -> a) -> Spec state () Source #

Modify a field in the ModelState

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 Test.QuickCheck.ContractModel.Internal.Spec Associated Types type StateType (Spec state) Source # Methods getModelState :: Spec state (ModelState (StateType (Spec state))) Source #
GetModelState (DL state) Source #
Instance details Defined in Test.QuickCheck.ContractModel.DL 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.

runSpec :: Spec state () -> Var SymIndex -> ModelState state -> ModelState state Source #

symbolicsCreatedBy :: Spec state () -> Var SymIndex -> ModelState state -> SymCreationIndex Source #

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.

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

Burn tokens. Equivalent to mint . inv.

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.

transfer Source #

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.

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

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