Skip to content

Commit

Permalink
fix-bufferreader: constrain the "in-bound" selectors vs the addresses (
Browse files Browse the repository at this point in the history
…privacy-scaling-explorations#1485)

### Description

In the BufferReaderGadget, there are two conflicting mechanisms that
enforces the zero padding, one based on `selectors`, and one based on
`bound_dist`. This causes the issue privacy-scaling-explorations#1484. This PR fixes this and
improves performance at the same time.


### Issue Link

privacy-scaling-explorations#1484 

### Type of change

- [x] Bug fix (non-breaking change which fixes an issue)
- [ ] New feature (non-breaking change which adds functionality)
- [ ] Breaking change (fix or feature that would cause existing
functionality to not work as expected)
- [ ] This change requires a documentation update

### Contents

- Remove the columns `bound_dist` and everything related to it.
- Repurpose the unused `selectors` and add constraints to it.
- The buffer length is taken as the sum of selectors, and compared to
the length implied by the start and end addresses.
- The cases where `start < end` and `end <= start` are supported
explicitly.
- The length is capped between 0 and the max buffer size using the
existing MinMaxGadget. A single MinMaxGadget is used thanks to a
`select`.
- Remove the unused methods `has_data` and `num_bytes`.

### Rationale

The simplest fix would be to remove the `selectors` and keep the
`bound_dist` mechanism. However, this PR does a more efficient way.
Indeed, the existing logic on the selectors is simple and cheap, while
the other is costly because it compares every index to the addresses.

### How Has This Been Tested?

`cargo test --package zkevm-circuits --features test --
evm_circuit::execution::calldataload`

---------

Co-authored-by: Aurélien Nicolas <[email protected]>
Co-authored-by: Rohit Narurkar <[email protected]>
  • Loading branch information
3 people authored Jul 4, 2023
1 parent ee93a18 commit 6cd8025
Show file tree
Hide file tree
Showing 2 changed files with 56 additions and 78 deletions.
10 changes: 2 additions & 8 deletions zkevm-circuits/src/evm_circuit/execution/calldataload.rs
Original file line number Diff line number Diff line change
Expand Up @@ -259,14 +259,8 @@ impl<F: Field> ExecutionGadget<F> for CallDataLoadGadget<F> {
}
}

self.buffer_reader.assign(
region,
offset,
src_addr,
src_addr_end,
&calldata_bytes,
&[true; N_BYTES_WORD],
)?;
self.buffer_reader
.assign(region, offset, src_addr, src_addr_end, &calldata_bytes)?;

Ok(())
}
Expand Down
124 changes: 54 additions & 70 deletions zkevm-circuits/src/evm_circuit/util/memory_gadget.rs
Original file line number Diff line number Diff line change
Expand Up @@ -15,10 +15,12 @@ use crate::{
};
use array_init::array_init;
use eth_types::{evm_types::GasCost, Field, ToLittleEndian, U256};
use gadgets::util::not;
use halo2_proofs::{
circuit::Value,
plonk::{Error, Expression},
};
use itertools::Itertools;

/// Decodes the usable part of an address stored in a Word
pub(crate) mod address_low {
Expand Down Expand Up @@ -394,11 +396,6 @@ pub(crate) struct BufferReaderGadget<F, const MAX_BYTES: usize, const N_BYTES_ME
/// The selectors that indicate if the corrsponding byte contains real data
/// or is padded
selectors: [Cell<F>; MAX_BYTES],
/// `bound_dist` is defined as `max(addr_end - addr_start - i, 0)` for `i`
/// in 0..MAX_BYTES
bound_dist: [Cell<F>; MAX_BYTES],
/// Check if bound_dist is zero
bound_dist_is_zero: [IsZeroGadget<F>; MAX_BYTES],
/// The min gadget to take the minimum of addr_start and addr_end
min_gadget: MinMaxGadget<F, N_BYTES_MEMORY_ADDRESS>,
}
Expand All @@ -413,39 +410,6 @@ impl<F: Field, const MAX_BYTES: usize, const ADDR_SIZE_IN_BYTES: usize>
) -> Self {
let bytes = array_init(|_| cb.query_byte());
let selectors = array_init(|_| cb.query_bool());
let bound_dist = array_init(|_| cb.query_cell());
let bound_dist_is_zero =
array_init(|idx| IsZeroGadget::construct(cb, bound_dist[idx].expr()));

// Define bound_dist[i] = max(addr_end - addr_start - i, 0)
// The purpose of bound_dist is to check if the access to the buffer
// is out of bound. When bound_dist[i] == 0, it indicates OOB access
// and so bytes[i] has to be 0.
// Because the bound_dist is decreasing by at most 1 each time, we can
// use this property to reduce the use of LtGadget by adding constraints
// to the diff between two consecutive bound_dists.

// The constraints on bound_dist[0].
// bound_dist[0] == addr_end - addr_start if addr_start < addr_end
// bound_dist[0] == 0 if addr_start >= addr_end
let min_gadget = MinMaxGadget::construct(cb, addr_start, addr_end.clone());
cb.require_equal(
"bound_dist[0] == addr_end - min(addr_start, add_end)",
bound_dist[0].expr(),
addr_end - min_gadget.min(),
);
// Constraints on bound_dist[1..MAX_BYTES]
// diff = bound_dist[idx - 1] - bound_dist[idx]
// diff == 1 if bound_dist[idx - 1] != 0
// diff == 0 if bound_dist[idx - 1] == 0
for idx in 1..MAX_BYTES {
let diff = bound_dist[idx - 1].expr() - bound_dist[idx].expr();
cb.require_equal(
"diff == 0 if bound_dist[i - 1] == 0; otherwise 1",
diff,
select::expr(bound_dist_is_zero[idx - 1].expr(), 0.expr(), 1.expr()),
)
}

// Constraints on bytes and selectors
for i in 0..MAX_BYTES {
Expand All @@ -465,17 +429,38 @@ impl<F: Field, const MAX_BYTES: usize, const ADDR_SIZE_IN_BYTES: usize>
"bytes[i] == 0 when selectors[i] == 0",
(1.expr() - selectors[i].expr()) * bytes[i].expr(),
);
cb.add_constraint(
"bytes[i] == 0 when bound_dist[i] == 0",
bound_dist_is_zero[i].expr() * bytes[i].expr(),
)
}

