Installation

There are two ways to install this toolchain: via Docker, or via this Linux release bundle.

Docker-based installation

We provide a Docker container with the Valida LLVM and Rust toolchains already installed. This is supported on any platform which supports Docker, including recent versions of MacOS and Windows. Docker is the only supported method of running on platforms other than x86 Linux.

x86_64-based platforms

To install and use the toolchain via Docker on a 64-bit computer with an Intel-compatible chipset (x86_64), such as Intel- or AMD-based computers:

# Download the container
docker pull ghcr.io/lita-xyz/llvm-valida-releases/valida-build-container:v0.8.0-alpha-amd64

# cd your-valida-project

# Enter the container:
docker run --platform linux/amd64 -it --rm -v $(realpath .):/src ghcr.io/lita-xyz/llvm-valida-releases/valida-build-container:v0.10.0-amd64

# You are now in a shell with the valida rust toolchain installed!

ARM64-based platforms

To install and use the toolchain via Docker on a 64-bit computer with an ARM64-compatible chipset (ARM64), such as Apple silicon-based computers:

# Download the container
docker pull ghcr.io/lita-xyz/llvm-valida-releases/valida-build-container:v0.10.0

# cd your-valida-project

# Enter the container:
docker run --platform linux/arm64 -it --rm -v $(realpath .):/src ghcr.io/lita-xyz/llvm-valida-releases/valida-build-container:v0.10.0

# You are now in a shell with the valida rust toolchain installed!

Linux-based installation

This section describes installation on Ubuntu 24.04 LTS, and other compatible Linux-based systems.

System requirements

This toolchain installation method supports x86_64 Linux based on glibc-2.9 or newer glibc.
rustup is required.
Arch Linux and Ubuntu 24.04 LTS are specifically supported, with other platforms possibly requiring some tinkering to make work.

Download

To download the Linux-based release bundle:

wget https://github.com/lita-xyz/valida-releases/releases/download/v0.10.0/llvm-valida-v0.10.0-linux-x86_64.tar.xz

Installation

First create a folder called /valida-toolchain and give your user permissions on it:

sudo mkdir -p /valida-toolchain
sudo chown $(whoami):users /valida-toolchain

From the untarred release bundle, in the directory called valida-toolchain, the same directory containing these release notes, run:

./install.sh

Entering the Valida shell

Upon having installed the toolchain, the Valida shell should be on your PATH, and if you run which valida-shell, you should see something like:

/home/morgan/.local/bin/valida-shell

If the result is very different from this, then either the installation did not complete successfully, or you had another executable named valida-shell somewhere on your PATH.

If you run valida-shell, then you should see a shell prompt that reads valida> . You should then have on your PATH all of the executables from the Valida toolchain needed to follow the usage instructions below.

Usage instructions

Compiling and running Rust programs

For examples of how to build a Rust program which compiles and runs on Valida, see lita-xyz/rust-examples on GitHub. You can use any of these examples as a starting point for developing your own programs using the Valida toolchain. Here are steps for doing so:

Clone the project template:

git clone https://github.com/lita-xyz/fibonacci.git

cd into the project template:

cd fibonacci

Build the project:

cargo +valida build

Run the code (taking input from stdin):

valida run --fast target/valida-unknown-baremetal-gnu/debug/fibonacci log

Prove the execution (taking input from stdin):

valida prove target/valida-unknown-baremetal-gnu/debug/fibonacci proof

Verify the proof:

valida verify target/valida-unknown-baremetal-gnu/debug/fibonacci proof log

You can control the tradeoff between prover space and time complexity, on the one hand, and proof size and verifier complexity, on the other hand, by adjusting the max segment size. The max segment size will determine the largest possible trace height for each segment. If you want to specify the max segment size, pass the --max-segment-size option to valida prove and valida verify, as in this example:

valida prove --max-segment-size 10000 target/valida-unknown-baremetal-gnu/debug/fibonacci proof
valida verify --max-segment-size 10000 target/valida-unknown-baremetal-gnu/debug/fibonacci proof log

The default segment size is 2^20 == 1048576.

You can also control the the CPU usage by modifying the number of segments that can be proved in parallel by modifying:

--max-parallel-segments

For example:

valida prove --max-parallel-segments 3 program proof input

