Skip to content
This repository has been archived by the owner on Jul 5, 2024. It is now read-only.

Add missing state circuit constraints #520

Merged
merged 14 commits into from
Apr 10, 2024
Merged

Add missing state circuit constraints #520

Changes from 6 commits
Commits
Show all changes
14 commits
Select commit Hold shift + click to select a range
483c3d7
synchronize state constraints
ashWhiteHat Apr 27, 2023
ca8160f
6.4 state_root eq prev
ChihChengLiang Apr 5, 2024
6e3dfd6
7.1 field_tag in AccountFieldTag range
ChihChengLiang Apr 5, 2024
c28344a
7.3 value copy from value_prev
ChihChengLiang Apr 5, 2024
53083b9
10.3 state_root eq prev
ChihChengLiang Apr 5, 2024
e086d92
11.2 state_root eq prev
ChihChengLiang Apr 5, 2024
8383f6e
9.3 state_root eq prev
ChihChengLiang Apr 5, 2024
bfefdb1
9.2 initial value is 0
ChihChengLiang Apr 5, 2024
35875e8
12.5 both value_prev and initial_value are 0
ChihChengLiang Apr 5, 2024
79589bd
6.2 10.4 first access read condition
ChihChengLiang Apr 5, 2024
a085cb6
rm 9.4 first access read
ChihChengLiang Apr 5, 2024
ace3d2e
Update specs/state-proof.md
ChihChengLiang Apr 5, 2024
a5c3699
8.1 state root eq
ChihChengLiang Apr 9, 2024
8a2f518
11.0 is_write -> true
ChihChengLiang Apr 9, 2024
File filter

Filter by extension

Filter by extension
Conversations
Failed to load comments.
Loading
Jump to
Jump to file
Failed to load files.
Loading
Diff view
Diff view
33 changes: 24 additions & 9 deletions specs/state-proof.md
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -48,6 +48,7 @@ to not be in the table.
- 1.2. `value` is 0
- 1.3. `initial_value` is 0
- 1.4. `state root` is the same if it's not first row
- 1.5. `value_prev` is 0

### Memory
- 2.0. `field_tag` and `storage_key` are 0
Expand All @@ -56,6 +57,7 @@ to not be in the table.
- 2.3. `value` is byte
- 2.4. `initial_value` is 0
- 2.5. `state root` is the same
- 2.6. `value_prev` equals `initial_value`

### Stack

Expand All @@ -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
ChihChengLiang marked this conversation as resolved.
Show resolved Hide resolved
- 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)
Copy link
Contributor

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

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

Copy link
Contributor

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

Account has the same issue

-
- 4.2. `value` column at previous rotation equals `value_prev` at current rotation

### Transient Storage
- 5.0. `field_tag` is 0

Expand All @@ -78,11 +82,14 @@ to not be in the table.
- 6.1. `field_tag` is in CallContextFieldTag range
- 6.2. `value` is 0 if first access and READ
ChihChengLiang marked this conversation as resolved.
Show resolved Hide resolved
- 6.3. `initial value` is 0
- 6.4. `state root` is the same
- 6.4. `state_root` eqauls `state_root_prev`
- 6.5. `value_prev` is 0

### Account
Copy link
Contributor

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

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

- 7.0. `id` and `storage_key` are 0
- 7.1. MPT storage lookup for last access to (address, field_tag)
- 7.1. `field_tag` is in AccountFieldTag range
- 7.2. MPT storage lookup for last access to (address, field_tag)
- 7.3. `value` column at previous rotation equals `value_prev` at current rotation

### Tx Refund
Copy link
Contributor

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

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

Copy link
Contributor

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

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?

- 8.0. `address`, `field_tag` and `storage_key` are 0
Expand All @@ -92,25 +99,33 @@ to not be in the table.

### Tx Access List Account
- 9.0. `field_tag` and `storage_key` are 0
- 9.1. `state root` is the same
- 9.2. First access for a set of all keys are 0 if `READ`

- 9.1. `value` is boolean
- 9.2. `initial_value` is false
ChihChengLiang marked this conversation as resolved.
Show resolved Hide resolved
- 9.3. `state root` is the same
ChihChengLiang marked this conversation as resolved.
Show resolved Hide resolved
- 9.4. First access for a set of all keys are 0 if `READ`
Copy link
Contributor

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

We don't have 9.4 in our circuit

Copy link
Contributor

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

Same comment as for tx refund

Copy link
Collaborator Author

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

removed rm 9.4 first access read

- 9.5. `value` column at previous rotation equals `value_prev` at current rotation

### Tx Access List Account Storage
- 10.0. `field_tag` is 0
- 10.1. `state root` is the same
- 10.2. First access for a set of all keys are 0 if `READ`
- 10.1. `value` is boolean
- 10.2. `initial_value` is 0
- 10.3. `state_root` eqauls `state_root_prev`
- 10.4. First access for a set of all keys are 0 if `READ`
ChihChengLiang marked this conversation as resolved.
Show resolved Hide resolved
- 10.5. `value` column at previous rotation equals `value_prev` at current rotation

### Tx Log
- 11.0. `is_write` is 1
ChihChengLiang marked this conversation as resolved.
Show resolved Hide resolved
- 11.1. `state root` is the same
- 11.1. `initial_value` is 0
- 11.2. `state_root` eqauls `state_root_prev`
- 11.3. `value_prev` equals `initial_value`

### Tx Receipt
KimiWu123 marked this conversation as resolved.
Show resolved Hide resolved
- 12.0. `address` and `storage_key` are 0
- 12.1. `field_tag` is boolean (according to EIP-658)
- 12.2. `tx_id` increases by 1 and `value` increases as well if `tx_id` changes
- 12.3. `tx_id` is 1 if it's the first row and `tx_id` is in 11 bits range
- 12.4. `state root` is the same
- 12.5. `value_prev_column` is 0
ChihChengLiang marked this conversation as resolved.
Show resolved Hide resolved

## About Account and Storage accesses

Expand Down
Loading