Specs for TLOAD TSTORE (#516)

* add spec for TLOAD and TSTORE * update evm-proof and state-proof specs * create OOG spec * use SLOAD_GAS variable * fix busmapping lookups count
privacy-scaling-explorations · Mar 23, 2024 · cb85f8b · cb85f8b
1 parent 09d1279
commit cb85f8b
Show file tree

Hide file tree

Showing 4 changed files with 146 additions and 33 deletions.
diff --git a/specs/error_state/ErrorOutOfGasTloadTstore.md b/specs/error_state/ErrorOutOfGasTloadTstore.md
@@ -0,0 +1,40 @@
+# ErrorOutOfGasTloadTstore state for both TLOAD and TSTORE OOG errors
+
+## Procedure
+
+Handle the corresponding out of gas errors for both `TLOAD` and `TSTORE` opcodes.
+
+### EVM behavior
+
+The out of gas error may occur for `constant gas`.
+
+#### TLOAD gas cost
+
+For this gadget, TLOAD gas cost in EIP-1153 is specified as the cost of hot SLOAD, currently `100`.
+
+#### TSTORE gas cost
+
+For this gadget, TSTORE gas cost in EIP-1153 is specified as the cost of SSTORE on an already SSTOREd slot, currently `100`.
+
+### Constraints
+
+1. For TLOAD, constrain `gas_left < gas_cost`.
+2. For TSTORE, constrain `gas_left < gas_cost`.
+3. Only for TSTORE, constrain `is_static == false`.
+4. Current call must fail.
+5. If it's a root call, it transits to `EndTx`.
+6. If it isn't a root call, it restores caller's context by reading to `rw_table`, then does step state transition to it.
+7. Constrain `rw_counter_end_of_reversion = rw_counter_end_of_step + reversible_counter`.
+
+### Lookups
+
+7 bus-mapping lookups for TLOAD and 8 for TSTORE:
+
+1. 5 call context lookups for `tx_id`, `is_static`, `callee_address`, `is_success` and `rw_counter_end_of_reversion`.
+2. 1 stack read for `transient_storage_key`.
+3. Only for TSTORE, 1 stack read for `value_to_store`.
+4. Only for TSTORE, 1 account transient storage read.
+
+## Code
+
+> TODO
diff --git a/specs/evm-proof.md b/specs/evm-proof.md
@@ -17,7 +17,7 @@ We define the following Python custom types for type hinting and readability:
 
 ## Random Accessible Data
 
-In EVM, the interpreter has ability to do any random access to data like account balance, account storage, or stack and memory in current scope, but it's hard for the EVM circuit to keep tracking these data to ensure their consistency from time to time. So EVM proof has the state proof to provide a valid list of random read-write access records indexed by the `GlobalCounter` as a lookup table to do random access at any moment.
+In EVM, the interpreter has ability to do any random access to data like account balance, account storage, account transient storage or stack and memory in current scope, but it's hard for the EVM circuit to keep tracking these data to ensure their consistency from time to time. So EVM proof has the state proof to provide a valid list of random read-write access records indexed by the `GlobalCounter` as a lookup table to do random access at any moment.
 
 We call the list of random read-write access records `BusMapping` because it acts like the bus in computer which transfers data between components. Similarly, read-only data are loaded as a lookup table into circuit for random access.
 
@@ -29,6 +29,7 @@ We call the list of random read-write access records `BusMapping` because it act
 | [`AccountBalance`](#AccountBalance)   | `{address}`       | `Read`, `Write` | Account's balance                                                  |
 | [`AccountCodeHash`](#AccountCodeHash) | `{address}`       | `Read`, `Write` | Account's code hash                                                |
 | [`AccountStorage`](#AccountStorage)   | `{address}.{key}` | `Read`, `Write` | Account's storage as a key-value mapping                           |
+| [`AccountTransientStorage`](#AccountTransientStorage)   | `{address}.{key}` | `Read`, `Write` | Account's transient storage as a key-value mapping                           |
 | [`Code`](#Code)                       | `{hash}.{index}`  | `Read`          | Executed code as a byte array                                      |
 | [`Call`](#Call)                       | `{id}.{enum}`     | `Read`          | Call's context decided by caller (includes EOA and internal calls) |
 | [`CallCalldata`](#CallCalldata)       | `{id}.{index}`    | `Read`          | Call's calldata as a byte array (only for EOA calls)               |

diff --git a/specs/opcode/92TLOAD_93TSTORE.md b/specs/opcode/92TLOAD_93TSTORE.md
@@ -0,0 +1,67 @@
+# TLOAD & TSTORE opcodes
+
+## Variables definition
+
+| Name | Value |
+| - | - |
+| SLOAD_GAS | 100 |
+
+## Constraints
+
+1. opcodeId checks
+   1. opId === OpcodeId(0x5c) for `TLOAD`
+   2. opId === OpcodeId(0x5d) for `TSTORE`
+2. state transition:
+   - gc
+     - `TLOAD`: +7
+       - 4 call_context read
+       - 2 stack operations
+       - 1 transient storage reads
+     - `TSTORE`: +8
+       - 5 call_context read
+       - 2 stack operations
+       - 1 transient storage reads/writes
+   - stack_pointer
+     - `TLOAD`: remains the same
+     - `TSTORE`: -2
+   - pc + 1
+   - reversible_write_counter
+     - `TLOAD`: +0
+     - `TSTORE`: +1 (for transient storage)
+   - gas:
+     - `TLOAD`:
+       - gas + SLOAD_GAS
+     - `SSTORE`:
+       - gas + SLOAD_GAS
+3. lookups:
+   - `TLOAD`: 7 busmapping lookups
+     - call_context:
+       - `tx_id`: Read the `tx_id` for this tx.
+       - `rw_counter_end_of_reversion`: Read the `rw_counter_end` if this tx get reverted.
+       - `is_persistent`: Read if this tx will be reverted.
+       - `callee_address`: Read the `callee_address` of this call.
+     - stack:
+       - `key` is popped off the top of the stack
+       - `value` is pushed on top of the stack
+     - transient storage: The 32 bytes of `value` are read from storage at `key`
+   - `TSTORE`: 8 busmapping lookups
+     - call_context:
+       - `tx_id`: Read the `tx_id` for this tx.
+       - `is_static`: Read the call's property `is_static`
+       - `rw_counter_end_of_reversion`: Read the `rw_counter_end` if this tx get reverted.
+       - `is_persistent`: Read if this tx will be reverted.
+       - `callee_address`: Read the `callee_address` of this call.
+     - stack:
+       - `key` is popped off the top of the stack
+       - `value` is popped off the top of the stack
+     - transient storage:
+       - The 32 bytes of new `value` are written to transient storage at `key`, with the previous `value` and `committed_value`
+
+## Exceptions
+
+1. gas out: remaining gas is not enough
+2. stack underflow:
+   - the stack is empty: `1024 == stack_pointer`
+   - only for `TSTORE`: contains a single value: `1023 == stack_pointer`
+3. context error
+   - only for `TSTORE`: the current execution context is from a `STATICCALL` (since Cancun fork).
diff --git a/specs/state-proof.md b/specs/state-proof.md
@@ -12,13 +12,14 @@ The operations recorded in the state proof are:
 2. `Memory`: Call's memory as a byte array
 3. `Stack`: Call's stack as RLC-encoded word array
 4. `Storage`: Account's storage as key-value mapping
-5. `CallContext`: Context of a Call
-6. `Account`: Account's state (nonce, balance, code hash)
-7. `TxRefund`: Value to refund to the tx sender
-8. `TxAccessListAccount`: State of the account access list
-9. `TxAccessListAccountStorage`: State of the account storage access list
-10. `TxLog`: State of the transaction log
-11. `TxReceipt`: State of the transaction receipt
+5. `TransientStorage`: Account's transient storage as key-value mapping
+6. `CallContext`: Context of a Call
+7. `Account`: Account's state (nonce, balance, code hash)
+8. `TxRefund`: Value to refund to the tx sender
+9. `TxAccessListAccount`: State of the account access list
+10. `TxAccessListAccountStorage`: State of the account storage access list
+11. `TxLog`: State of the transaction log
+12. `TxReceipt`: State of the transaction receipt
 
 Each operation uses different parameters for indexing.  See [RW Table](./tables.md#rw_table) for the complete details.
 
@@ -68,52 +69,56 @@ to not be in the table.
 ### Storage
 - 4.0. `field_tag` is 0
 - 4.1. MPT lookup for last access to (address, storage_key)
+- 
+### Transient Storage
+- 5.0. `field_tag` is 0
 
 ### Call Context
-- 5.0. `address` and `storage_key` are 0
-- 5.1. `field_tag` is in CallContextFieldTag range
-- 5.2. `value` is 0 if first access and READ
-- 5.3. `initial value` is 0
-- 5.4. `state root` is the same
+- 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
 
 ### Account
-- 6.0. `id` and `storage_key` are 0
-- 6.1. MPT storage lookup for last access to (address, field_tag)
+- 7.0. `id` and `storage_key` are 0
+- 7.1. MPT storage lookup for last access to (address, field_tag)
 
 ### Tx Refund
-- 7.0. `address`, `field_tag` and `storage_key` are 0
-- 7.1. `state root` is the same
-- 7.2. `initial_value` is 0
-- 7.3. First access for a set of all keys are 0 if `READ`
+- 8.0. `address`, `field_tag` and `storage_key` are 0
+- 8.1. `state root` is the same
+- 8.2. `initial_value` is 0
+- 8.3. First access for a set of all keys are 0 if `READ`
 
 ### Tx Access List Account
-- 8.0. `field_tag` and `storage_key` are 0
-- 8.1. `state root` is the same
-- 8.2. First access for a set of all keys are 0 if `READ`
+- 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`
 
 
 ### Tx Access List Account Storage
-- 9.0. `field_tag` is 0
-- 9.1. `state root` is the same
-- 9.2. First access for a set of all keys are 0 if `READ`
+- 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`
 
 ### Tx Log
-- 10.0. `is_write` is 1
-- 10.1. `state root` is the same
+- 11.0. `is_write` is 1
+- 11.1. `state root` is the same
 
 ### Tx Receipt
-- 11.0. `address` and `storage_key` are 0
-- 11.1. `field_tag` is boolean (according to EIP-658)
-- 11.2. `tx_id` increases by 1 and `value` increases as well if `tx_id` changes 
-- 11.3. `tx_id` is 1 if it's the first row and `tx_id` is in 11 bits range
-- 11.4. `state root` is the same
+- 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
 
 ## About Account and Storage accesses
 
 All account and storage reads and writes in the RwTable are linked to the Merkle
 Patricia Trie (MPT) Circuit.  This is because unlike the rest of entries, which
 are initialized at 0 in each block, account and storage persist during blocks via
-the Ethereum State and Storage Tries.
+the Ethereum State and Storage Tries. Transient storage is initialized at 0 in
+each transaction.
 
 In general we link the first and last accesses of each key (`[address,
 field_tag]` for Account, `[address, storage_key]` for Storage) to MPT proofs that