zkEVM review - Specs

Author: EmpieichO

docs/zkEVM/concepts/circom-intro-brief.md

@@ -1,4 +1,3 @@
-
 !!!info
     In this document, we describe the CIRCOM component of the zkProver. It is one of the four main components of the zkProver, as outlined [here](../architecture/zkprover/index.md). These principal components are; the Executor or Main SM, STARK Recursion, CIRCOM, and Rapid SNARK.
 
@@ -38,7 +37,7 @@ Once obtained, the R1CS can later be used by a zk-SNARK protocol to generate ver
 
 A valid proof attests to the fact that the prover knows an assignment to all wires of the circuit that fulfills all the constraints of the R1CS.
 
-An issue that arises, when applying Zero-Knowledge protocols to complex computations such as a circuit describing the logic of a ZK-rollup, is that the number of constraints to be verified can be extremely large.
+An issue that arises, when applying zero-Knowledge protocols to complex computations such as a circuit describing the logic of a ZK-rollup, is that the number of constraints to be verified can be extremely large.
 
 CIRCOM was developed for the very purpose of scaling complex Arithmetic circuits by realizing them as combined instantiations of smaller Arithmetic circuits.
 
@@ -77,25 +76,25 @@ The CIRCOM compiler is mainly written in Rust and it is open source.
 
 The CIRCOM language has its own peculiarities. The focus in this subsection is on a few features characteristic of CIRCOM.
 
-Consider as an example, the `Multiplier` circuit with input signals $\texttt{a}$ and $\texttt{b}$, and an output signal $\texttt{c}$ satisfying the constraint $\texttt{a} \times \texttt{b} \texttt{ - c = 0}$.
+Consider as an example, the _Multiplier_ circuit with input signals $\texttt{a}$ and $\texttt{b}$, and an output signal $\texttt{c}$ satisfying the constraint $\texttt{a} \times \texttt{b} \texttt{ - c = 0}$.
 
 ![A simple Multiplier Arithmetic circuit](../../img/zkEVM/03circom-simple-arith-circuit.png)
 
-The figure above depicts a simple `Multiplier` Arithmetic circuit with input wires labeled $\texttt{a}$ and $\texttt{b}$ and an output wire labeled $\texttt{c}$ such that $\texttt{a} \times \texttt{b\ = } \texttt{c}$. The wires are referred to as signals. The constraint related to this Multiplier circuit is:
+The figure above depicts a simple _Multiplier_ Arithmetic circuit with input wires labeled $\texttt{a}$ and $\texttt{b}$ and an output wire labeled $\texttt{c}$ such that $\texttt{a} \times \texttt{b\ = } \texttt{c}$. The wires are referred to as signals. The constraint related to this Multiplier circuit is:
 
 $$
 \texttt{a} \times \texttt{b} \texttt{ - c = 0}
 $$
 
-### The `pragma` instruction
+### The _pragma_ instruction
 
-The `pragma` instruction specifies the version of the CIRCOM compiler being used. It is meant to ensure compatibility between the circuit and the compiler version. If the two are incompatible, the compiler throws a warning.
+The _pragma_ instruction specifies the version of the CIRCOM compiler being used. It is meant to ensure compatibility between the circuit and the compiler version. If the two are incompatible, the compiler throws a warning.
 
 ```
 pragma circom 2.0.0;
 ```
 
-As a precautionary measure, all files with the `.circom` extension should start with a `pragma` instruction. In the absence of this instruction, it is assumed that the code is compatible with the latest compiler version.
+As a precautionary measure, all files with the _.circom_ extension should start with a _pragma_ instruction. In the absence of this instruction, it is assumed that the code is compatible with the latest compiler version.
 
 ### Declaration of signals
 
@@ -130,7 +129,7 @@ Templates are parametrizable in the sense that their outputs depend on free inpu
 
 They are general descriptions of circuits, that have some input and output signals, as well as a relation between the inputs and the outputs.
 
