Skip to content

Commit

Permalink
huuuge refactor, more content, better tests
Browse files Browse the repository at this point in the history
  • Loading branch information
erhant committed Feb 4, 2024
1 parent 2235f23 commit a797188
Show file tree
Hide file tree
Showing 36 changed files with 2,677 additions and 1,184 deletions.
3 changes: 2 additions & 1 deletion .gitignore
Original file line number Diff line number Diff line change
@@ -1,4 +1,5 @@
node_modules
circuits/test
circuits/main
build
build
.yarn
3 changes: 0 additions & 3 deletions .prettierrc

This file was deleted.

8 changes: 7 additions & 1 deletion .vscode/settings.json
Original file line number Diff line number Diff line change
@@ -1,11 +1,17 @@
{
// https://raw.githubusercontent.com/PKief/vscode-material-icon-theme/main/images/fileIcons.png
"material-icon-theme.files.associations": {
"*.circom": "Verilog"
},
// https://raw.githubusercontent.com/PKief/vscode-material-icon-theme/main/images/folderIcons.png
"material-icon-theme.folders.associations": {
"circuits": "App",
"inputs": "Json",
"book": "Docs"
"book": "Docs",
"arrays": "Constant",
"basics": "Resolver",
"control-flow": "Routes",
"comparators": "Benchmark",
"bits": "Base"
}
}
1 change: 1 addition & 0 deletions .yarnrc.yml
Original file line number Diff line number Diff line change
@@ -0,0 +1 @@
nodeLinker: node-modules
File renamed without changes.
12 changes: 7 additions & 5 deletions README.md
Original file line number Diff line number Diff line change
@@ -1,9 +1,9 @@
<p align="center">
<h1 align="center">
<kbd>circom101</kbd>
Circom101
</h1>
<p align="center">
<i>Deep dive into Circom circuits like never before.</i>
<i>Circom circuit implementations with in-depth explanations.</i>
</p>
</p>

Expand All @@ -24,10 +24,10 @@
Install packages with:

```sh
yarn
yarn install
```

### Book
## Book

We use `mdbook` to create the book, see the [book](./book/) folder. Serve the book locally with:

Expand All @@ -36,10 +36,12 @@ yarn book
yarn book:build # without serving
```

## Testing
## Tests

Run circuit tests with:

```sh
yarn test
```

The tests make use of [Circomkit](https://github.com/erhant/circomkit).
28 changes: 18 additions & 10 deletions book/src/README.md
Original file line number Diff line number Diff line change
@@ -1,17 +1,25 @@
# Circom 101
# About this Book

Zero-knowledge proofs are a fascinating area of cryptography that allows parties to prove a statement without revealing any extra information about it; just proving that statement alone. In other words, zero-knowledge proofs can demonstrate that something is true, without revealing what makes that "something" true.
Zero-knowledge cryptography is a fascinating area, where a party can prove a statement without revealing any extra information about it; proving that something is true without revealing what makes that "something" true.

There are great resources online to learn more about them, to name a few:
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.

- todo
- todo
- todo
## Resources

---
There are many resources about Circom & ZK out there, to list a few:

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.
- [Official Circom Docs](https://docs.circom.io/) by [@iden3](https://twitter.com/identhree).
- [Circomlib](https://github.com/iden3/circomlib/) is a collection of common circuits, by [@iden3](https://twitter.com/identhree).
- [Circom Tutorial](https://www.rareskills.io/post/circom-tutorial) by [RareSkills](https://twitter.com/RareSkills_io).
- [zkJargon Decoder](https://nmohnblatt.github.io/zk-jargon-decoder/foreword.html) by [@nico_mnbl](https://twitter.com/nico_mnbl).
- [BattleZips](https://battlezips.gitbook.io/battlezips/) by [BattleZips](https://github.com/BattleZips)

## Tests

We provide tests via [Circomkit](https://github.com/erhant/circomkit) that demonstrate each circuit described here. In the repository, you can run:

Although there are quite a lot of implementations of Circom online, I feel like there is a lack of documentation and explanation. For this reason, I have created this book, where we examine circuits and explain how they do what they do.
```sh
yarn test
```

> Throughout this book, we always try to make use of `in` and `out` signal naming convention if the circuit permits.
to run all tests.
5 changes: 2 additions & 3 deletions book/src/SUMMARY.md
Original file line number Diff line number Diff line change
Expand Up @@ -13,9 +13,8 @@
- [Alias Check](./comparators/alias-check.md)
- [Sign Check](./comparators/sign-check.md)
- [Range Check](./comparators/range-check.md)
- [Branching](./branching/README.md)
- [If-Then-Else](./branching/if-then-else.md)
- [Multiplexing](./branching/mux.md)
- [Control Flow](./control-flow/README.md)
- [Multiplexing](./control-flow/mux.md)
- [Arrays](./arrays/README.md)
- [Sorting](./arrays/sorting.md)
- [Merkle Trees](./merkle-trees/README.md)
Expand Down
2 changes: 1 addition & 1 deletion book/src/basics/magic.md
Original file line number Diff line number Diff line change
@@ -1,3 +1,3 @@
# Magic Square
# `MagicSquare`

TODO
18 changes: 18 additions & 0 deletions book/src/basics/multiplier.md
Original file line number Diff line number Diff line change
Expand Up @@ -45,3 +45,21 @@ There is really not much more to talk about in this circuit. It is simply a grea
> ```
>
> Then, within the `Multiplier` you can use the `Mul` gate for each multiplication.
## Soundness
Imagine that you would like to use the circuit above to prove that you know the prime factors $p_1, p_2, \ldots, p_n$ for some number:
$$
k = \prod_{i=1}^{n}p_i
$$
Would it be okay to use the circuit above as given, with `out` as the only public signal?
If you think about this for a while, you will realize that the circuit does not care if a factor is 1 or not! Meaning that one can provide the same proof just by providing an array `[k, 1, ..., 1]` since:
$$
k = \prod_{i=1}^{n}p_i = k \times \prod_{i=2}^{n}1
$$
The circuit author is responsible from checking these edge-cases, and writing the necessary constrains to prevent such soundness errors.
35 changes: 33 additions & 2 deletions book/src/bits/README.md
Original file line number Diff line number Diff line change
Expand Up @@ -12,7 +12,7 @@ template AssertBit() {
}
```

To assert that a given number $n$ is bit (i.e. 0 or 1) you only have to check that $n^2 = n$, as there are only two numbers whose square equals to itself: 0 and 1.
To assert that a given number $n$ is bit (i.e. 0 or 1) you only have to check that $n^2 = n$, as there are only two numbers whose square equals to itself: 0 and 1. This expression is equivalent to $n \times (n - 1) = 0$, which is how we've written in the circuit above.

Normally people assert that a signal is bit without the template above; instead, it is preferred to do this inline where it is needed. Well, nothing really stops you from using templates.

Expand Down Expand Up @@ -49,6 +49,37 @@ The important constraint in this template is that `out` when converted back to d
lc = out[0]*1 + out[1]*2 + out[2]*4 + ... + out[n-1]*2^(n-2)
```

