Spec: Move abort before collect in on-chain chapter

This also removes all samepage/newpage and [h] from figures.

spec/onchain.tex

@@ -89,19 +89,19 @@ \subsection{Init transaction}\label{sec:init-tx}
 
 \noindent The $\muHead(\seed)$ minting policy is the only script that verifies
 init transactions and can be redeemed with either a $\mathsf{mint}$ or
-	$\mathsf{burn}$ redeemer:
+$\mathsf{burn}$ redeemer:
 % TODO: mint redeemer conflicts with mint field
 \begin{itemize}
 	\item When evaluated with the $\mathsf{mint}$ redeemer,
 	      \begin{menumerate}
 		      \item The seed output is spent in this transaction. This guarantees uniqueness of the policy $\cid$ because the EUTxO ledger ensures that $\seed$ cannot be spent twice in the same chain.
 		      $(\seed, \cdot) \in \txInputs$
-          \item All entries of $\txMint$ are of this policy and of single quantity $\forall \{c \mapsto \cdot \mapsto q\} \in \txMint : c = \cid \land q = 1$
+		      \item All entries of $\txMint$ are of this policy and of single quantity $\forall \{c \mapsto \cdot \mapsto q\} \in \txMint : c = \cid \land q = 1$
 		      \item Right number of tokens are minted $|\txMint| = \nop + 1$
-            % TODO: |\txMint| may not be clear to the reader, maybe combine with item above, but be more explicit.
+		      % TODO: |\txMint| may not be clear to the reader, maybe combine with item above, but be more explicit.
 		      \item State token is sent to the head validator $\st \in \valHead$ % TODO: fact that it is goverend by nuHead is a bit implicit here.
 		      \item \textcolor{blue}{The correct number of initial outputs are present $|(\cdot, \nuInitial, \cdot) \in \txOutputs| = n$}
-              % TODO: this is implied by the ledger, so can be removed
+		      % TODO: this is implied by the ledger, so can be removed
 		      \item All participation tokens are sent to the initial validator as an initial output $\forall i \in [1 \dots n] : \{\cid \mapsto \cdot \mapsto 1\} \in \valInitial{i}$
 		      \item The $\datum_{\mathsf{head}}$ contains own currency id $\cid = \cid'$ and the right seed reference $\seed = \seed'$
 		      \item All initial outputs have a $\cid$ as their datum: $\forall i \in [1 \dots n] : \cid = \datumInitial{i}$
@@ -163,13 +163,81 @@ \subsection{Commit Transaction}\label{sec:commit-tx}
 Section~\ref{sec:abort-tx} transaction of the on-chain state machine, selected
 by the appropriate redeemer.
 
-\begin{figure}[h] \centering
+\begin{figure}
+	\centering
 	\includegraphics[width=0.8\textwidth]{figures/commitTx.pdf}
 	\caption{\mtxCom{} transaction spending an initial output and a single
 		committed output, and producing a commit output.}\label{fig:commitTx}
 \end{figure}
 \todo{update with multiple commits}
 
