The Inference Programming Language

Warning

The Inference programming language is currently under development. If you see this message, it means that the first stable release is not out yet. However, this book describes the current state of the language and currently available features. Therefore, feel free to explore and try out Inference!

To follow updates about the language and its development, follow the dev team’s official social media channels ・・・

We welcome contributions from the community. You can help improve Inference by trying out the language and sharing your experience, providing feedback on language features and design decisions, reporting implementation bugs, suggesting improvements to this documentation, or discussing new features on our Discord. Your input helps shape the development of Inference.

Foreword

Software correctness is a cornerstone of reliable computing systems. As humanity invents and develops more sophisticated and immersive technologies, the demand for resilient software that behaves exactly as intended has become increasingly critical. We have always had systems that must never fail because their real-world side effects are irreversible by nature. For example, nuclear power plant control software should never drain coolant from a reactor, and cars must never deploy airbags at highway speeds when no collision occurred.

The Inference project started in January 2023 to address the challenges that this new era of computing brings. With the advent of blockchain and cryptographic protocols, quantum computing, AI-managed systems, and robotics, the need for software that is provably correct and secure has never been more pressing. No one wants a household robot to decide to iron clothes that are currently being worn by someone. Likewise, smart contract exploits do more than just drain funds, they hinder the evolution of financial systems.

Traditional testing and debugging methods, while useful, often fall short of providing absolute guarantees about program behavior. Formal Verification (FV), despite being one of the most advanced and reliable techniques for ensuring the correctness of algorithm implementations, has for decades been underrepresented and used primarily in aerospace, military, and other safety-critical industries.

Inference aims to bring Formal Verification into the software engineering mainstream.

Introduction

You are reading a book about The Inference Programming Language. With Inference, you can write highly reliable, mission-critical programs with a high level of confidence that they will behave exactly as intended. Inference is designed from the ground up to support formal verification (FV) of program properties, allowing you to prove code correctness mathematically with machine-checked proofs of behavior without needing to learn complex mathematical theories or specialized verification tools. Inference lets you write programs and their specifications in the same language and even in the same file, much like you would do with unit tests.

Who Inference Is For

The key power of Inference is that it has formal verification built-in from the start. Therefore, Inference is best suited for developing high assurance software. Here are some groups of people who will benefit the most from using Inference.

Developer Teams

Inference provides a way to rigorously ensure the correctness of code through formal verification. For development teams working on mission-critical applications, this means they can obtain mathematical guarantees that specified properties of their programs always hold, rather than relying solely on testing and code review. This leads to substantially lower residual defect risk, higher quality software, increased reliability, and improved safety of its users.

Examples of such software include, but are not limited to:

• Cryptographic software and security systems
• Various vehicle control systems (e.g., automotive, aerospace, marine)
• Medical devices and healthcare software
• Design and production of chips and circuits
• Blockchain, financial systems and banking software
• Industrial automation and control systems

Researchers

Traditionally, formal verification has been a complex and specialized field, requiring deep knowledge of mathematical theories and specialized tools. Most of the existing formal verification tools are used by experts from academia and research institutions. Inference lowers the barrier of entry for researchers and provides a unified platform for writing and verifying code, making it easier to explore new ideas and push the boundaries of what is possible with formal verification.

Students

Students learning computer science can benefit from using Inference to gain a deeper understanding of programming languages, mathematical logic, reasoning, and formal verification concepts. By using Inference, students can learn how to write correct and reliable code from the start, developing good programming habits that will serve them well in their future careers.

People Who Value Reliability and Safety

Inference is an excellent choice for anyone who values reliability and safety in their software. Whether you are developing software for personal use or an open source library for a larger audience, Inference provides a way to ensure that your code behaves as intended and meets the highest standards of quality and reliability.

Who This Book Is For

This book assumes that you are already familiar with at least one programming language with systems-programming capabilities. However, no prior knowledge of formal verification or mathematical logic is required. The book will guide you through the key concepts of the Inference programming language and its formal verification capabilities, providing practical examples and exercises to help you learn by doing.

Common programming concepts will not be covered in depth, but sufficient explanations and examples will be provided to help you get started quickly.

New concepts and semantics specific to Inference will be explained thoroughly, with a sufficient amount of detail and examples.

How to Use This Book

Read this book in the order it is presented, from start to finish. Each chapter builds upon the previous one and newly introduced concepts will be used in the subsequent chapters.

Additional resources and references are provided in the appendix section for further reading and exploration. The infs CLI Reference appendix provides a complete guide to the toolchain manager.

Source Code

The source files from which this book is generated can be found on GitHub.

Getting Started

In this chapter, we will discuss the following topics:

• Installing Inference on Linux, macOS, and Windows
• Writing a program that returns a mysterious number 42

Installation

The recommended way to install Inference is via infs, the unified toolchain manager. infs downloads the compiler, manages multiple toolchain versions, and configures your PATH automatically.

Command Line Notation

In this book, commands you should type in a terminal start with $. Do not type the $ itself; it is just the prompt. Lines without $ show the output of the previous command. PowerShell examples use > instead of $.

Recommended: install with infs

Download the infs binary for your platform from the GitHub Releases page, place it on your PATH, then install a compiler toolchain:

$ infs install

On first install, infs configures your shell PATH automatically:

• Linux/macOS: appends ~/.inference/bin to ~/.bashrc, ~/.zshrc, or ~/.config/fish/config.fish.
• Windows: updates the user PATH in the registry.

After installation, restart your terminal (or source your shell profile) and verify:

$ infs version
$ infc --version

You should see both versions printed.

To install a specific toolchain version instead of the latest:

$ infs install 0.0.1

See Appendix D - infs CLI Reference for the full set of toolchain commands (list, default, doctor, uninstall, self update).

Manual installation

If you prefer to manage the compiler binary yourself — for CI environments, sandboxed setups, or to integrate infc into an existing build system — download the standalone compiler from the infc GitHub Releases page. It is a single binary with no external dependencies.

Linux and macOS

Download the release archive and extract the infc binary:

$ tar xzf infc-linux-x64.tar.gz

Windows

Download the zip archive and extract infc.exe. No additional libraries or dependencies are required.

Adding infc to your PATH

On Linux/macOS, add the following line to your shell configuration file (e.g., ~/.bashrc, ~/.zshrc):

