Skip to content
This repository has been archived by the owner on May 3, 2024. It is now read-only.

Commit

Permalink
Merge branch 'main' of github.com:taikoxyz/zkevm-circuits into recursion
Browse files Browse the repository at this point in the history
  • Loading branch information
johntaiko committed Jun 23, 2023
2 parents 3fec999 + c85976c commit 002edb8
Show file tree
Hide file tree
Showing 21 changed files with 1,974 additions and 126 deletions.
5 changes: 3 additions & 2 deletions Cargo.lock

Some generated files are not rendered by default. Learn more about how customized files appear on GitHub.

252 changes: 252 additions & 0 deletions gadgets/src/is_equal.rs
Original file line number Diff line number Diff line change
@@ -0,0 +1,252 @@
//! IsEqual chip can be used to check equality of two expressions.

use eth_types::Field;
use halo2_proofs::{
circuit::{Chip, Region, Value},
plonk::{Advice, Column, ConstraintSystem, Error, Expression, VirtualCells},
};

use super::is_zero::{IsZeroChip, IsZeroInstruction};

/// Instruction that the IsEqual chip needs to implement.
pub trait IsEqualInstruction<F: Field> {
/// Assign lhs and rhs witnesses to the IsEqual chip's region.
fn assign(
&self,
region: &mut Region<'_, F>,
offset: usize,
lhs: Value<F>,
rhs: Value<F>,
) -> Result<(), Error>;
}

/// Config for the IsEqual chip.
#[derive(Clone, Debug)]
pub struct IsEqualConfig<F> {
/// Stores an IsZero chip.
pub is_zero_chip: IsZeroChip<F>,
/// Expression that denotes whether the chip evaluated to equal or not.
pub is_equal_expression: Expression<F>,
}

/// Chip that compares equality between two expressions.
#[derive(Clone, Debug)]
pub struct IsEqualChip<F> {
/// Config for the IsEqual chip.
pub(crate) config: IsEqualConfig<F>,
}

