Introduction

Welcome to the Inference Compiler Book — a collection of design and implementation notes for the Inference compiler toolchain. Inference is a programming language for mission-critical software with first-class support for formal verification via translation to Rocq (Coq), and it targets WebAssembly as its primary runtime.

This book is not a language tutorial. It documents how the compiler works internally and why specific implementation decisions were made — the kind of context that is hard to recover from the source code alone. Each chapter takes a single subsystem or problem, explains the constraints, walks through the chosen approach, and compares it against how other compilers solve the same problem.

The compilation pipeline

The compiler is a multi-phase pipeline. Each .inf source file flows through:

.inf source → parse → type-check → analyze → codegen (WASM) → wasm-to-v (Rocq)

The chapters follow that order:

• The Inference Parser — the resilient recursive-descent parser that turns source text into the typed AST.
• Static Analysis in Inference — the rule-based pass that enforces the control-flow invariants formal verification depends on.
• Memory Allocation in WASM Codegen — linear-memory layout, stack frames, and array lowering.
• Arithmetic Overflow in WASM Codegen — WebAssembly's wrapping semantics and what they mean for proofs.
• Unreachable Emission in Codegen — why the compiler emits a trailing unreachable in non-void functions.
• Compilation Targets — compile vs. proof modes and the supported backends.

A second group of chapters covers how programs are organised and built beyond a single source file:

• Module Hierarchy & Multi-File Compilation — the file-as-module system, the use directive, and how a multi-file program flattens into one WASM module and one proof.
• Projects & the infs Toolchain — the Inference.toml manifest, project discovery, and the infs build/run workflow that drives the compiler.
• External Functions and WASM Linking — declaring external fns and binding them to pre-compiled .wasm modules.
• The WASM Linker — the static merge that folds external function bodies into a single self-contained module.

A third group covers the toolchain outside the batch compiler:

• The Language Server — the inference-lsp server and the layered ide/ crate stack: Salsa-memoized analyses, the router/worker/read-pool thread architecture, and how the editor gets real compiler answers on every keystroke.

The appendix preserves historical notes from the project's earlier LLVM-based backend, retained for reference.

Building this book

This book is built with mdBook. From the book/ directory:

mdbook build      # render static HTML into book/book/
mdbook serve      # serve locally with live reload at http://localhost:3000

Source for every chapter lives under book/src/.

The Inference Parser

This document explains how the Inference compiler turns .inf source text into a typed AST. It covers the resilient parser that lives in the core/parser crate (inference-parser), the rust-analyzer-derived architecture it is built on, and how it recovers from syntax errors without panicking.

Overview

Parsing is the first phase of the compilation pipeline. It is responsible for one job: read a string of Inference source and produce an AstArena — the arena-allocated, typed Abstract Syntax Tree that every later phase (type checking, static analysis, code generation, Rocq translation) consumes.

The parser is a single, self-contained component. Its design goals shape everything that follows:

• No C toolchain dependency. The parser is pure Rust, with no build script and no generated C scanner, which keeps cross-compilation (notably on Windows) simple.
• Resilient, structured errors. The parser never aborts and never panics — on any input it returns a tree plus a list of structured ParseError { span, message } values, so later phases and the IDE always have something to work with.
• Speed. The engine is fast (see Performance) and lowers straight into a compact arena-based AST.

The design follows two references closely:

• The rust-analyzer parser for the event-based engine (Markers, forward_parent, a flat event stream).
• matklad's Resilient LL Parsing Tutorial and Parsing Advances for error recovery and the loop-progress ("fuel" + advance-assertion) guarantee.

The parser implements the Inference language syntax directly; this crate is the syntactic source of truth for the compiler.

The pipeline

A single call to inference_parser::parse runs four internal stages:

  .inf source (&str)
        │
        ▼
  ┌───────────┐   Vec<Token>      ┌───────────┐   events        ┌──────────────┐
  │   lexer   │ ────────────────► │  parser   │ ──────────────► │  build_tree  │
  │ (lexer.rs)│  kind+span+joint  │(parser.rs)│  Start/Token/   │(syntax_tree) │
  └───────────┘  incl. trivia     │ + grammar │  Finish/Error   └──────┬───────┘
                                  └───────────┘                        │ owned CST
                                                                       ▼
                                                                 ┌───────────┐
                                                                 │   lower   │
                                                                 │ (lower.rs)│
                                                                 └─────┬─────┘
                                                                       ▼
                                                          AstArena + Vec<ParseError>
                                                                  (Parse)

The public surface is small (core/parser/src/lib.rs):

pub fn parse(src: &str) -> Parse;

pub struct Parse {
    pub arena: AstArena,
    pub errors: Vec<ParseError>,
}

// The CST seam, exposed mainly for testing grammar shape and recovery directly:
pub fn parse_to_cst(src: &str) -> (SyntaxNode, Vec<ParseError>);

The orchestration crate core/inference calls parse from inference::parse, mapping a non-empty errors list onto an anyhow::Error to fit the &str -> Result<AstArena> contract the rest of the compiler expects.

Crate layout

The dependency direction is inference → parser → ast. The parser depends on inference-ast only to allocate AST nodes; inference-ast knows nothing about the parser.

Stage 1: the lexer

The lexer (core/parser/src/lexer.rs) makes a single pass over the source bytes and emits a flat Vec<Token>:

pub struct Token {
    pub kind: SyntaxKind,
    pub loc: Location,   // byte offsets + 1-based line/column
    pub joint: bool,     // is this token byte-adjacent to the next?
}

Three properties matter:

• Trivia is preserved. Whitespace, // comments, and /// doc comments are emitted as Whitespace / Comment / DocComment tokens rather than discarded. This keeps the token stream lossless: concatenating every token's source slice reproduces the input byte-for-byte. (The parser later sees a trivia-free view; trivia is re-attached when the tree is built.)
• Joint bits drive token.immediate semantics. A token is joint when its end offset equals the next token's start offset (no whitespace between). The grammar needs this for constructs that must not have intervening whitespace: the path separator ::, the generic-argument terminator ' (as in Vec i32'), and the unit literal/type ().
• The lexer is total. It never panics and always terminates. Every byte is covered by exactly one token. Malformed input — an unterminated string, an unknown character — becomes an Error token rather than an exception, so even the lexer participates in error recovery.

A few Inference-specific lexical rules are worth calling out, because they affect parsing downstream:

• Prefix-position negative numbers. A leading - is part of a number literal when it is immediately followed by a digit and no expression has just ended, so -42 lexes as a single Number token, not Minus then Number. The lexer keeps a one-token lookbehind (prev_significant, ignoring trivia) and consults the EXPR_END token set for that second condition: after a, 1, ), ], @ and the other kinds an expression can end with, the - is subtraction, so v-1 lexes as three tokens. } is deliberately not in that set — it closes a block as well as a struct literal, and a statement may open with a negative literal, as in if c { } -1;. (- 42, with a space, lexes as two tokens and parses as a unary negation; analysis rule A046 then rejects that spelling, so the glued form is the only way to write a negative literal.)
• Reserved-but-not-keyword identifiers. constructor, proof, and uzumaki lex as ordinary identifiers, matching the grammar's reserved-identifier rule.

Stage 2: SyntaxKind and TokenSet

Like rust-analyzer, Inference uses a single SyntaxKind enum (core/parser/src/syntax_kind.rs) that holds both token kinds and node kinds:

#[repr(u16)]
pub enum SyntaxKind {
    // token kinds first: trivia, literals, keywords, punctuation, operators…
    Whitespace, Comment, DocComment, Number, String, Ident,
    FnKw, LetKw, /* … */ Plus, Minus, StarStar, ColonColon, At, Tick, /* … */
    Error, Eof,
    // …then node kinds:
    SourceFile, FunctionDefinition, BinaryExpression, /* … */ UnaryBitnot,
}

The boundary between the two groups is the module-level constant FIRST_NODE (the discriminant of the SourceFile variant). A compile-time assertion keeps all token kinds below 128:

pub(crate) const FIRST_NODE: u16 = SyntaxKind::SourceFile as u16;

const _: () = assert!(FIRST_NODE <= 128, "token kinds must fit a u128 TokenSet");

That bound exists because TokenSet (core/parser/src/token_set.rs) is a u128 bitset over token discriminants. Recovery sets and multi-token at(…) checks are then constant-time bit operations:

const STMT_START: TokenSet = TokenSet::new(&[LetKw, ReturnKw, IfKw, LoopKw, /* … */]);

Using one enum for tokens and nodes means the lexer, the parser, the CST, and the lowering all speak the same vocabulary — no conversions at the boundaries, and the CST is homogeneous (Node(kind) / Token(kind)).

Stage 3: the event-based parser

The parser (core/parser/src/parser.rs) does not build a tree directly. Following rust-analyzer, it consumes a trivia-free Input and emits a flat list of events:

pub enum Event {
    Start { kind: SyntaxKind, forward_parent: Option<u32> },
    Token { kind: SyntaxKind },
    Finish,
    Error { msg: String },
}

Grammar rules bracket their work with markers instead of nesting function results. A rule opens a marker, consumes tokens and sub-rules, then completes the marker with the node kind it turned out to be:

fn function_definition(p: &mut Parser) {
    let m = p.start();          // open a marker (a tombstone Start event)
    p.eat(SyntaxKind::PubKw);   // optional visibility
    p.bump(SyntaxKind::FnKw);
    name(p);
    argument_list(p);
    // …
    m.complete(p, SyntaxKind::FunctionDefinition); // fill in the node kind
}

This indirection buys the parser its most important trick: precede / forward_parent, which retroactively wraps an already-parsed node in a new parent. That is how left-associative and postfix forms are built — e.g. after parsing a, seeing .b reparents a under a MemberAccessExpression:

let lhs = atom(p);                  // CompletedMarker for `a`
let m = lhs.precede(p);             // open a parent *before* `a`
p.bump(SyntaxKind::Dot);
name(p);
m.complete(p, SyntaxKind::MemberAccessExpression);

Expressions: Pratt parsing

Binary and unary expressions are parsed by precedence climbing (core/parser/src/grammar/expr.rs). Each binary operator has a single binding power plus a right_assoc flag — the numbers live in a small bp module next to the Pratt loop and are the crate's definition of Inference's precedence (higher binds tighter):

The Pratt loop folds in any operator that binds tighter than the caller's floor. Right-associativity is handled with two small adjustments: a right-associative operator at exactly the floor still recurses (so a ** b ** c nests to the right), and it recurses with op_bp - 1 as the new floor:

while let Some((op_bp, right_assoc)) = binary_bp(p.current()) {
    if op_bp <= min_bp && !(right_assoc && op_bp == min_bp) {
        break;
    }
    let m = lhs.precede(p);          // reparent the LHS under a BinaryExpression
    p.bump_any();                    // the operator token
    let next_min = if right_assoc { op_bp - 1 } else { op_bp };
    expr_bp(p, next_min, allow_struct);
    lhs = m.complete(p, SyntaxKind::BinaryExpression);
}

Prefix operators (!, -, ~) bind tighter than any binary operator, and the postfix forms — call f(…), index a[…], member .x, type-member ::x — bind tightest of all. Assignment is deliberately not an expression operator: = is handled at statement level (assign_statement), matching the grammar.

Disambiguations the parser handles explicitly

An LL parser has to resolve a few grammar ambiguities by hand. The notable ones:

