Introduction

Vx (pronounced “vee-ex”) is a systems programming language for machines that are no longer a single processor. A modern node is a CPU, one or more GPUs, sometimes a neural accelerator, and a memory hierarchy with half a dozen distinct spaces in it — each with its own capacity, its own bandwidth, and its own rules about who is allowed to read it.

Most languages treat that hardware as infrastructure. You write the computation, and a large runtime library decides where it lands. The result is that a whole class of mistake — reading device memory from the host, exceeding the capacity of a scratchpad, using a buffer whose copy has not landed yet — is discovered at runtime, if you are lucky, and silently tolerated if you are not.

Vx takes the opposite position:

Heterogeneity belongs in the type system, not in the runtime.

A pointer into accelerator memory has a different type from a pointer into host DRAM. Crossing between them requires an explicit transfer(). A host thread dereferencing a device pointer is a compile error with a source span, not a segfault in production.

What that buys you

The compiler front-loads into type checking a set of bugs that normally surface much later:

Capacity admission is worth dwelling on, because it is the one with no equivalent elsewhere. Vx reads a machine file describing a real part — its memory hierarchy, capacities, bandwidths and interconnect — and checks your placements against it before a binary exists. An allocation that cannot fit in the scratchpad you assigned it to is a compile error, not an out-of-memory at training step 1200.

Who this is for

Vx is aimed at the layer underneath the machine-learning stack: runtimes, kernels, schedulers, inference engines, and the systems code that has to be correct across several kinds of silicon at once.

It is deliberately not aimed at exploratory work. PyTorch users mutate a model mid-loop, print a tensor’s shape, branch on it and carry on. In Vx — ahead-of-time compiled, statically regioned — that same dynamism takes real effort.

Vx is the right language for the thing that must be correct and fast across ten kinds of silicon. It is not the right language for the thing you are still figuring out.

How to read this book

If you want to run something in the next ten minutes, go to Install Vx and then Your first program.

If you want to know whether the language is worth your time before installing anything, read A tour of Vx, which covers the whole language with no accelerator involved, and then Topologies and memory, which is the part that is actually different.

If you are evaluating Vx for a real system, Machine files is the chapter that will tell you fastest whether the model matches your hardware.

Project status

Vx is young and under active development. The language, the type checker and the MLIR optimization pipeline are all still moving. Expect sharp edges, expect syntax to change, and please report what you hit — early bug reports are the most useful thing you can contribute right now.

Install Vx

Quick install

curl -fsSL https://vxlang.org/install.sh | sh

This downloads a prebuilt toolchain, verifies it against its published SHA-256, and unpacks it into ~/.vx. Nothing is written outside that directory and nothing needs root.

Then put it on your PATH:

export PATH="$HOME/.vx/bin:$PATH"

Add that line to ~/.zshrc or ~/.bashrc to make it permanent.

Supported platforms

Prerequisites

The installer checks for these and stops with the exact command to run if either is missing. It does not install them for you: a script piped into a shell should not quietly run your package manager.

LLVM 22

Vx lowers through MLIR, and shells out to mlir-translate, opt, llc and clang from LLVM 22 when it compiles. The version matters — the MLIR C API changes between major releases, so LLVM 21 or 23 will not work.

# macOS
brew install llvm@22

# Ubuntu / Debian
wget https://apt.llvm.org/llvm.sh && chmod +x llvm.sh && sudo ./llvm.sh 22
sudo apt-get install -y libmlir-22-dev mlir-22-tools

libmlir-22-dev is the package people miss. It ships the MLIR C API and is not pulled in by llvm-22-dev.

On macOS, Homebrew’s LLVM is keg-only, so it is deliberately not on your PATH. You do not need to change that — the installer records where it found LLVM, and the vxc wrapper points the compiler at it directly.

z3 (optional)

Seam verification — proving that an asynchronous transfer has been made visible before the buffer is read — is discharged by shelling out to z3. It is opt-in behind --verify-seams, so a toolchain without z3 compiles and runs everything else normally; you only need it when you turn that flag on.

The binary is executed, so installing libz3-dev alone is not enough.

brew install z3          # macOS
sudo apt-get install z3  # Ubuntu / Debian

Verify the install

The installer compiles and runs a small program as its last step, so if it finished without complaint you are already working. To check by hand:

vxc --version

Then compile something. Note that --run propagates the program’s own exit code, so a non-zero exit status here is your program’s return value rather than a failure:

cat > hello.vx <<'EOF'
fn main() -> i32 {
    let x : i32 = 21;
    return x * 2;
}
EOF

vxc --run hello.vx

The last line should read:

[JIT] Program exited with code: 42

Installing a specific version

VX_VERSION=v0.0.1 curl -fsSL https://vxlang.org/install.sh | sh

Toolchains are unpacked side by side under ~/.vx/toolchains/, and ~/.vx/current is a symlink to the active one, so switching versions is a matter of repointing that link.

Uninstalling

rm -rf ~/.vx

Then remove the PATH line from your shell profile. The installer puts nothing anywhere else.

Troubleshooting

vxc: command not found ~/.vx/bin is not on your PATH. See the export line above.

Failed to run mlir-translate: No such file or directory The compiler cannot find the LLVM tools. This normally means LLVM was installed after Vx, so the installer never recorded its location. Re-run the installer — it will find LLVM and rewrite ~/.vx/current/etc/llvm-env.sh.

the Vx runtime library is missing The toolchain directory is incomplete, usually from an interrupted download. Re-run the installer.

Undefined MLIR symbols, or a crash on startup The LLVM on your system is not version 22. Check with llvm-config --version, and note that on macOS a bare llvm-config usually resolves to Xcode’s copy rather than Homebrew’s.

macOS refuses to run the binary Gatekeeper quarantines downloads from the internet. Clear the attribute:

xattr -dr com.apple.quarantine ~/.vx

Next

• Your first program — write something real.
• A tour of Vx — the language in one sitting.

Building from source

You need this if you are on a platform with no prebuilt toolchain — Linux on arm64, or an Intel Mac — or if you intend to work on the compiler itself.

Everything below has been run on the platform it documents.

What the build needs

Plus cmake, ninja, pkg-config, python3 and a C++ compiler.

macOS (Apple Silicon)

xcode-select --install

brew install llvm z3 cmake ninja pkg-config python3 rustup
rustup-init -y --default-toolchain stable

Check that Homebrew’s LLVM is the pinned major version:

$(brew --prefix llvm)/bin/llvm-config --version    # expect 22.x

If Homebrew has moved on, install the pinned one with brew install llvm@22 and run LLVM_VERSION=22 ./setup.sh.

Linux x86_64 (Ubuntu 24.04)

scripts/provision/setup_linux.sh installs everything:

./scripts/provision/setup_linux.sh

It installs build tooling (build-essential, ninja-build, cmake, pkg-config), libraries (libffi-dev, libz3-dev, z3, zlib1g-dev, libzstd-dev, libedit-dev, libxml2-dev), and LLVM 22 from apt.llvm.org — Ubuntu’s own repositories lag the pinned version.

libmlir-22-dev is the package people miss. It ships the MLIR C API that the Rust bindings link against, and it is not pulled in by llvm-22-dev.

Rust is installed separately by the script, via rustup.

Sizing, if you are provisioning a box for this: 40 GB of disk (a release build leaves target/ at about 2 GB, and cargo test adds a second profile), and as many cores as you can get. A reference release build takes about 1m48s on 36 vCPU with a warm crate cache.

Configure and build

Identical on both platforms:

./setup.sh           # writes config.local -- LLVM path, cargo/rustup homes, PATH
source config.local  # required in every new shell, before any cargo command
cargo build --release

setup.sh puts LLVM first on PATH, so an unsuffixed llvm-config, mlir-translate or clang++ resolves to the pinned version rather than to Xcode’s or to another LLVM on the box. It warns if what it found does not match the pin.

If you get llvm-config: command not found or cargo: command not found, you opened a new shell and did not source config.local. It is once per shell, every shell.

Verify

cat > /tmp/hello.vx <<'EOF'
fn main() -> i32 {
    let x: i32 = 21;
    return x * 2;
}
EOF

source config.local
./target/release/vxc --run /tmp/hello.vx

Expect the last line to read [JIT] Program exited with code: 42. Then run the suite:

cargo test

Optional components

The build succeeds without any of these; each unlocks one path.

Autodiff (Enzyme) — needed for the autodiff tests and for grad/jvp/vjp lowering:

./scripts/provision/install_enzyme.sh
export ENZYME_LIB="$(pwd)/.cargo/enzyme/LLVMEnzyme-22.dylib"   # .so on Linux

Apple neural engine primitives (macOS only) — build.rs compiles CoreML primitive models, and invokes bare python3, so coremltools has to be importable from that interpreter:

python3 -m pip install coremltools

Without it the build prints warning: Failed to compile matmul_4x4 with coremlc and continues. Kernels fall back to CPU execution; only accelerator dispatch is unavailable.

CUDA (Linux) — detected automatically when /usr/local/cuda is present. Set VX_DISABLE_CUDA=1 to force it off. The toolkit alone is enough to build; a GPU is only needed to run.

Packaging a toolchain

To produce a redistributable tarball from a source build:

./scripts/release/package.sh v0.0.1

That stages the compiler, its runtime library, the standard library and the machine files under dist/, rewrites the linked library paths so the binaries find their own dependencies, generates the wrapper scripts, and writes a .tar.gz alongside its SHA-256.

Your first program

Hello, 42

Every Vx program starts at main, which returns an i32.

fn main() -> i32 {
    let x : i32 = 21;
    return x * 2;
}

Save that as hello.vx and run it:

vxc --run hello.vx

[JIT] Translating to LLVM IR...
[JIT] Optimizing LLVM IR (-O0)...
[JIT] Compiling to native object (-O0)...
[JIT] Linking native executable...
[JIT] Executing native binary...
[JIT] Program exited with code: 42

--run compiles the program and executes it immediately, then propagates the program’s own exit code. A non-zero exit status from vxc --run is your program’s return value, not a compiler failure — this program genuinely exits 42.

Printing

print takes a value; print! takes a literal. Neither needs an import.

fn main() -> i32 {
    print!("the answer is ");
    print(42);
    print!("\n");
    return 0;
}

Compiling ahead of time

The JIT is convenient for iterating. For anything you intend to keep, compile to a native executable:

vxc -c hello.vx -o hello.o

vxc --help lists the other actions — --emit-mlir and --emit-llvm are the two you will reach for most when you want to see what the compiler did with your code.

