updated pages

book/_build/html/.buildinfo

@@ -0,0 +1,4 @@
+# Sphinx build info version 1
+# This file hashes the configuration used when building these files. When it is not found, a full rebuild will be done.
+config: 02af6eb916b22e1e52b25f8425e8f337
+tags: 645f666f9bcd5a90fca523b33c5a78b7

book/_build/html/_sources/chiquito_programming_model.md

@@ -0,0 +1,104 @@
+# Chiquito programming model
+
+## ZKP as trace
+
+ZKP generates proofs that an algorithm has been execute correctly.
+
+The best way we can analyse a particular execution of an algorithm is by its trace.
+
+For example:
+
+```python=
+def bubbleSort(arr):
+	n = len(arr)
+	
+	for i in range(n-1):
+		for j in range(0, n-i-1):
+
+			if arr[j] > arr[j + 1]:
+				arr[j], arr[j + 1] = arr[j + 1], arr[j]
+```
+
+A trace for a particular input is the actual steps that are executed in order.
+
+For example if `arr = [64, 34, 25, 12, 22, 11, 90]`, the trace is:
+
+```
+set n to length of arr which is 7
+set i to 1
+set j to 0
+compare arr[j] > arr[j+1] => arr[0] > arr[1] => 64 > 34 => true
+set arr[0] to arr[1] and arr[1] to arr[0] => arr[0] = 34, arr[1] = 64
+// and so on...
+```
+
+It is important to understand that each step has a pre-state, with the values of the variables before the execution of the step, and a post-state with the values of the variables after the execution of the step. The post-state of a step is the pre-state of the next one.
+
+If we include the states indented:
+```
+	arr = [64, 34, 25, 12, 22, 11, 90]
+	n = ?, i = ?, j = ?
+set n to lenght of arr which is 7
+	arr = [64, 34, 25, 12, 22, 11, 90]
+	n = 7, i = ?, j = ?
+set i to 1
+	arr = [64, 34, 25, 12, 22, 11, 90]
+	n = 7, i = 1, j = ?
+set j to 0
+	arr = [64, 34, 25, 12, 22, 11, 90]
+	n = 7, i = 1, j = 0
+compare arr[j] > arr[j+1] => arr[0] > arr[1] => 64 > 34 => true
+	arr = [64, 34, 25, 12, 22, 11, 90]
+	n = 7, i = 1, j = 0
+set arr[0] to arr[1] and arr[1] to arr[0] => arr[0] = 34, arr[1] = 64
+	arr = [34, 64, 25, 12, 22, 11, 90]
+	n = 7, i = 1, j = 0
+// and so on...
+```
+
+## ZKP circuit as a trace checker
+
+We can see a ZKP circuit as a series of step types, and their constraints relative to the post-state and pre-state, and also potentially some internal values.
+
+For example, we can have the step type `set $variable to $value` and the constraint would be that the post state of `$variable` should be `$value`.
+
+## ZKP witness as a trace
+
+In the same way, we can see the witness as a the trace of a computation plus some information about the states between the steps.
+
+The programming model in chiquito follows 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).
+
+## Step types and step instances
+
+A trace is made of a sequence of step instances or trace steps, that contains the data about that step instance.
+
+Each step instance belong to a step type. A step types contains rules (or constraints) about whether a step instance is valid in relation to its data and the data of other step instances relative to it.
+
+Step types are part of the setup, which means that they cannot change between proofs, but this circuit can proof all possible traces, as they are part of the witness.
+
+## Signals and rotations
+
+Signals represent are elements of the witness that have a independent value for each trace step, but in chiquito paradigm you can see them as variables on the trace steps.
+
+Rotation refer to the capability of creating rules that involved the value of signals in other trace steps with an offset relative to the trace step, not just the value of a signal. A rotation of 0, represent the value of the signal in the same trace step, a rotation of 1 in the next step, a rotation of -1 in the previous step, in general any rotation number is posible.
+
+## Types of signals
+
+There are two types of signals that are shared between the step types, **forward** signals and **shared** signals. The difference is that forward signals can only rotate to the next step, while shared signals can rotate to any number of steps. However, circuits that only use forward signals are more efficient in some cases, so you should try to use only forward signals.
+
+**Internal** signals are not shared between step types, and belong to a specific step type and cannot be rotated.
+
+There is a special type of signal called **fixed**, that is not part of the witness and it is used to contain constants.
+
+|          | Scope            | Rotation  | Role    |
+| -------- | ---------------- | --------- | ------- |
+| Forward  | All step types   | Only next | Witness |
+| Shared   | All step types   | Any       | Witness |
+| Internal | Single step type | None      | Witness |
+| Fixed    | All step types   | Any       | Setup   |
+
+## Putting everything together
+
+TODO: Diagram
+
+