// Look at the data length, which can be negative, or within the buffer span, or larger.
// Decide what is the other operand of the MinMaxGadget gadget. If the buffer is empty
// because end <= start, compare the length to 0. Otherwise, compare to the buffer size.
let is_empty = not::expr(&selectors[0]);
let cap = select::expr(is_empty.expr(), 0.expr(), MAX_BYTES.expr());
let signed_len = addr_end - addr_start;
let min_gadget = MinMaxGadget::construct(cb, cap, signed_len);

// If we claim that the buffer is empty, we prove that the end is at or before the start.
// buffer_len = max(0, signed_len) = 0
cb.condition(is_empty.expr(), |cb| {
cb.require_zero("addr_end <= addr_start", min_gadget.max());
});

// Otherwise, the buffer length equals the data length, capped at the buffer size.
// buffer_len = min(MAX_BYTES, signed_len)
cb.condition(not::expr(is_empty), |cb| {
let buffer_len = sum::expr(&selectors);
let capped_len = min_gadget.min();

cb.require_equal(
"buffer length == end - start (capped)",
buffer_len,
capped_len,
);
});

BufferReaderGadget {
bytes,
selectors,
bound_dist,
bound_dist_is_zero,
min_gadget,
}
}
Expand All @@ -487,42 +472,41 @@ impl<F: Field, const MAX_BYTES: usize, const ADDR_SIZE_IN_BYTES: usize>
addr_start: u64,
addr_end: u64,
bytes: &[u8],
selectors: &[bool],
) -> Result<(), Error> {
self.min_gadget
.assign(region, offset, F::from(addr_start), F::from(addr_end))?;

assert_eq!(selectors.len(), MAX_BYTES);
for (idx, selector) in selectors.iter().enumerate() {
self.selectors[idx].assign(region, offset, Value::known(F::from(*selector as u64)))?;
self.bytes[idx].assign(region, offset, Value::known(F::from(bytes[idx] as u64)))?;
// assign bound_dist and bound_dist_is_zero
let oob = addr_start + idx as u64 >= addr_end;
let bound_dist = if oob {
F::ZERO
} else {
F::from(addr_end - addr_start - idx as u64)
};
self.bound_dist[idx].assign(region, offset, Value::known(bound_dist))?;
self.bound_dist_is_zero[idx].assign(region, offset, bound_dist)?;
assert_eq!(bytes.len(), MAX_BYTES);
for (idx, ((byte_col, &byte_val), selector_col)) in self
.bytes
.iter()
.zip_eq(bytes.iter())
.zip_eq(self.selectors.iter())
.enumerate()
{
let selector = (addr_start + idx as u64) < addr_end;
selector_col.assign(region, offset, Value::known(F::from(selector as u64)))?;
byte_col.assign(region, offset, Value::known(F::from(byte_val as u64)))?;
}

let is_empty = addr_start >= addr_end;
let cap = if is_empty { 0 } else { MAX_BYTES };
let signed_len = if is_empty {
-F::from(addr_start - addr_end)
} else {
F::from(addr_end - addr_start)
};
self.min_gadget
.assign(region, offset, F::from(cap as u64), signed_len)?;

// Completeness: MinMaxGadget requires `signed_len ∈ (cap-RANGE; cap+RANGE]`, covering all
// cases. If is_empty, signed_len ∈ (-RANGE; 0], otherwise signed_len ∈ [1; RANGE).
Ok(())
}

pub(crate) fn byte(&self, idx: usize) -> Expression<F> {
self.bytes[idx].expr()
}

pub(crate) fn has_data(&self, idx: usize) -> Expression<F> {
self.selectors[idx].expr()
}

/// Indicate whether the bytes\[idx\] is read from the buffer
pub(crate) fn read_flag(&self, idx: usize) -> Expression<F> {
self.has_data(idx) * (1.expr() - self.bound_dist_is_zero[idx].expr())
}

pub(crate) fn num_bytes(&self) -> Expression<F> {
sum::expr(&self.selectors)
self.selectors[idx].expr()
}
}

0 comments on commit 6cd8025

Please sign in to comment.