Incremental commits spec changes

.github/workflows/ci-nix.yaml

@@ -17,7 +17,7 @@ jobs:
       uses: actions/checkout@v4
 
     - name: ❄ Prepare nix
-      uses: cachix/install-nix-action@V27
+      uses: cachix/install-nix-action@v30
       with:
         extra_nix_config: |
           accept-flake-config = true

src/Hydra/Protocol/Figures/head-protocol-states.tex

@@ -1,7 +1,7 @@
 \begin{figure}[t!]
   \centering
   \begin{tikzpicture}[>=stealth,auto,node distance=2.8cm, initial text=$\mathsf{deposit}$, every
-    state/.style={text width=10mm, align=center}, color=red]
+    state/.style={text width=10mm, align=center}]
     \node[state, initial, text width=12mm] (pending) {$\mathsf{pending}$};
     \node[state, accepting] (final) [right of=pending] {$\mathsf{final}$};
 
@@ -19,7 +19,7 @@
 
     \path[->] (initial) edge [bend left=20] node {$\stCollect$} (open);
     \path[->] (open) edge [bend left=20] node {$\stClose$} (closed);
-    \path[->] (open) edge [loop above, color=red] node {$\mathsf{increment}$} (open);
+    \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);

src/Hydra/Protocol/Figures/offchain-protocol.tex

@@ -48,11 +48,11 @@
 							$\Uinit \gets \bigcup_{j=1}^{n} U_j$ \;
 							% $\Out~(\hpSnap,(0,U_0))$ \;
 							$\hatmL \gets \Uinit$ \;
-							$\bar{\mc S} \gets \blue{\Sno(0, 0, [], \Uinit, \emptyset \red{, \emptyset})}$ \;
+							$\bar{\mc S} \gets \blue{\Sno(0, 0, [], \Uinit, \emptyset , \emptyset)}$ \;
 							$\hatv, \hats \gets 0$ \;
 							$\hatmT \gets \emptyset$ \;
 							$\tx_\omega \gets \bot$ \;
-							\red{$U_\alpha \gets \emptyset$ \;}
+							$U_\alpha \gets \emptyset$ \;
 						}
 
 					\end{walgo}
@@ -75,45 +75,43 @@
 								$\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,\hatv,\bar{\mc S}.s+1,\hatmT, \red{U_\alpha}, \tx_\omega)$ \;
