Merge branch 'main' into add-test-coverage-reporting

.gitignore

@@ -5,3 +5,4 @@
 __pycache__
 *.so
 .ipynb_checkpoints
+_build

book/_config.yml

@@ -0,0 +1,28 @@
+# Book settings
+# Learn more at https://jupyterbook.org/customize/config.html
+
+title: Introduction to Chiquito
+author: Leo Lara, Steve Wang
+logo: pselogo.png
+
+# Force re-execution of notebooks on each build.
+# See https://jupyterbook.org/content/execute.html
+execute:
+  execute_notebooks: force
+
+# Define the name of the latex output file for PDF builds
+latex:
+  latex_documents:
+    targetname: book.tex
+
+# Information about where the book exists on the web
+repository:
+  url: https://github.com/privacy-scaling-explorations/chiquito  # Online location of your book
+  path_to_book: book  # Optional path to your book, relative to the repository root
+  branch: main  # Which branch of the repository should be used when creating links (optional)
+
+# Add GitHub buttons to your book
+# See https://jupyterbook.org/customize/config.html#add-a-link-to-your-repository
+html:
+  use_issues_button: true
+  use_repository_button: true

book/_toc.yml

@@ -0,0 +1,30 @@
+# Table of contents
+# Learn more at https://jupyterbook.org/customize/toc.html
+
+format: jb-book
+root: landing_page
+parts:
+  - caption: Part 1 - Intro to Chiquito
+    chapters:
+    - file: part1_chapter1
+    - file: part1_chapter2
+    - file: part1_chapter3
+    - file: part1_chapter4
+    - file: part1_chapter5
+  - caption: Part 2 - Fibonacci Example
+    chapters:
+    - file: part2_chapter1
+    - file: part2_chapter2
+    - file: part2_chapter3
+    - file: part2_chapter4
+    - file: part2_chapter5
+  - caption: Part 3 - MiMC7 Example
+    chapters:
+    - file: part3_chapter1
+    - file: part3_chapter2
+    - file: part3_chapter3
+    - file: part3_chapter4
+  - caption: Appendix
+    chapters:
+    - file: appendix_chapter1
+    - file: appendix_chapter2

book/appendix_chapter1.md

@@ -0,0 +1,9 @@
+# Design Principles
+
+**Abstraction**. As circuit complexity increases, abstraction is inevitable. By abstracting constraint building and column placement, Chiquito improves the readability and learnability of Halo2 circuits, which can not only standardize and simplify the code base for complex projects such as the zkEVM, but also onboard more circuit developers.
+
+**Composability**. Chiquito circuits are fully composable with Halo2 circuits, which allows developers to write any part or the entirety of a circuit in Chiquito and integrate with other Halo2 circuits.
+
+**Modularity**. The AST and IR representations of a circuit allow Chiquito to integrate any frontend that can compile into the AST data structure and any backend that can compile from the IR data structure. For example, we can have a Python frontend that compiles to Chiquito AST/IR, which compiles to a Sangria backend. Modularity allows for future extensions.
+
+**User Experience**. Chiquito simplifies and optimizes user experience. For example, annotations for constraints are automatically generated for debugging messages.

book/appendix_chapter2.md

@@ -0,0 +1,22 @@
+# Chiquito vs Halo2
+
+There are two major architectural differences between Chiquito and Halo2:
+
+- Chiquito circuit is composed of “step” instances. Each step type defines the constraints among witnesses, fixed columns, and lookup tables. Step instances are also called “super rows”, each composed of one or multiple rows in a PLONKish table. We made this design choice to allow for more complex constraints, which sometimes require allocating multiple Halo2 rows.
+- Chiquito DSL is based on “signals” rather than columns in order to abstract away column placements. One signal can be placed in different columns across different steps, all handled by Chiquito’s compiler.
+
+Chiquito circuit has the following architecture
+
+- Circuit
+    - Setup
+		- Forward signals
+		- Shared signals
+		- Fixed signals
+    	- Step types
+			- Setup
+				- Internal signals
+        		- Constraints
+        		- Transition constraints
+				- Lookup
+        	- Witness generation
+    - Trace

book/landing_page.md

@@ -0,0 +1,17 @@
+# Meet Chiquito
+
+Chiquito is a high-level structured language for implementing zero knowledge proof applications, currently being implemented in the DSL Working Group of PSE, Ethereum Foundation. It is a step-based zkDSL (zero knowledge domain specific language) that provides better syntax and abstraction for features like constraint building and column placement. Chiquito has a Halo2 backend, which is a low level zkDSL that writes circuits using the PLONKish arithemtization and is working on supporting additional backends.
+
+Chiquito can be written in both Python and Rust. This tutorial focuses on Python.
+
+The key advantages of Chiquito include: 
+- Abstraction and simplification on the readability and learnability of Halo2 circuits.
+- Composabiity with other Halo2 circuits.
+- Modularity of using multiple frontends (Python and Rust) and backends (Halo2 and beyond).
+- Smooth user experience with a dynamically typed language (Python).
+
+<p align="center">
+  <img src="https://hackmd.io/_uploads/HyuEr1cB2.png" width="180" height="80" alt="Image 2">
+  &nbsp; &nbsp; &nbsp;
+  <img src="https://hackmd.io/_uploads/HyZ0rycS2.png" width="70" height="100" alt="Image 3">
+</p>

