Safe Haskell	None
Language	Haskell2010

Hydra.Model

Contents

The Model
- Generator Helper
Running the model
- Performing actions
- Utility functions

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

data WorldState = WorldState {
- hydraParties :: [(SigningKey HydraKey, CardanoSigningKey)]
- hydraState :: GlobalState
}
data GlobalState
- = Start
- | Idle {
  - idleParties :: [Party]
  - cardanoKeys :: [VerificationKey PaymentKey]
  - idleContestationPeriod :: ContestationPeriod
  }
- | Initial {
  - headParameters :: HeadParameters
  - commits :: Committed Payment
  - pendingCommits :: PendingCommits
  }
- | Open {
  - headParameters :: HeadParameters
  - offChainState :: OffChainState
  }
- | Final {
  - finalUTxO :: UTxOType Payment
  }
isInitialState :: GlobalState -> Bool
isOpenState :: GlobalState -> Bool
isFinalState :: GlobalState -> Bool
isIdleState :: GlobalState -> Bool
isPendingCommitFrom :: Party -> GlobalState -> Bool
data OffChainState = OffChainState {
- confirmedUTxO :: UTxOType Payment
- seenTransactions :: [Payment]
}
type ActualCommitted = UTxOType Payment
genSeed :: Gen (Action WorldState ())
genContestationPeriod :: Gen ContestationPeriod
genInit :: [(SigningKey HydraKey, b)] -> Gen (Action WorldState ())
genCommit' :: [(SigningKey HydraKey, CardanoSigningKey)] -> (SigningKey HydraKey, CardanoSigningKey) -> Gen (Action WorldState [(CardanoSigningKey, Value)])
genPayment :: WorldState -> Gen (Party, Payment)
unsafeConstructorName :: Show a => a -> String
partyKeys :: Gen [(SigningKey HydraKey, CardanoSigningKey)]
data Nodes m = Nodes {
- nodes :: Map Party (TestHydraClient Tx m)
- logger :: Tracer m (HydraLog Tx ())
- threads :: [Async m ()]
}
newtype RunState m = RunState {
- nodesState :: TVar m (Nodes m)
}
newtype RunMonad m a = RunMonad {
- runMonad :: ReaderT (RunState m) m a
}
data RunException
- = TransactionNotObserved Payment UTxO
- | UnexpectedParty Party
- | UnknownAddress AddressInEra [(AddressInEra, CardanoSigningKey)]
- | CannotFindSpendableUTxO Payment UTxO
seedWorld :: (MonadDelay m, MonadAsync m, MonadTimer m, MonadThrow (STM m), MonadLabelledSTM m, MonadFork m, MonadMask m) => [(SigningKey HydraKey, CardanoSigningKey)] -> ContestationPeriod -> RunMonad m ()
performCommit :: (MonadThrow m, MonadTimer m) => [CardanoSigningKey] -> Party -> [(CardanoSigningKey, Value)] -> RunMonad m ActualCommitted
performNewTx :: (MonadThrow m, MonadAsync m, MonadTimer m) => Party -> Payment -> RunMonad m ()
waitForOpen :: MonadDelay m => TestHydraClient tx m -> RunMonad m ()
sendsInput :: (MonadSTM m, MonadThrow m) => Party -> ClientInput Tx -> RunMonad m ()
performInit :: (MonadDelay m, MonadThrow m, MonadAsync m, MonadTimer m) => Party -> RunMonad m ()
performAbort :: (MonadDelay m, MonadThrow m, MonadAsync m, MonadTimer m) => Party -> RunMonad m ()
stopTheWorld :: MonadAsync m => RunMonad m ()
showFromAction :: (Show a => b) -> Action WorldState a -> b
checkOutcome :: WorldState -> Action WorldState a -> a -> Bool
waitForUTxOToSpend :: forall m. (MonadDelay m, MonadTimer m) => UTxO -> CardanoSigningKey -> Value -> TestHydraClient Tx m -> m (Either UTxO (TxIn, TxOut CtxUTxO))
isOwned :: CardanoSigningKey -> (TxIn, TxOut ctx) -> Bool

The Model

data WorldState #

State maintained by the model.

Constructors

WorldState
Fields hydraParties :: [(SigningKey HydraKey, CardanoSigningKey)] List of parties identified by both signing keys required to run protocol. This list must not contain any duplicated key. hydraState :: GlobalState Expected consensus state All nodes should be in the same state.

Instances

Instances details

