Spec: Mainly remove incremental commit mentioning

Also add some decommit parts

hydra-node/src/Hydra/HeadLogic.hs

@@ -448,8 +448,6 @@ onOpenNetworkReqSn env ledger st otherParty sn requestedTxIds mDecommitTx =
       [] -> continue
       unseen -> wait $ WaitOnTxs unseen
 
-  -- TODO: We should probably check here that 'utxoToDecommit' from the 'Snapshot'
-  -- is matches the one from the 'decrementTx'
   requireApplicableDecommitTx cont =
     case mDecommitTx of
       Nothing -> cont (confirmedUTxO, Nothing)

spec/fig_SM_states_basic.tex

@@ -9,7 +9,6 @@
 
     \path[->] (initial) edge [bend left=20] node {$\stCollect$} (open);
     \path[->] (open) edge [bend left=20] node {$\stClose$} (closed);
-    \path[->] (open) edge [loop above] node {$\mathsf{increment}$} (open);
     \path[->] (open) edge [loop below] node {$\mathsf{decrement}$} (open);
     \path[->] (closed) edge [bend left=20] node {$\stFanout$} (final);
     \path[->] (closed) edge [loop above] node {$\stContest$} (closed);

spec/macros.tex

@@ -317,6 +317,7 @@
 \newcommand{\hpSeen}{\mathtt{seen}}
 \newcommand{\hpConf}{\mathtt{conf}}
 \newcommand{\hpSnap}{\mathtt{snap}}
+\newcommand{\hpDecommit}{\mathtt{decommit}}
 \newcommand{\hpClose}{\mathtt{close}}
 \newcommand{\hpCont}{\mathtt{cont}}
 \newcommand{\hpFO}{\mathtt{fanOut}}
@@ -413,6 +414,7 @@
 
 \newcommand{\hpNS}{\mathtt{newSn}}
 \newcommand{\hpRS}{\mathtt{reqSn}}
+\newcommand{\hpRD}{\mathtt{reqDec}}
 \newcommand{\hpAS}{\mathtt{ackSn}}
 \newcommand{\hpCS}{\mathtt{confSn}}
 

spec/offchain.tex

@@ -18,14 +18,12 @@ \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}
+					\item $\hpRD$: to request new decommit
 	      \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 $\hpDecommit$: 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}
@@ -175,28 +173,37 @@ \subsubsection{Processing transactions off-chain}
 snapshot
 leader, a message to request snapshot signatures $\hpRS$ is sent. \\
 
