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.

Public input

In Valida proofs of execution, the outputs are public (i.e., part of the statement being proven), and the inputs are non-public (i.e., not part of the statement being proven). Since Valida is not yet a zero knowledge proof system, the inputs cannot be assumed to be private, but they are not explicitly specified in the proof or the statement being proven.

If some of the input to the program should be public (i.e., part of the statement being proven), then this can be accomplished by echoing the part of the input onto the output. It is the responsibility of the application developer to do this if a public input is required.

If it is necessary to prove a relation between the input and the output, then the input must be public. For example, suppose a program computes elements of the Fibonacci sequence, proving statements of the form "the nth Fibonacci number is m." Suppose the input to the program is n. Then the program must echo the input n into its output, as well as outputting m. Otherwise, if it just outputs m, then it will prove statements of the form "m is a Fibonacci number."

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 -o $OUTPUT

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 -o $OUTPUT

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: same as -o, 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)