Implement constraints in state circuit spec by z2trillion · Pull Request #462 · privacy-ethereum/zkevm-circuits

z2trillion · 2022-04-14T04:13:12Z

This implements the constraints found in https://github.com/appliedzkp/zkevm-specs/blob/master/src/zkevm_specs/state.py, except for the https://github.com/appliedzkp/zkevm-specs/blob/f33ae436011cde6cf76b92e316e00662cd4ef2e1/src/zkevm_specs/state.py#L178 and https://github.com/appliedzkp/zkevm-specs/blob/master/src/zkevm_specs/state.py#L209. Adding those will require modifying the bus mapping to add the Rw::Start rows, so I will do it in a separate PR.

lispc · 2022-04-14T07:04:11Z

+    }
+
+    fn configure(meta: &mut ConstraintSystem<F>) -> Self::Config {
+        let selector = meta.fixed_column();


what about changing selector into advice column? Since it is not "fixed" now. ( We assign "1" to it only when a row is non empty, so this column is dynamic.)

There needs to be a fixed column or selector involved in each of the constraints, or the MockProver will return a ConstraintPoisoned error when it tries to verify.

We can fill up all the otherwise empty rows with Rw::Start's so that the selector column will not be dynamic. I haven't quite figured out how to do this without massively slowing down the tests though.

verify_at_rows can be helpful for this problem.

scroll-tech@34eb52f

Address this comment?

"fill up all the otherwise empty rows with Rw::Start" is also a bit counterintuitive..
Maybe we can merge this PR first(since we don't know how to fix it very cleanly now?), then revisit this problem (make sure vk generated from one circuit instance can verify another circuit) later.

ntampakas · 2022-04-14T11:01:30Z

Bench failed with the following error:

running 1 test
Start:   Setup generation with degree = 19
test state_circuit::tests::bench_state_circuit_prover has been running for over 60 seconds
End:     Setup generation with degree = 19 .........................................582.270s
[zkevm-circuits/src/state_circuit.rs:171] self.rows.clone() = []
[zkevm-circuits/src/state_circuit.rs:171] self.rows.clone() = []
Start:   State Proof generation with 19 rows
thread 'state_circuit::tests::bench_state_circuit_prover' panicked at 'proof generation should not fail: InvalidInstances', circuit-benchmarks/src/state_circu
it.rs:53:10
note: run with `RUST_BACKTRACE=1` environment variable to display a backtrace
test state_circuit::tests::bench_state_circuit_prover ... FAILED

failures:

failures:
    state_circuit::tests::bench_state_circuit_prover

test result: FAILED. 0 passed; 1 failed; 0 ignored; 0 measured; 2 filtered out; finished in 618.72s

error: test failed, to rerun pass '-p circuit-benchmarks --lib'

lispc · 2022-04-14T13:17:26Z

Bench failed with the following error:

running 1 test
Start:   Setup generation with degree = 19
test state_circuit::tests::bench_state_circuit_prover has been running for over 60 seconds
End:     Setup generation with degree = 19 .........................................582.270s
[zkevm-circuits/src/state_circuit.rs:171] self.rows.clone() = []
[zkevm-circuits/src/state_circuit.rs:171] self.rows.clone() = []
Start:   State Proof generation with 19 rows
thread 'state_circuit::tests::bench_state_circuit_prover' panicked at 'proof generation should not fail: InvalidInstances', circuit-benchmarks/src/state_circu
it.rs:53:10
note: run with `RUST_BACKTRACE=1` environment variable to display a backtrace
test state_circuit::tests::bench_state_circuit_prover ... FAILED

failures:

failures:
    state_circuit::tests::bench_state_circuit_prover

test result: FAILED. 0 passed; 1 failed; 0 ignored; 0 measured; 2 filtered out; finished in 618.72s

error: test failed, to rerun pass '-p circuit-benchmarks --lib'

related to #458

miha-stopar

I really like the new structure, it's really nice and easily readable! I just did a first pass though, will do some more reviewing in the next days.

miha-stopar · 2022-04-15T08:33:35Z

+        // q.rw_counter.value.clone()); });
+    }
+
+    fn build_account_destructed_constraints(&mut self, q: &Queries<F>) {


A similar method for when an account is created is probably needed?
Also, an MPT lookup is needed here too, right (whenever something changes in the state trie)?

These are the constraints for rows that match Rw::AccountDestructed. I believe that up to three Rw::Account will exist in the rw table for account creations? The constraints for these rows are in the build_account_constraints function.

I agree MPT lookup(s) will be required here. I need to review the specs to see what our plans (if any) are for handling account desctruction rows.

Yes, for the account creation I think we would have three modular changes - changing only one field at a time: nonce, balance, codehash. And we would need to add constraints for the order of these three changes. Is that right @han0110 @ed255 ?

But I think we could leave this for the future PR.

Regarding the account destructed, I remember from a discussion with @han0110 that he mentioned that after a SELFDESTRUCT the account is not immediately deleted. Looking at the yellowpaper I see:

SELFDESTRUCT: Halt execution and register account for later deletion.

So an account destructed row is not directly connected to the MPT, but we need to figure out a way to keep track of all pending account deletes, and at the step EndTx process all those deletions. Maybe we need to introduce a new tag in the state that signals an account deletion (which must match a previous non-reverted account destruction). Currently that's open to be specified.

Regarding account creation, I guess there are several ways to create an account:

Send balance to an empty account.

Tx with to = 0x0, CREATE, CREATE2

1 and 2 set different account fields.
I would assume that a non-existing account has the fields to a default value, and on account creation some of those fields are set to a different value. This makes me wonder if we need to explicitly set all the fields, or just the ones that get a non-default value; and I also wonder how the MPT handles non-existing accounts VS existing accounts with default values in their fields.

Yes, the accounts are deleted when root is recomputed.

Non-existing accounts are not stored in the trie (no leaf at the position specified by the account address), while for the account with default values there is a leaf which contains default values. However, in MPT circuit, when there is no account, a placeholder leaf with default values is set, so the lookup should contain default value as previous value. Because currently MPT circuit allows only one change at a time, there would be four lookups needed for the account creation. Just working on that actually. Let me prepare a hackmd note on that.

I am not very familiar with the current mpt circuit. But just a remainder: "However, in MPT circuit, when there is no account, a placeholder leaf with default values is set, so the lookup should contain default value as previous value.", maybe we should be very careful about the soundness if we allow both "non exist account(not exist in tree)" and "account with default value", where same semantic trees can have different roots.

I think this EIP can be very useful when reasoning about empty accounts and how they are represented in the MPT: https://eips.ethereum.org/EIPS/eip-161

I am not very familiar with the current mpt circuit. But just a remainder: "However, in MPT circuit, when there is no account, a placeholder leaf with default values is set, so the lookup should contain default value as previous value.", maybe we should be very careful about the soundness if we allow both "non exist account(not exist in tree)" and "account with default value", where same semantic trees can have different roots.

Agree, but I think I just didn't phrase it clearly. The two tries (with non-existent account and account with default values) are not equivalent in the MPT circuit, it's just that in case of a non-existent account a placeholder leaf is added not to break the MPT circuit layout. This placeholder leaf is then ignored in the circuit, but the circuit of course checks that this leaf is actually empty - this check happens in the branch (below this branch a placeholder leaf resides).

miha-stopar · 2022-04-15T08:38:56Z

+// 30 limbs in total -> can fit into two field elements
+#[derive(Clone)]
+pub struct Config<F: Field> {
+    diff_1: Column<Advice>,


Would it be possible to add a short description of this chip and especially of diff_1 and diff_2 fields?

I've added a comment describing this chip. I would love to hear any suggestions for better names for diff_1 and diff_2.

Thanks, it makes reading the code much easier! For diff_1 and diff_2 naming I am not sure - perhaps something that would give some intuition, like aggregated_limbs_1, aggregated_limbs_2? It would be also good perhaps to add some rationale why limbs are split into two parts, it's because of field overflow, right?

Why not just encode 6 fields into two 240-bit values, A_hi and A_lo? Then you just need to compare two 240-bit values, and only the diff needs to be encoded in 16-bit limbs for range check.

That would definately be easier to understand and explain, but it would require 30 advice columns for the limbs of the diff_hi and diff_lo instead of the 4 we use now.

agree. Proving cost of adding new gates is much smaller than adding new columns.

DreamWuGit · 2022-04-22T03:21:27Z

+#[derive(Clone)]
+pub struct Queries<F: Field, const N: usize> {
+    pub encoded: Expression<F>,
+    pub encoded_prev: Expression<F>,


want to know usage of encoded_prev, don't see its constraint anywhere

it's not used in the constraints anywhere for consistency with the specs in https://github.com/appliedzkp/zkevm-specs/blob/master/src/zkevm_specs/state.py, but those constraints will need to be added.

miha-stopar · 2022-04-25T12:45:22Z

+            .find(|(_, (a, b))| a != b);
+        let (index, (cur_limb, prev_limb)) = find_result.expect("repeated rw counter");
+
+        let mut diff_1 = F::from((cur_limb - prev_limb).into());


Doesn't this diff_1 computation imply diff_1 can only be Ai - Bi and not one of the following (cumulative) values specified above in the comment (and also used in the constraint):
// C0 = A0 - B0,
// C1 = C0 << 16 + A1 - B1,
// ...
// C14 = C13 << 16 + A14 - B14,

The constraints don't fail because Ci are 0 by having diff_1 computed this way.

The diff_1 computation implies only one change can occur in the first 15 limbs. Could be some explanation added why this is so? Also, specs repo doesn't seem to have info how lexicographic ordering is to be implemented, could that be added?

I think it's more clear to view it the other way around. The only way that diff_1 can only be one of the 15 values C0, ..., C14, and that diff_1 can fit into 16 bits is for diff_1 to be the first Ai - Bi such that Aj = Bj for j < i.

You're right that multiple difference can occur between the first 15 pairs of limbs, but (I think) that the constraints are such that diff_1 has to be the value of the most significant non-zero limb difference.

The specs are for lexicographic ordering in the spec repo are in the code here: https://github.com/scroll-tech/zkevm-specs/blob/master/src/zkevm_specs/state.py#L355. I plan to update that section and the book once the implementation is finalized here. I had to make some changes to how the bit-packing of the keys worked so that everything could fit into 2 field elements.

I think I got it now, thanks!

I think it would be helpful to add such details as above to the comments and docs. Perhaps write something like (if I understood correctly):

Assignment: diff_i is change in the 15 limbs that occurs first (if prev = (2, 1, 2, ...), curr = (2, 1, 6, ...), then diff_i = 4.
Constraint: diff_i will be equal to the first non-zero Ci.

Perhaps you could rename diff_1, diff_2 to first_diff_high, first_diff_low?

I've renamed them to upper_limb_difference and lower_limb_difference.

Cool, thanks!

lispc · 2022-04-29T04:51:22Z

-        prover.verify()?;
+        let state_circuit = StateCircuit::new(block.randomness, block.rws);
+        let power_of_randomness = state_circuit.instance();
+        let prover = MockProver::<Fr>::run(18, &state_circuit, power_of_randomness).unwrap();


For evm circuit, we dynamically decide the k. So many small tests will use only k = 12 (without bitwise fixed table).
If we use k = 18 for every state circuit here(since some big fixed tables are needed), the CI time will be quite long.

@han0110 @ed255 Do you have any thoughts in this?

what do you think about setting enable_state_circuit_test to be false for evm circuit tests, once we add more state circuit tests?

what do you think about setting enable_state_circuit_test to be false for evm circuit tests, once we add more state circuit tests?

This sounds like a good tradeoff to me.

ed255 · 2022-05-03T14:18:06Z

I assume that currently this PR is assigned to be reviewed by @miha-stopar (from the EF side) and either icemelon OR lispc OR DreamWuGit (from scroll-tech side). Let me know if you'd like me to review it as well at any point!

z2trillion · 2022-05-04T03:06:29Z

@miha-stopar , can you take a look at this again, please?

miha-stopar

LGTM

icemelon

LGTM

icemelon · 2022-05-05T18:24:32Z

+    }
+
+    fn configure(meta: &mut ConstraintSystem<F>) -> Self::Config {
+        let selector = meta.fixed_column();


Address this comment?

…ence

z2trillion requested a review from miha-stopar as a code owner April 14, 2022 04:13

z2trillion requested a review from a team April 14, 2022 04:13

z2trillion marked this pull request as draft April 14, 2022 04:13

lispc reviewed Apr 14, 2022

View reviewed changes

barryWhiteHat added the benchmarks: State Triggers a State circuit benchmark label Apr 14, 2022

z2trillion force-pushed the feat/state_circuit_refactor branch from 34eb52f to 340f324 Compare April 14, 2022 15:58

miha-stopar reviewed Apr 15, 2022

View reviewed changes

DreamWuGit reviewed Apr 22, 2022

View reviewed changes

miha-stopar reviewed Apr 25, 2022

View reviewed changes

z2trillion force-pushed the feat/state_circuit_refactor branch from f6b97c6 to eb88bc4 Compare April 28, 2022 18:29

z2trillion marked this pull request as ready for review April 28, 2022 18:31

z2trillion requested a review from pinkiebell as a code owner April 28, 2022 18:31

lispc reviewed Apr 29, 2022

View reviewed changes

This was referenced May 2, 2022

WIP state circuit: implement new spec scroll-tech/zkevm-circuits#111

Closed

state circuit: implement new spec part2 scroll-tech/zkevm-circuits#125

Closed

z2trillion requested a review from miha-stopar May 3, 2022 01:40

lispc approved these changes May 4, 2022

View reviewed changes

lispc mentioned this pull request May 4, 2022

Refactor StateCircuit + add lexicographic ordering constraints scroll-tech/zkevm-circuits#135

Closed

miha-stopar approved these changes May 4, 2022

View reviewed changes

icemelon approved these changes May 5, 2022

View reviewed changes

lispc mentioned this pull request May 6, 2022

META: management of "lts" branch named like scroll-dev-MMDD scroll-tech/zkevm-circuits#145

Closed

z2trillion and others added 25 commits May 9, 2022 20:15

Rename test files for clippy

e7c47c4

Cleanup benchmarks

450a202

fix build

79bff4a

Assign diff_inverse correctly

e39b198

Fix instance function and convert it to a method

ea9c4f8

Fix storage_key_be_limbs method

25750df

Add degree test

f8e6676

Have StateCircuit use Vec<Rw> instead of RwMap

691ea89

Compute first_access correctly

04847ec

wip, but tests pass

374cf71

Fix diff_2 assignment

c491a3a

cleanup

a3a5ce5

Use verify_at_rows to speed up tests and derive EnumIter

36293e5

Add cleanup and explain diff_1 and diff_2

37c0644

cleanup

12cb311

fmt

96bee8c

Add newline to fix cargo fmt

247c591

Fix degree test and TxLog table assignment

5a69934

Cleanup and change index type to u8 from usize

a96321f

Rename to diff_1->upper_limb_difference and diff_2->lower_limb_differ…

808c7fe

…ence

Explain assignment in comments

dd6126a

fix conflicts

243a012

lint

14c0f29

fix rebase

2295a4e

fix build and tests from rebase

fb920b8

z2trillion force-pushed the feat/state_circuit_refactor branch from 4746ee2 to fb920b8 Compare May 10, 2022 00:44

make change to rerun tests

19e25dc

icemelon merged commit 818cf2e into privacy-ethereum:main May 10, 2022

icemelon deleted the feat/state_circuit_refactor branch May 10, 2022 06:18

han0110 mentioned this pull request Jun 29, 2022

bug: value_assignment of Rw::Account Nonce is inconsistent #592

Closed

Conversation

z2trillion commented Apr 14, 2022

Uh oh!

lispc Apr 14, 2022 • edited Loading Uh oh! There was an error while loading. Please reload this page.

Uh oh!

Choose a reason for hiding this comment

Uh oh!

Choose a reason for hiding this comment

Uh oh!

Choose a reason for hiding this comment

Uh oh!

Choose a reason for hiding this comment

Uh oh!

lispc May 6, 2022 • edited Loading Uh oh! There was an error while loading. Please reload this page.

Uh oh!

Choose a reason for hiding this comment

Uh oh!

ntampakas commented Apr 14, 2022

Uh oh!

lispc commented Apr 14, 2022

Uh oh!

miha-stopar left a comment

Choose a reason for hiding this comment

Uh oh!

Choose a reason for hiding this comment

Uh oh!

Choose a reason for hiding this comment

Uh oh!

Choose a reason for hiding this comment

Uh oh!

Choose a reason for hiding this comment

Uh oh!

Choose a reason for hiding this comment

Uh oh!

lispc May 4, 2022 • edited Loading Uh oh! There was an error while loading. Please reload this page.

Uh oh!

Choose a reason for hiding this comment

Uh oh!

Choose a reason for hiding this comment

Uh oh!

Choose a reason for hiding this comment

Uh oh!

Choose a reason for hiding this comment

Uh oh!

Choose a reason for hiding this comment

Uh oh!

Choose a reason for hiding this comment

Uh oh!

Choose a reason for hiding this comment

Uh oh!

Choose a reason for hiding this comment

Uh oh!

Choose a reason for hiding this comment

Uh oh!

Choose a reason for hiding this comment

Uh oh!

Choose a reason for hiding this comment

Uh oh!

Uh oh!

Choose a reason for hiding this comment

Uh oh!

Choose a reason for hiding this comment

Uh oh!

Choose a reason for hiding this comment

Uh oh!

Choose a reason for hiding this comment

Uh oh!

Choose a reason for hiding this comment

Uh oh!

lispc Apr 29, 2022 • edited Loading Uh oh! There was an error while loading. Please reload this page.

Uh oh!

Choose a reason for hiding this comment

Uh oh!

Choose a reason for hiding this comment

Uh oh!

Choose a reason for hiding this comment

Uh oh!

ed255 commented May 3, 2022

Uh oh!

z2trillion commented May 4, 2022 • edited Loading Uh oh! There was an error while loading. Please reload this page.

lispc Apr 14, 2022 •

edited

Loading

lispc May 6, 2022 •

edited

Loading

lispc May 4, 2022 •

edited

Loading

lispc Apr 29, 2022 •

edited

Loading

z2trillion commented May 4, 2022 •

edited

Loading