Something with a shape to it

Types annotate a binding with :, let mut makes it mutable, and for ranges with ..:

fn sum_to(n : i32) -> i32 {
    let mut total : i32 = 0;
    for i in 0..n {
        total += i;
    }
    return total;
}

fn classify(x : i32) -> i32 {
    if x > 10 {
        return 1;
    } else if x == 10 {
        return 2;
    } else {
        return 3;
    }
}

fn main() -> i32 {
    print(sum_to(10));
    print!("\n");
    print(classify(15));
    print!("\n");
    return 0;
}

Diagnostics carry a code and a source span. Forget a return and the compiler says so directly:

Error[E3028] at 2:3: 'add' returns i32 but its body can finish without returning a value

Every code the compiler can emit is listed in the diagnostic index, grouped by the stage that raises it.

Arrays and tensors

An array literal is a tensor, and indexing reads an element back:

fn main() -> i32 {
    let a : Tensor<f32, [4]> = [ 1.0, 2.0, 3.0, 4.0 ];
    print(a[0]);
    print!(" ");
    print(a[3]);
    return 0;
}

Tensor<f32, [4]> is a tensor of four f32 with its shape known at compile time. A ? stands in for a dimension that is not — Tensor<f32, [?, ?]> is a matrix whose extents are runtime values, which you read with .extent(0) and .extent(1).

Structs and methods

struct Point {
    x: i32,
    y: i32,
}

impl Point {
    fn magnitude_squared(self: &Point) -> i32 {
        return self.x * self.x + self.y * self.y;
    }
}

fn main() -> i32 {
    let p = Point { x: 3, y: 4 };
    return p.magnitude_squared();
}

The receiver is written out in full: self: &Point borrows it, self: &mut Point borrows it mutably. There is no implicit self.

Where to go next

You now have enough to write ordinary programs. Two directions from here:

• A tour of Vx covers the rest of the language — generics, enums, pattern matching, ownership — none of which involves an accelerator.
• Topologies and memory is the part that makes Vx different from every other systems language: placing data in a named memory space and having the compiler check it.

A tour of Vx

This chapter covers the ordinary parts of the language — everything you would need to write a command-line program, with no accelerator in sight. If you have written Rust, most of this will look familiar; the differences are called out where they matter.

Values and types

#![allow(unused)]
fn main() {
let x : i32 = 21;      // annotated
let y = 21;            // inferred from context
let mut count = 0;     // mutable
}

Bindings are immutable unless you write mut.

The primitive types are the ones you would expect: i8 i16 i32 i64, u8 u16 u32 u64, f16 f32 f64, and bool.

There are no implicit numeric conversions. An i32 does not become an i64 because the context wants one; you write the conversion. Integer literals infer to the type the context requires, so let n : i64 = 5; is fine, but mixing two differently-typed values in one expression is an error. This is deliberate — silent widening is a common source of both bugs and unintended performance cliffs.

Functions

#![allow(unused)]
fn main() {
fn add(a : i32, b : i32) -> i32 {
    return a + b;
}
}

Parameter types and the return type are both mandatory — there is no inference for either, and a function with no useful result is written -> void. A function may end with a bare expression instead of return, as in Rust.

Control flow

#![allow(unused)]
fn main() {
if x > 10 {
    // ...
} else if x == 10 {
    // ...
} else {
    // ...
}

for i in 0..n {
    // ...
}

loop {
    // forever, until you break
    if done { break; }
}
}

There is no while. It is not a keyword, and writing one is a parse error. The two loops are for over a range and bare loop with an explicit break.

0..n is a half-open range: it includes 0 and excludes n.

Structs

struct Point {
    x: i32,
    y: i32,
}

fn main() -> i32 {
    let p = Point { x: 3, y: 4 };
    let a = p.x;
    return a;
}

Methods go in an impl block, and the receiver is written out in full — there is no implicit self:

#![allow(unused)]
fn main() {
impl Point {
    fn magnitude_squared(self: &Point) -> i32 {
        return self.x * self.x + self.y * self.y;
    }

    fn translate(self: &mut Point, dx: i32, dy: i32) -> void {
        self.x += dx;
        self.y += dy;
    }
}
}

A return type is never optional. A function that produces no useful result returns void, and exits early with a bare return;.

&Point borrows immutably, &mut Point mutably. A method with no self parameter is an associated function, called as Point::make(...).

Enums and pattern matching

Enums carry data:

#![allow(unused)]
fn main() {
enum Result {
    Ok(i32),
    Err(i32),
}

enum Color {
    Red, Green, Blue,
}
}

Construct a variant with ::, and take it apart with match:

#![allow(unused)]
fn main() {
fn unwrap_or(r: Result, default: i32) -> i32 {
    let mut out = default;
    match r {
        Result::Ok(val) => { out = val; },
        Result::Err(code) => { out = -code; },
    }
    return out;
}
}

A data-carrying enum is laid out as a tag plus a payload.

A match can also be used as a value directly, with each arm evaluating to a result:

#![allow(unused)]
fn main() {
fn pick(x : i32) -> i32 {
    match x { 0 => { 7 }, _ => { 9 } }
}
}

Arrays and tensors

An array literal is a tensor:

#![allow(unused)]
fn main() {
let a : Tensor<f32, [4]> = [ 1.0, 2.0, 3.0, 4.0 ];
let first = a[0];
}

The shape is part of the type. Tensor<f32, [4]> has four elements, known at compile time. A ? marks a dimension that is only known at runtime:

#![allow(unused)]
fn main() {
fn matmul(a : Tensor<f32, [?, ?]>, b : Tensor<f32, [?, ?]>) -> Tensor<f32, [?, ?]> {
    let mut result : Tensor<f32, [?, ?]> =
        Tensor<f32, [?, ?]>::uninit([a.extent(0), b.extent(1)]);

    for i in 0..a.extent(0) {
        for j in 0..b.extent(1) {
            result[i][j] = 0.0;
            for k in 0..a.extent(1) {
                result[i][j] += a[i][k] * b[k][j];
            }
        }
    }
    return result;
}
}

.extent(n) reads the size of dimension n. Shapes that are known statically get checked statically — a matmul whose inner dimensions disagree is a compile error rather than a runtime one.

Collections

The standard library ships the usual containers. Vec<T> is a growable array:

import std::vec;

fn main() -> i32 {
    let mut v = Vec<i32>::new();
    v.push(10);
    v.push(32);
    return v.get(0) + v.get(1);
}

Also available: HashMap, HashSet, Option, Result, String, Box, and iterator adaptors. See the standard library for the full list.

Modules

One file is one module. import pulls another in:

#![allow(unused)]
fn main() {
import std::vec;
import std::io;
import graph::traversal;
}

std:: resolves against the standard library shipped with your toolchain. Anything else resolves against the library search path and then the current directory.

Unsafe

Raw pointers exist, and the operations that can go wrong with them require unsafe:

extern "C" {
    fn vx_vec_new_i32() -> *mut i8;
    fn vx_vec_push_i32(vec : *mut i8, val : i32) -> i32;
}

fn main() -> i32 {
    unsafe {
        let v = vx_vec_new_i32();
        vx_vec_push_i32(v, 42);
    }
    return 0;
}

Dereferencing a raw pointer, indexing through one, reading a field through one, and calling an unsafe fn all require an unsafe block. A function that takes a caller’s raw pointer and dereferences it is itself unsafe fn, so the obligation is visible in its signature rather than buried in its body.

extern "C" blocks declare foreign functions. Vx’s C ABI interop is zero-overhead: there is no marshalling layer.

Comptime

if comptime selects a branch at compile time. The branches not taken are pruned before semantic analysis, so they may refer to things that do not exist on the target being compiled for:

#![allow(unused)]
fn main() {
let mut val = 0;

if comptime Topology::Current == Topology::CPU {
    val = 1;
} else if comptime Topology::Current == Topology::CPU_AVX512 {
    val = 2;
} else {
    val = 3;
}
}

Topology::Current is the topology the current region compiles for. This is how one source file carries code for several targets without the dead paths having to typecheck against all of them.

if is also an expression:

#![allow(unused)]
fn main() {
return if val == 1 { 0 } else { 1 };
}

Const generics let a value appear in a type — Tensor<f32, [N]> for a const N : i32 — and are resolved by monomorphization.

What is next

• Ownership and borrowing — the memory model.
• Generics and traits — abstraction without runtime cost.
• Topologies and memory — the reason Vx exists.

Control flow

Vx has four ways to branch or repeat: if, loop, for, and match.

if and else

fn classify(x : i32) -> i32 {
    if x < 0 {
        return 0;
    } else if x == 0 {
        return 1;
    } else {
        return 2;
    }
}

fn main() -> i32 {
    return classify(5) - 2;
}

Braces are always required. There is no single-statement form.

An if whose branches all return is a statement, not a value. An if used in value position has to produce a value on every path:

fn main() -> i32 {
    let x : i32 = 3;
    let label = if x > 2 { 1 } else { 0 };
    return label - 1;
}

loop

loop repeats until something breaks out of it.

fn main() -> i32 {
    let mut i : i32 = 0;
    loop {
        if i >= 3 {
            break;
        }
        i = i + 1;
    }
    return i - 3;
}

continue skips to the next turn of the loop:

fn main() -> i32 {
    let mut seen : i32 = 0;
    let mut i : i32 = 0;
    loop {
        i = i + 1;
        if i < 3 {
            continue;
        }
        seen = seen + 1;
        if i >= 5 {
            break;
        }
    }
    return seen - 3;
}

There is no while loop

while is not a keyword in Vx. Writing while i < n { ... } does not produce a “no such loop” message — while and i both lex as ordinary identifiers, and you get a confusing parse error about a missing ;.

Write the same thing with loop and a guard:

fn main() -> i32 {
    let mut i : i32 = 0;
    loop {
        if i >= 4 {
            break;
        }
        i = i + 1;
    }
    return i - 4;
}

Whether while should exist is Vx#506.

Loop invariants

A loop can carry an invariant: a condition that must hold on every turn. The prover checks it.

fn main() -> i32 {
    let mut i : i32 = 0;
    loop invariant(i >= 0) {
        if i >= 3 {
            break;
        }
        i = i + 1;
    }
    return 0;
}

The parentheses around the condition are required here, unlike requires and ensures on a function, which take theirs optionally. That inconsistency is not deliberate — it is Vx#501.

for

for walks a range or anything that implements Iterator.

