Implement Non-deterministic VM (Brillig)

[kevaundray]

Problem

Currently we use Directives to simulate non-determinism in ACVM.

This can be seen with, for example, Directives::Inverse which will indicate to the prover that they should compute the inversion of witness value outside of the circuit and set it as the value for a particular witness index.

These directives do one thing and so they are restrictive in scope. If we want the prover to, outside a circuit, run a for-loop over an arbitrary amount of values, then we currently have no way to direct them to do this.

Proposed solution

We generalize our Directives into a set of opcodes or instructions for a small VM.

This VM will be known as Brillig, because @jfecher was reading the Jabberwocky poem while we were formulating the idea.

We first need to introduce Brillig as a Directive to ACIR, hence, we add the following:

Directive::Brillig {
   inputs : Vec<Expression>,
   outputs: Vec<Witness>,
   bytecode: Vec<Opcode>,
}

This looks very similar to our current directives with the only difference being that we execute the bytecode in order to figure out the output.

Once the VM has executed the bytecode on the inputs, the state of the registers will be extracted in order to assign those values to the output witnesses.

Alternatives considered

No response

Additional context

This is a tracking issue, all issues related to this should reference this issue.

We will define the set of opcodes in a separate issue.

Submission Checklist

• Once I hit submit, I will assign this issue to the Project Board with the appropriate tags.

[kevaundray]

This is somewhat of a retroactive issue as we do have a hacked together version of Brillig already. We want to have documentation, specs and also we want to remove the Bootstrap opcode that was added.

[kevaundray]

Tagging @iAmMichaelConnor for visibility

[kevaundray]

Tagging @ludamad who will be working on this too

[kevaundray]

Closing as #152 has been merged