zcash.github.io/halo2

译自 halo2 book：README.md

halo2

用法(Usage)

本仓库包含 halo2_proofs 和 halo2_gadgets 两个 crate，应直接使用它们。

最低支持的 Rust 版本(Minimum Supported Rust Version)

需要 Rust 1.60 或更高版本。

最低支持的 Rust 版本将来可能变更，但变更时会伴随一次次版本号(minor version)的提升。

控制并行(Controlling parallelism)

halo2 目前使用 rayon 进行并行计算。可以通过 RAYON_NUM_THREADS 环境变量来设置线程数。

你可以通过禁用 "multicore" 特性(feature)来禁用 rayon。 警告！如果禁用 "multicore" 特性，Halo2 将无法使用并行能力。 这会显著降低性能。

许可证(License)

按以下任一许可证授权

• Apache License, Version 2.0, (LICENSE-APACHE 或 http://www.apache.org/licenses/LICENSE-2.0)
• MIT license (LICENSE-MIT 或 http://opensource.org/licenses/MIT)

由你自行选择。

贡献(Contribution)

除非你明确另行声明，否则你有意提交以纳入本作品的任何贡献（按 Apache-2.0 许可证中的定义），都将如上所述进行双重许可，且不附加任何额外条款或条件。

译自 halo2 book：concepts.md

概念

我们首先介绍零知识证明系统(zero-knowledge proof system)背后的概念；Halo 2 所使用的算术化(arithmetization)（一种电路描述方式）；以及我们用来构建电路实现的各种抽象。

译自 halo2 book：concepts/proofs.md

证明系统

任何证明系统(proof system)的目标都是能够证明有意思的数学或密码学陈述(statement)。

通常，在一个给定的协议中，我们会想要证明一族陈述，这些陈述的区别在于它们的公开输入(public inputs)。证明者(prover)还需要表明他们知道某些使该陈述成立的私有输入(private inputs)。

为此，我们写下一个关系(relation) $\mathcal{R}$，它指定了公开输入与私有输入的哪些组合是有效的。

上述术语意在与 ZKProof Community Reference 保持一致。

准确地说，我们应当区分关系 $\mathcal{R}$ 与它在证明系统中所用的实现。我们称后者为电路(circuit)。

我们用来为特定证明系统表达电路的语言被称为算术化(arithmetization)。通常，一种算术化会以某个域(field)上变量的多项式约束(polynomial constraints)的形式来定义电路。

将某个特定关系表达为电路的这一_过程_有时也被称为“算术化”，但我们会避免这种用法。

为了创建对某个陈述的证明，证明者需要知道私有输入，以及电路所使用的中间值，这些中间值被称为***建议(advice)***值。

我们假设可以根据私有输入和公开输入高效地计算出建议值。具体的建议值取决于我们如何编写电路，而不仅仅取决于高层的陈述。

私有输入与建议值合起来被称为见证(witness)。

有些作者把“见证”仅仅当作私有输入的同义词。但在我们的用法中，见证包含建议值，即它包含证明者提供给电路的所有值。

例如，假设我们想要证明知道一个哈希函数 $H$ 对于摘要 $y$ 的某个原像(preimage) $x$：

• 私有输入是原像 $x$。

• 公开输入是摘要 $y$。

• 关系是 $\{(x,y):H(x)=y\}$。

• 对于某个特定的公开输入 $Y$，陈述是：$\{(x):H(x)=Y\}$。

• 建议值是实现该哈希函数的电路中的所有中间值。见证则是 $x$ 加上建议值。

非交互式论证(Non-interactive Argument)允许证明者(prover)为给定的陈述和见证创建一个证明(proof)。证明是一些数据，可用来使验证者(verifier)相信：_存在_一个见证使该陈述成立。使这类证明无法虚假地说服验证者的那条安全性质称为可靠性(soundness)。

非交互式知识论证(Non-interactive Argument of Knowledge)（NARK）进一步使验证者相信证明者_知道_一个使该陈述成立的见证。这条安全性质称为知识可靠性(knowledge soundness)，它蕴含可靠性。

在实践中，知识可靠性对密码学协议比可靠性更有用：例如，若我们关心 Alice 在某个协议中是否持有一个密钥，我们需要 Alice 证明_她知道_这个密钥，而不仅仅是它存在。

知识可靠性的形式化表述是：必须存在一个能够精确观察证明是如何生成的提取器(extractor)，它能够计算出见证。

鉴于证明可能是可塑的(malleable)，这条性质相当微妙。也就是说，依赖于具体的证明系统，可能可以在不知道见证的情况下，取一个已有的证明（或一组证明）并对其进行修改，从而产生一个针对相同或相关陈述的不同证明。使用可塑证明系统的更高层协议需要把这一点考虑进去。

即便没有可塑性，证明也可能被重放(replayed)。例如，在我们的例子中，我们不希望 Alice 能够出示由别人生成的证明，并使其被当作她知道该密钥的凭证。

如果一个证明除了表明见证存在且为证明者所知之外，不泄露关于见证的任何信息，那么我们就说该证明系统是***零知识(zero knowledge)***的。

如果一个证明系统产生简短的证明——即长度关于电路规模是多对数(polylogarithmic)的——那么我们就说它是简洁(succinct)的。简洁的 NARK 被称为SNARK（简洁非交互式知识论证(Succinct Non-Interactive Argument of Knowledge)）。

按照这个定义，SNARK 不一定要求验证时间关于电路规模是多对数的。有些论文用***高效(efficient)***一词来描述具有该性质的 SNARK，但我们会避免使用这个词，因为对于支持摊销式或递归式验证的 SNARK（后面会谈到），它含义不清。

zk-SNARK 是一种零知识的 SNARK。

译自 halo2 book：concepts/arithmetization.md

PLONKish 算术化

Halo 2 所使用的算术化(arithmetization)来自 PLONK，更确切地说是它的扩展 UltraPLONK，后者支持自定义门(custom gates)和查找论证(lookup arguments)。我们称之为 PLONKish。

PLONKish 电路是以一个值的矩形矩阵来定义的。我们用通常的含义来指代该矩阵的行(rows)、列(columns)和单元格(cells)。

一个 PLONKish 电路依赖于一个配置(configuration)：

• 一个有限域(finite field) $\mathbb{F}$，其中单元格的值（对于给定的陈述和见证）将是 $\mathbb{F}$ 中的元素。

• 矩阵中列的数量，以及对每一列的规约——它是固定(fixed)、***建议(advice)还是实例(instance)***列。固定列由电路固定；建议列对应见证值；实例列通常用于公开输入（从技术上讲，它们可用于证明者与验证者之间共享的任何元素）。

• 可以参与相等约束(equality constraints)的列的一个子集。

• 一个最大约束次数(maximum constraint degree)。

• 一系列多项式约束(polynomial constraints)。这些是 $\mathbb{F}$ 上的多元多项式(multivariate polynomials)，它们对每一行都必须求值为零。多项式约束中的变量可以指代当前行某给定列中的一个单元格，或相对于当前行的另一行某给定列中的单元格（带回绕(wrap-around)，即对 $n$ 取模）。每个多项式的最大次数由最大约束次数给出。

• 一系列查找论证(lookup arguments)，它们定义在输入表达式(input expressions)（如上所述的多元多项式）和***表列(table columns)***的元组之上。

一个 PLONKish 电路还定义：

• 矩阵中的行数 $n$。$n$ 必须对应于 ${\mathbb{F}}^{\times }$ 的某个乘法子群(multiplicative subgroup)的大小；通常是 2 的幂。

• 一系列相等约束(equality constraints)，它们指定两个给定的单元格必须具有相等的值。

• 各行处固定列的值。

根据一个电路描述，我们可以生成一个证明密钥(proving key)和一个验证密钥(verification key)，它们是对该电路进行证明和验证操作所需要的。

注意，我们指定了列、多项式约束、查找论证和相等约束的顺序，尽管这些顺序并不影响电路的含义。这样做使得我们更容易将证明密钥和验证密钥的生成定义为一个确定性的过程。

通常，一个配置会定义一些多项式约束，这些约束由定义在固定列中的选择子(selectors)来开启和关闭。例如，约束 $q_i\cdot p(...)=0$ 可以通过令 $q_i=0$ 来对某个特定的行 $i$ 关闭。在这种情况下，我们有时会把一组由若干选择子列控制、被设计为一起使用的约束称为一个门(gate)。通常会有一个标准门(standard gate)，它支持诸如域乘法和域除法之类的通用操作，可能还会有支持更专门化操作的自定义门(custom gates)。

译自 halo2 book：concepts/chips.md

芯片

上一节给出了对电路相当底层的描述。在实现电路时，我们通常会使用一个更高层的 API，它旨在追求可审计性(auditability)、效率(efficiency)、模块化(modularity)和表达力(expressiveness)等理想特性。

这个 API 中使用的一些术语和概念取自与集成电路设计和布局的类比。正如对集成电路而言，通过组合那些为特定功能提供高效预制实现的芯片(chips)，上述理想特性更容易获得。

例如，我们可能会有实现特定密码学原语的芯片，比如哈希函数或密码(cipher)，或者诸如标量乘法(scalar multiplication)或配对(pairings)之类的算法。

在 PLONKish 电路中，仅凭做域乘法和域加法的标准门(standard gates)就可以搭建出任意的逻辑。然而，使用自定义门(custom gates)可以获得非常显著的效率提升。

利用我们的 API，我们定义那些“知道”如何使用特定自定义门集合的芯片。这创建了一个抽象层，将高层电路的实现与直接使用自定义门的复杂性隔离开来。

即便我们有时需要“身兼两职”，既实现一个高层电路，又实现它所使用的芯片，其用意在于：这种分离会带来更易于理解、审计、维护/复用的代码。部分原因在于，某些潜在的实现错误会由于这种构造方式而被排除掉。

PLONKish 电路中的门通过相对引用(relative references)来指代单元格，即指代某给定列、相对于门的选择子被设置的那一行处于某给定偏移的行中的单元格。当偏移非零时，我们称之为偏移引用(offset reference)（即偏移引用是相对引用的一个子集）。

相对引用与相等约束中使用的***绝对引用(absolute references)***形成对比，绝对引用可以指向任意单元格。

引入偏移引用的动机是减少配置中所需列的数量，从而减小证明大小。如果我们没有偏移引用，那么我们就需要一列来保存自定义门所引用的每一个值，并且需要使用相等约束把电路中其他单元格的值复制到该列中。有了偏移引用，我们不仅需要更少的列；而且也不需要对所有这些列都支持相等约束，这提升了效率。

在 R1CS（另一种算术化，某些读者可能更熟悉它，不熟悉也没关系）中，一个电路由一片“门之海(sea of gates)”构成，它们没有语义上有意义的顺序。而由于偏移引用，PLONKish 电路中行的顺序是有意义的。我们将做一些简化假设并定义一些抽象，以驯服由此产生的复杂性：目标是，在小工具层级(gadget level)——即我们进行大部分电路构造的地方——我们将不必显式地处理相对引用或门的布局。

我们会把一个电路划分为若干区域(regions)，每个区域包含一个互不相交的单元格子集，并且相对引用永远只指向某个区域内部。芯片实现的部分职责就是确保进行偏移引用的门被布局在某个区域内的正确位置上。

给定各区域及其***形状(shapes)的集合，我们将使用一个独立的布局规划器(floor planner)***来决定每个区域被放置在何处（即放在哪一行作为起始行）。有一个默认的布局规划器，它实现了一个非常通用的算法，但如果需要，你也可以编写自己的布局规划器。

布局规划一般会在矩阵中留下空隙，因为某给定行中的门并没有用到所有可用的列。这些空隙会——尽可能地——由那些不需要偏移引用的门来填补，这些门可以被放置在任意行上。

芯片也可以定义查找表(lookup tables)。如果对同一个查找论证定义了不止一个表，我们可以使用一个***标签列(tag column)***来指定每一行使用哪个表。也可以在若干个表的并集中执行查找（受多项式次数上界的限制）。

组合芯片

为了组合来自若干芯片的功能，我们把它们组合成一棵树。顶层芯片定义一组固定列、建议列和实例列，然后指定这些列应如何在更底层的芯片之间分配。

在最简单的情形下，每个更底层的芯片将使用与其他芯片互不相交的列。然而，也允许在芯片之间共享某一列。尤其重要的是要优化建议列的数量，因为它会影响证明大小。

其结果（可能在优化之后）是一个 PLONKish 配置。我们的电路实现将以一个芯片作为参数，并且可以通过顶层芯片使用所支持的更底层芯片的任何特性。

我们的期望是，不那么专业的用户通常能够找到一个已有的、支持其所需操作的芯片，或者只需对已有芯片做些微小修改。专家用户则将拥有完全的控制权，去做那种 ECC 公司以之闻名 的电路优化 🙂。

译自 halo2 book：concepts/gadgets.md

小工具

在实现一个电路时，我们本可以直接使用我们所选芯片(chips)的特性。不过，通常我们会通过***小工具(gadgets)***来使用它们。这种间接层是有用的，因为出于效率原因以及 PLONKish 电路所施加的限制，芯片接口往往会依赖于底层的实现细节。小工具接口可以提供一个更便利、更稳定的 API，把那些无关紧要的细节抽象掉。

例如，考虑一个像 SHA-256 这样的哈希函数。一个支持 SHA-256 的芯片的接口可能依赖于该哈希函数设计的内部细节，比如消息调度(message schedule)与压缩函数(compression function)之间的划分。相应的小工具接口可以提供一个更便利、更熟悉的 update/finalize API，并且还可以处理哈希函数中不需要芯片支持的部分，比如填充(padding)。这类似于 CPU 上密码学原语的加速指令通常是通过软件库来访问，而不是直接访问。

小工具还可以为更高层级的电路编程提供模块化、可复用的抽象，类似于它们在 libsnark 和 bellman 等库中的用法。除了抽象函数之外，它们还可以抽象类型，比如椭圆曲线点(elliptic curve points)或特定大小的整数。

译自 halo2 book：user.md

用户文档

你来这里大概是想写电路(circuit)吧？太好了！

本节将引导你完成用 halo2 创建电路的整个流程。

译自 halo2 book：user/dev-tools.md

开发者工具

halo2 crate 包含若干实用工具，帮助你设计和实现电路(circuit)。

模拟证明器(Mock prover)

halo2_proofs::dev::MockProver 是一个用于调试电路的工具，也可以在单元测试中以很低的成本验证电路的正确性。电路的私有输入和公开输入按照通常生成证明(proof)的方式构造，但 MockProver::run 不会真的生成证明，而是创建一个对象来直接测试电路中的每一条约束(constraint)。它会返回细粒度的错误消息，指出具体是哪一条约束（如果有的话）未被满足。

电路可视化

dev-graph 特性标志(feature flag)暴露了若干辅助方法，用于创建电路的图形化表示。

在 Debian 系统上，你需要安装以下额外的软件包：

sudo apt install cmake libexpat1-dev libfreetype6-dev libcairo2-dev

电路布局(Circuit layout)

halo2_proofs::dev::CircuitLayout 将电路布局渲染为一张网格：

fn main() {
    // Prepare the circuit you want to render.
    // You don't need to include any witness variables.
    let a = Fp::random(OsRng);
    let instance = Fp::ONE + Fp::ONE;
    let lookup_table = vec![instance, a, a, Fp::zero()];
    let circuit: MyCircuit<Fp> = MyCircuit {
        a: Value::unknown(),
        lookup_table,
    };

    // Create the area you want to draw on.
    // Use SVGBackend if you want to render to .svg instead.
    use plotters::prelude::*;
    let root = BitMapBackend::new("layout.png", (1024, 768)).into_drawing_area();
    root.fill(&WHITE).unwrap();
    let root = root
        .titled("Example Circuit Layout", ("sans-serif", 60))
        .unwrap();

    halo2_proofs::dev::CircuitLayout::default()
        // You can optionally render only a section of the circuit.
        .view_width(0..2)
        .view_height(0..16)
        // You can hide labels, which can be useful with smaller areas.
        .show_labels(false)
        // Render the circuit onto your area!
        // The first argument is the size parameter for the circuit.
        .render(5, &circuit, &root)
        .unwrap();
}

• 列(column)从左到右依次排布为 instance、advice 和 fixed。除此之外，列的顺序没有特定含义。
  • Instance 列采用白色背景。
  • Advice 列采用红色背景。
  • Fixed 列采用蓝色背景。
• 区域(region)显示为带标签的绿色方框（叠加在背景色之上）。如果某个区域的部分列恰好不相邻，它可能会显示为多个方框。
• 被电路赋值过的单元格(cell)会被涂成灰色。如果某些单元格被赋值了不止一次（这通常是个错误），它们会被涂得比周围的单元格更深。

电路结构

halo2_proofs::dev::circuit_dot_graph 会构建一个表示给定电路的 DOT 图字符串，然后可以用各种布局程序来渲染它。该图是根据电路内部以及它所使用的小工具(gadget)和芯片(chip)内部对 Layouter::namespace 的调用构建的。

fn main() {
    // Prepare the circuit you want to render.
    // You don't need to include any witness variables.
    let a = Fp::rand();
    let instance = Fp::one() + Fp::one();
    let lookup_table = vec![instance, a, a, Fp::zero()];
    let circuit: MyCircuit<Fp> = MyCircuit {
        a: None,
        lookup_table,
    };

    // Generate the DOT graph string.
    let dot_string = halo2_proofs::dev::circuit_dot_graph(&circuit);

    // Now you can either handle it in Rust, or just
    // print it out to use with command-line tools.
    print!("{}", dot_string);
}

成本估算器(Cost estimator)

cost-model 二进制程序接收电路设计的高层参数，并估算验证成本以及最终的证明大小。

Usage: cargo run --example cost-model -- [OPTIONS] k

Positional arguments:
  k                       2^K bound on the number of rows.

Optional arguments:
  -h, --help              Print this message.
  -a, --advice R[,R..]    An advice column with the given rotations. May be repeated.
  -i, --instance R[,R..]  An instance column with the given rotations. May be repeated.
  -f, --fixed R[,R..]     A fixed column with the given rotations. May be repeated.
  -g, --gate-degree D     Maximum degree of the custom gates.
  -l, --lookup N,I,T      A lookup over N columns with max input degree I and max table degree T. May be repeated.
  -p, --permutation N     A permutation over N columns. May be repeated.

例如，要估算一个具有三个 advice 列和一个 fixed 列（带各种旋转(rotation)）、且自定义门(custom gate)最大次数(degree)为 4 的电路的成本：

> cargo run --example cost-model -- -a 0,1 -a 0 -a-0,-1,1 -f 0 -g 4 11
    Finished dev [unoptimized + debuginfo] target(s) in 0.03s
     Running `target/debug/examples/cost-model -a 0,1 -a 0 -a 0,-1,1 -f 0 -g 4 11`
Circuit {
    k: 11,
    max_deg: 4,
    advice_columns: 3,
    lookups: 0,
    permutations: [],
    column_queries: 7,
    point_sets: 3,
    estimator: Estimator,
}
Proof size: 1440 bytes
Verification: at least 81.689ms

译自 halo2 book：user/simple-example.md

一个简单的示例

让我们从一个简单的电路(circuit)开始，向你介绍常用的 API 及其使用方式。这个电路将接收一个公开输入 $c$，并证明它知道两个满足如下关系的私有输入 $a$ 和 $b$

$$a^2\cdot b^2\cdot \mathrm{constant}=c,$$

其中 $\mathrm{constant}$ 是一个固定的数（域元素），例如 $\mathrm{constant}=7.$

定义指令(instructions)

首先，我们需要定义电路所依赖的指令(instruction)。指令是高层小工具(gadget)与底层电路操作之间的边界。指令可以是粗粒度的，也可以是细粒度的，但在实践中你需要在两者之间取得平衡：指令要足够大，以便能有效地优化其实现；同时又要足够小，以便有意义地被复用。

对于我们的电路，我们将使用三个指令：

• 将一个私有数值加载到电路中。
• 将两个数相乘。
• 将一个数作为公开输入暴露给电路。

我们还需要一个类型来表示一个数的变量。指令接口为它们的输入和输出提供了关联类型(associated type)，使得各种实现可以以最符合其优化目标的方式来表示这些类型。

trait NumericInstructions<F: Field>: Chip<F> {
    /// Variable representing a number.
    type Num;

    /// Loads a number into the circuit as a private input.
    fn load_private(&self, layouter: impl Layouter<F>, a: Value<F>) -> Result<Self::Num, Error>;

    /// Loads a number into the circuit as a fixed constant.
    fn load_constant(&self, layouter: impl Layouter<F>, constant: F) -> Result<Self::Num, Error>;

    /// Returns `c = a * b`.
    fn mul(
        &self,
        layouter: impl Layouter<F>,
        a: Self::Num,
        b: Self::Num,
    ) -> Result<Self::Num, Error>;

    /// Exposes a number as a public input to the circuit.
    fn expose_public(
        &self,
        layouter: impl Layouter<F>,
        num: Self::Num,
        row: usize,
    ) -> Result<(), Error>;
}

定义芯片(chip)实现

对于我们的电路，我们将构建一个芯片(chip)，为有限域提供上述数值指令。

/// The chip that will implement our instructions! Chips store their own
/// config, as well as type markers if necessary.
struct FieldChip<F: Field> {
    config: FieldConfig,
    _marker: PhantomData<F>,
}

每个芯片都需要实现 Chip trait。它定义了芯片的属性，布局器(Layouter)在综合(synthesize)电路时可以依赖这些属性，同时也使得芯片所需的任何初始状态能够被加载到电路中。

impl<F: Field> Chip<F> for FieldChip<F> {
    type Config = FieldConfig;
    type Loaded = ();

    fn config(&self) -> &Self::Config {
        &self.config
    }

    fn loaded(&self) -> &Self::Loaded {
        &()
    }
}

配置芯片

芯片需要配置好列(column)、置换(permutation)和门(gate)，这些是实现所有所需指令所必需的。

/// Chip state is stored in a config struct. This is generated by the chip
/// during configuration, and then stored inside the chip.
#[derive(Clone, Debug)]
struct FieldConfig {
    /// For this chip, we will use two advice columns to implement our instructions.
    /// These are also the columns through which we communicate with other parts of
    /// the circuit.
    advice: [Column<Advice>; 2],

    /// This is the public input (instance) column.
    instance: Column<Instance>,

    // We need a selector to enable the multiplication gate, so that we aren't placing
    // any constraints on cells where `NumericInstructions::mul` is not being used.
    // This is important when building larger circuits, where columns are used by
    // multiple sets of instructions.
    s_mul: Selector,
}

impl<F: Field> FieldChip<F> {
    fn construct(config: <Self as Chip<F>>::Config) -> Self {
        Self {
            config,
            _marker: PhantomData,
        }
    }

    fn configure(
        meta: &mut ConstraintSystem<F>,
        advice: [Column<Advice>; 2],
        instance: Column<Instance>,
        constant: Column<Fixed>,
    ) -> <Self as Chip<F>>::Config {
        meta.enable_equality(instance);
        meta.enable_constant(constant);
        for column in &advice {
            meta.enable_equality(*column);
        }
        let s_mul = meta.selector();

        // Define our multiplication gate!
        meta.create_gate("mul", |meta| {
            // To implement multiplication, we need three advice cells and a selector
            // cell. We arrange them like so:
            //
            // | a0  | a1  | s_mul |
            // |-----|-----|-------|
            // | lhs | rhs | s_mul |
            // | out |     |       |
            //
            // Gates may refer to any relative offsets we want, but each distinct
            // offset adds a cost to the proof. The most common offsets are 0 (the
            // current row), 1 (the next row), and -1 (the previous row), for which
            // `Rotation` has specific constructors.
            let lhs = meta.query_advice(advice[0], Rotation::cur());
            let rhs = meta.query_advice(advice[1], Rotation::cur());
            let out = meta.query_advice(advice[0], Rotation::next());
            let s_mul = meta.query_selector(s_mul);

            // Finally, we return the polynomial expressions that constrain this gate.
            // For our multiplication gate, we only need a single polynomial constraint.
            //
            // The polynomial expressions returned from `create_gate` will be
            // constrained by the proving system to equal zero. Our expression
            // has the following properties:
            // - When s_mul = 0, any value is allowed in lhs, rhs, and out.
            // - When s_mul != 0, this constrains lhs * rhs = out.
            vec![s_mul * (lhs * rhs - out)]
        });

        FieldConfig {
            advice,
            instance,
            s_mul,
        }
    }
}

实现芯片 trait

/// A variable representing a number.
#[derive(Clone)]
struct Number<F: Field>(AssignedCell<F, F>);

impl<F: Field> NumericInstructions<F> for FieldChip<F> {
    type Num = Number<F>;

    fn load_private(
        &self,
        mut layouter: impl Layouter<F>,
        value: Value<F>,
    ) -> Result<Self::Num, Error> {
        let config = self.config();

        layouter.assign_region(
            || "load private",
            |mut region| {
                region
                    .assign_advice(|| "private input", config.advice[0], 0, || value)
                    .map(Number)
            },
        )
    }

    fn load_constant(
        &self,
        mut layouter: impl Layouter<F>,
        constant: F,
    ) -> Result<Self::Num, Error> {
        let config = self.config();

        layouter.assign_region(
            || "load constant",
            |mut region| {
                region
                    .assign_advice_from_constant(|| "constant value", config.advice[0], 0, constant)
                    .map(Number)
            },
        )
    }

    fn mul(
        &self,
        mut layouter: impl Layouter<F>,
        a: Self::Num,
        b: Self::Num,
    ) -> Result<Self::Num, Error> {
        let config = self.config();

        layouter.assign_region(
            || "mul",
            |mut region: Region<'_, F>| {
                // We only want to use a single multiplication gate in this region,
                // so we enable it at region offset 0; this means it will constrain
                // cells at offsets 0 and 1.
                config.s_mul.enable(&mut region, 0)?;

                // The inputs we've been given could be located anywhere in the circuit,
                // but we can only rely on relative offsets inside this region. So we
                // assign new cells inside the region and constrain them to have the
                // same values as the inputs.
                a.0.copy_advice(|| "lhs", &mut region, config.advice[0], 0)?;
                b.0.copy_advice(|| "rhs", &mut region, config.advice[1], 0)?;

                // Now we can assign the multiplication result, which is to be assigned
                // into the output position.
                let value = a.0.value().copied() * b.0.value();

                // Finally, we do the assignment to the output, returning a
                // variable to be used in another part of the circuit.
                region
                    .assign_advice(|| "lhs * rhs", config.advice[0], 1, || value)
                    .map(Number)
            },
        )
    }

    fn expose_public(
        &self,
        mut layouter: impl Layouter<F>,
        num: Self::Num,
        row: usize,
    ) -> Result<(), Error> {
        let config = self.config();

        layouter.constrain_instance(num.0.cell(), config.instance, row)
    }
}

构建电路

现在我们已经有了所需的指令，以及一个实现了这些指令的芯片，终于可以构建我们的电路了！

/// The full circuit implementation.
///
/// In this struct we store the private input variables. We use `Option<F>` because
/// they won't have any value during key generation. During proving, if any of these
/// were `None` we would get an error.
#[derive(Default)]
struct MyCircuit<F: Field> {
    constant: F,
    a: Value<F>,
    b: Value<F>,
}

impl<F: Field> Circuit<F> for MyCircuit<F> {
    // Since we are using a single chip for everything, we can just reuse its config.
    type Config = FieldConfig;
    type FloorPlanner = SimpleFloorPlanner;

    fn without_witnesses(&self) -> Self {
        Self::default()
    }

    fn configure(meta: &mut ConstraintSystem<F>) -> Self::Config {
        // We create the two advice columns that FieldChip uses for I/O.
        let advice = [meta.advice_column(), meta.advice_column()];

        // We also need an instance column to store public inputs.
        let instance = meta.instance_column();

        // Create a fixed column to load constants.
        let constant = meta.fixed_column();

        FieldChip::configure(meta, advice, instance, constant)
    }

    fn synthesize(
        &self,
        config: Self::Config,
        mut layouter: impl Layouter<F>,
    ) -> Result<(), Error> {
        let field_chip = FieldChip::<F>::construct(config);

        // Load our private values into the circuit.
        let a = field_chip.load_private(layouter.namespace(|| "load a"), self.a)?;
        let b = field_chip.load_private(layouter.namespace(|| "load b"), self.b)?;

        // Load the constant factor into the circuit.
        let constant =
            field_chip.load_constant(layouter.namespace(|| "load constant"), self.constant)?;

        // We only have access to plain multiplication.
        // We could implement our circuit as:
        //     asq  = a*a
        //     bsq  = b*b
        //     absq = asq*bsq
        //     c    = constant*asq*bsq
        //
        // but it's more efficient to implement it as:
        //     ab   = a*b
        //     absq = ab^2
        //     c    = constant*absq
        let ab = field_chip.mul(layouter.namespace(|| "a * b"), a, b)?;
        let absq = field_chip.mul(layouter.namespace(|| "ab * ab"), ab.clone(), ab)?;
        let c = field_chip.mul(layouter.namespace(|| "constant * absq"), constant, absq)?;

        // Expose the result as a public input to the circuit.
        field_chip.expose_public(layouter.namespace(|| "expose c"), c, 0)
    }
}

测试电路

halo2_proofs::dev::MockProver 可用于测试电路是否正确工作。电路的私有输入和公开输入按照我们生成证明时的方式构造，但通过把它们传给 MockProver::run，我们会得到一个对象，它可以测试电路中的每一条约束(constraint)，并准确告诉我们哪里出了问题（如果有的话）。

    // The number of rows in our circuit cannot exceed 2^k. Since our example
    // circuit is very small, we can pick a very small value here.
    let k = 4;

    // Prepare the private and public inputs to the circuit!
    let constant = Fp::from(7);
    let a = Fp::from(2);
    let b = Fp::from(3);
    let c = constant * a.square() * b.square();

    // Instantiate the circuit with the private inputs.
    let circuit = MyCircuit {
        constant,
        a: Value::known(a),
        b: Value::known(b),
    };

    // Arrange the public input. We expose the multiplication result in row 0
    // of the instance column, so we position it there in our public inputs.
    let mut public_inputs = vec![c];

    // Given the correct public input, our circuit will verify.
    let prover = MockProver::run(k, &circuit, vec![public_inputs.clone()]).unwrap();
    assert_eq!(prover.verify(), Ok(()));

    // If we try some other public input, the proof will fail!
    public_inputs[0] += Fp::one();
    let prover = MockProver::run(k, &circuit, vec![public_inputs]).unwrap();
    assert!(prover.verify().is_err());

完整示例

你可以在这里找到本示例的源代码。

译自 halo2 book：user/lookup-tables.md

查表(lookup tables)

在普通程序中，你可以通过预计算并存储某部分计算的查表(lookup table)，用内存换取 CPU 来提升性能。在 halo2 电路(circuit)中我们也可以做同样的事情！

可以把查表理解为在变量之间强制实施一种关系(relation)，这种关系以表的形式表达。假设我们的约束系统(constraint system)中只有一个查表论证(lookup argument)，那么表的总大小受电路大小的限制：每一个表项占用一行，而每一次查表(lookup)也要占用一行。

TODO

译自 halo2 book：user/gadgets.md

小工具(Gadgets)

译自 halo2 book：user/tips-and-tricks.md

技巧与窍门

本节包含各种你在编写 halo2 电路(circuit)时可能会觉得有用的想法和代码片段。

小范围约束

R1CS 电路中常用的一种约束是布尔约束(boolean constraint)：$b\ast (1-b)=0$。这个约束只能被 $b=0$ 或 $b=1$ 满足。

在 halo2 电路中，你可以用类似的方式约束某个单元格(cell)取一小组值中的某一个。例如，要把 $a$ 约束到范围 $[\mathrm{0..5}]$，你可以创建如下形式的门(gate)：

$$a\cdot (1-a)\cdot (2-a)\cdot (3-a)\cdot (4-a)=0$$

而要把 $c$ 约束为 7 或 13，你可以使用：

$$(7-c)\cdot (13-c)=0$$

这里的底层原理是：我们构造一个多项式约束(polynomial constraint)，让它在我们想要允许的那组可能取值中的每一个值处都有一个根。在 R1CS 电路中，所支持的多项式最大次数(degree)为 2（因为所有约束都是 $a\ast b=c$ 的形式）。在 halo2 电路中，你可以使用任意次数的多项式——但前提是，次数越高的约束使用起来成本越高。

注意，这些根不必是常数；例如 $(a-x)\cdot (a-y)\cdot (a-z)=0$ 会把 $a$ 约束为等于 $\{x,y,z\}$ 中的某一个，其中后者可以是任意多项式，只要整个表达式保持在最大次数界限之内即可。

小集合插值

我们可以使用拉格朗日插值(Lagrange interpolation)构造一个多项式约束，对于小集合 $X\in \{x_i\},Y\in \{y_i\}$ 实现映射 $f(X)=Y$。

例如，假设我们想把一个 2 比特的值映射到一个与零交错排列的"展开(spread)"版本。我们首先预计算每个点处的取值：

$$\begin{array}{rcl}00\to 0000& ⟹& 0\to 0\\ 01\to 0001& ⟹& 1\to 1\\ 10\to 0100& ⟹& 2\to 4\\ 11\to 0101& ⟹& 3\to 5\end{array}$$

然后，我们使用如下恒等式为每个点构造拉格朗日基多项式(Lagrange basis polynomial)： $$l_j(X)=\prod _{0\le m<k,m\ne j}\frac{x-x_m}{x_j-x_m},$$ 其中 $k$ 是数据点的个数。（在上面的例子中 $k=4$。）

回顾一下，拉格朗日基多项式 $l_j(X)$ 在 $X=x_j$ 处取值为 $1$，在所有其他 $x_i,j\ne i$ 处取值为 $0$。

继续我们的例子，我们得到四个拉格朗日基多项式：

$$\begin{array}{ccc}{l}_0(X)& =& \frac{(X-3)(X-2)(X-1)}{(-3)(-2)(-1)}\\ l_1(X)& =& \frac{(X-3)(X-2)(X)}{(-2)(-1)(1)}\\ l_2(X)& =& \frac{(X-3)(X-1)(X)}{(-1)(1)(2)}\\ l_3(X)& =& \frac{(X-2)(X-1)(X)}{(1)(2)(3)}\end{array}$$

于是我们的多项式约束为

$$\begin{array}{cccccccccccl}& f(0)\cdot l_0(X)& +& f(1)\cdot l_1(X)& +& f(2)\cdot l_2(X)& +& f(3)\cdot l_3(X)& -& f(X)& =& 0\\ ⟹& 0\cdot l_0(X)& +& 1\cdot l_1(X)& +& 4\cdot l_2(X)& +& 5\cdot l_3(X)& -& f(X)& =& 0.\end{array}$$

译自 halo2 book：user/wasm-port.md

在 WASM 中使用 halo2

由于 halo2 是用 Rust 编写的，你可以把它编译成 WebAssembly (wasm)，这样你就能在浏览器应用中为你的电路(circuit)使用证明器(prover)和验证器(verifier)了。本教程会带你了解将电路编译成 wasm 所需的全部知识。

在整个教程中，我们会参考 Zordle 的代码仓库作为示例，它是已知最早一批基于 Halo 2 电路的 webapp 之一。Zordle 是 ZK 版的 Wordle，其电路把玩家输入的单词以及玩家的分享格子（灰色、黄色和绿色方块）作为 advice 值，并验证它们是否正确匹配。因此，该证明(proof)验证了玩家知道输出分享表的一个"原像(preimage)"，之后仅凭这份 ZK 证明就可以完成验证。

电路代码设置

第一步是在 Rust 中创建与浏览器应用对接的函数。对于证明器，这通常会输入某种形式的 advice 和 instance 数据，用它生成完整的见证(witness)，然后输出一份证明。对于验证器，这通常会输入一份证明和某种形式的 instance，然后输出一个布尔值，表示该证明是否验证通过。

在 Zordle 的例子里，这部分代码位于 wasm.rs，由两个主要函数组成：

证明器(Prover)

#[wasm_bindgen]
pub async fn prove_play(final_word: String, words_js: JsValue, params_ser: JsValue) -> JsValue {
  // Steps:
  // - Deserialise function parameters
  // - Generate the instance and advice columns using the words
  // - Instantiate the circuit and generate the witness
  // - Generate the proving key from the params
  // - Create a proof
}

虽然具体的输入及其序列化方式取决于你的电路和 webapp 设置，但了解 Zordle 这个特定场景下的格式还是有用的，因为你的使用场景很可能与之类似：

这个函数把用户想要凑出的 final_word，以及他们尝试使用的单词（以 words_js 的形式）作为输入。它还把电路的参数作为输入，这些参数序列化在 params_ser 中。我们将在下面的 Params 小节中展开说明。

注意，函数参数是以与 wasm_bindgen 兼容的格式传入的：String 和 JsValue。JsValue 类型来自 Serde 库。你可以在这里的文档中找到关于这个类型及其用法的更多细节。

输出是一个用 Serde 转换成 JSValue 的 Vec<u8>。之后它会作为输入传给验证器函数。

验证器(Verifier)

#[wasm_bindgen]
pub fn verify_play(final_word: String, proof_js: JsValue, diffs_u64_js: JsValue, params_ser: JsValue) -> bool {
  // Steps:
  // - Deserialise function parameters
  // - Generate the instance columns using the diffs representation of the columns
  // - Generate the verifying key using the params
  // - Verify the proof
}

与证明器类似，我们接收输入并输出一个布尔值 true/false，表示证明的正确性。diffs_u64_js 对象是一个二维 JS 数组，由每个单元格(cell)的值组成，这些值指示颜色：灰色、黄色或绿色。它们被用来组装电路的 instance 列。

参数(Params)

此外，证明器和验证器函数都会输入 params_ser，这是多项式承诺方案(polynomial commitment scheme)的公开参数的序列化形式。作为一种性能优化，这些参数是作为输入传入的（而不是在 prove/verify 函数中重新生成），因为它们仅根据电路的 K 值确定，是常量。我们可以把它们单独存放在一个静态 web 服务器上，然后作为输入传给 WASM。要生成这些参数的二进制序列化形式（在 WASM 函数之外单独生成），你可以运行类似下面的代码：

fn write_params(K: u32) {
    let mut params_file = File::create("params.bin").unwrap();
    let params: Params<EqAffine> = Params::new(K);
    params.write(&mut params_file).unwrap();
}

之后，我们可以在 JavaScript 中从 web 服务器以 Uint8Array 这种字节序列化的格式读取 params.bin 文件，并把它作为 params_ser 传给 WASM，再在 Rust 中使用 js_sys 库进行反序列化。

理想情况下，将来我们应该能够不必序列化这些参数，而是直接序列化并使用电路的证明密钥(proving key)和验证密钥(verifying key)，但目前该库尚不支持这一点，相关追踪见 issue #449 和 #443。

Rust 与 WASM 环境设置

通常，Rust 代码会用 wasm-pack 工具编译成 WASM，只需改改一些构建命令即可，非常简单。然而，对于 halo2 的证明器/验证器函数，我们需要对构建过程做一些额外的改动。具体来说，主要有两处改动：

• 并行(Parallelism)：halo2 使用 rayon 库来实现并行，而 WASM 并不直接支持它。不过，Chrome 团队提供了一个适配器，可以在浏览器中使用 Web Workers 实现类 rayon 的并行：wasm-bindgen-rayon。我们将用它在 WASM 证明器/验证器中启用并行。
• WASM 最大内存：wasm-bindgen 下 WASM 的默认内存上限被设为 2GB，这不足以为大型电路（K 大于 10 左右）运行 halo2 证明器。我们需要把这个上限提高到 WASM 允许的最大值（4GB！），以支持更大的电路（直到 K = 15 左右）。

首先，把你的 WASM 对接函数所特有的所有依赖添加到 Cargo.toml 文件中。你可以通过 WASM 目标特性标志(target feature flag)把这些依赖限定在 WASM 编译范围内。在 Zordle 的例子中，它看起来是这样的：

[target.'cfg(target_family = "wasm")'.dependencies]
getrandom = { version = "0.2", features = ["js"]}
wasm-bindgen = { version = "0.2.81", features = ["serde-serialize"]}
console_error_panic_hook = "0.1.7"
rayon = "1.5"
wasm-bindgen-rayon = { version = "1.0"}
web-sys = { version = "0.3", features = ["Request", "Window", "Response"] }
wasm-bindgen-futures = "0.4"
js-sys = "0.3"

接下来，让我们把 wasm-bindgen-rayon 集成到代码中。该库的 README 很好地概述了如何做到这一点。特别要注意对 Rust 编译流程的改动。你需要切换到 nightly 版本的 Rust，并启用对 WASM atomics 的支持。此外，记得在 Rust 代码中导出 init_thread_pool。

接下来，我们要把 wasm-pack 默认的 2GB 最大内存上限提上去。为此，在 .cargo/config 文件中为 wasm 目标添加 Rust 标志 "-C", "link-arg=--max-memory=4294967296"。完成 wasm-bindgen-rayon 的设置并提高内存上限后，.cargo/config 文件现在应该是这样的：

[target.wasm32-unknown-unknown]
rustflags = ["-C", "target-feature=+atomics,+bulk-memory,+mutable-globals", "-C", "link-arg=--max-memory=4294967296"]
...

特别感谢 @mattgibb，他在一个不起眼的 GitHub issue 里记录了这个晦涩的、用于提高最大内存的改动。¹

现在 Rust 这边已经设置好了，你应该可以直接用 wasm-pack build --target web --out-dir pkg 构建出一个 WASM 包，并在你的 webapp 中使用输出的 WASM 包了。

Webapp 设置

Zordle 附带了一个极简的 React 测试客户端作为示例（它只是在默认的 create-react-app 模板上加入了 WASM 支持）。你可以在这里找到这个测试客户端的代码。我建议你为自己的应用 fork 这个测试客户端，并以此为起点开始开发。

该测试客户端包含一个干净的 WebWorker，用于与 Rust WASM 包对接。把对接逻辑放进 WebWorker 中可以避免阻塞浏览器主线程，并为 React/应用逻辑提供一个干净的接口。查看 halo-worker.ts 了解 WebWorker 代码，并在 App.tsx 中看看如何从 React 与该 web worker 对接。

如果到目前为止你都做对了，那么你现在应该可以在浏览器中生成并验证证明了！在 Zordle 的例子里，一个 K = 14 的电路在我的笔记本上生成证明大约需要一分钟左右。在生成证明期间，如果你打开 Chrome/Firefox 的任务管理器，应该还能看到类似下面的画面：

Zordle 及其 test-client 默认把并行度设置为机器上可用的核心数。如果你想减少它，可以通过修改 initThreadPool 的参数来实现。

如果你更愿意使用自己的 Worker/React 设置，那么获取并序列化参数、证明以及其他 instance 和 advice 值的代码可能仍然值得一看！

Safari

注意，wasm-bindgen-rayon 库不被 Safari 支持，因为它会从一个 Web Worker 内部再派生(spawn)出新的 Web Workers。根据相关的 Webkit issue，对该特性的支持已于 2022 年 11 月进入 Safari Technology Preview，而且 Safari Technology Preview Release 155 的发行说明确实声称已支持，所以如果这一点对你很重要，值得去确认它是否已经进入正式版 Safari。

调试

你常常会遇到 Rust 代码出问题，看到 WASM 执行时报错 Uncaught (in promise) RuntimeError: unreachable，这是一个对调试完全没有帮助的错误。这是因为代码是以 release 模式编译的，作为性能优化它去掉了错误消息。要调试，你可以用 wasm-pack build 加上 --dev 标志，以 debug 模式构建 WASM 包。这会以 debug 模式构建，会显著拖慢执行速度，但能让你在浏览器控制台中看到任何运行时错误消息。此外，你可以安装 console_error_panic_hook crate（Zordle 就是这么做的），以便在发生运行时 panic 时也能得到有用的调试消息。

致谢

本指南由 Nalin 编写。另外感谢 Uma 和 Blaine 在弄清这些步骤上所做的大量工作。如果你在任何步骤上遇到困难，欢迎随时联系我。

1. 题外话，但让我相当惊讶的是，WASM 有一个 4GB 内存的硬性上限。这是因为 WASM 目前是 32 位架构，对于这样一门崭新的、面向未来的汇编语言来说，这一点让我颇为意外。不过，确实有一些公开的提案，主张把 WASM 迁移到更大的地址空间。 ↩

译自 halo2 book：dev.md

开发者文档(Developer Documentation)

你想为 Halo 2 的各个 crate 做贡献？太棒了！

本节介绍我们的开发流程与审查标准的相关信息，以及在维护和扩展代码库时有用的一些技巧。

译自 halo2 book：dev/features.md

特性开发(Feature development)

有时特性开发(feature development)需要随时间不断迭代某个设计。尽早在下游(downstream) crate 中开始使用某个特性，对积累 API 与功能上的使用经验很有帮助，而这些经验又能在特性稳定化之前反馈到它的设计中。为实现这一点，我们采用一种受 Rust 编译器启发（但并不完全相同）的三阶段 nightly -> beta -> stable 开发模式。

特性标志(Feature flags)

每个尚未稳定化的特性都有一个默认关闭的特性标志(feature flag)来启用它，形式为 unstable-*。当该特性标志被禁用时，各 crate 的稳定 API(stable API)绝不能受到影响，除非是某些会按具体情况逐一考量的复杂特性。

我们还提供了两个元标志(meta-flag)，用于启用某个稳定化级别的全部特性：

• beta 启用所有处于 "beta" 阶段的特性（并隐式启用所有处于 "stable" 阶段的特性）。
• nightly 启用所有处于 "beta" 和 "nightly" 阶段的特性（并隐式启用所有处于 "stable" 阶段的特性），即启用全部特性。
• 当两个标志都未启用（且没有任何特性专属标志被启用）时，实际上只启用处于 "stable" 阶段的特性。

特性工作流(Feature workflow)

• 如果维护者们达成了大致共识(rough consensus)，认为某个实验性特性总体上是受欢迎的，那么可以乐观地以较低的审查标准，把它的初始实现合并进代码库，并置于一个该特性专属的特性标志之后。该特性的标志会被加入 nightly 特性标志集合。
  • 在 halo2 各 crate 的下一次常规发布(general release)中，该特性即可被下游已发布的 crate 使用。
  • 该特性后续的开发与完善可以通过额外的 PR 就地(in-situ)进行，并配以额外的审查。
  • 如果该特性最终与其他特性（尤其是已稳定化的特性）产生不良交互，那么之后可以将其移除，而不影响 stable 或 beta 的 API。
• 一旦该特性经过了充分审查，并且达到了某个 halo2 用户认为其已可用于生产(production-ready)（且愿意或计划将其部署到生产环境）的程度，该特性的特性标志就会被移入 beta 特性标志集合。
• 一旦该特性经过了等同于 stable 审查策略的审查，并且达成了大致共识，认为该特性对更广泛的 halo2 用户群体有用，该特性的特性标志就会被移除，该特性也随之成为主维护代码库的一部分。

对于更复杂的特性，上述工作流可能会辅以 beta 和 nightly 分支；这一点将在某个需要此机制的特性被提名为纳入候选时再行确定。

进行中的特性(In-progress features)

译自 halo2 book:https://zcash.github.io/halo2/design.html

设计

关于术语的说明

我们使用与他人略有不同的术语来描述 PLONK 概念。以下是概览:

1. 我们倾向于把类 PLONK 的论证(argument)看作一张表格,其中每一列对应一条"线"(wire)。我们把表格中的条目称为"单元格"(cell)。
2. 我们倾向于把"选择子多项式"(selector polynomial)之类的东西改称为"固定列"(fixed column)。当一个固定列中的单元格被用来控制某条约束(constraint)是否在该行启用时,我们会专门称之为"选择子约束"(selector constraint)。
3. 当另一些多项式由证明者(prover)填充时,我们通常把它们称为"建议列"(advice column)。
4. 我们使用术语"规则"(rule)来指代像下面这样的"门"(gate): $$A(X)\cdot q_A(X)+B(X)\cdot q_B(X)+A(X)\cdot B(X)\cdot q_M(X)+C(X)\cdot q_C(X)=0.$$
   • TODO:检查我们在这一点上的一致性,并更新代码和文档以保持匹配。

译自 halo2 book:https://zcash.github.io/halo2/design/proving-system.html

证明系统(Proving system)

Halo 2 的证明系统可以分解为五个阶段:

1. 对编码电路主要组成部分的多项式做承诺(commit):
   • 单元格赋值(cell assignment)。
   • 每个查表论证(lookup argument)的置换值(permuted value)与乘积(product)。
   • 等式约束置换(equality constraint permutation)。
2. 构造消失论证(vanishing argument),以将所有电路关系约束为零:
   • 标准门(standard gate)与自定义门(custom gate)。
   • 查表论证规则。
   • 等式约束置换规则。
3. 在所有必要的点上对上述多项式求值:
   • 所有列上、所有自定义门所用的相对旋转(relative rotation)。
   • 消失论证的各个分片。
4. 构造多点打开论证(multipoint opening argument),以检查所有求值与各自的承诺保持一致。
5. 运行内积论证(inner product argument),为多点打开论证的多项式创建一个多项式承诺打开证明(polynomial commitment opening proof)。

本章接下来将依次介绍这些阶段。

示例

为了便于讲解,我们有时会引用如下示例约束系统(constraint system):

• 四个建议列(advice column)$a,b,c,d$。
• 一个固定列(fixed column)$f$。
• 三个自定义门:
  • $a\cdot b\cdot c_{-1}-d=0$
  • $f_{-1}\cdot c=0$
  • $f\cdot d\cdot a=0$

tl;dr(太长不看)

下表对 Halo 2 协议给出一个(可能过于)简洁的描述。这一描述很可能会被 Halo 2 论文及其安全性证明所取代,但目前可作为接下来各小节内容的摘要。

然后证明者与验证者:

• 使用 $x_4$ 的幂次,将 $\text{finalPoly}(X)$ 构造为 $\mathbf{Q}$ 与 $U$ 的线性组合;
• 将 $\text{finalPolyEval}$ 构造为 ${\mathbf{q}}_{\text{evals}}$ 与 $u_{\text{eval}}$ 的等价线性组合;并
• 执行 $\text{InnerProduct}(\text{finalPoly}(X),x_3,\text{finalPolyEval}).$

TODO:撰写提供零知识(zero-knowledge)的协议组件。

译自 halo2 book:https://zcash.github.io/halo2/design/proving-system/lookup.html

查表论证(Lookup argument)

Halo 2 使用以下查表技术,它允许在任意集合中进行查表,并且可以说比 Plookup 更简单。

关于术语的说明

除了关于术语的通用说明之外:

• 我们把 $Z(X)$ 多项式(置换论证中的大乘积论证多项式,grand product argument polynomial)称为"置换乘积"(permutation product)列。

技术描述

为了便于讲解,我们先描述一个忽略零知识(zero knowledge)的简化版本论证。

我们用一个"子集论证"(subset argument)来表达查表,该论证作用于一张具有 $2^k$ 行(从 0 开始编号)、含有列 $A$ 和 $S$ 的表格之上。

子集论证的目标是强制 $A$ 中的每个单元格都等于 $S$ 中的_某个_单元格。这意味着 $A$ 中的多个单元格可以等于 $S$ 中的_同一个_单元格,而 $S$ 中的某些单元格不需要等于 $A$ 中的任何单元格。

• $S$ 可以是固定的,但不必如此。也就是说,我们既支持在固定表中查值,也支持在变量表(后者包含建议列)中查值。
• $A$ 和 $S$ 可以包含重复项。如果 $A$ 和/或 $S$ 所表示的集合的大小不天然为 $2^k$,我们就用重复项扩充 $S$,并用已知存在于 $S$ 中的占位值(dummy value)扩充 $A$。
  • 或者,我们可以添加一个"查表选择子"(lookup selector),用来控制 $A$ 列中的哪些元素参与查表。这会修改下面置换规则中 $A(X)$ 的出现:当某行未被选中进行查表时,把 $A$ 替换为(例如)$S_0$。

设 ${\ell }_i$ 为拉格朗日基(Lagrange basis)多项式,它在第 $i$ 行求值为 $1$,其余处为 $0$。

我们先允许证明者提供 $A$ 和 $S$ 的置换列。分别称之为 $A^{\prime }$ 和 $S^{\prime }$。我们可以用一个带乘积列 $Z$ 的置换论证来强制它们确实是置换,规则如下:

$$Z(\omega X)\cdot (A^{\prime }(X)+\beta )\cdot (S^{\prime }(X)+\gamma )-Z(X)\cdot (A(X)+\beta )\cdot (S(X)+\gamma )=0$$$${\ell }_0(X)\cdot (1-Z(X))=0$$

即:只要不发生除以零的情况,对所有 $i\in [0,2^k)$ 我们有:

$$Z_{i+1}=Z_i\cdot \frac{(A_i+\beta )\cdot (S_i+\gamma )}{(A_i^{\prime }+\beta )\cdot (S_i^{\prime }+\gamma )}$$$$Z_{2^k}=Z_0=1.$$

这是置换论证的一个版本,它允许 $A^{\prime }$ 和 $S^{\prime }$ 分别是 $A$ 和 $S$ 的置换,但并不指定具体的置换。$\beta$ 和 $\gamma$ 是两个独立的挑战(challenge),这样我们就可以把这两个置换论证合并为一个,而不必担心它们彼此干扰。

这些置换的目标,是允许证明者以特定方式排列 $A^{\prime }$ 和 $S^{\prime }$:

1. $A^{\prime }$ 列中的所有单元格被排列成:取值相同的单元格在竖直方向上相邻。这可以通过某种排序算法完成,但真正重要的只是:取值相同的单元格在 $A^{\prime }$ 列中位于连续的行上,且 $A^{\prime }$ 是 $A$ 的一个置换。
2. 在 $A^{\prime }$ 中一段相同取值的序列里,第一行就是 $S^{\prime }$ 中具有相应取值的那一行。除此约束之外,$S^{\prime }$ 可以是 $S$ 的任意置换。

现在,我们用如下规则来强制要么 $A_i^{\prime }=S_i^{\prime }$,要么 $A_i^{\prime }=A_{i-1}^{\prime }$:

$$(A^{\prime }(X)-S^{\prime }(X))\cdot (A^{\prime }(X)-A^{\prime }({\omega }^{-1}X))=0$$

此外,我们用如下规则强制 $A_0^{\prime }=S_0^{\prime }$:

$${\ell }_0(X)\cdot (A^{\prime }(X)-S^{\prime }(X))=0$$

(尽管 ${\omega }^{-1}X$ 会"绕回",这里第一条规则中的 $A^{\prime }(X)-A^{\prime }({\omega }^{-1}X)$ 项在第 $0$ 行也不起作用,因为有第二条规则。)

这些约束合在一起,有效地强制 $A^{\prime }$(从而 $A$)中的每个元素都至少等于 $S^{\prime }$(从而 $S$)中的一个元素。证明:对各行前缀做归纳。

零知识调整

为了让基于 PLONK 的证明系统实现零知识,我们需要把每一列的最后 $t$ 行填充为随机值。这要求对查表论证作出调整,因为这些随机值并不满足上面描述的约束。

我们把可用行(usable row)的数量限制为 $u=2^k-t-1$。我们添加两个选择子:

• $q_{blind}$ 在最后 $t$ 行上置为 $1$,其余处为 $0$;
• $q_{last}$ 仅在第 $u$ 行置为 $1$,其余处为 $0$(即它被置于可用行与盲化行之间的那一行)。

我们仅对可用行启用上面的约束:

$$(1-(q_{last}(X)+q_{blind}(X)))\cdot (Z(\omega X)\cdot (A^{\prime }(X)+\beta )\cdot (S^{\prime }(X)+\gamma )-Z(X)\cdot (A(X)+\beta )\cdot (S(X)+\gamma ))=0$$$$(1-(q_{last}(X)+q_{blind}(X)))\cdot (A^{\prime }(X)-S^{\prime }(X))\cdot (A^{\prime }(X)-A^{\prime }({\omega }^{-1}X))=0$$

在第 $0$ 行启用的规则保持不变:

$${\ell }_0(X)\cdot (A^{\prime }(X)-S^{\prime }(X))=0$$$${\ell }_0(X)\cdot (1-Z(X))=0$$

由于我们不能再依赖绕回(wraparound)来保证乘积 $Z$ 在 ${\omega }^{2^k}$ 处重新变为 $1$,我们改为需要把 $Z({\omega }^u)$ 约束为 $1$。然而,这里存在一个潜在困难:如果对某个 $i\in [0,u)$,$A_i+\beta$ 或 $S_i+\gamma$ 中有任何一个为零,那么可能无法满足置换论证。这种情况在 $\beta$ 和 $\gamma$ 的选择上以可忽略的概率发生,但它既是实现完美零知识的障碍(因为对手可以排除掉会导致这种情况的见证值),也是实现完美完备性(perfect completeness)的障碍。

为了同时确保完美完备性和完美零知识,我们允许 $Z({\omega }^u)$ 取零或一:

$$q_{last}(X)\cdot (Z(X{)}^2-Z(X))=0$$

现在,如果对某个 $i$,$A_i+\beta$ 或 $S_i+\gamma$ 为零,我们就可以对 $i<j\le u$ 设 $Z_j=0$,从而满足约束系统。

注意,挑战 $\beta$ 和 $\gamma$ 是在对 $A$ 和 $S$(以及 $A^{\prime }$ 和 $S^{\prime }$)做出承诺之后才选定的,因此证明者无法强行制造出某个 $A_i+\beta$ 或 $S_i+\gamma$ 为零的情况。由于这种情况以可忽略的概率发生,可靠性(soundness)不受影响。

开销

• 有原始列 $A$ 和固定列 $S$。
• 有一个置换乘积列 $Z$。
• 有两个置换 $A^{\prime }$ 和 $S^{\prime }$。
• 这些门的次数(degree)都很低。

推广

Halo 2 的查表论证实现以如下方式推广了上述技术:

• $A$ 和 $S$ 可以扩展为多列,并用一个随机挑战组合起来。$A^{\prime }$ 和 $S^{\prime }$ 仍保持为单列。
  • 对 $S$ 各列的承诺可以预先计算,然后在挑战已知后,利用 Pedersen 承诺的同态(homomorphic)性质廉价地组合起来。
  • $A$ 的各列可以用相对引用以任意多项式表达式给出。这些表达式会被代入乘积列约束中,但要受最大次数界(maximum degree bound)的限制。这有可能节省一个或多个建议列。
• 然后,任意宽度关系的查表论证可以用子集论证来实现,即:为了在每一行约束 $\mathcal{R}(x,y,...)$,把 $\mathcal{R}$ 看作一个元组集合 $S$(使用上一点的方法),并检查 $(x,y,...)\in \mathcal{R}$。
  • 在 $\mathcal{R}$ 表示一个函数的情况下,这隐式地也检查了输入是否在定义域内。这通常正是我们想要的,且常常能省掉一次额外的范围检查(range check)。
• 我们可以在同一个电路中支持多张表,办法是把它们合并成单张表,其中包含一个标签列(tag column)来标识原始表。
  • 如果前面提到的"查表选择子"得以实现,标签列可以与之合并。

这些推广与 Plookup 论文第 4、5 节中的推广类似。也就是说,与 Plookup 的差异在于子集论证。这一论证随后可以用于所有相同的用途;例如,Plookup 论文第 5 节中优化的范围检查技术也可以与这个子集论证一起使用。

译自 halo2 book:https://zcash.github.io/halo2/design/proving-system/permutation.html

置换论证(Permutation argument)

鉴于 halo2 电路中的门是"局部地"操作的(作用于当前行或定义好的相对行中的单元格),因此常常需要把某个任意单元格中的值复制到当前行中,以供门使用。这是通过等式约束(equality constraint)来完成的,该约束强制源单元格与目标单元格包含相同的值。

我们实现这些等式约束的方式,是构造一个表示这些约束的置换,然后在证明中使用置换论证来强制它们成立。

记号

置换(permutation)是一个集合到其自身的一一(one-to-one)且映满(onto)的映射。一个置换可以唯一地分解为若干循环(cycle)的复合(在循环的排序以及每个循环的旋转意义下)。

我们有时使用循环记号(cycle notation)来书写置换。设 $(abc)$ 表示一个循环,其中 $a$ 映到 $b$,$b$ 映到 $c$,$c$ 映到 $a$(对任意大小的循环有显然的推广)。把两个或多个循环并排书写表示对应置换的复合。例如,$(ab)(cd)$ 表示这样的置换:把 $a$ 映到 $b$,$b$ 映到 $a$,$c$ 映到 $d$,$d$ 映到 $c$。

构造置换

目标

我们想要构造一个置换,使得处于同一等式约束集合中的每一组变量构成一个循环。例如,假设我们有一个电路,定义了如下等式约束:

• $a\equiv b$
• $a\equiv c$
• $d\equiv e$

由此我们得到等式约束集合 $\{a,b,c\}$ 和 $\{d,e\}$。我们想要构造置换:

$$(abc)(de)$$

它定义了从 $[a,b,c,d,e]$ 到 $[b,c,a,e,d]$ 的映射。

算法

我们需要跟踪一组循环,这是一个不相交集合的集合(set of disjoint sets)。针对这一问题已有高效的数据结构;为简单起见,我们选择一个并非渐近最优、但易于实现的数据结构。

我们将当前状态表示为:

• 一个数组 $\mathsf{mapping}$,表示置换本身;
• 一个辅助数组 $\mathsf{aux}$,跟踪每个循环的一个特定代表元素;
• 另一个数组 $\mathsf{sizes}$,跟踪每个循环的大小。

我们有这样一个不变式:对于给定循环 $C$ 中的每个元素 $x$,$\mathsf{aux}(x)$ 都指向同一个元素 $c\in C$。这使我们能够通过检查 $\mathsf{aux}(x)=\mathsf{aux}(y)$ 来快速判定给定的两个元素 $x$ 和 $y$ 是否在同一循环中。此外,$\mathsf{sizes}(\mathsf{aux}(x))$ 给出包含 $x$ 的循环的大小。(这一点仅对 $\mathsf{sizes}(\mathsf{aux}(x))$ 成立,而不对 $\mathsf{sizes}(x)$ 成立。)

算法以恒等置换(identity permutation)的表示作为起点:对所有 $x$,我们设 $\mathsf{mapping}(x)=x$,$\mathsf{aux}(x)=x$,$\mathsf{sizes}(x)=1$。

要添加一个等式约束 $left\equiv right$:

1. 检查 $left$ 和 $right$ 是否已经在同一循环中,即是否 $\mathsf{aux}(left)=\mathsf{aux}(right)$。若是,则无需做任何事。
2. 否则,$left$ 和 $right$ 属于不同的循环。让 $left$ 为较大的循环、$right$ 为较小的循环:当 $\mathsf{sizes}(\mathsf{aux}(left))<\mathsf{sizes}(\mathsf{aux}(right))$ 时把二者交换。
3. 设 $\mathsf{sizes}(\mathsf{aux}(left)):=\mathsf{sizes}(\mathsf{aux}(left))+\mathsf{sizes}(\mathsf{aux}(right)).$
4. 沿着映射绕较小(右侧)循环走一圈,对每个元素 $x$ 设 $\mathsf{aux}(x):=\mathsf{aux}(left)$。
5. 通过交换 $\mathsf{mapping}(left)$ 与 $\mathsf{mapping}(right)$,把较小的循环拼接(splice)进较大的循环中。

例如,给定两个不相交的循环 $(ABCD)$ 和 $(EFGH)$:

A +---> B
^       +
|       |
+       v
D <---+ C       E +---> F
                ^       +
                |       |
                +       v
                H <---+ G

在添加约束 $B\equiv E$ 之后,上述算法产生如下循环:

A +---> B +-------------+
^                       |
|                       |
+                       v
D <---+ C <---+ E       F
                ^       +
                |       |
                +       v
                H <---+ G

错误的替代做法

如果我们不检查 $left$ 和 $right$ 是否已经在同一循环中,那么我们可能会撤销一个等式约束。例如,如果我们有如下约束:

• $a\equiv b$
• $b\equiv c$
• $c\equiv d$
• $b\equiv d$

而我们试图仅用上述算法的第 5 步来实现等式约束的添加,那么我们最终会构造出循环 $(ab)(cd)$,而不是正确的 $(abcd)$。

论证规约(Argument specification)

我们需要检查 $m$ 列中单元格的一个置换,这些列以拉格朗日基表示为多项式 $v_0,\dots ,v_{m-1}$。

我们将给这 $m$ 列中的每个单元格标注一个 ${\mathbb{F}}^{\times }$ 中唯一的元素。

假设我们在这些标签上有一个置换, $$\sigma (\mathsf{column}:i,\mathsf{row}:j)=(\mathsf{column}:i^{\prime },\mathsf{row}:j^{\prime }).$$ 其中各循环对应于等式约束集合。

如果我们考虑序对的集合 $\{(label,value)\}$,那么每个循环中的各个值彼此相等,当且仅当用 $\sigma$ 对每个序对中的标签进行置换后,得到的是同一个集合:

由于标签互不相同,集合相等等同于多重集合(multiset)相等,而后者可以用乘积论证(product argument)来检查。

设 $\omega$ 为一个 $2^k$ 次单位根(root of unity),设 $\delta$ 为一个 $T$ 次单位根,其中 $T\cdot 2^S+1=p$,$T$ 为奇数且 $k\le S.$ 我们将用 ${\delta }^i\cdot {\omega }^j\in {\mathbb{F}}^{\times }$ 作为置换论证中第 $i$ 列第 $j$ 行单元格的标签。

我们用一个由 $m$ 个多项式 $s_i(X)$ 构成的向量来表示 $\sigma$,使得 $s_i({\omega }^j)={\delta }^{i^{\prime }}\cdot {\omega }^{j^{\prime }}.$

注意,恒等置换可以用由 $m$ 个多项式 ${\mathsf{ID}}_i({\omega }^j)$ 构成的向量来表示,使得 ${\mathsf{ID}}_i({\omega }^j)={\delta }^i\cdot {\omega }^j.$

我们将用一个挑战 $\beta$ 把每个 $(label,value)$ 序对压缩为 $value+\beta \cdot label.$ 正如我们在查表中所用的乘积论证一样,我们还使用一个挑战 $\gamma$ 来随机化乘积的每一项。

现在,给定由 $s_0,\dots ,s_{m-1}$ 表示的置换,作用于由 $v_0,\dots ,v_{m-1}$ 表示的各列,我们想要确保: $$\prod _{i=0}^{m-1}\prod _{j=0}^{n-1}\left(\frac{v_i({\omega }^j)+\beta \cdot {\delta }^i\cdot {\omega }^j+\gamma }{v_i({\omega }^j)+\beta \cdot s_i({\omega }^j)+\gamma }\right)=1$$

这里 $v_i({\omega }^j)+\beta \cdot {\delta }^i\cdot {\omega }^j$ 表示未置换的 $(label,value)$ 序对,而 $v_i({\omega }^j)+\beta \cdot s_i({\omega }^j)$ 表示已置换的 $(\sigma (label),value)$ 序对。

设 $Z_P$ 满足 $Z_P({\omega }^0)=Z_P({\omega }^n)=1$,且对 $0\le j<n$: $$\begin{array}{rl}{Z}_P({\omega }^{j+1})& =\prod _{h=0}^j\prod _{i=0}^{m-1}\frac{v_i({\omega }^h)+\beta \cdot {\delta }^i\cdot {\omega }^h+\gamma }{v_i({\omega }^h)+\beta \cdot s_i({\omega }^h)+\gamma }\\ & =Z_P({\omega }^j)\prod _{i=0}^{m-1}\frac{v_i({\omega }^j)+\beta \cdot {\delta }^i\cdot {\omega }^j+\gamma }{v_i({\omega }^j)+\beta \cdot s_i({\omega }^j)+\gamma }\end{array}$$

那么,强制如下规则就足够了: $$\begin{gathered} Z_P(\omega X)\cdot \prod _{i=0}^{m-1}\left(v_i(X)+\beta \cdot s_i(X)+\gamma \right)-Z_P(X)\cdot \prod _{i=0}^{m-1}\left(v_i(X)+\beta \cdot {\delta }^i\cdot X+\gamma \right)=0 \\ {\ell }_0\cdot (1-Z_P(X))=0 \end{gathered}$$

这里假设列数 $m$ 使得上述第一条规则中的多项式能够落在 PLONK 配置的次数界之内。我们将在下文看到如何处理更多列数的情况。

用于得到恒等置换简洁表示的这一优化由 Vitalik Buterin 为 PLONK 提出,描述在 PLONK 论文第 8 节末尾。注意,只要启用等式约束的列数不超过 $T$,这些 ${\delta }^i$ 就都是各不相同的二次非剩余(quadratic non-residue);对于 Halo 2 所用的曲线,这一点在实践中总是成立。

零知识调整

与查表论证类似,我们需要对上述论证作出调整,以应对每一列最后 $t$ 行被填充为随机值的情况。

我们把可用行的数量限制为 $u=2^k-t-1$。我们添加两个选择子,其定义方式与查表论证中相同:

• $q_{blind}$ 在最后 $t$ 行上置为 $1$,其余处为 $0$;
• $q_{last}$ 仅在第 $u$ 行置为 $1$,其余处为 $0$(即它被置于可用行与盲化行之间的那一行)。

我们仅对可用行启用上面的乘积规则:

$(1-(q_{last}(X)+q_{blind}(X)))\cdot$ $\left(Z_P(\omega X)\cdot \prod _{i=0}^{m-1}\left(v_i(X)+\beta \cdot s_i(X)+\gamma \right)-Z_P(X)\cdot \prod _{i=0}^{m-1}\left(v_i(X)+\beta \cdot {\delta }^i\cdot X+\gamma \right)\right)=0$

在第 $0$ 行启用的规则保持不变:

$${\ell }_0(X)\cdot (1-Z_P(X))=0$$

由于我们不能再依赖绕回来保证每个乘积 $Z_P$ 在 ${\omega }^{2^k}$ 处重新变为 $1$,我们改为需要约束 $Z({\omega }^u)=1$。这就引出了与查表论证中所描述的相同的问题。因此我们允许 $Z({\omega }^u)$ 取零或一:

$$q_{last}(X)\cdot (Z_P(X{)}^2-Z_P(X))=0$$

这给出了完美完备性和零知识。

跨越大量列

halo2 的实现在实践中并不限制可启用等式约束的列数。因此,它必须解决一个问题:上述方法可能产生一个乘积规则,其中的多项式超出了 PLONK 配置的次数界。次数界可以提高,但如果没有其他规则需要更大的次数,这样做会效率低下。

取而代之,我们把乘积拆分到 $b$ 个由 $m$ 列组成的列集(column set)上,使用乘积列 $Z_{P,0},\dots Z_{P,b-1}$,并用另一条规则把乘积从一个列集的末端复制到下一个列集的开端。

也就是说,对 $0\le a<b$ 我们有:

$(1-(q_{last}(X)+q_{blind}(X)))\cdot$ $\left(Z_{P,a}(\omega X)\cdot \prod _{i=am}^{(a+1)m-1}\left(v_i(X)+\beta \cdot s_i(X)+\gamma \right)-Z_P(X)\cdot \prod _{i=am}^{(a+1)m-1}\left(v_i(X)+\beta \cdot {\delta }^i\cdot X+\gamma \right)\right)$ $=0$

为简单起见,这里的书写假设启用等式约束的列数是 $m$ 的倍数;如果不是,那么最后一个列集的乘积将少于 $m$ 项。

对于第一个列集我们有:

$${\ell }_0\cdot (1-Z_{P,0}(X))=0$$

对于每个后续列集 $0<a<b$,我们用如下规则把 $Z_{P,a-1}({\omega }^u)$ 复制到下一个列集的起点 $Z_{P,a}({\omega }^0)$:

$${\ell }_0\cdot \left(Z_{P,a}(X)-Z_{P,a-1}({\omega }^{u}X)\right)=0$$

对于最后一个列集,我们允许 $Z_{P,b-1}({\omega }^u)$ 取零或一:

$$q_{last}(X)\cdot \left(Z_{P,b-1}(X{)}^2-Z_{P,b-1}(X)\right)=0$$

这与之前一样给出了完美完备性和零知识。

译自 halo2 book:https://zcash.github.io/halo2/design/proving-system/circuit-commitments.html

电路承诺(Circuit commitments)

对电路赋值做承诺

在证明创建之初,证明者持有一张单元格赋值表,它声称这些赋值满足约束系统。该表有 $n=2^k$ 行,并被划分为建议(advice)列、实例(instance)列和固定(fixed)列。我们定义 $F_{i,j}$ 为第 $i$ 个固定列第 $j$ 行的赋值。不失一般性,我们类似地定义 $A_{i,j}$ 来表示建议列和实例列的赋值。

我们在这里把固定列单独区分出来,因为它们由验证者提供,而建议列和实例列由证明者提供。在实践中,对实例列和固定列的承诺由证明者和验证者双方各自计算,只有建议列的承诺被存入证明中。

为了对这些赋值做承诺,我们在一个大小为 $n$ 的求值域(evaluation domain)上,为每一列构造次数为 $n-1$ 的拉格朗日多项式(其中 $\omega$ 是第 $n$ 个本原单位根,primitive root of unity):

• $a_i(X)$ 插值得到 $a_i({\omega }^j)=A_{i,j}$。
• $f_i(X)$ 插值得到 $f_i({\omega }^j)=F_{i,j}$。

然后,我们对每一列的多项式创建一个盲化承诺(blinding commitment):

$$\mathbf{A}=[\text{Commit}(a_0(X)),\dots ,\text{Commit}(a_i(X))]$$ $$\mathbf{F}=[\text{Commit}(f_0(X)),\dots ,\text{Commit}(f_i(X))]$$

$\mathbf{F}$ 作为密钥生成(key generation)的一部分构造,使用值为 $1$ 的盲化因子(blinding factor)。$\mathbf{A}$ 由证明者构造并发送给验证者。

对查表置换做承诺

验证者首先采样 $\theta$,它用于保持查表内部各个列彼此独立。然后,证明者按如下方式对每个查表的置换做承诺:

• 给定一个查表,其输入列多项式为 $[A_0(X),\dots ,A_{m-1}(X)]$,表列多项式为 $[S_0(X),\dots ,S_{m-1}(X)]$,证明者构造两个压缩多项式

  $$A_{\text{compressed}}(X)={\theta }^{m-1}{A}_0(X)+{\theta }^{m-2}{A}_1(X)+\cdots +\theta A_{m-2}(X)+A_{m-1}(X)$$ $$S_{\text{compressed}}(X)={\theta }^{m-1}{S}_0(X)+{\theta }^{m-2}{S}_1(X)+\cdots +\theta S_{m-2}(X)+S_{m-1}(X)$$

• 然后证明者按照查表论证的规则对 $A_{\text{compressed}}(X)$ 和 $S_{\text{compressed}}(X)$ 做置换,得到 $A^{\prime }(X)$ 和 $S^{\prime }(X)$。

证明者为所有查表创建盲化承诺

$$\mathbf{L}=\left[(\text{Commit}(A^{\prime }(X))),\text{Commit}(S^{\prime }(X))),\dots \right]$$

并将它们发送给验证者。

在验证者收到 $\mathbf{A}$、$\mathbf{F}$ 和 $\mathbf{L}$ 之后,它采样挑战 $\beta$ 和 $\gamma$,这两个挑战将用于置换论证以及下文中查表论证的剩余部分。(由于这些论证彼此独立,这些挑战可以复用。)

对等式约束置换做承诺

设 $c$ 为启用了等式约束的列数。

设 $m$ 为在不超过 PLONK 配置的最大约束次数的前提下,一个列集所能容纳的最大列数。

设 $u$ 为置换论证一节中定义的"可用"行数。

设 $b=\mathsf{ceiling}(c/m).$

证明者构造一个长度为 $bu$ 的向量 $\mathbf{P}$,使得对每个列集 $0\le a<b$ 和每一行 $0\le j<u$,

$${\mathbf{P}}_{au+j}=\prod _{i=am}^{\min (c,(a+1)m)-1}\frac{v_i({\omega }^j)+\beta \cdot {\delta }^i\cdot {\omega }^j+\gamma }{v_i({\omega }^j)+\beta \cdot s_i({\omega }^j)+\gamma }.$$

然后,证明者从 $1$ 开始计算 $\mathbf{P}$ 的连续乘积(running product),并按照置换论证一节所述,得到一个多项式向量 $Z_{P,\mathrm{0..}b-1}$,其中每个多项式的拉格朗日基表示对应于该连续乘积的一个大小为 $u$ 的切片。

