mirror of https://github.com/zcash/halo2.git
Add lookup_any
This commit is contained in:
kilic
parent
0e9b075c3a
commit
bebee898fe
|
|
@ -0,0 +1,377 @@
|
|||
use halo2_proofs::arithmetic::FieldExt;
|
||||
use halo2_proofs::circuit::{Cell, Chip, Layouter, Region, SimpleFloorPlanner};
|
||||
use halo2_proofs::dev::MockProver;
|
||||
use halo2_proofs::plonk::*;
|
||||
use halo2_proofs::poly::Rotation;
|
||||
use pairing::bn256::Fr as Fp;
|
||||
|
||||
use std::marker::PhantomData;
|
||||
|
||||
trait NumericInstructions<F: FieldExt>: 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: Option<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>;
|
||||
}
|
||||
|
||||
/// 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>,
|
||||
}
|
||||
|
||||
impl<F: FieldExt> Chip<F> for FieldChip<F> {
|
||||
type Config = FieldConfig;
|
||||
type Loaded = ();
|
||||
|
||||
fn config(&self) -> &Self::Config {
|
||||
&self.config
|
||||
}
|
||||
|
||||
fn loaded(&self) -> &Self::Loaded {
|
||||
&()
|
||||
}
|
||||
}
|
||||
|
||||
/// Chip state is stored in a config struct. This is generated by the chip
|
||||
/// during configuration, and then stored inside the chip.
|
||||
#[warn(dead_code)]
|
||||
#[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,
|
||||
|
||||
/// The fixed column used to load constants.
|
||||
constant: Column<Fixed>,
|
||||
}
|
||||
|
||||
impl<F: FieldExt> 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,
|
||||
constant,
|
||||
}
|
||||
}
|
||||
}
|
||||
|
||||
/// A variable representing a number.
|
||||
#[derive(Clone)]
|
||||
struct Number<F: FieldExt> {
|
||||
cell: Cell,
|
||||
value: Option<F>,
|
||||
}
|
||||
|
||||
impl<F: FieldExt> NumericInstructions<F> for FieldChip<F> {
|
||||
type Num = Number<F>;
|
||||
|
||||
fn load_private(
|
||||
&self,
|
||||
mut layouter: impl Layouter<F>,
|
||||
value: Option<F>,
|
||||
) -> Result<Self::Num, Error> {
|
||||
let config = self.config();
|
||||
|
||||
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::Synthesis),
|
||||
)?
|
||||
.cell();
|
||||
num = Some(Number { cell, value });
|
||||
Ok(())
|
||||
},
|
||||
)?;
|
||||
Ok(num.unwrap())
|
||||
}
|
||||
|
||||
fn load_constant(
|
||||
&self,
|
||||
mut layouter: impl Layouter<F>,
|
||||
constant: F,
|
||||
) -> Result<Self::Num, Error> {
|
||||
let config = self.config();
|
||||
|
||||
let mut num = None;
|
||||
layouter.assign_region(
|
||||
|| "load constant",
|
||||
|mut region| {
|
||||
let cell = region
|
||||
.assign_advice_from_constant(
|
||||
|| "constant value",
|
||||
config.advice[0],
|
||||
0,
|
||||
constant,
|
||||
)?
|
||||
.cell();
|
||||
num = Some(Number {
|
||||
cell,
|
||||
value: Some(constant),
|
||||
});
|
||||
Ok(())
|
||||
},
|
||||
)?;
|
||||
Ok(num.unwrap())
|
||||
}
|
||||
|
||||
fn mul(
|
||||
&self,
|
||||
mut layouter: impl Layouter<F>,
|
||||
a: Self::Num,
|
||||
b: Self::Num,
|
||||
) -> Result<Self::Num, Error> {
|
||||
let config = self.config();
|
||||
|
||||
let mut out = None;
|
||||
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.
|
||||
let lhs = region
|
||||
.assign_advice(
|
||||
|| "lhs",
|
||||
config.advice[0],
|
||||
0,
|
||||
|| a.value.ok_or(Error::Synthesis),
|
||||
)?
|
||||
.cell();
|
||||
let rhs = region
|
||||
.assign_advice(
|
||||
|| "rhs",
|
||||
config.advice[1],
|
||||
0,
|
||||
|| b.value.ok_or(Error::Synthesis),
|
||||
)?
|
||||
.cell();
|
||||
region.constrain_equal(a.cell, lhs)?;
|
||||
region.constrain_equal(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::Synthesis),
|
||||
)?
|
||||
.cell();
|
||||
|
||||
// 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(
|
||||
&self,
|
||||
mut layouter: impl Layouter<F>,
|
||||
num: Self::Num,
|
||||
row: usize,
|
||||
) -> Result<(), Error> {
|
||||
let config = self.config();
|
||||
|
||||
layouter.constrain_instance(num.cell, config.instance, row)
|
||||
}
|
||||
}
|
||||
|
||||
/// 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: FieldExt> {
|
||||
constant: F,
|
||||
a: Option<F>,
|
||||
b: Option<F>,
|
||||
}
|
||||
|
||||
impl<F: FieldExt> 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)
|
||||
}
|
||||
}
|
||||
|
||||
fn main() {
|
||||
// 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: Some(a),
|
||||
b: Some(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());
|
||||
}
|
||||
|
|
@ -940,6 +940,26 @@ impl<F: Field> ConstraintSystem<F> {
|
|||
index
|
||||
}
|
||||
|
||||
/// Add a lookup argument for some input expressions and table columns.
|
||||
///
|
||||
/// `table_map` returns a map between input expressions and the table columns
|
||||
/// they need to match.
|
||||
///
|
||||
/// This API allows any column type to be used as table columns.
|
||||
pub fn lookup_any(
|
||||
&mut self,
|
||||
table_map: impl FnOnce(&mut VirtualCells<'_, F>) -> Vec<(Expression<F>, Expression<F>)>,
|
||||
) -> usize {
|
||||
let mut cells = VirtualCells::new(self);
|
||||
let table_map = table_map(&mut cells);
|
||||
|
||||
let index = self.lookups.len();
|
||||
|
||||
self.lookups.push(lookup::Argument::new(table_map));
|
||||
|
||||
index
|
||||
}
|
||||
|
||||
fn query_fixed_index(&mut self, column: Column<Fixed>, at: Rotation) -> usize {
|
||||
// Return existing query, if it exists
|
||||
for (index, fixed_query) in self.fixed_queries.iter().enumerate() {
|
||||
|
|
|
|||
|
|
@ -0,0 +1,210 @@
|
|||
use std::marker::PhantomData;
|
||||
|
||||
use halo2_proofs::{
|
||||
arithmetic::FieldExt,
|
||||
circuit::{Layouter, SimpleFloorPlanner},
|
||||
dev::MockProver,
|
||||
plonk::{Advice, Circuit, Column, ConstraintSystem, Error, Instance, Selector},
|
||||
poly::Rotation,
|
||||
};
|
||||
use pairing::bn256::Fr as Fp;
|
||||
|
||||
#[test]
|
||||
fn lookup_any() {
|
||||
#[derive(Clone, Debug)]
|
||||
struct MyConfig<F: FieldExt> {
|
||||
input: Column<Advice>,
|
||||
// Selector to enable lookups on even numbers.
|
||||
q_even: Selector,
|
||||
// Use an advice column as the lookup table column for even numbers.
|
||||
table_even: Column<Advice>,
|
||||
// Selector to enable lookups on odd numbers.
|
||||
q_odd: Selector,
|
||||
// Use an instance column as the lookup table column for odd numbers.
|
||||
table_odd: Column<Instance>,
|
||||
_marker: PhantomData<F>,
|
||||
}
|
||||
|
||||
impl<F: FieldExt> MyConfig<F> {
|
||||
fn configure(meta: &mut ConstraintSystem<F>) -> Self {
|
||||
let config = Self {
|
||||
input: meta.advice_column(),
|
||||
q_even: meta.complex_selector(),
|
||||
table_even: meta.advice_column(),
|
||||
q_odd: meta.complex_selector(),
|
||||
table_odd: meta.instance_column(),
|
||||
_marker: PhantomData,
|
||||
};
|
||||
|
||||
// Lookup on even numbers
|
||||
meta.lookup_any(|meta| {
|
||||
let input = meta.query_advice(config.input, Rotation::cur());
|
||||
|
||||
let q_even = meta.query_selector(config.q_even);
|
||||
let table_even = meta.query_advice(config.table_even, Rotation::cur());
|
||||
|
||||
vec![(q_even * input, table_even)]
|
||||
});
|
||||
|
||||
// Lookup on odd numbers
|
||||
meta.lookup_any(|meta| {
|
||||
let input = meta.query_advice(config.input, Rotation::cur());
|
||||
|
||||
let q_odd = meta.query_selector(config.q_odd);
|
||||
let table_odd = meta.query_instance(config.table_odd, Rotation::cur());
|
||||
|
||||
vec![(q_odd * input, table_odd)]
|
||||
});
|
||||
|
||||
config
|
||||
}
|
||||
|
||||
fn witness_even(
|
||||
&self,
|
||||
mut layouter: impl Layouter<F>,
|
||||
value: Option<F>,
|
||||
) -> Result<(), Error> {
|
||||
layouter.assign_region(
|
||||
|| "witness even number",
|
||||
|mut region| {
|
||||
// Enable the even lookup.
|
||||
self.q_even.enable(&mut region, 0)?;
|
||||
|
||||
region.assign_advice(
|
||||
|| "even input",
|
||||
self.input,
|
||||
0,
|
||||
|| value.ok_or(Error::Synthesis),
|
||||
)?;
|
||||
Ok(())
|
||||
},
|
||||
)
|
||||
}
|
||||
|
||||
fn witness_odd(
|
||||
&self,
|
||||
mut layouter: impl Layouter<F>,
|
||||
value: Option<F>,
|
||||
) -> Result<(), Error> {
|
||||
layouter.assign_region(
|
||||
|| "witness odd number",
|
||||
|mut region| {
|
||||
// Enable the odd lookup.
|
||||
self.q_odd.enable(&mut region, 0)?;
|
||||
|
||||
region.assign_advice(
|
||||
|| "odd input",
|
||||
self.input,
|
||||
0,
|
||||
|| value.ok_or(Error::Synthesis),
|
||||
)?;
|
||||
Ok(())
|
||||
},
|
||||
)
|
||||
}
|
||||
|
||||
fn load_even_lookup(
|
||||
&self,
|
||||
mut layouter: impl Layouter<F>,
|
||||
values: &[F],
|
||||
) -> Result<(), Error> {
|
||||
layouter.assign_region(
|
||||
|| "load values for even lookup table",
|
||||
|mut region| {
|
||||
for (offset, value) in values.iter().enumerate() {
|
||||
region.assign_advice(
|
||||
|| "even table value",
|
||||
self.table_even,
|
||||
offset,
|
||||
|| Ok(*value),
|
||||
)?;
|
||||
}
|
||||
|
||||
Ok(())
|
||||
},
|
||||
)
|
||||
}
|
||||
}
|
||||
|
||||
#[derive(Default)]
|
||||
struct MyCircuit<F: FieldExt> {
|
||||
even_lookup: Vec<F>,
|
||||
even_witnesses: Vec<Option<F>>,
|
||||
odd_witnesses: Vec<Option<F>>,
|
||||
}
|
||||
|
||||
impl<F: FieldExt> Circuit<F> for MyCircuit<F> {
|
||||
// Since we are using a single chip for everything, we can just reuse its config.
|
||||
type Config = MyConfig<F>;
|
||||
type FloorPlanner = SimpleFloorPlanner;
|
||||
|
||||
fn without_witnesses(&self) -> Self {
|
||||
Self::default()
|
||||
}
|
||||
|
||||
fn configure(meta: &mut ConstraintSystem<F>) -> Self::Config {
|
||||
Self::Config::configure(meta)
|
||||
}
|
||||
|
||||
fn synthesize(
|
||||
&self,
|
||||
config: Self::Config,
|
||||
mut layouter: impl Layouter<F>,
|
||||
) -> Result<(), Error> {
|
||||
// Load allowed values for even lookup table
|
||||
config.load_even_lookup(
|
||||
layouter.namespace(|| "witness even numbers"),
|
||||
&self.even_lookup,
|
||||
)?;
|
||||
|
||||
// Witness even numbers
|
||||
for even in self.even_witnesses.iter() {
|
||||
config.witness_even(layouter.namespace(|| "witness even numbers"), *even)?;
|
||||
}
|
||||
|
||||
// Witness odd numbers
|
||||
for odd in self.odd_witnesses.iter() {
|
||||
config.witness_odd(layouter.namespace(|| "witness odd numbers"), *odd)?;
|
||||
}
|
||||
|
||||
Ok(())
|
||||
}
|
||||
}
|
||||
|
||||
// Run MockProver.
|
||||
let k = 4;
|
||||
|
||||
// Prepare the private and public inputs to the circuit.
|
||||
let even_lookup = vec![
|
||||
Fp::from(0),
|
||||
Fp::from(2),
|
||||
Fp::from(4),
|
||||
Fp::from(6),
|
||||
Fp::from(8),
|
||||
];
|
||||
let odd_lookup = vec![
|
||||
Fp::from(1),
|
||||
Fp::from(3),
|
||||
Fp::from(5),
|
||||
Fp::from(7),
|
||||
Fp::from(9),
|
||||
];
|
||||
let even_witnesses = vec![Some(Fp::from(0)), Some(Fp::from(2)), Some(Fp::from(4))];
|
||||
let odd_witnesses = vec![Some(Fp::from(1)), Some(Fp::from(3)), Some(Fp::from(5))];
|
||||
|
||||
// Instantiate the circuit with the private inputs.
|
||||
let circuit = MyCircuit {
|
||||
even_lookup: even_lookup.clone(),
|
||||
even_witnesses,
|
||||
odd_witnesses,
|
||||
};
|
||||
|
||||
// Given the correct public input, our circuit will verify.
|
||||
let prover = MockProver::run(k, &circuit, vec![odd_lookup]).unwrap();
|
||||
assert_eq!(prover.verify(), Ok(()));
|
||||
|
||||
// If we pass in a public input containing only even numbers,
|
||||
// the odd number lookup will fail.
|
||||
let prover = MockProver::run(k, &circuit, vec![even_lookup]).unwrap();
|
||||
assert!(prover.verify().is_err())
|
||||
}
|
||||
Loading…
Reference in New Issue