Using the Valida Rust API

The Valida Rust API streamlines the process of invoking the Valida VM from within Rust programs. See the Rust docs and the example for details on how to use it.

Using the Valida client-side API

The Valida client-side API enables creating and verifying Valida proofs of execution within the browser. This enables use cases which require proofs to run on the client side in web apps.

To use the Valida client-side API, you can start by copying the example project which is located in the installed toolchain at /valida-toolchain/examples/wasm/client-side-example.

You will need to embed your guest program (the one whose execution you wish to prove) in your client-side code. You can do this by taking the compiled guest program, base64 encoding it, and ingesting it using Webpack. The compiled guest program is located in target/valida-unknown-baremetal-gnu. For example, after you run cargo +valida build --release on your guest program called program, the compiled guest program is located at target/valida-unknown-baremetal-gnu/release/program.

Supposing the compiled program is located at ./program, to base64 encode it, you could run the following command: base64 program >program.base64.

The example project illustrates how to ingest the compiled, base64-encoded program into a client-side app. This is accomplished using the following rule in webpack.config.js:

  module: {
    rules: [
      {
        test: /\.base64/,
        type: 'asset/source',
      }
    ]
  }

With this rule in place, the base64-encoded program can be imported as simply as:

import programBase64 from "./program.base64";

To import the Valida prover, use a line like:

import * as valida from "valida-basic-api-wasm";

For this to work, valida-basic-api-wasm will need to be included in your package.json. Once you have done this, valida is an object containing methods with the following type signatures:

export function run(program_bytes: Uint8Array, stdin: Uint8Array, max_trace_height: number): Uint8Array;
export function prove(program_bytes: Uint8Array, stdin: Uint8Array, max_trace_height: number, max_parallel_segments: number): Uint8Array;
export function verify(program_bytes: Uint8Array, stdout: Uint8Array, proof: Uint8Array, max_trace_height: number): void;

The max_trace_height is in other words the max segment size. This parameter is not optional in the WASM API. The max_parallel_segments is the number of threads that are going to be initiated for parallel proving.

Writing Rust programs to run on Valida

For a starting point to build a project using the Rust Valida toolchain, you can create a Rust project using cargo new. You should be able to write Rust programs more or less
as normal. There are a few limitations to keep in mind:

All of the usual operating system facilities are unavailable, except for standard in (stdin)
and standard out (stdout). So for example, there is no access to command line arguments,
environment variables, networking, or the filesystem.
Multi-threading is not supported.
Interactive programs may not work as expected.

An example

Here is an example program using Valida, which computes Fibonacci numbers:

use std::io::stdin;

pub fn main() {
    println!("Please enter a number from 0 to 46:");
    let n = loop {
        let mut input = String::new();
        // Read a line from stdin and parse it as an u8.
        match stdin().read_line(&mut input) {
            Ok(_) => {
                match input.trim().parse::<u8>() {
                    Ok(num) => {
                        if num == 0 {
                            println!("The 0th fibonacci number is: 0");
                            return;
                        } else if num > 46 {
                            println!("Error: n is too large. Please enter a number no larger than 46.");
                        } else {
                            break num;
                        }
                    },
                    Err(e) => {
                        println!("Error reading input: {}. Please try again:", e);
                    }
                }
            }
            Err(e) => {
                println!("Error reading input: {}. Please try again:", e);
            }
        }
    };
    let mut a: u32 = 0;
    let mut b: u32 = 1;
    let mut sum: u32;
    for _ in 1..n {
        sum = a + b;
        a = b;
        b = sum;
    }
    println!("The {}-th fibonacci number is: {}", n, b);
}

More examples

The following examples are available under /valida-toolchain/examples/rust:

conway: Conway's game of life
ed25519: ECDSA Ed25519 signature verification
factorial: The factorial function
fibonacci: The Fibonacci sequence
fizzbuzz: The classic fizz-buzz interview problem
grep: Search text for a substring
guessing_game: An interactive number guessing example
hello_world: The classic "hello world" example
json_contains: JSON parsing and property fetching
keccak-crate: Computes a Keccak hash
palindrome: Test if a string is a palindrome
prime_factorization: Check prime factorization
secp256k1: ECDSA Secp256k1 signature verification
sha256: SHA-256 hashing
simple_calculator: A simple calculator app
sudoku: Checking solutions to Sudoku problems
unit_tests: A suite of tests of basic language functionality

