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

Commit

Permalink
Fully implement PUSHn (#1527)
Browse files Browse the repository at this point in the history 
### Description
We intend here to support PUSHn with bytecode length inferior to n.

### Issue Link
Issue #633 
Linked to specs issue
privacy-scaling-explorations/zkevm-specs#463

### Type of change

- [ ] Bug fix (non-breaking change which fixes an issue)
- [x] 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

- Update push.rs to support bytecode of size smaller than n
- Update stop.rs similarly

### Rationale

In pushn, "selectors" are switches to enable or disable lookup arguments
on the bytcode bytes as well as to check whether these are non-null if
needs be. They directly depend on "n" of PUSHn.
We add to these "selectors", "counters" which have similar role but are
a subset of them depending on the bytecode length. We added these extra
switches to be able to easily check the various identities at the risk
of some redundancy.

To support these changes, modifications in stop.py also had to be done.
More precisely, the check "is_out_of_range had to be extended to support
small bytecodes.

### How Has This Been Tested?

Extra tests have been added in push.rs (only).
  • Loading branch information
Raphael authored Jul 31, 2023
1 parent 1837e30 commit d6128b1
Show file tree
Hide file tree
Showing 2 changed files with 138 additions and 64 deletions.
166 changes: 119 additions & 47 deletions zkevm-circuits/src/evm_circuit/execution/push.rs
View file
Original file line number Diff line number Diff line change
@@ -1,13 +1,15 @@
use crate::{
evm_circuit::{
execution::ExecutionGadget,
param::N_BYTES_PROGRAM_COUNTER,
step::ExecutionState,
util::{
common_gadget::SameContextGadget,
constraint_builder::{
ConstrainBuilderCommon, EVMConstraintBuilder, StepStateTransition,
Transition::Delta,
},
math_gadget::LtGadget,
sum, CachedRegion, Cell,
},
witness::{Block, Call, ExecStep, Transaction},
Expand All @@ -25,7 +27,10 @@ use halo2_proofs::{circuit::Value, plonk::Error};
pub(crate) struct PushGadget<F> {
same_context: SameContextGadget<F>,
value: Word32Cell<F>,
selectors: [Cell<F>; 31],
is_pushed: [Cell<F>; 32],
is_padding: [Cell<F>; 32],
code_length: Cell<F>,
is_out_of_bound: LtGadget<F, N_BYTES_PROGRAM_COUNTER>,
}

impl<F: Field> ExecutionGadget<F> for PushGadget<F> {
Expand All @@ -35,10 +40,33 @@ impl<F: Field> ExecutionGadget<F> for PushGadget<F> {

fn configure(cb: &mut EVMConstraintBuilder<F>) -> Self {
let opcode = cb.query_cell();
let code_length = cb.query_cell();
let code_length_left = code_length.expr() - cb.curr.state.program_counter.expr() - 1.expr();

let value = cb.query_word32();
// Query selectors for each opcode_lookup
let selectors = array_init(|_| cb.query_bool());
// Query selectors for each opcode_lookup to know whether the current byte needs to be
// pushed
let is_pushed = array_init(|_| cb.query_bool());

// Query selectors for each opcode_lookup to know whether the current byte is actually
// padding
let is_padding = array_init(|_| cb.query_bool());

// Fetch the bytecode length from the bytecode table.
let code_hash = cb.curr.state.code_hash.clone();
cb.bytecode_length(code_hash.to_word(), code_length.expr());

// Deduce the number of bytes to push.
let num_pushed = opcode.expr() - OpcodeId::PUSH1.as_u64().expr() + 1.expr();

// If the number of bytes that needs to be pushed is greater
// than the size of the bytecode left, then we are out of range.
let is_out_of_bound: LtGadget<F, N_BYTES_PROGRAM_COUNTER> =
LtGadget::construct(cb, code_length_left.clone(), num_pushed.clone());

// Expected number of padding
let num_padding: halo2_proofs::plonk::Expression<F> =
is_out_of_bound.expr() * (num_pushed.clone() - code_length_left);

// The pushed bytes are viewed as left-padded big-endian, but our random
// linear combination uses little-endian, so we lookup from the LSB
Expand All @@ -53,48 +81,57 @@ impl<F: Field> ExecutionGadget<F> for PushGadget<F> {
// ▼ ▼
// [byte31, ..., byte2, byte1, byte0]
//
for idx in 0..32 {
// First is_pushed (resp. is_padding) will always be 1 (resp. 1)
let mut pu_prev = 1.expr();
let mut pa_prev = 1.expr();
for (idx, (pu, pa)) in is_pushed.iter().zip(is_padding.iter()).enumerate() {
let byte = &value.limbs[idx];
let index = cb.curr.state.program_counter.expr() + opcode.expr()
- (OpcodeId::PUSH1.as_u8() - 1 + idx as u8).expr();
if idx == 0 {
cb.opcode_lookup_at(index, byte.expr(), 0.expr())
} else {
cb.condition(selectors[idx - 1].expr(), |cb| {
cb.opcode_lookup_at(index, byte.expr(), 0.expr())
});
}
}
let index: halo2_proofs::plonk::Expression<F> =
cb.curr.state.program_counter.expr() + num_pushed.clone() - idx.expr();

// is_pushed can transit from 1 to 0 only once
// as 1 - [1, 1, 1, ..., 1, 0, 0, 0]
cb.require_boolean(
"Constrain is_pushed can only transit from 1 to 0",
pu_prev - pu.expr(),
);

for idx in 0..31 {
let selector_prev = if idx == 0 {
// First selector will always be 1
1.expr()
} else {
selectors[idx - 1].expr()
};
// selector can transit from 1 to 0 only once as [1, 1, 1, ...,
// 0, 0, 0]
// is_padding can transit from 1 to 0 only once
// as 1 - [1, 1, 0, ..., 0, 0, 0, 0] (out of bound)
// as 1 - [0, 0, 0, ..., 0, 0, 0, 0] (not out of bound)
cb.require_boolean(
"Constrain selector can only transit from 1 to 0",
selector_prev - selectors[idx].expr(),
"Constrain is_padding can only transit from 1 to 0",
pa_prev - pa.expr(),
);
// byte should be 0 when selector is 0

// byte is 0 if it is either not pushed or padding
cb.require_zero(
"Constrain byte == 0 when selector == 0",
value.limbs[idx + 1].expr() * (1.expr() - selectors[idx].expr()),
"Constrain byte == 0 when is_pushed == 0 OR is_padding == 1",
byte.expr() * (pa.expr() + (1.expr() - pu.expr())),
);

// if byte is pushed and not padding, we check consistency with bytecode table
cb.condition(pu.expr() * (1.expr() - pa.expr()), |cb| {
cb.opcode_lookup_at(index, byte.expr(), 0.expr())
});

pu_prev = pu.expr();
pa_prev = pa.expr();
}

// Deduce the number of additional bytes to push than PUSH1. Note that
// num_additional_pushed = n - 1 where n is the suffix number of PUSH*.
let num_additional_pushed = opcode.expr() - OpcodeId::PUSH1.as_u64().expr();
// Sum of selectors needs to be exactly the number of additional bytes
// that needs to be pushed.
// Sum of selectors is_pushed needs to be exactly the number of bytes
// that needs to be pushed
cb.require_equal(
"Constrain sum of is_pushed equal to num_pushed",
sum::expr(&is_pushed),
num_pushed.expr(),
);

// Sum of selectors is_padding needs to be exactly the number of padded bytes
cb.require_equal(
"Constrain sum of selectors equal to num_additional_pushed",
sum::expr(&selectors),
num_additional_pushed,
"Constrain sum of is_padding equal to num_padding",
sum::expr(&is_padding),
num_padding.expr(),
);

// Push the value on the stack
Expand All @@ -114,7 +151,10 @@ impl<F: Field> ExecutionGadget<F> for PushGadget<F> {
Self {
same_context,
value,
selectors,
is_pushed,
is_padding,
code_length,
is_out_of_bound,
}
}

Expand All @@ -124,23 +164,51 @@ impl<F: Field> ExecutionGadget<F> for PushGadget<F> {
offset: usize,
block: &Block<F>,
_: &Transaction,
_: &Call,
call: &Call,
step: &ExecStep,
) -> Result<(), Error> {
self.same_context.assign_exec_step(region, offset, step)?;

let opcode = step.opcode().unwrap();
let num_pushed = opcode.postfix().expect("opcode with postfix");
let npushed = num_pushed as usize;

let bytecode = block
.bytecodes
.get_from_h256(&call.code_hash)
.expect("could not find current environment's bytecode");

let code_length = bytecode.codesize() as u64;
self.code_length
.assign(region, offset, Value::known(F::from(code_length)))?;

let code_length_left = (code_length - step.pc - 1) as usize;
self.is_out_of_bound.assign(
region,
offset,
F::from(code_length_left as u64),
F::from(num_pushed as u64),
)?;

let value = block.get_rws(step, 0).stack_value();
self.value.assign_u256(region, offset, value)?;

let num_additional_pushed = opcode.postfix().expect("opcode with postfix") - 1;
for (idx, selector) in self.selectors.iter().enumerate() {
selector.assign(
region,
offset,
Value::known(F::from((idx < num_additional_pushed as usize) as u64)),
)?;
let is_out_of_bound = code_length_left < npushed;
let out_of_bound_padding = if is_out_of_bound {
npushed - code_length_left
} else {
0
};
for (i, (pu, pa)) in self
.is_pushed
.iter()
.zip(self.is_padding.iter())
.enumerate()
{
let pushed = i < npushed;
let padding = i < out_of_bound_padding;
pu.assign(region, offset, Value::known(F::from(pushed as u64)))?;
pa.assign(region, offset, Value::known(F::from(padding as u64)))?;
}

Ok(())
Expand All @@ -154,15 +222,17 @@ mod test {
use mock::TestContext;

fn test_ok(opcode: OpcodeId, bytes: &[u8]) {
assert!(bytes.len() == opcode.data_len());
assert!(bytes.len() <= opcode.data_len());

let mut bytecode = bytecode! {
.write_op(opcode)
};
for b in bytes {
bytecode.write(*b, false);
}
bytecode.op_stop();
if bytes.len() == opcode.data_len() {
bytecode.op_stop();
}

CircuitTestBuilder::new_from_test_ctx(
TestContext::<2, 1>::simple_ctx_with_bytecode(bytecode).unwrap(),
Expand All @@ -174,6 +244,7 @@ mod test {
fn push_gadget_simple() {
test_ok(OpcodeId::PUSH1, &[1]);
test_ok(OpcodeId::PUSH2, &[1, 2]);
test_ok(OpcodeId::PUSH5, &[1, 2, 3, 4, 5]);
test_ok(
OpcodeId::PUSH31,
&[
Expand All @@ -188,6 +259,7 @@ mod test {
24, 25, 26, 27, 28, 29, 30, 31, 32,
],
);
test_ok(OpcodeId::PUSH16, &[1, 2, 3, 4, 5, 6, 7, 8, 9, 10]);
}

#[test]
Expand Down
36 changes: 19 additions & 17 deletions zkevm-circuits/src/evm_circuit/execution/stop.rs
View file
Original file line number Diff line number Diff line change
@@ -1,14 +1,15 @@
use crate::{
evm_circuit::{
execution::ExecutionGadget,
param::N_BYTES_PROGRAM_COUNTER,
step::ExecutionState,
util::{
common_gadget::RestoreContextGadget,
constraint_builder::{
ConstrainBuilderCommon, EVMConstraintBuilder, StepStateTransition,
Transition::{Delta, Same},
},
math_gadget::IsZeroGadget,
math_gadget::ComparisonGadget,
CachedRegion, Cell,
},
witness::{Block, Call, ExecStep, Transaction},
Expand All @@ -26,7 +27,7 @@ use halo2_proofs::{circuit::Value, plonk::Error};
#[derive(Clone, Debug)]
pub(crate) struct StopGadget<F> {
code_length: Cell<F>,
is_out_of_range: IsZeroGadget<F>,
out_of_range: ComparisonGadget<F, N_BYTES_PROGRAM_COUNTER>,
opcode: Cell<F>,
restore_context: RestoreContextGadget<F>,
}
Expand All @@ -39,12 +40,17 @@ impl<F: Field> ExecutionGadget<F> for StopGadget<F> {
fn configure(cb: &mut EVMConstraintBuilder<F>) -> Self {
let code_length = cb.query_cell();
cb.bytecode_length(cb.curr.state.code_hash.to_word(), code_length.expr());
let is_out_of_range = IsZeroGadget::construct(

let out_of_range = ComparisonGadget::construct(
cb,
code_length.expr() - cb.curr.state.program_counter.expr(),
code_length.expr(),
cb.curr.state.program_counter.expr(),
);
let (lt, eq) = out_of_range.expr();
let is_out_of_range = lt + eq;

let opcode = cb.query_cell();
cb.condition(1.expr() - is_out_of_range.expr(), |cb| {
cb.condition(1.expr() - is_out_of_range, |cb| {
cb.opcode_lookup(opcode.expr(), 1.expr());
});

Expand Down Expand Up @@ -91,7 +97,7 @@ impl<F: Field> ExecutionGadget<F> for StopGadget<F> {

Self {
code_length,
is_out_of_range,
out_of_range,
opcode,
restore_context,
}
Expand All @@ -110,17 +116,13 @@ impl<F: Field> ExecutionGadget<F> for StopGadget<F> {
.bytecodes
.get_from_h256(&call.code_hash)
.expect("could not find current environment's bytecode");
self.code_length.assign(
region,
offset,
Value::known(F::from(code.codesize() as u64)),
)?;

self.is_out_of_range.assign(
region,
offset,
F::from(code.codesize() as u64) - F::from(step.pc),
)?;

let code_length = code.codesize() as u64;
self.code_length
.assign(region, offset, Value::known(F::from(code_length)))?;

self.out_of_range
.assign(region, offset, F::from(code_length), F::from(step.pc))?;

let opcode = step.opcode().unwrap();
self.opcode
Expand Down

0 comments on commit d6128b1

Please sign in to comment.