证明者对每个 $Z_{P,a}$ 多项式创建盲化承诺:

$${\mathbf{Z}}_{\mathbf{P}}=\left[\text{Commit}(Z_{P,0}(X)),\dots ,\text{Commit}(Z_{P,b-1}(X))\right]$$

并将它们发送给验证者。

对查表置换乘积列做承诺

除了对各个置换后的查表做承诺之外,对于每个查表,证明者还需要对置换乘积列做承诺:

• 证明者构造一个向量 $P$:

$$P_j=\frac{(A_{\text{compressed}}({\omega }^j)+\beta )(S_{\text{compressed}}({\omega }^j)+\gamma )}{(A^{\prime }({\omega }^j)+\beta )(S^{\prime }({\omega }^j)+\gamma )}$$

• 证明者构造一个多项式 $Z_L$,其拉格朗日基表示对应于 $P$ 的连续乘积,从 $Z_L(1)=1$ 开始。

$\beta$ 和 $\gamma$ 用于组合关于 $A^{\prime }(X)$ 和 $S^{\prime }(X)$ 的置换论证,同时保持它们彼此独立。这里重要的一点是:验证者在证明者已创建 $\mathbf{A}$、$\mathbf{F}$ 和 $\mathbf{L}$(从而已对查表列中用到的所有单元格值、以及每个查表的 $A^{\prime }(X)$ 和 $S^{\prime }(X)$ 做出承诺)之后,才采样 $\beta$ 和 $\gamma$。

