Skip to content

Commit

Permalink
completeness proofs
Browse files Browse the repository at this point in the history
  • Loading branch information
lizz-zard committed Jul 11, 2024
1 parent b7a12ff commit a2514d4
Show file tree
Hide file tree
Showing 5 changed files with 118 additions and 42 deletions.
2 changes: 1 addition & 1 deletion content/docs/gadgets/add2.md
Original file line number Diff line number Diff line change
Expand Up @@ -192,7 +192,7 @@ Where we get the "For $X$" due to zeroing parts of the polynomials (see [zero1](
2. The rest of the values in $\mathsf{Acc}$ are of the form $\mathsf{Acc}[i]=\mathsf{Arr}[i]+\mathsf{Acc}[i-1]$
3. The first value in $\mathsf{Acc}$ matches $\mathsf{Sum}_\mathsf{Arr}$

Which are precisely the conditions the Intuitions sections explains will hold if the prover contructs their Accumulator by following the protocol and using $\mathsf{Arr}$ such that $\mathsf{Sum}_\mathsf{Arr}=\sum_{i = 0}^{n-1} \mathsf{Arr}[i] \space \forall i \in [0, n - 1]$. This is what we assumed true about the prover, thus the $Y_\mathsf{Zero}(X)$ it creates by following the protocol is zero, and its transcipt will be accepted.
Which are precisely the conditions the Intuitions sections explains will hold if the prover contructs their Accumulator by following the protocol and using $\mathsf{Arr}$ such that $\mathsf{Sum}_\mathsf{Arr}=\sum_{i = 0}^{n-1} \mathsf{Arr}[i] \space \forall i \in [0, n - 1]$. This is what we assumed true about the prover, thus the $Y_\mathsf{Zero}$ it creates by following the protocol is zero, and its transcipt will be accepted.

### Soundness

Expand Down
8 changes: 4 additions & 4 deletions content/docs/gadgets/add3.md
Original file line number Diff line number Diff line change
Expand Up @@ -176,7 +176,7 @@ Finally, if the constraint system is true, the following constraint will be true

### Completeness

If $Y_\mathsf{Zero}$ is zero, then $\mathcal{V}$ will accept. Therefore, to show completeness, we show that any prover who holds $\mathsf{Arr}$ such that $\sum_{i = 0}^{n-1} \mathsf{Arr}_1[i]=\sum_{i = 0}^{n-1} \mathsf{Arr}_2[i] \space \forall i \in [0, n - 1]$ can follow the steps outlined in the above protocol and the resulting $Y_\mathsf{Zero}$ will be equal to zero. To see this, observed that $Y_\mathsf{Zero}$
If $Y_\mathsf{Zero}$ is zero, then $\mathcal{V}$ will accept. Therefore, to show completeness, we show that any prover who holds $\mathsf{Arr}_1$ and $\mathsf{Arr}_2$ such that $\sum_{i = 0}^{n-1} \mathsf{Arr}_1[i]=\sum_{i = 0}^{n-1} \mathsf{Arr}_2[i] \space \forall i \in [0, n - 1]$ can follow the steps outlined in the above protocol and the resulting $Y_\mathsf{Zero}$ will be equal to zero. To see this, observed that $Y_\mathsf{Zero}$

$ = Y_\mathsf{Vanish1} + \rho Y_\mathsf{Vanish2} + \rho^2 Y_\mathsf{Vanish3} + \rho^3 Y_\mathsf{Vanish4} + \rho^4 Y_\mathsf{Vanish5}- Q(\zeta)\cdot (\zeta^\kappa - 1)$

Expand Down Expand Up @@ -212,7 +212,7 @@ Where we get the "For $X$" due to zeroing parts of the polynomials (see [zero1](
4. The rest of the values in $\mathsf{Acc}_2$ are of the form $\mathsf{Acc_2}[i]=\mathsf{Arr_2}[i]+\mathsf{Acc_2}[i-1]$
5. The first value in $\mathsf{Acc_1}$ matches the first value in $\mathsf{Acc_2}$

Which are precisely the conditions the Intuitions sections explains will hold if the prover contructs their Accumulators by following the protocol and using $\mathsf{Arr}_1$ and $\mathsf{Arr_2}$ such that $\sum_{i = 0}^{n-1} \mathsf{Arr}_1[i] =\sum_{i = 0}^{n-1} \mathsf{Arr}_2[i] \space \forall i \in [0, n - 1]$. This is what we assumed true about the prover, thus the $Y_\mathsf{Zero}(X)$ it creates by following the protocol is zero, and its transcipt will be accepted.
Which are precisely the conditions the Intuitions sections explains will hold if the prover contructs their Accumulators by following the protocol and using $\mathsf{Arr}_1$ and $\mathsf{Arr_2}$ such that $\sum_{i = 0}^{n-1} \mathsf{Arr}_1[i] =\sum_{i = 0}^{n-1} \mathsf{Arr}_2[i] \space \forall i \in [0, n - 1]$. This is what we assumed true about the prover, thus the $Y_\mathsf{Zero}$ it creates by following the protocol is zero, and its transcipt will be accepted.

### Soundness

Expand All @@ -234,7 +234,7 @@ Our proof is as follows:

For the second win condition to be fulfilled, one of the five constraints must be false. But then the $\mathsf{Poly}_\mathsf{Vanish}$ corresponding to that constraint is not vanishing on $\mathcal{H}_\kappa$, so $Q(X)$ is not a polynomial (it is a rational function). This means that $\mathcal{A}$ cannot calcuated the correct commitment value $g^{Q(\tau)}$ without solving the t-SDH. Thus, $\mathcal{A}$ chooses an arbitrary value for $Q(\tau)$ and writes $K_Q = g^{Q(\tau)}$ to the transcript. Before this, it also writes commitments to $\mathsf{Poly}_\mathsf{Acc_1}(X)$, $\mathsf{Poly}_\mathsf{Arr_1}(X)$, $\mathsf{Poly}_\mathsf{Acc_2}(X)$, and $\mathsf{Poly}_\mathsf{Arr_2}(X)$. Each commitment $\mathcal{A}$ has written is a linear combination of the elements in $[g, g^\tau, g^{\tau^2}, \dots,g^{\tau^{n-1}}]$. $\mathcal{E}$ is given these coefficients (since $\mathcal{A}$ is an algebraic adversary) so $\mathcal{E}$ can output the original polynomials.

$\mathcal{A}$ then obtains the random challenge $\zeta$ (using strong Fiat-Shamir). By the binding property of KZG commitments, $\mathsf{Poly}_\mathsf{Arr_1}(\zeta)$, $\mathsf{Poly}_\mathsf{Acc_1}(\zeta)$, $\mathsf{Poly}_\mathsf{Acc_1}(\zeta \cdot \omega)$, $\mathsf{Poly}_\mathsf{Arr_2}(\zeta)$, $\mathsf{Poly}_\mathsf{Acc_2}(\zeta)$, and $\mathsf{Poly}_\mathsf{Acc_2}(\zeta \cdot \omega)$ can each only feasibliy be opened to one value. For $\mathcal{A}$ to have the verifier accept, it must produce a proof that $Q(\zeta)$ opens to $Q(\zeta) = \frac{Y_\mathsf{Vanish1} + \rho Y_\mathsf{Vanish2} + \rho^2 Y_\mathsf{Vanish3} + \rho^3 Y_\mathsf{Vanish4} + \rho^4Y_\mathsf{Vanish5}}{(\zeta^n - 1)}$. This means being able to produce $g^{q(\tau)}$ where $q(\tau) = \frac{Q(\tau) - Q(\zeta)}{\tau - \zeta}$ and $Q(\zeta) = \frac{Y_\mathsf{Vanish1} + \rho Y_\mathsf{Vanish2} + \rho^2 Y_\mathsf{Vanish3} + \rho^3 Y_\mathsf{Vanish4} + \rho^4Y_\mathsf{Vanish5}}{(\zeta^n - 1)}$. Since $Q(\tau)$ and $Q(\zeta)$ are known, this implies knowing $g^{\frac{1}{\tau - \zeta}}$. Thus $\mathcal{A}$ would have found $\langle\zeta,g^{\frac{1}{\tau - \zeta}}\rangle$, which is the t-SDH problem. We have shown that creating an accepting proof reduces to the t-SDH, so $\mathcal{A}$'s probability of success is negligible.
$\mathcal{A}$ then obtains the random challenge $\zeta$ (using strong Fiat-Shamir). By the binding property of KZG commitments, $\mathsf{Poly}_\mathsf{Arr_1}(\zeta)$, $\mathsf{Poly}_\mathsf{Acc_1}(\zeta)$, $\mathsf{Poly}_\mathsf{Acc_1}(\zeta \cdot \omega)$, $\mathsf{Poly}_\mathsf{Arr_2}(\zeta)$, $\mathsf{Poly}_\mathsf{Acc_2}(\zeta)$, and $\mathsf{Poly}_\mathsf{Acc_2}(\zeta \cdot \omega)$ can each only feasibliy be opened to one value. For $\mathcal{A}$ to have the verifier accept, it must produce a proof that $Q(\zeta)$ opens to $Q(\zeta) = \frac{Y_\mathsf{Vanish1} + \rho Y_\mathsf{Vanish2} + \rho^2 Y_\mathsf{Vanish3} + \rho^3 Y_\mathsf{Vanish4} + \rho^4Y_\mathsf{Vanish5}}{(\zeta^\kappa - 1)}$. This means being able to produce $g^{q(\tau)}$ where $q(\tau) = \frac{Q(\tau) - Q(\zeta)}{\tau - \zeta}$ and $Q(\zeta) = \frac{Y_\mathsf{Vanish1} + \rho Y_\mathsf{Vanish2} + \rho^2 Y_\mathsf{Vanish3} + \rho^3 Y_\mathsf{Vanish4} + \rho^4Y_\mathsf{Vanish5}}{(\zeta^\kappa - 1)}$. Since $Q(\tau)$ and $Q(\zeta)$ are known, this implies knowing $g^{\frac{1}{\tau - \zeta}}$. Thus $\mathcal{A}$ would have found $\langle\zeta,g^{\frac{1}{\tau - \zeta}}\rangle$, which is the t-SDH problem. We have shown that creating an accepting proof reduces to the t-SDH, so $\mathcal{A}$'s probability of success is negligible.

### Zero-Knowledge

Expand All @@ -244,6 +244,6 @@ The simulator $\mathcal{S}$ chooses arbitrary values for ${\mathsf{Poly}_\mathsf

Now, $\mathcal{S}$ generates the second random challenge point $\zeta$ (which we assume is not in $\mathcal{H}_\kappa$; if it is in $\mathcal{H}_\kappa$, $\mathcal{S}$ simply restarts and runs from the beginning). This is once again by strong Fiat-Shamir. $\mathcal{S}$ then create fake opening proofs for ${\mathsf{Poly}_\mathsf{Arr_1}(\zeta)}$, ${\mathsf{Poly}_\mathsf{Acc_1}(\zeta)}$, ${\mathsf{Poly}_\mathsf{Acc_1}(\zeta \cdot \omega)}$, ${\mathsf{Poly}_\mathsf{Arr_2}(\zeta)}$, ${\mathsf{Poly}_\mathsf{Acc_2}(\zeta)}$, and $\mathsf{Poly}_\mathsf{Acc_2}(\zeta\cdot\omega)$, to arbitrary values. This is done using the knowledge of $\tau$, calculating the respective witness $q(\tau) = \frac{{f(\tau) - f(\zeta)}}{\tau - \zeta}$ for each of the polynomials.

Finally, $\mathcal{S}$ creates a fake opening proof for $Q(\zeta) = \frac{Y_\mathsf{Vanish1} + \rho Y_\mathsf{Vanish2} + \rho^2 Y_\mathsf{Vanish3} + \rho^3 Y_\mathsf{Vanish4} + \rho^4Y_\mathsf{Vanish5}}{(\zeta^n - 1)}$. This is done using knowledge of $\tau$ to calculate an accepting witness $q(\tau)$, as above. This means that $Y_\mathsf{Zero}$ will be zero, and the transcript will be accepted by the verifier. It is indistinguishable from a transcript generates from a real execution, since $\mathsf{PolyCommit}_\mathsf{Ped}$ has the property of Indistinguishability of Commitments due to the randomization by $h^{\hat{\phi}(x)}$.
Finally, $\mathcal{S}$ creates a fake opening proof for $Q(\zeta) = \frac{Y_\mathsf{Vanish1} + \rho Y_\mathsf{Vanish2} + \rho^2 Y_\mathsf{Vanish3} + \rho^3 Y_\mathsf{Vanish4} + \rho^4Y_\mathsf{Vanish5}}{(\zeta^\kappa - 1)}$. This is done using knowledge of $\tau$ to calculate an accepting witness $q(\tau)$, as above. This means that $Y_\mathsf{Zero}$ will be zero, and the transcript will be accepted by the verifier. It is indistinguishable from a transcript generates from a real execution, since $\mathsf{PolyCommit}_\mathsf{Ped}$ has the property of Indistinguishability of Commitments due to the randomization by $h^{\hat{\phi}(x)}$.

- For mult2, the proof is written with a simulator that doesn't know the trapdoor; however, with small alterations the proof for mult2 should apply here and vice versa
Loading

0 comments on commit a2514d4

Please sign in to comment.