The reva example executes Ethereum blocks in Valida. This is a work in progress and may produce results that are incorrect. This is plausibly the most complex program that has been run in Valida so far.

Using Keccak acceleration

The Valida VM has the capability of accelerated Keccak hash proving. To use this capability in Rust, you can simply import sha3::Keccak256 and use the Keccak hasher in the sha3 crate in the usual way. The keccak-crate example located at /valida-toolchain/examples/rust/keccak-crate exemplifies this usage. You must use Lita's forked version of the Keccak crate, using a line in your Cargo.toml such as:

[dependencies]
sha3 = { git = "https://github.com/lita-xyz/hashes", default-features = false }

Compiling and running C programs

See /valida-toolchain/examples/c/ for some examples of C programs which can be compiled and run on Valida. Here is an example C program from this release bundle, called /valida-toolchain/examples/c/cat.c:

#include <stdio.h>

const unsigned EOF = 0xFFFFFFFF;

int main() {
    unsigned c = 0;
    while (1) {
        c = getchar();
        if (c == EOF) {
            break;
        } else {
            putchar(c);
        }
    }
}

To compile, for example, the cat.c example, after installing the toolchain, and with the toolchain on your PATH (such as, in the valida-shell or in the Docker container shell):

clang -target valida /valida-toolchain/examples/c/cat.c -o cat
valida run cat log

Once running, the cat example will wait for input. After you are done providing input, press ctrl+D. The program should echo back what you wrote, writing its output to log.

Compiling and running the other examples follows the same procedure, substituting $NAME for the name of the example:

clang -target valida /valida-toolchain/examples/${NAME}.c -o ${NAME}
valida run ${NAME} log

Some other C examples that are provided in this release bundle:

reverse.c will output its reversed input.
checksum.c will output a checksum, i.e., a sum of the characters, of its input.
merkle-path.c will verify an opening proof for a SHA256 binary Merkle tree
- For an example proof you can use as input, see examples/example-merkle-proof
sha256.c will output a SHA-256 hash of the first 256 bytes of its input.
sha256_32byte_in.c will output the SHA-256 hash of a constant array of 32 bytes. This is used as a benchmark.

Using `libc`

There is a partial libc for Valida, bundled with this release. This libc is a version of LLVM libc.

There is an example, /valida-toolchain/examples/cat-alpha.c, which makes use of this libc. This example echoes all of the alphabetic characters in its input. It makes use of the libc function isalpha. The following commands, run from this directory, should compile and run this example:

clang -target valida /valida-toolchain/examples/cat-alpha.c -o cat-alpha
valida run cat-alpha log

See the docs for more details on using the bundled version of libc for Valida.

LLDB & The Debug Server

/valida-toolchain/bin/valida-lldb-server

This should provide an output stating which port the debug server is listening for connections on.

Then run the debugger, from the same directory, with the command:

/valida-toolchain/bin/valida-lldb --remote-port <server port> --valida-exec <path to executable> --in-tape <input tape> --out-tape <output tape>

This will attach to the server and run the commands to prepare to debug the given executable. Execution cannot be started using run, but the server is ready to start stepping through the program. Use stepi to step one instruction at a time, next to step a source line, step to step into a function call, break and continue to set and run until hitting a breakpoint. Currently finish is not working.

Reporting issues

If you have any issues to report, please report them at the llvm-valida-releases issue tracker. Please include the following elements in your bug report: what release version you encountered the bug on, steps to reproduce, expected behavior, and actual behavior.

Known issues

The prover is unsound, which means that verifying a proof does not provide completely convincing evidence that the statement being proven is true. This will be resolved once some missing constraints are added.
There are some issues with reading input interactively using Rust standard I/O functions. Under some circumstances, pressing ctrl+D to signal end of input may need to be done more than once, when it should only need to be done once.

Changelog

v1.0.0

zk-VM

Supports parallel proving for multi-segment proofs
Supports an optional, configurable parameter to select the number of segments to prove in parallel
Speed up for fast run option via bug fixing
Added boolean constraints for opcode flags in the CPU trace
Added consistency check between program trace and opcode flags in the CPU trace
Added check that last instruction is STOP (fixed a regression bug)

