diff --git a/hydra-node/src/Hydra/HeadLogic.hs b/hydra-node/src/Hydra/HeadLogic.hs index 3fab99f06d0..032e856a58b 100644 --- a/hydra-node/src/Hydra/HeadLogic.hs +++ b/hydra-node/src/Hydra/HeadLogic.hs @@ -414,7 +414,7 @@ onOpenNetworkReqSn env ledger st otherParty sv sn requestedTxIds mDecommitTx = waitNoSnapshotInFlight $ -- Spec: require ̅S.𝑈 ◦ txω ≠ ⊥ -- ηω ← combine(outputs(txω)) - -- 𝑈_active ← ̅S.𝑈 ◦ txω + -- 𝑈_active ← ̅S.𝑈 ◦ txω \ outputs(txω) requireApplicableDecommitTx $ \(activeUTxO, mUtxoToDecommit) -> -- Resolve transactions by-id waitResolvableTxs $ \requestedTxs -> do @@ -1100,10 +1100,8 @@ update env ledger st ev = case (st, ev) of (Open openState, NetworkInput ttl (ReceivedMessage{msg = ReqTx tx})) -> onOpenNetworkReqTx env ledger openState ttl tx (Open openState, NetworkInput _ (ReceivedMessage{sender, msg = ReqSn sv sn txIds decommitTx})) -> - -- XXX: ttl == 0 not handled for ReqSn onOpenNetworkReqSn env ledger openState sender sv sn txIds decommitTx (Open openState, NetworkInput _ (ReceivedMessage{sender, msg = AckSn snapshotSignature sn})) -> - -- XXX: ttl == 0 not handled for AckSn onOpenNetworkAckSn env openState sender snapshotSignature sn ( Open openState@OpenState{headId = ourHeadId} , ChainInput Observation{observedTx = OnCloseTx{headId, snapshotNumber = closedSnapshotNumber, contestationDeadline}, newChainState} diff --git a/hydra-node/src/Hydra/HeadLogic/State.hs b/hydra-node/src/Hydra/HeadLogic/State.hs index 4e897b97f58..b52aa21b651 100644 --- a/hydra-node/src/Hydra/HeadLogic/State.hs +++ b/hydra-node/src/Hydra/HeadLogic/State.hs @@ -144,13 +144,13 @@ data CoordinatedHeadState tx = CoordinatedHeadState -- ^ Map containing all the transactions ever seen by this node and not yet -- included in a snapshot. Spec: Tall , confirmedSnapshot :: ConfirmedSnapshot tx - -- ^ The latest confirmed snapshot. Spec: U̅, s̅ and σ̅ + -- ^ The latest confirmed snapshot. Spec: S̅ , seenSnapshot :: SeenSnapshot tx -- ^ Last seen snapshot and signatures accumulator. Spec: Û, ŝ and Σ̂ , decommitTx :: Maybe tx -- ^ Pending decommit transaction. Spec: txω , version :: SnapshotVersion - -- ^ Last seen open state version. + -- ^ Last seen open state version. Spec: ̂v } deriving stock (Generic) diff --git a/spec/offchain.tex b/spec/offchain.tex index 0b5a6d39cf5..f6cfc220998 100644 --- a/spec/offchain.tex +++ b/spec/offchain.tex @@ -13,20 +13,20 @@ \section{Off-Chain Protocol}\label{sec:offchain} \item On-chain protocol transactions as introduced in Section~\ref{sec:on-chain}, which are posted to the mainchain and can be observed by all actors: - \begin{itemize} - \item $\mathtt{initialTx}$: initiates a head - \item $\mathtt{commitTx}$: commits UTxO to an initializing head - \item $\mathtt{collectComTx}$: opens a head - \red{\item $\mathtt{decrementTx}$: removes UTxO from an open head} - \item $\mathtt{closeTx}$: closes a head - \item $\mathtt{contestTx}$: contests a closed head - % NOTE: fanout not mentioned because not needed in off-chain protocol - % description - \end{itemize} + \begin{itemize} + \item $\mathtt{initialTx}$: initiates a head + \item $\mathtt{commitTx}$: commits UTxO to an initializing head + \item $\mathtt{collectComTx}$: opens a head + \item $\mathtt{decrementTx}$: removes UTxO from an open head + \item $\mathtt{closeTx}$: closes a head + \item $\mathtt{contestTx}$: contests a closed head + % NOTE: fanout not mentioned because not needed in off-chain protocol + % description + \end{itemize} \item Off-chain network messages sent between protocol actors (parties): \begin{itemize} \item $\hpRT$: to request a transaction to be included in the next snapshot - \red{\item $\hpRD$: to request exclusion of UTxO via a decommit transaction} + \item $\hpRD$: to request exclusion of UTxO via a decommit transaction \item $\hpRS$: to request a snapshot to be created \& signed by every head member \item $\hpAS$: to acknowledge a snapshot by replying with their signatures \end{itemize} @@ -108,7 +108,7 @@ \subsection{Variables} party's local state consists of the following variables: \begin{itemize} - \item \red{$\hatv$: Last seen open state version.} + \item $\hatv$: Last seen open state version. \item $\hats$: Sequence number of latest seen snapshot. \item $\hatSigma \in {(\tyNatural \times \tyBytes)}^{*}$: Accumulator of signatures of the latest seen snapshot, indexed by parties. @@ -116,21 +116,20 @@ \subsection{Variables} applying $\hatmT$ to $\bar{S}.U$ to validate requested transactions. \item $\hatmT \in \mT^{*}$: List of transactions applied locally and pending inclusion in a snapshot (if this party is the next leader). - \item \red{$\tx_{\omega} \in \mathcal{T}^{?}$: Pending decommit transaction, whose outputs are to be decommitted from the head. May be $\bot$ if nothing to decommit.} - \item \red{$\bar{\mc S}$: Snapshot object of the latest confirmed snapshot which contains: - \begin{center} - \begin{tabular}{|l|l|}\hline - $\bar{\mc S}.v$ & snapshot version \\ \hline - $\bar{\mc S}.s$ & snapshot number \\ \hline - $\bar{\mc S}.T$ & set of transactions relating this snapshot to its predecessor \\ \hline - $\bar{\mc S}.U$ & snapshotted UTxO set \\ \hline - $\bar{\mc S}.\tx_{\omega}$ & optional decommit transaction \\ \hline - $\bar{\mc S}.\sigma$ & multisignature \\ \hline - \end{tabular} - \end{center} - The function $\Sno(v,n,T,U,\tx_{\omega})$ initializes a snapshot object with no multi-signature set. - \todo{handwavy; types?} - } + \item $\tx_{\omega} \in \mathcal{T}^{?}$: Pending decommit transaction, whose outputs are to be decommitted from the head. May be $\bot$ if nothing to decommit. + \item $\bar{\mc S}$: Snapshot object of the latest confirmed snapshot which contains: + \begin{center} + \begin{tabular}{|l|l|}\hline + $\bar{\mc S}.v$ & snapshot version \\ \hline + $\bar{\mc S}.s$ & snapshot number \\ \hline + $\bar{\mc S}.T$ & set of transactions relating this snapshot to its predecessor \\ \hline + $\bar{\mc S}.U$ & snapshotted UTxO set \\ \hline + $\bar{\mc S}.\tx_{\omega}$ & optional decommit transaction \\ \hline + $\bar{\mc S}.\sigma$ & multisignature \\ \hline + \end{tabular} + \end{center} + The function $\Sno(v,n,T,U,\tx_{\omega})$ initializes a snapshot object with no multi-signature set. + \todo{add types?} \end{itemize} \subsection{Protocol flow} @@ -163,10 +162,10 @@ \subsubsection{Initializing the head} \dparagraph{$\mathtt{collectComTx}$.}\quad Upon observing the $\mtxCollect$ transaction, the parties compute $\Uinit \gets \bigcup_{j=1}^{n} C_j$ using previously observed $C_j$ and initialize $\hatmL = \Uinit$. The seen transaction set is -initialized empty $\hatmT = \emptyset$, \red{seen head state version $\hatv = 0$}, as -well as snapshot number $\hats = 0$. \red{No commit transaction is pending -$\tx_{\omega} = \bot$ and} the initial snapshot object is defined accordingly -$\bar{\mc S} \gets \Sno(0, 0, \Uinit, \emptyset, \red{\bot})$. +initialized empty $\hatmT = \emptyset$, seen head state version $\hatv = 0$, as +well as snapshot number $\hats = 0$. No commit transaction is pending +$\tx_{\omega} = \bot$ and the initial snapshot object is defined accordingly +$\bar{\mc S} \gets \blue{\Sno(0, 0, \Uinit, \emptyset, \bot)}$. \subsubsection{Processing transactions off-chain} @@ -186,40 +185,40 @@ \subsubsection{Processing transactions off-chain} receiving party $\party_{i}$ is the next snapshot leader, a message to request snapshot signatures $\hpRS$ is sent. \\ -\red{\dparagraph{$\hpRD$.}\quad Upon receiving request $(\hpRD,\tx)$, the - transaction is checked against the \emph{local} ledger state. If decommit is - not applicable yet, the protocol does $\KwWait$ to retry later and eventually - emmits an error message that another decommit is in flight. In case there is - no decommit in flight and party is the leader then $\hpRS$ is - emmitted containing the decommit transaction $\tx_{\omega}$.} \\ +\dparagraph{$\hpRD$.}\quad Upon receiving request $(\hpRD,\tx)$, the transaction is +checked against the \emph{local} ledger state. If decommit is not applicable yet +or another decommit is still pending, the protocol does $\KwWait$ to retry later or +eventually marks the decommit as invalid. In case there is no snapshot in flight +and party is the leader then a snapshot request $\hpRS$ is +sent containing the decommit transaction $\tx_{\omega}$. \\ -\red{\dparagraph{$\mathtt{decrementTx}$.}\quad Upon observing the \mtxDecrement{} - transaction, which removed outputs $U_{\omega}$ from the head, the corresponding - decommit transaction is cleared and the observed version is used for future - snapshots by - setting $\hatv = v$. This is required as that the version of the open head state is incremented on each \mtxDecrement{} transaction as described in Section~\ref{sec:decrement-tx}} \\ +\dparagraph{$\mathtt{decrementTx}$.}\quad Upon observing the \mtxDecrement{} +transaction, which removed outputs $U_{\omega}$ from the head, the corresponding +decommit transaction is cleared and the observed version $v$ is used for future +snapshots by +setting $\hatv \gets v$. Note that the version of the open head state is incremented on each \mtxDecrement{} transaction as described in Section~\ref{sec:decrement-tx} \\ \dparagraph{$\hpRS$.}\quad Upon receiving request -$(\hpRS,\red{v,}s,\mT_{\mathsf{req}}, \red{\tx_{\omega}})$\footnote{Snapshot requests +$(\hpRS,v,s,\mT_{\mathsf{req}}, \tx_{\omega})$\footnote{Snapshot requests with only transaction identifiers are possible too if all parties keep an index of previously seen transactions and their identifiers.} from party -$\party_j$, the receiver $\party_i$ checks that \red{$v$ refers to the current - open state version}\todo{wait or require?}, $s$ is the next snapshot number +$\party_j$, the receiving $\party_i$ $\Req$s that $v$ refers to the current +open state version, $s$ is the next snapshot number and that party $\party_j$ is responsible for leading its creation.\todo{define - $\hpLdr$} Party $\party_i$ has to $\KwWait$ until the previous snapshot is -confirmed ($\bar{\mc S}.s = \hats$). \red{If the decommit transaction $\tx_{\omega}$ - is not $\bot$, the transaction is $\Req$d to be applicable to the last confirmed - UTxO set $\bar{\mc S}.U$ and spent outputs must be removed, yielding the still - active UTxO set $U_{\mathsf{active}}$. Then, all requested transactions - $\mT_{\mathsf{req}}$ are $\Req$d to be applicable to $U_{\mathsf{active}}$,} + $\hpLdr$} Party $\party_i$ may has to $\KwWait$ until the previous snapshot is +confirmed ($\bar{\mc S}.s = \hats$). If the decommit transaction $\tx_{\omega}$ +is not $\bot$, the transaction is $\Req$d to be applicable to the last confirmed +UTxO set $\bar{\mc S}.U$ and decommitted transaction outputs must be removed, yielding the still +active UTxO set $U_{\mathsf{active}}$. Then, all requested transactions +$\mT_{\mathsf{req}}$ are $\Req$d to be applicable to $U_{\mathsf{active}}$, otherwise the snapshot is rejected as invalid. Only then, $\party_i$ increments their seen-snapshot counter $\hats$, resets the signature accumulator $\hatSigma$, and computes the UTxO set of the new local snapshot as -$U \gets \red{U_{\mathsf{active}}} \applytx \mT_{\mathsf{req}}$. Then, $\party_i$ +$U \gets U_{\mathsf{active}} \applytx \mT_{\mathsf{req}}$. Then, $\party_i$ creates a signature $\msSig_i$ using their signing key $\hydraSigningKey$ on a message comprised by the $\cid$, the new snapshot number $\hats$, the new $\eta$ resulting from canonically combining $U$ (see Section~\ref{sec:close-tx} for -details), \red{and $\eta_{\omega}$ derived from commit transaction $\tx_{\omega}$ outputs}. +details), and $\eta_{\omega}$ derived from decommit transaction $\tx_{\omega}$ outputs. The signature is sent to all head members via message $(\hpAS,\hats,\msSig_i)$. Finally, the local ledger state $\hatmL$ and pending transaction set $\hatmT$ get pruned by re-applying all locally pending transactions $\hatmT$ to the just @@ -232,14 +231,14 @@ \subsubsection{Processing transactions off-chain} $\hats = s$ and $\Req$ that the signature is not yet included in $\hatSigma$. They store the received signature in the signature accumulator $\hatSigma$, and if the signature from each party has been collected, $\party_i$ aggregates the -multisignature $\msCSig$ and $\Req$ it to be valid \red{(using the same message - as in $\hpRS$)}. If everything is fine, the snapshot can be considered +multisignature $\msCSig$ and $\Req$ it to be valid (constructing the signed message +as in $\hpRS$). If everything is fine, the snapshot can be considered confirmed by creating the snapshot object -$\bar{\mc S} \gets \Sno(\hatv, \hats, \hatmU, \hatmT \red{, \tx_{\omega}})$ and storing -the multi-signature $\msCSig$ in it for later reference. \red{In case there is a pending - decommit, any participant can now submit a \mtxDecrement{} transaction by - providing the just confirmed snapshot with its digests of the active UTxO set - $\eta$ and the to be removed UTxO set $\eta_{\omega}$.} Similar to the $\hpRT$, if +$\bar{\mc S} \gets \Sno(\hatv, \hats, \hatmU, \hatmT , \tx_{\omega})$ and storing +the multi-signature $\msCSig$ in it for later reference. In case there is a pending +decommit, any participant\todo{Shouldn't the decommitting party do this?} can now submit a \mtxDecrement{} transaction by +providing the just confirmed snapshot with its digests of the active UTxO set +$\eta$ and the to be removed UTxO set $\eta_{\omega}$. Similar to the $\hpRT$, if $\party_i$ is the next snapshot leader and there are already transactions to snapshot in $\hatmT$, a corresponding $\hpRS$ is distributed. @@ -297,8 +296,7 @@ \subsection{Rollbacks and protocol changes}\label{sec:rollbacks} \dparagraph{$\mathtt{rollforward}$.}\quad On every chain event that is paired or wrapped in a rollforward event $(\mathtt{rollback},p)$ with point $p$, protocol participants store their head state indexed by this point in a history -$\Omega$ of states -\todo{add version here also}$\Delta \gets (\hats, \bar{\mc S}.s, \bar{\mc S}.sigma, \hatmU, \barmU, \hatSigma, \hatmL, \hatmT)$ and $\Omega' = (p, \Delta) \cup \Omega$. \\ +$\Omega$ of states $\Delta \gets (\hatv, \hats, \hatmU, \hatSigma, \hatmL, \hatmT, \bar{\mc S})$ and $\Omega' = (p, \Delta) \cup \Omega$. \\ \dparagraph{$\mathtt{rollback}$.}\quad On a rollback $(\mathtt{rollback},p_{rb})$ to point $p_{rb}$, the corresponding head state