$ export PATH=$PATH:/path/to/infc-directory

On Windows, run the following in PowerShell:

> $env:Path += ";C:\path\to\infc-directory"

Verifying the download

To verify the integrity of the downloaded package, check its SHA256 checksum. The checksum is listed on the GitHub Releases page.

On Linux/macOS:

$ sha256sum infc-linux-x64.tar.gz

On Windows:

> Get-FileHash infc-windows-x64.zip -Algorithm SHA256

Installing a WebAssembly runtime

To run compiled WebAssembly modules, you need a WASM runtime. This book uses wasmtime, a popular and easy-to-use runtime. Visit its official website for installation instructions.

Note

wasmtime is only needed if you want to execute compiled programs locally. The Inference compiler itself does not require it.

Editor support

Inference has an official Visual Studio Code extension that provides syntax highlighting and language support. Install it from the VS Code Marketplace or search for “Inference” in the VS Code extensions panel.

Hello World

Traditionally, the very first program you write when learning a new programming language is one that prints “Hello, World!” to the screen. In Inference, however, we do not have built-in string and printing functionality. Instead, we will write a simple program that returns a magic number from a function. Later, by executing this program, we will see the result in the terminal.

Writing the Program

First, we need to create a new file for our program. Inference uses the .inf file extension for its source code files. Create a new file named hello_world.inf and open it in your favorite text editor. Then, add the following code to the file:

pub fn hello_world() -> i32 {
    return 42;
}

This code defines a function named hello_world that takes no parameters and returns a 32-bit signed integer (i32). The function simply returns the number 42.

Understanding the Code

Let’s break down the code to understand its components:

• pub is a visibility keyword that marks the function as exported from the compiled WebAssembly module, making it callable from outside;
• fn is a keyword used to define a function in Inference;
• hello_world is the name of the function;
• () is a pair of parentheses that groups the function parameters. In this case, there are no parameters;
• -> reads as “right arrow” and indicates the return type of the function;
• i32 specifies that the function returns a 32-bit signed integer;
• return is a keyword used to return a value from a function;
• 42 is the integer value (or literal) being returned by the function.

In the appendix, Language Reference, you can find more information about Inference keywords and data types.

Compiling the Program

To compile an .inf file into a WebAssembly module, use the infs build command. Open your terminal, navigate to the directory where you saved hello_world.inf, and run the following command:

On Linux or macOS:

$ infs build hello_world.inf

On Windows:

> infs build hello_world.inf

The compiler will generate a WebAssembly binary module at out/hello_world.wasm.

Note

You can also use the infc compiler directly as an alternative:

$ infc hello_world.inf

Both commands produce the same output.

Running the Program

To execute the compiled WebAssembly module, we can use any preferred Wasm runtime. In this example and throughout this book, we will use wasmtime, a popular and easy-to-use Wasm runtime. You can install and learn more about wasmtime from its official website.

Once you have wasmtime installed, you can run the compiled module using the following command:

On Linux or macOS:

$ wasmtime out/hello_world.wasm --invoke hello_world

On Windows:

> wasmtime out/hello_world.wasm --invoke hello_world

As a result, you will see the output 42 printed in the terminal, which is the value returned by the hello_world function.

Congratulations! You have successfully written, compiled, and executed your first Inference program. In the next chapters, we will explore more features of the Inference programming language.

Common Programming Concepts

This chapter covers common programming concepts that are shared across many programming languages. It does not focus on Inference-specific features. Instead, it presents Inference as a high-assurance, software-oriented programming language and introduces the core principles and syntax you need to write executables and libraries in Inference.

In this chapter, we cover data types, variables and mutability, functions, and comments. Understanding these concepts is essential for writing programs in Inference.

The chapters that follow will build on these concepts with expressions and operators, control flow, and arrays.

Inference keywords, data types, and other language constructs are covered in the Language Reference appendix.

Data Types

Inference is a statically typed language — every value and variable must have a known type at compile time.

Integer Types

Inference supports both signed and unsigned integer types:

let small: i8 = 127;
let byte: u8 = 255;
let number: i32 = 42;
let big: i64 = 1000000;
let positive: u32 = 0;

i32 is the most common integer type and maps directly to a 32-bit integer in WebAssembly.

Boolean Type

let flag: bool = true;
let done: bool = false;

Array Type

Fixed-size arrays are written as [T; N], where T is the element type and N is a compile-time constant:

let numbers: [i32; 3] = [1, 2, 3];

See Arrays for full coverage.

Struct Type

User-defined types with named fields:

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

let p: Point = Point { x: 10, y: 20 };

Methods are declared inside the struct body, after the fields — see Functions for details.

Enum Type

A type with a fixed set of named variants:

enum Color { Red, Green, Blue }

let c: Color = Color::Red;

See Enums for full coverage.

Floating-Point Types

Inference does not support floating-point types. It uses integer arithmetic to ensure determinism and precision in computations.

Variables and Mutability

Variables

Variables are declared with let, and require a type annotation and an initial value:

let x: i32 = 42;
let flag: bool = true;

Inference does not infer types — every variable must have an explicit type annotation.

Immutability by Default

Variables are immutable by default. Use let mut to allow reassignment:

let x: i32 = 5;
// x = 6;  // compiler error: x is not mutable

let mut y: i32 = 5;
y = 6;  // OK

Constants

Constants are declared with const and must be initialized with a literal value:

const MAX_SIZE: i32 = 100;
const THRESHOLD: i64 = 50000;
const ENABLED: bool = true;

Functions

A program is a sequence of instructions (or operations) that the computer executes to perform a specific task. Conceptually, a program is a function: it takes some input and produces some output. To write complex programs, we use functions as building blocks to decompose a program into smaller, manageable pieces. Similarly, libraries provide reusable functions that can be called from different programs. The Inference programming language is all about writing functions. As we saw in Hello World, the smallest Inference program is a function.

Anatomy of a Function

pub fn function_name(param1: Type1, param2: Type2) -> ReturnType {
    // function body
}

• pub makes the function exported from the compiled WebAssembly module. Without pub, a function is private to the file.
• -> ReturnType declares the return type. Functions without it return nothing.
• return is required to return a value — there are no implicit returns.

Parameters

Each parameter has a name and a type annotation:

