美文网首页
Halo2 源码分析

Halo2 源码分析

作者: 雪落无留痕 | 来源:发表于2022-01-21 19:15 被阅读0次

本文主要对 simple-example示例中的代码流程分析。

Circuit

先从一个简单的电路开始:

    // 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: Some(a),
        b: Some(b),
    };

其中 a, b隐私输入, constant 为常量, c 为公开输入。

MyCircuit 主要实现 Circuit接口:

/// This is a trait that circuits provide implementations for so that the
/// backend prover can ask the circuit to synthesize using some given
/// [`ConstraintSystem`] implementation.
pub trait Circuit<F: Field> {
    /// This is a configuration object that stores things like columns.
    type Config: Clone;   
    /// The floor planner used for this circuit. This is an associated type of the
    /// `Circuit` trait because its behaviour is circuit-critical.
    type FloorPlanner: FloorPlanner;    

    /// Returns a copy of this circuit with no witness values (i.e. all witnesses set to
    /// `None`). For most circuits, this will be equal to `Self::default()`.
    fn without_witnesses(&self) -> Self;

    /// The circuit is given an opportunity to describe the exact gate
    /// arrangement, column arrangement, etc.
    fn configure(meta: &mut ConstraintSystem<F>) -> Self::Config;

    /// Given the provided `cs`, synthesize the circuit. The concrete type of
    /// the caller will be different depending on the context, and they may or
    /// may not expect to have a witness present.
    fn synthesize(&self, config: Self::Config, layouter: impl Layouter<F>) -> Result<(), Error>;
}
  • Config 主要实现电路列的配置,MyCircuitconfig 类型为 FieldCofig, 其定义为:
/// 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,
}

其配置包含了两个Advice 列,一个Instance 例,一个Selector 列。

  • FloorPlanner 主要实现电路的综合synthesize, 其具体类型为: SimpleFloorPlanner,实现如下:
/// A simple [`FloorPlanner`] that performs minimal optimizations.
///
/// This floor planner is suitable for debugging circuits. It aims to reflect the circuit
/// "business logic" in the circuit layout as closely as possible. It uses a single-pass
/// layouter that does not reorder regions for optimal packing.
#[derive(Debug)]
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)
    }
}
  • configure 实现电路列和门电路的配置;
  • synthesize 实现电路约束系统的合成,也是电路中最关键的部署,后面具体分析。

ConstraintSystem

ConstraintSystem 主要描述电路的环境,包含门电路,列和置换等。

/// This is a description of the circuit environment, such as the gate, column and
/// permutation arrangements.
#[derive(Debug, Clone)]
pub struct ConstraintSystem<F: Field> {
    pub(crate) num_fixed_columns: usize,      // fixed 列的个数
    pub(crate) num_advice_columns: usize,     // advice 列的个数
    pub(crate) num_instance_columns: usize,   // instance 列的个数
    pub(crate) num_selectors: usize,              // selector个数  
    pub(crate) selector_map: Vec<Column<Fixed>>,
    pub(crate) gates: Vec<Gate<F>>,             // custom门电路     
    pub(crate) advice_queries: Vec<(Column<Advice>, Rotation)>,  //记录Advice 列的查询 
    // 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>,                         // 各个advice列查询的次数
    pub(crate) instance_queries: Vec<(Column<Instance>, Rotation)>,   // 记录instance 列的查询
    pub(crate) fixed_queries: Vec<(Column<Fixed>, Rotation)>,  // 记录 fixed 列的查询 

    // 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>,    // 最小的次数
}

Configure

通过configure 配置 ConstraintSystem, 生成2个advice列,1个instance列,1个常量列。

   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)
    }

再生成FieldConfig

    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,
        }
    }

上述配置中创建了一个mul 定制门,结构如下,a0a1为advice 列,s_mul为 selector 列:

        // | a0  | a1  | s_mul |
        // |-----|-----|-------|
        // | lhs | rhs | s_mul |
        // | out |     |       |

selector 用于确定定制门电路是否在当前行生效。

生成的约束门电路:

#[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>,   // 需要查询的selector
    queried_cells: Vec<VirtualCell>,    // 需要查询的Cell
}

VirtualCell 记录所用到的列,及相对位置。

#[derive(Clone, Debug)]
pub(crate) struct VirtualCell {
    pub(crate) column: Column<Any>,
    pub(crate) rotation: Rotation,
}

MockProver

约束系统最终的赋值保存在MockProver中,其结构如下:

#[derive(Debug)]
pub struct MockProver<F: Group + Field> {
    k: u32,
    n: u32,
    cs: ConstraintSystem<F>,     // 约束系统

    /// The regions in the circuit.
    regions: Vec<Region>,              // 包含的区域(Region)
    /// The current region being assigned to. Will be `None` after the circuit has been
    /// synthesized.
    current_region: Option<Region>,       // 当前所处的区域

    // The fixed cells in the circuit, arranged as [column][row].
    fixed: Vec<Vec<CellValue<F>>>,           // fixed 列赋值,每个向量代表一列
    // The advice cells in the circuit, arranged as [column][row].
    advice: Vec<Vec<CellValue<F>>>,          // advice 列赋值,每个向量代表一列
    // The instance cells in the circuit, arranged as [column][row].
    instance: Vec<Vec<F>>,                   // instance 列的赋值

