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: