Skip to content
New issue

Have a question about this project? Sign up for a free GitHub account to open an issue and contact its maintainers and the community.

By clicking “Sign up for GitHub”, you agree to our terms of service and privacy statement. We’ll occasionally send you account related emails.

Already on GitHub? Sign in to your account

feat: send sync region #180

Merged
Merged
Show file tree
Hide file tree
Changes from all commits
Commits
Show all changes
28 commits
Select commit Hold shift + click to select a range
5eebade
feat: send / sync region
alexander-camuto Apr 28, 2023
0564321
Update layout.rs
alexander-camuto Apr 29, 2023
ec58daa
update
alexander-camuto Apr 29, 2023
73bfe3b
lol
alexander-camuto Apr 29, 2023
582cca3
debug
alexander-camuto Apr 30, 2023
cc7a789
Update keygen.rs
alexander-camuto Apr 30, 2023
333bc77
Update keygen.rs
alexander-camuto Apr 30, 2023
e079474
Update keygen.rs
alexander-camuto Apr 30, 2023
c1fec19
Update keygen.rs
alexander-camuto Apr 30, 2023
94808de
thread-safe-region feature flag
alexander-camuto May 8, 2023
d01ced2
cleanup
alexander-camuto May 8, 2023
0933c69
patch dev-graph
alexander-camuto May 8, 2023
e3d88fb
patch non-determinism in mapping creation
alexander-camuto May 9, 2023
b2dd7a8
reduce mem usage for vk and pk
alexander-camuto May 10, 2023
6e503f1
mock proving examples
alexander-camuto May 13, 2023
545d48d
swap for hashmap for insertion speed
alexander-camuto May 13, 2023
4810921
reduce update overhead
alexander-camuto May 13, 2023
37047ed
replace BTree with Vec
alexander-camuto May 13, 2023
2633e8c
add benchmarks
alexander-camuto May 15, 2023
4b89de2
make the benchmarks massive
alexander-camuto May 15, 2023
c051697
patch clippy
alexander-camuto May 16, 2023
16a3dd4
simplify lifetimes
alexander-camuto May 16, 2023
d2c8bef
patch benches
alexander-camuto May 18, 2023
f2fb1df
Update halo2_proofs/src/plonk/permutation/keygen.rs
alexander-camuto May 19, 2023
fe0882d
Update halo2_proofs/examples/vector-mul.rs
alexander-camuto May 19, 2023
1d9c8c6
rm benches
alexander-camuto May 19, 2023
da218ca
order once
alexander-camuto May 25, 2023
f6ef249
patch lints
alexander-camuto May 25, 2023
File filter

Filter by extension

Filter by extension


Conversations
Failed to load comments.
Loading
Jump to
Jump to file
Failed to load files.
Loading
Diff view
Diff view
3 changes: 3 additions & 0 deletions halo2_proofs/Cargo.toml
Original file line number Diff line number Diff line change
Expand Up @@ -77,6 +77,7 @@ getrandom = { version = "0.2", features = ["js"] }
default = ["batch"]
dev-graph = ["plotters", "tabbycat"]
gadget-traces = ["backtrace"]
thread-safe-region = []
sanity-checks = []
batch = ["rand_core/getrandom"]
circuit-params = []
Expand All @@ -87,3 +88,5 @@ bench = false
[[example]]
name = "circuit-layout"
required-features = ["dev-graph"]


350 changes: 350 additions & 0 deletions halo2_proofs/examples/vector-mul.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_private(
&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_private(
&self,
mut layouter: impl Layouter<F>,
values: &[Value<F>],
) -> Result<Vec<Self::Num>, Error> {
let config = self.config();

layouter.assign_region(
|| "load private",
|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 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(
alexander-camuto marked this conversation as resolved.
Show resolved Hide resolved
|| "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.advice_column(),
meta.advice_column(),
meta.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_private(layouter.namespace(|| "load a"), &self.a)?;
let b = field_chip.load_private(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
}
Loading