pub fn add(a: i32, b: i32) -> i32 {
    return a + b;
}

Parameters are immutable by default. Declare with mut to allow modification inside the function body. All values are passed by copy — mutating a parameter does not affect the caller:

pub fn increment_and_return(mut x: i32) -> i32 {
    x = x + 1;
    return x;
}

Calling Functions

pub fn example() -> i32 {
    let result: i32 = add(10, 20);
    return result;
}

Function Body

A function body is a sequence of statements enclosed in curly braces {}.

Methods

Methods are declared inside the struct body, after the field list. Instance methods take self (or mut self) as the first parameter. Associated functions omit self and are called with ::.

struct Counter {
    value: i32;

    fn get(self) -> i32 {
        return self.value;
    }
    fn increment(mut self) {
        self.value = self.value + 1;
    }
    fn new(v: i32) -> Counter {
        return Counter { value: v };
    }
}

pub fn example() -> i32 {
    let c: Counter = Counter::new(10);
    c.increment();
    return c.get();
}

(module $methods
  (type (;0;) (func (result i32)))
  (type (;1;) (func (param i32) (result i32)))
  (type (;2;) (func (param i32)))
  (type (;3;) (func (param i32 i32)))
  (memory (;0;) 1 1)
  (global (;0;) (mut i32) i32.const 65536)
  (export "example" (func $example))
  (export "memory" (memory 0))
  (export "__stack_pointer" (global 0))
  (func $example (;0;) (type 0) (result i32)
    (local $c i32) (local $__frame_ptr i32)
    global.get 0
    i32.const 16
    i32.sub
    local.tee $__frame_ptr
    global.set 0
    local.get $__frame_ptr
    i32.const 0
    i32.const 16
    memory.fill
    local.get $__frame_ptr
    i32.const 10
    call $Counter.new
    local.get $__frame_ptr
    local.set $c
    local.get $c
    call $Counter.increment
    local.get $c
    call $Counter.get
    local.get $__frame_ptr
    i32.const 16
    i32.add
    global.set 0
    return
    unreachable
  )
  (func $Counter.get (;1;) (type 1) (param $self i32) (result i32)
    local.get $self
    i32.load
    return
    unreachable
  )
  (func $Counter.increment (;2;) (type 2) (param $self i32)
    (local $__frame_ptr i32)
    global.get 0
    i32.const 16
    i32.sub
    local.tee $__frame_ptr
    global.set 0
    local.get $__frame_ptr
    i32.const 0
    i32.const 16
    memory.fill
    local.get $__frame_ptr
    local.get $self
    i32.const 4
    memory.copy
    local.get $__frame_ptr
    local.set $self
    local.get $self
    local.get $self
    i32.load
    i32.const 1
    i32.add
    i32.store
    local.get $__frame_ptr
    i32.const 16
    i32.add
    global.set 0
  )
  (func $Counter.new (;3;) (type 3) (param $sret i32) (param $v i32)
    local.get $sret
    local.get $v
    i32.store
    return
    unreachable
  )
)

Definition example : module_func := {|
  modfunc_type := 0%N;
  modfunc_locals := T_num T_i32 :: T_num T_i32 :: nil;
  modfunc_body :=
    BI_global_get 0%N ::
    BI_const_num (Vi32 16) ::
    BI_binop T_i32 (Binop_i BOI_sub) ::
    BI_local_tee 1%N (*__frame_ptr*) ::
    BI_global_set 0%N ::
    BI_local_get 1%N (*__frame_ptr*) ::
    BI_const_num (Vi32 10) ::
    BI_call 3 ::
    BI_local_get 1%N (*__frame_ptr*) ::
    BI_local_set 0%N (*c*) ::
    BI_local_get 0%N (*c*) ::
    BI_call 2 ::
    BI_local_get 0%N (*c*) ::
    BI_call 1 ::
    BI_return ::
    nil;
|}.

(* The Counter.get / Counter.increment / Counter.new definitions and the
   final `Definition methods : module := { ... }` are produced in the same
   file. See `out/<name>.v` for the complete translation. *)

Counter::new(10) is an associated function call — note the :: — and produces a fresh Counter. c.increment() and c.get() are instance method calls using ..

Note

mut self lets the method body mutate its own copy of the receiver, but the caller’s value is not affected. Like every other parameter, self is passed by copy — after c.increment() returns, c in the caller is unchanged. This is enforced by the same value-copy semantics described under Parameters above.

Comments

Programmers often use comments to explain parts of the code that might be hard to understand or that need additional context. Comments can also describe, at a high level, what a file or function is responsible for. For these purposes, Inference supports two kinds of comments: single-line comments and docstring-style comments. Both kinds of comments are ignored by the compiler and are not part of the program itself.

Here is a simple single-line comment:

// This is a single-line comment

This is treated as a comment because the line starts with the two characters //. Everything that follows // on the same line is considered a comment and is ignored by the compiler.

You can attach a comment to a line of code, for example:

42; // The universal answer

For more descriptive explanations, Inference supports docstring-style comments that can span multiple lines. These comments start with triple forward slashes ///. Each line that begins with /// is treated as part of the same docstring comment block. For example:

/// This library provides verified cryptographic functions and primitives
/// for working with zero-knowledge proofs.

Expressions and Operators

• Arithmetic operators — +, -, *, /, %, unary -
• Comparison and logical operators — ==, !=, <, >, &&, ||, !
• Bitwise operators — &, |, ^, ~, <<, >>

Arithmetic Operators

All operators work with every integer type. Parentheses control evaluation order: (a + b) * c.

Integer Overflow

Integer arithmetic wraps on overflow, matching WebAssembly semantics. For i8, 127 + 1 wraps to -128. For u8, 0 - 1 wraps to 255. No runtime error is raised.

Division by Zero

Division and remainder by zero trap at runtime. Guard against it if the divisor may be zero:

pub fn safe_divide(a: i32, b: i32) -> i32 {
    if b == 0 {
        return 0;
    }
    return a / b;
}

Comparison and Logical Operators

Comparison Operators

All return bool. Work with all integer types. Sign-aware: i32 uses signed comparison, u32 uses unsigned.

Note

Enum values support == and != only.

Logical Operators

Operate on bool values:

Example

pub fn is_in_range(x: i32, lo: i32, hi: i32) -> bool {
    return (x >= lo) && (x <= hi);
}

Bitwise Operators

All operators work with every integer type. >> is arithmetic for signed types, logical for unsigned types.

Example

pub fn get_bit(x: i32, pos: i32) -> i32 {
    return (x >> pos) & 1;
}

pub fn set_bit(x: i32, pos: i32) -> i32 {
    return x | (1 << pos);
}

pub fn clear_bit(x: i32, pos: i32) -> i32 {
    return x & ~(1 << pos);
}

pub fn is_power_of_two(n: i32) -> bool {
    if n <= 0 {
        return false;
    }
    return (n & (n - 1)) == 0;
}

Control Flow

• Conditional statements — if and else
• Loops — loop and break
• Assertions — assert

Conditional Statements

if / else

pub fn max(a: i32, b: i32) -> i32 {
    if a > b {
        return a;
    } else {
        return b;
    }
}

if / else if / else

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

Important Differences

if is a statement, not an expression. You cannot write let x: i32 = if condition { 1 } else { 2 };. Use a mutable variable instead:

pub fn example(condition: bool) -> i32 {
    let mut result: i32 = 0;
    if condition {
        result = 1;
    } else {
        result = 2;
    }
    return result;
}

The condition must be bool. Inference does not coerce integers to booleans. Write if x != 0 { ... } instead of if x { ... }.

Curly braces are required, even for single-statement branches.

Loops

Inference uses loop for both conditional and infinite loops. There is no while or for.

Conditional Loop

pub fn sum_to_n(n: i32) -> i32 {
    let mut sum: i32 = 0;
    let mut i: i32 = 1;
    loop i <= n {
        sum = sum + i;
        i = i + 1;
    }
    return sum;
}

loop condition { body } checks the condition before each iteration. If false initially, the body never runs.

Infinite Loop

pub fn find_first_multiple(n: i32, target: i32) -> i32 {
    let mut x: i32 = n;
    loop {
        if x % target == 0 {
            break;
        }
        x = x + 1;
    }
    return x;
}

loop { body } runs until break or return.

break

break exits the innermost enclosing loop. continue is not yet supported.

Nested Loops

pub fn nested_count() -> i32 {
    let mut total: i32 = 0;
    let mut i: i32 = 0;
    loop i < 3 {
        let mut j: i32 = 0;
        loop j < 4 {
            total = total + 1;
            j = j + 1;
        }
        i = i + 1;
    }
    return total;
}

Assertions

assert(cond) evaluates a bool expression. If cond is false, the program traps and the WebAssembly runtime reports unreachable code reached. If cond is true, execution continues to the next statement.

Assertions are intended for invariants you expect to always hold — preconditions on function arguments, postconditions on intermediate results, or sanity checks around tricky logic.

Simple Assertion

pub fn checked_div(numerator: i32, denominator: i32) -> i32 {
    assert(denominator != 0);
    return numerator / denominator;
}

(module $assert_simple
  (type (;0;) (func (param i32 i32) (result i32)))
  (export "checked_div" (func $checked_div))
  (func $checked_div (;0;) (type 0) (param $numerator i32) (param $denominator i32) (result i32)
    local.get $denominator
    i32.const 0
    i32.ne
    i32.eqz
    if ;; label = @1
      unreachable
    end
    local.get $numerator
    local.get $denominator
    i32.div_s
    return
    unreachable
  )
)

Definition checked_div : module_func := {|
  modfunc_type := 0%N;
  modfunc_locals := nil;
  modfunc_body :=
    BI_local_get 1%N (*denominator*) ::
    BI_const_num (Vi32 0) ::
    BI_relop T_i32 (Relop_i ROI_ne) ::
    BI_testop T_i32 TO_eqz ::
    BI_if (BT_valtype None) (
      BI_unreachable ::
      nil) (
      nil) ::
    BI_local_get 0%N (*numerator*) ::
    BI_local_get 1%N (*denominator*) ::
    BI_binop T_i32 (Binop_i (BOI_div SX_S)) ::
    BI_return ::
    BI_unreachable ::
    nil;
|}.

The compiler lowers assert(cond) to cond; i32.eqz; if; unreachable; end — the smallest WASM shape that traps when the condition fails. In the Rocq translation, the same pattern becomes a BI_if block whose only effect on the failing branch is BI_unreachable.

Compound Conditions

assert accepts any boolean expression, including conjunctions, disjunctions, negations, and comparisons.

pub fn in_range(value: i32, low: i32, high: i32) -> i32 {
    assert((value >= low) && (value <= high));
    return value;
}

(module $assert_compound
  (type (;0;) (func (param i32 i32 i32) (result i32)))
  (export "in_range" (func $in_range))
  (func $in_range (;0;) (type 0) (param $value i32) (param $low i32) (param $high i32) (result i32)
    local.get $value
    local.get $low
    i32.ge_s
    local.get $value
    local.get $high
    i32.le_s
    i32.and
    i32.eqz
    if ;; label = @1
      unreachable
    end
    local.get $value
    return
    unreachable
  )
)

Definition in_range : module_func := {|
  modfunc_type := 0%N;
  modfunc_locals := nil;
  modfunc_body :=
    BI_local_get 0%N (*value*) ::
    BI_local_get 1%N (*low*) ::
    BI_relop T_i32 (Relop_i (ROI_ge SX_S)) ::
    BI_local_get 0%N (*value*) ::
    BI_local_get 2%N (*high*) ::
    BI_relop T_i32 (Relop_i (ROI_le SX_S)) ::
    BI_binop T_i32 (Binop_i BOI_and) ::
    BI_testop T_i32 TO_eqz ::
    BI_if (BT_valtype None) (
      BI_unreachable ::
      nil) (
      nil) ::
    BI_local_get 0%N (*value*) ::
    BI_return ::
    BI_unreachable ::
    nil;
|}.

Note

Assertions are emitted in both compilation modes — compile and proof. They are not a verification-only construct; the trap is part of the deployed program. See Appendix D - Compilation modes for the difference between the two modes.

Arrays

Fixed-size, compile-time-known arrays. Sizes cannot change at runtime.

• Array basics — declaration, indexing, modification
• Arrays and functions — value semantics, returning arrays

Array Basics

