1 形式语言
形式语言给出：语句的形式 proof 是什么。
设 sum 是任意集合，sum^* 是所有的长度有限的字符串 <x_1, .., x_n> ，其中 x_j 取自 sum ，空字符串 <> ∈ sum^* 。语言 L 是 sum^* 的子集。在这种情况下，sum 是语言 L 的子母表，sum 中的元素是字母，L 中的元素是单词。如果有规则指定 sum^* 中的字符串是否属于语言，该规则就被称为语法。如果 L_1 和 L_2 是基于同一个字母表的两个形式语言，且包含了相同的单词集，则称 L_1 和 L_2 是等价的。
1.1 Decision functions
在 SNARK 开发中，语言通常被定义为决策问题（decision problems），决策关系（deciding relation）R ⊂ sum^* 决定了字符串 x ∈ sum^∗ 是否是语言中的单词。如果 x ∈ R ，那么 x 是语言 L_R 中的单词，否则不是。关系 R 总结了语言 L_R 的语法，也称为决策函数（decision function）：
可用 R 定义语言：
语句（statement）S 是语言 L 包含单词 x 的声明，即存在一些 x ∈ L 。语句 S 的构造性证明（constructive proof）是给定一些字符串 P ∈ sum^* 并且该证明是通过 R(P) = true 而被验证的（verified）。这种情况下，P 被称为语句 S 的一个实例（instance）。
3-因子分解例子
设 sum := F_{13} ，L_{3.fac} 包含由来自 F_{13} 的 4 个元素组成的字符串 <x_1, x_2, x_3, x_4> ，且满足 x_1 · x_2 · x_3 = x_4 。例如 <2, 12, 4, 5> 是 L_{3.fac} 中的单词，而 <2, 12, 11> 就不是。可通过决策函数来更加形式化地描述 L_{3.fac} ：
字符串 <2, 12, 4, 5> 就是 L_{3.fac} 包含单词的 constructive proof，R_{3.fac}(<2, 12, 4, 5>) = true 是证明的验证。
1.2 Instance and Witness
语句在形式化语言中提供了成员关系声明，而实例则是这些声明的 constructive proof。在零知识证明系统中，可以隐藏 proof instance 的一部分，但仍然能证明语句。因此，在这种情况下，需要将 proof 分为未隐藏的公共部分（称为 instance）和隐藏的私有部分（称为 witness）。
为了将 proof instance 分为 instance 和 witness，前面的形式语言定义需要做些调整。不再使用单个子母表，而是使用两个子母表 sum_I 和 sum_W ，决策函数定义如下：
字符串 (i; w) ∈ {sum}_I^* × {sum}_I^* ，R(i; w) = true 。输入 i 为 instance，输入 w 为 witness。
语言的定义如下：
语句 S 是声明：给定 instance i ∈ {sum}_I^* ，总存在 witness w ∈ {sum}_I^* 使得语言 L 包含单词 (i; w)。语句 S 的一个 constructive proof 是存在字符串 P (i; w) ∈ {sum}_I^* × {sum}_I^* ，且 proof 被 R(P) = true 验证（verified）。
证明系统需要在不暴露 witness 的情况下证明语句。
语句可以被视为知识声明，而证明者声称知道对于给定 instance 的 witness。
3-因子分解例子
x_1, x_2, x_3 是 witness，乘积 x_4 是 instance。L_{3.fac} 重新定义如下：
也可以选择 x_4 为 witness，x_1, x_2, x_3 为 instance，或者都选为 witness，或者都选为 instance，取决于应用。
语言 L_{3.fac_zk} 就是使得决策函数 R_{3.fac_zk} 为 true 的选自 (F_{13}^*) × (F_{13}^*) 的字符串集合。
1.3 模块化
开发者通常需要使用简单的语句来构造复杂的语句。在零知识证明系统中，那些简单的块通常被称为小装置（gadgets），gadgets 库会包含原子类型如 bool、整型和一些哈希函数，椭圆曲线等。为了合成语句，开发者需要将预定义好的 gadgets 合成复杂的逻辑，称这种能力为模块化（modularity）。
2 语句表示
2.1 Rank-1 Quadratic Constraint Systems
尽管决策函数可以用各种方式表达，但是许多现代证明系统要求决策函数使用有限域上的二次方程组来表示。
秩-1 (二次 ) 约束系统（R1CS，Rank-1 (quadratic) Constraint Systems ）是零知识证明系统中的常见标准。
2.1.1 R1CS 表示
设 F 是域，n, m, k ∈ N，a_j^i, b_j^i, c_j^i ∈ F，其中 0 le j le n m 且 1 le i le k ，R1CS 可用如下 k 个等式表示：
k 为约束的个数，每个等式被称为约束。满足所有约束的 <I_1, .., I_n>;<W_1, ..., W_m> 中，<I_1, .., I_n> 为 instance，<W_1, .., W_m> 为 witness。
R1CS 的解就是程序正确执行的 proof。
3-因子分解例子
F_{3.fac_zk} 中包含取自 F_{13} 中的单词 (<I_1>;<W_1,W_2,W_3>) ，且 I_1 = W_1 · W_2 · W_3 。将将其重写为 R1CS 如下：
为了避免 3 个数相乘，引入 W_4
也可以写成：
R1CS 不是唯一的。
选择 n = 1, m = 4, k = 2，得到如下值：
然后可重写为：
2.1.2 R1CS 可满足性
R1CS 定义了形式语言，每个域 F 上的 R1CS 都定义了基于子母表 sum_I × sum_W = F × F 的决策函数：
语句是知识声明：给定 instance I，存在 witness W 使得 (I; W) 是 R1CS 的解。
sum = F ，语言定义如下：
3-因子分解例子
对于 I_1 = 11 ，为了证明语句“存在 witness W 使得 (I_1; W) 属于 L_{3.fac_zk} ”，一个 proof 必须是 R1CS 的解，即提供一组 witness 变量 W_1, W_2, W_3, W_4 的赋值 。一个正确的 constructive proof 是 π =< 2, 3, 4, 6 >
2.2 代数电路
2.2.1 代数电路表示
设 F 是域，一个代数电路 C(F) 是可以在 F 上计算一个多项式的有向无环（多重）图。源点代表函数的变量和常量，终点代表函数的输出。所有的节点都仅有两条入边，代表着域上的加法或乘法运算。边的方向代表沿着节点的计算流。
既不是源点也不是终点的节点称为算术门（arithmetic gates）。被 标记的算术门称为加法门（addition-gates），被 · 标记的称为乘法门（multiplication-gates）。每个算术门都恰好有两个输入，用两条入边表示。
因为边是有序的，所以可以写为 <E_1, E_2, ..., E_n> ，n ∈ N。边的标签可以说常量或符号如 I_j, W_j ，分别表示 instance 变量和 witness 变量。在绘制电路的最初的阶段，在没有确定一条边是 I 还是 W 时，可以先用 S_j 标签。
3-因子分解例子
f_{3.fac}: F_{13} × F_{13} × F_{13} rightarrow F_{13};(x_1, x_2, x_3) rightarrow x_1 · x_2 · x_3 。一个合理的 witness 是 f_{3.fac} 在点 I_1 ∈ F_{13} 处的原像，即 f_{3.fac}(W_1, W_2, W_3) = I_1
要将该函数转为 F_{13} 上的代数电路，要先在函数的定义中引入括号，改写为二元运算：
边的标签为 W_1 = x_1, W_2 = x_2, W_3 = x_3, I_1 = f_{3.fac}(x_1, x_2, x_3) ，得到如下电路：
该图有 3 个叶子节点 x_1, x_2, x_3 ，1 个根节点 f_{3.fac(x_1, x_2, x_3)} 和 2 个中间节点，均为乘法门。
电路不是唯一的，取决于括号的顺序。
2.2.2 电路执行
电路执行：根据输入获得输出。值从一个节点沿着边到达另一个节点，如果节点是门，则值会被转换，重复整个过程直到到达终点。
电路的正确执行中，不仅会获得输出，还会获得边上的值，将获得的边集值 <S_1, S_2, ..S_n> 称为电路的合法赋值（valid assignment），该合法赋值也被称为电路正确执行的证明（proofs for proper circuit execution）
3-因子分解例子
边集为 S := <I_1; W_1, W_2, W_3, W_4> ，一个合法赋值是 S_{valid} := <11; 2, 3, 4, 6>
2.2.3 电路可满足性
为了理解电路是如何产生形式语言，可以看到每个域 F 上的代数电路 C(F) 都定义了一个基于字母表 sum_I × sum_W 的决策函数：
语法是电路的形状，单词是电路正确执行时边的赋值，语句是声称知道“给定 instance I，存在 witness W 使得 (I; W) 是电路的合法赋值”。语句的一个 constructive proof 是为每个 witness 变量分配一个域元素，且该分配通过了电路执行的验证。
在零知识证明系统中，电路的执行通常被称为 witness generation，因为 instance 通常是公开的，所以任务就是计算 witness。
满足电路的语言：
2.2.4 关联约束系统
本节讲述如何将电路转为 R1CS。
C(F) 是有限域 F 上的代数电路，边的标签组成的字符串为 <S_1, S_2, .., S_n> 。从一个空的 R1CS 开始，每条边 S_j 上都执行如下其中一个步骤：
- 如果边 S_j 是乘法门的出边，则 R1CS 得到一个新的约束：(left input) · (right input) = S_j
- 如果边 S_j 是加法门的出边，则 R1CS 得到一个新的约束：(left input right input) · 1 = S_j
- 没有其它边可以为系统添加一个约束。
每个代数电路 C(F) 都可以生成一个 RICS R ，称为该电路的关联 R1CS。
3-因子分解例子
将如下电路转为 R1CS。
为了生成所有约束，需要迭代边标签集 <I_1; W_1, W_2, W_3, W_4> ：
- 从 I_1 开始，是一条乘法门的出边，入边都有标签，所以得到约束：W_4 · W_3 = I_1
- 然后考虑 W_1 ，因为不是乘法门或加法门的出边，所以不会添加约束。W_2 同理。
- 对于 W_4 ，是乘法门的出边，入边都有标签，所以得到约束：W_2 · W_1 = W_4
- 因为没有更多有标签的边了，所以所有的约束都生成了，把它们合在一起，生成了 C_{3.fac}(F_{13}) 的关联 R1CS： W_4 · W_3 = I_1 \ W_2 · W_1 = W_4
2.3 Quadratic Arithmetic Programs
R1CS 可转为 Quadratic Arithmetic Program QAP，QAP 是目前存在的一些最有效的 ZK-SNARK proof 生成器的基础。
2.3.1 QAP 表示
设 F 是域，R 是 F 上的一个 R1CS，F 中的非 0 元素个数大于R 中的约束个数 k 。a_j^i, b_j^i, c_j^i ∈ F 定义 R1CS 的常数，其中 0 ≤ j ≤ n m, space 1 ≤ i ≤ k ，m_1, ..., m_k 是 F 中的任意可逆的不同的元素。R1CS 的一个 Quadratic Arithmetic Program 是 F 上的如下多项式集合：
T(x) := prod_{l=1}^k(x-m_l) 是度为 k 的多项式，称为 QAP 的目标多项式，A_j, B_j, C_j 均是度为 k - 1 的多项式，定义如下：
给定 R1CS，一个关联的 QAP 可通过如下步骤算出：
- 如果 R1CS 包含 k 个约束，则先从 F 中选取 k 个不同的可逆元素，每种选择都会生成不同的 QAP。
- 计算目标多项式 T。
- 对于每个 1 le j le k ，使用如下点集根据 Lagrange 插值法计算多项式 A_j undefinedS_{A_j} = left{(m_1, a_j^1), ..., (m_k, a_j^k) right} 同理，对于每个 1 le j le k 计算 B_j,space C_j
3-因子分解例子
R1CS 如下
R1CS 中的常量 a_j^i, b_j^i, c_j^i 如下
因为 R1CS 定义于 F_{13} 上，有 2 个约束，所以需要从 F_{13} 中选择两个任意可逆的元素 m_1, m_2 ，我们选择 m_1=5, m_2=7 ，得到目标多项式：
然后根据 R1CS 的系数计算多项式 A_j, B_j, C_j 。因为 R1CS 有两个约束等式，所以 A_j, B_j, C_j 的度为 k - 1 = 1，且被点 m_1=5 和 m_2=7 处的等式定义。
在点 m_1 ，每个多项式 A_j 都被定义为 a_j^1 ；在点 m_2 ，每个多项式 A_j 都被定义为 a_j^2 ，B_j, C_j 同理，得到：
使用 S_{A_2} = left{(m_1, a_2^1), (m_2, a_2^2)right} = left{(5, 1), (7, 0)right} 借助 Lagrange 插值法计算 A_2 ：
同理可算出其它多项式。最终得到：
2.3.2 QAP 可满足性
设 R 是 R1CS，相关的变量为 (<I_1, ..., I_n>;<W_1, ..., W_m) ，QAP 为 R 的一个 Quadratic Arithmetic Program，当如下多项式可被目标多项式 T 整除时，(<I_1, ..., I_n>;<W_1, ..., W_m) 是 R1CS 的解：
域 F 上的 QAP 基于字母表 sum_I × sum_W = F × F 定义了一个决策函数：
在 QAP 中，一个合法的 proof 是包含一个可被 T 整除的多项式 P_{(I;W)} 。
给定 instance I ，为了计算 L_{QAP} 中一个语句的 constructive proof，证明者需要计算关联 R1CS 的一个 constructive proof W ，例如运行 R1CS 的电路。有了 (I;W) ，证明者就可以计算多项式 P_(I;W) ，并将该多项式公布为 proof。
3-因子分解例子
给定 I_1 = 11 ，我们知道 (W_1, W_2, W_3, W_4) = (2, 3, 4, 6) 是一个正确的 witness，因为 (<I_1>;<W_1, W_2, W_3, W_4>) = (<11>;<2, 3, 4, 6>) 是电路的一个合法赋值，所以是 R_{3._fac_zk} 的解，是语言 L_{R_{3.fac_zk}} 的 constructive proof。
为了将 constructive proof 转为语言 L_{R_{3.fac_zk}} 的指数证明，证明者需要使用 constructive proof 中的元素计算多项式 P_{(I;W)}
因为 P_{(I;W)} 等于目标多项式 T ，所以可被其整除 P / T = 1 ，所以验证者验证了该 proof 是对的。
3 Circom
编译为 R1CS 的编程语言在密码学和区块链中比较流行，这些语言提供了设计和实现代数电路的更高级抽像。有了这些编程语言，开发者只需要专注于电路逻辑，编译器会负责输出 R1CS 和其它用于有效计算电路赋值的程序。
Circom 是设计代数电路的领域专用语言。它将电路编译为 R1CS，并输出 WebAssembly 和 C 程序。
Circom 中的概念：
- 信号（signal）是底层域 F 的一个元素，是不可更改的，可定义为输入或输出。输入信号是私有的，除非特意声明为公有，而输出信号是公有的。剩余的信号是私有的，且不可被声明为公有。
- 模板（template）是创建通用电路的算法。模板是一个新的电路对象，可被其它电路使用。
- 组件（component）定义了代数电路，有输入信号，输出信号和中间信号，和常量集合。与信号一样，是不可变的。
如下是一个 Circom 程序示例 trivial_circuit.circom：
代码语言：javascript复制template trivial_circuit() {
signal private input in1 ;
signal private input in2 ;
var outc1 = 0 ;
var inc1 = 7 ;
signal output out1 ;
signal output out2 ;
out2 <== in1 ;
outc1 === in2 ;
}
component main = trivial_circuit() ;需注意，Circom 没有明确表示底层域，所以常量 0 和 7 没有直接意义。
使用如下命令进行编译：
代码语言：javascript复制circom trivial_circuit.circom --r1cs --wasm --symCircom 编译器会生成 3 个文件
- trivial_circuit.r1cs 包含 R1CS，是二进制形式
- trivial_circuit.wasm 是 wasm 代码可以根据给定 instance 计算 witness，是 R1CS 的解
- trivial_circuit.sym 是符号文件，用于 debug 或打印 R1CS
3-因子分解的例子（x_4 = x_1 · x_2 · x_3）
代码语言：javascript复制template Multiplier() {
signal input a ;
signal input b ;
signal output c ;
c <== a*b ;
}
template three_fac () {
signal input x1 ;
signal input x2 ;
signal input x3 ;
signal output x4 ;
component mult1 = Multiplier() ;
component mult2 = Multiplier() ;
mult1.a <== x1 ;
mult1.b <== x2 ;
mult2.a <== mult1.c ;
mult2.b <== x3 ;
x4 <== mult2.c ;
}
component main = three_fac() ;编译：
代码语言：javascript复制circom three_fac.circom --r1cs --wasm --sym打印电路状态，包括约束个数：
代码语言：javascript复制snarkjs r1cs info circuit.r1cs
[INFO] snarkJS: Curve: bn-128
[INFO] snarkJS: # of Wires: 6
[INFO] snarkJS: # of Constraints: 2
[INFO] snarkJS: # of Private Inputs: 0
[INFO] snarkJS: # of Public Inputs: 3
[INFO] snarkJS: # of Labels: 11
[INFO] snarkJS: # of Outputs: 1参考
The MoonMath Manual 第 6 章
