mirror of https://github.com/zcash/halo2.git
Fix examples to account for public input API changes.
This commit is contained in:
parent
b246897a8d
commit
0766983686
|
@ -5,7 +5,6 @@ use std::marker::PhantomData;
|
||||||
use halo2::{
|
use halo2::{
|
||||||
arithmetic::FieldExt,
|
arithmetic::FieldExt,
|
||||||
circuit::{Cell, Chip, Layouter, Region, SimpleFloorPlanner},
|
circuit::{Cell, Chip, Layouter, Region, SimpleFloorPlanner},
|
||||||
dev::VerifyFailure,
|
|
||||||
plonk::{Advice, Circuit, Column, ConstraintSystem, Error, Instance, Selector},
|
plonk::{Advice, Circuit, Column, ConstraintSystem, Error, Instance, Selector},
|
||||||
poly::Rotation,
|
poly::Rotation,
|
||||||
};
|
};
|
||||||
|
@ -50,14 +49,14 @@ struct FieldConfig {
|
||||||
/// the circuit.
|
/// the circuit.
|
||||||
advice: [Column<Advice>; 2],
|
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
|
// 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.
|
// any constraints on cells where `NumericInstructions::mul` is not being used.
|
||||||
// This is important when building larger circuits, where columns are used by
|
// This is important when building larger circuits, where columns are used by
|
||||||
// multiple sets of instructions.
|
// multiple sets of instructions.
|
||||||
s_mul: Selector,
|
s_mul: Selector,
|
||||||
|
|
||||||
// The selector for the public-input gate, which uses one of the advice columns.
|
|
||||||
s_pub: Selector,
|
|
||||||
}
|
}
|
||||||
|
|
||||||
impl<F: FieldExt> FieldChip<F> {
|
impl<F: FieldExt> FieldChip<F> {
|
||||||
|
@ -73,11 +72,11 @@ impl<F: FieldExt> FieldChip<F> {
|
||||||
advice: [Column<Advice>; 2],
|
advice: [Column<Advice>; 2],
|
||||||
instance: Column<Instance>,
|
instance: Column<Instance>,
|
||||||
) -> <Self as Chip<F>>::Config {
|
) -> <Self as Chip<F>>::Config {
|
||||||
|
meta.enable_equality(instance.into());
|
||||||
for column in &advice {
|
for column in &advice {
|
||||||
meta.enable_equality((*column).into());
|
meta.enable_equality((*column).into());
|
||||||
}
|
}
|
||||||
let s_mul = meta.selector();
|
let s_mul = meta.selector();
|
||||||
let s_pub = meta.selector();
|
|
||||||
|
|
||||||
// Define our multiplication gate!
|
// Define our multiplication gate!
|
||||||
meta.create_gate("mul", |meta| {
|
meta.create_gate("mul", |meta| {
|
||||||
|
@ -109,23 +108,10 @@ impl<F: FieldExt> FieldChip<F> {
|
||||||
vec![s_mul * (lhs * rhs + out * -F::one())]
|
vec![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_instance(instance, Rotation::cur());
|
|
||||||
let s = meta.query_selector(s_pub);
|
|
||||||
|
|
||||||
// We simply constrain the advice cell to be equal to the instance cell,
|
|
||||||
// when the selector is enabled.
|
|
||||||
vec![s * (p + a * -F::one())]
|
|
||||||
});
|
|
||||||
|
|
||||||
FieldConfig {
|
FieldConfig {
|
||||||
advice,
|
advice,
|
||||||
|
instance,
|
||||||
s_mul,
|
s_mul,
|
||||||
s_pub,
|
|
||||||
}
|
}
|
||||||
}
|
}
|
||||||
}
|
}
|
||||||
|
@ -239,26 +225,7 @@ impl<F: FieldExt> NumericInstructions<F> for FieldChip<F> {
|
||||||
fn expose_public(&self, mut layouter: impl Layouter<F>, num: Self::Num) -> Result<(), Error> {
|
fn expose_public(&self, mut layouter: impl Layouter<F>, num: Self::Num) -> Result<(), Error> {
|
||||||
let config = self.config();
|
let config = self.config();
|
||||||
|
|
||||||
layouter.assign_region(
|
layouter.constrain_instance(num.cell, config.instance, 0)
|
||||||
|| "expose public",
|
|
||||||
|mut region: Region<'_, F>| {
|
|
||||||
// Enable the public-input gate.
|
|
||||||
config.s_pub.enable(&mut region, 0)?;
|
|
||||||
|
|
||||||
// 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(num.cell, out)?;
|
|
||||||
|
|
||||||
// We don't assign to the instance column inside the circuit;
|
|
||||||
// the mapping of public inputs to cells is provided to the prover.
|
|
||||||
Ok(())
|
|
||||||
},
|
|
||||||
)
|
|
||||||
}
|
}
|
||||||
}
|
}
|
||||||
// ANCHOR_END: instructions-impl
|
// ANCHOR_END: instructions-impl
|
||||||
|
@ -342,24 +309,18 @@ fn main() {
|
||||||
b: Some(b),
|
b: Some(b),
|
||||||
};
|
};
|
||||||
|
|
||||||
// Arrange the public input. We expose the multiplication result in row 6
|
// 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.
|
// of the instance 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[0] = c;
|
||||||
|
|
||||||
// Given the correct public input, our circuit will verify.
|
// Given the correct public input, our circuit will verify.
|
||||||
let prover = MockProver::run(k, &circuit, vec![public_inputs.clone()]).unwrap();
|
let prover = MockProver::run(k, &circuit, vec![public_inputs.clone()]).unwrap();
|
||||||
assert_eq!(prover.verify(), Ok(()));
|
assert_eq!(prover.verify(), Ok(()));
|
||||||
|
|
||||||
// If we try some other public input, the proof will fail!
|
// If we try some other public input, the proof will fail!
|
||||||
public_inputs[6] += Fp::one();
|
public_inputs[0] += Fp::one();
|
||||||
let prover = MockProver::run(k, &circuit, vec![public_inputs]).unwrap();
|
let prover = MockProver::run(k, &circuit, vec![public_inputs]).unwrap();
|
||||||
assert_eq!(
|
assert!(prover.verify().is_err());
|
||||||
prover.verify(),
|
|
||||||
Err(vec![VerifyFailure::Constraint {
|
|
||||||
constraint: ((1, "public input").into(), 0, "").into(),
|
|
||||||
row: 6,
|
|
||||||
}])
|
|
||||||
);
|
|
||||||
// ANCHOR_END: test-circuit
|
// ANCHOR_END: test-circuit
|
||||||
}
|
}
|
||||||
|
|
|
@ -5,7 +5,6 @@ use std::marker::PhantomData;
|
||||||
use halo2::{
|
use halo2::{
|
||||||
arithmetic::FieldExt,
|
arithmetic::FieldExt,
|
||||||
circuit::{Cell, Chip, Layouter, Region, SimpleFloorPlanner},
|
circuit::{Cell, Chip, Layouter, Region, SimpleFloorPlanner},
|
||||||
dev::VerifyFailure,
|
|
||||||
plonk::{Advice, Circuit, Column, ConstraintSystem, Error, Instance, Selector},
|
plonk::{Advice, Circuit, Column, ConstraintSystem, Error, Instance, Selector},
|
||||||
poly::Rotation,
|
poly::Rotation,
|
||||||
};
|
};
|
||||||
|
@ -43,6 +42,7 @@ trait FieldInstructions<F: FieldExt>: AddInstructions<F> + MulInstructions<F> {
|
||||||
&self,
|
&self,
|
||||||
layouter: impl Layouter<F>,
|
layouter: impl Layouter<F>,
|
||||||
num: <Self as FieldInstructions<F>>::Num,
|
num: <Self as FieldInstructions<F>>::Num,
|
||||||
|
row: usize,
|
||||||
) -> Result<(), Error>;
|
) -> Result<(), Error>;
|
||||||
}
|
}
|
||||||
// ANCHOR_END: field-instructions
|
// ANCHOR_END: field-instructions
|
||||||
|
@ -87,8 +87,8 @@ struct FieldConfig {
|
||||||
/// the circuit.
|
/// the circuit.
|
||||||
advice: [Column<Advice>; 2],
|
advice: [Column<Advice>; 2],
|
||||||
|
|
||||||
// The selector for the public-input gate, which uses one of the advice columns.
|
/// Public inputs
|
||||||
s_pub: Selector,
|
instance: Column<Instance>,
|
||||||
|
|
||||||
add_config: AddConfig,
|
add_config: AddConfig,
|
||||||
mul_config: MulConfig,
|
mul_config: MulConfig,
|
||||||
|
@ -173,10 +173,7 @@ impl<F: FieldExt> AddChip<F> {
|
||||||
vec![s_add * (lhs + rhs + out * -F::one())]
|
vec![s_add * (lhs + rhs + out * -F::one())]
|
||||||
});
|
});
|
||||||
|
|
||||||
AddConfig {
|
AddConfig { advice, s_add }
|
||||||
advice,
|
|
||||||
s_add,
|
|
||||||
}
|
|
||||||
}
|
}
|
||||||
}
|
}
|
||||||
// ANCHOR END: add-chip-impl
|
// ANCHOR END: add-chip-impl
|
||||||
|
@ -317,10 +314,7 @@ impl<F: FieldExt> MulChip<F> {
|
||||||
vec![s_mul * (lhs * rhs + out * -F::one())]
|
vec![s_mul * (lhs * rhs + out * -F::one())]
|
||||||
});
|
});
|
||||||
|
|
||||||
MulConfig {
|
MulConfig { advice, s_mul }
|
||||||
advice,
|
|
||||||
s_mul,
|
|
||||||
}
|
|
||||||
}
|
}
|
||||||
}
|
}
|
||||||
// ANCHOR_END: mul-chip-impl
|
// ANCHOR_END: mul-chip-impl
|
||||||
|
@ -429,27 +423,14 @@ impl<F: FieldExt> FieldChip<F> {
|
||||||
advice: [Column<Advice>; 2],
|
advice: [Column<Advice>; 2],
|
||||||
instance: Column<Instance>,
|
instance: Column<Instance>,
|
||||||
) -> <Self as Chip<F>>::Config {
|
) -> <Self as Chip<F>>::Config {
|
||||||
let s_pub = meta.selector();
|
|
||||||
|
|
||||||
// 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_instance(instance, Rotation::cur());
|
|
||||||
let s = meta.query_selector(s_pub);
|
|
||||||
|
|
||||||
// We simply constrain the advice cell to be equal to the instance cell,
|
|
||||||
// when the selector is enabled.
|
|
||||||
vec![s * (p + a * -F::one())]
|
|
||||||
});
|
|
||||||
|
|
||||||
let add_config = AddChip::configure(meta, advice);
|
let add_config = AddChip::configure(meta, advice);
|
||||||
let mul_config = MulChip::configure(meta, advice);
|
let mul_config = MulChip::configure(meta, advice);
|
||||||
|
|
||||||
|
meta.enable_equality(instance.into());
|
||||||
|
|
||||||
FieldConfig {
|
FieldConfig {
|
||||||
advice,
|
advice,
|
||||||
s_pub,
|
instance,
|
||||||
add_config,
|
add_config,
|
||||||
mul_config,
|
mul_config,
|
||||||
}
|
}
|
||||||
|
@ -501,29 +482,11 @@ impl<F: FieldExt> FieldInstructions<F> for FieldChip<F> {
|
||||||
&self,
|
&self,
|
||||||
mut layouter: impl Layouter<F>,
|
mut layouter: impl Layouter<F>,
|
||||||
num: <Self as FieldInstructions<F>>::Num,
|
num: <Self as FieldInstructions<F>>::Num,
|
||||||
|
row: usize,
|
||||||
) -> Result<(), Error> {
|
) -> Result<(), Error> {
|
||||||
let config = self.config();
|
let config = self.config();
|
||||||
|
|
||||||
layouter.assign_region(
|
layouter.constrain_instance(num.cell, config.instance, row)
|
||||||
|| "expose public",
|
|
||||||
|mut region: Region<'_, F>| {
|
|
||||||
// Enable the public-input gate.
|
|
||||||
config.s_pub.enable(&mut region, 0)?;
|
|
||||||
|
|
||||||
// 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(num.cell, out)?;
|
|
||||||
|
|
||||||
// We don't assign to the instance column inside the circuit;
|
|
||||||
// the mapping of public inputs to cells is provided to the prover.
|
|
||||||
Ok(())
|
|
||||||
},
|
|
||||||
)
|
|
||||||
}
|
}
|
||||||
}
|
}
|
||||||
// ANCHOR_END: field-instructions-impl
|
// ANCHOR_END: field-instructions-impl
|
||||||
|
@ -576,7 +539,7 @@ impl<F: FieldExt> Circuit<F> for MyCircuit<F> {
|
||||||
let d = field_chip.add_and_mul(&mut layouter, a, b, c)?;
|
let d = field_chip.add_and_mul(&mut layouter, a, b, c)?;
|
||||||
|
|
||||||
// Expose the result as a public input to the circuit.
|
// Expose the result as a public input to the circuit.
|
||||||
field_chip.expose_public(layouter.namespace(|| "expose d"), d)
|
field_chip.expose_public(layouter.namespace(|| "expose d"), d, 0)
|
||||||
}
|
}
|
||||||
}
|
}
|
||||||
// ANCHOR_END: circuit
|
// ANCHOR_END: circuit
|
||||||
|
@ -603,24 +566,18 @@ fn main() {
|
||||||
c: Some(c),
|
c: Some(c),
|
||||||
};
|
};
|
||||||
|
|
||||||
// Arrange the public input. We expose the multiplication result in row 6
|
// 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.
|
// of the instance 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[7] = d;
|
public_inputs[0] = d;
|
||||||
|
|
||||||
// Given the correct public input, our circuit will verify.
|
// Given the correct public input, our circuit will verify.
|
||||||
let prover = MockProver::run(k, &circuit, vec![public_inputs.clone()]).unwrap();
|
let prover = MockProver::run(k, &circuit, vec![public_inputs.clone()]).unwrap();
|
||||||
assert_eq!(prover.verify(), Ok(()));
|
assert_eq!(prover.verify(), Ok(()));
|
||||||
|
|
||||||
// If we try some other public input, the proof will fail!
|
// If we try some other public input, the proof will fail!
|
||||||
public_inputs[7] += Fp::one();
|
public_inputs[0] += Fp::one();
|
||||||
let prover = MockProver::run(k, &circuit, vec![public_inputs]).unwrap();
|
let prover = MockProver::run(k, &circuit, vec![public_inputs]).unwrap();
|
||||||
assert_eq!(
|
assert!(prover.verify().is_err());
|
||||||
prover.verify(),
|
|
||||||
Err(vec![VerifyFailure::Constraint {
|
|
||||||
constraint: ((0, "public input").into(), 0, "").into(),
|
|
||||||
row: 7,
|
|
||||||
}])
|
|
||||||
);
|
|
||||||
// ANCHOR_END: test-circuit
|
// ANCHOR_END: test-circuit
|
||||||
}
|
}
|
||||||
|
|
Loading…
Reference in New Issue