WIP

spec/fig_offchain_prot.tex

@@ -182,9 +182,9 @@
 						%%% INCREMENT
 						\red{\On{$(\mathtt{incrementTx}, U'_\omega, v)$ from chain}{
 							\If{$\bar{\mc S}.U_\omega \not= \bot ~ \land ~ U'_\omega = \bar{\mc S}.U_\omega$}{
+								$\hatmL \gets \hatmL \cup U'_\omega$ \;
 								$U_\omega \gets \bot$\;
 								$\hatv \gets v$ \;
-								$\hatmL \gets \hatmL \cup U'_\omega$ \;
 								% TODO: always snapshot? not strictly needed (to clear pending decommits)?
 								\If{$\hats = \bar{\mc S}.s \land \hpLdr(\bar{\mc S}.s + 1) = i$}{
 									\Multi{} $(\hpRS,\hatv,\bar{\mc S}.s+1,\hatmT, \bot)$ \;

spec/offchain.tex

@@ -112,14 +112,14 @@ \subsection{Variables}
 \begin{itemize}
 	\item \red{$\hatv$: Last seen open state version.}
 	\item $\hats$: Sequence number of latest seen snapshot.
-	\item $\hatSigma \in {(\tyNatural \times \tyBytes)}^{*}$: 
+	\item $\hatSigma \in {(\tyNatural \times \tyBytes)}^{*}$:
 		Accumulator of signatures of the latest seen snapshot, indexed by parties.
 	\item $\hatmL$: UTxO set representing the local ledger state resulting from
 		applying $\hatmT$ to $\bar{S}.U$ to validate requested transactions.
 	\item $\hatmT \in \mT^{*}$: List of transactions applied locally and pending
 		inclusion in a snapshot (if this party is the next leader).
-	\item \red{$U_\omega \in \gcUTXOset$: Pending increment UTxO to be deposited to the head, 
-		or pending decrement UTxO to be withdrawn from the head. 
+	\item \red{$U_\omega \in \gcUTXOset$: Pending increment UTxO to be deposited to the head,
+		or pending decrement UTxO to be withdrawn from the head.
 		May be $\bot$ if nothing is pending to be applied.}
 	\item \red{$\bar{\mc S}$: Snapshot object of the latest confirmed snapshot which contains:
 		\begin{center}
@@ -194,18 +194,39 @@ \subsubsection{Processing transactions off-chain}
 receiving party $\party_{i}$ is the next snapshot
 leader, a message to request snapshot signatures $\hpRS$ is sent. \\
 
-\red{\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 in flight. In case there is
-	no decommit in flight and party is the leader then $\hpRS$ is
-	emmitted containing the decommit transaction $\tx_\omega$.} \\
+\red{\dparagraph{$\hpRD$.}\quad Upon receiving request $(\hpRD,\tx_\omega)$, if
+  another decrement (or increment) is pending to be settled the transaction is
+  rejected. Otherwise the transaction is checked against the \emph{local}
+  ledger state and if it is not applicable yet, the protocol does $\KwWait$ to
+  retry later or output an error message. After applying $\tx_\omega$, it's inputs
+  are removed from \emph{local} ledger state so that they are not available any
+  more and the outputs are kept in the local state ($U_\omega$) to be posted
+  on-chain in the next snapshot. If there is no current snapshot in flight
+  ($\hats = \bar{\mc S}.s$) and the receiving party $\party_{i}$ is the next
+  snapshot leader, a message to request snapshot signatures $\hpRS$ containing
+  the decrement transaction $\tx_\omega$ is sent.} \\
 
 \red{\dparagraph{$\mathtt{decrementTx}$.}\quad Upon observing the \mtxDecrement{}
 	transaction, which removed outputs $U_\omega$ from the head, the corresponding
 	decommit transaction is cleared and the observed version is used for future
-	snapshots by
-	setting $\hatv = v$. This is required as that the version of the open head state is incremented on each \mtxDecrement{} transaction as described in Section~\ref{sec:decrement-tx}} \\
+	snapshots by setting $\hatv = v$. The version of the open head state
+  is incremented on each \mtxDecrement{} transaction as described in Section~\ref{sec:decrement-tx}
+}
+\todo{missing to mention the multicast of $\hpRS$} \\
+
+\red{\dparagraph{$\hpRI$.}\quad Upon receiving request $(\hpRI,U_\omega)$,
+  if there is no pending increment, then UTxO is stored in the local state.
+  If there is no current snapshot in flight ($\hats = \bar{\mc S}.s$) and the
+  receiving party $\party_{i}$ is the next snapshot leader, a message to request
+  snapshot signatures $\hpRS$ containing the increment UTxO $U_\omega$ is sent.} \\
+
+\red{\dparagraph{$\mathtt{incrementTx}$.}\quad Upon observing the \mtxIncrement{}
+	transaction, which adds it's outputs to the confirmed UTxO in the Head, the corresponding
+	increment UTxO is cleared and the observed version is used for future
+	snapshots by setting $\hatv = v$. The version of the open head state
+  is incremented on each \mtxIncrement{} transaction as described in Section~\ref{sec:increment-tx}
+}
+\todo{missing to mention the multicast of $\hpRS$} \\
 
 \dparagraph{$\hpRS$.}\quad Upon receiving request
 $(\hpRS,\red{v,}s,\mT_{\mathsf{req}}, \red{\tx_\omega})$\footnote{Snapshot requests