Fix an error in the definition of the sortedness condition for Equihash.

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

protocol/protocol.tex

@@ -603,7 +603,6 @@
 \newcommand{\ECtoOSPXS}{\mathsf{EC2OSP\mhyphen{}XS}}
 \newcommand{\ItoOSP}[1]{\mathsf{I2OSP}_{#1}}
 \newcommand{\ItoBSP}[1]{\mathsf{I2BSP}_{#1}}
-\newcommand{\BStoIP}[1]{\mathsf{BS2IP}_{#1}}
 \newcommand{\FEtoIP}{\mathsf{FE2IP}}
 \newcommand{\BNImpl}{\mathtt{ALT\_BN128}}
 \newcommand{\vpubOld}{\mathsf{v_{pub}^{old}}}
@@ -856,6 +855,10 @@ defined either on integers or bit sequences according to context.
 The notation $\vsum{i=1}{\mathrm{N}} a_i$ means the sum of $a_{\allN{}}$.\;
 $\vxor{i=1}{\mathrm{N}} a_i$ means the bitwise exclusive-or of $a_{\allN{}}$.
 
+The binary relations $<$, $\leq$, $=$, $\geq$, and $>$ have their conventional
+meanings on integers and rationals, and are defined lexicographically on
+sequences of integers.
+
 The notation $\floor{x}$ means the largest integer $\leq x$.
 $\ceiling{x}$ means the smallest integer $\geq x$.
 
@@ -2927,11 +2930,6 @@ Define $\ItoBSP{} \typecolon (u \typecolon \Nat) \times \range{0}{2^u\!-\!1} \ri
 such that $\ItoBSP{u}(x)$ is the sequence of $u$ bits representing $x$ in
 big-endian order.
 
-Define $\BStoIP{} \typecolon (u \typecolon \Nat) \times \bitseq{u} \rightarrow \range{0}{2^u\!-\!1}$
-such that $\BStoIP{u}$ is the inverse of $\ItoBSP{u}$.
-
-Define $\Xi_r(a, b) := \BStoIP{2^{r-1} \mult \ell}(\concatbits(X_{i_{a..b}}))$.
-
 A \validEquihashSolution is then a sequence $i \typecolon \range{1}{N}^{2^k}$ that
 satisfies the following conditions:
 
@@ -2944,7 +2942,7 @@ $\vxor{j=1}{2^k} X_{i_j} = 0$.
 For all $r \in \range{1}{k\!-\!1}$, for all $w \in \range{0}{2^{k-r}\!-\!1}$:
 \begin{itemize}
   \item $\vxor{j=1}{2^r} X_{i_{w \mult 2^r + j}}$ has $\frac{n \mult r}{k+1}$ leading zeroes; and
-  \item $\Xi_r(w \mult 2^r + 1, w \mult 2^r + 2^{r-1}) < \Xi_r(w \mult 2^r + 2^{r-1} + 1, w \mult 2^r + 2^r)$.
+  \item $i_{w \mult 2^r + 1 .. w \mult 2^r + 2^{r-1}} < i_{w \mult 2^r + 2^{r-1} + 1 .. w \mult 2^r + 2^r}$ lexicographically.
 \end{itemize}
 
 \pnote{
@@ -3001,14 +2999,12 @@ and so the first 7 bytes of $\solution$ would be
 $[0, 2, 32, 0, 10, 127, 255]$.
 
 \pnote{
-$\ItoBSP{}$ and $\BStoIP{}$ are big-endian, while the encoding of
-integer fields in $\powheader$ and in the instantiation of $\EquihashGen{}$
-is little-endian. The rationale for this is that little-endian
-serialization of \blockHeaders is consistent with \Bitcoin, but using
-little-endian ordering of bits in the solution encoding would require
-bit-reversal (as opposed to only shifting). The comparison of $\Xi_r$
-values obtained by a big-endian conversion is equivalent to lexicographic
-comparison as specified in \cite[section IV A]{BK2016}.
+$\ItoBSP{}$ is big-endian, while integer field encodings in $\powheader$
+and in the instantiation of $\EquihashGen{}$ are little-endian.
+The rationale for this is that little-endian serialization of
+\blockHeaders is consistent with \Bitcoin, but using little-endian
+ordering of bits in the solution encoding would require bit-reversal
+(as opposed to only shifting).
 }
 
 \nsubsubsection{Difficulty filter} \label{difficulty}
@@ -3545,6 +3541,9 @@ The errors in the proof of Ledger Indistinguishability mentioned in
 \subparagraph{2016.0-beta-1.6}
 
 \begin{itemize}
+    \item Fix an error in the definition of the sortedness condition for Equihash:
+          it is the sequences of indices that are sorted, not the sequences of
+          hashes.
     \item Correct the number of bytes in the encoding of $\solutionSize$.
     \item Update the section on encoding of \transparent addresses.
           (The precise prefixes are not decided yet.)