Skip to content

Commit

Permalink
Add Byte Range Checks in LtChip (privacy-scaling-explorations#1364)
Browse files Browse the repository at this point in the history
### Description

Add Byte Range Checks in `LtChip`. This PR modifies the `LtChip`:

- Added Fixed Column `u8` to the configuration of the chip 
- Added a lookup constraint between each `diff` advice column and the
`u8` column
- Added `load` function that assigns each integer from 0 to 255 (8bits)
to the `u8` column

Furthermore, the following have been applied to the tests: 

- In `less_than` testing, the circuit now takes `k = 9` to support a
higher number of rows
- In `copy_circuit` testing, the `assign_copy_events` function now calls
`load` on the `lt_chip` to load the `u8` column
 
### Issue Link

Related to privacy-scaling-explorations#916 

### Type of change

- [x] Bug fix (non-breaking change which fixes an issue)

### How Has This Been Tested?

`make test-all`

---------

Co-authored-by: adria0.eth <[email protected]>
Co-authored-by: Chih Cheng Liang <[email protected]>
  • Loading branch information
3 people authored May 1, 2023
1 parent 77bc7e5 commit 4669a87
Show file tree
Hide file tree
Showing 2 changed files with 51 additions and 6 deletions.
55 changes: 49 additions & 6 deletions gadgets/src/less_than.rs
Original file line number Diff line number Diff line change
Expand Up @@ -3,8 +3,8 @@
use eth_types::Field;
use halo2_proofs::{
arithmetic::FieldExt,
circuit::{Chip, Region, Value},
plonk::{Advice, Column, ConstraintSystem, Error, Expression, VirtualCells},
circuit::{Chip, Layouter, Region, Value},
plonk::{Advice, Column, ConstraintSystem, Error, Expression, Fixed, VirtualCells},
poly::Rotation,
};

Expand All @@ -23,6 +23,9 @@ pub trait LtInstruction<F: FieldExt> {
lhs: F,
rhs: F,
) -> Result<(), Error>;

/// Load the u8 lookup table.
fn load(&self, layouter: &mut impl Layouter<F>) -> Result<(), Error>;
}

/// Config for the Lt chip.
Expand All @@ -31,8 +34,9 @@ pub struct LtConfig<F, const N_BYTES: usize> {
/// Denotes the lt outcome. If lhs < rhs then lt == 1, otherwise lt == 0.
pub lt: Column<Advice>,
/// Denotes the bytes representation of the difference between lhs and rhs.
/// Note that the range of each byte is not checked by this config.
pub diff: [Column<Advice>; N_BYTES],
/// Denotes the range within which each byte should lie.
pub u8: Column<Fixed>,
/// Denotes the range within which both lhs and rhs lie.
pub range: F,
}
Expand Down Expand Up @@ -61,6 +65,7 @@ impl<F: Field, const N_BYTES: usize> LtChip<F, N_BYTES> {
let lt = meta.advice_column();
let diff = [(); N_BYTES].map(|_| meta.advice_column());
let range = pow_of_two(N_BYTES * 8);
let u8 = meta.fixed_column();

meta.create_gate("lt gate", |meta| {
let q_enable = q_enable(meta);
Expand All @@ -81,7 +86,22 @@ impl<F: Field, const N_BYTES: usize> LtChip<F, N_BYTES> {
.map(move |poly| q_enable.clone() * poly)
});

LtConfig { lt, diff, range }
meta.annotate_lookup_any_column(u8, || "LOOKUP_u8");

diff[0..N_BYTES].iter().for_each(|column| {
meta.lookup_any("range check for u8", |meta| {
let u8_cell = meta.query_advice(*column, Rotation::cur());
let u8_range = meta.query_fixed(u8, Rotation::cur());
vec![(u8_cell, u8_range)]
});
});

LtConfig {
lt,
diff,
range,
u8,
}
}

/// Constructs a Lt chip given a config.
Expand Down Expand Up @@ -122,6 +142,25 @@ impl<F: Field, const N_BYTES: usize> LtInstruction<F> for LtChip<F, N_BYTES> {

Ok(())
}

fn load(&self, layouter: &mut impl Layouter<F>) -> Result<(), Error> {
const RANGE: usize = 256;

layouter.assign_region(
|| "load u8 range check table",
|mut region| {
for i in 0..RANGE {
region.assign_fixed(
|| "assign cell in fixed column",
self.config.u8,
i,
|| Value::known(F::from(i as u64)),
)?;
}
Ok(())
},
)
}
}

impl<F: Field, const N_BYTES: usize> Chip<F> for LtChip<F, N_BYTES> {
Expand Down Expand Up @@ -157,7 +196,7 @@ mod test {

// TODO: remove zk blinding factors in halo2 to restore the
// correct k (without the extra + 2).
let k = usize::BITS - $values.len().leading_zeros() + 2;
let k = 9;
let circuit = TestCircuit::<Fp> {
values: Some($values),
checks: Some($checks),
Expand All @@ -174,7 +213,7 @@ mod test {

// TODO: remove zk blinding factors in halo2 to restore the
// correct k (without the extra + 2).
let k = usize::BITS - $values.len().leading_zeros() + 2;
let k = 9;
let circuit = TestCircuit::<Fp> {
values: Some($values),
checks: Some($checks),
Expand Down Expand Up @@ -258,6 +297,8 @@ mod test {
let (first_value, values) = values.split_at(1);
let first_value = first_value[0];

chip.load(&mut layouter)?;

layouter.assign_region(
|| "witness",
|mut region| {
Expand Down Expand Up @@ -380,6 +421,8 @@ mod test {
.ok_or(Error::Synthesis)?;
let checks = self.checks.as_ref().ok_or(Error::Synthesis)?;

chip.load(&mut layouter)?;

layouter.assign_region(
|| "witness",
|mut region| {
Expand Down
2 changes: 2 additions & 0 deletions zkevm-circuits/src/copy_circuit.rs
Original file line number Diff line number Diff line change
Expand Up @@ -513,6 +513,8 @@ impl<F: Field> CopyCircuitConfig<F> {
let tag_chip = BinaryNumberChip::construct(self.copy_table.tag);
let lt_chip = LtChip::construct(self.addr_lt_addr_end);

lt_chip.load(layouter)?;

layouter.assign_region(
|| "assign copy table",
|mut region| {
Expand Down

0 comments on commit 4669a87

Please sign in to comment.