+									\Multi{} $(\hpRS,\hatv,\bar{\mc S}.s+1,\hatmT, U_\alpha, \tx_\omega)$ \;
 								}
 							}
 						}
 						\vspace{12pt}
 
 						%%% REC DEC
 						\On{$(\mathtt{reqDec},\tx)$ from $\party_j$}{
-							\Wait{$\red{U_{\alpha} = \emptyset ~ \land ~}\tx_\omega  = \bot ~ \land ~ \hatmL \applytx \tx \ne \bot$}{
+							\Wait{$U_{\alpha} = \emptyset ~ \land ~\tx_\omega  = \bot ~ \land ~ \hatmL \applytx \tx \ne \bot$}{
 								$\hatmL \gets \hatmL \applytx \tx \setminus \mathsf{outputs}(\tx)$ \;
 								$\tx_\omega \gets \tx$ \;
 								% issue snapshot if we are leader
 								\If{$\hats = \bar{\mc S}.s \land \hpLdr(\bar{\mc S}.s + 1) = i$}{
-									\Multi{} $(\hpRS,\hatv,\bar{\mc S}.s+1,\hatmT, \red{U_\alpha},\tx_\omega)$ \;
+									\Multi{} $(\hpRS,\hatv,\bar{\mc S}.s+1,\hatmT, U_\alpha,\tx_\omega)$ \;
 								}
 							}
 						}
 						\vspace{12pt}
 
 						%%% DEPOSIT
-						\red{
-							\On{$(\mathtt{depositTx}, U)$ from chain}{
-							  % FIXME: wait on chain events is a bit weird. Wait
-							  % in general feels like avoiding book keeping and
-							  % relying a lot on assumption of a perfect queue
-							  \Wait{$\tx_\omega = \bot ~ \land ~ U_{\alpha} = \emptyset$}{
-								$U_{\alpha} = U$ \;
-								% issue snapshot if we are leader
-								\If{$\hats = \bar{\mc S}.s \land \hpLdr(\bar{\mc S}.s + 1) = i$}{
-								  \Multi{} $(\hpRS,\hatv,\bar{\mc S}.s+1,\hatmT, \red{U_\alpha}, \tx_\omega)$ \;
-								}
-							  }
-							}
-						}
+					    \On{$(\mathtt{depositTx}, U)$ from chain}{
+					      % FIXME: wait on chain events is a bit weird. Wait
+					      % in general feels like avoiding book keeping and
+					      % relying a lot on assumption of a perfect queue
+					      \Wait{$\tx_\omega = \bot ~ \land ~ U_{\alpha} = \emptyset$}{
+					    	$U_{\alpha} = U$ \;
+					    	% issue snapshot if we are leader
+					    	\If{$\hats = \bar{\mc S}.s \land \hpLdr(\bar{\mc S}.s + 1) = i$}{
+					    	  \Multi{} $(\hpRS,\hatv,\bar{\mc S}.s+1,\hatmT, U_\alpha, \tx_\omega)$ \;
+					    	}
+					      }
+					    }
 						\vspace{12pt}
 
 						%%% REQ SN
-						\On{$(\hpRS,v,s,\underline{\tx}_{\mathsf{req}} \red{, U_\alpha} , \tx_\omega)$ from $\party_j$}{
-							\red{\Req{$\tx_\omega = \bot ~ \lor ~ U_\alpha = \emptyset$}} \;
+						\On{$(\hpRS,v,s,\underline{\tx}_{\mathsf{req}} , U_\alpha , \tx_\omega)$ from $\party_j$}{
+							\Req{$\tx_\omega = \bot ~ \lor ~ U_\alpha = \emptyset$} \;
 							\Req{$v = \hatv ~ \land ~ s = \hats + 1 ~ \land ~ \hpLdr(s) = j$} \;
 							\Wait{$\hats = \bar{\mc S}.s$}{
 								\blue{
@@ -125,9 +123,9 @@
 								$\hats \gets s$ \;
 								% TODO: DRY message creation
 								$\eta \gets \combine(U)$ \;
-								\red{$\eta_\alpha \gets \mathsf{combine}(U_\alpha)$ \;}
+								$\eta_\alpha \gets \mathsf{combine}(U_\alpha)$ \;
 								$\eta_\omega \gets \mathsf{combine}(\mathsf{outputs}(\tx_\omega))$ \;
-								$\msSig_i \gets \msSign(\hydraSigningKey, (\cid || v || \hats || \eta \red{ || \eta_\alpha} || \eta_\omega))$ \;
+								$\msSig_i \gets \msSign(\hydraSigningKey, (\cid || v || \hats || \eta || \eta_\alpha || \eta_\omega))$ \;
 								% TODO: use a seen snapshot to keep track of things easier
 								$\hatSigma \gets \emptyset$ \;
 								$\Multi{}~(\hpAS,\hats,\msSig_i)$ \;
@@ -161,30 +159,30 @@
 									% TODO: DRY message creation
 									$\eta \gets \combine(\hatmU)$ \;
 
-									\red{$\eta_\alpha \gets \mathsf{combine}(U_\alpha)$ \;}
+									$\eta_\alpha \gets \mathsf{combine}(U_\alpha)$ \;
 									$U_\omega \gets \mathsf{outputs}(\tx_\omega)$ \;
 									$\eta_\omega \gets \mathsf{combine}(U_\omega)$ \;
 									% NOTE: Implementation differs here and
 									% below as it stores seen version in seen
 									% snapshot and uses that to verify
-									\Req{} $\msVfy(\hydraKeysAgg, (\cid || \blue{\hatv ||} \hats || \eta \red{|| \eta_\alpha} || \eta_\omega), \msCSig)$ \;
+									\Req{} $\msVfy(\hydraKeysAgg, (\cid || \blue{\hatv ||} \hats || \eta || \eta_\alpha || \eta_\omega), \msCSig)$ \;
 									% create confirmed snapshot for later reference
 									\blue{$\bar{\mc S} \gets \Sno(\hatv, \hats, \hatmT, \hatmU, U_\alpha, U_\omega)$ \;}
 									$\bar{\mc S}.\sigma \gets \msCSig$ \;
 									%$\Out~(\hpSnap,(\bar{\mc S}.s,\bar{\mc S}.U))$ \;
 									$\forall \tx \in \mT_{\mathsf{req}} : \Out (\hpConf,\tx)$ \;
 
 									\If{${\bar S}.U_\omega \ne \bot$}{
-										$\PostTx{}~(\mathtt{decrementTx}, \hatv, \hats, \eta, \red{\eta_\alpha}, \eta_\omega)$ \;
+										$\PostTx{}~(\mathtt{decrementTx}, \hatv, \hats, \eta, \eta_\alpha, \eta_\omega)$ \;
 									}
 
-									\red{\If{${\bar S}.U_\alpha \ne \bot$}{
-										$\PostTx{}~(\mathtt{incrementTx}, \hatv, \hats, \eta, \red{\eta_\alpha}, \eta_\omega)$ \;
-									}}
+									\If{${\bar S}.U_\alpha \ne \bot$}{
+										$\PostTx{}~(\mathtt{incrementTx}, \hatv, \hats, \eta, \eta_\alpha, \eta_\omega)$ \;
+									}
 
 									% issue snapshot if we are leader
 									\If{$\hpLdr(s+1) = i \land \hatmT \neq \emptyset$}{
-										\Multi{} $(\hpRS,\hatv,\bar{\mc S}.s+1, \hatmT \red{, U_\alpha}, \tx_\omega)$ \;
+										\Multi{} $(\hpRS,\hatv,\bar{\mc S}.s+1, \hatmT , U_\alpha, \tx_\omega)$ \;
 									}
 								}
 							}
@@ -201,14 +199,14 @@
 						\vspace{12pt}
 
 						%%% INCREMENT
-						\red{\On{$(\mathtt{incrementTx}, U, v)$ from chain}{
+						\On{$(\mathtt{incrementTx}, U, v)$ from chain}{
 							% XXX: require?
 							\If{$U_\alpha = U$}{
 								$\hatmL \gets \hatmL \cup U$ \;
 								$U_\alpha \gets \emptyset$\;
 								$\hatv \gets v$ \;
 							}
-						}}
+						}
 
 					\end{walgo}
 				}
@@ -231,11 +229,11 @@
 					% CLOSE from client
 					\On{$(\hpClose)$ from client}{
 						$\eta \gets \combine(\bar{\mc S}.U)$ \;
-						\red{$\eta_\alpha \gets \combine(\bar{\mc S}.U_\alpha$) \;}
+						$\eta_\alpha \gets \combine(\bar{\mc S}.U_\alpha$) \;
 						$\eta_\omega \gets \combine(\bar{\mc S}.U_\omega)$ \;
 						$\xi \gets \bar{\mc S}.\sigma$ \;
 						% XXX: \hatv needed to distinguish between CloseType redeemer, explain how exactly?
-						$\PostTx{}~(\mtxClose, \hatv, \bar{\mc S}.v, \bar{\mc S}.s, \eta \red{, \eta_\alpha}, \eta_\omega, \xi)$ \;
+						$\PostTx{}~(\mtxClose, \hatv, \bar{\mc S}.v, \bar{\mc S}.s, \eta , \eta_\alpha, \eta_\omega, \xi)$ \;
 					}
 				\end{walgo}
 			}
@@ -245,11 +243,11 @@
 					\On{$(\gcChainClose, \eta) \lor (\gcChainContest, s_{c}, \eta)$ from chain}{
 						\If{$\bar{\mc S}.s > s_{c}$}{
 							$\eta \gets \combine(\bar{\mc S}.U)$ \;
-							\red{$\eta_\alpha \gets \combine(\bar{\mc S}.U_\alpha$) \;}
+							$\eta_\alpha \gets \combine(\bar{\mc S}.U_\alpha$) \;
 							$\eta_\omega \gets \combine({\bar{\mc S}.U_\omega})$ \;
 							$\xi \gets \bar{\mc S}.\sigma$ \;
 							% XXX: \hatv needed to distinguish between CloseType redeemer, explain how exactly?
-							$\PostTx{}~(\mtxContest, \hatv, \bar{\mc S}.v, \bar{\mc S}.s, \eta \red{, \eta_\alpha}, \eta_\omega , \xi)$ \;
+							$\PostTx{}~(\mtxContest, \hatv, \bar{\mc S}.v, \bar{\mc S}.s, \eta , \eta_\alpha, \eta_\omega , \xi)$ \;
 						}
 					}
 				\end{walgo}

src/Hydra/Protocol/Main.lagda

@@ -20,8 +20,6 @@
 
 \begin{code}[hide]
 module Hydra.Protocol.Main where
-
-open import Hydra.Protocol.Throwaway
 \end{code}
 
 \input{Hydra/Protocol/Introduction}
@@ -31,7 +29,6 @@ open import Hydra.Protocol.Throwaway
 \input{Hydra/Protocol/OnChain}
 \input{Hydra/Protocol/OffChain}
 \input{Hydra/Protocol/Security}
-\input{Hydra/Protocol/Throwaway}
 
 \bibliographystyle{plain}
 \bibliography{short}

src/Hydra/Protocol/OffChain.tex

@@ -17,8 +17,8 @@ \section{Off-Chain Protocol}\label{sec:offchain}
     \item $\mathtt{initialTx}$: initiates a head
     \item $\mathtt{commitTx}$: commits UTxO to an initializing head
     \item $\mathtt{collectComTx}$: opens a head
-    \item \red{$\mathtt{depositTx}$: prepares UTxO to be incremented}
-    \item \red{$\mathtt{incrementTx}$: adds UTxO to an open head}
+    \item $\mathtt{depositTx}$: prepares UTxO to be incremented
+    \item $\mathtt{incrementTx}$: adds UTxO to an open head
     \item $\mathtt{decrementTx}$: removes UTxO from an open head
     \item $\mathtt{closeTx}$: closes a head
     \item $\mathtt{contestTx}$: contests a closed head
@@ -114,7 +114,7 @@ \subsection{Variables}
         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_\alpha \in {(\txInputs \times \txOutputs)}^{*}$: UTxO set pending to be added to the head.}
