Experimental VM-based compilation to VampIR

[lukaszcz]

Implemented

• Adds a vampir-vm target which compiles to a VM run on top of VampIR (the VM is compiled to a circuit, specialized to the particular Juvix program).
• Introduces JuvixVM assembly bytecode (Juvix/Compiler/VM) with a parser and an interpreter. Similar to JuvixAsm/JuvixReg, but simpler, more "primitive", and thus easier to write an interpreter for in VampIR.
• VampIR runtime to execute (interpret) JuvixVM bytecode (runtime/src/vampir/vm.pir).
• Translation from JuvixVM to VampIR.
• Partial translation from JuvixReg to JuvixVM. In combination with the JuvixVM -> VampIR translation, this enables a Juvix -> VampIR VM pipeline. Some features are not supported, notably closures.

Not done and not planned

• Support for closures (requires JuvixVM runtime implementing general closure call with JuvixVM instructions). Clear how to do, but tedious engineering work.
• Pretty printing of JuvixVM code (useful only for debugging).
• Division and modulus require Feature request: a non-crashing modulo operation vamp-ir#113, otherwise they're too slow.

Conclusion

The approach is to translate to a VM that is compiled into a circuit. This doesn't seem feasible in practice. The efficiency of this solution is prohibitively poor and it's not clear how to substantially improve it.

It seems that zkVMs typically don't execute on circuits. They consist of an optimized executor which executes the program and generates an execution trace. A separate prover then checks and proves the validity of the execution trace, outputting a witness which can be independently verified. Hence, only the validity of the execution trace is subject to proof/verification. The VM is a conventional VM run natively, except that it generates an appropriate execution trace. Encoding a VM into a circuit seems completely infeasible.

See: Building a zkVM application

Possible future work

The JuvixVM language could potentially be used as a basis for an optimized low-level implementation of a VM generating appropriate execution traces.

[lukaszcz]

Since this doesn't work in practice at present, we defer the PR. See Deferred Pull Requests.