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.

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:

• Greedy negative numbers. A leading - is part of a number literal when it is immediately followed by a digit, so -42 lexes as a single Number token, not Minus then Number. (- 42, with a space, lexes as two tokens and parses as a unary negation.)
• 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 associated constant SyntaxKind::FIRST_NODE (the SourceFile variant). A compile-time assertion keeps all token kinds below 128:

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

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 come from the Inference grammar's PRECEDENCE map, so the parse shapes match the language definition exactly (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 — resolved in the lexer (greedy 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 (~1,600 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 ~200 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<AnalysisDiagnostic> independently.

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.

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 }
      |           |
      |           v
      |       Vec<AnalysisDiagnostic>
      |
      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<AnalysisDiagnostic> {
        // 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::AnalysisDiagnostic> {
        // 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<AnalysisDiagnostic> {
        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(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.

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::Module — recurses into the module's nested definitions (if the module has a body)
• 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, functions inside spec blocks, and functions inside modules are all covered by a single call to walk_function_bodies.

Depth Tracking

WalkContext carries three 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>,
}
}

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.

At each function boundary, walk_function_bodies asserts that all three 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

All five current rules are error-severity. Advisory rules (warning or info severity) are supported by the infrastructure but none have been defined yet.

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, walker};

crate::rule! {
    /// One-line description for rustdoc.
    #[id = "AXXX"]
    #[name = "Human readable name"]
    #[severity = error]
    pub struct YourRuleName;
    fn check(ctx: &TypedContext) -> Vec<AnalysisDiagnostic> {
        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
            // push to errors when the rule fires
        });
        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 with arrays is called, __stack_pointer is decremented by the frame size. When the function returns, it is restored. 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 with arrays 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.

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 arrays emits a prologue at entry and an epilogue at every exit point.

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. But the callee does not use the caller's memory directly. Instead, it copies the entire array into its own stack frame on entry — a copy-on-entry pattern that provides value semantics.

Copy-on-Entry

The callee's prologue allocates a frame, then copies each element from the caller's pointer into the callee's frame. After the copy, the parameter local is overwritten with the callee's frame address:

