Circom 2 语法

Recommend you go through the documentation of the circom for possible look-up later.

从 circom 的编译过程来看,circom 实际上是一个约束语言,它最终编译成多项式约束。相当于人与多项式约束,例如 R1CS 之间的一个桥梁。

  1. circomlib introduction

    circomlib contains a listing of audited, common circuit building blocks. You can find many of the circuits we’re discussing today in this library.

    All signals in the circom are field elements in the prime field of order: r = 21888242871839275222246405745257275088548364400416034343698204186575808495617 This is a 254-bit prime known as the BabyJubJub prime. It’s the curve order for BN254, a pairing-friendly elliptic curve used by Ethereum and (formerly) ZCash. You can read more about BN254 in Jonathan Wang’s excellent document here.

    Compared with general programming language, such as C++, circom as a DSL (Domain-specific language) can ensure constraint which is necessary for zkp, These constraints usually involve restrictions on data types and logical relationships, such as the need to avoid using types such as floating-point numbers, and the need to ensure that the circuit is binary pluggable

    Real-world application of circom: tornado cash, Dark forest, Semaphore

  2. circom 与 snarkjs

    circom 和 circomlib 库都是 JavaScript 语言的前端,他们可以支持多个后端,也就是真正的证明系统 proving system. 这两个库都是连接的 snarkjs proving system using BN254 curve. snarkjs is a JavaScript and Pure Web Assembly implementation of zkSNARK and PLONK schemes. It uses the Groth16 Protocol (3 point only and 3 pairings), PLONK and FFLONK. 支持 Groth16, PLONK.

    popular proving system implementation: Circom(snarkjs), ZoKrates(libsnark, bellman) To combine machine learning with circuit, For python, a not-mature library: PySNARK(snarkjs, libsnark)

    For javascript API about Pytorch, ONNX.js: Universal Deep Learning Models in The Browser | by Will Badr | Towards Data Science

  3. datatype date type in the circom:

    1. Field element value, integer values modulo the prime number p. The size is in the range of [0, p-1], which may be implemented by big int library in javascript.

    2. array with the same type (signal, var, or the same type of components or arrays again).

  4. circom 只接受 加号和乘号,可以接受的形式如下:

    a = b + c, a = b * c, a = b(b-1)+b Any equations with degree two or less can be accepted. The compiler will figure out how to break it down into a sequence of equations that are admitted by a particular constraint system we are working with.

    We can write linear equations and quadratic equations that dont have more one quadratic term.

  5. zkrepl syntax sugar: json comment input

  6. 使用三等号来写约束

  7. circom 约束的操作符只有加法和乘法, 可以写线性方程组或者只有一个二次项的二次方程。 关于 constraint 的限制可以看官方文档 Constraint Generation - Circom 2 Documentation. 官方文档阐述了 circom 的具体语法细节可以在编程时多看看。

  8. <-- 操作符是 derive 中间变量用的,可以用 javascript 的任意运算符,不局限于加法和乘法。

    syntax surgar: <== is equal to constraint <-- and witness assignment ===

    只有 <===== 才会被编译到最后的约束系统里,<-- 操作符是将符号输入 proving machine 之前人工计算的输入,只是这里用代码代替了而已。 一个对比是:<-- 符号计算的结果错误的话,Circom 会显示 circom safe 以及 assert fail mode 提示不满约束, 而约束等式错误整个意足思就变了。

    <-- 和一些其他的计算,是为了方便根据 input 生成 prove 用的,即使没有这些计算,prover 手动算出来放到最后 proving 过程里也可以。 只有需要约束的等式才只能用 乘法和加法。 之前的错误答案里的计算和赋值,只是实现了 “prover 不作恶情况下如何根据 input 计算出正确的值”,并不能防止 “恶意的 prover 用错误值通过 verify”, 因为这些没有进入最后的约束里。

    注意:signal output vari 中的 derived signal vari 时 derived 出来的公开变量,不需要在 zkrepl 的 input 中指定值。 注意:"<==" 的写法只适用于生成的时候也只包含加号和乘号的中间变量,如果生成中间变量的时候需要加和乘之外的操作,那就需要分开写成 <--=== 的样子了。

  9. range check, check 0 <= in =< 15,

    通过将其约束为四个 0/1 比特的表达形式,也就是 num2bit

  10. array

  11. for loop

  12. private and public

    variable private public
    signal signal input signal input and specify in main { public [ b ]}
    derived signal signal signal output
    1. signal x x is a intermediate value auto-generated by circom2 at proving time, default private
    2. component main { public [ b ]} = Num2Bits(4); b 是 public input signals for verifier, b can be an array, where the form of input in zkrepl should be "b": ["1", "2", "3","3"].
    3. signal output b[nBits]; output keyword is used to specify the derived signal that is made public while it's defined, which is an output of some computation that you want to reveal to the verifier.

    if you have defined the variable as signal output, it becomes a public output signal, and there is no need to add it in the component main { public [ b ]} = Num2Bits(4);. The public in the main is accompanied by the signal input`.

    the private and public keywords are the circom language features. zkSNARK machinery cannot tell which is public or private.

    from the programmer's point of view, only public input and output signals are visible from outside the circuit, and hence no intermediate signal can be accessed.

  13. witness refers to the set of all signals that are passed into the prover.

  14. varsignal 的区别

    1. var is mutable for convenience, however, signal is immutable.

    2. circom 中 var is intermediate variables, signal input variables are given by the user. Thus, only the input variables are at the risk of being forged when the constraints are not done well. ref:【session 2】在了解了约束后,对于 Num2Bits 电路突然产生了疑惑 · Antalpha-Labs/zkp-co-learn · Discussion #43

    3. The var variable hold either numerical values of the field or arithmetic expressions when they are used to build constraints (see Constraint Generation). They can be named using a variable identifier or can be stored in arrays.

      When the var variable is assigned as an arithmetic expression, it can be seen as a placeholder for you to write the circuit conveniently. In the end, the var variable will be replaced or expanded in the arithmetic expression, which should meet the requirement in Constraint Generation.

      ref: var 和 signal 之间的差异? · Antalpha-Labs/zkp-co-learn · Discussion #45 Variables & Mutability - Circom 2 Documentation

  15. TODO: Why there are IsEqual and IsZero function exist? the three equal === funciton can check the equality.

ZK-resources-for-ML-specialists

Modern ZK Crypto - Session 2 Lecture Notes - HackMD

References

  1. Modern ZK Crypto - Session 2 Lecture Notes - HackMD