MIR validation is layered because a legal early operation can be an illegal backend operation. “Well formed” therefore always means well formed for a named pipeline checkpoint.
Per-function verifier
The general verifier walks reachable blocks and checks:
- every used local exists and has an allowed definition;
- block targets exist and edge arguments match target parameters;
- whole and continuation forms agree with their required fields;
- local storage and inline aggregate regions are consistent;
- frame slots are aligned, in bounds, and mapped consistently;
- selected ABI facts agree with function role and shape;
- a tail call is the supported static self-call form;
- ownership operations are balanced on relevant paths;
- linear locals are neither cloned nor dropped;
- an uninitialized value is not dropped;
- no suspension appears inside an indivisible RC sequence.
The verifier reports all discovered issues as invariant-numbered records. In debug builds the pass manager runs it after transformations so the failure is attributed to the pass that broke the graph rather than to a later WebAssembly trap.
Optional strict checks
Some analyses need stronger conditions than the base representation promises:
- strict SSA discipline;
- no confined value escaping its allowed region;
- no live ownership balance leaking from function exits;
- raw-pointer barrier and escape discipline;
- selected collection-element and closure-completeness rules.
These checks are invoked at their owning checkpoints or by tests. Their existence is why generic code must not treat the phrase “SSA-style locals” as a global proof of strict SSA.
Cross-function checks
Some correctness properties cannot be decided one function at a time.
Recursion validation classifies call cycles and frame requirements. Recursion itself is legal; a recursive edge that would require infinite fixed child storage must use an indirection or flex-allocated child frame.
Ownership and borrowing can also depend on callee summaries or SCCs. Unit-wide checks validate caller/callee ownership agreement, exit balance, closure capture completeness, and generated walker compatibility.
Canonicalization boundary
Before WasmIR lowering, backend-boundary validators require all policy-bearing MIR forms to be selected or expanded. Rejected leaks include, depending on context:
- unexpanded aggregate and select carriers;
- unselected closure allocation or calls;
- frame-call policy that should already be primitive mechanics;
- high-level spawn or suspension constructs;
- stale function ABI layouts after a transforming pass;
- unsupported static calls or intrinsics;
- closure environment layouts inconsistent with their captures.
This boundary is intentionally strict. If WasmIR lowering had to ask whether a closure call is direct, how a helper returns, or where a result payload lives, MIR canonicalization failed to do its job.
Facts and invalidation
Passes can publish facts such as liveness, layout readiness, or validated well-formedness. A fact is evidence produced by a specific analysis, not a boolean field that remains true forever.
A transformation declares which facts it:
- requires before running;
- preserves without recomputation;
- invalidates because it changed relevant state;
- produces after successful analysis or validation.
Changing block edges invalidates dominance and liveness. Changing locals or storage can invalidate frame and ABI layouts. Changing call targets can invalidate effect, recursion, borrowing, and dispatch-related summaries. The pass manager must recompute or reject a missing fact; it must not assume the old proof still applies.
Failure behavior
Validation distinguishes source diagnostics from compiler invariants:
- a user program violating a representable backend restriction should receive a source-attributed diagnostic and no artifact;
- malformed MIR produced from an otherwise accepted program is a compiler defect;
- neither case may be repaired by silently deleting an operation, selecting a placeholder ABI, or emitting zero.
At the final gate, general well-formedness, project-aware ABI checks, raw pointer discipline, generated walker validation, and WebAssembly module validation combine to define a successful backend artifact.