Valida zk-VM

Background

Valida zk-VM originated as a pioneering cryptography research project at Delendum Research, where it was initially conceptualized and designed. The project's inception was driven by the ambition to create a cutting-edge, secure, and efficient zero-knowledge virtual machine that could support a wide range of cryptographic operations and applications. Following its initial research and development phase at Delendum Research, the project was further developed by Lita, alongside a dedicated team of open-source contributors, including but not limited to Daniel Lubarov, Max Gillett, and Tamir Hemo. This collaborative effort is turning the Valida zk-VM into a robust and versatile platform that serves as a foundation for secure, privacy-preserving computations.

Through its evolution, Valida zk-VM has garnered attention and adoption across various sectors, marking its significance in the field of cryptography and secure computing. The codebase for Valida zk-VM is maintained under an open-source license, facilitating a transparent and collaborative development environment. This approach encourages contributions from a global community of developers and researchers, continuously enriching the project's capabilities and applications. Valida zk-VM's journey from a research concept to a fully realized, production-grade virtual machine highlights its innovative essence and the collective effort of its contributors.

What is Valida?

1. An instruction set architecture (ISA) designed to be:

   • a good target language for modern compilers and programming languages, and

   • a good ISA for zk-VMs.

2. A zk-VM implementation in Rust, based on Plonky3, which implements the Valida ISA. This includes:

   • an execution engine which can run Valida programs in a virtualized environment;

   • a prover which can generate succinct proofs of execution of Valida programs; and

   • a verifier which can verify the proofs generated by the prover.

Valida aims to provide the fastest, most efficient generation of succinct and zero knowledge proofs of program execution (ZKPs). Hardware and zk-VMs are two implementation contexts which are substantially different. Therefore, an ISA optimized for hardware implementation cannot be optimized for zk-VM implementation, and vice versa. This is why the Valida zk-VM implementation is based on a new ISA instead of a pre-existing ISA designed for hardware. This helps Valida to achieve more efficient proof generation, at the cost of requiring new compiler technology to be developed.

Valida Instruction Set Architecture (ISA)

A modular instruction set architecture

• Open ended set of chips

• Each chip provides its own instruction set

• Ultra-RISC control unit chip

• 32-bit ALU chips

• Separate 32-bit program ROM and data RAM chips

• A RAM chip which holds (2^31 - 2^27) / 8 = 0xF000000 words (32 bits each).

Designed to be friendly for implementation in zero knowledge virtual machines (zk-VMs), specifically via STARKs over small fields.

Valida has two special-purpose registers:

1. pc: program counter

   • at end of instruction execution, holds the address of the next instruction to run

2. fp: frame pointer

   • holds the address of the start of the stack frame

Valida has no general purpose registers

• Instead, instructions reference stack operands directly

• A stack operand is referenced as a constant offset from fp

Access to special-purpose registers is via special-purpose opcodes only

• The values of fp and pc can be read into stack operands via LOADFP and JAL opcodes

• pc can be written via a branch instruction

• One can add an integer offset to fp but this is the only way to set the value of fp

Diagram of a basic Valida VM

Valida Implementation

• Valida’s implementation provides a framework for generating Valida VMs and provers using included and user-provided chips and compile-time parameters

• Application developers can use the included compile time macros to generate, with a little coding, a Valida VM and prover based on a chip set customized for their use case

• The Valida implementation is experimental and dual Apache / MIT licensed

The Valida zk-VM implementation is available to the public. Lita is still working on some known issues with the Valida zk-VM implementation affecting correctness and completeness of the prover / verifier pair, including:

1. The memory argument is not fully sound.

2. The following arithmetic operations are unconstrained or wrongly constrained:

   • DIV32 (32-bit unsigned division),

   • MULHU32 (32-bit unsigned multiply, high bits only), and

   • MULHS32 (32-bit signed multiply, high bits only).

   • SRA32 (32-bit signed arithmetic right shift)

   • SHL32 / SRL32 (32-bit unsigned right / left logical shifts)

3. The following opcodes need to be implemented:

   1. LOADS8 (8-bit sign-extending load)

   2. LE32 / GE32 (32-bit non-strict unsigned inequality comparisons)

   3. SLT32 / SGT32 (32-bit strict signed inequality comparisons)

   4. SLE32 / SGE32 (32-bit non-strict signed inequality comparisons)

4. The consistency of the program ROM with the trace is not being checked.

5. There are some under-constrained equality tests.

6. The 8-bit range checker chip is not constrained.

7. The verifier needs to check the commitments to the preprocessed trace columns.

8. There are some missing range checks, such as in the CPU chip when the third operand is an immediate operand.

9. There needs to be randomness added to the permutation arguments.

All of the known non-working and missing constraints are in the process of being added or replaced, or they are planned to be added or replaced in the near future. None of these appear particularly risky, either from a timeline or performance standpoint, in that workable approaches are known for all of them and we as Lita Foundation expect some of these to be reasonably performant.

We as Lita Foundation are internally auditing the Valida zk-VM. We will report any issues we find, as we find them. We also plan to submit Valida for a third party external audit.