impl<F: Field> IsEqualChip<F> {
/// Configure the IsEqual chip.
pub fn configure(
meta: &mut ConstraintSystem<F>,
value_inv: impl FnOnce(&mut ConstraintSystem<F>) -> Column<Advice>,
q_enable: impl FnOnce(&mut VirtualCells<'_, F>) -> Expression<F>,
lhs: impl FnOnce(&mut VirtualCells<'_, F>) -> Expression<F>,
rhs: impl FnOnce(&mut VirtualCells<'_, F>) -> Expression<F>,
) -> IsEqualConfig<F> {
let value = |meta: &mut VirtualCells<F>| lhs(meta) - rhs(meta);
let value_inv = value_inv(meta);
let is_zero_config = IsZeroChip::configure(meta, q_enable, value, value_inv);
let is_equal_expression = is_zero_config.is_zero_expression.clone();

IsEqualConfig {
is_zero_chip: IsZeroChip::construct(is_zero_config),
is_equal_expression,
}
}

/// Construct an IsEqual chip given a config.
pub fn construct(config: IsEqualConfig<F>) -> Self {
Self { config }
}
}

impl<F: Field> IsEqualInstruction<F> for IsEqualChip<F> {
fn assign(
&self,
region: &mut Region<'_, F>,
offset: usize,
lhs: Value<F>,
rhs: Value<F>,
) -> Result<(), Error> {
self.config.is_zero_chip.assign(region, offset, lhs - rhs)?;

Ok(())
}
}

impl<F: Field> Chip<F> for IsEqualChip<F> {
type Config = IsEqualConfig<F>;
type Loaded = ();

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

fn loaded(&self) -> &Self::Loaded {
&()
}
}

#[cfg(test)]
mod tests {
use std::marker::PhantomData;

use eth_types::Field;
use halo2_proofs::{
circuit::{Layouter, SimpleFloorPlanner, Value},
dev::MockProver,
halo2curves::bn256::Fr as Fp,
plonk::{Advice, Circuit, Column, ConstraintSystem, Error, Selector, VirtualCells},
poly::Rotation,
};
use rand::Rng;

use super::{IsEqualChip, IsEqualConfig, IsEqualInstruction};
use crate::util::Expr;

#[derive(Clone, Debug)]
struct TestCircuitConfig<F, const RHS: u64> {
q_enable: Selector,
value: Column<Advice>,
check: Column<Advice>,
is_equal: IsEqualConfig<F>,
}

#[derive(Default)]
struct TestCircuit<F: Field, const RHS: u64> {
values: Vec<u64>,
checks: Vec<bool>,
_marker: PhantomData<F>,
}

impl<F: Field, const RHS: u64> Circuit<F> for TestCircuit<F, RHS> {
type Config = TestCircuitConfig<F, RHS>;
type FloorPlanner = SimpleFloorPlanner;
type Params = ();

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

fn configure(meta: &mut ConstraintSystem<F>) -> Self::Config {
let q_enable = meta.complex_selector();
let value = meta.advice_column();
let check = meta.advice_column();

let lhs = |meta: &mut VirtualCells<F>| meta.query_advice(value, Rotation::cur());
let rhs = |_meta: &mut VirtualCells<F>| RHS.expr();

let is_equal = IsEqualChip::configure(
meta,
|meta| meta.advice_column(),
|meta| meta.query_selector(q_enable),
lhs,
rhs,
);

let config = Self::Config {
q_enable,
value,
check,
is_equal,
};

meta.create_gate("check is_equal", |meta| {
let q_enable = meta.query_selector(q_enable);

let check = meta.query_advice(check, Rotation::cur());

vec![q_enable * (config.is_equal.is_equal_expression.clone() - check)]
});

config
}

fn synthesize(
&self,
config: Self::Config,
mut layouter: impl Layouter<F>,
) -> Result<(), Error> {
let chip = IsEqualChip::construct(config.is_equal.clone());

layouter.assign_region(
|| "witness",
|mut region| {
let checks = self.checks.clone();

for (idx, (value, check)) in self.values.iter().cloned().zip(checks).enumerate()
{
region.assign_advice(
|| "value",
config.value,
idx + 1,
|| Value::known(F::from(value)),
)?;
region.assign_advice(
|| "check",
config.check,
idx + 1,
|| Value::known(F::from(check as u64)),
)?;
config.q_enable.enable(&mut region, idx + 1)?;
chip.assign(
&mut region,
idx + 1,
Value::known(F::from(value)),
Value::known(F::from(RHS)),
)?;
}

Ok(())
},
)
}
}

macro_rules! try_test {
($values:expr, $checks:expr, $rhs:expr, $is_ok_or_err:ident) => {
let k = usize::BITS - $values.len().leading_zeros() + 2;
let circuit = TestCircuit::<Fp, $rhs> {
values: $values,
checks: $checks,
_marker: PhantomData,
};
let prover = MockProver::<Fp>::run(k, &circuit, vec![]).unwrap();
assert!(prover.verify().$is_ok_or_err());
};
}

fn random() -> u64 {
rand::thread_rng().gen::<u64>()
}

#[test]
fn is_equal_gadget() {
try_test!(
vec![random(), 123, random(), 123, 123, random()],
vec![false, true, false, true, true, false],
123,
is_ok
);
try_test!(
vec![random(), 321321, 321321, random()],
vec![false, true, true, false],
321321,
is_ok
);
try_test!(
vec![random(), random(), random(), 1846123],
vec![false, false, false, true],
1846123,
is_ok
);
try_test!(
vec![123, 234, 345, 456],
vec![true, true, false, false],
234,
is_err
);
}
}
1 change: 1 addition & 0 deletions gadgets/src/lib.rs
Original file line number Diff line number Diff line change
Expand Up @@ -13,6 +13,7 @@

pub mod batched_is_zero;
pub mod binary_number;
pub mod is_equal;
pub mod is_zero;
pub mod less_than;
pub mod mul_add;
Expand Down
3 changes: 2 additions & 1 deletion zkevm-circuits/Cargo.toml
Original file line number Diff line number Diff line change
Expand Up @@ -37,6 +37,7 @@ rand_chacha = "0.3"
snark-verifier = { git = "https://github.com/brechtpd/snark-verifier.git", branch = "feat/add-sdk", default-features = false, features = ["loader_halo2", "system_halo2", "loader_evm", "parallel"] }
snark-verifier-sdk = { git = "https://github.com/brechtpd/snark-verifier.git", branch = "feat/add-sdk", default-features = false, features = ["loader_halo2", "loader_evm", "parallel", "display", "halo2_circuit_params"] }
cli-table = { version = "0.4", optional = true }
once_cell = "1.17.1"

[dev-dependencies]
bus-mapping = { path = "../bus-mapping", features = ["test"] }
Expand All @@ -58,4 +59,4 @@ stats = ["warn-unimplemented", "dep:cli-table"]

[[bin]]
name = "stats"
required-features = ["stats"]
required-features = ["stats"]
Loading

0 comments on commit 002edb8

Please sign in to comment.