Update offchain flow for ackSn

spec/fig_offchain_prot.tex

@@ -227,13 +227,7 @@
 									% TODO: DRY message creation
 									$\eta \gets \combine(\hatmU)$ \;
 
-									\red{
-										\eIf{$\psi \not= \bot ~ \land ~ \psi \in \tx_\omega$}{
-											$\eta_\omega \gets \tx_\omega$ \;
-										}{
-											$\eta_\omega \gets U_\omega$ \;
-										}
-									}
+									\red{$\eta_\omega \gets \psi$} \;
 
 									\Req{} $\msVfy(\hydraKeysAgg, (\cid || \red{\hatv ||} \hats || \eta \red{|| \eta_\omega}), \msCSig)$ \;
 									% create confirmed snapshot for later reference
@@ -244,11 +238,11 @@
 
 									\red{
 										\If{$\psi \not= \bot ~ \land ~ \psi \in \tx_\omega$}{
-											$\PostTx{}~(\mtxDecrement, \hatv, \hats, \eta, \eta_\omega)$ \;
+											$\PostTx{}~(\mathtt{decrementTx}, \hatv, \hats, \eta, \eta_\omega)$ \;
 											$\Out (\hpConf,\psi)$ \;
 										}
 										\If{$\psi \not= \bot ~ \land ~ \psi \in U_\omega$}{
-											$\PostTx{}~(\mtxIncrement, \hatv, \hats, \eta, \eta_\omega)$ \;
+											$\PostTx{}~(\mathtt{incrementTx}, \hatv, \hats, \eta, \eta_\omega)$ \;
 											$\Out (\hpConf,\psi)$ \;
 										}
 									}

spec/offchain.tex

@@ -263,22 +263,29 @@ \subsubsection{Processing transactions off-chain}
   requested snapshot's UTxO set iteratively and
   ultimately yielding a ``pruned'' version of $\hatmT$ and $\hatmL$. \\
 
-\dparagraph{$\hpAS$.}\quad Upon receiving acknowledgment $(\hpAS,s,\msSig_j)$, all
+\dparagraph{$\hpAS$.}\quad Upon receiving acknowledgment $(\hpAS,s,\msSig_j,\red{\psi})$, all
 participants $\Req$ that it is from an expected snapshot (either the last seen
 $\hats$ or + 1), potentially $\KwWait$ for the corresponding $\hpRS$ such that
 $\hats = s$ and $\Req$ that the signature is not yet included in $\hatSigma$.
 They store the received signature in the signature accumulator $\hatSigma$, and
 if the signature from each party has been collected, $\party_i$ aggregates the
 multisignature $\msCSig$ and $\Req$ it to be valid \red{(using the same message
-	as in $\hpRS$)}. If everything is fine, the snapshot can be considered
-confirmed by creating the snapshot object
-$\bar{\mc S} \gets \Sno(\hatv, \hats, \hatmU, \hatmT \red{, \tx_\omega})$ and storing
-the multi-signature $\msCSig$ in it for later reference. \red{In case there is a pending
-	decommit, any participant can now submit a \mtxDecrement{} transaction by
-	providing the just confirmed snapshot with its digests of the active UTxO set
-	$\eta$ and the to be removed UTxO set $\eta_\omega$.} Similar to the $\hpRT$, if
-$\party_i$ is the next snapshot leader and there are already transactions to
-snapshot in $\hatmT$, a corresponding $\hpRS$ is distributed.
+as in $\hpRS$)}. If everything is fine, the snapshot can be considered confirmed by creating 
+the snapshot object $\bar{\mc S} \gets \Sno(\hatv, \hats, \hatmU, \hatmT \red{, \eta_\omega})$ 
+and storing the multi-signature $\msCSig$ in it for later reference. \red{Then, in case:
+\begin{itemize}
+\item
+	there is a pending decrement any participant can now submit a $\mathtt{decrementTx}$
+	by providing the confirmed snapshot with its digests of the active UTxO set
+	$\eta$ and the UTxO set to be removed $\eta_\omega$.
+\item
+	there is a pending increment any participant can now submit an $\mathtt{incrementTx}$
+	by providing the confirmed snapshot with its digests of the active UTxO set
+	$\eta$ and the UTxO set to be added $\eta_\omega$.
+\end{itemize}
+}
+Similar to the $\hpRT$, if $\party_i$ is the next snapshot leader and there are
+already transactions to snapshot in $\hatmT$, a corresponding $\hpRS$ is distributed.
 
 \subsubsection{Closing the head}