Merge pull request #15 from scroll-tech/kunming/documentations

Update documentation

documentations/circ_blocks.md

@@ -0,0 +1,82 @@
+# CirC Blocks
+This document covers the basics of `circ_blocks` as well as how to use it.
+
+## Overview
+`circ_blocks` converts a program code of a high-level language into circuits used by SNARK codes. In particular, it performs the following conversion:
+```
+ZoKrates -> Basic Blocks -> Optimized Blocks -> CirC IR -> R1CS
+```
+
+## Basic Blocks
+`circ_blocks` takes in ZoKrates as its front-end language. See `zok_format` for detailed format of ZoKrates. The first [transformation](https://github.com/Jiangkm3/circ_blocks/blob/master/src/front/zsharp/blocks.rs#L568) converts zok programs into [blocks](https://github.com/Jiangkm3/circ_blocks/blob/master/src/front/zsharp/blocks.rs#L219) strictly following its control flow. As such, one should expect the emitted blocks to be the exact basic blocks of the program.
+
+## Optimizing Blocks
+To emit more efficient constraints, `circ_blocks` performs the following [optimizations](https://github.com/Jiangkm3/circ_blocks/blob/master/src/front/zsharp/blocks_optimization.rs#L1656) upon the basic blocks:
+- Liveness Analysis / Dead Code Elimination
+- Function Merge
+- Block Merge
+- Spilling
+- Register Allocation
+- Memory Allocation
+
+See [writeups](https://github.com/Jiangkm3/circ_blocks/blob/master/writeups) of `circ_blocks` for details of some of the implementations.
+
+## Lowering Blocks into Circuits
+`circ_blocks` repackages each block as standalone programs and lowers them into CirC IR and R1CS through the same functionality as CirC. See [bls_to_circ](https://github.com/Jiangkm3/circ_blocks/blob/master/src/front/zsharp/blocks.rs#L2173).
+
+## Interpreting Blocks
+The Prover generates witnesses through an [interpreter](https://github.com/Jiangkm3/circ_blocks/blob/master/src/front/zsharp/prover.rs#L200). It executes the program through the trace of blocks and records all intermediate program states. It terminates the interpretation once it reaches the exit block, or encounters an unsatisfiable assertion.
+
+## Running `circ_blocks`
+Build and run `circ_blocks` by:
+1. Navigate to `circ_blocks`
+2. Run `cargo build --release --example zxc --no-default-features --features r1cs,smt,zok` to build
+3. Run `target/release/examples/zxc <flags> <benchmark>`
+  - For ceno, use `ceno_demo/tower_verifier` for benchmark
+  - Flags include:
+    * `--no_opt`: disables most of the block optimizations
+    * `--verbose_opt`: emits new blocks after each optimization pass
+    * `--inline_spartan`: verifies ciruits automatically using `spartan_parallel`
+
+### Output Format
+`circ_blocks` prints out block representation of the program, where
+- without `--verbose_opt`, it prints out all basic blocks of the program and all optimized blocks
+- with `--verbose_opt`, it prints out all blocks after each optimization pass
+
+A block is of the following format:
+```
+Block 5:  <-- block label
+Func: main, Scope: 2  <-- the function and scope of the block (for optimization)
+Exec Bound: 1600, While Loop: false  <-- static upper bound on number of executions (to estimate circuit size)
+RO Ops: 0, VM Ops: 2  <-- number of memory operations within the block (read-only and RAM)
+Num Cons: 190  <-- estimated number of constraints
+Inputs:
+    %i1(BN): field  <-- block inputs
+    %i3(TS): field      should match outputs of the previous block
+    %i7: field
+    %i8: u32
+    ...
+Outputs:
+    %o1(BN): field  <-- block outputs
+    %o3(TS): field      should match inputs of the next block
+    %o7: field
+    %o8: u32
+    ...
+Instructions:
+    assert %i1(BN) == 5 <Field>
+    field %w1(TS) = %i3(TS)
+    field %w12 = %i7
+    u32 %w7 = %i8  <-- instructions: 
+    u32 %w8 = %i9      assertion, assignment, conditional, and mem_ops
+    ...
+    if %w5 < %w19 && %w19 < %w8 && %w20 < %w17:
+        u32 %w21 = %w12[%w19]
+        %w17 = %w21
+        %w18 = %w19
+    else:
+        Dummy Load
+    ...
+    field %o1(BN) = %w19 != 1600 <U32> ? 5 <Field> : 6 <Field>
+Transition: 
+    %w19 != 1600 <U32> ? -> 5 : -> 6  <-- transition marks the label of the next block
+```

documentations/spartan_parallel.md

@@ -0,0 +1,37 @@
+# Spartan Parallel
+
+## Overview
+`spartan_parallel` takes in circuits and witnesses of the blocks produced by `circ_blocks`, and generates and verifies a SNARK proof on the correct execution of the program code. One can treat `spartan_parallel` as a two-step process: first it emits 5 different (groups of, should really be number of blocks + 4) circuits based on the blocks and an execution trace, then it evokes a data-parallel proving process on those 5 circuits.
+
+## High-Level Idea
+The program is executed correctly iff all of the following holds:
+1. All blocks of the program are executed correctly
+2. All registers (including the label of the next block) are passed correctly between blocks.
+3. The memory state (read-only and RAM) stays coherent throughout the execution.
+
+Statement 1 can be checked directly through the block-specific circuits emitted by `circ_blocks`, while statement 2 and 3 can be checked by "extracting" inputs, outputs, and memory accesses out of block witnesses and check that they are pairwise consistent. `spartan_parallel` achieves so by generating "extraction circuits" and "consistency check circuits" based on compile-time metadata (number of inputs, outputs, and number of memory accesses per block). Furthermore, all three statements require witnesses to be arranged in different orders (statement 1 by block type, statement 2 by execution time, statement 3 by memory address), `spartan_parallel` inserts "permutation circuits" to verify the permutation between all three ordering: construct three univariate polynomials and test their equivalence by evaluating on a random point. [Let me know if this does not make sense!]
+
+Please refer to [instance.rs](https://github.com/Jiangkm3/spartan_parallel/blob/master/src/instance.rs) for details of the circuits.
+
+## Inputs and Circuit Generation
+At preprocessing stage, `spartan_parallel` reads in the following [inputs](https://github.com/Jiangkm3/spartan_parallel/blob/master/examples/interface.rs#L45):
+- Circuits of each basic block
+- Number of inputs, outputs, and memory operations of each block, as well as where these values are stored within the witnesses.
+- Max number of registers that need to be passed from one block to another
+- Max number of read-only memory accesses within a block
+- Max number of RAM accesses within a block
+
+Through the above inputs, `spartan_parallel` emits the following circuits during the preprocessing stage:
+1. `BLOCK_CORRECTNESS` ([link](https://github.com/Jiangkm3/spartan_parallel/blob/master/src/instance.rs#L246)): verifies the correct execution of every block and "extracts" (constructs the polynomials) inputs, outputs, and all memory values out of each block.
+2. `CONSIS_CHECK` ([link](https://github.com/Jiangkm3/spartan_parallel/blob/master/src/instance.rs#L545)): checks that when sorted in execution order, the output of the previous block matches with the input of the next block. This is performed similarly to an offline memory check.
+3. `PHY_MEM_COHERE` ([link](https://github.com/Jiangkm3/spartan_parallel/blob/master/src/instance.rs#L545)): checks that the read-only memory accesses are coherent via an offline memory check.
+4. `VIR_MEM_COHERE` ([link](https://github.com/Jiangkm3/spartan_parallel/blob/master/src/instance.rs#L545)): checks that all RAM accesses are coherent via an offline memory check.
+5. `PERM_ROOT` ([link](https://github.com/Jiangkm3/spartan_parallel/blob/master/src/instance.rs#L761)): performs permutation check by constructing the polynomials of inputs and memory entries in execution / address order (block type order is handled in `BLOCK CORRECTNESS`)
+
+## Verify Sumcheck in Parallel
+The main idea behind Spartan is to use _two sumcheck protocols_ to assert the correctness of an R1CS equation: `Az * Bz - Cz = 0`. Let `A`, `B`, `C` be circuits of size `x * y`, and subsequently `z` be a satisfying assignment of length `y`. Sumcheck 1 invokes `log(x)` rounds to prove that given `Az`, `Bz`, `Cz` supplied by the prover, the equation `Az * Bz - Cz = 0` holds. Sumcheck 2 then uses `log(y)` rounds to prove that `Az`, `Bz`, and `Cz` are computed correctly. 
+
+We expand Spartan to support `p` circuits, each with `q_i` satisfying assignments (equivalent to `p` blocks, each executed `q_i` times). Let `q_max = max_i q_i`, [sumcheck 1](https://github.com/Jiangkm3/spartan_parallel/blob/master/src/r1csproof.rs#L320) now requires `log(p) + log(q_max) + log(x)` rounds to prove every row of every circuit evaluates to 0, and [sumcheck 2](https://github.com/Jiangkm3/spartan_parallel/blob/master/src/r1csproof.rs#L462) now requires `log(p) + log(y)` rounds to check `Az`, `Bz`, and `Cz` for every `A`, `B`, and `C`. (Note: sumcheck 2 requires another `log(p)` rounds because `p` is a parameter to both the number of circuits and the number of witnesses. Without the extra `log(p)` rounds for flattening, the multiplication would be quadratic to `p`). The above protocol translates to `O(log(p) + 2 * log(q_max) + log(x))` work for the verifier. To bound prover work to `sum_i q_i` (as opposed to `p * q_i`), we use special [data structure](https://github.com/Jiangkm3/spartan_parallel/blob/master/src/custom_dense_mlpoly.rs#L22) to skip the unused "zero" entries within the dense polynomial.
+
+## Batched Commitments
+Spartan currently uses Hyrax for polynomial commitment, which is easily data-parallelizable. `spartan_parallel` commits to each circuit separately (but in batch), and commits witnesses by the type of circuit (block) they are being applied to. This allows the size and number of execution of each block to be different, but at the cost of having commitment size linear to number of circuits (blocks). Thus it is of top priority to try to reduce the number of blocks emitted.