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