WIP on Sapling statements.

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

protocol/protocol.tex

@@ -737,6 +737,8 @@ electronic commerce and payment, financial privacy, proof of work, zero knowledg
 \newcommand{\AuthProvePublic}{\mathsf{rk}}
 \newcommand{\NotePosition}{\mathsf{pos}}
 \newcommand{\NotePositionBase}{\mathcal{J}}
+\newcommand{\NotePositionTypeSprout}{\range{0}{2^{\MerkleDepthSprout}-1}}
+\newcommand{\NotePositionTypeSapling}{\range{0}{2^{\MerkleDepthSapling}-1}}
 \newcommand{\NullifierRand}{\mathsf{nr}}
 \newcommand{\Hashnr}{H^{\NullifierRand}}
 \newcommand{\Diversifier}{\mathsf{d}}
@@ -883,6 +885,7 @@ electronic commerce and payment, financial privacy, proof of work, zero knowledg
 \newcommand{\OutputIndexType}{\mathsf{OutputIndex}}
 \newcommand{\NoteCommitS}{\mathsf{s}}
 \newcommand{\cv}{\mathsf{cv}}
+\newcommand{\cvOld}[1]{\cv^\mathsf{old}_{#1}}
 \newcommand{\cvNew}[1]{\cv^\mathsf{new}_{#1}}
 \newcommand{\cm}{\mathsf{cm}}
 \newcommand{\cmOld}[1]{\cm^\mathsf{old}_{#1}}
@@ -1209,6 +1212,8 @@ electronic commerce and payment, financial privacy, proof of work, zero knowledg
 % TODO: should this be a named constant?
 \newcommand{\JubjubScalarThreshold}{2^{251}}
 
+\newcommand{\pack}{\mathsf{pack}}
+
 \newcommand{\Acc}{\mathsf{Acc}}
 \newcommand{\Base}{\mathsf{Base}}
 \newcommand{\Addend}{\mathsf{Addend}}
@@ -3476,51 +3481,74 @@ For details of the form and encoding of proofs, see \crossref{phgr}.
 \introsection
 \nsubsubsection{\SpendStatement{} (\Sapling)} \label{spendstatement}
 
-%A valid instance of $\ProofSpend$ assures that given a \term{primary input}:
+A valid instance of $\ProofSpend$ assures that given a \term{primary input}:
 
-\todo{}
+\begin{formulae}
-%\begin{formulae}
+  \item $(\rt \typecolon \MerkleHashSapling,\\
-%  \item $(\rt \typecolon \MerkleHash,\\
+   \hparen\cvOld{} \typecolon \ValueCommitOutput,\\
-%   \hparen\nfOld{\allOld} \typecolon \typeexp{\PRFOutput}{\NOld},\vspace{0.4ex}\\
+   \hparen\nfOld{} \typecolon \GroupJ)$,
-%   \hparen\cmNew{\allNew} \typecolon \typeexp{\NoteCommitSproutOutput}{\NNew},\vspace{0.8ex}\\
+\end{formulae}
-%   \hparen\vpubOld \typecolon \range{0}{2^{64}-1},\vspace{0.4ex}\\
-%   \hparen\vpubNew \typecolon \range{0}{2^{64}-1},\\
-%   \hparen\hSig \typecolon \hSigType,\\
-%   \hparen\h{\allOld} \typecolon \typeexp{\PRFOutput}{\NOld})$,
-%\end{formulae}
 
-%\introlist
+\introlist
-%the prover knows an \term{auxiliary input}:
+the prover knows an \term{auxiliary input}:
-%
-%\begin{formulae}
-%  \item $(\treepath{} \typecolon \typeexp{\MerkleHash}{\MerkleDepthSapling},\\
-%   \hparen\nOld{} \typecolon \NoteTypeSapling,\\
-%   \hparen\AuthProvePrivate \typecolon \bitseq{252})$
-%   \hparen\nNew{\allNew} \typecolon \typeexp{\NoteTypeSapling}{\NNew},\vspace{0.8ex}\\
-%   \hparen\NoteAddressPreRand \typecolon \bitseq{\NoteAddressPreRandLength}
-%\end{formulae}
 
-%where $\nOld{} = (\Diversifier, \DiversifiedTransmitPublic,
+\begin{formulae}
-%\vOld{}, \NoteAddressRandOld{}, \NoteCommitRandOld{})$
+  \item $(\treepath{} \typecolon \typeexp{\MerkleHash}{\MerkleDepthSapling} \times \NotePositionTypeSapling,\\
+   \hparen\nOld{} \typecolon \NoteTypeSapling,\\
+   \hparen\cmOld{} \typecolon \MerkleHashSapling,\\
+   \hparen\ValueCommitRandOld \typecolon \ValueCommitTrapdoor,\\
+   \hparen\DiversifiedTransmitBase \typecolon \KASaplingPublic,\\
+   \hparen\DiversifiedTransmitPublic \typecolon \KASaplingPublic,\\
+   \hparen\NoteCommitRandOld \typecolon \NoteCommitSaplingTrapdoor,\\
+   \hparen\AuthSignPublic \typecolon \KASaplingPublic,\\
+   \hparen\AuthProvePrivate \typecolon \KASaplingPrivate)$
+\end{formulae}
 
-%\introlist
+where $\nOld{} = (\Diversifier, \DiversifiedTransmitPublic, \vOld{}, \NoteCommitRandOld{})$
-%such that the following conditions hold:
 
-%\subparagraph{Merkle path validity} \label{saplingmerklepathvalidity}
+\introlist
+such that the following conditions hold:
 
-%$\treepath{}$ must be a valid \merklePath of depth $\MerkleDepthSapling$, as defined in
+\subparagraph{Note commitment integrity} \label{saplingnotecommitmentintegrity}
-%\crossref{merklepath}, from $\NoteCommitmentSapling(\nOld{})$ to \noteCommitmentTree root $\rt$.
 
-%\subparagraph{\Nullifier{} integrity} \label{saplingnullifierintegrity}
+$\cmOld{} \neq \UncommittedSapling$, and $\pack(\cmOld{}) = \NoteCommitmentSapling(\nOld{})$.
 
-%$\nfOld{} = \scalarmult{\PRFnr{\AuthProvePublic}(\NoteAddressRand)}{\scalarmult{8}{\AuthSignPublic}}$.
+\subparagraph{Merkle path validity} \label{saplingmerklepathvalidity}
 
-%\subparagraph{Spend authority} \label{saplingspendauthority}
+$\treepath{}$ must be a valid \merklePath of depth $\MerkleDepthSapling$, as defined in
+\crossref{merklepath}, from $\cmOld{}$ to \noteCommitmentTree root $\rt$.
 
-%for each $i \in \setofOld$:
+\subparagraph{Value commitment integrity} \label{saplingvaluecommitmentintegrity}
-%$\AuthPublicOld{i} = \PRFaddr{\AuthPrivateOld{i}}(0)$.
 
-%\vspace{2.5ex}
+$\cvOld{} = \ValueCommit{\ValueCommitRandOld{}}(\vOld{})$.
+
+\subparagraph{Point validity checks} \label{saplingpointvalidity}
+
+$\AuthSignPublic, \DiversifiedTransmitBase \in \GroupJ$.
+
+$\scalarmult{8}{\AuthSignPublic} \neq \ZeroJ$.
+
+$\scalarmult{8}{\DiversifiedTransmitBase} \neq \ZeroJ$.
+
+\subparagraph{\Nullifier{} integrity} \label{saplingnullifierintegrity}
+
+
+
+$\nfOld{} = \scalarmult{\PRFnr{\AuthProvePublic}(\NoteAddressRand)}{\scalarmult{8}{\AuthSignPublic}}$.
+
+where
+
+\begin{formulae}
+  \item $\AuthProvePublic = \scalarmult{\AuthProvePrivate}{\AuthProveBase}$
+  \item $\NoteAddressRand = \MixingPedersenHash(\cmOld{}, \NotePosition)$
+\end{formulae}
+
+\subparagraph{Spend authority} \label{saplingspendauthority}
+
+for each $i \in \setofOld$:
+$\AuthPublicOld{i} = \PRFaddr{\AuthPrivateOld{i}}(0)$.
+
+\vspace{2.5ex}
 For details of the form and encoding of \spendStatement proofs, see \crossref{groth}.
 
 \introsection