Eq WorldState #
Instance details Defined in Hydra.Model Methods (==) :: WorldState -> WorldState -> Bool # (/=) :: WorldState -> WorldState -> Bool #
Show WorldState #
Instance details Defined in Hydra.Model Methods showsPrec :: Int -> WorldState -> ShowS # show :: WorldState -> String # showList :: [WorldState] -> ShowS #
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 Seed :: {..} -> Action WorldState () Init :: Party -> Action WorldState () Commit :: Party -> UTxOType Payment -> Action WorldState ActualCommitted Abort :: Party -> Action WorldState () NewTx :: Party -> Payment -> Action WorldState () Wait :: DiffTime -> Action WorldState () ObserveConfirmedTx :: Payment -> Action WorldState () ObserveHeadIsOpen :: Action WorldState () StopTheWorld :: Action WorldState ()

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
Fields idleParties :: [Party] cardanoKeys :: [VerificationKey PaymentKey] idleContestationPeriod :: ContestationPeriod
Initial
Fields headParameters :: HeadParameters commits :: Committed Payment pendingCommits :: PendingCommits
Open
Fields headParameters :: HeadParameters offChainState :: OffChainState
Final
Fields finalUTxO :: UTxOType Payment

Instances

Instances details

Eq GlobalState #
Instance details Defined in Hydra.Model Methods (==) :: GlobalState -> GlobalState -> Bool # (/=) :: GlobalState -> GlobalState -> Bool #
Show GlobalState #
Instance details Defined in Hydra.Model Methods showsPrec :: Int -> GlobalState -> ShowS # show :: GlobalState -> String # showList :: [GlobalState] -> ShowS #

isInitialState :: GlobalState -> Bool #

isOpenState :: GlobalState -> Bool #

isFinalState :: GlobalState -> Bool #

isIdleState :: GlobalState -> Bool #

isPendingCommitFrom :: Party -> GlobalState -> Bool #

data OffChainState #

Constructors

OffChainState
Fields confirmedUTxO :: UTxOType Payment seenTransactions :: [Payment]

Instances

Instances details

Eq OffChainState #
Instance details Defined in Hydra.Model Methods (==) :: OffChainState -> OffChainState -> Bool # (/=) :: OffChainState -> OffChainState -> Bool #
Show OffChainState #
Instance details Defined in Hydra.Model Methods showsPrec :: Int -> OffChainState -> ShowS # show :: OffChainState -> String # showList :: [OffChainState] -> ShowS #

type ActualCommitted = UTxOType Payment #

Generator Helper

genSeed :: Gen (Action WorldState ()) #

genContestationPeriod :: Gen ContestationPeriod #

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

genCommit' :: [(SigningKey HydraKey, CardanoSigningKey)] -> (SigningKey HydraKey, CardanoSigningKey) -> Gen (Action WorldState [(CardanoSigningKey, Value)]) #

genPayment :: WorldState -> Gen (Party, Payment) #

unsafeConstructorName :: Show a => a -> String #

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 nodesState :: TVar m (Nodes m)

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 runMonad :: ReaderT (RunState m) m a

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

data RunException #

Constructors

TransactionNotObserved Payment UTxO
UnexpectedParty Party
UnknownAddress AddressInEra [(AddressInEra, CardanoSigningKey)]
CannotFindSpendableUTxO Payment UTxO

Instances

Instances details

Eq RunException #
Instance details Defined in Hydra.Model Methods (==) :: RunException -> RunException -> Bool # (/=) :: RunException -> RunException -> Bool #
Show RunException #
Instance details Defined in Hydra.Model Methods showsPrec :: Int -> RunException -> ShowS # show :: RunException -> String # showList :: [RunException] -> ShowS #
Exception RunException #
Instance details Defined in Hydra.Model Methods toException :: RunException -> SomeException # fromException :: SomeException -> Maybe RunException # displayException :: RunException -> String #

Performing actions

seedWorld :: (MonadDelay m, MonadAsync m, MonadTimer m, MonadThrow (STM m), MonadLabelledSTM m, MonadFork m, MonadMask m) => [(SigningKey HydraKey, CardanoSigningKey)] -> ContestationPeriod -> RunMonad m () #

performCommit :: (MonadThrow m, MonadTimer m) => [CardanoSigningKey] -> Party -> [(CardanoSigningKey, Value)] -> RunMonad m ActualCommitted #

performNewTx :: (MonadThrow m, MonadAsync m, MonadTimer m) => Party -> Payment -> RunMonad m () #

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.

sendsInput :: (MonadSTM m, MonadThrow m) => Party -> ClientInput Tx -> RunMonad m () #

performInit :: (MonadDelay m, MonadThrow m, MonadAsync m, MonadTimer m) => Party -> RunMonad m () #

performAbort :: (MonadDelay m, MonadThrow m, MonadAsync m, MonadTimer m) => Party -> RunMonad m () #

stopTheWorld :: MonadAsync m => RunMonad m () #

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 #

waitForUTxOToSpend :: forall m. (MonadDelay m, MonadTimer m) => UTxO -> CardanoSigningKey -> Value -> TestHydraClient Tx m -> m (Either UTxO (TxIn, TxOut CtxUTxO)) #

isOwned :: CardanoSigningKey -> (TxIn, TxOut ctx) -> Bool #