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 Instruction
s:
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::Closed
is an opaque type holding a compressed Ristretto point (represented by a 32-byte string).Commitment::Open
is 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 an enum:
Predicate::Opaque
is an opaque type to represent all predicates for the verifier’s VM.Predicate::Key
is a witness type representing a signing key forsignid
,signtag
andsigntx
instructions.Predicate::Tree
is a witness type representing the Taproot Merkle tree for thecall
instruction.Predicate::Program
is a witness type representing a program commitment for thecall
instruction.
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.