与之前一样,证明者对每个 $Z_L$ 多项式创建盲化承诺:

$${\mathbf{Z}}_{\mathbf{L}}=\left[\text{Commit}(Z_L(X)),\dots \right]$$

并将它们发送给验证者。

译自 halo2 book:https://zcash.github.io/halo2/design/proving-system/vanishing.html

消失论证(Vanishing argument)

在对电路赋值完成承诺后,证明者(prover)现在需要证明各种电路关系都被满足:

• 自定义门(custom gate),由多项式 ${\text{gate}}_i(X)$ 表示。
• 查找论证(lookup argument)的规则。
• 等式约束置换(equality constraint permutation)的规则。

这些关系中的每一个都被表示为一个关于电路列的、度数为 $d$(任意关系的最大度数)的多项式。鉴于每一列的赋值多项式度数为 $n-1$,这些关系多项式关于 $X$ 的度数为 $d(n-1)$。

在我们的示例中,这些就是门多项式,度数为 $3n-3$:

• ${\text{gate}}_0(X)=a_0(X)\cdot a_1(X)\cdot a_2(X{\omega }^{-1})-a_3(X)$
• ${\text{gate}}_1(X)=f_0(X{\omega }^{-1})\cdot a_2(X)$
• ${\text{gate}}_2(X)=f_0(X)\cdot a_3(X)\cdot a_0(X)$

如果一个关系的多项式等于零,则该关系被满足。证明这一点的一种方式是把每个关系多项式除以消失多项式(vanishing polynomial)$t(X)=(X^n-1)$,它是在每个 ${\omega }^i$ 处都有根的最低度数多项式。如果某个关系的多项式能被 $t(X)$ 整除,那么它在整个域(domain)上等于零(正如所期望的)。

这个简单的构造将需要对每个关系做一次多项式承诺(polynomial commitment)。我们改为同时对所有电路关系做承诺:验证者(verifier)采样 $y$,然后证明者构造商多项式(quotient polynomial)

$$h(X)=\frac{{\text{gate}}_0(X)+y\cdot {\text{gate}}_1(X)+\cdots +y^i\cdot {\text{gate}}_i(X)+\dots }{t(X)},$$

其中分子是各电路关系的一个随机(证明者在验证者采样 $y$ 之前已对单元格赋值做出承诺)线性组合。

• 如果分子多项式(以形式不定元 $X$ 表示)能被 $t(X)$ 完美整除,那么以高概率所有关系都被满足。
• 反之,如果至少有一个关系不被满足,那么以高概率 $h(x)\cdot t(x)$ 将不等于分子在 $x$ 处的求值。在这种情况下,分子多项式将不能被 $t(X)$ 完美整除。

对 $h(X)$ 做承诺

$h(X)$ 的度数为 $d(n-1)-n$(因为除数 $t(X)$ 的度数为 $n$)。然而,我们在 Halo 2 中使用的多项式承诺方案只支持对度数为 $n-1$ 的多项式做承诺(这是协议其余部分需要承诺的最大度数)。为了不增加多项式承诺方案的成本,证明者把 $h(X)$ 拆分成多个度数为 $n-1$ 的片段

$$h_0(X)+X^n{h}_1(X)+\cdots +X^{n(d-1)}{h}_{d-1}(X),$$

并对每个片段生成盲化承诺(blinding commitment)

$$\mathbf{H}=[\text{Commit}(h_0(X)),\text{Commit}(h_1(X)),\dots ,\text{Commit}(h_{d-1}(X))].$$

对多项式求值

到此为止,我们已经对电路的所有性质做出了承诺。验证者现在想要查看证明者是否承诺了正确的 $h(X)$ 多项式。验证者采样 $x$,证明者生成各个多项式在 $x$ 处的声称求值,涵盖电路中使用的所有相对偏移,以及 $h(X)$。

在我们的示例中,这将是:

• $a_0(x)$
• $a_1(x)$
• $a_2(x)$, $a_2(x{\omega }^{-1})$
• $a_3(x)$
• $f_0(x)$, $f_0(x{\omega }^{-1})$
• $h_0(x)$, ..., $h_{d-1}(x)$

