Tackle the ReqSn explanation

spec/offchain.tex

@@ -216,7 +216,7 @@ \subsubsection{Processing transactions off-chain}
 
 \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$) 
+  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
@@ -231,31 +231,34 @@ \subsubsection{Processing transactions off-chain}
 \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
+$(\hpRS,\red{v,}s,\mT_{\mathsf{req}}, \red{\psi})$\footnote{Snapshot requests
 	with only transaction identifiers are possible too if all parties keep an
 	index of previously seen transactions and their identifiers.} from party
 $\party_j$, the receiver $\party_i$ checks that \red{$v$ refers to the current
 	open state version}\todo{wait or require?}, $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 ($\bar{\mc S}.s = \hats$). \red{If the decommit transaction $\tx_\omega$
-	is not $\bot$, the transaction is $\Req$d to be applicable to the last confirmed
-	UTxO set $\bar{\mc S}.U$ and spent outputs must be removed, yielding the still
-	active UTxO set $U_{\mathsf{active}}$. Then, all requested transactions
-	$\mT_{\mathsf{req}}$ are $\Req$d to be applicable to $U_{\mathsf{active}}$,}
-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 of the new local snapshot as
-$U \gets \red{U_{\mathsf{active}}} \applytx \mT_{\mathsf{req}}$. Then, $\party_i$
-creates a signature $\msSig_i$ using their signing key $\hydraSigningKey$ on a
-message comprised by the $\cid$, the new snapshot number $\hats$, the new $\eta$
-resulting from canonically combining $U$ (see Section~\ref{sec:close-tx} for
-details), \red{and $\eta_\omega$ derived from commit transaction $\tx_\omega$ outputs}.
-The signature is sent to all head members via message $(\hpAS,\hats,\msSig_i)$.
-Finally, the local ledger state $\hatmL$ and pending transaction set $\hatmT$
-get pruned by re-applying all locally pending transactions $\hatmT$ to the just
-requested snapshot's UTxO set iteratively and
-ultimately yielding a ``pruned'' version of $\hatmT$ and $\hatmL$. \\
+  confirmed ($\bar{\mc S}.s = \hats$). \red{If $\psi$
+	is not $\bot$ then we need to either: \\ \\
+  - Check that $\tx_\omega$ transaction is applicable to the last confirmed
+	UTxO set $\hat{\mc S}.U$ and it's inputs are removed, yielding the still
+	active UTxO set $U_{\mathsf{active}}$. \\ \\
+  - Make sure that $U_\omega$ is part of the active UTxO set $U_{\mathsf{active}}$ \\ \\
+  Then, all requested transactions $\mT_{\mathsf{req}}$ are $\Req$d to be applicable
+  to $U_{\mathsf{active}}$,}
+  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 of the new local snapshot as
+  $U \gets \red{U_{\mathsf{active}}} \applytx \mT_{\mathsf{req}}$. Then, $\party_i$
+  creates a signature $\msSig_i$ using their signing key $\hydraSigningKey$ on a
+  message comprised by the $\cid$, the new snapshot number $\hats$, the new $\eta$
+  resulting from canonically combining $U$ (see Section~\ref{sec:close-tx} for
+  details), \red{and $\eta_\omega$ derived from $\psi$}.
+  The signature is sent to all head members via message $(\hpAS,\hats,\msSig_i, \red{\psi})$.
+  Finally, the local ledger state $\hatmL$ and pending transaction set $\hatmT$
+  get pruned by re-applying all locally pending transactions $\hatmT$ to the just
+  requested snapshot's UTxO set iteratively and
+  ultimately yielding a ``pruned'' version of $\hatmT$ and $\hatmL$. \\
 
 \dparagraph{$\hpAS$.}\quad Upon receiving acknowledgment $(\hpAS,s,\msSig_j)$, all
 participants $\Req$ that it is from an expected snapshot (either the last seen
@@ -279,7 +282,7 @@ \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 to decrement or to increment UTxO set $\eta_\omega$}, and the certifiate 
+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. \\
@@ -289,7 +292,7 @@ \subsubsection{Closing the head}
 \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}).