Skip to content

Releases: lita-xyz/valida-releases

Valida toolchain v0.7.0-alpha

16 Dec 23:42
@morganthomas morganthomas
v0.7.0-alpha
d97eb93
This commit was created on GitHub.com and signed with GitHub’s verified signature.
GPG key ID: B5690EEEBB952194
Learn about vigilant mode.
Compare
Choose a tag to compare
Valida toolchain v0.7.0-alpha Latest
Latest

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

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

Linux-based installation

This section describes installation on Ubuntu 24.04 LTS or newer, 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.7.0-alpha/llvm-valida-v0.7.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.

An example

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

#![no_main]

use std::io::stdin;

#[no_mangle]

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
  • 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 reth-valida 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.

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 usi...

Read more
Assets 3
Loading

Valida toolchain v0.6.0-alpha

01 Dec 07:11
@morganthomas morganthomas
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.
Compare
Choose a tag to compare
Valida toolchain v0.6.0-alpha

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 divisi...
Read more
Assets 3
Loading

llvm-valida v0.5.0-alpha

12 Nov 01:32
@morganthomas morganthomas
v0.5.0-alpha
f61a96b
Compare
Choose a tag to compare
llvm-valida v0.5.0-alpha

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

Download the toolchain

Installation

Run:

sudo ./install.sh

Usage instructions

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:

$ which valida-shell
/usr/local/bin/valida-shell

If the result is something else, then either the installation did not complete successfully, or you had another valida-shell executable 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 instructions below.

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. Enter the Valida shell:
$ valida-shell
  1. Build the project:
valida> cargo +valida build
  1. Run the code (taking input from stdin):
valida> valida run --fast target/delendum-unknown-baremetal-gnu/debug/fibonacci log
  1. Prove the execution (taking input from stdin):
valida> valida prove target/delendum-unknown-baremetal-gnu/debug/fibonacci proof
  1. Verify the proof:
valida> valida verify target/delendum-unknown-baremetal-gnu/debug/fibonacci proof

Writing Rust programs to run on Valida

The Valida Rust compiler can currently compile in no_std mode, I.E. it cannot yet provide access to the std library, but can compile Rust programs which only use functionality contained within core, and which are annotated as #![no_std].

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 #![no_std] program. The following is a demonstration of a simple program that shows how the main function must be declared instead:

#![no_main]

