Halo2 源码分析
2022-01-21 本文已影响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主要实现电路列的配置，MyCircuit的config类型为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 定制门，结构如下，a0 和 a1为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
电路的合成通过FloorPlanner的 synthesize 函数，最终调用电路的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 主要实现电路区域的布局，以下面的实现中，首先载入两个变量a 和 b 的值，然后实现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开关， 使定门乘法门电路生效，然后将分将变量a和b的值复制到 当前区域 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已经赋值； - 所有的定制门电路满足条件；
- 所有查询存在于查找表中；
- 满足置换关系。