+  \item $U_\alpha \in {(\txInputs \times \txOutputs)}^{*}$: UTxO set pending to be added to the head.
   \item $\tx_\omega \in \mathcal{T}$: Pending decrement transaction, whose outputs are to be
         withdrawn from the head.
   \item $\bar{\mc S}$: Snapshot object of the latest confirmed snapshot which
@@ -125,12 +125,12 @@ \subsection{Variables}
             $\bar{\mc S}.s$         & snapshot number \\ \hline
             $\bar{\mc S}.\mT$       & list of transactions relating this snapshot to the previous \\ \hline
             $\bar{\mc S}.U$         & snapshotted UTxO set \\ \hline
-            \red{$\bar{\mc S}.U_\alpha$} & \red{pending UTxO to increment} \\ \hline
+            $\bar{\mc S}.U_\alpha$ & pending UTxO to increment \\ \hline
             $\bar{\mc S}.U_\omega$       & pending UTxO to decrement \\ \hline
             $\bar{\mc S}.\sigma$         & multisignature \\ \hline
           \end{tabular}
         \end{center}
-        where constructor $\Sno(v,n,\mT,U,\red{U_\alpha}, U_\omega)$ initializes a new snapshot object with $\bar{\mc S}.\sigma = \emptyset$.
+        where constructor $\Sno(v,n,\mT,U,U_\alpha, U_\omega)$ initializes a new snapshot object with $\bar{\mc S}.\sigma = \emptyset$.
 \end{itemize}
 
 \subsection{Protocol flow}
