Incremental decommit spec

spec/fig_SM_states_basic.tex

@@ -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}

spec/fig_offchain_prot.tex

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

spec/macros.tex

@@ -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}
@@ -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}}
@@ -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}}
@@ -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}}
@@ -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}}
@@ -413,6 +417,7 @@
 
 \newcommand{\hpNS}{\mathtt{newSn}}
 \newcommand{\hpRS}{\mathtt{reqSn}}
+\newcommand{\hpRD}{\mathtt{reqDec}}
 \newcommand{\hpAS}{\mathtt{ackSn}}
 \newcommand{\hpCS}{\mathtt{confSn}}