From bfbfa80900989b8af1b6c81e6840835c05e22dad Mon Sep 17 00:00:00 2001 From: Jack Grigg Date: Wed, 3 Feb 2021 20:34:25 +0000 Subject: [PATCH 1/2] book: Add a comparison to BCMS20 --- book/src/SUMMARY.md | 1 + book/src/design/proving-system/comparison.md | 54 ++++++++++++++++++++ 2 files changed, 55 insertions(+) create mode 100644 book/src/design/proving-system/comparison.md diff --git a/book/src/SUMMARY.md b/book/src/SUMMARY.md index 56d8b0c..e6eb615 100644 --- a/book/src/SUMMARY.md +++ b/book/src/SUMMARY.md @@ -17,6 +17,7 @@ - [Multipoint opening argument](design/proving-system/multipoint-opening.md) - [Permutation argument](design/proving-system/permutation.md) - [Lookup argument](design/proving-system/lookup-argument.md) + - [Comparison to other work](design/proving-system/comparison.md) - [Implementation](design/implementation.md) - [Gadgets](design/gadgets.md) - [SHA-256](design/gadgets/sha256.md) diff --git a/book/src/design/proving-system/comparison.md b/book/src/design/proving-system/comparison.md new file mode 100644 index 0000000..56517ee --- /dev/null +++ b/book/src/design/proving-system/comparison.md @@ -0,0 +1,54 @@ +# Comparison to other work + +## BCMS20 Appendix A.2 + +Appendix A.2 of [BCMS20] describes a polynomial commitment scheme that is similar to the +one described in [BGH19] (BCMS20 being a generalization of the original Halo paper). Halo +2 builds on both of these works, and thus itself uses a polynomial commitment scheme that +is very similar to the one in BCMS20. + +[BGH19]: https://eprint.iacr.org/2019/1021 +[BCMS20]: https://eprint.iacr.org/2020/499 + +The following table provides a mapping between the variable names in BCMS20, and the +equivalent objects in Halo 2 (which builds on the nomenclature from the Halo paper): + +| BCMS20 | Halo 2 | +| :------------: | :-----------------: | +| $S$ | $H$ | +| $H$ | $U$ | +| $C$ | `msm` or $P$ | +| $\alpha$ | $\iota$ | +| $\xi_0$ | $z$ | +| $\xi_i$ | `challenge_i` | +| $H'$ | $[z] U$ | +| $\bar{p}$ | `s_poly` | +| $\bar{\omega}$ | `s_poly_blind` | +| $\bar{C}$ | `s_poly_commitment` | +| $h(X)$ | $g(X)$ | +| $\omega'$ | `blind` / $\xi$ | +| $\mathbf{c}$ | $\mathbf{a}$ | +| $c$ | $a = \mathbf{a}_0$ | +| $v'$ | $ab$ | + +Halo 2's polynomial commitment scheme differs from Appendix A.2 of BCMS20 in two ways: + +1. Step 8 of the $\text{Open}$ algorithm computes a "non-hiding" commitment $C'$ prior to + the inner product argument, which opens to the same value as $C$ but is a commitment to + a randomly-drawn polynomial. The remainder of the protocol involves no blinding. By + contrast, in Halo 2 we blind every single commitment that we make (even for auxiliary + and fixed polynomials, though using a blinding factor of 1 for the fixed polynomials); + this makes the protocol simpler to reason about. As a consequence of this, the verifier + needs to handle the cumulative blinding factor at the end of the protocol, and so there + is no need to derive an equivalent to $C'$ at the start of the protocol. + + - $C'$ is also an input to the random oracle for $\xi_0$; in Halo 2 we utilize a + transcript that has already committed to the equivalent components of $C'$ prior to + sampling $z$. + +2. The $\text{PC}_\text{DL}.\text{SuccinctCheck}$ subroutine (Figure 2 of BCMS20) computes + the initial group element $C_0$ by adding $[v] H' = [v \epsilon] H$, which requires two + scalar multiplications. Instead, we subtract $[v] G_0$ from the original commitment $P$, + so that we're effectively opening the polynomial at the point to the value zero. The + computation $[v] G_0$ is more efficient in the context of recursion because $G_0$ is a + fixed base (so we can use lookup tables). From 425c45d96b3d3d85f4bca4898009e8794c89d17b Mon Sep 17 00:00:00 2001 From: Jack Grigg Date: Fri, 5 Feb 2021 14:28:50 +0000 Subject: [PATCH 2/2] book: Add a simple example showing how the API is used --- book/src/user/simple-example.md | 85 +++++++- examples/simple-example.rs | 343 ++++++++++++++++++++++++++++++++ 2 files changed, 419 insertions(+), 9 deletions(-) create mode 100644 examples/simple-example.rs diff --git a/book/src/user/simple-example.md b/book/src/user/simple-example.md index 964471c..1ab8248 100644 --- a/book/src/user/simple-example.md +++ b/book/src/user/simple-example.md @@ -4,16 +4,83 @@ Let's start with a simple circuit, to introduce you to the common APIs and how t used. The circuit will take a public input $c$, and will prove knowledge of two private inputs $a$ and $b$ such that -$$a \cdot b = c.$$ +$$a^2 \cdot b^2 = c.$$ -```rust -# extern crate halo2; -use halo2::arithmetic::FieldExt; +## Define instructions -struct MyCircuit { - a: F, - b: F, -} +Firstly, we need to define the instructions that our circuit will rely on. Instructions +are the boundary between high-level [gadgets](../concepts/gadgets.md) and the low-level +circuit operations. Instructions may be as coarse or as granular as desired, but in +practice you want to strike a balance between an instruction being large enough to +effectively optimize its implementation, and small enough that it is meaningfully +reusable. + +For our circuit, we will use three instructions: +- Load a private number into the circuit. +- Multiply two numbers. +- Expose a number as a public input to the circuit. + +We also need a type for a variable representing a number. Instruction interfaces provide +associated types for their inputs and outputs, to allow the implementations to represent +these in a way that makes the most sense for their optimization goals. + +```rust,ignore,no_run +{{#include ../../../examples/simple-example.rs:instructions}} ``` -TODO +## Define a chip implementation + +For our circuit, we will build a [chip](../concepts/chips.md) that provides the above +numeric instructions for a finite field. + +```rust,ignore,no_run +{{#include ../../../examples/simple-example.rs:chip}} +``` + +Every chip needs to implement the `Chip` trait. This defines the properties of the chip +that a `Layouter` may rely on when synthesizing a circuit, as well as enabling any initial +state that the chip requires to be loaded into the circuit. + +```rust,ignore,no_run +{{#include ../../../examples/simple-example.rs:chip-impl}} +``` + +## Configure the chip + +The chip needs to be configured with the columns, permutations, and gates that will be +required to implement all of the desired instructions. + +```rust,ignore,no_run +{{#include ../../../examples/simple-example.rs:chip-config}} +``` + +## Implement chip traits + +```rust,ignore,no_run +{{#include ../../../examples/simple-example.rs:instructions-impl}} +``` + +## Build the circuit + +Now that we have the instructions we need, and a chip that implements them, we can finally +build our circuit! + +```rust,ignore,no_run +{{#include ../../../examples/simple-example.rs:circuit}} +``` + +## Testing the circuit + +`halo2::dev::MockProver` can be used to test that the circuit is working correctly. The +private and public inputs to the circuit are constructed as we will do to create a proof, +but by passing them to `MockProver::run` we get an object that can test every constraint +in the circuit, and tell us exactly what is failing (if anything). + +```rust,ignore,no_run +{{#include ../../../examples/simple-example.rs:test-circuit}} +``` + +## Full example + +You can find the source code for this example +[here](https://github.com/zcash/halo2/tree/main/examples/simple-example.rs). diff --git a/examples/simple-example.rs b/examples/simple-example.rs new file mode 100644 index 0000000..35cf550 --- /dev/null +++ b/examples/simple-example.rs @@ -0,0 +1,343 @@ +extern crate halo2; + +use std::marker::PhantomData; + +use halo2::{ + arithmetic::FieldExt, + circuit::{layouter::SingleChip, Cell, Chip, Layouter, Permutation}, + dev::VerifyFailure, + plonk::{Advice, Assignment, Aux, Circuit, Column, ConstraintSystem, Error, Fixed}, + poly::Rotation, +}; + +// ANCHOR: instructions +trait NumericInstructions: Chip { + /// Variable representing a number. + type Num; + + /// Loads a number into the circuit as a private input. + fn load_private( + layouter: &mut impl Layouter, + a: Option, + ) -> Result; + + /// Returns `c = a * b`. + fn mul( + layouter: &mut impl Layouter, + a: Self::Num, + b: Self::Num, + ) -> Result; + + /// Exposes a number as a public input to the circuit. + fn expose_public(layouter: &mut impl Layouter, num: Self::Num) -> Result<(), Error>; +} +// ANCHOR_END: instructions + +// ANCHOR: chip +/// The chip that will implement our instructions! Chips do not store any persistent state +/// themselves, and usually only contain type markers if necessary. +struct FieldChip { + _marker: PhantomData, +} +// ANCHOR_END: chip + +// ANCHOR: chip-config +/// Chip state is stored in a separate config struct. This is generated by the chip during +/// configuration, and then handed to the `Layouter`, which makes it available to the chip +/// when it needs to implement its instructions. +#[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; 2], + + // We need to create a permutation between our advice columns. This allows us to + // copy numbers within these columns from arbitrary rows, which we can use to load + // inputs into our instruction regions. + perm: Permutation, + + // 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: Column, + + // The selector for the public-input gate, which uses one of the advice columns. + s_pub: Column, +} + +impl FieldChip { + fn configure( + meta: &mut ConstraintSystem, + advice: [Column; 2], + aux: Column, + ) -> FieldConfig { + let perm = Permutation::new(meta, &advice); + let s_mul = meta.fixed_column(); + let s_pub = meta.fixed_column(); + + // 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_fixed(s_mul, Rotation::cur()); + + // The polynomial expression 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. + s_mul * (lhs * rhs + out * -F::one()) + }); + + // Define our public-input gate! + meta.create_gate("public input", |meta| { + // We choose somewhat-arbitrarily that we will use the second advice column + // for exposing numbers as public inputs. + let a = meta.query_advice(advice[1], Rotation::cur()); + let p = meta.query_aux(aux, Rotation::cur()); + let s = meta.query_fixed(s_pub, Rotation::cur()); + + // We simply constrain the advice cell to be equal to the aux cell, when the + // selector is enabled. + s * (p + a * -F::one()) + }); + + FieldConfig { + advice, + perm, + s_mul, + s_pub, + } + } +} +// ANCHOR_END: chip-config + +// ANCHOR: chip-impl +impl Chip for FieldChip { + type Config = FieldConfig; + type Field = F; + + fn load(_layouter: &mut impl Layouter) -> Result<(), halo2::plonk::Error> { + // None of the instructions implemented by this chip have any fixed state. But if + // we required e.g. a lookup table, this is where we would load it. + Ok(()) + } +} +// ANCHOR_END: chip-impl + +// ANCHOR: instructions-impl +/// A variable representing a number. +#[derive(Clone)] +struct Number { + cell: Cell, + value: Option, +} + +impl NumericInstructions for FieldChip { + type Num = Number; + + fn load_private( + layouter: &mut impl Layouter, + value: Option, + ) -> Result { + let config = layouter.config().clone(); + let mut num = None; + layouter.assign_region( + || "load private", + |mut region| { + let cell = region.assign_advice( + || "private input", + config.advice[0], + 0, + || value.ok_or(Error::SynthesisError), + )?; + num = Some(Number { cell, value }); + Ok(()) + }, + )?; + Ok(num.unwrap()) + } + + fn mul( + layouter: &mut impl Layouter, + a: Self::Num, + b: Self::Num, + ) -> Result { + let config = layouter.config().clone(); + let mut out = None; + layouter.assign_region( + || "mul", + |mut region| { + // 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. + region.assign_fixed(|| "example mul", config.s_mul, 0, || Ok(F::one()))?; + + // 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. + let lhs = region.assign_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(&config.perm, a.cell, lhs)?; + region.constrain_equal(&config.perm, 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()) + } + + fn expose_public(layouter: &mut impl Layouter, num: Self::Num) -> Result<(), Error> { + let config = layouter.config().clone(); + layouter.assign_region( + || "expose public", + |mut region| { + // Enable the public-input gate. + region.assign_fixed(|| "public result", config.s_pub, 0, || Ok(F::one()))?; + + // Load the output into the correct advice column. + let out = region.assign_advice( + || "public advice", + config.advice[1], + 0, + || num.value.ok_or(Error::SynthesisError), + )?; + region.constrain_equal(&config.perm, num.cell, out)?; + + // We don't assign to the auxiliary column inside the circuit; the mapping + // of public inputs to cells is provided to the prover. + Ok(()) + }, + ) + } +} +// ANCHOR_END: instructions-impl + +// ANCHOR: circuit +/// The full circuit implementation. +/// +/// In this struct we store the private input variables. We use `Option` because they +/// won't have any value during key generation. During proving, if any of these were +/// `None` we would get an error. +struct MyCircuit { + a: Option, + b: Option, +} + +impl Circuit for MyCircuit { + // Since we are using a single chip for everything, we can just reuse its config. + type Config = FieldConfig; + + fn configure(meta: &mut ConstraintSystem) -> 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 auxiliary column to store public inputs. + let aux = meta.aux_column(); + + FieldChip::configure(meta, advice, aux) + } + + fn synthesize(&self, cs: &mut impl Assignment, config: Self::Config) -> Result<(), Error> { + let mut layouter = SingleChip::new(cs, config); + + // Load our private values into the circuit. + let a = FieldChip::load_private(&mut layouter, self.a)?; + let b = FieldChip::load_private(&mut layouter, self.b)?; + + // We only have access to plain multiplication. We could implement our circuit as: + // asq = a*a + // bsq = b*b + // c = asq*bsq + // + // but it's more efficient to implement it as: + // ab = a*b + // c = ab^2 + let ab = FieldChip::mul(&mut layouter, a, b)?; + let c = FieldChip::mul(&mut layouter, ab.clone(), ab)?; + + // Expose the result as a public input to the circuit. + FieldChip::expose_public(&mut layouter, c) + } +} +// ANCHOR_END: circuit + +fn main() { + use halo2::{dev::MockProver, pasta::Fp}; + + // ANCHOR: test-circuit + // 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 = 3; + + // Prepare the private and public inputs to the circuit! + let a = Fp::from(2); + let b = Fp::from(3); + let c = a.square() * b.square(); + + // Instantiate the circuit with the private inputs. + let circuit = MyCircuit { + a: Some(a), + b: Some(b), + }; + + // Arrange the public input. We expose the multiplication result in row 4 of the aux + // column, so we position it there in our public inputs. + let mut public_inputs = vec![Fp::zero(); 1 << k]; + public_inputs[6] = 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[6] += Fp::one(); + let prover = MockProver::run(k, &circuit, vec![public_inputs]).unwrap(); + assert_eq!( + prover.verify(), + Err(VerifyFailure::Gate { + gate_index: 1, + gate_name: "public input", + row: 6, + }) + ); + // ANCHOR_END: test-circuit +}