Align onchain increment section

spec/fig_SM_states_basic.tex

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

spec/onchain.tex

@@ -317,43 +317,62 @@ \subsection{CollectCom Transaction}\label{sec:collect-tx}
 		$\stOpen$ head output.}\label{fig:collectComTx}
 \end{figure}
 
-\subsection{Increment Transaction}\label{sec:increment-tx}
+\subsection{\red{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.
+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'$.
+		  datum $\datumHead'$,
+    \item one or more inputs spent in this transaction $i_{1} \dots i_m$ where $m$ is the number of inputs to include and $\forall i \in \{i_{1} \dots i_{m}\}, i \notin I_{head}$.
 \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:
+the increment snapshot which authorizes addition of some UTxO $U_\alpha$. The
+validator 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$:
-  \[
-	(\stOpen,\cid,\hydraKeysAgg,\nop,\cPer,\eta) \xrightarrow[\xi]{\mathsf{increment}} (\stOpen,\cid,\hydraKeysAgg,\nop,\cPer,\eta')
-  \]
-	\item Increment snapshot is newer $s' > s$, where $(s, \cdot) = \eta$ is the
-		current and $(s', \cdot) = \eta'$ is the incremented snapshot number.
-	\item $\xi$ is a valid multi-signature of the new snapshot state
-    $\msVfy(\hydraKeysAgg,(\cid || \textcolor{red}{\eta_{0}} || \eta'),\xi) = \true$.
-  \item \todo{Need to ensure all value of $U_\alpha$ is captured} All committed value is in the output
-	$\valHead' \supseteq \valHead \cup (\bigcup_{j=1}^{m} \val_{\mathsf{committed}_{j}})$
+	\item State is advanced from $\datumHead \sim \stOpen$ to
+	$\datumHead' \sim \stOpen$, parameters $\cid,\hydraKeysAgg,\nop,\cPer,v$
+	stay unchanged and the new state is governed again by $\nuHead$:
+	\[
+		(\stOpen,\cid,\hydraKeysAgg,\nop,\cPer,v,\eta) \xrightarrow[\xi]{\mathsf{increment}} (\stOpen,\cid,\hydraKeysAgg,\nop,\cPer,v',\eta')
+	\]
+	\item Increment snapshot number $s'$ is higher than the currently stored snapshot number $s$
+	\[
+		s' > s
+	\]
+	\item Last known open state version is preserved
+	\[
+		v = v'
+	\]
+\item $\xi$ is a valid multi-signature of the new snapshot state (currency id $\cid$, the current state version $v$, new state $\eta'$, $\eta_{\alpha}$, $\eta_{\omega}$)
+	\[
+		\msVfy(\hydraKeys,(\cid || v || s || \eta' || \eta_{\omega} || \eta_{\alpha}),\xi) = \true
+	\]
+	where $\eta_{\alpha}$ must be the digest of all added UTxO
+	\[
+		\eta_{\alpha} = U^{\#}_{\alpha}  = \hash(\bigoplus_{j=1}^m \bytes(i_{j}))
+	\]
+	\item The value in the head output is increased accordingly
+	\todo{Redundant to above? Only check $\valHead' > \valHead$?}
+	\[
+		\valHead \cup (\bigcup_{j=1}^m \val_{i_{j}}) = \valHead'
+	\]
+	\item Transaction is signed by a participant
+	\todo{Allow anyone to do increments?}
+	\[
+		\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,
-		producing a new head output which includes new UTxO.}\label{fig:incrementTx}
+		producing a new head output which includes the new UTxO.}\label{fig:incrementTx}
 \end{figure}
 
 \subsection{\red{Decrement Transaction}}\label{sec:decrement-tx}
@@ -381,11 +400,15 @@ \subsection{\red{Decrement Transaction}}\label{sec:decrement-tx}
 	\[
 		(\stOpen,\cid,\hydraKeys,\cPer,v,\eta) \xrightarrow[\xi, s, m]{\mathsf{decrement}} (\stOpen,\cid,\hydraKeys,\cPer,v',\eta')
 	\]
+	\item Decrement snapshot number $s'$ is higher than the currently stored snapshot number $s$
+	\[
+		s' > s
+	\]
 	\item New version $v'$ is incremented correctly
 	\[
 		v' = v + 1
 	\]
-	\item $\xi$ is a valid multi-signature of the currency id $\cid$, the current state version $v$, and the new state $\eta'$
+	\item $\xi$ is a valid multi-signature of the new snapshot state (currency id $\cid$, the current state version $v$, and the new state $\eta'$)
 	\[
 		\msVfy(\hydraKeys,(\cid || v || s || \eta' || \eta_{\omega}),\xi) = \true
 	\]
@@ -433,7 +456,7 @@ \subsection{Close Transaction}\label{sec:close-tx}
 \red{$\mathsf{CloseType}$ is a hint against which open state to close} and checks:
 \begin{menumerate}
 	\item State is advanced from $\datumHead \sim \stOpen$ to
-	$\datumHead' \sim \stClosed$, parameters $\cid,\hydraKeys,\cPer$
+	$\datumHead' \sim \stClosed$, parameters $\cid,\hydraKeys,\cPer,v$
 	stay unchanged and the new state is governed again by $\nuHead$
 	\[
 		(\stOpen,\cid,\hydraKeys,\cPer,\red{v,}\eta) \xrightarrow[\red{\mathsf{CloseType}}]{\stClose} (\stClosed,\cid,\hydraKeys,\cPer,\red{v',s',\eta',\eta_{\Delta}'},\contesters,\Tfinal)

spec/overview.tex

@@ -81,10 +81,10 @@ \subsection{The Coordinated Head protocol}
 is now evidence that this state once existed during the head evolution.
 
 \red{Besides processing ``normal'' transactions, participants can also request
-  to take some UTxO they can spend out of the Head and make it available on main
-  chain using a \mtxDecrement{} transaction - the whole process is called
-  decommit. Another ``unusual`` transaction is \mtxIncrement{} transaction which
-  allows Head participants to add some UTxO from L1 to the Head.}
+  to withdraw some UTxO they can spend from the Head and make it available on main
+  chain, or deposit some UTxO they can spend from L1 and make it available within the Head.
+  These processes are called decrement, via the \mtxDecrement{} transaction, 
+  and increment, via the \mtxIncrement{} transaction.}
 
 \subsection{Closing the head}
 
@@ -118,7 +118,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).
-    \red{\item Allow for incremental decommits while head is open.}
+    \red{\item Allow for increments and decrements  while head is open.}
 \end{itemize}
 
 %%% Local Variables: