Some alignment between spec and impl

hydra-plutus/src/Hydra/Contract/HeadState.hs

@@ -36,8 +36,11 @@ data State
   | Closed
       { parties :: [Party]
       , snapshotNumber :: SnapshotNumber
+      -- ^ Spec: fst of η
       , utxoHash :: Hash
+      -- ^ Spec: snd of η
       , utxoToDecommitHash :: Hash
+      -- ^ Spec: ηω
       , contestationDeadline :: POSIXTime
       , contestationPeriod :: ContestationPeriod
       , headId :: CurrencySymbol

spec/onchain.tex

@@ -415,7 +415,7 @@ \subsection{Close Transaction}\label{sec:close-tx}
 		$\datumHead' \sim \stClosed$, parameters $\cid,\hydraKeysAgg,\nop,\cPer$
 		stay unchanged and the new state is governed again by $\nuHead$:
 		\[
-			(\stOpen,\cid,\hydraKeysAgg,\nop,\cPer,\eta) \xrightarrow[\xi]{\stClose} (\stClosed,\cid,\hydraKeysAgg,\nop,\cPer,\eta_0,\eta',\contesters,\Tfinal)
+			(\stOpen,\cid,\hydraKeysAgg,\nop,\cPer,\eta) \xrightarrow[\xi]{\stClose} (\stClosed,\cid,\hydraKeysAgg,\nop,\cPer,\eta_0,\eta',\textcolor{blue}{\eta_{\omega}},\contesters,\Tfinal)
 		\]
 		\item Records the initial snapshot state $\eta_0 = \eta$. \\
 		This makes off-chain signatures rollback and replay resistant,
@@ -433,6 +433,7 @@ \subsection{Close Transaction}\label{sec:close-tx}
 		% TODO: η₀ is not yet incorporated
 		and $\eta'$: $\mathsf{msg} = (\cid || \textcolor{red}{\eta_{0} ||} \eta')$.
 		% TODO: detailed CDDL definition of msg
+		\todo{snapshot/msg with pending decommit must work as well}
 		\item Initializes the set of contesters as $\contesters = \emptyset$. \\
 		This allows the closing party to also contest and is required for use
 		cases where pre-signed, valid in the future, close transactions are

spec/overview.tex

@@ -45,7 +45,9 @@ \subsection{Opening the head}
 evolves the initial UTxO set (the union over all UTxOs committed by all head
 members) independently of the mainchain. For the case where some head members
 fail to post a \mtxCom{} transaction, the head can be aborted by going directly
-from $\stInitial$ to $\stFinal$.
+from $\stInitial$ to $\stFinal$ \todo{increment / decrement}.
+
+
 \subsection{The Coordinated Head protocol}
 
 The actual Head protocol starts after the initialization phase with an initial
@@ -110,6 +112,7 @@ \subsection{Differences}
 	\item No hanging transactions due to `coordination'.
 	\item No acknowledgement nor confirmation of transactions.
 	\item No confirmation message for snapshots (two-round local confirmation).
+    \todo{increment / decrement extension}
 \end{itemize}
 
 %%% Local Variables: