零知识证明 - Halo2电路构建源代码导读

Star Li
更新于 2022-01-18 09:39
阅读 5008

理解Halo2，可以从两部分着手：1/ 电路构建 2/ 证明系统

理解Halo2，可以从两部分着手：1/ 电路构建 2/ 证明系统。从开发者的角度看，电路构建是接口。如何通过Halo2构建建电路，这些电路在Halo2的内部如何表示是理解电路构建的关键。本文就从源代码的角度深入浅出讲解Halo2的电路构建。

## 写在前面

在深入理解Halo2电路或者证明系统之前，请仔细查看Halo2的文档：

https://zcash.github.io/halo2/index.html

对应的中文翻译文档：

https://trapdoor-tech.github.io/halo2-book-chinese/

## 源代码目录结构

Halo2的源代码下载地址：

https://github.com/zcash/halo2.git

本文中采用的源代码的最后一个提交信息如下：

```
commit 658c2db4217b1b19b17ecd29577c0e370e1c4997
Merge: 3850b9c b46ef35
Author: str4d <jack@electriccoin.co>
Date:   Sat Oct 2 01:54:55 2021 +1300

Merge pull request #374 from zcash/trait-usage
    
    Clean up our trait usage
```

Halo2的目录结构如下：

![](https://img.learnblockchain.cn/2022/01/18/111.jpg)

主要逻辑在src目录下。benches是基准测试程序。book是Halo2的描述文档。examples目录下提供了简单电路示例。

## 电路结构

在深入Halo2电路细节之前，先介绍一下Halo2的整体的电路结构。Halo2和PLONK/Groth16的电路结构有一些区别。简单的说，PLONK/Groth16约束系统由一条条相对独立的约束组成（约束只能约束该行上的变量），并且一条约束指定了支持的计算（乘法或者加法组合）。Halo2的约束系统中的约束并不限定在一行上的变量，并且采用“custom gate”，任意指定约束需要的计算。

整体电路结构如下：

![](https://img.learnblockchain.cn/2022/01/18/222.jpg)

电路由列（Column）和行（Row）组成。列又分为三种类型：advice，instance和selector。列的类型定义在src/plonk/circuit.rs中。

```
pub enum Any {  
    Advice,  
    Fixed,  
    Instance,  
}
```

Advice列是witness信息，Instance列是public信息。Selector列，也是Fixed列，是选择子，可以选择某些约束开启或者关闭。为了更好的电路模块化，电路构建往往是相对于一个Region。同一个电路模块，可以在不同的Region中“复制”。

Cell定义在src/circuit.rs：

```
pub struct Cell {  
    region\_index: RegionIndex,  
    row\_offset: usize,  
    column: Column<Any>,  
}
```

Cell指定在一个Region中的某行某列。

## 几个术语

理解Halo2的电路构建，可以从一个简单的例子开始：examples/simple-example.rs。理解这个例子前，需要介绍几个术语。

#### **Chip**

电路由一个个Chip逻辑堆砌而成。每个Chip的创建从“Config”开始。

#### **Config**

所谓的Config，就是申请Chip需要的Column以及配置Fixed列的逻辑含义。这些配置可能是Custom Gate，可能是lookup。

#### **Instructions**

每一个Chip都有指令（Instruction）。通过指令的调用，将Chip的部分或者全部功能加入电路中。

#### **Layouter**

将Chip添加到一个电路上需要布局。Layouter就是用来实现布局。Layouter接口定义在src/circuit.rs中：

```
pub trait Layouter<F: Field> {
    type Root: Layouter<F>;
    
    fn assign_region<A, AR, N, NR>(&mut self, name: N, assignment: A) -> Result<AR, Error>
    where
        A: FnMut(Region<'_, F>) -> Result<AR, Error>,
        N: Fn() -> NR,
        NR: Into<String>;

fn assign_table<A, N, NR>(&mut self, name: N, assignment: A) -> Result<(), Error>
    where
        A: FnMut(Table<'_, F>) -> Result<(), Error>,
        N: Fn() -> NR,
        NR: Into<String>;

fn constrain_instance(
        &mut self,
        cell: Cell,
        column: Column<Instance>,
        row: usize,
    ) -> Result<(), Error>;

fn get_root(&mut self) -> &mut Self::Root;
    fn push_namespace<NR, N>(&mut self, name_fn: N)
    where
        NR: Into<String>,
        N: FnOnce() -> NR;
    fn pop_namespace(&mut self, gadget_name: Option<String>);
    fn namespace<NR, N>(&mut self, name_fn: N) -> NamespacedLayouter<'_, F, Self::Root>
    where
        NR: Into<String>,
        N: FnOnce() -> NR,
    {
        self.get_root().push_namespace(name_fn);

NamespacedLayouter(self.get_root(), PhantomData)
    }
}
```

Layouter本身存在层级关系，所以Layouter的接口定义了`get\_root/push\_namespace/pop\_namespace/namespace`相关的函数。核心逻辑在其他三个函数：

* assign\_region - 获取一个region，在这个region上可以进行各种“assignment”，定义在RegionLayouter接口中。
* assign\_table - 获取一个table，并设置table，接口定义在TableLayouter接口中。
* constrain\_instance - 限制一个Cell和Instance列中的某个Cell一致。

#### **Assignment**

Assignment是一个电路“赋值”的接口，定义在src/plonk/circuit.rs：

```
pub trait Assignment<F: Field> {
    fn enter_region<NR, N>(&mut self, name_fn: N)
    where
        NR: Into<String>,
        N: FnOnce() -> NR;

fn exit_region(&mut self);

fn enable_selector<A, AR>(
        &mut self,
        annotation: A,
        selector: &Selector,
        row: usize,
    ) -> Result<(), Error>
    where
        A: FnOnce() -> AR,
        AR: Into<String>;

fn query_instance(&self, column: Column<Instance>, row: usize) -> Result<Option<F>, Error>;

fn assign_advice<V, VR, A, AR>(
        &mut self,
        annotation: A,
        column: Column<Advice>,
        row: usize,
        to: V,
    ) -> Result<(), Error>
    where
        V: FnOnce() -> Result<VR, Error>,
        VR: Into<Assigned<F>>,
        A: FnOnce() -> AR,
        AR: Into<String>;

fn assign_fixed<V, VR, A, AR>(
        &mut self,
        annotation: A,
        column: Column<Fixed>,
        row: usize,
        to: V,
    ) -> Result<(), Error>
    where
        V: FnOnce() -> Result<VR, Error>,
        VR: Into<Assigned<F>>,
        A: FnOnce() -> AR,
        AR: Into<String>;

fn copy(
        &mut self,
        left_column: Column<Any>,
        left_row: usize,
        right_column: Column<Any>,
        right_row: usize,
    ) -> Result<(), Error>;

fn fill_from_row(
        &mut self,
        column: Column<Fixed>,
        row: usize,
        to: Option<Assigned<F>>,
    ) -> Result<(), Error>;

fn push_namespace<NR, N>(&mut self, name_fn: N)
    where
        NR: Into<String>,
        N: FnOnce() -> NR;

fn pop_namespace(&mut self, gadget_name: Option<String>);
}
```

## 电路内部框架

为了方便简化开发人员开发电路，Halo2的内部框架抽象了布局的接口（以SimpleFloorPlanner为例）：

![](https://img.learnblockchain.cn/2022/01/18/333.jpg)

目前有两套Layouter的实现：1/ SimpleFloorPlanner 2/ V1/V1Plan。为了方便理解Halo2的内部逻辑，详细讲解一下SimpleFloorPlanner。整个框架由四个接口组成：FloorPlanner，Layouter，RegionLayout/TableLayout以及Assignment。

简单的说，一个FloorPlanner拥有一个Layouter，一个Layouter可以分配多个RegionLayout或者TableLayout。电路对Cell的assignment都是通过Assignment实现。

先从三者的整体调用关系讲起：

* SimpleFloorPlanner是对FloorPlanner接口的实现，定义在src/circuit/floor\_planner/single\_pass.rs中：

```
pub struct SimpleFloorPlanner;

impl FloorPlanner for SimpleFloorPlanner {
    fn synthesize<F: Field, CS: Assignment<F>, C: Circuit<F>>(
        cs: &mut CS,
        circuit: &C,
        config: C::Config,
        constants: Vec<Column<Fixed>>,
    ) -> Result<(), Error> {
        let layouter = SingleChipLayouter::new(cs, constants)?;
        circuit.synthesize(config, layouter)
    }
}
```

SimpleFloorPlanner实现了FloorPlanner接口的synthesize函数。容易看出，该函数创建出SingleChipLayouter对象，并直接调用相应的synthesize函数开始电路的synthesize。

* SingleChipLayouter定义在src/circuit/floor\_planner/single\_pass.rs中，包括了电路的所有的信息。

```
pub struct SingleChipLayouter<'a, F: Field, CS: Assignment<F> + 'a> {
    cs: &'a mut CS,
    constants: Vec<Column<Fixed>>,
    /// Stores the starting row for each region.
    regions: Vec<RegionStart>,
    /// Stores the first empty row for each column.
    columns: HashMap<RegionColumn, usize>,
    /// Stores the table fixed columns.
    table_columns: Vec<TableColumn>,
    _marker: PhantomData<F>,
}
```

SingleChipLayouter的Region管理比较简单，某行整体属于某个Region。regions记录每个Region的行的开始偏移。cs是Assignment接口的实现，存储所有电路的赋值信息。columns记录当前操作RegionColumn对应的空的row的偏移。table\_columns记录Table需要的Fixed的Column。简单的说，SingleChipLayouter记录了电路（包括布局）需要的所有信息。

* SingleChipLayouter's assign\_region 函数实现一个Region的synthesize过程。简单的说，SingleChipLayouter的assign\_region函数的主要逻辑就是创建一个region，并将region内的布局转化为全局布局。SingleChipLayouter的assign\_region逻辑可以分成两部分：
  
  1/ 通过RegionShape获取Region的“形状”。所谓的“形状”，包括主要是采用的Column的信息。
  
  2/ 根据上一步获取的Column信息，找出和其他Region不冲突的起始问题。
  
  可以查看代码中的注释理解相应逻辑：

```
fn assign_region<A, AR, N, NR>(&mut self, name: N, mut assignment: A) -> Result<AR, Error>
where
    A: FnMut(Region<'_, F>) -> Result<AR, Error>,
    N: Fn() -> NR,
    NR: Into<String>,
{
    let region_index = self.regions.len(); //获取当前Region的编号

// Get shape of the region. //调用RegionShape的Region接口，收集该Region的电路涉及到的Column信息
    let mut shape = RegionShape::new(region_index.into());
    {
        let region: &mut dyn RegionLayouter<F> = &mut shape;
        assignment(region.into())?;
    }

// Lay out this region. We implement the simplest approach here: position the
    // region starting at the earliest row for which none of the columns are in use.
    let mut region_start = 0; //根据收集到的Column信息，获取Region开始的行号
    for column in &shape.columns {
        region_start = cmp::max(region_start, self.columns.get(column).cloned().unwrap_or(0));
    }
    self.regions.push(region_start.into());

// Update column usage information. //在Region中记录下所有使用的Column的信息
    for column in shape.columns {
        self.columns.insert(column, region_start + shape.row_count);
    }

// Assign region cells.
    self.cs.enter_region(name); //创建Region
    let mut region = SingleChipLayouterRegion::new(self, region_index.into());
    let result = {
        let region: &mut dyn RegionLayouter<F> = &mut region;
        assignment(region.into()) //采用SingleChipLayouterRegion对电路赋值
    }?;
    let constants_to_assign = region.constants;
    self.cs.exit_region(); //退出Region

// Assign constants. For the simple floor planner, we assign constants in order in
    // the first `constants` column.
    if self.constants.is_empty() {//如果制定了constants，需要增加置换限制
        if !constants_to_assign.is_empty() {
            return Err(Error::NotEnoughColumnsForConstants);
        }
    } else {
        let constants_column = self.constants[0];
        let next_constant_row = self
            .columns
            .entry(Column::<Any>::from(constants_column).into())
            .or_default();
        for (constant, advice) in constants_to_assign {
            self.cs.assign_fixed(
                || format!("Constant({:?})", constant.evaluate()),
                constants_column,
                *next_constant_row,
                || Ok(constant),
            )?;
            self.cs.copy(
                constants_column.into(),
                *next_constant_row,
                advice.column,
                *self.regions[*advice.region_index] + advice.row_offset,
            )?;
            *next_constant_row += 1;
        }
    }

Ok(result)
}
```

* SingleChipLayouter's assign\_table 函数当前的电路中增加查找表逻辑：

```
fn assign_table<A, N, NR>(&mut self, name: N, mut assignment: A) -> Result<(), Error>
where
    A: FnMut(Table<'_, F>) -> Result<(), Error>,
    N: Fn() -> NR,
    NR: Into<String>,
{
    // Maintenance hazard: there is near-duplicate code in `v1::AssignmentPass::assign_table`.
    // Assign table cells.
    self.cs.enter_region(name); //创建一个Region
    let mut table = SimpleTableLayouter::new(self.cs, &self.table_columns);
    {
        let table: &mut dyn TableLayouter<F> = &mut table;
        assignment(table.into()) //查找表赋值
    }?;
    let default_and_assigned = table.default_and_assigned;
    self.cs.exit_region(); //退出当前Region

// Check that all table columns have the same length `first_unused`,
    // and all cells up to that length are assigned.
    let first_unused = { //获取出所有查找表相关的Column对应的最大使用行数
        match default_and_assigned
            .values()
            .map(|(_, assigned)| {
                if assigned.iter().all(|b| *b) {
                    Some(assigned.len())
                } else {
                    None
                }
            })
            .reduce(|acc, item| match (acc, item) {
                (Some(a), Some(b)) if a == b => Some(a),
                _ => None,
            }) {
            Some(Some(len)) => len,
            _ => return Err(Error::SynthesisError), // TODO better error
        }
    };

// Record these columns so that we can prevent them from being used again.
    for column in default_and_assigned.keys() {
        self.table_columns.push(*column);
    }
    //根据default_and_assigned信息，采用default值扩展所有的column
    for (col, (default_val, _)) in default_and_assigned {
        // default_val must be Some because we must have assigned
        // at least one cell in each column, and in that case we checked
        // that all cells up to first_unused were assigned.
        self.cs
            .fill_from_row(col.inner(), first_unused, default_val.unwrap())?;
    }

Ok(())
}
```

default\_and\_assigned记录了在一个Fixed Column上的default值以及某个cell是否已经设置。

* SingleChipLayouterRegion实现了Region接口。如果在Region中需要给一个Advice列中Cell赋值，可以采用assign\_advice函数：

```
fn assign_advice<'v>(
    &'v mut self,
    annotation: &'v (dyn Fn() -> String + 'v),
    column: Column<Advice>,
    offset: usize,
    to: &'v mut (dyn FnMut() -> Result<Assigned<F>, Error> + 'v),
) -> Result<Cell, Error> {
    self.layouter.cs.assign_advice( //调用Assignment接口设置相应的Cell信息，特别注意的是在设置的时候需要Cell的全局偏移
        annotation,
        column,
        *self.layouter.regions[*self.region_index] + offset,
        to,
    )?;

Ok(Cell {
        region_index: self.region_index,
        row_offset: offset,
        column: column.into(),
    })
}
```

* cs.assign\_fixed函数，对fixed Column进行赋值。可以参考MockProver的实现，定义在src/dev.rs。

```
fn assign_fixed<V, VR, A, AR>(
    &mut self,
    _: A,
    column: Column<Fixed>,
    row: usize,
    to: V,
) -> Result<(), Error>
where
    V: FnOnce() -> Result<VR, Error>,
    VR: Into<Assigned<F>>,
    A: FnOnce() -> AR,
    AR: Into<String>,
{
    ... //在一些检查后，设置Fixed列中的某个Cell（column，row指定）
    *self
        .fixed
        .get_mut(column.index())
        .and_then(|v| v.get_mut(row))
        .ok_or(Error::BoundsFailure)? = CellValue::Assigned(to()?.into().evaluate());

Ok(())
}
```

* cs.copy函数，增加置换信息。

```
fn copy(
    &mut self,
    left_column: Column<Any>,
    left_row: usize,
    right_column: Column<Any>,
    right_row: usize,
) -> Result<(), crate::plonk::Error> {
    if !self.usable_rows.contains(&left_row) || !self.usable_rows.contains(&right_row) {
        return Err(Error::BoundsFailure);
    }

self.permutation //增加Permutation信息
        .copy(left_column, left_row, right_column, right_row)
}
```

接着我们再详细看看RegionLayouter和TableLayouter。RegionLayouter定义在src/circuit/layouter.rs：

```
pub trait RegionLayouter<F: Field>: fmt::Debug {
    //enable选择子
    fn enable_selector<'v>(
        &'v mut self,
        annotation: &'v (dyn Fn() -> String + 'v),
        selector: &Selector,
        offset: usize,
    ) -> Result<(), Error>;

//advice或者fixed赋值
    fn assign_advice<'v>(
        &'v mut self,
        annotation: &'v (dyn Fn() -> String + 'v),
        column: Column<Advice>,
        offset: usize,
        to: &'v mut (dyn FnMut() -> Result<Assigned<F>, Error> + 'v),
    ) -> Result<Cell, Error>;

fn assign_advice_from_constant<'v>(
        &'v mut self,
        annotation: &'v (dyn Fn() -> String + 'v),
        column: Column<Advice>,
        offset: usize,
        constant: Assigned<F>,
    ) -> Result<Cell, Error>;

fn assign_advice_from_instance<'v>(
        &mut self,
        annotation: &'v (dyn Fn() -> String + 'v),
        instance: Column<Instance>,
        row: usize,
        advice: Column<Advice>,
        offset: usize,
    ) -> Result<(Cell, Option<F>), Error>;

fn assign_fixed<'v>(
        &'v mut self,
        annotation: &'v (dyn Fn() -> String + 'v),
        column: Column<Fixed>,
        offset: usize,
        to: &'v mut (dyn FnMut() -> Result<Assigned<F>, Error> + 'v),
    ) -> Result<Cell, Error>;

//cell相等约束
    fn constrain_constant(&mut self, cell: Cell, constant: Assigned<F>) -> Result<(), Error>;

fn constrain_equal(&mut self, left: Cell, right: Cell) -> Result<(), Error>;
}
```

RegionLayouter的接口很容易理解，包括设置选择子，给cell赋值，约束cell相等。

TableLayouter的接口定义如下：

```
pub trait TableLayouter<F: Field>: fmt::Debug {
    fn assign_cell<'v>(
        &'v mut self,
        annotation: &'v (dyn Fn() -> String + 'v),
        column: TableColumn,
        offset: usize,
        to: &'v mut (dyn FnMut() -> Result<Assigned<F>, Error> + 'v),
    ) -> Result<(), Error>;
}
```

TableLayouter只有一个接口：assign\_cell。assign\_cell是对表中的某个TableColumn的Cell进行赋值。

至此，大体的电路构造的逻辑的框架相对清楚：Halo2中的Chip电路由一个个Region组成，在Halo2的框架中，Region通过Layouter进行分配。电路的所有的信息都存储在Assignment的接口中。MockProver是一个可以参考的Assignment的实现。

## ConstraintSystem

ConstraintSystem描述了电路相关的信息：

```
#[derive(Debug, Clone)]
pub struct ConstraintSystem<F: Field> {
    pub(crate) num_fixed_columns: usize,
    pub(crate) num_advice_columns: usize,
    pub(crate) num_instance_columns: usize,
    pub(crate) num_selectors: usize,
    pub(crate) selector_map: Vec<Column<Fixed>>,
    pub(crate) gates: Vec<Gate<F>>,
    pub(crate) advice_queries: Vec<(Column<Advice>, Rotation)>,
    // Contains an integer for each advice column
    // identifying how many distinct queries it has
    // so far; should be same length as num_advice_columns.
    num_advice_queries: Vec<usize>,
    pub(crate) instance_queries: Vec<(Column<Instance>, Rotation)>,
    pub(crate) fixed_queries: Vec<(Column<Fixed>, Rotation)>,

// Permutation argument for performing equality constraints
    pub(crate) permutation: permutation::Argument,

// Vector of lookup arguments, where each corresponds to a sequence of
    // input expressions and a sequence of table expressions involved in the lookup.
    pub(crate) lookups: Vec<lookup::Argument<F>>,

// Vector of fixed columns, which can be used to store constant values
    // that are copied into advice columns.
    pub(crate) constants: Vec<Column<Fixed>>,

pub(crate) minimum_degree: Option<usize>,
}
```

大部分字段都比较好理解。gates描述了“Custom Gate”的限制表达式：

```
#[derive(Clone, Debug)]
pub(crate) struct Gate<F: Field> {
    name: &'static str,
    constraint_names: Vec<&'static str>,
    polys: Vec<Expression<F>>,
    /// We track queried selectors separately from other cells, so that we can use them to
    /// trigger debug checks on gates.
    queried_selectors: Vec<Selector>,
    queried_cells: Vec<VirtualCell>,
}
```

注意polys中的表达式Expression就是用来表示“Custom Gate”。Halo2的电路构建分为两部分：1/Configure （电路配置）2/ Synthesize（电路综合）。简单的说，Configure就是进行电路本身的配置。Synthesize进行某个电路实例的综合。

## 看看示例

理解了如上的逻辑，来看看Halo2代码提供的简单的示例程序：examples/simple-example.rs

* **Configure过程**
  
  Configure调用ConstraintSystem申请各种列以及Gate的信息。调用某个Circuit的Configure函数会顺序调用电路涉及到的Chip的Configure信息，这些信息都记录在ConstraintSystem中。
  
  查看实例中的Chip的Configure函数：

```
impl<F: FieldExt> Circuit<F> for MyCircuit<F> {
    ...
    fn configure(meta: &mut ConstraintSystem<F>) -> Self::Config {
        let advice = [meta.advice_column(), meta.advice_column()];
        let instance = meta.instance_column();
        let constant = meta.fixed_column();

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

impl<F: FieldExt> 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.into());
        meta.enable_constant(constant);
        for column in &advice {
            meta.enable_equality((*column).into());
        }
        let s_mul = meta.selector();

meta.create_gate("mul", |meta| {
            // | a0  | a1  | s_mul |
            // |-----|-----|-------|
            // | lhs | rhs | s_mul |
            // | out |     |       |
            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);

vec![s_mul * (lhs * rhs - out)]
        });

FieldConfig {
            advice,
            instance,
            s_mul,
            constant,
        }
    }
}
```

示例电路申请了两个advice列，一个instance和fixed列。同时电路构造了一个乘法Gate：

```
vec![s_mul * (lhs * rhs - out)]
```

该乘法Gate就是相应的限制表达式。注意和其他零知识证明的约束系统不一样的是，一个约束可以采用多个行上的Cell。整个调用关系如下：

![](https://img.learnblockchain.cn/2022/01/18/4.jpg)

* **Synthesize过程**
  
  ```
  在Configure完电路后，可以调用synthesize综合某个电路实例。整个调用关系如下：
  ```

![](https://img.learnblockchain.cn/2022/01/18/5.jpg)

```
某个Chip调用Layouter分配Region，并在Region中指定约束。可以查看FieldChip的mul函数：
```

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

let mut out = None;
        layouter.assign_region(
            || "mul",
            |mut region: Region<'_, F>| {
                config.s_mul.enable(&mut region, 0)?; //获取到一个Region后，enable该row对应的乘法selector。

let lhs = region.assign_advice( //对两个advice进行赋值
                    || "lhs",
                    config.advice[0],
                    0,
                    || a.value.ok_or(Error::SynthesisError),
                )?;
                let rhs = region.assign_advice(
                    || "rhs",
                    config.advice[1],
                    0,
                    || b.value.ok_or(Error::SynthesisError),
                )?;
                region.constrain_equal(a.cell, lhs)?; //限制两个advice和之前的load的Cell一致
                region.constrain_equal(b.cell, rhs)?;

// Now we can assign the multiplication result into the output position.
                let value = a.value.and_then(|a| b.value.map(|b| a * b));
                let cell = region.assign_advice( //对乘法的输出进行赋值
                    || "lhs * rhs",
                    config.advice[0],
                    1,
                    || value.ok_or(Error::SynthesisError),
                )?;

// Finally, we return a variable representing the output,
                // to be used in another part of the circuit.
                out = Some(Number { cell, value });
                Ok(())
            },
        )?;

Ok(out.unwrap())
    }
    ...
}
```

## **总结：**

理解Halo2，可以从两部分着手：1/ 电路构建 2/ 证明系统。从开发者的角度看，电路构建是接口。如何通过Halo2创建电路，这些电路在Halo2的内部如何表示是理解电路构建的关键。Halo2中的Chip电路由一个个Region组成，在Halo2的框架中，Region通过Layouter进行分配。电路的所有的信息都存储在Assignment的接口中。Halo2的电路构建分为两部分：1/Configure （电路配置）2/ Synthesize（电路综合）。简单的说，Configure就是进行电路本身的配置。Synthesize进行某个电路实例的综合。

![](https://img.learnblockchain.cn/2021/08/11/16286676542313.jpg)

写在前面

在深入理解Halo2电路或者证明系统之前，请仔细查看Halo2的文档：

https://zcash.github.io/halo2/index.html

对应的中文翻译文档：

https://trapdoor-tech.github.io/halo2-book-chinese/

源代码目录结构

Halo2的源代码下载地址：

https://github.com/zcash/halo2.git

本文中采用的源代码的最后一个提交信息如下：

commit 658c2db4217b1b19b17ecd29577c0e370e1c4997
Merge: 3850b9c b46ef35
Author: str4d &lt;jack@electriccoin.co>
Date:   Sat Oct 2 01:54:55 2021 +1300

    Merge pull request #374 from zcash/trait-usage

    Clean up our trait usage

Halo2的目录结构如下：

主要逻辑在src目录下。benches是基准测试程序。book是Halo2的描述文档。examples目录下提供了简单电路示例。

电路结构

整体电路结构如下：

电路由列（Column）和行（Row）组成。列又分为三种类型：advice，instance和selector。列的类型定义在src/plonk/circuit.rs中。

pub enum Any {  
    Advice,  
    Fixed,  
    Instance,  
}

Cell定义在src/circuit.rs：

pub struct Cell {  
    region\_index: RegionIndex,  
    row\_offset: usize,  
    column: Column&lt;Any>,  
}

Cell指定在一个Region中的某行某列。

几个术语

理解Halo2的电路构建，可以从一个简单的例子开始：examples/simple-example.rs。理解这个例子前，需要介绍几个术语。

Chip

电路由一个个Chip逻辑堆砌而成。每个Chip的创建从“Config”开始。

Config

所谓的Config，就是申请Chip需要的Column以及配置Fixed列的逻辑含义。这些配置可能是Custom Gate，可能是lookup。

Instructions

每一个Chip都有指令（Instruction）。通过指令的调用，将Chip的部分或者全部功能加入电路中。

Layouter

将Chip添加到一个电路上需要布局。Layouter就是用来实现布局。Layouter接口定义在src/circuit.rs中：

pub trait Layouter&lt;F: Field> {
    type Root: Layouter&lt;F>;

    fn assign_region&lt;A, AR, N, NR>(&mut self, name: N, assignment: A) -> Result&lt;AR, Error>
    where
        A: FnMut(Region&lt;'_, F>) -> Result&lt;AR, Error>,
        N: Fn() -> NR,
        NR: Into&lt;String>;

    fn assign_table&lt;A, N, NR>(&mut self, name: N, assignment: A) -> Result&lt;(), Error>
    where
        A: FnMut(Table&lt;'_, F>) -> Result&lt;(), Error>,
        N: Fn() -> NR,
        NR: Into&lt;String>;

    fn constrain_instance(
        &mut self,
        cell: Cell,
        column: Column&lt;Instance>,
        row: usize,
    ) -> Result&lt;(), Error>;

    fn get_root(&mut self) -> &mut Self::Root;
    fn push_namespace&lt;NR, N>(&mut self, name_fn: N)
    where
        NR: Into&lt;String>,
        N: FnOnce() -> NR;
    fn pop_namespace(&mut self, gadget_name: Option&lt;String>);
    fn namespace&lt;NR, N>(&mut self, name_fn: N) -> NamespacedLayouter&lt;'_, F, Self::Root>
    where
        NR: Into&lt;String>,
        N: FnOnce() -> NR,
    {
        self.get_root().push_namespace(name_fn);

        NamespacedLayouter(self.get_root(), PhantomData)
    }
}

Layouter本身存在层级关系，所以Layouter的接口定义了get\_root/push\_namespace/pop\_namespace/namespace相关的函数。核心逻辑在其他三个函数：

assign_region - 获取一个region，在这个region上可以进行各种“assignment”，定义在RegionLayouter接口中。
assign_table - 获取一个table，并设置table，接口定义在TableLayouter接口中。
constrain_instance - 限制一个Cell和Instance列中的某个Cell一致。

Assignment

Assignment是一个电路“赋值”的接口，定义在src/plonk/circuit.rs：

pub trait Assignment&lt;F: Field> {
    fn enter_region&lt;NR, N>(&mut self, name_fn: N)
    where
        NR: Into&lt;String>,
        N: FnOnce() -> NR;

    fn exit_region(&mut self);

    fn enable_selector&lt;A, AR>(
        &mut self,
        annotation: A,
        selector: &Selector,
        row: usize,
    ) -> Result&lt;(), Error>
    where
        A: FnOnce() -> AR,
        AR: Into&lt;String>;

    fn query_instance(&self, column: Column&lt;Instance>, row: usize) -> Result&lt;Option&lt;F>, Error>;

    fn assign_advice&lt;V, VR, A, AR>(
        &mut self,
        annotation: A,
        column: Column&lt;Advice>,
        row: usize,
        to: V,
    ) -> Result&lt;(), Error>
    where
        V: FnOnce() -> Result&lt;VR, Error>,
        VR: Into&lt;Assigned&lt;F>>,
        A: FnOnce() -> AR,
        AR: Into&lt;String>;

    fn assign_fixed&lt;V, VR, A, AR>(
        &mut self,
        annotation: A,
        column: Column&lt;Fixed>,
        row: usize,
        to: V,
    ) -> Result&lt;(), Error>
    where
        V: FnOnce() -> Result&lt;VR, Error>,
        VR: Into&lt;Assigned&lt;F>>,
        A: FnOnce() -> AR,
        AR: Into&lt;String>;

    fn copy(
        &mut self,
        left_column: Column&lt;Any>,
        left_row: usize,
        right_column: Column&lt;Any>,
        right_row: usize,
    ) -> Result&lt;(), Error>;

    fn fill_from_row(
        &mut self,
        column: Column&lt;Fixed>,
        row: usize,
        to: Option&lt;Assigned&lt;F>>,
    ) -> Result&lt;(), Error>;

    fn push_namespace&lt;NR, N>(&mut self, name_fn: N)
    where
        NR: Into&lt;String>,
        N: FnOnce() -> NR;

    fn pop_namespace(&mut self, gadget_name: Option&lt;String>);
}

电路内部框架

为了方便简化开发人员开发电路，Halo2的内部框架抽象了布局的接口（以SimpleFloorPlanner为例）：

简单的说，一个FloorPlanner拥有一个Layouter，一个Layouter可以分配多个RegionLayout或者TableLayout。电路对Cell的assignment都是通过Assignment实现。

先从三者的整体调用关系讲起：

SimpleFloorPlanner是对FloorPlanner接口的实现，定义在src/circuit/floor_planner/single_pass.rs中：

pub struct SimpleFloorPlanner;

impl FloorPlanner for SimpleFloorPlanner {
    fn synthesize&lt;F: Field, CS: Assignment&lt;F>, C: Circuit&lt;F>>(
        cs: &mut CS,
        circuit: &C,
        config: C::Config,
        constants: Vec&lt;Column&lt;Fixed>>,
    ) -> Result&lt;(), Error> {
        let layouter = SingleChipLayouter::new(cs, constants)?;
        circuit.synthesize(config, layouter)
    }
}

SimpleFloorPlanner实现了FloorPlanner接口的synthesize函数。容易看出，该函数创建出SingleChipLayouter对象，并直接调用相应的synthesize函数开始电路的synthesize。

SingleChipLayouter定义在src/circuit/floor_planner/single_pass.rs中，包括了电路的所有的信息。

pub struct SingleChipLayouter&lt;'a, F: Field, CS: Assignment&lt;F> + 'a> {
    cs: &'a mut CS,
    constants: Vec&lt;Column&lt;Fixed>>,
    /// Stores the starting row for each region.
    regions: Vec&lt;RegionStart>,
    /// Stores the first empty row for each column.
    columns: HashMap&lt;RegionColumn, usize>,
    /// Stores the table fixed columns.
    table_columns: Vec&lt;TableColumn>,
    _marker: PhantomData&lt;F>,
}

SingleChipLayouter的Region管理比较简单，某行整体属于某个Region。regions记录每个Region的行的开始偏移。cs是Assignment接口的实现，存储所有电路的赋值信息。columns记录当前操作RegionColumn对应的空的row的偏移。table_columns记录Table需要的Fixed的Column。简单的说，SingleChipLayouter记录了电路（包括布局）需要的所有信息。

SingleChipLayouter's assign_region 函数实现一个Region的synthesize过程。简单的说，SingleChipLayouter的assign_region函数的主要逻辑就是创建一个region，并将region内的布局转化为全局布局。SingleChipLayouter的assign_region逻辑可以分成两部分：

1/ 通过RegionShape获取Region的“形状”。所谓的“形状”，包括主要是采用的Column的信息。

2/ 根据上一步获取的Column信息，找出和其他Region不冲突的起始问题。

可以查看代码中的注释理解相应逻辑：

fn assign_region&lt;A, AR, N, NR>(&mut self, name: N, mut assignment: A) -> Result&lt;AR, Error>
where
    A: FnMut(Region&lt;'_, F>) -> Result&lt;AR, Error>,
    N: Fn() -> NR,
    NR: Into&lt;String>,
{
    let region_index = self.regions.len(); //获取当前Region的编号

    // Get shape of the region. //调用RegionShape的Region接口，收集该Region的电路涉及到的Column信息
    let mut shape = RegionShape::new(region_index.into());
    {
        let region: &mut dyn RegionLayouter&lt;F> = &mut shape;
        assignment(region.into())?;
    }

    // Lay out this region. We implement the simplest approach here: position the
    // region starting at the earliest row for which none of the columns are in use.
    let mut region_start = 0; //根据收集到的Column信息，获取Region开始的行号
    for column in &shape.columns {
        region_start = cmp::max(region_start, self.columns.get(column).cloned().unwrap_or(0));
    }
    self.regions.push(region_start.into());

    // Update column usage information. //在Region中记录下所有使用的Column的信息
    for column in shape.columns {
        self.columns.insert(column, region_start + shape.row_count);
    }

    // Assign region cells.
    self.cs.enter_region(name); //创建Region
    let mut region = SingleChipLayouterRegion::new(self, region_index.into());
    let result = {
        let region: &mut dyn RegionLayouter&lt;F> = &mut region;
        assignment(region.into()) //采用SingleChipLayouterRegion对电路赋值
    }?;
    let constants_to_assign = region.constants;
    self.cs.exit_region(); //退出Region

    // Assign constants. For the simple floor planner, we assign constants in order in
    // the first `constants` column.
    if self.constants.is_empty() {//如果制定了constants，需要增加置换限制
        if !constants_to_assign.is_empty() {
            return Err(Error::NotEnoughColumnsForConstants);
        }
    } else {
        let constants_column = self.constants[0];
        let next_constant_row = self
            .columns
            .entry(Column::&lt;Any>::from(constants_column).into())
            .or_default();
        for (constant, advice) in constants_to_assign {
            self.cs.assign_fixed(
                || format!("Constant({:?})", constant.evaluate()),
                constants_column,
                *next_constant_row,
                || Ok(constant),
            )?;
            self.cs.copy(
                constants_column.into(),
                *next_constant_row,
                advice.column,
                *self.regions[*advice.region_index] + advice.row_offset,
            )?;
            *next_constant_row += 1;
        }
    }

    Ok(result)
}

SingleChipLayouter's assign_table 函数当前的电路中增加查找表逻辑：

fn assign_table&lt;A, N, NR>(&mut self, name: N, mut assignment: A) -> Result&lt;(), Error>
where
    A: FnMut(Table&lt;'_, F>) -> Result&lt;(), Error>,
    N: Fn() -> NR,
    NR: Into&lt;String>,
{
    // Maintenance hazard: there is near-duplicate code in `v1::AssignmentPass::assign_table`.
    // Assign table cells.
    self.cs.enter_region(name); //创建一个Region
    let mut table = SimpleTableLayouter::new(self.cs, &self.table_columns);
    {
        let table: &mut dyn TableLayouter&lt;F> = &mut table;
        assignment(table.into()) //查找表赋值
    }?;
    let default_and_assigned = table.default_and_assigned;
    self.cs.exit_region(); //退出当前Region

    // Check that all table columns have the same length `first_unused`,
    // and all cells up to that length are assigned.
    let first_unused = { //获取出所有查找表相关的Column对应的最大使用行数
        match default_and_assigned
            .values()
            .map(|(_, assigned)| {
                if assigned.iter().all(|b| *b) {
                    Some(assigned.len())
                } else {
                    None
                }
            })
            .reduce(|acc, item| match (acc, item) {
                (Some(a), Some(b)) if a == b => Some(a),
                _ => None,
            }) {
            Some(Some(len)) => len,
            _ => return Err(Error::SynthesisError), // TODO better error
        }
    };

    // Record these columns so that we can prevent them from being used again.
    for column in default_and_assigned.keys() {
        self.table_columns.push(*column);
    }
    //根据default_and_assigned信息，采用default值扩展所有的column
    for (col, (default_val, _)) in default_and_assigned {
        // default_val must be Some because we must have assigned
        // at least one cell in each column, and in that case we checked
        // that all cells up to first_unused were assigned.
        self.cs
            .fill_from_row(col.inner(), first_unused, default_val.unwrap())?;
    }

    Ok(())
}

default_and_assigned记录了在一个Fixed Column上的default值以及某个cell是否已经设置。

SingleChipLayouterRegion实现了Region接口。如果在Region中需要给一个Advice列中Cell赋值，可以采用assign_advice函数：

fn assign_advice&lt;'v>(
    &'v mut self,
    annotation: &'v (dyn Fn() -> String + 'v),
    column: Column&lt;Advice>,
    offset: usize,
    to: &'v mut (dyn FnMut() -> Result&lt;Assigned&lt;F>, Error> + 'v),
) -> Result&lt;Cell, Error> {
    self.layouter.cs.assign_advice( //调用Assignment接口设置相应的Cell信息，特别注意的是在设置的时候需要Cell的全局偏移
        annotation,
        column,
        *self.layouter.regions[*self.region_index] + offset,
        to,
    )?;

    Ok(Cell {
        region_index: self.region_index,
        row_offset: offset,
        column: column.into(),
    })
}

cs.assign_fixed函数，对fixed Column进行赋值。可以参考MockProver的实现，定义在src/dev.rs。

fn assign_fixed&lt;V, VR, A, AR>(
    &mut self,
    _: A,
    column: Column&lt;Fixed>,
    row: usize,
    to: V,
) -> Result&lt;(), Error>
where
    V: FnOnce() -> Result&lt;VR, Error>,
    VR: Into&lt;Assigned&lt;F>>,
    A: FnOnce() -> AR,
    AR: Into&lt;String>,
{
    ... //在一些检查后，设置Fixed列中的某个Cell（column，row指定）
    *self
        .fixed
        .get_mut(column.index())
        .and_then(|v| v.get_mut(row))
        .ok_or(Error::BoundsFailure)? = CellValue::Assigned(to()?.into().evaluate());

    Ok(())
}

cs.copy函数，增加置换信息。

fn copy(
    &mut self,
    left_column: Column&lt;Any>,
    left_row: usize,
    right_column: Column&lt;Any>,
    right_row: usize,
) -> Result&lt;(), crate::plonk::Error> {
    if !self.usable_rows.contains(&left_row) || !self.usable_rows.contains(&right_row) {
        return Err(Error::BoundsFailure);
    }

    self.permutation //增加Permutation信息
        .copy(left_column, left_row, right_column, right_row)
}

接着我们再详细看看RegionLayouter和TableLayouter。RegionLayouter定义在src/circuit/layouter.rs：

pub trait RegionLayouter&lt;F: Field>: fmt::Debug {
    //enable选择子
    fn enable_selector&lt;'v>(
        &'v mut self,
        annotation: &'v (dyn Fn() -> String + 'v),
        selector: &Selector,
        offset: usize,
    ) -> Result&lt;(), Error>;

    //advice或者fixed赋值
    fn assign_advice&lt;'v>(
        &'v mut self,
        annotation: &'v (dyn Fn() -> String + 'v),
        column: Column&lt;Advice>,
        offset: usize,
        to: &'v mut (dyn FnMut() -> Result&lt;Assigned&lt;F>, Error> + 'v),
    ) -> Result&lt;Cell, Error>;

    fn assign_advice_from_constant&lt;'v>(
        &'v mut self,
        annotation: &'v (dyn Fn() -> String + 'v),
        column: Column&lt;Advice>,
        offset: usize,
        constant: Assigned&lt;F>,
    ) -> Result&lt;Cell, Error>;

    fn assign_advice_from_instance&lt;'v>(
        &mut self,
        annotation: &'v (dyn Fn() -> String + 'v),
        instance: Column&lt;Instance>,
        row: usize,
        advice: Column&lt;Advice>,
        offset: usize,
    ) -> Result&lt;(Cell, Option&lt;F>), Error>;

    fn assign_fixed&lt;'v>(
        &'v mut self,
        annotation: &'v (dyn Fn() -> String + 'v),
        column: Column&lt;Fixed>,
        offset: usize,
        to: &'v mut (dyn FnMut() -> Result&lt;Assigned&lt;F>, Error> + 'v),
    ) -> Result&lt;Cell, Error>;

    //cell相等约束
    fn constrain_constant(&mut self, cell: Cell, constant: Assigned&lt;F>) -> Result&lt;(), Error>;

    fn constrain_equal(&mut self, left: Cell, right: Cell) -> Result&lt;(), Error>;
}

RegionLayouter的接口很容易理解，包括设置选择子，给cell赋值，约束cell相等。

TableLayouter的接口定义如下：

pub trait TableLayouter&lt;F: Field>: fmt::Debug {
    fn assign_cell&lt;'v>(
        &'v mut self,
        annotation: &'v (dyn Fn() -> String + 'v),
        column: TableColumn,
        offset: usize,
        to: &'v mut (dyn FnMut() -> Result&lt;Assigned&lt;F>, Error> + 'v),
    ) -> Result&lt;(), Error>;
}

TableLayouter只有一个接口：assign_cell。assign_cell是对表中的某个TableColumn的Cell进行赋值。

ConstraintSystem

ConstraintSystem描述了电路相关的信息：

#[derive(Debug, Clone)]
pub struct ConstraintSystem&lt;F: Field> {
    pub(crate) num_fixed_columns: usize,
    pub(crate) num_advice_columns: usize,
    pub(crate) num_instance_columns: usize,
    pub(crate) num_selectors: usize,
    pub(crate) selector_map: Vec&lt;Column&lt;Fixed>>,
    pub(crate) gates: Vec&lt;Gate&lt;F>>,
    pub(crate) advice_queries: Vec&lt;(Column&lt;Advice>, Rotation)>,
    // Contains an integer for each advice column
    // identifying how many distinct queries it has
    // so far; should be same length as num_advice_columns.
    num_advice_queries: Vec&lt;usize>,
    pub(crate) instance_queries: Vec&lt;(Column&lt;Instance>, Rotation)>,
    pub(crate) fixed_queries: Vec&lt;(Column&lt;Fixed>, Rotation)>,

    // Permutation argument for performing equality constraints
    pub(crate) permutation: permutation::Argument,

    // Vector of lookup arguments, where each corresponds to a sequence of
    // input expressions and a sequence of table expressions involved in the lookup.
    pub(crate) lookups: Vec&lt;lookup::Argument&lt;F>>,

    // Vector of fixed columns, which can be used to store constant values
    // that are copied into advice columns.
    pub(crate) constants: Vec&lt;Column&lt;Fixed>>,

    pub(crate) minimum_degree: Option&lt;usize>,
}

大部分字段都比较好理解。gates描述了“Custom Gate”的限制表达式：

#[derive(Clone, Debug)]
pub(crate) struct Gate&lt;F: Field> {
    name: &'static str,
    constraint_names: Vec&lt;&'static str>,
    polys: Vec&lt;Expression&lt;F>>,
    /// We track queried selectors separately from other cells, so that we can use them to
    /// trigger debug checks on gates.
    queried_selectors: Vec&lt;Selector>,
    queried_cells: Vec&lt;VirtualCell>,
}

看看示例

理解了如上的逻辑，来看看Halo2代码提供的简单的示例程序：examples/simple-example.rs

Configure过程

Configure调用ConstraintSystem申请各种列以及Gate的信息。调用某个Circuit的Configure函数会顺序调用电路涉及到的Chip的Configure信息，这些信息都记录在ConstraintSystem中。

查看实例中的Chip的Configure函数：

impl&lt;F: FieldExt> Circuit&lt;F> for MyCircuit&lt;F> {
    ...
    fn configure(meta: &mut ConstraintSystem&lt;F>) -> Self::Config {
        let advice = [meta.advice_column(), meta.advice_column()];
        let instance = meta.instance_column();
        let constant = meta.fixed_column();

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

impl&lt;F: FieldExt> FieldChip&lt;F> {
    fn construct(config: &lt;Self as Chip&lt;F>>::Config) -> Self {
        Self {
            config,
            _marker: PhantomData,
        }
    }

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

        meta.create_gate("mul", |meta| {
            // | a0  | a1  | s_mul |
            // |-----|-----|-------|
            // | lhs | rhs | s_mul |
            // | out |     |       |
            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);

            vec![s_mul * (lhs * rhs - out)]
        });

        FieldConfig {
            advice,
            instance,
            s_mul,
            constant,
        }
    }
}

示例电路申请了两个advice列，一个instance和fixed列。同时电路构造了一个乘法Gate：

vec![s_mul * (lhs * rhs - out)]

该乘法Gate就是相应的限制表达式。注意和其他零知识证明的约束系统不一样的是，一个约束可以采用多个行上的Cell。整个调用关系如下：

Synthesize过程

在Configure完电路后，可以调用synthesize综合某个电路实例。整个调用关系如下：

某个Chip调用Layouter分配Region，并在Region中指定约束。可以查看FieldChip的mul函数：

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

        let mut out = None;
        layouter.assign_region(
            || "mul",
            |mut region: Region&lt;'_, F>| {
                config.s_mul.enable(&mut region, 0)?; //获取到一个Region后，enable该row对应的乘法selector。

                let lhs = region.assign_advice( //对两个advice进行赋值
                    || "lhs",
                    config.advice[0],
                    0,
                    || a.value.ok_or(Error::SynthesisError),
                )?;
                let rhs = region.assign_advice(
                    || "rhs",
                    config.advice[1],
                    0,
                    || b.value.ok_or(Error::SynthesisError),
                )?;
                region.constrain_equal(a.cell, lhs)?; //限制两个advice和之前的load的Cell一致
                region.constrain_equal(b.cell, rhs)?;

                // Now we can assign the multiplication result into the output position.
                let value = a.value.and_then(|a| b.value.map(|b| a * b));
                let cell = region.assign_advice( //对乘法的输出进行赋值
                    || "lhs * rhs",
                    config.advice[0],
                    1,
                    || value.ok_or(Error::SynthesisError),
                )?;

                // Finally, we return a variable representing the output,
                // to be used in another part of the circuit.
                out = Some(Number { cell, value });
                Ok(())
            },
        )?;

        Ok(out.unwrap())
    }
    ...
}