fn main() -> i32 {
    let mut total : i32 = 0;
    for i in 0..4 {
        total = total + i;
    }
    return total - 6;
}

0..4 counts from 0 up to but not including 4, so that loop adds 0 + 1 + 2 + 3.

A for loop can carry an invariant in the same way a loop can.

match

match compares a value against patterns, in order, and runs the first arm that fits.

fn main() -> i32 {
    let x : i32 = 1;
    match x {
        0 => { return 1; }
        _ => { return 0; }
    }
}

_ matches anything. It is usually the last arm.

match is most useful with an enum, where each arm handles one variant:

enum Colour {
    Red,
    Green,
}

fn main() -> i32 {
    let c = Colour::Red;
    match c {
        Colour::Red => { return 0; }
        Colour::Green => { return 1; }
    }
}

Where to next

• Ownership and borrowing — who owns a value, and who may look at it
• Contracts and verification — requires, ensures, assert
• Generics and traits — writing code once for many types

Ownership and borrowing

Vx has no garbage collector and no mandatory reference counting. Memory is managed by ownership, checked at compile time, in the same family as Rust’s model.

Owning and borrowing

A binding owns its value. Passing it to a function by value moves it, and the original binding is no longer usable:

#![allow(unused)]
fn main() {
let v = make_buffer();
consume(v);      // v is moved
// reading v here is an error
}

Borrow instead of moving to keep the original alive:

#![allow(unused)]
fn main() {
fn total(v : &Vec<i32>) -> i32 { /* ... */ }
fn append(v : &mut Vec<i32>, x : i32) { /* ... */ }
}

&T is a shared borrow, &mut T is an exclusive one. The usual rule applies: any number of shared borrows, or exactly one exclusive borrow, never both at once. The checker tracks variance and regions, so a borrow cannot outlive what it points into.

Linear values

Some values are linear: they must be consumed exactly once, and the checker enforces it. Device buffers are the motivating case. A buffer that has been handed off to an accelerator has left your control, and reading it again is a use-after-move — reported as a compile error rather than as corrupted data.

This is stronger than an ordinary move check. A linear value cannot be quietly dropped either, because dropping a device allocation without releasing it is a leak the runtime cannot detect for you.

Boxing

Recursive types must be boxed. Box<T> is a heap allocation with a single owner:

#![allow(unused)]
fn main() {
import std::box;

struct Node {
    value: i32,
    next: Box<Node>,
}
}

The requirement is not an oversight — it is what lets the compiler give every nominal type a size without solving a fixpoint across module boundaries, which in turn is what lets the frontend compile modules in parallel with no shared state.

Raw pointers

*const T and *mut T are raw pointers, and they opt out of all of the above. Because of that, the operations that can go wrong with them require unsafe:

• dereferencing one
• indexing through one
• reading a field through one
• calling an unsafe fn

A function that takes a caller’s raw pointer and dereferences it is itself declared unsafe fn, so the obligation is visible in the signature rather than buried in the body.

unsafe fn read_first(p : *const i32) -> i32 {
    return *p;
}

fn main() -> i32 {
    let x : i32 = 42;
    unsafe {
        return read_first(&x);
    }
}

Keep unsafe blocks small. The point of the annotation is that the region a human has to verify by hand is written down and searchable.

Generics and traits

Generics in Vx are monomorphized: each instantiation becomes its own concrete function or type at compile time. There is no boxing, no vtable and no dynamic dispatch unless you ask for it.

Generic types and functions

#![allow(unused)]
fn main() {
struct Pair<T> {
    first: T,
    second: T,
}

enum Maybe<T> {
    Just(T),
    Nothing,
}
}

Instantiate by naming the argument:

fn main() -> i32 {
    let m = Maybe<i32>::Just(42);

    let mut result = 0;
    match m {
        Maybe<i32>::Just(val) => { result = val; },
        Maybe<i32>::Nothing => { result = 0; },
    }
    return result;
}

Generic impls

An impl block can be generic, or specific to one instantiation:

#![allow(unused)]
fn main() {
impl<T> Pair<T> {
    fn first(self: &Pair<T>) -> T {
        return self.first;
    }
}

impl Pair<i32> {
    fn sum(self: &Pair<i32>) -> i32 {
        return self.first + self.second;
    }
}
}

When several impls could apply, the most specific one wins.

Bounds

Constrain a parameter with ::

#![allow(unused)]
fn main() {
impl<T : Float> Tensor<T, [?, ?]> {
    // ...
}
}

Traits

Traits describe shared behaviour, and are implemented with impl ... for:

#![allow(unused)]
fn main() {
impl<T> Iterator<VecIter<T>, T> for VecIter<T> {
    // ...
}
}

That is how Vec participates in for loops and in the iterator adaptors — map and friends are ordinary generic functions over the Iterator trait rather than compiler magic.

Const generics

A value can be a type parameter, not only a type. This is what makes statically-shaped tensors work:

#![allow(unused)]
fn main() {
fn dot<const N : i32>(a : Tensor<f32, [N]>, b : Tensor<f32, [N]>) -> f32 {
    let mut acc = 0.0;
    for i in 0..N {
        acc += a[i] * b[i];
    }
    return acc;
}
}

Because N is part of the type, passing two tensors of different lengths to dot is a compile error rather than a runtime check you forgot to write. Each distinct N monomorphizes to its own function, so the loop bound is a constant the optimizer can see.

How this stays fast to compile

Every symbol, nominal type and monomorphized instantiation is identified by a flat 256-bit identifier rather than by a pointer into a shared tree. Combined with a nominal type system and mandatory boxing for recursive types, that decouples modules from one another: the frontend resolves and checks them in parallel across cores, with no query engine, no locks and no shared mutable state.

The observable consequence is that the same source produces byte-identical MLIR whether it is compiled serially or in parallel — which is asserted in the test suite rather than assumed.

Compile-time evaluation

comptime marks work that happens while the program is being compiled, not while it runs.

comptime blocks

A comptime block runs during compilation.

fn main() -> i32 {
    comptime {
        let size : i32 = 4 * 4;
    }
    return 0;
}

Everything inside has to be knowable at compile time. A comptime block cannot read a run-time value, call into C, or touch a device.

comptime conditions

if comptime chooses a branch at compile time. The branch not taken is not compiled.

fn main() -> i32 {
    if comptime 1 < 2 {
        return 0;
    }
    return 1;
}

This is different from an ordinary if with a constant condition. An ordinary if is compiled in full and then possibly folded by the optimiser; if comptime decides before code generation, so the untaken branch does not have to compile at all. That matters when a branch is only valid for some types or some hardware.

Const generic parameters

A generic parameter can be a value rather than a type, written with const:

fn buffer_size<const N : i32>() -> i32 {
    return N;
}

fn main() -> i32 {
    return buffer_size<4>() - 4;
}

The value is fixed when the function is instantiated, so it can be used where a compile-time constant is required — most usefully in a tensor’s shape.

Where this is used

Compile-time evaluation is what lets a shape be part of a type. Tensor<f32, [4, 4]> needs 4 to be known while type checking, not while running, and const generic parameters are how a function can be generic over a shape without giving up that knowledge:

fn main() -> i32 {
    let t : Tensor<f32, [2, 2]> = Tensor<f32, [2, 2]>();
    return 0;
}

Because the shape is in the type, a matrix multiply whose dimensions do not line up is a compile error rather than a run-time crash — the same argument as contracts, applied to dimensions.

Where to next

• Generics and traits — the rest of the generic system
• Contracts and verification — other things checked before the program runs

Contracts and verification

Most languages let you write down what a function expects only in a comment. Vx lets you write it in the signature, where the compiler can act on it.

There are four pieces: requires, ensures, invariant, and assert.

requires and ensures

requires states what must be true when the function is called. ensures states what will be true when it returns.

fn halve(x : i32) -> i32
    requires x > 0
    ensures return > 0
{
    return x;
}

fn main() -> i32 {
    return halve(4) - 4;
}

Inside ensures, the word return means the value the function is about to return.

A function may carry more than one of each. They are read as a list, all of which must hold:

fn clamp_positive(x : i32, hi : i32) -> i32
    requires x > 0
    requires hi > x
    ensures return > 0
{
    return x;
}

fn main() -> i32 {
    return clamp_positive(1, 2) - 1;
}

The condition may be written bare or in parentheses — requires x > 0 and requires (x > 0) are the same. (invariant is stricter; see below.)

invariant

An invariant on a loop states something that is true on every turn.

fn main() -> i32 {
    let mut i : i32 = 0;
    loop invariant(i >= 0) {
        if i >= 3 {
            break;
        }
        i = i + 1;
    }
    return 0;
}

Unlike requires and ensures, invariant requires its parentheses. invariant i >= 0 is a parse error. This is an inconsistency rather than a design decision, tracked as Vx#501.

What checks these

Conditions are discharged by an SMT solver — z3 — at compile time. If the prover cannot show a condition holds, compilation fails with a diagnostic in the E8xxx range rather than the program being allowed through.

This means two things worth understanding:

• z3 must be installed for contracts to be checked. The build instructions in Building from source cover it.
• The prover can fail to prove something true. A condition it cannot discharge is reported, not assumed. If you hit that, the usual fix is to state an intermediate fact the prover needs, rather than to remove the contract.

assert

assert is the run-time counterpart. It takes a condition and an optional message:

fn main() -> i32 {
    let x : i32 = 1;
    assert(x == 1, "x should be one");
    return 0;
}

If the condition is false at run time, the program stops and reports the message.

Use assert for what you cannot state statically. Use requires and ensures where you can, so the error arrives at compile time instead.

Verified

Verified<T> is a type that carries the fact that a value has been checked. A plain T and a Verified<T> are different types, so a function that demands a checked value cannot be handed an unchecked one by mistake.

fn main() -> i32 {
    let x : i32 = 1;
    let v = Verified(x);
    return 0;
}

This is the same idea as requires, moved into the type: rather than every function re-stating the condition, one function establishes it and the type carries it onwards.

Diagnostics

Contract failures report under their own codes. The full list is in the diagnostic index; the E8xxx group is the prover.

Where to next

• Control flow — where invariant attaches
• Ownership and borrowing — the other thing checked at compile time
• Unsafe and FFI — what the checks do not cover

Unsafe and FFI

Vx checks a lot at compile time: ownership, borrowing, memory placement, contracts. Some things cannot be checked — a pointer that came from C, a hardware register, a cast the compiler has no way to justify. unsafe is where you take responsibility for those.

unsafe does not switch the checks off. It permits a small, specific set of operations that are otherwise refused.

