zkSNARK

High-level idea

  1. Turn your problem (graph isomorphism, discrete log, etc.) into a function whose inputs you want to hide.
  2. Turn that function into an equivalent set of R1CS (or other) equations
    1. Basically, an arithmetic circuit, that is a bunch of + and * operations on prime field elements
    2. Simplified: equations of the form \(x_i + x_j = x_k, or x_i * x_j = x_k\)
  3. Generate a ZKP for satisfiability of the R1CS

zkSNARK prove constraints

The best is those zk protocols that generate a proof of the same size regardless of the length of the computation and the verification also takes the same time.

Example:

1
2
Function inputs: x1, x2, x3, x4
OUT = f(x) = (x1 + x2) * x3 - x4

zkSNARK: I know some secret (x1,x2,x3,x4) such that the result of this computation f is OUT. Here's is a signature that prove that I know such a tuple, without telling you what the tuple actually is.

From the perspective of a human, the procedure of the computation is made as follows:

1
2
3
4
Function inputs: x1, x2, x3, x4
y1 := x1 + x2
y2 := y1 * x3
OUT := y2 - x4

However, from perspective of SNARK generating the proof, where only + and * is made as follows: SNARK prover inputs: x1, x2, x3, x4, y1, y2, OUT SNARK prover output: a “signature” that only verifies if the following constraints are satisfied:

1
2
3
y1 == x1 + x2
y2 == y1 * x3
y2 == OUT + x4

The SNARK basically is just a proof of satifaction of some constraints. For the snark machinery, it will see seven varibles x1, x2, x3, x4, y1, y2, OUT. The prover's out is a signature、a proof that should only be valid if the above three equations are ture. OUT is the value that will be reveal to the verifier. The snark proof is about proving that the prover knows some six values satisfy this three equations for a particular public value of OUT. Proving that I know some solution to this set of equations is equivalent to proving that I have executed this function.

If you care about actually hiding some inputs, then the funtion you are computiong is better to be a funtion that cannot be recoverable or reversed, which is zkSNARK. But sometime you dont care about that, you just care about a succict proof of the computation, which is SNARK.

If the example include division, such as:

1
2
Function inputs: x1, x2, x3, x4
OUT = f(x) = (x1 + x2) / x3 - x4

Then, the computation can be seen as follows:

From the perspective of human,

1
2
3
4
Function inputs: x1, x2, x3, x4
y1 := x1 + x2
y2 := y1 / x3
OUT := y2 - x4

From the perspective of prover, (note the equivalence of the two representation)

1
2
3
4
5
SNARK prover inputs: x1, x2, x3, x4, y1, y2, OUT
SNARK prover output: a “signature” that only verifies if the following constraints are satisfied:
y1 == x1 + x2
y1 == y2 * x3 with x3 != 0
y2 == OUT + x4

In zkrepl, the code can be shown as follows:

1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
19
20
21
22
23
24
25
26
27
28
29
30
31
32
33
34
35
36
37
38
39
40
41
42
pragma circom 2.1.4;

template Example () {
    // instantiate the variables
    signal input x1;
    signal input x2;
    signal input x3;
    signal input x4;

    signal input y1;
    signal input y2;

    signal input OUT;

    // write the constraints
    y1 === x1 + x2;
    y1 === y2 * x3;
    y2 === OUT + x4;
}

// Circom allows you to specify which of your varibles are public to the verifier. By default, the varibles are private
component main { public [ OUT ] } = Example();

// the following lines is used to test whether the proof and verification is done right by using cases
/* INPUT = {
    "x1": "15",
    "x2": "13",
    "x3": "7",
    "x4": "1",

    "y1": "28",
    "y2": "4",
    "OUT": "3"
} */

// press shift + enter, "Everything went okay, circom safe" means the circom are able to generate the artifacts and proof of zkSANRK
/* if the following line appears under the “ARTIFACTS:"，it means constraint you write is ok,
which can be compiled as a proof, but the specific value you are using to test is not right, which is not meet the constraints
FAIL:
Error: Assert Failed.
Error in template Example_0 line: 17
*/

Note: In the end of the INPUT and before the }, no comma is allowed, or the error "Expected double-quoted property name in JSON at position 62" will be reported.

1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
19
20
21
22
23
24
25
26
27
28
29
30
31
32
33
34
pragma circom 2.1.4;

template Example () {
    // instantiate the variables
    signal input x1;
    signal input x2;
    signal input x3;
    signal input x4;

    signal y1;
    signal y2;

    signal output out;

    y1 <-- x1 + x2;
    y2 <-- y1 / x3;
    out <-- y2 - x4;

    // write the constraints
    y1 === x1 + x2;
    y1 === y2 * x3;
    y2 === out + x4;
}

