diff --git a/spec/fig_offchain_prot.tex b/spec/fig_offchain_prot.tex index 944278f4730..84fd98bfc04 100644 --- a/spec/fig_offchain_prot.tex +++ b/spec/fig_offchain_prot.tex @@ -47,10 +47,11 @@ $\Uinit \gets \bigcup_{j=1}^{n} U_j$ \; % $\Out~(\hpSnap,(0,U_0))$ \; $\hatmL \gets \Uinit$ \; - $\bar{\mc S} \gets \blue{\Sno(0, 0, \Uinit, \emptyset, \bot)}$ \; + $\bar{\mc S} \gets \blue{\Sno(0, 0, \Uinit, \emptyset, \bot \red{, \bot})}$ \; $\hatv, \hats \gets 0$ \; $\hatmT \gets \emptyset$ \; - $\tx_{\omega} \gets \bot$ \; + $\tx_\omega \gets \bot$ \; + \red{$\tx_\alpha \gets \bot$ \;} } \end{walgo} @@ -73,7 +74,7 @@ $\hatmT \gets \hatmT \cup \{\tx\}$ \; % issue snapshot if we are leader \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})$ \; + \Multi{} $(\hpRS,\hatv,\bar{\mc S}.s+1,\hatmT \red{,\tx_\alpha}, \tx_\omega)$ \; } } } @@ -81,21 +82,24 @@ \vspace{12pt} %%% REQ SN - \On{$(\hpRS,v,s,\mT_{\mathsf{req}}, \tx_{\omega})$ from $\party_j$}{ + \On{$(\hpRS,v,s,\mT_{\mathsf{req}} \red{, \tx_\alpha} , \tx_\omega)$ from $\party_j$}{ + \red{\Req{$\tx_\omega = \bot ~ \lor ~ \tx_\alpha = \bot$}} \; \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})}$ \; + \blue{ + \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}))$ \; + \red{$\eta_\alpha \gets \mathsf{combine}(\mathsf{inputs}(\tx_\alpha))$ \;} + $\eta_\omega \gets \mathsf{combine}(\mathsf{outputs}(\tx_\omega))$ \; % NOTE: WE could make included transactions auditable by adding % a merkle tree root to the (signed) snapshot data \eta - $\msSig_i \gets \msSign(\hydraSigningKey, (\cid || v || \hats || \eta || \eta_{\omega}))$ \; + $\msSig_i \gets \msSign(\hydraSigningKey, (\cid || v || \hats || \eta \red{ || \eta_\alpha} || \eta_\omega))$ \; $\hatSigma \gets \emptyset$ \; $\Multi{}~(\hpAS,\hats,\msSig_i)$ \; $\forall \tx \in \mT_{\mathsf{req}}: \Out~(\hpSeen,\tx)$ \; @@ -116,13 +120,14 @@ \adjustbox{valign=t,scale=\sfact}{ \begin{walgo}{0.7} %%% REC DEC + % \delta \in \tx_\omega \On{$(\mathtt{reqDec},\tx)$ from $\party_j$}{ - \Wait{$\tx_\omega = \bot ~ \land ~ \hatmL \applytx \tx \not= \bot$}{ + \Wait{$\tx_\omega \red{= \tx_{\alpha}} = \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 = \bar{\mc S}.s \land \hpLdr(\bar{\mc S}.s + 1) = i$}{ - \Multi{} $(\hpRS,\hatv,\bar{\mc S}.s+1,\hatmT, \tx_{\omega})$ \; + \Multi{} $(\hpRS,\hatv,\bar{\mc S}.s+1,\hatmT \red{,\tx_\alpha},\tx_\omega)$ \; } } } @@ -139,83 +144,116 @@ \vspace{12pt} - %%% ACK SN - \On{$(\hpAS,s,\msSig_j)$ from $\party_j$}{ - \Req{} $s \in \{\hats,\hats+1\}$ \; - \Wait{$\hats=s$}{ - \Req{} $(j, \cdot) \notin \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)$ \; - - % TODO: DRY message creation - $\eta \gets \combine(\hatmU)$ \; - $\eta_{\omega} \gets \combine(\mathsf{outputs}(\tx_{\omega}))$ \; - - % 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$ \; - - %$\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})$ \;} - } + %%% REC INC + \red{ + \On{$(\mathtt{reqInc}, \tx)$ from $\party_j$}{ + \Wait{$\tx_\alpha = \tx_{\omega} = \bot$}{ + $\tx_\alpha \gets \tx$\; % issue snapshot if we are leader - \If{$\hpLdr(s+1) = i \land \hatmT \neq \emptyset$}{ - \Multi{} $(\hpRS,\hatv,\bar{\mc S}.s+1, \hatmT, \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, \red{\tx_\alpha} , \tx_\omega)$ \; } } } } + + \vspace{12pt} + + %%% INCREMENT + \red{\On{$(\mathtt{incrementTx}, U, v)$ from chain}{ + \If{$\mathsf{inputs}(\tx_\alpha) = U$}{ + $\hatmL \gets \hatmL \cup U$ \; + $\tx_\alpha \gets \bot$\; + $\hatv \gets v$ \; + } + } + } + \end{walgo} } \end{tabular} + \end{tabular} + \end{algobox} - \\ - \multicolumn{1}{l}{\line(1,0){490}} - \\ +\end{figure*} +\clearpage +\begin{figure*}[t!] + + \def\sfact{0.8} + \begin{tabular}{c} + \\ + \multicolumn{1}{l}{\line(1,0){490}} + \\ + \begin{tabular}{c c} + \adjustbox{valign=t,scale=\sfact}{ + \begin{walgo}{0.6} + %%% ACK SN + \On{$(\hpAS,s,\msSig_j)$ from $\party_j$}{ + \Req{} $s \in \{\hats,\hats+1\}$ \; + \Wait{$\hats=s$}{ + \Req{} $(j, \cdot) \notin \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)$ \; + + % TODO: DRY message creation + $\eta \gets \combine(\hatmU)$ \; + + \red{$\eta_\alpha \gets \mathsf{combine}(\mathsf{inputs}(\tx_\alpha))$ \;} + $\eta_\omega \gets \mathsf{combine}(\mathsf{outputs}(\tx_\omega))$ \; + % 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 \red{|| \eta_\alpha} || \eta_\omega), \msCSig)$ \; + % create confirmed snapshot for later reference + \blue{$\bar{\mc S} \gets \Sno(\hatv, \hats, \hatmU, \hatmT, U_\alpha, U_\omega)$ \;} + $\bar{\mc S}.\sigma \gets \msCSig$ \; + %$\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{}~(\mathtt{decrementTx}, \hatv, \hats, \eta, \red{\eta_\alpha}, \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$}{ + \Multi{} $(\hpRS,\hatv,\bar{\mc S}.s+1, \hatmT \red{, \tx_\alpha}, \tx_\omega)$ \; + } + } + } + } + \end{walgo} + } %%% Closing the head - \begin{tabular}{c c} - \adjustbox{valign=t,scale=\sfact}{ - \begin{walgo}{0.6} - % CLOSE from client - \On{$(\hpClose)$ from client}{ + \adjustbox{valign=t,scale=\sfact}{ + \begin{walgo}{0.6} + % CLOSE from client + \On{$(\hpClose)$ from client}{ + $\eta \gets \combine(\bar{\mc S}.U)$ \; + $\eta_\omega \gets \combine(\bar{\mc S}.U_\omega)$ \; + \red{$\eta_\alpha \gets \combine(\bar{\mc S}.U_\alpha$) \;} + $\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 \red{, \eta_\alpha}, \eta_\omega, \xi)$ \; + } + \vspace{12pt} + \On{$(\gcChainClose, \eta) \lor (\gcChainContest, s_{c}, \eta)$ from chain}{ + \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))$ \; + $\eta_\omega \gets \combine({\bar{\mc S}.U_\omega})$ \; + \red{$\eta_\alpha \gets \combine(\bar{\mc S}.U_\alpha$) \;} $\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} - } - & - \adjustbox{valign=t,scale=\sfact}{ - \begin{walgo}{0.6} - \On{$(\gcChainClose, \eta) \lor (\gcChainContest, s_{c}, \eta)$ from chain}{ - \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)$ \; - } + $\PostTx{}~(\mtxContest, \hatv, \bar{\mc S}.v, \bar{\mc S}.s, \eta \red{, \eta_\alpha}, \eta_\omega , \xi)$ \; } - \end{walgo} - } - \end{tabular} + } + \end{walgo} + } \end{tabular} - \bigskip - \end{algobox} - + \end{tabular} \caption{Head-protocol machine for the \emph{coordinated head} from the perspective of party $\party_i$.}\label{fig:off-chain-prot} diff --git a/spec/figures/closeTx.pdf b/spec/figures/closeTx.pdf index 123f79def42..fc619aac76a 100644 Binary files a/spec/figures/closeTx.pdf and b/spec/figures/closeTx.pdf differ diff --git a/spec/figures/contestTx.pdf b/spec/figures/contestTx.pdf index 262d6d596d5..6de0c17244b 100644 Binary files a/spec/figures/contestTx.pdf and b/spec/figures/contestTx.pdf differ diff --git a/spec/figures/decrementTx.pdf b/spec/figures/decrementTx.pdf index 6b854be0f55..d1e6f29dd90 100644 Binary files a/spec/figures/decrementTx.pdf and b/spec/figures/decrementTx.pdf differ diff --git a/spec/figures/incrementTx.odg b/spec/figures/incrementTx.odg new file mode 100644 index 00000000000..dde118cae4f Binary files /dev/null and b/spec/figures/incrementTx.odg differ diff --git a/spec/figures/incrementTx.pdf b/spec/figures/incrementTx.pdf new file mode 100644 index 00000000000..25029006b04 Binary files /dev/null and b/spec/figures/incrementTx.pdf differ diff --git a/spec/macros.tex b/spec/macros.tex index 44143dbb49b..d52ba87e50e 100644 --- a/spec/macros.tex +++ b/spec/macros.tex @@ -242,6 +242,7 @@ \newcommand{\mtxCommit}{\textit{commit}} \newcommand{\mtxCCom}{\textit{collectCom}} \newcommand{\mtxCollect}{\textit{collectCom}} +\newcommand{\mtxIncrement}{\textit{increment}} \newcommand{\mtxDecrement}{\textit{decrement}} \newcommand{\mtxAbort}{\textit{abort}} \newcommand{\mtxClose}{\textit{close}} @@ -417,6 +418,7 @@ \newcommand{\hpNS}{\mathtt{newSn}} \newcommand{\hpRS}{\mathtt{reqSn}} +\newcommand{\hpRI}{\mathtt{reqInc}} \newcommand{\hpRD}{\mathtt{reqDec}} \newcommand{\hpAS}{\mathtt{ackSn}} \newcommand{\hpCS}{\mathtt{confSn}} diff --git a/spec/offchain.tex b/spec/offchain.tex index f6cfc220998..cc9b19ba9e8 100644 --- a/spec/offchain.tex +++ b/spec/offchain.tex @@ -26,6 +26,7 @@ \section{Off-Chain Protocol}\label{sec:offchain} \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 $\hpRI$: to request inclusion of UTxO via a commit 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 @@ -115,21 +116,24 @@ \subsection{Variables} \item $\hatmL$: UTxO set representing the local ledger state resulting from 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 $\tx_{\omega} \in \mathcal{T}^{?}$: Pending decommit transaction, whose outputs are to be decommitted from the head. May be $\bot$ if nothing to decommit. + inclusion in a snapshot (if this party is the next leader). + \item \red{$\tx_\alpha \in \mathcal{T}$: Pending increment transaction, whose inputs are to be deposited to the head.} + \item $\tx_\omega \in \mathcal{T}$: Pending decrement transaction, whose outputs are to be withdrawn from the head. \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?} + \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 + \red{$\bar{\mc S}.U_\alpha = \mathsf{inputs}(\tx_\alpha)$} & \red{pending UTxO to commit} \\ \hline + \red{$\bar{\mc S}.U_\omega = \mathsf{outputs}(\tx_\omega)$} & \red{pending UTxO to decommit} \\ \hline + $\bar{\mc S}.\sigma$ & multisignature \\ \hline + \end{tabular} + \end{center} + The function $\Sno(v,n,U,T,\red{U_\alpha}, U_\omega)$ initializes a snapshot object with no multi-signature set. + \todo{handwavy; types?} + \end{itemize} \subsection{Protocol flow} @@ -163,9 +167,10 @@ \subsubsection{Initializing the head} 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)}$. +well as snapshot number $\hats = 0$. No \red{increment/}decrement UTxO is pending +($U_\alpha = \mathsf{inputs}(\tx_\alpha) = \bot \land U_\omega = \mathsf{outputs}(\tx_\omega) = \bot$) +and the initial snapshot object is defined accordingly +$\bar{\mc S} \gets \blue{\Sno(0, 0, \Uinit, \emptyset, \red{U_\alpha}, U_\omega)}$. \subsubsection{Processing transactions off-chain} @@ -185,45 +190,66 @@ \subsubsection{Processing transactions off-chain} 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{$\hpRD$.}\quad Upon receiving request $(\hpRD,\tx_\omega)$, the transaction is +checked against the \emph{local} ledger state and if it is not applicable yet or another +commit or decommit is pending still, the protocol does $\KwWait$ to retry later or +eventually marks the decommit as invalid. \red{After applying $\tx$, it's inputs +are removed from \emph{local} ledger state so that they are not available any +more and the outputs are kept in the local state ($U_\omega$) to be posted +on-chain in the next snapshot.} Finally, 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$ containing +the decrement transaction $\tx_\omega$ is sent. \\ \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} \\ +transaction, which removed outputs $U$ from the head, the corresponding +pending decrement 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} +\todo{missing to mention the multicast of $\hpRS$} \\ + +\red{\dparagraph{$\hpRI$.}\quad Upon receiving request $(\hpRI,\tx)$, if another commit or decommit + is pending, the protocol does wait to retry later or eventually marks the decommit as invalid. + Otherwise the transaction inputs are kept in the local state ($U_\alpha$) to be included + in the \emph{local} ledger state upon observing the relevant transaction on-chain. + Finally, 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$ containing the increment transaction $\tx_\alpha$ is sent.} \\ + +\red{\dparagraph{$\mathtt{incrementTx}$.}\quad Upon observing the \mtxIncrement{} + transaction which inputs are added to the confirmed UTxO in the Head, we include + the inputs to the \emph{local} ledger state so that they become available. + Finally the corresponding pending increment + transaction is cleared and the observed version is used for future snapshots by setting + $\hatv = v$. The version of the open head state is incremented on each \mtxIncrement{} + transaction as described in Section~\ref{sec:increment-tx} +} +\todo{missing to mention the multicast of $\hpRS$} \\ \dparagraph{$\hpRS$.}\quad Upon receiving request -$(\hpRS,v,s,\mT_{\mathsf{req}}, \tx_{\omega})$\footnote{Snapshot requests +$(\hpRS,v,s,\mT_{\mathsf{req}}, \red{\tx_\alpha}, \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$. \\ + confirmed ($\bar{\mc S}.s = \hats$). + 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), \red{$\eta_\alpha$ derived from $\tx_\alpha$} and $\eta_\omega$ derived from $\tx_\omega$. + 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 @@ -232,32 +258,41 @@ \subsubsection{Processing transactions off-chain} 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 (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. +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{\mathsf{inputs}(tx_\alpha)}, \mathsf{outputs}(tx_\omega))$ +and storing the multi-signature $\msCSig$ in it for later reference. Then, in case: +\begin{itemize} +\item + there is a pending decrement any participant\todo{Shouldn't the decommitting party do this?} can now submit a $\mathtt{decrementTx}$ + by providing the just confirmed snapshot with its digests of the active UTxO set + $\eta$ and the UTxO set to be removed $\eta_\omega$. + +\red{\item + there is a pending increment any participant can now submit an $\mathtt{incrementTx}$ + by providing the confirmed snapshot with its digests of the active UTxO set + $\eta$ and the UTxO set to be added $\eta_\alpha$.} +\end{itemize} +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 $\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. \\ +create the new $\eta$-state from the last confirmed UTxO set, \red{the digest of +either increment or decrement UTxO set ($\eta_\alpha$ or $\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 the head getting closed or contested, the $\eta$-state extracted from the \mtxClose{} or \mtxContest{} transaction represents the latest head status that has been aggregated on-chain so far (by a sequence of \mtxClose{} and \mtxContest{} transactions). If the last confirmed (off-chain) snapshot is newer -than the observed (on-chain) snapshot number $s_{c}$, an updated $\eta$-state -and certificate $\xi$ is constructed posted in a \mtxContest{} transaction (see +than the observed (on-chain) snapshot number $s_{c}$, an updated $\eta$-state, +\red{along with the digest of either increment or decrement UTxO set ($\eta_\alpha$ or $\eta_\omega$)}, +and certificate $\xi$ is constructed and posted in a \mtxContest{} transaction (see Section~\ref{sec:contest-tx}). \subsection{Rollbacks and protocol changes}\label{sec:rollbacks} @@ -321,7 +356,7 @@ \subsection{Rollbacks and protocol changes}\label{sec:rollbacks} \todo{Write about contestation deadline vs. rollbacks} \input{fig_offchain_prot} - +\todo{FIXME: race-condition on RecInc/RecDec requests; use seen snapshot to resolve} \todo{In figure: $\combine$ on UTxO slightly different than on commits} %%% Local Variables: diff --git a/spec/onchain.tex b/spec/onchain.tex index 4dd23a7792a..570baece54e 100644 --- a/spec/onchain.tex +++ b/spec/onchain.tex @@ -315,9 +315,65 @@ \subsection{CollectCom Transaction}\label{sec:collect-tx} $\stOpen$ head output.}\label{fig:collectComTx} \end{figure} +\subsection{\red{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 zero or more inputs with reference $\txOutRef_{\mathsf{increment}_{j}}$ + spending output $o_{\mathsf{increment}_{j}}$ with + $\val_{\mathsf{increment}_{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, $s$, \txOutRef_{\mathsf{increment}})$, where $\xi$ is a multi-signature of +the increment snapshot which authorizes addition of some UTxO $U_\alpha$, $s$ is the snapshot number and $\txOutRef_{\mathsf{increment}}$ are the output references we need to spend. The +validator 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$: + \[ + (\stOpen,\cid,\hydraKeysAgg,\nop,\cPer,v,\eta) \xrightarrow[\xi, \txOutRef_{\mathsf{increment}}]{\mathsf{increment}} (\stOpen,\cid,\hydraKeysAgg,\nop,\cPer,v',\eta') + \] + \item New version $v'$ is incremented correctly + \[ + v' = v + 1 + \] +\item $\xi$ is a valid multi-signature of the new snapshot state (currency id $\cid$, the current state version $v$, the new state $\eta'$, UTxO to deposit $\eta_\alpha$) + \[ + \msVfy(\hydraKeys,(\cid || v || s || \eta' || \eta_\alpha || \bot),\xi) = \true + \] + where snapshot number $s$ is provided through the redeemer, $\eta_\alpha$ is the digest of all added UTxO. + \[ + \eta_\alpha = \hash(\bigoplus_{j=1}^m \bytes(o_{\mathsf{increment}_j})) + \] + \item The value in the head output is increased accordingly + \todo{Redundant to above? Only check $\valHead' > \valHead$?} + \[ + \valHead \cup (\bigcup_{j=1}^m \val_{i_{j}}) = \valHead' + \] + \item Transaction is signed by a participant + \todo{Allow anyone to do increments?} + \[ + \exists \{\cid \mapsto \keyHash_{i} \mapsto 1\} \in \valHead' \Rightarrow \keyHash_{i} \in \txKeys + \] +\end{menumerate} + +\begin{figure} + \centering + \includegraphics[width=0.8\textwidth]{figures/incrementTx.pdf} + \caption{\mtxIncrement{} transaction spending an open head output, + producing a new head output which includes the new UTxO.}\label{fig:incrementTx} +\end{figure} + \subsection{Decrement Transaction}\label{sec:decrement-tx} -\noindent The \mtxDecrement{} transaction (Figure~\ref{fig:DecrementTx}) allows +\noindent The \mtxDecrement{} transaction (Figure~\ref{fig:decrementTx}) allows a party to remove a UTxO from an already open head and consists of: \begin{itemize} @@ -343,13 +399,13 @@ \subsection{Decrement Transaction}\label{sec:decrement-tx} \[ v' = v + 1 \] - \item $\xi$ is a valid multi-signature of the currency id $\cid$, the current state version $v$, and the new state $\eta'$ + \item $\xi$ is a valid multi-signature of the new snapshot state (currency id $\cid$, the current state version $v$, the new state $\eta'$ \red{, UTxO to deposit $\eta_\alpha$} and UTxO to withdraw $\eta_\omega$) \[ - \msVfy(\hydraKeys,(\cid || v || s || \eta' || \eta_{\omega}),\xi) = \true + \msVfy(\hydraKeys,(\cid || v || s || \eta' || \red{\bot} || \eta_\omega),\xi) = \true \] - where snapshot number $s$ is provided through the redeemer and $\eta_{\omega}$ must be 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=2}^{m+1} \bytes(o_{j})) + \red{\eta_\omega} = \hash(\bigoplus_{j=2}^{m+1} \bytes(o_{j})) \] \item The value in the head output is decreased accordingly \todo{Redundant to above? Only check $\valHead' < \valHead$?} @@ -394,15 +450,14 @@ \subsection{Close Transaction}\label{sec:close-tx} $\datumHead' \sim \stClosed$, parameters $\cid,\hydraKeys,\cPer$ stay unchanged and the new state is governed again by $\nuHead$ \[ - (\stOpen,\cid,\hydraKeys,\cPer,v,\eta) \xrightarrow[\mathsf{CloseType}]{\stClose} (\stClosed,\cid,\hydraKeys,\cPer,v',s',\eta',\eta_{\Delta}',\contesters,\Tfinal) + (\stOpen,\cid,\hydraKeys,\cPer,v,\eta) \xrightarrow[\mathsf{CloseType}]{\stClose} (\stClosed,\cid,\hydraKeys,\cPer,v',s',\eta', \eta_\Delta', \contesters,\Tfinal) \] - \item Last known open state version is recorded in closed state \[ v' = v \] - \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: +\item Based on the redeemer $\mathsf{CloseType} = \mathsf{Initial} \red{\cup (\mathsf{UnusedInc}, \xi, \eta_\alpha)} \cup (\mathsf{UnusedDec}, \xi) \red{\cup (\mathsf{UsedInc}, \xi)} \cup (\mathsf{UsedDec}, \xi, \eta_\omega) $, where $\xi$ is a multi-signature of the closing snapshot \red{and $\eta_\alpha$} and $\eta_\omega$ are the digests of the UTxO to \red{increment or} decrement respectively, \red{five} cases are distinguished: \begin{menumerate} \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 \[ @@ -414,19 +469,57 @@ \subsection{Close Transaction}\label{sec:close-tx} \[ \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. + \red{ + \item $\mathsf{UnusedInc}$: Closing snapshot refers to current state version $v$ and any UTxO to increment must not be recorded in the closed state. + \[ + \eta_\Delta' = \bot + \] + \[ + \eta_\omega = \bot + \] + \[ + \msVfy(\hydraKeys,(\cid || v || s' || \eta' || \eta_\alpha || \eta_\omega),\xi) = \true + \] + where $\eta_\alpha$ is provided by the redeemer \footnote{$\eta_\alpha$ needs to be provided to verify the signature, but is otherwise not relevant for the closed state}. + } + \item $\mathsf{UnusedDec}$: Closing snapshot refers to current state version $v$ and any UTxO to decrement need to be present in the closed state too. \[ - \msVfy(\hydraKeys,(\cid || v || s' || \eta' || \eta_{\Delta}'),\xi) = \true + \eta_\omega = \eta_\Delta' \neq \bot \] - 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. + \red{ + \[ + \eta_\alpha = \bot + \] + } \[ - \eta_{\Delta}' = \bot + \msVfy(\hydraKeys,(\cid || v || s' || \eta' \red{|| \eta_\alpha} || \eta_\omega),\xi) = \true \] + \todo{this is hard to understand} + \red{ + \item $\mathsf{UsedInc}$: Closing snapshot refers the previous state $v - 1$ and any UTxO to increment must be recorded in the closed state. + \[ + \eta_\alpha = \eta_\Delta' \neq \bot + \] + \[ + \eta_\omega = \bot + \] + \[ + \msVfy(\hydraKeys,(\cid || v - 1 || s' || \eta' || \eta_\alpha || \eta_\omega ),\xi) = \true + \] + } + \item $\mathsf{UsedDec}$: Closing snapshot refers the previous state $v - 1$ and any UTxO to decrement must not be recorded in the closed state. \[ - \msVfy(\hydraKeys,(\cid || v - 1 || s' || \eta' || \eta_{\omega}),\xi) = \true + \eta_\omega = \eta_\Delta' = \bot \] - 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}. + \red{ + \[ + \eta_\alpha = \bot + \] + } + \[ + \msVfy(\hydraKeys,(\cid || v - 1 || s' || \eta' \red{|| \eta_\alpha} || \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 @@ -498,22 +591,60 @@ \subsection{Contest Transaction}\label{sec:contest-tx} \[ s' > s \] +\item $\mathsf{ContestType} = \red{(\mathsf{UnusedInc}, \xi, \eta_\alpha)} \cup (\mathsf{UnusedDec}, \xi) \red{\cup (\mathsf{UsedInc}, \xi)} \cup (\mathsf{UsedDec}, \xi, \eta_\omega)$, where $\xi$ is a multi-signature of the contesting snapshot \red{and $\eta_\alpha$} and $\eta_\omega$ are the digests of the UTxO to \red{increment or} decrement respectively, \red{four} cases are distinguished: - \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 $\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. + %% FIXME: \red{\item ...} does not work + \item \red{$\mathsf{UnusedInc}$: Contesting snapshot refers to current state version $v$ and any UTxO to increment must be $\bot$ in the closed state. + \[ + \eta_\alpha = \eta_\Delta' = \bot + \] + \[ + \eta_\omega = \bot + \] + \[ + \msVfy(\hydraKeys,(\cid || v || s' || \eta' || \eta_\alpha || \eta_\omega),\xi) = \true + \] + where $\eta_\alpha$ is provided by the redeemer \footnote{$\eta_\alpha$ needs to be provided to verify the signature, but is otherwise not relevant for the closed state}.} + + \item $\mathsf{UnusedDec}$: Contesting snapshot refers to current state version $v$ and any UTxO to decrement need to be present in the closed state too. + \[ + \eta_\omega = \eta_\Delta' \neq \bot + \] + \red{ + \[ + \eta_\alpha = \bot + \] + } \[ - \msVfy(\hydraKeys,(\cid || v || s' || \eta' || \eta_{\Delta}'),\xi) = \true + \msVfy(\hydraKeys,(\cid || v || s' || \eta' \red{|| \eta_\alpha} || \eta_\omega),\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. + \red{ + \item $\mathsf{UsedInc}$: Contesting snapshot refers the previous state $v - 1$ and any UTxO to increment must be recorded in the closed state. + \[ + \eta_\alpha = \eta_\Delta' \neq \bot + \] + \[ + \eta_\omega = \bot + \] + \[ + \msVfy(\hydraKeys,(\cid || v - 1 || s' || \eta' || \eta_\alpha || \eta_\omega ),\xi) = \true + \] + } + + \item $\mathsf{UsedDec}$: Contesting snapshot refers the previous state $v - 1$ and any UTxO to decrement must not be recorded in the closed state. \[ - \eta_{\Delta}' = \bot + \eta_\omega = \eta_\Delta' = \bot \] + \red{ + \[ + \eta_\alpha = \bot + \] + } \[ - \msVfy(\hydraKeys,(\cid || v - 1 || s' || \eta' || \eta_{\omega}),\xi) = \true + \msVfy(\hydraKeys,(\cid || v - 1 || s' || \eta' \red{|| \eta_\alpha} || \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}. + 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 diff --git a/spec/overview.tex b/spec/overview.tex index 05d70cf4b1a..94417379a32 100644 --- a/spec/overview.tex +++ b/spec/overview.tex @@ -80,9 +80,11 @@ \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. +\red{Besides processing ``normal'' transactions, participants can also request + to withdraw some UTxO they can spend from the Head and make it available on main + chain, or deposit some UTxO they can spend from L1 and make it available within the Head. + These processes are called decrement, via the \mtxDecrement{} transaction, + and increment, via the \mtxIncrement{} transaction.} \subsection{Closing the head} @@ -116,7 +118,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). - \item Allow for incremental decommits while head is open. + \item Allow for \red{incremental commits and} decommits while head is open. \end{itemize} %%% Local Variables: