zkVM
The DarkFi zkVM is a single zkSNARK circuit based on 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 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
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:
// Lookup and push constants onto the heap
for constant in &self.constants {
trace!(
target: "zk::vm",
"Pushing constant `{}` to heap address {}",
constant.as_str(),
heap.len()
);
match constant.as_str() {
"VALUE_COMMIT_VALUE" => {
let vcv = ValueCommitV;
let vcv = FixedPointShort::from_inner(ecc_chip.as_ref().unwrap().clone(), vcv);
heap.push(HeapVar::EcFixedPointShort(vcv));
}
"VALUE_COMMIT_RANDOM" => {
let vcr = OrchardFixedBasesFull::ValueCommitR;
let vcr = FixedPoint::from_inner(ecc_chip.as_ref().unwrap().clone(), vcr);
heap.push(HeapVar::EcFixedPoint(vcr));
}
"VALUE_COMMIT_RANDOM_BASE" => {
let vcr = ConstBaseFieldElement::value_commit_r();
let vcr =
FixedPointBaseField::from_inner(ecc_chip.as_ref().unwrap().clone(), vcr);
heap.push(HeapVar::EcFixedPointBase(vcr));
}
"NULLIFIER_K" => {
let nfk = ConstBaseFieldElement::nullifier_k();
let nfk =
FixedPointBaseField::from_inner(ecc_chip.as_ref().unwrap().clone(), nfk);
heap.push(HeapVar::EcFixedPointBase(nfk));
}
_ => {
error!(target: "zk::vm", "Invalid constant name: {}", constant.as_str());
return Err(plonk::Error::Synthesis)
}
}
}If all is successful, the VM proceeds with any available literals in
the circuit section and pushes them onto the literals heap:
// Load the literals onto the literal heap
// N.B. Only uint64 is supported right now.
for literal in &self.literals {
match literal.0 {
LitType::Uint64 => match literal.1.parse::<u64>() {
Ok(v) => litheap.push(v),
Err(e) => {
error!(target: "zk::vm", "Failed converting u64 literal: {}", e);
return Err(plonk::Error::Synthesis)
}
},
_ => {
error!(target: "zk::vm", "Invalid literal: {:?}", literal);
return Err(plonk::Error::Synthesis)
}
}
}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:
// 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.
for witness in &self.witnesses {
match witness {
Witness::EcPoint(w) => {
trace!(target: "zk::vm", "Witnessing EcPoint into circuit");
let point = Point::new(
ecc_chip.as_ref().unwrap().clone(),
layouter.namespace(|| "Witness EcPoint"),
w.as_ref().map(|cm| cm.to_affine()),
)?;
trace!(target: "zk::vm", "Pushing EcPoint to heap address {}", heap.len());
heap.push(HeapVar::EcPoint(point));
}
Witness::EcNiPoint(w) => {
trace!(target: "zk::vm", "Witnessing EcNiPoint into circuit");
let point = NonIdentityPoint::new(
ecc_chip.as_ref().unwrap().clone(),
layouter.namespace(|| "Witness EcNiPoint"),
w.as_ref().map(|cm| cm.to_affine()),
)?;
trace!(target: "zk::vm", "Pushing EcNiPoint to heap address {}", heap.len());
heap.push(HeapVar::EcNiPoint(point));
}
Witness::EcFixedPoint(_) => {
error!(target: "zk::vm", "Unable to witness EcFixedPoint, this is unimplemented.");
return Err(plonk::Error::Synthesis)
}
Witness::Base(w) => {
trace!(target: "zk::vm", "Witnessing Base into circuit");
let base = assign_free_advice(
layouter.namespace(|| "Witness Base"),
config.witness,
*w,
)?;
trace!(target: "zk::vm", "Pushing Base to heap address {}", heap.len());
heap.push(HeapVar::Base(base));
}
Witness::Scalar(w) => {
trace!(target: "zk::vm", "Witnessing Scalar into circuit");
let scalar = ScalarFixed::new(
ecc_chip.as_ref().unwrap().clone(),
layouter.namespace(|| "Witness ScalarFixed"),
*w,
)?;
trace!(target: "zk::vm", "Pushing Scalar to heap address {}", heap.len());
heap.push(HeapVar::Scalar(scalar));
}
Witness::MerklePath(w) => {
trace!(target: "zk::vm", "Witnessing MerklePath into circuit");
let path: Value<[pallas::Base; MERKLE_DEPTH_ORCHARD]> =
w.map(|typed_path| gen_const_array(|i| typed_path[i].inner()));
trace!(target: "zk::vm", "Pushing MerklePath to heap address {}", heap.len());
heap.push(HeapVar::MerklePath(path));
}
Witness::SparseMerklePath(w) => {
let path: Value<[pallas::Base; SMT_FP_DEPTH]> =
w.map(|typed_path| gen_const_array(|i| typed_path[i]));
trace!(target: "zk::vm", "Pushing SparseMerklePath to heap address {}", heap.len());
heap.push(HeapVar::SparseMerklePath(path));
}
Witness::Uint32(w) => {
trace!(target: "zk::vm", "Pushing Uint32 to heap address {}", heap.len());
heap.push(HeapVar::Uint32(*w));
}
Witness::Uint64(w) => {
trace!(target: "zk::vm", "Pushing Uint64 to heap address {}", heap.len());
heap.push(HeapVar::Uint64(*w));
}
}
}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:
for opcode in &self.opcodes {
match opcode.0 {
Opcode::EcAdd => {
trace!(target: "zk::vm", "Executing `EcAdd{:?}` opcode", opcode.1);
let args = &opcode.1;
let lhs: Point<pallas::Affine, EccChip<OrchardFixedBases>> =
heap[args[0].1].clone().try_into()?;
let rhs: Point<pallas::Affine, EccChip<OrchardFixedBases>> =
heap[args[1].1].clone().try_into()?;
let ret = lhs.add(layouter.namespace(|| "EcAdd()"), &rhs)?;
trace!(target: "zk::vm", "Pushing result to heap address {}", heap.len());
self.tracer.push_ecpoint(&ret);
heap.push(HeapVar::EcPoint(ret));
}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.