Skip to content

Commit

Permalink
WIP: Add version to off-chain code
Browse files Browse the repository at this point in the history
  • Loading branch information
@ch1bo
ch1bo committed Jun 19, 2024
1 parent 0f97ad8 commit f71eae5
Show file tree
Hide file tree
Showing 4 changed files with 67 additions and 48 deletions.
37 changes: 21 additions & 16 deletions spec/fig_offchain_prot.tex
View file
Original file line number Diff line number Diff line change
Expand Up @@ -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}
Expand All @@ -73,15 +73,16 @@
$\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}})$ \;
}
}
}

\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$}} \;
Expand All @@ -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)$ \;
Expand All @@ -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})$ \;
}
}
}
Expand All @@ -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}
Expand All @@ -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}})$ \;
}
}
}
Expand All @@ -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}
}
Expand All @@ -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}
Expand Down
3 changes: 2 additions & 1 deletion spec/macros.tex
View file
Original file line number Diff line number Diff line change
Expand Up @@ -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}}
Expand All @@ -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}}
Expand Down
73 changes: 43 additions & 30 deletions spec/offchain.tex
View file
Original file line number Diff line number Diff line change
Expand Up @@ -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.
Expand All @@ -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}

Expand Down Expand Up @@ -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}
Expand Down Expand Up @@ -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
Expand All @@ -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}

Expand All @@ -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
Expand Down Expand Up @@ -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}

Expand Down
2 changes: 1 addition & 1 deletion spec/prel.tex
View file
Original file line number Diff line number Diff line change
Expand Up @@ -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.
Expand Down

0 comments on commit f71eae5

Please sign in to comment.