Small edits to PIL and zkASM

nadimkobeissi · nadimkobeissi · commit 0720894daadc · 2023-12-01T14:22:05.000+01:00
diff --git a/docs/pos/how-to/smart-contracts/chainstack.md b/docs/pos/how-to/smart-contracts/chainstack.md
@@ -12,7 +12,7 @@ Chainstack provides infrastructure for Ethereum-based applications and other blo
 
 Foundry is a fast toolkit for Ethereum application development written in Rust. It provides testing, interaction with EVM smart contracts, sending transactions, and blockchain data retrieval.
 
-!!! note
+!!! tip
 
     If you have any questions, reach out in the [<ins>Chainstack Discord</ins>](https://discord.com/invite/Cymtg2f7pX) server.
 
diff --git a/docs/zkEVM/specifications/pil/compiling-using-pilcom.md b/docs/zkEVM/specifications/pil/compiling-using-pilcom.md
@@ -1,15 +1,4 @@
----
-id: pil-compile
-title: Compilation of PIL Programs
-sidebar_label: Compilation
-description: This document describes how Polynomial Identity Language programs are compiled by PILCOM.
-keywords:
-  - polygon
-  - PIL
-  - zkEVM
-  - pilcom
-  - compilation
----
+This document describes how Polynomial Identity Language programs are compiled by PILCOM.
 
 Depending on the language used in implementation, every PIL code can be compiled into either a $\texttt{JSON}$ file or a $\texttt{C++}$ code by using a compiler called $\bf{pilcom}$. 
 
diff --git a/docs/zkEVM/specifications/pil/configuration-files.md b/docs/zkEVM/specifications/pil/configuration-files.md
@@ -1,15 +1,4 @@
----
-id: pil-config
-title: PIL Configuration File
-sidebar_label: PIL Configuration
-description: The following document describes why Polynomial Identity Language uses a special configuration file.
-keywords:
-  - polygon
-  - PIL
-  - zkEVM
-  - configuration
-  - dependency inclusion
----
+The following document describes why Polynomial Identity Language uses a special configuration file.
 
 In order for PIL to securely enable modularity, especially in complex settings such as the Polygon zkEVM's, where the Main SM has several secondary state machines executing different computations, a **dependency inclusion feature** among different `.pil` files needed to be developed.
 
diff --git a/docs/zkEVM/specifications/pil/connection-arguments.md b/docs/zkEVM/specifications/pil/connection-arguments.md
@@ -1,29 +1,14 @@
----
-id: connect-arg
-title: Connection Arguments
-sidebar_label: Connection Arguments
-description: This document describes the Connection Arguments and how they are used in Polynomial Identity Language.
-keywords:
-  - polygon
-  - PIL
-  - zkEVM
-  - connection arguments
-  - Copy Satisfiability
----
-
-## Copy Satisfiability
+This document describes the Connection Arguments and how they are used in Polynomial Identity Language.
 
 ### Connection Argument
 
 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$ $\text{\it{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 $\text{\it{copy-satisfies}}$ a partition of $[n]$.
 
-:::info
+!!! info
 
-We use the term “connection” instead of “copy-satisfaction” because the argument is used in PIL in a more general sense than in the original definition given in [<ins>GWC19</ins>](https://eprint.iacr.org/2019/953).
-
-:::
+    We use the term “connection” instead of “copy-satisfaction” because the argument is used in PIL in a more general sense than in the original definition given in [<ins>GWC19</ins>](https://eprint.iacr.org/2019/953).
 
 ### Example
 
@@ -93,11 +78,9 @@ pol constant SA;
 
 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.
+!!! 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.
 
 ## Multiple Copy Satisfiability
 
diff --git a/docs/zkEVM/specifications/pil/cyclicity-in-pil.md b/docs/zkEVM/specifications/pil/cyclicity-in-pil.md
@@ -1,14 +1,4 @@
----
-id: cyclic-nature
-title: Cyclic Nature of PIL
-sidebar_label: Cyclic Nature
-description: This document describes how to introduce cyclicity to execution traces in Polynomial Identity Language.
-keywords:
-  - polygon
-  - PIL
-  - zkEVM
-  - cyclic nature
----
+This document describes how to introduce cyclicity to execution traces in Polynomial Identity Language.
 
 In order to synchronize the execution trace of a given program with the subgroup $G$ of the multiplicative group $\mathbb{F}^*$, over which interpolation is performed, an extra constant polynomial (or precompiled column) is added to the trace. 
 
@@ -44,27 +34,26 @@ $$
 
 Denote the cyclic group over which interpolation is carried out as $G = \{ g, g^2, g^3, g^4 = 1 \} \subset \mathbb{F}$.
 
-:::info Concession to an abuse of notation
-We use the symbols $\texttt{a}$ and $\texttt{b}$, that denote columns of the execution trace, to also denote the corresponding polynomials resulting from interpolation. The columns $\texttt{a}$ and $\texttt{b}$ are best expressed as arrays,
+!!! info Concession to an abuse of notation
+    We use the symbols $\texttt{a}$ and $\texttt{b}$, that denote columns of the execution trace, to also denote the corresponding polynomials resulting from interpolation. The columns $\texttt{a}$ and $\texttt{b}$ are best expressed as arrays,
 
-$$
-\texttt{a} = [1,0,-1,1] \ \text{and}\ \texttt{b} = [1,2,2,1]
-$$
+    $$
+    \texttt{a} = [1,0,-1,1] \ \text{and}\ \texttt{b} = [1,2,2,1]
+    $$
 
-while the respective polynomials that result from interpolation, should rather be denoted differently, say with, $P(X)$ and $Q(X)$, such that for each row index $i$,
+    while the respective polynomials that result from interpolation, should rather be denoted differently, say with, $P(X)$ and $Q(X)$, such that for each row index $i$,
 
-$$
-P(g^i) = \texttt{a}[i]\ \ \text{and}\ \ Q(g^i) = \texttt{b}[i] \tag{eqn}
-$$
+    $$
+    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}$ will therefore be seen written as,
 
-$$
-\texttt{a}(g^i) = \texttt{a}[i]\ \ \text{and}\ \ \texttt{b}(g^i) = \texttt{b}[i].
-$$
+    $$
+    \texttt{a}(g^i) = \texttt{a}[i]\ \ \text{and}\ \ \texttt{b}(g^i) = \texttt{b}[i].
+    $$
 
-For the sake of convenience, in this particular example, the row index starts at $0$ just so it syncs with the normal array indexing.
-:::
+    For the sake of convenience, in this particular example, the row index starts at $0$ just so it syncs with the normal array indexing.
 
 ### Constraints And Cyclicity
 
diff --git a/docs/zkEVM/specifications/pil/filling-polynomials.md b/docs/zkEVM/specifications/pil/filling-polynomials.md
@@ -1,20 +1,8 @@
----
-id: filling-polynomial
-title: Filling Polynomials
-sidebar_label: Filling Polynomials
-description: This document describes how to fill Polynomials in PIL using JavaScript and Pilcom.
-keywords:
-  - polygon
-  - PIL
-  - zkEVM
-  - pilcom
-  - Filling Polynomials
-  - execution trace
----
+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. 
 
-To do so, we are going to use the execution trace of a program previously discussed in the [Connecting Programs](connect-programs.md) section.
+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.
 
@@ -76,7 +64,7 @@ Using these, the polynomials can now be filled.
 
 ## `Main.pil` Code Example
 
-In our example, we recall the `main.pil` seen in the [Connecting Programs](connect-programs.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$.
 
diff --git a/docs/zkEVM/specifications/pil/generating-proofs.md b/docs/zkEVM/specifications/pil/generating-proofs.md
@@ -1,19 +1,6 @@
----
-id: generate-proof
-title: Generating Proofs Using pil-stark
-sidebar_label: Generating Proofs
-description: The following document describes how proofs of execution correctness are generated using pil-stark package.
-keywords:
-  - polygon
-  - PIL
-  - zkEVM
-  - proofs of execution correctness
-  - starkSetup
-  - starkGen
-  - starkVerify
----
-
-Once the constant and the committed polynomials are filled (as seen in the [Filling Polynomial section](filling-polynomial.md)), the next step is generation of a proof of correctness.
+The following document describes how proofs of execution correctness are generated using pil-stark package.
+
+Once the constant and the committed polynomials are filled (as seen in the [Filling Polynomial section](filling-polynomials.md)), the next step is generation of a proof of correctness.
 
 A Javascript package called `pil-stark` has been specially designed to work together with `pilcom` to generate STARK proofs for execution correctness of programs being verified.
 
diff --git a/docs/zkEVM/specifications/pil/inclusion-arguments.md b/docs/zkEVM/specifications/pil/inclusion-arguments.md
@@ -1,16 +1,4 @@
----
-id: pil-arguments
-title: Inclusion Arguments
-sidebar_label: Inclusion Arguments
-description: This document describes how Polynomial Identity Language implements Inclusion Arguments.
-keywords:
-  - polygon
-  - PIL
-  - zkEVM
-  - execution trace
-  - addition
-  - polynomials
----
+This document describes how Polynomial Identity Language implements Inclusion Arguments.
 
 For most of the programs used in the zkEVM's Prover, the values recorded in the columns of execution traces are field elements. 
 
diff --git a/docs/zkEVM/specifications/pil/index.md b/docs/zkEVM/specifications/pil/index.md
@@ -1,18 +1,3 @@
----
-id: introduction
-title: Polynomial Identity Language
-sidebar_label: Introduction
-description: Polynomial Identity Language (PIL) is a domain-specific language (DSL) created to provide developers with a holistic framework for constructing programs through an easy-to-use interface, and abstracting the complexity of proof/verification mechanisms.
-keywords:
-  - polygon
-  - PIL
-  - zkEVM
-  - introduction to PIL
-  - Polynomial Identity Language
----
-
-## Overview
-
 **Polynomial Identity Language (PIL)** is a domain-specific language (DSL) created to provide developers with a holistic framework for constructing programs through an easy-to-use interface, and abstracting the complexity of proof/verification mechanisms. In the zkEVM context, PIL is the very DNA of verification.
 
 One of the main peculiarities of PIL is its modularity, which allows programmers to define parametrizable programs called `namespaces`. Developers can therefore create their own custom namespaces and instantiate them from larger programs or some public library.
diff --git a/docs/zkEVM/specifications/pil/modular-programs.md b/docs/zkEVM/specifications/pil/modular-programs.md
@@ -1,14 +1,4 @@
----
-id: connect-programs
-title: Connecting Programs
-sidebar_label: Connecting Programs
-description: One of the core features of Polynomial Identity Language is that it allows modular design of its programs. This document describes how PIL connects programs.
-keywords:
-  - polygon
-  - PIL
-  - zkEVM
-  - modular
----
+One of the core features of Polynomial Identity Language is that it allows modular design of its programs. This document describes how PIL connects programs.
 
 ## Modular Design
 
@@ -72,11 +62,11 @@ pol commit a, neg_a , op;
 a in Global.BITS4;
 ```
 
-:::info Remarks about the above code
-`BITS4` is a polynomial containing each of the possible 4-bit integers. These 4-bit integers can be chosen in any order when constructing `BITS4` because **inclusion checks do not respect orderings**.
+!!! info "Remarks about the above code"
 
-Also, observe that `BITS4` is called from a namespace which is different from where it is defined. The syntax `Namespace.polynomial` can be used to access polynomials of other namespaces.
-:::
+    `BITS4` is a polynomial containing each of the possible 4-bit integers. These 4-bit integers can be chosen in any order when constructing `BITS4` because **inclusion checks do not respect orderings**.
+
+    Also, observe that `BITS4` is called from a namespace which is different from where it is defined. The syntax `Namespace.polynomial` can be used to access polynomials of other namespaces.
 
 The traditional procedure is to put different namespaces in separate files and then use the include keyword to **“connect”** them. For instance, two programs can be defined as follows.
 
diff --git a/docs/zkEVM/specifications/pil/permutation-arguments.md b/docs/zkEVM/specifications/pil/permutation-arguments.md
@@ -1,15 +1,4 @@
----
-id: permutation-arg
-title: Permutation Arguments
-sidebar_label: Permutation Arguments
-description: This document describes Permutation Arguments and how they are used in Polynomial Identity Language.
-keywords:
-  - polygon
-  - PIL
-  - zkEVM
-  - permutation arguments
-  
----
+This document describes Permutation Arguments and how they are used in Polynomial Identity Language.
 
 ## Definition
 
@@ -21,11 +10,9 @@ $$
 
 A protocol $(\mathcal{P}, \mathcal{V})$ is a **permutation argument** if the protocol can be used by $\mathcal{P}$ to prove to $\mathcal{V}$ that two vectors in $\mathbb{F}^n$ are a permutation of each other.
 
-:::note
+!!! note
 
-Unlike inclusion arguments, the two vectors subject to a permutation argument must have the same length.
-
-:::
+    Unlike inclusion arguments, the two vectors subject to a permutation argument must have the same length.
 
 In the PIL context, the Plookup permutation argument between two columns $\texttt{a}$ and $\texttt{b}$ can be declared using the keyword "$\texttt{is}$" and using the syntax "$\mathtt{ \{ a \}\ is\ \{ b \}}$", where $\texttt{a}$ and $\texttt{b}$ do not necessarily need to be defined in different programs.
 
@@ -96,8 +83,6 @@ pol commit d, e, f;
 pol commit sel;
 ```
 
-:::info Remark
-
-The $\texttt{sel}$ column should be turned on (i.e., $\texttt{sel}$ set to $1$) the same number of times in both programs. Otherwise, a permutation cannot exist between any of the columns, since the resulting vectors would be of different lengths. This allows the use of this kind of argument even if both execution traces do not contain the same amount of rows.
+!!! info Remark
 
-:::
+    The $\texttt{sel}$ column should be turned on (i.e., $\texttt{sel}$ set to $1$) the same number of times in both programs. Otherwise, a permutation cannot exist between any of the columns, since the resulting vectors would be of different lengths. This allows the use of this kind of argument even if both execution traces do not contain the same amount of rows.
diff --git a/docs/zkEVM/specifications/pil/plonk-in-pil.md b/docs/zkEVM/specifications/pil/plonk-in-pil.md
@@ -1,14 +1,4 @@
----
-id: pil-plonk
-title: PLONK In PIL
-sidebar_label: PLONK in PIL
-description: This document describes how PLONK verification is implemented in Polynomial Identity Language.
-keywords:
-  - polygon
-  - PIL
-  - zkEVM
-  - PLONK
----
+This document describes how PLONK verification is implemented in Polynomial Identity Language.
 
 This document will help us in understanding how to implement $\mathcal{PlonK}$ verification by using **connection arguments**. Let's begin!
 
diff --git a/docs/zkEVM/specifications/pil/public-values.md b/docs/zkEVM/specifications/pil/public-values.md
@@ -1,15 +1,4 @@
----
-id: public-values
-title: Public Values
-sidebar_label: Public Values
-description: Public Values refers to values of committed polynomials that are known to both the prover and the verifier, as part of the arithmetization process.
-keywords:
-  - polygon
-  - PIL
-  - zkEVM
-  - public values
-  - fibonacci
----
+Public Values refers to values of committed polynomials that are known to both the prover and the verifier, as part of the arithmetization process.
 
 Public Values refers to values of committed polynomials that are known to both the prover and the verifier, as part of the arithmetization process. For example, if the prover is claiming to know the output of a certain computation, then its arithmetization would lead to the inclusion of a public value to some of the polynomials representing such a computation.
 
diff --git a/docs/zkEVM/specifications/pil/simple-example.md b/docs/zkEVM/specifications/pil/simple-example.md
@@ -1,15 +1,4 @@
----
-id: simple-program
-title: Simple PIL Program
-sidebar_label: Simple PIL Program
-description: This document explains the fundamentals of Polynomial Identity Language with the help of a simple multiplier program.
-keywords:
-  - polygon
-  - PIL
-  - zkEVM
-  - simple PIL program
-  - multiplier
----
+This document explains the fundamentals of Polynomial Identity Language with the help of a simple multiplier program.
 
 PIL was designed with the aim to simplify the proving and verification of execution correctness. Given that PIL is geared towards modularity, each PIL code has to stipulate a unique identifier for each program. It therefore has an effective syntax that is easy to learn.
 
diff --git a/docs/zkEVM/specifications/zkasm/basic-syntax.md b/docs/zkEVM/specifications/zkasm/basic-syntax.md
@@ -16,13 +16,11 @@ keywords:
 
 This section is devoted to explain the basic syntax of zkASM from a high-level perspective. Advanced syntax is totally dependant on the use case (e.g. the design of a zkEVM) and will be explained in more detail with more complete examples later on.
 
-:::info
+!!! info
 
-Each instruction of the zkASM is executed sequentially (the exception being the execution of a jump) one after the other.
+    Each instruction of the zkASM is executed sequentially (the exception being the execution of a jump) one after the other.
 
-Instructions are depicted line by line and are divided in two parts. The left-side part includes the code that is actually getting executed in the corresponding file, while the right-side part is related to the execution of opcodes, jumps and subroutines, indicated by the colon "$:$" symbol.
-
-:::
+    Instructions are depicted line by line and are divided in two parts. The left-side part includes the code that is actually getting executed in the corresponding file, while the right-side part is related to the execution of opcodes, jumps and subroutines, indicated by the colon "$:$" symbol.
 
 ## Comments and Modules
 
diff --git a/mkdocs.yml b/mkdocs.yml
