Memory-Align state machine
The Memory Align State Machine is a secondary state machine that includes an executor (the Memory Align SM Executor) and an internal Memory Align PIL (program) that is a set of verification rules written in the PIL language.
The Memory Align SM Executor is written in two languages: Javascript and C/C++.
Overview¶
It checks memory reads/writes using a 32-byte word access, while the EVM can read and write 32-byte words with offsets at a byte level. The table below shows a sample of possible byte-addressed and 32-byte-addressed memory layouts for the same content (three words).
The relationship between the 32-byte word addressable layout and the byte addressable layout is called memory alignment and the Memory Align SM is the state machine that checks the correctness of this relationship.
In more detail, we have to check the following memory operations:
: It receives an offset and returns the 32 bytes in memory starting at that offset. : It receives an offset and saves 32 bytes from the offset address of the memory. : It receives an offset and saves one byte on that address of the memory.
In general cases,
Given that the memory’s contents are represented in the table above and that the EVM is addressed at the byte level, the value we should get if we check a read from the EVM of a word starting at the address
We denote the content of the words affected by an EVM memory read as
In our example, these words are the following:
We define a read block as the string concatenating the content of the words affected by the read:
The below figure shows the affected read words
Let us now introduce the flow at the time of validating a read.
Suppose that we want to validate that if we perform an
First of all, it will have to query for the values
Observe that it is easy to extract the memory positions to query from the address
Secondly, we should extract the correct
Now, the Main SM will check via a Plookup to the Memory Align State Machine that \val is a correct read given the affected words
Similarly,
The idea is very similar, but we are provided with a value \val that we want to write into a specific location of the memory. We will denote by
Following our previous example, suppose that we want to write:
in the address
The Main State Machine will need to perform several operations. We will be given an address
Now, the Main SM can compute
Finally, the last opcode
Source code¶
The Polygon zkEVM repository is available on GitHub.
Memory Align SM Executor: sm_mem_align.js
Memory Align SM PIL: mem_align.pil