@@ -164,9 +164,9 @@ \subsubsection{Initializing the head}
 transaction, the parties compute $\Uinit \gets \bigcup_{j=1}^{n} C_j$ using previously
 observed $C_j$ and initialize $\hatmL = \Uinit$. The seen transaction set is
 initialized empty $\hatmT = \emptyset$, seen head state version $\hatv = 0$, as well as
-snapshot number $\hats = 0$. No \red{UTxO to increment $U_{\alpha} = \emptyset$ and no}
+snapshot number $\hats = 0$. No UTxO to increment $U_{\alpha} = \emptyset$ and no
 decrement transaction $\tx_{\omega} = \bot$ is pending, and the last confirmed snapshot
-is initialized accordingly $\bar{\mc S} \gets \blue{\Sno(0, 0, [], \Uinit, \red{\emptyset}, \emptyset)}$.
+is initialized accordingly $\bar{\mc S} \gets \blue{\Sno(0, 0, [], \Uinit, \emptyset, \emptyset)}$.
 
 \subsubsection{Processing transactions off-chain}
 
@@ -196,22 +196,22 @@ \subsubsection{Processing transactions off-chain}
 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{depositTx}$.}\quad Upon observing a \mtxDeposit{}
+\dparagraph{$\mathtt{depositTx}$.}\quad Upon observing a \mtxDeposit{}
   transaction as settled\footnote{Protocol actors might use different techniques
     and delays to determine transaction finality. See also~\ref{sec:rollbacks}.}
   and no other commit or decommit is pending still, each party keeps track of
   the observed deposited UTxO as the pending increment UTxO set $U_{\alpha} = U$. If
   other commits or decommits are pending, the protocol $\KwWait$s and retries
   updating state later.\todo{smelly and fragile} If the observing party is the
   next snapshot leader, it may request a new snapshot by sending a $\hpRS$
