使用 snarkjs 解析 circom 编译后的 r1cs 文件

snarkjs 文档 (从 circom 到 zkproof)

https://github.com/iden3/snarkjs

circom 文档 (从 circom 到 zkproof)

https://github.com/iden3/circom

https://docs.circom.io/getting-started/installation/

https://docs.circom.io/circom-language/formats/sym/

https://docs.circom.io/circom-language/formats/constraints-json/

https://docs.circom.io/circom-language/formats/simplification-json/

视频

Zero Knowledge Proofs: A Technical Deep Dive

https://www.youtube.com/watch?v=JOCUTtEeXyk

example1

circuit code

pragma circom 2.0.0;


template Multiplier2 () {

   // Declaration of signals.
   signal input x;
   signal input y;
   signal output z;


   // Constraints.
   z <== x * y;
}

 component main {public [x]} = Multiplier2();

compile

❯ circom circuit1.circom --r1cs --wasm --sym --inspect;
template instances: 1
non-linear constraints: 1
linear constraints: 0
public inputs: 1
private inputs: 1
public outputs: 1
wires: 4
labels: 4
Written successfully: ./circuit1.r1cs
Written successfully: ./circuit1.sym
Written successfully: ./circuit1_js/circuit1.wasm
Everything went okay

从中可以看出只有一个约束

non-linear constraints: 1

export r1cs.json

snarkjs r1cs export json circuit1.r1cs circuit1.r1cs.json

{
  "n8": 32,
  "prime": "21888242871839275222246405745257275088548364400416034343698204186575808495617",
  "nVars": 4,
  "nOutputs": 1,
  "nPubInputs": 1,
  "nPrvInputs": 1,
  "nLabels": 4,
  "nConstraints": 1,
  "useCustomGates": false,
  "constraints": [
    [
      {
        "2": "21888242871839275222246405745257275088548364400416034343698204186575808495616"
      },
      {
        "3": "1"
      },
      {
        "1": "21888242871839275222246405745257275088548364400416034343698204186575808495616"
      }
    ]
  ],
  "map": [0, 1, 2, 3],
  "customGates": [],
  "customGatesUses": []
}

witness

这个电路的 witness 是[1, z, x, y]

从"map": [0, 1, 2, 3]可以确定 witness 的数组长度

顺序为[1, output signals, public signals, private signals, other signals]

当 output signals / public signals / private signals / internal signals 每个类型内有多个 signal 时

按照他们在 circom 代码中定义的顺序来排列

敲黑板!!! 对于 public signals, 不是他们在 main 里定义 public 时的顺序，而是和其他 signal 一样按照 circom 代码中定义的顺序来排列

另外，普通的变量不会被记录到 witness 中, 例如var y = 0;

编译后的labels: 4应该也是对应了 witness 数组优化前的长度。

优化后有些 signal 会被去掉，所以实际的 witness 长度可能会减少，具体要看 r1cs.json 中的内容。

r1cs 解析

确定 prime

{
...
"prime": "21888242871839275222246405745257275088548364400416034343698204186575808495617"
...
}

constraints 约束的解析

{
  ...
  "constraints": [
    [
      {
        "2": "21888242871839275222246405745257275088548364400416034343698204186575808495616"
      },
      {
        "3": "1"
      },
      {
        "1": "21888242871839275222246405745257275088548364400416034343698204186575808495616"
      }
    ]
  ],
 ...
}

其中 21888242871839275222246405745257275088548364400416034343698204186575808495616 其实为-1

至于为什么不用 1, 这个我暂时回答不了, 还需要继续学习。

再结合约束其实就是 w◯A * w◯B = w◯C

(w 代表 witness)

这个 json 可以这么理解

{
  ...
 "constraints": [
  [
   /*A*/{
    "2": "-1",
   },
   /*B*/{
    "3": "1"
   },
   /*C*/{
    "1": "-1"
   }
  ]
 ],
 ...
}

再结合我们刚才提到的 witness 为[1, z, x, y]

可以得到 A 为 [0, 0, -1, 0]

(先构造一个和 witness 定义一样格式的数组，所有值为 0, 再按照 json 中的 “2”: “-1”, key 为 A 数组的下标，value 为 A 数组的值，即 A[2] = -1)

同理我们可以得到 B 为 [0, 0, 1, 0]