    selectors: Vec<Vec<bool>>,              // selectors 列的赋值

    permutation: permutation::keygen::Assembly,   // 保存置换的相关信息

    // A range of available rows for assignment and copies.
    usable_rows: Range<usize>,                //可使用的行的范围
}

其中区域的定义如下:

#[derive(Debug)]
struct Region {
    /// The name of the region. Not required to be unique.
    name: String,                        // 区域的名字
    /// The columns involved in this region.
    columns: HashSet<Column<Any>>,      // 该区域所涉及的列
    /// The rows that this region starts and ends on, if known.
    rows: Option<(usize, usize)>,        //该区域行的起始位置(包含起始位置)      
    /// The selectors that have been enabled in this region. All other selectors are by
    /// construction not enabled.
    enabled_selectors: HashMap<Selector, Vec<usize>>,  // 该区域的Selector, 向量保存对应的行位置
    /// The cells assigned in this region. We store this as a `Vec` so that if any cells
    /// are double-assigned, they will be visibly darker.
    cells: Vec<(Column<Any>, usize)>,        // 该区域所汲的所有Cell位置,记录列和对应的行
}

其中置换的结构如:

#[derive(Debug)]
pub(crate) struct Assembly {
    columns: Vec<Column<Any>>,    // 参与置换的列
    pub(crate) mapping: Vec<Vec<(usize, usize)>>,  //二维矩阵,保存置换的映射关系
    aux: Vec<Vec<(usize, usize)>>,        // 二维矩阵,保存每个映射的特征值
    sizes: Vec<Vec<usize>>,               // 在特征值位置,保存一个置换关系的大小
}

Synthesize

电路的合成通过FloorPlannersynthesize 函数,最终调用电路的synthesize 函数:

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)
    }
}

SingleChipLayouter 的结构为:

/// A [`Layouter`] for a single-chip circuit.
pub struct SingleChipLayouter<'a, F: Field, CS: Assignment<F> + 'a> {
    cs: &'a mut CS,    // 实现Assignment特征,保存电路的相关赋值 
    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>,
}

synthesize 主要实现电路区域的布局,以下面的实现中,首先载入两个变量ab 的值,然后实现3个乘法定制门,最后约束公开输入的值的一致性。

    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)
    }

对于expose_public指定,限制最终输出结果c 和 `instance列的第0行值相等。

    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)
    }

FieldChip

synthesize 主要调用了FieldChip的指令,它的结构中包含了电路中的配置信息。

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

它主要实现了 NumericInstructions trait, 定义如下:

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

    /// 载入一个隐私变量的输入
    fn load_private(&self, layouter: impl Layouter<F>, a: Option<F>) -> Result<Self::Num, Error>;

    /// 载入一个常量的值
    fn load_constant(&self, layouter: impl Layouter<F>, constant: F) -> Result<Self::Num, Error>;

    /// 实现乘法门电路: `c = a * b`.
    fn mul(
        &self,
        layouter: impl Layouter<F>,
        a: Self::Num,
        b: Self::Num,
    ) -> Result<Self::Num, Error>;

    /// 约束公开输入的值
    fn expose_public(
        &self,
        layouter: impl Layouter<F>,
        num: Self::Num,
        row: usize,
    ) -> Result<(), Error>;
}

对于load_private, 其当从当前区域的第0列advice的第0行赋值。

    fn load_private(
        &self,
        mut layouter: impl Layouter<F>,
        value: Option<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.ok_or(Error::Synthesis),
                    )
                    .map(Number)
            },
        )
    }

对于load_constant, 首先将常量赋值当前区域的第0个advice 列第0行进行赋值,然后再赋值给fixed 列,然后再限制advice列和fixed列对应的值保持相等。

    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)
            },
        )
    }

对于mul指令,首先通过打开selector开关, 使定门乘法门电路生效,然后将分将变量ab的值复制到 当前区域 advice 0 和 1列的第0行,并约束其cell 值分别相等, 然后计算乘法的值,将其赋值给 当前advice 0 列下一行。

    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().and_then(|a| b.0.value().map(|b| *a * *b));

                // 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.ok_or(Error::Synthesis),
                    )
                    .map(Number)
            },
        )
    }

assign_region

上述指定主要调用了assign_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();   // 获取区域的索引 

        // 获取区域的赋值
        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;
        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.
        for column in shape.columns {
            self.columns.insert(column, region_start + shape.row_count);
        }

        // 对区域的cells 进行赋值
        self.cs.enter_region(name);
        let mut region = SingleChipLayouterRegion::new(self, region_index.into());
        let result = {
            let region: &mut dyn RegionLayouter<F> = &mut region;
            assignment(region.into())
        }?;
        let constants_to_assign = region.constants;
        self.cs.exit_region();

        // 对常量列进行赋值
        if self.constants.is_empty() {
            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)
    }

verify

主要验证以下几部分:

  • 每个区域指定的cells 已经赋值;
  • 所有的定制门电路满足条件;
  • 所有查询存在于查找表中;
  • 满足置换关系。

参考

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

https://github.com/zcash/

https://mp.weixin.qq.com/s/VerLN8-tqetKs1Hv6m4KLg

相关文章

网友评论

      本文标题:Halo2 源码分析

      本文链接:https://www.haomeiwen.com/subject/iifyhrtx.html