synchronize state constraints

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
 
@@ -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)
-- 
+- 4.2. `value` column at previous rotation equals `value_prev` at current rotation
+
 ### Transient Storage
 - 5.0. `field_tag` is 0
 
@@ -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
 - 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
 - 8.0. `address`, `field_tag` and `storage_key` are 0
@@ -92,25 +98,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
+- 9.3. `state root` is the same
+- 9.4. First access for a set of all keys are 0 if `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 false
+- 10.3. `state root` is the same
+- 10.4. First access for a set of all keys are 0 if `READ`
+- 10.5. `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.1. `initial_value` is 0
+- 11.2. `state root` is the same
+- 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_column` is 0
 
 ## About Account and Storage accesses