From 2871737843c9815f918b034bace1b8b54c6eb6fd Mon Sep 17 00:00:00 2001
From: Sebastian Nagel <sebastian.nagel@ncoding.at>
Date: Thu, 7 Mar 2024 10:14:33 +0100
Subject: [PATCH] Some alignment between spec and impl

---
 hydra-plutus/src/Hydra/Contract/HeadState.hs | 3 +++
 spec/onchain.tex                             | 3 ++-
 spec/overview.tex                            | 5 ++++-
 3 files changed, 9 insertions(+), 2 deletions(-)

diff --git a/hydra-plutus/src/Hydra/Contract/HeadState.hs b/hydra-plutus/src/Hydra/Contract/HeadState.hs
index ba780f8c062..86e529cab12 100644
--- a/hydra-plutus/src/Hydra/Contract/HeadState.hs
+++ b/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
diff --git a/spec/onchain.tex b/spec/onchain.tex
index fb07293e8e7..bb333d4c1bf 100644
--- a/spec/onchain.tex
+++ b/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
diff --git a/spec/overview.tex b/spec/overview.tex
index 514e2032c59..3fbb8c5b267 100644
--- a/spec/overview.tex
+++ b/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: