Rename close redeemer types and add \theta to the signature

Signed-off-by: Sasha Bogicevic <sasha.bogicevic@iohk.io>

spec/fig_offchain_prot.tex

@@ -237,13 +237,13 @@
 									% NOTE: Implementation differs here and
 									% below as it stores seen version in seen
 									% snapshot and uses that to verify
-									\Req{} $\msVfy(\hydraKeysAgg, (\cid || \blue{\hatv ||} \hats || \eta || \red{\eta_\theta}), \msCSig)$ \;
+                  \Req{} $\msVfy(\hydraKeysAgg, (\cid || \blue{\hatv ||} \hats || \eta || \red{\eta_\theta} || \red{\theta}), \msCSig)$ \;
 									% create confirmed snapshot for later reference
 									$\bar{\mc S} \gets \Sno(\hatv, \hats, \hatmU, \hatmT, \red{\eta_\theta})$ \;
 									$\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{$\psi \not= \bot ~ \land ~ \psi \in$} $\tx_\omega$}{
 										$\PostTx{}~(\mathtt{decrementTx}, \hatv, \hats, \eta, \red{\eta_\theta})$ \;
 										% NOTE: Needed for security?

spec/onchain.tex

@@ -348,7 +348,7 @@ \subsection{\red{Increment Transaction}}\label{sec:increment-tx}
 	\]
 	\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_\theta$)
 	\[
-		\msVfy(\hydraKeys,(\cid || v || s || \eta' || \eta_\theta),\xi) = \true
+    \msVfy(\hydraKeys,(\cid || v || s || \eta' || \eta_\theta || \red{\theta}),\xi) = \true
 	\]
   where snapshot number $s$ is provided through the redeemer, and $\eta_\theta$ is the digest of all added UTxO
 	\[
@@ -407,7 +407,7 @@ \subsection{Decrement Transaction}\label{sec:decrement-tx}
 	\]
 	\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 $\red{\eta_\theta}$)
 	\[
-		\msVfy(\hydraKeys,(\cid || v || s || \eta' || \red{\eta_\theta}),\xi) = \true
+		\msVfy(\hydraKeys,(\cid || v || s || \eta' || \red{\eta_\theta} || \red{\theta}),\xi) = \true
 	\]
     where snapshot number $s$ is provided through the redeemer, and $\red{\eta_\theta}$ must be the digest of all removed UTxO
 	\[
@@ -464,7 +464,7 @@ \subsection{Close Transaction}\label{sec:close-tx}
 		v' = v
 	\]
 
-	\item Based on the redeemer $\mathsf{CloseType} = \mathsf{Initial} \cup (\mathsf{Current}, \xi, \red{\theta}) \cup (\mathsf{Outdated}, \xi,  \eta_\theta, \red{\theta})$, where $\xi$ is a multi-signature of the closing snapshot\red{, $\theta$ is the snapshot type} and $\eta_\theta$ is the digest of the UTxO to \red{either increment or} decrement, \red{five} cases are distinguished:
+	\item Based on the redeemer $\mathsf{CloseType} = \mathsf{Initial} \cup (\mathsf{Unused}, \xi, \red{\theta}) \cup (\mathsf{Used}, \xi,  \eta_\theta, \red{\theta})$, where $\xi$ is a multi-signature of the closing snapshot\red{, $\theta$ is the snapshot type} and $\eta_\theta$ is the digest of the UTxO to \red{either increment or} decrement, \red{five} 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,32 +480,32 @@ \subsection{Close Transaction}\label{sec:close-tx}
 			\[
 			\theta = Normal
 			\]
-			\item $\mathsf{Current/Inc}$: Closing snapshot refers to current state version $v$, snapshot type $\theta = Inc$ and any UTxO to increment must be $\bot$ in the closed state.
+			\item $\mathsf{Unused/Inc}$: Closing snapshot refers to current state version $v$, snapshot type $\theta = Inc$ and any UTxO to increment must be $\bot$ in the closed state.
 			\[
-			\msVfy(\hydraKeys,(\cid || v || s' || \eta' || \eta_{\Delta}'),\xi) = \true
+			\msVfy(\hydraKeys,(\cid || v || s' || \eta' || \eta_{\Delta}' || \theta),\xi) = \true
 			\]
 			which implies $\eta_{\Delta}' = \eta_\theta$ while $\eta_\theta$ must not be provided.
-			\item $\mathsf{Current/Dec}$: Closing snapshot refers to current state version $v$, snapshot type $\theta = Dec$ and any UTxO to decrement need to be present in the closed state too.
+			\item $\mathsf{Unused/Dec}$: Closing snapshot refers to current state version $v$, snapshot type $\theta = Dec$ and any UTxO to decrement need to be present in the closed state too.
 			\[
-			\msVfy(\hydraKeys,(\cid || v || s' || \eta' || \eta_{\Delta}'),\xi) = \true
+        \msVfy(\hydraKeys,(\cid || v || s' || \eta' || \eta_{\Delta}' || \theta),\xi) = \true
 			\]
 			which implies $\eta_{\Delta}' = \eta_\theta$ while $\eta_\theta$ must be provided.
 			% TODO: put more into the redeemer to simplify?
 			\todo{this is hard to understand}
-			\item $\mathsf{Outdated/Dec}$: Closing snapshot refers the previous state $v - 1$ , snapshot type $\theta = Dec$  and any UTxO to decrement of the closing snapshot must not be recorded in the closed state.
+			\item $\mathsf{Used/Dec}$: Closing snapshot refers the previous state $v - 1$ , snapshot type $\theta = Dec$  and any UTxO to decrement of the closing snapshot must not be recorded in the closed state.
 			\[
 				\eta_{\Delta}' = \bot
 			\]
 			\[
-				\msVfy(\hydraKeys,(\cid || v - 1 || s' || \eta' || \eta_\theta),\xi) = \true
+        \msVfy(\hydraKeys,(\cid || v - 1 || s' || \eta' || \eta_\theta || \theta),\xi) = \true
 			\]
 			where $\eta_\theta$ is provided by the redeemer\footnote{$\eta_\theta$ needs to be provided to verify the signature, but is otherwise not relevant for the closed state}.
-			\item $\mathsf{Outdated/Inc}$: Closing snapshot refers the previous state $v - 1$ , snapshot type $\theta = Inc$  and any UTxO to increment of the closing snapshot must be recorded in the closed state.
+			\item $\mathsf{Used/Inc}$: Closing snapshot refers the previous state $v - 1$ , snapshot type $\theta = Inc$  and any UTxO to increment of the closing snapshot must be recorded in the closed state.
 			\[
 				\eta_{\Delta}' \neq \bot
 			\]
 			\[
-				\msVfy(\hydraKeys,(\cid || v - 1 || s' || \eta' || \eta_\theta),\xi) = \true
+				\msVfy(\hydraKeys,(\cid || v - 1 || s' || \eta' || \eta_\theta || \theta),\xi) = \true
 			\]
 			where $\eta_\theta$ must be provided in the closed state.
 		}
@@ -585,15 +585,15 @@ \subsection{Contest Transaction}\label{sec:contest-tx}
 	\begin{menumerate}
 		\item $\mathsf{Current}$: Contesting snapshot refers to the current state version $v$ and any UTxO to \red{increment/}decrement need to be present in the closed state too.
 		\[
-		\msVfy(\hydraKeys,(\cid || v || s' || \eta' || \eta_\Delta'),\xi) = \true
+      \msVfy(\hydraKeys,(\cid || v || s' || \eta' || \eta_\Delta' || \red{\theta}),\xi) = \true
 		\]
 		which implies $\eta_\Delta' = \eta_\theta$ while $\eta_\theta$ does not need to be provided.
 		\item $\mathsf{Outdated}$: Contesting snapshot refers the previous state version $v - 1$ and any UTxO to \red{increment/}decrement must not be recorded in the closed state.
 		\[
 			\eta_\Delta' = \bot
 		\]
 		\[
-			\msVfy(\hydraKeys,(\cid || v - 1 || s' || \eta' || \eta_\theta),\xi) = \true
+      \msVfy(\hydraKeys,(\cid || v - 1 || s' || \eta' || \eta_\theta || \red{\theta}),\xi) = \true
 		\]
 		where $\eta_\theta$ is provided by the redeemer\footnote{$\eta_\theta$ needs to be provided to verify the signature, but is otherwise not relevant for the closed state}.
 	\end{menumerate}