Update offchain prose sections in spec

This also removes the ^ from the Tall variable in spec and code.

hydra-node/src/Hydra/HeadLogic.hs

@@ -238,7 +238,7 @@ data CoordinatedHeadState tx = CoordinatedHeadState
   -- ^ List of transactions applied locally and pending inclusion in a snapshot. Spec: T̂
   , allTxs :: Map.Map (TxIdType tx) tx
   -- ^ Map containing all the transactions ever seen by this node and not yet
-  -- included in a snapshot. Spec: T̂all
+  -- included in a snapshot. Spec: Tall
   , confirmedSnapshot :: ConfirmedSnapshot tx
   -- ^ The latest confirmed snapshot. Spec: U̅, s̅ and σ̅
   , seenSnapshot :: SeenSnapshot tx
@@ -652,7 +652,7 @@ onOpenNetworkReqTx ::
   tx ->
   Outcome tx
 onOpenNetworkReqTx env ledger st ttl tx = do
-  -- Spec: T̂all ← ̂Tall ∪ { (hash(tx), tx) }
+  -- Spec: Tall ← ̂Tall ∪ { (hash(tx), tx) }
   let chs' = coordinatedHeadState{allTxs = allTxs <> fromList [(txId tx, tx)]}
   -- Spec: wait L̂ ◦ tx ≠ ⊥ combined with L̂ ← L̂ ◦ tx
   waitApplyTx chs' $ \utxo' -> do
