Skip to content
This repository was archived by the owner on Apr 18, 2025. It is now read-only.

Commit 2b4e90d

Browse files
lightsingRaphael Toledo
andauthored
full impl of PUSHn (#684)
Co-authored-by: Raphael Toledo <[email protected]>
1 parent 6deaabd commit 2b4e90d

File tree

1 file changed

+111
-66
lines changed
  • zkevm-circuits/src/evm_circuit/execution

1 file changed

+111
-66
lines changed

zkevm-circuits/src/evm_circuit/execution/push.rs

Lines changed: 111 additions & 66 deletions
Original file line numberDiff line numberDiff line change
@@ -1,15 +1,17 @@
11
use crate::{
22
evm_circuit::{
33
execution::ExecutionGadget,
4+
param::N_BYTES_PROGRAM_COUNTER,
45
step::ExecutionState,
56
util::{
7+
and,
68
common_gadget::SameContextGadget,
79
constraint_builder::{
810
ConstrainBuilderCommon, EVMConstraintBuilder, StepStateTransition,
911
Transition::Delta,
1012
},
11-
math_gadget::IsZeroGadget,
12-
not, select, sum, CachedRegion, Cell, Word,
13+
math_gadget::{IsZeroGadget, LtGadget},
14+
not, or, select, sum, CachedRegion, Cell, Word,
1315
},
1416
witness::{Block, Call, ExecStep, Transaction},
1517
},
@@ -24,7 +26,10 @@ pub(crate) struct PushGadget<F> {
2426
same_context: SameContextGadget<F>,
2527
is_push0: IsZeroGadget<F>,
2628
value: Word<F>,
27-
selectors: [Cell<F>; 32],
29+
is_pushed: [Cell<F>; 32],
30+
is_padding: [Cell<F>; 32],
31+
code_length: Cell<F>,
32+
is_out_of_bound: LtGadget<F, N_BYTES_PROGRAM_COUNTER>,
2833
}
2934

3035
impl<F: Field> ExecutionGadget<F> for PushGadget<F> {
@@ -38,19 +43,25 @@ impl<F: Field> ExecutionGadget<F> for PushGadget<F> {
3843
let is_push0 = IsZeroGadget::construct(cb, "", opcode.expr() - OpcodeId::PUSH0.expr());
3944

4045
let value = cb.query_word_rlc();
41-
cb.condition(not::expr(is_push0.expr()), |cb| cb.stack_push(value.expr()));
46+
cb.stack_push(value.expr());
4247

43-
// Query selectors for each opcode_lookup
44-
let selectors = array_init(|_| cb.query_bool());
48+
// Query selectors for each opcode_lookup whether byte in value needs to be pushed
49+
let is_pushed = array_init(|_| cb.query_bool());
50+
let is_padding = array_init(|_| cb.query_bool());
51+
52+
let code_length = cb.query_cell();
53+
let code_length_left = code_length.expr() - cb.curr.state.program_counter.expr() - 1.expr();
54+
cb.bytecode_length(cb.curr.state.code_hash.expr(), code_length.expr());
55+
56+
let num_bytes_needed = opcode.expr() - OpcodeId::PUSH0.expr();
57+
let is_out_of_bound =
58+
LtGadget::construct(cb, code_length_left.expr(), num_bytes_needed.expr());
59+
let num_bytes_padding = select::expr(
60+
is_out_of_bound.expr(),
61+
num_bytes_needed.expr() - code_length_left.expr(),
62+
0.expr(),
63+
);
4564

46-
// TODO:
47-
// The below constraints are failed when running test case
48-
// `push_gadget_out_of_range`. It seems that we cannot check the exact
49-
// length of `n` data bytes followed by `PUSHn` opcode. Since even if the
50-
// code ends with PUSH32 should succeed to run.
51-
// <https://github.com/ethereum/go-ethereum/blob/master/core/vm/analysis.go#L66>
52-
// <https://github.com/privacy-scaling-explorations/zkevm-circuits/blob/43c67c91ca566fd2b7f3588979c537006090f185/eth-types/src/bytecode.rs#L288>
53-
//
5465
// The pushed bytes are viewed as left-padded big-endian, but our random
5566
// linear combination uses little-endian, so we lookup from the LSB
5667
// which has index (program_counter + num_pushed), and then move left
@@ -64,45 +75,57 @@ impl<F: Field> ExecutionGadget<F> for PushGadget<F> {
6475
// ▼ ▼
6576
// [byte31, ..., byte2, byte1, byte0]
6677
//
67-
// for idx in 0..32 {
68-
// let byte = &value.cells[idx];
69-
// let index = cb.curr.state.program_counter.expr() + opcode.expr()
70-
// - (OpcodeId::PUSH0.as_u8() + idx as u8).expr();
71-
72-
// cb.condition(selectors[idx].expr(), |cb| {
73-
// cb.opcode_lookup_at(index, byte.expr(), 0.expr())
74-
// });
75-
// }
78+
let mut is_pushed_cell_prev = true.expr();
79+
let mut is_padding_cell_prev = true.expr();
80+
for (idx, (is_pushed_cell, is_padding_cell)) in
81+
is_pushed.iter().zip(is_padding.iter()).enumerate()
82+
{
83+
let byte = &value.cells[idx];
84+
let index =
85+
cb.curr.state.program_counter.expr() + num_bytes_needed.clone() - idx.expr();
7686

77-
for idx in 0..32 {
78-
let selector_prev = if idx == 0 {
79-
// First selector will always be 1
80-
1.expr()
81-
} else {
82-
selectors[idx - 1].expr()
83-
};
84-
// selector can transit from 1 to 0 only once as [1, 1, 1, ...,
85-
// 0, 0, 0]
8687
cb.require_boolean(
87-
"Constrain selector can only transit from 1 to 0",
88-
selector_prev - selectors[idx].expr(),
88+
"Constrain is_pushed can only transit from 1 to 0",
89+
is_pushed_cell_prev - is_pushed_cell.expr(),
90+
);
91+
cb.require_boolean(
92+
"Constrain is_padding can only transit from 1 to 0",
93+
is_padding_cell_prev - is_padding_cell.expr(),
94+
);
95+
96+
// byte is 0 if it is either not pushed or padding
97+
cb.condition(
98+
not::expr(or::expr(&[is_pushed_cell.expr(), is_padding_cell.expr()])),
99+
|cb| {
100+
cb.require_zero(
101+
"Constrain byte == 0 when is_pushed == 0 or is_padding == 0",
102+
byte.expr(),
103+
);
104+
},
89105
);
90-
// byte should be 0 when selector is 0
91-
cb.require_zero(
92-
"Constrain byte == 0 when selector == 0",
93-
value.cells[idx].expr() * (1.expr() - selectors[idx].expr()),
106+
cb.condition(
107+
and::expr(&[is_pushed_cell.expr(), not::expr(is_padding_cell.expr())]),
108+
|cb| {
109+
cb.opcode_lookup_at(index, byte.expr(), 0.expr());
110+
},
94111
);
112+
is_pushed_cell_prev = is_pushed_cell.expr();
113+
is_padding_cell_prev = is_padding_cell.expr();
95114
}
96115

97-
// Deduce the number of additional bytes to push than PUSH0. Note that
98-
// num_additional_pushed = n where n is the suffix number of PUSH*.
99-
let num_additional_pushed = opcode.expr() - OpcodeId::PUSH0.as_u64().expr();
100-
// Sum of selectors needs to be exactly the number of additional bytes
101-
// that needs to be pushed.
116+
// Sum of selectors is_pushed needs to be exactly the number of bytes
117+
// that needs to be pushed
102118
cb.require_equal(
103-
"Constrain sum of selectors equal to num_additional_pushed",
104-
sum::expr(&selectors),
105-
num_additional_pushed,
119+
"Constrain sum of is_pushed equal to num_bytes_needed",
120+
sum::expr(&is_pushed),
121+
num_bytes_needed.expr(),
122+
);
123+
124+
// Sum of selectors is_padding needs to be exactly the number of padded bytes
125+
cb.require_equal(
126+
"Constrain sum of is_padding equal to num_padding",
127+
sum::expr(&is_padding),
128+
num_bytes_padding.expr(),
106129
);
107130

108131
// State transition
@@ -123,7 +146,10 @@ impl<F: Field> ExecutionGadget<F> for PushGadget<F> {
123146
same_context,
124147
is_push0,
125148
value,
126-
selectors,
149+
is_pushed,
150+
is_padding,
151+
code_length,
152+
is_out_of_bound,
127153
}
128154
}
129155

@@ -133,7 +159,7 @@ impl<F: Field> ExecutionGadget<F> for PushGadget<F> {
133159
offset: usize,
134160
block: &Block<F>,
135161
_: &Transaction,
136-
_: &Call,
162+
call: &Call,
137163
step: &ExecStep,
138164
) -> Result<(), Error> {
139165
self.same_context.assign_exec_step(region, offset, step)?;
@@ -142,9 +168,17 @@ impl<F: Field> ExecutionGadget<F> for PushGadget<F> {
142168
self.is_push0.assign(
143169
region,
144170
offset,
145-
F::from(opcode.as_u64()) - F::from(OpcodeId::PUSH0.as_u64()),
171+
F::from(opcode.as_u64() - OpcodeId::PUSH0.as_u64()),
146172
)?;
147173

174+
let bytecode = block
175+
.bytecodes
176+
.get(&call.code_hash)
177+
.expect("could not find current environment's bytecode");
178+
let code_length = bytecode.bytes.len() as u64;
179+
self.code_length
180+
.assign(region, offset, Value::known(F::from(code_length)))?;
181+
148182
let value = if opcode.is_push_with_data() {
149183
block.rws[step.rw_indices[0]].stack_value()
150184
} else {
@@ -153,12 +187,32 @@ impl<F: Field> ExecutionGadget<F> for PushGadget<F> {
153187
self.value
154188
.assign(region, offset, Some(value.to_le_bytes()))?;
155189

156-
let num_additional_pushed = opcode.postfix().expect("opcode with postfix");
157-
for (idx, selector) in self.selectors.iter().enumerate() {
158-
selector.assign(
190+
let code_length_left = code_length
191+
.checked_sub(step.program_counter + 1)
192+
.expect("unexpected underflow");
193+
let num_bytes_needed = opcode.postfix().unwrap() as u64;
194+
let num_padding = num_bytes_needed.saturating_sub(code_length_left);
195+
self.is_out_of_bound.assign(
196+
region,
197+
offset,
198+
F::from(code_length_left),
199+
F::from(num_bytes_needed),
200+
)?;
201+
for (idx, (is_pushed_cell, is_padding_cell)) in self
202+
.is_pushed
203+
.iter()
204+
.zip(self.is_padding.iter())
205+
.enumerate()
206+
{
207+
is_pushed_cell.assign(
208+
region,
209+
offset,
210+
Value::known(F::from(((idx as u64) < num_bytes_needed) as u64)),
211+
)?;
212+
is_padding_cell.assign(
159213
region,
160214
offset,
161-
Value::known(F::from((idx < num_additional_pushed as usize) as u64)),
215+
Value::known(F::from(((idx as u64) < num_padding) as u64)),
162216
)?;
163217
}
164218

@@ -169,12 +223,10 @@ impl<F: Field> ExecutionGadget<F> for PushGadget<F> {
169223
#[cfg(test)]
170224
mod test {
171225
use crate::{evm_circuit::test::rand_bytes, test_util::CircuitTestBuilder};
172-
use eth_types::{bytecode, evm_types::OpcodeId, Bytecode};
226+
use eth_types::{bytecode, evm_types::OpcodeId};
173227
use mock::TestContext;
174228

175229
fn test_ok(opcode: OpcodeId, bytes: &[u8]) {
176-
assert!(bytes.len() == opcode.data_len());
177-
178230
let mut bytecode = bytecode! {
179231
.write_op(opcode)
180232
};
@@ -209,20 +261,13 @@ mod test {
209261
24, 25, 26, 27, 28, 29, 30, 31, 32,
210262
],
211263
);
212-
}
213264

214-
#[ignore]
215-
#[test]
216-
fn push_gadget_out_of_range() {
217-
let bytecode = Bytecode::from(vec![0x61, 0x00]);
218-
CircuitTestBuilder::new_from_test_ctx(
219-
TestContext::<2, 1>::simple_ctx_with_bytecode(bytecode).unwrap(),
220-
)
221-
.run();
265+
// out of bounds
266+
test_ok(OpcodeId::PUSH2, &[1]);
267+
test_ok(OpcodeId::PUSH16, &[1, 2, 3, 4, 5, 6, 7, 8, 9, 10]);
222268
}
223269

224270
#[test]
225-
#[ignore]
226271
fn push_gadget_rand() {
227272
for (idx, opcode) in vec![
228273
OpcodeId::PUSH1,

0 commit comments

Comments
 (0)