Skip to content

Commit

Permalink
feat: optional unblinded advice
Browse files Browse the repository at this point in the history
  • Loading branch information
alexander-camuto committed Oct 19, 2023
1 parent 0c3e3b5 commit b4320a2
Show file tree
Hide file tree
Showing 5 changed files with 389 additions and 13 deletions.
6 changes: 3 additions & 3 deletions halo2_proofs/examples/shuffle.rs
Original file line number Diff line number Diff line change
Expand Up @@ -57,11 +57,11 @@ impl<const W: usize> MyConfig<W> {
fn configure<F: Field>(meta: &mut ConstraintSystem<F>) -> Self {
let [q_shuffle, q_first, q_last] = [(); 3].map(|_| meta.selector());
// First phase
let original = [(); W].map(|_| meta.advice_column_in(FirstPhase));
let shuffled = [(); W].map(|_| meta.advice_column_in(FirstPhase));
let original = [(); W].map(|_| meta.advice_column_in(FirstPhase, true));
let shuffled = [(); W].map(|_| meta.advice_column_in(FirstPhase, true));
let [theta, gamma] = [(); 2].map(|_| meta.challenge_usable_after(FirstPhase));
// Second phase
let z = meta.advice_column_in(SecondPhase);
let z = meta.advice_column_in(SecondPhase, true);

meta.create_gate("z should start with 1", |_| {
let one = Expression::Constant(F::ONE);
Expand Down
350 changes: 350 additions & 0 deletions halo2_proofs/examples/vector-mul-unblinded.rs
Original file line number Diff line number Diff line change
@@ -0,0 +1,350 @@
use std::marker::PhantomData;

use halo2_proofs::{
arithmetic::Field,
circuit::{AssignedCell, Chip, Layouter, Region, SimpleFloorPlanner, Value},
plonk::{Advice, Circuit, Column, ConstraintSystem, Error, Instance, Selector},
poly::Rotation,
};

// ANCHOR: instructions
trait NumericInstructions<F: Field>: Chip<F> {
/// Variable representing a number.
type Num;

/// Loads a number into the circuit as a private input.
fn load_unblinded(
&self,
layouter: impl Layouter<F>,
a: &[Value<F>],
) -> Result<Vec<Self::Num>, Error>;

/// Returns `c = a * b`. The caller is responsible for ensuring that `a.len() == b.len()`.
fn mul(
&self,
layouter: impl Layouter<F>,
a: &[Self::Num],
b: &[Self::Num],
) -> Result<Vec<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>;
}
// ANCHOR_END: instructions

// ANCHOR: chip
/// 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>,
}
// ANCHOR_END: chip

// ANCHOR: chip-config
/// 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>; 3],

/// 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,
}

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>; 3],
instance: Column<Instance>,
) -> <Self as Chip<F>>::Config {
meta.enable_equality(instance);
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 | a2 | s_mul |
// |-----|-----|-----|-------|
// | lhs | rhs | out | s_mul |
//
// 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[2], Rotation::cur());
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,
}
}
}
// ANCHOR_END: chip-config

// ANCHOR: chip-impl
impl<F: Field> Chip<F> for FieldChip<F> {
type Config = FieldConfig;
type Loaded = ();

fn config(&self) -> &Self::Config {
&self.config
}

fn loaded(&self) -> &Self::Loaded {
&()
}
}
// ANCHOR_END: chip-impl

// ANCHOR: instructions-impl
/// A variable representing a number.
#[derive(Clone, Debug)]
struct Number<F: Field>(AssignedCell<F, F>);

