diff --git a/hydra-protocol/Hydra/Protocol/Figures/fig_offchain_prot.tex b/hydra-protocol/Hydra/Protocol/Figures/fig_offchain_prot.tex index 793dffd..93366fb 100644 --- a/hydra-protocol/Hydra/Protocol/Figures/fig_offchain_prot.tex +++ b/hydra-protocol/Hydra/Protocol/Figures/fig_offchain_prot.tex @@ -34,7 +34,7 @@ \On{$(\gcChainCommit, j, U)$ from chain}{ $C_j \gets U $ - \If{$\forall k \in [1..n]: C_k \neq $}{ + \If{$\forall k \in [1..n]: C_k \neq \undefinedrm$}{ $\eta \gets \combine([C_1 \dots C_n])$ \; $\PostTx{}~(\mtxCCom, \eta)$ \; } @@ -46,10 +46,11 @@ % Implictly means that all commits will defined as we cannot miss a commit (by assumption) $\Uinit \gets \bigcup_{j=1}^{n} U_j$ \; % $\Out~(\hpSnap,(0,U_0))$ \; - $\hatmU, \barmU, \hatmL \gets \Uinit$ \; - \textcolor{red}{$\tx_{\omega} \gets \bot$ \;} - $\hats,\bars \gets 0$ \; - $\mT, \hatmT, \barmT \gets \emptyset$ \; + $\hatmL \gets \Uinit$ \; + $\bar{\mc S} \gets \blue{\Sno(0, 0, \Uinit, \emptyset, \bot)}$ \; + $\hatv, \hats \gets 0$ \; + $\hatmT \gets \emptyset$ \; + $\tx_{\omega} \gets \bot$ \; } \end{walgo} @@ -65,23 +66,14 @@ \adjustbox{valign=t,scale=\sfact}{ \begin{walgo}{0.65} - %%% NEW TX - \On{$(\hpNew,\tx)$ from client}{ - \Multi{} $(\hpRT,\tx)$% - } - - \vspace{12pt} - %%% REQ TX \On{$(\hpRT,\tx)$ from $\party_j$}{ - $\mT_{\mathsf{all}} \gets \mT_{\mathsf{all}} \cup \{ (\hash(\tx),\tx )\}$ \; \Wait{$\hatmL \applytx \tx \neq \bot$}{ $\hatmL \gets \hatmL\applytx\tx$ \; $\hatmT \gets \hatmT \cup \{\tx\}$ \; % issue snapshot if we are leader - \If{$\hats = \bars \land \hpLdr(\bars + 1) = i$}{ - $\textcolor{blue}{\mT^{\#}_{req} \gets \{ \hash(\tx) ~ | ~ \forall tx \in \hatmT \}}$ \; - \Multi{} $(\hpRS,\bars+1, \textcolor{blue}{\mT^{\#}_{req}}, \textcolor{red}{\tx_{\omega}})$ \; + \If{$\hats = \bar{\mc S}.s \land \hpLdr(\bar{\mc S}.s + 1) = i$}{ + \Multi{} $(\hpRS,\hatv,\bar{\mc S}.s+1, \hatmT, \tx_{\omega})$ \; } } } @@ -89,35 +81,33 @@ \vspace{12pt} %%% REQ SN - \On{$(\hpRS,s,\mT^{\#}_{req}, \textcolor{red}{\tx_{\omega}})$ from $\party_j$}{ - \Req{$s = \hats + 1 ~ \land ~ \hpLdr(s) = j$} \; - \Wait{$\bars = \hats ~ \land ~ \forall h \in \mT^{\#}_{req} : (h, \cdot) \in \mT_{\mathsf{all}}$}{ - $\mT_{\mathsf{req}} \gets \{ \mT_{\mathsf{all}}[h] ~ | ~ \forall h \in \mT^{\#}_{req} \}$ \; - \textcolor{red}{\Req{$\barmU \applytx \tx_{\omega} \not= \bot$}} \; - \textcolor{red}{$\barmU_{\mathsf{active}} \gets \barmU \applytx \tx_{\omega}$} \; - \Req{$\textcolor{red}{\barmU_{\mathsf{active}}} \applytx \mT_{\mathsf{req}} \not= \bot$} \; - $\hatmU \gets \textcolor{red}{\barmU_{\mathsf{active}}} \applytx \mT_{\mathsf{req}}$ \; - $\hats \gets \bars + 1$ \; - \textcolor{red}{$\eta' \gets \combine(\hatmU)$} \; - % TODO: hanwavy combine/outputs here - $\textcolor{red}{\eta_{\omega} \gets \combine(\mathsf{outputs}(\tx_{\omega}))}$ \; + \On{$(\hpRS,v,s,\mT_{\mathsf{req}}, \tx_{\omega})$ from $\party_j$}{ + \Req{$v = \hatv ~ \land ~ s = \hats + 1 ~ \land ~ \hpLdr(s) = j$} \; + \Wait{$\hats = \bar{\mc S}.s$}{ + \Req{$\bar{\mc S}.U \applytx \tx_{\omega} \not= \bot$} \; + $U_{\mathsf{active}} \gets \bar{\mc S}.U \applytx \tx_{\omega} \setminus \mathsf{outputs(\tx_{\omega})}$ \; + \Req{$U_{\mathsf{active}} \applytx \mT_{\mathsf{req}} \not= \bot$} \; + $U \gets U_{\mathsf{active}} \applytx \mT_{\mathsf{req}}$ \; + $\hats \gets s$ \; + % TODO: DRY message creation + $\eta \gets \combine(U)$ \; + % TODO: handwavy combine/outputs here + $\eta_{\omega} \gets \combine(\mathsf{outputs}(\tx_{\omega}))$ \; % NOTE: WE could make included transactions auditable by adding - % a merkle tree root to the (signed) snapshot data \eta' - % TODO: sign \eta_{0} / previous state? - $\msSig_i \gets \msSign(\hydraSigningKey, (\cid || \textcolor{red}{\hats || \eta' || \eta_{\omega}}))$ \; + % a merkle tree root to the (signed) snapshot data \eta + $\msSig_i \gets \msSign(\hydraSigningKey, (\cid || v || \hats || \eta || \eta_{\omega}))$ \; $\hatSigma \gets \emptyset$ \; $\Multi{}~(\hpAS,\hats,\msSig_i)$ \; $\forall \tx \in \mT_{\mathsf{req}}: \Out~(\hpSeen,\tx)$ \; % TODO: Should we inform users if we drop a transaction? % XXX: This is a bit verbose for the spec - $\hatmL \gets \hatmU$ \; + $\hatmL \gets U$ \; $X\gets\hatmT$ \; $\hatmT\gets\emptyset$ \; \For{$\tx\in X : \hatmL\applytx \tx \not=\bot$}{ - $\hatmT\gets\hatmT\cup\{\tx\}$ + $\hatmT\gets\hatmT\cup\{\tx\}$ \; $\hatmL\gets\hatmL\applytx \tx$ \; } - $\mT_{\mathsf{all}} \gets \{ tx ~ | ~ \forall tx \in \mT_{\mathsf{all}} : tx \notin \mT_{\mathsf{req}} \}$ \; } } \end{walgo} @@ -125,37 +115,25 @@ \adjustbox{valign=t,scale=\sfact}{ \begin{walgo}{0.7} - %%% DECOMMIT - \On{$(\mathtt{decommit},\tx)$ from client}{ - \If{\textcolor{blue}{$\tx_{\omega} = \bot \land \barmU \applytx \tx \not= \bot$}}{ - \Multi{} $(\mathtt{reqDec},\tx)$% - } - } - - \vspace{12pt} - %%% REC DEC \On{$(\mathtt{reqDec},\tx)$ from $\party_j$}{ - \Wait{$\tx_\omega = \bot ~ \land ~ \barmU \applytx \tx \not= \bot$}{ - \textcolor{black}{ + \Wait{$\tx_\omega = \bot ~ \land ~ \hatmL \applytx \tx \not= \bot$}{ + $\hatmL \gets \hatmL \applytx \tx \setminus \mathsf{outputs}(\tx)$ \; $\tx_\omega \gets \tx$ \; % issue snapshot if we are leader - \If{$\hats = \bars \land \hpLdr(\bars + 1) = i$}{ - $\textcolor{blue}{\mT^{\#}_{req} \gets \{ \hash(\tx) ~ | ~ \forall tx \in \hatmT \}}$ \; - \Multi{} $(\hpRS,\bars+1,\mT^{\#}_{req}, \textcolor{blue}{\tx})$ \; + \If{$\hats = \bar{\mc S}.s \land \hpLdr(\bar{\mc S}.s + 1) = i$}{ + \Multi{} $(\hpRS,\hatv,\bar{\mc S}.s+1,\hatmT, \tx_{\omega})$ \; } - } } } \vspace{12pt} %%% DECREMENT - \On{$(\mathtt{decrementTx}, U_{\omega})$ from chain}{ - \textcolor{red}{ + \On{$(\mathtt{decrementTx}, U_{\omega}, v)$ from chain}{ \If{$\mathsf{outputs}(\tx_{\omega}) = U_{\omega}$}{ $\tx_{\omega} \gets \bot$ \; - } + $\hatv \gets v$ \; } } @@ -166,30 +144,33 @@ \Req{} $s \in \{\hats,\hats+1\}$ \; \Wait{$\hats=s$}{ \Req{} $(j, \cdot) \notin \hatSigma$ \; - % FIXME: missing a write to \hatSigma + $\hatSigma[j] \gets \sigma_{j}$ \; \If{$\forall k \in [1..n]: (k,\cdot) \in \hatSigma$}{ % TODO: MS-ASig used different than in the preliminaries $\msCSig \gets \msComb(\hydraKeys^{setup}, \hatSigma)$ \; - $\eta' \gets \combine(\hatmU)$ \; - % TODO: tx_ω undefined (else) case - $\textcolor{red}{\eta_{\omega} \gets \combine(\mathsf{outputs}(\tx_{\omega}))}$ \; + % TODO: DRY message creation + $\eta \gets \combine(\hatmU)$ \; + $\eta_{\omega} \gets \combine(\mathsf{outputs}(\tx_{\omega}))$ \; - % TODO: sign \eta_{0} / previous state? - \Req{} $\msVfy(\hydraKeysAgg, (\cid || \hats || \eta' || \textcolor{red}{\eta_{\omega}}), \msCSig)$ \; - $\barmU \gets \hatmU$ \; - $\bars \gets \hats$ \; - $\barsigma \gets \msCSig$ \; + % NOTE: Implementation differs here and + % below as it stores seen version in seen + % snapshot and uses that to verify + \Req{} $\msVfy(\hydraKeysAgg, (\cid || \blue{\hatv ||} \hats || \eta || \eta_{\omega}), \msCSig)$ \; + % create confirmed snapshot for later reference + \blue{$\bar{\mc S} \gets \Sno(\hatv, \hats, \hatmU, \hatmT , \tx_{\omega})$ \;} + $\bar{\mc S}.\sigma \gets \msCSig$ \; - $\textcolor{red}{\PostTx{}~(\mathtt{decrementTx}, \hats, \eta', \eta_{\omega})}$ \; - %$\Out~(\hpSnap,(\bars,\barmU))$ \; + %$\Out~(\hpSnap,(\bar{\mc S}.s,\bar{\mc S}.U))$ \; $\forall \tx \in \mT_{\mathsf{req}} : \Out (\hpConf,\tx)$ \; - + \If{${\bar S}.\tx_{\omega} \ne \bot$}{ + $\PostTx{}~(\mtxDecrement, \hatv, \hats, \eta, \eta_{\omega})$ \; + % NOTE: Needed for security? + \blue{$\Out (\hpConf,\tx_{\omega})$ \;} + } % issue snapshot if we are leader \If{$\hpLdr(s+1) = i \land \hatmT \neq \emptyset$}{ - % TODO: wasteful as we re-request U_ω? - $\textcolor{blue}{\mT^{\#}_{req} \gets \{ \hash(\tx) ~ | ~ \forall tx \in \hatmT \}}$ \; - \Multi{} $(\hpRS,s+1, \textcolor{blue}{\mT^{\#}_{req}}, \textcolor{red}{\tx_{\omega}})$ \; + \Multi{} $(\hpRS,\hatv,\bar{\mc S}.s+1, \hatmT, \tx_{\omega})$ \; } } } @@ -208,9 +189,11 @@ \begin{walgo}{0.6} % CLOSE from client \On{$(\hpClose)$ from client}{ - $\eta' \gets \combine(\barmU)$ \; - $\xi \gets \barsigma$ \; - $\PostTx{}~(\mtxClose, \bars, \eta', \xi)$ \; + $\eta \gets \combine(\bar{\mc S}.U)$ \; + $\eta_\omega \gets \combine(\mathsf{outputs}(\bar{\mc S}.\tx_\omega))$ \; + $\xi \gets \bar{\mc S}.\sigma$ \; + % XXX: \hatv needed to distinguish between CloseType redeemer, explain how exactly? + $\PostTx{}~(\mtxClose, \hatv, \bar{\mc S}.v, \bar{\mc S}.s, \eta, \eta_{\omega}, \xi)$ \; } \end{walgo} } @@ -218,10 +201,12 @@ \adjustbox{valign=t,scale=\sfact}{ \begin{walgo}{0.6} \On{$(\gcChainClose, \eta) \lor (\gcChainContest, s_{c}, \eta)$ from chain}{ - \If{$\bars > s_{c}$}{ - $\eta' \gets \combine(\barmU)$ \; - $\xi \gets \barsigma$ \; - $\PostTx{}~(\mtxContest, \bars, \eta', \xi)$ \; + \If{$\bar{\mc S}.s > s_{c}$}{ + $\eta \gets \combine(\bar{\mc S}.U)$ \; + $\eta_\omega \gets \combine(\mathsf{outputs}(\bar{\mc S}.\tx_\omega))$ \; + $\xi \gets \bar{\mc S}.\sigma$ \; + % XXX: \hatv needed to distinguish between CloseType redeemer, explain how exactly? + $\PostTx{}~(\mtxContest, \hatv, \bar{\mc S}.v, \bar{\mc S}.s, \eta, \eta_{\omega}, \xi)$ \; } } \end{walgo} diff --git a/hydra-protocol/Hydra/Protocol/Macros.tex b/hydra-protocol/Hydra/Protocol/Macros.tex index d653ce4..9ddd159 100644 --- a/hydra-protocol/Hydra/Protocol/Macros.tex +++ b/hydra-protocol/Hydra/Protocol/Macros.tex @@ -16,10 +16,15 @@ % - Algorithms % - Merkle-Patricia Trees +\newcommand{\undefinedrm}{\mathrm{undef}} + \makeatletter \newcommand{\removelatexerror}{\let\@latex@error\@gobble} \makeatother +\newcommand{\red}[1]{\textcolor{red}{#1}} +\newcommand{\blue}[1]{\textcolor{blue}{#1}} + \newtheorem{theorem}{Theorem} % \numberwithin{theorem}{chapter} \newtheorem{lemma}[theorem]{Lemma} @@ -36,6 +41,8 @@ \newtheorem{construction}{Construction} % === General === +\newcommand{\mc}{\mathcal} + \newcommand{\ith}[1]{#1^{\text{th}}} \newcommand{\nop}{n} @@ -256,6 +263,7 @@ \newcommand{\hpClose}{\mathtt{close}} \newcommand{\hpCont}{\mathtt{cont}} \newcommand{\hpFO}{\mathtt{fanOut}} +\newcommand{\hpRD}{\mathtt{reqDec}} % == Variables == @@ -293,6 +301,8 @@ \newcommand{\cardanoKeysinit}{\initial{\underline{k}}_\pu} +\newcommand{\hatv}{\hat v} +\newcommand{\barv}{\bar v} \newcommand{\hats}{\hat s} \newcommand{\bars}{\bar s} \newcommand{\barsigma}{\bar{\sigma}} @@ -304,7 +314,6 @@ \newcommand{\barmL}{\bar {\mathcal L}} \newcommand{\mT}{{\mathcal T}} \newcommand{\hatmT}{\hat {\mathcal T}} -\newcommand{\barmT}{\bar {\mathcal T}} \newcommand{\hatmDT}{\Delta\hat {\mathcal T}} \newcommand{\hatmR}{\hat {\mathcal R}} \newcommand{\mH}{{\mathcal H}} @@ -317,7 +326,6 @@ \newcommand{\txo}{\mathsf{tx}} - % == Commands == \newcommand{\hpRG}{\mathtt{req}} diff --git a/hydra-protocol/Hydra/Protocol/OffChain.tex b/hydra-protocol/Hydra/Protocol/OffChain.tex index c65c388..dd75640 100644 --- a/hydra-protocol/Hydra/Protocol/OffChain.tex +++ b/hydra-protocol/Hydra/Protocol/OffChain.tex @@ -12,24 +12,31 @@ \section{Off-Chain Protocol}\label{sec:offchain} \begin{enumerate} \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 + 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 + \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 + \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 - \item \texttt{reqInc} \todo{explain} - \item \texttt{reqDec} \todo{explain} \end{itemize} \item Commands issued by the participants themselves or on behalf of end-users and clients \begin{itemize} \item $\hpInit$: to start initialization of a head - \item \texttt{commit} to request an incremental commit - \item \texttt{decommit} to request an incremental decommit - \item $\hpNew$: to submit a new transaction to an open head \item $\hpClose$: to request closure of an open head \end{itemize} \end{enumerate} + % TODO: define states and e.g. that newTx not possible when closed? state diagram? The behavior is fully specified in Figure~\ref{fig:off-chain-prot}, while the @@ -98,26 +105,34 @@ \subsection{Notation} \subsection{Variables} Besides parameters agreed in the protocol setup (see Section~\ref{sec:setup}), a -party's local state consists of the following variables: \todo{update} +party's local state consists of the following variables: \begin{itemize} + \item $\hatv$: Last seen open state version. \item $\hats$: Sequence number of latest seen snapshot. - \item $\bars$: Sequence number of latest confirmed snapshot. - \item $\barsigma$: Signature associated with the latest confirmed snapshot. - \item $\hatmU$: UTxO set of the latest seen snapshot. - \item $\barmU$: UTxO set associated with the latest confirmed snapshot. \item $\hatSigma \in {(\tyNatural \times \tyBytes)}^{*}$: Accumulator of signatures of the latest seen snapshot, indexed by parties. \item $\hatmL$: UTxO set representing the local ledger state resulting from - applying $\hatmT$ to $\barmU$ to validate requested transactions. + 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 $\mT_{\mathsf{all}} \in (\tyBytes \times \mT)^{*}$: Associative list of all - seen transactions not yet included in a snapshot. + \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} -\todo{Make consistent with figure again} \subsubsection{Initializing the head} @@ -145,12 +160,12 @@ \subsubsection{Initializing the head} transaction and the protocol would end at this point.\\ \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 $\hatmU = \barmU = \hatmL = \Uinit$ -with it. The initial transaction sets are empty -$\mT = \barmT =\hatmT =\emptyset$, and $\bars = \hats = 0$. -% REVIEW: check $\eta$ against $\Uinit$? -\todo{add increment/decrement} +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$, 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} @@ -162,42 +177,53 @@ \subsubsection{Processing transactions off-chain} was configurable, the Coordinated Head protocol does specify a snapshot to be created after each transaction.\\ -\dparagraph{$\hpNew$.}\quad At any time, by sending request $(\hpNew,\tx)$, a -client of the protocol can submit a new transaction $\tx$ to the head, which -results in it being sent out to all parties as a $(\hpRT,\tx)$ message.\\ - -\dparagraph{$\hpRT$.}\quad Upon receiving request $(\hpRT,\tx)$, the transaction -gets recorded in $\mT_{\mathsf{all}}$ and applied to the \emph{local} ledger -state $\hatmL \applytx \tx$. If not applicable yet, the protocol does $\KwWait$ -to retry later or eventually marks this transaction as invalid (see assumption -about events piling up). After applying and if there is no current snapshot ``in -flight'' ($\hats = \bars$) and the receiving party $\party_{i}$ is the next -snapshot +\dparagraph{$\hpRT$.}\quad Upon receiving request $(\hpRT,\tx)$, the transaction is +applied to the \emph{local} ledger state $\hatmL \applytx \tx$. If not +applicable yet, the protocol does $\KwWait$ to retry later or eventually marks +this transaction as invalid (see assumption about events piling up). After +applying and if there is no current snapshot in flight ($\hats = \bar{\mc S}.s$) and the +receiving party $\party_{i}$ is the next snapshot leader, a message to request snapshot signatures $\hpRS$ is sent. \\ +\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}$. \\ + +\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,s,\mT_{\mathsf{req}}^{\#})$ from party $\party_j$, the receiver -$\party_i$ checks that $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 ($\bars = \hats$) and -all requested transaction hashes $\mT_{\mathsf{req}}^{\#}$ can be resolved in -$\mT_{\mathsf{all}}$. Then, all those resolved transactions $\mT_{\mathsf{req}}$ -are $\Req$d to be applicable to $\barmU$, 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 -$\hatmU$ of the new (seen) snapshot as -$\hatmU \gets \barmU \applytx \mT_{\mathsf{req}}$. Then, $\party_i$ creates a -signature $\msSig_i$ using their signing key $\hydraSigningKey$ on a message -comprised by the $\cid$, \textcolor{red}{the $\eta_{0}$ corresponding to the - initial UTxO set $\Uinit$}, and the new $\eta'$ given by the new snapshot number -$\hats$ and canonically combining $\hatmU$ (see Section~\ref{sec:close-tx} for -details). The signature is sent to all head members via message -$(\hpAS,\hats,\msSig_i)$. Finally, the pending transaction set $\hatmT$ gets -pruned by re-applying all locally pending transactions $\hatmT$ to the just -requested snapshot's UTxO set $\hatmU$ iteratively and ultimately yielding a -``pruned'' version of $\hatmT$ and $\hatmU$. Also, the set of all transactions -$\mT_{\mathsf{all}}$ can be reduced by the requested -transactions $\mT_{\mathsf{req}}$.\\ +$(\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 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$ 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 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), 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 +requested snapshot's UTxO set iteratively and +ultimately yielding a ``pruned'' version of $\hatmT$ and $\hatmL$. \\ \dparagraph{$\hpAS$.}\quad Upon receiving acknowledgment $(\hpAS,s,\msSig_j)$, all participants $\Req$ that it is from an expected snapshot (either the last seen @@ -205,23 +231,24 @@ \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. If everything is fine, the -snapshot can be considered confirmed by updating $\bars=s$ and participants also -store the UTxO set in $\barmU$, as well as the signature in $\barsigma$ for -later reference. 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. +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 , \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. \subsubsection{Closing the head} \dparagraph{$\hpClose$.}\quad In order to close a head, a client issues the -$\hpClose$ input which uses the latest confirmed snapshot $\barmU$ to create -\begin{itemize} - \item the new $\eta$-state $\eta'$ from the last confirmed UTxO set and snapshot - number, and - \item the certifiate $\xi$ using the corresponding multi-signature. -\end{itemize} -With $\eta'$ and $\xi$, the $\mtxClose$ transaction can be constructed and +$\hpClose$ input which uses the latest confirmed snapshot $\bar{\mc S}$ to +create the new $\eta$-state from the last confirmed UTxO set, the digest of +to-decommit UTxO set $\eta_{\omega}$, and the certifiate $\xi$ using the corresponding +multi-signature. With these, the $\mtxClose$ transaction can be constructed and posted. See Section~\ref{sec:close-tx} for details about this transaction. \\ \dparagraph{$\mathtt{closeTx}/\mathtt{contestTx}$.}\quad When a party observes @@ -234,9 +261,6 @@ \subsubsection{Closing the head} Section~\ref{sec:contest-tx}). \subsection{Rollbacks and protocol changes}\label{sec:rollbacks} -% FIXME: Need to address this fully -\todo{Discuss protocol updates as well, also in light of rollbacks} - The overall life-cycle of the Head protocol is driven by on-chain inputs (see introduction of Section~\ref{sec:offchain}) which stem from observing transactions on the mainchain. Most blockchains, however, do only provide @@ -272,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 -$\Delta \gets (\hats, \bars, \barsigma, \hatmU, \barmU, \hatSigma, \hatmL, \mT_{all}, \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 @@ -291,7 +314,11 @@ \subsection{Rollbacks and protocol changes}\label{sec:rollbacks} different UTxO and open the Head with a different initial UTxO set, while the already signed snapshots would still be (cryptographically) valid. To mitigate this, all signatures on snapshots need to incorporate the initial UTxO set by -including $\eta_{0}$.\todo{Write about contestation deadline vs. rollbacks} +including $\eta_{0}$. \todo{version-counting is less powerfull} +% FIXME: \eta_0 not compatible with versioning scheme +\todo{Expand to rollbacks in presence of decrements} + +\todo{Write about contestation deadline vs. rollbacks} \input{Hydra/Protocol/Figures/fig_offchain_prot} diff --git a/hydra-protocol/Hydra/Protocol/OnChain.tex b/hydra-protocol/Hydra/Protocol/OnChain.tex index 18d2371..df895b5 100644 --- a/hydra-protocol/Hydra/Protocol/OnChain.tex +++ b/hydra-protocol/Hydra/Protocol/OnChain.tex @@ -1,5 +1,7 @@ \clearpage \section{On-chain Protocol}\label{sec:on-chain} +% FIXME: update all figures: removed n and decrement changes +\todo{Update figures} \todo{Open problem: ensure abort is always possible. e.g. by individual aborts or undoing commits} \todo{Open problem: ensure fanout is always possible, e.g. by limiting complexity of $U_0$} @@ -9,7 +11,7 @@ \section{On-chain Protocol}\label{sec:on-chain} machine (see Figure~\ref{fig:SM_states_basic}). Each transition in this state machine is represented and caused by a corresponding Hydra protocol transaction on-chain: $\mtxInit{}$, $\mtxCom{}$, $\mtxAbort{}$, $\mtxCollect{}$, -$\mtxClose{}$, $\mtxContest{}$, and $\mtxFanout{}$. +$\mtxDecrement{}$, $\mtxClose{}$, $\mtxContest{}$, and $\mtxFanout{}$. % TODO: Could include a combined overview, slightly more detailed than Figure 1 % of the transaction trace for the full life cycle maybe? @@ -25,8 +27,8 @@ \section{On-chain Protocol}\label{sec:on-chain} \item $\nuCommit$ controls the collection of committed UTxOs into the head in $\mtxCollect$ or that funds are reimbursed in an $\mtxAbort{}$. \item $\nuHead$ represents the main protocol state machine logic and ensures - contract continuity throughout $\mtxCollect{}$, $\mtxClose{}$, - $\mtxContest{}$ and $\mtxFanout{}$. + contract continuity throughout $\mtxCollect{}$, $\mtxDecrement{}$, + $\mtxClose{}$, $\mtxContest{}$ and $\mtxFanout{}$. \end{itemize} \subsection{Init transaction}\label{sec:init-tx} @@ -42,7 +44,7 @@ \subsection{Init transaction}\label{sec:init-tx} \begin{figure} \centering - \includegraphics[width=0.8\textwidth]{Hydra/Protocol/Figures/initTx.pdf} + \includegraphics[width=0.8\textwidth]{Hydra/Protocol/Figures/initTx.pdf} \caption{\mtxInit{} transaction spending a seed UTxO, and producing the head output in state $\stInitial$ and initial outputs for each participant.}\label{fig:initTx} \end{figure} @@ -55,7 +57,7 @@ \subsection{Init transaction}\label{sec:init-tx} \texttt{HydraHeadV1}, i.e. $\st = \{\cid \mapsto \texttt{HydraHeadV1} \mapsto 1\}$. \item One \emph{Participation Token (PT)} per participant - $i \in \{1 \dots \nop \}$ to be used for authenticating further + $i \in \{1 \dots |\hydraKeys| \}$ to be used for authenticating further transactions and to ensure every participant can commit and cannot be censored. The token name is the participant's verification key hash $\keyHash_{i} = \hash(\msVK_{i})$ of the verification key as received @@ -66,23 +68,22 @@ \subsection{Init transaction}\label{sec:init-tx} \noindent Consequently, the \mtxInit{} transaction \begin{itemize} \item has at least input $\seed$, - \item mints the state thread token $\st$, and one $\pt$ for each of the $\nop$ + \item mints the state thread token $\st$, and one $\pt$ for each of the $|\hydraKeys|$ participants with policy $\cid$, - \item has $\nop$ initial outputs $o_{\mathsf{initial}_{i}}$ with datum $\datumInitial{} = \cid$, + \item has $|\hydraKeys|$ initial outputs $o_{\mathsf{initial}_{i}}$ with datum $\datumInitial{} = \cid$, \item has one head output $o_{\mathsf{head}}$, which captures the initial state of the protocol in the datum \[ - \datumHead = (\stInitial,\cid',\seed',\hydraKeysAgg,\nop,\cPer) + \datumHead = (\stInitial,\cid',\seed',\hydraKeys,\cPer) \] where \begin{mitemize} \item $\stInitial$ is a state identifier, \item $\cid'$ is the unique currency id of this instance, \item $\seed'$ is the output reference parameter of $\muHead$, - \item $\hydraKeysAgg$ is the aggregated off-chain multi-signature key established during the - setup phase, - \item $\nop$ is the number of head participants, and + \item $\hydraKeys$ are the off-chain multi-signature keys from the setup + phase, \item $\cPer$ is the contestation period. \end{mitemize} \end{itemize} @@ -97,14 +98,14 @@ \subsection{Init transaction}\label{sec:init-tx} \item The seed output is spent in this transaction. This guarantees uniqueness of the policy $\cid$ because the EUTxO ledger ensures that $\seed$ cannot be spent twice in the same chain. $(\seed, \cdot) \in \txInputs$ \item All entries of $\txMint$ are of this policy and of single quantity $\forall \{c \mapsto \cdot \mapsto q\} \in \txMint : c = \cid \land q = 1$ - \item Right number of tokens are minted $|\txMint| = \nop + 1$ + \item Right number of tokens are minted $|\txMint| = |\hydraKeys| + 1$ % TODO: |\txMint| may not be clear to the reader, maybe combine with item above, but be more explicit. \item State token is sent to the head validator $\st \in \valHead$ % TODO: fact that it is goverend by nuHead is a bit implicit here. - \item \textcolor{blue}{The correct number of initial outputs are present $|(\cdot, \nuInitial, \cdot) \in \txOutputs| = n$} - % TODO: this is implied by the ledger, so can be removed - \item All participation tokens are sent to the initial validator as an initial output $\forall i \in [1 \dots n] : \{\cid \mapsto \cdot \mapsto 1\} \in \valInitial{i}$ + \item \textcolor{blue}{The correct number of initial outputs are present $|(\cdot, \nuInitial, \cdot) \in \txOutputs| = |\hydraKeys|$} + % XXX: this is implied by the ledger, so can be removed + \item All participation tokens are sent to the initial validator as an initial output $\forall i \in [1 \dots |\hydraKeys|] : \{\cid \mapsto \cdot \mapsto 1\} \in \valInitial{i}$ \item The $\datum_{\mathsf{head}}$ contains own currency id $\cid = \cid'$ and the right seed reference $\seed = \seed'$ - \item All initial outputs have a $\cid$ as their datum: $\forall i \in [1 \dots n] : \cid = \datumInitial{i}$ + \item All initial outputs have a $\cid$ as their datum: $\forall i \in [1 \dots |\hydraKeys|] : \cid = \datumInitial{i}$ \end{menumerate} \item When evaluated with the $\mathsf{burn}$ redeemer, \begin{menumerate} @@ -127,7 +128,7 @@ \subsection{Init transaction}\label{sec:init-tx} \subsection{Commit Transaction}\label{sec:commit-tx} A \mtxCom{} transaction may be submitted by each participant -$\forall i \in \{1 \dots \nop\}$ to commit some UTxO into the head or +$\forall i \in \{1 \dots |\hydraKeys|\}$ to commit some UTxO into the head or acknowledge to not commit anything. The transaction is depicted in Figure~\ref{fig:commitTx} and has the following structure: \begin{itemize} @@ -165,7 +166,7 @@ \subsection{Commit Transaction}\label{sec:commit-tx} \begin{figure} \centering - \includegraphics[width=0.8\textwidth]{Hydra/Protocol/Figures/commitTx.pdf} + \includegraphics[width=0.8\textwidth]{Hydra/Protocol/Figures/commitTx.pdf} \caption{\mtxCom{} transaction spending an initial output and a single committed output, and producing a commit output.}\label{fig:commitTx} \end{figure} @@ -177,7 +178,7 @@ \subsection{Abort Transaction}\label{sec:abort-tx} party to abort the creation of a head and consists of \begin{itemize} \item one input spending from $\nuHead$ holding the $\st$ with $\datumHead$, - \item $\forall i \in \{1 \dots \nop\}$ inputs either + \item $\forall i \in \{1 \dots |\hydraKeys|\}$ inputs either \begin{itemize} \item spending from $\nuInitial$ with with $\pt_{i} \in \valInitial{i}$ and $\datumInitial{i} = \cid$, or \item spending from $\nuCommit$ with with $\pt_{i} \in \valCommit{i}$ and $\datumCommit{i} = (\cid, C_{i})$, @@ -210,9 +211,9 @@ \subsection{Abort Transaction}\label{sec:abort-tx} reimburse, and checks: \begin{menumerate} \item State is advanced from $\datumHead \sim \stInitial$ to terminal state - $\stFinal$: % XXX: What does this actually mean? + $\stFinal$: \[ - (\stInitial,\cid,\seed,\hydraKeysAgg,\nop,\cPer) \xrightarrow[m]{\stAbort} \stFinal. + (\stInitial,\cid,\seed,\hydraKeys,\cPer) \xrightarrow[m]{\stAbort} \stFinal. \] \item All UTxOs committed into the head are reimbursed exactly as they were committed. This is done by comparing hashes of serialised representations of @@ -221,17 +222,17 @@ \subsection{Abort Transaction}\label{sec:abort-tx} transaction, e.g for returning change.} with the canonically combined committed UTxOs in $C_{i}$: \[ - \hash(\bigoplus_{j=1}^{m} \bytes(o_{j})) = \combine([C_{i} ~ | ~ \forall [1\dots\nop], C_{i} \neq \bot]) + \hash(\bigoplus_{j=1}^{m} \bytes(o_{j})) = \combine([C_{i} ~ | ~ \forall [1 \dots |\hydraKeys|], C_{i} \neq \bot]) \] \item Transaction is signed by a participant $\exists \{\cid \mapsto \keyHash_{i} \mapsto -1\} \in \txMint \Rightarrow \keyHash_{i} \in \txKeys$. \item All tokens are burnt - $|\{\cid \mapsto \cdot \mapsto -1\} \in \txMint| = \nop + 1$. + $|\{\cid \mapsto \cdot \mapsto -1\} \in \txMint| = |\hydraKeys| + 1$. \end{menumerate} \begin{figure} \centering - \includegraphics[width=0.8\textwidth]{Hydra/Protocol/Figures/abortTx.pdf} + \includegraphics[width=0.8\textwidth]{Hydra/Protocol/Figures/abortTx.pdf} \caption{\mtxAbort{} transaction spending the $\stInitial$ state head output and collecting all initial and commit outputs, which get reimbursed by outputs $o_{1} \dots o_{m}$. Note that each $\pt$ may be in either, an @@ -244,7 +245,7 @@ \subsection{CollectCom Transaction}\label{sec:collect-tx} all the committed UTxOs to the same head. It has \begin{itemize} \item one input spending from $\nuHead$ holding the $\st$ with $\datumHead$, - \item $\forall i \in \{1 \dots \nop\}$ inputs spending commit outputs + \item $\forall i \in \{1 \dots |\hydraKeys|\}$ inputs spending commit outputs $(\valCommit{i}, \nuCommit, \datumCommit{i})$ with $\pt_{i} \in \valCommit{i}$ and $\datumCommit{i} = (\cid, C_{i})$, and \item one output paying to $\nuHead$ with value $\valHead'$ and @@ -255,21 +256,20 @@ \subsection{CollectCom Transaction}\label{sec:collect-tx} $\redeemerHead = \mathsf{collect}$ and checks: \begin{menumerate} \item State is advanced from $\datumHead \sim \stInitial$ to - $\datumHead' \sim \stOpen$, parameters $\cid,\hydraKeysAgg,\nop,\cPer$ stay + $\datumHead' \sim \stOpen$, parameters $\cid,\hydraKeys,\cPer$ stay unchanged and the new state is governed again by $\nuHead$ \[ - (\stInitial,\cid,\seed,\hydraKeysAgg,\nop,\cPer) \xrightarrow{\stCollect} (\stOpen,\cid,\hydraKeysAgg,\nop,\cPer,\eta,\textcolor{blue}{0},\eta) + (\stInitial,\cid,\seed,\hydraKeys,\cPer) \xrightarrow{\stCollect} (\stOpen,\cid,\hydraKeys,\cPer,v,\eta) \] + where snapshot version is initialized as $v = 0$. \item Commits are collected in $\eta$ \[ - \eta = U^{\#} = \combine([C_{1}, \dots, C_{\nop}]) + \eta = U^{\#} = \combine([C_{1}, \dots, C_{n}]) \] - where + where $n = |\hydraKeys|$ and \[ \combine(\underline{C}) = \hash(\mathsf{concat}({\sortOn(1, \mathsf{concat}(\underline{C}))}^{\downarrow2})) \] - % TODO: mention in off-chain that it is limited what we can fan out, so size - % & complexity of U needs to be contained, especially off-chain. That is, given a list of committed UTxO $\underline{C}$, where each element is a list of output references and the serialised representation of what was committed, $\combine$ first concatenates all commits together, sorts this list @@ -287,7 +287,7 @@ \subsection{CollectCom Transaction}\label{sec:collect-tx} number of tokens.} % NOTE: Implemented slightly different as we would only count PTs and = n \[ - |\{\cid \rightarrow . \rightarrow 1\} \in \valHead'| = \nop + 1 + |\{\cid \rightarrow . \rightarrow 1\} \in \valHead'| = |\hydraKeys| + 1 \] \item Transaction is signed by a participant \[ @@ -309,64 +309,13 @@ \subsection{CollectCom Transaction}\label{sec:collect-tx} \begin{figure} \centering - \includegraphics[width=0.8\textwidth]{Hydra/Protocol/Figures/collectComTx.pdf} + \includegraphics[width=0.8\textwidth]{Hydra/Protocol/Figures/collectComTx.pdf} \caption{\mtxCCom{} transaction spending the head output in $\stInitial$ state and collecting from multiple commit outputs into a single $\stOpen$ head output.}\label{fig:collectComTx} \end{figure} -\subsection{Increment Transaction}\label{sec:increment-tx} - -\noindent The \mtxIncrement{} transaction (Figure~\ref{fig:incrementTx}) allows -a party to add a UTxO to an already open head and consists of: - -\begin{itemize} - \item one input spending from $\nuHead$ holding the $\st$ with $\datumHead$, - \item one or more inputs with reference $\txOutRef_{\mathsf{committed}_{j}}$ - spending output $o_{\mathsf{committed}_{j}}$ with - $\val_{\mathsf{committed}_{j}}$, - \item one output paying to $\nuHead$ with value $\valHead'$ and - datum $\datumHead'$. -\end{itemize} - -\noindent The state-machine validator $\nuHead$ is spent with -$\redeemerHead = (\mathsf{increment}, \xi)$, where $\xi$ is a multi-signature of -the increment snapshot which authorizes addition of some UTxO $U_\alpha$, and checks: -\begin{menumerate} - \item State is advanced from $\datumHead \sim \stOpen$ to - $\datumHead' \sim \stOpen$, parameters $\cid,\hydraKeysAgg,\nop,\cPer$ - stay unchanged and the new state is governed again by $\nuHead$ - \todo{explain $\stOpen$ tuple} - \todo{need to check all fields!} - \[ - (\stOpen,\cid,\hydraKeysAgg,\nop,\cPer,\eta_{\mathsf{pre}},s,\eta) \xrightarrow[\xi]{\mathsf{increment}} (\stOpen,\cid,\hydraKeysAgg,\nop,\cPer,\eta,s',\eta') - \] - \item Increment snapshot number $s'$ is higher than the currently stored snapshot number $s$ - \[ - s' > s - \] - \item $\xi$ is a valid multi-signature of the currency id $\cid$, the current snapshot state $\eta$, the new snapshot number $s'$ and state $\eta'$ - \[ - \msVfy(\hydraKeysAgg,(\cid || \eta || s' || \eta' || \eta_{\alpha}),\xi) = \true - \] - where $\eta_{\alpha}$ is the digest of all added UTxO - \[ - \eta_{\alpha} = U^{\#}_{\alpha} = \hash(\bigoplus_{j=1}^{m} \bytes(o_{\mathsf{committed}_{j}})) - \] - \item Transaction is signed by a participant - \[ - \exists \{\cid \mapsto \keyHash_{i} \mapsto 1\} \in \valHead' \Rightarrow \keyHash_{i} \in \txKeys - \] -\end{menumerate} - -\begin{figure} - \centering - \includegraphics[width=0.8\textwidth]{Hydra/Protocol/Figures/incrementTx.pdf} - \caption{\mtxIncrement{} transaction spending an open head output and a single - committed output, and producing a new head output.}\label{fig:incrementTx} -\end{figure} - -\subsection{Decrement Transaction}\label{sec:increment-tx} +\subsection{Decrement Transaction}\label{sec:decrement-tx} \noindent The \mtxDecrement{} transaction (Figure~\ref{fig:DecrementTx}) allows a party to remove a UTxO from an already open head and consists of: @@ -375,46 +324,48 @@ \subsection{Decrement Transaction}\label{sec:increment-tx} \item one input spending from $\nuHead$ holding the $\st$ with $\datumHead$, \item one output paying to $\nuHead$ with value $\valHead'$ and datum $\datumHead'$, - \item one or more decommit outputs $o_{1} \dots o_{m}$. + \item one or more decommit outputs $o_{2} \dots o_{m+1}$. \end{itemize} \noindent The state-machine validator $\nuHead$ is spent with -$\redeemerHead = (\mathsf{decrement}, \xi, m)$, where $\xi$ is a multi-signature of -the decrement snapshot which authorizes removal of some UTxO $U_\omega$, and $m$ is -the number of outputs to reimburse. The validator checks: +$\redeemerHead = (\mathsf{decrement}, \xi, s, m)$, where $\xi$ is a multi-signature of +the decrement snapshot which authorizes removal of some UTxO, $s$ is the +used snapshot number and $m$ is the number of outputs to distribute. The +validator checks: \begin{menumerate} \item State is advanced from $\datumHead \sim \stOpen$ to - $\datumHead' \sim \stOpen$, parameters $\cid,\hydraKeysAgg,\nop,\cPer$ stay + $\datumHead' \sim \stOpen$, parameters $\cid,\hydraKeys,\cPer$ stay unchanged and the new state is governed again by $\nuHead$ - \todo{need to check all fields!} \[ - (\stOpen,\cid,\hydraKeysAgg,\nop,\cPer,\eta_{\mathsf{pre}},s,\eta) \xrightarrow[\xi]{\mathsf{decrement}} (\stOpen,\cid,\hydraKeysAgg,\nop,\cPer,\eta,s',\eta') + (\stOpen,\cid,\hydraKeys,\cPer,v,\eta) \xrightarrow[\xi, s, m]{\mathsf{decrement}} (\stOpen,\cid,\hydraKeys,\cPer,v',\eta') \] - \item Decrement snapshot number $s'$ is higher than the currently stored snapshot number $s$ + \item New version $v'$ is incremented correctly \[ - s' > s + v' = v + 1 \] - \item $\xi$ is a valid multi-signature of the currency id $\cid$, the current snapshot state $\eta$, the new snapshot number $s'$ and state $\eta'$ + \item $\xi$ is a valid multi-signature of the currency id $\cid$, the current state version $v$, and the new state $\eta'$ \[ - \msVfy(\hydraKeysAgg,(\cid || \eta || s' || \eta' || \eta_{\omega}),\xi) = \true + \msVfy(\hydraKeys,(\cid || v || s || \eta' || \eta_{\omega}),\xi) = \true \] - where $\eta_{\omega}$ is the digest of all removed UTxO + where snapshot number $s$ is provided through the redeemer and $\eta_{\omega}$ must be the digest of all removed UTxO \[ - \eta_{\omega} = U^{\#}_{\omega} = \hash(\bigoplus_{j=1}^{m} \bytes(o_{j})) + \eta_{\omega} = U^{\#}_{\omega} = \hash(\bigoplus_{j=2}^{m+1} \bytes(o_{j})) \] - \item Transaction is signed by a participant + \item The value in the head output is decreased accordingly + \todo{Redundant to above? Only check $\valHead' < \valHead$?} \[ - \exists \{\cid \mapsto \keyHash_{i} \mapsto 1\} \in \valHead' \Rightarrow \keyHash_{i} \in \txKeys + \valHead' \cup (\bigcup_{j=2}^{m+1} \val_{o_{j}}) = \valHead \] - \item The value in the head output is decreased accordingly \todo{really needed?} + \item Transaction is signed by a participant + \todo{Allow anyone to do decrements?} \[ - \valHead' \cup (\bigcup_{j=1}^{m} \val_{o_{j}}) = \valHead + \exists \{\cid \mapsto \keyHash_{i} \mapsto 1\} \in \valHead' \Rightarrow \keyHash_{i} \in \txKeys \] \end{menumerate} \begin{figure} \centering - \includegraphics[width=0.8\textwidth]{Hydra/Protocol/Figures/decrementTx.pdf} + \includegraphics[width=0.8\textwidth]{Hydra/Protocol/Figures/decrementTx.pdf} \caption{\mtxDecrement{} transaction spending an open head output, producing a new head output and multiple decommitted outputs.}\label{fig:decrementTx} \end{figure} @@ -431,49 +382,51 @@ \subsection{Close Transaction}\label{sec:close-tx} \begin{figure} \centering - \includegraphics[width=0.8\textwidth]{Hydra/Protocol/Figures/closeTx.pdf} + \includegraphics[width=0.8\textwidth]{Hydra/Protocol/Figures/closeTx.pdf} \caption{\mtxClose{} transaction spending the $\stOpen$ head output and producing a $\stClosed$ head output.}\label{fig:closeTx} \end{figure} \noindent The state-machine validator $\nuHead$ is spent with -$\redeemerHead = (\mathsf{close}, \xi, \textcolor{red}{\mathsf{CloseType}})$, where $\xi$ is a multi-signature of -the to be closed snapshot and $\mathsf{CloseType}$ is a hint against which state we close. The validator checks: +$\redeemerHead = (\mathsf{close}, \mathsf{CloseType})$, where +$\mathsf{CloseType}$ is a hint against which open state to close and checks: \begin{menumerate} \item State is advanced from $\datumHead \sim \stOpen$ to - $\datumHead' \sim \stClosed$, parameters $\cid,\hydraKeysAgg,\nop,\cPer$ + $\datumHead' \sim \stClosed$, parameters $\cid,\hydraKeys,\cPer$ stay unchanged and the new state is governed again by $\nuHead$ \[ - (\stOpen,\cid,\hydraKeysAgg,\nop,\cPer,\textcolor{red}{\eta_{\mathsf{pre}},s,\eta_{\mathsf{cur}}}) \xrightarrow[\xi]{\stClose} (\stClosed,\cid,\hydraKeysAgg,\nop,\cPer,\textcolor{red}{\eta_{c},s',\eta',\eta_{\Delta}},\contesters,\Tfinal) - \]\todo{this $\eta_{\Delta}$ might not work as we need to keep things separate} - - \item Closing snapshot number $s'$ is higher than the currently stored snapshot number $s$ - \[ - s' \geq s + (\stOpen,\cid,\hydraKeys,\cPer,v,\eta) \xrightarrow[\mathsf{CloseType}]{\stClose} (\stClosed,\cid,\hydraKeys,\cPer,v',s',\eta',\eta_{\Delta}',\contesters,\Tfinal) \] - \item Record the closed head state + + \item Last known open state version is recorded in closed state \[ - \eta_{c} = \eta_{\mathsf{cur}} + v' = v \] - \item Based on the redeemer $\mathsf{CloseType} = \mathsf{Initial} \cup \mathsf{Nominal} \cup (\mathsf{Preemptive},\eta_{\alpha}) \cup (\mathsf{Pending}, \eta_{\omega})$, we verify the signature distinguishing these cases: + + \item Based on the redeemer $\mathsf{CloseType} = \mathsf{Initial} \cup (\mathsf{Unused}, \xi) \cup (\mathsf{Used}, \xi, \eta_{\omega})$, where $\xi$ is a multi-signature of the closing snapshot and $\eta_{\omega}$ is a digest of the UTxO to decommit, three cases are distinguished: \begin{menumerate} - \item Initial close: The initial snapshot is used to close the head. No signatures are available and it suffices to check - \[ - s' = 0 - \] - \item Nominal close: Closing snapshot refers to current state $\eta_{\mathsf{cur}}$ and no UTxO is pending to be committed or decommitted. - \[ - \msVfy(\hydraKeysAgg,(\cid || \eta_{\mathsf{cur}}|| s' || \eta' || \bot || \bot),\xi) = \true - \] - \item Preemptive close: Instead of incrementing/decrementing, the head is closed with a snapshot that references the current state $\eta_{\mathsf{cur}}$, but has pending UTxO to commit. - \[ - \msVfy(\hydraKeysAgg,(\cid || \eta_{\mathsf{cur}} || s' || \eta' || \eta_{\alpha} || \eta_{\Delta}),\xi) = \true - \] - where $\eta_{\alpha}$ is provided by the redeemer. \todo{explain why this is enough} - \item Pending close: After incrementing/decrementing, the head is closed with a snapshot that is still referencing the previous state $\eta_{\mathsf{pre}}$ and pending UTxO to decommit. - \[ - \msVfy(\hydraKeysAgg,(\cid || \eta_{\mathsf{pre}} || s' || \eta' || \eta_{\Delta} || \eta_{\omega}),\xi) = \true - \] - where $\eta_{\omega}$ is provided by the redeemer. \todo{explain why this is enough} + \item $\mathsf{Initial}$: The initial snapshot is used to close the head and open state was not updated. No signatures are available and it suffices to check + \[ + v = 0 + \] + \[ + s' = 0 + \] + \[ + \eta' = \eta + \] + \item $\mathsf{Unused}$: Closing snapshot refers to current state version $v$ and any UTxO to decommit need to be present in the closed state too. + \[ + \msVfy(\hydraKeys,(\cid || v || s' || \eta' || \eta_{\Delta}'),\xi) = \true + \] + which implies $\eta_{\Delta}' = \eta_{\omega}$ while $\eta_{\omega}$ does not need to be provided. + \item $\mathsf{Used}$: Closing snapshot refers the previous state $v - 1$ and any UTxO to decommit of the closing snapshot must not be recorded in the closed state. + \[ + \eta_{\Delta}' = \bot + \] + \[ + \msVfy(\hydraKeys,(\cid || v - 1 || s' || \eta' || \eta_{\omega}),\xi) = \true + \] + where $\eta_{\omega}$ is provided by the redeemer\footnote{$\eta_{\omega}$ needs to be provided to verify the signature, but is otherwise not relevant for the closed state}. \end{menumerate} % TODO: detailed CDDL definition of msg @@ -485,13 +438,27 @@ \subsection{Close Transaction}\label{sec:close-tx} cases where pre-signed, valid in the future, close transactions are used to delegate head closing. - \item Correct contestation deadline is set $\Tfinal = \txValidityMax + T$. + \item Correct contestation deadline is set + \[ + \Tfinal = \txValidityMax + T + \] \item Transaction validity range is bounded by - $\txValidityMax - \txValidityMin \leq T$. \\ - This ensures the contestation deadline $\Tfinal$ is at most $2*T$ in the future. - \item Value in the head is preserved $\valHead' = \valHead$. - \item Transaction is signed by a participant $\exists \{\cid \mapsto \keyHash_{i} \mapsto 1\} \in \valHead' \Rightarrow \keyHash_{i} \in \txKeys$. - \item No minting or burning $\txMint = \varnothing$. + \[ + \txValidityMax - \txValidityMin \leq T + \] + to ensure the contestation deadline $\Tfinal$ is at most $2*T$ in the future. + \item Value in the head is preserved + \[ + \valHead' = \valHead + \] + \item Transaction is signed by a participant + \[ + \exists \{\cid \mapsto \keyHash_{i} \mapsto 1\} \in \valCommit{i} \Rightarrow \keyHash_{i} \in \txKeys + \] + \item No minting or burning + \[ + \txMint = \varnothing + \] \end{menumerate} \subsection{Contest Transaction}\label{sec:contest-tx} @@ -506,44 +473,61 @@ \subsection{Contest Transaction}\label{sec:contest-tx} \end{itemize} \begin{figure} - \centering \includegraphics[width=0.8\textwidth]{Hydra/Protocol/Figures/contestTx.pdf} + \includegraphics[width=0.8\textwidth]{Hydra/Protocol/Figures/contestTx.pdf} \caption{\mtxContest{} transaction spending the $\stClosed$ head output and producing a different $\stClosed$ head output.}\label{fig:contestTx} \end{figure} \noindent The state-machine validator $\nuHead$ is spent with -$\redeemerHead = (\mathsf{contest}, \xi)$, where $\xi$ is a multi-signature of -the contest snapshot, and checks: +$\redeemerHead = (\mathsf{contest}, \mathsf{ContestType})$, where +$\mathsf{ContestType}$ is a hint how to verify the snapshot and checks: \begin{menumerate} - \item State stays $\stClosed$ in both $\datumHead$ and $\datumHead'$, - parameters $\cid,\hydraKeysAgg,\nop,\cPer$ stay - unchanged and the new state is governed again by $\nuHead$: + \item State is advanced from $\datumHead \sim \stOpen$ to + $\datumHead' \sim \stClosed$, parameters $\cid,\hydraKeys,\cPer$ + stay unchanged and the new state is governed again by $\nuHead$ \[ - (\stClosed,\cid,\hydraKeysAgg,\nop,\cPer,s',\textcolor{red}{\eta_{c},\eta,\eta_{\Delta}},\contesters,\Tfinal) \xrightarrow[\xi]{\stContest} (\stClosed,\cid,\hydraKeysAgg,\nop,\cPer,s',\textcolor{red}{\eta_{c},\eta',\eta_{\Delta}'},\contesters',\Tfinal') + (\stClosed,\cid,\hydraKeys,\cPer,v,s,\eta,\eta_{\Delta},\contesters,\Tfinal) \xrightarrow[\mathsf{ContestType}]{\stContest} (\stClosed,\cid,\hydraKeys,\cPer,v',s',\eta',\eta_{\Delta}',\contesters',\Tfinal') + \] + + \item Last known open state version stays recorded in closed state + \[ + v' = v \] \item Contested snapshot number $s'$ is higher than the currently stored snapshot number $s$ \[ s' > s \] - \item We distinguish these cases: \todo{what happens to $\eta_{\Delta}$ if it is there?} + \item Based on the redeemer $\mathsf{ContestType} = (\mathsf{Unused}, \xi) \cup (\mathsf{Used}, \xi, \eta_{\omega})$, where $\xi$ is a multi-signature of the contesting snapshot and $\eta_{\omega}$ is a digest of the UTxO to decommit, two cases are distinguished: \begin{menumerate} - \item Nominal contest: Contesting snapshot refers to currently closed state $\eta$ and no UTxO is pending to be committed or decommitted. - \item Preemptive close: The head is contested with a snapshot that references the currently closed state $\eta$, but has either pending UTxO to commit, decommit or both. - \item Pending close: The head is contested with a snapshot that references the originally closed $\eta_{c}$ and has either pending UTxO to commit, decommit or both. + \item $\mathsf{Unused}$: Contesting snapshot refers to the current state version $v$ and any UTxO to decommit need to be present in the closed state too. + \[ + \msVfy(\hydraKeys,(\cid || v || s' || \eta' || \eta_{\Delta}'),\xi) = \true + \] + which implies $\eta_{\Delta}' = \eta_{\omega}$ while $\eta_{\omega}$ does not need to be provided. + \item $\mathsf{Used}$: Contesting snapshot refers the previous state version $v - 1$ and any UTxO to decommit must not be recorded in the closed state. + \[ + \eta_{\Delta}' = \bot + \] + \[ + \msVfy(\hydraKeys,(\cid || v - 1 || s' || \eta' || \eta_{\omega}),\xi) = \true + \] + where $\eta_{\omega}$ is provided by the redeemer\footnote{$\eta_{\omega}$ needs to be provided to verify the signature, but is otherwise not relevant for the closed state}. \end{menumerate} + % TODO: detailed CDDL definition of msg - - - - \textcolor{red}{Ensure $\eta_{\Delta}$ evolves correctly!?} $\xi$ is a valid multi-signature of the new snapshot state - $\msVfy(\hydraKeysAgg,(\cid || s' || \textcolor{red}{\eta_{0}} || \eta'),\xi) = \true$. \todo{$\eta_{0}$ replacement} - - \item The single signer $\{\keyHash\} = \txKeys$ has not already contested - $\keyHash \notin \contesters$ and is added to the set of contesters - $\contesters' = \contesters \cup \keyHash$. - \item Transaction is posted before deadline $\txValidityMax \leq \Tfinal$. + \item The single signer $\{\keyHash\} = \txKeys$ has not already contested and is added to the set of contesters + \[ + \keyHash \notin \contesters + \] + \[ + \contesters' = \contesters \cup \keyHash + \] + \item Transaction is posted before deadline + \[ + \txValidityMax \leq \Tfinal + \] \item Contestation deadline is updated correctly to \[ \Tfinal' = \left\{\begin{array}{ll} @@ -551,10 +535,18 @@ \subsection{Contest Transaction}\label{sec:contest-tx} \Tfinal + T & \mathrm{otherwise.} \end{array}\right. \] + \item Value in the head is preserved + \[ + \valHead' = \valHead + \] \item Transaction is signed by a participant - $\exists \{\cid \mapsto \keyHash_{i} \mapsto 1\} \in \valHead' \Rightarrow \keyHash_{i} \in \txKeys$. - \item Value in the head is preserved $\valHead' = \valHead$. - \item No minting or burning $\txMint = \varnothing$. + \[ + \exists \{\cid \mapsto \keyHash_{i} \mapsto 1\} \in \valCommit{i} \Rightarrow \keyHash_{i} \in \txKeys + \] + \item No minting or burning + \[ + \txMint = \varnothing + \] \end{menumerate} \subsection{Fan-Out Transaction} @@ -564,7 +556,7 @@ \subsection{Fan-Out Transaction} distributes UTxOs from the head according to the latest state. It consists of \begin{itemize} \item one input spending from $\nuHead$ holding the $\st$, and - \item outputs $o_{1} \dots o_{m}$ to distribute UTxOs. + \item outputs $o_{1} \dots o_{m+n}$ to distribute UTxOs. \end{itemize} Note that \mtxFanout{} represents a final transition of the state machine and @@ -572,25 +564,31 @@ \subsection{Fan-Out Transaction} \begin{figure} \centering - \includegraphics[width=0.8\textwidth]{Hydra/Protocol/Figures/fanoutTx.pdf} + \includegraphics[width=0.8\textwidth]{Hydra/Protocol/Figures/fanoutTx.pdf} \caption{\mtxFanout{} transaction spending the $\stClosed$ head output and distributing funds with outputs $o_{1} \dots o_{m}$.}\label{fig:fanoutTx} \end{figure} \noindent The state-machine validator $\nuHead$ is spent with -$\redeemerHead = (\mathsf{fanout}, m)$, where $m$ is the number of outputs to -distribute, and checks: +$\redeemerHead = (\mathsf{fanout}, m, n)$, where $m$ and $n$ are +outputs to distribute from the $\stClosed$ state, and checks: \begin{menumerate} \item State is advanced from $\datumHead \sim \stClosed$ to terminal state $\stFinal$: % XXX: What does this actually mean? \[ - (\stClosed,\cid,\hydraKeysAgg,\nop,\cPer,\eta_0,s,\eta,\contesters,\Tfinal) \xrightarrow[m]{\stFanout} \stFinal + (\stClosed,\cid,\hydraKeys,\cPer,v, s,\eta,\eta_{\Delta},\contesters,\Tfinal) \xrightarrow[m,n]{\stFanout} \stFinal + \] + \item The first $m$ outputs are distributing funds according to $\eta$. That is, + the outputs exactly correspond to the UTxO canonically combined $U^{\#}$ (see + Section~\ref{sec:collect-tx}): + \[ + \eta = U^{\#} = \hash(\bigoplus_{j=1}^{m} \bytes(o_{j})) \] - \item The first $m$ outputs are distributing funds according to - $\eta$. That is, the outputs exactly correspond to the UTxO - canonically combined $U^{\#}$ (see Section~\ref{sec:collect-tx}): + \item The following $n$ outputs are distributing funds according to + $\eta_{\Delta}$. That is, the outputs exactly correspond to the UTxO canonically + combined $U^{\#}_{\Delta}$ (see Section~\ref{sec:collect-tx}): \[ - \hash(\bigoplus_{j=1}^{m} \bytes(o_{j})) = U^{\#} = \eta + \eta_{\Delta} = U^{\#}_{\Delta} = \hash(\bigoplus_{j=m}^{m+n} \bytes(o_{j})) \] \item Transaction is posted after contestation deadline $\txValidityMin > \Tfinal$. \item All tokens are burnt diff --git a/hydra-protocol/Hydra/Protocol/Overview.tex b/hydra-protocol/Hydra/Protocol/Overview.tex index 23ee636..dc96f79 100644 --- a/hydra-protocol/Hydra/Protocol/Overview.tex +++ b/hydra-protocol/Hydra/Protocol/Overview.tex @@ -45,7 +45,7 @@ \subsection{Opening the head} evolves the initial UTxO set (the union over all UTxOs committed by all head members) independently of the mainchain. For the case where some head members fail to post a \mtxCom{} transaction, the head can be aborted by going directly -from $\stInitial$ to $\stFinal$ \todo{increment / decrement}. +from $\stInitial$ to $\stFinal$. \subsection{The Coordinated Head protocol} @@ -59,8 +59,8 @@ \subsection{The Coordinated Head protocol} set of UTxOs evolved from the initial UTxO set by applying transactions as they are received from the other parties. -To confirm transactions and allow for an on-chain decommit of the resulting UTxO -set without needing the whole transaction history, snapshots are created by the +To confirm transactions and allow for distribution of the resulting UTxO set +without needing the whole transaction history, snapshots are created by the protocol participants. The initial snapshot $U_{0}$ corresponds to the initial UTxO set, while snapshots thereafter $\Uset_1,\Uset_2,\ldots$ are created with monotonically increasing snapshot numbers. @@ -80,6 +80,10 @@ \subsection{The Coordinated Head protocol} transactions that have been processed into it as the snapshot's multi-signature is now evidence that this state once existed during the head evolution. +Besides processing normal transactions, participants can also request to take +UTxO they can spend out of the Head and make it available on the main chain +using a \mtxDecrement{} transaction --- the whole process is called decommit. + \subsection{Closing the head} The head protocol is designed to allow any head member at any point in time to @@ -112,7 +116,7 @@ \subsection{Differences} \item No hanging transactions due to `coordination'. \item No acknowledgement nor confirmation of transactions. \item No confirmation message for snapshots (two-round local confirmation). - \todo{increment / decrement extension} + \item Allow for incremental decommits while head is open. \end{itemize} %%% Local Variables: diff --git a/hydra-protocol/Hydra/Protocol/Preliminaries.tex b/hydra-protocol/Hydra/Protocol/Preliminaries.tex index 6de8439..8011758 100644 --- a/hydra-protocol/Hydra/Protocol/Preliminaries.tex +++ b/hydra-protocol/Hydra/Protocol/Preliminaries.tex @@ -97,7 +97,7 @@ \subsection{Extended UTxO}\label{sec:eutxo} \begin{figure}[h] \centering - \includegraphics[width=0.5\textwidth]{Hydra/Protocol/Figures/utxo-graph.pdf} + \includegraphics[width=0.5\textwidth]{Hydra/Protocol/Figures/utxo-graph.pdf} \caption{Example of a plain UTxO graph}\label{fig:utxo-graph} \end{figure} @@ -175,6 +175,7 @@ \subsubsection{Scripts} \end{definition} \subsubsection{Transactions} +\todo{actual transactions $\mathcal{T}$ are not defined} We define EUTxO inputs, outputs and transactions as they are available to scripts and just enough to specify the behavior of the Hydra validator scripts.