Memory Allocation in WASM Codegen

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

The Problem

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

Three allocation strategies are available:

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

Inference uses option 3. Arrays have stack-scoped lifetimes (they are created when a function is entered and destroyed when it returns), so they fit naturally into a stack discipline. No runtime, no allocator, no GC.

Linear Memory Layout

WebAssembly linear memory is a contiguous byte array. Inference allocates one page (64 KB) and uses it entirely as a stack:

Linear Memory (1 page = 64KB)
+--------------------------------------------+  0x10000 (65536)
|                                            |
|     (free space)                           |
|     (future: data sections, heap)          |
|                                            |
+-- __stack_pointer -------------------------+  STACK_SIZE (65536)
|                                            |
|         Stack (grows downward)             |
|                                            |
+--------------------------------------------+  0x00000
  overflow below 0 = WASM OOB trap

__stack_pointer is a mutable i32 WebAssembly global initialized to 65536 — the top of the stack region. When a function 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. Future data sections and heap allocations will be placed above the stack region, starting at STACK_SIZE and growing upward.

Programs without arrays do not get a memory section, a global section, or any memory-related exports. The compiler tracks a has_memory flag and only emits these sections when at least one function uses arrays. Existing programs produce identical WASM output — zero regression.

Stack Frame Layout

Each function 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

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. 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. Those stores live in a .wasm the compiler never type-checked, so it cannot see them. Any parameter that flows to an external argument therefore keeps its copy, and the foreign writes land in the callee's frame rather than in the caller's memory.

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 this: the body, not the declaration. The mut marker 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. Whether a copy is emitted is a separate, internal question about what the body actually does, so a mut parameter that is never assigned 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. 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.

The external case deserves its own note, because it is the one place where a write is invisible in Inference source. Linking merges every module into one linear memory, and a compound external fn parameter is lowered to a raw i32 pointer with no copy between the call site and the foreign body. The external is free to store through that pointer. A method or function that hands a parameter — or any projection of one, such as self.field or arr[i] — to an external therefore keeps its copy, so the foreign stores land on the callee's own bytes. This is conservative in the harmless direction: an external that only reads still costs its callers a copy, because the declaration does not yet say which of its parameters it writes. Making that claim explicit and checking it against the merged body is future work; until then, a parameter forwarded to an external is never passed by reference. The linker's side of this arrangement 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; Inference does not currently emit bounds checks (this is deferred to a future BuildProfile feature).

WASM Section Layout

When has_memory is true, the compiler emits three additional sections in the WASM module:

These sections are ordered according to the WASM specification: Type, Function, Memory, Global, Export, Code, Name. The ordering is mandatory — a misordered module fails validation.

When no function uses arrays, these sections are omitted entirely. The output is byte-identical to what the compiler produced before array support was added.

Formal Verification Implications

Modeling Arrays in Rocq

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

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 Future Proof Obligation

Array index access is bounds-checked: a constant out-of-bounds index is rejected at compile time (analysis rule A037), and a dynamic index emits a runtime guard (index >= length -> unreachable) in all Compile-mode builds.

The remaining verification step is Proof mode. Emitting the guard in proof mode and extending the Rocq ValidModule/ValidSpec contract with a "no reachable trap" clause would turn the bound into a proof obligation — the programmer proves 0 <= i < array_length to discharge it, and a proven module can then elide the runtime guard so the verified artifact is the deployed artifact. This is tracked as future work (issue #214).

Current Implementation

The memory infrastructure is in core/wasm-codegen/src/memory.rs (constants, data structures, store/load helpers, prologue/epilogue emission, parameter copy). Frame layout computation and array lowering methods are in core/wasm-codegen/src/compiler.rs, 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: