Draft off-chain protocol changes for incremental decommit

This is breaking the figure formatting, but good enough for a first draft.

spec/fig_offchain_prot.tex

@@ -47,6 +47,7 @@
 							$\Uinit \gets \bigcup_{j=1}^{n} U_j$ \;
 							% $\Out~(\hpSnap,(0,U_0))$ \;
 							$\hatmU, \barmU, \hatmL \gets \Uinit$ \;
+							\textcolor{red}{$\mathcal{U}_{\omega} \gets \bot$ \;}
 							$\hats,\bars \gets 0$ \;
 							$\mT, \hatmT, \barmT \gets \emptyset$ \;
 						}
@@ -79,25 +80,67 @@
 								$\hatmT \gets \hatmT \cup \{\tx\}$ \;
 								% issue snapshot if we are leader
 								\If{$\hats = \bars \land \hpLdr(\bars + 1) = i$}{
-									\Multi{} $(\hpRS,\bars+1,\hatmT)$ \;
+									\Multi{} $(\hpRS,\bars+1,\hatmT, \textcolor{red}{\mathcal{U}_{\omega}})$ \;
 								}
 							}
 						}
 
 						\vspace{12pt}
 
+						%%% DECOMMIT
+						\On{$(\mathtt{decommit},\tx)$ from client}{
+						    \textcolor{red}{
+							\Req{$\barmU \applytx \tx \not= \bot$} \;
+							\Multi{} $(\mathtt{reqDec},\tx)$%
+							}
+						}
+
+						\vspace{12pt}
+
+						%%% REC DEC
+						\On{$(\mathtt{reqDec},\tx)$ from $\party_j$}{
+						    \textcolor{red}{
+							\Wait{$\mathcal{U}_\omega = \bot ~ \land ~ \barmU \applytx \tx \not= \bot$}{
+								$\mathcal{U}_\omega \gets \barmU \applytx \tx$ \;
+								% issue snapshot if we are leader
+								\If{$\hats = \bars \land \hpLdr(\bars + 1) = i$}{
+									\Multi{} $(\hpRS,\bars+1,\hatmT, \mathcal{U}_{\omega})$ \;
+								}
+							}
+							}
+						}
+
+						\vspace{12pt}
+
+						%%% DECREMENT
+						\On{$(\mathtt{decrementTx}, U_{\omega}, \eta_{\omega})$ from chain}{
+						    \textcolor{red}{
+							\If{$\mathcal{U}_{\omega} = U_{\omega}$}{
+								$\mathcal{U}_{\omega} \gets \bot$ \;
+							}
+							}
+						}
+					\end{walgo}
+				} &
+
+				\adjustbox{valign=t,scale=\sfact}{
+					\begin{walgo}{0.7}
 						%%% REQ SN
-						\On{$(\hpRS,s,\mT^{\#}_{req})$ from $\party_j$}{
+						\On{$(\hpRS,s,\mT^{\#}_{req}, \textcolor{red}{\mathcal{U}_{\omega}})$ from $\party_j$}{
 							\Req{$s = \hats + 1 ~ \land ~ \hpLdr(s) = j$} \;
+							\textcolor{red}{\Req{$\barmU \supseteq \mathcal{U}_{\omega}$}} \;
 							\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}}$ \;
+								\textcolor{red}{$\barmU_{\mathsf{active}} \gets \barmU \setminus \mathcal{U}_{\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$ \;
+                                % TODO: eta without snapshot number
 								$\eta' \gets (\hats, \combine(\hatmU))$ \;
+								$\textcolor{red}{\eta_{\omega} \gets \combine(\mathcal{U}_{\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'))$ \;
+								$\msSig_i \gets \msSign(\hydraSigningKey, (\cid || \textcolor{red}{\eta_{0} ||} \eta' || \textcolor{red}{\eta_{\omega}}))$ \;
 								$\hatSigma \gets \emptyset$ \;
 								$\Multi{}~(\hpAS,\hats,\msSig_i)$ \;
 								$\forall \tx \in \mT_{\mathsf{req}}: \Out~(\hpSeen,\tx)$ \;
@@ -113,11 +156,9 @@
 								$\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}
+						\vspace{12pt}
+
 						%%% ACK SN
 						\On{$(\hpAS,s,\msSig_j)$ from $\party_j$}{
 							\Req{} $s \in \{\hats,\hats+1\}$ \;
@@ -128,15 +169,24 @@
 									$\msCSig \gets \msComb(\hydraKeys^{setup}, \hatSigma)$ \;
 
 									$\eta' \gets (\hats, \combine(\hatmU))$ \;
-									\Req{} $\msVfy(\hydraKeysAgg, (\textcolor{red}{\cid || \eta_{0} ||} \eta'), \msCSig)$ \;
+									% TODO: U_ω undefined (else) case
+								    $\textcolor{red}{\eta_{\omega} \gets \combine(\mathcal{U}_{\omega})}$ \;
+
+									% TODO: \eta_0 signing still needed?
+									\Req{} $\msVfy(\hydraKeysAgg, (\cid || \textcolor{red}{\eta_{0} ||} \eta' || \textcolor{red}{\eta_{\omega}}), \msCSig)$ \;
+
+									$\textcolor{red}{\PostTx{}~(\mathtt{decrementTx}, \eta', \eta_{\omega})}$ \;
+
 									$\barmU \gets \hatmU$ \;
 									$\bars \gets \hats$ \;
 									$\barsigma \gets \msCSig$ \;
 									%$\Out~(\hpSnap,(\bars,\barmU))$ \;
 									$\forall \tx \in \mT_{\mathsf{req}} : \Out (\hpConf,\tx)$ \;
+
 									% issue snapshot if we are leader
 									\If{$\hpLdr(s+1) = i \land \hatmT \neq \emptyset$}{
-										\Multi{} $(\hpRS,s+1,\hatmT)$ \;
+									    % TODO: wasteful as we re-request U_ω?
+										\Multi{} $(\hpRS,s+1,\hatmT, \textcolor{red}{\mathcal{U}_{\omega}})$ \;
 									}
 								}
 							}