valida_rs::entrypoint!main(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

To enter the Valida shell, run:

valida-shell

See the lita-xyz/valida-c-examples repo on Github for some examples of C programs which can be compiled and run on Valida. Here is an example C program from this repo, called cat.c:

const unsigned EOF = 0xFFFFFFFF;

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

To compile, for example, the cat.c example, from within the Valida shell:

clang -target delendum ./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 delendum ./examples/${NAME}.c -o ${NAME}
valida run ${NAME} log

Some other examples that are provided in the valida-c-examples repo:

  • 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.

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.
  • Code which assumes that memory is initialized to zero might not work properly. This includes realloc in the C standard library. This will be resolved by updating the VM to treat uninitialized memory as having a value of zero.
  • The compiler might emit incorrect code for some 64-bit arithmetic operations. This will be resolved by adding appropriate tests and fixing any issues that come up.

Changelog

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 ch...
Read more
Assets 3
Loading

llvm-valida v0.4.0-alpha

23 Oct 02:36
@morganthomas morganthomas
v0.4.0-alpha
f61a96b
Compare
Choose a tag to compare
llvm-valida v0.4.0-alpha

This is the 0.4.0-alpha release of the LLVM Valida toolchain by Lita.

System requirements

This template supports x86-64 Linux. rustup is required. Arch Linux and Ubuntu are specifically supported, with other platforms possibly requiring some tinkering to make work.

Installation

Run:

sudo ./install.sh

Usage instructions

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:

$ which valida-shell
/usr/local/bin/valida-shell

If the result is something else, then either the installation did not complete successfully, or you had another valida-shell executable 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 instructions below.

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. Enter the Valida shell:
$ valida-shell
  1. Build the project:
valida> cargo +valida build
  1. Run the code:
valida> valida run --fast target/delendum-unknown-baremetal-gnu/debug/fibonacci log

Writing Rust programs to run on Valida

The Valida Rust compiler can currently compile in no_std mode, I.E. it cannot yet provide access to the std library, but can compile Rust programs which only use functionality contained within core, and which are annotated as #![no_std].

The first requirement for Rust code for Valida is to annotate the entrypoint (main.rs) file with #![no_main] and follow the requirements for writing programs which do not use the standard library (see here for details). We also 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 #![no_std] program. The following is a demonstration of a simple program that shows how the main function must be declared instead:

#![no_main]

entrypoint::entrypoint!main(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.

Compiling and running C programs

To compile, for example, the cat.c example, from within the Valida shell:

clang -c -target delendum ./examples/cat.c
ld.lld --script=./valida.ld cat.o -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 -c -target delendum ./examples/${NAME}.c
ld.lld --script=/valida-toolchain/valida.ld /valida-toolchain/DelendumEntryPoint.o ${NAME}.o -o ${NAME}
valida run ${NAME} log

Some other examples that are provided:

  • 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, 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:

CPATH="$(pwd)/libc" ./clang -nostdinc -c -target delendum ./examples/cat-alpha.c
./ld.lld --script=./valida.ld ./libc/libc.a ./cat-alpha.o -o cat-alpha
./valida run cat-alpha log

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

  • A lot of execution proofs are not verifiable, due to the STARK constraints for certain opcodes being works in progress.
  • There is some evidence that some Rust programs may fail to terminate due to an unknown compiler bug.
  • The Rust compiler may at times emit unaligned LOAD32 / STORE32 opcodes, causing the Valida VM to panic.
  • Code which assumes that memory is initialized to zero might not work properly. This includes realloc in the C standard library.
  • The compiler might emit incorrect code for some 64-bit arithmetic operations.

Changelog

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

llvm-valida v0.3.0-alpha

08 Aug 21:05
@nhlita nhlita
v0.3.0-alpha
f61a96b
Compare
Choose a tag to compare
llvm-valida v0.3.0-alpha

Usage instructions

Compiling and running C programs

To compile, for example, the cat.c example, from within the decompressed release package directory:

./clang -c -target delendum ./examples/cat.c
./ld.lld --script=./valida.ld cat.o -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 -c -target delendum ./examples/${NAME}.c
./ld.lld --script=./valida.ld ${NAME}.o -o ${NAME}
./valida run ${NAME} log

Some other examples that are provided:

  • 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, 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:

CPATH="$(pwd)/libc" ./clang -nostdinc -c -target delendum ./examples/cat-alpha.c
./ld.lld --script=./valida.ld ./libc/libc.a ./cat-alpha.o -o cat-alpha
./valida run cat-alpha log

Compiling and running Rust programs

First make sure you have a proper version of rustc in your system PATH. A convenient way to do this is using rustup. If you have rustup installed, then you can set a proper version of rustc this way:

rustup install nightly-2024-07-29
rustup default nightly-2024-07-29

To build the Rust examples, you can use the following script, and just replace fib-write in line 2 with the name of the example:

#!/usr/bin/env bash
EXAMPLE=fib-write
rustc --emit=llvm-ir -Cpanic="abort" -C opt-level=3  -C target-cpu=generic ./examples/$EXAMPLE.rs
./llc -march=delendum -filetype=obj $EXAMPLE.ll
./ld.lld --script=./valida.ld $EXAMPLE.o -L . -lstdio -o $EXAMPLE

To make this process a little easier, this script is included in this release bundle as ./build-rust.sh.

You can add your own examples and possibly build them this way, subject to the following limitations.

Rust to Valida limitations

  • Exception handling is not yet supported
  • Multi-file compilation is not yet supported
  • The Rust standard library is not yet supported
  • The Rust compiler toolchain (rustc, cargo, etc) is not yet supported
  • Due to the lack of thorough testing so far, it is safe to assume that there are other limitations not documented here.

Next steps on Rust to Valida support involve getting the Rust compiler toolchain to work with Valida. Once Valida is integrated into the Rust compiler toolchain, pieces like multi-file compilation and the Rust standard library should begin to fall into place.

Writing Rust programs to run on Valida

Use this template and insert your code accordingly.

#![no_std]
#![feature(start)]

use core::panic::PanicInfo;

#[panic_handler]
fn panic(_info: &PanicInfo) -> ! {
    loop {}
}

extern { fn read_stdin() -> u8;}
extern { fn write_stdout(n: u8); }

#[start]
fn main(_argc: isize, _argv: *const *const u8) -> isize {
    // insert your code here
}

Changelog 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

llvm-valida 0.2.0-alpha

02 Jul 20:31
@nhlita nhlita
0.2.0-alpha
f61a96b
Compare
Choose a tag to compare
llvm-valida 0.2.0-alpha

Changes:

  • Updated to LLVM 18
  • Fixed an issue with loading certain data sections from ELF object files
Assets 3
Loading

llvm-valida v0.1.0-alpha

30 May 19:33
@nhlita nhlita
v0.1.0-alpha
f61a96b
Compare
Choose a tag to compare
llvm-valida v0.1.0-alpha

Introducing the Valida C Compiler Toolchain

We are excited to announce the alpha release of the Valida C Compiler Toolchain, designed to compile C programs to run on the Valida zk-VM. This package includes:

  • Valida C Compiler: This compiler converts C programs to Valida-compatible code.
  • Valida zk-VM: A virtual machine for executing and verifying Valida programs.

What You Can Do:

With this package, you can:

  1. Compile C Programs: Convert your C code into Valida-compatible programs using the included C to Valida compiler.
  2. Run and Verify Programs: Execute your programs on the Valida zk-VM and create succinct proofs of execution.
  3. Test and Debug: Explore the capabilities and limitations of both the compiler and the VM in this alpha release.

Important Caveats:

This software is in its alpha stage and has several limitations:

Compiler Limitations:

  • No Floating Point: The compiler does not support floating-point operations.
  • No 64-bit Integers: Types like long long and unsigned long long are unsupported.
  • No libc Support: You must rely on built-in functions for I/O operations.
  • Limited Inline Support: String and array literals cannot be used inline in function bodies.
  • Struct Issues: Local variables of struct types may not always work properly.
  • Varargs: The compiler does not support variable arguments.

zk-VM Limitations:

  • Incomplete Proving System: Some constraints are missing or incorrect, allowing false statements to be proven.
  • Arithmetic Overflows: The VM cannot handle executions involving arithmetic overflows.
  • No Zero Knowledge Proofs: The VM does not yet produce zero-knowledge proofs.

Usage Instructions:

To compile, for example, the cat.c example, from within the decompressed release package directory:

./clang -c -target delendum ./examples/cat.c
./ld.lld --script=./valida.ld cat.o -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 -c -target delendum ./examples/${NAME}.c
./ld.lld --script=./valida.ld ${NAME}.o -o ${NAME}
./valida run ${NAME} log

There are three other examples not mentioned yet: reverse, checksum, and sha256. reverse will reverse the bytes of the input provided on the console and print out the reversed input. checksum will add up the bytes of the input and print out the least significant byte of the result. sha256 will compute the SHA-256 hash of the first 256 bytes of input and print out the resulting hash. Each of them will write their output to log or whichever file you specify on the command line.

Writing Your Own Programs:

To create your own programs in C:

  • No libc Support: Use built-in functions __builtin_delendum_read_advice() (for getc(stdin)) and __builtin_delendum_write(x) (for putc(x, stdout)).
  • Mind the Limitations: The compiler's current limitations necessitate workarounds, particularly for I/O, structures, and other unsupported features.

Benchmarks:

Here are some reports on benchmarks that we have run comparing the proving performance of Valida to RISC Zero:

These benchmarks indicate that Valida is an industry leading competitor in terms of speed and efficiency of generating zero knowledge proofs.

Source repositories

Here are the source repositories used to generate the contents of this release bundle:

Conclusion:

The Valida C Compiler Toolchain offers exciting possibilities for compiling and running C programs on the Valida zk-VM. While this alpha release has limitations, it provides a solid foundation for future developments. We encourage you to test the toolchain, provide feedback, and contribute to its evolution.

For more information or support, visit our website or contact our team directly.

Assets 3
Loading