Skip to content

Valida toolchain v0.6.0-alpha
Compare
Choose a tag to compare
@morganthomas morganthomas released this 01 Dec 07:11
· 8 commits to main since this release
v0.6.0-alpha
7bb1b92
This commit was created on GitHub.com and signed with GitHub’s verified signature.
GPG key ID: B5690EEEBB952194
Learn about vigilant mode.

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.

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

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.6.0-alpha

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

Linux-based installation

System requirements

  • This toolchain 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/llvm-valida-releases/releases/download/v0.6.0-alpha/llvm-valida-v0.6.0-alpha-linux-x86_64.tar.xz

Installation

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

sudo ./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:

  1. Clone the project template:
git clone https://github.com/lita-xyz/fibonacci.git
  1. cd into the project template:
cd fibonacci
  1. Build the project:
cargo +valida build
  1. Run the code (taking input from stdin):
valida run --fast target/valida-unknown-baremetal-gnu/debug/fibonacci log
  1. Prove the execution (taking input from stdin):
valida prove target/valida-unknown-baremetal-gnu/debug/fibonacci proof
  1. Verify the proof:
valida verify target/valida-unknown-baremetal-gnu/debug/fibonacci proof --claimed-output log

Writing Rust programs to run on Valida

We do not (yet) support a main function signature that takes any arguments, so it's not possible to follow the normal method of specifying a main function in a Rust program. The following is a demonstration of a simple program that shows how the main function must be declared instead:

#![no_main]

#[no_mangle]
fn main() {
   ...
}

For a starting point to build a project using the Rust Valida toolchain, please take a look at
the template project. You can clone this repo and use
it as a starting point for your project.

The template project depends on the valida-rs crate. This contains a macro for generating an entry point, and some custom versions of standard library functions.

For projects with dependencies on io or rand, make sure your main and Cargo.toml include the code in this template. Also, make sure you have the same .cargo/config.toml in your project. If you want to build the project not targeting Valida, remove the [build] section in .cargo/config.toml and cargo will build the project targeting the host machine, unless otherwise specified.

We edited some functions to make them compatible with the Valida VM. When using these, the default Rust functions won't work. We call the Valida version with the entrypoint:: prefix.

  • io: Valida only supports standard io to the extent of stdin and stdout. To use println in Valida, one needs to call entrypoint::io::println as in my-project. A better io library will be added later.
  • rand: to ensure the VM can prove the calculation of a given random number, we use our own function to generate a random byte with a specific seed.

These implementations are in valida-rs/src/io.rs and valida-rs/src/rand.rs.

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.

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.

Changelog

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:
  • 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
Assets 3
Loading