or
or
By clicking below, you agree to our terms of service.
New to HackMD? Sign up
Syntax | Example | Reference | |
---|---|---|---|
# Header | Header | 基本排版 | |
- Unordered List |
|
||
1. Ordered List |
|
||
- [ ] Todo List |
|
||
> Blockquote | Blockquote |
||
**Bold font** | Bold font | ||
*Italics font* | Italics font | ||
~~Strikethrough~~ | |||
19^th^ | 19th | ||
H~2~O | H2O | ||
++Inserted text++ | Inserted text | ||
==Marked text== | Marked text | ||
[link text](https:// "title") | Link | ||
 | Image | ||
`Code` | Code |
在筆記中貼入程式碼 | |
```javascript var i = 0; ``` |
|
||
:smile: | ![]() |
Emoji list | |
{%youtube youtube_id %} | Externals | ||
$L^aT_eX$ | LaTeX | ||
:::info This is a alert area. ::: |
This is a alert area. |
On a scale of 0-10, how likely is it that you would recommend HackMD to your friends, family or business associates?
Please give us some advice and help us improve HackMD.
Do you want to remove this version name and description?
Syncing
xxxxxxxxxx
Update
Introduction
State circuit serves as a random accessible data holder of stack, memory, storage, and all the others things evm interpreter could access at any time.
This note tried to focus on stack and memory first. It goes through memory and stack sub-circuit, then explain how these sub-circuits provides the valid access records, the bus mapping, for evm circuit to read and write.
I take this naive but concrete solidity code as example:
When function
memory_sample
is executed, the evm should has such log (only focus on the function body in this note):Definition
fq
- 253-bit value.op
- A byte representing EVM operation codecode
- A vector ofop
compiled from smart contractpc
- Program countergc
- Global counter, is offset to0
for simplicitysp
- Stack pointerstack
- A vector offq
with max size1024
memory
- A vector of bytes$a === $b
-$a
is equal to$b
$t_lookup
- A function that ensures the input is in table$t
Memory Circuit
In memory circuit, prover should collect all
MLOAD
andMSTORE
operation and order them bykey
and then bygc
, then build a layout with columnkey
,val
,rw
andgc
, which stands:key
-key
ofmemory
we are operatingval
-memory[key]
after operationrw
- access enum, could be0
-Read
1
-Write
With some auxiliary notation:
key_prev
-key
value in previous rowgc_prev
-gc
value in previous rowval_prev
-val
value in previous rowThe constraint will be:
rw === Write
and
val === 0
prev
)*
rw ∈ [0, 1]
rw
*
key - key_prev ∈ [0, ?]
*
val ∈ [0, 255]
key != key_prev
rw === Write
and
val === 0
0
key == key_prev
gc > gc_prev
rw == Read
val === val_prev
In the above sample, the memory table should be like:
key
val
rw
gc
0x40
0
Write
0x40
0x80
Write
code
0x40
0x80
Read
56 MLOAD
0x80
0
Write
0x80
0xdeadbeef
Write
63 MSTORE
0x80
0xdeadbeef
Read
70 MLOAD
0x80
0x1d97c6efb
Write
73 MSTORE
0xa0
0
Write
0xa0
0xcafeb0ba
Write
83 MSTORE
Stack Circuit
Stack circuit is like memory circuit, but to prevent modification on every entry when
PUSH
orPOP
, we let evm circuit maintain a stack pointersp
inited at1024
to lookup the top value of stack. For example,PUSH
doessp--
andPOP
doessp++
.The constraint will be:
rw === Write
and
val === 0
prev
)*
rw ∈ [0, 1]
rw
*
key - key_prev ∈ [0, 1023]
*
key ∈ [0, 1023]
key != key_prev
rw === Write
and
val === 0
0
key == key_prev
gc > gc_prev
rw == Read
val === val_prev
Some
op
should be accompanied by multiple stack read/write at the same time, forDUPX
as example, we have to check if the source and new pushed value is equal, so it requires aRead
and aWrite
to be in bus mapping.We let evm circuit to use multiple lookup to ensure these read/write happen at the same time (memory as well if needed), so we could have these constraints (
$x
means variable, should be equal in the sameop
):op == PUSH
bus_mapping_lookup(
gc,
Stack,
key,
val,
Write
)
op == DUPX
bus_mapping_lookup(
gc,
Stack,
key+X,
val,
Read
)
andbus_mapping_lookup(
gc+1,
Stack,
key,
val,
Write
)
op == MLOAD
bus_mapping_lookup(
gc,
Stack,
key,
$key,
Read
)
andbus_mapping_lookup(
gc+1,
Stack,
key,
$val,
Write
)
andbus_mapping_lookup(
gc+2,
Memory,
$key,
$val,
Read
)
$key
stackRead
,$val
stackWrite
, and memoryRead
should exist in bus mapping.op == MSTORE
bus_mapping_lookup(
gc,
Stack,
key,
$key,
Read
)
andbus_mapping_lookup(
gc+1,
Stack,
key+1,
$val,
Read
)
andbus_mapping_lookup(
gc+2,
Memory,
$key,
$val,
Write
)
$key
$val
stackRead
, and memoryWrite
should exist in bus mapping.op == SWAPX
In the above sample, the stack table should be like:
key
val
rw
gc
1020
0
Write
1020
0x80
Write
81 DUP3
1020
0x80
Read
82 ADD.POP
1021
0
Write
1021
0x80
Write
62 DUP2
1021
0x80
Read
63 MSTORE.POP
1021
0x80
Write
69 DUP2
1021
0x80
Read
70 MLOAD.POP
1021
0xdeadbeef
Write
70 MLOAD.PUSH
1021
0xdeadbeef
Read
71 ADD.POP
1021
0x80
Write
72 DUP2
1021
0x80
Read
73 MSTORE.POP
1021
0x20
Write
79 PUSH1
1021
0x20
Read
82 ADD.POP
1021
0xa0
Write
82 ADD.PUSH
1021
0xa0
Read
83 MSTORE.POP
1022
0
Write
1022
0xdeadbeef
Write
57 PUSH4
1022
0xdeadbeef
Read
63 MSTORE.POP
1022
0xfaceb00c
Write
64 PUSH4
1022
0xfaceb00c
Read
71 ADD.POP
1022
0x1d97c6efb
Write
71 ADD.PUSH
1022
0x1d97c6efb
Read
73 MSTORE.POP
1022
0xcafeb0ba
Write
74 PUSH4
1022
0xcafeb0ba
Read
83 MSTORE.POP
1023
0
Write
1023
0x40
Write
54 PUSH1 40
1023
0x40
Read
56 MLOAD.POP
1023
0x80
Write
56 MLOAD.PUSH
1023
0x80
Read
62 DUP2
1023
0x80
Read
69 DUP2
1023
0x80
Read
72 DUP2
1023
0x80
Read
81 DUP3
Storage Circuit
Storage access is not covered by this note, see here for more details
Bus Mapping
Memory and stack circuit will provide the valid and meaningful access record (some rows like init will not be included) to the bus mapping lookup table, which is shared by the state circuit and evm circuit.
It has a unique
gc
to serves as a synchronizing clock, atarget
to specify the residue of the access record, and many arbitraryvalX
if necessary. In evm circuit, we lookup allgc
one by one and finally check the bus mapping degree is bounded togc
in the execution end, then we have confidence that no malicious write is inserted.We have enum
target
with theirvalX
representation:Stack
val1
-key
val2
-val
val3
-rw
Memory
val1
-key
val2
-val
val3
-rw
Storage
val1
-key
val2
-val
val3
-rw
val4
-val_prev
val5
-is_first_touch
...
In the above sample, the bus mapping should be like (order by gc increasingly):
gc
target
val1
val2
val3
Stack
1023
0x40
Write
54 PUSH1 40
Stack
1023
0x40
Read
56 MLOAD.POP
Stack
1023
0x80
Write
56 MLOAD.PUSH
Memory
0x40
0x80
Read
56 MLOAD
Stack
1022
0xdeadbeef
Write
57 PUSH4
Stack
1023
0x80
Read
62 DUP2
Stack
1021
0x80
Write
62 DUP2
Stack
1021
0x80
Read
63 MSTORE.POP
Stack
1022
0xdeadbeef
Read
63 MSTORE.POP
Memory
0x80
0xdeadbeef
Write
63 MSTORE
Stack
1022
0xfaceb00c
Write
64 PUSH4
Stack
1023
0x80
Read
69 DUP2
Stack
1021
0x80
Write
69 DUP2
Stack
1021
0x80
Read
70 MLOAD.POP
Stack
1021
0xdeadbeef
Write
70 MLOAD.PUSH
Memory
0x80
0xdeadbeef
Read
70 MLOAD
Stack
1021
0xdeadbeef
Read
71 ADD.POP
Stack
1022
0xfaceb00c
Read
71 ADD.POP
Stack
1022
0x1d97c6efb
Write
71 ADD.PUSH
Stack
1023
0x80
Read
72 DUP2
Stack
1021
0x80
Write
72 DUP2
Stack
1021
0x80
Read
73 MSTORE.POP
Stack
1022
0x1d97c6efb
Read
73 MSTORE.POP
Memory
0x80
0x1d97c6efb
Write
73 MSTORE
Stack
1022
0xcafeb0ba
Write
74 PUSH4
Stack
1021
0x20
Write
79 PUSH1
Stack
1023
0x80
Read
81 DUP3
Stack
1020
0x80
Write
81 DUP3
Stack
1020
0x80
Read
82 ADD.POP
Stack
1021
0x20
Read
82 ADD.POP
Stack
1021
0xa0
Write
82 ADD.PUSH
Stack
1021
0xa0
Read
83 MSTORE.POP
Stack
1022
0xcafeb0ba
Read
83 MSTORE.POP
Memory
0xa0
0xcafeb0ba
Write
83 MSTORE
Call Context
In different EOA calls or internal calls, their stack and memory will be seperated by
call_context
. This is beneficial in two way:CALLDATACOPY
orRETURNDATACOPY
, we just locating the memory by caller or callee'scall_context
and ensure they are indeed there.call_context
directly in evm circuit, and decompress it when switching back to caller's context.This note only describes how the state circuit works within the same call and doesn't cover
call_context
, see here for more information.Question & Discussion
Q1. Memory is actually a byte array
Memory is actually a byte array which can be access at any position, how do we handle them if the operation has overlap? For example,
mstore(0x20, 0x1234) + mstore(0x19, 0x56) => mload(0x20) = 0x5634
Another TBD part is how large memory address we allow to be access. If we are checking the non-strict monotonicity of memory address by lookup, larger memory address will require a larger table (or more cells to store chunks if using smaller table).
For now in evm, the gas cost of memory expansion follows qudratic cost, and if we assume the gas limit per block is up to \(20,000,000\), we can have an inequality equation to find the max memory address access which is also runnable:
\[ \begin{aligned} & 3\cdot\textsf{memSizeWord} + \frac{\textsf{memSizeWord}^2}{512} \le 20,000,000 \ & \textsf{memSizeWord} \le 2^{16.62} \ & \textsf{memSize} = 32 \cdot \textsf{memSizeWord} \le 2^{21.62} \end{aligned} \]
Naively we can have a really large table from \(1\) to \(2^{22}\) and lookup
key - key_prev
to check the non-strict monotonicity in memory circuit. Or we can split it into 10-bit chunks to lookup each by a smaller 10-bit table.Q2. Do we put stack pointer inside stack table?
Q3. How and where do we handle
DUPX
,SWAPX
?How do we ensure swapped or duplicated value is same to the other one?
Q4. How to handle
MSTORE
When
MSTORE
happens, it is accompanied by twoRead
at different stackkey
, and we have to combine them to lookup bus mapping to ensure tokey
(firstRead
)val
(secondRead
) is stored tomemory
, but instack
table we sort them bykey
and thengc
, so they are far away from each other. Need to think more on this.Q5. What if we put more things in bus mapping (add more
valX
)?In the above approach, it uses
(key, val, rw)
as(val, val2, val3)
in the bus mapping contributed bystack
table, which works for most op. But it always cost 2 slot for op likeDUPX
because in evm circuit we need to lookup aRead
at duplication source(sp + X, $val, Read)
and aWrite
at stack top(sp, $val, Write)
.If we can have an extra
val4
in the bus mapping, we can set them(sp, $val, Write, sp + X)
and only do 1 slot in evm circuit (we save aRead
check). It cost one more multiplication and addition incompress
, but seems not to increase the constraint degree because they are multiplied by constant (randomness) and added at the end.Take another example, for
MLOAD
, we can make the bus mapping(sp, $val, Write, $key)
, where$key
should be the preivous row'sval
instack
table. Then($key, $val)
should serve as(key, val)
to lookupmemory
entry. Then we gain 1 slotMLOAD
instead of 2.Q6. EVM supports 256-bit value, which definitely not fits 253-bit
In this note, all the values of stack should be in compressed form instead of actual values and the actual values will not be used in state circuit, here we use actual values for clarity.
Actual values will be split into 8-bit array (byte array) and we use the same
compress
function to compress them into singlefq
Q7. How do we ensure
val
of two slot in op are same if we are expecting?For
DUPX
as example, how do we make sure the two lookup has same$val
in different slot? I think copy constraint won't work because we never know which one is which slot.Reference