more docs, arrays, more todos

.vscode/settings.json

@@ -12,6 +12,8 @@
     "basics": "Resolver",
     "control-flow": "Routes",
     "comparators": "Benchmark",
-    "bits": "Base"
+    "bits": "Base",
+    "merkle-trees": "Context",
+    "hashing": "App"
   }
 }

book/src/README.md

@@ -4,6 +4,17 @@ Zero-knowledge cryptography is a fascinating area, where a party can prove a sta
 
 Circom is a hardware description language (HDL) specifically designed for creating zero-knowledge proofs. It enables developers to create arithmetic circuits, which are then used to generate proofs that demonstrate a certain statement is true, without revealing any additional information about the inputs used to make that statement. Circom has opened up new possibilities for creating privacy-preserving applications, such as digital identities, voting systems, and financial transactions, where proving the validity of a statement is necessary, but keeping the underlying data private is critical.
 
+## Organization
+
+The book is organized as follows:
+
+- [Preliminary](./preliminary/README.md) has some preliminary theory for those who are interested in it. It is not 100% required to know the theory & math behind the relevant cryptography areas to write good Circom code; however, it could allow the reader to:
+  - Write more efficient code by utilizing mathematical tricks.
+  - Understand certain low-level code.
+  - Consider more edge cases & write more secure code.
+- [Basics](./basics/README.md) has several hello-world level Circom programs, to get the reader started. The reader is free to skip this part & come back later, however it is strongly recommended to understand how the programs here work.
+- [Bits](./bits/README.md) describe methods related to bits: signals with value `0` or `1`.
+
 ## Resources
 
 There are many resources about Circom & ZK out there, to list a few:

book/src/SUMMARY.md

@@ -1,7 +1,9 @@
 # Summary
 
 - [Introduction](./README.md)
-
+- [Preliminary](./preliminary/README.md)
+  - [Group Theory](./preliminary/group-theory.md)
+  - [Commitments](./preliminary/commitments.md)
 - [Basics](./basics/README.md)
   - [Multiplier](./basics/multiplier.md)
   - [Fibonacci](./basics/fibonacci.md)
@@ -16,7 +18,11 @@
 - [Control Flow](./control-flow/README.md)
   - [Multiplexing](./control-flow/mux.md)
 - [Arrays](./arrays/README.md)
+  - [Distinct](./arrays/distinct.md)
   - [Sorting](./arrays/sorting.md)
+- [Hashing](./hashing/README.md)
+  - [Poseidon](./hashing/poseidon.md)
+  - [MiMC](./hashing/mimc.md)
 - [Merkle Trees](./merkle-trees/README.md)
   - [Dense Merkle Tree](./merkle-trees/dense.md)
   - [Sparse Merkle Tree](./merkle-trees/smt.md)

book/src/arrays/README.md

@@ -1,3 +1,112 @@
 # Arrays
 
-TODO
+Circom arrays are a different kind of beast. The main reason is that in Circom, array operations must be **known** at compile-time. What do we mean by this:
+
+- Array sizes are fixed, e.g. you can't define an array based on the user input after compiling the circuit.
+- Array indexing should be known at compile time, e.g. you can't ask a user for index `i` and return `arr[i]` like you _normally_ do.
+
+Before we get to the problematic unknown-at-compile-time stuff, let's quickly recap the known-time array operations. An array of signals (with fixed size) is defined with:
+
+```cs
+signal arr[N];
+```
+
+> Arrays can be multi-dimensional too:
+>
+> ```cs
+> signal arr[N][M];
+> ```
+
+With that, we can read & write to this array as with the usual notation in programming:
+
+```cs
+// for some compile-time known `i`:
+arr[i] <== foo;
+bar <== arr[i];
+```
+
+So now, what if we want to read or write to an index unknown at compile time?
+
+## `ArrayRead`
+
+```cs
+template ArrayRead(n) {
+  signal input in[n];
+  signal input index;
+  signal output out;
+
+  signal intermediate[n];
+  for (var i = 0; i < n; i++) {
+    var isIndex = IsEqual()([index, i]);
+    intermediate[i] <== isIndex * in[i];
+  }
+
+  out <== Sum(n)(intermediate);
+}
+```
+
+To read an unknown index, we could instead read ALL signals (which is an operation known-at-compile-time) and then return a linear combination of them, with each value multiplied with an equality-check with our index.
+
+```py
+arr_i =
+  A[0]   * (i == 0)
++ A[1]   * (i == 1)
++ ...
++ A[n-1] * (i == n-1)
+```
+
+This way, our array accesses are known at compile-time but we are still able to get the value at index `i`.
+
+```py
+arr_i =
+  A[0]   * 0
++ A[1]   * 0
++ ...
++ A[i]   * 1
++ ...
++ A[n-1] * 0
+= A[i]
+```
+
+Note that this will incur some contraint costs.
+
+> The `Sum(n)` here is rather straight-forward:
+>
+> ```cs
+> template Sum(n) {
+>   signal input in[n];
+>   signal output out;
+>
+>   var lc = 0;
+>   for (var i = 0; i < n; i++) {
+>     lc += in[i];
+>   }
+>   out <== lc;
+> }
+> ```
+>
+> `lc` here means "linear combination" and its just a variable that stores:
+>
+> ```py
+> lc = in[0] + in[1] + ... + in[n-1]
+> ```
+
+## `ArrayWrite`
+
+```cs
+template ArrayWrite(n) {
+  signal input in[n];
+  signal input index;
+  signal input value;
+  signal output out[n];
+
+  for (var i = 0; i < n; i++) {
+    var isIndex = IsEqual()([index, i]);
+    out[i] <== IfElse()(isIndex, value, in[i]);
+  }
+}
+```
+
+Writing to an unknown-index works in a similar way to reading one. The idea is to simply copy the input signal array to an output array, but only at the index `i` we will use our new value instead of the existing one at `in[i]`.
+
+We had defined the `IfElse` template at [control-flow](../control-flow/) section.

