Update offchain protocol flow

spec/fig_offchain_prot.tex

@@ -73,7 +73,8 @@
 								$\hatmT \gets \hatmT \cup \{\tx\}$ \;
 								% issue snapshot if we are leader
 								\If{$\hats = \bar{\mc S}.s \land \hpLdr(\bar{\mc S}.s + 1) = i$}{
-                  					\Multi{} $(\hpRS,\red{\hatv,}\bar{\mc S}.s+1,\hatmT,\red{\bot})$ \;
+									\red{$\psi \gets \bot$} \;
+                  					\Multi{} $(\hpRS,\red{\hatv,}\bar{\mc S}.s+1,\hatmT,\red{\psi})$ \;
 								}
 							}
 						}
@@ -137,9 +138,9 @@
 							\Wait{$U_\omega = \bot ~ \land ~ \hatmL \applytx \tx_\omega \not= \bot$}{
 							  $\hatmL \gets \hatmL \setminus \mathsf{inputs}(\tx_\omega)$ \;
 							  $U_\omega \gets \mathsf{outputs}(\tx_\omega)$ \;
-							  $\psi \gets \tx_\omega$ \;
 							  % issue snapshot if we are leader
 							  \If{$\hats = \bar{\mc S}.s \land \hpLdr(\bar{\mc S}.s + 1) = i$}{
+								$\psi \gets \tx_\omega$ \;
 								\Multi{} $(\hpRS,\hatv,\bar{\mc S}.s+1,\hatmT,\psi)$ \;
 							  }
 							}
@@ -150,7 +151,7 @@
 
 						%%% DECREMENT
 						\red{\On{$(\mathtt{decrementTx}, \tx_\omega, v)$ from chain}{
-							\If{$\bar{\mc S}.U_\omega \not= \bot ~ \land ~ \mathsf{outputs}(\tx_\omega) = \bar{\mc S}.U_\omega$}{
+							\If{$U_\omega \not= \bot ~ \land ~ \mathsf{outputs}(\tx_\omega) = \bar{\mc S}.U_\omega$}{
 								$U_\omega \gets \bot$\;
 								$\hatv \gets v$ \;
 								% TODO: always snapshot? not strictly needed (to clear pending decommits)?
@@ -168,9 +169,9 @@
 							\On{$(\mathtt{reqInc},U'_\omega)$ from $\party_j$}{
 								\Wait{$U_\omega = \bot$}{
 									$U_\omega \gets U'_\omega$\;
-									$\psi \gets U'_\omega$ \;
 									% issue snapshot if we are leader
 									\If{$\hats = \bar{\mc S}.s \land \hpLdr(\bar{\mc S}.s + 1) = i$}{
+										$\psi \gets U'_\omega$ \;
 										\Multi{} $(\hpRS,\hatv,\bar{\mc S}.s+1,\hatmT,\psi)$ \;
 									}
 								}
@@ -181,10 +182,10 @@
 
 						%%% 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$}{
+							\If{$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,41 @@ \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. Finally, 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}} \\
+	pending decrement transaction 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 \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
+  another decrement (or increment) is pending to be settled the transaction is
+  rejected. Otherwise the requestd UTxO is kept in the local state ($U_\omega$) 
+  to be posted on-chain in the next snapshot.
+  Finally, 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
+	pending 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
@@ -255,17 +278,19 @@ \subsubsection{Closing the head}
 
 \dparagraph{$\hpClose$.}\quad In order to close a head, a client issues the
 $\hpClose$ input which uses the latest confirmed snapshot $\bar{\mc S}$ to
-create the new $\eta$-state from the last confirmed UTxO set, the digest of
-to-decommit UTxO set $\eta_\omega$, and the certifiate $\xi$ using the corresponding
-multi-signature. With these, the $\mtxClose$ transaction can be constructed and
-posted. See Section~\ref{sec:close-tx} for details about this transaction. \\
+create the new $\eta$-state from the last confirmed UTxO set, \red{the digest of
+either to decrement or to increment UTxO set $\eta_\omega$}, and the certifiate 
+$\xi$ using the corresponding multi-signature. With these, the $\mtxClose$ transaction
+can be constructed and posted. See Section~\ref{sec:close-tx} for details about this
+transaction. \\
 
 \dparagraph{$\mathtt{closeTx}/\mathtt{contestTx}$.}\quad When a party observes
 the head getting closed or contested, the $\eta$-state extracted from the
 \mtxClose{} or \mtxContest{} transaction represents the latest head status that
 has been aggregated on-chain so far (by a sequence of \mtxClose{} and
 \mtxContest{} transactions). If the last confirmed (off-chain) snapshot is newer
-than the observed (on-chain) snapshot number $s_{c}$, an updated $\eta$-state
+than the observed (on-chain) snapshot number $s_{c}$, an updated $\eta$-state, 
+\red{along with the digest of either to decrement or to increment UTxO set $\eta_\omega$},
 and certificate $\xi$ is constructed posted in a \mtxContest{} transaction (see
 Section~\ref{sec:contest-tx}).