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

[curryrasul]

Description

This PR aims to fix #1475 by adding missing constraints.

Issue Link

#1475

Type of change

• Bug fix (non-breaking change which fixes an issue)

Questions / Need Help

1. Meaning of value_prev argument in account_access_list_write_unchecked. Why is it sometimes set to 0, and sometimes to bool values such as is_coinbase_warm or is_caller_callee_equal. What is is_caller_callee_equal for?
2. There's expression: https://github.com/privacy-scaling-explorations/zkevm-circuits/blob/main/zkevm-circuits/src/evm_circuit/execution/begin_tx.rs#L163
   Why do we have summation - if is_empty_code_hash.expr() is enough (as well as callee_not_exists is enough)?
3. What's caller_nonce_hash_bytes? Is it Keccak(sender, nonce) and we have to constrain this exact value?

[ChihChengLiang]

Quick comment for the first batch of questions. I'll comment more next.

[curryrasul]

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

[ed255]

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

[curryrasul]

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

[curryrasul]

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.

[ed255]

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.

[curryrasul]

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?

[ed255]

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:

• self.caller_address (via self.caller_address_rlc())
• self.nonce
  Which are unconstrained at the construction of the gadget:
  

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

  Lines 219 to 220 in 3bbc757

  	let caller_address = cb.query_account_address();
  	let nonce = RlpU64Gadget::construct(cb);

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

[ed255]

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| {

[curryrasul]

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

[ed255]

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

[curryrasul]

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

[ed255]

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

[curryrasul]

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.

[ed255]

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.

[curryrasul]

Thanks a lot for explanation

[ed255]

A part from the dbg! line, all looks good!

[ed255]

This slipped through! Can you remove it?

[curryrasul]

Sorry, missed that. Done!

[ChihChengLiang]

LGTM 👍🏽