-  including the UTxO to increment $U_{\alpha}$.}  \\
+  including the UTxO to increment $U_{\alpha}$.  \\
 
 \dparagraph{$\hpRS$.}\quad Upon receiving request
-$(\hpRS,v,s,\underline{\tx}_{\mathsf{req}}, \red{U_\alpha}, \tx_\omega)$\footnote{Snapshot
+$(\hpRS,v,s,\underline{\tx}_{\mathsf{req}}, U_\alpha, \tx_\omega)$\footnote{Snapshot
   requests with only transaction identifiers and output references are possible
   if all parties keep an index of previously seen transactions and their
   identifiers.} from party $\party_j$, the receiving $\party_i$ $\Req$s
-\red{that only a commit or decommit is currently pending, and} that $v$ refers
+  that only a commit or decommit is currently pending, and that $v$ refers
 to the current open state version, $s$ is the next snapshot number and that
 party $\party_j$ is responsible for leading its creation.\todo{define $\hpLdr$}
 Party $\party_i$ may has to $\KwWait$ until the previous snapshot is confirmed
@@ -244,7 +244,7 @@ \subsubsection{Processing transactions off-chain}
 multisignature $\msCSig$ and $\Req$ it to be valid (constructing the signed
 message as in $\hpRS$). If everything is fine, the snapshot can be considered
 confirmed by creating the snapshot object
-$\bar{\mc S} \gets \Sno(\hatv, \hats, \hatmT, \hatmU, \red{U_{\alpha},} \mathsf{outputs}(\tx_{\omega}))$
+$\bar{\mc S} \gets \Sno(\hatv, \hats, \hatmT, \hatmU, U_{\alpha}, \mathsf{outputs}(\tx_{\omega}))$
 and storing the multi-signature $\msCSig$ in it for later reference. In case
 there is a pending decommit, any participant can now submit a \mtxDecrement{}
 transaction by providing the just confirmed snapshot with its digests of the
@@ -262,20 +262,20 @@ \subsubsection{Processing transactions off-chain}
 is incremented on each \mtxDecrement{} transaction as described in
 Section~\ref{sec:decrement-tx}. \\
 
-\red{\dparagraph{$\mathtt{incrementTx}$.}\quad Upon observing the \mtxIncrement{}
+\dparagraph{$\mathtt{incrementTx}$.}\quad Upon observing the \mtxIncrement{}
   transaction, which added outputs $U$ to the head, the local ledger state
   $\hatmL$ is extended with the newly addded UTxO while the pending increment
   state $U_{\alpha}$ is cleared. Also the observed version $v$ is used for future
   snapshots by setting $\hatv = v$. Note that the version of the open head state
   is incremented on each \mtxIncrement{} transaction as described in
-  Section~\ref{sec:increment-tx}}
+  Section~\ref{sec:increment-tx}
 
 \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, \red{the digest of
-either increment or decrement UTxO set ($\eta_\alpha$ or $\eta_\omega$)}, and the certifiate
+create the new $\eta$-state from the last confirmed UTxO set, the digest of
+either increment or decrement UTxO set ($\eta_\alpha$ or $\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. \\
@@ -286,7 +286,7 @@ \subsubsection{Closing the head}
 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,
-\red{along with the digest of either increment or decrement UTxO set ($\eta_\alpha$ or $\eta_\omega$)},
+along with the digest of either increment or decrement UTxO set ($\eta_\alpha$ or $\eta_\omega$),
 and certificate $\xi$ is constructed and posted in a \mtxContest{} transaction (see
 Section~\ref{sec:contest-tx}).