Problem

Vera's higher-order array combinators — array_map, array_filter, array_fold, and the helpers array_map_go, array_filter_go, array_fold_go — are currently implemented in vera/prelude.py as recursive Vera functions that get inlined into every program that uses them. Each element processed = one recursive call = one stack frame on the GC shadow stack.

This directly caused #464 (the GC shadow stack overflow). The fix in #464 / #472 raised the shadow stack from 4K to 16K and added a bounds-checking trap, which lets ~1,365 recursive frames fit. But recursion-per-element is the wrong complexity class: the stack grows linearly with the input size, not with the logical nesting depth of the program. A 10,000-element array mapped twice (nested calls) will still blow the stack even at 16K.

When the new combinators proposed in #466 land — especially array_mapi, array_reverse, array_sort, array_index_of, array_find — adding them to prelude.py as recursive Vera would re-expose the same concern. The #464 fix is a defense-in-depth trap, not a cure.

Approach

Reimplement these combinators so each operation is O(1) shadow stack space regardless of input size:

1. Direct WASM iterative loops — like string_concat, string_slice, array_append already are. The WASM translator in vera/wasm/calls_strings.py, calls_arrays.py etc. emits a loop / br_if loop with a single local index.
2. Host imports for complex ops — array_sort in particular should be a host import (Python sorted() uses Timsort, battle-tested, O(n log n) — implementing sort in Vera is 50+ error-prone lines).

The iterative-WASM approach keeps the work inside the Vera module (no host round-trip for simple maps), gets O(1) shadow stack usage, and handles arbitrary input sizes. The host-import approach is right for cases where the algorithm is non-trivial (sorting) or where the host language has a better implementation.

Scope

• Existing combinators to migrate (from vera/prelude.py):
  • array_map / array_map_go
  • array_filter / array_filter_go
  • array_fold / array_fold_go
• New combinators from #466 — implement iteratively from the start:
  • array_mapi, array_reverse, array_sort, array_sort_by, array_flatten
  • array_contains, array_index_of, array_find, array_any, array_all

Implementation sketch

Each iterative combinator follows the same template in vera/wasm/calls_arrays.py (already exists as a mixin for the arrays domain). For array_map<A, B>(arr, fn):

(local $idx i32)
(local $len i32)
(local $dst i32)
...
;; Evaluate arr → (ptr, len) on stack; save.
;; Allocate dst: len * sizeof(B) bytes.
;; Loop: for idx in [0, len):
;;   load arr[idx] into locals matching B's WASM shape
;;   call the closure via call_indirect
;;   store result at dst[idx]
;; Push (dst, len) as the result.

The closure dispatch reuses the existing call_indirect infrastructure from vera/wasm/closures.py.

Why this matters

• Correctness: closes a class of bugs similar to #464. A well-typed, contract-verified Vera program should not have stack-size failure modes that depend on input size.
• Benchmark story: VeraBench tasks that map or filter large arrays would currently hit the 16K ceiling at deep-enough nesting. Moving to iterative ops lifts that ceiling to "memory" rather than "stack depth".
• Prerequisite for #466: the new combinators should land iteratively from day one, not as recursive prelude functions that need migrating later.

Priority

Do this before or as part of #466. Retrofitting the existing three (array_map / array_filter / array_fold) is a bonus that can land in the same PR or separately.

Testing

• Existing tests/test_codegen.py coverage for array_map / array_filter / array_fold continues to pass (pure behavioural test).
• Add a stress test: iterate over 10,000 elements without blowing the stack (would fail under the current recursive implementation).
• Conformance tests using higher-order array ops still pass at their declared level.

Related

• #464 — the original GC shadow stack overflow this prevents recurring.
• #472 — the defensive fix that raised the shadow stack ceiling.
• #466 — adds new array combinators that depend on this structural choice.