Compiler toolchain

Adds LLDB debugger support
Optimizes codegen for branching on equality
Enables operand folder to operate across basic block boundaries

Acknowledgements

Thanks to Hideaki Takahashi at Columbia University for pointing out and fixing three soundness-related bugs: the CPU opcode flag boolean checks and program consistency checks, and the last instruction is STOP.

v0.10.0

zk-VM

Supports proving long executions using multi-segment proofs
Supports an optional, configurable segment size parameter to adjust the trade-off between prover space & time complexity vs. proof size & verifier complexity
Experimental memcpy opcode added to the execution engine (but not the prover / verifier)
Experimental Secp256k1 curve opcodes added to the execution engine (but not the prover / verifier)
Reduced memory usage and improved performance in the prover
Commit to public traces

Compiler toolchain

Updated Rust language version to 1.86.0
Updated LLVM version to 18.1.7
A majority of the unit tests for the Rust standard library now run and pass in Valida
Fixes to floating point support (using software emulation)
Improved randomness support in Rust using the experimental core::random
Added stddef.h include to stdio.h
Match Rust ABI for struct passing / returning in C
Change ABI alignment to fix variadics
Experimental memcpy opcode added to the compiler; ExpandMemCpy operation disabled when it is enabled
Experimental Secp256k1 opcodes added to the compiler
Refactor call, call indirect and ret to late expansion pseudos
Indicate that we do not support dynamic stack realignments
Fix compilation on GCC15 libstdc++
Handle llvm.threadlocal.address intrinsic by removing it

reva

Use ciborium instead of serde_json in client-eth
Use tiny-keccak

v0.9.0-alpha

zk-VM

Added Keccak permutation chip
Removed support for memory backends other than HashMap

Compiler toolchain

Added support for accelerated Keccak hashing using the Keccak permutation chip
Added the Valida API, which supports calling the prover, verifier, and execution engine as Rust methods
Added support for client-side proving and proof verification in Web browsers
Turned on link time optimization (LTO) in default Rust release build profile
Bugfixes in and improvements to compiler optimization pathways
The x86 Linux native toolchain installer no longer requires to be run as root

v0.8.0-alpha

Core WASM support
Valida API: provides programmatic access to the Valida execution engine, prover, and verifier
AVX-2 support for accelerated proving
Increased VM heap size to 512MB
Expanded standard I/O support for Rust and C
- Read functions in Rust
- printf in C
Improvements to Valida command line interface (CLI)
Added support for alloca.h C header file
valida run writes to output file in real time instead of in batch mode

v0.7.0-alpha

Valida zk-VM

ARM64 binary distribution of prover / verifier via Docker
Bugfix for valida run --fast
Bugfix for writing output in the VM

Compiler toolchain

ARM64 binary distribution of toolchain via Docker
Expanded support for Rust standard I/O functions
Added support for compiling floating point arithmetic to Valida via software emulation
Added proof of concept support for WASM: example at /valida-toolchain/examples/wasm.
- Can compile WASM programs which compute functions from a single integer to a single integer
- More comprehensive WASM support is in progress but not included in this release

v0.6.0-alpha

Valida zk-VM

More constraints added in, bringing the prover closer to soundness
- Signed 32-bit division constraints
- JALV (jump to variable and link) constraints
- Fixes for interpolating public traces
- Fixes for reading from an address which is not previously written to
Added a zk-VM binary which is compiled with support for logging timing data to standard out

Compiler toolchain

Support for certain Rust standard I/O functions and macros like println!
Removed support for Valida-specific I/O functions
Support for 64-bit atomics
Support for link time optimization via the -flto flag
Provide a useful error message when unrecoverable errors occur in Valida program execution, such as in the cases of:
- A failed assertion in Rust
- A failed malloc in C
Fixes for immediate value handling in the disassembler
Examples and their test scripts are bundled in release, instead of referenced in a public repo
- Currently, example test script requires sudo to run from release bundle
Replace references to "delendum" with "valida"

Docs

Specify --claimed-output
Simplified usage for libc
Removed references to valida-c-examples and valida-rust-examples repos
Added a tutorial
Use Rust standard I/O