C 为[0, -1, 0, 0]

witness	z	x	y
A	0	-1	0
B	0	0	1
C	-1	0	0

w◯A 对应的表达式为 -x

w◯B 对应的表达式为 y

w◯C 对应的表达式为 -z

w◯A * w◯B = w◯C 也就是 -x \* y = -z

这对应着 circom 中的z <== x * y;

example2

circuit code

pragma circom 2.0.0;

template Multiplier2 () {

   // Declaration of signals.
   signal input x;
   signal input y;
   signal output z;


   // Constraints.
   z <== x * (y+1);
}

 component main {public [x]} = Multiplier2();

compile

❯ circom circuit2.circom --r1cs --wasm --sym --inspect;
template instances: 1
non-linear constraints: 1
linear constraints: 0
public inputs: 1
private inputs: 1
public outputs: 1
wires: 4
labels: 4
Written successfully: ./circuit2.r1cs
Written successfully: ./circuit2.sym
Written successfully: ./circuit2_js/circuit2.wasm
Everything went okay

从中可以看出只有一个约束

non-linear constraints: 1

export r1cs.json

snarkjs r1cs export json circuit2.r1cs circuit2.r1cs.json

{
  "n8": 32,
  "prime": "21888242871839275222246405745257275088548364400416034343698204186575808495617",
  "nVars": 4,
  "nOutputs": 1,
  "nPubInputs": 1,
  "nPrvInputs": 1,
  "nLabels": 4,
  "nConstraints": 1,
  "useCustomGates": false,
  "constraints": [
    [
      {
        "0": "21888242871839275222246405745257275088548364400416034343698204186575808495616",
        "3": "21888242871839275222246405745257275088548364400416034343698204186575808495616"
      },
      {
        "2": "1"
      },
      {
        "1": "21888242871839275222246405745257275088548364400416034343698204186575808495616"
      }
    ]
  ],
  "map": [0, 1, 2, 3],
  "customGates": [],
  "customGatesUses": []
}

witness

[1, z, x, y]

r1cs 解析

constraints 约束的解析

{
  ...
 "constraints": [
  [
   /*A*/{
    "0": "-1",
    "3": "-1",
   },
   /*B*/{
    "2": "1"
   },
   /*C*/{
    "1": "-1"
   }
  ]
 ],
 ...
}

witness	1	z	x	y
A	-1	0	0	-1
B	0	0	1	0
C	0	-1	0	0

w◯A 对应的表达式为 -(1+y)

w◯B 对应的表达式为 x

w◯C 对应的表达式为 -z

w◯A * w◯B = w◯C 也就是 -(1+y) * x = -z

这对应着 circom 中的z <== x * (y+1);

example3

circuit code

pragma circom 2.0.0;

template Multiplier2 () {

   // Declaration of signals.
   signal input x;
   signal input y;
   signal output z;


   // Constraints.
   z <== (x+1) * (y+1);
}

 component main {public [x]} = Multiplier2();

r1cs.json

{
  "n8": 32,
  "prime": "21888242871839275222246405745257275088548364400416034343698204186575808495617",
  "nVars": 4,
  "nOutputs": 1,
  "nPubInputs": 1,
  "nPrvInputs": 1,
  "nLabels": 4,
  "nConstraints": 1,
  "useCustomGates": false,
  "constraints": [
    [
      {
        "0": "21888242871839275222246405745257275088548364400416034343698204186575808495616",
        "2": "21888242871839275222246405745257275088548364400416034343698204186575808495616"
      },
      {
        "0": "1",
        "3": "1"
      },
      {
        "1": "21888242871839275222246405745257275088548364400416034343698204186575808495616"
      }
    ]
  ],
  "map": [0, 1, 2, 3],
  "customGates": [],
  "customGatesUses": []
}

witness

[1, z, x, y]

constraints

witness	1	z	x	y
A	-1	0	-1	0
B	1	0	0	1
C	0	-1	0	0

w◯A 对应的表达式为 -(1+x)

w◯B 对应的表达式为 1+y

w◯C 对应的表达式为 -z

w◯A * w◯B = w◯C 也就是 -(1+x) * (1+y) = -z

这对应着 circom 中的z <== (x+1) * (y+1);

example4

circuit code

pragma circom 2.0.0;

