Vera version: vera 0.0.138 (current main, commit ec46cf8)
Symptom class: WASM compile-time trap — vera check is silent, vera run traps at module load.
Found by: Agent attempting to write terminal Tetris on Vera 0.0.138.

Minimum reproducer

private data K { A, B }
private data S { Mk(Array<Int>, K) }

private fn s_arr(@S -> @Array<Int>) requires(true) ensures(true) effects(pure)
{ match @S.0 { Mk(@Array<Int>, @K) -> @Array<Int>.0 } }

public fn main(@Unit -> @Int) requires(true) ensures(true) effects(pure)
{
  let @S = Mk([10, 20, 30], A);
  let @Array<Int> = array_map(array_range(0, 3), fn(@Int -> @Int) effects(pure) {
    s_arr(@S.0)[@Int.0]
  });
  @Array<Int>.0[1]
}

Observed

$ vera check t.vera
OK: t.vera
$ vera run t.vera
Error: Unhandled WASM trap: failed to compile: wasm[0]::function[3]::main

Caused by:
    0: WebAssembly translation error
    1: Invalid input WebAssembly code at offset 1374: unknown table 0: table index out of bounds

Confirmed reproducing on current main (commit ec46cf8).

Expected

20 printed (the result of arr[1] where arr = [10, 20, 30]).

What triggers it

The closure captures an outer data ADT (@S) and passes it as an argument to a function call (s_arr(@S.0)) inside the closure body. Variations:

• Single-variant ADT also reproduces — data S { Mk(...) } traps the same way.
• Capture without function call is fine — a closure that just match-es the captured ADT directly, or returns it unchanged, does not trap.
• Pre-extracting the inner field outside the closure works (workaround below).
• The triggering boundary appears to be "function call with the captured ADT as an argument" specifically; needs narrowing to confirm whether any cross-function-boundary use of the captured ADT triggers it, or just direct argument passing.

Workaround

Pre-extract the inner field outside the closure so the closure captures the extracted value, not the ADT itself:

let @S = Mk([10, 20, 30], A);
let @Array<Int> = match @S.0 { Mk(@Array<Int>, @K) -> @Array<Int>.0 };  -- pre-extract
let @Array<Int> = array_map(array_range(0, 3), fn(@Int -> @Int) effects(pure) {
  @Array<Int>.0[@Int.0]   -- capture the Array, not the S
});

Returns 20 correctly.

Hypothesis

Likely a closure-lifting / slot-relocation pass bug — the env-struct serialisation appears to not handle captured-ADT-passed-as-argument correctly. Possibly related to the walker-completeness audit (#597) — _walk_free_vars (#588) was missing eight AST node-type branches, and a similar walker-incompleteness in the closure-lifter could explain why cross-function-boundary uses miscompile.

The trap message unknown table 0: table index out of bounds consistently points at the closure that captures the ADT — adding a Vera-level frame to the trap (file/line of the closure literal) would make this orders of magnitude easier to localise.

Diagnostic suggestion

If the closure-lifting pass computes the env-struct layout, assert that every captured slot is correctly serialised before call_indirect emission, and emit a clear compile-time error when the lifter can't represent the capture rather than letting WASM validation catch a malformed table.

Origin

Discovered while writing terminal Tetris in Vera; hit consistently on collision-check shapes that pass the captured State ADT into helper functions inside array_all closures. The hypothesised umbrella with Bug B (#615) is sketched in the source friction document.