WIP

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,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