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/offchain.tex

@@ -18,10 +18,14 @@ \section{Off-Chain Protocol}\label{sec:offchain}
 		      \item $\hpRT$: to request a transaction to be included in the next snapshot
 		      \item $\hpRS$: to request a snapshot to be created \& signed by every head member
 		      \item $\hpAS$: to acknowledge a snapshot by replying with their signatures
+					\item \texttt{reqInc} \todo{explain}
+					\item \texttt{reqDec} \todo{explain}
 	      \end{itemize}
 	\item Commands issued by the participants themselves or on behalf of end-users and clients
 	      \begin{itemize}
 		      \item $\hpInit$: to start initialization of a head
+		      \item \texttt{commit} to request an incremental commit
+		      \item \texttt{decommit} to request an incremental decommit
 		      \item $\hpNew$: to submit a new transaction to an open head
 		      \item $\hpClose$: to request closure of an open head
 	      \end{itemize}
@@ -94,7 +98,7 @@ \subsection{Notation}
 \subsection{Variables}
 
 Besides parameters agreed in the protocol setup (see Section~\ref{sec:setup}), a
-party's local state consists of the following variables:
+party's local state consists of the following variables: \todo{update}
 
 \begin{itemize}
 	\item $\hats$: Sequence number of latest seen snapshot.
@@ -146,6 +150,7 @@ \subsubsection{Initializing the head}
 with it. The initial transaction sets are empty
 $\mT = \barmT =\hatmT =\emptyset$, and $\bars = \hats = 0$.
 % REVIEW: check $\eta$ against $\Uinit$?
+\todo{add increment/decrement}
 
 \subsubsection{Processing transactions off-chain}
 

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: