Add missing state circuit constraints

[ChihChengLiang]

We rebase and apply the work from #415.

[KimiWu123]

initial_value and value_prev are not used for some of tags. Some of them describe it as initial_value is 0 and value_prev equals initial_value and others are initial_value is 0 and value_prev is 0. We should align it and it happens at 1, 2, 3, 6, 11 and 12.

I would suggest to describe it as initial_value is 0 and value_prev is 0 bcs it looks more straightforward and one can easily understand we're not using these columns for the tag.

[KimiWu123]

We don't have 9.4 in our circuit

[rrtoledo]

Same comment as for tx refund

[ChihChengLiang]

removed rm 9.4 first access read

[ChihChengLiang]

Resolved some feedback that I'm confident fixing correctly.

[rrtoledo]

There is the constraint "mpt_proof_type is field_tag or NonExistingStorageProof" in the code that is before 4.1.
I'd suggest to either gathering the two under 4.1 and perhaps writing a bit more to explain the constrain, or to add another 4.x for it here

[rrtoledo]

Account has the same issue

[rrtoledo]

Nitpicking: we could update the code so that the constraints "blocks" (account, tx refund...) are in the same order (and make sure all are numbered) as in the specs

[rrtoledo]

8.1 to be changed to something like : state_root equals state_root_prev

p.s. nitpicking: in the code this section is 7.x so needs to be updated

[rrtoledo]

Constraint in spec 8.3 and code differs:
- 8.3. First access for a set of all keys are 0 if READ``

        self.condition(q.not_first_access.clone(), |cb| {
            cb.require_word_equal(
                "value column at Rotation::prev() equals value_prev at Rotation::cur()",
                q.rw_table.value_prev.clone(),
                q.value_prev_column(),
            );
        });

From the general constraints, we have that at the first access, the value_prev_column equals the initial value. From 8.2 we have that init value = 0. And now we have that, at all but the first access, the value at the previous rotation equals value value_prev_column. So all values are indeed set at 0 but there is no if READ condition. Is that implicit?

edit: should that be a new constraint as in 9.5 actually and so 8.3 is missing?

[rrtoledo]

Same comment as for tx refund

[rrtoledo]

Overall good! Just a few constraints that are missed and some nitpicking.

Extra nipicking: should we replace state root by state_root ?

[rrtoledo]

Would it make sense to rename value_prev and value_prev_column (edit: in the code)? I find these a bit confusing.

value_prev: WordLoHi<Expression>, // meta.query(value, Rotation::prev()) could be renamed value_rot_prev for instance
pub value_prev_column: WordLoHi<Expression>, // meta.query(prev_value, Rotation::cur()) be renamed value_prev

[ChihChengLiang]

Finished addressing feedbacks from @KimiWu123

[ChihChengLiang]

removed rm 9.4 first access read

[ChihChengLiang]

@rrtoledo I'm thinking to wrap up this PR as the current state. I'm a little bit lost on what changes to apply. Can you approve the PR?
I plan to create a followup PR and add a "general rule" section to address the feedback for first access and read. apply-415...general-constraints

[rrtoledo]

Account has the same issue