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 7 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
28 changes: 19 additions & 9 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 @@ -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,23 @@ 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(),
);

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

create.code_hash_keccak_rlc(cb),
32.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.

I'm not sure that this length is correct. What it should be equals to?

cb.curr.state.code_hash.to_word(),
);
cb.require_equal_word(
Copy link
Member Author

Choose a reason for hiding this comment

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

Do we also need to add this constraint? Cause after creating ContractCreateGadget we checked nonce equivalence, and some other things but not this for example.

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 not needed. The code_hash in the create gadget seems to be only for the CREATE2 opcode. The code_hash for creation via BeginTx follows a different pattern (it's hash of tx.calldata).

So here we're using a create.code_hash witness from the ContractCreateGadget to compare it against another code_hash. But the create.code_hash doesn't appear in any constraint inside ContractCreateGadget because we're never calling create.input_rlc with IS_CREATE2 = true. So the create.code_hash will have whichever value the prover assigns, so this equality check is meaningless.

"code hash equivalence",
code_hash.to_word(),
create.code_hash().to_word(),
);

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