zk-VM: Advanced Usage

For basic usage of the Valida zk-VM, see QUICK STARK: Valida zk-VM. This page covers more advanced usage options for the Valida zk-VM.

Separate preprocessing stage

By default, the Valida prover and verifier perform the preprocessing stage of the argument from scratch each time. If you wish to perform the preprocessing stage of the argument as a separate step and write the result to a file, you can do so as follows:

valida preprocess $PROGRAM $NAME

This assumes that $PROGRAM is the path to a Valida executable file. It writes the proving key to $NAME.pk and $NAME.vk.

To supply the proving key to the prover:

valida prove --proving-key $NAME.pk $PROGRAM $PROOF [$INPUT]

To supply the verifying key to the verifier:

valida verify --verifying-key $NAME.vk $PROGRAM $PROOF

Universal vs. program-specific setup

When the program being executed is part of the statement being proven, this is called a universal setup. When the program is not part of the statement being proven, this is called a program-specific setup. By default, Valida uses a universal setup. To use a program-specific setup, pass the --program-specific flag to valida preprocess, valida prove, and valida verify:

valida preprocess --program-specific $PROGRAM $NAME
valida prove --program-specific --proving-key $NAME.pk $PROGRAM $PROOF $INPUT
valida verify --program-specific --verifying-key $NAME.vk $PROGRAM $PROOF

The universal setup is useful because it allows for the same verifier to verify proofs of execution for arbitrary programs. The program-specific setup is useful because it allows for more succinct statements which are easier to verify, due to the program being excluded from the statement.

Memory backends

The Valida zk-VM supports multiple memory backends, which have different time and space utilization characteristics. The memory backend can be selected by passing the --backend $BACKEND option to any of the zk-VM commands.

The following values of $BACKEND are supported:

• btree: a binary tree memory representation

• hashmap: a hash map memory representation

• array: a sparse array memory representation with a bit vector indicating which addresses have been set

• lean: a sparse array memory representation without a bit vector indicating which addresses have been set

To minimize space utilization for execution and proving, pick a btree or hashmap memory backend. To minimize execution time, pick an array or lean memory backend.

Advanced preprocessing options

The valida preprocess command takes the following options:

• --help: print usage instructions

• --show-preprocessed causes the preprocessed traces to be printed.

• --program-specific chooses a program-specific setup instead of a universal setup.

• --backend $BACKEND chooses $BACKEND as the memory representation.

Advanced execution options

The valida run command takes the following options:

• --help: print usage instructions

• --initial-fp $INITIAL_FP: sets the initial value of the frame pointer (fp) special purpose register to $INITIAL_FP

• --fast: turns off trace generation, reducing the time and space usage of the execution engine

• --program-specific: chooses a program-specific setup instead of a universal setup (affects trace generation only)

• --backend $BACKEND chooses $BACKEND as the memory representation.

Advanced prover options

The valida prove command takes the following options:

• --help: print usage instructions

• --initial-fp $INITIAL_FP: sets the initial value of the frame pointer (fp) special purpose register to $INITIAL_FP

• --program-specific: chooses a program-specific setup instead of a universal setup (affects trace generation only)

• --backend $BACKEND chooses $BACKEND as the memory representation.

• --show-public: shows the public inputs to the prover (i.e., the public traces)

• --show-preprocessed: shows the preprocessed inputs to the prover (i.e., the preprocessed traces)

• --show-main: shows the main traces (i.e., the non-public, non-preprocessed traces)

• --show-interactions: shows the interactions which go into the permutation argument

Advanced verifier options

The valida verify command takes the following options:

• --help: print usage instructions

• --claimed-output $OUTPUT: verifies that the output of the proven execution is $OUTPUT

• --initial-fp $INITIAL_FP: sets the initial value of the frame pointer (fp) special purpose register to $INITIAL_FP

• --program-specific: chooses a program-specific setup instead of a universal setup (affects trace generation only)

• --backend $BACKEND chooses $BACKEND as the memory representation.

• --show-public: shows the public inputs to the prover (i.e., the public traces)

• --show-preprocessed: shows the preprocessed inputs to the prover (i.e., the preprocessed traces)