Skip to content

Commit 5863881

Browse files
committed
reviewed architecture low-level section
1 parent b7944cb commit 5863881

22 files changed

+664
-529
lines changed

docs/zkEVM/architecture/zkprover/arithmetic-sm.md

Lines changed: 20 additions & 20 deletions
Original file line numberDiff line numberDiff line change
@@ -1,19 +1,19 @@
1-
The Arithmetic State Machine is a secondary state machine that also has an executor (the Arithmetic SM Executor) and an internal Arithmetic program (a set of verification rules written in the PIL language). The Arithmetic SM Executor is available in two languages: Javascript and C/C++.
1+
The Arithmetic state machine is a secondary state machine that also has an executor (the Arithmetic SM executor) and an internal Arithmetic program (a set of verification rules written in the PIL language). The Arithmetic SM executor is available in two languages: Javascript and C/C++.
22

3-
It is one of the six secondary state machines receiving instructions from the Main SM Executor. The main purpose of the Arithmetic SM is to carry out elliptic curve arithmetic operations, such as Point Addition and Point Doubling as well as performing 256-bit operations like addition, product or division.
3+
It is one of the six secondary state machines receiving instructions from the Main SM executor. The main purpose of the Arithmetic SM is to carry out elliptic curve arithmetic operations, such as Point Addition and Point Doubling as well as performing 256-bit operations like addition, product or division.
44

55
## Standard elliptic curve arithmetic
66

77
Consider an elliptic curve $E$ defined by $y^2 = x^3 + ax + b$ over the finite field $\mathbb{F} = \mathbb{Z}_p$, where $p$ is the prime,
88

99
$$
10-
p = 2^{256} - 2^{32} - 2^9 - 2^8 - 2^7 -2^6 - 2^4 - 1.
10+
p = 2^{256} - 2^{32} - 2^9 - 2^8 - 2^7 -2^6 - 2^4 - 1
1111
$$
1212

1313
Set the coefficients $a = 0$ and $b = 7$, so that $E$ reduces to
1414

1515
$$
16-
y^2 = x^3 + 7.
16+
y^2 = x^3 + 7
1717
$$
1818

1919
### Point addition
@@ -55,15 +55,15 @@ For instance, if $C = 0$, then $\bf{Eqn\ A}$ states that the result of multiplyi
5555

5656
Or, if $B = 1$, $\bf{Eqn\ A}$ states that the result of adding $A$ and $C$ is the same as before: $E$ with a carry of $D$. Similarly, division and modular reductions can also be expressed as derivatives of $\bf{Eqn\ A}$.
5757

58-
These operations are performed in the Arithmetic State Machine, with registers satisfying the following PIL relation,
58+
These operations are performed in the Arithmetic state machine, with registers satisfying the following PIL relation,
5959

6060
$$
6161
\text{EQ}_0 \colon \quad x_1 \cdot y_1 + x_2 - y_2 \cdot 2^{256} - y_3 = 0
6262
$$
6363

6464
#### Remark
6565

66-
Since the above Elliptic Curve operations are implemented in the PIL language, it is more convenient to express them in terms of the constraints they must satisfy. These constraints are:
66+
Since the above elliptic curve operations are implemented in the PIL language, it is more convenient to express them in terms of the constraints they must satisfy. These constraints are:
6767

6868
$$
6969
\begin{aligned}
@@ -113,22 +113,22 @@ Use the following notation:
113113

