Valida ISA Spec, version 1.0: A zk-Optimized Instruction Set Architecture

TL;DR

Valida ISA v1.0 targets zkVMs to enable efficient, succinct proofs of program execution by using a registerless, stack-addressed Harvard architecture that minimizes proving work relative to traditional hardware ISAs. The paper provides a rigorous semantic framework: a formal program/state model, an initial-state function, a multi-chip transition function, and a result function, all designed to be a precise starting point for formalization and verification. It details a comprehensive chip-wise instruction set, including memory, I/O, and arithmetic/logic operations, along with a robust fetch/update scheme that drives CPU, Memory, and Output transitions under a uniform transition model. The specification aims to support implementing Valida runtimes and compiler toolchains, enabling correct, verifiable zkVM execution and serving as a foundation for formal verification efforts in succinct-proofs ecosystems.

Abstract

The Valida instruction set architecture is designed for implementation in zkVMs to optimize for fast, efficient execution proving. This specification intends to guide implementors of zkVMs and compiler toolchains for Valida. It provides an unambiguous definition of the semantics of Valida programs and may be used as a starting point for formalization efforts.

Figures (5)

• Figure 1: The chips in the basic Valida machine.
• Figure 2: The Valida opcodes (1 of 2).
• Figure 3: The Valida opcodes (2 of 2).
• Figure 4: Binary function opcodes (1 of 2)
• Figure 5: Binary function opcodes (2 of 2)