Polygon zkEVM可验证计算简单状态机示例

Posted 2022-09-21 mutourend

Next we show the arithmetization process of a more complex but yet simple state machine. Unlike the Fibonacci state machine, our simple state machine transitions from one state to the next in response to certain external instructions. See Figure 1 below, for such a state machine, with registries $\text{A}$ and $\text{B}$, and a state $({\text{A}}^{\text{i}},{\text{B}}^{\text{i}})$ that changes to another state $({\text{A}}^{\text{i+2}},{\text{B}}^{\text{i+2}})$ in accordance to two instructions, ${\text{Instruction}}^{\text{i}}$ and ${\text{Instruction}}^{\text{i+1}}$.

Figure 1: A State Machine Receiving Instructions

In the context of the zkProver, these instructions are written as zk-Assembly (zkASM) codes, and stored in a ROM in JSON-format.

State Machine Instructions

Suppose the above simple state machine receives an input, together with the following execution instruction, ${\text{Instruction}}^{\text{1}}$, written in Assembly.

Table 1: Instruction^1 written in zk-Assembly

$$\begin{array}{lc}& {\text{Instruction}}^{\text{1}}\\ \text{line 1}& \$\mathtt{getInput}()=>\mathtt{A}\\ \text{line 2}& 3=>\mathtt{B}\\ \text{line 3}& :\mathtt{ADD}\\ \text{line 4}& 0=>\mathtt{A},\mathtt{B}\end{array}$$

In accordance with each line of ${\text{Instruction}}^{\text{1}}$, the state machine executor must;

• $\text{line 1}$: Get a free input value and move it into register $\text{A}$.
• $\text{line 2}$: Move the value $3$ into register $\mathtt{B}$.
• $\text{line 3}$: Compute the sum of registry values $\mathtt{A}$ and $\mathtt{B}$, and save the output into register $\mathtt{A}$.
• $\text{line 4}$: Set the registers $\mathtt{A}$ and $\mathtt{B}$ to the value $0$.

For a free input value of $7$, the corresponding state transitions can be recorded in a table as follows;

Table 2: Record of all State Changes

$$\begin{array}{lcccccc}& {\text{Instruction}}^{\text{1}}& \mathtt{free}& \mathtt{A}& {\mathtt{A}}^{\prime }& \mathtt{B}& {\mathtt{B}}^{\prime }\\ \text{line 1}& \$\mathtt{getInput}()=>\mathtt{A}& 7& 0& 7& 0& 0\\ \text{line 2}& 3=>\mathtt{B}& 0& 7& 7& 0& 3\\ \text{line 3}& :\mathtt{ADD}& 0& 7& 10& 3& 3\\ \text{line 4}& 0=>\mathtt{A},\mathtt{B}& 0& 10& 0& 3& 0\end{array}$$

Note that ${\mathtt{A}}^{\prime }$ and ${\mathtt{B}}^{\prime }$ denote the next state of the registers $\mathtt{A}$ and $\mathtt{B}$, respectively.

Observe also that, each line of ${\text{Instruction}}^{\text{1}}$ does not always affect all register values. Since every register is initialised to $0$ at the start, the state transitions are such that,

• $\text{line 1}$ only affects two registers; $\mathtt{free}$ and ${\mathtt{A}}^{\prime }$.
• $\text{line 2}$ affects the register ${\mathtt{B}}^{\prime }$ alone. Any other state change is due to the rules and the logic of the state machine (i.e., changes in registers; $\mathtt{free}$ and $\mathtt{A}$).
• $\text{line 3}$ affects the register ${\mathtt{A}}^{\prime }$ alone. Again, the state change in register $\mathtt{B}$ is due to the state machine’s rules and logic.
• $\text{line 4}$ affects only two registers; ${\mathtt{A}}^{\prime }$ and ${\mathtt{B}}^{\prime }$. The state change in register $\mathtt{A}$ is also due to the rules and the logic of the state machine.

Computational Trace

Recall that the intention with developing these state machines is not only to carry out computations, but to also ensure that correctness of these computations is verifiable. In addition, verification must be achievable even by users with modest computer power. That said, keeping record of computations, as seen in Table 2 above, is not preferable for verification purposes, because the registry values can be very large for some state machines. And thus, defeating the ultimate purpose and aim of our rollup.

One therefore needs a way to keep track of all the computations and their correct execution, without requiring excessive memory. This is achieved by utilising the computational trace.

For our verification purposes, the computational trace does not capture the actual state values of each state transition, but uses selectors and setters to keep record of whether registry values have been altered (during each state transition) in a way that tallies with the received instructions.

Like switches that can either be ON or OFF, selectors and setters can also be either $1$ or $0$.

Rule for the $\text{inFree}$ selector: Record $\text{inFree}$ as $1$ only if the value of the register $\text{free}$ is non-zero.

Rule for selectors $\text{setX}$: Each selector $\text{setX}$ is recorded;

• As the value $1$, if the value of the corresponding registry $\text{X}$ was involved in (or contributed to) the computation,
• Otherwise, $\text{selX}$ is recorded as the value $0$.

Rule for setters $\text{setY}$: Each setter $\text{setY}$ is recorded;

• As the value $1$, if the corresponding registry value $\text{Y}$ was altered by the instruction,
• Or, as the value $0$, otherwise.

The computational trace therefore consists mostly of bits, instead of large registry values.

In the zkEVM context, the computational trace is stored as a lookup table in the ROM of the relevant state machine.

Example (Computational Trace)

Take as an example, ${\text{Instruction}}^{}$

Polygon zkEVM哈希状态机——Keccak-256和Poseidon

Polygon zkEVM R1CS与Plonk电路转换

Polygon zkEVM Memory状态机

Polygon zkEVM Memory Align状态机

Polygon zkEVM的pil-stark Fibonacci状态机代码解析