Skip to content

Commit

Permalink
Incremental decommit spec (#1479)
Browse files Browse the repository at this point in the history 
Only specification changes for #1057 to get them merged first as
described in #1473.

:nail_care: Marked sections red that are about to change with
incremental decommits.

:nail_care: Adds `decrementTx` which removes UTxO from the head state to
protocol overview, on-chain and off-chain sections.

:nail_care: Updates close, contest and fanout steps accordingly.

:nail_care: Uses a "version counting" scheme to distinguish cases where
the same snapshot is used to decrement and close the head.

:nail_care: Removes $\mathcal{T}_{\mathsf{all}}$ book-keeping and makes
snapshots request full transactions. Adds a note that requesting only
transaction ids is possible if all parties keep an index. This
simplifies the specification (but departs from a 1:1 mapping to
implemented protocol logic in `Hydra.HeadLogic`)

:nail_care: (Re-)introduces snapshot objects to group confirmed
variables (e.g. $\bar{s}, \bar{v}$) which are just kept to refer to them
later on in `close`.

---

<!-- Consider each and tick it off one way or the other -->
* [ ] CHANGELOG updated or not needed
* [x] Documentation updated
* [x] Haddocks not needed
* [ ] No new TODOs introduced or explained herafter
   - [x] ~~Figures are not updated~~
- [ ] Some handwavy-ness when dealing with $tx_\omega$ and interface
between off-chain and on-chain in regards with $\mathsf{CloseType}$ is
unsharp

---------

Co-authored-by: Sasha Bogicevic <sasha.bogicevic@iohk.io>
  • Loading branch information
@ch1bo @v0d1ch
ch1bo and v0d1ch committed Jul 1, 2024
1 parent ff72844 commit 7a871c1
Show file tree
Hide file tree
Showing 11 changed files with 529 additions and 288 deletions.
3 changes: 2 additions & 1 deletion spec/fig_SM_states_basic.tex
View file
Original file line number Diff line number Diff line change
Expand Up @@ -9,9 +9,10 @@

\path[->] (initial) edge [bend left=20] node {$\stCollect$} (open);
\path[->] (open) edge [bend left=20] node {$\stClose$} (closed);
\path[->] (open) edge [loop below] node {\red{$\mathsf{decrement}$}} (open);
\path[->] (closed) edge [bend left=20] node {$\stFanout$} (final);
\path[->] (closed) edge [loop above] node {$\stContest$} (closed);
\path[->] (initial) edge node {$\stAbort$} (final);
\path[->] (initial) edge [bend right=20] node {$\stAbort$} (final);
\end{tikzpicture}

\caption{Mainchain state diagram for this version of the Hydra protocol.}\label{fig:SM_states_basic}
Expand Down
127 changes: 83 additions & 44 deletions spec/fig_offchain_prot.tex
View file
Original file line number Diff line number Diff line change
Expand Up @@ -35,7 +35,7 @@
$C_j \gets U $

\If{$\forall k \in [1..n]: C_k \neq \undefined$}{
$\eta \gets (0, \combine([C_1 \dots C_n]))$ \;
$\eta \gets \combine([C_1 \dots C_n])$ \;
$\PostTx{}~(\mtxCCom, \eta)$ \;
}
}
Expand All @@ -46,9 +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$ \;
$\hats,\bars \gets 0$ \;
$\mT, \hatmT, \barmT \gets \emptyset$ \;
$\hatmL \gets \Uinit$ \;
\red{$\bar{\mc S} \gets \Sno(0, 0, \Uinit, \emptyset, \bot)$ \;}
\red{$\hatv, \hats \gets 0$ \;}
$\hatmT \gets \emptyset$ \;
\red{$\tx_{\omega} \gets \bot$ \;}
}

\end{walgo}
Expand All @@ -64,79 +66,115 @@
\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$}{
\Multi{} $(\hpRS,\bars+1,\hatmT)$ \;
\If{$\hats = \bar{\mc S}.s \land \hpLdr(\bar{\mc S}.s + 1) = i$}{
\Multi{} $(\hpRS,\red{\hatv,}\bar{\mc S}.s+1, \hatmT, \red{\tx_{\omega}})$ \;
}
}
}

