Add missing state circuit constraints #520
Conversation
There was a problem hiding this comment.
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.
specs/state-proof.md
Outdated
| - 9.1. `value` is boolean | ||
| - 9.2. `initial_value` is false | ||
| - 9.3. `state root` is the same | ||
| - 9.4. First access for a set of all keys are 0 if `READ` |
There was a problem hiding this comment.
We don't have 9.4 in our circuit
There was a problem hiding this comment.
Same comment as for tx refund
There was a problem hiding this comment.
removed rm 9.4 first access read
| @@ -65,11 +67,13 @@ to not be in the table. | |||
| - 3.3. Stack pointer increases 0 or 1 only | |||
| - 3.4. `initial_value` is 0 | |||
| - 3.5. `state root` is the same | |||
| - 3.6. `value_prev` equals `initial_value` | |||
|
|
|||
| ### Storage | |||
| - 4.0. `field_tag` is 0 | |||
| - 4.1. MPT lookup for last access to (address, storage_key) | |||
There was a problem hiding this comment.
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
There was a problem hiding this comment.
Account has the same issue
| @@ -79,10 +83,12 @@ to not be in the table. | |||
| - 6.2. `value` is 0 if first access and READ | |||
| - 6.3. `initial value` is 0 | |||
| - 6.4. `state root` is the same | |||
| - 6.5. `value_prev` is 0 | |||
|
|
|||
| ### Account | |||
There was a problem hiding this comment.
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
|
|
||
| ### Account | ||
| - 7.0. `id` and `storage_key` are 0 | ||
| - 7.1. MPT storage lookup for last access to (address, field_tag) | ||
| - 7.2. `value_prev` equals `initial_value` | ||
|
|
||
| ### Tx Refund |
There was a problem hiding this comment.
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
There was a problem hiding this comment.
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?
specs/state-proof.md
Outdated
| - 9.1. `value` is boolean | ||
| - 9.2. `initial_value` is false | ||
| - 9.3. `state root` is the same | ||
| - 9.4. First access for a set of all keys are 0 if `READ` |
There was a problem hiding this comment.
Same comment as for tx refund
|
Overall good! Just a few constraints that are missed and some nitpicking. Extra nipicking: should we replace |
|
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 |
specs/state-proof.md
Outdated
| - 9.1. `value` is boolean | ||
| - 9.2. `initial_value` is false | ||
| - 9.3. `state root` is the same | ||
| - 9.4. First access for a set of all keys are 0 if `READ` |
There was a problem hiding this comment.
removed rm 9.4 first access read
Co-authored-by: Raphael <raphael.r.toledo@gmail.com>
|
@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? |
| @@ -65,11 +67,13 @@ to not be in the table. | |||
| - 3.3. Stack pointer increases 0 or 1 only | |||
| - 3.4. `initial_value` is 0 | |||
| - 3.5. `state root` is the same | |||
| - 3.6. `value_prev` equals `initial_value` | |||
|
|
|||
| ### Storage | |||
| - 4.0. `field_tag` is 0 | |||
| - 4.1. MPT lookup for last access to (address, storage_key) | |||
There was a problem hiding this comment.
Account has the same issue
We rebase and apply the work from #415.