+\subsection{Abort Transaction}\label{sec:abort-tx}
+
+The \mtxAbort{} transaction (see Figure~\ref{fig:abortTx}) allows a
+party to abort the creation of a head and consists of
+\begin{itemize}
+	\item one input spending from $\nuHead$ holding the $\st$ with $\datumHead$,
+	\item $\forall i \in \{1 \dots \nop\}$ inputs either
+	      \begin{itemize}
+		      \item spending from $\nuInitial$ with with $\pt_{i} \in \valInitial{i}$ and $\datumInitial{i} = \cid$, or
+		      \item spending from $\nuCommit$ with with $\pt_{i} \in \valCommit{i}$ and $\datumCommit{i} = (\cid, C_{i})$,
+	      \end{itemize}
+	\item outputs $o_{1} \dots o_{m}$ to redistribute already committed UTxOs.
+\end{itemize}
+
+Note that \mtxAbort{} represents a final transition of the state
+machine and hence there is no state machine output.
+
+\noindent Each spent $\nuInitial$ validator with $\datumInitial{i} = \cid$ and $\redeemerInitial{i} = \mathsf{abort}$ ensures that:
+\begin{menumerate}
+	\item The state token of currency $\cid$ is getting burned $\{\st \mapsto -1\} \subseteq \txMint$.
+\end{menumerate}
+
+\noindent Each spent $\nuCommit$ validator with $\datumCommit{i} = (\cid,\cdot)$ and $\redeemerCommit{i} = \mathsf{abort}$ ensures that:
+\begin{menumerate}
+	\item The state token of currency $\cid$ is getting burned $\{\st \mapsto -1\} \subseteq \txMint$.
+\end{menumerate}
+
+\noindent The $\muHead(\seed)$ minting policy governs the burning of tokens via
+redeemer $\mathsf{burn}$ that:
+\begin{menumerate}
+	\item All tokens in $\txMint$ need to be of negative quantity
+	$\forall \{\cid \mapsto \cdot \mapsto q\} \in \txMint : q < 0$.
+\end{menumerate}
+
+\noindent The state-machine validator $\nuHead$ is spent with
+$\redeemerHead = (\mathsf{abort}, m)$, where $m$ is the number of outputs to
+reimburse, and checks:
+\begin{menumerate}
+	\item State is advanced from $\datumHead \sim \stInitial$ to terminal state
+	$\stFinal$: % XXX: What does this actually mean?
+	\[
+		(\stInitial,\cid,\seed,\hydraKeysAgg,\nop,\cPer) \xrightarrow[m]{\stAbort} \stFinal.
+	\]
+	\item All UTxOs committed into the head are reimbursed exactly as they were
+	committed. This is done by comparing hashes of serialised representations of
+	the $m$ reimbursing outputs $o_{1} \dots o_{m}$\footnote{Only the first $m$
+		outputs are used for reimbursing, while more outputs may be present in the
+		transaction, e.g for returning change.} with the canonically combined
+	committed UTxOs in $C_{i}$:
+	\[
+		\hash(\bigoplus_{j=1}^{m} \bytes(o_{j})) = \combine([C_{i} ~ | ~ \forall [1\dots\nop], C_{i} \neq \bot])
+	\]
+
+	\item Transaction is signed by a participant $\exists \{\cid \mapsto \keyHash_{i} \mapsto -1\} \in \txMint \Rightarrow \keyHash_{i} \in \txKeys$.
+	\item All tokens are burnt
+	$|\{\cid \mapsto \cdot \mapsto -1\} \in \txMint| = \nop + 1$.
+\end{menumerate}
+
+\begin{figure}
+	\centering
+	\includegraphics[width=0.8\textwidth]{figures/abortTx.pdf}
+	\caption{\mtxAbort{} transaction spending the $\stInitial$ state head
+		output and collecting all initial and commit outputs, which get reimbursed
+		by outputs $o_{1} \dots o_{m}$. Note that each $\pt$ may be in either, an
+		initial or commit output.}\label{fig:abortTx}
+\end{figure}
+
 \subsection{CollectCom Transaction}\label{sec:collect-tx}
 
 \noindent The \mtxCCom{} transaction (Figure~\ref{fig:collectComTx}) collects
@@ -227,7 +295,7 @@ \subsection{CollectCom Transaction}\label{sec:collect-tx}
 	$\st \in \valHead'$.
 \end{menumerate}
 
-\begin{figure}[h]
+\begin{figure}
 	\centering
 	\includegraphics[width=0.8\textwidth]{figures/collectComTx.pdf}
 	\caption{\mtxCCom{} transaction spending the head output in $\stInitial$
@@ -279,14 +347,13 @@ \subsection{Increment Transaction}\label{sec:increment-tx}
 	\]
 \end{menumerate}
 
-\begin{figure}[h] \centering
+\begin{figure}
+	\centering
 	\includegraphics[width=0.8\textwidth]{figures/incrementTx.pdf}
 	\caption{\mtxIncrement{} transaction spending an open head output and a single
 		committed output, and producing a new head output.}\label{fig:incrementTx}
 \end{figure}
 
-\newpage
-
 \subsection{Decrement Transaction}\label{sec:increment-tx}
 
 \noindent The \mtxDecrement{} transaction (Figure~\ref{fig:DecrementTx}) allows