book/_build/html/_sources/landing_page.md

@@ -0,0 +1,11 @@
+# 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>

tutorials/part3_chapter1.ipynb → book/_build/html/_sources/part2_chapter1.ipynb

@@ -6,7 +6,7 @@
    "id": "14a9a617-1c05-40c8-b4ef-3cc2fbcf99fe",
    "metadata": {},
    "source": [
-    "# Part 3: Fibonacci Example\n",
+    "# Part 2: Fibonacci Example\n",
     "The best learning is by doing, In this Chapter, we will walk through the [fibonacci.py](https://github.com/privacy-scaling-explorations/chiquito/blob/main/examples/fibonacci.py) example.\n",
     "# Chapter 1: Fibonacci and Chiquito Concepts\n",
     "The Fibonacci series is an infinite series, starting from \"1\" and \"1\", in which every number in the series is the sum of two numbers preceding it in the series. The first few rounds for the Fibonacci series are:\n",

tutorials/part3_chapter2.ipynb → book/_build/html/_sources/part2_chapter2.ipynb

@@ -5,7 +5,7 @@
    "id": "8ab5d5e4-6d9e-4856-ad0b-0e2cf7bb13fb",
    "metadata": {},
    "source": [
-    "# Part 3: Fibonacci Example\n",
+    "# Part 2: Fibonacci Example\n",
     "# Chapter 2: StepType and Circuit\n",
     "In this Chapter, we code out the concepts learned in Chapter 1 in PyChiquito, but before that, let's import the dependencies first.\n",
     "## Imports"

tutorials/part3_chapter3.ipynb → book/_build/html/_sources/part2_chapter3.ipynb

@@ -5,7 +5,7 @@
    "id": "aab29f93-4311-4bff-a123-38f412556922",
    "metadata": {},
    "source": [
-    "# Part 3: Fibonacci Example\n",
+    "# Part 2: Fibonacci Example\n",
     "# Chapter 3: Witness\n",
     "Now, we will generate multiple witnesses to test the soundness of our circuit constraints. Note that we only intend to accept the following set of values for signals \"a\", \"b\", and \"c\". \"Soundness\" in this context refers to faulty witness successfully verified against the constraints (false positives), so any set of witness assignments that is different from the table below but still passes the constraints incurs a \"soundness\" error.\n",
     "\n",

tutorials/part3_chapter4.ipynb → book/_build/html/_sources/part2_chapter4.ipynb

@@ -5,7 +5,7 @@
    "id": "291ef2c6-bce5-4166-973d-d34d04f31bfb",
    "metadata": {},
    "source": [
-    "# Part 3: Fibonacci Example\n",
+    "# Part 2: Fibonacci Example\n",
     "# Chapter 4: Multiple StepTypes"
    ]
   },

tutorials/part3_chapter5.ipynb → book/_build/html/_sources/part2_chapter5.ipynb

@@ -5,7 +5,7 @@
    "id": "5ec470ae-aca1-4c7e-a048-d115633531d8",
    "metadata": {},
    "source": [
-    "# Part 3: Fibonacci Example\n",
+    "# Part 2: Fibonacci Example\n",
     "# Chapter 5: Padding and Exposing Signals\n",
     "In prior examples, all Fibonacci circuit witnesses have the same number of step instances. According to our analogy where a circuit is considered a piece of hardware and its witnesses compatible softwares, it's natural to think that we'd allow for more flexibility for our witnesses. Most immediately, and we shouldn't limit all Fibonacci circuit witnesses to have the same number of step instances.\n",
     "\n",

tutorials/part4_chapter1.ipynb → book/_build/html/_sources/part3_chapter1.ipynb

@@ -5,7 +5,7 @@
    "id": "2b08fd8e-65b8-433b-8a99-71aa13ad30ad",
    "metadata": {},
    "source": [
-    "# Part 4: MiMC7 Example\n",
+    "# Part 3: MiMC7 Example\n",
     "In this Chapter, we will walk through the [mimc7.py] (https://github.com/privacy-scaling-explorations/chiquito/blob/main/examples/mimc7.py) example.\n",
     "# Chapter 1: MiMC7 Concepts\n",
     "MiMC7 is a zk-friendly hash function. By \"zk-friendly\" we mean that the function is designed to minimize circuit size for zero knowledge proofs by using only additions and multiplications. Other common non-zk-friendly hash functions such as SHA256 requires many bit operations and therefore can be very costly in terms of circuit size.\n",

tutorials/part4_chapter2.ipynb → book/_build/html/_sources/part3_chapter2.ipynb

@@ -5,7 +5,7 @@
    "id": "1c24b711-a68f-4215-a8e6-556c078dddec",
    "metadata": {},
    "source": [
-    "# Part 4: MiMC7 Example\n",
+    "# Part 3: MiMC7 Example\n",
     "# Chapter 2: First Attempt\n",
     "In this Chapter, we will code out the MiMC7 circuit based on our understanding of the algorithm from the prior chapter. There are no new Chiquito concepts other than the ones introduced in **Part 3: Fibonacci Example**, which you are highly recommended to go through first before starting this Chapter.\n",
     "\n",

tutorials/part4_chapter3.ipynb → book/_build/html/_sources/part3_chapter3.ipynb

@@ -5,7 +5,7 @@
    "id": "f6da1ade-1de6-4921-9485-40f1c18b1098",
    "metadata": {},
    "source": [
-    "# Part 4: MiMC7 Example\n",
+    "# Part 3: MiMC7 Example\n",
     "# Chapter 2: Witness\n",
     "As is the best practice with circuit building, we will generate evil witnesses to test the soundness of our circuit constraints. It's always helpful to review the circuit table again:\n",
     "\n",

tutorials/part4_chapter4.ipynb → book/_build/html/_sources/part3_chapter4.ipynb

@@ -5,7 +5,7 @@
    "id": "be7fb603-4820-410e-8250-abc52e81a6b0",
    "metadata": {},
    "source": [
-    "# Part 4: MiMC7 Example\n",
+    "# Part 3: MiMC7 Example\n",
     "# Chapter 4: Fixed Signals, Lookup Tables, and Super Circuit\n",
     "\n",
     "## Lookup Tables\n",

book/_build/html/_sources/python_syntax.md

@@ -0,0 +1,157 @@
+# Python syntax
+
+## Constraint builder
+
+One of the most important parts of defining a circuit is the constraints. The basis for writing constraints are arithmetic operations with signals. You use the operators `*`, `+` and `-` with numbers and signals. For example:
+
+`a + 1 * b`
+
+When you need to do a rotation on a signal you can use the operators `.next()`, `prev()` and or `.rot(n)`.  For example:
+
+`a + 1 * b.next()`
+
+ There are several helper functions to define constraints:
+ + `cb_and([a1 ... an])`: And operator
+ + `cb_or([a1 ... an])`: Or operator
+ + `xor(a, b)`: Xor operator
+ + `eq(a, b)`: Arithmetic equality.
+ + `select(selector, when_true, when_false)`: trinary operator
+ + `when(selector, when_true)`:  Logical imply.
+ + `unless(selector, when_false)`: Logical imply when !selector.
+ + `cb_not(a)`: Not operator.
+ + isz(a): Equal to zero.
+ + `if_next_step(step_type, a)`: If next step is step_type, implies a.
+ + `next_step_must_be(step_type)`: Enforces next step must be step_type.
+ + `next_step_must_not_be(step_type)`: Enforces next step must not be step_type.
+
+In the current version of chiquito these operator cannot be combined arbitrarily, there is a solution in the works. For example `cb_and` cannot have operands that are `eq`.
+
+## Defining a step
+
+A chiquito circuit is made of steps, this is how we define steps:
+
+```python=
+class AStep(StepType):
+	def setup(self):
+		# setup: rules about a valid step
+	def wg(self, a, b, c):
+		# witness generation: set data for a step instance
+```
+
+For the setup we need to define constraints that define which step witness is valid and also define the internal signals. For example:
+
+```python=
+class AStep(StepType):
+	def setup(self):
+		self.c = self.internal("c")
+```
+
+To access shared signals we can do it with `self.circuit.signal_identifier`.
+
+For the constraints that we can use the method `constr`. For example:
+
+```python=
+class AStep(StepType):
+	def setup(self):
+		self.constr(eq(self.circuit.a, self.circuit.b * 3))
+		self.constr(when(self.circuit.a, eq(self.circuit.b, self.c))
+
+# ...
+```
+
+The first constraint means that `a` must be equal to `b times 3`. The second that when `a` value is `1` then `b` must be equal to `c`.
+
+When you have a rotation you should use the method `transition`. For example:
+
+```python=
+class AStep(StepType):
+	def setup(self):
+		self.transition(eq(self.circuit.a, self.circuit.b.next() * 3))
+		self.transition(when(self.circuit.a, eq(self.circuit.b.next(), self.c))
+
+# ...
+```
+
+
+For the data of one step instance in the `wg` method we must use the `assign` method to assign all signals.
+
+```python=
+class AStep(StepType):
+	def wg(self, a_val, b_val):
+		self.assign(self.circuit.a, a_val)
+		self.assign(self.circuit.b, b_val)
+		self.assign(self.c, a_val + b_val)
+
+# ...
+```
+
+The method `wg` can have any parameters, and do any computation to calculate the assignations. But signals cannot be rotated for assignation, you can only assign the current step.
+
+## Defining the circuit
+
+To put everything together we define the circuit, also with two methods.
+
+```python=
+class ACircuit(Circuit):
+	def setup(self):
+		# Define shared signals and step types used, number of total steps plus more setup configuration.
+	def trace(self, arg1, arg2):
+		# Define algorithm to create the trace from the input.
+```
+
+For the setup we defined shared signals, step types and number of steps in the trace. For example:
+
+```python=
+class ACircuit(Circuit):
+	def setup(self):
+		# shared signals
+		self.a = self.forward("a")
+		self.b = self.forward("b")
+		self.n = self.forward("n")
+
+		# step types
+		self.a_step = self.step_type(AStep(self, "a_step"))
+		self.b_step = self.step_type(BStep(self, "b_step"))
+		self.c_step = self.step_type(CStep(self, "c_step"))
+
+		# number of trace steps
+		self.pragma_num_steps(10)
+
+# ...
+```
+
+There are many optional things that you can also configure in the circuit setup:
+
+```python=
+class ACircuit(Circuit):
+	def setup(self):
+		self.pragma_first_step(self.a_step)
+		self.pragma_last_step(self.b_step)
+
+		self.expose(self.b, Last())
+		self.expose(self.n, Last())
+
+# ... 
+```
+
+Then, we should define `trace`, this method add step instances or trace steps to create a particular trace. The most important method is `add()`, the first parameter is a step type, and the rest are the parameters to the step type `wg` method. This method adds a trace step
+
+For example:
+
+```python=
+class ACircuit(Circuit):
+	def trace(self, n):
+		self.add(self.a_step, 1, 1, n)
+		a = 1
+		b = 2
+		for i in range(1, n):
+			self.add(self.b_step, a, b, n)
+			prev_a = a
+			a = b
+			b += prev_a
+		
+		while self.needs_padding():
+			self.add(self.b_step, a, b, n)
+
+# ... 
+```