Skip to content

Commit

Permalink
fix images for dark mode
Browse files Browse the repository at this point in the history
  • Loading branch information
rot256 committed Nov 13, 2024
1 parent 48ee9d0 commit ac7bc45
Show file tree
Hide file tree
Showing 11 changed files with 298 additions and 161 deletions.
12 changes: 8 additions & 4 deletions book.toml
Original file line number Diff line number Diff line change
Expand Up @@ -12,16 +12,20 @@ extra-watch-dirs = ["halo-hero"]

[preprocessor.admonish]
command = "mdbook-admonish"
assets_version = "2.0.0" # do not edit: managed by `mdbook-admonish install`
assets_version = "3.0.2" # do not edit: managed by `mdbook-admonish install`


[[preprocessor.admonish.custom]]
[preprocessor.admonish.directive.custom.exercise]
directive = "exercise"
icon = "./rocket.svg"
# magenta
color = "#FFA62B"
aliases = ["ex"]

[preprocessor.admonish.directive.builtin.tip]
directive = "hint"
icon = "./brain-circuit.svg"
color = "#4CAF50"
collapsible = true

[output]

[output.html]
Expand Down
186 changes: 91 additions & 95 deletions mdbook-admonish.css

Large diffs are not rendered by default.

51 changes: 17 additions & 34 deletions src/bonus-circuit-architecture/index.md
Original file line number Diff line number Diff line change
@@ -1,15 +1,6 @@
# Bonus: Circuit Architecture

<svg width="100%" height="400" xmlns="http://www.w3.org/2000/svg">
<circle cx="400" cy="150" r="80" fill="#FFD700" />
<rect x="100" y="200" width="300" height="150" fill="#4169E1" transform="rotate(-15)" />
<polygon points="600,100 700,150 600,200 500,150" fill="#FF4500" />
<line x1="200" y1="50" x2="600" y2="350" stroke="#000000" stroke-width="5" />
<ellipse cx="640" cy="280" rx="120" ry="30" fill="#32CD32" transform="rotate(30)" />
<path d="M300 300 Q 400 350 500 300" stroke="#FF1493" stroke-width="8" fill="none" />
<circle cx="200" cy="100" r="20" fill="#9932CC" />
<circle cx="600" cy="300" r="25" fill="#FF6347" />
</svg>
<img src="./top-light-themed.svg" width="100%">

We have seen a number of different techniques.

Expand All @@ -35,15 +26,13 @@ However, there is a better way: this can be achieved with only one multi-scalar
Architect a circuit which achieves this.
```

<details>
<summary>Hint 1</summary>
```admonish hint
Use a challenge
</details>
```

<details>
<summary>Hint 2</summary>
```admonish hint
Exploit the linearity of the inner product.
</details>
```


```admonish exercise
Expand All @@ -68,37 +57,31 @@ Help design chips for these operations.
1. How could you combine this with our regular expression matching circuit?
```

<details>
<summary>Hint 1</summary>
```admonish hint
Use a column to store the strings.
</details>
```

<details>
<summary>Hint 2</summary>
```admonish hint
Use a challenge to compute fingerprints of each string.
Add a gate to ensure that the fingerprints are correctly computed.
</details>
```

<details>
<summary>Hint 3</summary>
```admonish hint
Compute on the fingerprints to check that the concatenation is correct.
</details>
```

<details>
<summary>Hint 4</summary>
```admonish hint
Add a column containing the length / index of every character in the string.
</details>
```

<details>
<summary>Hint 5</summary>
```admonish hint
Decompose the string into three parts: the prefix, the substring, and the suffix.
</details>
```

<details>
<summary>Hint 6</summary>
```admonish hint
Use the concatenation gate to extract the substring.
</details>
```

```admonish exercise
**Exercise:** Battle Ships
Expand Down
10 changes: 10 additions & 0 deletions src/bonus-circuit-architecture/top-dark-themed.svg
Loading
Sorry, something went wrong. Reload?
Sorry, we cannot display this file.
Sorry, this file is invalid so it cannot be displayed.
10 changes: 10 additions & 0 deletions src/bonus-circuit-architecture/top-light-themed.svg
Loading
Sorry, something went wrong. Reload?
Sorry, we cannot display this file.
Sorry, this file is invalid so it cannot be displayed.
30 changes: 19 additions & 11 deletions src/challenges/index.md
Original file line number Diff line number Diff line change
Expand Up @@ -4,8 +4,9 @@

*"And what is the use of a book," thought Alice, "without pictures or conversations?"*

Because of how PlonK works, it is trivial to add multiple "rounds of interaction" to a proof
in which the prover commits to some values, the verifier sends a challenge and the prover commits to some more values, etc.
Because of how PlonK works, it is trivial to add multiple "rounds of interaction"
in which the prover commits to some values,
the verifier sends a challenge and the prover commits to some more values, etc.
This back and forth can be repeated essentially for as many rounds as you like,
Halo2 (as implemented) supports three such "phases" of interaction.

