Reuse ηω for both increment and decrement

As we dont want to maintain both in flight at the same time.
For this reason, we removed ηα and adapted the onchain spec accordingly.

spec/onchain.tex

@@ -331,11 +331,11 @@ \subsection{\red{Increment Transaction}}\label{sec:increment-tx}
 
 \noindent The state-machine validator $\nuHead$ is spent with
 $\redeemerHead = (\mathsf{increment}, \xi)$, where $\xi$ is a multi-signature of
-the increment snapshot which authorizes addition of some UTxO $U_\alpha$. The
+the increment snapshot which authorizes addition of some UTxO $U_\omega$. The
 validator checks:
 \begin{menumerate}
 	\item State is advanced from $\datumHead \sim \stOpen$ to
-	$\datumHead' \sim \stOpen$, parameters $\cid,\hydraKeysAgg,\nop,\cPer,v$
+	$\datumHead' \sim \stOpen$, parameters $\cid,\hydraKeysAgg,\nop,\cPer$
 	stay unchanged and the new state is governed again by $\nuHead$:
 	\[
 		(\stOpen,\cid,\hydraKeysAgg,\nop,\cPer,v,\eta) \xrightarrow[\xi]{\mathsf{increment}} (\stOpen,\cid,\hydraKeysAgg,\nop,\cPer,v',\eta')
@@ -344,17 +344,17 @@ \subsection{\red{Increment Transaction}}\label{sec:increment-tx}
 	\[
 		s' > s
 	\]
-	\item Last known open state version is preserved
+	\item New version $v'$ is incremented correctly
 	\[
-		v = v'
+		v' = v + 1
 	\]
-\item $\xi$ is a valid multi-signature of the new snapshot state (currency id $\cid$, the current state version $v$, new state $\eta'$, $\eta_{\alpha}$, $\eta_{\omega}$)
+	\item $\xi$ is a valid multi-signature of the new snapshot state (currency id $\cid$, the current state version $v$, the new state $\eta'$, and $\eta_{\omega}$)
 	\[
-		\msVfy(\hydraKeys,(\cid || v || s || \eta' || \eta_{\alpha} || \eta_{\omega}),\xi) = \true
+		\msVfy(\hydraKeys,(\cid || v || s || \eta' || \eta_{\omega}),\xi) = \true
 	\]
-  where snapshot number $s$ is provided through the redeemer, $\eta_{\alpha}$ is the digest of all added UTxO and  $\eta_{\omega}$ must be the digest of all removed UTxO
+  where snapshot number $s$ is provided through the redeemer, and $\eta_{\omega}$ is the digest of all added UTxO
 	\[
-		\eta_{\alpha} = U^{\#}_{\alpha}  = \hash(\bigoplus_{j=1}^m \bytes(i_{j}))
+		\eta_{\omega} = U^{\#}_{\omega}  = \hash(\bigoplus_{j=1}^m \bytes(i_{j}))
 	\]
 	\item The value in the head output is increased accordingly
 	\todo{Redundant to above? Only check $\valHead' > \valHead$?}
@@ -389,7 +389,7 @@ \subsection{\red{Decrement Transaction}}\label{sec:decrement-tx}
 
 \noindent The state-machine validator $\nuHead$ is spent with
 $\redeemerHead = (\mathsf{decrement}, \xi, s, m)$, where $\xi$ is a multi-signature of
-the decrement snapshot which authorizes removal of some UTxO, $s$ is the
+the decrement snapshot which authorizes removal of some UTxO $U_\omega$, $s$ is the
 used \todo{Decrement redeemer doesn't contain snapshot number} snapshot number and $m$ is the number of outputs to distribute. The
 validator checks:
 \begin{menumerate}
@@ -408,11 +408,11 @@ \subsection{\red{Decrement Transaction}}\label{sec:decrement-tx}
 	\[
 		v' = v + 1
 	\]
-	\item $\xi$ is a valid multi-signature of the new snapshot state (currency id $\cid$, the current state version $v$, and the new state $\eta'$)
+	\item $\xi$ is a valid multi-signature of the new snapshot state (currency id $\cid$, the current state version $v$, the new state $\eta'$, and $\eta_{\omega}$)
 	\[
-		\msVfy(\hydraKeys,(\cid || v || s || \eta' || \eta_{\alpha} || \eta_{\omega}),\xi) = \true
+		\msVfy(\hydraKeys,(\cid || v || s || \eta' || \eta_{\omega}),\xi) = \true
 	\]
-    where snapshot number $s$ is provided through the redeemer, $\eta_{\alpha}$ is the digest of all added UTxO and  $\eta_{\omega}$ must be the digest of all removed UTxO
+    where snapshot number $s$ is provided through the redeemer, and $\eta_{\omega}$ must be the digest of all removed UTxO
 	\[
 		\eta_{\omega} = U^{\#}_{\omega}  = \hash(\bigoplus_{j=2}^{m+1} \bytes(o_{j}))
 	\]
@@ -468,7 +468,7 @@ \subsection{Close Transaction}\label{sec:close-tx}
 		\]
 	}
 
-	\item \red{Based on the redeemer $\mathsf{CloseType} = \mathsf{Initial} \cup (\mathsf{Current}, \xi) \cup (\mathsf{Outdated}, \xi,  \eta_{\omega})$, where $\xi$ is a multi-signature of the closing snapshot and $\eta_{\omega}$ is a digest of the UTxO to decommit, three cases are distinguished:
+	\item \red{Based on the redeemer $\mathsf{CloseType} = \mathsf{Initial} \cup (\mathsf{Current}, \xi) \cup (\mathsf{Outdated}, \xi,  \eta_{\omega})$, where $\xi$ is a multi-signature of the closing snapshot and $\eta_{\omega}$ is the digest of the UTxO to either increment or decrement, three cases are distinguished:
 		\begin{menumerate}
 			\item $\mathsf{Initial}$: The initial snapshot is used to close the head and open state was not updated. No signatures are available and it suffices to check
 			\[
@@ -480,21 +480,21 @@ \subsection{Close Transaction}\label{sec:close-tx}
 			\[
 				\eta' = \eta
 			\]
-			\item $\mathsf{Current}$: Closing snapshot refers to current state version $v$ and any UTxO to decommit need to be present in the closed state too.
+			\item $\mathsf{Current}$: Closing snapshot refers to current state version $v$ and any UTxO to increment/decrement need to be present in the closed state too.
 			\[
-        \msVfy(\hydraKeys,(\cid || v || s' || \eta' || \eta_{\alpha} || \eta_{\Delta}'),\xi) = \true
+        \msVfy(\hydraKeys,(\cid || v || s' || \eta' || \eta_{\Delta}'),\xi) = \true
 			\]
-			which implies $\eta_{\Delta}' = \eta_{\omega}$ while $\eta_{\omega}$ does not need to be provided and $\eta_{\alpha}$ is provided in the snapshot.
+			which implies $\eta_{\Delta}' = \eta_{\omega}$ while $\eta_{\omega}$ does not need to be provided.
 			% TODO: put more into the redeemer to simplify?
 			\todo{this is hard to understand}
-			\item $\mathsf{Outdated}$: Closing snapshot refers the previous state $v - 1$ and any UTxO to decommit of the closing snapshot must not be recorded in the closed state.
+			\item $\mathsf{Outdated}$: Closing snapshot refers the previous state $v - 1$ and any UTxO to increment/decrement of the closing snapshot must not be recorded in the closed state.
 			\[
 				\eta_{\Delta}' = \bot
 			\]
 			\[
-				\msVfy(\hydraKeys,(\cid || v - 1 || s' || \eta' || \eta_{\alpha} || \eta_{\omega}),\xi) = \true
+				\msVfy(\hydraKeys,(\cid || v - 1 || s' || \eta' || \eta_{\omega}),\xi) = \true
 			\]
-			where $\eta_{\alpha}$ is provided in the snapshot and $\eta_{\omega}$ is provided by the redeemer\footnote{$\eta_{\omega}$ needs to be provided to verify the signature, but is otherwise not relevant for the closed state}.
+			where $\eta_{\omega}$ is provided by the redeemer\footnote{$\eta_{\omega}$ needs to be provided to verify the signature, but is otherwise not relevant for the closed state}.
 		\end{menumerate}
 	}
 	% TODO: detailed CDDL definition of msg
@@ -569,21 +569,21 @@ \subsection{Contest Transaction}\label{sec:contest-tx}
 		s' > s
 	\]
 
-	\item \red{Based on the redeemer $\mathsf{ContestType} = (\mathsf{Current}, \xi) \cup (\mathsf{Outdated}, \xi,  \eta_{\omega})$, where $\xi$ is a multi-signature of the contesting snapshot and $\eta_{\omega}$ is a digest of the UTxO to decommit, two cases are distinguished:
+	\item \red{Based on the redeemer $\mathsf{ContestType} = (\mathsf{Current}, \xi) \cup (\mathsf{Outdated}, \xi,  \eta_{\omega})$, where $\xi$ is a multi-signature of the contesting snapshot and $\eta_{\omega}$ is the digest of the UTxO to either increment or decrement, two cases are distinguished:
 		\begin{menumerate}
-			\item $\mathsf{Current}$: Contesting snapshot refers to the current state version $v$ and any UTxO to decommit need to be present in the closed state too.
+			\item $\mathsf{Current}$: Contesting snapshot refers to the current state version $v$ and any UTxO to increment/decrement need to be present in the closed state too.
 			\[
-        \msVfy(\hydraKeys,(\cid || v || s' || \eta' || \eta_{\alpha} || \eta_{\Delta}'),\xi) = \true
+        \msVfy(\hydraKeys,(\cid || v || s' || \eta' || \eta_{\Delta}'),\xi) = \true
 			\]
-			which implies $\eta_{\Delta}' = \eta_{\omega}$ while $\eta_{\omega}$ does not need to be provided and $\eta_{\alpha}$ is provided in the snapshot.
-			\item $\mathsf{Outdated}$: Contesting snapshot refers the previous state version $v - 1$ and any UTxO to decommit must not be recorded in the closed state.
+			which implies $\eta_{\Delta}' = \eta_{\omega}$ while $\eta_{\omega}$ does not need to be provided.
+			\item $\mathsf{Outdated}$: Contesting snapshot refers the previous state version $v - 1$ and any UTxO to increment/decrement must not be recorded in the closed state.
 			\[
 				\eta_{\Delta}' = \bot
 			\]
 			\[
-				\msVfy(\hydraKeys,(\cid || v - 1 || s' || \eta' || \eta_{\alpha} || \eta_{\omega}),\xi) = \true
+				\msVfy(\hydraKeys,(\cid || v - 1 || s' || \eta' || \eta_{\omega}),\xi) = \true
 			\]
-			where $\eta_{\alpha}$ is provided in the snapshot and $\eta_{\omega}$ is provided by the redeemer\footnote{$\eta_{\omega}$ needs to be provided to verify the signature, but is otherwise not relevant for the closed state}.
+			where $\eta_{\omega}$ is provided by the redeemer\footnote{$\eta_{\omega}$ needs to be provided to verify the signature, but is otherwise not relevant for the closed state}.
 		\end{menumerate}
 	}
 	% TODO: detailed CDDL definition of msg