book: Add high-level doc on zkVM.

doc/src/SUMMARY.md

@@ -27,6 +27,7 @@
   - [Transaction lifetime](architecture/sc/tx-lifetime.md)
 - [zkas](zkas/index.md)
   - [Bincode](zkas/bincode.md)
+  - [zkVM](zkas/zkvm.md)
   - [Examples](zkas/examples.md)
     - [Anonymous voting](zkas/examples/voting.md)
     - [Anonymous payments](zkas/examples/sapling.md)

doc/src/zkas/zkvm.md

@@ -0,0 +1,69 @@
+zkVM
+====
+
+The DarkFi zkVM is a single zkSNARK circuit based on
+[Halo2](https://github.com/zcash/halo2) which requires no trusted
+setup and is able to execute and prove compiled _zkas_ bincode.
+
+The zkVM is designed in such a way that it's able to choose code paths
+based on the bincode and as such, create a zkSNARK proof specific to
+the zkas circuit. In this document, we'll explain this machinery from
+a high level. A preliminary to understanding the zkVM is to understand
+the [zkas bincode](bincode.md) and its layout.
+
+## High-level operation
+
+The entire VM can be thought of as a machine with heap
+access to values (variables) that are constructed within
+the ZK circuit.  Upon initialization, the VM instantiates
+two heaps, of which one holds literals (currently `u64` is
+supported), and the other holds arbitrary types defined in
+[`HeapVar`](https://darkrenaissance.github.io/darkfi/development/darkfi/zk/vm_heap/enum.HeapVar.html)
+
+Once the heaps are instantiated, the circuit initializes all the
+available halo2 gadgets so they're ready for use, and also to create
+and have access to any lookup tables.
+
+Next, if there are any constants defined in the `constant` section
+of zkas, they are created and pushed to the heap:
+
+```rust,no_run,no_playground
+{{#include ../../../src/zk/vm.rs:constant_init}}
+```
+
+If all is successful, the VM proceeds with any available literals in
+the `circuit` section and pushes them onto the literals heap:
+
+```rust,no_run,no_playground
+{{#include ../../../src/zk/vm.rs:literals_init}}
+```
+
+At this point, the VM is done with initializing the constants used,
+and proceeds with the private witnesses of the ZK proof that are
+located in the `witness` section of the zkas bincode. We simply
+loop through the witnesses in order, and depending on what they are,
+we witness them with specialized halo2 functions:
+
+```rust,no_run,no_playground
+{{#include ../../../src/zk/vm.rs:witness_init}}
+```
+
+Once this is done, everything is set up and the VM proceeds with
+executing the input opcodes that are located in the `circuit` section
+of the zkas bincode in a sequential fashion. Opcodes are able to
+take a defined number of inputs and are able to optionally produce
+a single output. The inputs are referenced from the heap, by index.
+The output that can be produced by an opcode is also pushed onto the
+heap when created. An example of this operation can be seen within
+the following snippet from the zkVM:
+
+```rust,no_run,no_playground
+{{#include ../../../src/zk/vm.rs:opcode_begin}}
+```
+
+As the opcodes are being executed, the halo2 API lets us return any
+possible proof verification error so the verifier is able to know
+if the input proof is valid or not. Any possible public inputs to a
+circuit are also fed into the `constrain_instance` opcode, so that's
+how even public inputs can be enforced in the same uniform fashion
+like the rest.

src/zk/vm.rs

@@ -346,6 +346,7 @@ impl Circuit<pallas::Base> for ZkCircuit {
             Value::known(pallas::Base::one()),
         )?;
 
+        // ANCHOR: constant_init
         // Lookup and push constants onto the heap
         for constant in &self.constants {
             trace!(
@@ -377,7 +378,9 @@ impl Circuit<pallas::Base> for ZkCircuit {
                 }
             }
         }
+        // ANCHOR_END: constant_init
 
+        // ANCHOR: literals_init
         // Load the literals onto the literal heap
         // N.B. Only uint64 is supported right now.
         for literal in &self.literals {
@@ -395,7 +398,9 @@ impl Circuit<pallas::Base> for ZkCircuit {
                 }
             }
         }
+        // ANCHOR_END: literals_init
 
+        // ANCHOR: witness_init
         // Push the witnesses onto the heap, and potentially, if the witness
         // is in the Base field (like the entire circuit is), load it into a
         // table cell.
@@ -470,11 +475,13 @@ impl Circuit<pallas::Base> for ZkCircuit {
                 }
             }
         }
+        // ANCHOR_END: witness_init
 
         // =============================
         // And now, work through opcodes
         // =============================
         // TODO: Copy constraints
+        // ANCHOR: opcode_begin
         for opcode in &self.opcodes {
             match opcode.0 {
                 Opcode::EcAdd => {
@@ -492,7 +499,7 @@ impl Circuit<pallas::Base> for ZkCircuit {
                     trace!(target: "zk::vm", "Pushing result to heap address {}", heap.len());
                     heap.push(HeapVar::EcPoint(ret));
                 }
-
+                // ANCHOR_END: opcode_begin
                 Opcode::EcMul => {
                     trace!(target: "zk::vm", "Executing `EcMul{:?}` opcode", opcode.1);
                     let args = &opcode.1;