Hello World on Ethereum

This example is a variation of the previous Hello World, targeting verification on Ethereum. In this example we will cover how to generate proofs directly using a Keccak transcript instead of the Poseidon transcript of the previous example, which will enable us to verify proofs onchain. There are almost no differences from the CLI perspective.

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;
    }
}

Since the following command creates a proof, a Solidity verifier, and verifies the proof on the EVM, we need to have solc available in the system. One easy way to install it is by using svm.

powdr pil test_data/asm/book/hello_world.asm --field bn254 --inputs 0 --prove-with halo2 --backend-options "snark_single" -f --params params.bin

The extra parameter --backend-options snark_single tells powdr to produce a single SNARK that uses Keccak. The option -f forces overwriting the compiled files that have been generated before, which is useful if you are running the examples on the same directory as the previous example.

When the a proof is generated, it is verified on a simulated EVM transaction as well!

Verifying SNARK in the EVM...

We can observe again that a proof was created at hello_world_proof.bin.

Now we can generate a Solidity verifier, using the same setup (params) as the previous example:

powdr export-verifier test_data/asm/book/hello_world.asm --field bn254 --backend halo2 --backend-options "snark_single" --params params.bin

A Solidity file verifier.sol is generated. You can verify the same proof that we just generated by passing it to the contract together with the public inputs (which we have not used so far).

Note that the more complex your VM is, the larger the verifier contract will be. In some cases, it might exceed Ethereum's contract size limit. You can mitigate that by using proof recursion on proofs that use Poseidon transcripts. See the next section for details.