美文网首页
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