// Circom allows you to specify which of your varibles are public to the verifier. By default, the varibles are private
component main = Example();

// the following lines is used to test whether the proof and verification is done right by using cases
/* INPUT = {
    "x1": "4",
    "x2": "6",
    "x3": "2",
    "x4": "1"
} */

The circom is a specification of a constraint system that you are allowed to prove satisfaction, rather than a program To elimanate the intermediate value redundancy for us, the circom provide the function like what we precompute the intermediate value in python or somewhere else.

1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
19
20
21
22
23
24
25
26
27
28
29
30
31
32
33
34
pragma circom 2.1.4;

template Example () {
    // instantiate the variables
    signal input x1;
    signal input x2;
    signal input x3;
    signal input x4;

    signal y1;
    signal y2;

    signal output out;

    y1 <-- x1 + x2;
    y2 <-- y1 / x3;
    out <-- y2 - x4;

    // write the constraints
    y1 === x1 + x2;
    y1 === y2 * x3;
    y2 === out + x4;
}

// Circom allows you to specify which of your varibles are public to the verifier. By default, the varibles are private
component main = Example();

// the following lines is used to test whether the proof and verification is done right by using cases
/* INPUT = {
    "x1": "4",
    "x2": "6",
    "x3": "2",
    "x4": "1"
} */

Num2Bits

1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
19
20
21
22
pragma circom 2.1.4;

template Num2Bits (nBits) {
    signal input in;
    signal input b[nBits];

    var sum = 0;
    for(var i = 0; i < nBits; i++){
        sum += (2**i) * b[i];
    }
    in === sum;
    for(var i = 0; i < nBits; i++){
        0 === b[i] * (b[i] - 1);
    }
}

component main { public [ b ] } = Num2Bits(5);
// note: b array is from b0 to b(n-1), the left bit is the least significant bit
/* INPUT = {
    "in": "11",
    "b":["1", "1", "0", "1","0"]
} */

simplify the above code,

1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
19
20
21
22
23
24
25
26
pragma circom 2.1.4;

template Num2Bits (nBits) {
    signal input in;
    signal output b[nBits];

    for(var i = 0; i < nBits; i++){
        //  b[i] <-- (in \ 2 ** i) % 2;
        b[i] <-- (in >> i) & 1;
    }

    var sum = 0;
    for(var i = 0; i < nBits; i++){
        sum += (2**i) * b[i];
    }
    in === sum;
    for(var i = 0; i < nBits; i++){
        0 === b[i] * (b[i] - 1);
    }
}

component main = Num2Bits(5);
// note: b array is from b0 to b(n-1), the left bit is the least significant bit
/* INPUT = {
    "in": "11"
} */

Errors like the following report, normally the problem is that a semicolon is forget to be put at the end of a sentences.

1
2
error[P1000]: UnrecognizedToken { token: (586, Token(78, "}"), 587), expected: ["\"!=\"", "\"%\"", "\"&\"", "\"&&\"", "\")\"", "\"*\"", "\"**\"", "\"+\"", "\",\"", "\"-\"", "\"-->\"", "\"/\"", "\":\"", "\";\"", "\"<\"", "\"<--\"", "\"<<\"", "\"<=\"", "\"<==\"", "\"=\"", "\"==\"", "\"===\"", "\"==>\"", "\">\"", "\">=\"", "\">>\"", "\"?\"", "\"\\\\\"", "\"]\"", "\"^\"", "\"|\"", "\"||\""] }
   ┌─ "main.circom":28:1

Note: the private input signal should be declared as signal input.

template and component

template is more like the declaration, and component is more like the initiation.

The input signal of a template allows us to connect a wire into the subcomponent of the whole subcircuit

1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
19
20
21
22
23
24
25
26
27
28
29
30
31
32
33
34
pragma circom 2.1.4;

template Num2Bits (nBits) {
    signal input in;
    signal output b[nBits];

    for(var i = 0; i < nBits; i++){
        //  b[i] <-- (in \ 2 ** i) % 2;
        b[i] <-- (in >> i) & 1;
    }

    var sum = 0;
    for(var i = 0; i < nBits; i++){
        sum += (2**i) * b[i];
    }
    in === sum;
    for(var i = 0; i < nBits; i++){
        0 === b[i] * (b[i] - 1);
    }
}

template Main(){
    signal input in;
    signal output thirdBit;
    component bitfier = Num2Bits(5);
    bitfier.in <== in;
    thirdBit <== bitfier.b[3] + 3; // the index of b is from 0
}

component main = Main();
// note: b array is from b0 to b(n-1), the left bit is the least significant bit
/* INPUT = {
    "in": "11"
} */

Poseidon hash function is a snark friendly hash, which is composed of a bunch of pluses and times operations.