@@ -333,81 +400,13 @@ \subsection{Decrement Transaction}\label{sec:increment-tx}
 	\]
 \end{menumerate}
 
-\begin{figure}[h] \centering
+\begin{figure}
+	\centering
 	\includegraphics[width=0.8\textwidth]{figures/decrementTx.pdf}
 	\caption{\mtxDecrement{} transaction spending an open head output,
 		producing a new head output and multiple decommitted outputs.}\label{fig:decrementTx}
 \end{figure}
 
-\subsection{Abort Transaction}\label{sec:abort-tx}
-
-The \mtxAbort{} transaction (see Figure~\ref{fig:abortTx}) allows a
-party to abort the creation of a head and consists of
-\begin{itemize}
-	\item one input spending from $\nuHead$ holding the $\st$ with $\datumHead$,
-	\item $\forall i \in \{1 \dots \nop\}$ inputs either
-	      \begin{itemize}
-		      \item spending from $\nuInitial$ with with $\pt_{i} \in \valInitial{i}$ and $\datumInitial{i} = \cid$, or
-		      \item spending from $\nuCommit$ with with $\pt_{i} \in \valCommit{i}$ and $\datumCommit{i} = (\cid, C_{i})$,
-	      \end{itemize}
-	\item outputs $o_{1} \dots o_{m}$ to redistribute already committed UTxOs.
-\end{itemize}
-
-Note that \mtxAbort{} represents a final transition of the state
-machine and hence there is no state machine output.
-
-\begin{figure}[h]
-	\centering
-	\includegraphics[width=0.8\textwidth]{figures/abortTx.pdf}
-	\caption{\mtxAbort{} transaction spending the $\stInitial$ state head
-		output and collecting all initial and commit outputs, which get reimbursed
-		by outputs $o_{1} \dots o_{m}$. Note that each $\pt$ may be in either, an
-		initial or commit output.}\label{fig:abortTx}
-\end{figure}
-
-\begin{samepage}
-	\noindent The state-machine validator $\nuHead$ is spent with
-	$\redeemerHead = (\mathsf{abort}, m)$, where $m$ is the number of outputs to
-	reimburse, and checks:
-	\begin{menumerate}
-		\item State is advanced from $\datumHead \sim \stInitial$ to terminal state
-		$\stFinal$: % XXX: What does this actually mean?
-		\[
-			(\stInitial,\cid,\seed,\hydraKeysAgg,\nop,\cPer) \xrightarrow[m]{\stAbort} \stFinal.
-		\]
-		\item All UTxOs committed into the head are reimbursed exactly as they were
-		committed. This is done by comparing hashes of serialised representations of
-		the $m$ reimbursing outputs $o_{1} \dots o_{m}$\footnote{Only the first $m$
-			outputs are used for reimbursing, while more outputs may be present in the
-			transaction, e.g for returning change.} with the canonically combined
-		committed UTxOs in $C_{i}$:
-		\[
-			\hash(\bigoplus_{j=1}^{m} \bytes(o_{j})) = \combine([C_{i} ~ | ~ \forall [1\dots\nop], C_{i} \neq \bot])
-		\]
-
-		\item Transaction is signed by a participant $\exists \{\cid \mapsto \keyHash_{i} \mapsto -1\} \in \txMint \Rightarrow \keyHash_{i} \in \txKeys$.
-		\item All tokens are burnt
-		$|\{\cid \mapsto \cdot \mapsto -1\} \in \txMint| = \nop + 1$.
-	\end{menumerate}
-\end{samepage}
-
-\noindent Each spent $\nuInitial$ validator with $\datumInitial{i} = \cid$ and $\redeemerInitial{i} = \mathsf{abort}$ ensures that:
-\begin{menumerate}
-	\item The state token of currency $\cid$ is getting burned $\{\st \mapsto -1\} \subseteq \txMint$.
-\end{menumerate}
-
-\noindent Each spent $\nuCommit$ validator with $\datumCommit{i} = (\cid,\cdot)$ and $\redeemerCommit{i} = \mathsf{abort}$ ensures that:
-\begin{menumerate}
-	\item The state token of currency $\cid$ is getting burned $\{\st \mapsto -1\} \subseteq \txMint$.
-\end{menumerate}
-
-\noindent The $\muHead(\seed)$ minting policy governs the burning of tokens via
-redeemer $\mathsf{burn}$ that:
-\begin{menumerate}
-	\item All tokens in $\txMint$ need to be of negative quantity
-	$\forall \{\cid \mapsto \cdot \mapsto q\} \in \txMint : q < 0$.
-\end{menumerate}
-
 \subsection{Close Transaction}\label{sec:close-tx}
 
 In order to close a head, a head member may post the \mtxClose{} transaction