@@ -673,9 +673,9 @@ onOpenNetworkReqTx env ledger st ttl tx = do
                   { coordinatedHeadState =
                       chs''
                         { seenSnapshot =
-                            -- FIXME: Open point: This state update has no
-                            -- equivalence in the spec. Do we really need to
-                            -- store that we have requested a snapshot?
+                            -- XXX: This state update has no equivalence in the
+                            -- spec. Do we really need to store that we have
+                            -- requested a snapshot? If yes, should update spec.
                             RequestedSnapshot
                               { lastSeen = seenSnapshotNumber seenSnapshot
                               , requested = nextSn
@@ -752,9 +752,9 @@ onOpenNetworkReqSn env ledger st otherParty sn requestedTxIds =
   requireReqSn $
     -- Spec: wait s̅ = ŝ
     waitNoSnapshotInFlight $
-      -- Spec: wait ∀h ∈ Treq : (h, ·) ∈ T̂all
+      -- Spec: wait ∀h ∈ Treq : (h, ·) ∈ Tall
       waitResolvableTxs $ do
-        -- Spec: Treq ← {T̂all [h] | h ∈ Treq#}
+        -- Spec: Treq ← {Tall [h] | h ∈ Treq#}
         let requestedTxs = mapMaybe (`Map.lookup` allTxs) requestedTxIds
         -- Spec: require U̅ ◦ Treq /= ⊥ combined with Û ← Ū̅ ◦ Treq
         requireApplyTxs requestedTxs $ \u -> do
@@ -765,7 +765,7 @@ onOpenNetworkReqSn env ledger st otherParty sn requestedTxIds =
           (Effects [NetworkEffect $ AckSn snapshotSignature sn] `Combined`) $ do
             -- Spec: for loop which updates T̂ and L̂
             let (localTxs', localUTxO') = pruneTransactions u
-            -- Spec: T̂all ← {tx | ∀tx ∈ T̂all : tx ∉ Treq }
+            -- Spec: Tall ← {tx | ∀tx ∈ Tall : tx ∉ Treq }
             let allTxs' = foldr Map.delete allTxs requestedTxIds
             NewState
               ( Open

spec/fig_offchain_prot.tex

@@ -75,7 +75,7 @@
 						\On{$(\hpRT,\tx)$ from $\party_j$}{%
 
 							% track tx in state
-							$\hatmT_{\mathsf{all}} \gets \hatmT_{\mathsf{all}} \cup \{ (\hash(\tx),\tx )\}$
+							$\mT_{\mathsf{all}} \gets \mT_{\mathsf{all}} \cup \{ (\hash(\tx),\tx )\}$
 
 							\Wait{$\hatmL \applytx \tx \neq \bot$}{
 
@@ -98,13 +98,13 @@
 						\Req{$s = \hats + 1 ~ \land ~ \hpLdr(s) = j$} \; %
 
 						% Wait for snapshot no snapshot in flight anymore and all txs applicable
-						\Wait{$\bars = \hats ~ \land ~ \forall h \in  \mT^{\#}_{req} : (h, \cdot) \in \hatmT_{\mathsf{all}}$}{
+						\Wait{$\bars = \hats ~ \land ~ \forall h \in  \mT^{\#}_{req} : (h, \cdot) \in \mT_{\mathsf{all}}$}{
 
-							$\mT_{req} \gets \{ \hatmT_{\mathsf{all}}[h] ~ | ~ \forall h \in \mT^{\#}_{req} \}$
+							$\mT_{\mathsf{req}} \gets \{ \mT_{\mathsf{all}}[h] ~ | ~ \forall h \in \mT^{\#}_{req} \}$
 
-							\Req{$\barmU \applytx \mT_{req} \not= \bot$}
+							\Req{$\barmU \applytx \mT_{\mathsf{req}} \not= \bot$}
 
-							$\hatmU \gets \barmU \applytx \mT_{req}$ \; %
+							$\hatmU \gets \barmU \applytx \mT_{\mathsf{req}}$ \; %
 
 							$\hats \gets \bars + 1$ \; %
 
@@ -117,7 +117,7 @@
 
 							$\Multi{}~(\hpAS,\hats,\msSig_i)$ \; %
 
-							$\forall \tx \in \mT_{req}: \Out~(\hpSeen,\tx)$ \; %
+							$\forall \tx \in \mT_{\mathsf{req}}: \Out~(\hpSeen,\tx)$ \; %
 
 							% TODO: Should we inform users if we drop a transaction?
 							% XXX: This is a bit verbose for the spec
@@ -129,7 +129,7 @@
 								$\hatmL\gets\hatmL\applytx \tx$ \;
 							}
 
-							$\hatmT_{\mathsf{all}} \gets \{ tx ~ | ~ \forall tx \in \hatmT_{\mathsf{all}} : tx \notin \mT_{req} \}$
+							$\mT_{\mathsf{all}} \gets \{ tx ~ | ~ \forall tx \in \mT_{\mathsf{all}} : tx \notin \mT_{\mathsf{req}} \}$
 						}
 					\end{walgo}
 				} &
@@ -160,7 +160,7 @@
 									$\barsigma \gets \msCSig$ \; %
 
 									%$\Out~(\hpSnap,(\bars,\barmU))$ \;  %
-									$\forall \tx \in \mT_{req} : \Out (\hpConf,\tx)$ \; %
+									$\forall \tx \in \mT_{\mathsf{req}} : \Out (\hpConf,\tx)$ \; %
 
 									% issue snapshot if we are leader
 									\If{$\hpLdr(s+1) = i \land \hatmT \neq \emptyset$}{%

spec/offchain.tex

@@ -108,7 +108,7 @@ \subsection{Variables}
 	      applying $\hatmT$ to $\barmU$ 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 $\hatmT_{\mathsf{all}} \in (\tyBytes \times \mT)^{*}$: Associative list of all
+	\item $\mT_{\mathsf{all}} \in (\tyBytes \times \mT)^{*}$: Associative list of all
 	      seen transactions not yet included in a snapshot.
 \end{itemize}
 
@@ -162,42 +162,50 @@ \subsubsection{Processing transactions off-chain}
 results in it being sent out to all parties as a $(\hpRT,\tx)$ message.\\
 
 \dparagraph{$\hpRT$.}\quad Upon receiving request $(\hpRT,\tx)$, the transaction
-gets recorded in $\hatmT$ and $\mT$ and applied to the local \emph{seen} ledger state
-$\hatmL \applytx \tx$. If there is no current snapshot ``in flight''
-($\hats = \bars$) and the receiving party $\party_{i}$ is the next snapshot
+gets recorded in $\mT_{\mathsf{all}}$ and applied to the \emph{local} ledger
+state $\hatmL \applytx \tx$. If not applicable yet, the protocol does $\KwWait$
+to retry later or eventually marks this transaction as invalid (see assumption
+about events piling up). After applying and if there is no current snapshot ``in
+flight'' ($\hats = \bars$) and the receiving party $\party_{i}$ is the next
+snapshot
 leader, a message to request snapshot signatures $\hpRS$ is sent. \\
 
-\dparagraph{$\hpRS$.}\quad Upon receiving request $(\hpRS,s,\mT_{res})$ from
-party $\party_j$, the receiver $\party_i$ checks that $s$ is the next snapshot
-number and that party $\party_j$ is responsible for leading its
-creation.\todo{define $\hpLdr$} Party $\party_i$ then waits until the previous
-snapshot is confirmed ($\bars = \hats$), and all requested transactions have
-been seen ($\mT_{res} \subseteq \mT$). Then all requested transactions $\mT_{res}$
-must be applicable to $\barmU$, otherwise the snapshot is rejected as invalid.
-Only then, $\party_i$ increments their seen-snapshot counter $\hats$, resets the
-signature accumulator $\hatSigma$, and computes the UTxO set $\hatmU$ of the new
-(seen) snapshot as $\hatmU \gets \barmU \applytx \mT_{res}$. Then, $\party_i$
-creates a signature $\msSig_i$ using their signing key $\hydraSigningKey$ on a
-message comprised by \textcolor{red}{the $\cid$, the $\eta_{0}$ corresponding to
-	the initial UTxO set $\Uinit$, and} the new $\eta'$ given by the new snapshot
-number $\hats$ and canonically combining $\hatmU$ (see
-Section~\ref{sec:close-tx} for details). The signature is sent to all head
-members via message $(\hpAS,\hats,\msSig_i)$. Finally, the pending transaction
-set $\hatmT$ gets pruned by the just requested transactions $\mT_{res}$ and the
-local ledger state $\hatmL$ is updated accordingly.\\
-
-\dparagraph{$\hpAS$.}\quad Upon receiving acknowledgment $(\hpAS,s,\msSig_j)$,
-all participants $\Req$ that it is from an expected snapshot (either the last
-seen $\hats$ or + 1), potentially $\KwWait$ for the corresponding $\hpRS$ such
-that $\hats = s$ and $\Req$ that the signature is not yet included in
-$\hatSigma$. They store the received signature in the signature accumulator
-$\hatSigma$, and if signature from each party has been collected, $\party_i$
-aggregates the multisignature $\msCSig$ and $\Req$ it to be valid. If everything
-is fine, the snapshot can be considered confirmed by updating $\bars=s$ and
-participants also store the UTxO set in $\barmU$, as well as the signature in
-$\barsigma$ for later reference. Similar to the $\hpRT$, if $\party_i$ is the
-next snapshot leader and there are already transactions to snapshot in $\hatmT$,
-a corresponding $\hpRS$ is distributed.
+\dparagraph{$\hpRS$.}\quad Upon receiving request
+$(\hpRS,s,\mT_{\mathsf{req}}^{\#})$ from party $\party_j$, the receiver
+$\party_i$ checks that $s$ is the next snapshot number and that party $\party_j$
+is responsible for leading its creation.\todo{define $\hpLdr$} Party $\party_i$
+has to $\KwWait$ until the previous snapshot is confirmed ($\bars = \hats$) and
+all requested transaction hashes $\mT_{\mathsf{req}}^{\#}$ can be resolved in
+$\mT_{\mathsf{all}}$. Then, all those resolved transactions $\mT_{\mathsf{req}}$
+are $\Req$d to be applicable to $\barmU$, otherwise the snapshot is rejected
+as invalid. Only then, $\party_i$ increments their seen-snapshot counter
+$\hats$, resets the signature accumulator $\hatSigma$, and computes the UTxO set
+$\hatmU$ of the new (seen) snapshot as
+$\hatmU \gets \barmU \applytx \mT_{\mathsf{req}}$. Then, $\party_i$ creates a
+signature $\msSig_i$ using their signing key $\hydraSigningKey$ on a message
+comprised by \textcolor{red}{the $\cid$, the $\eta_{0}$ corresponding to the
+	initial UTxO set $\Uinit$, and} the new $\eta'$ given by the new snapshot number
+$\hats$ and canonically combining $\hatmU$ (see Section~\ref{sec:close-tx} for
+details). The signature is sent to all head members via message
+$(\hpAS,\hats,\msSig_i)$. Finally, the pending transaction set $\hatmT$ gets
+pruned by re-applying all locally pending transactions $\hatmT$ to the just
+requested snapshot's UTxO set $\hatmU$ iteratively and ultimately yielding a
+``pruned'' version of $\hatmT$ and $\hatmU$. Also, the set of all transactions
+$\mT_{\mathsf{all}}$ can be reduced by the requested
+transactions $\mT_{\mathsf{req}}$.\\
+
+\dparagraph{$\hpAS$.}\quad Upon receiving acknowledgment $(\hpAS,s,\msSig_j)$, all
+participants $\Req$ that it is from an expected snapshot (either the last seen
+$\hats$ or + 1), potentially $\KwWait$ for the corresponding $\hpRS$ such that
+$\hats = s$ and $\Req$ that the signature is not yet included in $\hatSigma$.
+They store the received signature in the signature accumulator $\hatSigma$, and
+if the signature from each party has been collected, $\party_i$ aggregates the
+multisignature $\msCSig$ and $\Req$ it to be valid. If everything is fine, the
+snapshot can be considered confirmed by updating $\bars=s$ and participants also
+store the UTxO set in $\barmU$, as well as the signature in $\barsigma$ for
+later reference. Similar to the $\hpRT$, if $\party_i$ is the next snapshot
+leader and there are already transactions to snapshot in $\hatmT$, a
+corresponding $\hpRS$ is distributed.
 
 \subsubsection{Closing the head}