v0.5.0-alpha

Valida zk-VM

Resolves all known issues with prover completeness
- Executions that are shorter than the segment size can be proven.
- Proofs of execution can be verified.
Adds or fixes STARK constraints for MULHS, bit shifts, and single-byte memory operations
Enables proving subtractions with borrowing
Fixes a bug in the execution engine which incorrectly resulted in non-termination for programs using division opcodes

Compiler toolchain

Improvements to valida-rs Rust support crate
- Additional I/O functions: read, write, and read_and_deserialize
- Use little endian for serialization / deserialization
Passes an expanded Rust test suite

v0.4.0-alpha

Valida zk-VM

Passes an expanded test suite
Makes valida run much faster, and enables arbitrary length executions in valida run
Adds a mostly-complete memory argument
Checks consistency of fetched instructions with program ROM
Change order of reads during STORE instruction to match STARK constraints
Improved ELF executable file loader
The verifier no longer attempts to re-execute the program
Uses little endian consistently
Fixes STARK constraints for many ALU instructions
Supports the ability for the program to be included in the instance data or not
Adds missing STARK constraints for the program counter
Adds a separate preprocessing stage and the ability to read setup data from a file
Execution engine supports reading memory which has not been previously written, which results in zero
Exposes initial register values as instance data

Compiler toolchain

Passes an expanded test suite
Supports building Rust projects via cargo build
Supports dynamic memory management in C: malloc, free, calloc, realloc, aligned_alloc
Enables use of -O3
Supports variadic arguments
Uses stack allocation to lower constant pool nodes
Fixed bugs in the disassembler
Corrected calling convention when returning 64-bit integers
Fixes to 64-bit arithmetic
Enables DAGCombiner
Fixed truncload / extstore handling when addr is FPMemOpnd
Strips atomics and thread local storage attributes
Enables operand folder for some opcodes
Fixes by value argument passing in calling convention
Emits IMM32 instructions to represent immediate operands outside the field size
Improves linker script

v0.3.0-alpha

Valida

Completed the output chip, resulting in more executions being provable
Added support for public / instance data in the prover and verifier
Completed the 8-bit range check chip and used it in some relevant places
Added a general-purpose lookup argument, which is used in the range check chip
Fixed loading of .bss sections in ELF executable files
Pre-compute the preprocessed traces, instead of computing them each time the prover or verifier runs

LLVM-Valida

Added partial Rust support, including:
- The ability to compile a subset of Rust to LLVM IR and then to Valida object code
- The ability to link Rust code compiled for Valida with C code compiled for Valida
- Example programs using basic computation and I/O
Added partial LLVM libc support, including:
- A subset of libc header files, bundled with the release and customized for the LLVM Valida compiler backend
- A linkable object code library (libc.a) compiled to run on Valida
- An example program using isalpha
Bugfixes in the code generation backend, including:
- Removed a pattern that prevented insertion of loadfp
- Refined type legalization
- Disabled tail call optimization
- Fixed endianness related issues
- Disabled branch analysis
- Fixed FP alignment
- Disabled generating jump tables

Valida toolchain 1.0.0

Installation

Docker-based installation

x86_64-based platforms

ARM64-based platforms

Linux-based installation

System requirements

Download

Installation

Entering the Valida shell

Usage instructions

Compiling and running Rust programs

Using the Valida Rust API

Using the Valida client-side API

Writing Rust programs to run on Valida

An example

More examples

Using Keccak acceleration

Compiling and running C programs

Using libc

LLDB & The Debug Server

Reporting issues

Known issues

Changelog

v1.0.0

zk-VM

Compiler toolchain

Acknowledgements

v0.10.0

zk-VM

Compiler toolchain

reva

v0.9.0-alpha

zk-VM

Compiler toolchain

v0.8.0-alpha

v0.7.0-alpha

Valida zk-VM

Compiler toolchain

v0.6.0-alpha

Valida zk-VM

Compiler toolchain

Docs

v0.5.0-alpha

Valida zk-VM

Compiler toolchain

v0.4.0-alpha

Valida zk-VM

Compiler toolchain

v0.3.0-alpha

Valida

LLVM-Valida

Uh oh!

Using `libc`