diff --git a/zkevm-circuits/src/evm_circuit/execution/calldataload.rs b/zkevm-circuits/src/evm_circuit/execution/calldataload.rs index f443980188..16aadd4e8e 100644 --- a/zkevm-circuits/src/evm_circuit/execution/calldataload.rs +++ b/zkevm-circuits/src/evm_circuit/execution/calldataload.rs @@ -260,14 +260,8 @@ impl ExecutionGadget for CallDataLoadGadget { } } - 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(()) } diff --git a/zkevm-circuits/src/evm_circuit/util/memory_gadget.rs b/zkevm-circuits/src/evm_circuit/util/memory_gadget.rs index 49ba183ad6..2a84933323 100644 --- a/zkevm-circuits/src/evm_circuit/util/memory_gadget.rs +++ b/zkevm-circuits/src/evm_circuit/util/memory_gadget.rs @@ -25,6 +25,7 @@ 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 { @@ -609,11 +610,6 @@ pub(crate) struct BufferReaderGadget; MAX_BYTES], - /// `bound_dist` is defined as `max(addr_end - addr_start - i, 0)` for `i` - /// in 0..MAX_BYTES - bound_dist: [Cell; MAX_BYTES], - /// Check if bound_dist is zero - bound_dist_is_zero: [IsZeroGadget; MAX_BYTES], /// The min gadget to take the minimum of addr_start and addr_end min_gadget: MinMaxGadget, } @@ -628,39 +624,6 @@ impl ) -> 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 { @@ -680,17 +643,38 @@ impl "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, } } @@ -702,25 +686,32 @@ impl 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(()) } @@ -728,16 +719,8 @@ impl self.bytes[idx].expr() } - pub(crate) fn has_data(&self, idx: usize) -> Expression { - self.selectors[idx].expr() - } - /// Indicate whether the bytes\[idx\] is read from the buffer pub(crate) fn read_flag(&self, idx: usize) -> Expression { - self.has_data(idx) * (1.expr() - self.bound_dist_is_zero[idx].expr()) - } - - pub(crate) fn num_bytes(&self) -> Expression { - sum::expr(&self.selectors) + self.selectors[idx].expr() } }