template Multiplier2 () {

   // Declaration of signals.
   signal temp;
   signal input y;
   signal output z;
   signal input a;
   signal input x;

   temp <== a * (y + 1);
   z <== (x+y) * temp;
}

component main {public [x, a]} = Multiplier2();

r1cs.json

{
  "n8": 32,
  "prime": "21888242871839275222246405745257275088548364400416034343698204186575808495617",
  "nVars": 6,
  "nOutputs": 1,
  "nPubInputs": 2,
  "nPrvInputs": 1,
  "nLabels": 6,
  "nConstraints": 2,
  "useCustomGates": false,
  "constraints": [
    [
      {
        "0": "21888242871839275222246405745257275088548364400416034343698204186575808495616",
        "4": "21888242871839275222246405745257275088548364400416034343698204186575808495616"
      },
      {
        "2": "1"
      },
      {
        "5": "21888242871839275222246405745257275088548364400416034343698204186575808495616"
      }
    ],
    [
      {
        "3": "21888242871839275222246405745257275088548364400416034343698204186575808495616",
        "4": "21888242871839275222246405745257275088548364400416034343698204186575808495616"
      },
      {
        "5": "1"
      },
      {
        "1": "21888242871839275222246405745257275088548364400416034343698204186575808495616"
      }
    ]
  ],
  "map": [0, 1, 2, 3, 4, 5],
  "customGates": [],
  "customGatesUses": []
}

witness

[1, z, a, x, y, temp]

"map": [0, 1, 2, 3, 4, 5] 确定 witness 数组长度
顺序为[1, output signals, public signals, private signals, internal signals]

重点注意 x 和 a 的顺序，以及 temp 的顺序
- 虽然public [x, a]中 x 在前面, 但是 x 和 a 的顺序应该由 circom 中的定义顺序确定
- temp 虽然是 circom 中第一个定义的 signal, 但是他应该是算 internal signals, 所以应该放在其他信号的后面

constraints

` “nConstraints”: 2`

一共有两个约束

相应的, 我们也可以看到 json 中的 constraints 数组中有两个元素

constraints 1

witness	1	a	y	temp
A	-1	0	-1	0
B	0	1	0	0
C	0	0	0	-1

A 对应的表达式为 -(1+y)

B 对应的表达式为 a

C 对应的表达式为 -temp

也就是 -(1+y) * a = -temp

这对应着 circom 中的temp <== (1+y)*a

constraints 2

witness	z	x	y	temp
A	0	-1	-1	0
B	0	0	0	1
C	-1	0	0	0

w◯A 对应的表达式为 -(x+y)

w◯B 对应的表达式为 temp

w◯C 对应的表达式为 -z

w◯A * w◯B = w◯C 也就是 -(x+y) * temp = -z

这对应着 circom 中的z <== (x+y)*temp

example5

circuit code

pragma circom 2.0.0;

template Multiplier2 () {

   // Declaration of signals.
   signal temp;
   signal input y;
   signal output z;
   signal input a;
   signal input x;



   // Constraints.
   temp <== (a + x) * (x + y + 3);
   z <== (x + y + a) * (temp + x + 1);
}

 component main {public [x, a]} = Multiplier2();

r1cs.json

{
  "n8": 32,
  "prime": "21888242871839275222246405745257275088548364400416034343698204186575808495617",
  "nVars": 6,
  "nOutputs": 1,
  "nPubInputs": 2,
  "nPrvInputs": 1,
  "nLabels": 6,
  "nConstraints": 2,
  "useCustomGates": false,
  "constraints": [
    [
      {
        "2": "21888242871839275222246405745257275088548364400416034343698204186575808495616",
        "3": "21888242871839275222246405745257275088548364400416034343698204186575808495616"
      },
      {
        "0": "3",
        "3": "1",
        "4": "1"
      },
      {
        "5": "21888242871839275222246405745257275088548364400416034343698204186575808495616"
      }
    ],
    [
      {
        "2": "21888242871839275222246405745257275088548364400416034343698204186575808495616",
        "3": "21888242871839275222246405745257275088548364400416034343698204186575808495616",
        "4": "21888242871839275222246405745257275088548364400416034343698204186575808495616"
      },
      {
        "0": "1",
        "3": "1",
        "5": "1"
      },
      {
        "1": "21888242871839275222246405745257275088548364400416034343698204186575808495616"
      }
    ]
  ],
  "map": [0, 1, 2, 3, 4, 5],
  "customGates": [],
  "customGatesUses": []
}

