Table of Contents
はじめに
本稿ではzk-SNARKライブラリhalo2[1]の実装の仕組みの一部を簡単に解説します。
実装の概要
Halo2ではPLONKish回路と呼ばれる回路を用いて証明を行います。PLONKish回路の出力と証明者の主張する値が一致することを確認することで、証明者が正しい知識を持っていることを検証できます。
以下ではhalo2ライブラリに例として挙げられている、halo2/halo2_proofs/examples/simple-example.rsを元にその実装を解説します。この例では、証明者が公開された変数cに対してc=a^2\cdot b^2を満たすようなa,bの値を知っていることの証明を行なっています。
PLONKish回路
PLONKish回路は行列の形で定義され、
- 行列の要素が定義される有限体
- 列の数とその種類。列の種類は以下のいずれかです。
- fixed（固定値）
- advice（知識）
- instance（証明者と検証者で共有される値）
- 変数コピー制約
- 多項式制約
- lookup arguments
がconfigurationによって定義されます。
このPlonkish回路によって定義された多項式制約はゲートと呼ばれ、セレクター変数によって制御されます。
ゲートには群上の演算などを定めたスタンダードゲートと、特殊な操作を定義したカスタムゲートがあります。
Chip
Plonkish回路による操作はChipを組み合わせることによって実現されます。
Chipを利用することで、複雑なPlonkish回路の実装を簡単に利用することができます。
ChipはRegionに分けられ、そのregionの位置はFloor plannerによって定義されます。
Chipによって実装されたPlonkish回路はgadgetsを通して利用されます。
Instruction
PLONKish回路によって証明したい関係は、Instructionによって定義された操作を利用することで行われます。今回の例では以下の部分がInstructionです。
trait NumericInstructions<F: Field>: Chip<F> {
/// Variable representing a number.
type Num;
/// Loads a number into the circuit as a private input.
fn load_private(&self, layouter: impl Layouter<F>, a: Value<F>) -> Result<Self::Num, Error>;
/// Loads a number into the circuit as a fixed constant.
fn load_constant(&self, layouter: impl Layouter<F>, constant: F) -> Result<Self::Num, Error>;
/// Returns `c = a * b`.
fn mul(
&self,
layouter: impl Layouter<F>,
a: Self::Num,
b: Self::Num,
) -> Result<Self::Num, Error>;
/// Exposes a number as a public input to the circuit.
fn expose_public(
&self,
layouter: impl Layouter<F>,
num: Self::Num,
row: usize,
) -> Result<(), Error>;
}ここでは
- プライベート変数のロード
- 変数の乗算
- 得られた積をpublicに公開
の操作を定めています。
Chip
Instructionで定められた操作を実際に実行するのがChipです。FieldChipという構造体で実装されています。
/// The chip that will implement our instructions! Chips store their own
/// config, as well as type markers if necessary.
struct FieldChip<F: Field> {
config: FieldConfig,
_marker: PhantomData<F>,
}Chipでは回路が以下のように行列の形で実装されており、この行列の列は
- Fixed（固定値）
- Advice（知識）
- Instance（証明者と検証者で共有される値）
の種類に分かれています。今回の実装では回路の値が割り当てられるa0, a1の列はAdvice、セレクターが割り当てられるs_mulの列はFixedです。（セレクターは固定値の特殊な場合と解釈できます。）
impl<F: Field> FieldChip<F> {
fn construct(config: <Self as Chip<F>>::Config) -> Self {
Self {
config,
_marker: PhantomData,
}
}
fn configure(
meta: &mut ConstraintSystem<F>,
advice: [Column<Advice>; 2],
instance: Column<Instance>,
constant: Column<Fixed>,
) -> <Self as Chip<F>>::Config {
meta.enable_equality(instance);
meta.enable_constant(constant);
for column in &advice {
meta.enable_equality(*column);
}
let s_mul = meta.selector();
// Define our multiplication gate!
meta.create_gate("mul", |meta| {
// To implement multiplication, we need three advice cells and a selector
// cell. We arrange them like so:
//
// | a0 | a1 | s_mul |
// |-----|-----|-------|
// | lhs | rhs | s_mul |
// | out | | |
//
// Gates may refer to any relative offsets we want, but each distinct
// offset adds a cost to the proof. The most common offsets are 0 (the
// current row), 1 (the next row), and -1 (the previous row), for which
// `Rotation` has specific constructors.
let lhs = meta.query_advice(advice[0], Rotation::cur());
let rhs = meta.query_advice(advice[1], Rotation::cur());
let out = meta.query_advice(advice[0], Rotation::next());
let s_mul = meta.query_selector(s_mul);
// Finally, we return the polynomial expressions that constrain this gate.
// For our multiplication gate, we only need a single polynomial constraint.
//
// The polynomial expressions returned from `create_gate` will be
// constrained by the proving system to equal zero. Our expression
// has the following properties:
// - When s_mul = 0, any value is allowed in lhs, rhs, and out.
// - When s_mul != 0, this constrains lhs * rhs = out.
vec![s_mul * (lhs * rhs - out)]
});
FieldConfig {
advice,
instance,
s_mul,
}
}
}Chipの状態はFieldConfigureに保存されます。
/// 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,
}Instructionの実装は以下のようになります。
ここで、ゲートで用いられる変数は同じRegionのCellに割り当てなければなりません。この例ではlhs*rhsの計算に用いられるlhsとrhsが同じRegionのCellに割り当てられています。
/// A variable representing a number.
#[derive(Clone)]
struct Number<F: Field>(AssignedCell<F, F>);
impl<F: Field> NumericInstructions<F> for FieldChip<F> {
type Num = Number<F>;
fn load_private(
&self,
mut layouter: impl Layouter<F>,
value: Value<F>,
) -> Result<Self::Num, Error> {
let config = self.config();
layouter.assign_region(
|| "load private",
|mut region| {
region
.assign_advice(|| "private input", config.advice[0], 0, || value)
.map(Number)
},
)
}
fn load_constant(
&self,
mut layouter: impl Layouter<F>,
constant: F,
) -> Result<Self::Num, Error> {
let config = self.config();
layouter.assign_region(
|| "load constant",
|mut region| {
region
.assign_advice_from_constant(|| "constant value", config.advice[0], 0, constant)
.map(Number)
},
)
}
fn mul(
&self,
mut layouter: impl Layouter<F>,
a: Self::Num,
b: Self::Num,
) -> Result<Self::Num, Error> {
let config = self.config();
layouter.assign_region(
|| "mul",
|mut region: Region<'_, F>| {
// We only want to use a single multiplication gate in this region,
// so we enable it at region offset 0; this means it will constrain
// cells at offsets 0 and 1.
config.s_mul.enable(&mut region, 0)?;
// The inputs we've been given could be located anywhere in the circuit,
// but we can only rely on relative offsets inside this region. So we
// assign new cells inside the region and constrain them to have the
// same values as the inputs.
a.0.copy_advice(|| "lhs", &mut region, config.advice[0], 0)?;
b.0.copy_advice(|| "rhs", &mut region, config.advice[1], 0)?;
// Now we can assign the multiplication result, which is to be assigned
// into the output position.
let value = a.0.value().copied() * b.0.value();
// Finally, we do the assignment to the output, returning a
// variable to be used in another part of the circuit.
region
.assign_advice(|| "lhs * rhs", config.advice[0], 1, || value)
.map(Number)
},
)
}
fn expose_public(
&self,
mut layouter: impl Layouter<F>,
num: Self::Num,
row: usize,
) -> Result<(), Error> {
let config = self.config();
layouter.constrain_instance(num.0.cell(), config.instance, row)
}
}Plonkish回路全体の実装
以上を用いて実装されたInstructionを利用してPlonkish回路が以下です。
これは公開された変数cに対してc=a^2\cdot b^2を満たす変数a,bを知っていることを証明する回路となっています。
/// The full circuit implementation.
///
/// In this struct we store the private input variables. We use `Option<F>` because
/// they won't have any value during key generation. During proving, if any of these
/// were `None` we would get an error.
#[derive(Default)]
struct MyCircuit<F: Field> {
constant: F,
a: Value<F>,
b: Value<F>,
}
impl<F: Field> Circuit<F> for MyCircuit<F> {
// Since we are using a single chip for everything, we can just reuse its config.
type Config = FieldConfig;
type FloorPlanner = SimpleFloorPlanner;
fn without_witnesses(&self) -> Self {
Self::default()
}
fn configure(meta: &mut ConstraintSystem<F>) -> Self::Config {
// We create the two advice columns that FieldChip uses for I/O.
let advice = [meta.advice_column(), meta.advice_column()];
// We also need an instance column to store public inputs.
let instance = meta.instance_column();
// Create a fixed column to load constants.
let constant = meta.fixed_column();
FieldChip::configure(meta, advice, instance, constant)
}
fn synthesize(
&self,
config: Self::Config,
mut layouter: impl Layouter<F>,
) -> Result<(), Error> {
let field_chip = FieldChip::<F>::construct(config);
// Load our private values into the circuit.
let a = field_chip.load_private(layouter.namespace(|| "load a"), self.a)?;
let b = field_chip.load_private(layouter.namespace(|| "load b"), self.b)?;
// Load the constant factor into the circuit.
let constant =
field_chip.load_constant(layouter.namespace(|| "load constant"), self.constant)?;
// We only have access to plain multiplication.
// We could implement our circuit as:
// asq = a*a
// bsq = b*b
// absq = asq*bsq
// c = constant*asq*bsq
//
// but it's more efficient to implement it as:
// ab = a*b
// absq = ab^2
// c = constant*absq
let ab = field_chip.mul(layouter.namespace(|| "a * b"), a, b)?;
let absq = field_chip.mul(layouter.namespace(|| "ab * ab"), ab.clone(), ab)?;
let c = field_chip.mul(layouter.namespace(|| "constant * absq"), constant, absq)?;
// Expose the result as a public input to the circuit.
field_chip.expose_public(layouter.namespace(|| "expose c"), c, 0)
}
}この回路の証明はMockProver::runを用いることで作ることができます。
以下がそのコードです。
// The number of rows in our circuit cannot exceed 2^k. Since our example
// circuit is very small, we can pick a very small value here.
let k = 4;
// Prepare the private and public inputs to the circuit!
let constant = Fp::from(7);
let a = Fp::from(2);
let b = Fp::from(3);
let c = constant * a.square() * b.square();
// Instantiate the circuit with the private inputs.
let circuit = MyCircuit {
constant,
a: Value::known(a),
b: Value::known(b),
};
// Arrange the public input. We expose the multiplication result in row 0
// of the instance column, so we position it there in our public inputs.
let mut public_inputs = vec![c];
// Given the correct public input, our circuit will verify.
let prover = MockProver::run(k, &circuit, vec![public_inputs.clone()]).unwrap();
assert_eq!(prover.verify(), Ok(()));
// If we try some other public input, the proof will fail!
public_inputs[0] += Fp::one();
let prover = MockProver::run(k, &circuit, vec![public_inputs]).unwrap();
assert!(prover.verify().is_err());その他
- 計算のコストを抑えるために、変数の関係を前計算したものを保存したLookup Tableを用意して、それを参照するLookup Argumentと呼ばれる手法を用いています。これはPlookup[2]と呼ばれるプロトコルの簡単なものの様ですが詳細は理解できていません。
感想
論文を元にhalo2のプロトコルを理解することを試みましたが、理解できない箇所が多数残ってしまいました。本当にこのプロトコルが安全かどうか、確かめられていません。プロトコルが非常に複雑なため、halo2を実際に使用するためには、安全性を慎重に確認する必要があると思います。
参考文献
[1]zcash/halo2
[2]plookup: A simplified polynomial protocol for lookup tables
