Move AckSn and Close to next page

cardano-scaling · Jul 16, 2024 · b674350 · b674350
1 parent 2960d42
commit b674350
Showing 1 changed file with 58 additions and 53 deletions.
diff --git a/spec/fig_offchain_prot.tex b/spec/fig_offchain_prot.tex
@@ -172,56 +172,72 @@
 							}
 						}
 
-						\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)$ \;
-
-									% TODO: DRY message creation
-									$\eta \gets \combine(\hatmU)$ \;
-
-                  \eIf{\red{$\tx_{\omega} \not= \bot$}}{
-									  % TODO: tx_ω undefined (else) case
-								    $\red{\eta_{\omega} \gets \combine(\mathsf{outputs}(\tx_{\omega}))}$ \;
-                  }{
-								    $\red{\eta_{\omega} \gets \combine(\bigcup_{\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)$ \;
-                  \If{\red{$\tx_{\omega} \ne \bot \lor \bigcup_{omega} \ne \bot$}}{
-                    $\PostTx{}~(\mtxDecrement, \hatv, \hats, \eta, \red{\eta_{\omega}})$ \;
-                    \red{$\Out (\hpConf,\tx_{\omega} \lor \bigcup_{\omega})$ \;}
-									}
-									% issue snapshot if we are leader
-									\If{$\hpLdr(s+1) = i \land \hatmT \neq \emptyset$}{
-                    \Multi{} $(\hpRS,\red{\hatv},\bar{\mc S}.s+1, \hatmT, \red{\tx_{\omega}, \bigcup_{\omega}})$ \;
-									}
-								}
-							}
-						}
 					\end{walgo}
 				}
 			\end{tabular}
 
+
+		\end{tabular}
+	\end{algobox}
+
+\end{figure*}
+\clearpage
+\begin{figure*}[t!]
+
+	\def\sfact{0.8}
+		\begin{tabular}{c}
+
 			\\
 			\multicolumn{1}{l}{\line(1,0){490}}
 			\\
 
-			%%% Closing the head
+
+
 			\begin{tabular}{c c}
+				\adjustbox{valign=t,scale=\sfact}{
+					\begin{walgo}{0.6}
+			 %%% 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)$ \;
+
+			  				% TODO: DRY message creation
+			  				$\eta \gets \combine(\hatmU)$ \;
+
+                \eIf{\red{$\tx_{\omega} \not= \bot$}}{
+			  				  % TODO: tx_ω undefined (else) case
+			  			    $\red{\eta_{\omega} \gets \combine(\mathsf{outputs}(\tx_{\omega}))}$ \;
+                }{
+			  			    $\red{\eta_{\omega} \gets \combine(\bigcup_{\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)$ \;
+                \If{\red{$\tx_{\omega} \ne \bot \lor \bigcup_{omega} \ne \bot$}}{
+                  $\PostTx{}~(\mtxDecrement, \hatv, \hats, \eta, \red{\eta_{\omega}})$ \;
+                  \red{$\Out (\hpConf,\tx_{\omega} \lor \bigcup_{\omega})$ \;}
+			  				}
+			  				% issue snapshot if we are leader
+			  				\If{$\hpLdr(s+1) = i \land \hatmT \neq \emptyset$}{
+                  \Multi{} $(\hpRS,\red{\hatv},\bar{\mc S}.s+1, \hatmT, \red{\tx_{\omega}, \bigcup_{\omega}})$ \;
+			  				}
+			  			}
+			  		}
+			  	}
+
+					\end{walgo}
+				}
+			%%% Closing the head
 				\adjustbox{valign=t,scale=\sfact}{
 					\begin{walgo}{0.6}
 						% CLOSE from client
@@ -231,11 +247,7 @@
 							$\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}
+			    	\vspace{12pt}
 						\On{$(\gcChainClose, \eta) \lor (\gcChainContest, s_{c}, \eta)$ from chain}{
 							\If{$\bar{\mc S}.s > s_{c}$}{
 							  $\eta \gets \combine(\bar{\mc S}.U)$ \;
@@ -248,16 +260,9 @@
 				}
 			\end{tabular}
 		\end{tabular}
-		\bigskip
-	\end{algobox}
-
 	\caption{Head-protocol machine for the \emph{coordinated head} from the perspective of party $\party_i$.}\label{fig:off-chain-prot}
-
-
 \end{figure*}
 
-
-
 %%% Local Variables:
 %%% mode: latex
 %%% TeX-master: "main"