Safe Haskell | None |
---|---|
Language | Haskell2010 |
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
- data WorldState = WorldState {}
- data GlobalState
- isInitialState :: GlobalState -> Bool
- isOpenState :: GlobalState -> Bool
- isFinalState :: GlobalState -> Bool
- isIdleState :: GlobalState -> Bool
- isPendingCommitFrom :: Party -> GlobalState -> Bool
- data OffChainState = OffChainState {}
- 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 {}
- newtype RunState m = RunState {
- nodesState :: TVar m (Nodes m)
- newtype RunMonad m a = RunMonad {}
- data RunException
- 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
|
Instances
Eq WorldState # | |
Defined in Hydra.Model | |
Show WorldState # | |
Defined in Hydra.Model Methods showsPrec :: Int -> WorldState -> ShowS # show :: WorldState -> String # showList :: [WorldState] -> ShowS # | |
StateModel WorldState # | Basic instantiation of |
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)] nextState :: Typeable a => WorldState -> Action WorldState a -> Var a -> WorldState precondition :: WorldState -> Action WorldState a -> Bool | |
HasVariables WorldState # | |
Defined in Hydra.Model Methods getAllVariables :: WorldState -> Set (Any Var) | |
DynLogicModel WorldState # | |
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) # | |
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) # | |
Defined in Hydra.Model Methods (==) :: Action WorldState a -> Action WorldState a -> Bool # (/=) :: Action WorldState a -> Action WorldState a -> Bool # | |
Show (Action WorldState a) # | |
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) # | |
Defined in Hydra.Model Methods getAllVariables :: Action WorldState a -> Set (Any Var) | |
data Action WorldState a # | |
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 | |
Fields | |
Initial | |
Fields | |
Open | |
Fields | |
Final | |
Instances
Eq GlobalState # | |
Defined in Hydra.Model | |
Show GlobalState # | |
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 |
Instances
Eq OffChainState # | |
Defined in Hydra.Model Methods (==) :: OffChainState -> OffChainState -> Bool # (/=) :: OffChainState -> OffChainState -> Bool # | |
Show OffChainState # | |
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 ()) #
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
Concrete state needed to run actions against the implementation.
This state is used and might be updated when actually perform
ing actions generated from the StateModel
.
Constructors
Nodes | |
Fields
|
Constructors
RunState | |
Fields
|
Our execution MonadTrans
former.
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.
Instances
MonadTrans RunMonad # | |
Defined in Hydra.Model | |
(MonadAsync m, MonadFork m, MonadMask m, MonadTimer m, MonadThrow (STM m), MonadLabelledSTM m) => RunModel WorldState (RunMonad m) # | |
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) # | |
Functor m => Functor (RunMonad m) # | |
Applicative m => Applicative (RunMonad m) # | |
Defined in Hydra.Model | |
MonadThrow m => MonadThrow (RunMonad m) # | |
MonadSTM m => MonadState (Nodes m) (RunMonad m) # | |
Monad m => MonadReader (RunState m) (RunMonad m) # | |
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. |
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
Eq RunException # | |
Defined in Hydra.Model | |
Show RunException # | |
Defined in Hydra.Model Methods showsPrec :: Int -> RunException -> ShowS # show :: RunException -> String # showList :: [RunException] -> ShowS # | |
Exception RunException # | |
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 show
able 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)) #