book/part1_chapter1.md

@@ -0,0 +1,58 @@
+# What is Zero Knowledge Proof (Developer POV)?
+
+Zero Knowledge proofs (or ZKP) allow developers to create mathematical proofs that a computation have been executed correctly, while not having to reveal all the data of this computation.
+
+## What are the applications of ZKP?
+
+There are three main areas of application:
+ + Privacy: because not all data has to be reveal we can proof computations and facts while preserving privacy or secrecy of some part of the data.
+ + Scalability and verified computation: usually to check that a computation has been executed correctly you would need to execute it and check the results are the same. With ZKP you can validate the mathematical proof of the computation, and in some systems this could require less time and space resources than executing the computation itself.
+ + Interoperability and trustlessness: because ZKPs are based on mathematical proofs, an organisation or individual can trust a ZKP proof without trusting other participants.
+
+## What are ZKP proving systems?
+
+Proving systems allow to create ZKP for arbitrary computations. They are like a computer system that can execute an arbitrary computation. A ZKP circuit is a definition for a proving system that proofs a specific computation. For example, for bubble sort algorithm you could write a circuit for a specific proving system that proofs bubble sort executions.
+
+## What are the elements of a ZKP circuit?
+
+The main elements are:
+ + The witness: which is the data of the computation. The witness is made of many elements, sometimes called signals or cells. Some signals are public and other private, the public part is sometimes called the **instance** and the private part is sometimes called the **advice**. The witness usually contains the input and output of the computation, but also most or all its intermediate values (the trace).
+ + Setup: it is a series of constraints or assertions over the witness data, that define which computations are valid.
+ + Witness generation: an algorithm that helps calculating the right values for all the signals.
+ + Proving and validation key: given a setup the proving system can generate proving and validation pair of keys. Both can be made public.
+ + Proof and prover: given a setup and a witness, the prover using the proving key can generate a proof. This proof will be valid if and only if the witness follows the setup constraints.
+ + Validator: given a proof and the public part of the witness and a validation key, the validator using the proving system can check that the proof is valid. That is, to generate that proof the prover had to have a witness (if which this public part is part of) that followed the setup.
+
+It is important to note that if the prover and validator have agreed on the setup will have the same proving and validation keys, and will not have to trust each other.
+
+![](../images/zkp-process-diagram.png)
+
+## What is a ZKP arithmetization?
+
+An arithmetization is the way to represent the setup to the proving system. They are very low level and based on polynomials. As a simile, if the proving system is a CPU, the arithmetization is its machine code.
+
+## What is a ZKP low-level DSL?
+
+It is a tool to write arithmetization in a more developer friendly way, but still very close to the arithmetization. If arithmetization is machine code, a ZKP low-level DSL is like assembly.
+
+## What is a ZKP high-level structured language?
+
+They allow to write the setup in a way that is closer to the way a developer thinks about the computation, and they get compiled to the arithmetization. Following the previous simile a ZKP high-level structured language is like Python.
+
+Chiquito is an example of ZKP high-level structured language that is based on steps.
+
+## What is a Finite Prime Field?
+
+In ZKP the witness signals are not made of bytes, they are elements (or values) of a Finite Prime Field. We need to understand how FPFs work in order to write circuits.
+
+As a developer you can see it as a unsigned integer type where the maximum value is a prime minus one (`p - 1` instead of `2^n-1`) and addition and multiplication overflows as expected, so `a + b = a + b mod p` and `a * b = a * b mod p`.
+
+Negative values are obtained by the formula `a + (-a) mod p = 0`.
+
+The prime `p` is usually a very big number when used in ZKP, but we can see an easy example with `p = 7`.
+
+The posible values would be `0, 1, 2, 3, 4, 5` and `6`. If we go over `p` it overflows around to `0`. So for example `6 + 1 = 0` or `5 + 3 = 1`.
+
+Then for example  `-3 + 3 mod 7 = 0 ` which is satisfied by `4 + 3 mod 7 = 0 => -3 = 4`.
+
+This is a very short summary of what you need to know about FPFs.

book/part1_chapter2.md