Expand All @@ -14,10 +15,10 @@ the prover and verifier passing the spreadsheet back and forth while taking turn
first the prover fills out some columns in the spreadsheet, then the verifier fills out some columns,
then the prover fills out some more columns, etc.


## Configuration of Challenges

In Halo2, the "challenges" are used by allocating a `Challenge` which acts very similarly to the columns we have seen so far:
In Halo2, the "challenges" are used by allocating a `Challenge`
which acts very similarly to the columns we have seen so far:
You can think of `Challenge` as a column where *every row contains the same random challenge value*.
They are allocated with a "Phase" using `challenge_usable_after`:

Expand All @@ -28,7 +29,8 @@ They are allocated with a "Phase" using `challenge_usable_after`:
In the example above, we are asking for a challenge that is usable *after the first phase* of the interaction.
The *first phase* is the "default": it is the implicit phase that we have been using to allocate all the `Advice` columns so far:
it is the first time the prover gets to fill in values in the spreadsheet.
This means that only after assigning values to these `Advice` columns, does the prover learn the challenge value (the random value assigned to `alpha`):
This means that only after assigning values to these `Advice` columns,
does the prover learn the challenge value (the random value assigned to `alpha`):
so the first phase values cannot depend on the challenge `alpha` in our example.

```admonish question
Expand All @@ -37,9 +39,11 @@ Stop and think.
Does it make sense to have other column types, besides `Advice`, in any other phases?
```

Before we continue with the challenges, a natural question is: how do we assign `Advice` columns *after* the challenge?
Before we continue with the challenges, a natural question is:
how do we assign `Advice` columns *after* the challenge?
In other words, how do we allow the prover to "respond" to the challenge `alpha`?
It's straightforward: you simply use `meta.advice_column_in(SecondPhase)` instead of `meta.advice_column()` when allocating the column.
It's straightforward: you simply use `meta.advice_column_in(SecondPhase)`
instead of `meta.advice_column()` when allocating the column.

```rust,noplaypen
{{#include ../../halo-hero/examples/challenges.rs:phase2_alloc}}
Expand Down Expand Up @@ -75,7 +79,8 @@ So we need to do:

- A pass over the circuit, assigning all the `FirstPhase` advice columns.
- Obtain the first challenge value (`alpha` in our example).
- Then do another pass over the circuit, assigning all the `SecondPhase` advice columns which might depend on the challenge value.
- Then do another pass over the circuit, assigning all the `SecondPhase`
advice columns which might depend on the challenge value.
- Obtain the second challenge value.
- etc.

Expand All @@ -89,7 +94,8 @@ if the challenge is available during this pass the value will be `Value::known`
let chal = layouter.get_challenge(self.challenge);
```

This allows us to compute `Value`s for the second phase: these will be `Value::unknown` during the first pass and `Value::known` during the second pass.
This allows us to compute `Value`s for the second phase:
these will be `Value::unknown` during the first pass and `Value::known` during the second pass.
For instance:

```rust
Expand Down Expand Up @@ -122,7 +128,8 @@ Create a circuit which verifies Sudoku solutions.
```

```admonish hint
To verify that every row/column/diagonal/3x3 square must contain exactly one of each number 1-9, you can use the following trick:
To verify that every row/column/diagonal/3x3 square must contain
exactly one of each number 1-9, you can use the following trick:
Use the fact that for a set \\( C \\) if you define the polynomials:
\\[
Expand All @@ -137,7 +144,8 @@ Then
C = \\{ 1, 2, 3, 4, 5, 6, 7, 8, 9 \\} \iff
f(X) = g(X)
\\]
You can then check \\(f(X) = g(X) \\) by evaluating the polynomials at a random challenge \\( \alpha \\) and enforcing \\( f(\alpha) = g(\alpha) \\)
You can then check \\(f(X) = g(X) \\) by evaluating the polynomials at
a random challenge \\( \alpha \\) and enforcing \\( f(\alpha) = g(\alpha) \\)
```

