The ZkVM specification covers the verification rules for transactions that are already created, but does not describe how to create such transactions. This is the goal of this document.
The Prover and Verifier are two entry points to the ZkVM:
Prover is an API for creating a transaction object Tx out of a stream of Instructions:
VM executes the instructions, producing a serialized program bytecode, aggregated transaction signature
and a zero-knowledge R1CS proof for the Cloak protocol and custom statements expressed by instructions.
Verifier is an API for verifying a transaction object Tx: it parses the bytecode, executes it, verifies the aggregated transaction signature and the R1CS proof, producing a VerifiedTx as a result. Verification logic is described by the ZkVM specification.
Note that VM execution is used twice: first, for proving, then for verifying.
How does the Prover know how to sign transaction and make a proof? The prover’s input is not an opaque sequence of instruction codes, but witness-bearing instructions. That is, a push instruction on the prover’s side does not hold an opaque string of bytes, but an accurate witness type that may contain secret data and necessary structure for creating the proofs and signatures.
We call a type opaque if it provides only enough information for the verification of a ZkVM transaction or some sub-protocol.
We call a type witness if it contains secret data and structure necessary for the prover to create a zero-knowledge proof or a signature.
Pedersen commitment is represented with an enum Commitment:
Commitment::Closedis an opaque type holding a compressed Ristretto point (represented by a 32-byte string).Commitment::Openis a witness type that holds a pair of a secret value (scalar witness) and a secret blinding factor. These are used to create a R1CS proof using the prover’s instance of the VM.
Predicate is a structure that encapsulates an opaque VerificationKey and an optional dynamically typed PredicateWitness. Witness may contain a private key directly, or metadata that helps creating a signature such as Multikey layout, derivation sequence number etc.
Variables are represented as type-wrappers around Pedersen commitments. The secret assignments for the variables are stored within the commitment witnesses as described above.
Expressions store their witness data as an optional assignment Option<ScalarWitness>.
The verifier’s VM sees None and the prover’s VM sees Some(...).
See also scalar witness.
Constraints do not have explicit witness data. They can be computed on the fly by evaluating the boolean function that the constraint represents, taking the underlying expressions’ assignments as input.
A signtx instruction expects a predicate point to be a verification key. In the Prover such key is represented as a Data::Witness type that holds PredicateWitness::Key. When the prover’s VM pops such item from the stack it remembers it. At the end of the VM execution, the prover queries the key storage for the corresponding secret keys and creates a transaction signature. Verifier uses the accumulated verification keys to verify the aggregated signature.
An input instruction decodes a serialized contract. In the prover’s VM it pops an Input item from the stack that contains a previously created Output object with usual data items (with witnesses) and “frozen values”: values where quantity and flavors are represented by open commitments instead of variables.
The VM extracts the Output object from the Input and converts it to a Contract type by allocating variables for each commitment within frozen values, turning them into actual Value types.
Scalar witness represents either:
- a scalar, or
- a signed integer
Arithmetic operations on scalar witnesses preserve integers until overflow. If an addition/multiplication of two integers overflows the range of ±(2^64-1), the result is promoted to a scalar modulo Ristretto group order.
Range proof gadget in Cloak requires a witness to be an integer (and also checks that it is non-negative) and does not attempt to carve 64 bits out of a scalar. For safety, integer overflows immediately promote the integer to a scalar: any higher-level protocol that wishes to operate on integer quantities must ensure that they never overflow.