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 <[email protected]>

* 8.1 state root eq

* 11.0 is_write -> true

---------

Co-authored-by: ashWhiteHat <[email protected]>
Co-authored-by: Raphael <[email protected]>

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,53 +66,63 @@ 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
 - 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` is 0 and `initial_value` is 0
 
 ## About Account and Storage accesses