Bug

$alloc in vera/codegen/assembly.py grows memory by exactly 1 WASM page (64 KB) when the requested total exceeds current memory size, without checking whether 1 page is enough. If the requested allocation is more than ~64 KB larger than current free heap space, the fall-through bump-allocate writes past memory.size, triggering a WASM out of bounds memory access trap.

Reproducer

After #484 lands (raising the 16-bit size-field ceiling), this reproduces with any ≥50 K-element Int array operation:

source = '''
public fn main(-> @Int)
  requires(true) ensures(true) effects(pure)
{
  let @Array<Int> = array_range(0, 50000);
  let @Array<Int> = array_map(@Array<Int>.0, fn(@Int -> @Int) effects(pure) { @Int.0 + 1 });
  @Array<Int>.0[49999]
}
'''
assert _run(source, fn='main') == 50000   # traps: memory fault at wasm address 0x20000

Each array is 400 KB; two of them need ~800 KB total. Initial memory is 2 pages (128 KB). First allocation forces grow to 3 pages; second allocation asks for 400 KB but only +1 page (256 KB total) gets grown, leaving us 144 KB short. The code then bump-allocates anyway and WASM traps.

Location

vera/codegen/assembly.py around lines 454-470 (in $alloc):

    ;; Still OOM — grow memory
    global.get $heap_ptr
    local.get $total
    i32.add
    memory.size
    i32.const 16
    i32.shl
    i32.gt_u
    if
      i32.const 1          ;; <-- only grows by 1 page, regardless of how many needed
      memory.grow
      i32.const -1
      i32.eq
      if
        unreachable
      end
    end

Fix

Compute the number of pages needed and grow by that many. Sketch:

    ;; pages_needed = ceil((heap_ptr + total - memory.size*65536) / 65536)
    global.get $heap_ptr
    local.get $total
    i32.add
    memory.size
    i32.const 16
    i32.shl
    i32.sub                ;; shortage in bytes
    i32.const 65535
    i32.add                ;; + (page-1) for ceiling
    i32.const 16
    i32.shr_u              ;; / page_size
    memory.grow
    i32.const -1
    i32.eq
    if
      unreachable
    end

Alternative: keep the 1-page grow but wrap it in a loop that re-checks. The compute-pages variant is simpler and avoids repeated GC cycles.

Impact

• Blocks large single allocations (≥ ~64 KB more than current free space).
• Stays latent until GC object header size field is 16-bit — allocations >65535 bytes corrupt memory #484 lands because today's 16-bit size cap (GC object header size field is 16-bit — allocations >65535 bytes corrupt memory #484) blocks those allocations upstream with a different, wronger symptom.
• Pure codegen fix in one place; no user-facing API change.