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

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

Changes from 10 commits
Commits
Show all changes
14 commits
Select commit Hold shift + click to select a range
8c231e1
fix(begin_tx): add todo
curryrasul Feb 21, 2024
4390f88
fix(zkevm-circuits/begin_tx): add comments
curryrasul Feb 22, 2024
4f77fa2
fix(zkevm-circuits/begin_tx): remove unnecessary comments
curryrasul Feb 23, 2024
1ab9f99
fix(zkevm-circuits/begin_tx): remove unnecessary comments
curryrasul Feb 23, 2024
8996f37
fix(zkevm-circuits/begin_tx): minor refactor & todo comment
curryrasul Mar 4, 2024
13d9cba
fix(zkevm-circuits/begin_tx): remove unnecessary comment
curryrasul Mar 4, 2024
c40d3da
fix(zkevm-circuits/begin_tx): add constraints
curryrasul Mar 4, 2024
bc6715a
fix(zkevm-circuits/begin_tx): fix added constraints
curryrasul Mar 4, 2024
757dbf1
fix(zkevm-circuits/begin_tx): fix the constraint
curryrasul Mar 5, 2024
496829a
Merge branch 'main' into fix/begintx-missingconstraint
curryrasul Mar 5, 2024
2291146
fix: add missing copy event, keccak input, cell assignments, calldata…
ed255 Mar 6, 2024
3af8f8f
Merge branch 'main' into fix/begintx-missingconstraint
curryrasul Mar 6, 2024
f69053e
fix(zkevm-circuits/begin_tx): remove unnecessary import
curryrasul Mar 6, 2024
b6494f1
fix(bus_mapping/begin_end_tx): remove dbg
curryrasul Mar 8, 2024
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
41 changes: 30 additions & 11 deletions zkevm-circuits/src/evm_circuit/execution/begin_tx.rs
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -20,13 +20,13 @@ use crate::{
},
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 Down Expand Up @@ -190,6 +190,14 @@ impl<F: Field> ExecutionGadget<F> for BeginTxGadget<F> {
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 @@ -202,21 +210,32 @@ impl<F: Field> ExecutionGadget<F> for BeginTxGadget<F> {
)
.to_word(),
);
});
Copy link
Member Author

@curryrasul curryrasul Mar 4, 2024 •
edited
Loading

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:

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

Lines 202 to 212 in c40d3da

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:

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

Lines 213 to 217 in c40d3da

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

which calls:

zkevm-circuits/zkevm-circuits/src/evm_circuit/util/math_gadget/rlp.rs

Line 327 in 3bbc757

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:

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

Lines 188 to 192 in c40d3da

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

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

Lines 194 to 198 in c40d3da

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:

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

Lines 200 to 201 in c40d3da

// 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()):

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

Line 193 in 3bbc757

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

and the other one:

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

Line 213 in 3bbc757

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()):

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

Line 193 in 3bbc757

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

and the other one:

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

Line 213 in 3bbc757

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(),
);

let length = cb.tx_context(tx_id.expr(), TxContextFieldTag::CallDataLength, None);
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(),
0.expr(),
length.expr(),
0.expr(),
length.expr(),
rlc_acc.expr(),
0.expr(),
Copy link
Member Author

Choose a reason for hiding this comment

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

Not sure why the check is failed, but can it be because I made rwc_inc = 0, as we discussed during the call @ed255 ?
In the previous commit it was equal to cb.query_cell().expr()

Copy link
Member

Choose a reason for hiding this comment

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

I checked the errors and noticed there were quite a few things missing! I think it's not trivial to be aware of the missing things without being familiar with the entire system :)

Take a look at this commit where I added the missing things in order to make the tests pass 2291146

Here's a list of changes:

  • The cells calldata_length and calldata_rlc in BeginTx where not being assigned, so I added them to the gadget and assigned them in BeginTx::assign_exec_step
  • The keccak table didn't have the input for tx.call_data when the tx is creation, so I added it via the bus-mapping
  • The copy table didn't have the input for copying the tx.call_data into rlc when the tx is creation, so I added it via the bus-mapping
  • The copy table only contains an entry in case there's at least 1 byte copied. If tx.call_data.len() == 0 there will be no entry in the copy table, so the lookup will fail. I added a conditional on the copy table lookup for the case tx.call_data.len() > 0, and otherwise I directly set call_data_rlc = 0

Copy link
Member Author

Choose a reason for hiding this comment

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

May I ask - is it necessary add calldata_length, calldata_rlc, etc. to the gadget, and therefore assign them. Why wouldn't it work the way I made it before? Or the cells "were not there" before?

For example what's the fundamental difference between this:

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

and having a separate calldata_length field/cell in the gadget, and doing the lookup:

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

Lines 226 to 231 in 2291146

cb.tx_context_lookup(
tx_id.expr(),
TxContextFieldTag::CallDataLength,
None,
WordLoHi::from_lo_unchecked(calldata_length.expr()),
);

The copy table only contains an entry in case there's at least 1 byte copied. If tx.call_data.len() == 0 there will be no entry in the copy table, so the lookup will fail. I added a conditional on the copy table lookup for the case tx.call_data.len() > 0, and otherwise I directly set call_data_rlc = 0

Yes, I was going through Scroll's begin_tx and they have similar thing; I forgot to add the same check here, sorry.

Thanks for help, I'll merge branches and push it here.

Copy link
Member

Choose a reason for hiding this comment

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

May I ask - is it necessary add calldata_length, calldata_rlc, etc. to the gadget, and therefore assign them. Why wouldn't it work the way I made it before? Or the cells "were not there" before?

If you don't add these cells to the gadget, they will not be part of the config, and if they are not part of the config, you don't have the reference to do the witness assignment, and then they will be assigned to 0, so the constraints will fail. It was working before because these two cells didn't exists before.

For example what's the fundamental difference between this:

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

and having a separate calldata_length field/cell in the gadget, and doing the lookup:

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

Lines 226 to 231 in 2291146

cb.tx_context_lookup(
tx_id.expr(),
TxContextFieldTag::CallDataLength,
None,
WordLoHi::from_lo_unchecked(calldata_length.expr()),
);

The first option is always nicer, but it does two things:

  1. Allocate the cell
  2. Perform the lookup with that cell

In this case, we need to allocate the cell unconditionally because we want to store it in the config to later on use it for witness assignment, but the lookup must be conditional!

Another option would be doing something like this:

let length = cb.condition(tx.is_create.expr(), |cb| {
    // [...]
    let length = cb.tx_context(tx_id, TxContextFieldTag::CallDataLength, None);
    // [...]
    length
};

That would be equivalent.

Copy link
Member Author

Choose a reason for hiding this comment

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

Thanks a lot for explanation

);
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:

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

Lines 61 to 72 in 3bbc757

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:

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

Line 115 in 3bbc757

CopyDataType::TxCalldata.expr(),

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

rlc_acc.expr(),
length.expr(),
cb.curr.state.code_hash.to_word(),
);

cb.account_write(
call_callee_address.to_word(),
AccountFieldTag::Nonce,
Expand Down
Loading