Corrections to the specification of \abstJ and the security argument for GroupHash.

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

protocol/protocol.tex

@@ -7846,8 +7846,12 @@ that $\reprJ\Of{u, \varv} = \ItoLEBSP{256}\big(\varv + 2^{255} \smult \tilde{u}\
 $\tilde{u} = u \bmod 2$.
 
 \vspace{-1ex}
-Define $\abstJ \typecolon \ReprJ \rightarrow \maybe{\GroupJ}$ as follows:
+Define $\abstJ \typecolon \ReprJ \rightarrow \maybe{\GroupJ}$ such that
+$\abstJ\Of{P\Repr}$ is computed as follows:
 \begin{formulae}
+  \item let ${\varv\Repr} \typecolon \bitseq{255}$ be the first $255$ bits of $P\Repr$ and let $\tilde{u} \typecolon \bit$ be the last bit.
+  \item if $\LEBStoIPOf{255}{\varv\Repr} \geq \ParamJ{q}$ then return $\bot$, otherwise
+        let $\varv \typecolon \GF{\ParamJ{q}} = \LEBStoIPOf{255}{\varv\Repr} \pmod{\ParamJ{q}}$.
   \item if $\ParamJ{a} - \ParamJ{d} \smult \varv^2 = 0$, return $\bot$.
   \item let $u = \optsqrt{\hfrac{1 - \varv^2}{\ParamJ{a} - \ParamJ{d} \mult \varv^2}}$.
   \item if $u = \bot$, return $\bot$.
@@ -7861,7 +7865,7 @@ This differs from the specification above:
 \begin{itemize}
   \item Previously, $\abstJ\Of{\ItoLEBSP{256}\big(2^{255} + 1\big)\!}$ and $\abstJ\Of{\ItoLEBSP{256}\big(2^{255} - 1\big)\!}$ were defined as $\bot$.
   \item In the current specification, $\abstJ\Of{\ItoLEBSP{256}\big(2^{255} + 1\big)\!} = \abstJ\big(\ItoLEBSPOf{256}{1}\kern-0.27em\big) = (0, 1) = \ZeroJ$,
-        and also $\abstJ\Of{\ItoLEBSP{256}\big(2^{255} - 1\big)\!} = \abstJ\big(\ItoLEBSPOf{256}{-1}\kern-0.27em\big) = (0, -1) = -\ZeroJ$.
+        and also $\abstJ\Of{\ItoLEBSP{256}\big(2^{255} - 1\big)\!} = \abstJ\big(\ItoLEBSPOf{256}{-1}\kern-0.27em\big) = (0, -1)$.
 \end{itemize}
 }
 
@@ -7992,7 +7996,7 @@ The hash $\GroupJHash{\URS}(D, M) \typecolon \SubgroupJstar$ is calculated as fo
         $\vphantom{a^b}\BlakeTwos{256}$ in the security analysis.
 
         $\exclusivefun{\HashOutput \typecolon \byteseq{32}}
-          {\abstJ\big(\LEOStoBSP{256}(\HashOutput)\kern-0.12em\big) \typecolon \GroupJ}{\setof{\bot,\, \ZeroJ, -\ZeroJ}}$
+          {\abstJ\big(\LEOStoBSP{256}(\HashOutput)\kern-0.12em\big) \typecolon \GroupJ}{\setof{\bot,\, \ZeroJ,\, (0, -1)}}$
         is injective, and both it and its inverse are efficiently computable.
 
         $\exclusivefun{P \typecolon \GroupJ}
@@ -10521,6 +10525,11 @@ Peter Newell's illustration of the Jubjub bird, from \cite{Carroll1902}.
 \historyentry{2020.1.9}{}
 \begin{itemize}
     \item Acknowledge Jane Lusby and Teor.
+\sapling{
+    \item Correct an error introduced in 2020.1.8; ``$-\ZeroJ$'' was incorrectly used when
+          the point $(0, -1)$ on \Jubjub was meant.
+    \item Precisely specify the conversion from a bit sequence in $\abstJ$.
+} %sapling
 \end{itemize}