Declaration

Array type is [T; N], where T is the element type and N is a compile-time constant. Supported element types: all integers, bool, struct types, and arrays (for multidimensional arrays). Every element must be provided at initialization.

let numbers: [i32; 3] = [10, 20, 30];
let flags: [bool; 4] = [true, false, true, false];
let bytes: [u8; 2] = [255, 0];

Reading and Writing Elements

pub fn modify_array() -> i32 {
    let mut data: [i32; 3] = [1, 2, 3];
    let first: i32 = data[0];     // read
    data[0] = 99;                  // write (requires mut)
    data[2] = data[0] + data[1];
    return data[2];                // returns 101
}

The index can be any integer expression, not just a literal.

Warning

Inference does not perform array bounds checking at compile time or runtime. Accessing an element beyond the array’s size results in undefined behavior.

Arrays and Functions

Value Semantics

Arrays are passed by copy. The function receives its own copy — the caller’s array is not affected:

fn modify_copy(mut arr: [i32; 3]) -> i32 {
    arr[0] = 99;
    return arr[0];
}

pub fn original_unchanged() -> i32 {
    let data: [i32; 3] = [1, 2, 3];
    let ignored: i32 = modify_copy(data);
    return data[0];  // returns 1, not 99
}

Here, mut attributes the function parameter so that arr can be modified within the function. However, this does not affect the caller’s data array, which remains unchanged.

Returning Arrays

Functions can return fixed-size arrays:

pub fn make_sequence() -> [i32; 3] {
    return [10, 20, 30];
}

pub fn use_sequence() -> i32 {
    let arr: [i32; 3] = make_sequence();
    return arr[1];
}

Array return values must be assigned to a variable first — make_sequence()[0] is not supported.

Enums

An enum defines a type with a fixed set of named variants.

Defining an Enum

enum Direction {
    North,
    South,
    East,
    West
}

pub enum exports the type from the module. Variants are comma-separated. Each enum is a distinct type.

Using Enum Values

Variants are accessed with :::

pub fn go_west() -> Direction {
    let d: Direction = Direction::West;
    return d;
}

Comparing Enums

Enums support == and !=. Ordering operators (<, >, <=, >=) are not supported.

enum Status { Active, Inactive }

pub fn is_active(s: Status) -> bool {
    return s == Status::Active;
}

pub fn are_not_equal(a: Status, b: Status) -> bool {
    return a != b;
}

Enums and Functions

Enums work as function parameters and return types like any other type:

enum Dir { Up, Down, Left, Right }

pub fn dir_to_int(d: Dir) -> i32 {
    if d == Dir::Up {
        return 10;
    }
    if d == Dir::Down {
        return 20;
    }
    if d == Dir::Left {
        return 30;
    }
    return 40;
}

Reassignment

Enum variables declared with let mut can be reassigned:

enum Color { Red, Green, Blue }

pub fn reassign() -> Color {
    let mut c: Color = Color::Red;
    c = Color::Blue;
    return c;
}

Enums in Arrays

enum Color { Red, Green, Blue }

pub fn second_color() -> i32 {
    let colors: [Color; 3] = [Color::Red, Color::Green, Color::Blue];
    if colors[1] == Color::Green {
        return 1;
    }
    return 0;
}

Enums in Structs

Enum types can be used as struct fields:

enum Status { Active, Inactive }

struct Item {
    status: Status;
    value: i32;
}

pub fn get_status() -> i32 {
    let item: Item = Item { status: Status::Inactive, value: 42 };
    if item.status == Status::Inactive {
        return 1;
    }
    return 0;
}

Note

Enums do not support data-carrying variants, explicit discriminant values, methods, or pattern matching. They are simple named constants grouped under a type for better code organization and readability.

Non-Determinism

Inference’s non-deterministic constructs — @, forall, exists, assume, unique — exist for writing specifications, not for writing executable code. They appear only inside a spec block: as the body of a spec function, or nested within another non-deterministic block in such a body.

Outside a spec, the analysis phase rejects these constructs:

error[A006]: uzumaki (@) is only valid inside a non-deterministic block

A non-deterministic value (@) is a value attribute that represents every value its type can hold — the entire domain in one expression, not a single arbitrary pick. The enclosing non-deterministic block decides how the verifier reads that domain:

• forall — every execution path completes without trapping.
• exists — at least one execution path completes without trapping.
• unique — exactly one execution path completes without trapping.
• assume — filters out execution paths that do not satisfy a condition; only the surviving paths continue.

In compile mode spec blocks are stripped from the WebAssembly output entirely, so non-deterministic constructs have no effect on the deployed program. In proof mode (with -v) they are preserved and translated to Rocq alongside the rest of the module — see Appendix D - Compilation modes.

This chapter has three sections:

• Non-Deterministic Values — the @ operator.
• Non-Deterministic Blocks — forall, exists, assume, unique as the body of a spec function and as nested filters.
• Specifications — spec blocks that group properties about a module.

Non-Deterministic Values

The expression @ (read uzumaki) is a value attribute that represents every value the surrounding type can hold — not a single arbitrary pick, but the entire domain in one expression. Binding let x: i32 = @; makes x carry all 2^32 integers of type i32 at once; the enclosing non-deterministic block then decides how the verifier reads that — by quantifying over the whole domain (forall, exists, unique) or by narrowing it (assume).

@ is only valid inside a non-deterministic block (forall, exists, unique, or assume) that lives inside a spec. Using @ anywhere else — directly in a pub fn, in an ordinary helper function, in a top-level expression — is rejected at the analysis phase:

error[A006]: uzumaki (@) is only valid inside a non-deterministic block

A minimal use

Below, square is the executable function we want to reason about. SquareProps is a spec block whose single property claims that for every i32 value of x, square(x) is at least zero. let x: i32 = @; binds x to the whole i32 domain; the surrounding forall requires the final assert to hold for every one of those values — except those the inner assume filters out.

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

spec SquareProps {
    fn square_is_non_negative() forall {
        let x: i32 = @;
        assume {
            assert(x > -46340);
            assert(x < 46340);
        }
        assert(square(x) >= 0);
    }
}

