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 — why +, -, * and unary - trap, what wrapping(...) restores, and what either means for proofs.
• Unreachable Emission in Codegen — why the compiler emits a trailing unreachable in non-void functions.
• Compilation Targets — compile vs. proof modes and the supported backends.

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

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

A third group covers the toolchain outside the batch compiler:

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

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

Building this book

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

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

Source for every chapter lives under book/src/.

The Inference Parser

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

Overview

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

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

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

The design follows two references closely:

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

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

The pipeline

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

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

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

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

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

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

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

Crate layout

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

Stage 1: the lexer

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

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

Three properties matter:

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

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

• Prefix-position negative numbers. A leading - is part of a number literal when it is immediately followed by a digit and no expression has just ended, so -42 lexes as a single Number token, not Minus then Number. The lexer keeps a one-token lookbehind (prev_significant, ignoring trivia) and consults the EXPR_END token set for that second condition: after a, 1, ), ], @ and the other kinds an expression can end with, the - is subtraction, so v-1 lexes as three tokens. } is deliberately not in that set — it closes a block as well as a struct literal, and a statement may open with a negative literal, as in if c { } -1;. (- 42, with a space, lexes as two tokens and parses as a unary negation; analysis rule A046 then rejects that spelling, so the glued form is the only way to write a negative literal.)
• Reserved-but-not-keyword identifiers. constructor, proof, and uzumaki lex as ordinary identifiers, matching the grammar's reserved-identifier rule.
• unit is a keyword no position accepts. The unit type is spelled (), and unit lexes as its own UnitKw so the grammar can refuse the word by name rather than read it as an identifier naming a type nothing declares. Where a type is written, the parser reports that the unit type is spelled () and completes the node () would have produced, so lowering sees the unit type and nothing after the parser has more to say. Where the position says what a name names — a declared binding, parameter, field, function, struct, enum, variant, constant, spec, type alias or type parameter, a module path segment, an imported item, the last segment of a type path with no type arguments — it reports what the word tried to name. Where it does not — a reference in an expression such as return unit;, s.unit or unit::k(), which may name a module, a type, a function, a field or a value, and inside a type the base of a generic name, bare or at the end of a path, and an array size — the identifier rule every name reaches reports only that the word cannot be used as a name. In every case the word is consumed as the name, which is what keeps one misuse to one diagnostic: a keyword a position does not expect is otherwise read as whatever the rule wants next, and cascades. Only the whole word is reserved; units and unit_count are ordinary identifiers.

Stage 2: SyntaxKind and TokenSet

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

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

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

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

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

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

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

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

Stage 3: the event-based parser

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

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

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

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

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

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

Expressions: Pratt parsing

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

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

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

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

Disambiguations the parser handles explicitly

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