unsafe blocks

An unsafe block is an expression. It can produce a value.

fn main() -> i32 {
    let x : i32 = 7;
    let p : *const i32 = &x;
    let v = unsafe { *p };
    return v - 7;
}

Reading through a raw pointer — *p — is the operation that needs the block. So does indexing through one, or reading a field through one.

Raw pointers

Two kinds, matching the two kinds of reference:

Unlike &T and &mut T, raw pointers are not tracked by the borrow checker. Nothing stops two *mut T pointing at the same value. That is exactly why dereferencing one needs unsafe.

unsafe functions

A function whose body is not the dangerous part — but whose contract is — should be marked unsafe itself. A caller then has to opt in.

unsafe fn read_at(p : *const i32) -> i32 {
    return unsafe { *p };
}

fn main() -> i32 {
    return 0;
}

Unsafe-ness is part of the function’s type. An unsafe fn cannot be passed where a safe function is expected, so the obligation cannot be lost by storing the function in a variable.

The rule for when to mark a function unsafe: if a caller can make it misbehave by passing something the compiler cannot check — a dangling pointer, a wrong length — it is unsafe. If the function checks everything itself, it is not, even if its body uses unsafe internally.

Calling C

An extern block declares functions that exist outside Vx.

extern "C" {
    safe fn abs(x : i32) -> i32;
}

fn main() -> i32 {
    return abs(0);
}

By default an extern function is unsafe to call — the compiler knows nothing about what is on the other side. safe marks one that genuinely is safe to call with any arguments its types allow, so callers do not need an unsafe block.

abs qualifies: every i32 is a valid input and it cannot misuse memory. A function taking a pointer and a length would not qualify, because passing a mismatched pair breaks it.

Use safe sparingly. It is a promise the compiler cannot verify, and it is the one place in an extern block where a mistake is silent.

What unsafe does not unlock

unsafe covers operations the type system cannot justify. It does not override placement.

A pointer into device memory still cannot be dereferenced from the host inside an unsafe block — that is not an unchecked operation, it is a wrong one, and it stays a compile error. See Topologies and memory.

Where to next

• Ownership and borrowing — the checks unsafe steps around
• Topologies and memory — the checks it does not
• Standard library reference — which std functions are unsafe, and why

Automatic differentiation

Vx can differentiate a function you wrote, at compile time. There is no tape, no graph built at run time, and no separate framework — the derivative is generated from the function’s own code.

Three forms, matching the three things people usually want.

grad

grad gives the derivative of a function with respect to its input.

fn square(x : f32) -> f32 {
    return x * x;
}

fn main() -> i32 {
    let d = grad(square, 3.0);
    return 0;
}

grad(square, 3.0) is the derivative of square evaluated at 3.0. For x * x that is 2 * x, so 6.0.

vjp — reverse mode

A vector-Jacobian product. This is what backpropagation computes, and it is the efficient choice when a function has many inputs and few outputs — the usual shape of a loss function.

fn square(x : f32) -> f32 {
    return x * x;
}

fn main() -> i32 {
    let g = vjp(square, 2.0, 1.0);
    return 0;
}

The arguments are the function, the point to evaluate at, and the seed — the vector to multiply the Jacobian by, which for a scalar loss is 1.0.

jvp — forward mode

A Jacobian-vector product. The efficient choice in the opposite case: few inputs, many outputs.

fn square(x : f32) -> f32 {
    return x * x;
}

fn main() -> i32 {
    let d = jvp(square, 2.0, 1.0);
    return 0;
}

Same arguments, but the seed is a direction in the input space, and the result is how the outputs move in that direction.

Choosing between them

The cost of vjp scales with the number of outputs; the cost of jvp scales with the number of inputs. That is the whole reason both exist.

How it works

Differentiation is done by Enzyme, which differentiates LLVM IR. Because it works on the IR rather than on source, it differentiates through the optimiser’s view of your code, including calls into other functions.

Enzyme has to be present when the compiler is built — Building from source covers installing it.

Limits worth knowing

A function must be differentiable to be differentiated. Differentiating something with a discrete result — an integer comparison, a branch on equality — is not meaningful. Vx does not yet reject every such case: grad of a discrete-valued function is currently accepted rather than refused, which is Vx#503. Until that is fixed, the compiler will not stop you asking for a derivative that does not exist.

Where to next

• Compile-time evaluation — the other thing that happens before the program runs
• Topologies and memory — running the result on an accelerator

Topologies and memory

This is the chapter that makes Vx different from other systems languages. Everything up to here you could have done in Rust or C++; none of it needed a new language.

The two vocabularies

Vx describes a machine with two kinds of declaration, and they answer different questions:

• Memory — where data lives. Memory::CPU_DRAM, Memory::NPU_HBM, a scratchpad, a cache level. Each has a capacity, a bandwidth, and a scope.
• Topology — where code runs. Topology::CPU, Topology::NPU[0], Topology::GPU. A topology is bound to the memory it can address.

A tensor’s type records which memory space it is in. A region of code records which topology it runs on. The checker’s job is to make sure those two agree everywhere.

Placement and transfer

Moving data between memory spaces is explicit:

#![allow(unused)]
fn main() {
let a = transfer(a_host, Memory::NPU_HBM);
let b = transfer(b_host, Memory::NPU_HBM);
}

transfer yields a value whose type says it lives in NPU_HBM. The original is still typed as living where it was.

The explicitness is the point, and it is required even when the hardware boundary costs nothing. On Apple’s unified memory the CPU and the GPU address the same physical DRAM, so the copy compiles away to nearly nothing — and you still write it. The reason is that data locality should be provable by reading the source, not by profiling the binary. A transfer you cannot find in the text is a transfer you cannot reason about.

Two things the compiler checks here:

• Reachability — there must be a declared path between the two spaces. A transfer between memories with no route between them is an error, not a runtime hang.
• Admission — the destination must have room. This is checked against the machine file, before any binary exists.

Running code somewhere else

spawn on runs a block on a named topology:

fn main() -> i32 {
    let mut host : Tensor<f32, [4, 4]> = Tensor<f32, [4, 4]>::uninit();
    for i in 0..4 {
        for j in 0..4 {
            host[i][j] = 1.0;
        }
    }

    let mut device = transfer(host, Memory::NPU_HBM);

    spawn on(Topology::NPU[0]) {
        for i in 0..4 {
            for j in 0..4 {
                device[i][j] += 1.0;
            }
        }
    }

    return 0;
}

Tensor<f32, [4, 4]>::uninit() takes no arguments: the shape is already part of the type. Only the dynamic form needs extents passed — Tensor<f32, [?, ?]>::uninit([rows, cols]).

The block is outlined into a kernel and handed to the dispatcher for that topology. On Apple Silicon that means CoreML and the neural engine; on an NVIDIA box it means PTX. The source does not change between the two — the machine file does.

Every value the block touches must already live in a memory the target topology can address. That is why the transfer comes first. Skip it, and the error names the value and the space it is in rather than crashing inside a vendor runtime.

The block also calls no helper function. A function declared without a topology belongs to the host, and calling it from inside a device region is a compile error:

Error[E6001]: Function 'f' requires topology 'CPU', but is called from 'ANE'

That is the address-space rule doing its job. Code meant for a device is written in the region, or in a function declared for that topology.

Not implemented yet. spawn on is a statement. The design intends it to become an expression yielding a Future, so a host thread could fan work across several accelerators and join later. There is no future type and no await in the language today.

What gets rejected

The point of putting placement in the type system is the errors you get for free.

Dereferencing a device pointer from the host. A Pinned<T, NPU_SRAM> that escapes into a host expression is a type error with a source span. This is the error that motivates the whole design: in C++ with CUDA it is a segfault, and in Python it is a silent wrong answer.

Working set overflow. A tile you place in a scratchpad that cannot hold it is rejected at compile time, with the required and available figures in the diagnostic. See machine files.

Use-after-move. Buffers are linear values. Consuming one and then reading it again is an error.

Unvisible transfers. An asynchronous transfer whose completion has not been made visible before the buffer is read is a seam violation. Turn the check on with --verify-seams; it discharges the obligation with an SMT solver, and needs z3 on your PATH.

Verified values

Verified<T> marks a value whose computation carried its proof obligations all the way through. A function returning Verified<Tensor> is asserting that the placement, capacity and visibility conditions on the path that produced it were all discharged, not merely unchecked.

#![allow(unused)]
fn main() {
fn custom_matmul(a : Pinned<Tensor<f32, [4, 4]>, Topology::NPU[0]>,
                 b : Pinned<Tensor<f32, [4, 4]>, Topology::NPU[0]>)
    -> Verified<Tensor<f32, [4, 4], Memory::NPU_HBM>> {

    let mut result = Tensor<f32, [4, 4], Memory::NPU_HBM>::uninit();

    spawn on(Topology::NPU[0]) {
        for i in 0..4 {
            for j in 0..4 {
                result[i][j] = 0.0;
                for k in 0..4 {
                    result[i][j] += a[i][k] * b[k][j];
                }
            }
        }
    }

    return Verified(result);
}
}

Pinned<T, Topology> says the value is resident on a particular device. Note the third type argument on Tensor — the memory space it lives in — and that Verified(...) wraps the result after the region, not inside it.

Choosing a machine at compile time

The same program compiles against different hardware by swapping the machine file:

vxc --machine fleet/h100-sxm.vx program.vx -o program
vxc --machine fleet/m4-uma.vx  program.vx -o program

You can ask what the compiler concluded, as JSON, rather than reading it out of diagnostics:

vxc --machine fleet/h100-sxm.vx program.vx --diagnostics-json out.json

That record carries every diagnostic with its structured fields — a capacity rejection includes the space, the amount required, the amount available and the margin — plus the staging routes and per-edge costs that an admitted program resolved to.

Next

Machine files covers how a real part gets described, and what the compiler derives from that description.

Machine files

Most compilers hard-code a cost model. Vx reads one.

A machine file describes the memory hierarchy and interconnect of a real part. The compiler admits or rejects your placements against it, and derives transfer costs from it, before a binary exists.

An example

#![allow(unused)]
fn main() {
Memory HBM  { capacity: 80 GiB, bandwidth: 3.35 TB/s, managed: explicit, scope: device }
Memory L2   { within: Memory::HBM, capacity: 50 MiB, bandwidth: 12 TB/s, managed: cached }
Memory SMEM { within: Memory::L2, capacity: 228 KiB, bandwidth: 128 B/cyc,
              clock: 1.98 GHz, replicas: 132, granule: 1 KiB, scope: sm }

Topology Device {
    arch: nvptx64,
    memory: Memory::HBM,
    transfer Memory::CPU_DRAM -> Memory::HBM : 63 GB/s,
}
}