(module $uzumaki_intro
  (type (;0;) (func (param i32) (result i32)))
  (type (;1;) (func))
  (func $square (;0;) (type 0) (param $x i32) (result i32)
    local.get $x
    local.get $x
    i32.mul
    return
    unreachable
  )
  (func $square_is_non_negative (;1;) (type 1)
    (local $x i32)
    i32.uzumaki
    local.set $x
    (assume
      local.get $x
      i32.const -46340
      i32.gt_s
      i32.eqz
      if
        unreachable
      end
      local.get $x
      i32.const 46340
      i32.lt_s
      i32.eqz
      if
        unreachable
      end
    )
    local.get $x
    call $square
    i32.const 0
    i32.ge_s
    i32.eqz
    if
      unreachable
    end
  )
)

Definition square : module_func := {|
  modfunc_type := 0%N;
  modfunc_locals := nil;
  modfunc_body :=
    BI_local_get 0%N (*x*) ::
    BI_local_get 0%N (*x*) ::
    BI_binop T_i32 (Binop_i BOI_mul) ::
    BI_return ::
    BI_unreachable ::
    nil;
|}.

Definition square_is_non_negative : module_func := {|
  modfunc_type := 1%N;
  modfunc_locals := T_num T_i32 :: nil;
  modfunc_body :=
    BI_uzumaki_num T_i32 ::
    BI_local_set 0%N (*x*) ::
    BI_assume (BT_valtype None) (
      BI_local_get 0%N ::
      BI_const_num (Vi32 -46340) ::
      BI_relop T_i32 (Relop_i (ROI_gt SX_S)) ::
      BI_testop T_i32 TO_eqz ::
      BI_if (BT_valtype None) (
        BI_unreachable ::
        nil) (
        nil) ::
      BI_local_get 0%N ::
      BI_const_num (Vi32 46340) ::
      BI_relop T_i32 (Relop_i (ROI_lt SX_S)) ::
      BI_testop T_i32 TO_eqz ::
      BI_if (BT_valtype None) (
        BI_unreachable ::
        nil) (
        nil) ::
      nil) ::
    BI_local_get 0%N (*x*) ::
    BI_call 0 ::
    BI_const_num (Vi32 0) ::
    BI_relop T_i32 (Relop_i (ROI_ge SX_S)) ::
    BI_testop T_i32 TO_eqz ::
    BI_if (BT_valtype None) (
      BI_unreachable ::
      nil) (
      nil) ::
    nil;
|}.

Definition uzumaki_intro__SquareProps_specs : list N := [1]%N.

Theorem valid_uzumaki_intro__SquareProps : ValidSpec uzumaki_intro uzumaki_intro__SquareProps_specs.
Proof.
  (* TODO: fill the proof *)
Qed.

The assume block narrows the universe of x values: only paths where x stays within a range that does not overflow x * x continue to the final assert. Without that filter, the forall would have to consider paths where square(x) wraps to a negative value, and the property would not hold.

Note

The type of @ is inferred from its context. In let x: i32 = @; it is i32. In let y: u64 = @; it is u64. The compiler emits a different non-det opcode per type — i32.uzumaki is 0xfc 0x31, i64.uzumaki is 0xfc 0x32.

Non-Deterministic Blocks

There are four block forms. Each appears either as the body of a spec function — written fn <name>() <quantifier> { ... } — or, in the case of assume, as a nested filter inside another quantifier’s body.

Inside the body of any of these blocks you can use let bindings, calls to ordinary fns, assert statements, and @ values. Quantifier blocks may also nest — most commonly, assume appears inside the body of a forall, exists, or unique spec function.

forall

Every execution path through the body must complete without trapping. For each @ value in scope, the verifier considers every value of that type; the property holds iff no assert in the body fails on any of those paths.

spec Props {
    fn add_zero_is_identity() forall {
        let x: i32 = @;
        assert(x + 0 == x);
    }
}

(module $blocks_forall
  (type (;0;) (func))
  (func $add_zero_is_identity (;0;) (type 0)
    (local $x i32)
    i32.uzumaki
    local.set $x
    local.get $x
    i32.const 0
    i32.add
    local.get $x
    i32.eq
    i32.eqz
    if
      unreachable
    end
  )
)

Definition add_zero_is_identity : module_func := {|
  modfunc_type := 0%N;
  modfunc_locals := T_num T_i32 :: nil;
  modfunc_body :=
    BI_uzumaki_num T_i32 ::
    BI_local_set 0%N (*x*) ::
    BI_local_get 0%N (*x*) ::
    BI_const_num (Vi32 0) ::
    BI_binop T_i32 (Binop_i BOI_add) ::
    BI_local_get 0%N (*x*) ::
    BI_relop T_i32 (Relop_i ROI_eq) ::
    BI_testop T_i32 TO_eqz ::
    BI_if (BT_valtype None) (
      BI_unreachable ::
      nil) (
      nil) ::
    nil;
|}.

exists

At least one execution path through the body must complete without trapping. Equivalently: there is at least one assignment to the @ values for which no assert in the body fails.

spec Props {
    fn equation_has_a_root() exists {
        let x: i32 = @;
        assert(x * x == 16);
    }
}

(module $blocks_exists
  (type (;0;) (func))
  (func $equation_has_a_root (;0;) (type 0)
    (local $x i32)
    i32.uzumaki
    local.set $x
    local.get $x
    local.get $x
    i32.mul
    i32.const 16
    i32.eq
    i32.eqz
    if
      unreachable
    end
  )
)

Definition equation_has_a_root : module_func := {|
  modfunc_type := 0%N;
  modfunc_locals := T_num T_i32 :: nil;
  modfunc_body :=
    BI_uzumaki_num T_i32 ::
    BI_local_set 0%N (*x*) ::
    BI_local_get 0%N (*x*) ::
    BI_local_get 0%N (*x*) ::
    BI_binop T_i32 (Binop_i BOI_mul) ::
    BI_const_num (Vi32 16) ::
    BI_relop T_i32 (Relop_i ROI_eq) ::
    BI_testop T_i32 TO_eqz ::
    BI_if (BT_valtype None) (
      BI_unreachable ::
      nil) (
      nil) ::
    nil;
|}.

The verifier discharges this claim by finding any value of x for which the body does not trap — for example 4 or -4.

unique

Exactly one execution path through the body completes without trapping. There is one and only one assignment to the @ values for which no assert fails.