+\dparagraph{$\hpRD$.}\quad Upon receiving request $(\hpRD,\tx)$, the
+transaction is checked against the \emph{local} ledger state. If decommit is
+not applicable yet, the protocol does $\KwWait$ to retry later and eventually
+emmits an error message that another decommit is \emph{in flight}. In case
+there is no decommit \emph{in flight} and party is the leader then $\hpRS$ is
+emmitted containing the utxo to decommit. \\
+
 \dparagraph{$\hpRS$.}\quad Upon receiving request
 $(\hpRS,s,\mT_{\mathsf{req}}^{\#})$ from party $\party_j$, the receiver
-$\party_i$ checks that $s$ is the next snapshot number and that party $\party_j$
-is responsible for leading its creation.\todo{define $\hpLdr$} Party $\party_i$
-has to $\KwWait$ until the previous snapshot is confirmed ($\bars = \hats$) and
-all requested transaction hashes $\mT_{\mathsf{req}}^{\#}$ can be resolved in
-$\mT_{\mathsf{all}}$. Then, all those resolved transactions $\mT_{\mathsf{req}}$
-are $\Req$d to be applicable to $\barmU$, otherwise the snapshot is rejected
-as invalid. Only then, $\party_i$ increments their seen-snapshot counter
-$\hats$, resets the signature accumulator $\hatSigma$, and computes the UTxO set
-$\hatmU$ of the new (seen) snapshot as
-$\hatmU \gets \barmU \applytx \mT_{\mathsf{req}}$. Then, $\party_i$ creates a
-signature $\msSig_i$ using their signing key $\hydraSigningKey$ on a message
-comprised by the $\cid$, \textcolor{red}{the $\eta_{0}$ corresponding to the
-	initial UTxO set $\Uinit$}, and the new $\eta'$ given by the new snapshot number
-$\hats$ and canonically combining $\hatmU$ (see Section~\ref{sec:close-tx} for
-details). The signature is sent to all head members via message
-$(\hpAS,\hats,\msSig_i)$. Finally, the pending transaction set $\hatmT$ gets
-pruned by re-applying all locally pending transactions $\hatmT$ to the just
-requested snapshot's UTxO set $\hatmU$ iteratively and ultimately yielding a
-``pruned'' version of $\hatmT$ and $\hatmU$. Also, the set of all transactions
-$\mT_{\mathsf{all}}$ can be reduced by the requested
+$\party_i$ checks that $s$ is the next snapshot number and that party
+$\party_j$ is responsible for leading its creation.\todo{define $\hpLdr$} Party
+$\party_i$ has to $\KwWait$ until the previous snapshot is confirmed ($\bars =
+\hats$) and all requested transaction hashes $\mT_{\mathsf{req}}^{\#}$ can be
+resolved in $\mT_{\mathsf{all}}$. In the presence of decommits the requested
+decommit needs to be removed from the active UTxO set (by applying a decommit
+transaction) and the new UTxO set is then passed to further handling of
+$\hpRS$. Then, all those resolved transactions $\mT_{\mathsf{req}}$ are $\Req$d
+to be applicable to $\barmU$, otherwise the snapshot is rejected as invalid.
+Only then, $\party_i$ increments their seen-snapshot counter $\hats$, resets
+the signature accumulator $\hatSigma$, and computes the UTxO set $\hatmU$ of
+the new (seen) snapshot as $\hatmU \gets \barmU \applytx \mT_{\mathsf{req}}$.
+Then, $\party_i$ creates a signature $\msSig_i$ using their signing key
+$\hydraSigningKey$ on a message comprised by the $\cid$, \textcolor{red}{the
+$\eta_{0}$ corresponding to the initial UTxO set $\Uinit$}, and the new $\eta'$
+given by the new snapshot number $\hats$ and canonically combining $\hatmU$
+(see Section~\ref{sec:close-tx} for details). The signature is sent to all head
+members via message $(\hpAS,\hats,\msSig_i)$. Finally, the pending transaction
+set $\hatmT$ gets pruned by re-applying all locally pending transactions
+$\hatmT$ to the just requested snapshot's UTxO set $\hatmU$ iteratively and
+ultimately yielding a ``pruned'' version of $\hatmT$ and $\hatmU$. Also, the
+set of all transactions $\mT_{\mathsf{all}}$ can be reduced by the requested
 transactions $\mT_{\mathsf{req}}$.\\
 
 \dparagraph{$\hpAS$.}\quad Upon receiving acknowledgment $(\hpAS,s,\msSig_j)$, all

spec/onchain.tex

@@ -315,58 +315,7 @@ \subsection{CollectCom Transaction}\label{sec:collect-tx}
 		$\stOpen$ head output.}\label{fig:collectComTx}
 \end{figure}
 
-\subsection{Increment Transaction}\label{sec:increment-tx}
-
-\noindent The \mtxIncrement{} transaction (Figure~\ref{fig:incrementTx}) allows
-a party to add a UTxO to an already open head and consists of:
-
-\begin{itemize}
-	\item one input spending from $\nuHead$ holding the $\st$ with $\datumHead$,
-	\item one or more inputs with reference $\txOutRef_{\mathsf{committed}_{j}}$
-	      spending output $o_{\mathsf{committed}_{j}}$ with
-	      $\val_{\mathsf{committed}_{j}}$,
-	\item one output paying to $\nuHead$ with value $\valHead'$ and
-	      datum $\datumHead'$.
-\end{itemize}
-
-\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$, and checks:
-\begin{menumerate}
-	\item State is advanced from $\datumHead \sim \stOpen$ to
-	$\datumHead' \sim \stOpen$, parameters $\cid,\hydraKeysAgg,\nop,\cPer$
-	stay unchanged and the new state is governed again by $\nuHead$
-	\todo{explain $\stOpen$ tuple}
-	\todo{need to check all fields!}
-	\[
-		(\stOpen,\cid,\hydraKeysAgg,\nop,\cPer,\eta_{\mathsf{pre}},s,\eta) \xrightarrow[\xi]{\mathsf{increment}} (\stOpen,\cid,\hydraKeysAgg,\nop,\cPer,\eta,s',\eta')
-	\]
-	\item Increment snapshot number $s'$ is higher than the currently stored snapshot number $s$
-	\[
-		s' > s
-	\]
-	\item $\xi$ is a valid multi-signature of the currency id $\cid$, the current snapshot state $\eta$, the new snapshot number $s'$ and state $\eta'$
-	\[
-		\msVfy(\hydraKeysAgg,(\cid || \eta || s' || \eta' || \eta_{\alpha}),\xi) = \true
-	\]
-	where $\eta_{\alpha}$ is the digest of all added UTxO
-	\[
-		\eta_{\alpha} = U^{\#}_{\alpha}  = \hash(\bigoplus_{j=1}^{m} \bytes(o_{\mathsf{committed}_{j}}))
-	\]
-	\item Transaction is signed by a participant
-	\[
-		\exists \{\cid \mapsto \keyHash_{i} \mapsto 1\} \in \valHead' \Rightarrow \keyHash_{i} \in \txKeys
-	\]
-\end{menumerate}
-
-\begin{figure}
-	\centering
-	\includegraphics[width=0.8\textwidth]{figures/incrementTx.pdf}
-	\caption{\mtxIncrement{} transaction spending an open head output and a single
-		committed output, and producing a new head output.}\label{fig:incrementTx}
-\end{figure}
-
-\subsection{Decrement Transaction}\label{sec:increment-tx}
+\subsection{Decrement Transaction}\label{sec:decrement-tx}
 
 \noindent The \mtxDecrement{} transaction (Figure~\ref{fig:DecrementTx}) allows
 a party to remove a UTxO from an already open head and consists of:
@@ -464,12 +413,7 @@ \subsection{Close Transaction}\label{sec:close-tx}
 	  \[
 		\msVfy(\hydraKeysAgg,(\cid || \eta_{\mathsf{cur}}|| s' || \eta' || \bot || \bot),\xi) = \true
 	  \]
-	  \item Preemptive close: Instead of incrementing/decrementing, the head is closed with a snapshot that references the current state $\eta_{\mathsf{cur}}$, but has pending UTxO to commit.
-	  \[
-		\msVfy(\hydraKeysAgg,(\cid || \eta_{\mathsf{cur}} || s' || \eta' || \eta_{\alpha} || \eta_{\Delta}),\xi) = \true
-	  \]
-	  where $\eta_{\alpha}$ is provided by the redeemer. \todo{explain why this is enough}
-	  \item Pending close: After incrementing/decrementing, the head is closed with a snapshot that is still referencing the previous state $\eta_{\mathsf{pre}}$ and pending UTxO to decommit.
+	  \item Pending close: After decrementing, the head is closed with a snapshot that is still referencing the previous state $\eta_{\mathsf{pre}}$ and pending UTxO to decommit.
 	  \[
 		\msVfy(\hydraKeysAgg,(\cid || \eta_{\mathsf{pre}} || s' || \eta' || \eta_{\Delta} || \eta_{\omega}),\xi) = \true
 	  \]

spec/overview.tex

@@ -39,13 +39,15 @@ \subsection{Opening the head}
 locks (on the mainchain) the UTxOs that the party wants to commit to the head,
 or deliberately acknowledges to commit nothing.
 
-The commit transactions are subsequently collected by the \mtxCCom{} transaction
-causing a transition from $\stInitial$ to $\stOpen$. Once the $\stOpen$ state is
-confirmed, the head members start running the off-chain head protocol, which
-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
+The commit transactions are subsequently collected by the \mtxCCom{}
+transaction causing a transition from $\stInitial$ to $\stOpen$. Once the
+$\stOpen$ state is confirmed, the head members start running the off-chain head
+protocol, which evolves the initial UTxO set (the union over all UTxOs
+committed by all head members) independently of the mainchain. Head member can
+also decide to take some UTxO they own out of the Head and make it available on
+main chain. We call this action decrement. 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$ \todo{increment / decrement}.
+from $\stInitial$ to $\stFinal$.
 
 
 \subsection{The Coordinated Head protocol}