\vspace{12pt}

%%% REQ SN
\On{$(\hpRS,s,\mT^{\#}_{req})$ 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} \}$ \;
\Req{$\barmU \applytx \mT_{\mathsf{req}} \not= \bot$} \;
$\hatmU \gets \barmU \applytx \mT_{\mathsf{req}}$ \;
$\hats \gets \bars + 1$ \;
$\eta' \gets (\hats, \combine(\hatmU))$ \;
\On{$(\hpRS,\red{v,}s,\mT_{\mathsf{req}}, \red{\tx_{\omega}})$ from $\party_j$}{
\Req{$\red{v = \hatv ~ \land} ~ s = \hats + 1 ~ \land ~ \hpLdr(s) = j$} \;
\Wait{$\hats = \bar{\mc S}.s$}{
\red{\Req{$\bar{\mc S}.U \applytx \tx_{\omega} \not= \bot$}} \;
\red{$U_{\mathsf{active}} \gets \bar{\mc S}.U \applytx \tx_{\omega}$} \;
\Req{$\red{U_{\mathsf{active}}} \applytx \mT_{\mathsf{req}} \not= \bot$} \;
$U \gets \red{U_{\mathsf{active}}} \applytx \mT_{\mathsf{req}}$ \;
% XXX: why +1? ̂s ← s would be clearer here
$\hats \gets \bar{\mc S}.s + 1$ \;
% TODO: DRY message creation
$\eta \gets \combine(U)$ \;
% TODO: handwavy combine/outputs here
$\red{\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'
$\msSig_i \gets \msSign(\hydraSigningKey, (\textcolor{red}{\cid || \eta_{0} ||} \eta'))$ \;
% a merkle tree root to the (signed) snapshot data \eta
$\msSig_i \gets \msSign(\hydraSigningKey, (\cid || \red{v ||} \hats || \eta \red{|| \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}
} &

\adjustbox{valign=t,scale=\sfact}{
\begin{walgo}{0.6}
\begin{walgo}{0.7}
%%% REC DEC
\red{\On{$(\mathtt{reqDec},\tx)$ from $\party_j$}{
\Wait{$\tx_\omega = \bot ~ \land ~ \hatmL \applytx \tx \not= \bot$}{
$\hatmL \gets \hatmL \setminus \mathsf{inputs}(\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})$ \;
}
}
}
}

\vspace{12pt}

%%% DECREMENT
\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 = \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}

%%% 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)$ \;

$\eta' \gets (\hats, \combine(\hatmU))$ \;
\Req{} $\msVfy(\hydraKeysAgg, (\textcolor{red}{\cid || \eta_{0} ||} \eta'), \msCSig)$ \;
$\barmU \gets \hatmU$ \;
$\bars \gets \hats$ \;
$\barsigma \gets \msCSig$ \;
%$\Out~(\hpSnap,(\bars,\barmU))$ \;
% TODO: DRY message creation
$\eta \gets \combine(\hatmU)$ \;
% TODO: tx_ω undefined (else) case
$\red{\eta_{\omega} \gets \combine(\mathsf{outputs}(\tx_{\omega}))}$ \;

\Req{} $\msVfy(\hydraKeysAgg, (\cid || \red{\hatv ||} \hats || \eta \red{|| \eta_{\omega}}), \msCSig)$ \;
% create confirmed snapshot for later reference
$\bar{\mc S} \gets \Sno(\hatv, \hats, \hatmU, \hatmT \red{, \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)$ \;
\red{\If{$\tx_{\omega} \ne \bot$}{
$\PostTx{}~(\mtxDecrement, \hatv, \hats, \eta, \eta_{\omega})$ \;
\red{$\Out (\hpConf,\tx_{\omega})$ \;}
}}
% issue snapshot if we are leader
\If{$\hpLdr(s+1) = i \land \hatmT \neq \emptyset$}{
\Multi{} $(\hpRS,s+1,\hatmT)$ \;
\Multi{} $(\hpRS,\red{\hatv},\bar{\mc S}.s+1, \hatmT, \red{\tx_{\omega}})$ \;
}
}
}
Expand All @@ -155,21 +193,22 @@
\begin{walgo}{0.6}
% CLOSE from client
\On{$(\hpClose)$ from client}{
$\eta' \gets (\bars, \combine(\barmU))$ \;
$\xi \gets \barsigma$ \;
$\PostTx{}~(\mtxClose, \eta', \xi)$ \;
$\eta \gets \combine(\bar{\mc S}.U)$ \;
\red{$\eta_\omega \gets \combine(\mathsf{outputs}(\bar{\mc S}.\tx_\omega))$ \;}
$\xi \gets \bar{\mc S}.\sigma$ \;
$\PostTx{}~(\mtxClose, \red{\bar{\mc S}.v}, \bar{\mc S}.s, \eta, \red{\eta_{\omega},} \xi)$ \;
}
\end{walgo}
}
&
\adjustbox{valign=t,scale=\sfact}{
\begin{walgo}{0.6}
\On{$(\gcChainClose, \eta) \lor (\gcChainContest, \eta)$ from chain}{
$(s_{c}, \cdot) \gets \eta$ \;
\If{$\bars > s_{c}$}{
$\eta' \gets (\bars, \combine(\barmU))$ \;
$\xi \gets \barsigma$ \;
$\PostTx{}~(\mtxContest, \eta', \xi)$ \;
\On{$(\gcChainClose, \eta) \lor (\gcChainContest, s_{c}, \eta)$ from chain}{
\If{$\bar{\mc S}.s > s_{c}$}{
$\eta \gets \combine(\bar{\mc S}.U)$ \;
\red{$\eta_\omega \gets \combine(\mathsf{outputs}(\bar{\mc S}.\tx_\omega))$ \;}
$\xi \gets \bar{\mc S}.\sigma$ \;
$\PostTx{}~(\mtxContest, \red{\bar{\mc S}.v}, \bar{\mc S}.s, \eta, \red{\eta_{\omega},} \xi)$ \;
}
}
\end{walgo}
Expand Down
Binary file modified spec/figures/SM-close.pdf
View file
Binary file not shown.
Binary file modified spec/figures/closeTx.pdf
View file
Binary file not shown.
Binary file modified spec/figures/contestTx.pdf
View file
Binary file not shown.
Binary file added spec/figures/decrementTx.pdf
View file
Binary file not shown.
9 changes: 7 additions & 2 deletions spec/macros.tex
View file
Original file line number Diff line number Diff line change
Expand Up @@ -26,6 +26,9 @@

\newcommand{\ignore}[1]{}

\newcommand{\red}[1]{\textcolor{red}{#1}}
\newcommand{\blue}[1]{\textcolor{blue}{#1}}

\newcommand{\TODO}[1]{
\if\relax\detokenize{#1}\relax
\textcolor{red}{TODO}
Expand Down Expand Up @@ -239,7 +242,6 @@
\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}}
Expand Down Expand Up @@ -317,6 +319,7 @@
\newcommand{\hpSeen}{\mathtt{seen}}
\newcommand{\hpConf}{\mathtt{conf}}
\newcommand{\hpSnap}{\mathtt{snap}}
\newcommand{\hpDecommit}{\mathtt{decommit}}
\newcommand{\hpClose}{\mathtt{close}}
\newcommand{\hpCont}{\mathtt{cont}}
\newcommand{\hpFO}{\mathtt{fanOut}}
Expand Down Expand Up @@ -376,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 @@ -387,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 All @@ -413,6 +417,7 @@

\newcommand{\hpNS}{\mathtt{newSn}}
\newcommand{\hpRS}{\mathtt{reqSn}}
\newcommand{\hpRD}{\mathtt{reqDec}}
\newcommand{\hpAS}{\mathtt{ackSn}}
\newcommand{\hpCS}{\mathtt{confSn}}

Expand Down
Loading

0 comments on commit 7a871c1

Please sign in to comment.