(func $sum_array (param $arr i32) (result 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
  ;; --- 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. Any mutations the callee makes to arr (if it is declared mut) affect 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

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.

Why Value Semantics

The alternative to copy-on-entry is reference semantics — the callee reads and writes the caller's memory directly. Reference semantics would be faster (no copy) but introduces three problems:

1. Breaks the mut system: A function receiving arr: [i32; 3] (not mut) could still mutate the caller's array through the pointer, violating the type system's guarantee.

2. Breaks referential transparency: If f(arr) can modify arr, then f(arr); g(arr) and g(arr); f(arr) may produce different results. Value semantics ensure function calls are independent.

3. Complicates formal verification: Rocq proofs with value parameters model function calls as substitution — the callee operates on a fresh copy. Mutable references require heap effect reasoning and aliasing analysis, dramatically increasing proof complexity.

Inference optimizes for provability, not performance. The copy cost is acceptable.

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 one remaining difference is the borrow checker: a &[i32; 3] reference can be passed without copying because the borrow checker guarantees no aliasing. Inference does not have a borrow checker, so it always copies.

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.

The copy-on-entry semantics for parameters are particularly beneficial for verification. In Rocq, a function f(arr: [i32; 3]) can be modeled as taking a Vector.t int32 3 argument by value. The proof does not need to reason about aliasing, mutation through shared pointers, or frame conditions on the caller's state. The callee's array is a fresh value, independent of the caller's.

Zero-Initialization as a Proof Obligation

The unconditional zero-initialization via memory.fill in the prologue 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.

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.

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 directly. The compiler emits bare arithmetic instructions with no additional guards. There is no compile-time overflow detection and no runtime overflow check.

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_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. Inference does not emit truncation or masking instructions after arithmetic on sub-i32 types. The WASM i32.add instruction operates on the full 32-bit value, and the result is stored back as a 32-bit local. This means that arithmetic on i8 variables can produce results outside the range -128..127 without any compiler-inserted truncation.

This is a known gap tracked in the project. A complete implementation would emit i32.extend8_s or a masking sequence after arithmetic on sub-i32 types. The current behavior matches C's integer promotion rules (arithmetic is done in the promoted width) but does not truncate back to the sub-type width on store.

Division and Modulo

Division and modulo instructions are emitted without compiler-added guards. The div_s (MIN, -1) trap and the division-by-zero trap pass through as WASM traps. When triggered, a runtime environment will report an unhandled WASM trap.

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_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

The type-checker or a future constant-folding pass could evaluate constant expressions at compile time and report an error when the result overflows. For example, const x: i8 = 200 could be flagged at compile time because 200 exceeds i8::MAX (127). This does not require runtime guards — it is purely a front-end diagnostic.

This is already tracked as a known gap: the current type-checker accepts let a: i8 = 200 without error. A literal range validation pass would catch this class of overflow without touching codegen at all.

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

A correctness-oriented future change is to emit truncation after arithmetic on sub-i32 types. For i8 addition, the correct sequence is:

local.get $a     ;; i8 stored as i32
local.get $b     ;; i8 stored as i32
i32.add
i32.const 0xff   ;; mask low 8 bits
i32.and
i32.extend8_s    ;; sign-extend from 8 bits (requires sign-ext proposal)

Without this truncation, i8 variables can hold values outside -128..127 after arithmetic. The current behavior matches C's promotion rules but not the semantic expectation of a typed language with distinct i8 and i32 types.

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: A core/analysis/ crate will enforce that all non-void functions return on every code path, producing a compile-time error for violations.
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/inference/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/inference/src/project.rs.

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
spec LibSpec {
    fn obligation() -> i32 {
        return 2;
    }
}

// main.inf
use lib::checks;

spec EntrySpec {
    fn obligation() -> i32 {
        return 1;
    }
}

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/inference/src/project.rs — parse_project, discover_files, 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"
# 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.

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()

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

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;
}

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
    |
    +-- discover_and_load(Inference.toml)
    |
    +-- find_infc()          # INFC_PATH > system PATH > managed toolchain
    |
    +-- compatibility handshake
    |       infc --commit-hash    # short-circuit: same-build binaries always compatible
    |       infc --abi-version    # major mismatch → hard error; minor mismatch → warning
    |
    +-- spawn infc
            CWD = <project root>
            arg: src/main.inf
            arg: --mode proof           (if effective proof mode)
            arg: -v                     (if .v requested)
            arg: --out-dir <dir>        (if effective proof mode + ABI ≥ 1.1)
            arg: --wasm-dep name=path   (one per [wasm-dependencies] entry)
            arg: -L <dir>               (repeated for each --wasm-lib-dir)

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

Note: The current ABI version is 1.1.

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.1 (COMPILER_ABI_MAJOR = 1, COMPILER_ABI_MINOR = 1 in core/compiler-interface/src/lib.rs). The --out-dir flag was introduced at minor 1. infs gates its use: --out-dir is forwarded only to an infc that reports ABI minor ≥ 1 (or matches by commit hash). 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. System PATH (which infc).
3. The managed toolchain directory (~/.inference/toolchains/<version>/infc).

INFERENCE_HOME overrides the managed toolchain root (default ~/.inference).

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 front-end validation step (validate_extern) reports a SignatureMismatch error before any code is generated.

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 from the extern_name_to_idx table built during the pre-scan phase.

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:

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:

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.

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

Sign-extension (i32.extend8_s, i64.extend32_s, etc.) and saturating float-to-int (i32.trunc_sat_f32_s, etc.) are also excluded: the Rocq translator has no lowering for either, and Inference codegen emits neither.

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 and bulk memory (memory.copy/memory.fill).

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

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.