Hello World

Let's write a minimal VM and generate a proof!

machine HelloWorld with degree: 8 {
    // this simple machine does not have submachines

    reg pc[@pc];
    reg X[<=];
    reg Y[<=];
    reg A;

    instr incr X -> Y {
        Y = X + 1
    }

    instr decr X -> Y {
        Y = X - 1
    }

    instr assert_zero X {
        X = 0
    }

    // the main function assigns the first prover input to A, increments it, decrements it, and loops forever
    function main {
        A <=X= ${ std::prelude::Query::Input(0, 1) };
        A <== incr(A);
        A <== decr(A);
        assert_zero A;
        return;
    }
}

Let's generate a proof of execution for the valid prover input 0 (since 0 + 1 - 1 == 0)

powdr pil test_data/asm/book/hello_world.asm --field bn254 --inputs 0 --prove-with halo2

We observe that several artifacts are created in the current directory:

  • hello_world.pil: the compiled PIL file.
  • hello_world_opt.pil: the optimized PIL file.
  • hello_world_constants.bin: the computed fixed columns which only have to be computed once per PIL file.
  • hello_world_commits.bin: the computed witness which needs to be computed for each proof.
  • hello_world_proof.bin: the ZK proof!

Note that the output directory can be specified with option -o|--output, and . is used by default.

Now let's try for the invalid input 1:

powdr pil test_data/asm/book/hello_world.asm --field bn254 --inputs 1 --prove-with halo2

In this case witness generation fails, and no proof is created.

Setup & Verification

The example above omits some important steps in proof generation: Setup and Verification key generation. Some proof systems, such as Halo2 (and other SNARKs), require a Setup to be performed before the proof. Such Setup can be specific to the program or universal, where its artifact is a binary usually called parameters or params. STARKs do not require a previous Setup.

Another step required before the proof is computed is key generation. A proving key and a verification key are generated taking into account the constraints and potentially Setup parameters. The proving key is used by the prover to generate the proof, and the verification key is used by the verifier to verify such proof. A single verification key can be used to verify any number of different proofs for a given program.

Therefore, when computing a proof, it is important that the Setup parameters and the verification key are also available as artifacts.

Below we reproduce the same proof as in the example above, keeping the artifacts needed for verification:

First we run the Setup, where the number given must match the degree of our source file (degree 8). The command below generates file params.bin.

powdr setup 8 --backend halo2 --field bn254

We can now compute the verification key, output in vkey.bin:

powdr verification-key test_data/asm/book/hello_world.asm --field bn254 --backend halo2 --params "params.bin"

The command above can read previously generated constants from the directory specified via -d|--dir, where . is used by default. If the constants are not present it computes them before generating the verification key.

The next command compiles and optimizes the given source, generating the file hello_world_opt.pil. It also computes both the fixed data and the witness needed for the proof, stored respectively in hello_world_constants.bin and hello_world_commits.bin.

powdr pil test_data/asm/book/hello_world.asm --field bn254 --force --inputs 0

We can now generate the proof:

powdr prove test_data/asm/book/hello_world.asm --field bn254 --backend halo2 --params "params.bin" --vkey "vkey.bin"

The proof can be verified by anyone via:

powdr verify test_data/asm/book/hello_world.asm --field bn254 --backend halo2 --vkey "vkey.bin" --params "params.bin" --proof "hello_world_proof.bin"

Note that CLI proof verification works analogously for eSTARK, without the setup step and using the Goldilocks field instead of Bn254.

Another aspect that was omitted in this example is the fact that this proof uses a Poseidon transcript and cannot be verified in a cheap way on Ethereum, even though we can verify it efficiently via powdr. There are two ways to enable verification on Ethereum:

  1. Use a different transcript when generating this proof. See section Hello World on Ethereum for the same example targeting EVM verification.
  2. Use proof aggregation to compress the proof we just generated using a circuit that can be verified on Ethereum. See section Hello World on Ethereum via proof aggregation to learn how to do that.