Thankfully, this is a quadratic constraint and we can simply check if `lc === in` to ensure the bitwise representation is correct.
Thankfully, this entire equality is a quadratic constraint and we can simply check if `lc === in` to ensure the bitwise representation is correct.

> **Exercise**: How would you modify `Num2Bits` above to obtain a template like `AssertBits(n)` that ensures a number can be represented by `n` bits?

## `Bits2Num`

```cs
template Bits2Num(n) {
assert(n < 254);
signal input in[n];
signal output out;

var lc = 0;
var bit_value = 1;
for (var i = 0; i < n; i++) {
AssertBit()(in[i]);

lc += in[i] * bit_value;
bit_value <<= 1;
}

out <== lc;
}
```

If we can convert from an `n`-bit number to its binary representation, surely we should be able to convert from the binary representation with `n`-bits to the number itself. We do that with `Bits2Num`. This operation is rather straightforward, we just need to compute:

$$
n = \sum_{i = 0}^{n-1}\texttt{in}_i2^i
$$

We use `bit_value` to keep track of $2^i$, and this entire sum expression is stored within the `lc` (linear combination). In the end, we constrain the output signal to be equal to this expression.

> Note that for both `Num2Bits` and `Bits2Num`, the most-significant bit is the last element of the array, and least-significant bit is the first element of the array. To demonstrate, consider the 4-bit number 11, normally shown as $(1011)_2$ in maths. However, in these circuits we store the array `[1, 1, 0, 1]`, in the opposite order!
103 changes: 102 additions & 1 deletion book/src/bits/logic-gates.md
Original file line number Diff line number Diff line change
@@ -1,3 +1,104 @@
# Logic Gates

TODO
It is often required to do some logical operations like `AND`, `OR`, `NOT` and `XOR` within a circuit. For the circuits within this chapter, we can assume that the inputs are asserted to be bits, i.e. they are either 0 or 1.

## `AND`

```cs
template AND() {
signal input in[2];
signal output out;

out <== in[0]*in[1];
}
```

The logic table of `AND` is as follows:

| $\land$ | 0 | 1 |
| ------- | --- | --- |
| 0 | 0 | 0 |
| 1 | 0 | 1 |