impl<F: Field> NumericInstructions<F> for FieldChip<F> {
type Num = Number<F>;

fn load_unblinded(
&self,
mut layouter: impl Layouter<F>,
values: &[Value<F>],
) -> Result<Vec<Self::Num>, Error> {
let config = self.config();

layouter.assign_region(
|| "load unblinded",
|mut region| {
values
.iter()
.enumerate()
.map(|(i, value)| {
region
.assign_advice(|| "private input", config.advice[0], i, || *value)
.map(Number)
})
.collect()
},
)
}

fn mul(
&self,
mut layouter: impl Layouter<F>,
a: &[Self::Num],
b: &[Self::Num],
) -> Result<Vec<Self::Num>, Error> {
let config = self.config();
assert_eq!(a.len(), b.len());

#[cfg(feature = "thread-safe-region")]
{
use maybe_rayon::prelude::{
IndexedParallelIterator, IntoParallelRefIterator, ParallelIterator,
};
layouter.assign_region(
|| "mul",
|region: Region<'_, F>| {
let thread_safe_region = std::sync::Mutex::new(region);
a.par_iter()
.zip(b.par_iter())
.enumerate()
.map(|(i, (a, b))| {
let mut region = thread_safe_region.lock().unwrap();

config.s_mul.enable(&mut region, i)?;

a.0.copy_advice(|| "lhs", &mut region, config.advice[0], i)?;
b.0.copy_advice(|| "rhs", &mut region, config.advice[1], i)?;

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[2], i, || value)
.map(Number)
})
.collect()
},
)
}

#[cfg(not(feature = "thread-safe-region"))]
layouter.assign_region(
|| "mul",
|mut region: Region<'_, F>| {
a.iter()
.zip(b.iter())
.enumerate()
.map(|(i, (a, b))| {
config.s_mul.enable(&mut region, i)?;

a.0.copy_advice(|| "lhs", &mut region, config.advice[0], i)?;
b.0.copy_advice(|| "rhs", &mut region, config.advice[1], i)?;

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[2], i, || value)
.map(Number)
})
.collect()
},
)
}

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)
}
}
// ANCHOR_END: instructions-impl

// ANCHOR: circuit
/// 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> {
a: Vec<Value<F>>,
b: Vec<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;
#[cfg(feature = "circuit-params")]
type Params = ();

fn without_witnesses(&self) -> Self {
Self::default()
}

fn configure(meta: &mut ConstraintSystem<F>) -> Self::Config {
// We create the three advice columns that FieldChip uses for I/O.
let advice = [
meta.unblinded_advice_column(),
meta.unblinded_advice_column(),
meta.unblinded_advice_column(),
];

// We also need an instance column to store public inputs.
let instance = meta.instance_column();

FieldChip::configure(meta, advice, instance)
}

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_unblinded(layouter.namespace(|| "load a"), &self.a)?;
let b = field_chip.load_unblinded(layouter.namespace(|| "load b"), &self.b)?;

let ab = field_chip.mul(layouter.namespace(|| "a * b"), &a, &b)?;

for (i, c) in ab.iter().enumerate() {
// Expose the result as a public input to the circuit.
field_chip.expose_public(layouter.namespace(|| "expose c"), c, i)?;
}
Ok(())
}
}
// ANCHOR_END: circuit

fn main() {
use halo2_proofs::dev::MockProver;
use halo2curves::pasta::Fp;

const N: usize = 20000;
// 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 = 16;

// Prepare the private and public inputs to the circuit!
let a = [Fp::from(2); N];
let b = [Fp::from(3); N];
let c: Vec<Fp> = a.iter().zip(b).map(|(&a, b)| a * b).collect();

// Instantiate the circuit with the private inputs.
let circuit = MyCircuit {
a: a.iter().map(|&x| Value::known(x)).collect(),
b: b.iter().map(|&x| Value::known(x)).collect(),
};

// 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 = c;

let start = std::time::Instant::now();
// 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(()));
println!("positive test took {:?}", start.elapsed());

// If we try some other public input, the proof will fail!
let start = std::time::Instant::now();
public_inputs[0] += Fp::one();
let prover = MockProver::run(k, &circuit, vec![public_inputs]).unwrap();
assert!(prover.verify().is_err());
println!("negative test took {:?}", start.elapsed());
// ANCHOR_END: test-circuit
}
4 changes: 2 additions & 2 deletions halo2_proofs/src/dev.rs
Original file line number Diff line number Diff line change
Expand Up @@ -2241,7 +2241,7 @@ mod tests {
(
(
Any::Advice(Advice {
phase: FirstPhase.to_sealed()
phase: FirstPhase.to_sealed(),
}),
0
)
Expand Down Expand Up @@ -2269,7 +2269,7 @@ mod tests {
(
(
Any::Advice(Advice {
phase: FirstPhase.to_sealed()
phase: FirstPhase.to_sealed(),
}),
2
)
Expand Down
Loading

0 comments on commit b4320a2

Please sign in to comment.