book/src/arrays/distinct.md

@@ -0,0 +1,53 @@
+# Distinct
+
+We may often require to check if an array has non-repeating values, also known as unique values or distinct values. A common example of this would be for a Sudoku circuit, e.g. you would like to assert that all values in a row are in range [1, 9] and that the row has distinct values.
+
+## `AssertDistinct`
+
+```cs
+template AssertDistinct(n) {
+  signal input in[n];
+
+  for (var i = 0; i < n-1; i++){
+    for (var j = i+1; j < n; j++){
+      var eq = IsEqual()([in[i], in[j]]);
+      eq === 0;
+    }
+  }
+}
+```
+
+To assert that an array has distinct values, we can loop over the values and check each unique pair to be non-equal using the `IsEqual` template. For example, in an array of 4 elements this corresponds to the following checks:
+
+```cs
+IsEqual()([in[0], in[1]]) === 0
+IsEqual()([in[0], in[2]]) === 0
+IsEqual()([in[0], in[3]]) === 0
+IsEqual()([in[1], in[2]]) === 0
+IsEqual()([in[1], in[3]]) === 0
+IsEqual()([in[2], in[3]]) === 0
+```
+
+## `IsDistinct`
+
+```cs
+template IsDistinct(n) {
+  signal input in[n];
+  signal output out;
+
+  var acc = 0;
+  for (var i = 0; i < n-1; i++){
+    for (var j = i+1; j < n; j++){
+      var eq = IsEqual()([in[i], in[j]]);
+      acc += eq;
+    }
+  }
+
+  signal outs <== acc;
+  out <== IsZero()(outs);
+}
+```
+
+If you would like to return a bit-signal based on whether an array has all distinct values or not, you can slightly modify the `AssertDistinct` template to obtain that functionality. Instead of asserting each `IsZero` check, we accumulate them and then return whether that final sum is equal to zero or not.
+
+> Note that technically it is possible for `acc` to overflow and wrap back to 0, however, that is unlikely to happen given how large the prime-field is and we would need that many components to be able to overflow using 1+1+...+1 only.

book/src/comparators/range-check.md

@@ -1,4 +1,10 @@
-# `AssertInRange`
+# Range Check
+
+A range-check is a common utility, asserting that a number is in some range `[MIN, MAX]`. It is important to keep in mind that you can make use of bit-decompositions to check for range `[0, 2^n)`, which would be done by simply checking if a number is representable with `n`-bits.
+
+> Lookup-tables are often used for range checks in other zkDSLs, but I dont yet know how to use them in Circom.
+
+## `AssertInRange`
 
 ```cs
 template AssertInRange(MIN, MAX) {
@@ -15,7 +21,7 @@ template AssertInRange(MIN, MAX) {
 }
 ```
 
-A range-check is a common utility, asserting that a number is in some range `[MIN, MAX]`. Above is one way of doing that. Our approach here is to check:
+Above is one way of doing a generic range check. Our approach here is to check:
 
 - `in - MIN` is a b-bit value
 - `in + 2^b - 1 - MAX` is a b-bit value

