Merge pull request #88 from zcash/book-bits

More book bits

.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/
 

.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)

book/book.toml

@@ -4,3 +4,5 @@ language = "en"
 multilingual = false
 src = "src"
 title = "The halo2 Book"
+
+[preprocessor.katex]

book/src/SUMMARY.md

@@ -3,5 +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)

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.

book/src/user/lookup-tables.md

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

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 \cdot b = c.$$
+
+```rust
+# extern crate halo2;
+use halo2::arithmetic::FieldExt;
+
+struct MyCircuit<F: FieldExt> {
+    a: F,
+    b: F,
+}
+```
+
+TODO

book/src/user/tips-and-tricks.md

@@ -0,0 +1,27 @@
+# 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 \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) \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
+> 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.