NCC audit: Propagate \bot from the inputs of MerkleCRH^Orchard to its output, and add an explicit

consensus rule that rt^Orchard computed from appending a note commitment is not \bot.

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

protocol/protocol.tex

@@ -3326,6 +3326,17 @@ In a given \blockChain, \sapling{for each of \Sprout and \SaplingAndOrchard,}
 \sapling{There is no equivalent of interstitial \treestates for \Sapling\nufive{ or
 for \Orchard}.}
 
+\nufive{
+\vspace{1ex}
+$\MerkleCRH{Orchard}$ can produce $\bot$ as output (with insignificant probability).
+If either input is $\bot$, this is propagated to the output, and so if any \merkleNode
+of a \noteCommitmentTree is $\bot$, then the \merkleRoot of that tree will be $\bot$.
+
+\vspace{-1ex}
+\consensusrule{The \merkleRoot of the \Orchard \noteCommitmentTree \MUSTNOT be $\bot$
+in any (intermediate or output) \treestate created by a \block.}
+} %nufive
+
 
 \lsubsection{JoinSplit Transfers and Descriptions}{joinsplit}
 
@@ -3624,13 +3635,14 @@ The following \hashFunctions are used in \crossref{merklepath}:
 
 \begin{tabular}{@{\hskip 2em}l@{\;}l@{\;}l@{\;}l@{\;}l}
 $\MerkleCRH{Sprout}$              &$\typecolon\, \MerkleLayer{Sprout}$ &$\times\; \MerkleHash{Sprout}$ &$\times\; \MerkleHash{Sprout}$ &$\rightarrow \MerkleHash{Sprout}$ \\
-\setsapling $\MerkleCRH{Sapling}$ &\setsapling $\typecolon\, \MerkleLayer{Sapling}$ &\setsapling $\times\; \MerkleHash{Sapling}$ &\setsapling $\times\; \MerkleHash{Sapling}$ &\setsapling $\rightarrow \MerkleHash{Sapling}$\notnufive{.} \\
-\setnufive  $\MerkleCRH{Orchard}$ &\setnufive  $\typecolon\, \MerkleLayer{Orchard}$ &\setnufive  $\times\; \MerkleHash{Orchard}$ &\setnufive  $\times\; \MerkleHash{Orchard}$ &\setnufive  $\rightarrow \MerkleHash{Orchard}$.
+\setsapling $\MerkleCRH{Sapling}$ &\setsapling $\typecolon\, \MerkleLayer{Sapling}$ &\setsapling $\times\; \MerkleHash{Sapling}$ &\setsapling $\times\; \MerkleHash{Sapling}$ &\setsapling $\rightarrow \MerkleHash{Sapling}$\notbeforenufive{ \\
+\setnufive  $\MerkleCRH{Orchard}$ &\setnufive  $\typecolon\, \MerkleLayer{Orchard}$ &\setnufive  $\times\; \maybe{\MerkleHash{Orchard}}$ &\setnufive  $\times\; \maybe{\MerkleHash{Orchard}}$ &\setnufive  $\rightarrow \maybe{\MerkleHash{Orchard}}$}.
 \end{tabular}
 
 $\MerkleCRH{Sprout}$ is \collisionResistant except on its first argument.
 \sapling{$\MerkleCRH{Sapling}$\notnufive{ is}\nufive{ and $\MerkleCRH{Orchard}$ are}
-\collisionResistant on all\notnufive{ its}\nufive{ their} arguments.}
+\collisionResistant on all\notnufive{ its}\nufive{ their} arguments\nufive{ (restricted
+to non-$\bot$ inputs in the case of $\MerkleCRH{Orchard}$)}.}
 
 These functions are instantiated in \crossref{merklecrh}.
 
@@ -7833,12 +7845,15 @@ but using a prefix that cannot collide with a layer prefix, as noted in \crossre
 \vspace{-2ex}
 Let $\SinsemillaHash$ be as specified in \crossref{concretesinsemillahash}.
 
-$\MerkleCRH{Orchard} \typecolon \MerkleLayer{Orchard} \times \MerkleHash{Orchard} \times \MerkleHash{Orchard}
-\rightarrow \MerkleHash{Orchard}$ is defined as follows:
+$\MerkleCRH{Orchard} \typecolon \MerkleLayer{Orchard} \times \maybe{\MerkleHash{Orchard}} \times \maybe{\MerkleHash{Orchard}}
+\rightarrow \maybe{\MerkleHash{Orchard}}$ is defined as follows:
 
 \begin{formulae}
-  \item $\MerkleCRH{Orchard}(\mathsf{layer}, \mathsf{left}, \mathsf{right}) := \SinsemillaHash(\ascii{z.cash:Orchard-MerkleCRH},
-           l \bconcat \mathsf{left} \bconcat \mathsf{right})$
+  \item $\MerkleCRH{Orchard}(\mathsf{layer}, \mathsf{left}, \mathsf{right}) := \begin{cases}
+           \bot, &\caseif \mathsf{left} = \bot \text{ or } \mathsf{right} = \bot \\
+           \Longunderstack[l]{$\SinsemillaHash(\ascii{z.cash:Orchard-MerkleCRH},$ \\
+                              $\hspace{6.7em} l \bconcat \mathsf{left} \bconcat \mathsf{right}),$} &\Longunderstack{\\ \squash otherwise}
+        \end{cases}$
   \item where $l = \ItoLEBSP{10}\big(\MerkleDepth{Orchard} - 1 - \mathsf{layer}\big)$.
 \end{formulae}
 
@@ -13817,6 +13832,9 @@ Peter Newell's illustration of the Jubjub bird, from \cite{Carroll1902}.
             \item Change the output types of $\NoteCommitAlg{Orchard}$ and $\CommitIvkAlg$ to
                   reflect that these can return $\bot$, and change the \actionStatement to be
                   satisfied if they do.
+            \item Propagate $\bot$ from the inputs of $\MerkleCRH{Orchard}$ to its output, and
+                  add an explicit consensus rule that $\rt{Orchard}$ computed from appending a
+                  \noteCommitment is not $\bot$.
           \end{itemize}
     \item Correct the description of $\lengthField$ in \crossref{unifiedpaymentaddrencoding}.
     \item Correct the type signature of $\DiversifyHash{Orchard}$ in \crossref{abstracthashes}.