• -42 vs - x vs v-1 — resolved in the lexer by the one-token lookbehind (prefix-position negative numbers, above).
• :: and ' immediacy — only treated as a path separator / generic terminator when the joint bit says there is no intervening whitespace.
• Struct literal { vs block { — S { a: 1 } is a struct literal, but in an if/loop condition a { opens the body. The expression parser threads a no_struct flag through condition parsing to forbid struct literals there.
• Contextual keywords — self, type, from, and spec are keywords only in the rules that introduce them; everywhere an identifier is expected they are ordinary identifiers (so self.type = … and spec::Auction::new() parse). The parser accepts these tokens where an identifier is wanted and remaps them to Ident.

Stage 4: the owned CST

process() (core/parser/src/event.rs) resolves the forward_parent chains and flattens the events into a linear Vec<Step> of Enter(kind) / Token / Leave / Error. build_tree (core/parser/src/syntax_tree.rs) then walks the steps together with the full token list (trivia included) to produce an owned, immutable concrete syntax tree:

pub enum SyntaxElement {
    Node(SyntaxNode),
    Token(Token),
}

pub struct SyntaxNode {
    pub kind: SyntaxKind,
    pub loc: Location,
    pub children: Vec<SyntaxElement>,
}

Trivia tokens are re-attached as Token children at the position they occur, so the tree is lossless. Each node's loc spans its first-to-last non-trivia descendant token. The CST is private to the crate — it is an intermediate, not a public artifact. (Exposing a persistent red/green tree for IDE use is possible future work but out of scope.)

SyntaxNode provides kind-based navigation helpers (child(kind), children_of(kind), nth_node(n), child_token(kind), text(src)) that the lowering uses to find the children it needs.

Stage 5: lowering to the AstArena

lower.rs walks the CST and allocates typed AST nodes into the AstArena. This is the largest module in the crate (~3,000 lines).

AstArena indices are sequential la_arena slots, so the order in which nodes are allocated is part of the AST's identity — every later phase indexes into the arena by slot. The lowering therefore allocates in a fixed, deterministic order, and a few allocation-order rules are worth calling out:

• function parameters allocate type before name;
• a bare return; still allocates a UnitLiteral expression;
• named call/struct arguments allocate the name as an expression before the value;
• the SourceFileData node is allocated last, after all of its definitions.

The methods (lower_source_file, lower_definition, lower_statement, lower_expression, lower_type, …) follow the structure of the grammar one rule at a time, which keeps the allocation order easy to read off and to test (see Testing).

Error recovery and the never-panic guarantee

The parser's central contract is that parse never panics on any input and always returns a Parse. Resilience is built in at three levels.

Resilient LL recovery. When the parser hits a token it cannot use, it does not unwind — it emits an Error event and, where appropriate, consumes the offending token into an Error node so that progress is guaranteed. Two strategies are used depending on context:

• Top-level item parsing, which has no closing delimiter, uses err_recover(RECOVERY_SET) to resynchronize on the start of the next item.
• Delimited bodies (a { … } block, a spec body, a struct body) use err_and_bump, which always consumes a token. Using a recovery set inside a delimited body can spin if the stuck token is itself in the set, so the always-consume rule is the safe choice there.

The fuel + advance guard. A resilient LL parser can, if a rule is written incorrectly, loop forever by retrying a recovery path that consumes nothing. The parser borrows matklad's safeguard: a fuel counter (const FUEL: u32 = 256, a Cell<u32>) is decremented on every lookahead and refilled whenever real progress is made — a token is bumped or a node is completed. An assertion fires (in debug and release) the moment fuel hits zero, turning a would-be infinite loop into an immediate, localized crash during development rather than a hang in production. On well-formed grammar rules the guard never trips; it is a backstop, not part of normal control flow.

Lowering is total. Because the grammar can produce a node whose expected child was lost to recovery (e.g. a. with no name after the dot), the lowering never unwraps a child that recovery might have dropped. Every such site falls back to a synthesized <error> placeholder node and records a ParseError. The adversarial test corpus — truncated items, dangling operators, random bytes, and deeply nested unterminated input like "fn f(){".repeat(200) — is run through the full public parse under catch_unwind to prove zero panics.

Errors surface as structured values (core/parser/src/errors.rs):

pub struct ParseError {
    pub span: Location,
    pub message: String,
}

Each error is given a source span by tracking the token cursor through the step stream, so a message such as expected ; points at the right place. The richer diagnostics this enables (labels, notes, IDE squiggles) are intentionally left for later work; for now inference::parse aggregates the messages into one error to keep its existing contract.

Testing and verification

The parser is covered at two levels: in-crate unit tests for every stage, and the compiler's end-to-end suites that exercise it as the real front end.

In-crate, core/parser carries ~260 unit tests spanning:

• the lexer (every token class, joint bits, round-trip losslessness, edge cases like -42 and unterminated strings);
• the engine (markers, forward_parent/precede, the advance guard);
• the grammar (CST shape per construct, precedence and associativity);
• the lowering (arena structure per construct, plus the error-recovery fallbacks);
• resilience (the full adversarial corpus through parse, asserting no panic).

End to end, the AST tests in tests/src/ast and the four-tier WASM codegen golden suite run on the arenas this parser produces, so any change in parsing that would alter the AST — and therefore the generated WebAssembly — is caught by a golden diff. To support exact arena comparisons in tests, AstArena derives PartialEq/Eq.

Performance

The parser is substantially faster than the tree-sitter front end it replaced. Measured on the same inputs (release build, full source → AstArena path):

The speedup is intrinsic to the engine — it holds even when only the parse stage (no AST lowering) is measured, and tree-sitter's per-call parser-construction cost turned out to be negligible. Removing the tree-sitter C dependency is a separate, additional win for build times and cross-platform robustness.

The one trade-off is allocation: the owned CST is built from many small per-node Vecs, so the new parser performs more allocations than tree-sitter's single internal arena. This is transient (well under 20 MB for an 80 KB file) and is the natural target for future optimization (arena-allocating CST children, or lowering directly from the event stream).

Summary

The Inference parser is a recursive-descent parser modeled on rust-analyzer's event engine and matklad's resilient-LL techniques. It lexes trivia-aware tokens, parses them into a flat event stream via markers, builds a lossless owned CST, and lowers that CST into the AstArena that the rest of the compiler consumes. It is fast, depends on no C toolchain, never panics on malformed input, and is covered by in-crate unit tests together with the compiler's end-to-end AST and golden-codegen suites.

References

• rust-analyzer parser crate
• matklad, Resilient LL Parsing Tutorial
• matklad, Simple but Powerful Pratt Parsing
• matklad, Parsing Advances

Static Analysis in Inference

The Inference compiler performs a static analysis pass between type checking and code generation. This document explains why that pass exists, what invariants it enforces, how it is structured internally, and what the formal verification implications are for each rule.

Why Analysis Exists

The Inference compilation pipeline is:

parse -> type_check -> analyze -> codegen -> wasm_to_v

Type checking verifies that every expression has a consistent type: that a function receives arguments of the declared types, that struct fields are accessed correctly, that return types match. It answers the question "is this program well-typed?"

Analysis answers a different question: "does this program have the control flow structure that makes formal verification tractable?" These are separable concerns. A program can be perfectly well-typed and still contain control flow patterns that make it impossible — or extremely difficult — to reason about in a proof assistant.

The analysis crate (core/analysis) enforces those structural invariants. It receives the TypedContext produced by the type checker, runs a set of independent rules over every function body, and either returns an AnalysisResult containing advisory findings or an AnalysisErrors value that blocks compilation.

Why Formal Verification Demands Stricter Control Flow

Inference targets Rocq (Coq) as its verification backend. Rocq is a proof assistant based on the calculus of constructions: proofs are total, all functions must terminate, and reasoning about a program requires that the program's execution paths be fully enumerable.

Inference's non-deterministic blocks (forall, exists, unique) make this requirement explicit at the language level. A forall block asserts that a property holds on all computation paths through the block. An exists block asserts that at least one path satisfies the property. These semantics are sound only when all paths are actually explored. A break or return inside such a block would short-circuit path exploration, silently invalidating the assertion without a type error. That is the class of mistake that analysis is designed to catch.

Fundamental Principles

Rule Independence

Each analysis check is a distinct zero-sized struct implementing the Rule trait. Rules do not communicate with each other. They do not share mutable state. Each rule receives the same &TypedContext and produces its own Vec<LabeledDiagnostic> independently — each finding paired with the module path of the file it belongs to, so a multi-file report can name the file an imported finding came from.

This design has several consequences. Rules can be added or removed without touching each other. Rules could be executed in parallel on separate threads — the Send + Sync bounds on Rule are specified now, not added later. Test cases for one rule cannot silently affect another. And because a rule is a pure query over the TypedContext, the same all_rules() set runs unchanged inside the language server, where each finding becomes an editor diagnostic tagged with its rule id.

Severity Model

Every rule declares exactly one severity level: Error, Warning, or Info. The severity is not a runtime value — it is encoded in the rule's severity() method, which the rule! macro generates from a literal identifier at the call site.

The analyze() function in core/analysis/src/lib.rs routes each finding into one of three buckets based on its rule's severity:

Errors   -> Err(AnalysisErrors) when any are present
Warnings -> Ok(AnalysisResult)  always
Infos    -> Ok(AnalysisResult)  always

The bifurcation is intentional. Errors block the pipeline: codegen and wasm_to_v will not run if analyze() returns Err. Warnings and infos are advisory — the pipeline continues, and the orchestration layer decides whether to display them to the user.

This means a rule author makes a deliberate choice when assigning a severity. An error-severity rule is making a strong claim: no valid Inference program should ever trigger this finding, and any program that does must be corrected before it can be compiled.

Exhaustive Collection

All rules run to completion before any findings are reported. The loop in analyze() iterates every registered rule and extends the appropriate bucket:

#![allow(unused)]
fn main() {
for &r in rules::all_rules() {
    let findings = r.check(typed_context);
    match r.severity() {
        Severity::Error   => errors.extend(findings),
        Severity::Warning => warnings.extend(findings),
        Severity::Info    => infos.extend(findings),
    }
}
}

There is no early exit on the first error. A developer fixing a compilation failure sees every problem in a single compile cycle, not one at a time. This is the same design Rust's type checker uses: collect all errors, report all errors.

Diagnostic Format

Diagnostics follow the GCC/Clang/rustc convention:

<line>:<column>: <severity>[<rule_id>]: <message>

A concrete example:

3:5: error[A001]: break statement is only valid inside a loop body; if you intended to exit the function, use 'return'

The message body follows a what; why; how structure. The what states the violation directly. The why explains the constraint in terms the developer can reason about. The how gives actionable guidance. All three are present in every diagnostic message.

When multiple diagnostics are present, they are sorted by source location (line, then column) before display, regardless of severity. A developer reading output from top to bottom encounters issues in the order they appear in the source file.

Data Flow

TypedContext (read-only)
      |
      v
  analyze()
      |
      +-- for each Rule in all_rules():
      |       rule.check(ctx)
      |           |
      |           v
      |       walk_function_bodies(ctx, visitor)
      |           |
      |           +-- for each source file:
      |           |       for_each_function_body(defs)
      |           |           |
      |           |           v
      |           |       walk_block / walk_statement
      |           |           |
      |           |           v
      |           |       visitor(stmt_id, &WalkContext)
      |           |           { loop_depth, nondet_depth,
      |           |             nondet_block_kind, module_path }
      |           |
      |           v
      |       Vec<LabeledDiagnostic>
      |
      v
  partition by severity
      |
      +-- errors non-empty -> Err(AnalysisErrors { errors, warnings, infos })
      +-- errors empty     -> Ok(AnalysisResult  { warnings, infos })

The analysis crate receives &TypedContext — a shared, read-only reference. It does not modify the AST, does not modify type annotations, and does not produce any output other than diagnostics. It is a pure query over an immutable data structure.

The rule! Macro

Defining a rule requires a struct and a Rule trait implementation covering four methods: id(), name(), severity(), and check(). Without the macro, even a trivial rule requires roughly 25 lines of boilerplate. With the macro, the same rule is expressed in about 10 lines, and the connection between the struct declaration and the trait implementation is visually immediate.

Syntax

#![allow(unused)]
fn main() {
crate::rule! {
    /// Break statement must appear inside a loop body.
    #[id = "A001"]
    #[name = "Break outside loop"]
    #[severity = error]
    pub struct BreakOutsideLoop;
    fn check(ctx: &TypedContext) -> Vec<LabeledDiagnostic> {
        // implementation
    }
}
}

Each pseudo-attribute has a specific role:

• #[id = "A001"] — the string that appears in diagnostic output as [A001] and in rule_id(). Conventionally A followed by a three-digit decimal number.
• #[name = "Break outside loop"] — a human-readable name for tooling and documentation.
• #[severity = error] — one of the three literal identifiers error, warning, or info. Any other identifier is a compile error via __severity!.

What the Macro Expands To

The macro produces a public struct with the given name and a full Rule trait implementation:

#![allow(unused)]
fn main() {
/// Break statement must appear inside a loop body.
pub struct BreakOutsideLoop;

impl crate::rule::Rule for BreakOutsideLoop {
    fn id(&self) -> &'static str { "A001" }
    fn name(&self) -> &'static str { "Break outside loop" }
    fn severity(&self) -> crate::errors::Severity {
        crate::__severity!(error)   // expands to Severity::Error
    }
    fn check(&self, ctx: &crate::rule::TypedContext) -> Vec<crate::errors::LabeledDiagnostic> {
        // the body you wrote
    }
}
}

The struct is zero-sized. Rule objects are stored as &'static dyn Rule in the all_rules() slice, meaning no heap allocation occurs for rule instances.

The __severity! Helper

The __severity! macro validates the severity identifier at compile time:

#![allow(unused)]
fn main() {
macro_rules! __severity {
    (error)   => { $crate::errors::Severity::Error   };
    (warning) => { $crate::errors::Severity::Warning };
    (info)    => { $crate::errors::Severity::Info    };
    ($other:ident) => {
        compile_error!(concat!(
            "invalid severity: `", stringify!($other),
            "`, expected `error`, `warning`, or `info`"
        ))
    };
}
}

The catch-all arm produces a compile_error! for any unrecognized identifier. This is a design choice: rather than silently defaulting to a severity or requiring a runtime parse, the compiler rejects malformed rule definitions at build time. There is no way to add a rule with an invalid severity and have it compile.

Why a Macro Rather than a Derive

A derive macro operates on struct and enum items only. The rule! macro needs to capture a function body (fn check(...) { ... }) as part of the same syntactic unit as the struct declaration. That is not possible with derive — derive can only inspect the struct's fields and attributes, not an accompanying function definition. A declarative macro_rules! macro can match any syntactic pattern, including the function body, making the check implementation co-located with the struct declaration in a single syntactic block.

Complete Example: A001

The full source of the simplest rule in the codebase:

#![allow(unused)]
fn main() {
crate::rule! {
    /// Break statement must appear inside a loop body.
    #[id = "A001"]
    #[name = "Break outside loop"]
    #[severity = error]
    pub struct BreakOutsideLoop;
    fn check(ctx: &TypedContext) -> Vec<LabeledDiagnostic> {
        let mut errors = Vec::new();
        let arena = ctx.arena();
        walker::walk_function_bodies(ctx, &mut |stmt_id, walk_ctx| {
            if matches!(arena[stmt_id].kind, Stmt::Break)
                && walk_ctx.loop_depth == 0
            {
                errors.push(LabeledDiagnostic::new(
                    walk_ctx.module_path.clone(),
                    AnalysisDiagnostic::BreakOutsideLoop {
                        location: arena[stmt_id].location,
                    },
                ));
            }
        });
        errors
    }
}
}

The check body is two conditions: the statement is a Break, and loop_depth is zero, meaning no enclosing loop exists at this point in the traversal. When both conditions are true, the statement's source location is captured in the diagnostic, wrapped in a LabeledDiagnostic carrying the module path of the file being walked.

The Shared Walker

Most rules need to visit every statement in every function body and inspect the statement in the context of its enclosing scopes. Implementing that traversal separately in each rule would produce identical boilerplate and separate compilation of the same code. walk_function_bodies extracts the traversal once.

walk_function_bodies and for_each_function_body

walk_function_bodies is the entry point for rules that use the shared traversal. It iterates all source files in the TypedContext, calls for_each_function_body to locate every function body, asserts that the WalkContext depths are clean at function boundaries (a debug-time invariant check), and delegates to walk_block for each body.

for_each_function_body handles all definition kinds:

• Def::Function — calls the callback with the function's body block
• Def::Struct — iterates methods and calls the callback for each method's body
• Def::Spec — recurses into the spec's nested definitions
• Def::Enum, Def::Constant, Def::ExternFunction, Def::TypeAlias — skipped

This ensures every function body in the program is visited regardless of where it is defined: top-level functions, struct methods, and functions inside spec blocks are all covered by a single call to walk_function_bodies. There is no module arm because modules are files, not AST nodes — walk_function_bodies reaches an imported module's bodies by iterating every source file in the TypedContext.

Depth Tracking

WalkContext carries four fields through the traversal:

#![allow(unused)]
fn main() {
pub(crate) struct WalkContext {
    pub loop_depth: u32,
    pub nondet_depth: u32,
    pub nondet_block_kind: Option<&'static str>,
    pub module_path: Vec<String>,
}
}

loop_depth is incremented when the walker enters a Stmt::Loop body and decremented when it exits. A rule checking the placement of break reads walk_ctx.loop_depth == 0 to determine whether the current statement is inside a loop.

nondet_depth is incremented when the walker enters a block with a non-deterministic BlockKind (forall, exists, assume, unique) and decremented on exit. A rule checking for statements inside non-det blocks reads walk_ctx.nondet_depth > 0.

nondet_block_kind stores the label of the innermost non-deterministic block ("forall", "exists", etc.) so that diagnostic messages can name the specific block kind. The walker saves and restores the previous value on entry and exit from each non-det block:

#![allow(unused)]
fn main() {
if block.block_kind.is_non_det() {
    let prev_kind = ctx.nondet_block_kind;           // save
    ctx.nondet_block_kind = Some(block_kind_label(block.block_kind));
    ctx.nondet_depth += 1;
    walk_statements(arena, &block.stmts, ctx, visitor);
    ctx.nondet_depth -= 1;
    ctx.nondet_block_kind = prev_kind;               // restore
}
}

This save/restore pattern handles nested non-det blocks correctly: if a forall block contains an exists block, the visitor sees nondet_block_kind = Some("exists") while inside the inner block, and Some("forall") again after exiting it.

module_path is not nesting state: it names the file whose bodies are currently being walked (empty for the entry file) and is reset as walk_function_bodies moves from one source file to the next. A rule clones it into each LabeledDiagnostic it emits, which is how a finding inside an imported file is attributed to that file in a multi-file report.

At each function boundary, walk_function_bodies asserts that the three nesting fields have returned to their initial values. This is a programming invariant, not user input validation: a mismatch would indicate a bug in the walker itself.

Why dyn FnMut

The visitor parameter is &mut dyn FnMut(StmtId, &WalkContext) rather than a generic impl FnMut(...). A generic parameter would cause the compiler to monomorphize walk_function_bodies separately for every closure passed to it — one copy per rule that uses the shared walker. With dyn FnMut, a single compiled copy of the walker is shared by every rule, at the cost of one indirect call per statement per rule. For a traversal whose bottleneck is AST access rather than dispatch overhead, the monomorphization savings dominate.

A004: Custom Traversal

A004 (infinite loop without break) does not use walk_function_bodies. It implements its own traversal. The reason is that its check requires scoping logic that differs from the shared walker's logic in a critical way.

The question A004 asks is: "does this loop body contain a break that targets this loop?" A break inside a nested loop targets the inner loop, not the outer one, so it must not be counted. A break inside a non-det block is prohibited by A002, so the search can stop at non-det block boundaries. But a break inside an if/else arm or a regular { } block does target the enclosing loop, so those must be recursed into.

The shared walker cannot express this. It tracks depth globally and visits every statement regardless of the nesting pattern. A004's contains_break_for_this_loop function implements exactly the required scoping:

• Recurses into if/else then-arms and else-arms
• Recurses into Stmt::Block when block_kind == Regular
• Does not recurse into Stmt::Loop bodies (break there targets the nested loop)
• Does not recurse into non-det blocks (block_kind != Regular)

This custom traversal is explicitly documented in a module-level comment in core/analysis/src/rules/infinite_loop_without_break.rs so that future maintainers understand why A004 diverges from the shared walker pattern.

Current Rules

Forty rules are registered in all_rules(). Thirty-five are error-severity — they block compilation — and five are warnings; no info-severity rule has been defined yet. Three ids in the numbering range (A013, A021, A030) are currently unassigned. The tables below group the rules by the invariant family they protect; the descriptions are condensed from the rules' own doc comments.

Control flow and termination

This family carries the core verification argument. A break with no enclosing loop (A001) has no target — the WASM br it would lower to would be malformed. A break or return inside a forall, exists, assume, or unique block (A002, A005) would short-circuit path exploration, silently invalidating an assertion whose soundness depends on every path being enumerated. A return inside a loop (A003) breaks the single-exit discipline that keeps the Rocq translation's proof obligations uniform. An infinite loop with no reachable break (A004) makes the translation non-total — Rocq requires termination. A function that can fall off its end without returning (A007) is the same non-totality in another guise (see Unreachable Emission). Recursion (A035) and unbounded stack growth (A036) are rejected in the spirit of the Power of Ten rules for safety-critical code: a statically bounded call graph is one the proof — and the runtime — can always exhaust.

Uzumaki placement

An @ outside a non-deterministic block (A006) has no set of execution paths to range over, and a standalone @ (A008) selects a value nobody observes. The rest of the family protects a codegen invariant: a compound (struct- or array-typed) @ lowers through a named stack slot, so every position that has no such slot — an argument list, a literal field or element, a reassignment — is rejected rather than silently mis-lowered.

Compound values (structs and arrays)

Compound values live in linear memory, not on the WASM value stack (see Memory Allocation). Every rule in this family fences off a position where a compound value would need to materialize without a named destination to own its memory.

Values and indexing

A022 exists because WebAssembly arithmetic wraps silently — the rule closes the front door on values that could never round-trip through their declared type (see Arithmetic Overflow). A037 turns a guaranteed runtime trap into a compile-time error when the index is statically known.

Language restrictions

These are honesty rules: each rejects, with a named diagnostic, a construct the pipeline does not (or does not yet) support — rather than letting it fail obscurely further down. A025 and A041 also remove whole classes of ambiguity (reads of uninitialized memory, shadowing) that would otherwise need proof obligations of their own. A042, A043, and A046 are permanent rather than not-yet-supported restrictions: non-deterministic blocks are proof-only by design, the two reserved names collide with codegen's own synthetic WASM exports, and a negative literal has exactly one spelling — the lexer folds the sign into the digits only when they are written together, so a separated minus is a negation of the bare magnitude and would make the same value compile or fail on a space (- 100 fits i8, - 128 does not, though -128 is a valid i8). Rejecting the separated spelling is what keeps whitespace out of the meaning of a program, in the same spirit as A033's ban on combined unary operators.

Advisory rules

The warnings are the advisory tier the severity model was designed for: each flags code that is almost certainly not what the author meant, but blocks nothing — the pipeline continues and the finding is reported alongside any errors.

Adding a New Rule

Decision: Shared Walker or Custom Traversal?

Use the shared walker when the rule's check is a simple predicate on each statement given its current depth counters. The visitor closure receives a StmtId and a &WalkContext and needs only to inspect those two values.

Use a custom traversal when the check requires different scoping than the shared walker provides — specifically, when "does this enclosing construct contain a pattern" needs to stop recursion at different boundaries than loop/non-det nesting. A004 is the canonical example.

Step-by-Step Recipe

Step 1. Create core/analysis/src/rules/your_rule.rs:

#![allow(unused)]
fn main() {
//! AXXX: Description of what the rule checks.

use inference_ast::nodes::Stmt;
use crate::{
    errors::{AnalysisDiagnostic, LabeledDiagnostic},
    walker,
};

crate::rule! {
    /// One-line description for rustdoc.
    #[id = "AXXX"]
    #[name = "Human readable name"]
    #[severity = error]
    pub struct YourRuleName;
    fn check(ctx: &TypedContext) -> Vec<LabeledDiagnostic> {
        let mut errors = Vec::new();
        let arena = ctx.arena();
        walker::walk_function_bodies(ctx, &mut |stmt_id, walk_ctx| {
            // inspect arena[stmt_id].kind and walk_ctx fields; when the
            // rule fires, push a LabeledDiagnostic pairing
            // walk_ctx.module_path with the diagnostic
        });
        errors
    }
}
}

Step 2. Register the module in core/analysis/src/rules/mod.rs:

#![allow(unused)]
fn main() {
pub mod your_rule;
use your_rule::YourRuleName;

pub fn all_rules() -> &'static [&'static dyn crate::rule::Rule] {
    &[
        // ... existing rules ...
        &YourRuleName,
    ]
}
}

Step 3. Add a diagnostic variant to AnalysisDiagnostic in core/analysis/src/errors.rs:

#![allow(unused)]
fn main() {
#[error("what happened; why it is a problem; how to fix it")]
YourDiagnosticVariant { location: Location },
}

Step 4. Add the rule_id() arm in the same file:

#![allow(unused)]
fn main() {
AnalysisDiagnostic::YourDiagnosticVariant { .. } => "AXXX",
}

Step 5. Update the rule_ids_match_diagnostic_rule_ids test in core/analysis/src/lib.rs. This test asserts that all_rules().len() == diagnostics.len() and that each rule's id() matches its corresponding diagnostic's rule_id(). Adding a rule without updating this test will fail the build.

#![allow(unused)]
fn main() {
AnalysisDiagnostic::YourDiagnosticVariant { location: dummy_location() },
}

Step 6. Write tests. The test suite for each rule lives alongside the rule source or in tests/src/analysis/. Test at minimum: the rule fires on a program that should trigger it, and the rule does not fire on a valid program.

Related Resources

• core/analysis/src/rule.rs — Rule trait definition and rule! / __severity! macro implementations
• core/analysis/src/walker.rs — walk_function_bodies, for_each_function_body, WalkContext
• core/analysis/src/lib.rs — analyze() entry point, rule dispatch loop, rule_ids_match_diagnostic_rule_ids test
• core/analysis/src/errors.rs — AnalysisDiagnostic, AnalysisErrors, AnalysisResult, Severity
• core/analysis/src/rules/ — one file per rule
• book/unreachable-emission-in-codegen.md — related discussion of control flow enforcement in the codegen pass
• book/arithmetic-overflow-in-wasm-codegen.md — example of another property with formal verification implications

Memory Allocation in WASM Codegen

Inference compiles fixed-size arrays to WebAssembly linear memory using a shadow stack. This document explains how arrays are allocated, initialized, accessed, passed to functions, and deallocated. It covers the WASM instructions emitted for each operation, the rationale behind the design, how other compilers handle the same problems, and the formal verification implications.

The Problem

WebAssembly's native value model is flat: every local variable is a scalar (i32, i64, f32, f64). There is no instruction for declaring a local of type "array of 3 integers." When a language has compound types — arrays, structs, strings — the compiler must place them somewhere in linear memory and manipulate them via pointers and load/store instructions.

Three allocation strategies are available:

1. Static data segment: Embed the array in the module's data section. Works for immutable constants but not for stack-scoped mutable arrays.
2. Heap allocation: Use a malloc/free scheme or a garbage collector. Requires a runtime, introduces allocation failure modes, and makes formal verification significantly harder.
3. Shadow stack: Reserve a region of linear memory and manage it with a stack pointer global, mirroring how native compilers manage function call frames.

Inference uses option 3. Arrays have stack-scoped lifetimes (they are created when a function is entered and destroyed when it returns), so they fit naturally into a stack discipline. No runtime, no allocator, no GC.

Linear Memory Layout

WebAssembly linear memory is a contiguous byte array. Inference allocates one page (64 KB) and uses it entirely as a stack:

Linear Memory (1 page = 64KB)
+--------------------------------------------+  0x10000 (65536)
|                                            |
|     (free space)                           |
|     (future: data sections, heap)          |
|                                            |
+-- __stack_pointer -------------------------+  STACK_SIZE (65536)
|                                            |
|         Stack (grows downward)             |
|                                            |
+--------------------------------------------+  0x00000
  overflow below 0 = WASM OOB trap

__stack_pointer is a mutable i32 WebAssembly global initialized to 65536 — the top of the stack region. When a function that needs a frame is called, __stack_pointer is decremented by the frame size; when the function returns, it is restored. Not every function that touches arrays needs a frame: a function whose only compound values are parameters it provably never writes reads them through the caller's pointers and never touches __stack_pointer at all (see Array Parameter Passing). The stack grows downward toward address 0, following the --stack-first convention used by Rust and Zig when targeting WebAssembly. Any stack overflow that pushes the pointer below address 0 causes a WASM out-of-bounds memory trap automatically, providing free overflow protection without a runtime guard. Future data sections and heap allocations will be placed above the stack region, starting at STACK_SIZE and growing upward.

Programs without arrays do not get a memory section, a global section, or any memory-related exports. The compiler tracks a has_memory flag and only emits these sections when at least one function uses arrays. Existing programs produce identical WASM output — zero regression.

Stack Frame Layout

Each function that needs frame memory gets a FrameLayout — a per-function data structure computed before code generation. It maps each array variable to an ArraySlot describing its byte offset within the frame, element size, and element count. Array variables always occupy the frame; an array parameter occupies it only when the callee may write it (see Array Parameter Passing).

Consider a function with two arrays:

pub fn two_arrays() -> i32 {
    let a: [i32; 2] = [1, 2];
    let b: [i32; 2] = [3, 4];
    return 0;
}

The frame layout computation:

1. a: [i32; 2] — element size 4, count 2, total 8 bytes, offset 0
2. b: [i32; 2] — element size 4, count 2, total 8 bytes, offset 8
3. Raw size: 16 bytes
4. Aligned to 16-byte boundary: 16 bytes (already aligned)

Frame alignment is 16 bytes, matching the LLVM and Rust WASM convention. A function with a single [bool; 3] array (3 bytes raw) gets a 16-byte frame. A function with [i64; 3] (24 bytes raw) gets a 32-byte frame.

Each array within the frame is aligned to its element type's natural alignment — the same convention used by LLVM, Rust, and BasicCABI. A [bool; 3] (1-byte elements) followed by a [i32; 2] (4-byte elements) gets 1 byte of padding inserted between them so the i32 array starts at a 4-byte-aligned offset. The padding bytes are automatically zeroed by memory.fill in the prologue. This makes the MemArg alignment hints in load/store instructions truthful, which allows runtimes to use optimized aligned load paths where available.

The frame pointer is stored in a synthetic WASM local named __frame_ptr. This local is added during the local pre-scan phase alongside the user's declared locals.

Function Prologue and Epilogue

Every function with a frame emits a prologue at entry and an epilogue at every exit point. A function whose layout comes out empty — including one whose only compound values are read-only parameters — emits neither.

Prologue

The prologue decrements __stack_pointer, saves the frame pointer, and zero-initializes the entire frame:

;; Prologue for a 16-byte frame
global.get 0              ;; load __stack_pointer
i32.const 16              ;; frame size
i32.sub                   ;; decrement
local.tee $__frame_ptr    ;; save frame pointer AND keep on stack
global.set 0              ;; update __stack_pointer
local.get $__frame_ptr    ;; destination for memory.fill
i32.const 0               ;; fill value (zero)
i32.const 16              ;; fill length
memory.fill               ;; zero-initialize entire frame

The zero-initialization via memory.fill prevents uninitialized reads, ensures deterministic behavior across function calls, and eliminates information leakage between stack frames. This matches Zig's approach to stack initialization.

The memory.fill is technically redundant when all array elements are explicitly initialized (e.g., let arr: [i32; 3] = [1, 2, 3]). The simplicity and safety of unconditional zeroing outweigh the negligible runtime cost. A future optimization pass could skip memory.fill when all arrays in the frame are provably fully initialized.

Epilogue

The epilogue restores __stack_pointer to its pre-call value:

;; Epilogue for a 16-byte frame
local.get $__frame_ptr    ;; saved frame pointer
i32.const 16              ;; frame size
i32.add                   ;; compute original stack pointer
global.set 0              ;; restore __stack_pointer

The epilogue is emitted at two sites:

1. Before every return statement
2. Before the function-end unreachable / end sequence

Both sites must emit the epilogue. Missing one would silently corrupt __stack_pointer, causing subsequent function calls to allocate overlapping frames.

Here is the complete WAT output for a function that allocates, initializes, and returns:

(func $i32_array (type 0) (result i32)
  (local $arr i32) (local $__frame_ptr i32)
  ;; --- prologue ---
  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
  ;; --- store elements ---
  local.get $__frame_ptr
  i32.const 0
  i32.add
  i32.const 10
  i32.store              ;; arr[0] = 10
  local.get $__frame_ptr
  i32.const 4
  i32.add
  i32.const 20
  i32.store              ;; arr[1] = 20
  local.get $__frame_ptr
  i32.const 8
  i32.add
  i32.const 30
  i32.store              ;; arr[2] = 30
  local.get $__frame_ptr
  local.set $arr         ;; arr = frame_ptr (base address)
  ;; --- return with epilogue ---
  i32.const 0
  local.get $__frame_ptr
  i32.const 16
  i32.add
  global.set 0           ;; restore __stack_pointer
  return
  ;; --- function-end epilogue + unreachable ---
  local.get $__frame_ptr
  i32.const 16
  i32.add
  global.set 0
  unreachable
)

Array Literal Lowering

An array literal [10, 20, 30] is lowered by storing each element at its computed offset from the frame pointer:

;; For element i of an array at frame offset `array_offset`:
local.get $__frame_ptr
i32.const <array_offset + i * elem_size>
i32.add
<push element value>
<store instruction>

After all elements are stored, the variable is set to the array's base address:

local.get $__frame_ptr
i32.const <array_offset>
i32.add
local.set $arr

The array variable itself is an i32 local holding the base pointer. All subsequent reads and writes go through this pointer.

Store Instruction Selection

The store instruction depends on the element type:

WASM encodes alignment as log2(byte_alignment). A 4-byte i32.store with natural alignment encodes align=2 because 2^2 = 4.

For a [bool; 4] array, elements are packed byte-by-byte:

;; let flags: [bool; 4] = [true, false, true, false];
local.get $__frame_ptr
i32.const 0
i32.add
i32.const 1              ;; true
i32.store8               ;; 1 byte at offset 0
local.get $__frame_ptr
i32.const 1
i32.add
i32.const 0              ;; false
i32.store8               ;; 1 byte at offset 1
local.get $__frame_ptr
i32.const 2
i32.add
i32.const 1              ;; true
i32.store8               ;; 1 byte at offset 2
local.get $__frame_ptr
i32.const 3
i32.add
i32.const 0              ;; false
i32.store8               ;; 1 byte at offset 3

Array Index Read

Reading arr[i] emits a load instruction. The exact instruction sequence depends on whether the index is zero, a non-zero compile-time constant, or a runtime expression.

Zero index (arr[0]) — the base pointer is the element address; no offset computation:

;; return arr[0]  where arr: [i32; 3]
local.get $arr            ;; push base pointer (i32)
i32.load                  ;; load i32 directly at base address

Constant non-zero index (arr[1], arr[2], ...) — the byte offset is folded at compile time:

;; return arr[1]  where arr: [i32; 3]
local.get $arr            ;; push base pointer (i32)
i32.const 4               ;; compile-time offset = 1 * elem_size
i32.add                   ;; address = base + 4
i32.load                  ;; load i32 from computed address

Variable index (arr[i]) — offset computed at runtime:

;; return arr[i]  where arr: [i32; 3]
local.get $arr            ;; push base pointer (i32)
local.get $i              ;; push index (i32)
i32.const 4               ;; element size
i32.mul
i32.add                   ;; address = base + index * 4
i32.load                  ;; load i32 from computed address

Load Instruction Selection

The load instruction depends on the element type and its signedness:

Signed types use sign-extending loads (load8_s, load16_s) to correctly propagate the sign bit from the stored byte/halfword into the full i32 value. Unsigned types and bool use zero-extending loads (load8_u, load16_u).

This distinction matters: an i8 value of -1 is stored as 0xFF. When loaded with i32.load8_s, it becomes 0xFFFFFFFF (-1 as i32). When loaded with i32.load8_u, it would become 0x000000FF (255 as i32). Using the wrong extension would silently corrupt signed values.

Array Index Write

Writing arr[i] = value emits a store instruction using the same three-case index specialization as array index read.

Zero index (arr[0] = x) — no offset computation:

;; arr[0] = 42  where arr: [i32; 3]
local.get $arr            ;; push base pointer
i32.const 42              ;; push value
i32.store                 ;; store i32 at base address

Constant non-zero index (arr[N] = x) — offset folded at compile time:

;; arr[1] = 42  where arr: [i32; 3]
local.get $arr            ;; push base pointer
i32.const 4               ;; compile-time offset = 1 * elem_size
i32.add                   ;; address = base + 4
i32.const 42              ;; push value
i32.store                 ;; store i32 at computed address

Variable index (arr[i] = x) — offset computed at runtime:

;; arr[i] = 42  where arr: [i32; 3]
local.get $arr            ;; push base pointer
local.get $i              ;; push index
i32.const 4               ;; element size
i32.mul
i32.add                   ;; address = base + index * 4
i32.const 42              ;; push value
i32.store                 ;; store i32 at computed address

The type checker enforces that the array variable is declared mut before allowing index assignment. Writing to a non-mutable array is a compile-time error.

Array Parameter Passing

Arrays are passed to functions by pointer at the WASM level. At call sites, the caller pushes the array's base address (an i32) onto the stack:

;; Caller: sum_array(data)
local.get $data           ;; push array base pointer
call $sum_array

The callee receives this pointer as a regular i32 parameter. What it does with that pointer depends on whether anything can write through it. A parameter the callee may write is copied into the callee's own stack frame on entry, so the write lands on a private copy and the caller's array is untouched. A parameter that is provably only ever read is used where it is — the callee loads straight from the caller's memory, allocating no frame slot and emitting no copy.

Both lowerings implement the same language rule: an argument's value does not change across a call. The copy is how that rule is enforced where it could otherwise be broken, not the rule itself. Everything in this section applies equally to struct parameters and to method receivers, which are parameters like any other.

When a Copy Is Emitted

A compound parameter — an array, or a struct with at least one byte of fields — is copied on entry when either of two things is true of the callee's body.

1. It is assigned through. Any assignment whose target is rooted at the parameter counts: arr[0] = 9, p.x = 9, g.cells[1].y = 9, whole-binding reassignment p = P { .. }, and the non-deterministic form p = @. Stmt::Assign is the language's only write statement — there is no compound-assignment form and no += family — so this is the complete set of writes a body can perform on its own parameters.

2. It reaches an external fn argument. A linked external shares the program's single linear memory and receives a compound argument as a raw pointer, so its body can store through that pointer. Those stores live in a .wasm the compiler never type-checked, so it cannot see them. Any parameter that flows to an external argument therefore keeps its copy, and the foreign writes land in the callee's frame rather than in the caller's memory.

A parameter that does neither is passed by reference. Reads are unaffected either way: a field or element address is the base pointer plus an offset computed the same way in both lowerings, and the base pointer is the only thing the two disagree about.

Note what decides this: the body, not the declaration. The mut marker is a contract with the type checker — it states whether the function is permitted to assign through the parameter, and a program that assigns through a parameter declared without it is rejected. Whether a copy is emitted is a separate, internal question about what the body actually does, so a mut parameter that is never assigned is passed by reference exactly like a non-mut one. Deciding on the marker instead would mean that dropping a mut a function does not need makes the program faster, putting the annotation's cost in opposition to its purpose. Neither lowering is observable from Inference source, so there is no reason to write a program one way rather than another in order to obtain one of them.

By-Reference Parameters

sum_array reads three elements and writes nothing, so its parameter gets no frame slot. Nothing else in the function needs memory either, so the function gets no frame at all:

(func $sum_array (param $arr i32) (result i32)
  local.get $arr
  i32.load                ;; arr[0], loaded from the caller's memory
  local.get $arr
  i32.const 4
  i32.add
  i32.load                ;; arr[1]
  i32.add
  local.get $arr
  i32.const 8
  i32.add
  i32.load                ;; arr[2]
  i32.add
  return
  unreachable             ;; function-end sentinel after the terminal return
)

There is no __frame_ptr local, no zero-initialization, no copy, no epilogue, and — the part that matters most for verification — no read or write of __stack_pointer. A leaf reader like this one is a pure function of memory rather than a function that mutates a global, which is a simplification every caller inherits.

Copy-on-Entry

mutate_copy assigns through its parameter, so the parameter earns a frame slot. The prologue allocates and zero-initializes the frame (see Function Prologue and Epilogue), each element is copied from the caller's pointer into that slot, and the parameter local is then overwritten with the slot's address so the rest of the body is identical whichever lowering was chosen:

(func $mutate_copy (param $arr i32) (result i32)
  (local $__frame_ptr i32)
  ;; --- prologue: allocate and zero a 16-byte frame ---
  ;; --- copy element 0 ---
  local.get $__frame_ptr
  i32.const 0
  i32.add
  local.get $arr          ;; source: caller's pointer
  i32.load                ;; load element 0 from caller
  i32.store               ;; store into callee's frame
  ;; --- copy element 1 ---
  local.get $__frame_ptr
  i32.const 4
  i32.add
  local.get $arr
  i32.const 4
  i32.add
  i32.load
  i32.store
  ;; --- copy element 2 ---
  local.get $__frame_ptr
  i32.const 8
  i32.add
  local.get $arr
  i32.const 8
  i32.add
  i32.load
  i32.store
  ;; --- redirect parameter to local copy ---
  local.get $__frame_ptr
  local.set $arr          ;; now $arr points to callee's copy
  ;; ... function body uses $arr normally ...
)

After the copy, $arr points to the callee's own memory, so the mutation affects only the local copy. The caller's array is untouched.

This can be verified with the verify_copy_semantics test:

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

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

mutate_copy modifies its local copy and returns 99. verify_copy_semantics passes data to mutate_copy, then reads data[0] — which is still 1. The callee's mutation did not affect the caller.

Copy Optimization

Where a copy is emitted, its shape depends on the array's size. For arrays with 16 or fewer elements, the copy is unrolled element by element (as shown above). For arrays with more than 16 elements, a single memory.copy instruction replaces the unrolled loop:

;; Bulk copy for arr: [i32; 64] (256 bytes)
local.get $__frame_ptr
i32.const <offset>
i32.add                   ;; destination: callee's frame
local.get $arr            ;; source: caller's pointer
i32.const 256             ;; byte count
memory.copy               ;; bulk copy

The threshold of 16 elements balances code size (unrolled copies are larger but avoid call overhead) against simplicity.

Receivers and Linked Externals

A method receiver is a parameter, and the rule above is the whole rule for it too. A method that assigns through self copies the receiver on entry; a method that only reads it does not, whether the receiver is written self or mut self.

The external case deserves its own note, because it is the one place where a write is invisible in Inference source. Linking merges every module into one linear memory, and a compound external fn parameter is lowered to a raw i32 pointer with no copy between the call site and the foreign body. The external is free to store through that pointer. A method or function that hands a parameter — or any projection of one, such as self.field or arr[i] — to an external therefore keeps its copy, so the foreign stores land on the callee's own bytes. This is conservative in the harmless direction: an external that only reads still costs its callers a copy, because the declaration does not yet say which of its parameters it writes. Making that claim explicit and checking it against the merged body is future work; until then, a parameter forwarded to an external is never passed by reference. The linker's side of this arrangement is described in The WASM Linker.

Why Value Semantics

The language guarantee is that an argument's value does not change across a call. The alternative — reference semantics, where a callee reads and writes the caller's memory directly and any function may mutate what it is handed — would avoid every copy, and it introduces three problems that the guarantee exists to prevent:

1. It breaks the mut system: a function receiving arr: [i32; 3] (not mut) could mutate the caller's array through the pointer, violating what the type system promised. The copy is what keeps that promise wherever a write is possible, and where no write is possible there is nothing to break.

2. It breaks referential transparency: if f(arr) can modify arr, then f(arr); g(arr) and g(arr); f(arr) may produce different results. Because a parameter is passed by reference only when the callee provably never writes it, calls stay independent.

3. It complicates formal verification: proofs against mutable references need heap effect reasoning and aliasing analysis. Passing a read-only parameter by pointer introduces neither, since a region no one writes during the call cannot be the subject of either.

Inference optimizes for provability, not performance — which is why the guarantee is stated in terms of observable values and the copy is treated as one way to obtain it. A copy that no program can distinguish from its absence buys no provability, and eliding it removes instructions, a frame, and a global effect from the proof surface without weakening anything a proof may assume.

Arrays in Non-Deterministic Blocks

Arrays work inside forall, exists, assume, and unique blocks. The frame layout scanner recurses into all block types to discover array variables, and prologue/epilogue emission handles them uniformly.

Uzumaki Arrays

The uzumaki operator @ can initialize an entire array with non-deterministic values:

pub fn array_uzumaki_init() {
    forall {
        let arr: [i32; 3] = @;
        let x: i32 = arr[0];
    }
}

This is lowered by emitting an i32.uzumaki (opcode 0xfc 0x31) for each element and storing it at the corresponding offset:

;; Element-wise uzumaki for arr: [i32; 3] = @
local.get $__frame_ptr
i32.const <offset + 0>
i32.add
0xfc 0x31                 ;; i32.uzumaki — non-deterministic i32
i32.store

local.get $__frame_ptr
i32.const <offset + 4>
i32.add
0xfc 0x31                 ;; i32.uzumaki
i32.store

local.get $__frame_ptr
i32.const <offset + 8>
i32.add
0xfc 0x31                 ;; i32.uzumaki
i32.store

Each element gets an independent non-deterministic value. This means forall { let arr: [i32; 3] = @; } quantifies over all possible 3-element i32 arrays — the Cartesian product of all i32 values for each position.

Individual array elements can also be assigned uzumaki values:

pub fn array_assign_uzumaki_in_forall() {
    let mut arr: [i32; 2] = [0, 0];
    forall {
        arr[0] = @;
    }
}

This emits a single i32.uzumaki + i32.store at the computed index address.

Comparison with Other Compilers

LLVM / Clang to WASM

LLVM uses the same shadow stack pattern with a __stack_pointer mutable global. The convention is documented in the WebAssembly tool conventions. Key differences:

• LLVM keeps __stack_pointer as an internal global (not exported by default). Inference exports it unconditionally, which is useful for test harnesses but exposes internal state. A future BuildProfile feature will make this conditional — export in Debug, hide in Release.
• LLVM uses wasm-ld to link objects and manage the stack. Inference generates complete modules directly via wasm-encoder, with no linker step.
• LLVM may use memory.copy and memory.fill via the bulk-memory proposal. Inference also uses both instructions.

Rust to WASM

Rust arrays on WASM use the same LLVM shadow stack with --stack-first layout: the stack occupies the bottom of the address space and grows downward toward address 0, while data sections are placed above. [i32; 3] is allocated on the shadow stack with a frame pointer pattern identical to Inference's output. Rust passes small arrays by value (copying into the callee's frame) and large aggregates by reference with compiler-generated memcpy.

Inference now matches Rust's stack-first layout. The remaining difference is how each language earns the right to skip a copy. Rust's borrow checker lets the caller pass &[i32; 3] explicitly, and the reference is part of the signature. Inference has no borrow checker and no reference type; it recovers the same lowering from the callee's body instead, passing a compound parameter by pointer whenever nothing in that body can write through it. The result is a compiler-internal decision rather than a type, so it cannot be requested, spelled, or observed in Inference source.

Zig to WASM

Zig also uses --stack-first layout when targeting WASM, placing the stack at low addresses so overflow naturally traps. Inference matches this layout. Zig zero-initializes local arrays (matching Inference's memory.fill approach). Zig's safety modes add bounds checks on array access; Inference does not currently emit bounds checks (this is deferred to a future BuildProfile feature).

WASM Section Layout

When has_memory is true, the compiler emits three additional sections in the WASM module:

These sections are ordered according to the WASM specification: Type, Function, Memory, Global, Export, Code, Name. The ordering is mandatory — a misordered module fails validation.

When no function uses arrays, these sections are omitted entirely. The output is byte-identical to what the compiler produced before array support was added.

Formal Verification Implications

Modeling Arrays in Rocq

Arrays in linear memory map naturally to Rocq's list or Vector.t n types. The shadow stack's frame-scoped lifetime means each array has a clear birth (prologue) and death (epilogue), avoiding the need for heap allocation reasoning.

Parameter passing is particularly beneficial for verification, and the property it supplies is no mutable aliasing: every compound region has at most one writer for as long as a call is live.

The two lowerings supply it differently. A parameter the callee may write is copied into a region no other frame can name, so in Rocq f(arr: [i32; 3]) is modeled as taking a Vector.t int32 3 by value — a fresh value, independent of the caller's, with no aliasing and no frame condition on the caller's state. A parameter the callee provably never writes is passed by pointer and does alias the caller's region, but neither frame stores into that region for the duration of the call, so no proof has to order the two frames' accesses. It is modeled as a read over a region the caller's frame condition already pins — the weaker and cheaper of the two obligations. What must be pinned is exactly what the caller already had to establish: that the region holds the value the caller put there. The callee adds no clause.

The elision also removes an effect rather than just instructions. A function whose parameters and bindings all need no memory has no frame, so it never reads or writes __stack_pointer. A leaf reader is then a pure function of memory instead of a function carrying a global-effect clause that every caller inherits transitively.

The one case where the property would not hold on its own is a parameter forwarded to a linked external, whose foreign body can store through the pointer it is handed. Such a parameter is always copied, which puts the foreign writer back inside a region only it can name.

Zero-Initialization as a Proof Obligation

The prologue's unconditional whole-frame zero-initialization establishes a known precondition: every byte in the frame is zero before any user code executes. In Rocq, this can be encoded as:

forall (offset : nat), offset < frame_size -> load_byte (frame_ptr + offset) = 0

This precondition holds for free — the compiler guarantees it, so the Rocq proof can assume it without additional proof obligation on the programmer.

It survives by-reference parameters unchanged, because it quantifies over the frame that exists. A frame is still zeroed in full: no region within it is skipped, and no side condition about which offsets are live is introduced. A parameter passed by pointer contributes no bytes to the frame, so it is simply outside the quantifier's range — and a function with no frame at all discharges the hypothesis vacuously. Partial or region-selective filling would be a different matter: it would replace this one-line hypothesis with a layout-dependent side condition and make the model depend on what the emitter happens to emit, which is why the fill stays unconditional.

Bounds Checking as a Future Proof Obligation

Array index access is bounds-checked: a constant out-of-bounds index is rejected at compile time (analysis rule A037), and a dynamic index emits a runtime guard (index >= length -> unreachable) in all Compile-mode builds.

The remaining verification step is Proof mode. Emitting the guard in proof mode and extending the Rocq ValidModule/ValidSpec contract with a "no reachable trap" clause would turn the bound into a proof obligation — the programmer proves 0 <= i < array_length to discharge it, and a proven module can then elide the runtime guard so the verified artifact is the deployed artifact. This is tracked as future work (issue #214).

Current Implementation

The memory infrastructure is in core/wasm-codegen/src/memory.rs (constants, data structures, store/load helpers, prologue/epilogue emission, parameter copy). Frame layout computation and array lowering methods are in core/wasm-codegen/src/compiler.rs, including the body scan that decides whether a compound parameter is written or forwarded to an external and therefore needs a frame slot at all. That decision is made in one place, when the frame layout is computed: the entry-copy loop emits a copy exactly when a slot exists, so the two cannot disagree.

The implementation uses coverage marks to verify that each code path is exercised by the test suite:

Arithmetic Overflow in WASM Codegen

Inference compiles to WebAssembly. WebAssembly integer arithmetic wraps silently on overflow for add, subtract, and multiply. This document explains what that means exactly, how it differs from other languages, what Inference's codegen currently does, and why this matters for a language that targets formal verification.

The Problem

Every fixed-width integer type has a representable range. When an arithmetic result falls outside that range, the implementation must choose: trap, wrap, saturate, or invoke undefined behavior. The choice is not cosmetic — it determines what programs mean, what optimizers are allowed to do, and what formal proofs must encode.

For a language like Inference, whose core value proposition is verification via Rocq translation, the overflow semantics of every arithmetic operation must be precisely defined. An underspecified overflow behavior makes it impossible to write a sound proof about any computation that could overflow.

WebAssembly Overflow Semantics

The WebAssembly specification, section 4.3.2 defines integer arithmetic as follows:

The result is computed modulo 2^N, where N is the bit width.

This is a complete and unconditional specification. WASM integer add, subtract, and multiply never trap. They always produce a result by discarding the bits that do not fit. There is no undefined behavior, no implementation-defined behavior, no signal.

Wrapping Instructions

The following instructions wrap silently on overflow:

In two's complement, "result mod 2^N" is the same as taking the low N bits of the mathematical result. i32::MAX + 1 produces i32::MIN. i32::MIN - 1 produces i32::MAX. Multiplying i32::MAX * 2 produces -2. These are not errors — they are the defined results.

Trapping Instructions

Division and remainder behave differently:

The div_s (MIN, -1) trap is the one case where division produces a result that cannot be represented: i32::MIN / -1 would be 2147483648, which exceeds i32::MAX. WASM traps rather than wrap here. The corresponding rem_s (MIN, -1) does not trap because the mathematical remainder is 0, which is representable.

This asymmetry between div_s and rem_s on (MIN, -1) is a common source of confusion for compiler authors and is worth explicit documentation in any codebase that lowers division.

Negation

WASM has no integer negation instruction. Negation is computed as 0 - x using i32.sub or i64.sub. Because subtraction wraps, negating the minimum value of a signed type wraps back to itself:

0 - i32::MIN = 0 - (-2147483648) = 2147483648 mod 2^32 = -2147483648

Negating i32::MIN gives i32::MIN. This is correct two's complement behavior and is the WASM-mandated result.

Shift Instructions

Shift amounts are masked to the bit width of the value being shifted. For i32, the shift amount is masked to 5 bits (values 0–31). For i64, the shift amount is masked to 6 bits (values 0–63). Shifting by the full bit width is not a trap — it produces a shift by 0, which is the identity. This is specified in section 4.3.2 of the WASM specification.

Inference's Current Approach

Inference inherits WASM's wrapping semantics for add, subtract, multiply, and negation: those emit bare arithmetic instructions with no overflow guard, and there is no compile-time overflow detection for them. Division is the one exception — signed division overflow (MIN / -1) traps at every width, natively for i32/i64 and via a compiler-added guard for the narrow types (see Division and Modulo). Separately, a dynamic (runtime-index) array access and a failing assert emit their own runtime traps.

Binary Expression Lowering

lower_binary_expression in core/wasm-codegen/src/compiler.rs dispatches to the appropriate WASM instruction based on the left operand's type and emits it unconditionally:

;; Inference: return 2147483647 + 1
i32.const 2147483647
i32.const 1
i32.add          ;; wraps to -2147483648 — no trap, no check
return

No overflow check precedes the i32.add. The result is exactly what WASM's specification says: -2147483648.

Negation Lowering

lower_prefix_unary_expression lowers the unary negation operator -x as 0 - x:

;; Inference: return -min  (where min = i32::MIN)
i32.const 0
local.get $min   ;; pushes -2147483648
i32.sub          ;; 0 - (-2147483648) wraps to -2147483648
return

Negating i32::MIN produces i32::MIN. This is verifiable against the golden WAT output in tests/test_data/codegen/wasm/arith_overflow/arith_overflow.wat:

(func $i32_neg_min (;6;) (type 6) (result i32)
  (local $min i32)
  i32.const -2147483648
  local.set $min
  i32.const 0
  local.get $min
  i32.sub
  return
  unreachable
)

Unsigned Types and Bit-Pattern Reinterpretation

WASM has no unsigned integer types. All integer values are stored in i32 or i64 slots and interpreted as unsigned or signed by the individual instruction. Inference maps u32 to i32 and u64 to i64 by reinterpreting the bit pattern.

Unsigned literals use .cast_signed() in lower_number_literal:

#![allow(unused)]
fn main() {
// u32 literal: parse as u32, reinterpret bits as i32
let val = number_literal.value.parse::<u32>()
    .expect("Failed to parse unsigned 32-bit integer literal")
    .cast_signed();
func.instruction(&Instruction::I32Const(val));
}

u32::MAX (4294967295) has the bit pattern 0xFFFFFFFF. When reinterpreted as a two's complement i32, that is -1. The wrapping behavior is identical: i32.add(-1, 1) produces 0, which is the correct WASM result for u32::MAX + 1.

Sub-i32 Types (i8, i16, u8, u16)

Sub-i32 types are promoted to i32 for all arithmetic. The WASM i32.add instruction operates on the full 32-bit value, so a result that would overflow the sub-type's declared width is possible immediately after the raw operation.

Inference closes that gap by re-narrowing the result at the producing instruction, immediately after the operation and before it is stored to a local. memory::emit_sub_i32_narrowing (core/wasm-codegen/src/memory.rs:652) emits the shape appropriate to the type:

• Signed (i8, i16): shl <32-width> then shr_s <32-width> — shifting the value up so the sub-type's sign bit lands in bit 31, then an arithmetic shift back down, which sign-extends from that bit. For i8 this is shl 24 / shr_s 24; for i16, shl 16 / shr_s 16.
• Unsigned (u8, u16): and 0xFF / and 0xFFFF — a zero-extending bitmask.

i32.extend8_s/i32.extend16_s would express the signed case more directly, but Inference does not use them. The historical reason was that the wasm-to-v translator had no case for those opcodes, so shl/shr_s was the only spelling that stayed translatable to Rocq; the translator now lowers all five sign-extension opcodes to BI_unop t (Unop_extend n), so the constraint no longer binds and the two-instruction decomposition is simply what codegen still emits. Changing it would move every golden .wasm for no semantic gain.

This narrowing is emitted at every place a sub-i32 value is produced, not just arithmetic:

• Binary expressions (lower_binary_expression, core/wasm-codegen/src/compiler.rs:4404) — for every operator except comparisons (Eq/Ne/Lt/Le/Gt/Ge, which produce bool, not the operand's sub-type), Mod, And, Or, and Shr.
• Unary negation (core/wasm-codegen/src/compiler.rs:4439) and unary bitwise-not (core/wasm-codegen/src/compiler.rs:4456).
• A scalar uzumaki (@) draw of a narrow type — see Sub-i32 Truncation below; bool and enum draws get an analogous and 1 / rem_u <variant count> constraint rather than this mask/shift shape, since their domains aren't sub-i32 integer ranges.

Signed division is the one producer whose promoted result can fall outside the narrow type's range in a way this re-narrowing would silently mask rather than merely truncate: for (MIN, -1) the promoted quotient is +128/+32768, which the shl/shr_s re-narrowing would wrap back to MIN — the wrong answer, with no failure signal. That case is caught by an overflow guard emitted before the re-narrowing, so division overflow traps instead of wrapping. See Division and Modulo.

The current behavior therefore matches C's integer promotion rule (arithmetic is done in the promoted width) and truncates back to the sub-type's width immediately afterward, so a sub-i32 local never holds a value outside its declared range.

Division and Modulo

Integer arithmetic wraps at every width, with one deliberate exception: division overflow traps at every width. Divide-by-zero and remainder-by-zero pass through as native WASM traps at every width, and so does signed division's single overflow case, MIN / -1.

For i32/i64, wasm's own div_s already traps on (MIN, -1). The narrow signed types (i8/i16) divide in the promoted i32 width, where the overflowing quotient (+128/+32768) is representable — so no wasm trap fires — and the mandatory re-narrowing would silently sign-wrap it back to MIN. The compiler closes that gap with a guard on the promoted quotient, emitted after div_s and before the re-narrowing:

i32.div_s
local.tee $scratch    ;; single-evaluate the promoted quotient
i32.const 128         ;; 32768 for i16
i32.eq
if (empty)
  unreachable
end
local.get $scratch

A single equality is exhaustive because the operands are canonical sign-extended values (ABI entry normalization, producing-instruction re-narrowing, and sign-extending loads all keep a narrow local in range), so |q| <= |a| <= 2^(w-1) and the promoted quotient equals +2^(w-1) only for (MIN, -1). Running the guard after div_s preserves the native divide-by-zero trap. The guard is emitted in both compile and proof modes, so a proof carries the same cannot-trap obligation at every width.

MIN % -1 is 0 at every width — the mathematically correct remainder, always representable — and is intentionally not trapped; only x % 0 traps (natively). The trap kind differs by width: the narrow guard traps as unreachable, while i32/i64 report wasm's native integer-overflow trap. It is the trap-or-not contract, not the trap code, that is width-uniform.

Exported ABI Parameter Guards

At the WebAssembly ABI boundary a host may pass any i32 bit pattern for a parameter, so an exported function normalizes or validates each parameter in its prologue. The rule is: normalize where a host convention already assigns every wire value a meaning, and trap where the domain is partial. A narrow integer parameter takes its low bits (the C ABI) and a bool takes truthiness (any nonzero is true) — both are total maps, so they are normalized silently. An enum parameter is different: only tags 0..N-1 name a variant, so a tag >= N names nothing under any convention, and the prologue rejects it with i32.const N; i32.ge_u; if; unreachable; end (a negative tag arrives as a huge unsigned value and is caught by the same unsigned compare). A variantless enum is uninhabited, so its guard (>= 0) traps on every host call.

This is the same rem_u opcode the uzumaki draw uses to constrain an enum draw to 0..N-1 (see Sub-i32 Truncation), used in a different context. A non-deterministic draw is provenance-free: it needs only a surjection onto the variant domain, and rem_u N is a valid one. A host-supplied tag is a concrete input with provenance, so mapping it with rem_u N would silently relabel it as a variant the host never named — inventing data. Concrete out-of-domain inputs are therefore trapped, not folded.

Comparison with Other Languages

The critical distinction is between defined behavior and undefined behavior. C's undefined behavior for signed overflow means the optimizer is allowed to assume overflow never occurs, leading to deleted bounds checks, eliminated branches, and silent wrong results. WASM has no such latitude — the specification fully defines every overflow result, making the behavior predictable regardless of optimization level.

Compiler Patterns

rustc to WASM

When Rust compiles to wasm32-unknown-unknown in debug mode, it inserts overflow checks for every arithmetic operation on integer types. The check is implemented via the checked_add / checked_sub / checked_mul intrinsics in MIR: each operation returns Option<T>, and if the value is None (overflow occurred), execution falls through to a panic call. On WASM, that panic call lowers to unreachable. The net effect is a conditional unreachable that fires on overflow:

;; Conceptual structure of Rust's debug-mode overflow check for i32 + i32
;; (actual Cranelift output may differ in register usage and block layout)
local.get $a
local.get $b
i32.add
local.tee $result
local.get $a
local.get $b
;; check if overflow occurred (Cranelift uses uadd_overflow_trap or equivalent)
i32.gt_s
if
  unreachable    ;; panic!("attempt to add with overflow")
end
local.get $result

In release mode, rustc omits the check and emits a bare i32.add. The programmer can opt into explicit wrapping via i32::wrapping_add(), which always emits a bare i32.add regardless of build profile.

The Rust standard library also provides i32::checked_add() (returns Option<i32>) and i32::saturating_add() (clamps to the boundary), all of which lower to distinct WASM instruction sequences.

Clang / LLVM to WASM

C's undefined behavior for signed overflow is an optimizer license. When Clang targets WASM with -O2 or higher, the optimizer may hoist, fold, or eliminate computations on the assumption that signed overflow never occurs. The resulting WASM still wraps at runtime — but the sequence of WASM instructions may not correspond to what the C source code appears to request, because the optimizer has transformed it under the UB assumption.

Unsigned overflow in C is defined wrapping, so Clang emits bare WASM arithmetic for unsigned types at all optimization levels.

-fwrapv disables the optimizer's signed overflow assumption, making both signed and unsigned arithmetic lower to bare WASM arithmetic instructions without transformation.

Zig to WASM

In Zig's safe build mode (-ODebug or -OSafeRelease), every integer arithmetic operation is accompanied by an overflow check. The check is a @addWithOverflow intrinsic that returns a struct of {value, overflow_flag}. If the overflow flag is set, Zig calls its panic handler, which in a WASM context emits unreachable. In unsafe mode (-OReleaseSmall, -OReleaseFast), bare WASM arithmetic is emitted. Zig also provides explicit wrapping operators (+%, -%, *%) that unconditionally emit bare WASM arithmetic, mirroring Rust's wrapping_add pattern.

Formal Verification Implications

Overflow behavior is not optional context for formal verification — it is a load-bearing assumption in every arithmetic proof.

Modeling Integer Arithmetic in Coq

Coq's standard library provides Coq.ZArith.BinInt for arbitrary-precision integers (Z) and Coq.NArith.BinNat for natural numbers (N). These are unbounded and do not model machine overflow. To reason about WASM arithmetic, the Rocq translator must encode the modular arithmetic explicitly.

CompCert's Integers.v provides a battle-tested model for this. It defines machine integer types as records containing a value field bounded by the bit width, with all arithmetic operations defined as mathematical operations followed by unsigned z mod (2^wordsize). The key lemma is:

Lemma add_unsigned: forall x y,
  add x y = repr (unsigned x + unsigned y).

where repr n = n mod 2^wordsize. This is the Coq encoding of WASM's wrap-on-overflow guarantee.

For Inference's WASM-to-Rocq translation, every i32.add in the WASM binary must be translated to Int32.add (or equivalent), which encodes the modular semantics. A translation that maps i32.add to Coq's Z.add would be unsound — it would allow the proof to assume no overflow when the runtime behavior does wrap.

Proof Obligations for Overflow-Free Code

When writing a Rocq proof about Inference code, the user must either:

1. Prove that no overflow can occur (typically by establishing bounds on inputs), or
2. Account for wrapping in the proof (the result is defined, so the proof is possible, but it may be unexpected).

Option 1 is more common. A function that receives an i32 parameter and returns param + 1 requires the user to prove that the input is less than i32::MAX before the proof obligation result == input + 1 can be discharged over integers. If that precondition is missing, the proof must instead discharge result == (input + 1) mod 2^32, which is a different and weaker claim about the function's behavior.

Overflow Checks as Proof Obligations

A future direction for Inference is to treat compile-time overflow checks not as inserted runtime traps but as proof obligations discharged by the verifier. Under this model:

• In compile mode, the compiler emits bare WASM arithmetic (no checks, maximum performance).
• In proof mode, each arithmetic operation generates a Rocq proof obligation: "the inputs to this operation are within bounds."
• The programmer discharges the obligation via a proof or by establishing sufficient preconditions in the function's spec block.

This would make Inference's overflow handling fundamentally different from Rust's or Zig's: rather than inserting a runtime guard that might or might not be reached, the verifier would guarantee at proof time that the guard is never needed.

Current Implementation Details

All arithmetic lowering is in core/wasm-codegen/src/compiler.rs.

lower_binary_expression dispatches on the left operand's TypeInfoKind using is_i64_type() and is_unsigned_type(), then emits a single WASM instruction with no surrounding guards:

#![allow(unused)]
fn main() {
OperatorKind::Add => {
    if is_i64 { Instruction::I64Add } else { Instruction::I32Add }
}
}

lower_prefix_unary_expression handles negation as 0 - x:

#![allow(unused)]
fn main() {
UnaryOperatorKind::Neg => {
    // emit 0 constant (i32 or i64 depending on type)
    // lower the operand expression
    // emit Sub
}
}

lower_number_literal uses .cast_signed() for unsigned types to perform bit-pattern reinterpretation without value conversion:

#![allow(unused)]
fn main() {
// u32: parse bits as u32, reinterpret as i32 for WASM storage
let val = number_literal.value.parse::<u32>()
    .expect("Failed to parse unsigned 32-bit integer literal")
    .cast_signed();
func.instruction(&Instruction::I32Const(val));
}

The test suite for overflow behavior is in tests/src/codegen/wasm/arith_overflow.rs. It covers eight cases: i32::MAX + 1, i32::MIN - 1, i64::MAX + 1, i64::MIN - 1, u32::MAX + 1, i32::MAX * 2, -i32::MIN, and -i64::MIN. Each case is verified against a golden WAT file and executed via Wasmtime to confirm the wrapping result at runtime.

Future Considerations

Checked Arithmetic Mode

Inference could add a compiler flag (e.g., --overflow=trap) that inserts an overflow check before every arithmetic operation in compile mode, identical to what Rust does in debug mode. The check sequence for a + b would be:

;; overflow check for i32.add
local.get $a
local.get $b
i32.add
local.tee $result
local.get $a
local.get $b
;; detect overflow: if (a > 0 && b > i32::MAX - a) || (a < 0 && b < i32::MIN - a)
;; ... conditional unreachable ...
local.get $result

This mode would be appropriate for development builds. It has a direct cost in code size and throughput, which is why Rust defaults to wrapping in release mode.

Constant Folding and Compile-Time Detection

A constant-folding pass could evaluate constant expressions at compile time and report an error when the result overflows. This does not require runtime guards — it is purely a front-end diagnostic.

The literal case is already closed: analysis rule A022 (Literal out of range) rejects let a: i8 = 200 at compile time, because 200 exceeds i8::MAX (127) and the value could never round-trip through its declared type (see Static Analysis). What remains open is folding computed constants — 127 + 1 assigned to an i8 still wraps silently.

Overflow Checks in Non-Deterministic Blocks

Non-deterministic blocks (forall, exists, unique) operate over all possible execution paths. If overflow checks are added as runtime traps in compile mode, those checks would need to be stripped from spec blocks (which are excluded from compile mode output) but preserved in proof mode. The interaction between overflow check emission and spec-block stripping would need to be specified explicitly.

Sub-i32 Truncation

Sub-i32 truncation after arithmetic is implemented (see Sub-i32 Types above); for i8 addition, the emitted sequence is:

local.get $a     ;; i8 stored as i32
local.get $b     ;; i8 stored as i32
i32.add
i32.const 24     ;; shl/shr_s width for i8
i32.shl
i32.const 24
i32.shr_s        ;; sign-extend from 8 bits without the sign-ext proposal

The last producer that did not follow this convention was the scalar uzumaki (@) draw: the draw opcode always yields a full-width value, so a narrow-typed let x: i8 = @; previously left the drawn value ranging over all of i32, not just -128..127. emit_uzumaki_domain_constraint (core/wasm-codegen/src/compiler.rs:4196) now closes this by emitting the same mask / shl+shr_s shapes immediately after the draw for i8/u8/i16/u16, plus two constraints outside the sub-i32-integer case: bool gets i32.and 1, and a non-empty enum gets i32.rem_u <variant count> (variant tags are assigned by declaration position, so the range 0..N-1 is always contiguous). A variantless enum draw is left unconstrained — the type is uninhabited, and rem_u 0 would trap.

The same bool/enum constraint is applied to a compound (array/struct) uzumaki leaf before its store (emit_compound_uzumaki_domain_constraint, core/wasm-codegen/src/compiler.rs:4240). A compound narrow-int leaf needs no separate constraint: the element's store8/store16 truncation, combined with the sign- or zero-extending typed load used to read it back, already realizes the domain on every round trip through memory.

This matters specifically for the non-deterministic blocks in Overflow Checks in Non-Deterministic Blocks above: a forall/exists/unique quantifier ranges over every value the draw can produce, so an unconstrained draw of a narrow type made the Rocq-side quantifier range over all 2^32 bit patterns rather than the declared type's actual value set — a soundness gap for exactly the constructs this document's proof-obligation sections depend on. Every mapping above is surjective onto the target domain, so quantifying over the raw draw and then mapping is equivalent to quantifying over the domain directly.

Unreachable Emission in Codegen

The Inference compiler emits a WebAssembly unreachable instruction before the end of every non-void function body. This document explains why, how other compilers handle the same problem, and why the alternatives are worse.

The Problem

WebAssembly is a stack-typed bytecode format. When a function declares a return type, the WASM validator requires a matching value on the stack at the function's end instruction. Consider a function where all control-flow paths exit via explicit return:

(func $if_else_branch (param $x i32) (result i32)
  local.get $x
  i32.const 0
  i32.gt_s
  if
    i32.const 1
    return
  else
    i32.const 0
    return
  end
  ;; <-- nothing on the stack here, but validator expects i32
)

Both arms return, so the code after end of the if block is dead. But the WASM validator does not perform control-flow analysis — it checks the stack type at every reachable textual position. Without something to satisfy the type at function end, the module fails validation.

The Solution

Emit unreachable before the function's end:

(func $if_else_branch (param $x i32) (result i32)
  local.get $x
  i32.const 0
  i32.gt_s
  if
    i32.const 1
    return
  else
    i32.const 0
    return
  end
  unreachable   ;; makes stack polymorphic — satisfies any return type
)

The unreachable instruction is stack-polymorphic per the WASM specification: after it, the stack matches any type signature. The validation algorithm enters a polymorphic state where the required return type is trivially satisfied.

When the program is correct (all paths return), the unreachable is dead code and never executes. When the program has a bug (a path falls through without returning), the unreachable traps at runtime — a fail-fast behavior that prevents silent wrong results.

For void functions (unit return type), no value is expected on the stack at end, so the unreachable is omitted.

WASM Specification Rationale

WebAssembly design issue #998 explains why unreachable makes the stack polymorphic:

There is no control edge from unconditional control transfer instructions (br, br_table, return, unreachable) to the following instruction, so no constraint needs to be imposed between them regarding the stack.

The specification deliberately supports this pattern because "disallowing unreachable code would be problematic for producers." The unreachable instruction exists precisely to let compilers satisfy validation in dead code positions. See also design issue #1379 for further discussion of unreachable state typing.

How the Validation Algorithm Works

The validation algorithm maintains a control stack and an operand stack. Each frame tracks an unreachable boolean. When unreachable is visited:

1. The frame's unreachable flag is set to true
2. The operand stack is truncated to the frame's height

After this, any attempt to pop an operand from the stack returns Bottom — a special type that matches any expected type. When the function's end instruction is reached, the validator pops each result type; in a polymorphic frame, each pop trivially succeeds via Bottom. This works for zero, one, or multiple return values.

The same mechanism is used by all unconditional control transfers (br, return, br_table, throw). Stack polymorphism is a fundamental design property of the WASM type system, not an incidental feature.

Compatibility with WASM proposals

No current or proposed WASM extension changes how unreachable interacts with function-end validation:

The polymorphic stack mechanism is so fundamental that no proposal can break it without redesigning the entire type system. The WASM Community Group has explicitly stated that "disallowing unreachable code would be problematic for producers."

How Production Compilers Handle This

rustc (Rust)

Rust enforces exhaustive returns through its type system (the ! / never type and exhaustive match checking) and still emits trap/unreachable instructions in codegen as a safety net.

MIR to codegen. When MIR contains TerminatorKind::Unreachable, the LLVM backend emits llvm.unreachable and the Cranelift backend emits trap(TrapCode::user(1)) with the block marked cold.

TrapUnreachable. PR #45920 enabled LLVM's TrapUnreachable flag, converting unreachable IR into hardware trap instructions (ud2 on x86, unreachable on WASM). Code-size impact was measured at 0.0%–0.1%. The flag defaults to true for all targets including wasm32-unknown-unknown — WASM targets do not override it.

Security motivation. The PR was motivated by issue #28728: LLVM removed an infinite loop (optimizing "must progress" assumption), causing code to fall through to a match with no arms, executing arbitrary memory. TrapUnreachable converts this from silent corruption to a deterministic trap.

Intentional design. In issue #52998, the Rust team confirmed this is intentional: "This behaviour is very much intended" (Nagisa, compiler team). hanna-kruppe clarified: "It's a hardening measure, not something ensuring soundness." PR #88826, which proposed turning TrapUnreachable off, was closed without merging — consensus: keep it on.

All-paths-return enforcement. Rust checks this in the type checker (rustc_hir_typeck), using the Diverges enum to track whether code paths converge or diverge. The CoerceMany collector gathers return types and demands the final LUB coerces to the declared return type. This is front-end checking, orthogonal to the codegen safety net.

The pattern is: front-end enforces all-paths-return, codegen emits trap as defense-in-depth.

LLVM / Clang (C/C++)

Clang emits @llvm.trap() (debug builds) or unreachable (optimized builds) at the end of non-void functions that may fall through. LLVM issue #75797 discusses this extensively. A real-world vulnerability (CVE-2014-9296 in OpenSSL) demonstrated how a missing return value can be exploited when the compiler optimizes the undefined behavior path.

WASM target specifically. LLVM forces --trap-unreachable=1 and --no-trap-after-noreturn=0 for all WASM targets. These flags are forced even if the user explicitly passes different values. Both @llvm.trap() and LLVM IR unreachable lower to the same WASM unreachable opcode. The LLVM WASM backend handles unreachable in its assembler type checker (LLVM review D112953).

The active debate in the LLVM community is not about whether to emit traps, but about whether optimized builds should use unreachable (which the optimizer can exploit as UB) or @llvm.trap() (which always traps). On WASM, this distinction is moot — there is only one trapping instruction.

GCC

GCC uses __builtin_unreachable() to mark code paths that should never execute. The -funreachable-traps flag (enabled by default at -O0/-Og) converts __builtin_unreachable to a trap instruction. A 2025 patch strengthens this by converting standalone __builtin_unreachable to __builtin_trap even at higher optimization levels.

Without __builtin_unreachable, GCC issues -Wreturn-type: "control reaches the end of a non-void function." The GCC documentation describes this as intended for "situations where the compiler cannot deduce the unreachability of the code."

Zig

Zig's self-hosted WASM backend (src/codegen/wasm/CodeGen.zig, line 1242-1248) uses the exact same pattern:

In case we have a return value, but the last instruction is a noreturn (such as a while loop) we emit an unreachable instruction to tell the stack validator that part will never be reached.

All three of Zig's airTrap, airBreakpoint, and airUnreachable emit the same WASM unreachable opcode — there is no distinction on WASM targets. Zig also emits unreachable in the implicit else path of if-without-else (line 4087).

Binaryen

Binaryen (the WebAssembly optimizer/toolchain library) explicitly emits unreachable opcodes after constructs that make subsequent code dead. From issue #1056:

Binaryen IR has an unreachable type for loops, but wasm binaries do not. To fix that, after it emits a loop that is unreachable it also emits an unreachable opcode, which ensures we are in an unreachable zone in the binary.

Binaryen's dead code elimination pass can remove instructions that precede unreachable but does NOT remove the unreachable instruction itself — it serves as the dead code marker. The wasm-snip tool uses unreachable as a canonical "removed function" placeholder.

Formal Verification Perspective

Mechanised proofs

Conrad Watt's mechanised WASM specification (CPP 2018) provides a fully mechanised Isabelle specification of WASM 1.0 with a verified executable interpreter and type checker. The soundness proof of the WebAssembly type system was mechanised end-to-end. This directly validates that unreachable's stack-polymorphic typing is sound — placing unreachable in any context is guaranteed to pass validation regardless of the expected stack type.

"A Type System with Subtyping for WebAssembly's Stack Polymorphism" (ICTAC 2022) by McDermott, Morita, and Uustalu formalises the two flavors of stack polymorphism in Agda, proving that every typable instruction sequence has a principal type.

Iris-Wasm (PLDI 2023) provides a mechanised higher-order separation logic for WASM built on Coq and Iris. In this framework, trapping instructions correspond to false preconditions, making them trivially verifiable.

CompCert analogy

CompCert (the formally verified C compiler) handles unreachable code through "stuck states" — when the reference interpreter encounters undefined behavior, execution gets stuck. CompCert's correctness theorem only covers defined-behavior paths. For Inference, which targets formal verification via Rocq translation, the unreachable instruction makes the "stuck" explicit and deterministic rather than silent.

Impact on WASM-to-Rocq translation

The unreachable instruction at function boundaries provides a clear semantic for the Rocq translator: "this path is impossible; any proof obligation here is vacuously true" (analogous to False_rect in Coq). This is beneficial for formal verification — it creates an explicit proof obligation rather than silently accepting potentially incorrect behavior.

Why the Alternatives Are Worse

Emit a default return value (e.g., i32.const 0)

If a front-end bug allows a missing return and this code executes, silently returning zero is more dangerous than trapping. The unreachable approach is strictly safer because it fails fast. This also uses more bytes (2+ bytes for i32.const 0 vs 1 byte for unreachable). WebAssembly design issue #448 explicitly states this concern: "the producer would have to materialize a bogus return value just to make the type check pass."

Only emit unreachable when control-flow analysis proves the end is unreachable

This adds a whole analysis pass to eliminate a single harmless instruction. The unreachable is dead code when the program is correct, and a trap when it is not — both are correct behaviors. Control-flow analysis is valuable for compile-time diagnostics (catching missing returns as errors), but it should not gate whether codegen emits a safety net.

Rely solely on front-end checking (no codegen safety net)

No production compiler does this. Every compiler listed above enforces returns in the front-end and emits traps in codegen. Rust's issue #28728 demonstrated why: LLVM removed an infinite loop, code fell through to a match with no arms, executing random memory. Defense-in-depth is standard practice for safety-critical toolchains.

Cost Analysis

Security Context

CERT C Coding Standard, rule MSC37-C: "Ensure that control never reaches the end of a non-void function." This standard documents how flowing off the end of a non-void function has caused real vulnerabilities. Emitting unreachable converts this from "undefined behavior" to "deterministic trap."

WebAssembly provides inherent control-flow integrity: all functions and their types are declared at load time, compiled code is immutable, and structured control flow prevents arbitrary jumps. The unreachable instruction complements this by ensuring that if execution reaches an impossible point, a deterministic trap occurs rather than silent corruption.

Inference's Approach

Inference follows the same layered strategy as rustc, LLVM, GCC, Zig, and Binaryen:

1. Front-end: The core/analysis/ crate enforces that all non-void functions return on every code path — rule A007 (Missing return) produces a compile-time error for violations (see Static Analysis).
2. Codegen: The unreachable instruction before function end serves as a safety net. If the front-end has a bug, the program traps instead of silently misbehaving.

Compilation Targets

Compilation Matrix

non_det_operations = { spec, uzumaki, forall_block, assume_block, exists_block, unique_block }

compile mode produces a .wasm binary (executable or library). proof mode produces a .v Rocq file (via wasm_to_v). Non-deterministic operations can only appear inside spec blocks. In compile mode, spec nodes are stripped (they have no runtime meaning). In proof mode, all code including spec blocks is emitted.

compile mode: Produces production binaries. Debug/release profiles control optimization. Non-det spec nodes are stripped from codegen since they have no runtime meaning. The output can be the verification target — the artifact whose behavior is proven correct by Rocq proofs.

proof mode: Emits all code (including spec functions with non-det intrinsics) into a single WASM module for wasm_to_v Rocq translation. Only spec functions (those containing non_det_operations) receive optnone+noinline barriers to preserve 1:1 structural correspondence with the source code — this ensures Rocq readability. Execution functions are compiled at the target's default release optimization, identical to compile mode release, so that Rocq proofs cover the actual deployed code. If the source has no non_det_operations, proof mode output is identical to compile mode release output (Option 5 = Option 2). The target is always Wasm32 (custom intrinsics require strict MVP). Build profiles (debug/release) do not apply to proof mode — execution always uses release optimization, spec always uses O0 + barriers.

The contract between the generated .wasm binary, the per-spec function index map carried alongside (or embedded as the inference.spec_funcs custom section), and the Rocq predicates the generated .v file depends on is documented in core/wasm-to-v/ROCQ_CONTRACT.md.

Selecting a mode at the CLI

Pass --mode {compile,proof} to either CLI: infs build path/to/file.inf --mode proof or infc path/to/file.inf --mode proof. Equivalently, infc -v (emit Rocq) implies --mode proof unless --mode compile is also passed; mirror-rule: --mode proof implies -v. Without either flag, the default is compile mode.

For project-aware builds — Inference.toml, project discovery, and the infs build/run workflow that resolves a mode from the manifest — see Projects and the infs Toolchain.

Verification Scenario: External Module Linking

Inference verifies the final artifact — the deployed WASM module. This module can be:

1. Produced by infc from .inf source code (compile mode, spec stripped)
2. A WASM module built elsewhere (e.g., a Rust cryptographic library compiled to WASM)

In the linking scenario, a user:

1. Compiles their library to WASM (e.g., my_crypto.wasm from Rust)
2. Writes an .inf specification that imports external functions from the module
3. Writes spec blocks with assertions: assert(my_crypto_function(input) == 0)
4. infc in proof mode links the external module with the compiled spec into a unified WASM module
5. The unified module is translated to Rocq (.v) by wasm_to_v
6. The user writes Rocq proofs establishing properties about the external function's behavior

The external artifact remains as-is (potentially fully optimized). The spec code requires structural identity for Rocq readability. Execution code — whether from Inference source or external modules — is compiled at the target's default release optimization so that Rocq proofs cover the actual deployed artifact. Only spec functions receive optnone+noinline barriers; execution functions are optimized normally.

The language-level constructs that import external functions (external fn, use … from) are documented in External Functions and WASM Linking; the static merge that folds them into the verified artifact — feasibility tiers and the Tier-B provenance proof — in The WASM Linker.

Targets

Target parameters are locked per target variant and cannot be overridden in Inference.toml. The only user-facing configuration is target selection and build profile (debug/release) for compile mode.

Target::Wasm32 (default)

General-purpose WASM target with custom non-deterministic instruction support for specs. Used in both compile and proof modes. WebAssembly is generated directly via wasm-encoder. Purpose: general WASM execution and verification of Inference code.

Stellar Soroban

Produces Soroban-compatible WASM binaries matching the wasm32v1-none Rust target configuration. The target's default optimization applies (-Oz for Soroban, -O3 for Wasm32). Purpose: deploy to Stellar network as Soroban smart contracts.

Soroban VM WASM feature matrix (from rs-soroban-env wasmi config):

Soroban target flags

• --no-entry — reactor model, no _start (same as Wasm32)
• --export-dynamic — export all symbols with default visibility (Soroban host discovers exports by name)
• --gc-sections — strip unreachable code (critical for 64KB limit)
• -z stack-size=1048576 — 1MB stack (Soroban default)
• --stack-first — place stack before data in linear memory (Soroban convention)

Appendix A: Optimization Levels

Appendix B: WebAssembly Features

Module Hierarchy & Multi-File Compilation

This chapter explains how Inference distributes source code across multiple .inf files and flattens the whole program into a single self-contained WebAssembly module and a single Rocq .v file. It covers the file-as-module model, the two forms of the use directive, the import-closure walk, cross-file type identity, WASM function naming, and the implications for formal verification.

Why Multiple Files?

A language that restricts all code to a single file does not scale to real programs. As a codebase grows, a single-file constraint forces either monolithic structures or custom tooling to concatenate sources before compilation — neither is acceptable.

At the same time, Inference has a hard constraint inherited from its verification architecture: the Rocq output must be one self-contained .v file. The proof assistant reasons about the whole program simultaneously; splitting the proof into separate modules would require constructing cross-module proof obligations, a significant increase in complexity for proof authors. The same argument applies to the WebAssembly side: a self-contained .wasm with no outstanding imports is simpler to verify and deploy than a bundle of linked modules.

The design goal is therefore: code organisation without losing whole-program compilation or verification. Multiple source files map to one output module.

File-Based Modules

Each .inf file is a module. The module tree mirrors the directory tree under the source root. The source root is the directory that contains the entry file — the file named on the infc or infs command line.

The module's canonical path is the list of path segments from the source root to the file, without the .inf extension:

source root: src/

  src/main.inf        →  module path: []          (the entry; empty)
  src/util.inf        →  module path: ["util"]
  src/lib/arith.inf   →  module path: ["lib", "arith"]
  src/lib/geo.inf     →  module path: ["lib", "geo"]

The entry file always has the empty path. Its items keep unqualified names throughout the compilation pipeline, so a single-file program produces byte-identical output to a multi-file one where the entire code lives in the entry file.

The Two Forms of use

The use directive has two syntactically distinct forms. They are easy to confuse but serve entirely different purposes.

Path-form use — source imports

The path form names a sibling .inf file to include in the compilation:

use util;
use lib::arith;
use lib::geo::{Point};

• use util; makes the file <root>/util.inf part of the compilation. Items in that file are accessed as util::helper().
• use lib::arith; names <root>/lib/arith.inf. Items are accessed as lib::arith::add(1, 2).
• use lib::geo::{Point}; names the same file <root>/lib/geo.inf as the brace-free form. The braces select which items are accessible without the full path, but the file imported is identical: a braced item import and its brace-free equivalent are both resolved to the same file and both pull that file into the compilation closure.

use root; is a reserved handle that refers to the entry file itself; a literal src/root.inf on disk is shadowed by the reserved name.

Glob imports (use lib::arith::*;) are not supported and produce a diagnostic.

From-form use — external WASM imports

The from form binds an external fn declaration to a pre-compiled .wasm library:

external fn sort(ptr: i32, len: i32);
use { sort } from collections;

This form is not a source import. It names a logical WASM module identifier, not a file path. The compiler-time front end (core/project-model/src/project.rs) skips it entirely when walking the import closure. The from form is resolved at link time by inference-wasm-linker.

The distinction is crisp: if the directive contains from, it is an external WASM binding; otherwise it is a source file import. The two forms do not interact, and mixing them in one file is valid:

use lib::arith::{add};          // source import: lib/arith.inf
use { sort } from collections;  // external WASM: resolved at link time

The from form is documented in detail in External Functions and WASM Linking and The WASM Linker.

Qualified Access with ::

Items from an imported file are accessed through the :: path operator. The path is the module's canonical path with :: as the separator:

use util;
use lib::arith;
use lib::geo::{Point};

pub fn run() -> i32 {
    let p: Point = Point::at(8);  // constructor from lib::geo
    return util::helper();        // free function from util
}

The math::arith::add(1, 2) form works transitively through re-exports (see Re-exports below).

When use lib::geo::{Point}; brings a name into scope without a path prefix, the type name is available unqualified, but the calling convention stays the same:

use lib::geo::{Point};

pub fn run() -> i32 {
    let p: Point = Point::at(8);  // `Point` unqualified; `Point::at` still uses `::`
    return p.dist();
}

The fixture in tests/test_data/codegen/wasm/multi_file_golden/method_mangling/src/ demonstrates this pattern: main.inf imports {Point} from lib::geo and calls Point::at(8) and p.dist().

Visibility

Items are private by default. The pub keyword makes an item accessible from other files:

// lib/arith.inf — private fn is invisible outside this file
fn internal_helper(x: i32) -> i32 { return x * 2; }

// pub fn is accessible as lib::arith::add
pub fn add(a: i32, b: i32) -> i32 { return a + b; }

// pub struct is accessible as lib::arith::Point
pub struct Point {
    x: i32;    // fields inherit the struct's visibility; no per-field modifier
    y: i32;
}

Visibility rules:

• A file's own private items are visible everywhere within that file.
• Cross-file access requires pub.
• Struct fields inherit the struct's visibility. There is no per-field pub modifier.
• external fn declarations are always file-local; they cannot be re-exported or accessed from other files.
• Spec blocks see their own file's private items, but when a spec in file A references a type or function from file B, only pub items in B are in scope.
• WASM exports: only pub fns defined in the entry file are exported from the generated WASM module. A pub fn in an imported file has intra-project visibility — the function is compiled and callable within the program, but it does not appear in the WASM export section. This keeps the module's public ABI explicitly controlled.

Re-exports

A pub use directive re-exports a module path, making it accessible through the re-exporting file's namespace:

// math.inf
pub use lib::arith;

Callers that import math can then reach lib::arith's items through the math namespace:

// main.inf
use math;

pub fn run() -> i32 {
    return math::arith::add(1, 2);
}

The fixture in tests/test_data/codegen/wasm/multi_file_golden/re_export_chain/src/ demonstrates this: math.inf re-exports lib::arith with pub use lib::arith;, and main.inf calls math::arith::add(1, 2).

Re-exports also drive the import closure: if math.inf carries pub use lib::arith;, the compiler includes lib/arith.inf in the compilation even though main.inf names only math. Both pub use and plain use pull the named file into the closure; visibility affects name accessibility, not discovery.

Re-export chains can be arbitrarily deep. Circular re-exports between files are permitted and terminate correctly (see Import-Closure Walk below).

Cross-File Type Identity

Two different files may each define a struct or enum with the same bare name:

// main.inf
pub struct Pair {
    a: i32;
    b: i32;
}

// lib/shapes.inf
pub struct Pair {
    a: i64;
    b: i32;
}

These are distinct types. The type checker keys each type by its canonical type key — the :: path of its defining file prefixed onto the bare name:

Pair  defined in the entry file → canonical key:  "Pair"
Pair  defined in lib/shapes.inf → canonical key:  "lib::shapes::Pair"

This key is computed from the type's defining scope (not the call site's scope) and threads consistently through every phase: the type checker uses it for identity comparisons and layout lookups; codegen uses the same derivation to key memory layout and frame-slot allocations. Two files may therefore define identically-named structs with completely different field layouts, and the compiler keeps them distinct without any source-level disambiguation.

The fixture in tests/test_data/codegen/wasm/multi_file_golden/dup_struct/src/ exercises this: both main.inf and lib/shapes.inf define struct Pair, but with different field types. The codegen produces correct, separate frame layouts for each, and the type checker rejects any attempt to use one where the other is expected.

Import-Closure Walk

The compiler resolves the full set of files to compile through a breadth-first walk from the entry file. This walk is implemented in core/project-model/src/project.rs — a leaf crate (inference-project-model) extracted from the orchestration crate so that the batch compiler and the language server share one closure walk. The compiler enters it through inference::parse_project (re-exported unchanged), while the IDE enters through load_project_resilient, which reads files through a FileLoader seam so the editor's unsaved buffers take priority over what is on disk.

The algorithm:

1. Start with the entry file (module path []) in the visited set and in the work queue.
2. Parse the front of the queue.
3. Extract all path-form use directives (from-form use directives are skipped).
4. For each named module path not already in the visited set, compute the corresponding filesystem path (<root>/a/b.inf for ["a", "b"]), verify the file exists, add it to the visited set, and enqueue it.
5. Repeat until the queue is empty.

Properties of the walk:

• Import cycles terminate. The visited set is keyed by canonical module path, so a file reached by two different import chains is parsed once. A file that imports itself, or two files that import each other, is handled correctly.
• All paths are src-root-relative. A use lib::arith; directive written inside deep/inner.inf resolves to <root>/lib/arith.inf, not to <root>/deep/lib/arith.inf. All imports are relative to the one shared source root, not to the importer's location.
• Unreachable files warn. After the walk, the compiler scans every .inf file under the source root and emits a ProjectWarning::UnreachableFile for each file not reached by any import chain. The build still succeeds; the warning is advisory.

After discovery, the files are lowered into a single AstArena in canonical order: the entry file first, then all imported files sorted lexicographically by module path. This ordering is independent of discovery order (which is BFS and depends on the order use directives appear in source). A project with the same files and the same code produces the same canonical order regardless of which use comes first in any given file.

entry: []
imports (lexicographic):
  ["lib", "arith"]
  ["lib", "geo"]
  ["math"]
  ["util"]

WASM Codegen and Function Naming

All reachable files are flattened into one WASM module. The FnKey abstraction (core/fn-key/src/lib.rs) provides a structured identity for every function across the whole program, used by both codegen (to assign WASM function indices) and analysis (to build the call graph). The four variants of FnKey are:

Every variant carries the module_path of the defining file. This is what keeps two fn add functions in two different files as distinct internal keys.

The function names written into the WASM name section (and visible in .wat output) use the bare function name (or StructName.method_name for methods), not a file-prefixed form. When two functions share a bare name across files, the WAT renderer deduplicates them with a numbered suffix like #func2 there_b. The FnKey dot-qualified string (lib.arith.add) is an internal key used for function-index lookup — it does not appear verbatim in the binary's name section.

WASM exports are controlled by the entry file and by visibility. The rule:

• Only a pub fn defined in the entry file becomes a WASM export.
• A pub fn in an imported file is compiled and callable within the program, but is not exported from the WASM module.
• Methods and spec-inner functions are never exported.

This makes the module's external ABI explicit: whatever the entry file declares pub is the interface; imported library code is internal.

;; root_only_export example: lib::arith::add is compiled but not exported
(module $output
  (export "run" (func $run))   ;; only the entry-file pub fn is exported
  (func $run ...)
  (func $add ...)              ;; add is compiled but unexported
)

Specs in Multi-File Proofs

Spec blocks carry their own names in the Rocq output. When a spec is defined in a non-entry file, its name is file-qualified by joining the module path with underscores, then prepending to the bare spec name. This is done by the fold_spec_name function (core/fn-key/src/lib.rs):

module path: ["lib", "checks"]
spec name: "LibSpec"
folded name: "lib_checks_LibSpec"

The entry file's specs keep their bare names (the empty module path folds to nothing).

The fold uses underscores rather than dots because the result must be a legal Rocq identifier. The fold is intentionally non-injective: the paths ["lib", "checks"] and ["lib_checks"] both fold to the same prefix lib_checks. The FnKey type keeps the module path and the bare spec name structurally separate (not pre-folded) to preserve injectivity as an internal key; the fold is applied only at rendering time.

The fixture in tests/test_data/codegen/wasm/multi_file_golden/proof_specs/src/ illustrates this:

// lib/checks.inf
fn lib_value() -> i32 {
    return 2;
}

spec LibSpec {
    fn obligation() forall {
        assert(lib_value() == 2);
    }
}

// main.inf
use lib::checks;

fn entry_value() -> i32 {
    return 1;
}

spec EntrySpec {
    fn obligation() forall {
        assert(entry_value() == 1);
    }
}

The computing helpers sit at file scope rather than inside the spec block: a specification function must state a property, and one whose body only computes yields an obligation any proof discharges without reading the program, which code generation rejects as P010. A specification function still applies a file-scope function as a T_app, so the helper loses nothing by moving out.

EntrySpec (entry file, empty path) keeps its name in the Rocq output; LibSpec (defined in lib/checks.inf) is rendered as lib_checks_LibSpec.

A file-qualified spec name must remain a valid Rocq identifier after folding. In particular, a file stem or spec name that contains a __ run, or begins or ends with _, can produce a name that conflicts with Rocq's reserved <module>__<spec> separator in the emitted proof grammar. Codegen detects this and reports a CodegenError::SpecNameReservesSeparator with a rename suggestion before emitting any output. This restriction applies to spec names in proof mode; it is not a restriction on file names used by import directives.

Current Limitations

• No import aliasing. use lib::arith as ar; is not supported. The module must be accessed through its canonical path.
• No per-field visibility. Struct fields inherit the struct's pub or private visibility. There is no pub modifier on individual fields.
• Circular const/type-alias value initialization is an error. Import cycles between files are legal and handled correctly, but circular value initialization — a constant whose value depends (through a chain of constants or type aliases) on itself — is rejected with a CircularDefinition error.
• Bare infc src/main.inf treats src/ as the source root. In this mode, sibling .inf files under src/ that are not reachable from main.inf produce unreachable warnings. The infs project toolchain (see Projects and the infs Toolchain) handles project-level discovery and build coordination.

Comparison with Other Languages

The Inference model is closer to Zig than to Rust: files are modules implicitly, without explicit mod declarations, and import cycles are allowed. Inference differs from both in that all files flatten into one compilation unit; there is no concept of separate crates or build artifacts for sub-libraries within a project.

Formal Implications

The whole-program flattening has a direct consequence for formal verification: every function the proof references is defined in the same .v file. There are no cross-module lemma imports, no proof namespace hierarchies, and no linker-time proof composition. A proof obligation on main::run can refer directly to lib::arith::add's definition without any module-qualification syntax in the Rocq source.

The canonical per-file type identity ensures soundness across the flattening: two same-named structs from two different files carry distinct canonical keys through the type-checker, layout computation, and codegen. A Rocq proof that reasons about one struct cannot inadvertently apply to the other, because the generated .v definitions carry different names derived from the canonical keys.

Related Resources

• core/project-model/src/project.rs — parse_project, load_project_resilient, the import-closure walk, collect_unreachable_warnings
• core/fn-key/src/lib.rs — FnKey variants, fold_spec_name, qualify_dotted
• core/type-checker/src/symbol_table.rs — canonical_key_for_scope, file_module_path_of_scope
• core/ast/src/nodes.rs — Visibility, UseDirective
• tests/test_data/codegen/wasm/multi_file_golden/ — golden fixture files for all multi-file scenarios: two_file, item_import, method_mangling, re_export_chain, dup_struct, cross_file_struct, proof_specs, root_only_export
• External Functions and WASM Linking — the from form of use, external WASM binding, and the link step
• The WASM Linker — merge algorithm for pre-compiled .wasm dependencies
• Projects and the infs Toolchain — project-aware build and the infs CLI
• Compilation Targets — compile vs. proof modes and the supported backends

Projects & the infs Toolchain

Motivation

infc is a single-file compiler. Given one .inf source file it parses, type-checks, analyses, and emits a WASM binary. That model is fine for self-contained examples, but real codebases need more: a place to declare external .wasm dependencies, a way to express whether a build is meant to produce an executable or a Rocq proof, and a project root that tools can agree on so artifacts land in predictable locations.

infs is the unified toolchain entry point that provides all of this. It discovers a project, reads its manifest, resolves the configuration, and spawns infc with the right arguments and working directory. The split is deliberate: infc stays a pure compiler that knows nothing about project structure; infs is the orchestrator that wraps it.

Project Layout

infs new myproject scaffolds the following structure:

myproject/
+-- Inference.toml       # manifest
+-- src/
|   +-- main.inf         # entry point (project mode always compiles this)
+-- out/                 # created by the first build (gitignored)
|   +-- main.wasm
+-- tests/
|   +-- .gitkeep
+-- proofs/              # proof-mode artifacts land here by default
|   +-- .gitkeep
+-- .gitignore

The layout mirrors Cargo's conventions: manifest at the root, sources under src/, build outputs under out/. The out/ directory is not committed; it is created automatically by infc (relative to its working directory, which infs sets to the project root). proofs/ is tracked via .gitkeep so that curated hand-authored proof sources stay in version control even when generated .wasm/.v artifacts are gitignored by extension.

The Manifest (Inference.toml)

Inference.toml is the project manifest. Only [package] is required; all other sections default if absent.

[package]
name = "myproject"
version = "0.1.0"
infc_version = "0.1.0"

# Optional package fields:
# description = "A brief description"
# authors = ["Name <email@example.com>"]
# license = "MIT"

[build]
# "compile" (default) or "proof"
mode = "compile"
# Post-MVP WebAssembly proposals to opt into; empty (the default) keeps the
# output pure WebAssembly 1.0. Currently supported: "bulk-memory".
# wasm-features = ["bulk-memory"]
# target and optimize are recognized but not yet consumed.

[verification]
# Output directory for proof artifacts (honored only in proof mode).
# Defaults to "proofs/" if this section is omitted.
# output-dir = "proofs/"

[wasm-dependencies]
# Logical module name -> compiled .wasm, resolved relative to this file.
arith = { path = "libs/arith.wasm" }

The fields:

mode is case-sensitive: "Proof" is rejected. The field is validated on load; an invalid value is an immediate error with the allowed set named in the message. The same load-time strictness applies to keys: every fixed-schema table rejects a key it does not recognize, naming the offending key and the fields the table accepts — a misspelled wasm_features fails the build rather than silently shipping a differently-configured artifact. Only [dependencies] and [wasm-dependencies] accept arbitrary keys, because their keys name the dependencies. wasm-features entries are WebAssembly proposal names ("bulk-memory"), not instruction names, and the setting is honored in project builds, single-file builds, and single-file infs run. [wasm-dependencies] entries have the same reach: project build, project run, single-file build, and single-file run all forward every declared entry to infc. See apps/infs/docs/inference-toml.md for the full reference.

Reserved Project Names

Project names must start with a letter or underscore and contain only alphanumeric characters, underscores, or hyphens. Names that match Inference language keywords or conventional directory names are reserved and rejected (case-insensitively). The reserved set includes: fn, let, mut, if, else, match, return, type, struct, impl, trait, pub, use, mod, ndet, assume, assert, forall, exists, spec, requires, ensures, invariant, const, enum, loop, break, continue, external, unique; and the directory names src, out, target, proofs, tests, self, super, crate.

Real Manifest Examples

From scratch/raytracing-in-one-weekend/Inference.toml (single WASM dependency):

[package]
name = "raytracing-in-one-weekend"
version = "0.1.0"
infc_version = "0.1.0"

[wasm-dependencies]
fixmath = { path = "libs/fixmath.wasm" }

From scratch/linker-e2e/Inference.toml (multiple dependencies):

[package]
name = "linker-e2e"
version = "0.1.0"
infc_version = "0.1.0"

[wasm-dependencies]
arith = { path = "libs/arith.wasm" }
memlib = { path = "libs/memlib.wasm" }
sortlib = { path = "libs/sortlib.wasm" }

Neither example sets [build] or [verification] — those sections are omitted when all values are at their defaults.

Project Discovery

When infs build or infs run receives no path argument, it walks up the directory tree from the current working directory looking for Inference.toml. The nearest ancestor containing the file wins — the same convention Cargo uses, so a nested project's manifest shadows an outer one. The walk stops at the filesystem root; if no manifest is found, the command errors with a remediation message naming infs new and infs init.

After discovery, infc is spawned with its working directory set to the project root. This means out/ always lands at the root regardless of where the command was invoked from inside the project tree, and all source-relative paths in .inf files resolve from the same stable base.

~/projects/myproject/src/utils/
$ infs build           # walks up, finds ~/projects/myproject/Inference.toml
                       # infc CWD = ~/projects/myproject/
                       # artifact  = ~/projects/myproject/out/main.wasm

infs build

infs build has two modes of operation:

infs build                           # project mode: discovers Inference.toml, compiles src/main.inf
infs build path/to/file.inf          # single-file mode: compiles that file directly

Flags:

Mode resolution (precedence, highest first):

1. CLI --mode when present.
2. Manifest [build] mode = "proof" — forwards --mode proof to infc.
3. Manifest [build] mode = "compile" (explicit or defaulted) — forwards nothing, leaving infc's own -v ↔ proof implication intact.

The rule about forwarding nothing for compile mode is deliberate: infc's normalize_args function owns the -v ↔ --mode proof implication as its single source of truth. If infs also forwarded --mode compile it would suppress that implication for users who pass only -v, turning a spec-aware proof build into a spec-stripped one.

--out-dir and [verification] output-dir: in effective proof mode (CLI --mode proof or manifest mode = "proof"), infs reads [verification] output-dir (defaulting to proofs/), normalizes it to a project-relative path, and forwards it to infc as --out-dir. This relocates both .wasm and .v artifacts to that directory. In compile mode, [verification] output-dir is ignored entirely — the compile artifact must always land under out/.

Forwarding --out-dir requires infc ABI ≥ 1.1 (see Relationship to infc below). Using a non-default output-dir with an older infc is a hard error with remediation.

Artifacts per Mode

In single-file mode (infs build path/to/file.inf) the output always goes to out/ relative to infc's inherited CWD (the invoking shell's current directory), with no manifest output-dir forwarded.

infs run

infs run builds and then executes the resulting WASM via wasmtime:

infs run                                 # project mode: build + invoke main
infs run program.inf                     # single-file: compile and invoke main
infs run program.inf --entry-point helper  # single-file: invoke helper()
infs run program.inf -L libs             # single-file: search libs/ for external .wasm

Flags:

In single-file mode, -L and the other options must appear before the first bare trailing token: infs run program.inf -L libs 1 parses -L libs and passes 1 to the invoked function, while infs run program.inf 1 -L libs passes 1 -L libs verbatim as two trailing arguments, parsing no -L at all. Use -- to pass arguments that themselves look like flags.

In project mode (no path given):

• Always builds in compile mode, regardless of [build] mode in the manifest. Proof-mode WASM embeds custom non-deterministic opcodes (0xfc family) that wasmtime cannot execute.
• Always invokes main. Passing --entry-point to anything other than main is rejected with guidance to use single-file mode instead.
• Checks wasmtime availability before starting the build, failing fast if the runtime is absent.
• Resolves the manifest's [wasm-dependencies] and forwards any -L directories the same way project build does, anchored to the invocation directory, so a project binding use { … } from <module> runs without a separate link step.
• out/main.wasm is the expected artifact; if the build succeeds but the file is absent, run errors before invoking wasmtime.

In single-file mode (path given), --entry-point (default main) selects which exported function to invoke. main is called with argc=0, argv=0 automatically; other functions receive the trailing arguments from the command line — anything after the first bare token that options did not consume, or after --. Single-file run also resolves the enclosing manifest's [wasm-dependencies] and forwards any -L directories verbatim: infc inherits the invoking shell's working directory here, so a relative -L already means what it meant at the shell, with no anchoring step needed.

Both modes require wasmtime in PATH. Installation instructions are printed when it is not found.

Scaffolding

infs new <name> creates a new project directory with the layout shown above and optionally initializes a git repository (pass --no-git to skip).

infs init [name] initializes the current directory as a project — it writes Inference.toml and src/main.inf without creating a new parent directory. The name defaults to the current directory's name. If .git/ is present, infs init also creates .gitignore and .gitkeep files without overwriting anything that already exists.

Both commands scaffold src/main.inf with a minimal entry point:

// Entry point for the Inference program

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

Toolchain Management

Project workflow is only half of infs's surface. The other half is a rustup-style toolchain manager — the part that makes "install Inference" a one-command operation and lets several compiler versions coexist:

Toolchains live under INFERENCE_HOME (default ~/.inference), and the release manifest is fetched from the distribution server (overridable via INFS_DIST_SERVER). infs build and infs run resolve the infc they spawn through this installation — the resolution order is described in the next section.

Relationship to infc

infs is a thin orchestrator. It does not link, parse, or type-check anything itself — all of that is infc's responsibility. The relationship:

infs build / infs run (project mode)
    |
    +-- discover_and_load(Inference.toml)
    |
    +-- find_infc_with_source()  # INFC_PATH > sibling of infs > system PATH > managed toolchain
    |
    +-- compatibility handshake
    |       infc --commit-hash    # short-circuit: same-build binaries always compatible
    |                             # sibling tier only: differing commits warn (stale neighbour)
    |       infc --abi-version    # major mismatch → hard error; minor mismatch → warning
    |
    +-- spawn infc
            CWD = <project root>
            arg: src/main.inf
            arg: -v                     (if .v requested; `run` never requests it)
            arg: --mode proof           (if effective proof mode; `run` never requests it)
            arg: --out-dir <dir>        (if effective proof mode + ABI ≥ 1.1; `run` never requests it)
            arg: --wasm-lib-dir <dir>   (one per -L/--wasm-lib-dir; a relative
                                         dir is anchored to the invocation
                                         directory, since infc runs at the root —
                                         `build` and `run` both pass their own
                                         `-L` flags through here)
            arg: --wasm-dep name=path   (one per [wasm-dependencies] entry; the
                                         declared path resolved against the root)
            arg: --wasm-features <list> (if [build] wasm-features requests any;
                                         requires infc ABI ≥ 1.2. Applies in both
                                         modes — a `.v` describing a different
                                         instruction set than the shipped `.wasm`
                                         would be worthless)

Project run forces compile mode (mode = None) and never requests --out-dir, so the -v/--mode proof/--out-dir lines above never fire for it — but it shares this exact spawn otherwise, including the -L and [wasm-dependencies] forwarding.

Single-file build <path> and run <path> spawn infc directly instead of through the shared project-build helper, and — unlike the two project-mode paths above — they do not send infc the same argument list: build forwards only what the user explicitly passed, leaning on infc's own phase-flag default for the rest, while run always requests the full pipeline explicitly, because it needs the finished WASM artifact in hand to execute it. What they do agree on: neither sets current_dir, so infc inherits the invocation directory; every -L is forwarded verbatim, with no anchoring step; and whichever of --wasm-lib-dir, --wasm-dep, and --wasm-features a given invocation sends, they appear in that same relative order.

infs build <path> (single-file mode)
    |
    +-- enclosing_manifest(path)   # walk up from the source file; optional
    |
    +-- compatibility handshake     # unconditional — always runs, before any
    |       infc --commit-hash      # flag below is decided (unlike `run`,
    |       infc --abi-version      # which only handshakes when wasm-features
    |                               # are requested)
    |
    +-- spawn infc
            CWD = inherited from the invoking shell
            arg: <path>
            arg: -v                     (if `-v` was passed; `run` never sends it)
            arg: --mode <mode>          (if `--mode` was passed; `run` never
                                         sends it)
            arg: --wasm-lib-dir <dir>   (one per -L/--wasm-lib-dir, forwarded
                                         verbatim; no anchoring step runs)
            arg: --wasm-dep name=path   (one per [wasm-dependencies] entry from
                                         the enclosing manifest, if any)
            arg: --wasm-features <list> (if the enclosing manifest requests any;
                                         requires infc ABI ≥ 1.2)

build never adds --parse, --codegen, or -o: with no phase flag at all, infc's own default — full compilation, WASM written to disk — already does what build wants.

infs run <path> (single-file mode)
    |
    +-- enclosing_manifest(path)   # walk up from the source file; optional
    |
    +-- compatibility handshake     # conditional — runs only when the
    |       infc --commit-hash      # enclosing manifest requests wasm-features,
    |       infc --abi-version      # the only thing here needing a capability
    |                               # check; skipped entirely otherwise, unlike
    |                               # `build`
    |
    +-- spawn infc
            CWD = inherited from the invoking shell
            arg: <path>
            arg: --parse                (always; `build` never sends it)
            arg: --codegen              (always; `build` never sends it)
            arg: -o                     (always; `build` never sends it)
            arg: --wasm-lib-dir <dir>   (one per -L/--wasm-lib-dir, forwarded
                                         verbatim; no anchoring step runs)
            arg: --wasm-dep name=path   (one per [wasm-dependencies] entry from
                                         the enclosing manifest, if any)
            arg: --wasm-features <list> (if the enclosing manifest requests any;
                                         requires infc ABI ≥ 1.2)

run always requests --parse --codegen -o explicitly rather than relying on infc's default, and neither -v nor --mode is ever part of its argv: the RunArgs struct (apps/infs/src/commands/run.rs) carries no such flags.

infc flags confirmed against core/cli/src/parser.rs:

Note: The current ABI version is 1.2.

The default behavior when no phase flag is supplied is full compilation with WASM output written to disk — equivalent to --codegen -o.

ABI Versioning and the --out-dir Gate

infs and infc communicate their compatibility through two probes run before every project build. First, infc --commit-hash is compared with infs's build commit: a match means the two binaries came from the same tree and are guaranteed compatible, skipping further checks. Otherwise, infc --abi-version is parsed as <major>.<minor>:

• Major mismatch: hard error with remediation (rebuild or set INFC_PATH).
• Minor mismatch: warning only; compilation proceeds.
• Unknown/old (infc exits non-zero or prints unknown): silent; treated as graceful skip, equivalent to ABI unknown.

The current ABI is 1.2 (COMPILER_ABI_MAJOR = 1, COMPILER_ABI_MINOR = 2 in core/compiler-interface/src/lib.rs). Each additive flag is gated at the minor it was introduced at, independently: --out-dir landed at minor 1, and --wasm-features at minor 2. infs forwards each only to an infc that reports an ABI minor at or above the flag's own (or matches by commit hash) — an infc that reports minor 1, for instance, supports --out-dir but not --wasm-features. Pairing a manifest with a non-default [verification] output-dir against an older infc is a hard error:

error: the resolved infc does not support `--out-dir` (requires infc ABI ≥ 1.1);
       update the toolchain or remove `[verification] output-dir` from Inference.toml.

Compiler Resolution

infs locates infc by checking, in order:

1. INFC_PATH environment variable — an explicit override, useful for development and CI.
2. The infc sitting in the same directory as the running infs. A driver and its companion tools ship as one unit, so adjacency identifies the paired compiler — the same rule clang and rustc use to find theirs. Nothing about the directory is inspected, only that the two binaries share it, so this holds for a cargo build under any CARGO_TARGET_DIR, --target-dir, profile, or target triple, and for an unpacked release tarball alike.
3. System PATH (which infc).
4. The managed toolchain directory (~/.inference/toolchains/<version>/infc).

Step 2 assumes a pairing rather than proving one, so the handshake checks it: when the sibling tier resolved the compiler and infc --commit-hash disagrees with the commit infs was built from, the build warns and names both. The other three tiers stay silent on a commit mismatch, because for an explicitly pinned, system-installed, or managed infc a differing commit is the normal state — only adjacency claims the two binaries are a pair. The check sees cross-commit drift only: two binaries built from one commit with different working trees report the same hash.

INFERENCE_HOME overrides the managed toolchain root (default ~/.inference). INFS_VERBOSE traces which of the four resolved, and reports when step 2 found no neighbour and fell through.

Comparison with Cargo

The parallels to Cargo are intentional:

Where Inference is deliberately simpler: there are no build profiles beyond the compile/proof axis (debug vs. release optimization is not yet user-configurable via the manifest), no workspace support, and no package registry — external .wasm modules are referenced by filesystem path.

Current Limitations

• Fixed entry point in project mode. Project mode always compiles src/main.inf and invokes main. Custom entry files and custom exported functions are only available in single-file mode.
• Single entry file. infc follows the import-reachable closure from src/main.inf; there is no mechanism to specify additional top-level files.
• No workspaces. A single Inference.toml defines one project. Multi-crate workspace support is not yet implemented.
• No package registry. [wasm-dependencies] accepts only local filesystem paths. Version-pinned or registry-sourced dependencies are reserved for a future manifest extension.

Related Resources

• Compilation Targets — compile vs. proof modes, optimization levels, and the WASM target matrix; the --mode flag is specified in detail there.
• External Functions and WASM Linking — how use { f } from <module>; binds to [wasm-dependencies] entries and how the linker merges them.
• The WASM Linker — the static merge algorithm that folds external .wasm bodies into the output module.
• Module Hierarchy and Multi-File Compilation — how infc follows imports across files within a project.

External Functions and WASM Linking

Inference programs can call functions from pre-compiled .wasm libraries using two cooperating language constructs: external fn and use … from. The compiler emits the calls as WebAssembly imports, and a separate link step (provided by inference-wasm-linker) folds the external function bodies into the output so the final .wasm and .v files are self-contained.

Declaring an External Function

Use external fn to declare a function whose body lives in another .wasm module. The declaration looks like an ordinary function signature without a body:

external fn sum(a: i32, b: i32) -> i32;

Parameter names are optional in the declaration. The following is equivalent:

external fn sum(i32, i32) -> i32;

The type signature must match the exported function in the external module exactly. If the types disagree, the validation step (validate_extern, run by the link driver when it resolves each binding against the real .wasm bytes) reports a SignatureMismatch error and no linked module is produced.

Binding an External Function to a Module

An external fn declaration is not tied to a particular module until a use directive names the source:

use { sum } from arith;

The name after from is a logical module reference, not a file path. The compiler resolves it at build time by searching:

1. The [wasm-dependencies] table in Inference.toml (highest priority).
2. Directories passed via -L / --wasm-lib-dir on the command line.
3. Directories listed in the INFERENCE_WASM_LIB_PATH environment variable (a PATH-style list, separated by : on Unix and ; on Windows).

A :: separator is used for namespaced logical names:

use { sha256 } from crypto::digest;

This resolves to crypto/digest.wasm in one of the search directories (using the platform's path separator at resolution time, so the source stays portable across operating systems).

Multiple names from the same module are grouped in one use directive:

external fn sum(a: i32, b: i32) -> i32;
external fn neg(a: i32) -> i32;
use { sum, neg } from arith;

Calling an External Function

Once declared and bound, an external function is called exactly like a local one:

external fn sum(a: i32, b: i32) -> i32;
use { sum } from arith;

pub fn add_three(x: i32) -> i32 {
    return sum(x, 3);
}

The type-checker validates the call site (argument types, return type) using the declared signature. If the call passes type checking, codegen emits call 0 — the import index — identically to how it would emit a call to a local function.

What the Compiler Emits (Intermediate Form)

Before linking, the compiled module contains a WASM import section. The single-import example above produces:

(module
  (type (;0;) (func (param i32 i32) (result i32)))
  (type (;1;) (func (param i32) (result i32)))
  (import "arith" "sum" (func (;0;) (type 0)))
  (func $add_three (;1;) (type 1) (param $x i32) (result i32)
    local.get $x
    i32.const 3
    call 0
    return
    unreachable)
  (export "add_three" (func 1)))

Imported functions occupy the lowest WASM function indices. The local add_three is shifted to index 1 (after the one import at index 0). The call target call 0 is the import index, resolved statically during the pre-scan phase: the compiler resolves the callee name to the external fn declaration in scope where the call is written — its file, and the spec block enclosing it — and takes the import that declaration reserved. Identity is the declaration, not the name, so two files may each declare scale and bind it to a different module, and each file's calls reach its own.

The Link Step

inference-wasm-linker consumes the intermediate module and the resolved external .wasm binaries, and produces a single self-contained module with the imports satisfied and removed. The external function bodies are merged in and every index reference is rewritten into the unified index space.

main.wasm (with imports) ──┐
arith.wasm ────────────────┼──▶ inference-wasm-linker ──▶ unified.wasm
                           │                                     │
                                                          wasm-to-v
                                                                 ↓
                                                          unified.v

After linking:

• No (import …) referencing arith remains in the output.
• The bodies of sum (and any functions it calls transitively) are appended after add_three and called by index.
• The unified module passes validation and flows into wasm-to-v as an ordinary module whose merged functions translate to Rocq Definitions.

For the merge algorithm itself — transitive-closure computation, index re-encoding, the Tier-B provenance proof, and the full link-error taxonomy — see The WASM Linker.

Memory-Merge Feasibility

Not all external functions can be merged. The linker classifies each closure:

Tiers A and B turn on what the closure uses. A global the function never reads or writes, and a table with no element segment that nothing names, do not force Tier C — so the __stack_pointer global lld puts in every wasm32-unknown-unknown artifact no longer rejects it on sight.

That is a necessary step toward linking stock toolchain output, not a sufficient one. Such an artifact also declares a multi-page linear memory, and the merge never relaxes the anchor module's declared bound, so against an Inference main — which emits a fixed one-page (memory 1 1) — it now clears the tier gate and fails at memory reconciliation instead. Configurable linear memory is a separate change.

A Tier-C function produces a clear error at link time:

error: external function `lookup` requires a relocatable build:
         defines or initializes its own static data segments

Build the library with a relocatable/position-independent toolchain to enable Tier-C support in a future release.

Current Restrictions

• External functions that themselves import their host environment (memory, globals) are rejected with a clear error: a static merge cannot reconstruct that environment.
• Analysis rule A024 (ExternFunctionCall) is scope-aware: a call to a bound external (one named by a use { … } from <module>; in scope) is allowed and flows through the codegen + link path. Only a call to an unbound bare external fn — one with no use binding — is rejected, since codegen emits no import for it and so cannot compile the call.
• Only one version of each logical module is resolved per build. Multi-version dependency resolution is deferred to a future manifest update.

Example: Two Libraries, One Module

external fn sort(ptr: i32, len: i32);
external fn checksum(ptr: i32, len: i32) -> i32;
use { sort } from collections;
use { checksum } from crypto;

pub fn process(ptr: i32, len: i32) -> i32 {
    sort(ptr, len);
    return checksum(ptr, len);
}

The compiler emits two imports (indices 0 and 1), the local process at index 2. The linker searches both collections.wasm and crypto.wasm, computes the closure of each export, and merges the bodies into a single output module.

Related Resources

• The WASM Linker — the subsystem deep-dive: merge algorithm, feasibility tiers, the Tier-B provenance proof, and the link-error taxonomy
• Projects and the infs Toolchain — declaring external .wasm modules in Inference.toml under [wasm-dependencies]
• core/wasm-linker/README.md — the merge algorithm, tier classification, and entry point API
• core/wasm-codegen/docs/function-calls-lowering.md — three-stage index pre-scan and import section emission
• core/type-checker — ExternOrigin, extern_origins(), and the A024 ExternFunctionCall analysis rule
• WebAssembly import section — binary format reference

The WASM Linker

The language-level constructs — external fn, use … from, resolution priority — are documented in External Functions and WASM Linking. This chapter is the subsystem deep-dive: what inference-wasm-linker actually does to the bytes, why each decision was made, and where the approach diverges from conventional linkers.

Motivation

Inference programs can call pre-compiled .wasm library functions, but verification requires a single self-contained module. Imports are the enemy of that goal: a module with a dangling (import "arith" "sum" …) cannot be fully verified, because the Rocq translator has no body to reason about. Dynamic linking trades one problem for another — it moves the unverifiable part from the import section to runtime.

The solution is a static whole-body merge: after codegen emits an import-bearing module, the linker copies the needed function bodies in, rewrites every index reference into a unified index space, and removes the import section entirely. The output has no dangling imports, no relocation step, and no runtime loader. Verification then covers the actual deployed artifact, not a stand-in.

Where the Linker Fits in the Pipeline

Codegen produces an intermediate module whose external calls lower to (import …) entries. The linker consumes that module plus the resolved .wasm binaries and produces the self-contained module that flows into wasm-to-v:

.inf source
    │
    ▼
  parse ──▶ type-check ──▶ analyze
                                  │
                                  ▼
                            codegen (wasm-codegen)
    │
    ▼  main.wasm (import-bearing)
    │                               arith.wasm ──┐
    │                               sortlib.wasm ─┤
    └─────────────────────────────────────────────┤
                                                  ▼
                                       inference-wasm-linker
                                                  │
                                    unified.wasm (no imports)
                                                  │
                                    ┌─────────────┤
                                    ▼             ▼
                                  .out         wasm-to-v
                                             (Rocq .v file)

The linker is provided by the inference-wasm-linker crate (core/wasm-linker/). Its public API is a single function:

#![allow(unused)]
fn main() {
use inference_wasm_linker::{link, LinkError};

let unified: Vec<u8> = link(
    main_wasm,
    &[("arith", arith_wasm), ("sortlib", sortlib_wasm)],
)?;
}

Each external is tagged with the logical module name codegen recorded for it. The merge resolves each import by matching both the logical module name and the export field name, so two libraries exporting the same field name under different logical modules are never conflated.

The Merge Algorithm

For each import in the main module:

1. Find which external module exports a function of that name under the right logical module.
2. Compute the transitive closure of that export inside its source module via breadth-first search — the functions it calls recursively, plus any unexported helpers.
3. Classify the closure's feasibility tier (A, B, or C — see below).
4. Dedup the closure's function types into the output type section (two functions with identical signatures share one type entry; the key is a byte-packed encoding of the parameter and result value types).
5. Append the closure's bodies after the main module's local functions, rewriting every index-bearing instruction into the unified index space.
6. Remove the satisfied import and redirect the main module's calls from the old import index onto the merged body's new index.

Index Space After Merging

The output defines one function index space, with no import section:

[0 .. main_local_count)       main module's local functions (imports removed)
[main_local_count .. total)   merged external functions, in closure order

Operator Re-encoding

The rewrite module walks each copied body's operator stream and re-encodes only the index-bearing operators: call, return_call, ref.func, call_indirect, return_call_indirect, and block/loop/if when carrying a function type index. Every other operator is copied verbatim from the source bytes. The main module's own bodies are re-encoded for the same reason: removing imports shifts their local-function indices downward.

Dead-Code Exclusion

The transitive closure walk collects only the functions actually reachable from each satisfied export. An unused function that the source module exports but that no satisfied import calls is never pulled into the closure, so it does not appear in the merged output.

The Example from the Repository

The scratch/linker-e2e/ demo links three external modules simultaneously. The Inference.toml declares them:

[wasm-dependencies]
arith   = { path = "libs/arith.wasm"   }
memlib  = { path = "libs/memlib.wasm"  }
sortlib = { path = "libs/sortlib.wasm" }

The source uses all three:

external fn sum(a: i32, b: i32) -> i32;
external fn neg(a: i32) -> i32;
use { sum, neg } from arith;

external fn store_at(ptr: i32, val: i32);
external fn load_at(ptr: i32) -> i32;
use { store_at, load_at } from memlib;

external fn sort_pair(ptr: i32);
use { sort_pair } from sortlib;

arith is pure arithmetic (Tier A). memlib and sortlib access memory only through the caller-supplied pointer (Tier B). sort_pair transitively calls a non-exported swap helper — the closure walk drags that helper in automatically, and both functions merge. After linking, the output has no imports and one reconciled linear memory shared by all three modules' bodies.

Feasibility Tiers

Not all external functions can be merged without relocation metadata. The linker classifies each closure:

What Each Tier May Touch

The classification logic inspects the parsed module structure and the closure's ClosureEffects, collected as a side effect of the operator allow-list scan:

Reading or writing a module global is not a Tier-C signal: the closure's globals are merged into the output alongside the main module's, with every global.get / global.set remapped onto the merged index space. A global used to address memory is still rejected, because the address it produces is not parameter-derived.

If no Tier-C signals are present, the closure is Tier B when any body accesses linear memory (load, store, copy, fill, size, or grow), and Tier A otherwise.

Globals and table use are gated on use; data and element segments on declaration. A global no body reads or writes, and a table with no element segment that no instruction names, are inert — and they are exactly what real toolchains emit unconditionally (lld puts a __stack_pointer global into every wasm32-unknown-unknown artifact, and an empty (table 1 1 funcref) into every std one), so rejecting on their declaration would exclude every such artifact.

The two declaration-gated signals rest on different arguments. An active data segment writes memory at instantiation whether or not any instruction names it, so an unreferenced one still changes program behavior — a correctness argument. An element segment is rejected as conservatism: dropping one is unobservable, since the merged output declares no table for it to initialize, but it marks a module built around indirect dispatch and admitting it would silently discard a construct the author wrote.

Dropping an admitted external's globals and tables is sound because ClosureEffects is closure-scoped: a closure admitted with no global or table effect contains no operator naming either index space. That matters most for globals — the merge re-emits main's global section, so a leaked global.get 0 would rebind to main's first global and, the types agreeing, still pass post-merge validation. A leaked table operator is fail-safe by comparison: no table section is emitted, so validation rejects it as an unknown table.

Clearing the tier gate is not the same as linking. A stock artifact also declares a multi-page memory that the merge will not reconcile against an Inference main's fixed one-page (memory 1 1); see the memory reconciliation rules below.

A Tier-A function carries no shared-memory surface at all: it reads its parameters, does arithmetic, and returns. Merge cost is a body copy, a type dedup, and an index rewrite.

A Tier-B function shares the single linear memory the main module owns. No address relocation is needed because every address is caller-supplied at runtime. However, the linker must prove this property — it cannot assume it from the section structure alone.

Tier-C Rejection

A Tier-C closure is rejected with LinkError::RequiresRelocatableBuild listing the specific reasons:

error: external function `lookup` requires a relocatable build:
         defines or initializes its own static data segments

The reasons field is a Vec<String> so a closure that simultaneously has its own globals and uses memory.init reports both signals in one diagnostic.

Tier-B Provenance Analysis

The provenance analysis is the most novel part of the linker. Tier B's contract is that a merged external touches shared linear memory only through addresses the caller passes in. A function that fabricates an address from a constant or reads one from its own global would alias the host program's own linear memory at a fixed offset — a silent miscompile the section-inspection tier check cannot detect, because the function validates cleanly and its export signature matches.

The linker proves the contract with a sound, flow-sensitive, interprocedural abstract interpretation over the whole closure.

The Provenance Lattice

Every operand-stack slot and every local carries one of three provenance tags:

The lattice join is a must-join: a value stays Param only when it is Param on every incoming control-flow path. The mask at a join point is the union of the per-path masks (on every path it derives from some parameter, so on the merged path it derives from one of the union). A value arriving as Const on one path and Param on another widens to NotParam.

Why Const Is a Separate Tag

Const exists so a Param + Const expression (a struct-field or array-element offset: base_ptr + 8) can stay Param while a Param + NotParam expression cannot. A NotParam addend means not provably parameter-derived, not constant. It may hold C - p (a constant minus a parameter), and (C - p) + p == C is a caller-independent absolute address. Restricting the non-Param addend to a proven Const closes that cancellation attack.

For the same reason sub propagates Param only from the minuend when the subtrahend is Const (caller_base - fixed_offset is still caller-relative), and Param - Param demotes to NotParam (since b - b == 0, a caller-independent constant).

Every other binary operator — multiply, divide, bitwise, shift, rotate, comparison — and every unary operator produces NotParam. The analysis is deliberately conservative: it cannot distinguish param << 0 (value-preserving) from param & 0 (value-destroying), so it treats all such operators uniformly.

Bulk-Memory Extent Operands

For memory.fill and memory.copy, the size/extent operand carries the same caller-derivation requirement as the address operand. The operation touches the contiguous region [address, address + size), so a caller-bounded start is not enough — a constant or global size would let the operation clobber or read an unbounded span above a caller pointer (memory.fill(base, v, 0x8000) scorches host memory the caller never exposed). A Param size (a caller-supplied len) is admitted; a Const or NotParam size fails the subset check.

Interprocedural Fixpoint

Each function in the closure is summarised once by seeding parameter i with Prov::Param({i}). The summary records, per function, the provenance mask of every memory access, and per call site, the argument mask of every argument in the calling function's own parameter terms.

A greatest-fixpoint pass over the call graph then computes, for every function g, the set trusted[g] — the subset of g's parameters that are provably caller-derived:

• The closure root's parameters are all trusted (the host that calls the exported function supplies them).
• A parameter j of a non-root function g is trusted if and only if, at every internal call site f → g, the argument in position j has a non-empty mask that is a subset of trusted[f].

The iteration starts from "all parameters trusted" and removes any parameter contradicted at a reachable call site, converging in at most (slot count + 1) rounds. The fixpoint handles self- and mutual recursion correctly. A function reachable only through the table (no direct call site) starts with the empty trusted set — a dereference of its parameter is rejected.

Finally, every recorded memory access is verified: its address mask must be non-empty and a subset of its function's trusted set. A failure at any point rejects the whole closure as Tier C, never Tier B.

root_params = {ptr, len}        (trusted by the external caller)

inner(addr, count):
  addr derived from ptr → trusted
  count derived from len → trusted
  memory.fill(addr, 0, count) → both masks ⊆ trusted → Tier B ✓

inner2(addr, count):
  count is i32.const 0x8000 → Const, mask = {} → mask ⊄ trusted → Tier C ✗

Proof-Only Stripping

Inference non-deterministic blocks (forall, exists, assume, unique) and uzumaki rvalues (i32.uzumaki, i64.uzumaki) are proof-only constructs: they have meaning solely in the Rocq lowering and no executable runtime semantics. A function that is merged into the output is part of an executable binary, so a proof-only opcode inside such a body would yield a non-executable output.

The operator allow-list (src/safety.rs) rejects every proof-only opcode from an external body with LinkError::UnsupportedConstruct:

unsupported WASM construct for static merge: non-deterministic block `forall`
    has no executable semantics and cannot be merged into an executable binary

The main module's own proof scaffolding (its spec blocks and non-det opcodes) is preserved and passed through verbatim — the re-encoder recognises those opcodes and copies them intact onto the main-module bodies, which are not subject to the allow-list. Those bodies flow through wasm-to-v as the proof obligations the user wrote.

Floating-Point Exclusion

The Inference language has no f32/f64 types. The Rocq translator models no float instruction. The linker enforces this at two gates:

1. Feature gate (SUPPORTED_WASM_FEATURES in src/lib.rs): every external module is structurally validated before any body is touched. The feature set deliberately omits FLOATS, so a float-using external is rejected upfront with LinkError::UnsupportedWasmFeature naming the exact feature.

2. Operator allow-list (src/safety.rs): the main-module re-encode path does not pass through the feature gate, so the allow-list is the backstop. Every float instruction — comparisons, arithmetic, conversions, reinterprets, loads/stores, and constants — is rejected with LinkError::UnsupportedConstruct naming the exact mnemonic (e.g. floating-point instruction 'f32.add' is not supported).

Saturating float-to-int (i32.trunc_sat_f32_s, etc.) is also excluded: its operands are floats, and the Rocq translator declares no float number type.

Sign-extension (i32.extend8_s, i64.extend32_s, etc.) is not excluded, though Inference codegen still emits none of it. The Rocq translator lowers all five opcodes to BI_unop t (Unop_extend n) — the proof model classifies sign-extension as a unop, beside clz/ctz/popcnt, not as a conversion — so an external compiled by a real toolchain can carry them.

Name Preservation

The linker preserves the WASM name custom section so the Rocq translator emits named Definitions rather than opaque func_<idx> placeholders:

• Main module local functions keep their source debug names, re-indexed onto the import-free output space.
• Every merged external function is named under its source's logical module using a module.field form:
  • A closure root satisfying import sum bound under logical module mathlib becomes mathlib.sum.
  • An internal callee the source module named keeps that name, prefixed: mathlib.helper.
  • A nameless inner callee (an external with no name section) receives a deterministic fallback derived from its output index: mathlib.func_<idx>.

The . separator prevents collision between two libraries that export same-named fields under different logical modules. The Rocq translator (core/wasm-to-v/src/rocq_names.rs) sanitizes every non-alphanumeric character to _, so mathlib.sum becomes Definition mathlib_sum in the .v file. A residual collision after sanitization (e.g. two modules that sanitize to the same identifier) is still disambiguated by the translator's index suffix; the module prefix removes the common case rather than every possible one.

Error Reference

Supported WASM Subset

The linker accepts only the following feature set (SUPPORTED_WASM_FEATURES in src/lib.rs):

• Integer core: i32/i64 value types, all integer arithmetic, comparisons, loads/stores, and the three integer width conversions (i32.wrap_i64, i64.extend_i32_s/u).
• Mutable globals, bulk memory (memory.copy/memory.fill), and sign-extension (i32.extend8_s, i32.extend16_s, i64.extend8_s, i64.extend16_s, i64.extend32_s).

Everything else is rejected at the feature gate or the operator allow-list before any body is copied.

Formal Implications

Once merged, every external function becomes an ordinary local function in the output module. The Rocq translator processes that module without knowing which functions originated externally: each merged body becomes a Rocq Definition in the .v file, exactly as a locally-defined function does.

Verification therefore covers the actual deployed merged artifact, not a stand-in. A proof that sort_demo returns the expected value reasons about the real mathlib_sort and memlib_store_at bodies — not their declared signatures.

The inference.spec_funcs custom section (src/spec_funcs.rs) carries the WASM function indices the Rocq translator must turn into proof obligations. The merge removes imports and shifts indices, so the linker decodes this section, remaps every index through the unified index space, and re-emits it. The round-trip is byte-stable: proof obligations are never lost across the link step.

Comparison with Traditional Linkers

Traditional wasm-ld (LLVM's WebAssembly linker) supports relocatable object files: each compiled translation unit emits relocation metadata (symbol tables, reloc sections), and wasm-ld patches absolute addresses and index references at link time. That model handles Tier-C inputs (static data, globals, indirect-call tables) without a provenance proof, because the relocation metadata describes exactly what needs patching.

Inference cannot use wasm-ld for two reasons:

1. Verification needs a relocation-free module. wasm-ld produces a module that is self-contained at runtime but which was assembled from relocatable pieces. The Rocq translator expects to reason about the final module; it has no model for relocation metadata or the toolchain decisions it encodes.

2. External libraries are not necessarily compiled with Inference. They may come from any WASM toolchain and need not carry wasm-ld-compatible relocation sections. The static merge works on any conforming WASM binary — no toolchain cooperation is required for Tier-A and Tier-B inputs.

The provenance analysis fills the gap: instead of relocation metadata, the linker proves that the merged function cannot produce an address the host program did not supply. A function passing that proof needs no relocation, because its memory accesses are bounded to whatever region the caller chose to expose.

Tier-C support via relocation metadata is a stated future direction. The current linker explicitly gates on Tier A and B rather than risk a silent miscompile from an unproven address.

Related Resources

• External Functions and WASM Linking — the language-level feature: external fn, use … from, resolution priority, and the Tier A/B/C overview
• Projects and the infs Toolchain — configuring [wasm-dependencies] and building with the project-aware CLI
• Compilation Targets — compile vs. proof modes; the merged module flows through the same -v proof path as a locally-compiled module
• core/wasm-linker/README.md — merge algorithm, tier classification, index space, name section, testing, and fuzzing
• core/wasm-linker/src/provenance.rs — full source of the abstract interpreter (module-level doc comment is a complete specification)
• WebAssembly binary format — section ordering, index spaces, and the name custom section

The Language Server

This chapter explains how Inference ships IDE support: the inference-lsp server in apps/lsp and the four-crate IDE stack under ide/ that it is built on. It covers the layering that keeps the protocol, the features, and the compiler apart; the thread architecture that keeps typing responsive even though analysis is strictly serial; the Salsa-based memoization that makes repeated queries cheap; and the resilience story — what happens when the compiler panics underneath an editor session.

Design goals

Four constraints shape everything in the stack:

• Real compiler answers. Diagnostics, hovers, and completions come from the same parser, type checker, and analysis rules that infc runs — not from a parallel re-implementation that would drift. What the editor underlines is exactly what the build would reject.
• The editor's buffer is the source of truth. The user's unsaved text — the overlay — takes priority over whatever is on disk, for the open document and for every file its imports reach.
• Serial analysis, responsive editing. The semantic stack holds !Send state, so analysis is strictly serial: one computation at a time. A keystroke must nevertheless never wait behind a stale request, which forces an interruption mechanism rather than a concurrency one (issue #157).
• A compiler bug must not take the session down. The type checker and the analysis passes are under active development; a todo!() reached through some half-typed input has to cost one request, not the editor session.

The layered stack

The server is the thin protocol shell on top of a strictly layered set of crates:

  editors/vscode      LanguageClient, speaks LSP over stdio
        │
  apps/lsp            inference-lsp — router / analysis worker / read pool
        │
  ide/ide             inference-ide — feature API (AnalysisHost, Analysis)
        │
  ide/ide-db          inference-ide-db — Salsa database, memoized analyses
        │                              │
  ide/base-db         positions        core/… — the compiler front end
  ide/vfs             file identity      (parser, type-checker, analysis)

Two dependency firewalls hold the layering in place:

• The protocol layer never sees the semantic machinery. apps/lsp depends on inference-ide alone and talks to it in paths, byte offsets, and ide-owned result types — no compiler type crosses the boundary. A guard test (apps/lsp/tests/no_salsa_in_lsp.rs) fails the build if any source line in the crate so much as mentions Salsa, naming the offending file:line.
• The IDE never links the backend. ide-db reaches the compiler through the leaf inference-project-model crate plus the parser, type-checker, and analysis crates — not through the inference orchestration crate — so WASM code generation and the Rocq translator are never compiled into the editor toolchain.

Protocol choices

The server is built on lsp-server — the same minimal, synchronous crate rust-analyzer uses — rather than an async framework like tower-lsp. Analysis is serial and CPU-bound; an async runtime would add scheduling machinery without adding concurrency where it matters. Threads and crossbeam channels model the actual shape of the work.

The transport is stdio: stdout carries framed JSON-RPC exclusively, and all logging goes to stderr. The capability set advertised at initialize (apps/lsp/src/capabilities.rs) is deliberately small and fully implemented:

Position encoding is left unnegotiated, so the LSP default of UTF-16 applies — the one encoding the convert module translates the compiler's byte offsets into.

Full-text sync is a deliberate v1 choice, not an oversight: the resilient parser re-parses a document in well under a millisecond, AnalysisHost::change_document replaces the overlay wholesale, and the closure-aware invalidation in ide-db already makes reanalysis cheap. An incremental protocol would add a delta-application layer with nothing downstream able to exploit the deltas.

A router, a worker, and a read pool

apps/lsp/src/server.rs splits a session across three kinds of thread, joined under std::thread::scope:

  stdin ──► router ──Job{epoch,message}──► analysis worker ──► responses,
              │                              │        ▲          publishes
              │ $/cancelRequest,             │        │ WorkerEvent
              │ cancellation firing      ReadTask     │
              │                              ▼        │
              └──────────────────────────  read pool (2 threads)

• The router reads the transport and forwards every message to the worker instantly over an unbounded channel. It handles inline only what must not wait behind an analysis: request-id bookkeeping, $/cancelRequest, and — for a document write it adopts, and for shutdown/exit — firing cancellation of the worker's in-flight analysis before forwarding the message.
• The analysis worker owns the ServerState (the AnalysisHost plus per-document bookkeeping) and processes jobs one at a time, in arrival order. Every response and every published diagnostic leaves from here, with one exception: the router answers a cancelled request's -32800 itself.
• The read pool — two threads — serves pure read requests off database snapshots concurrently with the worker (covered below).

Why this shape? Analysis cannot be parallelized (the semantic state is !Send), but it can be interrupted. The router is the always-listening ear: because it never computes, it can always fire the cancellation flag the moment a newer write makes the in-flight computation moot. The worker is "the message loop, one thread over" — the serial semantics are preserved exactly, but a stale analysis now dies in microseconds instead of finishing on principle.

Every thread that runs analysis gets a 64 MiB stack (mirroring rust-analyzer's main-loop stack). The pipeline recurses with the input's nesting depth, and a stack overflow aborts the process — it cannot be caught — so the only mitigation is headroom.

Cancellation: one epoch, two meanings

Cancellation is driven by a single monotonic write epoch paired with a Salsa cancellation token (AnalysisCancelSource in ide/ide-db). The router bumps the epoch and fires the token before forwarding an adopted write, and stamps the forwarded job with the post-bump epoch. The analysis polls the token at checkpoints between pipeline stages and unwinds when it is set.

When the worker catches a cancellation unwind, the epoch disambiguates it:

• Superseded — the source's epoch is newer than the job's: a write landed after this job was routed. The request is answered ContentModified (-32801) so the client retries against the new content; the cache is left intact.
• Residual self-cancel — the epochs match: the unwind consumed a signal meant for earlier work (the write's own eager publish, for example). The work is simply retried; a genuinely newer write always carries a newer epoch, which bounds the retry.

Stamping the write's job with the post-bump epoch is the crux of the protocol: it is what lets the worker classify the write's own follow-up work as current rather than cancelling it with the very signal the write fired.

A client's $/cancelRequest is deliberately weaker, matching rust-analyzer: a still-pending request is answered -32800 immediately and its late response suppressed, but the in-flight compute is not interrupted. Only writes preempt computation, because only writes make it wrong.

Coalescing keystrokes and deferring dependents

The unbounded job channel is the buffer a typing burst accumulates in. At dequeue, the worker drains whatever has piled up and collapses consecutive didChange notifications for the same document into the final text (coalesced_job_batch), so a burst of keystrokes runs the pipeline a handful of times instead of once each. The collapse is conservative: a didOpen or didClose for that document, or any request, is a barrier the coalescer never reorders across, and no non-didChange job is ever dropped.

A change to one file can also invalidate another open document whose import closure includes it. The worker publishes eagerly only for the changed document; every other invalidated document goes into a pending-republish set that drains when the loop next goes idle — after the interactive request that arrived right behind the keystroke has been answered. A feature request that hits a queued document publishes it fresh immediately, so the client never keeps a stale diagnostic set; documents the change did not touch keep their memoized analysis and are never republished at all.

Memoizing analyses with Salsa

ide-db is built on Salsa (pinned to 0.27, matching rust-analyzer) — but it uses Salsa very differently than rust-analyzer does.

One coarse query

There is a single memoized query, analyze_entry: its body is the entire front-end pipeline for one document — resilient project load through the overlay-then-disk loader, lossless type check, all analysis rules — producing one FileAnalysis. rust-analyzer decomposes analysis into hundreds of fine-grained queries so an edit recomputes only slivers; Inference's pipeline is fast enough to run whole-document, so the memoization boundary sits at the document instead. That trades incremental granularity for a radically simpler invariant: a document's analysis is either memoized and current, or it is recomputed from scratch.

Inputs and edges

Salsa can only track what goes through its inputs, and file content deliberately does not: the analysis reads files through the same overlay-then-disk Vfs loader seam the compiler uses, which must stay Salsa-free so compiler and IDE share one import-resolution path. The database therefore represents change signals, not content, as inputs:

• EntryInput { path, src_root, evicted } — a project entry's identity, plus the eviction lever (below);
• FileStamp { stamp } — an opaque monotonic counter per reachable file, bumped on any overlay write to that path;
• AvailabilityEpoch — a singleton bumped when a didOpen makes overlay content available where there was none.

Invalidation is edge-driven: after computing, the query registers a dependency on the stamp of every file in the import closure it actually resolved. Bumping one path's stamp then invalidates exactly the memos whose closure contains that path. A file that failed to resolve names no path at all, so the query additionally reads the availability epoch only when its parse recorded an unresolved import — a deliberately coarse edge that re-fires exactly the analyses a newly opened file might fix.

Eviction by sentinel swap

Salsa 0.27 has no per-memo eviction: a memoized value lives as long as its input. But a closed document's analysis — or one computed for a never-opened path a feature request touched — must be releasable. The database frees them with a sentinel swap: setting the entry's evicted input invalidates the memo, and the next recompute routes to a tiny sentinel value, which pushes the fat analysis onto Salsa's deleted list to be freed at the next revision boundary. Un-evicting takes one input write back and forces exactly one full recompute.

Open documents are never evicted. Never-opened analyses are capped at MAX_UNOPENED_ANALYSES = 8 in FIFO order, which bounds the resident set of a session at roughly open documents + 8 fat analyses.

Serving pure reads concurrently

Serial analysis has one more cost: with a single worker, a slow request blocks a fast one even when both only read. The read pool removes that without touching the serial-write invariant.

For the five read-only methods (hover, goto definition, completions, document symbols, inlay hints), the worker asks the database for a ReadPlan. If the document's analysis is memoized — or stale in a way that can be recomputed against a cached source root — the plan carries an AnalysisSnapshot: a second database handle cloned from the same Salsa storage, sharing the overlay and the memo table. The request is handed to a pool thread, which serves it off the snapshot and sends the response itself; the worker moves on immediately. Everything else — writes, diagnostics publishes, and any read that cannot be planned concurrently — stays on the serial path.

The safety argument leans on Salsa's own synchronization: an overlay write bumps the file stamp first, and Salsa's setter blocks until every outstanding snapshot handle is dropped — while the fired cancellation token makes the readers holding those handles unwind at their next checkpoint. So a write can stall only microseconds behind a reader, and a reader can never observe a half-applied write. A read that loses this race is routed back to the worker and served serially under its original epoch, preserving the exact supersede-or-answer classification it would have had on the serial path.

Two pool threads are enough to overlap an interactive request with a slow one, while bounding the wasted partial computes when a write cancels the pool mid-flight.

Resilience: containing the compiler

Every request and every notification is dispatched inside catch_unwind, and the catch classifies the unwind: a cancellation follows the epoch protocol above; a panic is contained.

A panicking request is answered InternalError with its original id, so the client can correlate the failure. A panicking notification publishes nothing. In both cases the analysis host — which the unwinding computation may have left half-updated — is discarded and rebuilt from the tracked open documents' last-seen text, without reading anything from disk (the overlay may never have been saved). The first query afterwards recomputes from scratch; every other document keeps working. Before this boundary existed, a panic during didOpen was fatal — and because clients re-send the same didOpen on restart, the server crash-looped until the client gave up.

Two deliberate non-recoveries: a stack overflow aborts the process (the 64 MiB stacks are the mitigation, not a catch), and a didChange for a document that was never opened — a protocol violation some clients commit in tab-close races — is logged and dropped rather than guessed at.

Shutdown

After answering shutdown, the server performs no further idle work: the pending-republish queue is abandoned rather than flushed, because LSP 3.17 forbids notifications after shutdown — the client can no longer act on a publish, and the router fired cancellation ahead of the shutdown request, so draining the queue would recompute stale entries under a set cancellation flag and stall teardown behind doomed analyses.

What is not abandoned is a response owed to a pre-shutdown request: a read still parked in the route-back path is answered ContentModified rather than dropped. A response is not a notification — it stays protocol-legal after shutdown, and dropping it would leave a request id dangling in the client. The exit notification then ends the loop; the scoped threads join on every path, so teardown cannot hang.

Diagnostics come from the real front end

Publishing diagnostics for a document runs the full pipeline: project load (overlay first, disk second) rooted at the document's source root, the lossless type check, and every analysis rule. Four diagnostic sources merge into one sorted, deduplicated list, each tagged with a stable code:

Only the entry document's own diagnostics are published — errors inside an imported file are that file's diagnostics when it is open, though a broken import is still summarized on the use directive that names it.

The analysis model is per-document: each open file is analyzed as its own project entry together with its import closure, and there is no shared project-wide index in v1 — two open documents that import the same file each analyze it independently. That costs duplicate work but keeps a hard simplicity: no cross-document consistency protocol, no workspace indexing phase, and eviction that follows document lifecycle directly.

One feature is worth singling out: hovering a non-deterministic construct — forall, exists, unique, assume, or @ — answers with its verification meaning, including how it lowers into Rocq (for example, that a forall block becomes a BI_forall obligation). The prose is authored once, in ide/ide/src/nondet_docs.rs, and inlay hints annotate the same constructs. For a language whose semantics live partly in the proof world, hover is documentation infrastructure, not a convenience.

The VS Code extension

The extension (editors/vscode) is a thin vscode-languageclient shell. It resolves the server binary in strict order: the inference.lsp.path setting (used verbatim — a configured but non-executable path is an error, not a fallback), then the managed toolchain at <INFERENCE_HOME>/bin/inference-lsp, then PATH. Missing everywhere means the language features quietly stay off; the editor remains usable.

Restarts are imperative and serialized: switching or installing a toolchain version through the extension's own commands, changing any inference.lsp.* setting, or invoking the manual restart command all funnel into one stop-then-start path. What does not restart the server is mutating the toolchain behind the extension's back (an infs default in a terminal) — the extension deliberately does not watch the filesystem for that.

Comparison with rust-analyzer

The stack borrows rust-analyzer's load-bearing decisions and diverges where Inference's scale allows something simpler:

Borrowed: the lsp-server crate and its synchronous connection model; a Salsa database at the semantic core; the 64 MiB analysis stack; the cancel-and-retry discipline where writes preempt reads and superseded requests answer ContentModified; $/cancelRequest as bookkeeping only; the VFS-with-overlay file model.

Diverged: one coarse memoized query per document instead of a fine-grained query graph — Inference's whole front end runs in the time rust-analyzer budgets for a fraction of one feature, so incrementality below the document level is not yet worth its complexity. A fixed two-thread read pool with explicit route-back instead of a snapshot per request. Full-text sync instead of incremental edits. Per-document projects instead of a workspace-wide crate graph. And no filesystem watching in v1: what the editor has not opened, the server sees only through disk reads at analysis time.

Testing and verification

The server's logic lives in ServerState, which does no I/O — one request in, one response out — so the unit tests in apps/lsp/src/server.rs drive routing, coalescing, cancellation classification, panic recovery, and shutdown semantics directly, without a transport.

End to end, apps/lsp/tests/e2e.rs spawns the compiled server binary and speaks framed JSON-RPC over its real stdio through a timeout-guarded test client (tests/harness/). The scenarios cover the full lifecycle — initialize through exit — plus the awkward cases: malformed frames, requests before initialization, cancellation races, panic containment, and stdout hygiene (a full session must write nothing to stdout that is not framed protocol).

Two guard tests keep the architecture honest: the no-Salsa-in-apps/lsp scan described above, and a drift guard tying the pool-eligible method list to the pool dispatcher. Debug-only seams (deliberate slow-downs, panics, and rendezvous points injected into the analysis path) let the concurrency tests force the interleavings — a write landing mid-read, a pool panic, a shutdown during a drain — that real editors produce only rarely and never on demand.

Summary

The language server is a thin, synchronous protocol shell over a strictly layered IDE stack. A router thread keeps the server listening while a single analysis worker preserves the compiler's serial semantics; a write epoch threaded through every job turns cancellation into a precise supersede-or-retry decision; and a small read pool serves memoized reads concurrently without weakening the serial-write invariant. Salsa memoizes one coarse analysis per document, invalidated edge-wise through per-file change stamps and evicted by sentinel swap. Diagnostics run the real front end, so the editor and the build can never disagree. And the whole stack is built to survive its own compiler: a panic costs one request and one cache, never the session.

References

• LSP 3.17 specification
• rust-analyzer architecture
• lsp-server — rust-analyzer's synchronous LSP scaffold
• Salsa — incremental computation framework
• apps/lsp/README.md, ide/ide-db/README.md, ide/ide/README.md — the per-crate documentation this chapter condenses

Appendix B: LLVM Features (Legacy)

Note: Starting from the version after v0.0.1-beta.3, the Inference compiler no longer uses LLVM. WebAssembly is generated directly via wasm-encoder. This appendix is preserved as a reference for users on older versions.

LLVM Legacy Setup (v0.0.1-beta.3 and earlier)

Note: Starting from version after v0.0.1-beta.3, the Inference compiler no longer requires LLVM, inf-llc, rust-lld, or libLLVM. The compiler now generates WebAssembly directly via wasm-encoder. This document is preserved for users working with v0.0.1-beta.3 or earlier releases.

The GCP-hosted binaries remain available, so these older builds continue to work.

LLVM 21 Installation

Linux (Ubuntu/Debian)

wget https://apt.llvm.org/llvm.sh
chmod +x llvm.sh
sudo ./llvm.sh 21
sudo apt-get install -y llvm-21-dev libpolly-21-dev

Verify:

llvm-config-21 --version

Linux (Fedora)

sudo dnf install -y llvm21-devel polly21-devel

macOS

brew install llvm@21

If llvm@21 is not available:

brew install llvm

Verify:

$(brew --prefix llvm@21 2>/dev/null || brew --prefix llvm)/bin/llvm-config --version

Note: Homebrew's LLVM is "keg-only" and not symlinked to /usr/local/bin by default.

Windows (MSYS2)

In the MSYS2 UCRT64 terminal:

cd /tmp
curl -LO 'https://repo.msys2.org/mingw/ucrt64/mingw-w64-ucrt-x86_64-llvm-21.1.1-2-any.pkg.tar.zst'
curl -LO 'https://repo.msys2.org/mingw/ucrt64/mingw-w64-ucrt-x86_64-llvm-libs-21.1.1-2-any.pkg.tar.zst'
curl -LO 'https://repo.msys2.org/mingw/ucrt64/mingw-w64-ucrt-x86_64-llvm-tools-21.1.1-2-any.pkg.tar.zst'
curl -LO 'https://repo.msys2.org/mingw/ucrt64/mingw-w64-ucrt-x86_64-clang-21.1.1-2-any.pkg.tar.zst'
curl -LO 'https://repo.msys2.org/mingw/ucrt64/mingw-w64-ucrt-x86_64-clang-libs-21.1.1-2-any.pkg.tar.zst'

pacman -U --noconfirm \
  /tmp/mingw-w64-ucrt-x86_64-llvm-21.1.1-2-any.pkg.tar.zst \
  /tmp/mingw-w64-ucrt-x86_64-llvm-libs-21.1.1-2-any.pkg.tar.zst \
  /tmp/mingw-w64-ucrt-x86_64-llvm-tools-21.1.1-2-any.pkg.tar.zst \
  /tmp/mingw-w64-ucrt-x86_64-clang-21.1.1-2-any.pkg.tar.zst \
  /tmp/mingw-w64-ucrt-x86_64-clang-libs-21.1.1-2-any.pkg.tar.zst

Important: LLVM 21.1.1 is required. Version 21.1.7 has compatibility issues.

To prevent accidental upgrades:

echo "IgnorePkg = mingw-w64-ucrt-x86_64-llvm mingw-w64-ucrt-x86_64-llvm-libs mingw-w64-ucrt-x86_64-llvm-tools mingw-w64-ucrt-x86_64-clang mingw-w64-ucrt-x86_64-clang-libs" | sudo tee -a /etc/pacman.conf

External Binaries

Download Links (GCP)

Linux

• inf-llc: Download → Extract to external/bin/linux/
• rust-lld: Download → Extract to external/bin/linux/
• libLLVM: Download → Extract to external/lib/linux/

macOS

• inf-llc: Download → Extract to external/bin/macos/
• rust-lld: Download → Extract to external/bin/macos/

macOS does NOT require the libLLVM.so shared library.

Windows

• inf-llc.exe: Download → Extract to external/bin/windows/
• rust-lld.exe: Download → Extract to external/bin/windows/

Setup

# Linux
mkdir -p external/bin/linux external/lib/linux
curl -L "https://storage.googleapis.com/external_binaries/linux/bin/inf-llc.zip" -o /tmp/inf-llc.zip
unzip -o /tmp/inf-llc.zip -d external/bin/linux/
curl -L "https://storage.googleapis.com/external_binaries/linux/bin/rust-lld.zip" -o /tmp/rust-lld.zip
unzip -o /tmp/rust-lld.zip -d external/bin/linux/
curl -L "https://storage.googleapis.com/external_binaries/linux/lib/libLLVM.so.21.1-rust-1.94.0-nightly.zip" -o /tmp/libLLVM.zip
unzip -o /tmp/libLLVM.zip -d external/lib/linux/
chmod +x external/bin/linux/inf-llc external/bin/linux/rust-lld

# macOS
mkdir -p external/bin/macos
curl -L "https://storage.googleapis.com/external_binaries/macos/bin/inf-llc.zip" -o /tmp/inf-llc.zip
unzip -o /tmp/inf-llc.zip -d external/bin/macos/
curl -L "https://storage.googleapis.com/external_binaries/macos/bin/rust-lld.zip" -o /tmp/rust-lld.zip
unzip -o /tmp/rust-lld.zip -d external/bin/macos/
chmod +x external/bin/macos/inf-llc external/bin/macos/rust-lld

Environment Variables

Troubleshooting

"LLVM not found" or "llvm-sys build failed"

1. Verify LLVM 21 is installed: llvm-config-21 --version
2. Check environment variable: echo $LLVM_SYS_211_PREFIX
3. Verify path exists: ls -la $LLVM_SYS_211_PREFIX

"inf-llc not found" or "rust-lld not found"

1. Verify binaries exist: ls -la external/bin/<platform>/
2. Check they are executable: file external/bin/<platform>/inf-llc
3. Make executable: chmod +x external/bin/<platform>/inf-llc external/bin/<platform>/rust-lld

"libLLVM.so: cannot open shared object file" (Linux)

1. Verify library exists: ls -la external/lib/linux/
2. Re-download if missing
3. Rebuild: cargo clean && cargo build

macOS Gatekeeper quarantine

xattr -d com.apple.quarantine external/bin/macos/inf-llc
xattr -d com.apple.quarantine external/bin/macos/rust-lld

"LLVMConst*Mul undefined reference" (Windows)

You likely have LLVM 21.1.7 instead of 21.1.1. Downgrade to 21.1.1.