That is an H100, in eleven lines.

The fields

capacity — how much the space holds. Checked against the working set of anything you place there.

bandwidth — either a rate (3.35 TB/s) or a per-cycle figure with a clock (128 B/cyc at 1.98 GHz). The second form is how scratchpads are usually specified in vendor documentation.

within — containment. L2 sits inside HBM. The containment relation must be acyclic, a child may not exceed its parent’s capacity, and scope narrows as you descend.

managed — explicit if software moves the data, cached if hardware does.

scope — who can see it. device is visible to the whole accelerator; sm is private to one streaming multiprocessor.

replicas — how many copies of the space exist. 132 SMs means 132 scratchpads, and a placement is admitted against one of them, not their sum.

granule — the allocation quantum. A 1 KiB granule means a 100-byte tensor occupies 1 KiB, and admission rounds accordingly.

Units are exact

SI prefixes are decimal and IEC prefixes are binary:

Conversions are exact integer arithmetic, never floating point. A figure copied off a vendor datasheet means precisely what the datasheet meant, and does not drift by a fraction of a percent on the way through the compiler.

What the compiler derives

From that declaration alone, before any code is generated:

Admission — whether a tensor’s working set fits the space it is placed in, with granule rounding applied. A rejection carries the space, the amount required, the amount available and the margin.

Routing — the cheapest legal path between two spaces, over the declared transfer graph. If you transfer from a space that has no declared route to the destination, that is an error rather than a silently inserted staging copy.

Transfer cost — a roofline over the containment tree. A containment hop is charged at both endpoints, because data has to leave the parent as well as enter the child.

Coherence of the model itself — within is acyclic, no child exceeds its parent, scope narrows downward, and every edge has exactly one cost source. A machine file that contradicts itself is rejected as a machine file, before your program is even considered.

The bundled fleet

The repository ships machine files for real parts under fleet/: H100, H200, B200, A100, MI300X, Apple M4 unified memory, multi-GPU nodes and hosts. Each one cites its sources, and marks figures that have not been validated against hardware as unverified.

That last part matters. A declared bandwidth is often the vendor’s hardware peak rather than an achievable rate — Apple’s 120 GB/s for the base M4 is the memory system’s ceiling, not what a copy loop will reach. The fleet files state the vendor’s claim rather than a number already fitted to a measurement, so the gap between prediction and reality stays visible instead of being quietly tuned away.

Using one

vxc --machine fleet/h100-sxm.vx program.vx -o program

--machine prepends the declarations to your compilation unit. They are visible to capacity and placement checks exactly as if you had written them inline. A name declared by both the machine file and the program is an error, never a silent shadow.

--machine describes an accelerator and says nothing about the host it hangs off. If your program stages through host memory, declare the host too:

vxc --machine fleet/h100-sxm.vx --host default program.vx -o program

--host default means “the machine doing the compiling”. A host file declares no capacity, on purpose: host memory is virtual, and a tensor larger than physical RAM pages rather than failing. A hard limit there would reject programs that actually run.

Writing your own

Start from the closest file in fleet/ and change the numbers. The compiler will tell you if the result is incoherent, which makes the edit-check loop fast. Two habits worth keeping:

1. Cite every figure. The fleet files carry the source of each number in a comment. When a prediction is wrong, the first question is always whether the model or the measurement is at fault, and a citation answers it in seconds.
2. Mark what you have not verified. A number from a datasheet and a number from a benchmark are different kinds of thing, and the difference should survive in the file.

Carrying facts across boundaries

A correlation is a fact about two or more values rather than about one: j <= i, tile * B + r == idx, “these two tensors share a dimension”, “this buffer lives on that device”, “the caller is still holding a tile while the callee runs”.

Programs are full of them, and analyses are not built to hold them. A production dataflow analysis records one fact per value, so a relation between values is not weakened at a merge, it is destroyed. The mechanisms that recover one — peepholes, GVN, ScalarEvolution, the affine/Presburger layer — are all scope-local. The single mechanism that crosses a scope is inlining, and it works by deleting the boundary, so it stops at the inliner’s budget, again at an opaque framework op, and completely at a separately compiled kernel launch, which cannot be inlined at all.

At that last seam the loss is not a matter of analysis effort. One kernel body can be linked into a host program where the relation holds and into one where it does not. An analysis reading only the kernel sees the same body in both and must return the same verdict, and the only verdict sound for both is “do not optimize”. The fact is not underdetermined; it is absent.

So the question is not how to re-derive a relation on the far side of a boundary. It is how to carry it. The six programs below are the ways Vx does that today. Each one is a program the compiler refuses, or compiles into code that carries the fact onward, and each names the boundary it is about.

The two kinds

Refusing (1, 2, 3, 4, 6). The relation is the premise of a correctness check. Losing it does not make the program slower; it makes the compiler agree to something it cannot support: a host read of device memory, a working set that does not fit, a transfer with no path, a buffer that may be read stale, a tile that does not fit the part it will be rented on. Every one of these is refused on a laptop, before a machine is booked.

Licensing (5). The relation is the premise of an optimization. Nothing is wrong with the program; there is work in it that is dead, and only the host knows so. The certificate is what lets the device compiler act on that.

1. Residency across a call

The memory space is part of the type, so the producer’s return type carries it across the call and the caller’s read is refused with both spaces named.

fn stage_to_device() -> Tensor<f32, [4, 4], Memory::GPU_HBM> {
  let host_data : Tensor<f32, [4, 4]> = Tensor<f32, [4, 4]>::new();
  return transfer(host_data, Memory::GPU_HBM);
}

fn main() -> i32 {
  let kv = stage_to_device();
  print(kv[0][0]);   // refused: the host cannot address GPU_HBM
  return 0;
}

Error[E6003] at 43:9: 'kv' lives in GPU_HBM but CPU sees only [CPU_DRAM, NPU_HBM];
insert an explicit transfer to CPU_DRAM (cost 50 on the declared path)

The repair is one line — let home = transfer(kv, Memory::CPU_DRAM); — and it is the copy the C++ version also needed and did not get told about. The price in the message comes from the declared machine.

2. A working set across a call

Neither function overflows the 4 MiB space on its own. Only the sum does, and the sum exists only across the call.

// 3 MiB in W. Fits on its own.
fn stage<T>(_t: T) -> i32 {
  let y = Tensor<f32, [1024, 768]>::uninit();
  let _sy = transfer(y, Memory::W);
  return 1;
}

fn main() -> i32 {
  let x = Tensor<f32, [1024, 768]>::uninit();
  // `sx` is read after the call, so its 3 MiB is still resident while `stage`
  // runs. That liveness is what the summary records at the call site.
  let sx = transfer(x, Memory::W);
  let r = stage(7);
  let _back = transfer(sx, Memory::CPU_DRAM);
  return r;
}

Error[E6027] at 59:11: the working set along call path 'main -> stage$i32' in memory
space 'W' peaks at 6291456 bytes, over its 4194304 byte capacity: 'main' holds 3145728
bytes across its call, 'stage$i32' itself peaks at 3145728 bytes

Vx does not inline to get this. Each function exports a summary — its own peak per memory space, and per call site the bytes still live at that site — and one whole-program fold over the call graph composes them. Sequential calls compose by max; a tile held across a call composes by +. The refusal names the path rather than the function, because the overflow is a property of the path.

3. Reachability across a generic call

“Data can get from topology A to topology B” holds between two values rather than of either one, which is exactly the kind of fact a non-relational analysis cannot record. The function below is generic over three devices and never names one:

#![allow(unused)]
fn main() {
fn pipeline<A: Topology, B: Topology, C: Topology>(
  a: Pinned<i32, Topology::A>,
  b: Pinned<i32, Topology::B>,
  c: Pinned<i32, Topology::C>
) -> i32
where Reachable<A, B>, Reachable<B, C>
{
  return 0;
}
}

Island declares memory with no transfer edge into it, so nothing can reach it:

Error: unsatisfied `where Reachable<B, C>` in call to 'pipeline':
no transfer path from CPU to Custom("Island")

The relation is written once and discharged at every call site. The failing constraint is named; the first hop, GPU -> CPU, holds and is not reported.

4. Freshness across the launch

to_device_relaxed() drops the release, and with it the visibility guarantee the consumer depends on. The kernel body is identical either way.

#![allow(unused)]
fn main() {
fn stage(a: Tensor<i32, [4]>) -> i32 {
  let local_a = a.to_device_relaxed();
  spawn on(Topology::NPU[0]) {
    assert(local_a[0] == 42);   // the contract the seam must preserve
  };
  return 0;
}
}

Error[E6004] at 40:17: relaxed transfer of 'a' across the CPUDRAM -> NPUHBM seam
violates the boundary contract: the buffer carries no synchronizing release, so a
consumer may read it stale

The consumer’s assert becomes an obligation on the seam, discharged by z3. Swap in to_device() and the same program is admitted. This check needs z3 on PATH and is requested with --verify-seams.

5. A certificate across the launch

Nothing is wrong with this program. There is work in it that is dead, and only the host knows so:

#![allow(unused)]
fn main() {
fn launch(kblk_start: i32, qblk_end: i32, x: f32) -> f32 {
  // The host's proof. This is the certificate; everything else is transport.
  assert(kblk_start > qblk_end);
  let mut out = Tensor<f32, [64]>::uninit();
  spawn on(Topology::GPU) {
    // Mask-as-data: the causal condition is a value, not a loop constraint.
    // There is no iteration domain left to split.
    let masked = kblk_start > qblk_end;
    for i in 0..64 {
      let mut e: f32 = x;
      for _k in 0..256 {
        e = e * x + 1.5;     // dead whenever `masked` holds
      }
      if masked { out[i] = 0.0; } else { out[i] = e; }
    }
  };
  return out[0];
}
}

The kernel alone cannot know masked is always true, so -O3 keeps the 256-trip FMA chain and provably cannot do otherwise. With --emit-seam-certs the host’s proof is re-materialized inside the kernel as llvm.intr.assume, and the chain folds:

base: fmul=2 fadd=2
cert: fmul=0 fadd=0

Both versions print the same answer.

6. Capacity against a declared machine

One program text, a flag per SKU. The machine loads as a peer module, so the same source is admitted or refused according to the part it is compiled for:

fn main() -> i32 {
  // 50 GiB of f16: over the 40 GB part, under the 80 GB one.
  let kv : Tensor<f16, [51200, 524288]> = Tensor<f16, [51200, 524288]>::uninit();
  let _staged = transfer(kv, Memory::HBM);
  return 0;
}

vxc --host default --machine fleet/a100-40.vx 06_capacity_against_a_declared_machine.vx

Error[E6009]: transferred tensor needs 53687091200 bytes but memory space 'HBM'
has capacity 42949672960 bytes

Against fleet/a100-80.vx the same text is admitted.

What makes transport sound

A certificate is only as good as the proof behind it. Example 5 transports exactly the facts the host has already established — the condition of an assert — and only into a kernel that names every variable the fact mentions, so each operand resolves to a value the kernel body can already see. Break the relation and the assert fires before the kernel is ever reached, so the assumption the device compiled against is never live.

Nothing here re-derives a relation on the far side. The fact is proved once, where it is known, and moved forward.

Not yet carried

A shared dimension between two parameters — fn scores<const S: i32>(q: Tensor<f32, [S, D]>, k: Tensor<f32, [S, D]>) — reads as the relation “q and k agree on S”, and today it is not checked: S binds from the first argument and is silently rebound by the second, so a [4] and a [7] are accepted together. Concrete extents are checked (E3003); it is the relation between two generic ones that is not. This is the same relation a framework tracer discovers at trace time and drops at lowering, and it belongs on this page once the checker keeps it.

Running them

The six programs live next to this page, with a script that runs each one and checks its verdict:

./www/book/src/correlation/run.sh

A clean run is one where the compiler says “no” five times for five different reasons, and folds the FMA chain once. Example 4 needs z3 and is skipped without it; the -O3 comparison in example 5 needs mlir-translate and opt from the same LLVM as the build.

Standard library reference

Every public type and function in the 21 std modules, taken from their signatures.

Import a module with its path, then use the names it declares:

import std::vec;

fn main() -> i32 {
    let mut v = Vec<i32>::new();
    v.push(10);
    v.push(32);
    return v.get(0) + v.get(1);
}

The toolchain also ships a graph library outside std, imported as graph::traversal and friends.

