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

fix(zkevm-circuits/begin_tx): add missing constraints #1776

Merged
merged 14 commits into from
Mar 12, 2024
Merged
Show file tree
Hide file tree
Changes from 13 commits
Commits
File filter

Filter by extension

Filter by extension

Conversations
Failed to load comments.
Loading
Jump to
Jump to file
Failed to load files.
Loading
Diff view
Diff view
3 changes: 2 additions & 1 deletion bus-mapping/src/circuit_input_builder/block.rs
Original file line number Diff line number Diff line change
Expand Up @@ -84,7 +84,8 @@ pub struct Block {
pub block_steps: BlockSteps,
/// Copy events in this block.
pub copy_events: Vec<CopyEvent>,
/// Inputs to the SHA3 opcode
/// Inputs to the SHA3 opcode as well as data hashed during the EVM execution like init code
/// and address creation inputs.
pub sha3_inputs: Vec<Vec<u8>>,
/// Exponentiation events in the block.
pub exp_events: Vec<ExpEvent>,
Expand Down
27 changes: 26 additions & 1 deletion bus-mapping/src/evm/opcodes/begin_end_tx.rs
Original file line number Diff line number Diff line change
@@ -1,6 +1,8 @@
use super::TxExecSteps;
use crate::{
circuit_input_builder::{Call, CircuitInputStateRef, ExecState, ExecStep},
circuit_input_builder::{
Call, CircuitInputStateRef, CopyDataType, CopyEvent, ExecState, ExecStep, NumberOrHash,
},
operation::{AccountField, AccountOp, CallContextField, TxReceiptField, TxRefundOp, RW},
state_db::CodeDB,
Error,
Expand Down Expand Up @@ -148,6 +150,29 @@ fn gen_begin_tx_steps(state: &mut CircuitInputStateRef) -> Result<ExecStep, Erro
stream.append(&nonce_prev);
stream.out().to_vec()
});
// We also hash the call_data as it will be used as init code, and the
// call_context.code_hash needs to be checked against the hash of this call_data.
state.block.sha3_inputs.push(state.tx.call_data.to_vec());

// Append the copy for the CopyCircuit to calculate RLC(call_data) for the keccack lookup
if state.tx.call_data.len() > 0 {
state.push_copy(
&mut exec_step,
CopyEvent {
src_addr: 0,
src_addr_end: state.tx.call_data.len() as u64,
src_type: CopyDataType::TxCalldata,
src_id: NumberOrHash::Number(state.tx.id as usize),
dst_addr: 0,
dst_type: CopyDataType::RlcAcc,
dst_id: NumberOrHash::Number(0),
log_id: None,
rw_counter_start: state.block_ctx.rwc,
bytes: state.tx.call_data.iter().map(|b| (*b, false)).collect(),
},
);
}
dbg!((state.tx.id, state.tx.call_data.len(), &state.tx.call_data));
Copy link
Member

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

This slipped through! Can you remove it?

Copy link
Member Author

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

Sorry, missed that. Done!

}