• -42 vs - x vs v-1 — resolved in the lexer by the one-token lookbehind (prefix-position negative numbers, above).
• :: and ' immediacy — only treated as a path separator / generic terminator when the joint bit says there is no intervening whitespace.
• Struct literal { vs block { — S { a: 1 } is a struct literal, but in an if/loop condition a { opens the body. The expression parser threads a no_struct flag through condition parsing to forbid struct literals there.
• Contextual keywords — self, type, from, and spec are keywords only in the rules that introduce them; wherever a rule reaches the identifier rule they are ordinary names, remapped to Ident (so self.type = … and spec::Auction::new() parse, and fn type() { } declares a function). Two identifier positions are the exception, decided by a dispatch on the bare Ident token before that rule is reached: a parameter name and a struct-field name refuse all four spellings. type is the odd one of the four: the language has no type-alias declaration, and its rule exists only to consume type Name = T; and refuse it, so the token stays contextual for the sake of every other position it can appear in — and the refusal is gated on that declaration's type <name> head, so a statement the rule receives for any other reason is not blamed on an alias.

Stage 4: the owned CST

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

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

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

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

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

Stage 5: lowering to the AstArena

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

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

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

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

Error recovery and the never-panic guarantee

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

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

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

The fuel + advance guard. A resilient LL parser can, if a rule is written incorrectly, loop forever by retrying a recovery path that consumes nothing. The parser borrows matklad's safeguard: a fuel counter (const FUEL: u32 = 256, a Cell<u32>) is decremented on every lookahead and refilled whenever real progress is made — a token is bumped, or a node is completed that the cursor has moved through since it was opened, which is how a deep parse unwinding at end of input closes its frames. Closing a node opened at the cursor is not progress: a recovery that reports an error and closes its node without consuming the token it could not use would otherwise be retried by its loop forever, each round refilling the fuel it spent. An assertion fires (in debug and release) the moment fuel hits zero, turning a would-be infinite loop into an immediate, localized crash during development rather than a hang in production. On well-formed grammar rules the guard never trips; it is a backstop, not part of normal control flow.

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

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

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

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

Testing and verification

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

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

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

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

Performance

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

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

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

Summary

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

References

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

Static Analysis in Inference

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

Why Analysis Exists

The Inference compilation pipeline is:

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

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

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

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

Why Formal Verification Demands Stricter Control Flow

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

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

Fundamental Principles

Rule Independence

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

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

Severity Model

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

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

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

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

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

Exhaustive Collection

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

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

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

Diagnostic Format

Diagnostics follow the GCC/Clang/rustc convention:

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

A concrete example:

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

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

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

Data Flow

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

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

The rule! Macro

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

Syntax

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

Each pseudo-attribute has a specific role:

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

What the Macro Expands To

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

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

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

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

The __severity! Helper

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

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

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

Why a Macro Rather than a Derive

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

Complete Example: A001

The full source of the simplest rule in the codebase:

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

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

The Shared Walker

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

walk_function_bodies and for_each_function_body

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

for_each_function_body handles all definition kinds:

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

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

Depth Tracking

WalkContext carries four fields through the traversal:

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

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

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

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

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

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

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

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

Why dyn FnMut

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

A004: Custom Traversal

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

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

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

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

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

Current Rules

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

Control flow and termination

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

Uzumaki placement

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

Compound values (structs and arrays)

Compound values live in linear memory, not on the WASM value stack (see Memory Allocation). Every rule in this family fences off a position where a compound value would need to materialize without a named destination to own its memory. A045 is the family's odd rule out in mechanism rather than in subject: a field-less struct occupies zero bytes, so it fences off every position that would need to hold a value of it — literal, binding, parameter, return, field, self receiver — rather than one unsupported expression shape. Declaring such a struct, and using it as a pure method namespace, stays legal.

Values and indexing

A022 exists because a value that could never round-trip through its declared type is a mistake wherever it is written, whatever the operators around it do — the rule closes the front door on it (see Arithmetic Overflow). Its premise is unaffected by checked(...), which changes what an operator does with a result and never what a literal means: a literal outside its type's range is out of range under either annotation and under none. A037 turns a guaranteed runtime trap into a compile-time error when the index is statically known. A044 closes the same front door as A022, aimed at a shift's count operand rather than an assigned or compared value: WebAssembly's runtime shift already takes the count modulo the operand's bit width, so x << 32 on an i32 silently becomes x << 0, and A044 rejects a statically-known literal count outside 0..width as a program error instead of letting it fold to a value the source never wrote. Dynamic and const-declared counts are out of its scope, the same statically-known-literal boundary A022 draws.

A052 is the compile-time half of the overflow trap. +, -, * and unary - trap when their result leaves the operand type, so an operation whose operands are known before the program runs and whose result does not fit is not a value at all: it is a trap taken on every run that reaches it, and no envelope or specification recovers it. Literals, function-body const bindings, parentheses, annotations and nested arithmetic fold; a let binding and a call do not, since neither carries a value this rule may assume. An operator inside a wrapping(...) is exempt and folds modularly — after this rule that spelling is the only way left to write a constant that wraps. An operation with an operand A022 already owns is skipped, through the shared predicate both rules read, so let x: u8 = 300 + 1; is one finding about one literal rather than two about the same mistake. A forall-quantified specification body and an unquantified one are turned into obligation terms and never lowered, so nothing written in them ever runs and the rule skips them; an exists/unique body is compiled and reduced, so it is examined like any other. The overflow the issue this rule came from opened with — a fixed-point multiply whose product leaves i64 — is not one of its findings: those operands are parameters, and nothing folds.

A053 and A054 are the two ways to write an arithmetic-mode annotation that does nothing, split by severity because they are different mistakes. A053 is a typo: there is no +, -, * or unary - inside the annotation for it to govern. Two shapes account for nearly every instance, and the message names both because neither is visible from the site the rule fires on — a call, since wrapping(mix(s)) annotates the call and the annotation does not reach into mix's body, and a glued negative literal, since -2147483648 is one token carrying its own sign rather than a negation applied to a value. It is an error because no default makes it right: the annotation is somewhere other than where it was meant to go, and a checked(...) that governs nothing reads as a guarantee no guard backs. A054 is the redundancy — the mode named is already the mode in force — and it is a warning because which spelling is redundant is decided by the language's default rather than by the expression. The comparison is against the enclosing effective mode, so checked(a * wrapping(b + c)) is redundant nowhere, and a stack of same-mode annotations reports its outermost member once, the convention A048 and A049 already use.

A056 is the other half of A037. Every array access whose index is not a bare literal carries a runtime guard (index >= length -> unreachable), and a trap is a halt rather than a recovery, so A056 requires the program to make that guard unreachable itself: a value-range analysis has to prove, from the code the programmer wrote, that the index lies in 0..length on every run that reaches the access. An out-of-range index is then a path the program handles — an else, an early return, a loop's exit — and never an implicit trap:

if i >= 0 && i < 8 { r = arr[i]; } else { r = -1; }

The analysis follows the language's structured control flow directly, with no control-flow graph: an if joins its arms, a loop iterates to a fixpoint at its head, a break carries its state to the loop's exit. Facts come from the conditions of if and loop, from the left operand of a short-circuiting && or ||, from initializers, and from the arithmetic applied since, modelled as the code generator emits it — a checked + that did not trap produced the mathematical sum, a wrapping(...) one that can leave its type can be anything. So the common shapes need no annotation: a counter that starts at 0 and only grows is proven by its loop condition without a written i >= 0, i % 8 and k & 7 are bounded by their right operand, and a u8 index into a [T; 256] is proven by its type alone. A signed index guarded only from above is not, because the guard's unsigned compare would trap on a negative one. Only a plain local is narrowed by a condition; an index read from a field or an element is proven by its type alone, so the fix is to bind it to a local and guard that.

An assert proves nothing for A056: it establishes its condition only by halting when the condition is false, which is the outcome the rule exists to rule out. A057 closes the matching path on the other side of a guard — an assert that fails on every run reaching it, such as assert(false) in the else of a bounds check — since that is an unconditional halt written as a check. Both rules are intraprocedural, because the language has no preconditions: a parameter can hold any value of its type, and a function that indexes with one guards it itself. A specification's envelope does not stand in for that guard, since it describes only the calls the specification makes. By default the runtime guard stays in every build; A056 proves it dead rather than removing it. A project that sets [build] bounds-checks = "omit-proven" has code generation omit the guard of every access A056 proves, trading that second layer of protection for size and speed (see Omitting proven guards).

Language restrictions

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

A048 and A049 belong to the not-yet-supported half, and each replaces an abort rather than an obscure failure. string and String are registered as builtin type names, so every annotation that spells one type-checks — and nothing after the type checker can act on it: there is no layout for a string in linear memory, no WebAssembly type to pass one in, and no term for a proof to describe one with. A049 draws a narrower line, between the absence of a value and a value of nothing. The first is what the unit type is for and is fully implemented, so -> () and an omitted return type both stay legal, as do return;, return (); and a bare (); statement. The second — a unit binding, parameter, struct field or array element — is a declaration the compiler cannot honour, because a unit value occupies no bytes and has no WebAssembly type, so there is no slot for it to arrive in and nothing for a binding to store. Both rules look through array nesting at any depth, and both descend into spec bodies, which proof mode lowers to real WebAssembly functions. Each is deleted the day its feature lands.

A050 is permanent, and its argument is the one A033 and A046 make: a concept should have one spelling. The grammar admits name: T, _: T and a bare T, and on a function with a body the third says strictly less than the second while occupying the same slot — it binds no name for the body to read, labels no argument at a call site, and where _: T deliberately declares a present and unused parameter, a bare T states nothing at all. external fn keeps the bare form, because an extern declares an ABI signature with no body to read a parameter in, so a positional type is a complete statement of it.

Only one of A051's two halves belongs to the not-yet-supported family. A function declaring type parameters is a promise the backend cannot keep: the type checker infers a type argument at each call site and checks the body against it, and nothing carries that substitution any further, so a binder reaches code generation still standing for no type — no layout to size a frame slot with, no WebAssembly type to pass a value in, no term for a proof to describe one with. That half is deleted the day monomorphization lands, which is tracked in issue #76. A type application — Q i32' written as a parameter, return, field or binding type, or standing on its own in expression position — is not waiting on anything: no type declaration in Inference takes type arguments, since a struct, an enum and an external fn each declare a bare name and only a function binds one, so Q i32' names no declaration at all. That half survives monomorphization and must not be deleted with the first. The rule reads a declaration's declared binders and nothing else, with no reachability filter and no entry-point carve-out, because every narrowing leaves a real defect standing: a binder appearing in no lowered type is uncallable — nothing can infer it — yet was still emitted, exported, and in proof mode shipped a complete obligation with the binder discarded, and a binder shadowing a declared type was read as the parameter by the type checker and as the type by code generation, which emitted a module WebAssembly validation rejects. A type position is looked through array nesting at any depth, and an expression is descended to any depth. A function type is refused for its own reason, with or without a type parameter in it.

External function write-through

A linked external shares the program's single linear memory, so a compound (struct or array) argument at its call boundary is not copied at all: the callee receives a raw pointer into the caller's own frame, and the foreign body may store through it. mut on an external fn parameter is the declaration that this may happen (see External Functions and WASM Linking), and the linker checks the claim against the merged bytes at link time. That makes this the one place in the language where a write to a binding is invisible in source — the store lives in a .wasm the type checker never reads — so A047 requires the call site to carry the statement instead: a struct or array argument at a mut position must be rooted at a mut binding, exactly as an assignment through that binding would require. A scalar argument is out of A047's scope, deliberately: a scalar passes a value rather than a region, so there is no binding at the call site for the rule to check, and the documented external fn store_at(mut ptr: i32, val: i32); idiom is unaffected. This is an accepted gap, not an absence of risk: the shadow stack occupies [0, stack_size) of the very same linear memory a scalar i32 addresses, and under the default layout — one page, entirely stack — a caller's own frame sits just below address 65536, so store_at(65528, 7) overwrites that caller's own locals through a plain i32.store. The linker admits it, because Tier B's derivation proof does not bound where a parameter-derived address lands, only that it derives from a parameter; A047 stays silent, because a scalar carries no binding for it to check. The exemption is kept anyway, to preserve the book's own external fn store_at(mut ptr: i32, val: i32); idiom — the declaration still has to say mut, because the linker's write-set check is type-agnostic; what the exemption buys is that the call site is not held to a mut binding, since the argument is an integer rather than a region. Closing the gap the exemption leaves open is tracked in issue #420.

Target limits

A055 measures a program against the runtime it is built for rather than stating a property of the source alone — as A036 does against the shadow stack the build emits — and it is the one rule that reads the build target. SpaceWasm's interpreter counts a function's parameters in four-byte words — two for an i64 or u64, one for any other type, a struct or an array being passed as its address — and keeps the count in a single byte, so it refuses to load a module whose function declares more than 255. The build's post-link conformance check (see Compilation Targets) has always refused such a module, but it can only name the finished module's function and a number. The rule asks the same question of the source, underlines the declaration's parameter list, and itemizes where the words went: so many for so many parameters of each type, one for a self receiver, and one for the hidden pointer a struct or array result is written through — the word the parameter list does not show. The count is the signature code generation emits, held to it by a differential test over the corpus against the conformance checker's own reading of each module. A build for any other target is not measured, and neither is a spec, which a compile-mode build strips, or an external fn, which is an import. A function a linked module brings in is left to the post-link check, which is the only place its words exist.

The editor measures a file for the target its project's Inference.toml names under [build] target, so a spacewasm project shows A055 where it is written (see The Language Server).

Static memory footprint

An Inference program allocates nothing at run time, so everything it will ever hold in linear memory is known before it runs: the shadow stack at [0, stack-size), and directly above it the static data region — the bytes of every array and struct module constant a function reads, written once by an active data segment when the module is instantiated. These two rules together prove that the program can never need more memory than it declares (Power of Ten, Rule 3): every call chain fits the stack, and the stack and the data fit the pages the module is guaranteed at instantiation.

The type checker computes every module constant and lays the region out; the build's memory layout places it. A stack the build did not size keeps its default 64 KiB when the memory has room for the data above it and otherwise gives up exactly the part the data needs, rounded to the 16-byte frame grid — so a program with a few constant tables builds in the default page without a [memory] table, and A036 measures its call chains against the smaller stack. A stack-size the build asked for is never shrunk. A058 fires when the data leaves a default stack less than one frame, or when a requested stack and the data together need more than the pages hold. Both rules read the same placement code generation emits, so the stack they measure is the stack the module declares.

Both findings say what makes up the footprint and how to fix it, in the manifest's spelling and the command line's (infs forwards the manifest as flags, so the compiler cannot tell which one the build used):

error[A036]: maximum stack depth main -> work -> alloc uses 98304 bytes, exceeding the 65536-byte stack by 32768 bytes; reduce array/struct frame sizes along this call chain
note: its frames are 32768 bytes for `main` and 65536 bytes for `alloc`
note: the stack is the default 65536 bytes, the whole of the 1-page memory
help: or give the stack the 98304 bytes it needs: `stack-size = 98304` and `pages = 2` under `[memory]`, or `--stack-size 98304 --memory-pages 2`

error[A058]: the program's constant data does not fit in linear memory: the 65536-byte shadow stack and 4100 bytes of static data need 69636 bytes, 4100 more than the 1-page (65536-byte) linear memory holds
note: the constant data is 4000 bytes for `TABLE`, 96 bytes for `lib::LUT` and 4 bytes of alignment padding
help: raise the memory to 2 pages: `pages = 2` under `[memory]`, or `--memory-pages 2`
help: or lower the stack to at most 61424 bytes, which still holds the deepest call chain's 1024: `stack-size = 61424` under `[memory]`, or `--stack-size 61424`

The suggested layout is computed by MemoryLayout itself, so it is never one the build would refuse, and following it clears the finding. A036's frame sizes are upper bounds of the frames code generation allocates, so a suggestion can over-ask but never under-ask. A058 is anchored at the first constant that no longer fits, in the file that declares it, and names the largest constants by the path the entry file would use for them.

What lies outside these rules is not a static allocation: the bytes a host writes into memory for an exported function's compound parameters, and the stores an admitted Tier-B external makes through a pointer it is handed (see The WASM Linker). Neither is allocated by the program.

Advisory rules

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

Adding a New Rule

Decision: Shared Walker or Custom Traversal?

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

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

Step-by-Step Recipe

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

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

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

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

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

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

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

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

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

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

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

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

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

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

Related Resources

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

Memory Allocation in WASM Codegen

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

The Problem

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

Three allocation strategies are available:

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

Inference uses option 3 for every array a function owns. Those 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.

Option 1 is the right one for exactly the case it fits: a module-scope const array or struct is immutable and lives for the whole run, so its bytes go in the module's data section, directly above the stack (see Module Constants and the Static Data Region). Option 2 is never used: a heap's failure modes are exactly what the static footprint check exists to rule out.

Linear Memory Layout

WebAssembly linear memory is a contiguous byte array. By default Inference allocates one page (64 KiB) and uses it as a stack, less whatever the program's module constants need at its top:

Linear Memory (1 page = 64KB)
+--------------------------------------------+  0x10000 (65536)
|                                            |
|     (free space)                           |
|                                            |
+--------------------------------------------+  STACK_SIZE + data
|     static data: module constants          |
|                                            |
+-- __stack_pointer -------------------------+  STACK_SIZE (65536 without constants)
|                                            |
|         Stack (grows downward)             |
|                                            |
+--------------------------------------------+  0x00000
  overflow below 0 = WASM OOB trap

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

Configuring the layout

The layout above is the default, not a constant. A project sets it in the [memory] table of Inference.toml, and a direct infc invocation with the matching flags:

Any key may be given alone; the others keep their defaults, and the three numbers are checked together as the layout they complete to. The stack must fit in pages, and be a multiple of the 16-byte frame alignment. Directly above the stack lies the static data region, and above that, up to the end of memory, ordinary addressable memory that nothing the compiler emits reads or writes. The whole memory is exported, so a host reads a program's values in place — an array a program hands to a host import arrives as the address of the caller's copy, inside the stack region.

The memory is fixed unless a build sets max-pages above pages: the memory section (or the memory import) declares min == max, so memory.grow can never move the end of memory. Nothing the compiler emits grows memory; a larger maximum is room for the host to grow into or, in a module that defines its memory, for a linked module to, and the linker refuses a module that grows memory against a fixed one. The maximum is always a number — there is no unbounded memory — and the spacewasm target refuses a growable one outright, because its interpreter is loaded with memory.grow disallowed.

A configured layout is declared even by a program whose own code touches no memory. Otherwise the module would have no memory for the layout to describe, and linked modules that address memory would bring their own: the linker builds a memoryless program's memory from those modules' declarations — one module's exactly as declared, several modules' as the tightest fit to all of them (see The Shared Linear Memory) — so the size and maximum the build asked for, a bound included, would silently give way to the libraries'. Configuring a layout is also how a program settles libraries that disagree: its own maximum then governs every one of them, and the linker names, in a warning, each library that grows memory and declares a maximum other than the program's (or none), since growth there now stops at the program's. The default layout is still emitted only when something uses it, and one page that may grow to one page is the default, so max-pages = 1 alone declares nothing. A layout that imports its memory is never the default, however its numbers read: every such program imports one, so what a host has to supply does not depend on what the program uses.

The overflow trap constrains the maximum. A wrapped stack pointer lands at 2^32 - stack-size or above, and must land past the end of memory to trap, so the memory at its maximum and the stack must fit the 32-bit address space together: max-pages × 64 KiB + stack-size ≤ 2^32. The check is made against the maximum rather than the size because growth moves the end of memory up to it. A layout that breaks it is refused when the manifest loads or the flags are read.

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 — or when the build configures a layout other than the default, as above, or imports its memory (see Importing the memory). Existing programs produce identical WASM output — zero regression.

Importing the memory

By default a module defines its linear memory, and whatever runs it gets the memory the module declares. An embedder that owns the memory its modules run in can ask for the opposite. [memory] import = true in Inference.toml, or infc --import-memory, has the emitted module import its memory as env.memory instead of defining it, and the host supply it. The key is a boolean and defaults to false; import = false is the same as leaving it out. The import takes its limits from the layout above, and the stack and the static data region are placed in it exactly as they are in a defined memory. The name is fixed — no key renames it — and is the one wasm-ld --import-memory imports a memory under by default, so a host that already supplies memory to modules built that way needs no new name for this one.

Take this program, built with [memory] pages = 2 and import = true:

external fn clock_ms() -> i64;
use { clock_ms } from host::env;

const TABLE: [i32; 3] = [10, 20, 30];

pub fn at(i: i32) -> i32 {
    if i >= 0 && i < 3 { return TABLE[i]; }
    return 0;
}

pub fn now() -> i64 {
    return clock_ms();
}

The memory declaration, the stack pointer, the exports and the data segment of the module it emits read:

(import "env" "memory" (memory (;0;) 2 2))        ;; the host's memory: memory 0
(import "env" "clock_ms" (func (;0;) (type 0)))   ;; function imports follow it
...
(global (;0;) (mut i32) i32.const 65536)          ;; still defined by the module
...
(export "memory" (memory 0))                      ;; a re-export of the host's memory
(export "__stack_pointer" (global 0))
...
(data (;0;) (i32.const 65536) "\0a\00\00\00\14\00\00\00\1e\00\00\00")

No (memory …) is defined. The data segment is the ordinary active segment of Module Constants and the Static Data Region, and instantiation now writes TABLE into the host's memory.

The limits. The import declares the layout's pages as its minimum and max-pages as its maximum, which is pages unless the build raised it, as a defined memory would. The maximum is always declared, and the memory is 32-bit and unshared. WebAssembly import matching then admits a host memory only if it has at least pages pages and declares a maximum of its own that is at most max-pages: a memory with no maximum, and a shared memory, do not match, and instantiation fails. That is what keeps the overflow-trap rule of Configuring the layout true of a memory the module did not create. The headroom max-pages × 64 KiB + stack-size ≤ 2^32 is measured against the maximum because growth moves the end of memory up to it, and a host can never hand over more than max-pages pages; an import without a maximum would admit a memory of any size, and a wrapped stack pointer could then land inside it instead of trapping. The minimum is pages, the least a host can supply, which is what the stack and the static data region are placed in and what A058 checks them against.

What else changes, and what does not. The memory import is the first import, ahead of every function import. Imported memories precede defined ones, so it is memory 0, the memory every load and store addresses, and the function index space counts function imports only, so no function index moves. __stack_pointer is still a defined global, initialized to the stack size and exported as __stack_pointer, and memory is still exported as memory 0, now a re-export of the host's own memory object. It follows that whenever the defined-memory build of the same program declares a memory, every section but Import and Memory is the same bytes in both builds: the import-mode Import section is the memory entry followed by the defined build's entries, and no function, global or custom-section index differs. tests/src/codegen/wasm/memory_import.rs holds the two builds to that relation across array, struct, constant, host-import, overflow-checked and omitted-guard programs, at the default, a growable and a small-stack layout, and then runs the builds under wasmtime against a memory the test creates.

One program is the exception. A program that touches no memory, at the default layout, has a defined build with no memory, no stack pointer and neither export. In import mode it still imports env.memory and defines and exports the stack pointer and memory, because a layout that imports its memory is never the default; the type, function, code and custom sections are still the defined build's.

A runnable example. inference-host-memory-demo is a small project built with import = true and max-pages = 4. Its browser walkthrough creates the memory, hands an Inference program sensor readings through host functions, and reads the two arrays the program reports in place, at addresses inside that memory. It then grows the memory up to the program's four pages while the program runs, shows the engine refusing a fifth, and lets the reader offer memories the import does not admit. It also embeds the module in a second WebAssembly program that shares the memory: that program keeps to the pages above the module's, answers its host calls itself, and reads its results by address, with no JavaScript between the two. Two Node.js scripts run the replay and the embedding from a terminal and check their results.

The embedder contract

WebAssembly import matching checks the memory's type — its limits, and that it is unshared, 32-bit and of the default page size — and nothing about its contents or how the host uses it. The first rule below is enforced by that check; the others are rules the embedder keeps, because the module cannot check them when it is instantiated.

1. Supply a memory the import admits. It has at least pages pages and a maximum of its own no greater than max-pages. For the program above, which imports (memory 2 2), a JavaScript host writes:

   const memory = new WebAssembly.Memory({ initial: 2, maximum: 2 });
   const { instance } = await WebAssembly.instantiate(bytes, {
     env: { memory, clock_ms: () => BigInt(Date.now()) },
   });
   

   and a Rust host using wasmtime's API writes:

   use wasmtime::{Engine, Linker, Memory, MemoryType, Module, Store};
   
   let engine = Engine::default();
   let module = Module::from_file(&engine, "out/main.wasm")?;
   let mut store = Store::new(&engine, ());
   
   let memory = Memory::new(&mut store, MemoryType::new(2, Some(2)))?;
   let mut linker = Linker::new(&engine);
   linker.define(&store, "env", "memory", memory)?;
   linker.func_wrap("env", "clock_ms", || -> i64 { /* read the clock */ 0 })?;
   let instance = linker.instantiate(&mut store, &module)?;

   The memory is registered as env.memory, beside the host functions the program binds. A memory with no maximum, a shared memory, one with fewer than pages pages, or one whose maximum exceeds max-pages makes the engine refuse the instantiation with an incompatible-import error that names the import. The default layout imports (memory 1 1), so its host supplies exactly one page with a maximum of one.

2. Leave the module's pages alone, except where a call hands you an address. The module owns the first pages pages: its shadow stack occupies [0, stack-size) and its constants lie directly above it. In the program above the stack fills the first page and the twelve bytes of TABLE start the second. The host may read these pages — a struct or array argument reaches a host function as the address of the caller's copy, inside them — but writes nothing there, with one exception: during a call to one of the host's functions, it may write through an argument declared mut, at the address it is handed, and through no other. Every struct or array the host itself places in memory lives above the module's pages: a struct or array a host function returns, which it returns as an address the module reads the value from, and the addresses it passes to an exported function that takes a struct or array or returns one. That memory exists only when max-pages exceeds pages: the host supplies a memory with more than pages pages up front, or grows it. The default one-page layout therefore leaves the host nothing, and so does the program above, whose maximum is its two pages; under such a layout the contract admits only exports that take and return scalars, and only host functions that return scalars. The rest of the first pages pages is memory the compiled code does not touch today, but the layout does not set it aside for the host either.

3. Do not write the constants. Instantiation writes the static data region into the host's memory, over whatever the memory held there, and nothing the program does writes it again. A later host write into the region changes the program's constants: TABLE[i] is a load from that address. A host need not zero the memory first: today the module reads no byte of its region that it has not written, which An Imported Memory Has No Proof Artifact says more about.

4. Give each instance a memory of its own. Every instance puts its shadow stack at address 0 and its constants directly above it. Two instances on one memory — two instantiations of one module, two Inference modules, or a host-import callback that calls into a second instance on the same memory — overwrite each other's stack and constants.

5. Leave __stack_pointer alone. It is exported, which is useful to a test harness, and it is the module's own state: every frame is carved from it, so a host write relocates the next frame to an address the host chose.

6. Expect no layout negotiation. The layout is stack-first at address 0, so the module claims the bottom of the memory. Inference has no counterpart of wasm-ld's --global-base, so the base cannot be moved. Sharing one memory between several modules is not a goal of this mode.

Targets, proof mode, linking and tooling

• Targets. wasm32 only; every other target refuses it before the program is parsed. stellar never supports it: a Soroban contract defines and exports the memory it uses, and the value-ABI rewrite every stellar artifact goes through accepts no import, so a contract importing env.memory could not be deployed (see Stellar). spacewasm does not support it yet: the interpreter can bind a memory its embedder registers, but this toolchain does not build for one, and the F´ reference hosts infs run provides register functions only; building for an imported memory at that target is tracked under issue #547 (see SpaceWasm). Both refusals name the setting to remove, and Target::supports_imported_memory() is the predicate they share.
• Proof mode. A module that imports its memory has no proof artifact. Every build that writes a .v is refused — infc --mode proof, -v and --mode compile -v, and infs build with -v, --mode proof or a manifest's [build] mode = "proof", which infs build --mode compile overrides — because the proof contract instantiates a module on its own, with an empty import list. An Imported Memory Has No Proof Artifact says what a proof of the defined-memory build does and does not cover.
• Linking. A program that binds a module through [wasm-dependencies] (or --wasm-dep, --wasm-lib-dir or INFERENCE_WASM_LIB_PATH) cannot import its memory: the static merge models only a memory its modules define, not one a host supplies, and the build is refused before external resolution (tracked under issue #546; see The WASM Linker and The Link Step). Host imports are a different matter and work beside the memory import, with one exception: a host binding imported as env.memory, which the build refuses, because an embedder that resolves each import by its module and field name alone, as the JavaScript API and wasmtime's Linker do, cannot supply a function and a memory under one name. Bind that function from another host module (see Host Imports).
• The toolchain. infs build echoes the layout as memory: 2 page(s), maximum 2, 65536-byte stack, imported from env.memory or, when the maximum exceeds the size, memory: 1 page(s) growable to 4, 65536-byte stack, imported from env.memory, and refuses an infc older than ABI 1.11 when the manifest sets import = true; import = false forwards nothing and gates nothing. [build.wasm-opt] output that adds, removes, renames or changes the limits of the memory import fails the build, leaving the compiler's artifact in place, and infs never passes Binaryen --zero-filled-memory, since a host memory is not zero-filled. infs run supplies the memory itself, because the wasmtime CLI supplies none, and still refuses an artifact that imports a function (see infs run).

Module Constants and the Static Data Region

A const declared at the top of a file is computed by the type checker, once, under the program's own arithmetic: a checked + that would overflow, a division by zero, a shift by the width or an index past the end refuses the build at that operation, since the program would trap there. What code generation emits for it depends on its type:

• A scalar constant — an integer, a bool, an enum — is an immediate at every use, exactly the instruction its literal would be. It occupies no memory.
• An array or struct constant that some function, method or specification reads is laid out as bytes of the static data region, in source order, each at its natural alignment, with the layout a frame slot of its type has. One active data segment writes the whole region at STACK_SIZE when the module is instantiated, and a read of the constant is i32.const <address>, where a compound binding's read would be local.get of its slot address — so indexing, field access, copying and passing it as an argument lower exactly as they do for a binding. A compound constant only another constant's initializer reads is folded into that constant's value and takes no bytes.

const TABLE: [i32; 3] = [10, 20, 30];
pub fn at(i: i32) -> i32 { if i >= 0 && i < 3 { return TABLE[i]; } return 0; }

(memory (;0;) 1 1)
(global (;0;) (mut i32) i32.const 65520)          ;; the stack gave up 16 bytes
...
  i32.const 65520                                 ;; TABLE's address
  local.get 0
  ...                                             ;; bounds guard, then index
  i32.load
...
(data (;0;) (i32.const 65520) "\0a\00\00\00\14\00\00\00\1e\00\00\00")

Nothing ever writes the region. The type checker refuses an assignment rooted at a constant, however the constant is named — an item import included. A binding initialized from one receives a copy of its bytes, a callee that writes a compound parameter copies it into its own frame first, a returned constant is copied through the result pointer, and A047 refuses a constant at a mut parameter of an external fn. A host can write the exported memory, which is outside what the program controls, as it always was.

The stack makes room. A stack the build did not size keeps its default 64 KiB when the memory has room for the data above it, and otherwise gives up exactly the part the data needs, rounded down to the 16-byte frame grid. A program with a few constant tables therefore builds in the default page with no [memory] table, and A036 measures its call chains against the smaller stack — naming the constant data in its note when that is why the stack is below 64 KiB. A stack-size the build asked for is never shrunk: the data has to fit between its top and the end of pages, which A058 checks, naming the constants and offering either more pages or a smaller stack that still holds the deepest call chain. The data is measured against pages, not max-pages, because it is written at instantiation, before any growth.

Analysis and code generation read one placement, computed by the type checker, and place it with one function, MemoryLayout::with_static_data. That is what makes the stack A036 measures the stack the module declares.

Stack Frame Layout

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

Consider a function with two arrays:

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

The frame layout computation:

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

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

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

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

Function Prologue and Epilogue

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

Prologue

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

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

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

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

Epilogue

The epilogue restores __stack_pointer to its pre-call value:

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

The epilogue is emitted at two sites:

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

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

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

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

Array Literal Lowering

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

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

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

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

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

Store Instruction Selection

The store instruction depends on the element type:

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

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

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

Repeated Array Literals

A repeated array literal [value; N] is an array of N copies of value, typed [T; N]:

let zeros: [u8; 64] = [0; 64];
let points: [Point; 8] = [Point { x: 1, y: 2 }; 8];
let grid: [[i32; 3]; 4] = [row; 4];

The count is an integer literal of at least 1, the same rule as the size in [T; N], and @ cannot appear in the value: the value is evaluated once, so [@; N] would draw one value for every element. A non-deterministic array is written @ for the whole array.

The lowering stores value once into element 0, with the same stores a one-element list would emit, and then fills the rest by copying the filled prefix onto the next stretch of the array, doubling it each time: element 0 to element 1, elements 0–1 to 2–3, 0–3 to 4–7, the last copy taking only what remains. [x; 13] takes four copies (1, 2, 4 and 5 elements), and an array of N elements takes ceil(log2 N). Each copy is between two disjoint regions, so it is the ordinary region copy the compiler emits for any compound value: a single memory.copy when the build enables bulk memory, otherwise straight-line loads and stores for a short region and a loop for a long one. A repeat whose value is zero at every leaf emits nothing at all when it initializes a binding, because the prologue has already zeroed the frame.

Array Index Read

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

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

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

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

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

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

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

Load Instruction Selection

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

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

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

Array Index Write

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

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

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

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

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

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

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

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

Array Parameter Passing

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

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

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

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

When a Copy Is Emitted

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

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

2. It reaches an external fn argument whose declaration marks any parameter mut. A linked external shares the program's single linear memory and receives a compound argument as a raw pointer, so its body can store through that pointer. mut on one of the external's declared parameters is the statement that this may happen (External Functions and WASM Linking), and the linker checks the claim against the merged bytes at link time, rejecting a body that stores where its declaration did not permit. A parameter that flows to such a call keeps its copy — and it keeps it for every position the call reaches it at, not only the mut one: the gate decides per external, not per parameter, because narrowing further would rest on a containment property the linker's provenance proof does not establish (see The WASM Linker). A parameter that reaches only externals declaring no mut parameter at all is passed by reference like any other unwritten parameter — the linker requires such a closure to record no store anywhere, so eliding the caller's copy is unobservable.

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

Note what decides each half of this, because the two halves are decided differently. Whether the body assigns through the parameter is still a fact about the body alone: the mut marker on an Inference parameter is a contract with the type checker — it states whether the function is permitted to assign through the parameter, and a program that assigns through a parameter declared without it is rejected — but it is not itself the input to this decision, so a mut parameter the body never assigns through is passed by reference exactly like a non-mut one. Deciding on the marker instead would mean that dropping a mut a function does not need makes the program faster, putting the annotation's cost in opposition to its purpose. Whether the parameter reaches a writing external, by contrast, is a fact about that external's own declaration: codegen reads the callee's mut markers, because the merged .wasm body itself is bytes the compiler never sees — there is no body to scan the way there is for an Inference-level assignment. Neither lowering is observable from Inference source, so there is no reason to write a program one way rather than another in order to obtain one of them.

By-Reference Parameters

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

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

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

Copy-on-Entry

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

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

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

This can be verified with the verify_copy_semantics test:

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

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

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

Copy Optimization

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

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

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

Receivers and Linked Externals

A method receiver is a parameter, and the rule above is the whole rule for it too. A method that assigns through self copies the receiver on entry; a method that only reads it does not, whether the receiver is written self or mut self. Forwarding an immutable receiver to a mut external fn position is a different matter, covered next.

The external case is the one place where a write is invisible in Inference source: linking merges every module into one linear memory, a compound external fn parameter is lowered to a raw i32 pointer with no copy between the call site and the foreign body, and the foreign body is free to store through that pointer. mut on an external fn parameter is the declaration that this may happen, and the linker checks the claim against the merged bytes at link time — a body that stores where its declaration did not permit fails to link. Because such a write can be invisible in source, the language does not let it happen to a binding that never said it could change: passing a struct or array argument — or any projection of one, such as self.field or arr[i] — to a mut external parameter requires the projection's own binding (the receiver or the parameter it is rooted at) to be mut itself, enforced at the call site by analysis rule A047. An immutable self or an immutable compound parameter can therefore no longer be forwarded to a mut external position at all. Codegen's copy rule follows the same declaration: a parameter that reaches an external declaring any mut parameter keeps its copy (see When a Copy Is Emitted); one that reaches only externals declaring no mut parameter at all does not, since the linker then requires the closure to record no store anywhere. The linker's side of this arrangement — the write set it derives from the merged bytes, and precisely what it does and does not prove about where a declared store lands — is described in The WASM Linker.

Why Value Semantics

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

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

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

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

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

Arrays in Non-Deterministic Blocks

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

Uzumaki Arrays

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

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

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

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

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

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

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

Individual array elements can also be assigned uzumaki values:

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

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

Comparison with Other Compilers

LLVM / Clang to WASM

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

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

Rust to WASM

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

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

Zig to WASM

Zig also uses --stack-first layout when targeting WASM, placing the stack at low addresses so overflow naturally traps. Inference matches this layout. Zig zero-initializes local arrays (matching Inference's memory.fill approach). Zig's safety modes add bounds checks on array access under a build mode; Inference emits its bounds guard in every build, proof mode included, because the artifact a proof is written about has to be the artifact that ships. A project can opt out of the guards its analysis proved dead ([build] bounds-checks = "omit-proven", below), and that choice too applies to both modes alike.

WASM Section Layout

When has_memory is true, or the build configured a non-default layout or imports its memory, the compiler emits three additional sections in the WASM module, and a fourth when the program reads a compound module constant:

These sections are ordered according to the WASM specification: Type, Import, Function, Memory, Global, Export, Code, Data, Name, where the Import section is present only when the module imports something and the Memory section only when it defines a memory. The ordering is mandatory — a misordered module fails validation. No DataCount section is emitted: it is required only by memory.init and data.drop, which nothing emits, and the SpaceWasm interpreter cannot decode one.

When no function uses arrays and the layout is the default, these sections are omitted entirely. The output is byte-identical to what the compiler produced before array support was added. A layout that imports its memory is never the default, so it emits its memory import, its stack pointer and both exports even for a program with no arrays; see Importing the memory.

Formal Verification Implications

This section is about a module that defines its memory. A module that imports it has no proof artifact: see An Imported Memory Has No Proof Artifact at the end of the section.

Modeling Arrays in Rocq

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

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

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

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

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

Zero-Initialization as a Proof Obligation

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

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

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

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

Bounds Checking as a Proof Obligation

Array index access is bounds-checked: a literal out-of-bounds index is rejected at compile time (analysis rule A037), and any other index emits a runtime guard (index >= length -> unreachable). The guard is emitted in every build, Proof mode included, so the artifact a proof is written about is byte-for-byte the artifact that ships.

The line between the two halves is narrower than "constant" suggests. Code generation folds a direct number literal and nothing else, so arr[3] needs no guard while arr[K] for a const K — and arr[1 + 1] — take the guarded path. A037 draws its line in the same place, wanting the literal directly under the access.

Every guarded access must also be proven in bounds before the program compiles (analysis rule A056): a value-range analysis has to show, from the code the programmer wrote — an enclosing if or loop condition, an early exit, the index's initializer and arithmetic — that the index lies in 0..length on every run that reaches the access. The guard is therefore dead in every accepted executable function, an out-of-range index is a path the program handles rather than a trap, and a named or computed constant out of range is rejected statically. By default the guard stays anyway: it is what an analysis bug would fall back to, and the Rocq obligation below is stated against it. See Static Analysis.

That guard is what makes the bound provable. A proof-mode dynamic access used to lower to a bare BI_load/BI_store carrying no side condition, leaving the emitted .v with nothing to be about; it now lowers to the guard, and the guard is a trap the Rocq contract can already see.

The obligation that forces the bound is one the contract already had, not a new predicate. HA_app_ok f τs — the assertion a bare call statement in a specification body emits — denotes that the interpretation is defined at f(τs), and realizing that claim requires proving fun_computes, which is stated through a total-correctness judgment: the body must reduce to a value stack, never to a trap. So claiming a call is realized is claiming its body does not trap, and a body containing the guard cannot be trap-free unless the index is in range at every access. A specification that declares its envelope with assume and then calls the function therefore carries 0 <= i < array_length as a real, dischargeable obligation.

Omitting proven guards

A project can choose to give that second layer up. Under [build] bounds-checks = "omit-proven" in Inference.toml (infc --bounds-checks omit-proven), code generation omits the guard of every access A056 proved in bounds, identically in compile and proof mode. The default, "all", keeps both layers: an access is safe if the range analysis is right or the guard runs, and the guard always runs. Opting out makes the proven accesses rest on the analysis alone, which changes three things:

• The failure mode. A flaw in the range analysis, or a mismatch between what it assumes and what code generation emits, would read or write the neighbouring linear memory instead of trapping. The WebAssembly sandbox still holds, and an address past the end of memory still traps, but data inside it can be silently corrupted.
• What is trusted. Memory safety at a proven access rests on the range analysis and on code generation agreeing with it, rather than on a five-instruction check whose correctness is evident.
• The proof. At an omitted guard the .v carries no index <u length side condition, so the realization obligation above no longer re-establishes the bound: A056 discharged it from the source, and is what is trusted for it.

What it buys is size and speed. Across the 18 corpus modules that index dynamically, the policy removes 60 guards and 736 of 31,591 bytes (about 2.3%), and each removed guard is a compare and a branch per access at run time, which matters only in loops that index. A guard stays wherever there is no proof, under either policy: in a forall body a proof build compiles, and at an access A056 accepts only because no run reaches it.

The choice is recorded in the artifact. A module built under omit-proven lists the functions that lost a guard in its inference.bounds_elided custom section; the static merge linker rewrites that list into a merged module, so a project that keeps every guard and links a library that did not still says so in the module it ships, and infs marks the list opaque after [build.wasm-opt] renumbers the functions it names. tests/src/codegen/wasm/bounds_elision.rs runs every corpus program under both policies side by side and compares results, traps and memory; that makes an analysis flaw less likely to reach an omit-proven build, but it checks only the programs it runs, and does not give back the guarantee the guard gives every program.

Extending ValidModule with a blanket "no reachable trap" clause would not have worked, and it is worth saying why. ValidModule is structural well-formedness — WasmCert's module_typing — and reduces nothing. More decisively, unreachable is emitted from six sites in seven roles, and in two of them trapping is the mechanism rather than a defect: an ordinary executable assert, whose entire purpose is to trap when its condition is false, and every reachability filter in a retained specification body, which the judgment counts on to discard the choice vectors the specification rejects. A blanket clause would make assert unusable in Proof mode and falsify every reachability obligation at once. The bounds guard, the narrow signed-division overflow guard, an exported entry's enum tag guard and the overflow guard on a +, -, * or unary - are the opposite case — a conditional trap whose condition is a property worth proving — and a value-returning function's dead tail is neither, since analysis rule A007 is what keeps it unreached. Trap-freedom belongs where a programmer asks for it, per call, which is what HA_app_ok gives.

One shape is refused rather than obligated: a non-constant index inside an exists/unique body (diagnostic P016). Those bodies are the ones the reachability judgment reduces, and it fixes an arbitrary typed entry vector before the choices range — so an entry whose index trips the guard leaves an empty observation set and makes the theorem false rather than narrower. P016 folds the wider notion of constant, so a[K] passes it and is then guarded anyway by the narrower one; that guard is dead, because the same pass has already checked K against the array's declared length — the length the guard compares against.

Two elisions have been proposed, and they are not the same proposal. Issue #215 drops the guard of a particular access proven in bounds, and is the omit-proven policy above: the guard it removes is dead, the range analysis A056 runs is exactly the proof it needs, and the decision reads the source, the proof and the project's policy but never the mode, so the artifact a proof is written about is still the one that ships. What it gives up is the fallback, which is why it is a choice rather than the default. Dropping a live guard in the deployed build on the strength of a module having been proven is #214's own step 3, left unimplemented: it would trade away the property described above, since the artifact that ships would no longer be the artifact that was proven, and no mechanism for it exists today — there is no proof-status type, attestation, or manifest key to stand behind it.

The full statement lives in core/wasm-to-v/ROCQ_CONTRACT.md.

An Imported Memory Has No Proof Artifact

A layout that imports its memory (Importing the memory) is refused in proof mode, at every target, and infc writes no .v for it. The Rocq contract gives an obligation over memory, globals, calls, exists or unique a runtime to speak about by instantiating the module on its own, with an empty import list (see Obligations only an import-free module can discharge). A module importing env.memory cannot be instantiated that way, so every such obligation over it would be a theorem no proof can discharge, and the build refuses to write the .v rather than hand a prover an unprovable goal.

A project that wants a proof and an imported memory builds the proof from the defined-memory build of the same program, at the same numbers, and ships the other. This is open only to a program that binds no host import: infc refuses a .v for every host-import program, whichever way it holds its memory, so for one there is no proof to carry over. infs build has no per-build override for [memory] import, so a project builds the proof with the key set to false (or removed), or runs infc without --import-memory. Whenever the defined-memory build declares a memory, the two modules differ only in their Import and Memory sections, but a proof of the first is a statement about that module running alone, in a memory it created, and the second is not run that way. The proof carries over only if both of these hold:

• The host writes nothing in the module's region — its stack and its constants — for as long as the instance exists. The proof's memory is written by the module and by nothing else; a host that writes the region is a writer the proof does not contain. The embedder contract states the rule from the host's side.
• Compiled code never reads a byte of its region before its instance has written it. The proof starts from a memory the module created and the semantics zeroed, while a host memory holds whatever the host left in it. Today this holds because the prologue zero-fills every frame unconditionally and the data segment covers its whole region, padding included, and the module tests run their programs against a memory filled with 0xAA as well as a zeroed one.

Neither premise is a theorem. Both are documented here and not proved, and if either fails, the proof of the defined-memory build says nothing about the module that ships.

Current Implementation

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

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

Arithmetic Overflow in WASM Codegen

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

Inference does not pass that behavior through. +, -, * and unary - trap when the result leaves the operand type, and wrapping(e) is how a program asks for the machine's answer instead: it makes every one of those operators written between its parentheses wrap. checked(e) names the other direction, which is what an operator no annotation encloses already does. Checked and Wrapping Arithmetic is the surface, the guard shapes it emits, and what a proof can say about them. The lowering examples before it are the wrapping ones, and each carries the annotation that selects them.

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

A +, -, * or unary - written inside a wrapping(...) inherits WASM's semantics: it emits the bare arithmetic instruction with no overflow guard. Everywhere else — which is everywhere the source has not asked for the wrap — the same operator emits a guard sequence that traps instead, in both compilation modes; see Checked and Wrapping Arithmetic. The lowerings shown in the rest of this section are the wrapping ones.

Division stands apart from both spellings — signed division overflow (MIN / -1) traps at every width whatever encloses it, natively for i32/i64 and via a compiler-added guard for the narrow types (see Division and Modulo). Separately, a dynamic (runtime-index) array access and a failing assert emit their own runtime traps.

Binary Expression Lowering

lower_binary_expression in core/wasm-codegen/src/compiler.rs dispatches to the appropriate WASM instruction based on the left operand's type. Where the operator's effective mode is wrapping it emits that instruction and nothing else:

;; Inference: return wrapping(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. Drop the annotation and this particular expression never reaches code generation: both operands are constants and the sum leaves i32, which analysis rule A052 refuses. Written over values the compiler cannot fold, the same addition compiles to a guard and traps.

Negation Lowering

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

;; Inference: return wrapping(-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 — the one input at which negation has no representable result, and the one input an unmarked -x traps on. This is verifiable against the golden WAT output in tests/test_data/codegen/wasm/arith_overflow/arith_overflow.wat:

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

Unsigned Types and Bit-Pattern Reinterpretation

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

Unsigned literals use .cast_signed() in lower_number_literal:

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

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

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

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

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

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

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

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

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

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

The current behavior therefore matches C's integer promotion rule (arithmetic is done in the promoted width) and truncates back to the sub-type's width immediately afterward, so a sub-i32 local never holds a value outside its declared range. Where the operator is guarded rather than wrapping, this re-narrowing is also the overflow test: the guard runs it, compares, and traps exactly when it would have changed the promoted result — see The guard shapes.

Division and Modulo

Division overflow traps at every width, and unlike the four arithmetic operators it does so under either annotation and under none: checked(...) and wrapping(...) never govern / or %. Divide-by-zero and remainder-by-zero pass through as native WASM traps at every width, and so does signed division's single overflow case, MIN / -1.

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

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

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

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

Exported ABI Parameter Guards

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

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

Checked and Wrapping Arithmetic

checked(e) and wrapping(e) are prefix expression forms that fix how the arithmetic written inside e behaves on overflow. checked(e) makes every +, -, * and unary - between its parentheses trap when the mathematical result leaves the operand type; wrapping(e) makes them compute the result modulo two to the power of the width, which is what the bare WebAssembly operator does. The expression has the type of e.

Both words are reserved. Nothing in a program may be named checked or wrapping — not a variable, a constant or a function, not a struct field, a method or an enum variant, and not a source file, whose stem becomes a module path segment.

What an annotation governs

The rule is lexical and it is about the parentheses. An annotation reaches the +, -, * and unary - written between its own, and no others:

• They nest, innermost first. In checked(a * wrapping(b + c)) the multiply traps and the addition wraps. The inner annotation restores wrapping inside a region the outer one had made checked.
• They do not reach into a callee. wrapping(f(x)) annotates the call, not f's body, which keeps whatever its own source says. This is the mistake authors of hashes, mixers and pseudo-random generators make most often, so the compiler rejects an annotation with no operator to govern outright (analysis rule A053) rather than letting it read as a guarantee nothing backs.
• A negative number is one token, not a negation. -2147483648 carries its own sign, so wrapping(-2147483648) governs no operator and is the same A053 error.
• /, %, the shifts and the bitwise operators are never governed. Signed division traps on its own at the one quotient a width cannot hold, % cannot overflow at any width, and a shift discards the bits it moves out by definition.
• The inner expression may be any scalar. checked(a + b > c) is a boundary shape authors write, and the bool the comparison yields is a fine thing to annotate — the arithmetic being governed is inside it. A struct, an array, a unit value or a function has no arithmetic to govern and is a type error.
• A const initializer is an ordinary expression. const SCALE: i32 = wrapping(2147483647 + 1); is how a wrapped constant is written.

An operator no annotation encloses has the language's default mode, which is checked. wrapping(...) is therefore the opt-out — the one way to ask for the machine's own answer — and a checked(...) that no wrapping(...) encloses names the mode already in force and changes nothing. That is reported as a warning (A054) rather than an error, because which spelling is redundant is decided by the default rather than by the expression.

The guard shapes

A guarded operator is emitted inline: the operation, then a test of what it produced, then unreachable on the failing side. Nothing is factored into a helper function, because a synthetic function would renumber every index an obligation names its callee by.

There is no wider width to compute a candidate result in — an i64 product has nowhere to be checked — so each row saves its operands or its result in a scratch local and recomputes the question from those. The scratch is one shared pool per function, reserved before the body is emitted and holding at most three slots per width class present; a function whose governed operators are all inside a wrapping(...), or that has none, reserves nothing.

Each width class the pool holds costs a further 2 bytes of locals declarations. The figures are instruction bytes over the same source with the operator written wrapping(...). There is no unsigned negation row because there is no unsigned negation: -x at a u32 is a type error, not an operation that could overflow.

Four things about that table are worth a sentence each.

Multiply is checked by dividing back. There is no wider width and no conversion opcode in the emitter's vocabulary, so the product is recovered by r /s b and compared against a. That check has two inputs it must not be handed: b == 0, where the division traps, and (a, b) = (MIN, -1), where the division would reach WebAssembly's own integer overflow trap. Both arms are therefore explicit and both come before any division runs. Without the b == -1 arm the multiply would still refuse the overflow, but by the wrong trap.

Narrow widths are cheap because the promoted value is still there. An i8 operator runs at i32 and is re-narrowed afterwards, so overflow is exactly "re-narrowing changes the result". The guard runs the same re-narrowing every narrow operation already ends with and leaves its value behind, which is why the lowering site does not emit that re-narrowing a second time.

Every guard traps through unreachable. That is a design constraint, not an accident of the shapes: the Rocq contract enumerates the roles BI_unreachable is emitted in, and a guard that reached a native trap instead would be a trap kind that table does not describe. The execution matrix over the catalogue asserts the trap kind for exactly this reason.

The annotation and the default are two spellings of one thing. wrapping(e) emits what the operator emitted before either keyword existed and nothing else, and checked(e) emits what an operator with no annotation around it emits. Both directions are pinned by compiling one source under each fallback and comparing bytes, which is also what makes the figures above measurable: each is the difference between one module and the module the same source produces with wrapping(...) written around the operator. The catalogue fixture is the case in point: it writes wrapping(...) only where a row needs modular arithmetic to be about something else, and every other guard in it comes from the default alone.

Here is the signed + row as the golden emits it at i32:

local.get $a
local.get $b
local.set 3      ;; keep b
local.tee 2      ;; keep a
local.get 3
i32.add
local.tee 4      ;; keep r
local.get 2
i32.lt_s         ;; r <s a
local.get 3
i32.const 0
i32.lt_s         ;; b <s 0
i32.ne           ;; the two disagree exactly when the sum overflowed
if
  unreachable
end
local.get 4

Both modes, and no dial

A guard is emitted in Compile and Proof mode alike. Nothing gates it on the mode, because the Rocq translation has to describe the program that ships: a proof-mode-only guard would be a proof about a module nobody runs, and a compile-mode-only one would be a module nobody proved. The same reasoning rules out a build setting: which operator a + b denotes is a property of the language, so it is absent from the compiler's options, the CLI, the manifest and the infs↔infc ABI. One source compiles to one program.

The reproducer

Q20.20 fixed point multiplies two scaled numbers and divides the product back by the scale. At 4194304000 the true product needs 64 bits it does not have:

pub fn fixmul(a: i64, b: i64) -> i64 {
  const ONE: i64 = 1048576;
  return a * b / ONE;
}

pub fn run() -> i64 {
  const H: i64 = 4194304000;
  return fixmul(H, H);
}

run traps. Write the multiply as wrapping(a * b) and it returns -814970044416 for a true value of 16777216000000, which is the failure mode this design exists to end. The language cannot compute the right answer here — there is no wider type, no cast and no widening multiply — so what the guard buys is a loud failure in place of a quiet wrong number.

What a proof can say about it

An overflow guard is the trap site that makes a no-overflow claim expressible, and HA_app_ok — the atom a bare call statement in a specification body emits — is what carries it. Downstream that atom unfolds to total correctness: the callee's body must reduce to a value stack, and a trapped run reduces to AI_trap instead. So a forall specification that bounds its operands with assume and then calls fixmul states exactly that no admitted pair overflows:

spec OverflowRealization {
  fn fixmul_is_realized() forall {
    let a: i64 = @;
    let b: i64 = @;
    assume { assert(-3037000499 <= a && a <= 3037000499); }
    assume { assert(-3037000499 <= b && b <= 3037000499); }
    fixmul(a, b);
  }
}

The guard is the whole of what makes that claim informative. Over a fixmul whose multiply is written wrapping(a * b) the emitted obligation is byte-for-byte the same text and is unconditionally true: with no trap in the callee every argument pair reduces to a value, and each conjunct of the envelope can be ignored. An HA_app_ok over wrapping arithmetic constrains nothing about overflow, and its silence must not be read as coverage.

The envelope is exact rather than generous. 3037000499 is the largest N with N² inside i64, and an i64 declaration contributes only a width to the obligation, never a range, so the assume is the sole source of the bound and both halves of each pair are load-bearing. core/wasm-codegen/docs/specification-obligations.md sets out the emitted obligation and how it is read.

Two positions refuse arithmetic rather than proving anything about it, both in specification bodies. A forall or plain body becomes an obligation term, whose +, - and * are the modular machine operators with no second operator downstream for an annotation to select, so either annotation there is refused (P017, first wording) instead of being silently dropped. An exists- or unique-quantified body is the opposite case: it is compiled and the judgment reduces it, so an operator whose effective mode traps puts a trap on the path being reduced, which makes the theorem false rather than narrower — refused by the same code's second wording, with wrapping(...) accepted throughout as the remedy. Because the judgment reduces callee activations too, a retained body that reaches a guarded function through calls is refused as well (P018), and a merged body a library supplied is judged the same way at link time.

Read together: a forall body states a claim and is never run, so its arithmetic is the wrapping operator and cannot be annotated; an exists or unique body is run by its own judgment, so its arithmetic has to say which operator it is.

Trap attribution at run time

Every trap this compiler emits reports the same thing. A bounds check, a narrow division guard, a failing assert, an exported entry's enum tag guard and an overflow guard all surface as wasm trap: wasm 'unreachable' instruction executed, and no WebAssembly mechanism distinguishes them at the instruction level short of DWARF, which this compiler does not emit.

What is available is function-level attribution, for free. The compiler emits a name section, so a wasmtime backtrace names the function that trapped and gives a code offset within it. The recipe is: read the frame name from the backtrace, then disassemble that function and look at the offset. Note that [build.wasm-opt] strips the name section, so an optimized artifact gives you an index instead of a name.

Letting an overflow guard reach WebAssembly's native integer overflow trap would produce a better message for free, and it is deliberately not done: that would add a trap shape the Rocq contract's role table does not describe, which is a poor trade for a string.

Comparison with Other Languages

Inference's default is Rust's debug behavior and Zig's safe-mode behavior, with the difference that no build profile takes it away: there is no release mode in which the same source stops trapping. Its spelling of the escape is closest to Zig's +% and Rust's wrapping_add — both behaviors are written down, and neither is reached by a build setting — but it scopes the choice to a parenthesized expression rather than to an operator or a method call, which is the only form available in a language with no methods on primitives and no width-generic functions. It also differs from every row above in that the choice is not a safety switch: a proof is what the trap is for, and What a proof can say about it is where that cashes out.

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, over the same signed-addition predicate Inference's own row uses — the sum's sign disagrees with the sign the addend predicted:

;; Conceptual structure of a debug-mode signed overflow check for i32 + i32.
;; Actual rustc output goes through a two-result MIR operation and block
;; layout that this flattens; the predicate is what carries over.
local.get $a
local.get $b
i32.add
local.tee $result
local.get $a
i32.lt_s          ;; r <s a
local.get $b
i32.const 0
i32.lt_s          ;; b <s 0
i32.ne            ;; the two disagree exactly when the sum overflowed
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

Which of two jobs a proof faces is decided by the source, not by the prover:

1. Where the operator is guarded, prove that no overflow can occur — typically by establishing bounds on the inputs.
2. Where it is written wrapping(...), account for the wrap: the result is defined, so the proof is possible, but it may be unexpected.

The first is the ordinary case. A function that receives an i32 parameter and returns param + 1 traps at i32::MAX, so a specification that calls it has to bound the argument below i32::MAX before the claim that the call is realized can close — and if that bound is missing or too wide, the claim is false rather than weaker. Written wrapping(param + 1) the function cannot trap, and what a proof has to discharge instead is result == (input + 1) mod 2^32, a different and weaker statement about the function's behavior.

Overflow Checks as Proof Obligations

Inference treats a checked overflow check as both things at once: a runtime trap in the shipped binary, and the site an obligation is about. The obligation is not per operation and not a separate channel — it is HA_app_ok at a call, which the contract already carried for bounds. What a proof can say about it has the mechanism; three properties of it are worth stating here, because each rules out a design a reader might expect.

The guard is emitted in both modes, not synthesized in proof mode. A design in which compile mode emits bare arithmetic and proof mode generates an obligation would have the verifier describe a different program than the one that ships, which is precisely what the toolchain's byte-identity rule exists to prevent. The obligation says something about overflow only because the artifact it describes really traps.

The claim is per call, not per operation. Obligations are keyed by specification function, and the only carrier that speaks about a body's behavior is the application. So a function nobody names in a specification gets its trap and no theorem, and overflow is proved absent only at the argument vectors some specification actually named.

Discharging it means proving the guard unreachable, which needs a bound. The programmer supplies that bound as an assume envelope over the operands. Where the bound is missing or too wide, the obligation is not weaker — it is false, and it will not close.

Current Implementation Details

Arithmetic lowering is in core/wasm-codegen/src/compiler.rs, and the guard catalogue it consults is core/wasm-codegen/src/overflow_guard.rs. There are exactly two source-level arithmetic lowering sites — the binary expression and the prefix unary one — which is what keeps the annotation's reach tractable: the several dozen other add/sub/mul emissions in the crate are frame, offset and index arithmetic reached through different code paths, so they are never inside an annotated expression and are excluded by construction rather than by a predicate.

overflow_guard::guard_kind is the single classifier. Both lowering sites ask it what to emit, and the pre-body pass that reserves the scratch pool asks it what to reserve, so a body cannot reach a guard whose scratch was never reserved.

lower_binary_expression dispatches on the left operand's TypeInfoKind using is_i64_type() and is_unsigned_type(). Where the effective mode is wrapping it emits a single WASM instruction with no surrounding guards:

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

lower_prefix_unary_expression handles negation as 0 - x:

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

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

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

The boundary suite is tests/src/codegen/wasm/arith_overflow.rs, and it carries eight cases twice. i32::MAX + 1, i32::MIN - 1, i64::MAX + 1, i64::MIN - 1, u32::MAX + 1, i32::MAX * 2, -i32::MIN and -i64::MIN are each written once with wrapping(...) over constants, asserting the modular value, and once over parameters with no annotation, asserting that the call traps on the vector its twin wraps at. Parameters are what makes the second half writable at all: a constant whose result leaves its type is refused by A052 before code generation, and the golden path runs analysis.

The guarded half is tests/src/codegen/wasm/checked_arith.rs, over a fixture carrying one exported function per catalogue row plus the reproducer. Its execution matrix runs each row at its boundary vectors and asserts the trap kind rather than merely that a trap occurred — the vector that makes that necessary is (MIN, -1) at a signed multiply, which is the one an unguarded round-trip check would fail through the machine's integer overflow trap instead. It also pins the vectors that must not trap, 2^62 * -2 landing exactly on i64::MIN among them.

Limitations and Open Questions

Reaching a Value the Language Cannot Compute

A guard turns a wrong answer into a trap; it does not produce the right one. The reproducer above needs the high half of a 64-by-64 product, and there is nothing in the language to hold it: no type wider than i64, no cast operator, and no widening multiply. An author who needs that value has to change the algorithm, not the annotation.

The narrow types are the same shape of problem at the other end. i8 and u8 arithmetic reaches its boundary early, and Rust's escape of widening each operand is unavailable — two different types never combine, and there is no cast to reach a wider one. Declare the arithmetic at the width the result needs; narrow types are for storage and boundaries.

Constant Folding and Compile-Time Detection

An operation whose operands are known before the program runs can be evaluated at compile time and reported there when the result overflows. That needs no runtime guard: it is purely a front-end diagnostic, and it is the compile-time half of the trap.

Both halves are closed. Analysis rule A022 (Literal out of range) rejects let a: i8 = 200 at compile time, because 200 exceeds i8::MAX (127) and the value could never round-trip through its declared type. A052 (Constant arithmetic overflow) takes the computed case: let a: i8 = 127 + 1; is refused, because both operands fold and the sum leaves the type it is performed at, so the operation is not a value the program computes but a trap it takes on every run that reaches it. Literals, a body's const bindings, parentheses, annotations and nested arithmetic fold; a let binding and a call do not. An operator inside a wrapping(...) folds modularly and is exempt, which after this rule makes wrapping(127 + 1) the only way to write a constant that wraps. What stays outside the front end is everything that does not fold — a parameter, a let binding, a value a call returns — and for those the emitted guard is the only answer. See Static Analysis.

Overflow Checks in Non-Deterministic Blocks

The framing this section used to carry — that checks would have to be stripped from spec blocks and preserved in proof mode — describes a compiler that no longer exists. A forall or plain specification function has no compiled body to strip anything from: it becomes an obligation and is left out of the module's function list entirely. What replaced the question is three rules, and each is about a different body.

A body that becomes a term cannot be annotated (P017, first wording). That covers forall and plain bodies, and a value-returning fn declared inside a spec block, which is translated into an obligation of its own. The obligation's +, - and * are the modular machine operators and there is no other operator downstream for the annotation to name, so both spellings would translate identically. They are refused rather than dropped in silence. The range belongs in an assume envelope over the operands, and the arithmetic whose overflow you want proved absent belongs in the executable function the specification claims the realization of.

A retained body's arithmetic must be wrapping (P017, second wording). An exists- or unique-quantified body is compiled, and its judgment reduces it. A trap on the path being reduced empties the observation set at the entry that reaches it, so the theorem becomes false rather than narrowed — and in a unique body it is worse than false, because a trapping choice shrinks the successful set and can make a uniqueness claim hold for a reason the source never states. wrapping(...) is accepted throughout such a body and is the remedy.

A retained body may not reach a guard through a call (P018). The judgment reduces callee activations too, so a guard one call deep is the same trap. The walk uses code generation's own call resolution, re-scoped at each hop, counts a callee it cannot resolve as guarded, and skips external fn callees — the compiler never sees a dependency's bytes. A merged body is judged instead at link time, off the inference.checked section each input carries.

Sub-i32 Truncation

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

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

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

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

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

Unreachable Emission in Codegen

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

That function-tail instruction is one of seven roles unreachable is emitted in, and it is the only one this chapter is about. The others are an ordinary assert, a reachability filter inside a retained specification body, a dynamic array access's bounds guard, a narrow signed division's overflow guard, an exported entry's enum tag guard, and the overflow guard on a +, -, * or unary -. They cannot be told apart by looking at the instruction, which matters to anyone reading a trap at run time and to anyone writing a proof about a module: core/wasm-to-v/ROCQ_CONTRACT.md § Trap-freedom enumerates all seven and says which of them a proof obligation can usefully range over. The distinction that section draws is between a trap that is never meant to be reached and a conditional trap whose condition is a property worth proving; the function tail is the first kind, and the four guards are the second.

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 (() return type, or none), no value is expected on the stack at end, so the unreachable is omitted.

WASM Specification Rationale

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

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

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

How the Validation Algorithm Works

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

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

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

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

Compatibility with WASM proposals

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

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

How Production Compilers Handle This

rustc (Rust)

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

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

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

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

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

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

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

LLVM / Clang (C/C++)

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

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

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

GCC

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

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

Zig

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

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

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

Binaryen

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

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

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

Formal Verification Perspective

Mechanised proofs

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

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

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

CompCert analogy

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

Impact on WASM-to-Rocq translation

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

Why the Alternatives Are Worse

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

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

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

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

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

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

Cost Analysis

Security Context

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

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

Inference's Approach

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

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

Compilation Targets

Compilation Matrix

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

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

compile mode: Produces production binaries. 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 a single WASM module for wasm_to_v Rocq translation, preserving the specification code that compile mode strips. The non-deterministic constructs do not survive into the module: a forall-quantified (or plain) spec function becomes an hassert obligation and is omitted from the module record altogether, while an exists- or unique-quantified one is retained with a vanilla body — each scalar @ becomes a hidden trailing choice parameter, and each assume/assert a trap-on-false filter. What proof mode does preserve is source order and shape: statements lower in the order written and the compiler applies no optimization pass to reshape them, so a retained body reads against its source and there is no optimization barrier to insert. Execution functions are byte-for-byte identical to what compile mode's release profile emits for the same source, so Rocq proofs cover the artifact that actually ships. 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: every other target supports compile mode only, because the custom 0xfc instructions proof mode is made of are decodable by no runtime but our own tooling. Build profiles (debug/release) do not change proof mode's output — only the OptLevel value it records, which today changes no emitted byte either way (see Appendix A below).

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.

Both spellings of a Rocq request are refused at --target stellar: --mode proof (and a bare -v, which implies it) because the target cannot decode the instructions proof mode emits, and --mode compile -v because the .v would describe the module before the value-ABI rewrite while the .wasm beside it is the module after. See Stellar below.

At --target spacewasm only the first of those is refused. --mode proof and a bare -v fail for the same reason as at Stellar, but --mode compile -v succeeds and writes the .v a wasm32 compile-mode build writes, character for character — there is no rewrite for the translation to run ahead of, because the two builds are the same module. See SpaceWasm below.

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 (however it was built, and by whatever compiler produced it). The spec code requires structural identity for Rocq readability, which the compiler gives it by lowering it 1:1 from source rather than by withholding an optimizer that does not otherwise run. Execution code — whether from Inference source or external modules — is exactly the bytes that will run, so Rocq proofs cover the actual deployed artifact.

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

Produces a deployable Soroban smart contract for the Stellar network, selected with infc --target stellar or [build] target = "stellar" in an Inference.toml.

The value ABI

A Soroban host does not call a contract method with its declared WebAssembly parameters. Every method takes and returns Val: a 64-bit word whose low byte is a tag naming what the rest of the word holds. add(a: u32, b: u32) -> u32 therefore reaches the host as (i64, i64) -> i64, not as (i32, i32) -> i32.

The compiler does not emit that convention. Code generation is target-blind — the module it produces for Stellar is the module it produces for wasm32, byte for byte — and the value ABI is applied afterwards, to the linked artifact, by a rewriter. Per exported method the rewriter appends one wrapper function that unwraps each argument, calls the original body, and wraps the result; the export section is retargeted onto the wrappers, and every existing function keeps its index and its bytes. That ordering is the whole point of the design: the module you prove is the module you deploy, minus a marshalling shell that contains no arithmetic, no memory access and no control flow beyond one guard per argument.

An argument whose tag is wrong traps. It is worth knowing what that looks like from the caller's side: a wrong tag, a wrong argument type and an out-of-range boolean all produce the byte-identical host report WasmVm, InvalidAction / "VM call trapped: UnreachableCodeReached". A caller cannot tell which argument was wrong, or that the problem was a type at all. The contract's contractspecv0 section carries that information for tooling (see Invoking a contract from the CLI below), and the build log summarizes it: infc prints one summary line naming each method and its value arity:

Stellar contract: add/2, flip/1, nothing/0; env protocol 20; 558 bytes

That size includes the three contract sections the rewriter appends, not just the wrappers.

What an exported function may declare

An exported function is a contract method, and a contract method is confined to the scalars the convention encodes without a host object:

Everything else is refused at code generation, before any byte exists, naming the function and the offending element. The refusals differ because the reasons do:

• A 64-bit integer (u64, i64): "…the host's word is 64 bits wide and spends part of it on a tag, so no 64-bit value fits in one, and it travels as a host object built through host functions this target refuses to import, their call convention not being bound here yet — issue #324."
• A narrow integer (u8, i8, u16, i16): "…the host has no narrower word, so what an exported u8 does with a caller-supplied 300 is a language question rather than a layout one, and it is not settled. Widen the declaration to u32 or i32." This one is not blocked on host objects and never will be.
• A struct, array or enum: "A compound value crosses the contract boundary as a host object, which a contract has to build and read through host functions it imports; this target refuses a host binding, because the Soroban host-call convention is not bound here yet."
• A compound return additionally explains the mechanism it cannot use: the caller would receive it through a hidden pointer into linear memory, and a contract method hands back one host word and has no pointer to give.
• A name over 32 bytes: "…the host holds a method name of at most 32. A longer one is not expressible by any caller, so the method would upload and be unreachable — rename it."
• A module with no exported function: refused outright — it would upload with no method to call.
• A parameter written _: "…because parameter 2 is written '_', which gives it no name. A contract's contractspecv0 section describes each method's parameters by name, and stellar contract invoke takes each argument as a --<name> flag built from it; the compiler does not invent a name you did not write. Name the parameter — _unused if the body does not read it; a leading underscore is kept as written. …"
• A parameter name over 30 bytes: "…because parameter 2 'amount_in_the_smallest_currency' has a name of 31 bytes, and a contract method's parameter name is at most 30 bytes: the contract's contractspecv0 section records each name whole in a field that wide, and a longer one would leave the section unreadable to stellar contract invoke and every other tool that reads it. Shorten the name. …"
• A parameter name that is another parameter's CLI flag alias: "…because parameter 1 'x' and parameter 2 '_x' claim one stellar CLI flag: --x is the flag of 'x' and also the one the CLI derives for '_x'. The stellar CLI gives every parameter a second flag in kebab case and resolves a flag to whichever parameter claims it first, in an order that changes from run to run, so a call may reach the wrong parameter or be refused. Rename one of them. …"

The first two are quoted for the second parameter of an exported transfer, the third for an exported f(x: u32, _x: u32): each message opens by naming the function — "Stellar target: exported function 'transfer' cannot be a contract method" — labels the parameter by its one-based position and, where it has one, by its name (the second also gives the name's length in bytes, and the third labels both parameters of the pair, the earlier first), and closes, as the type refusals do, with the advice to remove pub from a function not meant to be a contract method.

Within one exported function, the three name rules run after its type and return rules, in the order listed — _, then length, then the pair — so a type or return refusal on that function is reported before a name refusal on it, and each name rule runs over every parameter before the next begins. Functions are checked one at a time in export order, and the first refusal ends the build.

The pair rule is the CLI's own. stellar contract invoke gives each parameter the flag --<name>, the one its --help lists, and an alias, the name in heck 0.5.0's kebab case: split into words at every character that is not a letter or a digit, between a lowercase letter, or a digit following one, and a capital, and before the last capital of a run followed by a lowercase letter; each word lowercased, and the words joined with -. So toAddr is to-addr, and Amount, one word, is amount. The CLI then resolves a flag to whichever parameter claims it first, in an order that changes from run to run. A name that is another parameter's alias makes the flag listed for it ambiguous, so x beside _x, X, x_ or __x is refused. Two aliases that merely agree leave each parameter a listed flag of its own, so _x beside __x, and to_addr beside _to_addr or toAddr, build: measured with stellar CLI 28.0.0 against a deployed contract, every call to them through the flags --help lists succeeded, while x beside X failed six calls of eight and x beside x_ five. Both gates compute the alias with one function, stellar_cli_flag_alias in core/wasm-codegen, and tests/tests/stellar/MEASURED_ABI.md records the measurement.

main is a contract method like any other: it is exported under its own name and held to the same rules. There is no entry point to a contract, so nothing distinguishes it.

Only the entry file's top-level pub fn declarations are exported, so an inadmissible type inside a private function, a method, or an imported file is not the gate's business.

The custom sections

A contract carries three contract sections beyond the ones every build has — the name section, and inference.checked and inference.bounds_elided where code generation wrote them — and each is written for a different primary reader.

contractenvmetav0. Every contract carries this section, declaring the environment protocol it was built for. A module without one is refused at upload by every Soroban host there has ever been, so the rewriter appends it unconditionally, last in the module, as 32 fixed bytes.

The declared protocol is 20, with pre-release 0. The rule a host applies is that the declared protocol must not be newer than the ledger's, and that a pre-release of 0 is required below it; 20 is the protocol Soroban arrived in, so a contract declaring it is uploadable to every Soroban network that has ever existed. Declaring today's protocol instead would make the artifact un-uploadable to any network still behind it.

That constant is not permanent. It is the minimum the contract needs, and it must become the maximum of the minimum protocols of the host functions the contract imports once host imports are admitted at this target (issue #324). Until then this target refuses every host import, so a contract imports nothing and the floor is the whole answer.

contractspecv0. The XDR description of every method the contract exports: each method's name, each input's name and type, and what it returns. Read by tooling, never by the host: it is what stellar contract invoke reads to turn --a 2 --b 40 into typed Val arguments, what stellar contract info interface renders, and what stellar contract bindings rust reads to write a client. A contract carrying no such section still uploads and is callable by the host, and so is one carrying a malformed one — the host never looks for it; the CLI, by contrast, offers such a contract no command. It is the tooling's readers, named below — Spec::new and soroban_spec::read::from_wasm — that refuse a malformed section. Its body is one SCSpecEntry per exported method, in export order, each the FunctionV0 arm with an empty doc string, the method's name, one input per parameter — an empty doc string, the parameter's name exactly as the source spells it (a leading underscore included), and its type code — and the outputs. The type codes are SC_SPEC_TYPE_BOOL = 1, SC_SPEC_TYPE_U32 = 4 and SC_SPEC_TYPE_I32 = 5, published in Stellar-contract-spec.x at the stellar-xdr revision 9c9c145953e80990d6ff1ae3a6a973a0ce6d0694 (core/stellar-abi/src/spec.rs records the provenance beside each constant). A method that returns nothing is described by an empty outputs vector, not by a fourth code, SC_SPEC_TYPE_VOID = 2: that is what soroban-sdk writes for a function with no return, and what the CLI expects.

contractmetav0. One key-value entry about the contract itself: SCMetaV0 { key: "infver", val }, where val is the crate version the workspace declares (CONTRACT_META_TOOLCHAIN_VERSION; currently 0.0.6) — the toolchain that produced the contract, not a network protocol. stellar contract info meta displays it. Tooling reads it too: soroban-spec's spec shaking (src/shaking.rs) looks there for the Rust SDK's own key, rssdk_spec_shaking, and its absence means spec-shaking version 1, which is what this toolchain's single-entry section amounts to. The host reads none of this.

The rewriter appends the three in one order: contractspecv0, then contractmetav0, then contractenvmetav0 last, so a contract still ends with the same 32 measured bytes it ended with before the other two sections existed — the host imposes no order on custom sections, and this order is a choice made to keep that tail true.

Because the host parses neither tooling section — measured in tests/tests/stellar/envelope.rs: well-formed sections, a spec of arbitrary bytes and a meta entry of a kind that does not exist all upload and invoke — their correctness is the toolchain's alone to check, and the CLI is strict about it: Spec::new (soroban-spec-tools 28.0.0), the reader stellar contract invoke builds a call's arguments with from the deployed contract, and stellar contract info interface runs on a file, decodes all three sections and fails the command if any one does not decode (read from the CLI's source at v28.0.0; the tier mirrors it in spec::every_contract_decodes_the_way_the_cli_reads_a_deployed_contract). So a malformed contractmetav0 or contractspecv0 breaks invoke and info interface even though the host itself uploads and runs the contract without ever parsing either one, while soroban-spec's and stellar-xdr's readers refuse each of those bodies first.

Invoking a contract from the CLI

Measured against stellar CLI 28.0.0 on a local stellar/quickstart network, 2026-09-24; the transcript is tests/tests/stellar/MEASURED_ABI.md's "CLI measurement" chapter. Commands and outputs are quoted verbatim; a line reading … marks lines elided, and home-directory paths are shortened.

Reading the sections from a compiled u32_methods.wasm renders the interface in the SDK's own trait form:

$ stellar contract info interface --wasm u32_methods.wasm
ℹ️ Loading contract spec from file...
#[soroban_sdk::contractargs(name = "Args")]
#[soroban_sdk::contractclient(name = "Client")]
pub trait Contract {
    fn identity(env: soroban_sdk::Env, x: u32) -> u32;
    fn add(env: soroban_sdk::Env, a: u32, b: u32) -> u32;
}

Deploying it first funds a local key and returns a contract id:

$ stellar keys generate alice --network local --fund --overwrite
❗️ Overwriting identity 'alice'
✅ Key saved with alias alice in "…/.config/stellar/identity/alice.toml"
✅ Account alice funded on "Standalone Network ; February 2017"

$ stellar contract deploy --wasm u32_methods.wasm --source alice --network local
ℹ️ Uploading contract WASM…
…
✅ Transaction submitted successfully!
✅ Deployed!
CCRE5RTDJCATV2J4HLBZTKS5SNP2Q2S7EEJ3A572FZX7TSM47CDHDEE3

$ID below stands for the contract id deploy printed, alone on the last line and the only one it writes to standard output, and alice is the funded local key keys generate created.

Deployed and invoked with named arguments, the CLI reports it is simulating a read-only call and prints the answer:

$ stellar contract invoke --id $ID --source alice --network local -- add --a 2 --b 40
ℹ️ Simulation identified as read-only. Send by rerunning with `--send=yes`.
42

A mistyped argument is refused by the CLI itself, before any host call, naming the parameter and its declared type:

$ stellar contract invoke --id $ID --source alice --network local -- add --a two --b 40
❌ error: Failed to parse argument 'a': expected ident at line 1 column 2

Context: Expected type u32 (unsigned 32-bit integer), but received: 'two'

Suggestion: Ensure the value is a valid integer within the type's range

Contrast that with the value ABI above: a raw Val of the wrong tag earns the host's undiscriminated WasmVm, InvalidAction / "VM call trapped: UnreachableCodeReached", identically whichever argument and whichever tag were wrong. The spec is what lets the CLI catch the mistake with the parameter's own name and type instead.

Against a contract carrying neither section — what this toolchain produced before it emitted them — the same CLI panics on info interface and offers invoke no command at all.

What is not supported, and why

• Host imports — anything stateful. Storage, ledger access, events, authorization, cross-contract calls and the host-object constructors all arrive as imported host functions. The language spells such a binding use { f } from host::<module>;, and at this target infc refuses it before external resolution, and so ahead of the allowlist, while code generation refuses it again, in the same words, as the backstop for a caller that skips that step. The refusal names one host binding — the first by module and field name, not by position in the source — and says why: the Soroban host-call convention is not bound by this toolchain, each of those host functions takes and returns the host's 64-bit tagged word, and nothing here maps an external fn onto one of them. It offers two ways out — remove the host binding to build a contract, or build for wasm32, where a host import is supported. Issue #324 is where binding that convention is tracked. Everything below follows from it.
• Compound types and 64-bit integers at the contract boundary. Both travel as host objects, which are built and read through those same imports.
• Proof mode. --mode proof fails the build, and so does --mode compile -v — see the next section for why the second one is refused rather than allowed.
• --wasm-features. permits_bulk_memory() is false for this target, so the one post-MVP family the compiler can emit is refused before a byte is emitted.
• An imported linear memory. [memory] import = true and infc --import-memory are refused before the program is parsed, for the reason given under Module shape below: a contract defines and exports its own memory.
• [build.wasm-opt]. Declaring it alongside target = "stellar" is a load-time manifest error. Whether an external Binaryen preserves the wrappers and contractenvmetav0 depends on which version is installed, and nothing in the manifest pins one.
• infs run. Refused, before anything is built. The runtimes infs run executes a build under — wasmtime for wasm32, the SpaceWasm interpreter for spacewasm — invoke an export by name and pass each argument as a decimal, so 5 would arrive as a word whose low byte is read as tag 5 and whose payload is empty, decoding to a zero-valued integer rather than to five. That is a wrong answer reported as a success. A contract is invoked by a Soroban host and by nothing else.

Proving the wasm32 build and deploying the Stellar one

Because code generation never reads the target, the module a Stellar build starts from is the module a wasm32 build finishes with. That is what makes "prove one, deploy the other" a statement about bytes rather than a hope, and it is why the Rocq path is refused here rather than qualified: wasm_to_v reads the linked, pre-rewrite bytes, so a .v written during a Stellar build would describe a module whose exports point at different functions, with none of the value-ABI wrappers and none of the three contract sections the rewrite appends — not the .wasm beside it on disk. infc refuses that pairing and tells you to build the same source at wasm32 instead.

The procedure:

# The module to reason about, and its Rocq translation.
infc contract.inf --target wasm32 -v --out-dir proofs/

# The module to deploy. Same source, same emitter, plus the marshalling shell.
infc contract.inf --target stellar --out-dir out/

proofs/contract.wasm is, byte for byte, the module out/contract.wasm was rewritten from. The claim is checked mechanically over a set of fixtures — each side built at its own default optimization level, as the CLI really builds them:

cargo test -p inference-tests --lib \
  codegen::wasm::stellar_gate::stellar_gate_tests::a_stellar_build_is_byte_identical_to_the_default_build

To see the relationship in the artifacts themselves, disassemble both. Every function of the wasm32 module appears in the Stellar module at the same index with the same body; what the Stellar module adds is one (param i64 …) (result i64) wrapper per exported method, appended after them, and the three custom sections at the end, the environment metadata last.

What the host accepts — the runtime's wasmi configuration. This is the envelope a module is admitted against, not a description of what Inference puts in one:

What the compiler emits is narrower than that envelope on two of the three enabled rows:

• mutable-globals — used. The shadow-stack pointer is a mutable global and the module exports it as __stack_pointer, which is what the proposal permits. An exported mutable global is accepted at upload; this was measured, not assumed.
• sign-ext — never emitted, at any target. No i32.extend8_s/i32.extend16_s (or their i64 forms) appears anywhere in code generation; a narrow signed value is normalized with i32.shl followed by i32.shr_s.
• bulk-memory — refused at this target. Target::permits_bulk_memory() is false for it, so --wasm-features bulk-memory (or the manifest's wasm-features) fails the build before a byte is emitted, and region fills and copies take the load/store lowering instead.

Module shape. No lld-style link step runs and no linker flags exist to pass: every LLVM dependency, rust-lld among them, was removed when the compiler moved to direct emission. (The .wasm-into-.wasm static merge described in The WASM Linker is a different thing and takes no such flags either.) The two facts that decide the module's shape are therefore properties of code generation:

• Exports are every top-level non-method pub fn in the entry file, under its own name, main included. A pub fn in an imported file is intra-project visibility and is not exported; methods and spec-inner functions are never exported. No dead-code-elimination pass runs, so a private, never-called function in a compiled file is still emitted.
• Linear memory is stack-first: the shadow stack occupies the low end and grows downward from its top toward 0, and the program's array and struct module constants sit directly above it, written by one active data segment at instantiation. Its size is one fixed 64 KiB page by default and is set through [memory] / --memory-pages / --stack-size, not by a link-time flag. [memory] max-pages / --max-memory-pages lets the contract's memory grow up to a declared bound. The contract defines that memory and exports it; it never imports one. [memory] import / --import-memory is refused at this target, because the value-ABI rewrite every artifact goes through accepts no import, so a contract importing env.memory could not be deployed.

SpaceWasm

Produces a module for the SpaceWasm flight interpreter — NASA JPL's no_std WebAssembly 1.0 interpreter for flight software, which decodes a module into its own IR on a fixed allocation and executes it with no operating system underneath. Selected with infc --target spacewasm or [build] target = "spacewasm" in an Inference.toml.

Unlike the Stellar target, this one imposes no calling convention and adds nothing to the module. There is no marshalling shell, none of the contract sections a Stellar build appends, and no rewrite: the artifact a SpaceWasm build writes is, byte for byte, the artifact a wasm32 build writes from the same source. What the target does is narrow what a build may contain — the instruction set and the shape of its linear memory, and nothing else.

What the interpreter decodes

The instruction set is the WebAssembly 1.0 MVP plus mutable-globals. Several further proposals are tracked upstream and not implemented, and only one of them, bulk-memory, costs an Inference build anything at all:

Decode-time limits

Decoding a module is where the interpreter checks its own maxima, and a module that exceeds one would be refused on the device rather than at build time. The build asks the same questions first — see Conformance below. The fixed limits are refusals: a module this target accepts meets every one of them, so its declarations fit the fields the decoder reads them into and not merely its instruction set. That is a claim about this table rather than a proof of decodability — core/target-conformance's README classifies every refusal the interpreter can raise, either as one of the rows here or with the reason it is out of reach, and nothing is left unclassified. The two embedder-configured rows cannot be refusals, because their values belong to a deployment rather than to the interpreter; the build measures them instead and prints what they have to be. One shape is refused here although the interpreter would load it, and it is the only one: a module that references a function or a global it defines at position 65,536 or beyond. The interpreter narrows those two index spaces to sixteen bits without checking the narrowing, so it loads such a module and then runs it against the definition 65,536 below — a call reaching the wrong function, a global.get reading the wrong word. There is no load failure to move to build time there, only a wrong execution to inherit, and for a flight computer a build that fails is better than an artifact that flies and calls the wrong function. core/target-conformance's README carries the mechanism, the five places a module can name a definition, and the measurements behind them; the narrowing is reported upstream as nasa/spacewasm#201. This compiler emits one global and no build approaches either count, which is why it is a sentence here rather than a row above.

The last two are the ones to read carefully: they belong to whoever embedded the interpreter, not to the interpreter, so "does this module fit" is only answerable against a particular flight configuration. spacewasm_std's 64 and 256 are the reference numbers a report can be read against, not a promise about the vehicle.

Foreign modules

A module bound through [wasm-dependencies] or -L is merged into the artifact, so it is held to the same instruction set the artifact is. The build asks that of each external before the merge, while each one is still its own file:

$ infc main.inf -L lib/ --target spacewasm
The `spacewasm` target: the external module `rustlib`, resolved to lib/rustlib.wasm,
is not a WebAssembly 1.0 module: sign extension operations support is not enabled (at
offset 0x1b). This target's artifact is WebAssembly 1.0 throughout and this module is merged
into it, so the artifact is refused as a whole rather than in part. Rebuild `rustlib`
for the WebAssembly 1.0 instruction set — a stock Rust `wasm32-unknown-unknown` build
emits sign-extension instructions by default — or build this program at --target
wasm32, which links the module as it is.

Asked after the merge instead, the same question could only answer with a byte offset into bytes that came from no single file. The linker itself is deliberately more permissive — it accepts sign extension, bulk memory and mutable globals, which is what an ordinary foreign toolchain emits — so this refusal is the target's, not the linker's, and the same external links without complaint at --target wasm32. The conformance check below still asks the whole-artifact question afterwards, as the backstop for anything that reaches the module by some other route.

Host imports

This target admits the binding. A program that binds use { f } from host::<module>; compiles here, and its artifact carries the import for the embedder to satisfy — the module a wasm32 build writes, since nothing on the emission path reads the target. What the target adds is a check against three registration caps. An embedder supplies an import by registering a host function under the import's two names, and the registration API names a host module and a host function through a 31-byte name type and builds a host function of at most nine parameters and one result, so an import outside those caps may decode, but it can never be bound. That API is the authority for all three, and infc asks them of the program's declarations — after external resolution, before the allowlist and before any byte is emitted — so the refusal asks for an edit to the source rather than to an import section in a module no file holds. For a module name of 32 bytes:

external fn telemetry(channel: i32, value: i32) -> i32;
use { telemetry } from host::fprime_core_telemetry_downlink_a;

pub fn report(channel: i32) -> i32 {
    return telemetry(channel, 7);
}

$ infc main.inf --target spacewasm
Parsed: main.inf
Analyzed: main.inf
SpaceWasm conformance failed: the host imports this program declares cannot all be registered by a SpaceWasm embedder.
No file was written.

  import name too long: import module name `fprime_core_telemetry_downlink_a` on `fprime_core_telemetry_downlink_a`.`telemetry` is 32 bytes; SpaceWasm accepts at most 31.
    This is a registration limit, not a decode limit: the decoder reads a name of up to 32 bytes, but an embedder registers host modules and host functions through a 31-byte name type, so a 32-byte name decodes and can never be bound to a host. 31 is the cap that matters.
    Shorten the module name this extern is bound under.

The declaration-level check takes on trust that the declarations are the imports the artifact will carry, so the post-link conformance check asks the same three caps of the bytes as the backstop; the two cannot disagree about an import both see, because they run one rule. Why the caps are asked before the allowlist rather than after it is set out in What is refused, and by which layer. Of the three caps, the one-result cap is unreachable from Inference source, since an external fn returns one value or none; it earns its findings on the byte-level path.

Such a program has no proof path: infc refuses every build that writes a .v for a program that binds a host import, at every target, so the procedure in Proving the wasm32 build and deploying the SpaceWasm one does not apply to it. infs run runs one whose imports are all F´ (F Prime) reference hosts at their reference signatures — see Running a SpaceWasm build — and for any other import the embedder harness can register a stub per import — see the --host transcript in Running a module under the embedder harness.

Conformance

Every SpaceWasm build checks the module it is about to write against every fixed limit in the table above, and measures the two that an embedder chooses. The check runs after linking and before any file is written, so a refusal leaves nothing on disk:

$ infc main.inf --target spacewasm
Parsed: main.inf
Analyzed: main.inf
Codegen complete
spacewasm: conformant with WebAssembly 1.0; deepest control nesting 7 in `render_row`,
tallest operand stack 19 values in `mix` (peak 27 stack words in `mix`). Build the
embedder with MAX_CONTROL_FRAMES >= 7 and MAX_STACK_DEPTH >= 19 (spacewasm_std uses
64 and 256); limits from spacewasm 0.7.1.
WASM generated at: out/main.wasm

What is failed. Anything outside WebAssembly 1.0 plus mutable globals — which for a linked build means a post-1.0 instruction in a foreign module, refused earlier and by name, see Foreign modules — and each decode-time and registration-time limit in the table: parameter words, local words, call-frame words, a locals group, a call_indirect type index or br_table width over the interpreter's 16-bit IR immediate, a branch discarding more than 255 operand words, an import module or field name over 31 bytes, a host function over nine parameters or one result, a custom section name over 32 bytes, and a memory over the address space. One further refusal is the build being deliberately stricter than the interpreter rather than agreeing with it: a reference to a defined function or global at position 65,536 or beyond, which the interpreter loads and then resolves to the wrong definition, as Decode-time limits above describes. Every refusal names the two numbers, says which cap it met, and gives one thing to change. Six of them describe module shapes this compiler cannot produce; those say so, and ask you to rebuild the external module or report a compiler bug, because you did not write the file the shape is in — the two IR-immediate ones and the truncation one still name the edit that would shorten it, since for those there is one.

What is asked of the source first. One limit in the table is also a property of a declaration: a function's parameter words follow from its signature. Analysis rule A055 asks it of every function the program defines, before code generation runs, and refuses one over 255 on its parameter list, saying where the words went — so many for each parameter type, one for a self receiver, one for the hidden pointer a struct or array result is written through. For a wide.inf declaring fn wide(p0: u32, p1: u32, …, p255: u32) -> u32 on its first line:

$ infc wide.inf --target spacewasm
Parsed: wide.inf
1:9: error[A055]: `wide` declares 256 parameter words, and SpaceWasm accepts at most 255 in one function: 256 for 256 `u32` parameters; SpaceWasm counts a function's parameters in four-byte words — two for an `i64` or `u64`, one for any other type, a struct or an array included, since it is passed as its address — and records the count in a single byte, so it refuses to load a module that declares more; pass related values together in a struct, which costs one word however many fields it has, or split the function

The conformance check still counts parameter words in the finished module, where it is the only check that sees a function a linked module brings in: such a function has no declaration in the program for a source-level rule to read. The editor reports A055 too, for a project whose Inference.toml names target = "spacewasm" under [build].

What is reported. Three numbers, and each carries its unit because two of them sound alike and are not the same quantity:

• Deepest control nesting, in frames, counting the implicit function-body frame that both the interpreter and the compiler's checker push before reading an operator. Compare it directly against MAX_CONTROL_FRAMES; there is no off-by-one to apply.
• Tallest operand stack, in values — one entry per value whatever its width. This is the unit of MAX_STACK_DEPTH, so it is the number the second const generic must clear.
• Peak stack words, the same high-water mark weighted by width, where an i64 counts two. This is not MAX_STACK_DEPTH's unit: it is what the engine's value stack holds, and it is what Engine::new's stack budget is sized from.

Sizing the verifier's const generic from the word figure over-allocates; sizing the engine's stack from the value figure under-allocates and fails in flight. That is why both are printed, each labelled, and why the line ends with the release the limits were read from.

When a maximum exceeds the spacewasm_std reference configuration the build still succeeds — a conformant module that needs a bigger const generic is not a broken module — and prints a warning naming the three functions that reach highest, so the choice between raising the generic and flattening a function is made with the functions in front of you:

warning: spacewasm: control nesting 71 exceeds spacewasm_std's MAX_CONTROL_FRAMES of 64.
Deepest functions: `render_row` (71), `blend` (66), `mix` (65). Either raise the const
generic in your embedder or flatten the nesting in these functions.

The wasm-opt re-check. This target keeps [build.wasm-opt] — its artifact is plain WebAssembly 1.0 with nothing layered on top, and size is the scarce resource on a flight computer, which is why -Os is its recorded level. But the optimizer is an external Binaryen that nothing here pins, and it reshapes control flow and coalesces locals — both of them quantities the report above measures. So infs runs the same check again on the optimized bytes, immediately before they are moved into place, and a failure leaves the artifact the compiler wrote exactly where it was:

$ infs build
...
SpaceWasm conformance failed: out/main.wasm is not a module a SpaceWasm embedder can load and run as written.
The original artifact is unchanged; try `--no-wasm-opt`, or a different Binaryen version.

The invariant is "the checked bytes are the bytes that ship", which is why the re-check sits after every rewrite that step performs rather than beside the re-validation next to it. A re-check that passes reprints the summary, so the last budget in the log is the one describing the artifact on disk rather than the one the compiler wrote before the optimizer saw it.

Running a SpaceWasm build

infs run executes a spacewasm build in process, under the SpaceWasm interpreter itself — spacewasm 0.7.1, embedded through the inference-spacewasm-runner crate — and never looks for wasmtime. It loads the artifact at the configuration of spacewasm_std, the reference embedder in the SpaceWasm repository: verifier bounds of 64 control frames and 256 operand-stack values, 256 IR code pages, and 1,024 words of value stack. A conformant module over either verifier bound is refused on load, naming the function and the const generic an embedder would have to raise, and a call chain whose frames need more than 1,024 words ends in a StackOverflow trap. The interpreter's own allocations are the one part of the configuration that is not the reference embedder's: they go to this machine's allocator, with no bound, where spacewasm_std runs behind an allocator of sixteen 8 KiB pages (core/spacewasm-runner/README.md says why).

A program may bind the six F´ (F Prime) reference host functions spacewasm_std registers, at the signatures it registers them with, and no others. An array argument is passed as its address, so every buffer travels as one i32 with its length beside it:

Every import is checked against this table before a byte of the module is decoded, and a program importing anything else, or a reference host at another signature, is refused with nothing executed, naming each such import and the declaration that would match. The hosts are stubs: command and telemetry answer 0, the time telemetry writes into the caller's buffer is zero, clock_ms reads this machine's clock, and panic always stops the program. Each but clock_ms logs its calls to stderr as it is made, in the style of the reference embedder's lines — MESSAGE hello, COMMAND 42 7, TELEMETRY 3 — and core/spacewasm-runner/README.md lists the five ways they differ from the reference embedder's. One of them keeps every call on one line: a MESSAGE or PANIC payload has its control characters escaped, so a buffer padded with zeros logs as MESSAGE hello\0\0\0, and a newline inside a payload cannot forge a log line of its own.

The value the entry point returns is the last line on stdout, after Invoking 'main' with the SpaceWasm interpreter (spacewasm 0.7.1)..., and a function returning nothing prints nothing after it. The value prints as a signed decimal, as it does under wasmtime, so a u32 or u64 result above its type's signed maximum prints as the negative number with the same bits: a u32 of 4294967295 prints -1. The exit status is 0 whenever the call returns, whatever it returned; a refused load, a refused argument, a trap and an exhausted budget exit with status 1, and a trap is reported with the interpreter's reason and what it means in Inference code. --fuel N stops the run after N of the interpreter's own instructions, and without it a run has no budget. In single-file mode the arguments after the source path are read as the invoked function's parameters — an i32 or an i64, in its signed or its unsigned range — and their count is checked; in project mode main is given none, and a main that takes any is refused with the single-file command that passes them.

A first run. The program below is a health check in the shape of an F´ component: it announces itself, sends a command, downlinks one telemetry value and counts what went wrong. Create a project, point it at this target by replacing the commented-out # target = "wasm32" line under [build] in its Inference.toml with target = "spacewasm", and replace its src/main.inf with the program:

infs new fprime_demo
cd fprime_demo

// A health check in the shape of an F´ component: announce itself, send a
// command, downlink one telemetry value, and count what went wrong.
//
// Inference has no string type, so text is a byte array. A host function that
// takes a buffer takes its address and its length, and an array argument is
// passed as its address.
external fn message(text: [u8; 5], len: i32);
external fn command(opcode: i32, arg: i32) -> i32;
external fn telemetry(id: i32, mut time: [u8; 11], time_len: i32, value: [u8; 4], value_len: i32) -> i32;
use { message, command, telemetry } from host::fprime_core;

external fn clock_ms() -> i64;
use { clock_ms } from host::env;

pub fn main() -> i32 {
    let started: i64 = clock_ms();

    let hello: [u8; 5] = [104, 101, 108, 108, 111]; // "hello"
    message(hello, 5);

    let status: i32 = command(42, 7);

    let mut time: [u8; 11] = [0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0];
    let reading: [u8; 4] = [21, 0, 0, 0]; // 21, as a little-endian u32
    let sent: i32 = telemetry(3, time, 11, reading, 4);

    let elapsed: i64 = clock_ms() - started;

    let mut faults: i32 = 0;
    if status != 0 {
        faults = faults + 1;
    }
    if sent != 0 {
        faults = faults + 1;
    }
    if elapsed > 1000 {
        faults = faults + 1;
    }
    return faults;
}

$ infs run 2> host.log
target: spacewasm
Parsed: src/main.inf
Analyzed: src/main.inf
Codegen complete
host imports (no allowlist): env.clock_ms, fprime_core.command, fprime_core.message, fprime_core.telemetry
spacewasm: conformant with WebAssembly 1.0; deepest control nesting 3 in `main`, tallest operand stack 5 values in `main` (peak 5 stack words in `main`). Build the embedder with MAX_CONTROL_FRAMES >= 3 and MAX_STACK_DEPTH >= 5 (spacewasm_std uses 64 and 256); limits from spacewasm 0.7.1.
WASM generated at: out/main.wasm
Invoking 'main' with the SpaceWasm interpreter (spacewasm 0.7.1)...
0
$ cat host.log
MESSAGE hello
COMMAND 42 7
TELEMETRY 3

Standard output carries the build log, the Invoking 'main' … line and the return value; the host lines go to standard error, which the first command sends to host.log. Without the redirection a terminal shows them between the Invoking 'main' … line and the 0, as each call is made. Read against the program:

• 0 is the nominal answer. command and telemetry answered 0, as the stubs always do, and no more than a second passed between the two readings of the clock, so main counted no fault. The run exits with status 0, and it would have exited 0 having counted three: the status says that the call returned, and what it returned is the last line of standard output.

• clock_ms logs nothing. It was called twice, and neither call has a line.

• time is mut because the host writes into it. An array argument is passed as its address, not copied, so the eleven bytes telemetry writes land in main's own time, which after the call holds the host's zero time whatever it held before. mut on the parameter is why the call site needs a mut binding (A047), but nothing checks the declaration against what the host does: with mut left off both, the program compiles and runs, and its time is overwritten all the same. See mut on a host parameter is an assertion, not a contract and issue #470.

• The host trusts len. It reads len bytes at the address it is given, whatever the array's length: message(hello, 3) logs MESSAGE hel, and a len past the end of the array reads whatever follows it in memory, with no refusal. What stops the program is a range that leaves linear memory, with a trap naming the host, the address, the length and the size of the memory, or bytes that are not UTF-8, since message and panic print text.

• telemetry writes an eleven-byte F´ time. infs run stops the program, before anything is written, when time_len is less than eleven — a departure from the reference embedder, which writes the eleven bytes whatever time_len says, past the end of a shorter buffer and into the caller's frame. Passing 8 instead of 11 ends the run with:

  Error: `main` trapped: `fprime_core.telemetry` writes an 11-byte F Prime time, and `time_len` is 8 (Host).
  Declare the parameter `mut time: [u8; 11]` and pass 11.
  

• --fuel can stop a run part way. Sixty of the interpreter's instructions take this program through its calls to message and command and not as far as telemetry, as standard error alone shows:

  $ infs run --fuel 60 > /dev/null
  MESSAGE hello
  COMMAND 42 7
  Error: `main` ran out of fuel: the SpaceWasm interpreter stopped it after 60 interpreter instructions (`--fuel 60`) before it returned. Either it never returns or it needs a larger budget: raise `--fuel`, or leave it out to run without one. The host calls logged above had already been made.
  

  The count is of the interpreter's own compiled form of the module, so the budget that stops a program at a given point depends on the compiler and the interpreter that produced that form.

A project written for a flight embedder can also name the host functions it may bind in a [host-imports] allowlist, so that infc refuses a program that binds any other; infs run decides what it can execute from the artifact's imports, with or without one.

In single-file mode any exported function can be run with --entry-point, and an array or struct in its signature stands for an address: such a parameter receives the number given on the command line as an address, and a function returning an array or struct takes a hidden first parameter, the address to write its result to, and prints nothing (see infs run).

What a run shows, and what it does not. infs run executes the artifact once, under the interpreter the target is for, against stand-in hosts. It is a test: it shows that this module loads at the reference limits, what this execution computed, and which host functions it called, as far as their log lines record the calls. It is not a proof. A program that binds a host import has no proof path at all — host imports are not yet modeled in the proof translation, so infc refuses every build that writes a .v for such a program, at every target (issue #469) — and running it changes nothing about that. The reference hosts are stubs: command and telemetry answer 0, the time telemetry writes is zero, and clock_ms reads this machine's clock, so two runs of one program need not agree. A run therefore says nothing about how the program behaves against real F´ flight software. It also runs on this machine's allocator at spacewasm_std's reference limits, not on a vehicle's configuration. For a program that binds no host import, Proving the wasm32 build and deploying the SpaceWasm one still applies unchanged, and a run under the interpreter is a differential check of the very module that proof is about.

Running a module under the embedder harness

To run a program, use infs run — see Running a SpaceWasm build. The SpaceWasm interpreter runs a module only inside an embedder, which decides the hosts it registers, the limits it loads under and what a run reports, and infs run is the embedder for a program: it builds the source, supplies the F´ reference hosts and reports what the program did. This repository also ships a developer tool, an example of the test crate, for the questions infs run leaves alone: running an artifact that is already on disk, standing a stub in for any import at any signature, not only the six reference hosts, and measuring the IR a module compiled to (--stats, and --json for a script to read). It loads at the reference embedder's verifier bounds and IR code pages, but with the 65,536 words of value stack the SpaceWasm test tier runs the codegen corpus with rather than the reference 1,024. Every transcript below is a real run, so the figures can be re-derived rather than taken on trust, and all but the last two are against one artifact — out/main.wasm, built by infc main.inf --target spacewasm from pub fn main() -> i32 { return 10; }, whose pub is what puts main in the export section:

cargo run -p inference-tests --example spacewasm-embed -- out/main.wasm --invoke main
main = 10

It loads the artifact, calls one export, and prints the result as NAME = value, or NAME = (unit) for a function that returns nothing. Arguments follow the export name and are decimal integers coerced to the parameter types the artifact declares (--invoke add 2 40). With neither --invoke nor --stats it reports what the module exports and stops, which is the cheapest way to ask whether an artifact loads at all; asking for a measurement makes the measurement the report.

Each way a run can end has an exit code of its own — a module that could not be read, one the interpreter refused, a missing export, a trap, an exhausted fuel budget — so a script can tell them apart without reading the message. A trap prints the interpreter's own reason. Execution always runs under an instruction budget, 100,000,000 unless --fuel N sets another, so a program that does not terminate fails the run instead of hanging it — where infs run runs without a budget unless it is given one.

--stats reports what the module cost the interpreter — the IR pages it compiled to, the sixteen-bit words written into them against the words those pages hold, those words as bytes, the artifact's size, and the ratio of the two:

cargo run -p inference-tests --example spacewasm-embed -- out/main.wasm --stats
code pages: 1
IR words (16-bit): 4 / 256 (1.56%)
IR bytes: 8
wasm bytes: 62
IR bytes per wasm byte: 0.13

The page and word figures are computed the way upstream's own spacewasm_std demonstration binary computes them, so they can be read beside its output. The last line is deliberately not spelled the way upstream spells its own compilation ratio: that one is a different quantity — the live bytes its bounded page allocator holds, the engine and the guest memory as much as the IR — and this harness cannot produce it, because it runs on an unbounded allocator that keeps no statistics. A figure that is not upstream's should not travel under upstream's name. Adding --json prints the measurement as a single line of JSON instead, for a script to read; the keys are documented where the harness is implemented, and the ratio is carried there at full precision — the two decimals above are a courtesy to a reader, not the figure. How these figures move as the compiler changes is tracked by the benchmark described in Tracking what a build costs the interpreter.

A program binding use { f } from host::<module>; compiles at this target and its artifact carries the import, but it loads only once something supplies that import — and the harness can stand in for an embedder just far enough to run it. --host MODULE.FIELD=PARAMS[:RESULT], repeated once per import, registers a stub under the import's two names, with the signature spelled in the interpreter's own alphabet: one character per value type, i for i32, I for i64, f for f32 and d for f64, so env.clock_ms=:I takes nothing and returns an i64. A stub answers zero of its result type, never traps and never reads guest memory, and each call it receives is printed to stderr as host call: module.field(arg, …), ahead of the result of the invocation that made it. An array argument reaches a host as the address of the caller's buffer, so a stub logs that address, not the bytes behind it. What that shows is which host functions the program asked for, with which arguments and in which order; what a real host would have answered is your embedder's to decide. For the F´ program, which binds all six host functions of the F´ (F Prime) reference set, at the signatures spacewasm_std registers them with, and calls four of them,

external fn panic(text: [u8; 6], len: i32, line: i32);
external fn rsleep(ticks: i64);
external fn command(opcode: i32, arg: i32) -> i32;
external fn message(text: [u8; 6], len: i32);
external fn telemetry(id: i32, mut time: [u8; 11], time_len: i32, value: [u8; 4], value_len: i32) -> i32;
use { panic, rsleep, command, message, telemetry } from host::fprime_core;

external fn clock_ms() -> i64;
use { clock_ms } from host::env;

pub fn report(channel: i32) -> i64 {
    let text: [u8; 6] = [114, 101, 112, 111, 114, 116]; // "report"
    message(text, 6);
    let id: i32 = command(1, channel);
    let mut time: [u8; 11] = [1, 2, 3, 4, 5, 6, 7, 8, 9, 10, 11]; // distinct from zeroed memory
    let value: [u8; 4] = [21, 0, 0, 0]; // 21, as a little-endian u32
    let status: i32 = telemetry(id, time, 11, value, 4);
    if status != 0 {
        return 0;
    }
    return clock_ms();
}

built into out/main.wasm the same way:

cargo run -p inference-tests --example spacewasm-embed -- out/main.wasm \
    --host fprime_core.panic=iii --host fprime_core.rsleep=I \
    --host fprime_core.command=ii:i --host fprime_core.message=ii \
    --host fprime_core.telemetry=iiiii:i --host env.clock_ms=:I \
    --invoke report 3
host call: fprime_core.message(65504, 6)
host call: fprime_core.command(1, 3)
host call: fprime_core.telemetry(0, 65510, 11, 65521, 4)
host call: env.clock_ms()
report = 0

Every stub answered zero: command's zero became telemetry's id, telemetry's zero read as accepted, so report went on to ask the clock, and the clock's zero is what it returned. These imports are all F´ reference hosts at their reference signatures, so infs run runs this program as well, from a project whose manifest sets target = "spacewasm" (infs run src/main.inf --entry-point report 3), against the hosts themselves: message and panic read the buffers they are given, and telemetry writes the time into its buffer. A stub reads no buffer and writes nothing, and the harness registers one for any import, in that set or out of it. panic and rsleep are bound and never called, and still need a stub, because the interpreter binds every import when it decodes the module. A name longer than 31 bytes, more than nine parameters or more than one result is a usage error that names the interpreter's own refusal and the limit behind it, both read from the interpreter rather than restated by the harness. Two counts are usage errors as well, because the interpreter does not check them and would bind the excess imports to other stubs without a word: more than 256 module names, which its one-byte host-module reference cannot address, and more than 65,536 stubs under one module name, whose positions its binder narrows to sixteen bits.

A module whose imports have no stub is still a load failure. The interpreter's verdict names no import, so the harness reads the module a second time and lists each module.field beside the spec it needs:

cargo run -p inference-tests --example spacewasm-embed -- out/main.wasm --invoke report 3
error: out/main.wasm does not load under the SpaceWasm interpreter: FunctionImportNotFound at byte 73
  reading the Import section
  it imports these, and no `--host` stub was registered for any of them:
    fprime_core.panic: no stub; it needs `--host fprime_core.panic=iii`
    fprime_core.rsleep: no stub; it needs `--host fprime_core.rsleep=I`
    fprime_core.command: no stub; it needs `--host fprime_core.command=ii:i`
    fprime_core.message: no stub; it needs `--host fprime_core.message=ii`
    fprime_core.telemetry: no stub; it needs `--host fprime_core.telemetry=iiiii:i`
    env.clock_ms: no stub; it needs `--host env.clock_ms=:I`
  register a stub for each with `--host MODULE.FIELD=PARAMS[:RESULT]`, or run the module from the embedder that supplies them

An import registered with a stub of another signature is listed beside that stub and the half of its signature that differs. One no stub can supply — a global, say — is listed with the reason. A spec naming no import of the module is listed after the imports, which is where a misspelt name shows up.

Tracking what a build costs the interpreter

For a flight target the IR a module compiles to and the instructions a call takes are budget numbers: the code builder fills a fixed number of IR pages, and a call has to finish inside its cycle. A second developer tool of the test crate, the spacewasm-bench example, measures both on a fixed set of programs and keeps the measurements in tests/bench/spacewasm/history.jsonl, so how they move as the compiler changes is on record.

The programs are the ones the SpaceWasm test tier runs: every function exported by every single-file codegen fixture that builds at this target, binds no host import and carries no verification operator — the fixtures the tier's differential sweep runs under wasmtime and the interpreter alike — called with zero for each parameter, which for an array or a struct is the address 0, and four F´ programs run against the reference hosts infs run supplies, among them report(3) of the program shown in the previous section. Zero arguments make every call the same on every run, if not always a meaningful one: some trap, and a trap ends the same way each time. Each call is one measurement: the IR code pages, IR words, size and IR bytes per byte of its module, as --stats measures them, and the exact number of the interpreter's instructions the call took. The interpreter reports how a run ended and never how much of its budget it spent, so the benchmark runs each call one instruction at a time, through the runner's Instance::invoke_counting, and a budget of exactly the count is the least that runs the call to the same end.

Each line of the history is one measurement, stamped with the day it was recorded, the commit and the interpreter release:

{"date":"2026-09-26","commit":"3171415bd6732f1707d73d222f225de299430108","interpreter":"spacewasm 0.7.1","program":"fprime/spin","export":"spin","args":["1000"],"outcome":"returned","instructions":22027,"code_pages":1,"ir_words":79,"wasm_bytes":225,"ir_bytes_per_wasm_byte":0.7022222222222222}

The figures are in the interpreter's own terms, its IR and its instructions over that IR, so they change with its release as well as with the compiler, and a comparison only sets a measurement beside one made under the same release. The keys are documented in tests/tests/spacewasm/bench.rs.

Comparing. A pull request's CI runs

cargo run -p inference-tests --example spacewasm-bench -- compare

on Linux, which measures the tree and sets each measurement beside the last line the history holds for the same program, function and arguments. A call whose instructions, or a module whose IR words, grew by more than 5% is a warning — a ::warning annotation on the pull request inside GitHub Actions, and --threshold N sets another whole percentage — and a measurement that is new, gone from the latest snapshot or ending another way is a note. A program the benchmark could not measure — a fixture whose module the interpreter refuses, or an F´ program that does not load, start or take its call — is a warning as well, since nothing it costs was compared, and the summary line counts it. It exits 0 whatever it finds: it reports a cost, and whether the cost is worth paying is the reviewer's call. The history is recorded once a release, so every warning about a figure names the snapshot it compares with, and a figure that grew is reported on every pull request until the next snapshot records it.

Recording. Before a release, from a clean checkout of the commit being released, run

cargo run -p inference-tests --example spacewasm-bench -- record

and commit the lines it appends: one snapshot, a line per measurement, stamped with git rev-parse HEAD — or the commit --commit SHA names — the day in UTC and the interpreter release. A snapshot is recorded whole or not at all: when a program could not be measured, record names each one and why, appends nothing and exits 1. compare looks for what is gone in the newest snapshot alone, so a snapshot that left a program out would end its series, and no later comparison would report it gone. A fixture the differential sweep stops running is a change to the set of programs rather than a failure: it is not measured, it never stops record, and compare notes its measurements as gone. A pull request that moves the interpreter's pin records a snapshot as well, since until one exists under the new release there is nothing to compare with; a test fails until it does.

Proving the wasm32 build and deploying the SpaceWasm one

Because code generation never reads the target, a SpaceWasm build and a wasm32 build of the same source are the same module. Not "the module the other was derived from" — the same file.

The procedure:

# The module to reason about, and its Rocq translation. `-v` implies proof mode.
infc main.inf --target wasm32 -v --out-dir proofs/

# The module to deploy, and the same source at the default target.
infc main.inf --target spacewasm --out-dir out/spacewasm/
infc main.inf --target wasm32    --out-dir out/wasm32/

# The two compile-mode modules are the same file.
cmp out/wasm32/main.wasm out/spacewasm/main.wasm    # fc /b on Windows

The cmp is the second of the two links below. It compares two compile-mode builds, which is the comparison the target claim is about; proofs/main.wasm is a proof-mode artifact and carries whatever the specifications in the source add to it, so it is the first link — not this one — that ties it to out/wasm32/main.wasm.

That cmp is a statement about this target and no other. The Stellar procedure above deliberately does not have one: a Stellar artifact carries appended wrappers and the three contract sections, so its relationship to the proved module is "rewritten from", not "equal to".

The same difference shows up as a command line that works here and not there. Proof mode is refused at both targets, for the same reason — it emits the custom 0xfc instructions and neither runtime decodes them — so --mode proof and a bare -v fail either way. But --mode compile -v, the one spelling that keeps compile mode and still asks for a translation, succeeds at spacewasm and writes exactly the .v a wasm32 compile-mode build writes:

infc main.inf --target spacewasm --mode compile -v --out-dir out/spacewasm/
infc main.inf --target wasm32    --mode compile -v --out-dir out/wasm32/
cmp out/wasm32/main.v out/spacewasm/main.v          # fc /b on Windows

At stellar that spelling is refused, because there the translation reads the pre-rewrite bytes while the .wasm written beside it is the contract. Here there is no rewrite for it to run ahead of. It is a decision rather than a consequence of where the refusal happens to be written, and the CLI suite pins it — a refusal widened from "the rewriting target" to "any non-default target" would take this with it.

What the SpaceWasm build buys today is the envelope, applied to a build whose output is otherwise the default target's. Named rather than counted, because only two of the three are rows in the settings table above: a build for this target refuses proof mode, refuses every post-MVP instruction family, and refuses a non-deterministic construct — a forall, exists, assume or unique block, or an @ — anywhere in a function that ships.

The third is not a narrowing this target introduces. Analysis rules A042 and A006 refuse non-determinism outside a spec in every build at every target, with a source location, and every infc build runs both. What this target adds is that code generation asks the question again, as a backstop for a caller that reached it without running analysis; the default target does not ask it, because there the custom 0xfc instructions are ones Inference's own tooling decodes — no general-purpose embedder does — which is what makes this a target-specific question rather than a second copy of A042. The backstop reaches the same programs the rules do: it descends every nested block, every statement and every operand, so a forall in a loop body and an @ under an operator are refused here as surely as a return @ is. What the rules have that it does not is the source location. Either way the refusal is about executable code only: compile mode strips spec bodies before either check looks at them, so a specification written in those constructs costs a SpaceWasm build nothing.

The conformance report against the decode-time limits is what makes the envelope buy more, and every build produces one: see Conformance above for what a build fails on, what it reports, and how to read the report against an embedder's MAX_CONTROL_FRAMES and MAX_STACK_DEPTH.

The two links. For the deployed bytes to be the proved bytes, two identities have to hold, and each has its own guard in the test suite:

1. A proof-mode module's execution functions are byte-identical to compile mode's. Codegen applies no optimization pass in either mode, so the only difference a proof build can carry is the spec functions compile mode drops.

   cargo test -p inference-tests --lib \
     codegen::wasm::checked_arith::checked_arith_tests::proof_and_compile_builds_of_a_guarded_source_are_byte_identical
   

2. A compile-mode SpaceWasm module is byte-identical to a compile-mode wasm32 module. This is checked over every single-file fixture in the code-generation corpus, each side built at its own default optimization level as the two command lines really build them:

   cargo test -p inference-tests --lib \
     codegen::wasm::target_identity::target_identity_tests::every_target_emits_what_the_default_target_emits
   

Break either link and the .v describes a program that is not the one on the vehicle. Both hold, so it is.

Appendix A: Optimization Levels

OptLevel is a single per-build value recorded on the compiled output — not a per-function-kind setting, and not something the compiler itself currently acts on. No optimization pass runs during WASM emission in either mode: the descriptions below are the levels' intended meaning for a future consumer (a wasm-opt integration, say), not present-day behavior.

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(mut ptr: i32, len: i32);
use { sort } from collections;

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

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

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

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

Qualified Access with ::

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

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

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

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

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

use lib::geo::{Point};

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

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

Visibility

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

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

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

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

Visibility rules:

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

Re-exports

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

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

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

// main.inf
use math;

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

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

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

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

Cross-File Type Identity

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

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

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

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

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

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

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

Import-Closure Walk

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

The algorithm:

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

Properties of the walk:

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

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

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

WASM Codegen and Function Naming

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

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

The function names written into the WASM name section (and visible in .wat output) are file-qualified for every non-entry-file function: the symbol is FnKey::name_section_symbol(), which joins the defining file's .-separated module path onto the bare name (or StructName.method_name for a method). An entry-file function keeps its unqualified name (add, Point.new); an add in lib/arith.inf is lib.arith.add, and a method defined in lib/geo.inf is lib.geo.Point.dist. This is the same dot-qualified string FnKey::Display renders for free and method keys, and it appears exactly this way, verbatim, in the binary's name section — it is not merely an internal function-index lookup key.

Because two functions in different files ordinarily write distinct strings, the WAT renderer has nothing left to disambiguate when their bare names collide: no numbered suffix, no (@name …) annotation.

The join is not injective, though: a method's StructName.method_name and a free function's file-qualified name are both built by joining segments with the same ., so the two shapes can land on one string. A method make on a struct mid defined in lib.inf and a free function make defined in lib/mid.inf both render lib.mid.make — the struct join and the file-path join are indistinguishable once written. Codegen only rejects this when it would actually mislead something: CodegenError::NameSectionSymbolCollision fires exclusively when a proof obligation applies the colliding symbol (a T_app or HA_app_ok head), since the name section is read by a symbol only there. The two functions still get distinct Rocq Definition names and distinct WASM indices regardless of the shared name-section string, so a collision nothing applies is harmless and the program keeps building — but the WAT text does still show it the old way: with two functions genuinely sharing one name-section entry, the renderer's own duplicate-name fallback (the numbered synthetic id plus (@name …) annotation from before file qualification existed) is exactly what fires, e.g. (func $"#func1 lib.mid.make" (@name "lib.mid.make") ...) for the second. That fallback did not go away; qualification only makes it unreachable for the common case of two same-kind functions in different files. Only the Free and Method keys can collide this way; a specification function is the deliberate exception to file qualification in the first place — its symbol stays bare regardless of its defining file, because spec membership travels separately as indices in inference.spec_funcs rather than through the name section (see Specs in Multi-File Proofs below), so it is never a candidate for this check either.

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 $lib.arith.add ...)          ;; add is compiled, file-qualified, and unexported
)

Specs in Multi-File Proofs

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

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

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

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

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

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

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

// main.inf
use lib::checks;

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

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

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

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

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

Current Limitations

• No import aliasing. use lib::arith as ar; is not supported. The module must be accessed through its canonical path.
• No per-field visibility. Struct fields inherit the struct's pub or private visibility. There is no pub modifier on individual fields.
• Circular const 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, on itself — is rejected with a CircularDefinition error.
• Bare infc src/main.inf treats src/ as the source root. In this mode, sibling .inf files under src/ that are not reachable from main.inf produce unreachable warnings. The infs project toolchain (see Projects and the infs Toolchain) handles project-level discovery and build coordination.

Comparison with Other Languages

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

Formal Implications

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

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

Related Resources

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

Projects & the infs Toolchain

Motivation

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

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

Project Layout

infs new myproject scaffolds the following structure:

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

The layout mirrors Cargo's conventions: manifest at the root, sources under src/, build outputs under out/. The out/ directory is not committed; it is created automatically by infc (relative to its working directory, which infs sets to the project root). proofs/ is tracked via .gitkeep so that curated hand-authored proof sources stay in version control even when generated .wasm/.v artifacts are gitignored by extension. What coqc writes when one of those proofs is checked — a .vo, a .glob, a .<module>.aux — is gitignored too, and anywhere in the project rather than only under proofs/: a .v can be hand-authored, so its location decides whether it is output, while coqc's products never are and land beside whichever source it is given.

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]
# The runtime the module is built for; "wasm32" (the default) is generic
# WebAssembly, "stellar" builds a Soroban smart contract, and "spacewasm"
# builds for the SpaceWasm flight interpreter. Validated on load: an
# unrecognized name is an error.
# target = "wasm32"
# "compile" (default) or "proof"
mode = "compile"
# Post-MVP WebAssembly proposals to opt into; empty (the default) keeps the
# output pure WebAssembly 1.0. Currently supported: "bulk-memory".
# wasm-features = ["bulk-memory"]
# "all" (default) keeps every array bounds guard; "omit-proven" drops the
# guards the analysis proved can never fire.
# bounds-checks = "all"
# optimize is recognized but not yet consumed.

# [memory]
# Linear memory of the emitted module; any key may be given alone. The memory
# is fixed at `pages` unless `max-pages` lets a linked module or the host grow it.
# `import = true` imports it from the host as `env.memory` instead of defining
# it, for the `wasm32` target only, and not in a proof build.
# pages = 1
# max-pages = 1
# stack-size = 65536
# import = false

[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" }

# [host-imports]
# The host functions the program may bind, one array per import module; a
# header with no keys admits none. Omit the table to apply no policy.
# fprime_core = ["telemetry", "command"]
# env = ["clock_ms"]

The fields:

target and mode are case-sensitive: "Wasm32", "SpaceWasm" and "Proof" are all rejected, and neither key trims whitespace. The wire spelling of every target name is one lower-case word, so "space-wasm" and "space_wasm" are rejected too. Both are validated on load; an invalid value is an immediate error with the allowed set named in the message, never a fall back to the default. target names the same vocabulary as infc --target and is rejected with the same wording; "soroban", the former name of "stellar", earns a message redirecting to the current spelling rather than the generic unknown-target one.

target = "stellar" narrows the rest of the manifest. It cannot be combined with a [build.wasm-opt] table — that pairing is itself a load error, because whether an external Binaryen preserves a contract's value-ABI wrappers and its contractenvmetav0 section depends on a version nothing here pins — it admits no wasm-features, mode = "proof" is a load error too, and infs run refuses the project outright, since a contract is invoked by a Soroban host and not by a plain WebAssembly runtime. What an exported function may declare is narrowed too; see Compilation Targets. A [memory] that imports its memory (import = true) is not narrowed on load, here or at "spacewasm": the manifest loads, and the compiler refuses the build, naming the setting to remove (see Importing the memory).

target = "spacewasm" narrows it less, and the difference is instructive. It admits no wasm-features and no mode = "proof", on load, for the same reason — the interpreter decodes neither the post-MVP families nor the custom 0xfc instructions. But it keeps [build.wasm-opt], because what that refusal protects is a contract's wrappers and its contractenvmetav0 section, and this target's module has neither, and it keeps infs run, which executes the build in process under the SpaceWasm interpreter itself rather than under wasmtime. Nothing narrows what an exported function may declare: the bytes are the "wasm32" build's. The same load-time strictness applies to keys: every fixed-schema table rejects a key it does not recognize, naming the offending key and the fields the table accepts — a misspelled wasm_features fails the build rather than silently shipping a differently-configured artifact. Three tables accept arbitrary keys, because their keys are the data: [dependencies] and [wasm-dependencies], whose keys name dependencies, and [host-imports], whose keys name the import modules an embedder registers host functions under. wasm-features entries are WebAssembly proposal names ("bulk-memory"), not instruction names, and the setting is honored in project builds, single-file builds, and single-file infs run. [wasm-dependencies] entries have the same reach: project build, project run, single-file build, and single-file run all forward every declared entry to infc, and all four forward a [host-imports] table too. The unknown-key refusal first shipped in v0.0.6, though: a release through v0.0.5 reads past a root table it does not know with no diagnostic, and for [host-imports] that means building under no policy at all, so a project that relies on its allowlist has to be built with an infs that knows the table. See apps/infs/docs/inference-toml.md for the full reference.

Reserved Project Names

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

Reserved Module Segment

A module name has one reservation of its own, separate from the project-name set above and applied in a different position: host as the first segment of a use … from clause names the embedder, not a module this build links. So use { clock_ms } from host::env; binds a host import of the module env, and a [wasm-dependencies] key whose first segment is host — host, or host::io — is refused on every build and run route before infc is asked to build, because no linked module can be named under it; a host import needs no dependency entry at all, and belongs under [host-imports] if the project keeps an allowlist. The match is exact and first-segment only: hostlib, Host and a::host are ordinary module names. Contrast the path grammar's reserved root, which names the entry file in use root; and shadows a literal src/root.inf — root is reserved among the files of this project, host among the modules outside it. See What host reserves, and what it does not.

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.

A manifest with [memory] import = true has no proof artifact, so infc refuses every build of it that writes a .v: -v, --mode proof, and the --mode proof that infs passes for a project whose manifest sets [build] mode = "proof". Build the imported-memory module with infs build --mode compile, which overrides the manifest's proof mode. infs has no per-build override for [memory] import, so a project builds the proof of the same program with import set to false or removed. That proof is about the defined-memory module. It carries over to the imported-memory one only under premises that are documented rather than proved, and only for a program that binds no host import, since infc refuses a .v for every host-import program whichever way its memory is built (see An Imported Memory Has No Proof Artifact).

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

A build that writes a .v names the Rocq module after the source file's stem, so in single-file mode the stem has to be usable as one. infs build term.inf -v is refused in infc's words, with no artifact, because term is a name the proof contract declares and the module record would shadow it for any proof that imports the .v after the contract library; the message says to rename the file to term_module.inf. Refused: a stem that is not a legal Rocq identifier (my-prog, café), one containing __ or longer than 255 characters, one ending in _ when the program has a spec, a Rocq keyword or curated prelude name, a preamble helper, a contract name, or ho; a stem that is not valid UTF-8 is refused too. The infc README lists the rules in full. The same file builds without -v or --mode proof, since the .wasm has no Rocq name. Project mode compiles src/main.inf, whose stem main is never reserved. The rule and its rationale are in Reserved names.

infs run

infs run builds and then executes the resulting WASM where the build's [build] target says: a wasm32 build under wasmtime, and a spacewasm build in process under the SpaceWasm interpreter, with the F´ (F Prime) reference host functions and no wasmtime at all (see Running a SpaceWasm build). A stellar build is refused before anything is built.

infs run                                 # project mode: build + invoke main
infs run program.inf                     # single-file: compile and invoke main
infs run program.inf --entry-point helper  # single-file: invoke helper()
infs run program.inf -L libs             # single-file: search libs/ for external .wasm
infs run --fuel 1000000                  # spacewasm: stop after 10^6 interpreter instructions

Flags:

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

In project mode (no path given):

• Always builds in compile mode, regardless of [build] mode in the manifest. Proof-mode WASM embeds custom non-deterministic opcodes (0xfc family) that neither wasmtime nor the SpaceWasm interpreter can decode. The one thing [build] mode can still do to run is stop it before it starts: mode = "proof" paired with a target that has no proof mode is a load error for every command, run included — a value run would ignore can still refuse to be read.
• Always invokes main, with no arguments, so a main that takes any runs only in single-file mode: one that declares parameters, and one that returns a struct or array, which takes a hidden result address (see below). Such a main is refused before it is invoked, on either runtime, naming what it takes and the single-file command that passes it. Passing --entry-point to anything other than main is rejected with guidance to use single-file mode instead.
• For a wasm32 build, checks wasmtime availability before starting the build, failing fast if the runtime is absent; a spacewasm build never looks for it.
• Resolves the manifest's [wasm-dependencies] and forwards any -L directories the same way project build does, anchored to the invocation directory, so a project binding use { … } from <module> runs without a separate link step.
• out/main.wasm is the expected artifact; if the build succeeds but the file is absent, run errors before executing anything.
• Judges the imports of the artifact it built — after [build.wasm-opt], so the bytes it asks about are the ones that would run — before anything runs. A wasm32 artifact that imports any function is refused: run registers no host function under wasmtime, and does not let wasmtime stand in for the embedder a program binding use { … } from host::… is written for — not even for the WASI functions the wasmtime CLI provides on its own. The refusal names each import and, when every one is an F´ reference host at its reference signature, the spacewasm target that provides them. The wasmtime check above still comes first, so a machine without the runtime is told to install it before it can hear this refusal. A spacewasm artifact may import the F´ reference hosts at their reference signatures and nothing else, and one that imports anything else is refused before the interpreter decodes a byte of it. Single-file run refuses the same way, naming out/<stem>.wasm.
• Supplies the memory a wasm32 artifact imports, the one import it does supply under wasmtime. A project built with [memory] import = true produces a module that imports env.memory, and the wasmtime command line provides no such memory, so the module would not instantiate. run reads the limits of the import off the artifact itself — after linking and [build.wasm-opt], so they are the limits of the bytes that run, not the manifest's — writes a small module that defines and exports one memory at exactly those limits beside the artifact, under a name that is this run's own (out/main.wasm.<pid>-0.memory), and invokes wasmtime with --preload env=out/main.wasm.<pid>-0.memory ahead of --invoke. The file is removed when wasmtime returns, whether the run succeeded or failed, and because each run creates its own, two runs of one artifact that overlap never share or remove each other's. An artifact that imports a function as well as its memory is still refused, for the function. Single-file run supplies the memory the same way, beside out/<stem>.wasm. Nothing else touches that memory and no other module shares it, and a project's main takes no argument and returns no struct or array, so a project's run meets the embedder contract by construction. A single-file run of an entry point that takes or returns a struct or array does not: the supplied memory has no pages above the module's, so the addresses typed on its command line, which run passes on unchecked, can only point into the module's own pages.
• As in infs build, which shares this step, holds [build.wasm-opt] to the memory import the compiler wrote. Binaryen output that adds, removes, renames or re-limits it is refused, as output importing a function the compiler's artifact did not already import is: the build fails, the optimized output is discarded, and the artifact infc wrote stays in place. The import is a contract with the host, not an interface the optimizer may narrow. infs never passes Binaryen's --zero-filled-memory, because a memory the host supplies is not zero-filled and the flag would let the optimizer drop the zero bytes of the constants segment the module writes into it.

In single-file mode (path given), --entry-point (default main) selects which exported function to invoke, and that function receives the trailing arguments from the command line — anything after the first bare token that options did not consume, or after --. main is no exception: each argument becomes the matching parameter of the compiled function, so infs run program.inf 41 hands 41 to a pub fn main(x: i32). Under wasmtime the arguments are handed to wasmtime as written, and it parses them; under the SpaceWasm interpreter run reads each as the parameter's i32 or i64, in its signed or its unsigned range, and refuses a count that differs. Those parameters are the ones the source declares, with two differences that apply to every function, main included. A struct or array parameter is a memory address. A function that returns a struct or array takes the address to write its result to as a hidden first parameter and returns nothing, so pub fn main() -> [i32; 4] needs that address on the command line and prints no value. run passes these addresses as numbers and checks none of them. Single-file run also resolves the enclosing manifest's [wasm-dependencies] and forwards any -L directories verbatim: infc inherits the invoking shell's working directory here, so a relative -L already means what it meant at the shell, with no anchoring step needed.

A wasm32 build requires wasmtime in PATH, in both modes, and installation instructions are printed when it is not found. A spacewasm build requires no runtime at all: the interpreter is part of infs.

Scaffolding

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

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

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

// Entry point for the Inference program

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

Toolchain Management

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

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

Relationship to infc

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

infs build / infs run (project mode)
    |
    +-- discover_and_load(Inference.toml)
    |
    +-- find_infc_with_source()  # INFC_PATH > sibling of infs > system PATH > managed toolchain
    |
    +-- compatibility handshake
    |       infc --commit-hash    # short-circuit: same-build binaries always compatible
    |                             # sibling tier only: differing commits warn (stale neighbour)
    |       infc --abi-version    # major mismatch → hard error; minor mismatch → warning
    |
    +-- spawn infc
            CWD = <project root>
            arg: src/main.inf
            arg: -v                     (if .v requested; `run` never requests it)
            arg: --mode proof           (if effective proof mode; `run` never requests it)
            arg: --out-dir <dir>        (if effective proof mode + ABI ≥ 1.1; `run` never requests it)
            arg: --wasm-lib-dir <dir>   (one per -L/--wasm-lib-dir; a relative
                                         dir is anchored to the invocation
                                         directory, since infc runs at the root —
                                         `build` and `run` both pass their own
                                         `-L` flags through here)
            arg: --wasm-dep name=path   (one per [wasm-dependencies] entry; the
                                         declared path resolved against the root)
            arg: --target <name>        (if [build] target names a non-default
                                         target; gated on that name's own minor)
            arg: --wasm-features <list> (if [build] wasm-features requests any;
                                         requires infc ABI ≥ 1.2. Applies in both
                                         modes — a `.v` describing a different
                                         instruction set than the shipped `.wasm`
                                         would be worthless)
            arg: --bounds-checks <policy> (if [build] bounds-checks is
                                         "omit-proven"; ABI ≥ 1.9; both modes)
            arg: --memory-pages <n>     (if [memory] declares `pages`; ABI ≥ 1.3)
            arg: --max-memory-pages <n> (if [memory] declares `max-pages`;
                                         ABI ≥ 1.10)
            arg: --stack-size <n>       (if [memory] declares `stack-size`; ABI ≥ 1.3)
            arg: --import-memory        (if [memory] sets `import = true`;
                                         ABI ≥ 1.11)
            arg: --adopt-external-specs (if [verification] asks for it on a
                                         proof-artifact build; ABI ≥ 1.4; `run`
                                         never requests it)
            arg: --host-imports=<list>  (if a [host-imports] table is declared,
                                         as one argument — `--host-imports=` for
                                         a table with no keys; requires infc
                                         ABI ≥ 1.8)

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

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

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

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

infs run <path> (single-file mode)
    |
    +-- enclosing_manifest(path)   # walk up from the source file; optional
    |
    +-- compatibility handshake     # conditional — runs only when the
    |       infc --commit-hash      # enclosing manifest asks for something an
    |       infc --abi-version      # older infc could not honor: a target,
    |                               # wasm-features, bounds-checks =
    |                               # "omit-proven", a [memory] table, or a
    |                               # [host-imports] table (present, even
    |                               # empty); skipped entirely otherwise,
    |                               # unlike `build`
    |
    +-- spawn infc
            CWD = inherited from the invoking shell
            arg: <path>
            arg: --parse                (always; `build` never sends it)
            arg: --codegen              (always; `build` never sends it)
            arg: -o                     (always; `build` never sends it)
            arg: --wasm-lib-dir <dir>   (one per -L/--wasm-lib-dir, forwarded
                                         verbatim; no anchoring step runs)
            arg: --wasm-dep name=path   (one per [wasm-dependencies] entry from
                                         the enclosing manifest, if any)
            arg: --target <name>        (as the project route sends it)
            arg: --wasm-features <list> (if the enclosing manifest requests any;
                                         requires infc ABI ≥ 1.2)
            arg: --bounds-checks <policy> (as the project route sends it)
            arg: --memory-pages <n>     (as the project route sends them)
            arg: --max-memory-pages <n>
            arg: --stack-size <n>
            arg: --import-memory
            arg: --host-imports=<list>  (if the enclosing manifest declares a
                                         [host-imports] table; one argument;
                                         requires infc ABI ≥ 1.8)

run always requests --parse --codegen -o explicitly rather than relying on infc's default, and neither -v nor --mode is ever part of its argv: the RunArgs struct (apps/infs/src/commands/run.rs) carries no such flags. Once infc exits, both run routes read the imports off the artifact they are about to execute before anything runs: a wasm32 artifact that imports any function is refused before wasmtime is invoked, since run registers no host function there, while one that imports only its memory has that memory supplied; and a spacewasm artifact importing anything but the F´ reference hosts at their reference signatures is refused before the interpreter decodes it — see infs run.

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

Note: The current ABI version is 1.11.

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.11 (COMPILER_ABI_MAJOR = 1, COMPILER_ABI_MINOR = 11 in core/compiler-interface/src/lib.rs). Each additive flag is gated at the minor it was introduced at, independently: --out-dir landed at minor 1, --wasm-features at minor 2, --memory-pages and --stack-size at minor 3, --adopt-external-specs at minor 4, --target at minor 5, --host-imports at minor 8, --bounds-checks at minor 9, --max-memory-pages at minor 10, and --import-memory at minor 11. infs forwards each only to an infc that reports an ABI minor at or above the flag's own (or matches by commit hash) — an infc that reports minor 1, for instance, supports --out-dir but not --wasm-features. --host-imports is forwarded from the [host-imports] table, and only from a declared one, so a project without the table puts no minor-8 floor under its compiler; a project with one is refused against an older infc rather than built without the flag, because that compiler would admit every host import the program binds and write an artifact identical to the one the table exists to police. --target is gated on the name rather than on the flag: each target became requestable at its own minor (wasm32 at 5, stellar at 6, spacewasm at 7), and an infc that parses the flag but predates a name would accept it and build for the default runtime — a wrong artifact rather than a refusal. That is true even where the two builds are the same bytes: dropping spacewasm produces the module a wasm32 build produces and drops the target's acceptance envelope with it, so what the name was written for never runs. The default target is never forwarded at all, so a project that names none puts no floor under its compiler. [memory] is gated per key for the same reason: pages and stack-size need minor 3 and max-pages minor 10, so a project that declares no maximum puts no minor-10 floor under its compiler, and one that does is refused against an older infc rather than built with a fixed memory. import = true needs minor 11 on its own, and its gate is the one that matters most: built without the flag, the module defines its own memory, and an embedder that resolves imports by name, as the JavaScript API and wasmtime's Linker do, ignores the env.memory it supplies and the module never asks for. The module instantiates, and the host then reads and writes a memory the module never touches, with nothing to say so. import = false forwards nothing and gates nothing, so a project that sets only the numbers builds against minor 3 or 10 as before. Pairing a manifest with a non-default [verification] output-dir against an older infc is a hard error:

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

Compiler Resolution

infs locates infc by checking, in order:

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

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

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

Comparison with Cargo

The parallels to Cargo are intentional:

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

Current Limitations

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

Related Resources

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

External Functions and WASM Linking

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

Self-contained holds for every use … from clause that names a file. A clause whose first segment is host names none: the function is supplied by whatever embedder instantiates the module, there is nothing for the link step to merge, and the import survives into the artifact on purpose. Such a program's .wasm is deliberately not self-contained — see Host Imports.

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;

Its parameter and return types may be any a function signature can name, including a struct or enum declared in another file, written the same way: geo::Point under use geo;, or Point under use geo::{Point};. A struct or an array reaches the foreign function as the i32 address of the caller's value and an enum as its i32 tag, so at the WebAssembly level

use geo;

external fn send(p: geo::Point, l: geo::Level) -> i32;

is a function of two i32 parameters returning an i32.

A named parameter may be declared mut:

external fn store_at(mut ptr: i32, val: i32);

mut on a linked external fn parameter declares that the foreign body may store through the address that parameter denotes — for a compound parameter that is the pointer the caller hands over, for a scalar it is the integer's own value. This is a claim about the linked library, not a request: the linker derives, from the merged .wasm bytes, which parameters the body actually stores through, and rejects the link when that set is not covered by the declaration. An external whose body stores through an undeclared parameter fails to link with UndeclaredExternWrite; a parameter declared mut that the body never writes through links anyway, since mut here is a permission the body is not obliged to exercise. The linker's side of this check — including exactly what it does and does not prove about where a declared store lands — is the subject of The WASM Linker.

The word linked carries the whole of what makes this a check rather than a claim: the derivation reads the merged body's bytes. A host import has no bytes in this build, so mut on one is an assertion nothing tests — see mut on a host parameter.

The set this check requires you to declare is looser than "the parameter itself denotes the address" suggests. Attribution is affine: a store's address is attributed to every parameter that may contribute a term to it, not only the one playing the role of base pointer. The ordinary scaled-index write mem[ptr + (idx << 2)] = val attributes to both ptr and idx, so external fn set_elem(ptr: i32, idx: i32, val: i32); bound to a body that writes this way must declare set_elem(mut ptr: i32, mut idx: i32, val: i32); — idx included, even though idx never itself denotes a location the body writes to; it only scales ptr's. Narrowing the attribution to the one operand that "looks like" a base pointer would need the linker to tell a base from an offset, which an affine form alone does not carry; the safe direction to err in is attributing too broadly, since that can only demand a wider declaration than the informal reading of mut suggests, never let an undeclared write through. This over-attribution is specific to a store's own address computation: a read-only pointer, such as the source of a memory.copy(dest, src, size), contributes to no store's dependency and so is never forced mut merely for being touched by the same instruction that writes dest.

mut is required on every parameter a linked external's body stores through, compound or scalar alike — there is no exemption for a pointer-shaped i32. Passing a compound argument (a struct or an array) to a mut position additionally requires the argument to be rooted at a mut binding, enforced at the call site by analysis rule A047 (see Static Analysis): exactly the same requirement an ordinary assignment through that binding would carry, since a foreign store through a mut parameter is otherwise the one write in the language invisible at the call site. A scalar argument is not checked by A047 — it passes a value, not a region, so there is no binding at the call site for the rule to root — which keeps the check honest rather than complete: a foreign store through an undeclared caller-supplied integer is still possible and is closed only by a future containment analysis (issue #420).

Parameter names are optional in the declaration, for a parameter no merged body writes through:

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

The unnamed form and the named form are equivalent only when nothing is written through the parameter. Neither ArgKind::Ignored (_: i32) nor ArgKind::TypeOnly (a bare type) carries a mutability field, and the grammar gives neither a slot for mut, so a parameter a linked body stores through cannot be declared in the unnamed form at all: external fn sort_pair([i32; 2]); bound to a library that writes through it has an empty declared write set by construction and fails to link with UndeclaredExternWrite, whose message says to name the parameter first. Give every parameter of a writing external a name.

The type signature must match the exported function in the external module exactly. If the types disagree, the validation step (validate_extern, run by the link driver when it resolves each binding against the real .wasm bytes) reports a SignatureMismatch error and no linked module is produced. A related resolution-time check: two files that each declare and bind the same (module, field) must agree on which parameters are mut — a disagreement is rejected as ConflictingWriteSet, naming both files, since the linker checks the merged body once and cannot honor two different declarations of it.

A host import reaches neither check. There is no .wasm file to resolve it against, so validate_extern never runs on it and no SignatureMismatch is possible: the declarations are the only description of the function. What stands in their place is a consistency check among the declarations themselves — two files that declare one (module, field) at different lowered signatures are rejected as ConflictingHostSignature, and two that declare it with different mut parameters as ConflictingHostWriteSet, each naming both files. Neither compares a declaration to a body, because there is none to compare it to.

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

That is the resolution for a clause naming a file. A clause whose first segment is host names none, and consults none of these three sources: nothing is searched for and nothing on disk can satisfy it — see Host Imports.

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;

Host Imports

A use … from clause whose first segment is host binds its names to functions the embedder supplies at instantiation, not to functions this build links:

external fn telemetry(id: i32, mut time: [u8; 11], time_len: i32, value: [u8; 4], value_len: i32) -> i32;
use { telemetry } from host::fprime_core;
external fn clock_ms() -> i64;
use { clock_ms } from host::env;

host::fprime_core imports from the WASM module fprime_core, and host::env from env; the host segment names the provider, not a path component. The emitted entry is (import "fprime_core" "telemetry" …) — the same two-level name an embedder registers a host function under — and host appears nowhere in the artifact. Both belong to the F´ (F Prime) host set that spacewasm_std, the reference embedder in the SpaceWasm repository, registers, and are declared at its signatures: an array argument is passed as its address, so time and value each arrive as one i32, and the length after each says how many bytes the buffer holds.

What host reserves, and what it does not

host is reserved only as the first segment of a from clause. Everything else spelled host is untouched: a src/host/ directory and the files under it, the file import use host::x;, any variable, field, parameter, type or function named host, and a linked module whose name merely contains the segment, such as use { f } from a::host;.

The path grammar has a reserved handle of its own — root, which names the entry file (see Module Hierarchy and Multi-File Compilation) — and a reader looking for the symmetry should know where it stops. Both reserve one name in one position, but in different grammars: root is reserved in use root;, which names files in this project, while host is reserved after from, which names modules outside it. They differ in what becomes of a file of that name, too. root shadows a literal src/root.inf — the name resolves elsewhere, to the entry file — whereas a from host::… clause consults no file at all, so a host/io.wasm on disk is not shadowed by anything; it is simply never looked for.

Exactly one segment may follow host. use { f } from host::a::b; is refused, because an import module string is flat: what an embedder registers is a name, not a path, and WebAssembly has no nested module name for a runtime to take apart. Joining the segments into a::b would emit a name the author never wrote, so the compiler refuses the clause and says which one segment to keep.

mut on a host parameter is an assertion, not a contract

Declaring an External Function defines mut as a claim the linker checks: it derives the body's write set from the merged .wasm bytes and rejects a declaration that does not cover it. That definition is about a linked external. A host import has no bytes in this build, so nothing derives what the embedder's function stores through, and mut on a host parameter is the author's assertion and stays one — there is no UndeclaredExternWrite for a host import, because there is no body to read it from. A reviewer weighing what mut proves about a mission-critical program should read it as documentation at a host position and as a checked contract at a linked one.

The call site is still held to it. A047 requires a compound argument passed to a mut host parameter to be rooted at a mut binding, exactly as it does for a linked external and exactly as an ordinary assignment through that binding would. So the caller is constrained by the declaration; only the declaration itself is unverified, and the write — when it happens — is performed by code outside the artifact and outside anything the proof translation describes. A proof build that admitted host imports would therefore have to carry a mut host parameter as a frame condition on the call or refuse it, since nothing in the build derives a write set to check the declaration against; as it is, a proof build refuses any program that binds a host import (see No contract travels with a host import).

A bound host import is emitted whether or not it is called

The import is emitted for the binding, not for a call. An external fn bound to host::… and never called still appears in the import section of the artifact infc writes, and the module still fails to instantiate until an embedder offers a matching function. That is deliberate: the binding is where a program declares what its environment must supply, so the artifact infc writes carries every import the program declares, and what it requires of an embedder can be read off the source.

An optimized build narrows that interface to the imports the program uses, also by design. A project whose Inference.toml declares [build.wasm-opt] has Binaryen rewrite out/main.wasm in place after infc exits, and at any level other than "0", wasm-opt removes unused module elements — an imported function the program never calls among them (-O0 runs no passes and keeps it). The artifact that ships then declares only the host imports the program calls, and the build log says so right after the optimizer's size line, naming what went and what is left. This program calls command and telemetry and binds clock_ms without calling it:

external fn telemetry(id: i32, mut time: [u8; 11], time_len: i32, value: [u8; 4], value_len: i32) -> i32;
external fn command(opcode: i32, arg: i32) -> i32;
use { telemetry, command } from host::fprime_core;
external fn clock_ms() -> i64;
use { clock_ms } from host::env;

pub fn main() -> i32 {
    let id: i32 = command(1, 0);
    let mut time: [u8; 11] = [0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0];
    let value: [u8; 4] = [21, 0, 0, 0];
    return telemetry(id, time, 11, value, 4);
}

Its manifest admits all three and turns the optimizer on:

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

[host-imports]
fprime_core = ["telemetry", "command"]
env = ["clock_ms"]

[build.wasm-opt]
level = "z"

and infs build, with Binaryen 130, prints:

host-imports allowlist: env.clock_ms, fprime_core.command, fprime_core.telemetry
Parsed: src/main.inf
Analyzed: src/main.inf
Codegen complete
host imports: env.clock_ms, fprime_core.command, fprime_core.telemetry
WASM generated at: out/main.wasm
wasm-opt -Oz: main.wasm 300 -> 202 bytes
wasm-opt removed 1 host import the program never calls: env.clock_ms; the artifact now imports fprime_core.command, fprime_core.telemetry

So in an optimized build, editing a caller out can change what a deployment must provide, and never silently: the last word on the imports in the log describes the artifact that ships, and a build whose imports the optimizer left alone prints no such line. The allowlist still bounds what ships, by construction: the optimizer may only remove imports, and optimized bytes importing a function the artifact infc wrote did not import are refused, leaving that artifact in place, so every import that ships is one infc admitted. The memory import of a build that imports its memory ([memory] import = true; see Importing the memory) is held tighter still, because it is a contract with the embedder rather than an interface the program may narrow: it must survive unchanged, so optimized bytes that remove, rename or re-limit it, or add one the artifact did not have, are refused the same way. infs run judges the final bytes, so a program whose host imports are all uncalled runs under it once they are optimized away (see Running a program that binds host imports).

What is refused, and by which layer

The proof refusal is raised before external resolution deliberately. A program that is both mixed and a proof build would otherwise hear the mixed-program refusal first, and its first remedy is to bind every extern to host::… — advice that walks the author into the proof refusal having rewritten every clause for nothing. It asks for the build without the artifact rather than naming a mode, because -v requests a .v on its own and --mode compile -v is a spelling that already has the mode the advice would otherwise ask for. It asks for every request to go — a build can pass both, and dropping one of two changes nothing — and names the one a reader may not have typed: infs build passes --mode proof itself for a project whose Inference.toml sets [build] mode = "proof", and there the setting is what to change.

The rest of the order follows the same rule: a refusal is raised before any other whose remedy it would make void. The stellar refusal sits beside the proof refusal for the same reason, and ahead of the allowlist too, which would otherwise ask for an entry admitting an import the target refuses anyway. The SpaceWasm registration caps come before the allowlist because an allowlist entry has to spell the import's final name: asked the other way round, the allowlist asks the reader to admit a name no embedder can register, and the rename the caps then ask for leaves that entry matching nothing. The imported-memory refusal of a binding is raised before external resolution too: a linked binding whose library is missing would first read "External module resolution failed", and a host import named env.memory would be told by the allowlist to admit env.memory, and each remedy only leads into that refusal.

The allowlist

infc --host-imports=<list> names the host functions a build may bind, as comma-separated module.field pairs:

infc prog.inf --host-imports=fprime_core.telemetry,env.clock_ms

The flag has three states, and the = is required so that the empty one is spellable at all:

An import outside the allowlist is refused before any file is written, and every unadmitted import is reported by one build rather than one per rebuild. The findings are grouped one paragraph per import module, naming every unadmitted field of it in one edit, because both the flag and the table hold one list per module: two separate paragraphs about env would ask for a duplicate table key and for two halves of one command-line list.

Entries are trimmed, so a list pasted out of the inventory line — which separates its pairs with , — is read as written, provided the paste is quoted:

infc prog.inf --host-imports="env.clock_ms, fprime_core.telemetry"

Unquoted, the shell splits the list at each space before infc sees it, and the second pair arrives as an argument of its own, which infc refuses as unexpected without mentioning the space. An entry that is empty once trimmed is a stray or trailing comma and is named as one, since --host-imports= is the deliberate spelling one character away from it.

The separator here is a dot and never ::, and an entry that uses :: is told so. The clause being transcribed is use { clock_ms } from host::env;, and both of its obvious transcriptions are wrong: env::clock_ms keeps the path separator, and host::env.clock_ms keeps a segment that names the provider and is never part of an import name. The entry is env.clock_ms, and the refusal spells the entry its reader meant — for fprime_core::telemetry or host::fprime_core::telemetry alike, fprime_core.telemetry — naming as the fault whichever of the two mistakes the entry actually makes.

A project keeps its allowlist in Inference.toml, one array of field names per import module, and infs fills the flag from it:

[host-imports]
fprime_core = ["telemetry", "command"]
env = ["clock_ms"]

The table has the flag's three states. Absent, no policy applies. Declared with no keys under it, it admits no host function at all — the state --host-imports= spells on a command line. With keys, it admits exactly the fields it lists. Every route that compiles a project — infs build, infs run, and both of their single-file forms — forwards it as one argument, since the flag requires its =: --host-imports=env.clock_ms,fprime_core.command,fprime_core.telemetry, sorted by module and then field whatever order the manifest listed them in, or exactly --host-imports= for the empty table. Each also echoes the policy before infc runs:

host-imports allowlist: env.clock_ms, fprime_core.command, fprime_core.telemetry
host-imports allowlist: empty (no host function admitted)

The echo is what shows a policy was applied; the inventory line infc prints next says which imports that policy admitted. The forward is gated on compiler ABI 1.8, the minor --host-imports landed at, and an older infc is refused rather than handed the build without the flag: it would accept every host import the program binds, and the artifact it wrote would be byte for byte the one the table exists to police.

The table is validated whenever the manifest is loaded, not only where it is forwarded — a malformed allowlist is a defect in a policy, and a project carrying one should not build anything. A key is one import module name: host::env and env::v2 are both refused, because the module string an embedder registers is flat — it never contains :: — and the host:: prefix of the clause names the provider and is not part of it, so the key for use { clock_ms } from host::env; is env. Each value is a non-empty array of field names, each an identifier and none listed twice. The empty array is refused rather than read as "nothing from this module" because the flag has no spelling for a module with no admitted field; keeping every key populated keeps the table's modules and the flag's the same set, which is what lets an infc refusal tell its reader whether to add a key or to add a name to the entry already there.

The inventory line

infc prints one line naming every pair it emits, sorted by module and then field:

host imports: env.clock_ms, fprime_core.telemetry
host imports (no allowlist): env.clock_ms, fprime_core.telemetry

The parenthetical is not decoration. It separates an import admitted by a reviewed policy from one admitted by the absence of a policy, which two otherwise identical build logs cannot be told apart by.

In a project whose [build.wasm-opt] step runs above level "0", the set that ships can be smaller, and a wasm-opt removed … line printed after this one then names it (see A bound host import is emitted whether or not it is called). The inventory line is also the only compile-time surface that reports the silent reinterpretation described next, so it is worth reading even on a build that succeeds.

The breaking change

host was an ordinary module name before it was reserved, and two spellings changed meaning:

• use { f } from host; no longer resolves host.wasm. It is a malformed host clause now, and is refused with the spelling to write instead.
• use { f } from host::io; used to resolve host/io.wasm and link it. It is a host import of the module io now: no file is read, the embedder becomes responsible for f, and the build still succeeds. No build diagnostic is issued — the inventory line is where the change shows up, and infs run refuses the program, naming io.f.

The remedy for either is to rename the module out of that first segment: the .wasm file or directory, the [wasm-dependencies] key or --wasm-dep name, and the use … from clause that binds it.

No contract travels with a host import

Nothing in this build describes what a host function does. There is no .wasm to validate the declared signature against, no write set to derive from a body, and no specification an embedder is held to. The declaration is the only description, and it is checked for internal consistency — two declarations of one pair must agree — and for nothing else. That is why a proof build is refused rather than qualified: a .v written over a module with an unmodelled hole in it would claim more than the artifact supports. Admitting host imports into a proof build later means giving the author a way to state the contract, so a host import's declaration may come to carry more than a signature.

Running a program that binds host imports

A program that binds a host import runs under the embedder that supplies it. infs run supplies one set of host functions, and to a spacewasm build only: the F´ (F Prime) reference hosts of spacewasm_std, the reference embedder in the SpaceWasm repository, at the signatures that embedder registers them with (Running a SpaceWasm build lists them). A spacewasm build whose imports are all among them runs in process under the SpaceWasm interpreter, each host logging its calls to stderr; one that imports anything else, or a reference host at another signature, is refused with nothing executed, naming each such import and the declaration that would match.

A wasm32 build runs under wasmtime. There infs run registers no host function, though it does supply the linear memory of a program built to import its own (below), and it does not let wasmtime stand in for an embedder either — not even for the WASI functions the wasmtime CLI provides on its own, which a program importing them could otherwise run against. Which host functions happen to be at hand is a property of the runtime, not of the program. infs run therefore builds such a program and then refuses to execute it, naming each function the artifact imports — and, when every one is an F´ reference host at its reference signature, the target that provides them:

Error: `infs run` cannot execute this program at the `wasm32` target: out/main.wasm imports 3 functions that its embedder must supply.
  env.clock_ms
  fprime_core.command
  fprime_core.telemetry
A `wasm32` build runs under wasmtime, where `infs run` registers no host functions. All three are F Prime reference hosts, which `infs run` provides to a `spacewasm` build: set `target = "spacewasm"` under `[build]` in Inference.toml and run it again to execute the program under the SpaceWasm interpreter. Otherwise, run it from the embedder that supplies them. See the book's External Functions and WASM Linking chapter ("Running a program that binds host imports").

A project whose manifest sets mode = "proof" or a wasm-features list, which a manifest naming the spacewasm target may not, or a [memory] that target refuses when the build runs — a max-pages above pages, or import = true — is told to remove them as well as to set the target. A file outside any project is told to run infs init first, since it has no manifest to name a target in. A program with any other import is told only that infs run provides host functions to a spacewasm build alone, and only the F´ reference set at its reference signatures, and to run it from the embedder that supplies them.

A program built to import its linear memory ([memory] import = true) is not refused on that account. infs run supplies the memory, one defined at exactly the limits the artifact's own import declares, and runs the program against it; an artifact that imports a function as well as its memory is refused for the function. See infs run for how the memory is supplied.

The refusal is decided from the artifact rather than from the manifest, because a [host-imports] table is an allowlist and not a declaration: a project can list functions it never binds, or bind them with no table at all. It is asked of the bytes that would run, too — in a project build, the bytes [build.wasm-opt] leaves behind, which may have lost an import nothing calls (see A bound host import is emitted whether or not it is called).

An embedder registers each function under the two names its import carries, before it instantiates the module. For a program declaring

external fn telemetry(id: i32, mut time: [u8; 11], time_len: i32, value: [u8; 4], value_len: i32) -> i32;
use { telemetry } from host::fprime_core;
external fn clock_ms() -> i64;
use { clock_ms } from host::env;

an embedder using wasmtime's Rust API registers the following. The two arrays arrive as addresses into the calling module's linear memory, which every module this compiler emits with a linear memory exports as memory, so the host reaches them through the caller:

let mut linker = wasmtime::Linker::new(&engine);
linker.func_wrap(
    "fprime_core",
    "telemetry",
    |mut caller: wasmtime::Caller<'_, ()>,
     id: i32,
     time_ptr: i32,
     time_len: i32,
     value_ptr: i32,
     value_len: i32|
     -> i32 {
        /* write the time and read the value through `memory`, then forward
           them to the flight software's telemetry channel */
        0
    },
)?;
linker.func_wrap("env", "clock_ms", || -> i64 { /* read the mission clock */ 0 })?;
let instance = linker.instantiate(&mut store, &module)?;

A program built with [memory] import = true imports its memory too, as env.memory ahead of these functions, so an embedder like this one also defines that memory before it instantiates. For pages = 2, whose maximum is then also 2, the host builds a memory with exactly those limits:

let memory = wasmtime::Memory::new(&mut store, wasmtime::MemoryType::new(2, Some(2)))?;
linker.define(&store, "env", "memory", memory)?;

What the embedder may supply, and what it must leave alone once the module is instantiated in it, is stated in The embedder contract.

An embedder of the SpaceWasm interpreter registers through spacewasm's host API instead: one HostModule per import module name, handed to the engine before the artifact is decoded, because the decoder binds each import against that set as it reads it. For clock_ms, with spacewasm 0.7.1:

use core::ops::ControlFlow;
use spacewasm::{Engine, HostFunction, HostModule, HostName, HostValList, Value};

let clock_ms = HostFunction::try_new(
    HostName::try_from_str("clock_ms")?,
    HostValList::try_new("")?,  // no parameters
    HostValList::try_new("I")?, // one i64 result
    |_engine, _args| {
        ControlFlow::Continue(Some(Value::I64(/* read the mission clock */ 0)))
    },
)?;
let env = HostModule {
    name: HostName::try_from_str("env")?,
    globals: spacewasm::Vec::zero(),
    functions: spacewasm::Vec::from_array([clock_ms])?,
    memory: spacewasm::Vec::zero(),
    table: spacewasm::Vec::zero(),
};
let hosts = spacewasm::Vec::from_array([env])?;
let engine = Engine::new(stack_words, max_modules, hosts)?;

Either way, the signature registered must be the one the external fn declared, in WebAssembly's types — each array a single i32 address, as telemetry shows — since the artifact's import carries that type and the runtime checks it when it binds the import: wasmtime at instantiation, SpaceWasm while it decodes the module.

Without an embedder of your own, infs run on a spacewasm build is the ready-made way to run a program whose imports are the F´ reference hosts. For any other import, the repository's SpaceWasm harness is: each --host MODULE.FIELD=PARAMS[:RESULT] builds a function like clock_ms above that answers zero and logs each call it receives, and the harness runs the program under the flight interpreter. See Running a module under the embedder harness.

Calling an External Function

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

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

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

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

What the Compiler Emits (Intermediate Form)

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

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

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

The Link Step

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

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

After linking:

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

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

Memory-Merge Feasibility

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

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

That is a necessary step toward linking stock toolchain output, not a sufficient one. Such an artifact also declares a multi-page linear memory. The merge widens the main module's minimum to cover it but never relaxes the main module's declared maximum, so a closure that addresses memory, merged into an Inference main whose memory is the default — a fixed one-page (memory 1 1) — clears the tier gate and fails at memory reconciliation instead. The layout is configurable: a main whose [memory] maximum (max-pages, which defaults to pages) reaches the external's declared minimum reconciles; see Configuring the layout. A program whose own code touches no memory and that configures no layout takes its memory from the linked modules' declarations instead, the same whichever order its external fn lines are written in, and refuses a combination no single memory can honor; see The Shared Linear Memory.

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.
• A main module that imports its own memory ([memory] import = true) cannot link [wasm-dependencies] modules yet. The static merge models only a memory its modules define, not one a host supplies, so infc refuses a program that binds a linked module in that mode, before external resolution, and the merge itself refuses a main module with a non-function import should one reach it. Linking with an imported memory is tracked under issue #546.
• 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.
• A mut scalar parameter's argument is not checked by analysis rule A047: a scalar carries no region for the rule to root a binding in, so a call passing a plain i32 has nothing at the call site to reject. This is an accepted, documented gap, not an absence of risk — the shadow stack occupies [0, stack_size) of the same linear memory a scalar i32 addresses, and under the default layout (one page, entirely stack) a caller's own frame sits just below address 65536, so store_at(65528, 7) overwrites that caller's own locals through a plain i32.store, admitted by the linker because Tier-B admission proves only that the address derives from a parameter, not where it lands — see The WASM Linker for what that proof does and does not bound. Closing it is tracked in issue #420.

A program that binds host imports (see Host Imports) meets restrictions of its own:

• It cannot bind linked modules as well (MixedHostAndLinked); see What is refused, and by which layer.
• It has no proof artifact: infc refuses every build of it that writes a .v; see What is refused, and by which layer.
• mut on a host parameter is not checked against what the embedder's function writes (the build holds no body to derive a write set from), though declarations of one pair must still agree and A047 still holds the call site to it; see mut on a host parameter.
• It cannot build at stellar, which refuses host imports; see What is refused, and by which layer.
• In a build that imports its memory ([memory] import = true), no host import can be named env.memory, the name the memory is imported under: an embedder that resolves each import by its module and field name alone cannot supply a function and a memory under one name, so infc refuses the build; see What is refused, and by which layer.
• An import module or field name has to be an Inference identifier, and nothing maps a declaration onto any other import string: wasi_snapshot_preview1 can be bound, while field names such as Soroban's _ and 0 cannot be spelled.
• No contract travels with a host import: nothing in the build describes what the function does, and its declaration holds an embedder to nothing.
• infs run executes it only as a spacewasm build whose imports are all F´ reference hosts at their reference signatures, and refuses every other artifact that still imports a function once the build has finished, including a project's [build.wasm-opt] step; see Running a program that binds host imports. A [build.wasm-opt] step that runs at any level but "0" leaves out a host import the program never calls, so an optimized program whose host imports are all uncalled runs; see A bound host import is emitted whether or not it is called.

Example: Two Libraries, One Module

external fn sort(mut 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]
• Compilation Targets: SpaceWasm host imports — the registration caps infc asks of a host import's declaration at --target spacewasm, and the conformance check that asks them again of the bytes
• Compilation Targets: Running a SpaceWasm build — infs run executing a spacewasm build under the SpaceWasm interpreter, with the F´ reference hosts and nothing else
• Compilation Targets: the embedder harness — running a host-import program under the SpaceWasm interpreter with --host stubs that log each call
• 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.

Two kinds of import do survive, and they get there by skipping the link rather than by passing through it. A use { f } from host::<module>; clause binds a host import: a function the embedder supplies at instantiation, with no .wasm in the build for the merge to fold in (see Host Imports). A build whose memory layout asks to import its memory ([memory] import = true) leaves the other: the module's linear memory, imported as env.memory for the embedder to supply (see Importing the memory). For a program that links no module and either binds only host imports or imports its memory, inference::link_resolved never calls the merge. It ships the code-generation bytes verbatim, after proving that the artifact's imports are exactly the declared host functions and, when the layout asks to import its memory, that env.memory import, by name and limits — see The Host-Only Pass-Through. The merge itself is unchanged, and every module it produces still has no import section. A program that binds host imports and linked modules together is refused at external resolution, before any .wasm is searched for; a merge that lets a host import survive beside the modules it links is not built. A host import is also exactly the dangling import this section calls unverifiable, which is why a program that binds one is refused any build that writes a .v. A program that imports its memory is refused every such build for the same reason, and is refused beside a linked module too, by infc before external resolution, because the merge models only a memory its modules define, not one a host supplies (tracked under issue #546). inference::link_resolved refuses the combination itself as well (ModulesWithImportedMemory), whatever the artifact imports, so a library caller that hands it resolved modules and an expected memory import cannot link a module that would leave the host's memory unread.

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)],
    None,
)?;
}

The third argument, contracts: Option<&[ImportWriteSet]>, is the mode that decides whether The Declared Write-Set Check runs at all: None skips it (the mode for hand-written .wasm fixtures with no Inference declaration behind them, such as the linker's own tests), while Some(list) — the mode infc/infs uses — holds every satisfied import to a declared write set built from the program's external fn declarations.

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 Shared Linear Memory

The output has one linear memory, shared by the main module and every merged external whose closure touches memory, with a load, a store, memory.size or memory.grow; an external whose closure touches no memory contributes nothing, whatever its module declares. The merge records each satisfied import's memory and computes the output memory once, from all of them together. Fixing it import by import would make it depend on the order the main module lists its imports in, which is the order the program wrote its external fn declarations in — and swapping two declaration lines would then change the emitted memory, what memory.grow returns, and the machine the .v describes.

If your program has its own memory, its maximum governs every linked module, and the linker warns about each growing module whose own maximum it replaces. Otherwise the linked memory is the tightest fit to the modules' own declarations, which relaxes no module's bound, and a link that no memory fits, or that would move where any module's memory.grow stops, is refused.

• A main module with a memory keeps its maximum, whatever the externals' own caps, and widens its minimum to the largest any module declares. An external minimum above main's maximum is refused. A module that grows memory under a different maximum of its own is linked all the same, and the link raises one LinkWarning::MemoryMaximumOverridden naming each such import as module::field and saying whether the program's maximum raised or lowered the module's, so you can see where memory.grow there now stops. A program built with infc --max-memory-pages 10 that links b::growB, whose module declares (memory 1 2), prints:

  warning: the program's linear memory has a maximum of 10 pages, which governs
           `memory.grow` in every linked module and replaces the maximum a
           growing module declares where the two differ: raised for the module
           providing `b::growB`, which declares a maximum of 2 pages, so
           `memory.grow` there now stops at 10 pages instead of 2. Under a
           raised maximum, `memory.grow` can succeed where the module alone
           would return -1. The program decides the maximum by design, which is
           what lets libraries whose maximums differ link together. This is not
           a fault found in the program or the library; the program's maximum is
           set by `max-pages` in the `[memory]` table of `Inference.toml`, or by
           `infc --max-memory-pages <N>`.
  

  The warning is silent when the program's maximum equals the module's, and for a module that never grows memory, since only memory.grow observes the maximum. A module that declares no maximum is named under any growable program, because its memory.grow is now bounded.

• A memoryless main gets the largest declared minimum and the smallest declared maximum, unbounded only when no external declares one — the memory WebAssembly import matching would accept for every external's declaration. One external's memory is therefore adopted exactly as declared. With several, two outcomes are refused rather than settled by picking one module's bound over another's: declarations no memory satisfies, such as one module needing five pages beside one allowing at most two, and a module that grows memory under a cap other than the shared one. A module whose cap is lowered but that never grows memory is accepted: only memory.grow observes the maximum, and a memoryless main exports no memory for a host to grow.

Either way, an external whose closure grows memory is refused when the resulting memory is pinned (max == min), since every memory.grow would fail. That includes a lone external adopted exactly as declared: one declaring five pages that may grow to five, whose closure grows memory, is refused onto a memoryless main rather than linked with a memory it can never grow.

Each refusal above names the remedy on the main module's side: pages (or infc --memory-pages) for a minimum larger than main's memory can hold, and max-pages (or infc --max-memory-pages) for the others. A [memory] table makes the program declare a memory of its own even when its code touches none, and that memory's maximum then decides. One page that may grow to one page is the default layout, so max-pages = 1 alone does not. Contributions are counted per satisfied import rather than per call, so an external fn the program declares but never calls still brings its module's memory.

The Main Module's Data Segments

Module-scope compound constants (arrays and structs) live in linear memory above the shadow stack, at [stack_size, stack_size + data_bytes), and the main module initializes that region with one active data segment at an i32.const offset. The merge carries the main module's segments into the output unchanged — same order, same offsets, same bytes — in a Data section written right after the Code section. A module with no segments gets no Data section, so a data-free program links to exactly the bytes it did before segments were carried.

Three facts make "unchanged" correct rather than merely convenient. No data index moves: only memory.init and data.drop name a segment, Inference codegen emits neither, the linker refuses either in a main body, and an external closure using either is Tier C, so no external segment ever joins the index space. No offset moves: the main module's memory stays memory 0 of the output. And the segment still fits: memory reconciliation only widens the minimum from the main module's and keeps its maximum. The output never carries a DataCount section, which SpaceWasm cannot decode; the validator requires one only of code that names a segment, which the first fact rules out.

Any other main-side segment is refused with LinkError::UnsupportedConstruct naming the segment and its problem: a passive segment, a segment over a memory other than 0, or an offset expression other than a lone i32.const. These are shapes Inference codegen does not emit; the refusals guard the public library API. An external's data segments are a different matter and stay Tier C (see What Each Tier May Touch).

Nothing in the program writes the constant region, and a linked external cannot be handed it to write through a declared path: analysis rule A047 refuses a compound argument at a mut external fn parameter unless it is rooted at a mut binding, which a const is not, and the repair it suggests copies the constant into a mut binding on the stack; a closure that stores through a parameter not declared mut fails the declared write-set check. That covers the declared path and nothing more. Tier B proves derivation, not containment, so an address the program passes as a scalar i32, or a displacement past a granted buffer, can reach a constant exactly as it can reach a caller's frame — the gap issue #420 tracks.

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(mut ptr: i32, val: i32);
external fn load_at(ptr: i32) -> i32;
use { store_at, load_at } from memlib;

external fn sort_pair(mut 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:

The segment-indexed table forms (table.init, elem.drop, table.copy) never reach classification: the operator allow-list rejects them as LinkError::UnsupportedConstruct.

Reading or writing a module global is not a Tier-C signal: the closure's globals are merged into the output alongside the main module's, with every global.get / global.set remapped onto the merged index space. A global used to address memory is still rejected, because the address it produces is not parameter-derived. Writing one is no such hazard: a global.set between computing an address and using it leaves that address's provenance intact.

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

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

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

Dropping an admitted external's globals and tables is sound because ClosureEffects is closure-scoped: a closure admitted with no global or table effect contains no operator naming either index space. Neither half would fail silently if that were ever violated. An external whose globals were dropped has an empty global remap, so a leaked global.get finds no mapping and the link fails with LinkError::UnsupportedConstruct, rather than rebinding onto main's first global and, the types agreeing, passing post-merge validation with a wrong value. A leaked table operator names a table the output does not have, since no table section is emitted, and validation rejects it as unknown.

Clearing the tier gate is not the same as linking, and reconciling the memory is one gate among several. A stock artifact also declares a multi-page memory, which the merge adopts only for a closure that addresses memory: it widens the main module's minimum to cover it but keeps the main module's maximum. A closure that addresses memory, merged into a main whose memory is the default, a fixed one-page (memory 1 1), therefore clears the tier gate and fails at memory reconciliation with LinkError::IncompatibleMemory; a main whose [memory] maximum reaches the artifact's minimum reconciles.

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 output's single linear memory — the main module's own, or, for a main that declares none, one built from the linked modules' declarations (see The Shared Linear Memory). 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 both uses memory.init and performs an indirect call 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 ✗

The Declared Write-Set Check

Tier-B admission proves that every memory address a closure computes derives from a caller-supplied parameter. It does not say which parameter licenses a given store, and it does not have to — until the closure is also held to a declared write set.

mut on an external fn parameter is the Inference-side declaration of that licence: it states that the foreign body may store through the address that parameter denotes. The linker checks the claim, keyed on (module, field) — the same pair an import is satisfied on — against the merged bytes, in one of two ways depending on what the declaration says:

• No parameter marked mut (an empty declared set) is checked structurally: the merged closure must record no Store access anywhere, not merely an attributed write set that happens to come out empty. A caller relying on "this closure writes nothing, anywhere" then inherits none of the attribution pass's own assumptions.
• Some parameter marked mut is checked against a second, forward least-fixpoint attribution pass — distinct from the greatest-fixpoint trusted[g] computation above — that computes, for every function g in the closure, the set of the root export's parameters each of g's own parameters may derive from, seeded at the root and propagated through every call site's argument dependencies. Every Store access's address is then attributed to the union of root parameters its dependencies may derive from. The attributed set must be a subset of the declared one, or the link fails with LinkError::UndeclaredExternWrite, naming the offending parameter by index and, where the declaration gave it a name, by name.

An import the checked mode's declaration list does not mention is treated as declaring no mut parameter, never skipped — see Where the Linker Fits in the Pipeline for the two contracts modes that decide whether the check runs at all, and for which callers use each one.

This check licenses derivation-to-a-parameter, not containment within it — the same limit Tier-B Provenance Analysis describes. W ⊆ D bounds which parameter a store's address derives from; it says nothing about which bytes the store touches, or whether they stay inside the region the caller meant that parameter to grant. A declaration external fn writer(mut a: [i32; 2], b: [i32; 2]); whose body stores at a + 8 — past a's own two elements — links cleanly, because the address still derives from parameter 0. Closing that gap needs the numeric/interval domain issue #420 tracks; the write-set check narrows which parameter a store may be attributed to, not where within it the store lands.

That narrower guarantee is nonetheless enough to license one thing safely: core/wasm-codegen's by-reference optimization elides a compound parameter's entry copy only when every external it reaches declares no mut parameter at all. An empty declared set forces the structural "no Store access anywhere" fact above, and a closure that never stores cannot disturb a caller's elided copy — no containment property is needed for that narrower claim. A mixed declaration (writer(mut a, b)) still costs every parameter it reaches a copy, including b's: per-position elision is deliberately not implemented, because it would need the containment property this check does not have. See core/wasm-codegen/docs/arrays-and-memory.md for the codegen side of this decision.

The attributed set can also be broader than "this parameter is itself a written-through address" suggests, for a reason distinct from the containment gap above: the attribution is affine, and it counts every parameter that may contribute to a store's address, not only the one playing the role of base pointer. The ordinary scaled-index write mem[ptr + (idx << 2)] = val attributes to both ptr and idx — idx never denotes an address on its own, but it scales one, and the affine form the attribution tracks does not distinguish that role from a base pointer's. A declaration external fn set_elem(ptr: i32, idx: i32, val: i32); bound to a body that writes this way must therefore mark idx, not only ptr, mut — set_elem(mut ptr: i32, mut idx: i32, val: i32); — or the link fails naming parameter 1, even though nothing about idx's own value is a location the body writes to. This runs in the same conservative direction as the containment gap: attributing too broadly can force a wider declaration than the informal reading of mut suggests, never let an actual write through undeclared.

The read/write split above is what keeps this from over-reaching further. memory.copy(dest, src, size)'s src operand is recorded as a Load, never a Store, so it never contributes to any Store access's dependency and is never pulled into the attributed write set — even though the same instruction also writes dest. A pure source pointer stays correctly unforced; it is specifically a store's own address computation whose affine contributors all get pulled in, idx-style scaling parameters included.

Proof-Only Stripping

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

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

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

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

Floating-Point Exclusion

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

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

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

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

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

Name Preservation

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

• Main module local functions keep their source debug names, re-indexed onto the import-free output space.
• Every merged external function is named under its source's logical module, joined with :::
  • A closure root satisfying import sum bound under logical module mathlib becomes mathlib::sum.
  • An internal callee the source module named keeps that name behind an internal mark: 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 section is one namespace with two halves, and :: is the boundary. A compiled function's name-section symbol is built from Inference identifiers joined by ., so it can never carry a :: a source module named mathlib and a linked logical module named mathlib are free to coexist. Within the merged half, the module prefix keeps two libraries that export the same field apart, and the internal mark keeps a module's private callees from shadowing its own roots — an inner debug name comes from the foreign module and is unconstrained, so it may be exactly an export field.

A WASM name map holds one name per function index. When one foreign body satisfies two imports (an export bound under two fields), the least of its root names is recorded and an obligation over the other is rewritten onto it, so both declarations still describe the body they name.

The Rocq translator (core/wasm-to-v/src/rocq_names.rs) maps every byte outside [A-Za-z0-9_] to _ and collapses the runs, so mathlib::sum becomes Definition mathlib_sum in the .v file — the same identifier the dotted form produced. A residual collision after sanitization (two modules that sanitize to one identifier) is still disambiguated by the translator's index suffix; the scheme removes the common cases rather than every possible one.

The Host-Only Pass-Through

A program whose externs are all host imports has nothing to merge: there is no .wasm to fold in, and its imports are meant to survive for an embedder to satisfy. So does a program that links no module and imports its memory: the memory is meant to survive for the embedder to supply. inference::link_resolved — the one place the choice between the two paths is made, and the path infc ships through — therefore returns the code-generation bytes unchanged whenever no module was resolved and there is something to keep, a host import, an imported memory or both. The memory is not part of resolution's answer: it is the memory: Option<MemoryImport> argument, which infc fills from the build's layout and which is None for a build that defines its memory. The language surface that produces a host import is described under Host Imports.

What stands in for the merge's guarantee is one check: the artifact's import section must equal the declared host set, compared on module, field, parameters and results, in both directions, and must carry the memory import the layout asked for and no other. An import no declaration covers (Undeclared), a declaration no import covers (Missing), a signature that differs (SignatureMismatch), and one two-level name imported twice (Duplicated) are each refused, as is any import of a table, a global or a tag, or of a memory when the layout asked for none (NonFunctionImport). When the layout does ask for one, the memory import is accepted once, and only if it is named env.memory and has the type the layout declares: 32-bit, unshared, at the default page size, with pages as its minimum and max-pages as its maximum, which is always present. A memory under another name or at another type — other limits, no maximum, shared, 64-bit or a custom page size — is a MemoryImportMismatch, whether it stands in place of the expected import or beside it; a second memory under the memory's name, or a function imported under that name beside the memory, is Duplicated; and an artifact that imports no memory when the layout asked for one is a MissingMemoryImport. Bytes that do not decode are a refusal too, never an empty import list: an empty list compares equal to an empty declared set, so bytes that do not parse would otherwise pass as a module that imports nothing. The declared set comes from the external-module driver's walk over the type checker's extern provenance, and the import section from code generation's own walk over the same declarations. A disagreement between the two is the compiler contradicting itself rather than anything an author wrote, so each of these refusals (inference::wasm_link::HostImportError, reported by infc as Link step failed: …) ends by asking for a compiler-bug report. The memory import is held to the layout instead, the value code generation wrote it from, and a disagreement there is the same contradiction.

The memory is held to the layout, and not merely to being a memory, because the program was laid out in it: the stack and the static data sit within the minimum, and the headroom the stack-overflow trap relies on is measured against the maximum (see Configuring the layout). An import that drifted from the layout would hand the embedder a contract the program was not laid out for.

What is not checked is everything the merge's main-side gate exists for. That gate lets the merge assume a module it can rewrite — index spaces it can renumber, sections it can concatenate — and no rewrite happens here. So the pass-through accepts what the linker would refuse in a main module: a data segment of a shape the merge does not carry (passive, over another memory, or at a computed offset), an element segment, a start function, a table, a memory of the module's own (a second one, or one beside the imported memory), a float or v128 in one of the module's own signatures, and a duplicated or malformed inference.spec_funcs or inference.hspecs custom section. No body is re-encoded through the operator allow-list, no tier is classified, and no write set is derived, since there is no foreign body to derive one from; that is why mut on a host parameter is an assertion rather than a checked contract (see mut on a host parameter). The shapes that pass are ones this compiler's code generation does not emit; what cannot be taken on trust about bytes nobody rewrote is that their surviving imports are the ones the build asked for, the author's host bindings and the memory its configuration imports, and that is what the check establishes.

Nor does validate_extern run: there is no library to hold a declared signature against, and the consistency check among the declarations at resolution stands in for it (see Declaring an External Function).

Error Reference