Hello World

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

machine HelloWorld {

    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= ${ ("input", 0) };
        A <== incr(A);
        A <== decr(A);
        assert_zero A;
        return;
    }
}

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

powdr pil hello_world.asm --field bn254 --force --inputs 0 --prove-with halo2

We observe that a proof was created at proof.bin. Now let's try for the invalid input 1

powdr pil hello_world.asm --field bn254 --force --inputs 1 --prove-with halo2

We observe that witness generation fails, and no proof is created.