tests
Safe HaskellNone
LanguageHaskell2010

Hydra.Model

Description

A Model of the Hydra head Protocol.

This model integrates in a single state-machine like abstraction the whole behaviour of a Hydra Head, taking into account both on-chain state and contracts, and off-chain interactions. It is written from the point of view of a pre-defined set of Hydra node operators that want to create a channel between them. It's a "happy path" model that does not implement any kind of adversarial behaviour and whose transactions are very simple: Each tx is a payment of one Ada-only UTxO transferred to another party in full, without any change.

More intricate and specialised models shall be developed once we get a firmer grasp of the whole framework, injecting faults, taking into account more parts of the stack, modelling more complex transactions schemes...

Synopsis

The Model

data WorldState #

State maintained by the model.

Constructors

WorldState 

Fields

Instances

Instances details
Eq WorldState # 
Instance details

Defined in Hydra.Model

Show WorldState # 
Instance details

Defined in Hydra.Model

StateModel WorldState #

Basic instantiation of StateModel for our WorldState state.

Instance details

Defined in Hydra.Model

Associated Types

data Action WorldState a

Methods

actionName :: Action WorldState a -> String

arbitraryAction :: VarContext -> WorldState -> Gen (Any (Action WorldState))

shrinkAction :: Typeable a => VarContext -> WorldState -> Action WorldState a -> [Any (Action WorldState)]

initialState :: WorldState

nextState :: Typeable a => WorldState -> Action WorldState a -> Var a -> WorldState

precondition :: WorldState -> Action WorldState a -> Bool

HasVariables WorldState # 
Instance details

Defined in Hydra.Model

Methods

getAllVariables :: WorldState -> Set (Any Var)

DynLogicModel WorldState # 
Instance details

Defined in Hydra.Model

Methods

restricted :: Action WorldState a -> Bool

(MonadAsync m, MonadFork m, MonadMask m, MonadTimer m, MonadThrow (STM m), MonadLabelledSTM m) => RunModel WorldState (RunMonad m) # 
Instance details

Defined in Hydra.Model

Methods

perform :: Typeable a => WorldState -> Action WorldState a -> LookUp (RunMonad m) -> RunMonad m (Realized (RunMonad m) a)

postcondition :: (WorldState, WorldState) -> Action WorldState a -> LookUp (RunMonad m) -> Realized (RunMonad m) a -> PostconditionM (RunMonad m) Bool

monitoring :: (WorldState, WorldState) -> Action WorldState a -> LookUp (RunMonad m) -> Realized (RunMonad m) a -> Property -> Property

Eq (Action WorldState a) # 
Instance details

Defined in Hydra.Model

Methods

(==) :: Action WorldState a -> Action WorldState a -> Bool #

(/=) :: Action WorldState a -> Action WorldState a -> Bool #

Show (Action WorldState a) # 
Instance details

Defined in Hydra.Model

Methods

showsPrec :: Int -> Action WorldState a -> ShowS #

show :: Action WorldState a -> String #

showList :: [Action WorldState a] -> ShowS #

HasVariables (Action WorldState a) # 
Instance details

Defined in Hydra.Model

Methods

getAllVariables :: Action WorldState a -> Set (Any Var)

data Action WorldState a # 
Instance details

Defined in Hydra.Model

data Action WorldState a where

data GlobalState #

Global state of the Head protocol. While each participant in the Hydra Head protocol has its own private view of the state, we model the expected global state whose properties stem from the consensus built into the Head protocol. In other words, this state is what each node's local state should be eventually.

Constructors

Start

Start of the "world". This state is left implicit in the node's logic as it represents that state where the node does not even exist.

Idle 
Initial 
Open 
Final 

Instances

Instances details
Eq GlobalState # 
Instance details

Defined in Hydra.Model

Show GlobalState # 
Instance details

Defined in Hydra.Model

data OffChainState #

Instances

Instances details
Eq OffChainState # 
Instance details

Defined in Hydra.Model

Show OffChainState # 
Instance details

Defined in Hydra.Model

Generator Helper

genSeed :: Gen (Action WorldState ()) #

genInit :: [(SigningKey HydraKey, b)] -> Gen (Action WorldState ()) #

partyKeys :: Gen [(SigningKey HydraKey, CardanoSigningKey)] #

Generate a list of pairs of Hydra/Cardano signing keys. All the keys in this list are guaranteed to be unique.

Running the model

data Nodes m #

Concrete state needed to run actions against the implementation. This state is used and might be updated when actually performing actions generated from the StateModel.

Constructors

Nodes 

Fields

  • nodes :: Map Party (TestHydraClient Tx m)

    Map from party identifiers to a handle for interacting with a node.

  • logger :: Tracer m (HydraLog Tx ())

    Logger used by each node. The reason we put this here is because the concrete value needs to be instantiated upon the test run initialisation, outiside of the model.

  • threads :: [Async m ()]

    List of threads spawned when executing RunMonad

Instances

Instances details
MonadSTM m => MonadState (Nodes m) (RunMonad m) # 
Instance details