@@ -418,54 +417,52 @@ \subsection{Close Transaction}\label{sec:close-tx}
 	      datum $\datumHead'$.
 \end{itemize}
 
-\begin{figure}[h]
+\begin{figure}
 	\centering
 	\includegraphics[width=0.8\textwidth]{figures/closeTx.pdf}
 	\caption{\mtxClose{} transaction spending the $\stOpen$ head output and producing a $\stClosed$ head output.}\label{fig:closeTx}
 \end{figure}
 
-\begin{samepage}
-	\noindent The state-machine validator $\nuHead$ is spent with
-	$\redeemerHead = (\mathsf{close}, \xi)$, where $\xi$ is a multi-signature of
-	the to be closed snapshot, and checks:
-	\begin{menumerate}
-		\item State is advanced from $\datumHead \sim \stOpen$ to
-		$\datumHead' \sim \stClosed$, parameters $\cid,\hydraKeysAgg,\nop,\cPer$
-		stay unchanged and the new state is governed again by $\nuHead$:
-		\[
-			(\stOpen,\cid,\hydraKeysAgg,\nop,\cPer,s,\eta) \xrightarrow[\xi]{\stClose} (\stClosed,\cid,\hydraKeysAgg,\nop,\cPer,\eta_0,s',\eta',\textcolor{blue}{\eta_{\omega}},\contesters,\Tfinal)
-		\]
-		\item Records the initial snapshot state $\eta_0 = \eta$. \todo{$\eta \not= \eta_{0}$ anymore with incr/decr}
-		This makes off-chain signatures rollback and replay resistant,
-		see~\ref{sec:rollbacks} for details.
-		\item New snapshot state is the initial $\eta_{0}$
-		or correctly signed by all participants in $\xi$. \\
-		Given the closed snapshot number $s'$,
-		\[
-			\left\{\begin{array}{ll}
-				\msVfy(\hydraKeysAgg,\mathsf{msg},\xi) = \true & \mathrm{if} ~ s' > 0, \\
-				\eta' = \eta_{0}                               & \mathrm{otherwise.}
-			\end{array}\right.
-		\]
-		where $\mathsf{msg}$ is the concatenated bytes of $\cid$, $\eta_{0}$
-		% TODO: η₀ is not yet incorporated
-		and $\eta'$: $\mathsf{msg} = (\cid || s' || \textcolor{red}{\eta_{0} ||} \eta')$.
-		% TODO: detailed CDDL definition of msg
-		\todo{snapshot/msg with pending decommit must work as well}
-		\item Initializes the set of contesters as $\contesters = \emptyset$. \\
-		This allows the closing party to also contest and is required for use
-		cases where pre-signed, valid in the future, close transactions are
-		used to delegate head closing.
-
-		\item Correct contestation deadline is set $\Tfinal = \txValidityMax + T$.
-		\item Transaction validity range is bounded by
-		$\txValidityMax - \txValidityMin \leq T$. \\
-		This ensures the contestation deadline $\Tfinal$ is at most $2*T$ in the future.
-		\item Value in the head is preserved $\valHead' = \valHead$.
-		\item Transaction is signed by a participant $\exists \{\cid \mapsto \keyHash_{i} \mapsto 1\} \in \valHead' \Rightarrow \keyHash_{i} \in \txKeys$.
-		\item No minting or burning $\txMint = \varnothing$.
-	\end{menumerate}
-\end{samepage}
+\noindent The state-machine validator $\nuHead$ is spent with
+$\redeemerHead = (\mathsf{close}, \xi)$, where $\xi$ is a multi-signature of
+the to be closed snapshot, and checks:
+\begin{menumerate}
+	\item State is advanced from $\datumHead \sim \stOpen$ to
+	$\datumHead' \sim \stClosed$, parameters $\cid,\hydraKeysAgg,\nop,\cPer$
+	stay unchanged and the new state is governed again by $\nuHead$:
+	\[
+		(\stOpen,\cid,\hydraKeysAgg,\nop,\cPer,s,\eta) \xrightarrow[\xi]{\stClose} (\stClosed,\cid,\hydraKeysAgg,\nop,\cPer,\eta_0,s',\eta',\textcolor{blue}{\eta_{\omega}},\contesters,\Tfinal)
+	\]
+	\item Records the initial snapshot state $\eta_0 = \eta$. \todo{$\eta \not= \eta_{0}$ anymore with incr/decr}
+	This makes off-chain signatures rollback and replay resistant,
+	see~\ref{sec:rollbacks} for details.
+	\item New snapshot state is the initial $\eta_{0}$
+	or correctly signed by all participants in $\xi$. \\
+	Given the closed snapshot number $s'$,
+	\[
+		\left\{\begin{array}{ll}
+			\msVfy(\hydraKeysAgg,\mathsf{msg},\xi) = \true & \mathrm{if} ~ s' > 0, \\
+			\eta' = \eta_{0}                               & \mathrm{otherwise.}
+		\end{array}\right.
+	\]
+	where $\mathsf{msg}$ is the concatenated bytes of $\cid$, $\eta_{0}$
+	% TODO: η₀ is not yet incorporated
+	and $\eta'$: $\mathsf{msg} = (\cid || s' || \textcolor{red}{\eta_{0} ||} \eta')$.
+	% TODO: detailed CDDL definition of msg
+	\todo{snapshot/msg with pending decommit must work as well}
+	\item Initializes the set of contesters as $\contesters = \emptyset$. \\
+	This allows the closing party to also contest and is required for use
+	cases where pre-signed, valid in the future, close transactions are
+	used to delegate head closing.
+
+	\item Correct contestation deadline is set $\Tfinal = \txValidityMax + T$.
+	\item Transaction validity range is bounded by
+	$\txValidityMax - \txValidityMin \leq T$. \\
+	This ensures the contestation deadline $\Tfinal$ is at most $2*T$ in the future.
+	\item Value in the head is preserved $\valHead' = \valHead$.
+	\item Transaction is signed by a participant $\exists \{\cid \mapsto \keyHash_{i} \mapsto 1\} \in \valHead' \Rightarrow \keyHash_{i} \in \txKeys$.
+	\item No minting or burning $\txMint = \varnothing$.
+\end{menumerate}
 
 \subsection{Contest Transaction}\label{sec:contest-tx}
 
@@ -478,44 +475,42 @@ \subsection{Contest Transaction}\label{sec:contest-tx}
 	      datum $\datumHead'$.
 \end{itemize}
 
-\begin{figure}[h]
+\begin{figure}
 	\centering \includegraphics[width=0.8\textwidth]{figures/contestTx.pdf}
 	\caption{\mtxContest{} transaction spending the $\stClosed$ head output and
 		producing a different $\stClosed$ head output.}\label{fig:contestTx}
 \end{figure}
 
-\begin{samepage}
-	\noindent The state-machine validator $\nuHead$ is spent with
-	$\redeemerHead = (\mathsf{contest}, \xi)$, where $\xi$ is a multi-signature of
-	the contest snapshot, and checks:
-	\begin{menumerate}
-		\item State stays $\stClosed$ in both $\datumHead$ and $\datumHead'$,
-		parameters $\cid,\hydraKeysAgg,\nop,\cPer, \textcolor{red}{\eta_{0}}$ stay
-		unchanged and the new state is governed again by $\nuHead$:
-		\[
-			(\stClosed,\cid,\hydraKeysAgg,\nop,\cPer,\eta_0,s,\eta,\contesters,\Tfinal) \xrightarrow[\xi]{\stContest} (\stClosed,\cid,\hydraKeysAgg,\nop,\cPer,\eta_0,s',\eta',\contesters',\Tfinal')
-		\]
-	  \item Contested snapshot number is newer $s' > s$, where $s$ is the
-		currently stored and $s'$ the snapshot number of the contest snapshot.
-		\item $\xi$ is a valid multi-signature of the new snapshot state
-		$\msVfy(\hydraKeysAgg,(\cid || s' || \textcolor{red}{\eta_{0}} || \eta'),\xi) = \true$. \todo{$\eta_{0}$ replacement}
-		\item The single signer $\{\keyHash\} = \txKeys$ has not already contested
-		$\keyHash \notin \contesters$ and is added to the set of contesters
-		$\contesters' = \contesters \cup \keyHash$.
-		\item Transaction is posted before deadline $\txValidityMax \leq \Tfinal$.
-		\item Contestation deadline is updated correctly to
-		\[
-			\Tfinal' = \left\{\begin{array}{ll}
-				\Tfinal     & \mathrm{if} ~ |\contesters'| = n, \\
-				\Tfinal + T & \mathrm{otherwise.}
-			\end{array}\right.
-		\]
-		\item Transaction is signed by a participant
-		$\exists \{\cid \mapsto \keyHash_{i} \mapsto 1\} \in \valHead' \Rightarrow \keyHash_{i} \in \txKeys$.
-		\item Value in the head is preserved $\valHead' = \valHead$.
-		\item No minting or burning $\txMint = \varnothing$.
-	\end{menumerate}
-\end{samepage}
+\noindent The state-machine validator $\nuHead$ is spent with
+$\redeemerHead = (\mathsf{contest}, \xi)$, where $\xi$ is a multi-signature of
+the contest snapshot, and checks:
+\begin{menumerate}
+	\item State stays $\stClosed$ in both $\datumHead$ and $\datumHead'$,
+	parameters $\cid,\hydraKeysAgg,\nop,\cPer, \textcolor{red}{\eta_{0}}$ stay
+	unchanged and the new state is governed again by $\nuHead$:
+	\[
+		(\stClosed,\cid,\hydraKeysAgg,\nop,\cPer,\eta_0,s,\eta,\contesters,\Tfinal) \xrightarrow[\xi]{\stContest} (\stClosed,\cid,\hydraKeysAgg,\nop,\cPer,\eta_0,s',\eta',\contesters',\Tfinal')
+	\]
+	\item Contested snapshot number is newer $s' > s$, where $s$ is the
+	currently stored and $s'$ the snapshot number of the contest snapshot.
+	\item $\xi$ is a valid multi-signature of the new snapshot state
+	$\msVfy(\hydraKeysAgg,(\cid || s' || \textcolor{red}{\eta_{0}} || \eta'),\xi) = \true$. \todo{$\eta_{0}$ replacement}
+	\item The single signer $\{\keyHash\} = \txKeys$ has not already contested
+	$\keyHash \notin \contesters$ and is added to the set of contesters
+	$\contesters' = \contesters \cup \keyHash$.
+	\item Transaction is posted before deadline $\txValidityMax \leq \Tfinal$.
+	\item Contestation deadline is updated correctly to
+	\[
+		\Tfinal' = \left\{\begin{array}{ll}
+			\Tfinal     & \mathrm{if} ~ |\contesters'| = n, \\
+			\Tfinal + T & \mathrm{otherwise.}
+		\end{array}\right.
+	\]
+	\item Transaction is signed by a participant
+	$\exists \{\cid \mapsto \keyHash_{i} \mapsto 1\} \in \valHead' \Rightarrow \keyHash_{i} \in \txKeys$.
+	\item Value in the head is preserved $\valHead' = \valHead$.
+	\item No minting or burning $\txMint = \varnothing$.
+\end{menumerate}
 
 \subsection{Fan-Out Transaction}
 
@@ -530,7 +525,7 @@ \subsection{Fan-Out Transaction}
 Note that \mtxFanout{} represents a final transition of the state machine and
 hence there is no state machine output.
 
-\begin{figure}[h]
+\begin{figure}
 	\centering
 	\includegraphics[width=0.8\textwidth]{figures/fanoutTx.pdf}
 	\caption{\mtxFanout{} transaction spending the $\stClosed$ head output and