This can be achieved by simply multiplying the two inputs!

## `OR`

```cs
template OR() {
signal input in[2];
signal output out;

out <== in[0] + in[1] - in[0]*in[1];
}
```

The logic table of `OR` is as follows:

| $\lor$ | 0 | 1 |
| ------ | --- | --- |
| 0 | 0 | 1 |
| 1 | 1 | 1 |

We _almost_ achieve the result by adding the two numbers, except that we get 2 when both are 1. Well, `AND` is only 1 when both numbers are 1, so we subtract it from the result to solve that issue.

What we have is equivalent to `in[0] + in[1] - AND(in)`.

## `XOR`

```cs
template XOR() {
signal input in[2];
signal output out;

out <== in[0] + in[1] - 2*in[0]*in[1];
}
```

The logic table of `XOR` is as follows:

| $\oplus$ | 0 | 1 |
| -------- | --- | --- |
| 0 | 0 | 1 |
| 1 | 1 | 0 |

We can use the same trick for `OR`, just once more, to make the `1 + 1` turn to a zero. What we have is equivalent to `in[0] + in[1] - 2 * AND(in)`.

## `NOT`

```cs
template NOT() {
signal input in;
signal output out;

out <== 1 - in;
}
```

A `NOT` gate maps 0 to 1, and 1 to 0. We can achieve this by simply subtracting the signal from 1. Since $1 - 0 = 1$ and $1 - 1 = 0$.

## `NAND`

```cs
template NAND() {
signal input in[2];
signal output out;

out <== 1 - in[0]*in[1];
}
```

`NAND` is equivalent to `NOT(AND(in))`, giving us the circuit above.

## `NOR`

```cs
template NOR() {
signal input in[2];
signal output out;

out <== 1 - (in[0] + in[1] - in[0]*in[1]);
}
```

`NOR` is equivalent to `NOT(OR(in))`, giving us the circuit above.
3 changes: 0 additions & 3 deletions book/src/branching/README.md

This file was deleted.

3 changes: 0 additions & 3 deletions book/src/branching/if-then-else.md

This file was deleted.

88 changes: 88 additions & 0 deletions book/src/control-flow/README.md
Original file line number Diff line number Diff line change
@@ -0,0 +1,88 @@
# Control Flow

In the world of arithmetic circuits, control flow is a bit different than what most developers are used to. In normal programming, only one of the branches are executed:

```c
if (cond) {
foo(); // only if cond == true
} else {
bar(); // only if cond == false
}
```

That is not how things work in our circuits! Instead, both branches are executed but only one of them is "returned".

To understand why, first remind yourself that we are ALWAYS working with integers in our circuits. Both `foo()` and `bar()` will return an integer, and `cond` is either 0 or 1. The trick is to combine these results with `cond` and `NOT(cond)` in a simple sum expression:

```c
cond*foo() + NOT(cond)*bar();
```
Opening this up, we have:
```c
cond*foo() + (1-cond)*bar();
```

In fact, we can use one multiplication instead of two, using the following form:

```c
cond*(foo() - bar()) + bar();
```

## `IfElse`

```cs
template IfElse() {
signal input cond;
signal input ifTrue;
signal input ifFalse;
signal output out;

out <== cond * (ifTrue - ifFalse) + ifFalse;
}
```

Following our description above, an `if-else` is defined by the given circuit. Remember that both `ifTrue` and `ifFalse` signals are computed, regardless of the condition, but only one of them is returned.

### Conditional Constraints

In your application, there may be cases where `ifTrue` and `ifFalse` can't be valid at the same time, due to some condition; `ifTrue` might constrain a signal to be 0 but `ifFalse` might constrain that same signal to something else.

In these cases, we may add an auxillary signal which can enable/disable a constraint check. As an example, imagine the following template that constraints a signal to be 5:

```cs
template IsFive() {
signal input in;

in - 5 === 0;
}
```

We can add an auxillary `isEnabled` signal that is either 0 or 1, and disable this circuit when `isEnabled = 0` as follows:

```cs
template IsFive() {
signal input in;
signal input isEnabled;

isEnabled * (in - 5) === 0;
}
```

If `isEnabled = 1` both circuits are equivalent, but if `isEnabled = 0` this circuit will always have `0 === 0` regardless of the `in` signal.

## `Switch`

```cs
template Switch() {
signal input cond;
signal input in[2];
signal output out[2];

out[0] <== cond * (in[1] - in[0]) + in[0];
out[1] <== cond * (in[0] - in[1]) + in[1];
}
```

It is often useful to switch the places of two signals based on a condition, which can be achieved with two `IfElse` lines together.
File renamed without changes.
Loading

0 comments on commit a797188

Please sign in to comment.