Defined in Hydra.Model

Methods

get :: RunMonad m (Nodes m) #

put :: Nodes m -> RunMonad m () #

state :: (Nodes m -> (a, Nodes m)) -> RunMonad m a #

newtype RunState m #

Constructors

RunState 

Fields

Instances

Instances details
Monad m => MonadReader (RunState m) (RunMonad m) # 
Instance details

Defined in Hydra.Model

Methods

ask :: RunMonad m (RunState m) #

local :: (RunState m -> RunState m) -> RunMonad m a -> RunMonad m a #

reader :: (RunState m -> a) -> RunMonad m a #

newtype RunMonad m a #

Our execution MonadTransformer.

This type is needed in order to keep the execution monad m abstract and thus simplify the definition of the RunModel instance which requires a proper definition of Realized type family. See this issue for a discussion on why this monad is needed.

We could perhaps getaway with it and just have a type based on IOSim monad but this is cumbersome to write.

Constructors

RunMonad 

Fields

Instances

Instances details
MonadTrans RunMonad # 
Instance details

Defined in Hydra.Model

Methods

lift :: Monad m => m a -> RunMonad m a #

(MonadAsync m, MonadFork m, MonadMask m, MonadTimer m, MonadThrow (STM m), MonadLabelledSTM m) => RunModel WorldState (RunMonad m) # 
Instance details

Defined in Hydra.Model

Methods

perform :: Typeable a => WorldState -> Action WorldState a -> LookUp (RunMonad m) -> RunMonad m (Realized (RunMonad m) a)

postcondition :: (WorldState, WorldState) -> Action WorldState a -> LookUp (RunMonad m) -> Realized (RunMonad m) a -> PostconditionM (RunMonad m) Bool

monitoring :: (WorldState, WorldState) -> Action WorldState a -> LookUp (RunMonad m) -> Realized (RunMonad m) a -> Property -> Property

Monad m => Monad (RunMonad m) # 
Instance details

Defined in Hydra.Model

Methods

(>>=) :: RunMonad m a -> (a -> RunMonad m b) -> RunMonad m b #

(>>) :: RunMonad m a -> RunMonad m b -> RunMonad m b #

return :: a -> RunMonad m a #

Functor m => Functor (RunMonad m) # 
Instance details

Defined in Hydra.Model

Methods

fmap :: (a -> b) -> RunMonad m a -> RunMonad m b #

(<$) :: a -> RunMonad m b -> RunMonad m a #

Applicative m => Applicative (RunMonad m) # 
Instance details

Defined in Hydra.Model

Methods

pure :: a -> RunMonad m a #

(<*>) :: RunMonad m (a -> b) -> RunMonad m a -> RunMonad m b #

liftA2 :: (a -> b -> c) -> RunMonad m a -> RunMonad m b -> RunMonad m c #

(*>) :: RunMonad m a -> RunMonad m b -> RunMonad m b #

(<*) :: RunMonad m a -> RunMonad m b -> RunMonad m a #

MonadThrow m => MonadThrow (RunMonad m) # 
Instance details

Defined in Hydra.Model

Methods

throwIO :: Exception e => e -> RunMonad m a #

bracket :: RunMonad m a -> (a -> RunMonad m b) -> (a -> RunMonad m c) -> RunMonad m c #

bracket_ :: RunMonad m a -> RunMonad m b -> RunMonad m c -> RunMonad m c #

finally :: RunMonad m a -> RunMonad m b -> RunMonad m a #

MonadSTM m => MonadState (Nodes m) (RunMonad m) # 
Instance details

Defined in Hydra.Model

Methods

get :: RunMonad m (Nodes m) #

put :: Nodes m -> RunMonad m () #

state :: (Nodes m -> (a, Nodes m)) -> RunMonad m a #

Monad m => MonadReader (RunState m) (RunMonad m) # 
Instance details

Defined in Hydra.Model

Methods

ask :: RunMonad m (RunState m) #

local :: (RunState m -> RunState m) -> RunMonad m a -> RunMonad m a #

reader :: (RunState m -> a) -> RunMonad m a #

type Realized (RunMonad m) a #

This type family is needed to link the _actual_ output from runnign actions with the ones that are modelled.

In our case we can keep things simple and use the same types on both side of the fence.

Instance details

Defined in Hydra.Model

type Realized (RunMonad m) a = a

Performing actions

waitForOpen :: MonadDelay m => TestHydraClient tx m -> RunMonad m () #

Wait for the head to be open by searching from the beginning. Note that there rollbacks or multiple life-cycles of heads are not handled here.

Utility functions

showFromAction :: (Show a => b) -> Action WorldState a -> b #

Bring Show instance in scope drawing it from the Action type.

This is a neat trick to provide showable results from action in a context where there's no explicit `Show a` instance, eg. in the monitoring and postcondition functions. We don't have access to an a directly because its value depends on type family Realized.

checkOutcome :: WorldState -> Action WorldState a -> a -> Bool #