zec
/
zips
mirror of https://github.com/zcash/zips.git
1
0
Fork 0
Code Issues Projects Releases Wiki Activity

Complete the proof of theorem A.3.4. 

Signed-off-by: Daira Hopwood <daira@jacaranda.org>
This commit is contained in:
Daira Hopwood 2018-07-18 07:51:52 +01:00
parent dcd929291a
commit 0200f63ace
1 changed files with 49 additions and 56 deletions
Show Stats Download Patch File Download Diff File Expand all files Collapse all files

105
protocol/protocol.tex
View File

@ -1638,7 +1638,7 @@ electronic commerce and payment, financial privacy, proof of work, zero knowledg
\newcommand{\HomomorphicPedersenCommit}[1]{\HomomorphicPedersenCommitAlg_{#1}}
\newcommand{\Digits}{\mathsf{Digits}}
\newcommand{\PedersenRangeOffset}{\Delta}
\newcommand{\Mask}{\mathsf{Mask}}
\newcommand{\Sign}{\mathsf{\Theta}}
% Consensus rules
@ -5907,7 +5907,7 @@ $\vsum{j=1}{k_i} \enc(m_j) \mult 2^{4 \mult (j-1)}$ is a subset of
the allowable range $\rangenozero{-\hfrac{\ParamJ{r}-1}{2}}{\hfrac{\ParamJ{r}-1}{2}}$.
The range of this expression is a subset of
$\rangenozero{-\PedersenRangeOffset}{\PedersenRangeOffset}$ where
$\PedersenRangeOffset = 4 \mult \vsum{i=0}{c-1} 2^{4 \mult i} = 4 \mult \hfrac{2^{4 \mult c}}{15}$.
$\PedersenRangeOffset = 4 \mult \vsum{i=1}{c} 2^{4 \mult (i-1)} = 4 \mult \hfrac{2^{4 \mult c}}{15}$.
\introlist
When $c = 63$, we have
@ -9544,6 +9544,7 @@ Peter Newell's illustration of the Jubjub bird, from \cite{Carroll1902}.
\begin{itemize}
\item No changes to \Sprout.
\sapling{
\item Complete the proof of \theoremref{thmpedersendistinctabsindices}.
\item Add a note about redundancy in the nonsmall-order checking of $\AuthSignRandomizedPublic$.
} %sapling
\end{itemize}
@ -11026,23 +11027,23 @@ from \crossref{cctmontarithmetic} is met. This requires splitting the
input into segments (each using an independent generator), calculating
an intermediate result for each segment, and then converting to the
Edwards curve and summing the intermediate results using Edwards addition.
If the resulting point is $R$, then (abstracting away the changes of curve)
this calculation can be written as:
Abstracting away the changes of curve, this calculation can be written as:
\begin{formulae}
\item $\PedersenHashToPoint(D, M) = \vsum{j=1}{N} \scalarmult{\PedersenEncode{M_j}}{\PedersenGen{D}{j}}$
\end{formulae}
\vspace{-2ex}
where $\PedersenEncode{\paramdot}$ and $\PedersenGen{D}{j}$
are defined as in \crossref{concretepedersenhash}.
\introlist
\vspace{1ex}
We have to prove that:
\begin{itemize}
\item the \distinctXCriterion is met for all Montgomery additions within
a segment;
\item the Montgomery-to-Edwards conversions can be implemented without
exceptional cases.
exceptional cases;
\item the \distinctXCriterion is met for all Montgomery additions within
a segment.
\end{itemize}
The proof of \theoremref{thmpedersenencodeinjective} showed that
@ -11061,66 +11062,58 @@ We also need to show that the indices of addition inputs are
all distinct disregarding sign.
\begin{theorem} \label{thmpedersendistinctabsindices}
For all disjoint nonempty subsets $S$ and $S'$ of $\range{1}{c}$, and for all
$m \in \typeexp{\bitseq{3}}{c}$,
For all disjoint nonempty subsets $S$ and $S'$ of $\range{1}{c}$, all
$m \in \typeexp{\bitseq{3}}{c}$, and all $\Sign \in \setof{-1, 1}$:
\begin{formulae}
\item $\vsum{j \in S\vphantom{S'}}{} \enc(m_j) \mult 2^{4 \mult (j-1)}
\neq \pm\!\!\vsum{j' \in S'}{} \enc(m_{\kern -0.1em j'}) \mult 2^{4 \mult (j'-1)}$
\item $\vsum{j \in S\vphantom{S'}}{} \enc(m_j) \mult 2^{4 \mult (j-1)} \neq
\Sign \mult\!\!\vsum{j' \in S'}{} \enc(m_{\kern -0.1em j'}) \mult 2^{4 \mult (j'-1)}$.
\end{formulae}
\end{theorem}
\begin{proof}
\todo{...}
%Since $\PedersenEncode{\paramdot}$ is injective, the given condition is
%equivalent to:
Suppose for a contradiction that $S$, $S'$, $m$, $\Sign$ is a counterexample. Taking the multiplication
by $\Sign$ on the right hand side inside the summation, we have:
\begin{formulae}
\item $\vsum{j \in S\vphantom{S'}}{} \enc(m_j) \mult 2^{4 \mult (j-1)} =
\!\!\vsum{j' \in S'}{} \Sign \mult \enc(m_{\kern -0.1em j'}) \mult 2^{4 \mult (j'-1)}$.
\end{formulae}
%\begin{formulae}
% \item for all disjoint subsets $S$ and $S'$ of $\range{1}{c}$, and for all
% $M \in \bitseq{3 \mult c},\; \PedersenEncodeSub{S}{M} \neq \pm \PedersenEncodeSub{S'}{M}$
%\end{formulae}
Define $\enc' \typecolon \setof{-1, 1} \times \bitseq{3} \rightarrow \range{0}{8} \setminus \setof{4}$ as
$\enc'_\theta(m_i) := 4 + \theta \mult \enc(m_i)$.
%where $\PedersenEncodeSub{S}{M} = \vsum{j \in S}{} \enc(m_j) \mult 2^{4 \mult (j-1)}$.
Let $\PedersenRangeOffset = 4 \mult \ssum{i=1}{c} 2^{4 \mult (i-1)}$
as in the proof of \theoremref{thmpedersenencodeinjective}.
By adding $\PedersenRangeOffset$ to both sides, we get
\begin{formulae}
\item $\vsum{j \in S\vphantom{S'}}{} \enc'_1(m_j) \mult 2^{4 \mult (j-1)} + \vsum{j \in \range{1}{c} \setminus S\vphantom{S'}}{} 4 \mult 2^{4 \mult (j-1)} =
\vsum{j' \in S'}{} \enc'_{\Sign}(m_{\kern -0.1em j'}) \mult 2^{4 \mult (j'-1)} + \vsum{j' \in \range{1}{c} \setminus S'}{} 4 \mult 2^{4 \mult (j'-1)}$
\end{formulae}
\vspace{-1ex}
where all of the $\enc'_1(m_j)$ and $\enc'_{\Sign}(m_{\kern -0.1em j'})$ are in $\range{0}{8} \setminus \setof{4}$.
%This is in turn equivalent to:
%\begin{formulae}
% \item for all disjoint subsets $S$ and $S'$ of $\range{1}{c}$, and for all
% $M \in \bitseq{3 \mult c},\;
% \PedersenEncodeSub{S}{M \band \Mask} \neq \PedersenEncodeSub{S'}{M \band \Mask}$
%\end{formulae}
%where $\Mask = \vsum{j=1}{c} 3 \mult 2^{4 \mult (j-1)}$.
%(This masks off the bit controlling the sign of each digit, which effectively
%takes the absolute value of each digit.)
%Since $S$ and $S'$ are disjoint and each term of the RHS is separated,
%it follows that $\Mask_S \band \Mask_{S'} = 0$ and so ...
%Suppose this were not
%the case, then there would exist disjoint subsets of windows $S$ and $S'$
%such that ..., the space of indices spanned by ...
%does not overlap the space spanned by $S'$.
%is met because all of the terms in the Montgomery addition, as well as any
%intermediate result formed from adding a subset of terms, have distinct indices
%(this bound makes no assumption about the order of additions; the actual
%maximum will be smaller).
Each term on the left and on the right affects the single hex digit indexed by
$j$ and $j'$ respectively. Since $S$ and $S'$ are disjoint subsets of $\range{1}{c}$
and $S$ is nonempty, $S \intersection (\range{1}{c} \setminus S')$ is nonempty.
Therefore the left hand side has at least one hex digit not equal to $4$ such that
the corresponding right hand side digit is $4$; contradiction.
\end{proof}
When these hashes are used in the circuit, the first two windows of the input
are fixed and can be optimized (for example, in the Merkle tree hashes they
represent the layer number).
This is done by precomputing the sum of the relevant two points, and adding them
to the intermediate result for the remainder of the first segment.
This requires 3 constraints for a single Montgomery addition rather than
.. constraints for 2 window lookups and 2 additions.
This implies that the terms in the Montgomery addition, as well as any
intermediate result formed from adding a distinct subset of terms, have distinct indices.
(We make no assumption about the order of additions.)
Taking into account this optimization, the cost of a Pedersen hash over
$\ell$ bits, with the first 6 bits fixed, is ... constraints. In particular,
for the Merkle tree hashes $\ell = 516$, so the cost is ... constraints.
\todo{Describe the lookup subcircuit.}
When these hashes are used in the circuit, the first 6 bits of the input
are fixed. For example, in the Merkle tree hashes they represent the layer number.
This would allow a precomputation for the first two windows, but that
optimization is not done in \Sapling.
The cost of a Pedersen hash over $\ell$ bits (where $\ell$ includes the fixed
bits) is ... constraints. In particular, for the Merkle tree hashes $\ell = 516$,
so the cost is ... constraints.
\introlist