From a9146ae4722962df0b74a6fb93038b5c2df30333 Mon Sep 17 00:00:00 2001 From: Jack Grigg Date: Thu, 10 Dec 2020 20:09:47 +0000 Subject: [PATCH 1/7] book: Add KaTeX support --- .github/workflows/book.yml | 6 ++++++ book/book.toml | 2 ++ 2 files changed, 8 insertions(+) diff --git a/.github/workflows/book.yml b/.github/workflows/book.yml index 404e4735..c66530a7 100644 --- a/.github/workflows/book.yml +++ b/.github/workflows/book.yml @@ -16,6 +16,12 @@ jobs: with: mdbook-version: '0.4.4' + - name: Install mdbook-katex + uses: actions-rs/cargo@v1 + with: + command: install + args: mdbook-katex + - name: Build halo2 book run: mdbook build book/ diff --git a/book/book.toml b/book/book.toml index eb4a8d9c..c6278076 100644 --- a/book/book.toml +++ b/book/book.toml @@ -4,3 +4,5 @@ language = "en" multilingual = false src = "src" title = "The halo2 Book" + +[preprocessor.katex] From e16946f56b5f3c28ba47178fe2f35946d5cc84fb Mon Sep 17 00:00:00 2001 From: Jack Grigg Date: Thu, 10 Dec 2020 20:18:32 +0000 Subject: [PATCH 2/7] CI: Build crate and make it available to book tests --- .github/workflows/ci.yml | 6 +++++- 1 file changed, 5 insertions(+), 1 deletion(-) diff --git a/.github/workflows/ci.yml b/.github/workflows/ci.yml index dbe01265..a82544dd 100644 --- a/.github/workflows/ci.yml +++ b/.github/workflows/ci.yml @@ -69,12 +69,16 @@ jobs: runs-on: ubuntu-latest steps: - uses: actions/checkout@v2 + - name: cargo build + uses: actions-rs/cargo@v1 + with: + command: build - name: Setup mdBook uses: peaceiris/actions-mdbook@v1 with: mdbook-version: '0.4.4' - name: Test halo2 book - run: mdbook test book/ + run: mdbook test -L target/debug/deps book/ clippy: name: Clippy (stable) From 2a7df99478e9ef886fb137121861b9652e03fc6d Mon Sep 17 00:00:00 2001 From: Jack Grigg Date: Thu, 10 Dec 2020 20:35:36 +0000 Subject: [PATCH 3/7] book: Start collecting tips and tricks --- book/src/SUMMARY.md | 1 + book/src/user/tips-and-tricks.md | 25 +++++++++++++++++++++++++ 2 files changed, 26 insertions(+) create mode 100644 book/src/user/tips-and-tricks.md diff --git a/book/src/SUMMARY.md b/book/src/SUMMARY.md index e743c380..f0ccfe30 100644 --- a/book/src/SUMMARY.md +++ b/book/src/SUMMARY.md @@ -4,4 +4,5 @@ - [Concepts](concepts.md) - [User Documentation](user.md) - [Gadgets](user/gadgets.md) + - [Tips and tricks](user/tips-and-tricks.md) - [Design](design.md) diff --git a/book/src/user/tips-and-tricks.md b/book/src/user/tips-and-tricks.md new file mode 100644 index 00000000..3cfe471e --- /dev/null +++ b/book/src/user/tips-and-tricks.md @@ -0,0 +1,25 @@ +# Tips and tricks + +This section contains various ideas and snippets that you might find useful while writing +halo2 circuits. + +## Small range constraints + +A common constraint used in R1CS circuits is the boolean constraint: $b * (1 - b) = 0$. +This constraint can only be satisfied by $b = 0$ or $b = 1$. + +In halo2 circuits, you can similarly constrain a cell to have one of a small set of +values. For example, to constrain $a$ to the range $[0..5]$, you would create a gate of +the form: + +$$a * (1 - a) * (2 - a) * (3 - a) * (4 - a) = 0$$ + +while to constraint $c$ to be either 7 or 13, you would use: + +$$(7 - c) * (13 - c) = 0$$ + +> The underlying principle here is that we create a polynomial constraint with roots at +> each value in the set of possible values we want to allow. In R1CS circuits, the maximum +> supported polynomial degree is 2 (due to all constraints being of the form $a * b = c$). +> In halo2 circuits, you can use arbitrary-degree polynomials - with the proviso that +> higher-degree constraints are more expensive to use. From e1c770a59193d4a6e9186894765aaa5dff89447f Mon Sep 17 00:00:00 2001 From: Jack Grigg Date: Thu, 10 Dec 2020 20:43:01 +0000 Subject: [PATCH 4/7] book: Add some more placeholder sections to the user guide --- book/src/SUMMARY.md | 2 ++ book/src/user.md | 4 ++++ book/src/user/lookup-tables.md | 7 +++++++ book/src/user/simple-example.md | 19 +++++++++++++++++++ 4 files changed, 32 insertions(+) create mode 100644 book/src/user/lookup-tables.md create mode 100644 book/src/user/simple-example.md diff --git a/book/src/SUMMARY.md b/book/src/SUMMARY.md index f0ccfe30..3502ccf2 100644 --- a/book/src/SUMMARY.md +++ b/book/src/SUMMARY.md @@ -3,6 +3,8 @@ [halo2](README.md) - [Concepts](concepts.md) - [User Documentation](user.md) + - [A simple example](user/simple-example.md) + - [Lookup tables](user/lookup-tables.md) - [Gadgets](user/gadgets.md) - [Tips and tricks](user/tips-and-tricks.md) - [Design](design.md) diff --git a/book/src/user.md b/book/src/user.md index 3a51d9a2..c13533a5 100644 --- a/book/src/user.md +++ b/book/src/user.md @@ -1 +1,5 @@ # User Documentation + +You're probably here because you want to write circuits? Excellent! + +This section will guide you through the process of creating circuits with halo2. diff --git a/book/src/user/lookup-tables.md b/book/src/user/lookup-tables.md new file mode 100644 index 00000000..25e60e97 --- /dev/null +++ b/book/src/user/lookup-tables.md @@ -0,0 +1,7 @@ +# Lookup tables + +In normal programs, you can trade memory for CPU to improve performance, by pre-computing +and storing lookup tables for some part of the computation. We can do the same thing in +halo2 circuits! + +TODO diff --git a/book/src/user/simple-example.md b/book/src/user/simple-example.md new file mode 100644 index 00000000..20ecbee9 --- /dev/null +++ b/book/src/user/simple-example.md @@ -0,0 +1,19 @@ +# A simple example + +Let's start with a simple circuit, to introduce you to the common APIs and how they are +used. The circuit will take a public input $c$, and will prove knowledge of two private +inputs $a$ and $b$ such that + +$$a * b = c.$$ + +```rust +# extern crate halo2; +use halo2::arithmetic::FieldExt; + +struct MyCircuit { + a: F, + b: F, +} +``` + +TODO From 8f929888afbacdab1a7469720b05cb82cf588580 Mon Sep 17 00:00:00 2001 From: str4d Date: Fri, 11 Dec 2020 18:34:59 +0000 Subject: [PATCH 5/7] book: Describe a lookup table as representing a relation Co-authored-by: Daira Hopwood --- book/src/user/lookup-tables.md | 4 ++++ 1 file changed, 4 insertions(+) diff --git a/book/src/user/lookup-tables.md b/book/src/user/lookup-tables.md index 25e60e97..2709a94f 100644 --- a/book/src/user/lookup-tables.md +++ b/book/src/user/lookup-tables.md @@ -4,4 +4,8 @@ In normal programs, you can trade memory for CPU to improve performance, by pre- and storing lookup tables for some part of the computation. We can do the same thing in halo2 circuits! +A lookup table can be thought of as enforcing a *relation* between variables, where the relation is expressed as a table. +Assuming we have only one lookup argument in our constraint system, the total size of tables is constrained by the size of the circuit: +each table entry costs one row, and it also costs one row to do each lookup. + TODO From 653cb6ca88e3d0c72984bb3b16e925b46c3efc38 Mon Sep 17 00:00:00 2001 From: str4d Date: Fri, 11 Dec 2020 18:36:46 +0000 Subject: [PATCH 6/7] book: Use \cdot for multiplications Co-authored-by: Daira Hopwood --- book/src/user/simple-example.md | 2 +- book/src/user/tips-and-tricks.md | 4 ++-- 2 files changed, 3 insertions(+), 3 deletions(-) diff --git a/book/src/user/simple-example.md b/book/src/user/simple-example.md index 20ecbee9..964471ce 100644 --- a/book/src/user/simple-example.md +++ b/book/src/user/simple-example.md @@ -4,7 +4,7 @@ Let's start with a simple circuit, to introduce you to the common APIs and how t used. The circuit will take a public input $c$, and will prove knowledge of two private inputs $a$ and $b$ such that -$$a * b = c.$$ +$$a \cdot b = c.$$ ```rust # extern crate halo2; diff --git a/book/src/user/tips-and-tricks.md b/book/src/user/tips-and-tricks.md index 3cfe471e..e1dcce58 100644 --- a/book/src/user/tips-and-tricks.md +++ b/book/src/user/tips-and-tricks.md @@ -12,11 +12,11 @@ In halo2 circuits, you can similarly constrain a cell to have one of a small set values. For example, to constrain $a$ to the range $[0..5]$, you would create a gate of the form: -$$a * (1 - a) * (2 - a) * (3 - a) * (4 - a) = 0$$ +$$a \cdot (1 - a) \cdot (2 - a) \cdot (3 - a) \cdot (4 - a) = 0$$ while to constraint $c$ to be either 7 or 13, you would use: -$$(7 - c) * (13 - c) = 0$$ +$$(7 - c) \cdot (13 - c) = 0$$ > The underlying principle here is that we create a polynomial constraint with roots at > each value in the set of possible values we want to allow. In R1CS circuits, the maximum From 2aea5828651539cb0a72b2afdae2c7b1ce649384 Mon Sep 17 00:00:00 2001 From: str4d Date: Fri, 11 Dec 2020 18:45:14 +0000 Subject: [PATCH 7/7] book: Note that roots don't have to be constant Co-authored-by: Daira Hopwood --- book/src/user/tips-and-tricks.md | 2 ++ 1 file changed, 2 insertions(+) diff --git a/book/src/user/tips-and-tricks.md b/book/src/user/tips-and-tricks.md index e1dcce58..9f1cb735 100644 --- a/book/src/user/tips-and-tricks.md +++ b/book/src/user/tips-and-tricks.md @@ -23,3 +23,5 @@ $$(7 - c) \cdot (13 - c) = 0$$ > supported polynomial degree is 2 (due to all constraints being of the form $a * b = c$). > In halo2 circuits, you can use arbitrary-degree polynomials - with the proviso that > higher-degree constraints are more expensive to use. + +Note that the roots don't have to be constants; for example $(a - x) \cdot (a - y) \cdot (a - z) = 0$ will constrain $a$ to be equal to one of $\{ x, y, z \}$ where the latter can be arbitrary polynomials, as long as the whole expression stays within the maximum degree bound.