```admonish hint
Expand Down
2 changes: 1 addition & 1 deletion src/dynamic-lookups/index.md
Original file line number Diff line number Diff line change
Expand Up @@ -2,7 +2,7 @@

![](./top.webp)

*What if I don't know what I want to look up?*
*"No, no!" said the Queen. "Sentence first—verdict afterwards."*

## Dynamic Lookups

Expand Down
47 changes: 31 additions & 16 deletions src/static-lookups/index.md
Original file line number Diff line number Diff line change
Expand Up @@ -11,12 +11,16 @@ Rather than trotting through yet another example with range checks,
we will explore *lookups* by creating a
"circuit" that can (very efficiently) match regular expressions.
Regular expression matching has been used in projects such as [zk-email](https://blog.aayushg.com/zkemail/),
although the approach outlined here is more efficient than that of [zk-email](https://blog.aayushg.com/zkemail/#regex-with-deterministic-finite-automata).
although the approach outlined here is more efficient than that of
[zk-email](https://blog.aayushg.com/zkemail/#regex-with-deterministic-finite-automata)
owing to the power of Halo2.

You might already be thinking that regular expressions are not very efficient to check using a circuit over a finite field,
and you would be right.
Fortunately, lookups enable us to implement this kind of very non-field-friendly functionality in an efficient way.
It might also sound complicated, but in fact, the whole (barebones) circuit fits in just over 200 lines of code.
You might be thinking that regular expressions are relatively inefficient
to check using a circuit over a finite field, and you would be right.
Fortunately, lookups enable us to implement this kind of
very non-field-friendly functionality in an efficient way.
It might also sound complicated, but in fact, the whole (barebones)
circuit fits in just over 200 lines of code.

## Brief Detour: Regular Expressions

Expand Down Expand Up @@ -51,7 +55,7 @@ and every edge is labeled with a character.
You are allowed to move between states if the next character in the string matches the edge label.
For instance, for our regular expression `a+b+c`, an NFA would look like this:

![Regex](./nfa.svg)
![Regex](./nfa-light-themed.svg)

Meaning:

Expand All @@ -65,13 +69,15 @@ Meaning:
- In state `ST_C`, you can:
- Only move to `ST_DONE` if the next character is `c`.

For instance, if the string we are matching is `aaabbc`, we would move through the states like this:
For instance, if the string we are matching is `aaabbc`,
we would move through the states like this:

```
ST_A -> ST_A -> ST_A -> ST_B -> ST_B -> ST_C -> ST_DONE
```

Conversely, if you have the string `aaabbb`, you would get stuck in state `ST_B` after the third `b` and not be able to move to `ST_C`.
Conversely, if you have the string `aaabbb`,
you would get stuck in state `ST_B` after the third `b` and not be able to move to `ST_C`.
We can represent this "NFA" as a table of valid state transitions:

| State | Character | Next State |
Expand All @@ -89,8 +95,10 @@ In Rust we could encode this table as follows:
```

The "values" of the states (e.g. `const ST_A: usize = 1`) are just arbitrary distinct integers.
We introduce a special `EOF` character which we will use to "pad" the end of the string: our circuit has a fixed size, but we want it to accommodate strings of different lengths.
We also add another transition `ST_DONE -> ST_DONE` for the `EOF` character: you can stay in the `ST_DONE` state forever by consuming the special `EOF` padding character.
We introduce a special `EOF` character which we will use to "pad" the end of the string:
our circuit has a fixed size, but we want it to accommodate strings of different lengths.
We also add another transition `ST_DONE -> ST_DONE` for the `EOF` character:
you can stay in the `ST_DONE` state forever by consuming the special `EOF` padding character.

If you are still confused, it simply means that we are now matching strings like:

Expand All @@ -102,12 +110,15 @@ Of some fixed length, where `<EOF>` is a special character.

```admonish note
In this example, we will just match the regular expression,
but in general you want to do something more interesting with the result or restrict the string being matched.
but in general you want to do something more interesting
with the result or restrict the string being matched.
For instance, in [zk-email](https://blog.aayushg.com/zkemail/#regex-with-deterministic-finite-automata) it is used to extract the sender's address from an email after *verifying a DKIM signature* on the email:
For instance, in [zk-email](https://blog.aayushg.com/zkemail/)
it is used to extract the sender's address from an email after *verifying a DKIM signature* on the email:
in this case the string being matched comes with a digital signature (an RSA signature).
In our case, the string ends up in a column and it is trivial to use it for further processing, like hashing it to check a digital signature on it.
In our case, the string ends up in a column and it is trivial to use it for further processing,
like hashing it to check a digital signature on it.
```

## Configuration
Expand Down Expand Up @@ -212,7 +223,9 @@ Nothing new here, we saw similar code in the section of `Column<Fixed>`.

### Assign Transitions

The meat of the circuit is in the region where we assign the sequence of states we are transitioning through, as well as the sequence of characters we are consuming:
The meat of the circuit is in the region where we assign
the sequence of states we are transitioning through,
as well as the sequence of characters we are consuming:

```rust,noplaypen
{{#include ../../halo-hero/examples/regex.rs:region_steps}}
Expand Down Expand Up @@ -243,7 +256,8 @@ we must somehow be able to transition from matching `a`s without consuming an `a
```

```admonish exercise
Create a circuit which computes a single round of [AES](https://en.wikipedia.org/wiki/Advanced_Encryption_Standard) encryption.
Create a circuit which computes a single round of
[AES](https://en.wikipedia.org/wiki/Advanced_Encryption_Standard) encryption.
You may ignore the key schedule.
```
Expand All @@ -269,7 +283,8 @@ Therefore, we can replace a single lookup in a 256x256 table with two lookups in
```

```admonish exercise
Create a circuit which takes an AES ciphertext as public input (instance) and a key as private input (witness) and checks that the ciphertext decrypts to a known plaintext.
Create a circuit which takes an AES ciphertext as public input (instance)
and a key as private input (witness) and checks that the ciphertext decrypts to a known plaintext.
```

```rust,noplaypen
Expand Down
Loading

0 comments on commit ac7bc45

Please sign in to comment.