State maintained by the model.

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.

How a closed head's fanout is driven. A plain Fanout drains the head automatically, possibly in several steps; PartialFanoutStep hands the node one selection at a time and the node only drains what it was given. The two cannot be mixed: once a partial fanout started, Fanout is rejected.

Add a finalized commit to the head's UTxO and bump the on-chain version.

Remove a decommitted output from the head's UTxO (it leaves the L2 ledger with the snapshot carrying the decommit).

Account for a finalized decrement: bump the on-chain version.

Whether random RestartNode actions are generated. On: a restarted node recovers head state (event store), chain point, network consumer offset (etcd-style) and the full chain-sync localChainState history, so it converges under load like a real fail-recovery. Flip to False to drop the fail-recovery dimension if it ever proves flaky.

The default seed settles each deposit and decommit before the next action, see WorldState.

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

Exactly n distinct parties, for scripted scenarios (see partyKeys).

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.

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.

Deposit period used by all nodes and the performDeposit.

(Re-)create and start a single hydra node on the given event store, recovering its state from the store's events, and wait for it to be in sync with the chain. Shared by seedWorld and performRestartNode.

Deadline for deposits made by the model: far enough in the future that the deposit is still claimable once it activates (at created + depositActivation, with created up to half a deposit period ahead of submission) even when several deposits settle one after the other, each taking a few blocks. It expires at deadline - depositPeriod.

Submit a deposit and wait until every node has recorded it on chain. Its settlement is observed separately, see performObserveCommitFinalized.

Wait until every node has confirmed a snapshot claiming the given deposit (CommitApproved): the increment is now in flight.

Wait until every node has reported the increment claiming the given deposit for the n-th time. A wedged settlement surfaces here as a timeout.

Wait until every node's output history holds at least n outputs matching the predicate, or fail after observationTimeout.

Unlike waitUntilMatch this does not consume outputs, so settlements can be observed in any order (several may be in flight and finalize in an order the model does not control) and repeatedly (a settlement re-landing after a fork is reported again). It also does not swallow reports that arrive earlier than expected, e.g. a decrement observed on chain before its snapshot confirmed locally.

Wait until every node's output history satisfies the predicate, or fail after observationTimeout. See waitForOutputs.

How long an observation waits for the nodes to report something. Every observed step (a settlement landing, re-landing after a fork, a snapshot confirming) takes a handful of blocks of 20s, so an hour is generous while still failing a wedged head reasonably fast.

Request a decommit and wait until every node has confirmed the snapshot carrying it (DecommitApproved), i.e. the outputs have left the L2 ledger and the decrement is in flight. Its settlement is observed separately, see performObserveDecommitFinalized.

Wait until every node has reported the decrement distributing the given decommitted UTxO for the n-th time.

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.

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.

Send Fanout once the head is ready for it, without waiting for the fanout to complete.

Wait for the head to be finalized on the given party's node and return what the fanout distributed.

Hand the node a selection to fan out (manual mode) and wait until every node reports all of it distributed: over one or more partial steps, or by the final fanout if the selection drains the head.

Wait until every node has reported at least n partial fanout steps.

Crash a node (cancelling its main thread, so any in-flight inputs and in-memory-only state are lost) and start it again from its own event store, re-syncing the chain from genesis. Models a node operator restart / fail-recovery under load: the head must stay live through it.

Convert payment-style utxos into transaction outputs.

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.