Merge pull request #178 from zcash/simple-example-comments

Reflow simple-example.rs comments
This commit is contained in:
str4d 2021-02-13 05:09:15 +13:00 committed by GitHub
commit 13ac4e7573
No known key found for this signature in database
GPG key ID: 4AEE18F83AFDEB23

View file

@ -34,21 +34,22 @@ trait NumericInstructions: Chip {
// ANCHOR_END: instructions // ANCHOR_END: instructions
// ANCHOR: chip // ANCHOR: chip
/// The chip that will implement our instructions! Chips do not store any persistent state /// The chip that will implement our instructions! Chips do not store any persistent
/// themselves, and usually only contain type markers if necessary. /// state themselves, and usually only contain type markers if necessary.
struct FieldChip<F: FieldExt> { struct FieldChip<F: FieldExt> {
_marker: PhantomData<F>, _marker: PhantomData<F>,
} }
// ANCHOR_END: chip // ANCHOR_END: chip
// ANCHOR: chip-config // ANCHOR: chip-config
/// Chip state is stored in a separate config struct. This is generated by the chip during /// Chip state is stored in a separate config struct. This is generated by the chip
/// configuration, and then handed to the `Layouter`, which makes it available to the chip /// during configuration, and then handed to the `Layouter`, which makes it available
/// when it needs to implement its instructions. /// to the chip when it needs to implement its instructions.
#[derive(Clone, Debug)] #[derive(Clone, Debug)]
struct FieldConfig { struct FieldConfig {
/// For this chip, we will use two advice columns to implement our instructions. These /// For this chip, we will use two advice columns to implement our instructions.
/// are also the columns through which we communicate with other parts of the circuit. /// These are also the columns through which we communicate with other parts of
/// the circuit.
advice: [Column<Advice>; 2], advice: [Column<Advice>; 2],
// We need to create a permutation between our advice columns. This allows us to // We need to create a permutation between our advice columns. This allows us to
@ -86,18 +87,18 @@ impl<F: FieldExt> FieldChip<F> {
// | lhs | rhs | s_mul | // | lhs | rhs | s_mul |
// | out | | | // | out | | |
// //
// Gates may refer to any relative offsets we want, but each distinct offset // Gates may refer to any relative offsets we want, but each distinct
// adds a cost to the proof. The most common offsets are 0 (the current row), // offset adds a cost to the proof. The most common offsets are 0 (the
// 1 (the next row), and -1 (the previous row), for which `Rotation` has // current row), 1 (the next row), and -1 (the previous row), for which
// specific constructors. // `Rotation` has specific constructors.
let lhs = meta.query_advice(advice[0], Rotation::cur()); let lhs = meta.query_advice(advice[0], Rotation::cur());
let rhs = meta.query_advice(advice[1], Rotation::cur()); let rhs = meta.query_advice(advice[1], Rotation::cur());
let out = meta.query_advice(advice[0], Rotation::next()); let out = meta.query_advice(advice[0], Rotation::next());
let s_mul = meta.query_fixed(s_mul, Rotation::cur()); let s_mul = meta.query_fixed(s_mul, Rotation::cur());
// The polynomial expression returned from `create_gate` will be constrained // The polynomial expression returned from `create_gate` will be
// by the proving system to equal zero. Our expression has the following // constrained by the proving system to equal zero. Our expression
// properties: // has the following properties:
// - When s_mul = 0, any value is allowed in lhs, rhs, and out. // - When s_mul = 0, any value is allowed in lhs, rhs, and out.
// - When s_mul != 0, this constrains lhs * rhs = out. // - When s_mul != 0, this constrains lhs * rhs = out.
s_mul * (lhs * rhs + out * -F::one()) s_mul * (lhs * rhs + out * -F::one())
@ -105,14 +106,14 @@ impl<F: FieldExt> FieldChip<F> {
// Define our public-input gate! // Define our public-input gate!
meta.create_gate("public input", |meta| { meta.create_gate("public input", |meta| {
// We choose somewhat-arbitrarily that we will use the second advice column // We choose somewhat-arbitrarily that we will use the second advice
// for exposing numbers as public inputs. // column for exposing numbers as public inputs.
let a = meta.query_advice(advice[1], Rotation::cur()); let a = meta.query_advice(advice[1], Rotation::cur());
let p = meta.query_aux(aux, Rotation::cur()); let p = meta.query_aux(aux, Rotation::cur());
let s = meta.query_fixed(s_pub, 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 // We simply constrain the advice cell to be equal to the aux cell,
// selector is enabled. // when the selector is enabled.
s * (p + a * -F::one()) s * (p + a * -F::one())
}); });
@ -132,8 +133,8 @@ impl<F: FieldExt> Chip for FieldChip<F> {
type Field = F; type Field = F;
fn load(_layouter: &mut impl Layouter<Self>) -> Result<(), halo2::plonk::Error> { fn load(_layouter: &mut impl Layouter<Self>) -> Result<(), halo2::plonk::Error> {
// None of the instructions implemented by this chip have any fixed state. But if // None of the instructions implemented by this chip have any fixed state.
// we required e.g. a lookup table, this is where we would load it. // But if we required e.g. a lookup table, this is where we would load it.
Ok(()) Ok(())
} }
} }
@ -182,15 +183,15 @@ impl<F: FieldExt> NumericInstructions for FieldChip<F> {
layouter.assign_region( layouter.assign_region(
|| "mul", || "mul",
|mut region| { |mut region| {
// We only want to use a single multiplication gate in this region, so we // We only want to use a single multiplication gate in this region,
// enable it at region offset 0; this means it will constrain cells at // so we enable it at region offset 0; this means it will constrain
// offsets 0 and 1. // cells at offsets 0 and 1.
region.assign_fixed(|| "example mul", config.s_mul, 0, || Ok(F::one()))?; 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, // 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 // 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 // assign new cells inside the region and constrain them to have the
// values as the inputs. // same values as the inputs.
let lhs = region.assign_advice( let lhs = region.assign_advice(
|| "lhs", || "lhs",
config.advice[0], config.advice[0],
@ -215,8 +216,8 @@ impl<F: FieldExt> NumericInstructions for FieldChip<F> {
|| value.ok_or(Error::SynthesisError), || value.ok_or(Error::SynthesisError),
)?; )?;
// Finally, we return a variable representing the output, to be used in // Finally, we return a variable representing the output,
// another part of the circuit. // to be used in another part of the circuit.
out = Some(Number { cell, value }); out = Some(Number { cell, value });
Ok(()) Ok(())
}, },
@ -242,8 +243,8 @@ impl<F: FieldExt> NumericInstructions for FieldChip<F> {
)?; )?;
region.constrain_equal(&config.perm, num.cell, out)?; region.constrain_equal(&config.perm, num.cell, out)?;
// We don't assign to the auxiliary column inside the circuit; the mapping // We don't assign to the auxiliary column inside the circuit;
// of public inputs to cells is provided to the prover. // the mapping of public inputs to cells is provided to the prover.
Ok(()) Ok(())
}, },
) )
@ -254,9 +255,9 @@ impl<F: FieldExt> NumericInstructions for FieldChip<F> {
// ANCHOR: circuit // ANCHOR: circuit
/// The full circuit implementation. /// The full circuit implementation.
/// ///
/// In this struct we store the private input variables. We use `Option<F>` because they /// In this struct we store the private input variables. We use `Option<F>` because
/// won't have any value during key generation. During proving, if any of these were /// they won't have any value during key generation. During proving, if any of these
/// `None` we would get an error. /// were `None` we would get an error.
struct MyCircuit<F: FieldExt> { struct MyCircuit<F: FieldExt> {
a: Option<F>, a: Option<F>,
b: Option<F>, b: Option<F>,
@ -283,7 +284,8 @@ impl<F: FieldExt> Circuit<F> for MyCircuit<F> {
let a = FieldChip::load_private(&mut layouter, self.a)?; let a = FieldChip::load_private(&mut layouter, self.a)?;
let b = FieldChip::load_private(&mut layouter, self.b)?; let b = FieldChip::load_private(&mut layouter, self.b)?;
// We only have access to plain multiplication. We could implement our circuit as: // We only have access to plain multiplication.
// We could implement our circuit as:
// asq = a*a // asq = a*a
// bsq = b*b // bsq = b*b
// c = asq*bsq // c = asq*bsq
@ -304,8 +306,8 @@ fn main() {
use halo2::{dev::MockProver, pasta::Fp}; use halo2::{dev::MockProver, pasta::Fp};
// ANCHOR: test-circuit // ANCHOR: test-circuit
// The number of rows in our circuit cannot exceed 2^k. Since our example circuit is // The number of rows in our circuit cannot exceed 2^k. Since our example
// very small, we can pick a very small value here. // circuit is very small, we can pick a very small value here.
let k = 3; let k = 3;
// Prepare the private and public inputs to the circuit! // Prepare the private and public inputs to the circuit!
@ -319,8 +321,8 @@ fn main() {
b: Some(b), b: Some(b),
}; };
// Arrange the public input. We expose the multiplication result in row 4 of the aux // Arrange the public input. We expose the multiplication result in row 6
// column, so we position it there in our public inputs. // of the aux column, so we position it there in our public inputs.
let mut public_inputs = vec![Fp::zero(); 1 << k]; let mut public_inputs = vec![Fp::zero(); 1 << k];
public_inputs[6] = c; public_inputs[6] = c;