-The following code shows how a `Multiplier template` is created:
+The following code shows how a _Multiplier template_ is created:
 
 ```
 pragma circom 2.0.0;
@@ -147,15 +146,15 @@ template Multiplier () {
 
 ### Instantiation of templates
 
-Although the above code succeeds in creating the `Multiplier template`, the template is yet to be instantiated.
+Although the above code succeeds in creating the _Multiplier template_, the template is yet to be instantiated.
 
 In CIRCOM, the instantiation of a template is called a component, and it is created as follows:
 
 ```
 component main = Multiplier();
 ```
 
-The `Multiplier template` does not depend on any parameter.
+The _Multiplier template_ does not depend on any parameter.
 
 However, it is possible to initially create a generic, parametrizable template that can later be instantiated using specific parameters to construct the circuit.
 
@@ -165,7 +164,7 @@ Small circuits can be defined which can be combined to create larger circuits by
 
 ### Compiling a circuit
 
-As previously mentioned, the use of the operator "<==" in the `Multiplier template` has dual functionality:
+As previously mentioned, the use of the operator "<==" in the _Multiplier template_ has dual functionality:
 
 - It captures the arithmetic relation between signals, and
 - It also provides a way to compute $\texttt{c}$ from $\texttt{a}$ and $\texttt{b}$.
@@ -174,13 +173,13 @@ In general, the description of a CIRCOM circuit also keeps dual functionality. T
 
 This enables the compiler to easily generate the R1CS describing a circuit, together with instructions to compute intermediate and output values of a circuit.
 
-Given a circuit with the `multiplier.circom` extension, the following line of code instructs the compiler to carry out the two types of tasks:
+Given a circuit with the _multiplier.circom_ extension, the following line of code instructs the compiler to carry out the two types of tasks:
 
 ```
 circom multiplier.circom --r1cs --c --wasm --sym
 ```
 
-After compiling the `.circom` circuit, the compiler returns four files:
+After compiling the _.circom_ circuit, the compiler returns four files:
 
 - A file with the R1CS constraints (symbolic task)
 - A C++ program for computing values of the circuit wires (computational task)
@@ -195,47 +194,47 @@ Recall that a valid set of circuit input, intermediate and output values is call
 
 ### Private and public signals
 
-Depending on the `template` being used, some signals are `private` while others are `public`.
+Depending on the _template_ being used, some signals are _private_ while others are _public_.
 
-In the case of the `Multiplier template`, a signal is `private` by default, unless it is declared to be `public` in the instantiation of the template as shown below.
+In the case of the _Multiplier template_, a signal is _private_ by default, unless it is declared to be _public_ in the instantiation of the template as shown below.
 
 ```
 component main {public [a]} = Multiplier();
 ```
 
-According to the above line, the input signal $\texttt{a}$ is `public`, while $\texttt{b}$ is `private` by default.
+According to the above line, the input signal $\texttt{a}$ is _public_, while $\texttt{b}$ is _private_ by default.
 
 ### Main component
 
-The CIRCOM compiler needs a specific component as an entry point. And this initial component is called `main`.
+The CIRCOM compiler needs a specific component as an entry point. And this initial component is called _main_.
 
-In the same way the `Multiplier template` needed instantiation as a component, so does the `main` component.
+In the same way the _Multiplier template_ needed instantiation as a component, so does the _main_ component.
 
-However, unlike other intermediate components, the `main` component defines the global input and output signals of a circuit.
+However, unlike other intermediate components, the _main_ component defines the global input and output signals of a circuit.
 
 Denote a list of $\texttt{n}$ signals by $\{\mathtt{ s1, s2, \dots , sn }\}$.
 
-The general syntax to specify the `main` component is the following:
+The general syntax to specify the _main_ component is the following:
 
 ```
 component main {public [s1,..,sn]} = templateID(v1,..,vn);
 ```
 
-Specifying the list of public signals of the circuit, indicated as `{public [s1,..,sn]}`, is optional.
+Specifying the list of public signals of the circuit, indicated as _{public [s1,..,sn]}_, is optional.
 
-Note that global inputs are considered `private` signals while global outputs are considered `public`.
+Note that global inputs are considered _private_ signals while global outputs are considered _public_.
 
-However, the `main` component has a special attribute to set a list of global inputs as public signals.
+However, the _main_ component has a special attribute to set a list of global inputs as public signals.
 
-The rule of thumb is: Any other input signal not included in this list `{public [s1,..,sn]}`, is considered private.
+The rule of thumb is: Any other input signal not included in this list _{public [s1,..,sn]}_, is considered private.
 
 ### Concluding CIRCOM's features
 
 There are many more features that distinguish CIRCOM from other known ZK tools. The rest of these features delineated in the original [CIRCOM paper](https://www.techrxiv.org/articles/preprint/CIRCOM_A_Robust_and_Scalable_Language_for_Building_Complex_Zero-Knowledge_Circuits/19374986/1).
 
 We conclude this document by putting together the mentioned CIRCOM features in one code example.
 
-The `Multiplier template` is again used as an example. But the `pragma` instruction is omitted for simplicity's sake.
+The _Multiplier template_ is again used as an example. But the _pragma_ instruction is omitted for simplicity's sake.
 
 ```
 template Multiplier() {

docs/zkEVM/spec/index.md

@@ -1,5 +1,5 @@
 This section contains specifications of other zkEVM features not covered in the Architecture section of this documentation.
 
-First are the two novel languages: The zero-knowledge Assembly (zkASM) language which interprets the firmware of microprocessor-type state machines, and the Polynomial Identity Language (PIL) which is instrumental in enabling verification of state transitions.
+First are the two novel languages: The _zero-knowledge Assembly_ (zkASM) language which interprets the firmware of microprocessor-type state machines, and the _Polynomial Identity Language_ (PIL) which is instrumental in enabling verification of state transitions.
 
 Second are some of the differences between Polygon zkEVM and the EVM. These are differences in terms of opcodes, supported precompiled contracts, newly added features and other variances.

docs/zkEVM/spec/pil/connection-arguments.md

@@ -4,7 +4,7 @@ This document describes the connection arguments and how they are used in Polyno
 
 Given a vector $a = ( a_1 , \dots , a_n) \in \mathbb{F}_n$ and a partition ${\large{\S}} = \{ S_1, \dots , S_t \}$ of $[n]$, we say "$a$ $\textit{copy-satisfies}$ ${\large{\S}}$" if for each $S_k \in {\large{\S}}$, we have that $a_i = a_j$ whenever $i, j \in S_k$ , with $i, j \in [n]$ and $k \in [t]$.
 
-Moreover, we say that a protocol $(\mathcal{P}, \mathcal{V})$ is a **connection argument** if the protocol can be used by $\mathcal{P}$ to prove to $\mathcal{V}$ that a vector $\textit{copy-satisfies}$ a partition of $[n]$.
+Moreover, we say that a protocol $(\mathcal{P}, \mathcal{V})$ is a _connection argument_ if the protocol can be used by $\mathcal{P}$ to prove to $\mathcal{V}$ that a vector $\textit{copy-satisfies}$ a partition of $[n]$.
 
 !!! info
 
@@ -48,7 +48,7 @@ Observe that, since the singleton $\{2\}$ is in ${\large{\S}}$, then $\mathtt{a}
 
 Also, the vector $\mathtt{b}$ does not $\textit{copy-satisfies}\ {\large{\S}}$ because $\mathtt{b}_1 = \mathtt{b}_5 =3 \not= 7 = \mathtt{b}_3$.
 
-In the context of programs, connection arguments can be written easily in PIL by introducing a column associated with the chosen partition. This is also done in [GWC19](https://eprint.iacr.org/2019/953).
+In the context of programs, connection arguments can be written easily in PIL by introducing a column associated with the chosen partition. This is also done in [[GWC19]](https://eprint.iacr.org/2019/953).
 
 Recall that column values are evaluations of a polynomial at $G = \langle g \rangle$ and $\texttt{N}$ is the length of the execution trace.
 
@@ -80,7 +80,7 @@ A valid execution trace for this example was shown in Table 1 above.
 
 !!! info Remark
 
-    The column $\texttt{SA}$ does not need to be declared as a constant polynomial. The **connection argument** will still hold true even if it is declared as committed.
+    The column $\texttt{SA}$ does not need to be declared as a constant polynomial. The _connection argument_ still holds true even if it is declared as committed.
 
 ## Multiple copy satisfiability
 
@@ -106,7 +106,7 @@ $$
 
 where $k_1, k_2 \in \mathbb{F}$ are introduced here as a way of obtaining more elements (in a group $G$ of size $n$) and enabling correct encoding of the $[3n] \to [3n]$ permutation $\sigma$.
 
-See [GWC19](https://eprint.iacr.org/2019/953) for more details on this encoding.
+See [[GWC19]](https://eprint.iacr.org/2019/953) for more details on this encoding.
 
 The below table shows how to compute the polynomials $\texttt{SA}$, $\texttt{SB}$ and $\texttt{SC}$ encoding the permutation of the above example:
 

docs/zkEVM/spec/pil/cyclicity-in-pil.md

@@ -34,7 +34,7 @@ Denote the cyclic group over which interpolation is carried out as $G = \{ g, g^
     P(g^i) = \texttt{a}[i]\ \ \text{and}\ \ Q(g^i) = \texttt{b}[i] \tag{eqn}
     $$
 
-    **But in order to keep the PIL code simple and easily relatable to the execution trace**, we replace the $P$ and $Q$ with $\texttt{a}$ and $\texttt{b}$, respectively. The above $\text{eqn}$ will therefore be seen written as,
+    But in order to keep the PIL code simple and easily relatable to the execution trace, we replace the $P$ and $Q$ with $\texttt{a}$ and $\texttt{b}$, respectively. The above $\text{eqn}$ is therefore seen written as,
 
     $$
     \texttt{a}(g^i) = \texttt{a}[i]\ \ \text{and}\ \ \texttt{b}(g^i) = \texttt{b}[i].
@@ -84,7 +84,7 @@ $$
 \text{RHS} =\ \texttt{a}(g^3) + \texttt{b}(g^3) =\ \texttt{a}[3] + \texttt{b}[3] = 1 + 1 = 2.
 $$
 
-This proves that second constraint is not satisfied for $i = 3$. And therefore the execution trace is **not cyclic**.
+This proves that second constraint is not satisfied for $i = 3$. And therefore the execution trace is _not cyclic_.
 
 ## Introducing cyclicity
 

docs/zkEVM/spec/pil/filling-polynomials.md

@@ -1,14 +1,14 @@
 This document describes how to fill Polynomials in PIL using JavaScript and Pilcom.
 
-In this document, we are going to use **Javascript** and **pilcom** to generate a specific execution trace for a given PIL.
+In this document, we are going to use _Javascript_ and _pilcom_ to generate a specific execution trace for a given PIL.
 
 To do so, we are going to use the execution trace of a program previously discussed in the [Connection arguments](connection-arguments.md) section.
 
-We will also use the **pil-stark** library, which is a utility that provides a framework for setup, generation and verification of proofs. It uses an FGL class which mimics a finite field, and it is required by some functions that provide the **pilcom** package.
+We also use the _pil-stark_ library, which is a utility that provides a framework for setup, generation and verification of proofs. It uses an FGL class which mimics a finite field, and it is required by some functions that provide the _pilcom_ package.
 
 ## Execute code
 
-First of all, under the scope of an asynchronous function called `execute`, we parse the provided PIL code (which is, in our case, `main.pil`) into a **Javascript** object using the `compile` function of **pilcom**.
+First of all, under the scope of an asynchronous function called _execute_, we parse the provided PIL code (which is, in our case, _main.pil_) into a _Javascript_ object using the _compile_ function of _pilcom_.
 
 In code, we obtain the following;
 
@@ -24,12 +24,12 @@ async function execute() {
 
 ## Pilcom package
 
-The **pilcom** package also provides two functions; `newConstPolsArray` and `newCommitPolsArray`. Both these functions use the `pil` object in order to create two crucial objects:
+The _pilcom_ package also provides two functions; _newConstPolsArray_ and _newCommitPolsArray_. Both these functions use the _pil_ object in order to create two crucial objects:
 
-1. First is the constant polynomials object `constPols`, which is created by the `newConstPolsArray` function, and
-2. Second is the committed polynomials object `cmPols`, created by `newCommitPolsArray`.
+1. First is the constant polynomials object _constPols_, which is created by the _newConstPolsArray_ function, and
+2. Second is the committed polynomials object _cmPols_, created by _newCommitPolsArray_.
 
-Below is an outline of the **pilcom** package.
+Below is an outline of the _pilcom_ package.
 
 ```js
 const { newConstantPolsArray, newCommitPolsArray, compile } = require("pilcom");
@@ -45,7 +45,7 @@ async function execute() {
 
 ## Accessing execution trace
 
-The above-mentioned objects contain useful information about the PIL itself, such as the provided length of the program `N`, the total number of constant polynomials and the total number of committed polynomials. Accessing these objects will allow us to fill the entire execution trace for that PIL.
+The above-mentioned objects contain useful information about the PIL itself, such as the provided length of the program N, the total number of constant polynomials and the total number of committed polynomials. Accessing these objects allows us to fill the entire execution trace for that PIL.
 
 A specific position of the execution trace can be accessed by using the syntax:
 
@@ -55,16 +55,16 @@ pols.Namespace.Polynomial[i]
 
 Note that;
 
-- `pols` points to one of the above-mentioned objects; `constPols` and `cmPols` objects
-- `Namespace` is a specific `namespace` among the ones defined by the PIL files
-- `Polynomial` refers to one of the polynomials defined under the scope of the `namespace`
+- _pols_ points to one of the above-mentioned objects; _constPols_ and _cmPols_ objects
+- _Namespace_ is a specific _namespace_ among the ones defined by the PIL files
+- _Polynomial_ refers to one of the polynomials defined under the scope of the _namespace_
 - index $i$ is an integer in the range $[0, N − 1]$, representing the row of the current polynomial
 
 Using these, the polynomials can now be filled.
 
-## `Main.pil` code example
+## _Main.pil_ code example
 
-In our example, we recall the `main.pil` seen in the [Connection arguments](connection-arguments.md) section about $4$-bit integers.
+In our example, we recall the _main.pil_ seen in the [Connection arguments](connection-arguments.md) section about $4$-bit integers.
 
 Since we are only allowed to use $4$-bit integers, inputs for the trace, which are also the ones introduced in the $\mathtt{Main.a}$ polynomial, is a chain of integers n ascending cyclically from $0$ to $15$.
 
@@ -117,9 +117,9 @@ async function buildcommittedPolynomials(cmPols, polDeg) {
 }
 ```
 
-Once the constant and committed polynomials have been filled in, we can check whether these polynomials actually satisfy the constraints defined in the PIL file, by using a function called `verifyPil`.
+Once the constant and committed polynomials have been filled in, we can check whether these polynomials actually satisfy the constraints defined in the PIL file, by using a function called _verifyPil_.
 
-Below is the piece of code that constructs the polynomials and checks the constraints. If the verification procedure fails, we should not proceed to the proof generation because it will lead to false proof. For the sake of brevity, we simply use the line ```// ... Previous Code``` to indicate where the PIL code being verified would be inserted.
+Below is the piece of code that constructs the polynomials and checks the constraints. If the verification procedure fails, we should not proceed to the proof generation because it leads to false proof. For the sake of brevity, we simply use the line `// ... Previous Code` to indicate where the PIL code being verified would be inserted.
 
 ```js
 const { newConstantPolsArray, newCommitPolsArray, compile, verifyPil } = require("pilcom");