验证者检查这些求值是否满足 $h(X)$ 的形式:

$$\frac{{\text{gate}}_0(x)+\cdots +y^i\cdot {\text{gate}}_i(x)+\dots }{t(x)}=h_0(x)+\cdots +x^{n(d-1)}{h}_{d-1}(x)$$

现在确信这些求值整体上满足门约束后,验证者需要检查这些求值本身与原始的电路承诺以及 $\mathbf{H}$ 是一致的。为了高效地实现这一点,我们使用多点打开论证(multipoint opening argument)。

译自 halo2 book:https://zcash.github.io/halo2/design/proving-system/multipoint-opening.html

多点打开论证(Multipoint opening argument)

考虑对多项式 $a(X),b(X),c(X),d(X)$ 的承诺 $A,B,C,D$。假设 $a$ 和 $b$ 在点 $x$ 处被查询,而 $c$ 和 $d$ 在 $x$ 与 $\omega x$ 两个点处都被查询。(这里,$\omega$ 是我们用来构造这些多项式的乘法子群中的本原单位根(primitive root of unity)。)

为了打开(open)这些承诺,我们可以为每个查询的点(对应电路中使用的每个相对旋转)创建一个多项式 $Q$。但这在电路中并不高效;例如,$c(X)$ 会出现在多个多项式中。

我们改为按照查询点的集合对承诺进行分组: $$\begin{array}{ccccc}& \{x\}& & \{x,\omega x\}& \\ & A& & C& \\ & B& & D& \end{array}$$