witness

[1, z, a, x, y, temp]

constraints

` “nConstraints”: 2`

一共有两个约束

相应的, 我们也可以看到 json 中的 constraints 数组中有两个元素

constraints 1

witness	1	a	x	y	temp
A	0	-1	-1	0	0
B	3	0	1	1	0
C	0	0	0	0	-1

w◯A 对应的表达式为 -(a+x)

w◯B 对应的表达式为 3+x+y

w◯C 对应的表达式为 -temp

w◯A * w◯B = w◯C 也就是 -(a+x) * (3+x+y) = -temp

这对应着 circom 中的temp <== (a + x) * (x + y + 3);

constraints 2

witness	1	z	a	x	y	temp
A	0	0	-1	-1	-1	0
B	1	0	0	1	0	1
C	0	-1	0	0	0	0

w◯A 对应的表达式为 -(a+x+y)

w◯B 对应的表达式为 1+x+temp

w◯C 对应的表达式为 -z

w◯A * w◯B = w◯C 也就是 -(a+x+y) * (1+x+temp) = -z

这对应着 circom 中的z <== (x + y + a) * (temp + x + 1);

example6

视频中的例子

y = x ** 3 + 2x + 5

circuit code


pragma circom 2.0.0;

template calc () {

   // Declaration of signals.
   signal T2;
   signal T1;
   signal z;

   signal output y;

   signal input x;

   //y = x ** 3 + 2x + 5
   // Constraints.
   T1 <== x * x;
   z <== T1 * x;
   T2 <== z + 2 * x;
   y <== T2 + 5;
}

component main  = calc();

r1cs.json

{
  "n8": 32,
  "prime": "21888242871839275222246405745257275088548364400416034343698204186575808495617",
  "nVars": 4,
  "nOutputs": 1,
  "nPubInputs": 0,
  "nPrvInputs": 1,
  "nLabels": 6,
  "nConstraints": 2,
  "useCustomGates": false,
  "constraints": [
    [
      {
        "2": "21888242871839275222246405745257275088548364400416034343698204186575808495616"
      },
      {
        "2": "1"
      },
      {
        "3": "21888242871839275222246405745257275088548364400416034343698204186575808495616"
      }
    ],
    [
      {
        "3": "21888242871839275222246405745257275088548364400416034343698204186575808495616"
      },
      {
        "2": "1"
      },
      {
        "0": "5",
        "1": "21888242871839275222246405745257275088548364400416034343698204186575808495616",
        "2": "2"
      }
    ]
  ],
  "map": [0, 1, 2, 4],
  "customGates": [],
  "customGatesUses": []
}

witness

优化前的 witness 应该是[1, y, x, T2, T1, z]

从"map": [0, 1, 2, 4] 中间有些 signal 被优化掉了

取一下对应下标，结果是:

[1, y, x, T1]

也可以通过 sym 文件来获得 witness 的下标, 参见https://docs.circom.io/circom-language/formats/sym/

使用–O0 可以禁止优化, 具体的步骤参见https://docs.circom.io/circom-language/formats/constraints-json/

constraints

` “nConstraints”: 2`

一共有两个约束

相应的, 我们也可以看到 json 中的 constraints 数组中有两个元素

circom 里定义了 4 个约束, 因此肯定也有被优化的

constraints 1

witness	1	x	T1
A	0	-1	0
B	3	1	0
C	0	0	-1

w◯A 对应的表达式为 -x

w◯B 对应的表达式为 x

w◯C 对应的表达式为 -T1

w◯A * w◯B = w◯C 也就是 -x * x = -T1

这对应着 circom 中的T1 <== x * x;

constraints 2

witness	1	y	x	T1
A	0	0	0	-1
B	3	0	1	0
C	5	-1	2	0

w◯A 对应的表达式为 -T1

w◯B 对应的表达式为 x

w◯C 对应的表达式为 5 - y + 2x

w◯A * w◯B = w◯C 也就是 -T1 * x = 5 - y + 2x

等式两边移项

y = T1 * x + 2x + 5

对应着 circom 中如下代码优化后的结果

   z <== T1 * x;
   T2 <== z + 2 * x;
   y <== T2 + 5;