spec Props {
    fn only_one_zero() unique {
        let x: i32 = @;
        assert(x == 0);
    }
}

(module $blocks_unique
  (type (;0;) (func))
  (func $only_one_zero (;0;) (type 0)
    (local $x i32)
    i32.uzumaki
    local.set $x
    local.get $x
    i32.const 0
    i32.eq
    i32.eqz
    if
      unreachable
    end
  )
)

Definition only_one_zero : module_func := {|
  modfunc_type := 0%N;
  modfunc_locals := T_num T_i32 :: nil;
  modfunc_body :=
    BI_uzumaki_num T_i32 ::
    BI_local_set 0%N (*x*) ::
    BI_local_get 0%N (*x*) ::
    BI_const_num (Vi32 0) ::
    BI_relop T_i32 (Relop_i ROI_eq) ::
    BI_testop T_i32 TO_eqz ::
    BI_if (BT_valtype None) (
      BI_unreachable ::
      nil) (
      nil) ::
    nil;
|}.

assume

assume is a filter. It appears as a nested block inside the body of another quantifier — typically forall — and drops every execution path on which the assume body would trap. Only the surviving paths continue into the code that follows.

The example below proves that for every i32 value of x in (-1000, 1000), abs(x) is non-negative. Without the assume, the forall would have to consider values where 0 - x overflows, and the property would not hold.

fn abs(x: i32) -> i32 {
    if x >= 0 {
        return x;
    }
    return 0 - x;
}

spec Props {
    fn abs_is_non_negative_for_small() forall {
        let x: i32 = @;
        assume {
            assert(x > -1000);
            assert(x < 1000);
        }
        assert(abs(x) >= 0);
    }
}

(module $blocks_assume
  (type (;0;) (func (param i32) (result i32)))
  (type (;1;) (func))
  (func $abs (;0;) (type 0) (param $x i32) (result i32)
    local.get $x
    i32.const 0
    i32.ge_s
    if
      local.get $x
      return
    end
    i32.const 0
    local.get $x
    i32.sub
    return
    unreachable
  )
  (func $abs_is_non_negative_for_small (;1;) (type 1)
    (local $x i32)
    i32.uzumaki
    local.set $x
    (assume
      local.get $x
      i32.const -1000
      i32.gt_s
      i32.eqz
      if
        unreachable
      end
      local.get $x
      i32.const 1000
      i32.lt_s
      i32.eqz
      if
        unreachable
      end
    )
    local.get $x
    call $abs
    i32.const 0
    i32.ge_s
    i32.eqz
    if
      unreachable
    end
  )
)

Definition abs : module_func := {|
  modfunc_type := 0%N;
  modfunc_locals := nil;
  modfunc_body :=
    BI_local_get 0%N (*x*) ::
    BI_const_num (Vi32 0) ::
    BI_relop T_i32 (Relop_i (ROI_ge SX_S)) ::
    BI_if (BT_valtype None) (
      BI_local_get 0%N ::
      BI_return ::
      nil) (
      nil) ::
    BI_const_num (Vi32 0) ::
    BI_local_get 0%N (*x*) ::
    BI_binop T_i32 (Binop_i BOI_sub) ::
    BI_return ::
    BI_unreachable ::
    nil;
|}.

Definition abs_is_non_negative_for_small : module_func := {|
  modfunc_type := 1%N;
  modfunc_locals := T_num T_i32 :: nil;
  modfunc_body :=
    BI_uzumaki_num T_i32 ::
    BI_local_set 0%N (*x*) ::
    BI_assume (BT_valtype None) (
      BI_local_get 0%N ::
      BI_const_num (Vi32 -1000) ::
      BI_relop T_i32 (Relop_i (ROI_gt SX_S)) ::
      BI_testop T_i32 TO_eqz ::
      BI_if (BT_valtype None) (
        BI_unreachable ::
        nil) (
        nil) ::
      BI_local_get 0%N ::
      BI_const_num (Vi32 1000) ::
      BI_relop T_i32 (Relop_i (ROI_lt SX_S)) ::
      BI_testop T_i32 TO_eqz ::
      BI_if (BT_valtype None) (
        BI_unreachable ::
        nil) (
        nil) ::
      nil) ::
    BI_local_get 0%N (*x*) ::
    BI_call 0 ::
    BI_const_num (Vi32 0) ::
    BI_relop T_i32 (Relop_i (ROI_ge SX_S)) ::
    BI_testop T_i32 TO_eqz ::
    BI_if (BT_valtype None) (
      BI_unreachable ::
      nil) (
      nil) ::
    nil;
|}.

Specifications

A spec block groups properties that describe a module. Each fn inside a spec block is a verification obligation rather than a function the host can call — spec functions are never exported, and in compile mode the whole block is stripped during codegen.

spec <Name> {
    fn <property_name>() <non-deterministic-block> {
        // body
    }
}

A spec for a tiny module

Below is an executable function double and a DoubleProps specification that claims doubling a positive number produces a result larger than the original. The body of the spec function uses the same non-deterministic constructs introduced in the previous sections.

fn double(x: i32) -> i32 {
    return x + x;
}

spec DoubleProps {
    fn doubling_increases_positives() forall {
        let x: i32 = @;
        assume {
            assert(x > 0);
        }
        assert(double(x) > x);
    }
}

(module $spec_for_module
  (type (;0;) (func (param i32) (result i32)))
  (type (;1;) (func))
  (func $double (;0;) (type 0) (param $x i32) (result i32)
    local.get $x
    local.get $x
    i32.add
    return
    unreachable
  )
  (func $doubling_increases_positives (;1;) (type 1)
    (local $x i32)
    i32.uzumaki
    local.set $x
    (assume
      local.get $x
      i32.const 0
      i32.gt_s
      i32.eqz
      if
        unreachable
      end
    )
    local.get $x
    call $double
    local.get $x
    i32.gt_s
    i32.eqz
    if
      unreachable
    end
  )
)

Definition double : module_func := {|
  modfunc_type := 0%N;
  modfunc_locals := nil;
  modfunc_body :=
    BI_local_get 0%N (*x*) ::
    BI_local_get 0%N (*x*) ::
    BI_binop T_i32 (Binop_i BOI_add) ::
    BI_return ::
    BI_unreachable ::
    nil;
|}.

