diff --git a/easy/main.typ b/easy/main.typ index d080880..0649a04 100644 --- a/easy/main.typ +++ b/easy/main.typ @@ -45,6 +45,7 @@ #part[SNARKs] #chapter("src/zkintro.typ") #chapter("src/plonk.typ") +#chapter("src/copy-constraints.typ") #chapter("src/fs.typ") #chapter("src/snark-takeaways.typ") diff --git a/easy/src/copy-constraints.typ b/easy/src/copy-constraints.typ new file mode 100644 index 0000000..d8c03a0 --- /dev/null +++ b/easy/src/copy-constraints.typ @@ -0,0 +1,252 @@ +#import "preamble.typ":* + +#let rbox(s) = [#text(red)[#ellipse(stroke: red, inset: 2pt, s)]] +#let bbox(s) = [#text(blue)[#rect(stroke: blue, inset: 4pt, s)]] + += Copy Constraints in PLONK + +To ease into it slightly, +we provide a solution to a "simpler" problem called "permutation-check". +Then we explain how to deal with the full copy check. + +== Easier case: permutation-check + +#problem[ +Suppose we have polynomials $P, Q in FF_q [X]$ +which encode two vectors of values +$ arrow(p) &= angle.l P(omega^1), P(omega^2), ..., P(omega^n) angle.r \ + arrow(q) &= angle.l Q(omega^1), Q(omega^2), ..., Q(omega^n) angle.r. $ +Is there a way that one can quickly verify $arrow(p)$ and $arrow(q)$ +are the same up to permutation of the $n$ entries? +] + +Well, actually, it would be necessary and sufficient for the identity +#eqn[ + $ (T+P(omega^1))(T+P(omega^2)) ... (T+P(omega^n)) \ + = (T+Q(omega^1))(T+Q(omega^2)) ... (T+Q(omega^n)) $ + +] +to be true, in the sense both sides are the same polynomial in $FF_q [T]$ +in a single formal variable $T$. +And for that, it is sufficient that a single random challenge +$T = lambda$ passes @permcheck-poly: if the two sides of @permcheck-poly +aren't the same polynomial, +then the two sides can have at most $n-1$ common values. +So for a randomly chosen $lambda$ +(chosen from a field with $q approx 2^(256)$ elements), +the chances that $T = lambda$ passes @permcheck-poly are extremely small. + +We can then get a proof of @permcheck-poly +using the technique of adding an _accumulator polynomial_. +The idea is this: Victor picks a random challenge $lambda in FF_q$. +Peggy then interpolates the polynomial $F_P in FF_q [T]$ such that +$ + F_P (omega^1) &= lambda + P(omega^1) \ + F_P (omega^2) &= (lambda + P(omega^1))(lambda + P(omega^2)) \ + &dots.v \ + F_P (omega^n) &= (lambda + P(omega^1))(lambda + P(omega^2)) dots.c (lambda + P(omega^n)). +$ +Then the accumulator $F_Q in FF_q [T]$ is defined analogously. + +So to prove @permcheck-poly, the following algorithm works: + +#algorithm[Permutation-check][ + Suppose Peggy has committed $Com(P)$ and $Com(Q)$. + + 1. Victor sends a random challenge $lambda in FF_q$. + 2. Peggy interpolates polynomials $F_P [T]$ and $F_Q [T]$ + such that $F_P (omega^k) = product_(i <= k) (lambda + P(omega^i))$. + Define $F_Q$ similarly. + Peggy sends $Com(F_P)$ and $Com(F_Q)$. + 3. Peggy uses @root-check to prove all of the following statements: + + - $F_P (X) - (lambda + P(X))$ + vanishes at $X = omega$; + - $F_P (omega X) - (lambda + P(omega X)) F_P (X)$ + vanishes at $X in {omega, ..., omega^(n-1)}$; + - The previous two statements also hold with $F_P$ replaced by $F_Q$; + - $F_P (X) - F_Q (X)$ vanishes at $X = 1$. +] + +== Copy check + +Moving on to copy-check, let's look at a concrete example where $n=4$. +Suppose that our copy constraints were +$ #rbox($a_1$) = #rbox($a_4$) = #rbox($c_4$) + #h(1em) "and" #h(1em) + #bbox($b_2$) = #bbox($c_1$). $ +(We've colored and circled the variables that will move around for readability.) +So, the copy constraint means we want the following equality of matrices: +#eqn[ + $ + mat( + a_1, b_1, c_1; + a_2, b_2, c_2; + a_3, b_3, c_3; + a_4, b_4, c_4 + ) + = + mat( + #rbox($a_4$), b_1, #bbox($b_2$) ; + a_2, #bbox($c_1$), c_2 ; + a_3, b_3, c_3 ; + #rbox($c_4$), b_4, #rbox($a_1$); + ) + . + $ + +] +Again, our goal is to make this into a _single_ equation. +There's a really clever way to do this by tagging each entry with $+ eta^j omega^k mu$ +in reading order for $j = 0, 1, 2$ and $k = 1, ..., n$; +here $eta in FF_q$ is any number such that $eta^2$ doesn't happen to be a power of $omega$, +so all the tags are distinct. +Specifically, if @copy1 is true, then for any $mu in FF_q$, we also have +#eqn[ + $ + & mat( + a_1 + omega^1 mu, b_1 + eta omega^1 mu, c_1 + eta^2 omega^1 mu; + a_2 + omega^2 mu, b_2 + eta omega^2 mu, c_2 + eta^2 omega^2 mu; + a_3 + omega^3 mu, b_3 + eta omega^3 mu, c_3 + eta^2 omega^3 mu; + a_4 + omega^4 mu, b_4 + eta omega^4 mu, c_4 + eta^2 omega^4 mu; + ) \ + =& + mat( + #rbox($a_4$) + omega^1 mu, b_1 + eta omega^1 mu, #bbox($b_2$) + eta^2 omega^1 mu; + a_2 + omega^2 mu, #bbox($c_1$) + eta omega^2 mu, c_2 + eta^2 omega^2 mu; + a_3 + omega^3 mu, b_3 + eta omega^3 mu, c_3 + eta^2 omega^3 mu; + #rbox($c_4$) + omega^4 mu, b_4 + eta omega^4 mu, #rbox($a_1$) + eta^2 omega^4 mu; + ) + . + $ + +] +Now how can the prover establish @copy2 succinctly? +The answer is to run a permutation-check on the $3n$ entries of @copy2! +The prover will simply prove that the twelve matrix entries +of the matrix on the left +are a permutation of the twelve matrix entries +of the matrix on the right. + +The reader should check that this is correct! +If the prover starts with values $a_i$, $b_i$, and $c_i$ +that don't satisfy all the copy constraints, +then a randomly selected $mu$ is very unlikely to satisfy this +permutation check. +The right-hand side will not be a permutation of the left-hand side, +and the check will fail. + +To clean things up, shuffle the $12$ terms on the right-hand side of @copy2 +so that each variable is in the cell it started at: +We want to prove +#eqn[ + $ + mat( + a_1 + omega^1 mu, b_1 + eta omega^1 mu, c_1 + eta^2 omega^1 mu; + a_2 + omega^2 mu, b_2 + eta omega^2 mu, c_2 + eta^2 omega^2 mu; + a_3 + omega^3 mu, b_3 + eta omega^3 mu, c_3 + eta^2 omega^3 mu; + a_4 + omega^4 mu, b_4 + eta omega^4 mu, c_4 + eta^2 omega^4 mu; + ) \ + "is a permutation of" \ + mat( + a_1 + #rbox($eta^2 omega^4 mu$), b_1 + eta omega^1 mu, c_1 + #bbox($eta omega^2 mu$) ; + a_2 + omega^2 mu, b_2+ #bbox($eta^2 omega^1 mu$), c_2 + eta^2 omega^2 mu; + a_3 + omega^3 mu, b_3 + eta omega^3 mu, c_3 + eta^2 omega^3 mu; + a_4 + #rbox($omega^1 mu$), b_4 + eta omega^4 mu, c_4 + #rbox($omega^4 mu$) + ) + . + $ + +] +The permutations needed are part of the problem statement, hence globally known. +So in this example, both parties are going to interpolate cubic polynomials +$sigma_a, sigma_b, sigma_c$ that encode the weird coefficients row-by-row: +$ + mat( + delim: #none, + sigma_a (omega^1) = #rbox($eta^2 omega^4$), + sigma_b (omega^1) = eta omega^1, + sigma_c (omega^1) = #bbox($eta omega^2$) ; + sigma_a (omega^2) = omega^2, + sigma_b (omega^2) = #bbox($eta^2 omega^1$), + sigma_c (omega^2) = eta^2 omega^2; + sigma_a (omega^3) = omega^3, + sigma_b (omega^3) = eta omega^3, + sigma_c (omega^3) = eta^2 omega^3; + sigma_a (omega^4) = #rbox($omega^1$), + sigma_b (omega^4) = eta omega^4, + sigma_c (omega^4) = #rbox($omega^4$). + ) +$ +Then the prover can start defining accumulator polynomials, after +re-introducing the random challenge $lambda$ from permutation-check. +We're going to need six in all, three for each side of @copy3: +we call them $F_a$, $F_b$, $F_c$, $F_a'$, $F_b'$, $F_c'$. +The ones on the left-hand side are interpolated so that +#eqn[ + $ + F_a (omega^k) &= product_(i <= k) (a_i + omega^i mu + lambda) \ + F_b (omega^k) &= product_(i <= k) (b_i + eta omega^i mu + lambda) \ + F_c (omega^k) &= product_(i <= k) (c_i + eta^2 omega^i mu + lambda) \ + $ + +] +while the ones on the right have the extra permutation polynomials +#eqn[ + $ + F'_a (omega^k) &= product_(i <= k) (a_i + sigma_a (omega^i) mu + lambda) \ + F'_b (omega^k) &= product_(i <= k) (b_i + sigma_b (omega^i) mu + lambda) \ + F'_c (omega^k) &= product_(i <= k) (c_i + sigma_c (omega^i) mu + lambda). + $ + +] +And then we can run essentially the algorithm from before. +There are six initialization conditions +#eqn[ + $ + F_a (omega^1) &= A(omega^1) + omega^1 mu + lambda \ + F_b (omega^1) &= B(omega^1) + eta omega^1 mu + lambda \ + F_c (omega^1) &= C(omega^1) + eta^2 omega^1 mu + lambda \ + F_a (omega^1) &= A(omega^1) + sigma_a (omega^1) mu + lambda \ + F_b (omega^1) &= B(omega^1) + sigma_b (omega^1) mu + lambda \ + F_c (omega^1) &= C(omega^1) + sigma_c (omega^1) mu + lambda. + $ + +] +and six accumulation conditions +#eqn[ + $ + F_a (omega X) &= F_a (X) dot (A(omega X) + X mu + lambda) \ + F_b (omega X) &= F_b (X) dot (B(omega X) + eta X mu + lambda) \ + F_c (omega X) &= F_c (X) dot (C(omega X) + eta^2 X mu + lambda) \ + F'_a (omega X) &= F'_a (X) dot (A(omega X) + sigma_a (X) mu + lambda) \ + F'_b (omega X) &= F'_b (X) dot (B(omega X) + sigma_b (X) mu + lambda) \ + F'_c (omega X) &= F'_c (X) dot (C(omega X) + sigma_c (X) mu + lambda) \ + $ + +] +before the final product condition +#eqn[ + $ + F_a (1) F_b (1) F_c (1) = F'_a (1) F'_b (1) F'_c (1) + $ + +] + +To summarize, the copy-check goes as follows: +#algorithm[Copy-check][ + 0. Peggy has already sent the three commitments + $Com(A), Com(B), Com(C)$ to Victor; + these commitments bind her to the values of all the variables + $a_i$, $b_i$, and $c_i$. + 1. Both parties compute the degree $n-1$ polynomials + $sigma_a, sigma_b, sigma_c in FF_q [X]$ described above, + based on the copy constraints in the problem statement. + 2. Victor chooses random challenges $mu, lambda in FF_q$ and sends them to Peggy. + 3. Peggy interpolates the six accumulator polynomials $F_a$, ..., $F'_c$ defined + in @copycheck-left and @copycheck-right. + 4. Peggy uses @root-check to prove @copycheck-init holds. + 5. Peggy uses @root-check to prove @copycheck-accum holds + for $X in {omega, omega^2, ..., omega^(n-1)}$. + 6. Peggy uses @root-check to prove @copycheck-final holds. +] \ No newline at end of file diff --git a/easy/src/plonk.typ b/easy/src/plonk.typ index 0e109c7..514368e 100644 --- a/easy/src/plonk.typ +++ b/easy/src/plonk.typ @@ -9,14 +9,13 @@ == Arithmetization The promise of programmable cryptography is that we should be able to -perform zero-knowledge proofs for arbitrary functions. +perform proofs for arbitrary functions. That means we need a "programming language" that we'll write our function in. - For PLONK (and Groth16 in the next section), the choice that's used is: -*systems of quadratic equations over $FF_q$*. +*systems of quadratic equations over $FF_q$*. In other words, PLONK is going to +give us the ability to prove that we have solutions to a system of quadratic +equations. -In other words, PLONK is going to give us the ability to prove -that we have solutions to a system of quadratic equations. #situation[ Suppose we have a system of $m$ equations in $k$ variables $x_1, dots, x_k$: $ @@ -36,29 +35,18 @@ that we have solutions to a system of quadratic equations. the $k$ values $x_1, dots, x_k$ satisfy all $m$ quadratic equations. ] -This leads to the natural question of how a function like -the hash function SHA-256 can be encoded -into a system of quadratic equations. -Well, quadratic equations over $FF_q$, -viewed as an NP-problem called Quad-SAT, is NP-complete, -as the following example shows. - -(If you're not familiar with NP-completeness, -the point of the example is to show that -"any problem" can be converted to a system of quadratic equations, -so that solutions to the problem give you -solutions to the system of equations. - -In the example, the "any problem" will be encoded -as a Boolean algebra problem called 3-SAT: -a system of constraints, like "(a_1 AND a_2) OR NOT a_3," -in variables $a_1, a_2, dots$ that can take the Boolean values -TRUE or FALSE.) - -#remark([Quad-SAT is pretty obviously NP-complete])[ - If you can't see right away that Quad-SAT is NP-complete, - the following example instance can help, - showing how to convert any instance of 3-SAT into a Quad-SAT problem: +This leads to the natural question of how a function like SHA-256 can be encoded +into a system of quadratic equations. This process of encoding a problem +into algebra is called _arithmetization_. It turns out that quadratic equations +over $FF_q$, viewed as an NP-problem called Quad-SAT, is _NP-complete_; +recall that NP-complete problems are that they are problems complex +enough that all problems in the well-known family of NP problems reduce to +them; in other words, any NP problem can be rewritten into an NP-complete problem. If you are not familiar with this concept, the upshot is that Quad-SAT +being NP-complete means it can serve as a reasonable arithmetization that can +express most reasonable (NP) problems. + +#remark([Quad-SAT is NP-complete])[ + We assume knowledge of 3-SAT and it being NP-complete. The following example instance illustrates how to convert any instance of 3-SAT into a Quad-SAT problem: $ x_i^2 &= x_i #h(1em) forall 1 <= i <= 1000 & \ y_1 &= (1-x_(42)) dot x_(17), & #h(1em) & 0 = y_1 dot x_(53) & \ @@ -293,250 +281,9 @@ or there are at most $3n-4$ values for which it's true == Step 3: Proving the copy constraints -The copy constraints are the trickier step. -There are a few moving parts to this idea, so to ease into it slightly, -we provide a solution to a "simpler" problem called "permutation-check". -Then we explain how to deal with the full copy check. - -=== Easier case: permutation-check - -Suppose we have polynomials $P, Q in FF_q [X]$ -which encode two vectors of values -$ arrow(p) &= angle.l P(omega^1), P(omega^2), ..., P(omega^n) angle.r \ - arrow(q) &= angle.l Q(omega^1), Q(omega^2), ..., Q(omega^n) angle.r. $ -Is there a way that one can quickly verify $arrow(p)$ and $arrow(q)$ -are the same up to permutation of the $n$ entries? - -Well, actually, it would be necessary and sufficient for the identity -#eqn[ - $ (T+P(omega^1))(T+P(omega^2)) ... (T+P(omega^n)) \ - = (T+Q(omega^1))(T+Q(omega^2)) ... (T+Q(omega^n)) $ - -] -to be true, in the sense both sides are the same polynomial in $FF_q [T]$ -in a single formal variable $T$. -And for that, it is sufficient that a single random challenge -$T = lambda$ passes @permcheck-poly: if the two sides of @permcheck-poly -aren't the same polynomial, -then the two sides can have at most $n-1$ common values. -So for a randomly chosen $lambda$ -(chosen from a field with $q approx 2^(256)$ elements), -the chances that $T = lambda$ passes @permcheck-poly are extremely small. - -We can then get a proof of @permcheck-poly -using the technique of adding an _accumulator polynomial_. -The idea is this: Victor picks a random challenge $lambda in FF_q$. -Peggy then interpolates the polynomial $F_P in FF_q [T]$ such that -$ - F_P (omega^1) &= lambda + P(omega^1) \ - F_P (omega^2) &= (lambda + P(omega^1))(lambda + P(omega^2)) \ - &dots.v \ - F_P (omega^n) &= (lambda + P(omega^1))(lambda + P(omega^2)) dots.c (lambda + P(omega^n)). -$ -Then the accumulator $F_Q in FF_q [T]$ is defined analogously. - -So to prove @permcheck-poly, the following algorithm works: - -#algorithm[Permutation-check][ - Suppose Peggy has committed $Com(P)$ and $Com(Q)$. - - 1. Victor sends a random challenge $lambda in FF_q$. - 2. Peggy interpolates polynomials $F_P [T]$ and $F_Q [T]$ - such that $F_P (omega^k) = product_(i <= k) (lambda + P(omega^i))$. - Define $F_Q$ similarly. - Peggy sends $Com(F_P)$ and $Com(F_Q)$. - 3. Peggy uses @root-check to prove all of the following statements: - - - $F_P (X) - (lambda + P(X))$ - vanishes at $X = omega$; - - $F_P (omega X) - (lambda + P(omega X)) F_P (X)$ - vanishes at $X in {omega, ..., omega^(n-1)}$; - - The previous two statements also hold with $F_P$ replaced by $F_Q$; - - $F_P (X) - F_Q (X)$ vanishes at $X = 1$. -] - -=== Copy check - -Moving on to copy-check, let's look at a concrete example where $n=4$. -Suppose that our copy constraints were -$ #rbox($a_1$) = #rbox($a_4$) = #rbox($c_4$) - #h(1em) "and" #h(1em) - #bbox($b_2$) = #bbox($c_1$). $ -(We've colored and circled the variables that will move around for readability.) -So, the copy constraint means we want the following equality of matrices: -#eqn[ - $ - mat( - a_1, b_1, c_1; - a_2, b_2, c_2; - a_3, b_3, c_3; - a_4, b_4, c_4 - ) - = - mat( - #rbox($a_4$), b_1, #bbox($b_2$) ; - a_2, #bbox($c_1$), c_2 ; - a_3, b_3, c_3 ; - #rbox($c_4$), b_4, #rbox($a_1$); - ) - . - $ - -] -Again, our goal is to make this into a _single_ equation. -There's a really clever way to do this by tagging each entry with $+ eta^j omega^k mu$ -in reading order for $j = 0, 1, 2$ and $k = 1, ..., n$; -here $eta in FF_q$ is any number such that $eta^2$ doesn't happen to be a power of $omega$, -so all the tags are distinct. -Specifically, if @copy1 is true, then for any $mu in FF_q$, we also have -#eqn[ - $ - & mat( - a_1 + omega^1 mu, b_1 + eta omega^1 mu, c_1 + eta^2 omega^1 mu; - a_2 + omega^2 mu, b_2 + eta omega^2 mu, c_2 + eta^2 omega^2 mu; - a_3 + omega^3 mu, b_3 + eta omega^3 mu, c_3 + eta^2 omega^3 mu; - a_4 + omega^4 mu, b_4 + eta omega^4 mu, c_4 + eta^2 omega^4 mu; - ) \ - =& - mat( - #rbox($a_4$) + omega^1 mu, b_1 + eta omega^1 mu, #bbox($b_2$) + eta^2 omega^1 mu; - a_2 + omega^2 mu, #bbox($c_1$) + eta omega^2 mu, c_2 + eta^2 omega^2 mu; - a_3 + omega^3 mu, b_3 + eta omega^3 mu, c_3 + eta^2 omega^3 mu; - #rbox($c_4$) + omega^4 mu, b_4 + eta omega^4 mu, #rbox($a_1$) + eta^2 omega^4 mu; - ) - . - $ - -] -Now how can the prover establish @copy2 succinctly? -The answer is to run a permutation-check on the $3n$ entries of @copy2! -The prover will simply prove that the twelve matrix entries -of the matrix on the left -are a permutation of the twelve matrix entries -of the matrix on the right. - -The reader should check that this is correct! -If the prover starts with values $a_i$, $b_i$, and $c_i$ -that don't satisfy all the copy constraints, -then a randomly selected $mu$ is very unlikely to satisfy this -permutation check. -The right-hand side will not be a permutation of the left-hand side, -and the check will fail. - -To clean things up, shuffle the $12$ terms on the right-hand side of @copy2 -so that each variable is in the cell it started at: -We want to prove -#eqn[ - $ - mat( - a_1 + omega^1 mu, b_1 + eta omega^1 mu, c_1 + eta^2 omega^1 mu; - a_2 + omega^2 mu, b_2 + eta omega^2 mu, c_2 + eta^2 omega^2 mu; - a_3 + omega^3 mu, b_3 + eta omega^3 mu, c_3 + eta^2 omega^3 mu; - a_4 + omega^4 mu, b_4 + eta omega^4 mu, c_4 + eta^2 omega^4 mu; - ) \ - "is a permutation of" \ - mat( - a_1 + #rbox($eta^2 omega^4 mu$), b_1 + eta omega^1 mu, c_1 + #bbox($eta omega^2 mu$) ; - a_2 + omega^2 mu, b_2+ #bbox($eta^2 omega^1 mu$), c_2 + eta^2 omega^2 mu; - a_3 + omega^3 mu, b_3 + eta omega^3 mu, c_3 + eta^2 omega^3 mu; - a_4 + #rbox($omega^1 mu$), b_4 + eta omega^4 mu, c_4 + #rbox($omega^4 mu$) - ) - . - $ - -] -The permutations needed are part of the problem statement, hence globally known. -So in this example, both parties are going to interpolate cubic polynomials -$sigma_a, sigma_b, sigma_c$ that encode the weird coefficients row-by-row: -$ - mat( - delim: #none, - sigma_a (omega^1) = #rbox($eta^2 omega^4$), - sigma_b (omega^1) = eta omega^1, - sigma_c (omega^1) = #bbox($eta omega^2$) ; - sigma_a (omega^2) = omega^2, - sigma_b (omega^2) = #bbox($eta^2 omega^1$), - sigma_c (omega^2) = eta^2 omega^2; - sigma_a (omega^3) = omega^3, - sigma_b (omega^3) = eta omega^3, - sigma_c (omega^3) = eta^2 omega^3; - sigma_a (omega^4) = #rbox($omega^1$), - sigma_b (omega^4) = eta omega^4, - sigma_c (omega^4) = #rbox($omega^4$). - ) -$ -Then the prover can start defining accumulator polynomials, after -re-introducing the random challenge $lambda$ from permutation-check. -We're going to need six in all, three for each side of @copy3: -we call them $F_a$, $F_b$, $F_c$, $F_a'$, $F_b'$, $F_c'$. -The ones on the left-hand side are interpolated so that -#eqn[ - $ - F_a (omega^k) &= product_(i <= k) (a_i + omega^i mu + lambda) \ - F_b (omega^k) &= product_(i <= k) (b_i + eta omega^i mu + lambda) \ - F_c (omega^k) &= product_(i <= k) (c_i + eta^2 omega^i mu + lambda) \ - $ - -] -while the ones on the right have the extra permutation polynomials -#eqn[ - $ - F'_a (omega^k) &= product_(i <= k) (a_i + sigma_a (omega^i) mu + lambda) \ - F'_b (omega^k) &= product_(i <= k) (b_i + sigma_b (omega^i) mu + lambda) \ - F'_c (omega^k) &= product_(i <= k) (c_i + sigma_c (omega^i) mu + lambda). - $ - -] -And then we can run essentially the algorithm from before. -There are six initialization conditions -#eqn[ - $ - F_a (omega^1) &= A(omega^1) + omega^1 mu + lambda \ - F_b (omega^1) &= B(omega^1) + eta omega^1 mu + lambda \ - F_c (omega^1) &= C(omega^1) + eta^2 omega^1 mu + lambda \ - F_a (omega^1) &= A(omega^1) + sigma_a (omega^1) mu + lambda \ - F_b (omega^1) &= B(omega^1) + sigma_b (omega^1) mu + lambda \ - F_c (omega^1) &= C(omega^1) + sigma_c (omega^1) mu + lambda. - $ - -] -and six accumulation conditions -#eqn[ - $ - F_a (omega X) &= F_a (X) dot (A(omega X) + X mu + lambda) \ - F_b (omega X) &= F_b (X) dot (B(omega X) + eta X mu + lambda) \ - F_c (omega X) &= F_c (X) dot (C(omega X) + eta^2 X mu + lambda) \ - F'_a (omega X) &= F'_a (X) dot (A(omega X) + sigma_a (X) mu + lambda) \ - F'_b (omega X) &= F'_b (X) dot (B(omega X) + sigma_b (X) mu + lambda) \ - F'_c (omega X) &= F'_c (X) dot (C(omega X) + sigma_c (X) mu + lambda) \ - $ - -] -before the final product condition -#eqn[ - $ - F_a (1) F_b (1) F_c (1) = F'_a (1) F'_b (1) F'_c (1) - $ - -] - -To summarize, the copy-check goes as follows: -#algorithm[Copy-check][ - 0. Peggy has already sent the three commitments - $Com(A), Com(B), Com(C)$ to Victor; - these commitments bind her to the values of all the variables - $a_i$, $b_i$, and $c_i$. - 1. Both parties compute the degree $n-1$ polynomials - $sigma_a, sigma_b, sigma_c in FF_q [X]$ described above, - based on the copy constraints in the problem statement. - 2. Victor chooses random challenges $mu, lambda in FF_q$ and sends them to Peggy. - 3. Peggy interpolates the six accumulator polynomials $F_a$, ..., $F'_c$ defined - in @copycheck-left and @copycheck-right. - 4. Peggy uses @root-check to prove @copycheck-init holds. - 5. Peggy uses @root-check to prove @copycheck-accum holds - for $X in {omega, omega^2, ..., omega^(n-1)}$. - 6. Peggy uses @root-check to prove @copycheck-final holds. -] +The copy constraints are the trickiest step. +There are a few moving parts to this idea, so we skip it for now and dedicate a +whole subsection to it. == Public and private witnesses diff --git a/easy/src/snark-takeaways.typ b/easy/src/snark-takeaways.typ index 3b2edc5..22fd49a 100644 --- a/easy/src/snark-takeaways.typ +++ b/easy/src/snark-takeaways.typ @@ -5,6 +5,6 @@ #green[ 1. A _SNARK_ can be used to succinctly prove that a piece of computation has been done correctly; specifically, it proves to some Verifier that the Prover had the K(nowledge) of some information that worked as feasible inputs to some computational circuit. 2. The _arithmetization_ of the circuit is a way of converting circuits to arithmetic. Specifically for PLONK (but also other SNARKs, e.g. Groth16), our arithmetization is systems of quadratic equations over $FF_q$, meaning that what PLONK does under the hood is proving that a system of these equations are satisfied. -3. The work under the hood of PLONK comes down to polynomial commitments (specifically KZG). The constructions "powered by" KZG power concepts such as copy checks and permutation checks, which are key to PLONK. +3. The work under the hood of PLONK comes down to polynomial commitments (specifically KZG). KZG allows PLONK's gate checks and copy checks. 4. The N(oninteractivity) of SNARKs basically come down to the _Fiat-Shamir heuristic_, which is very common in this field. Generally speaking, the "meat" of zkSNARKs are mostly about S(uccinctness) of the AR(guments). ]