Change the statement of Theorem 5.4.3 to exclude ⊥ outputs from SinsemillaHashToPoint.

Previously the proof did not match the statement.

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

protocol/protocol.tex

@@ -8652,8 +8652,8 @@ due to the requirement that $2^n \leq 2^c \leq \frac{\ParamP{r}-1}{2}$. The clai
 
 Let $D \typecolon \byteseqs$ be a personalization input, and let $\ell \typecolon \range{0}{k \mult c}$.
 Finding a collision $M, M' \typecolon \bitseq{\ell}$ with $M \neq M'$ such that
-$\SinsemillaHashToPoint(D, M) = \SinsemillaHashToPoint(D, M')$ efficiently yields a nontrivial
-discrete logarithm relation, and similarly for $\SinsemillaHash(D, M) = \SinsemillaHash(D, M')$.
+$\SinsemillaHashToPoint(D, M) = \SinsemillaHashToPoint(D, M') \neq \bot$ efficiently yields a nontrivial
+discrete logarithm relation, and similarly for $\SinsemillaHash(D, M) = \SinsemillaHash(D, M') \neq \bot$.
 \end{theorem}
 
 \begin{proof}
@@ -8673,8 +8673,10 @@ Since $\ell \in \range{0}{k \mult c}$ we have $n \in \range{0}{c}$. Then:
 This is a Pedersen vector hash of the $\chi(m)$ elements, with a fixed offset $\scalarmult{2^n}{\SinsemillaGenInit(D)}$.
 The fixed offset does not affect \collisionResistance in this context. (See below for why
 it cannot be eliminated for $\SinsemillaHash$, or when using incomplete addition.)
-It follows that the \collisionResistance of $\SinsemillaHash$ can be tightly reduced,
-via the proof in \cite[Appendix A]{BGG1995}, to the Discrete Logarithm Problem over $\GroupP$.
+\theoremref{thmsinsemillaex} will prove that a $\bot$ output from $\SinsemillaHashToPoint$
+yields a nontrivial discrete log relation. It follows that the \collisionResistance of
+$\SinsemillaHashToPoint$ can be tightly reduced, via the proof in \cite[Appendix A]{BGG1995},
+to the Discrete Logarithm Problem over $\GroupP$.
 
 Note that \cite{BGG1995} requires for their main scheme that the scalars are nonzero, which
 is not necessarily the case in our context. However, their proof in Appendix A does not depend
@@ -8682,9 +8684,11 @@ on this, given that $n$ is fixed. The restriction that scalars are nonzero appea
 been motivated by wanting to support variable-length messages and incremental hashing, which
 we do not.
 
-Now we consider $\SinsemillaHash$. We want to prove that, for a given $D$, if we can find two distinct
-messages $M$ and $M'$ such that $\ExtractPbot\big(\SinsemillaHashToPoint(D, M)\kern-0.1em\big) =
-\ExtractPbot\big(\SinsemillaHashToPoint(D, M')\kern-0.1em\big)$ then we can efficiently extract a discrete logarithm.
+Now we consider $\SinsemillaHash$. We want to prove that, for given $D$, if we can find two distinct
+messages $M$ and $M'$ such that $\ExtractPbot\smash{\big(\SinsemillaHashToPoint(D, M)\kern-0.1em\big)} =
+\ExtractPbot\smash{\big(\SinsemillaHashToPoint(D, M')\kern-0.1em\big)} \neq \bot$ then we can efficiently
+extract a discrete logarithm. The inputs to $\ExtractPbot$ are not $\bot$, therefore they are in $\GroupP$.
+$\ExtractPbot$ maps $P, Q \in \GroupP$ to the same output if and only if $P = \pm Q$.
 So either $\SinsemillaHashToPoint(D, M) = \SinsemillaHashToPoint(D, M')$ (in which case use the original Pedersen
 hash proof) or $\SinsemillaHashToPoint(D, M) = -\SinsemillaHashToPoint(D, M')$. In the latter case, let
 $m = \pad_n(M)$ and $m' = \pad_n(M')$, then we have
@@ -8752,6 +8756,9 @@ $|\alpha \mult 2^i| \leq \ParamP{r}-1$ for all $i \in \range{1}{n}$ and $\alpha
 \end{proof}
 
 \vspace{-0.5ex}
+Similarly, a $\bot$ output from $\SinsemillaHash$ yields a nontrivial discrete logarithm relation,
+because $\ExtractPbot$ only returns $\bot$ when its input is $\bot$.
+
 Since by assumption it is hard to find a nontrivial discrete logarithm relation,
 we can argue that it is safe to use incomplete additions when computing Sinsemilla
 inside a circuit.
@@ -14242,6 +14249,10 @@ Peter Newell's illustration of the Jubjub bird, from \cite{Carroll1902}.
     \item Include $\NoteUniqueRand$ as an input to the derivation of
           $\NoteNullifierRand$, $\EphemeralPrivate$, and $\NoteCommitRand$ in \Orchard.
           This was originally intended and as described in \cite[Section 3.5 Nullifiers]{Zcash-Orchard}.
+    \item Change the statement of \theoremref{thmsinsemillacr} to exclude $\bot$ outputs
+          from $\SinsemillaHashToPoint$. This does not affect security given
+          \theoremref{thmsinsemillaex}, but the $\bot$ case is only handled by the latter
+          proof and not the former.
     \item Delegate to \cite{ZIP-316} for the specification of \unifiedPaymentAddresses,
           \unifiedIncomingViewingKeys, and \unifiedFullViewingKeys (\crossref{unifiedencodings}).
     \item Specify that \diversifierIndices for \Orchard \paymentAddresses should be chosen