Spec: re-order pseudocode blocks

input-output-hk · May 7, 2024 · 417d459 · 417d459
1 parent de0f9a4
commit 417d459
Showing 1 changed file with 37 additions and 37 deletions.
diff --git a/spec/fig_offchain_prot.tex b/spec/fig_offchain_prot.tex
@@ -88,6 +88,43 @@
 
 						\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}))}$ \;
+								% 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}}))$ \;
+								$\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$ \;
+								$X\gets\hatmT$ \;
+								$\hatmT\gets\emptyset$ \;
+								\For{$\tx\in X : \hatmL\applytx \tx \not=\bot$}{
+									$\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$}}{
@@ -123,43 +160,6 @@
 							}
 							}
 						}
-					\end{walgo}
-				} &
-
-				\adjustbox{valign=t,scale=\sfact}{
-					\begin{walgo}{0.7}
-						%%% 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}))}$ \;
-								% 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}}))$ \;
-								$\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$ \;
-								$X\gets\hatmT$ \;
-								$\hatmT\gets\emptyset$ \;
-								\For{$\tx\in X : \hatmL\applytx \tx \not=\bot$}{
-									$\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}} \}$ \;
-							}
-						}
 
 						\vspace{12pt}