对于这些分组中的每一个,我们把它们合并成一个多项式集合,并为该集合创建单个 $Q$,然后在每个旋转处打开它。

优化步骤

多点打开优化以下列内容作为输入:

• 由验证者采样的随机 $x$,我们在该点对 $a(X),b(X),c(X),d(X)$ 求值。
• 由证明者提供的、每个多项式在每个相关点处的求值: $a(x),b(x),c(x),d(x),c(\omega x),d(\omega x)$

这些是消失论证(vanishing argument)的输出。

多点打开优化按如下方式进行:

1. 采样随机 $x_1$,以保持 $a,b,c,d$ 线性无关。

2. 根据多项式被查询时所在的点集,累加多项式及其对应的求值: q_polys: $$\begin{array}{rcclc}{q}_1(X)& =& a(X)& +& x_{1}b(X)\\ q_2(X)& =& c(X)& +& x_{1}d(X)\end{array}$$ q_eval_sets:

           [
               [a(x) + x_1 b(x)],
               [
                   c(x) + x_1 d(x),
                   c(\omega x) + x_1 d(\omega x)
               ]
           ]
   

   注:q_eval_sets 是一个由求值集合构成的向量,其中外层向量对应点集(本例中为 $\{x\}$ 和 $\{x,\omega x\}$),内层向量对应每个集合中的点。

3. 对 q_eval_sets 中的每个值集合做插值(interpolate): r_polys: $$\begin{array}{cccc}{r}_1(X)s.t.& & & \\ & r_1(x)& =& a(x)+x_{1}b(x)\\ r_2(X)s.t.& & & \\ & r_2(x)& =& c(x)+x_{1}d(x)\\ & r_2(\omega x)& =& c(\omega x)+x_{1}d(\omega x)\end{array}$$

4. 构造 f_polys,用于检查 q_polys 的正确性: f_polys $$\begin{array}{rcl}{f}_1(X)& =& \frac{q_1(X)-r_1(X)}{X-x}\\ f_2(X)& =& \frac{q_2(X)-r_2(X)}{(X-x)(X-\omega x)}\end{array}$$

   如果 $q_1(x)=r_1(x)$,那么 $f_1(X)$ 应当是一个多项式。 如果 $q_2(x)=r_2(x)$ 且 $q_2(\omega x)=r_2(\omega x)$, 那么 $f_2(X)$ 应当是一个多项式。

5. 采样随机 $x_2$ 以保持 f_polys 线性无关。

6. 构造 $f(X)=f_1(X)+x_2{f}_2(X)$。

7. 采样随机 $x_3$,我们在该点对 $f(X)$ 求值: $$\begin{array}{rcccl}f(x_3)& =& f_1(x_3)& +& x_2{f}_2(x_3)\\ & =& \frac{q_1(x_3)-r_1(x_3)}{x_3-x}& +& x_2\frac{q_2(x_3)-r_2(x_3)}{(x_3-x)(x_3-\omega x)}\end{array}$$

8. 采样随机 $x_4$ 以保持 $f(X)$ 与 q_polys 线性无关。

9. 构造 final_poly,$$final\_poly(X)=f(X)+x_4{q}_1(X)+x_4^2{q}_2(X),$$ 这就是我们在内积论证(inner product argument)中要承诺的多项式。

译自 halo2 book:https://zcash.github.io/halo2/design/proving-system/inner-product.html

内积论证(Inner product argument)

Halo 2 使用了一种多项式承诺方案(polynomial commitment scheme),我们可以基于内积论证(Inner Product Argument)为其创建多项式承诺打开证明(opening proof)。

TODO: 解释 Halo 2 的 IPA 变体。

它与 BCMS20 附录 A.2 中的 ${\text{PC}}_{\text{DL}}.\text{Open}$ 非常相似。 详见此对比。

译自 halo2 book:https://zcash.github.io/halo2/design/proving-system/comparison.html

与其他工作的对比

BCMS20 附录 A.2

BCMS20 的附录 A.2 描述了一种多项式承诺方案(polynomial commitment scheme),它与 BGH19 中描述的方案相似(BCMS20 是原始 Halo 论文的推广)。Halo 2 建立在这两项工作之上,因此其自身使用的多项式承诺方案与 BCMS20 中的方案非常相似。

下表给出了 BCMS20 中的变量名与 Halo 2 中等价对象(其建立在 Halo 论文的命名法之上)之间的映射:

Halo 2 的多项式承诺方案与 BCMS20 附录 A.2 在两个方面有所不同:

1. $\text{Open}$ 算法的第 8 步在内积论证(inner product argument)之前计算一个"非隐藏(non-hiding)"承诺 $C^{\prime }$,它打开到与 $C$ 相同的值,但它是对一个随机抽取的多项式所做的承诺。协议的其余部分不涉及任何盲化(blinding)。相比之下,在 Halo 2 中我们对我们做出的每一个承诺都进行盲化(即便是对实例(instance)和固定(fixed)多项式也是如此,不过对固定多项式使用盲化因子 1);这使得协议更易于推理分析。由此带来的结果是,验证者需要在协议末尾处理累积的盲化因子,因此无需在协议开始时推导出等价于 $C^{\prime }$ 的对象。

   • $C^{\prime }$ 也是 ${\xi }_0$ 的随机预言机(random oracle)的一个输入;在 Halo 2 中,我们使用的副本(transcript)在采样 $z$ 之前已经对 $C^{\prime }$ 的等价组成部分做出了承诺。

2. ${\text{PC}}_{\text{DL}}.\text{SuccinctCheck}$ 子例程(BCMS20 的图 2)通过加上 $[v]H^{\prime }=[v{\xi }_0]H$ 来计算初始群元素 $C_0$,这需要两次标量乘法。我们改为从原始承诺 $P$ 中减去 $[v]G_0$,从而实际上将多项式在该点打开到值零。计算 $[v]G_0$ 在递归(recursion)语境下更高效,因为 $G_0$ 是一个固定基(fixed base)(所以我们可以使用查找表)。

译自 halo2 book:https://zcash.github.io/halo2/design/protocol.html

协议描述(Protocol Description)

预备知识

我们取 $\lambda$ 作为安全参数(security parameter),除非另有明确说明,所有算法和敌手(adversary)都是在该安全参数下以多项式时间运行的概率性(交互式)图灵机。我们用 $\text{negl}(\lambda )$ 表示一个在 $\lambda$ 上可忽略(negligible)的函数。

密码学群(Cryptographic Groups)

我们令 $\mathbb{G}$ 表示一个素数阶 $p$ 的循环群。群的单位元写作 $\mathcal{O}$。我们把 $\mathbb{G}$ 中元素的标量(scalar)称为大小为 $p$ 的标量域(scalar field)$\mathbb{F}$ 中的元素。群元素用大写字母书写,标量用小写字母或希腊字母书写。标量向量或群元素向量用粗体书写,即 $\mathbf{a}\in {\mathbb{F}}^n$ 和 $\mathbf{G}\in {\mathbb{G}}^n$。群运算以加法形式书写,群元素 $G$ 乘以标量 $a$ 写作 $[a]G$。

我们经常用记号 $⟨\mathbf{a},\mathbf{b}⟩$ 来表示两个等长标量向量 $\mathbf{a},\mathbf{b}\in {\mathbb{F}}^n$ 的内积(inner product)。我们也用这个记号来表示群元素的线性组合,例如 $⟨\mathbf{a},\mathbf{G}⟩$,其中 $\mathbf{a}\in {\mathbb{F}}^n,\mathbf{G}\in {\mathbb{G}}^n$,在实践中通过多标量乘法(multiscalar multiplication)来计算。

我们用 $0^n$ 表示一个长度为 $n$、仅包含 $\mathbb{F}$ 中零元素的向量。

离散对数关系问题(Discrete Log Relation Problem)。 优势度量(advantage metric) $${\mathsf{Adv}}_{\mathbb{G},n}^{\text{dl-rel}}(\mathcal{A},\lambda )=\text{Pr}\left[{\mathsf{G}}_{\mathbb{G},n}^{\text{dl-rel}}(\mathcal{A},\lambda )\right]$$ 是相对于以下博弈(game)定义的。 $$\begin{array}{ll}& \underline{\mathbf{Game}{\mathsf{G}}_{\mathbb{G},n}^{\text{dl-rel}}(\mathcal{A},\lambda ):}\\ & \mathbf{G}\leftarrow {\mathbb{G}}_{\lambda }^n\\ & \mathbf{a}\leftarrow \mathcal{A}(\mathbf{G})\\ & \text{Return}\left(⟨\mathbf{a},\mathbf{G}⟩=\mathcal{O}\wedge \mathbf{a}\ne 0^n\right)\end{array}$$

给定一个 $n$ 长度的群元素向量 $\mathbf{G}\in {\mathbb{G}}^n$,离散对数关系问题 要求找出 $\mathbf{g}\in {\mathbb{F}}^n$ 使得 $\mathbf{g}\ne 0^n$ 但 $⟨\mathbf{g},\mathbf{G}⟩=\mathcal{O}$,我们称之为一个 非平凡的 离散对数关系。如 [JT20] 的引理 3 所示,该问题的困难性可由群中离散对数问题的困难性紧致地推出。形式上,我们使用上面定义的博弈 ${\mathsf{G}}_{\mathbb{G},n}^{\text{dl-rel}}$ 来刻画该问题。

交互式证明(Interactive Proofs)

交互式证明 是一个三元组算法 $\text{IP}=(\text{Setup},\mathcal{P},\mathcal{V})$。算法 $\text{Setup}(1^{\lambda })$ 输出某些 公共参数(public parameters),通常用 $\mathsf{pp}$ 来指代。证明者 $\mathcal{P}$ 和验证者 $\mathcal{V}$ 是交互式机器(可访问 $\mathsf{pp}$),我们用 $⟨\mathcal{P}(x),\mathcal{V}(y)⟩$ 表示一个在它们之间以输入 $x,y$ 执行两方协议的算法。该协议的输出是它们交互的一个 副本(transcript),包含 $\mathcal{P}$ 与 $\mathcal{V}$ 之间发送的所有消息。在协议结束时,验证者输出一个决策比特。

零知识知识论证(Zero knowledge Arguments of Knowledge)

知识证明(proofs of knowledge)是这样的交互式证明:证明者旨在使验证者相信,对于某个陈述 $x$ 和多项式时间可判定关系 $\mathcal{R}$,他们知道一个证据(witness)$w$ 使得 $(x,w)\in \mathcal{R}$。我们将处理 论证(arguments) 形式的知识证明,它假设证明者在计算上是有界的。

我们将通过四种安全概念来分析知识论证。

• 完备性(Completeness): 如果证明者持有一个有效的证据,他们能 总是 说服验证者吗?理解这一性质很有用,因为它可能会对其他安全概念产生影响。
• 可靠性(Soundness): 一个作弊的证明者能否虚假地使验证者相信一个实际上并不正确的陈述的正确性?我们把作弊证明者能虚假地说服验证者的概率称为 可靠性误差(soundness error)。
• 知识可靠性(Knowledge soundness): 当验证者被说服相信陈述是正确的时,证明者是否确实持有("知道")一个有效的证据?我们把作弊证明者虚假地使验证者相信这种知识的概率称为 知识误差(knowledge error)。
• 零知识(Zero knowledge): 验证者除了能从陈述的正确性以及证明者拥有有效证据这一事实推断出来的内容之外,是否还学到了别的东西?

首先,我们来看完备性的简单定义。

完美完备性(Perfect Completeness)。 一个交互式论证 $(\text{Setup},\mathcal{P},\mathcal{V})$ 具有 完美完备性,如果对于所有多项式时间可判定关系 $\mathcal{R}$ 以及所有非一致(non-uniform)多项式时间敌手 $\mathcal{A}$ $$Pr\left[(x,w)\notin \mathcal{R}\vee ⟨\mathcal{P}(\mathsf{pp},x,w),\mathcal{V}(\mathsf{pp},x)⟩\text{accepts}|\begin{array}{ll}& \mathsf{pp}\leftarrow \text{Setup}(1^{\lambda })\\ & (x,w)\leftarrow \mathcal{A}(\mathsf{pp})\end{array}\right]=1$$