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 {
                target: "zk::vm",
                "Pushing constant `{}` to heap address {}",
            match constant.as_str() {
                "VALUE_COMMIT_VALUE" => {
                    let vcv = ValueCommitV;
                    let vcv = FixedPointShort::from_inner(ecc_chip.clone(), vcv);
                "VALUE_COMMIT_RANDOM" => {
                    let vcr = OrchardFixedBasesFull::ValueCommitR;
                    let vcr = FixedPoint::from_inner(ecc_chip.clone(), vcr);
                "NULLIFIER_K" => {
                    let nfk = NullifierK;
                    let nfk = FixedPointBaseField::from_inner(ecc_chip.clone(), 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(
                        layouter.namespace(|| "Witness EcPoint"),
                        w.as_ref().map(|cm| cm.to_affine()),

                    trace!(target: "zk::vm", "Pushing EcPoint to heap address {}", heap.len());

                Witness::EcNiPoint(w) => {
                    trace!(target: "zk::vm", "Witnessing EcNiPoint into circuit");
                    let point = NonIdentityPoint::new(
                        layouter.namespace(|| "Witness EcNiPoint"),
                        w.as_ref().map(|cm| cm.to_affine()),

                    trace!(target: "zk::vm", "Pushing EcNiPoint to heap address {}", heap.len());

                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"),

                    trace!(target: "zk::vm", "Pushing Base to heap address {}", heap.len());

                Witness::Scalar(w) => {
                    // NOTE: Because the type in `halo2_gadgets` does not have a `Clone`
                    //       impl, we push scalars as-is to the heap. They get witnessed
                    //       when they get used.
                    trace!(target: "zk::vm", "Pushing Scalar to heap address {}", heap.len());

                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());

                Witness::Uint32(w) => {
                    trace!(target: "zk::vm", "Pushing Uint32 to heap address {}", heap.len());

                Witness::Uint64(w) => {
                    trace!(target: "zk::vm", "Pushing Uint64 to heap address {}", heap.len());

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>> =

                    let rhs: Point<pallas::Affine, EccChip<OrchardFixedBases>> =

                    let ret = lhs.add(layouter.namespace(|| "EcAdd()"), &rhs)?;

                    trace!(target: "zk::vm", "Pushing result to heap address {}", heap.len());

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.