114114
$$
115115
\begin{aligned}
116-
\mathbf{eq\ } &= x_1[0] \cdot y_1[0] \\
117-
\mathbf{eq'} &= x_1[0] \cdot y_1[1] + x_1[1] \cdot y_1[0]
116+
\mathtt{eq\ } &= x_1[0] \cdot y_1[0] \\
117+
\mathtt{eq'} &= x_1[0] \cdot y_1[1] + x_1[1] \cdot y_1[0]
118118
\end{aligned}
119119
$$
120120

121-
But then, the carry generated by $\mathbf{eq}$ has to be taken into account by $\mathbf{eq'}$.
121+
But then, the carry generated by $\mathtt{eq}$ has to be taken into account by $\mathtt{eq'}$.
122122

123123
Going back to our equations $\text{EQ}_0, \text{EQ}_1, \text{EQ}_2, \text{EQ}_4$; let's see how the operation is performed in $\text{EQ}_0$.
124124

125-
1. Compute $\mathbf{eq}_0 = (x_1[0] \cdot y_1[0]) + x_2[0] - y_3[0]$
125+
1. Compute $\mathtt{eq}_0 = (x_1[0] \cdot y_1[0]) + x_2[0] - y_3[0]$
126126

127-
2. Compute $\mathbf{eq}_1 = (x_1[0] \cdot y_1[1]) + (x_1[1] \cdot y_1[0]) + x_2[1] - y_3[1]$
127+
2. Compute $\mathtt{eq}_1 = (x_1[0] \cdot y_1[1]) + (x_1[1] \cdot y_1[0]) + x_2[1] - y_3[1]$
128128

129-
3. $\mathbf{eq}_2 = (x_1[0] \cdot y_1[2]) + (x_1[1] \cdot y_1[1]) + (x_1[2] \cdot y_1[0]) + x_2[2] - y_3[2]$
129+
3. $\mathtt{eq}_2 = (x_1[0] \cdot y_1[2]) + (x_1[1] \cdot y_1[1]) + (x_1[2] \cdot y_1[0]) + x_2[2] - y_3[2]$
130130

131-
This is continued until one reaches the computation, $\mathbf{eq}_{15} = (x_1[0] \cdot y_1[15]) + (x_1[1] \cdot y_1[14]) + \dots + x_2[15] - y_3[15]$.
131+
This is continued until one reaches the computation, $\mathtt{eq}_{15} = (x_1[0] \cdot y_1[15]) + (x_1[1] \cdot y_1[14]) + \dots + x_2[15] - y_3[15]$.
132132

133133
At this stage $y_2$ comes into place.
134134

@@ -138,9 +138,9 @@ Therefore, we obtain that:
138138

139139
$$
140140
\begin{aligned}
141-
\mathbf{eq}_{16} &= (x_1[1]
141+
\mathtt{eq}_{16} &= (x_1[1]
142142
\cdot y_1[15]) + (x_1[2] \cdot y_1[14]) + \dots - y_2[0], \\
143-
\mathbf{eq}_{17} &= (x_1[2] \cdot y_1[15]) + (x_1[3] \cdot y_1[14]) + \dots - y_2[1]
143+
\mathtt{eq}_{17} &= (x_1[2] \cdot y_1[15]) + (x_1[3] \cdot y_1[14]) + \dots - y_2[1]
144144
\end{aligned}
145145
$$
146146

@@ -150,15 +150,15 @@ Continuing until the last two:
150150

151151
$$
152152
\begin{aligned}
153-
\mathbf{eq}_{30} &= (x_1[15] \cdot y_1[15]) - y_2[14], \\
154-
\mathbf{eq}_{31} &= -y_2[15].
153+
\mathtt{eq}_{30} &= (x_1[15] \cdot y_1[15]) - y_2[14], \\
154+
\mathtt{eq}_{31} &= -y_2[15].
155155
\end{aligned}
156156
$$
157157

158-
Now, notice that the carry generated by the $\mathbf{eq}_i$'s is not important for them. That means, if $\mathbf{eq}_i = 10$, then what we really want the result to be is $0$ and save $1$ as a carry for the next operation. To express this fact as a constraint, we say that the following has to be satisfied:
158+
Now, notice that the carry generated by the $\mathtt{eq}_i$'s is not important for them. That means, if $\mathtt{eq}_i = 10$, then what we really want the result to be is $0$ and save $1$ as a carry for the next operation. To express this fact as a constraint, we say that the following has to be satisfied:
159159

160160
$$
161-
\mathbf{eq} + \text{carry} = \text{carry}' \cdot 2^{16},
161+
\mathtt{eq} + \text{carry} = \text{carry}' \cdot 2^{16},
162162
$$
163163

164164
where $\text{carry}$ represents the carry taken into account in the actual clock, and $\text{carry}'$ represents the carry generated by the actual operation.
@@ -175,6 +175,6 @@ $$
175175

176176
The Polygon zkEVM repository is available on [GitHub](https://github.com/0xPolygonHermez).
177177

178-
Arithmetic SM Executor: [sm_arith folder](https://github.com/0xPolygonHermez/zkevm-proverjs/tree/main/src/sm/sm_arith)
178+
Arithmetic SM executor: [sm_arith folder](https://github.com/0xPolygonHermez/zkevm-proverjs/tree/main/src/sm/sm_arith)
179179

180180
Arithmetic SM PIL: [arith.pil](https://github.com/0xPolygonHermez/zkevm-proverjs/blob/main/pil/arith.pil)

0 commit comments

Comments
 (0)