Safe Haskell	Safe-Inferred
Language	GHC2021

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
  - toCommit :: Uncommitted
  }
- | Initial {
  - headParameters :: HeadParameters
  - commits :: Committed Payment
  - pendingCommits :: Uncommitted
  }
- | Open {
  - headParameters :: HeadParameters
  - offChainState :: OffChainState
  - committed :: Committed Payment
  }
- | Closed {
  - closedUTxO :: UTxOType Payment
  }
- | Final {
  - finalUTxO :: UTxOType Payment
  }
isPendingCommitFrom :: Party -> GlobalState -> Bool
type Uncommitted = Map Party (UTxOType Payment)
newtype OffChainState = OffChainState {
- confirmedUTxO :: UTxOType Payment
}
type ActualCommitted = UTxOType Payment
genSeed :: Gen (Action WorldState ())
genToCommit :: (SigningKey HydraKey, CardanoSigningKey) -> Gen (Map Party [(CardanoSigningKey, Value)])
genContestationPeriod :: Gen ContestationPeriod
genInit :: [(SigningKey HydraKey, b)] -> Gen (Action WorldState ())
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 ()]
- chain :: SimulatedChainNetwork Tx 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 :: (MonadAsync m, MonadTimer m, MonadThrow (STM m), MonadLabelledSTM m, MonadFork m, MonadMask m, MonadDelay m) => [(SigningKey HydraKey, CardanoSigningKey)] -> ContestationPeriod -> Uncommitted -> RunMonad m ()
performCommit :: (MonadThrow m, MonadTimer m) => [CardanoSigningKey] -> Party -> [(CardanoSigningKey, Value)] -> RunMonad m ActualCommitted
performNewTx :: (MonadThrow m, MonadAsync m, MonadTimer m, MonadDelay m) => Party -> Payment -> RunMonad m Payment
waitForOpen :: MonadDelay m => TestHydraClient tx m -> RunMonad m ()
waitForReadyToFanout :: MonadDelay m => TestHydraClient tx m -> RunMonad m ()
sendsInput :: (MonadSTM m, MonadThrow m) => Party -> ClientInput Tx -> RunMonad m ()
performInit :: (MonadThrow m, MonadAsync m, MonadTimer m) => Party -> RunMonad m ()
performAbort :: (MonadThrow m, MonadAsync m, MonadTimer m) => Party -> RunMonad m ()
performClose :: (MonadThrow m, MonadAsync m, MonadTimer m, MonadDelay m) => Party -> RunMonad m ()
performFanout :: (MonadThrow m, MonadAsync m, MonadDelay m) => Party -> RunMonad m UTxO
performCloseWithInitialSnapshot :: (MonadThrow m, MonadTimer m, MonadDelay m, MonadAsync m) => WorldState -> Party -> RunMonad m ()
performRollbackAndForward :: (MonadThrow m, MonadTimer m) => Natural -> RunMonad m ()
stopTheWorld :: MonadAsync m => RunMonad m ()
toTxOuts :: [(CardanoSigningKey, Value)] -> [TxOut CtxUTxO]
toRealUTxO :: UTxOType Payment -> UTxOType Tx
mkTxOut :: CardanoSigningKey -> Value -> TxOut CtxUTxO
mkMockTxIn :: CardanoSigningKey -> Word -> TxIn
showFromAction :: (Show a => b) -> Action WorldState a -> b
(===) :: (Eq a, Show a, Monad m) => a -> a -> PostconditionM m Bool
waitForUTxOToSpend :: forall m. (MonadTimer m, MonadDelay m) => UTxO -> CardanoSigningKey -> Value -> TestHydraClient Tx m -> m (Either UTxO (TxIn, TxOut CtxUTxO))
isOwned :: CardanoSigningKey -> (TxIn, TxOut ctx) -> Bool
headIsOpen :: ServerOutput tx -> Bool
headIsReadyToFanout :: ServerOutput tx -> Bool

The Model

data WorldState Source #

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