@@ -0,0 +1,111 @@
+# What is Chiquito?
+
+Chiquito is a high-level structured language for implementing zero knowledge proof applications.
+
+Chiquito is being implemented in the DSL Working Group of PSE, Ethereum Foundation.
+
+<p align="center">
+  <img src="https://hackmd.io/_uploads/HyuEr1cB2.png" width="180" height="80" alt="Image 2">
+  &nbsp; &nbsp; &nbsp;
+  <img src="https://hackmd.io/_uploads/HyZ0rycS2.png" width="70" height="100" alt="Image 3">
+</p>
+
+
+## Why is chiquito different from other ZKP DSLs?
+
+Most ZKP DSLs are based on writing constraints, witness generation and some abstraction for DRY like templates or gadgets.
+
+Chiquito allows the developer to think in more high-level and structured abstractions that most ZKP DSLs, while not sacrificing performance.
+
+## What is the chiquito programming model?
+
+Chiquito starts from the idea that every zero knowledge proof represents a program (the setup), which can have many computations (the trace) that is proven for a certain input, output and intermediate values (the witness).
+
+The main structured abstraction in chiquito is the **step**. Any computation can be divided in individual steps. A program is represented by a circuit that has one or many **step types**, a particular computation is represented as a series of **step instances** or **trace steps** that can have arbitrary order.
+
+A step type contains:
+ + Setup: a series of constraints or assertions that must hold for a step instance of this type to be valid.
+ + Witness generation: code that for a particular input sets the values of the witness for a particular step instance.
+
+A chiquito circuit contains a trace function that for a given input will generate the step instances in a particular order and use the step type witness generation.
+
+Another important piece of Chiquito are the signals. They represent elements of the witness.
+
+Chiquito has many more features, but these are enough to start writing basic circuits.
+
+## What proving system chiquito uses?
+
+Currently Halo2 backend is implemented, but we are looking into implementing other backends.
+
+Chiquito frontend comes in two flavours: rust and python, so you can write Chiquito applications in either Rust or Python. PyChiquito, and any other language interface in the future, uses ChiquitoCore for most of its work, so adding new languages is easy.
+
+## What are the features of chiquito?
+
+ + Step-based, that abstracts out the computation that you want to prove.
+ + Signals, that abstract out the data (witness) and how it is placed and handled.
+ + Constraint builder, allows you to write the constraints of your application in a more readable and natural way.
+ + Trace based witness generation, a way to generate the data that you are trying to prove that matches how computation is done.
+ + Super circuits, that allow combining many circuits into one.
+ + Lookup tables, that allow sharing data between multiple circuits.
+ + Expose signals as public very easily.
+ + Automatic padding.
+ + Completely modular platform, that allows writing circuits in multiple languages and use different proving systems.
+
+PLONKish-specific features:
+ + Halo2 backend ready.
+ + PLONKish Cell Managers. These are modular strategies to place signals in the PLONKish columns and rotations. These allows for steps to use different numbers of rows and columns, in a configurable way, so you can find the most efficient structure for your circuit.
+ + PLONKish step selector builders. These are modular strategies to activate the steps in the witness.
+
+Planned:
+ + Nested steps, will allow more complex circuits and allow circuits coordination in proving systems without advice based lookup tables.
+ + Gadget abstraction.
+ + Arbitrary boolean assertions.
+
+In research:
+ + Signal typing system, which allows statically checking for soundness issues.
+ + Folding backend with ProtoStar, HyperNova, and/or others.
+ + Tracers
+
+## Fibonacci circtuit in PyChiquito.
+
+But better see for yourself:
+
+```
+class FiboStep(StepType):
+    def setup(self: FiboStep):
+        self.c = self.internal("c")
+        self.constr(eq(self.circuit.a + self.circuit.b, self.c))
+        self.transition(eq(self.circuit.b, self.circuit.a.next()))
+        self.transition(eq(self.c, self.circuit.b.next()))
+
+    def wg(self: FiboStep, args: Tuple[int, int]):
+        a_value, b_value = args
+        self.assign(self.circuit.a, F(a_value))
+        self.assign(self.circuit.b, F(b_value))
+        self.assign(self.c, F(a_value + b_value))
+
+class Fibonacci(Circuit):
+    def setup(self: Fibonacci):
+        self.a: Queriable = self.forward("a")
+        self.b: Queriable = self.forward("b")
+
+        self.fibo_step = self.step_type(FiboStep(self, "fibo_step"))
+
+        self.pragma_num_steps(11)
+
+    def trace(self: Fibonacci, args: Any):
+        self.add(self.fibo_step, (1, 1))
+        a = 1
+        b = 2
+        for i in range(1, 11):
+            self.add(self.fibo_step, (a, b))
+            prev_a = a
+            a = b
+            b += prev_a
+
+fibo = Fibonacci()
+fibo_witness = fibo.gen_witness(None)
+fibo.halo2_mock_prover(fibo_witness)
+```
+
+This is explained in more detail in the tutorial, but you can see already how concise and clear it is.