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

Specs for TLOAD TSTORE #516

Merged
merged 5 commits into from
Mar 23, 2024
Merged

Specs for TLOAD TSTORE #516

Show file tree
Hide file tree
Changes from all commits
Commits
Show all changes
5 commits
Select commit Hold shift + click to select a range
fb1fcc5
add spec for TLOAD and TSTORE
zemse Feb 20, 2024
e1e7925
update evm-proof and state-proof specs
zemse Feb 21, 2024
3ad7c0f
create OOG spec
zemse Feb 21, 2024
7aaef43
use SLOAD_GAS variable
zemse Feb 21, 2024
fea4c32
fix busmapping lookups count
zemse Mar 7, 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
40 changes: 40 additions & 0 deletions specs/error_state/ErrorOutOfGasTloadTstore.md
View file
Open in desktop
Original file line number Diff line number Diff line change
@@ -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:
Copy link
Contributor

Choose a reason for hiding this comment

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

Is it 6 instead of 7?

Copy link
Member Author

Choose a reason for hiding this comment

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

I think 7 is correct because it is in 92TLOAD_93TSTORE.md too? Or can you please correct me?

Copy link
Contributor

Choose a reason for hiding this comment

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

Hm, 7 doesn't match the listed lookups below (5 call context lookups and 1 stack read). Note that for TLOAD we don't need is_static. But on the other hand, one stack operation seems to be missing (value read), so this is the reason for the difference in failure and success cases. But I agree, I think these two numbers should be the same.

Note, however, that the numbers in failure/success cases are different for SLOAD/SSTORE too. Is there a mistake?

One additional thing that I find a bit confusing is that the failure case is using only is_success while the success case is using only is_persistent, shouldn't be used both in both cases?

Copy link
Member Author

Choose a reason for hiding this comment

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

Note that for TLOAD we don't need is_static.

I agree. I saw SLOAD's OOG also having is_static in the specs. That needs to be fixed?

But I agree, I think these two numbers should be the same. Note, however, that the numbers in failure/success cases are different for SLOAD/SSTORE too. Is there a mistake?

It would be very helpful if @ChihChengLiang or @ed255 could chime in regarding this.

One additional thing that I find a bit confusing is that the failure case is using only is_success while the success case is using only is_persistent, shouldn't be used both in both cases?

Yeah the same name should be used. is_persistent seems to convey the idea better than is_success. I can update that.

Copy link
Contributor

Choose a reason for hiding this comment

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

I will have another look, but just before you do any modifications - note that is_persistent and is_success are two different fields of Call struct which mean different things (is't not just the naming):

/// This call is persistent or call stack reverts at some point
pub is_persistent: bool,
/// This call ends successfully or not
pub is_success: bool,

Copy link
Contributor

Choose a reason for hiding this comment

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

I think is_success and is_persistent are ok as they are (is_success needs to be false and is checked for each OOG error in CommonErrorGadget).

I think if you remove is_static lookup for from the error lookups for SLOAD, it should be fine (that would sum up to 5 SLOAD lookups in the error case).

SLOAD/SSTORE docs are ok in my opinion, except that for SSLOAD there is a redundant is_static in the error case.

Copy link
Member

Choose a reason for hiding this comment

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

I agree that SLOAD OOG doesn't need to read is_static, and the same would happen for TLOAD OOG. On the other hand, by looking at the implementation I see that is_static value is ignored in the SLOAD OOG case:
https://github.com/privacy-scaling-explorations/zkevm-circuits/blob/4996eb6c11fb4eb4bcde7eff55827ecf6cfaaf03/zkevm-circuits/src/evm_circuit/execution/error_oog_sload_sstore.rs#L70-L71
So the implementation is technically correct, even though we could skip the read of is_static in the SLOAD case. I think this is a very minor detail; skipping the read means one less row in the RwTable, which is an optimization, but I think the effects are negligible.

But I agree, I think these two numbers should be the same.

Note, however, that the numbers in failure/success cases are different for SLOAD/SSTORE too. Is there a mistake?

Do you mean that SLOAD.rwc_delta == OOG_SLOAD.rwc_delta and SSTORE.rwc_delta == OOG_SSTORE.rwc_delta?

If that's the case, notice that in a success SLOAD, there's the value pushed to the stack, but in OOG, the call will be aborted, so no one is going to read the result of SLOAD, which means there's no need to push a result value to the stack. So that's one RwTable lookup that appears in SLOAD but not in OOG_SLOAD. There are other differences like in SLOAD we update the access list, but in OOG_SLOAD we don't.

Copy link
Contributor

Choose a reason for hiding this comment

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

Thanks Edu! Yes, I think it's ok as it is (I realised later there's no additional push in the error case). Agree that the additional is_static call in TLOAD/SLOAD doesn't change things much, so I am approving the PR.


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
3 changes: 2 additions & 1 deletion specs/evm-proof.md
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -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.

Expand All @@ -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) |
Expand Down
67 changes: 67 additions & 0 deletions specs/opcode/92TLOAD_93TSTORE.md
View file
Open in desktop
Original file line number Diff line number Diff line change
@@ -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).
69 changes: 37 additions & 32 deletions specs/state-proof.md
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -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.

Expand Down Expand Up @@ -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
Expand Down
Loading