Add specification of Output statement.

Signed-off-by: Daira Hopwood <daira@jacaranda.org>

protocol/protocol.tex

@@ -788,6 +788,7 @@ electronic commerce and payment, financial privacy, proof of work, zero knowledg
 \newcommand{\enc}{\mathsf{enc}}
 \newcommand{\DHSecret}[1]{\mathsf{sharedSecret}_{#1}}
 \newcommand{\EphemeralPublic}{\mathsf{epk}}
+\newcommand{\EphemeralPublicRepr}{\Repr{\EphemeralPublic}}
 \newcommand{\EphemeralPrivate}{\mathsf{esk}}
 \newcommand{\TransmitPublic}{\mathsf{pk_{enc}}}
 \newcommand{\TransmitPublicSup}[1]{\mathsf{pk}^{#1}_\mathsf{enc}}
@@ -3751,8 +3752,60 @@ For details of the form and encoding of \spendStatement proofs, see \crossref{gr
 \introsection
 \subsubsection{\OutputStatement{} (\Sapling)} \label{outputstatement}
 
-\todo{}
+A valid instance of $\ProofOutput$ assures that given a \primaryInput:
 
+\begin{formulae}
+  \item $(\cvNew{} \typecolon \ValueCommitOutput,\\
+   \hparen\cmNew{} \typecolon \NoteCommitSaplingOutput,\\
+   \hparen\EphemeralPublic \typecolon \GroupJ)$,
+\end{formulae}
+
+\introlist
+the prover knows an \auxiliaryInput:
+
+\begin{formulae}
+  \item $(\DiversifiedTransmitBaseRepr \typecolon \bitseq{\ellJ},\\
+   \hparen\DiversifiedTransmitPublicRepr \typecolon \bitseq{\ellJ},\\
+   \hparen\vNew{} \typecolon \range{0}{2^{64}-1},\\
+   \hparen\ValueCommitRandNew{} \typecolon \ValueCommitTrapdoor,\\
+   \hparen\NoteCommitRandNew{} \typecolon \NoteCommitSaplingTrapdoor,\\
+   \hparen\EphemeralPrivate \typecolon \range{0}{2^{252}-1})$
+\end{formulae}
+
+\introlist
+such that the following conditions hold:
+
+\snarkcondition{Note commitment integrity} \label{outputnotecommitmentintegrity}
+
+$\pack(\cmNew{}) = \NoteCommitSapling{\NoteCommitRandNew{}}(\DiversifiedTransmitBaseRepr,
+                                                            \DiversifiedTransmitPublicRepr,
+                                                            \vNew{})$.
+
+\todo{define $\pack$.}
+
+\snarkcondition{Value commitment integrity} \label{outputvaluecommitmentintegrity}
+
+$\cvNew{} = \ValueCommit{\ValueCommitRandNew{}}(\vNew{})$.
+
+\snarkcondition{Point validity checks} \label{outputpointvalidity}
+
+$\DiversifiedTransmitBase \in \GroupJ$ and is not of small order,
+i.e.\ $\scalarmult{8}{\DiversifiedTransmitBase} \neq \ZeroJ$, where
+
+\begin{formulae}
+  \item $\DiversifiedTransmitBase = \abstJOf{\DiversifiedTransmitBaseRepr}$.
+\end{formulae}
+
+\snarkcondition{Ephemeral public key integrity} \label{outputepkintegrity}
+
+$\EphemeralPublic = \scalarmult{\EphemeralPrivate}{\DiversifiedTransmitBase}$ where
+
+\begin{formulae}
+  \item $\EphemeralPublic = \abstJOf{\EphemeralPublicRepr}$.
+\end{formulae}
+
+
+\vspace{2.5ex}
 For details of the form and encoding of \outputStatement proofs, see \crossref{groth}.
 } %sapling
 
@@ -7556,6 +7609,7 @@ Daira Hopwood, Sean Bowe, and Jack Grigg.
     \item Updates to transaction format and consensus rules for Overwinter and Sapling.
 } %nuzero
 \sapling{
+    \item Add specification of the \outputStatement.
     \item Change $\MerkleDepthSapling$ from $29$ to $32$.
     \item Updates to \Sapling construction, changing how the \nullifier is
           computed and separating it from the \authRandomizedVerifyingKey