This page is generated from stdlib/std/*.vx by scripts/tools/gen_stdlib_reference.py. Signatures are exactly what the source declares.

Contents

• std::alloc — Raw allocation and deallocation.
• std::box — Box<T>, a single-owner heap allocation. Required for recursive types.
• std::closure — The closure types the compiler lowers |x| ... into.
• std::fs — Files and directories.
• std::googletest — Assertions for tests written in Vx.
• std::hash_map — HashMap<K, V>.
• std::hash_set — HashSet<T>.
• std::io — Standard input, output and error.
• std::iter — The Iterator trait and its adaptors, which for loops and .map build on.
• std::libc — Direct bindings to the C library.
• std::llama — Helpers used by the Llama 2 example.
• std::math — Mathematical functions and constants.
• std::mmap — Memory-mapped files.
• std::net — TCP and UDP sockets.
• std::option — Option<T>, for a value that may be absent.
• std::result — Result<T, E>, for an operation that may fail.
• std::simd — SIMD vector types and operations.
• std::string — String and text manipulation.
• std::tensor — Operations on Tensor, including shape queries and elementwise maths.
• std::time — Clocks and durations.
• std::vec — Vec<T>, a growable array.

std::alloc

Raw allocation and deallocation.

Functions (bound directly to C)

#![allow(unused)]
fn main() {
fn malloc(size : i64) -> *mut i8
fn realloc(ptr : *mut i8, size : i64) -> *mut i8
fn free(ptr : *mut i8) -> i32
}

std::box

Box<T>, a single-owner heap allocation. Required for recursive types.

Types

• struct Box<T>

Box<T> methods

#![allow(unused)]
fn main() {
fn new(val : T) -> Box<T>
fn free(self : &mut Box<T>) -> i32
}

std::closure

The closure types the compiler lowers |x| ... into.

Types

• struct Closure0<Ret>
• struct Closure1<Arg, Ret>
• struct Closure2<Arg1, Arg2, Ret>
• struct Closure3<Arg1, Arg2, Arg3, Ret>

std::fs

Files and directories.

Types

• struct File

File methods

#![allow(unused)]
fn main() {
unsafe fn open(path : *const i8, mode : i32) -> File
unsafe fn read(self : *mut File, buffer : *mut u8, len : i64) -> i64
unsafe fn write(self : *mut File, buffer : *const u8, len : i64) -> i64
fn seek(self : *mut File, offset : i64, whence : i32) -> i64
unsafe fn file_drop(file : *mut File) -> void
}

C bindings (the native functions this module is built on)

#![allow(unused)]
fn main() {
fn vx_file_open(c_path : *const i8, mode : i32) -> *mut i8
fn vx_file_read(ptr : *mut i8, buffer : *mut u8, len : i64) -> i64
fn vx_file_write(ptr : *mut i8, buffer : *const u8, len : i64) -> i64
fn vx_file_seek(ptr : *mut i8, offset : i64, whence : i32) -> i64
fn vx_file_drop(ptr : *mut i8) -> i32
fn fopen(path : *const i8, mode : *const i8) -> *mut i8
fn fread(ptr : *mut u8, size : i64, nmemb : i64, stream : *mut i8) -> i64
fn fclose(stream : *mut i8) -> i32
fn fileno(f : *mut i8) -> i32
fn fseek(f : *mut i8, offset : i64, whence : i32) -> i32
fn ftell(f : *mut i8) -> i64
fn mmap(addr : *mut i8, len : i64, prot : i32, flags : i32, fd : i32, offset : i64) -> *mut i8
fn munmap(addr : *mut i8, len : i64) -> i32
}

std::googletest

Assertions for tests written in Vx.

Types

• trait GoogletestEq

Functions

#![allow(unused)]
fn main() {
fn expect_eq(self : Self, expected : Self) -> i32
}

GoogletestEq for f32 methods

#![allow(unused)]
fn main() {
fn expect_eq(self : f32, expected : f32) -> i32
}

GoogletestEq for i32 methods

#![allow(unused)]
fn main() {
fn expect_eq(self : i32, expected : i32) -> i32
fn expect_eq<T : GoogletestEq>(actual : T, expected : T) -> i32
}

C bindings (the native functions this module is built on)

#![allow(unused)]
fn main() {
fn vx_googletest_expect_eq_f32(actual : f32, expected : f32) -> i32
fn vx_googletest_expect_eq_i32(actual : i32, expected : i32) -> i32
}

std::hash_map

HashMap<K, V>.

Functions (bound directly to C)

#![allow(unused)]
fn main() {
fn vx_hash_map_new_i32_i32() -> *mut i8
fn vx_hash_map_insert_i32_i32(ptr : *mut i8, key : i32, val : i32) -> i32
fn vx_hash_map_get_i32_i32(ptr : *mut i8, key : i32) -> *mut i8
fn vx_hash_map_contains_key_i32_i32(ptr : *mut i8, key : i32) -> Bool
fn vx_hash_map_len_i32_i32(ptr : *mut i8) -> i32
fn vx_hash_map_drop_i32_i32(ptr : *mut i8) -> i32
fn vx_hash_map_new_i32_f32() -> *mut i8
fn vx_hash_map_insert_i32_f32(ptr : *mut i8, key : i32, val : f32) -> i32
fn vx_hash_map_get_i32_f32(ptr : *mut i8, key : i32) -> *mut i8
fn vx_hash_map_contains_key_i32_f32(ptr : *mut i8, key : i32) -> Bool
fn vx_hash_map_len_i32_f32(ptr : *mut i8) -> i32
fn vx_hash_map_drop_i32_f32(ptr : *mut i8) -> i32
}

std::hash_set

HashSet<T>.

Functions (bound directly to C)

#![allow(unused)]
fn main() {
fn vx_hash_set_new_i32() -> *mut i8
fn vx_hash_set_insert_i32(ptr : *mut i8, val : i32) -> i32
fn vx_hash_set_contains_i32(ptr : *mut i8, val : i32) -> Bool
fn vx_hash_set_len_i32(ptr : *mut i8) -> i32
fn vx_hash_set_drop_i32(ptr : *mut i8) -> i32
}

std::io

Standard input, output and error.

Functions

#![allow(unused)]
fn main() {
unsafe fn stdout_write(buffer : *const u8, len : i64) -> i64
unsafe fn stderr_write(buffer : *const u8, len : i64) -> i64
unsafe fn stdin_read(buffer : *mut u8, len : i64) -> i64
}

C bindings (the native functions this module is built on)

#![allow(unused)]
fn main() {
fn vx_stdout_write(buffer : *const u8, len : i64) -> i64
fn vx_stderr_write(buffer : *const u8, len : i64) -> i64
fn vx_stdin_read(buffer : *mut u8, len : i64) -> i64
}

std::iter

The Iterator trait and its adaptors, which for loops and .map build on.

Types

• trait Iterator<T, Item>

Functions

#![allow(unused)]
fn main() {
fn next(self : &mut T) -> Option<Item>
}

Iterator<Map<I, F, Item, NewItem>, NewItem> for Map<I, F, Item, NewItem> methods

#![allow(unused)]
fn main() {
fn next(self : &mut Map<I, F, Item, NewItem>) -> Option<NewItem>
}

Map<I, F, Item, NewItem> methods

#![allow(unused)]
fn main() {
fn collect(self : &mut Map<I, F, Item, NewItem>) -> Vec<NewItem>
}

std::libc

Direct bindings to the C library.

Functions (bound directly to C)

#![allow(unused)]
fn main() {
fn open(path : *const i8, flags : i32) -> i32
fn close(fd : i32) -> i32
fn lseek(fd : i32, offset : i64, whence : i32) -> i64
}

std::llama

Helpers used by the Llama 2 example.

Types

• struct LlamaConfig
• struct TransformerWeightOffsets
• struct Tokenizer

LlamaConfig methods

#![allow(unused)]
fn main() {
fn load(filepath : *const i8) -> LlamaConfig
}

TransformerWeightOffsets methods

#![allow(unused)]
fn main() {
fn calculate(c : &LlamaConfig) -> TransformerWeightOffsets
fn load_all_weights(filepath : *const i8, c : &LlamaConfig) -> Tensor<f32, [?, ?]>
}

Tokenizer methods

#![allow(unused)]
fn main() {
fn load(filepath : *const i8, vocab_size : i32) -> Tokenizer
fn decode(self : &Tokenizer, prev_token : i32, token : i32) -> String
}

C bindings (the native functions this module is built on)

#![allow(unused)]
fn main() {
fn vx_load_config(filepath : *const i8) -> *mut i32
fn vx_load_weights(filepath : *const i8) -> *mut f32
fn vx_build_tokenizer(filepath : *const i8, vocab_size : i32) -> *mut i8
fn vx_decode_token(tokenizer_ptr : *mut i8, prev_token : i32, token : i32) -> *const i8
fn vx_encode_prompt(tokenizer_ptr : *mut i8, text_ptr : *const i8) -> *mut i32
fn vx_read_prompt_file(filepath : *const i8) -> *const i8
fn vx_get_llama_config() -> *mut i32
}

std::math

Mathematical functions and constants.

Types

• trait Math

Functions

#![allow(unused)]
fn main() {
fn sin(self : Self) -> Self
fn cos(self : Self) -> Self
fn tan(self : Self) -> Self
fn abs(self : Self) -> Self
fn sqrt(self : Self) -> Self
fn exp(self : Self) -> Self
fn ln(self : Self) -> Self
fn asin(self : Self) -> Self
fn acos(self : Self) -> Self
fn atan(self : Self) -> Self
fn log2(self : Self) -> Self
fn log10(self : Self) -> Self
}

Math for f32 methods

#![allow(unused)]
fn main() {
fn sin(self : f32) -> f32
fn cos(self : f32) -> f32
fn tan(self : f32) -> f32
fn abs(self : f32) -> f32
fn sqrt(self : f32) -> f32
fn exp(self : f32) -> f32
fn ln(self : f32) -> f32
fn asin(self : f32) -> f32
fn acos(self : f32) -> f32
fn atan(self : f32) -> f32
fn log2(self : f32) -> f32
fn log10(self : f32) -> f32
}

Math for f64 methods

#![allow(unused)]
fn main() {
fn sin(self : f64) -> f64
fn cos(self : f64) -> f64
fn tan(self : f64) -> f64
fn abs(self : f64) -> f64
fn sqrt(self : f64) -> f64
fn exp(self : f64) -> f64
fn ln(self : f64) -> f64
fn asin(self : f64) -> f64
fn acos(self : f64) -> f64
fn atan(self : f64) -> f64
fn log2(self : f64) -> f64
fn log10(self : f64) -> f64
}

C bindings (the native functions this module is built on)

#![allow(unused)]
fn main() {
fn sinf(x : f32) -> f32
fn cosf(x : f32) -> f32
fn tanf(x : f32) -> f32
fn asinf(x : f32) -> f32
fn acosf(x : f32) -> f32
fn atanf(x : f32) -> f32
fn fabsf(x : f32) -> f32
fn sqrtf(x : f32) -> f32
fn expf(x : f32) -> f32
fn logf(x : f32) -> f32
fn log2f(x : f32) -> f32
fn log10f(x : f32) -> f32
fn sin(x : f64) -> f64
fn cos(x : f64) -> f64
fn tan(x : f64) -> f64
fn asin(x : f64) -> f64
fn acos(x : f64) -> f64
fn atan(x : f64) -> f64
fn fabs(x : f64) -> f64
fn sqrt(x : f64) -> f64
fn exp(x : f64) -> f64
fn log(x : f64) -> f64
fn log2(x : f64) -> f64
fn log10(x : f64) -> f64
}

std::mmap

Memory-mapped files.

Functions (bound directly to C)

#![allow(unused)]
fn main() {
fn mmap(addr : *mut i8, length : i64, prot : i32, flags : i32, fd : i32, offset : i64) -> *mut i8
fn munmap(addr : *mut i8, length : i64) -> i32
}

std::net

TCP and UDP sockets.

Types

• struct TcpStream
• struct UdpSocket
• struct TcpListener

TcpStream methods

#![allow(unused)]
fn main() {
unsafe fn connect(addr : *const i8) -> TcpStream
unsafe fn read(self : *mut TcpStream, buffer : *mut u8, len : i64) -> i64
unsafe fn write(self : *mut TcpStream, buffer : *const u8, len : i64) -> i64
unsafe fn tcp_stream_drop(stream : *mut TcpStream) -> void
}

UdpSocket methods

#![allow(unused)]
fn main() {
unsafe fn bind(addr : *const i8) -> UdpSocket
unsafe fn recv(self : *mut UdpSocket, buffer : *mut u8, len : i64) -> i64
unsafe fn send_to(self : *mut UdpSocket, buffer : *const u8, len : i64, addr : *const i8) -> i64
unsafe fn udp_socket_drop(socket : *mut UdpSocket) -> void
}

TcpListener methods

#![allow(unused)]
fn main() {
unsafe fn bind(addr : *const i8) -> TcpListener
fn accept(self : *mut TcpListener) -> TcpStream
unsafe fn tcp_listener_drop(listener : *mut TcpListener) -> void
}

C bindings (the native functions this module is built on)

#![allow(unused)]
fn main() {
fn vx_tcp_stream_connect(c_addr : *const i8) -> *mut i8
fn vx_tcp_stream_read(ptr : *mut i8, buffer : *mut u8, len : i64) -> i64
fn vx_tcp_stream_write(ptr : *mut i8, buffer : *const u8, len : i64) -> i64
fn vx_tcp_stream_drop(ptr : *mut i8) -> i32
fn vx_udp_socket_bind(c_addr : *const i8) -> *mut i8
fn vx_udp_socket_recv(ptr : *mut i8, buffer : *mut u8, len : i64) -> i64
fn vx_udp_socket_send_to(ptr : *mut i8, buffer : *const u8, len : i64, c_addr : *const i8) -> i64
fn vx_udp_socket_drop(ptr : *mut i8) -> i32
fn vx_tcp_listener_bind(c_addr : *const i8) -> *mut i8
fn vx_tcp_listener_accept(ptr : *mut i8) -> *mut i8
fn vx_tcp_listener_drop(ptr : *mut i8) -> i32
}

std::option

Option<T>, for a value that may be absent.

Types

• enum Option<T>

Option<T> methods

#![allow(unused)]
fn main() {
fn is_some(self : &Option<T>) -> Bool
fn is_none(self : &Option<T>) -> Bool
fn unwrap(self : Option<T>) -> T
}

std::result

Result<T, E>, for an operation that may fail.

Functions (bound directly to C)

#![allow(unused)]
fn main() {
fn vx_result_new_ok_i32_i32(val : i32) -> *mut i8
fn vx_result_new_err_i32_i32(err : i32) -> *mut i8
fn vx_result_is_ok_i32_i32(ptr : *mut i8) -> Bool
fn vx_result_is_err_i32_i32(ptr : *mut i8) -> Bool
fn vx_result_unwrap_i32_i32(ptr : *mut i8) -> i32
fn vx_result_drop_i32_i32(ptr : *mut i8) -> i32
}

std::simd

SIMD vector types and operations.

Functions

#![allow(unused)]
fn main() {
unsafe fn simd_add_f32x4(a : *const f32, b : *const f32, out : *mut f32) -> i32
unsafe fn simd_sub_f32x4(a : *const f32, b : *const f32, out : *mut f32) -> i32
unsafe fn simd_mul_f32x4(a : *const f32, b : *const f32, out : *mut f32) -> i32
unsafe fn simd_div_f32x4(a : *const f32, b : *const f32, out : *mut f32) -> i32
unsafe fn simd_fma_f32x4(a : *const f32, b : *const f32, c : *const f32, out : *mut f32) -> i32
}

C bindings (the native functions this module is built on)

#![allow(unused)]
fn main() {
fn vx_simd_add_f32x4(a : *const f32, b : *const f32, out : *mut f32) -> i32
fn vx_simd_sub_f32x4(a : *const f32, b : *const f32, out : *mut f32) -> i32
fn vx_simd_mul_f32x4(a : *const f32, b : *const f32, out : *mut f32) -> i32
fn vx_simd_div_f32x4(a : *const f32, b : *const f32, out : *mut f32) -> i32
fn vx_simd_fma_f32x4(a : *const f32, b : *const f32, c : *const f32, out : *mut f32) -> i32
}

std::string

String and text manipulation.

Types

• struct String

String methods

#![allow(unused)]
fn main() {
fn new() -> String
unsafe fn from_c_str(c_str : *const i8) -> String
unsafe fn push_c_str(self : *mut String, c_str : *const i8) -> i32
fn len(self : *mut String) -> i32
fn as_c_str(self : *mut String) -> *const i8
fn drop(self : *mut String) -> i32
}

i32 methods

#![allow(unused)]
fn main() {
fn to_string(self : i32) -> String
unsafe fn string_length(s : *const i8) -> i32
unsafe fn string_compare(s1 : *const i8, s2 : *const i8) -> i32
unsafe fn parse_int(s : *const i8) -> i32
}

C bindings (the native functions this module is built on)

#![allow(unused)]
fn main() {
fn vx_string_new() -> *mut i8
fn vx_string_from_c_str(ptr : *const i8) -> *mut i8
fn vx_string_push_c_str(ptr : *mut i8, c_str : *const i8) -> i32
fn vx_string_len(ptr : *mut i8) -> i32
fn vx_string_as_c_str(ptr : *mut i8) -> *const i8
fn vx_string_free_c_str(ptr : *const i8) -> i32
fn vx_string_drop(ptr : *mut i8) -> i32
fn vx_i32_to_string(val : i32) -> *mut i8
}

std::tensor

Operations on Tensor, including shape queries and elementwise maths.

Tensor<T, [?, ?]> methods

#![allow(unused)]
fn main() {
fn from_ptr_1d(ptr : *mut T, d1 : i32) -> Tensor<T, [?, ?]>
fn from_ptr_2d(ptr : *mut T, d1 : i32, d2 : i32) -> Tensor<T, [?, ?]>
fn slice_2d(self : &Tensor<T, [?, ?]>, row : i32, d1 : i32, d2 : i32) -> Tensor<T, [?, ?]>
fn slice_2d_from_1d(self : &Tensor<T, [?, ?]>, start : i32, d1 : i32, d2 : i32) -> Tensor<T, [?, ?]>
fn slice_1d(self : &Tensor<T, [?, ?]>, start : i32, d1 : i32) -> Tensor<T, [?, ?]>
fn fill(self : &mut Tensor<T, [?, ?]>, val : T) -> void
fn copy(self : &mut Tensor<T, [?, ?]>, src : &Tensor<T, [?, ?]>) -> void
fn assign(self : &mut Tensor<T, [?, ?]>, val : T) -> void
fn compare(self : &Tensor<T, [?, ?]>, other : &Tensor<T, [?, ?]>) -> bool
}

Tensor<T, [N, M]> methods

#![allow(unused)]
fn main() {
fn fill_static(self : &mut Tensor<T, [ N, M ]>, val : T) -> void
}

std::time

Clocks and durations.

Functions

#![allow(unused)]
fn main() {
fn now() -> f32
fn sleep(seconds : f32) -> i32
fn unix_timestamp() -> f64
unsafe fn bench_report(name : *const i8, unit : *const i8, value : f32) -> i32
}

C bindings (the native functions this module is built on)

#![allow(unused)]
fn main() {
fn vx_get_time() -> f32
fn vx_sleep(seconds : f32) -> i32
fn vx_unix_timestamp() -> f64
fn vx_bench_report(name : *const i8, unit : *const i8, value : f32) -> i32
}

std::vec

Vec<T>, a growable array.

Types

• struct Vec<T>
• struct VecIter<T>
• struct VecMap<T, NewItem>

Vec<T> methods

#![allow(unused)]
fn main() {
fn new() -> Vec<T>
fn with_capacity(capacity : i32) -> Vec<T>
fn free(self : &mut Vec<T>) -> i32
fn as_mut_ptr(self : &Vec<T>) -> *mut T
fn as_mut_slice(self : &mut Vec<T>) -> &mut T
fn as_slice(self : &Vec<T>) -> &T
fn push(self : &mut Vec<T>, val : T) -> i32
fn get(self : &Vec<T>, index : i32) -> T
fn set(self : &mut Vec<T>, index : i32, val : T) -> i32
fn len(self : &Vec<T>) -> i32
fn iter(self : &Vec<T>) -> VecIter<T>
}

Iterator<VecIter<T>, T> for VecIter<T> methods

#![allow(unused)]
fn main() {
fn next(self : &mut VecIter<T>) -> Option<T>
}

VecIter<T> methods

#![allow(unused)]
fn main() {
fn map<NewItem>(self : VecIter<T>, f : Closure1<T, NewItem>) -> VecMap<T, NewItem>
}

Iterator<VecMap<T, NewItem>, NewItem> for VecMap<T, NewItem> methods

#![allow(unused)]
fn main() {
fn next(self : &mut VecMap<T, NewItem>) -> Option<NewItem>
}

VecMap<T, NewItem> methods

#![allow(unused)]
fn main() {
fn collect(self : &mut VecMap<T, NewItem>) -> Vec<NewItem>
}

C bindings (the native functions this module is built on)

#![allow(unused)]
fn main() {
fn vx_vec_alloc(elem_size : i64, cap : i64) -> *mut i8
fn vx_vec_grow(ptr : *mut i8, old_cap : i64, new_cap : i64, elem_size : i64) -> *mut i8
fn vx_vec_free(ptr : *mut i8, cap : i64, elem_size : i64) -> i32
fn vx_vec_bounds_check(index : i64, len : i64) -> i32
}

228 functions across 21 modules.

Diagnostic index

Every diagnostic the Vx compiler can emit, with the code it reports and what it means.

Codes are grouped by the compilation stage that raises them, and the group is readable off the number: E1xxx is the parser, E3xxx the type checker, E6xxx the placement and capacity rules, and so on. A W prefix is a warning rather than an error.

This file is generated from src/diagnostic.rs by scripts/tools/gen_error_index.py. Edit the doc comments on the codes there, not this file.

Contents

• Warnings — W1001–W1031 (23 codes)
• Parser Errors — E1001–E1013 (13 codes)
• Name Resolution Errors — E2001–E2007 (7 codes)
• Type Errors — E3001–E3029 (29 codes)
• Borrow/Ownership Errors — E4001–E4005 (5 codes)
• Safety Errors — E5001–E5002 (2 codes)
• Topology/Hardware Errors — E6001–E6028 (28 codes)
• Tensor/Math Errors — E7001–E7004 (4 codes)
• Contract/Verification Errors — E8001–E8002 (2 codes)

Warnings

Reported without stopping the compile. A warning means the program is accepted but something in it is probably not what was intended.

Parser Errors

Raised while turning source text into an AST. The program is not syntactically valid Vx.

Name Resolution Errors

Raised when a name cannot be resolved to a declaration, or resolves to something of the wrong kind.

Type Errors

Raised by the type checker. Vx performs no implicit numeric conversion, so many of these are mismatches that a language with coercion would have silently accepted.

Borrow/Ownership Errors

Raised by the borrow checker and the linear-type rules. These rule out use-after-move, aliasing violations and lifetimes that outlive what they point at.

Safety Errors

Raised where an operation needs an unsafe context and does not have one.

Topology/Hardware Errors

Raised by the placement and capacity rules — the checks that make Vx different from a single-address-space language. A value in the wrong memory space, a region on the wrong device, a working set that does not fit, or a transfer with no declared route.

Tensor/Math Errors

Raised on tensor shapes and numeric operations, including shape mismatches that are decided at compile time.

Contract/Verification Errors

Raised when a requires, ensures or invariant clause cannot be discharged, or when a seam obligation is left unproven.

113 diagnostics.

The compiler

Actions

vxc runs one action per invocation. The default is run-jit.

vxc --run program.vx
vxc -c program.vx -o program.o
vxc --emit-mlir program.vx

Optimization is -O0 through -O3, defaulting to -O0.

Hardware and machine models

--diagnostics-json is the one to reach for in a build script or a CI job. The schema is versioned, and a capacity rejection carries the space, the requirement, the availability and the margin as fields rather than as prose you would have to parse out of a message.

Note that with --verify-seams and no solver on PATH, the compile fails rather than certifying seams it could not check. VX_ALLOW_UNVERIFIED=1 downgrades that to a warning.

Separate compilation

--emit-interface writes a .vxlib: the module’s frozen registry and portable flat-HIR bodies. A downstream compile consumes it with --link-interface and resolves calls into that module without parsing its source.

vxc --emit-interface lib.vx -o lib.vxlib
vxc --link-interface lib.vxlib main.vx -o main

The .vxlib format carries a version tag, and a compiler rejects artifacts written by a different one. Regenerate them when you upgrade the toolchain rather than keeping them in a cache.

The other tools

vx-format has no options worth learning: there is one canonical style, and it applies it.

vx-format src/*.vx

The standard library

21 modules, imported as std::<name>. Every type and function is listed in the standard library reference, generated from the sources.

Beyond std the toolchain ships graph, imported as graph::traversal and friends.

The repository also carries examples/llama.vx, a Llama 2 inference port, and an early packages/vx_linalg. Several other package directories exist under packages/ but are still empty placeholders — do not plan around them yet.

Environment variables

An installed toolchain sets the first several of these for you through a wrapper script, so you normally need none of them.

Editor support

VS Code

The extension lives in vscode-vx/ in the repository. It provides syntax highlighting and connects to the language server.

Until it is published to the marketplace, install it from source:

cd vscode-vx
npm install
npm run package
code --install-extension vx-*.vsix

The language server

vx-analyzer speaks the Language Server Protocol, so any LSP-capable editor can use it. It ships with the toolchain, at ~/.vx/bin/vx-analyzer for a standard install.

Point your editor’s LSP client at that binary for files with the .vx extension. In Neovim with nvim-lspconfig, for example, that is a cmd of { "vx-analyzer" } and a filetypes of { "vx" }.

Formatting

vx-format is the canonical formatter. There is one style and no configuration:

vx-format path/to/file.vx

It rewrites files in place. Wire it to format-on-save in your editor, and run it over a directory before committing — the project’s CI checks that tracked .vx files are formatted.

Contributing

Vx is early. The most valuable contribution right now is a clear bug report: a program that should compile and does not, or one that compiles and does the wrong thing.

Reporting a bug

Open an issue at github.com/vx-lang/Vx/issues with:

• the smallest .vx file that reproduces it,
• the exact command you ran,
• what you expected and what happened,
• vxc --version and your platform.

If the compiler produced MLIR, --emit-mlir output is often the fastest way to show what went wrong.

Your first change

Issues labelled good first issue are self-contained and do not assume you know the compiler. Each one states the problem, shows the current behaviour, and says what the fix should look like.

A sample of what is open:

If one of these is unclear, say so on the issue. A first issue that cannot be picked up cold is a bug in the issue, not in you.

help wanted holds larger pieces that are still well specified.

Working on the compiler

Start with building from source. Once cargo test passes you have a working development setup.

For how the compiler is put together — the phase pipeline, the two code generators, how to add a language feature, and how the test tiers work — read the developer guide.

The repository layout:

src/                the vxc compiler (Rust)
  lexer, parser/    source to AST
  syntax/           AST, types, topologies, declarations
  hir/              lowering, type checking, borrow checking
    check/          transfer, calls, access, autodiff, region traffic
    memory.rs       the memory algebra: containment, capacity, derived cost
    seam.rs         asynchronous-visibility contracts
    flatten.rs      the flat, AST-annihilated path
  codegen/          MLIR emission
  dialect/          the Vx dialect and its lowering (C++)
  plugin/           vendor MLIR pass plugins
fleet/              machine files
runtime/            dispatch and the distributed fleet runtime (C++)
stdlib/             the standard library
vx-analyzer/        language server
tests/              integration suites and unit tests

Conventions worth knowing

No locks in the compiler. A compilation has to be isolated, and CI rejects Mutex, RwLock, OnceLock and friends anywhere under src/. Process-global atomics are banned for the same reason: a static that a worker thread can write is shared mutable state whether or not it takes a lock to do it, and a cached answer survives across compilations in a long-lived process such as the language server.

Determinism is gated, not hoped for. Several tests assert that the pipeline emits byte-identical MLIR at one thread, at four, and with the thread pool off the path entirely. If your change makes output depend on iteration order, those will catch it.

Format before you commit. cargo fmt for Rust, vx-format for .vx files, clang-format for C++. CI checks all three, and clippy runs with -D warnings.

Tests come with the change. New backend behaviour needs a fixture under tests/; the check lines are generated by utils/update_mlir_test_checks.rs rather than written by hand.

Extending the compiler for new hardware

Vendors are not expected to patch the compiler. A new accelerator arrives as:

1. a machine file declaring its memory hierarchy and interconnect, and
2. an MLIR pass plugin under src/plugin/ that lowers the Vx dialect for that target.

docs/adding_a_topology.md walks through the process.