PetraVM

PetraVM is a general-purpose virtual machine that is succinctly verifiable using the Binius proof system. The PetraVM execution model and instruction set are designed specifically for efficient proving with Binius. The VM is intended to handle several use cases simultaneously:

  1. recursive proof verification,
  2. general purpose computation, via compilation from WebAssembly, and
  3. high-performance verifiable computing use cases, using a custom high-level language called PetraML.

The VM consists of a basic instruction set and optional instruction set extensions. The arithmetization of the machine enables the prover and verifier to only handle the ISA extensions used by an agreed-upon program.

The full machine specification can be found here.

Documentation

Documentation is still incomplete and will be improved over time. You can go through the PetraVM book for explanations on the zkVM design and architecture.

Features

  • Binary field and arithmetic operations
  • Memory and control flow primitives
  • Efficient support for recursion
  • Write-once memory model (VROM)

Instruction Set

PetraVM's full instruction set is divided into five categories:

  • Binary field operations
  • Arithmetic & Logic operations
  • Memory operations
  • Control Flow instructions
  • Function Calls

Prover support for the full instruction set is a work in progress, tracked below.

The VM will also define a minimal ISA tailored for efficient recursion.

Expansion to include RAM-related instructions is kept for future work.

Prover Support (Work in Progress)

Note: In PetraVM, variables refer to addresses in VROM (Value ROM, a write-once memory region). Instructions operate on values at these addresses unless specified as "immediate" operations.

Note: Check out our instruction set test suite for a complete overview of supported instructions and their usage.

Binary Field Operations

  • B32_MUL - 32-bit binary field multiplication
  • B32_MULI - 32-bit binary field multiplication with immediate
  • B128_ADD - 128-bit binary field addition
  • B128_MUL - 128-bit binary field multiplication

Arithmetic Operations

  • ADD - Integer addition
  • ADDI - Integer addition with immediate
  • SUB - Integer subtraction
  • MUL - Signed multiplication
  • MULI - Signed multiplication with immediate
  • MULU - Unsigned multiplication
  • MULSU - Signed × unsigned multiplication

Logic Operations

  • AND - Bitwise AND
  • ANDI - Bitwise AND with immediate
  • OR - Bitwise OR
  • ORI - Bitwise OR with immediate
  • XOR - Bitwise XOR
  • XORI - Bitwise XOR with immediate

Shift Operations

  • SLL - Shift left logical
  • SLLI - Shift left logical with immediate
  • SRL - Shift right logical
  • SRLI - Shift right logical with immediate
  • SRA - Shift right arithmetic
  • SRAI - Shift right arithmetic with immediate

Comparison Operations

  • SLT - Set if less than (signed)
  • SLTI - Set if less than immediate (signed)
  • SLTU - Set if less than (unsigned)
  • SLTIU - Set if less than immediate (unsigned)
  • SLE - Set if less than or equal (signed)
  • SLEI - Set if less than or equal immediate (signed)
  • SLEU - Set if less than or equal (unsigned)
  • SLEIU - Set if less than or equal immediate (unsigned)

VROM Operations

  • LDI.W - Load immediate word
  • MVV.W - Move word between addresses
  • MVV.L - Move 128-bit value between addresses
  • MVI.H - Move immediate half-word

Control Flow

  • J - Jump to label or address
    • JUMPI - Jump to immediate address
    • JUMPV - Jump to address in variable
  • BNZ - Branch if not zero

Function Calls

  • CALLI - Call function at immediate address
  • CALLV - Call function at variable address
  • TAILI - Tail call to immediate address
  • TAILV - Tail call to variable address
  • RET - Return from function

Future Random-Access Memory Extensions

  • LW/SW - Load/Store word
  • LB/SB - Load/Store byte
  • LBU - Load byte unsigned
  • LH/SH - Load/Store halfword
  • LHU - Load halfword unsigned

Example Programs

The project includes several example programs that demonstrate the capabilities of PetraVM:

  • Fibonacci: Prove a Fibonacci number
  • Collatz: Prove the Collatz sequence for a given number

Running Examples

# Calculate and prove the 10th Fibonacci number
RUSTFLAGS="-C target-cpu=native" cargo run --release --example fibonacci -- -n 10

# Run Collatz conjecture for starting value 7
RUSTFLAGS="-C target-cpu=native" cargo run --release --example collatz -- -n 7

Development Status

The project is actively developed. Many instructions are already supported by the prover, with new instructions and additional features added regularly.

Crates

  • assembly: zkVM assembly DSL, parser and program executor
  • prover: Circuit definition and proof generation

License

Licensed under Apache 2.0. See LICENSE.

Contributing

The PetraVM project is a collaboration between several teams and welcomes community contributions. Please open issues or pull requests for bugs, features, or improvements. See the CONTRIBUTING document for guidelines.

The initial development is led by Polygon and Irreducible.

We reserve the right to close issues and PRs deemed unnecessary or not bringing sufficient interest.