Skip to content

Commit

Permalink
Recopy over master from hydra repo
Browse files Browse the repository at this point in the history
  • Loading branch information
@locallycompact
locallycompact committed Jul 31, 2024
1 parent 0f0a88a commit 035baae
Show file tree
Hide file tree
Showing 6 changed files with 350 additions and 327 deletions.
133 changes: 59 additions & 74 deletions hydra-protocol/Hydra/Protocol/Figures/fig_offchain_prot.tex
View file
Original file line number Diff line number Diff line change
Expand Up @@ -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)$ \;
}
Expand All @@ -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}
Expand All @@ -65,97 +66,74 @@
\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})$ \;
}
}
}

\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}
} &

\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$ \;
}
}

Expand All @@ -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})$ \;
}
}
}
Expand All @@ -208,20 +189,24 @@
\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}
}
&
\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}
Expand Down
12 changes: 10 additions & 2 deletions hydra-protocol/Hydra/Protocol/Macros.tex
View file
Original file line number Diff line number Diff line change
Expand Up @@ -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}
Expand All @@ -36,6 +41,8 @@
\newtheorem{construction}{Construction}

% === General ===
\newcommand{\mc}{\mathcal}

\newcommand{\ith}[1]{#1^{\text{th}}}

\newcommand{\nop}{n}
Expand Down Expand Up @@ -256,6 +263,7 @@
\newcommand{\hpClose}{\mathtt{close}}
\newcommand{\hpCont}{\mathtt{cont}}
\newcommand{\hpFO}{\mathtt{fanOut}}
\newcommand{\hpRD}{\mathtt{reqDec}}


% == Variables ==
Expand Down Expand Up @@ -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}}
Expand All @@ -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}}
Expand All @@ -317,7 +326,6 @@

\newcommand{\txo}{\mathsf{tx}}


% == Commands ==

\newcommand{\hpRG}{\mathtt{req}}
Expand Down
Loading

0 comments on commit 035baae

Please sign in to comment.