book/src/hashing/README.md

@@ -0,0 +1 @@
+# Hashing

book/src/hashing/mimc.md

@@ -0,0 +1 @@
+# MiMC

book/src/hashing/poseidon.md

@@ -0,0 +1 @@
+# Poseidon

book/src/merkle-trees/README.md

@@ -1,3 +1,3 @@
 # Merkle Trees
 
-TODO
+If you have been in the world of crypto for a while, it is highly likely that you have heard the term Merkle Tree. A Merkle Tree is a cryptographic commitment scheme.

book/src/preliminary/README.md

@@ -0,0 +1 @@
+# Preliminaries

book/src/preliminary/commitments.md

@@ -0,0 +1,28 @@
+# Commitments
+
+In a commitment scheme, Alice can commit to a value $x$ to obtain a commitment $\boxed{x}$. At some point later, Bob would like for Alice to reveal the committed value behind $\boxed{x}$, and show that indeed Alice was the one that had committed in the first place.
+
+A rough informal sketch of this interaction can be shown as:
+
+```mermaid
+sequenceDiagram
+	actor A as Alice
+	actor B as Bob
+
+	note over A: Alice commits to x
+  note over A: [x] := x
+  A ->> B: [x]
+
+  note over A, B: sometime later
+  B ->> A: show me!
+  A ->> B: x
+
+  note over B: im convinced.
+```
+
+A cryptographic commitment scheme has two notable properties:
+
+- **Hiding**: A commitment $\boxed{x}$ should reveal nothing about the underlying $x$.
+- **Binding**: A commitment $\boxed{x}$, should only be revealed to $x$, i.e. for some $x' \ne x$ we shouldn't be able to compute a commitment $\boxed{x'} = \boxed{x}$.
+
+TODO: more needed

book/src/preliminary/group-theory.md

@@ -0,0 +1,3 @@
+# Group Theory
+
+TODO

circuits/arrays/distinct.circom

@@ -0,0 +1,52 @@
+pragma circom 2.1.0;
+
+include "../comparators/index.circom";
+
+// Asserts that values in an array are unique.
+//
+// Parameters:
+// - n: length of `in`
+//
+// Inputs:
+// - in: an array of `n` values
+template AssertDistinct(n) {
+  signal input in[n];
+
+  for (var i = 0; i < n-1; i++){
+    for (var j = i+1; j < n; j++){
+      var eq = IsEqual()([in[i], in[j]]);
+      eq === 0;
+    }
+  }
+}
+
+
+// Returns 1 if all values are distinct in a given array.
+//
+// Parameters:
+// - n: length of `in`
+//
+// Inputs:
+// - in: an array of `n` values
+//
+// Outputs:
+// - out: 1 if all values are distinct
+template IsDistinct(n) {
+  signal input in[n];
+  signal output out;
+
+  var acc = 0;
+  for (var i = 0; i < n-1; i++){
+    for (var j = i+1; j < n; j++){
+      var eq = IsEqual()([in[i], in[j]]);
+      acc += eq;
+    }
+  }
+
+  // note that technically it is possible for `acc` to overflow
+  // and wrap back to 0, however, that is unlikely to happen given
+  // how large the prime-field is and we would need that many components
+  // to be able to overflow
+  signal outs <== acc;
+  out <== IsZero()(outs);
+}

circuits/arrays/index.circom

@@ -15,7 +15,6 @@ include "../control-flow/index.circom";
 //
 // Outputs:
 // - `out`: value at `in[index]`
-//
 template ArrayRead(n) {
   signal input in[n];
   signal input index;
@@ -42,7 +41,6 @@ template ArrayRead(n) {
 //
 // Outputs:
 // - `out`: array
-//
 template ArrayWrite(n) {
   signal input in[n];
   signal input index;
@@ -65,7 +63,6 @@ template ArrayWrite(n) {
 //
 // Outputs:
 // - `out`: sum of all values in `in`
-//
 template Sum(n) {
   signal input in[n];
   signal output out;
@@ -76,22 +73,3 @@ template Sum(n) {
   }
   out <== lc;
 }
-
-// Asserts that values in an array are unique.
-//
-// Parameters:
-// - `n`: length of `in`
-//
-// Inputs:
-// - `in`: an array of `n` values
-//
-template AssertDistinct(n) {
-  signal input in[n];
-
-  for (var i = 0; i < n-1; i++){
-    for (var j = i+1; j < n; j++){
-      var eq = IsEqual()([in[i], in[j]]);
-      eq === 0;
-    }
-  }
-}