From f71eae566ebb078dd3f9e8de1b603b589f849210 Mon Sep 17 00:00:00 2001 From: Sebastian Nagel Date: Wed, 19 Jun 2024 20:06:56 +0200 Subject: [PATCH] WIP: Add version to off-chain code --- spec/fig_offchain_prot.tex | 37 ++++++++++--------- spec/macros.tex | 3 +- spec/offchain.tex | 73 ++++++++++++++++++++++---------------- spec/prel.tex | 2 +- 4 files changed, 67 insertions(+), 48 deletions(-) diff --git a/spec/fig_offchain_prot.tex b/spec/fig_offchain_prot.tex index 0bf68cf111e..a6a662aa167 100644 --- a/spec/fig_offchain_prot.tex +++ b/spec/fig_offchain_prot.tex @@ -49,8 +49,8 @@ $\hatmU, \barmU, \hatmL \gets \Uinit$ \; \red{$\tx_{\omega} \gets \bot$ \;} $\hats,\bars \gets 0$ \; - \red{$v \gets 0$ \;} % FIXME: use version - $\mT, \hatmT, \barmT \gets \emptyset$ \; + \red{$\hatv \gets 0$ \;} % FIXME: use version + $\mT, \hatmT \gets \emptyset$ \; } \end{walgo} @@ -73,7 +73,7 @@ $\hatmT \gets \hatmT \cup \{\tx\}$ \; % issue snapshot if we are leader \If{$\hats = \bars \land \hpLdr(\bars + 1) = i$}{ - \Multi{} $(\hpRS,\bars+1, \hatmT, \textcolor{red}{\tx_{\omega}})$ \; + \Multi{} $(\hpRS,\red{\hatv,}\bars+1, \hatmT, \textcolor{red}{\tx_{\omega}})$ \; } } } @@ -81,7 +81,8 @@ \vspace{12pt} %%% REQ SN - \On{$(\hpRS,s,\mT_{\mathsf{req}}, \textcolor{red}{\tx_{\omega}})$ from $\party_j$}{ + \On{$(\hpRS,\red{v,}s,\mT_{\mathsf{req}}, \textcolor{red}{\tx_{\omega}})$ from $\party_j$}{ + \red{\Req{$v = \hatv$} \;} \Req{$s = \hats + 1 ~ \land ~ \hpLdr(s) = j$} \; \Wait{$\bars = \hats$}{ \textcolor{red}{\Req{$\barmU \applytx \tx_{\omega} \not= \bot$}} \; @@ -95,7 +96,7 @@ % 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}}))$ \; + $\msSig_i \gets \msSign(\hydraSigningKey, (\cid || \textcolor{red}{v || \hats || \eta' || \eta_{\omega}}))$ \; $\hatSigma \gets \emptyset$ \; $\Multi{}~(\hpAS,\hats,\msSig_i)$ \; $\forall \tx \in \mT_{\mathsf{req}}: \Out~(\hpSeen,\tx)$ \; @@ -122,7 +123,7 @@ $\tx_\omega \gets \tx$ \; % issue snapshot if we are leader \If{$\hats = \bars \land \hpLdr(\bars + 1) = i$}{ - \Multi{} $(\hpRS,\bars+1,\hatmT, \tx_{\omega})$ \; + \Multi{} $(\hpRS,\hatv,\bars+1,\hatmT, \tx_{\omega})$ \; } } } @@ -131,12 +132,16 @@ \vspace{12pt} %%% DECREMENT - \On{$(\mathtt{decrementTx}, U_{\omega})$ from chain}{ - \textcolor{red}{ + \red{\On{$(\mathtt{decrementTx}, U_{\omega}, v)$ from chain}{ \If{$\mathsf{outputs}(\tx_{\omega}) = U_{\omega}$}{ $\tx_{\omega} \gets \bot$ \; + $\hatv \gets v$ \; + % TODO: always snapshot? not strictly needed (to clear pending decommits)? + \If{$\hats = \bars \land \hpLdr(\bars + 1) = i$}{ + \Multi{} $(\hpRS,\hatv,\bars+1,\hatmT, \tx_{\omega})$ \; + } } - } + } } \vspace{12pt} @@ -155,21 +160,21 @@ % TODO: tx_ω undefined (else) case $\textcolor{red}{\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)$ \; + \Req{} $\msVfy(\hydraKeysAgg, (\cid || \red{\hatv ||} \hats || \eta' || \textcolor{red}{\eta_{\omega}}), \msCSig)$ \; $\barmU \gets \hatmU$ \; + $\barv \gets \hatv$ \; $\bars \gets \hats$ \; $\barsigma \gets \msCSig$ \; %$\Out~(\hpSnap,(\bars,\barmU))$ \; $\forall \tx \in \mT_{\mathsf{req}} : \Out (\hpConf,\tx)$ \; \red{\If{$\eta_{\omega} \ne \bot$}{ - $\PostTx{}~(\mathtt{decrementTx}, \hats, \eta', \eta_{\omega})$ \; + $\PostTx{}~(\mtxDecrement, \barv, \bars, \eta', \eta_{\omega})$ \; }} % issue snapshot if we are leader - \If{$\hpLdr(s+1) = i \land (\hatmT \neq \emptyset \lor \tx_{\omega} \ne \bot)$}{ - \Multi{} $(\hpRS,s+1, \hatmT, \textcolor{red}{\tx_{\omega}})$ \; + \If{$\hpLdr(s+1) = i \land \hatmT \neq \emptyset$}{ + \Multi{} $(\hpRS,\red{\hatv,}\bars+1, \hatmT, \textcolor{red}{\tx_{\omega}})$ \; } } } @@ -190,7 +195,7 @@ \On{$(\hpClose)$ from client}{ $\eta' \gets \combine(\barmU)$ \; $\xi \gets \barsigma$ \; - $\PostTx{}~(\mtxClose, \bars, \eta', \xi)$ \; + $\PostTx{}~(\mtxClose, \red{\bar{v},} \bars, \eta', \red{\eta_{\omega},} \xi)$ \; } \end{walgo} } @@ -201,7 +206,7 @@ \If{$\bars > s_{c}$}{ $\eta' \gets \combine(\barmU)$ \; $\xi \gets \barsigma$ \; - $\PostTx{}~(\mtxContest, \bars, \eta', \xi)$ \; + $\PostTx{}~(\mtxContest, \red{\bar{v},} \bars, \eta', \red{\eta_{\omega},} \xi)$ \; } } \end{walgo} diff --git a/spec/macros.tex b/spec/macros.tex index f4a4d38a75a..44143dbb49b 100644 --- a/spec/macros.tex +++ b/spec/macros.tex @@ -379,6 +379,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}} @@ -390,7 +392,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}} diff --git a/spec/offchain.tex b/spec/offchain.tex index 12202363d98..13d7b013cb0 100644 --- a/spec/offchain.tex +++ b/spec/offchain.tex @@ -108,6 +108,9 @@ \subsection{Variables} party's local state consists of the following variables: \todo{update} \begin{itemize} + \item \red{$\hatv$: Last seen open state version.} + % FIXME: refactor to have a snapshot holding confirmed things + \item \red{$\barv$: State version referred by latest confirmed snapshot.} \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. @@ -119,11 +122,10 @@ \subsection{Variables} applying $\hatmT$ to $\barmU$ 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). - \red{\item $\tx_{\omega} \in \mathcal{T}^{?}$: Decommit transaction, whose outputs are to be decommitted from the head. Maybe be $\bot$ if nothing to decommit.} + \item \red{$\tx_{\omega} \in \mathcal{T}^{?}$: Decommit transaction, whose outputs are to be decommitted from the head. Maybe be $\bot$ if nothing to decommit.} \end{itemize} \subsection{Protocol flow} -\todo{\red{Make consistent with figure again}} \subsubsection{Initializing the head} @@ -151,10 +153,10 @@ \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$. +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 +seen transaction set is initialized empty $\hatmT =\emptyset$, \red{head state version +$\hatv = 0$}, as well as snapshot numbers $\bars = \hats = 0$. % REVIEW: check $\eta$ against $\Uinit$? \subsubsection{Processing transactions off-chain} @@ -182,22 +184,28 @@ \subsubsection{Processing transactions off-chain} no decommit in flight and party is the leader then $\hpRS$ is emmitted containing the decommit transaction $\tx_{\omega}$.} \\ +\red{\dparagraph{$\mathtt{collectComTx}$.}\quad Upon observing the \mtxDecrement{} + transaction, which removed outputs $U_{\omega}$ from the head, the corresponding + decommit transaction is cleared and the observed version is used for future + snapshots by + setting $\hatv = v$. This is required as that the version of the open head state is incremented on each \mtxDecrement{} transaction as described in Section~\ref{sec:decrement-tx}} \\ + \dparagraph{$\hpRS$.}\quad Upon receiving request -$(\hpRS,s,\mT_{\mathsf{req}}, \tx_{\omega})$\footnote{Snapshot requests with only - transaction identifiers are possible too if all parties keep an index of +$(\hpRS,\red{v,}s,\mT_{\mathsf{req}}, \tx_{\omega})$\footnote{Snapshot requests with + only transaction identifiers are possible too if all parties keep an index of previously seen transactions and their identifiers.} from party $\party_j$, -the receiver $\party_i$ checks that $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$). \red{If the decommit transaction $\tx_{\omega}$ is not $\bot$, the - transaction is $\Req$d to be applicable to the last confirmed UTxO set - $\barmU$ and spent outputs must be removed, yielding the still active UTxO set - $\barmU_{\mathsf{active}}$. Then, all requested transactions - $\mT_{\mathsf{req}}$ are $\Req$d to be applicable to - $\barmU_{\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 $\hatmU$ of the new -local snapshot as +the receiver $\party_i$ checks that \red{$v$ refers to the current open state + version}\todo{wait or require?}, $s$ is the next snapshot number 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$). \red{If + the decommit transaction $\tx_{\omega}$ is not $\bot$, the transaction is $\Req$d to + be applicable to the last confirmed UTxO set $\barmU$ and spent outputs must + be removed, yielding the still active UTxO set $\barmU_{\mathsf{active}}$. + Then, all requested transactions $\mT_{\mathsf{req}}$ are $\Req$d to be + applicable to $\barmU_{\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 +$\hatmU$ of the new local snapshot as $\hatmU \gets \red{\barmU_{\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 @@ -215,12 +223,16 @@ \subsubsection{Processing transactions off-chain} $\hats = s$ and $\Req$ that the signature is not yet included in $\hatSigma$. They store the received signature in the signature accumulator $\hatSigma$, and if the signature from each party has been collected, $\party_i$ aggregates the -multisignature $\msCSig$ and $\Req$ it to be valid \red{(using the same message as in -$\hpRS$)}. If everything is fine, the snapshot can be considered 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 \red{(using the same message + as in $\hpRS$)}. 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. \red{In + case there is a pending decommit, any participant can now submit a + \mtxDecrement{} transaction by providing the just confirmed snapshot and 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} @@ -244,9 +256,6 @@ \subsubsection{Closing the head} Section~\ref{sec:contest-tx}). \subsection{Rollbacks and protocol changes}\label{sec:rollbacks} -% FIXME: mention \eta_0 / referencing or versioning -\todo{Describe $\eta_0$ / referencing or versioning} - 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 @@ -301,7 +310,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{fig_offchain_prot} diff --git a/spec/prel.tex b/spec/prel.tex index 8f9609b19b3..9602d3f822a 100644 --- a/spec/prel.tex +++ b/spec/prel.tex @@ -175,7 +175,7 @@ \subsubsection{Scripts} \end{definition} \subsubsection{Transactions} -\todo{actual transactions \mathcal{T} are not defined} +\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.