Show WorldState Source #
Instance details Defined in Hydra.Model Methods showsPrec :: Int -> WorldState -> ShowS Source # show :: WorldState -> String Source # showList :: [WorldState] -> ShowS Source #
Eq WorldState Source #
Instance details Defined in Hydra.Model Methods (==) :: WorldState -> WorldState -> Bool Source # (/=) :: WorldState -> WorldState -> Bool Source #
DynLogicModel WorldState Source #
Instance details Defined in Hydra.Model Methods restricted :: Action WorldState a -> Bool
StateModel WorldState Source #	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 failureNextState :: Typeable a => WorldState -> Action WorldState a -> WorldState precondition :: WorldState -> Action WorldState a -> Bool validFailingAction :: WorldState -> Action WorldState a -> Bool
HasVariables WorldState Source #
Instance details Defined in Hydra.Model Methods getAllVariables :: WorldState -> Set (Any Var)
(MonadAsync m, MonadFork m, MonadMask m, MonadTimer m, MonadThrow (STM m), MonadLabelledSTM m, MonadDelay m) => RunModel WorldState (RunMonad m) Source #
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 postconditionOnFailure :: (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
Show (Action WorldState a) Source #
Instance details Defined in Hydra.Model Methods showsPrec :: Int -> Action WorldState a -> ShowS Source # show :: Action WorldState a -> String Source # showList :: [Action WorldState a] -> ShowS Source #
Eq (Action WorldState a) Source #
Instance details Defined in Hydra.Model Methods (==) :: Action WorldState a -> Action WorldState a -> Bool Source # (/=) :: Action WorldState a -> Action WorldState a -> Bool Source #
HasVariables (Action WorldState a) Source #
Instance details Defined in Hydra.Model Methods getAllVariables :: Action WorldState a -> Set (Any Var)
data Action WorldState a Source #
Instance details Defined in Hydra.Model data Action WorldState a where Seed :: {..} -> Action WorldState () Init :: Party -> Action WorldState () Commit :: Party -> UTxOType Payment -> Action WorldState (UTxOType Payment) Abort :: Party -> Action WorldState () Close :: Party -> Action WorldState () Fanout :: Party -> Action WorldState (UTxO' (TxOut CtxUTxO Era)) NewTx :: Party -> Payment -> Action WorldState Payment Wait :: DiffTime -> Action WorldState () ObserveConfirmedTx :: Var Payment -> Action WorldState () ObserveHeadIsOpen :: Action WorldState () RollbackAndForward :: Natural -> Action WorldState () CloseWithInitialSnapshot :: Party -> Action WorldState () StopTheWorld :: Action WorldState ()

data GlobalState Source #

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 toCommit :: Uncommitted
Initial
Fields headParameters :: HeadParameters commits :: Committed Payment pendingCommits :: Uncommitted
Open
Fields headParameters :: HeadParameters offChainState :: OffChainState committed :: Committed Payment
Closed
Fields closedUTxO :: UTxOType Payment
Final
Fields finalUTxO :: UTxOType Payment

Instances

Instances details

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

isPendingCommitFrom :: Party -> GlobalState -> Bool Source #

type Uncommitted = Map Party (UTxOType Payment) Source #

newtype OffChainState Source #

Constructors

OffChainState
Fields confirmedUTxO :: UTxOType Payment

Instances

Instances details

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

type ActualCommitted = UTxOType Payment Source #

Generator Helper

genSeed :: Gen (Action WorldState ()) Source #

genToCommit :: (SigningKey HydraKey, CardanoSigningKey) -> Gen (Map Party [(CardanoSigningKey, Value)]) Source #

genContestationPeriod :: Gen ContestationPeriod Source #

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

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

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

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

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

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
chain :: SimulatedChainNetwork Tx m

Instances

Instances details

MonadSTM m => MonadState (Nodes m) (RunMonad m) Source #
Instance details Defined in Hydra.Model Methods get :: RunMonad m (Nodes m) Source # put :: Nodes m -> RunMonad m () Source # state :: (Nodes m -> (a, Nodes m)) -> RunMonad m a Source #

newtype RunState m Source #

Constructors

RunState
Fields nodesState :: TVar m (Nodes m)

Instances

Instances details

Monad m => MonadReader (RunState m) (RunMonad m) Source #
Instance details Defined in Hydra.Model Methods ask :: RunMonad m (RunState m) Source # local :: (RunState m -> RunState m) -> RunMonad m a -> RunMonad m a Source # reader :: (RunState m -> a) -> RunMonad m a Source #

newtype RunMonad m a Source #

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 Source #
Instance details Defined in Hydra.Model Methods lift :: Monad m => m a -> RunMonad m a Source #
(MonadAsync m, MonadFork m, MonadMask m, MonadTimer m, MonadThrow (STM m), MonadLabelledSTM m, MonadDelay m) => RunModel WorldState (RunMonad m) Source #
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 postconditionOnFailure :: (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
Applicative m => Applicative (RunMonad m) Source #
Instance details Defined in Hydra.Model Methods pure :: a -> RunMonad m a Source # (<>) :: RunMonad m (a -> b) -> RunMonad m a -> RunMonad m b Source # liftA2 :: (a -> b -> c) -> RunMonad m a -> RunMonad m b -> RunMonad m c Source # (>) :: RunMonad m a -> RunMonad m b -> RunMonad m b Source # (<*) :: RunMonad m a -> RunMonad m b -> RunMonad m a Source #
Functor m => Functor (RunMonad m) Source #
Instance details Defined in Hydra.Model Methods fmap :: (a -> b) -> RunMonad m a -> RunMonad m b Source # (<$) :: a -> RunMonad m b -> RunMonad m a Source #
Monad m => Monad (RunMonad m) Source #
Instance details Defined in Hydra.Model Methods (>>=) :: RunMonad m a -> (a -> RunMonad m b) -> RunMonad m b Source # (>>) :: RunMonad m a -> RunMonad m b -> RunMonad m b Source # return :: a -> RunMonad m a Source #
MonadThrow m => MonadThrow (RunMonad m) Source #
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
Monad m => MonadReader (RunState m) (RunMonad m) Source #
Instance details Defined in Hydra.Model Methods ask :: RunMonad m (RunState m) Source # local :: (RunState m -> RunState m) -> RunMonad m a -> RunMonad m a Source # reader :: (RunState m -> a) -> RunMonad m a Source #
MonadSTM m => MonadState (Nodes m) (RunMonad m) Source #
Instance details Defined in Hydra.Model Methods get :: RunMonad m (Nodes m) Source # put :: Nodes m -> RunMonad m () Source # state :: (Nodes m -> (a, Nodes m)) -> RunMonad m a Source #
type Realized (RunMonad m) a Source #	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 Source #

Constructors

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

Instances

Instances details

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

Performing actions

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

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

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

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

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.

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

Wait for the head to be closed 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 () Source #

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

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

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

performFanout :: (MonadThrow m, MonadAsync m, MonadDelay m) => Party -> RunMonad m UTxO Source #

performCloseWithInitialSnapshot :: (MonadThrow m, MonadTimer m, MonadDelay m, MonadAsync m) => WorldState -> Party -> RunMonad m () Source #

performRollbackAndForward :: (MonadThrow m, MonadTimer m) => Natural -> RunMonad m () Source #

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

Utility functions

toTxOuts :: [(CardanoSigningKey, Value)] -> [TxOut CtxUTxO] Source #

Convert payment-style utxos into transaction outputs.

toRealUTxO :: UTxOType Payment -> UTxOType Tx Source #

Convert payment-style utxos into real utxos. The Payment tx domain is smaller than UTxO and we map every unique signer + value entry to a mocked TxIn on the real cardano domain.

mkTxOut :: CardanoSigningKey -> Value -> TxOut CtxUTxO Source #

mkMockTxIn :: CardanoSigningKey -> Word -> TxIn Source #

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

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.

(===) :: (Eq a, Show a, Monad m) => a -> a -> PostconditionM m Bool Source #

Like ===, but works in PostconditionM.

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

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

headIsOpen :: ServerOutput tx -> Bool Source #

headIsReadyToFanout :: ServerOutput tx -> Bool Source #