// There are 4 branches from here.
Expand Down
80 changes: 67 additions & 13 deletions zkevm-circuits/src/evm_circuit/execution/begin_tx.rs
Original file line number Diff line number Diff line change
Expand Up @@ -12,21 +12,22 @@ use crate::{
},
is_precompiled,
math_gadget::{
ContractCreateGadget, IsEqualWordGadget, IsZeroWordGadget, RangeCheckGadget,
ContractCreateGadget, IsEqualWordGadget, IsZeroGadget, IsZeroWordGadget,
RangeCheckGadget,
},
not,
not, rlc,
tx::{BeginTxHelperGadget, TxDataGadget},
AccountAddress, CachedRegion, Cell, StepRws,
},
witness::{Block, Call, ExecStep, Transaction},
},
table::{AccountFieldTag, BlockContextFieldTag, CallContextFieldTag},
table::{AccountFieldTag, BlockContextFieldTag, CallContextFieldTag, TxContextFieldTag},
util::{
word::{Word32Cell, WordExpr, WordLoHi, WordLoHiCell},
Expr,
},
};
use bus_mapping::state_db::CodeDB;
use bus_mapping::{circuit_input_builder::CopyDataType, state_db::CodeDB};
use eth_types::{evm_types::PRECOMPILE_COUNT, keccak256, Field, OpsIdentity, ToWord, U256};
use halo2_proofs::{
circuit::Value,
Expand All @@ -45,6 +46,9 @@ pub(crate) struct BeginTxGadget<F> {
code_hash: WordLoHiCell<F>,
is_empty_code_hash: IsEqualWordGadget<F, WordLoHi<Expression<F>>, WordLoHi<Expression<F>>>,
caller_nonce_hash_bytes: Word32Cell<F>,
calldata_length: Cell<F>,
calldata_length_is_zero: IsZeroGadget<F>,
calldata_rlc: Cell<F>,
create: ContractCreateGadget<F, false>,
callee_not_exists: IsZeroWordGadget<F, WordLoHiCell<F>>,
is_caller_callee_equal: Cell<F>,
Expand Down Expand Up @@ -183,12 +187,23 @@ impl<F: Field> ExecutionGadget<F> for BeginTxGadget<F> {
);

let caller_nonce_hash_bytes = cb.query_word32();
let calldata_length = cb.query_cell();
let calldata_length_is_zero = cb.is_zero(calldata_length.expr());
let calldata_rlc = cb.query_cell_phase2();
let create = ContractCreateGadget::construct(cb);
cb.require_equal_word(
"tx caller address equivalence",
tx.caller_address.to_word(),
create.caller_address(),
);

cb.require_equal(
"tx nonce equivalence",
tx.nonce.expr(),
create.caller_nonce(),
);

// 1. Handle contract creation transaction.
cb.condition(tx.is_create.expr(), |cb| {
cb.require_equal_word(
"call callee address equivalence",
Expand All @@ -201,21 +216,45 @@ impl<F: Field> ExecutionGadget<F> for BeginTxGadget<F> {
)
.to_word(),
);
});
Copy link
Member Author

@curryrasul curryrasul Mar 4, 2024

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

I removed this; before there were two separate cb.condition with the same condition (that tx.is_create). I think we can merge them.
And actually in the #1475 it is stated that we need to check if callee address is equal to keccak(rlp(sender, nonce)) - but we actually have this constraint already, right? - call callee address equivalence constraint and keccak table lookup for caller_nonce_hash_bytes seems to be enough. Am I missing something?

Copy link
Member

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

I think this is needed. Notice that here we're checking against call_callee_address:

cb.require_equal_word(
"call callee address equivalence",
call_callee_address.to_word(),
AccountAddress::<F>::new(
caller_nonce_hash_bytes.limbs[0..N_BYTES_ACCOUNT_ADDRESS]
.to_vec()
.try_into()
.unwrap(),
)
.to_word(),
);

And caller_nonce_hash_bytes is constrained via:

cb.keccak_table_lookup(
create.input_rlc(cb),
create.input_length(),
caller_nonce_hash_bytes.to_word(),
);

which calls:
pub(crate) fn input_rlc(&self, cb: &EVMConstraintBuilder<F>) -> Expression<F> {

Now notice how input_rlc uses:

So we must check that they are correct.

This checks the nonce (your deleted code):

        cb.require_equal(
            "tx nonce equivalence",
            tx.nonce.expr(),
            create.caller_nonce(),
        );

And this checks the address:

cb.require_equal_word(
"tx caller address equivalence",
tx.caller_address.to_word(),
create.caller_address(),
);

Copy link
Member

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

Sorry I just saw that the removed nonce check was moved to

cb.require_equal(
"tx nonce equivalence",
tx.nonce.expr(),
create.caller_nonce(),
);

So I'm a bit confused.

Are you talking about the removal of the nonce check? Or something else?

I think it would be cleaner if all the create fields equality checks are inside the condition:

// 1. Handle contract creation transaction.
cb.condition(tx.is_create.expr(), |cb| {

Copy link
Member Author

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

There were two cb.condition(tx.is_create.expr()):

cb.condition(tx.is_create.expr(), |cb| {

and the other one:
cb.condition(tx.is_create.expr(), |cb| {

I think it would be cleaner if all the create fields equality checks are inside the condition:
I think that's what I wanted to do as well, that's why I merged them.


But the second thing I asked is do we still need the constraint from here: #1475 (comment)

The callee address of the new context should be the keccak(RLP([sender_address, sender_nonce]))

I think we already have that, right?
cc. @ed255

Copy link
Member

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

There were two cb.condition(tx.is_create.expr()):

cb.condition(tx.is_create.expr(), |cb| {

and the other one:

cb.condition(tx.is_create.expr(), |cb| {

I think it would be cleaner if all the create fields equality checks are inside the condition:
I think that's what I wanted to do as well, that's why I merged them.

Ah, thanks for the clarification! On the constraint level it's the same, but I think in the code level it looks cleaner.

But the second thing I asked is do we still need the constraint from here: #1475 (comment)

The callee address of the new context should be the keccak(RLP([sender_address, sender_nonce]))

I think we already have that, right? cc. @ed255

Ah yes, I see now that this point was already done. I think I just missed this
https://github.com/privacy-scaling-explorations/zkevm-circuits/blob/3bbc757a20d9d9f7759db47c096d5395361bee74/zkevm-circuits/src/evm_circuit/execution/begin_tx.rs#L193C1-L205C12
Due to it being apart from all the logic of the is_create case. So yeah, all is good regarding this point :)

cb.require_equal(
"tx nonce equivalence",
tx.nonce.expr(),
create.caller_nonce(),
);

// 1. Handle contract creation transaction.
cb.condition(tx.is_create.expr(), |cb| {
cb.keccak_table_lookup(
create.input_rlc(cb),
create.input_length(),
caller_nonce_hash_bytes.to_word(),
);

cb.tx_context_lookup(
tx_id.expr(),
TxContextFieldTag::CallDataLength,
None,
WordLoHi::from_lo_unchecked(calldata_length.expr()),
);
// If calldata_length > 0 we use the copy circuit to calculate the calldata_rlc for the
// keccack input.
cb.condition(not::expr(calldata_length_is_zero.expr()), |cb| {
cb.copy_table_lookup(
WordLoHi::from_lo_unchecked(tx_id.expr()),
CopyDataType::TxCalldata.expr(),
WordLoHi::zero(),
CopyDataType::RlcAcc.expr(),
0.expr(),
calldata_length.expr(),
0.expr(),
calldata_length.expr(),
calldata_rlc.expr(),
0.expr(),
)
});
// If calldata_length == 0, the copy circuit will not contain any entry, so we skip the
// lookup and instead force calldata_rlc to be 0 for the keccack input.
cb.condition(calldata_length_is_zero.expr(), |cb| {
cb.require_equal("calldata_rlc = 0", calldata_rlc.expr(), 0.expr());
});
cb.keccak_table_lookup(
Copy link
Member Author

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

Is this how we should add a constraint for cb.curr.state.code_hash = keccak(tx.calldata)?

Copy link
Member

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

Hm, I don't think this is correct.
The length should be something like this (via lookup to TxTable):

let length = cb.tx_context(tx_id, TxContextFieldTag::CallDataLength, None);

The input should be the rlc of the TxCalldata, which is dynamic length. Take a look at the SHA3 opcode to see how it calculates the keccak of memory:

cb.copy_table_lookup(
WordLoHi::from_lo_unchecked(cb.curr.state.call_id.expr()),
CopyDataType::Memory.expr(),
WordLoHi::from_lo_unchecked(cb.curr.state.call_id.expr()),
CopyDataType::RlcAcc.expr(),
memory_address.offset(),
memory_address.address(),
0.expr(), // dst_addr for CopyDataType::RlcAcc is 0.
memory_address.length(),
rlc_acc.expr(),
copy_rwc_inc.expr(),
);

An then CALLDATACOPY to see how it uses the copy circuit with TxCalldata as input:

And from understanding those you should make a copy event that has TxCalldata as input and RLC as ouput. Something like this:

            let copy_rwc_inc = cb.query_cell();
            let rlc_acc = cb.query_cell_phase2();
            cb.copy_table_lookup(
                WordLoHi::from_lo_unchecked(tx_id.expr()),
                CopyDataType::TxCalldata.expr(),
                WordLoHi::zero(),
                CopyDataType::RlcAcc.expr(),
                zero,
                length, // The TxCalldata length calculated previously
                0.expr(), // dst_addr for CopyDataType::RlcAcc is 0.
                length, // The TxCalldata length calculated previously
                rlc_acc.expr(),
                copy_rwc_inc.expr(),
            );

Now you can use rlc_acc as input to keccak_table_lookup

calldata_rlc.expr(),
calldata_length.expr(),
cb.curr.state.code_hash.to_word(),
);

cb.account_write(
call_callee_address.to_word(),
AccountFieldTag::Nonce,
Expand Down Expand Up @@ -434,6 +473,9 @@ impl<F: Field> ExecutionGadget<F> for BeginTxGadget<F> {
code_hash,
is_empty_code_hash,
caller_nonce_hash_bytes,
calldata_length,
calldata_length_is_zero,
calldata_rlc,
create,
callee_not_exists,
is_caller_callee_equal,
Expand Down Expand Up @@ -522,6 +564,18 @@ impl<F: Field> ExecutionGadget<F> for BeginTxGadget<F> {
offset,
U256::from_big_endian(&untrimmed_contract_addr),
)?;
self.calldata_length.assign(
region,
offset,
Value::known(F::from(tx.call_data.len() as u64)),
)?;
self.calldata_length_is_zero
.assign(region, offset, F::from(tx.call_data.len() as u64))?;
let calldata_rlc = region
.challenges()
.keccak_input()
.map(|randomness| rlc::value(tx.call_data.iter().rev(), randomness));
self.calldata_rlc.assign(region, offset, calldata_rlc)?;
self.create.assign(
region,
offset,
Expand Down
Loading