Improvements to notation to remove ambiguity.

Signed-off-by: Daira Hopwood <daira@jacaranda.org>
This commit is contained in:
Daira Hopwood 2016-09-19 01:57:28 +01:00
parent 8a0e10c520
commit c872968acf
1 changed files with 94 additions and 73 deletions

View File

@ -280,8 +280,12 @@
\newcommand{\bytes}[1]{\underline{\raisebox{-0.22ex}{}\smash{#1}}}
\newcommand{\zeros}[1]{[0]^{#1}}
\newcommand{\bit}{\mathds{B}}
\newcommand{\bitseq}[1]{\bit^{#1}}
\newcommand{\byteseqs}{\bit^{8\star}}
\newcommand{\Nat}{\mathbb{N}}
\newcommand{\PosInt}{\mathbb{N}^+}
\newcommand{\Rat}{\mathbb{Q}}
\newcommand{\typeexp}[2]{{#1}\vphantom{)}^{[{#2}]}}
\newcommand{\bitseq}[1]{\typeexp{\bit}{#1}}
\newcommand{\byteseqs}{\typeexp{\bit}{8\mult\Nat}}
\newcommand{\concatbits}{\mathsf{concat}_\bit}
\newcommand{\hexint}[1]{\mathbf{0x{#1}}}
\newcommand{\dontcare}{\kern -0.06em\raisebox{0.1ex}{\footnotesize{$\times$}}}
@ -302,14 +306,13 @@
\newcommand{\FullHashbox}[1]{\FullHash\left(\Justthebox{#1}\right)}
\newcommand{\setof}[1]{\{{#1}\}}
\newcommand{\range}[2]{\{{#1}\,..\,{#2}\}}
\newcommand{\Nat}{\mathbb{N}}
\newcommand{\PosInt}{\mathbb{N}^+}
\newcommand{\minimum}{\mathsf{min}}
\newcommand{\floor}[1]{\mathsf{floor}\!\left({#1}\right)}
\newcommand{\ceiling}[1]{\mathsf{ceiling}\!\left({#1}\right)}
\newcommand{\vsum}[2]{\smashoperator[r]{\sum_{#1}^{#2}}}
\newcommand{\vxor}[2]{\smashoperator[r]{\bigoplus_{#1}^{#2}}}
\newcommand{\xor}{\oplus}
\newcommand{\mult}{\cdot}
\newcommand{\rightarrowR}{\buildrel{\scriptstyle\mathrm{R}}\over\rightarrow}
% key pairs:
@ -458,7 +461,7 @@
\newcommand{\dataToBeSigned}{\mathsf{dataToBeSigned}}
% Merkle tree
\newcommand{\MerkleDepth}{\mathsf{d}}
\newcommand{\MerkleDepth}{\mathsf{d_{Merkle}}}
\newcommand{\MerkleNode}[2]{\mathsf{M}^{#1}_{#2}}
\newcommand{\MerkleSibling}{\mathsf{sibling}}
\newcommand{\MerkleCRH}{\mathsf{MerkleCRH}}
@ -729,14 +732,35 @@ one valid \nullifier, and so attempting to spend a \note twice would reveal the
\nsection{Notation}
The notation $\hexint{}$ followed by a string of \textbf{boldface} hexadecimal
digits means the corresponding integer converted from hexadecimal.
The notation $\bit$ means the type of bit values, i.e. $\setof{0, 1}$.
The notation $\bit$ means the set of bit values, i.e. $\setof{0, 1}$.
The notation $\Nat$ means the set of nonnegative integers. $\PosInt$
means the set of positive integers. $\Rat$ means the set of rationals.
The notation $x \typecolon T$ is used to specify that $x$ has type $T$.
A cartesian product type is denoted by $S \times T$, and a function type
by $S \rightarrow T$. The type of a randomized algorithm is denoted by $S \rightarrowR T$.
The domain of a randomized algorithm may be $()$, indicating that it requires
no arguments. An argument to a function can determine other argument or result
types.
Initial arguments to a function or randomized algorithm may be
written as subscripts, e.g.\ if $x \typecolon X$, $y \typecolon Y$, and
$\PRF{}{} \typecolon X \times Y \rightarrow Z$, then an invocation of
$\PRF{}{}(x, y)$ can also be written $\PRF{x}{}(y)$.
The notation $\typeexp{T}{\ell}$, where $T$ is a type and $\ell$ is an integer,
means the type of sequences of length $\ell$ with elements in $T$. For example,
$\bitseq{\ell}$ means the set of sequences of $\ell$ bits.
The notation $T \subseteq U$ indicates that $T$ is an inclusive subset or subtype of $U$.
$\byteseqs$ means the set of bit sequences constrained to be of length
a multiple of 8 bits.
The notation $\hexint{}$ followed by a string of \textbf{boldface} hexadecimal
digits means the corresponding integer converted from hexadecimal.
The notation $\ascii{...}$ means the given string represented as a
sequence of bytes in US-ASCII. For example, $\ascii{abc}$ represents the
byte sequence $[\hexint{61}, \hexint{62}, \hexint{63}]$.
@ -744,13 +768,13 @@ byte sequence $[\hexint{61}, \hexint{62}, \hexint{63}]$.
The notation $a..b$, used as a subscript, means the sequence of values
with indices $a$ through $b$ inclusive. For example,
$\AuthPublicNew{\allNew}$ means the sequence $[\AuthPublicNew{\mathrm{1}},
\AuthPublicNew{\mathrm{2}}, ...\;\AuthPublicNew{\NNew}]$.
\AuthPublicNew{\mathrm{2}}, ...\,\AuthPublicNew{\NNew}]$.
(For consistency with the notation in \cite{BCG+2014} and in \cite{BK2016},
this specification uses 1-based indexing and inclusive ranges,
notwithstanding the compelling arguments to the contrary made in
\cite{EWD-831}.)
The notation $\range{a}{b}$ means the set of integers from $a$ through
The notation $\range{a}{b}$ means the set or type of integers from $a$ through
$b$ inclusive.
The notation $[f(x)$ for $x$ from $a$ up to $b\,]$ means the sequence
@ -766,19 +790,23 @@ concatenating the elements of $S$ viewed as bit sequences. If the
elements of $S$ are byte sequences, they are converted to bit sequences
with the \emph{most significant} bit of each byte first.
The notation $\Nat$ means the set of nonnegative integers. $\PosInt$
means the set of positive integers.
The notation $\GF{n}$ means the finite field with $n$ elements, and
$\GFstar{n}$ means its group under multiplication.
$\GF{n}[z]$ means the ring of polynomials over $z$ with coefficients
in $\GF{n}$.
The notation $a \bmod q$, for integers $a \geq 0$ and $q > 0$, means the
remainder on dividing $a$ by $q$.
The notation $a \mult b$ means the result of multiplying $a$ and $b$.
This may refer to multiplication of integers, rationals, or
finite field elements according to context.
The notation $a^b$, for $a$ an integer or finite field element and
$b$ an integer, means the result of raising $a$ to the exponent $b$.
The notation $a \bmod q$, for $a \typecolon \Nat$ and $q \typecolon \PosInt$,
means the remainder on dividing $a$ by $q$.
The notation $a \xor b$ means the bitwise exclusive-or of $a$ and $b$,
defined either on integers or bit sequences depending on context.
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{}}$.
@ -788,20 +816,6 @@ $\ceiling{x}$ means the smallest integer $\geq x$.
The symbol $\bot$ is used to indicate unavailable information or a failed decryption.
The notation $T \subseteq U$ indicates that $T$ is an inclusive subset or subtype of $U$.
The notation $x \typecolon T$ is used to specify that $x$ has type $T$.
A cartesian product type is denoted by $S \times T$, and a function type
by $S \rightarrow T$. The type of a randomized algorithm is denoted by $S \rightarrowR T$.
The domain of a randomized algorithm may be $()$, indicating that it requires
no arguments. An argument to a function can determine other argument or result
types.
Initial arguments to a function or randomized algorithm may be
written as subscripts, e.g.\ if $x \typecolon X$, $y \typecolon Y$, and
$\PRF{}{} \typecolon X \times Y \rightarrow Z$, then an invocation of
$\PRF{}{}(x, y)$ can also be written $\PRF{x}{}(y)$.
The following integer constants will be instantiated in \crossref{constants}:
$\MerkleDepth$, $\NOld$, $\NNew$, $\MerkleHashLength$, $\hSigLength$,
$\PRFOutputLength$, $\NoteCommitRandLength$, $\RandomSeedLength$, $\AuthPrivateLength$,
@ -1045,7 +1059,7 @@ is a collision-resistant hash function used in \crossref{merklepath}.
It is instantiated in \crossref{merklecrh}.
\changed{
$\hSigCRH{} \typecolon \bitseq{\RandomSeedLength} \times (\PRFOutput)^{\NOld} \times \JoinSplitSigPublic \rightarrow \hSigType$
$\hSigCRH{} \typecolon \bitseq{\RandomSeedLength} \times \typeexp{\PRFOutput}{\NOld} \times \JoinSplitSigPublic \rightarrow \hSigType$
is a collision-resistant hash function used in \crossref{joinsplitdesc}.
It is instantiated in \crossref{hsigcrh}.
@ -1353,9 +1367,9 @@ where
\crossref{blockchain}, for the output \treestate of either
a previous \block, or a previous \joinSplitTransfer in this
\transaction.
\item $\nfOld{\allOld} \typecolon (\PRFOutput)^{\NOld}$ is
\item $\nfOld{\allOld} \typecolon \typeexp{\PRFOutput}{\NOld}$ is
the sequence of \nullifiers for the input \notes;
\item $\cmNew{\allNew} \typecolon (\CommitOutput)^{\NNew}$ is
\item $\cmNew{\allNew} \typecolon \typeexp{\CommitOutput}{\NNew}$ is
the sequence of \noteCommitments for the output \notes;
\item \changed{$\EphemeralPublic \typecolon \KAPublic$ is
a key agreement public key, used to derive the key for encryption
@ -1363,12 +1377,12 @@ where
\item \changed{$\RandomSeed \typecolon \RandomSeedType$ is
a seed that must be chosen independently at random for each
\joinSplitDescription};
\item $\h{\allOld} \typecolon (\PRFOutput)^{\NOld}$ is
\item $\h{\allOld} \typecolon \typeexp{\PRFOutput}{\NOld}$ is
a sequence of tags that bind $\hSig$ to each
$\AuthPrivate$ of the input \notes;
\item $\JoinSplitProof \typecolon \ZKJoinSplitProof$ is
the \zeroKnowledgeProof for the \joinSplitStatement;
\item $\TransmitCiphertext{\allNew} \typecolon (\Ciphertext)^{\NNew}$ is
\item $\TransmitCiphertext{\allNew} \typecolon \typeexp{\Ciphertext}{\NNew}$ is
a sequence of ciphertext components for the encrypted output \notes.
\end{itemize}
@ -1572,22 +1586,22 @@ A valid instance of $\JoinSplitProof$ assures that given a \term{primary input}:
\begin{itemize}
\item[] $(\rt \typecolon \MerkleHash,
\nfOld{\allOld} \typecolon (\PRFOutput)^{\NOld},
\cmNew{\allNew} \typecolon (\CommitOutput)^{\NNew},
\nfOld{\allOld} \typecolon \typeexp{\PRFOutput}{\NOld},
\cmNew{\allNew} \typecolon \typeexp{\CommitOutput}{\NNew},
\changed{\vpubOld \typecolon \range{0}{2^{64}-1},}\,
\vpubNew \typecolon \range{0}{2^{64}-1},\\
\hphantom{(}
\hSig \typecolon \hSigType,
\h{\allOld} \typecolon (\PRFOutput)^{\NOld})$,
\h{\allOld} \typecolon \typeexp{\PRFOutput}{\NOld})$,
\end{itemize}
the prover knows an \term{auxiliary input}:
\begin{itemize}
\item[] $(\treepath{\allOld} \typecolon ((\MerkleHash)^{\MerkleDepth})^{\NOld},
\nOld{\allOld} \typecolon \NoteType^{\NOld},
\AuthPrivateOld{\allOld} \typecolon (\bitseq{\AuthPrivateLength})^{\NOld},
\nNew{\allNew} \typecolon \NoteType^{\NOld}\changed{,}\\
\item[] $(\treepath{\allOld} \typecolon \typeexp{\typeexp{\MerkleHash}{\MerkleDepth}}{\NOld},
\nOld{\allOld} \typecolon \typeexp{\NoteType}{\NOld},
\AuthPrivateOld{\allOld} \typecolon \typeexp{\bitseq{\AuthPrivateLength}}{\NOld},
\nNew{\allNew} \typecolon \typeexp{\NoteType}{\NOld}\changed{,}\\
\hphantom{(}
\changed{\NoteAddressPreRand \typecolon \bitseq{\NoteAddressPreRandLength},
\EnforceCommit{\allOld} \typecolon \bitseq{\NOld}})$,
@ -1833,18 +1847,18 @@ and represent the byte sequence $[\hexint{D2}, \hexint{BC}, \hexint{3A}, \hexint
Define:
\begin{itemize}
\item[] $\MerkleDepth = \changed{29}$
\item[] $\NOld = 2$
\item[] $\NNew = 2$
\item[] $\MerkleHashLength = 256$
\item[] $\hSigLength = 256$
\item[] $\PRFOutputLength = 256$
\item[] $\NoteCommitRandLength = \changed{256}$
\item[] $\changed{\RandomSeedLength = 256}$
\item[] $\AuthPrivateLength = \changed{252}$
\item[] $\NoteAddressPreRandLength = \changed{252}$
\item[] $\Uncommitted = \zeros{\MerkleHashLength}$
\item[] $\MAXMONEY = \changed{2.1 \times 10^{15}}$.
\item[] $\MerkleDepth \typecolon \Nat := \changed{29}$
\item[] $\NOld \typecolon \Nat := 2$
\item[] $\NNew \typecolon \Nat := 2$
\item[] $\MerkleHashLength \typecolon \Nat := 256$
\item[] $\hSigLength \typecolon \Nat := 256$
\item[] $\PRFOutputLength \typecolon \Nat := 256$
\item[] $\NoteCommitRandLength \typecolon \Nat := \changed{256}$
\item[] $\changed{\RandomSeedLength \typecolon \Nat := 256}$
\item[] $\AuthPrivateLength \typecolon \Nat := \changed{252}$
\item[] $\NoteAddressPreRandLength \typecolon \Nat := \changed{252}$
\item[] $\Uncommitted \typecolon \bitseq{\MerkleHashLength} := \zeros{\MerkleHashLength}$
\item[] $\MAXMONEY \typecolon \Nat := \changed{2.1 \mult 10^{15}}$ (\zatoshi)
\end{itemize}
@ -1939,8 +1953,8 @@ Let $\powcount(g) := \Justthebox{\powcountbox}$.
Let $\EquihashGen{n, k}(S, i) := T_{h+1\hairspace..\hairspace h+n}$, where
\begin{itemize}
\item $m := \floor{\frac{512}{n}}$;
\item $h := (i-1 \bmod m)\, n$;
\item $T := \Blake{(n m)}(\powtag,\, S \,||\, \powcount(\floor{\frac{i-1}{m}}))$.
\item $h := (i-1 \bmod m) \mult n$;
\item $T := \Blake{(\mathnormal{n \mult m})}(\powtag,\, S \,||\, \powcount(\floor{\frac{i-1}{m}}))$.
\end{itemize}
Indices of bits in $T$ are 1-based.
@ -2387,9 +2401,9 @@ The pairing is of type $\GroupG{1} \times \GroupG{2} \rightarrow \GroupG{T}$, wh
\item $\GroupG{1}$ is a Barreto--Naehrig curve over $\GF{q}$ with equation
$y^2 = x^3 + b$. This curve has embedding degree 12 with respect to $r$.
\item $\GroupG{2}$ is the subgroup of order $r$ in the twisted Barreto-Naehrig curve
over $\GF{q^2}$ with equation $y^2 = x^3 + b/xi$. We represent elements of $\GF{q^2}$ as
polynomials $a_1 t + a_0 \typecolon \GF{q}[t]$, modulo the irreducible polynomial
$t^2 + 1$.
over $\GF{q^2}$ with equation $y^2 = x^3 + \frac{b}{x \mult i}$. We represent elements
of $\GF{q^2}$ as polynomials $a_1 \mult t + a_0 \typecolon \GF{q}[t]$, modulo the
irreducible polynomial $t^2 + 1$.
\item $\GroupG{T}$ is $\mu_r$, the subgroup of $r^\mathrm{th}$ roots of unity in
$\GFstar{q^{12}}$.
\end{itemize}
@ -2399,10 +2413,10 @@ Let $\PointP{1} \typecolon \GroupG{1} = (1, 2)$.
\begin{tabular}{@{}l@{}r@{}l@{}}
Let $\PointP{2} \typecolon \GroupG{2} =\;$
% are these the right way round?
&$(11559732032986387107991004021392285783925812861821192530917403151452391805634$ & $\,t\;+$ \\
&$ 10857046999023057135944570762232829481370756359578518086990519993285655852781$ & $, $ \\
&$ 4082367875863433681332203403145435568316851327593401208105741076214120093531$ & $\,t\;+$ \\
&$ 8495653923123431417604973247489272438418190587263600148770280649306958101930$ & $). $
&$(11559732032986387107991004021392285783925812861821192530917403151452391805634$ & $\mult\, t\;+$ \\
&$ 10857046999023057135944570762232829481370756359578518086990519993285655852781$ & $, $ \\
&$ 4082367875863433681332203403145435568316851327593401208105741076214120093531$ & $\mult\, t\;+$ \\
&$ 8495653923123431417604973247489272438418190587263600148770280649306958101930$ & $). $
\end{tabular}
$\PointP{1}$ and $\PointP{2}$ are generators of $\GroupG{1}$ and $\GroupG{2}$ respectively.
@ -2462,9 +2476,9 @@ of \libsnark, to ensure compatibility.
\end{bytefield}
\end{lrbox}
Define $\ItoOSP{} \typecolon (k \typecolon \Nat) \times \range{0}{256^k\!-\!1} \rightarrow \range{0}{255}^k$
such that $\ItoOSP{\ell}(n)$ is the sequence of $\ell$ bytes representing $n$ in
big-endian order.
Define $\ItoOSP{} \typecolon (k \typecolon \Nat) \times \range{0}{256^k\!-\!1} \rightarrow
\typeexp{\range{0}{255}}{k}$ such that $\ItoOSP{\ell}(n)$ is the sequence of $\ell$ bytes
representing $n$ in big-endian order.
For a point $P \typecolon \GroupG{1} = (x_P, y_P)$:
\begin{itemize}
@ -2477,9 +2491,9 @@ For a point $P \typecolon \GroupG{1} = (x_P, y_P)$:
For a point $P \typecolon \GroupG{2} = (x_P, y_P)$:
\begin{itemize}
\item A field element $w \typecolon \GF{q^2}$ is represented as
a polynomial $a_{w,1} t + a_{w,0} \typecolon \GF{q}[t]$ modulo $t^2 + 1$.
a polynomial $a_{w,1} \mult t + a_{w,0} \typecolon \GF{q}[t]$ modulo $t^2 + 1$.
Define $\FEtoIP \typecolon \GF{q^2} \rightarrow \range{0}{q^2\!-\!1}$ such that
$\FEtoIP(w) = a_{w,1} q + a_{w,0}$.
$\FEtoIP(w) = a_{w,1} \mult q + a_{w,0}$.
\item Let $x = \FEtoIP(x_P)$, $y = \FEtoIP(y_P)$, and $y' = \FEtoIP(-y_P)$.
\item Let $\tilde{y} = \begin{cases} 1, &\text{if } y > y' \\0, &\text{otherwise.} \end{cases}$
\item $P$ is encoded as $\Justthebox{\gtwobox}$.
@ -2583,7 +2597,7 @@ Bytes & \heading{Name} & \heading{Data Type} & \heading{Description} \\
\Varies\;$\dagger$ & $\nJoinSplit$ & \compactSize & The number of \joinSplitDescriptions
in $\vJoinSplit$. \\ \hline
\Longunderstack{1802 $\times$ \\ $\nJoinSplit\,\dagger$} & $\vJoinSplit$ & \type{JoinSplitDescription} \type{[$\nJoinSplit$]} &
\Longunderstack{1802 $\mult$ \\ $\nJoinSplit\,\dagger$} & $\vJoinSplit$ & \type{JoinSplitDescription} \type{[$\nJoinSplit$]} &
A \sequenceOfJoinSplitDescriptions, each encoded as described in \crossref{joinsplitencoding}. \\ \hline
32 $\ddagger$ & $\joinSplitPubKey$ & \type{char[32]} & An encoding of a $\JoinSplitSig$
@ -2649,7 +2663,7 @@ this \transaction. \\ \hline
64 & $\nullifiersField$ & \type{char[32][$\NOld$]} & A sequence of \nullifiers of the input
\notes $\nfOld{\allOld}$. \\ \hline
64 & $\commitments$ & \type{char[32][$\NNew$]}. & A sequence of \noteCommitments for the
64 & $\commitments$ & \type{char[32][$\NNew$]} & A sequence of \noteCommitments for the
output \notes $\cmNew{\allNew}$. \\ \hline
\setchanged 32 &\setchanged $\ephemeralKey$ &\setchanged \type{char[32]} &\mbox{}\setchanged
@ -2792,7 +2806,7 @@ 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} \ell}(\concatbits(X_{i_{a..b}}))$.
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:
@ -2805,8 +2819,8 @@ $\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 2^r + j}}$ has $\frac{nr}{k+1}$ leading zeroes; and
\item $\Xi_r(w 2^r + 1, w 2^r + 2^{r-1}) < \Xi_r(w 2^r + 2^{r-1} + 1, w 2^r + 2^r)$.
\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)$.
\end{itemize}
\pnote{
@ -3300,6 +3314,13 @@ The errors in the proof of Ledger Indistinguishability mentioned in
\nsection{Change history}
\subparagraph{2016.0-beta-1.4}
\begin{itemize}
\item Improve notation (for example ``$\mult$'' for multiplication and
``$\typeexp{T}{\ell}$'' for sequence types) to avoid ambiguity.
\end{itemize}
\subparagraph{2016.0-beta-1.3}
\begin{itemize}