Definition doubling_increases_positives : module_func := {|
  modfunc_type := 1%N;
  modfunc_locals := T_num T_i32 :: nil;
  modfunc_body :=
    BI_uzumaki_num T_i32 ::
    BI_local_set 0%N (*x*) ::
    BI_assume (BT_valtype None) (
      BI_local_get 0%N ::
      BI_const_num (Vi32 0) ::
      BI_relop T_i32 (Relop_i (ROI_gt SX_S)) ::
      BI_testop T_i32 TO_eqz ::
      BI_if (BT_valtype None) (
        BI_unreachable ::
        nil) (
        nil) ::
      nil) ::
    BI_local_get 0%N (*x*) ::
    BI_call 0 ::
    BI_local_get 0%N (*x*) ::
    BI_relop T_i32 (Relop_i (ROI_gt SX_S)) ::
    BI_testop T_i32 TO_eqz ::
    BI_if (BT_valtype None) (
      BI_unreachable ::
      nil) (
      nil) ::
    nil;
|}.

Definition nd_spec__DoubleProps_specs : list N := [1]%N.

Theorem valid_nd_spec__DoubleProps : ValidSpec nd_spec nd_spec__DoubleProps_specs.
Proof.
  (* TODO: fill the proof *)
Qed.

The translator emits one Definition per function (executable or spec), then a list N naming the indices of the spec functions, then a Theorem valid_<module>__<SpecName> that ties the spec back to the module via the ValidSpec predicate. The proof body is left as (* TODO: fill the proof *) — the translator produces obligations, not closed proofs.

Compile-mode behaviour

Compile the same source without -v. The resulting .wasm binary contains only double; the entire spec DoubleProps { ... } block is stripped, so the deployed module is byte-for-byte the same as if the spec had not been written:

$ infc spec_block.inf            # only out/spec_block.wasm, spec stripped
$ infc spec_block.inf -v         # out/spec_block.wasm + out/spec_block.v, spec preserved

Note

Spec functions are never WASM-exported even when declared pub. They exist for the verifier only.

Appendix

The appendices provide supplementary information that supports the main content of this book.

Here are the appendices included in this book:

A - Language Reference

Keywords

Note

The grammar reserves type, external, use, and module for future use. These are recognised as keywords but the corresponding language features are not yet fully implemented and using them today will result in a compilation error.

Data Types

Operators

Arithmetic Operators

Note

Integer arithmetic wraps on overflow. For example, adding 1 to the maximum i32 value wraps around to the minimum i32 value.

Comparison Operators

Comparison operators evaluate to a bool value.

Note

Enum values support only == and !=. Ordering comparisons (<, <=, >, >=) require numeric types.

Logical Operators

Logical operators work on bool values and produce a bool result.

Bitwise Operators

Bitwise operators work on the binary representation of integer values.

Access Operators

B - Inference Programming Language Specification

If you want to understand the foundational principles and formal definitions of the Inference programming language — including its mathematical models, syntax, and semantics — we recommend referring to the official Language Specification.

C - Inference Compiler

infc is the official compiler for the Inference programming language. It takes .inf source files and produces WebAssembly modules directly, with no external toolchain needed.

infs is the unified CLI that wraps infc with project management, toolchain installation, and build/run commands. See Appendix D for the full infs reference.

Both tools are open source and available in the inference GitHub repository. Refer there for the latest releases, discussions, and feature or bug tracking.

D - infs CLI Reference

infs is the unified command-line interface for the Inference compiler toolchain. It wraps the infc compiler with project management, toolchain installation, and build/run commands.

Compilation Commands

Build Options

When no phase flag is given, infs build runs the full pipeline and writes out/<name>.wasm. The phase flags below stop the pipeline early — supplying one means only that phase (and any required predecessors) runs.

Run Options

Examples

# Full compilation (writes out/example.wasm)
$ infs build example.inf

# Compile with Rocq translation (writes out/example.wasm and out/example.v)
$ infs build example.inf -v

# Build and run
$ infs run example.inf

# Run a specific exported function
$ infs run example.inf --entry-point my_function

Using infc Directly

The underlying infc compiler accepts the same phase and output flags as infs build and can be invoked standalone — useful for embedding into custom build systems or CI without the toolchain wrapper:

$ infc example.inf
$ infc example.inf --parse
$ infc example.inf -v

When no flags are given, infc performs full compilation and writes the WASM binary — equivalent to --codegen -o.

Note

infc currently supports single-file compilation only. Multi-file projects and project file (.infp) support are planned for future releases.

Compilation modes

The compiler has two modes that change how spec blocks and non-deterministic constructs are handled:

• compile (default): produces a release-optimized WASM binary intended for execution. spec blocks are stripped during codegen, so non-deterministic constructs (@, forall, exists, assume, unique) that appear only inside spec blocks do not reach the output.
• proof (implied by -v): keeps spec functions unoptimized so the structure of the source survives into the Rocq translation. The compiler emits both out/<name>.wasm and out/<name>.v. The .v file is a Rocq (Coq) translation suitable for formal verification.

In other words: use the default mode when you want to run the program; pass -v when you want to prove things about it.

Project Management

Creating a New Project

$ infs new myproject

This creates the following project structure:

myproject/
├── Inference.toml
├── src/
│   └── main.inf
├── tests/
└── proofs/

The generated src/main.inf contains a minimal program:

// Entry point for the Inference program

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

Use --no-git to skip git initialization:

$ infs new myproject --no-git

Initializing an Existing Directory

$ infs init

Creates Inference.toml and src/main.inf in the current directory. If a .git directory exists, it also creates .gitignore and .gitkeep files.

Toolchain Management

Installing a Toolchain

# Install latest stable version
$ infs install

# Install a specific version
$ infs install 0.1.0

On first install, infs automatically configures your system PATH:

• Linux/macOS: Adds ~/.inference/bin to your shell profile (~/.bashrc, ~/.zshrc, or ~/.config/fish/config.fish)
• Windows: Updates the user PATH in the registry

After installation, restart your terminal or source your shell profile.

Checking Installation Health

$ infs doctor

This runs diagnostic checks and provides recommendations if anything needs attention.

Other Commands

Compiler Resolution

When running build or run, infs locates the infc compiler using the following priority:

Environment Variables