Spec for opcode BALANCE

[silathdiir]

Circuit: privacy-ethereum/zkevm-circuits#683

Not confirm if necessary to constrain "If the given account doesn't exist, then it will push 0 onto the stack instead." in the circuit.
And is there a method (could be used in circuit) to lookup if account is existing? Thanks.

[CPerezz]

The implementation looks good.

Some questions regarding the markdown specs.

[CPerezz]

To be honest I'm not sure about:

necessary to constrain "If the given account doesn't exist, then it will push 0 onto the stack instead." in the circuit.
And is there a method (could be used in circuit) to lookup if account is existing?

This got me thinking. I'd say yes, we definitely need to do this check right? But how? How can we assert that an account exists? This would require a lookup and I think we don't have any mechanism in our tables (see https://github.com/privacy-scaling-explorations/zkevm-specs/blob/master/specs/tables.md) that allows us to gather this info.

We would need to have a table with all the accounts for which we need to check it's existance. Or at the very least, to add a tag for this thing in the rw table for example.
cc: @han0110 @ed255

[ed255]

To be honest I'm not sure about:

necessary to constrain "If the given account doesn't exist, then it will push 0 onto the stack instead." in the circuit.
And is there a method (could be used in circuit) to lookup if account is existing?

This got me thinking. I'd say yes, we definitely need to do this check right? But how? How can we assert that an account exists? This would require a lookup and I think we don't have any mechanism in our tables (see https://github.com/privacy-scaling-explorations/zkevm-specs/blob/master/specs/tables.md) that allows us to gather this info.

We would need to have a table with all the accounts for which we need to check it's existance. Or at the very least, to add a tag for this thing in the rw table for example. cc: @han0110 @ed255

Here's a summary of a discussion we had about this via chat:

There are 2 options for the MPT table API.
A. One is that you just do a balance lookup, and the MPT circuit constraints the value to be 0 when the account doesn't exist (using an MPT proof of non-existence).
B. The other option is to have a tag for the MPT table for account exists, which would mean that the BALANCE opcode needs to do 2 lookups:

1. Account exists
2. Account balance
   I think option B is simpler for the MPT circuit, but I'm not sure if it already supports option A.

Some circuits require proving that an account doesn't exist. With option B that is done with a single lookup. With option A that would be done with the check nonce == 0 && balance == 0 && code_hash == empty_hash.

I'm more favorable towards option B.

For this PR I would say to go with one of the options (probably option A is simpler), and then we can revisit all lookups to non-existing accounts if necessary once we settle on which option we take.

[CPerezz]

Pending on #249 update

[silathdiir]

Hi @CPerezz and @ed255, I updated the code to use option A to check account existence (via nonce == 0 && balance == 0 && code_hash == empty_hash), and add a TODO for updating later when the issue #249 is fixed.

Please help review again when you have time. Thanks.

[CPerezz]

Hey @silathdiir I think that #249 is close enough to be merged that this will not be necessary. And we can wait, rebase this on the top of the new main and then resolve the TODO in this PR.

Note that this means that we'll need to go for option 2.
Hope you agree with that! :)

[silathdiir]

Hey @silathdiir I think that #249 is close enough to be merged that this will not be necessary. And we can wait, rebase this on the top of the new main and then resolve the TODO in this PR.

Note that this means that we'll need to go for option 2. Hope you agree with that! :)

Got it. Will try to update after #249 is closed. Thanks.

[ed255]

#291 should unlock this PR

[ed255]

@silathdiir #291 has just been merged, so this PR is now unlocked to be completed :)

[silathdiir]

@silathdiir #291 has just been merged, so this PR is now unlocked to be completed :)

Thanks a lot. I updated this PR according to #291 (will update similar code of extcodehash in another PR).

@CPerezz @ed255 please help review again when you have time. Thanks.

[adria0]

Is reversible_write_counter always zero?

[silathdiir]

I tried to review reversible-write-reversion doc. It seems that reversible_write_counter should be initialized to 0.

And I referenced the code of test_extcodecopy.py and test_extcodehash.py.

[adria0]

I readed the document for first time, and, ups, it's tricky!

BTW I changed with random values this lines in SLOAD and test are passing

https://github.com/privacy-scaling-explorations/zkevm-specs/blob/947e012c6d8d1566b295f8bfd717a82eeb475e18/tests/evm/test_sload.py#L56-L57

so are we missing something here? (cc/ @ed255 @ChihChengLiang )

unsure about this revertion parameters, but for the rest, LGTM

[ed255]

I think in this test the rw_counter_end_of_reversion and reversible_write_counter are not super relevant because we're only checking the constraints of the BALANCE step with the STOP/REVERT step as next. But we're not checking the constraints of the STOP/REVERT step.
The constraints related to rw_counter_end_of_reversion and reversible_write_counter are checked during the REVERT step, so even if we have wrong values here the test would pass.

As @silathdiir reversible_write_counter should start at 0 when a call begins. I think rw_counter_end_of_reversion should be 9 + the count of reversible operations that happened (which I think should be 1 for the account access list write).

[silathdiir]

Fixed rw_counter_end_of_reversion to 10 with comment:

# 9 + 1 reversible operation (the account access list write)
rw_counter_end_of_reversion = 0 if is_persistent else 10

[adria0]

I readed the document for first time, and, ups, it's tricky!

BTW I changed with random values this lines in SLOAD and test are passing

https://github.com/privacy-scaling-explorations/zkevm-specs/blob/947e012c6d8d1566b295f8bfd717a82eeb475e18/tests/evm/test_sload.py#L56-L57

so are we missing something here? (cc/ @ed255 @ChihChengLiang )

unsure about this revertion parameters, but for the rest, LGTM

[ed255]

I think in this test the rw_counter_end_of_reversion and reversible_write_counter are not super relevant because we're only checking the constraints of the BALANCE step with the STOP/REVERT step as next. But we're not checking the constraints of the STOP/REVERT step.
The constraints related to rw_counter_end_of_reversion and reversible_write_counter are checked during the REVERT step, so even if we have wrong values here the test would pass.

As @silathdiir reversible_write_counter should start at 0 when a call begins. I think rw_counter_end_of_reversion should be 9 + the count of reversible operations that happened (which I think should be 1 for the account access list write).

[ed255]

I noticed that in a few places the rwc counter increase is outdated (check my suggested changes).
Other than that, everything looks good!

[silathdiir]

I noticed that in a few places the rwc counter increase is outdated (check my suggested changes).
Other than that, everything looks good!

I updated code according to the suggestions. Thanks a lot.

[ed255]

LGTM! Great work!