From 4f272c2b6ddfaf2b0815d1b93a6b32e38f5d8fb8 Mon Sep 17 00:00:00 2001 From: Chih Cheng Liang Date: Thu, 11 Apr 2024 00:40:23 +0800 Subject: [PATCH] Add missing state circuit constraints (#520) * synchronize state constraints * 6.4 state_root eq prev * 7.1 field_tag in AccountFieldTag range * 7.3 value copy from value_prev * 10.3 state_root eq prev * 11.2 state_root eq prev * 9.3 state_root eq prev * 9.2 initial value is 0 * 12.5 both value_prev and initial_value are 0 * 6.2 10.4 first access read condition * rm 9.4 first access read * Update specs/state-proof.md Co-authored-by: Raphael * 8.1 state root eq * 11.0 is_write -> true --------- Co-authored-by: ashWhiteHat Co-authored-by: Raphael --- specs/state-proof.md | 40 ++++++++++++++++++++++++++-------------- 1 file changed, 26 insertions(+), 14 deletions(-) diff --git a/specs/state-proof.md b/specs/state-proof.md index 7743704ad..84fdeadbe 100644 --- a/specs/state-proof.md +++ b/specs/state-proof.md @@ -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 @@ -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 @@ -64,46 +66,55 @@ to not be in the table. - 3.2. Stack pointer is less than 1024 - 3.3. Stack pointer increases 0 or 1 only - 3.4. `initial_value` is 0 -- 3.5. `state root` is the same +- 3.5. `state_root` equals `state_root_prev` +- 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) -- +- 4.2. `value` column at previous rotation equals `value_prev` at current rotation + ### Transient Storage - 5.0. `field_tag` is 0 ### Call Context - 6.0. `address` and `storage_key` are 0 - 6.1. `field_tag` is in CallContextFieldTag range -- 6.2. `value` is 0 if first access and READ -- 6.3. `initial value` is 0 -- 6.4. `state root` is the same +- 6.2. `initial value` is 0 +- 6.3. `state_root` eqauls `state_root_prev` +- 6.4. `value_prev` is 0 ### Account - 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 - 8.0. `address`, `field_tag` and `storage_key` are 0 -- 8.1. `state root` is the same +- 8.1. `state_root` eqauls `state_root_prev` - 8.2. `initial_value` is 0 - 8.3. First access for a set of all keys are 0 if `READ` ### 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 0 +- 9.3. `state_root` eqauls `state_root_prev` +- 9.4. `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. `value` column at previous rotation equals `value_prev` at current rotation ### Tx Log -- 11.0. `is_write` is 1 -- 11.1. `state root` is the same +- 11.0. `is_write` is true +- 11.1. `initial_value` is 0 +- 11.2. `state_root` eqauls `state_root_prev` +- 11.3. `value_prev` equals `initial_value` ### Tx Receipt - 12.0. `address` and `storage_key` are 0 @@ -111,6 +122,7 @@ to not be in the table. - 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` is 0 and `initial_value` is 0 ## About Account and Storage accesses