Emit iterative WASM for array_map (#480 PR 1)

CHANGELOG.md

@@ -6,6 +6,9 @@ The format is based on [Keep a Changelog](https://keepachangelog.com/en/1.1.0/).
 
 ## [Unreleased]
 
+### Changed
+- **Iterative WASM `array_map`** ([#480](https://github.com/aallan/vera/issues/480) PR 1) — `array_map<A, B>(arr, fn)` is now emitted as a single WAT `loop` driven by a `call_indirect` on the closure, replacing the recursive prelude implementation (`array_map_go`). Shadow-stack usage is now O(1) regardless of input length — the old recursive version hit the 16K shadow-stack ceiling (post-[#464](https://github.com/aallan/vera/issues/464)) around 4K elements. The generic higher-order signature (`forall<A, B>`) is preserved via a `FunctionInfo` built-in registration, so source code is unchanged. Also discovered and filed [#484](https://github.com/aallan/vera/issues/484) — a pre-existing 16-bit GC-header size-field limits allocations to 65535 bytes; the stress test caps at 8K Int elements (64,000 bytes) until that's fixed.
+
 ### Added
 - **CHANGELOG enforcement at pre-push and CI** ([#478](https://github.com/aallan/vera/issues/478)) — new `scripts/check_changelog_updated.py` fails a PR if any substantive file (`vera/`, `spec/`, `SKILL.md`) is changed without a matching new entry in `CHANGELOG.md`. Runs at the `pre-push` hook stage locally (opt in with `pre-commit install --hook-type pre-push`) and in the CI `lint` job. Escape hatches: a `Skip-changelog: <reason>` commit trailer (Git-native) or a `skip-changelog` PR label (CI-only). Prevents the kind of missed release-prep that happened on [#474](https://github.com/aallan/vera/pull/474).
 

KNOWN_ISSUES.md

@@ -10,6 +10,7 @@ Bugs and limitations tracked against the [issue tracker](https://github.com/aall
 | GC shadow stack pollution from opaque handle parameters | [#347](https://github.com/aallan/vera/issues/347) |
 | GC worklist overflow for deeply nested object graphs | [#348](https://github.com/aallan/vera/issues/348) |
 | WASM call translators: 10 pre-existing bugs (INT64_MIN to_string, string/array slice i64→i32 narrowing, char_code no bounds check, expression-bodied Exn handler result type, Map<K, Array<T>> lowering, url_parse/url_join round-trip, base64 `=` validation, parse_nat/int embedded spaces, float fractional carry) | [#475](https://github.com/aallan/vera/issues/475) |
+| GC object header size field is 16-bit — allocations >65535 bytes corrupt memory (sweeper truncates size, links middle-of-payload as fake free blocks) | [#484](https://github.com/aallan/vera/issues/484) |
 
 ## Limitations
 

ROADMAP.md

@@ -8,7 +8,7 @@ See [HISTORY.md](HISTORY.md) for a narrative account of how the compiler was bui
 
 ## Where we are
 
-The compiler is complete end-to-end: parse, type-check, verify contracts via Z3, compile to WebAssembly, and run — at the command line and in the browser. The language has 122 built-in functions, algebraic effects (IO, Http, State, Exceptions, Async, Inference), constrained generics, a module system, contract-driven testing, and a canonical formatter. Type inference for bare constructors (`None`, `Err`, `Ok`) now works correctly across all call sites. The compiler has 3,319 tests, 73 conformance programs, 30 examples, and a 13-chapter specification.
+The compiler is complete end-to-end: parse, type-check, verify contracts via Z3, compile to WebAssembly, and run — at the command line and in the browser. The language has 122 built-in functions, algebraic effects (IO, Http, State, Exceptions, Async, Inference), constrained generics, a module system, contract-driven testing, and a canonical formatter. Type inference for bare constructors (`None`, `Err`, `Ok`) now works correctly across all call sites. The compiler has 3,324 tests, 73 conformance programs, 30 examples, and a 13-chapter specification.
 
 Significant progress has been made towards Vera being a viable agent target. [VeraBench](https://github.com/aallan/vera-bench) — a 50-problem benchmark across 5 difficulty tiers — now covers 6 models across 3 providers (v0.0.7). The headline result: Kimi K2.5 achieves 100% run_correct on Vera, beating both Python (86%) and TypeScript (91%). Three models beat TypeScript on Vera. The flagship tier averages 93% Vera run_correct vs 93% Python — essentially parity. These are single-run results with high variance; stable rates will require pass@k evaluation. The remaining gaps are empirical breadth (repeated trials, more models), standard library depth (HTTP hardening, server effects), and tooling integration (LSP).
 
@@ -223,7 +223,7 @@ These are not milestone-gated — they should be addressed continuously alongsid
 | Item | Issue | Effort | Impact |
 |------|-------|--------|--------|
 | Add property-based testing with Hypothesis | [#386](https://github.com/aallan/vera/issues/386) | 2–4 hours | Catches parser/formatter edge cases via round-trip properties |
-| Add mutation testing with mutmut (detection only) | [#387](https://github.com/aallan/vera/issues/387) | 2–4 hours | Measures whether 3,319 tests catch real bugs, not just execute paths |
+| Add mutation testing with mutmut (detection only) | [#387](https://github.com/aallan/vera/issues/387) | 2–4 hours | Measures whether 3,324 tests catch real bugs, not just execute paths |
 | Investigate parser fuzzing with Atheris | [#402](https://github.com/aallan/vera/issues/402) | 4–8 hours | Crash-inducing inputs for parser and type checker |
 | Improve browser runtime test coverage to >80% | [#349](https://github.com/aallan/vera/issues/349) | 2–4 hours | Parity with Python-side coverage gate |
 | Add `check_changelog_updated.py` pre-push hook + CI check | [#478](https://github.com/aallan/vera/issues/478) | 30–60 min | Fails PRs that touch `vera/`/`spec/`/`SKILL.md` without a CHANGELOG entry; prevents the #474 miss from recurring |
@@ -268,4 +268,4 @@ The compiler was built through ten development phases from February to March 202
 | C8.5 | v0.0.66–v0.0.88 | **Completeness** — builtins, IO runtime, types, effects, browser target | Done |
 | C9 | v0.0.89–v0.0.101 | **Abilities, standard library, data types, effects** — Eq/Ord/Hash/Show, Map/Set, JSON, HTML, Markdown, Http, Decimal, Inference, standard prelude, combinators, higher-order array ops | Done |
 
-**810+ commits, 113 tagged releases, 3,319 tests, 96% coverage, 73 conformance programs, 30 examples, 13 spec chapters.** See [HISTORY.md](HISTORY.md) for the full narrative of how the compiler was built.
+**810+ commits, 113 tagged releases, 3,324 tests, 96% coverage, 73 conformance programs, 30 examples, 13 spec chapters.** See [HISTORY.md](HISTORY.md) for the full narrative of how the compiler was built.

TESTING.md

@@ -6,7 +6,7 @@ This is the single source of truth for Vera's testing infrastructure, coverage d
 
 | Metric | Value |
 |--------|-------|
-| **Tests** | 3,319 across 28 files (~34,000 lines of test code; 3,308 passed, 11 skipped) |
+| **Tests** | 3,324 across 28 files (~34,000 lines of test code; 3,313 passed, 11 skipped) |
 | **Compiler code coverage** | 96% of 15,149 statements (CI minimum: 80%) |
 | **Conformance programs** | 73 programs across 9 spec chapters, validating every language feature |
 | **Example programs** | 30, all validated through `vera check` + `vera verify` |
@@ -57,7 +57,7 @@ python scripts/fix_allowlists.py --fix               # auto-fix stale allowlists
 | `test_verifier.py` | 132 | 1,886 | Z3 verification, counterexamples, tier classification, call-site preconditions, branch-aware preconditions, pipe operator, cross-module contracts, match/ADT verification, decreases verification, mutual recursion, refined Bool/String/Float64 param sorts |
 | `test_codegen.py` | 862 | 10,563 | WASM compilation, arithmetic, Float64, Byte, arrays (incl. compound element types), ADTs, match (incl. nested patterns), generics, State\<T\>, Exn\<E\> handlers, control flow, strings, string escape sequences, IO (read\_line, read\_file, write\_file, args, exit, get\_env), bounds checking, quantifiers, assert/assume, refinement type aliases, pipe operator, string built-ins, built-in shadowing, parse\_nat Result, GC, Markdown host bindings, Regex host bindings, Map collection, Set collection, Decimal type, Json type, Html type, Http effect, Inference effect, example round-trips, GC shadow stack overflow |
 | `test_codegen_contracts.py` | 32 | 576 | Runtime pre/postconditions, contract fail messages, old/new state postconditions |
-| `test_codegen_monomorphize.py` | 52 | 897 | Generic instantiation, type inference, monomorphization edge cases, ability constraint satisfaction (Eq/Ord/Hash/Show), operation rewriting (eq/compare), show/hash dispatch, ADT auto-derivation, array operations (slice/map/filter/fold) |
+| `test_codegen_monomorphize.py` | 57 | 1,013 | Generic instantiation, type inference, monomorphization edge cases, ability constraint satisfaction (Eq/Ord/Hash/Show), operation rewriting (eq/compare), show/hash dispatch, ADT auto-derivation, array operations (slice/map/filter/fold) |
 | `test_codegen_closures.py` | 19 | 473 | Closure lifting, captured variables, higher-order functions |
 | `test_codegen_modules.py` | 19 | 565 | Cross-module guard rail, cross-module codegen, name collision detection (E608/E609/E610) |
 | `test_codegen_coverage.py` | 5 | 250 | Defensive error paths: E600, E601, E605, E606, unknown module calls  |
@@ -74,7 +74,7 @@ python scripts/fix_allowlists.py --fix               # auto-fix stale allowlists
 | `test_markdown.py` | 59 | 394 | Markdown parser: block/inline parsing, rendering, round-trips, edge cases |
 | `test_browser.py` | 61 | 749 | Browser parity: Python/wasmtime vs Node.js/JS-runtime output equivalence across IO, State, contracts, Markdown, Regex, and all compilable examples |
 | `test_conformance.py` | 365 | 102 | Parametrized conformance suite: parse, check, verify, run, format idempotency across 73 programs |
-| `test_prelude.py` | 24 | 406 | Prelude injection: Option/Result/array operation detection, combinator shadowing, type aliases, end-to-end compilation |
+| `test_prelude.py` | 24 | 419 | Prelude injection: Option/Result/array operation detection, combinator shadowing, type aliases, end-to-end compilation |
 | `test_readme.py` | 2 | 79 | README code sample parsing |
 | `test_html.py` | 4 | 164 | HTML landing page code samples: parse, check, verify |
 | `test_build_site.py` | 17 | 213 | `_abs_links` unit tests: relative link rewriting, fenced block immunity (backtick and tilde fences, inline backticks inside fences), http/https/fragment pass-through, Vera effect syntax not mis-parsed |

tests/test_codegen_monomorphize.py

@@ -895,3 +895,119 @@ def test_array_fold_type_check(self) -> None:
 }
 """
         _compile_ok(source)
+
+    # ----------------------------------------------------------------
+    # array_map — regression tests for the iterative implementation
+    # (#480).  These exercise paths the existing tests above don't:
+    # large inputs (stress the loop, not the recursion), closures
+    # that capture outer variables, A != B with pair output, and
+    # scalar Int → scalar Bool type change.
+    # ----------------------------------------------------------------
+
+    def test_array_map_large_input_no_stack_overflow(self) -> None:
+        """8,000-element map without blowing the shadow stack.
+
+        Regression guard: under the old recursive prelude implementation
+        this would allocate 8,000 stack frames and hit the 16K shadow
+        stack ceiling (post-#464).  The iterative implementation uses a
+        single WAT ``loop`` with O(1) stack depth regardless of input
+        size.
+
+        Size note: the GC's object-header size field is currently 16-bit
+        (max 65535 bytes) — see #484.  Output allocations must stay
+        under that limit or the sweep corrupts the payload.  8,000 Int
+        elements = 64,000 bytes — just under the ceiling.  Once #484
+        lands this test can grow to 100K+.
+        """
+        source = """\
+public fn main(-> @Int)
+  requires(true) ensures(true) effects(pure)
+{
+  let @Array<Int> = array_range(0, 8000);
+  let @Array<Int> = array_map(@Array<Int>.0, fn(@Int -> @Int) effects(pure) { @Int.0 * 2 });
+  @Array<Int>.0[7999]
+}
+"""
+        # Last element: 7999 * 2 = 15998
+        assert _run(source, fn="main") == 15998
+
+    def test_array_map_type_change_int_to_bool(self) -> None:
+        """Map Int → Bool — exercises the distinct-A-and-B codegen path.
+
+        All the existing tests keep the element type (Int → Int).  This
+        one converts to Bool, which has a different WASM type (i32) and
+        different element width (1 byte vs 8) from Int.  The store ops
+        must pick up the B-sized layout, not reuse A's.
+        """
+        source = """\
+public fn main(-> @Int)
+  requires(true) ensures(true) effects(pure)
+{
+  let @Array<Bool> = array_map([0, 1, 2, 3], fn(@Int -> @Bool) effects(pure) { @Int.0 > 1 });
+  -- [false, false, true, true] → sum of 1-for-each-true = 0+0+1+1 = 2
+  if @Array<Bool>.0[0] then { 1 } else { 0 } +
+  if @Array<Bool>.0[1] then { 1 } else { 0 } +
+  if @Array<Bool>.0[2] then { 1 } else { 0 } +
+  if @Array<Bool>.0[3] then { 1 } else { 0 }
+}
+"""
+        assert _run(source, fn="main") == 2
+
+    def test_array_map_closure_captures_outer_variable(self) -> None:
+        """Closure passed to array_map references a captured outer value.
+
+        Ensures the iterative loop body correctly sets up the closure
+        environment — the free-variable walker must lift the captured
+        binding into the closure struct, and the inside-the-loop
+        ``call_indirect`` must pass the env pointer so captures
+        resolve.
+        """
+        source = """\
+public fn main(-> @Int)
+  requires(true) ensures(true) effects(pure)
+{
+  let @Int = 100;
+  let @Array<Int> = array_map([1, 2, 3], fn(@Int -> @Int) effects(pure) { @Int.0 + @Int.1 });
+  @Array<Int>.0[2]
+}
+"""
+        # Outer @Int.0 = 100 (captured); [1, 2, 3][2] = 3;
+        # closure returns element + captured = 3 + 100 = 103.
+        assert _run(source, fn="main") == 103
+
+    def test_array_map_pair_element_output(self) -> None:
+        """Map Int → String — output is a pair-typed element (i32_pair).
+
+        This exercises the pair-output path in the iterative
+        translator: the store sequence must lay down ptr at offset 0
+        and len at offset 4, keyed off an 8-byte stride.
+        """
+        source = """\
+public fn main(-> @Int)
+  requires(true) ensures(true) effects(pure)
+{
+  let @Array<String> = array_map([1, 2, 3], fn(@Int -> @String) effects(pure) { to_string(@Int.0) });
+  string_length(@Array<String>.0[2])
+}
+"""
+        # "3" has length 1
+        assert _run(source, fn="main") == 1
+
+    def test_array_map_empty_input(self) -> None:
+        """Empty input → empty output; loop init/term exercised at n=0.
+
+        Exercises the zero-length boundary: the loop's ``idx >= arr_len``
+        guard must fire on the very first iteration so the body never
+        runs, the closure is never invoked, and the allocated output
+        array has length 0.
+        """
+        source = """\
+public fn main(-> @Nat)
+  requires(true) ensures(true) effects(pure)
+{
+  let @Array<Int> = array_range(0, 0);
+  let @Array<Int> = array_map(@Array<Int>.0, fn(@Int -> @Int) effects(pure) { @Int.0 * 2 });
+  array_length(@Array<Int>.0)
+}
+"""
+        assert _run(source, fn="main") == 0

tests/test_prelude.py

@@ -43,8 +43,11 @@ def _alias_names(prog: ast.Program) -> set[str]:
 # Prelude combinator function names
 _OPTION_FN_NAMES = {"option_unwrap_or", "option_map", "option_and_then"}
 _RESULT_FN_NAMES = {"result_unwrap_or", "result_map"}
+# ``array_map`` is emitted as iterative WASM by codegen (#480);
+# it no longer has a prelude-injected recursive implementation.
+# ``array_filter`` / ``array_fold`` remain recursive prelude functions
+# until their own iterative migration lands.
 _ARRAY_FN_NAMES = {
-    "array_map", "array_map_go",
     "array_filter", "array_filter_go",
     "array_fold", "array_fold_go",
 }
@@ -110,7 +113,14 @@ def test_result_combinators_injected(self) -> None:
         assert _RESULT_FN_NAMES.issubset(names)
 
     def test_array_operations_injected(self) -> None:
-        """Array operations always injected."""
+        """Array operations always injected — except array_map.
+
+        ``array_map`` / ``array_map_go`` are emitted as iterative WASM
+        by codegen (#480) and must NOT appear in the prelude-injected
+        function set.  The explicit negative assertion guards against
+        accidental re-injection if someone widens ``_ARRAY_FN_NAMES``
+        without updating the prelude.
+        """
         prog = _make_program(
             "public fn main(@Unit -> @Int)\n"
             "  requires(true) ensures(true) effects(pure)\n"
@@ -119,6 +129,9 @@ def test_array_operations_injected(self) -> None:
         inject_prelude(prog)
         names = _fn_names(prog)
         assert _ARRAY_FN_NAMES.issubset(names)
+        # Regression: array_map is a built-in, not a prelude function.
+        assert "array_map" not in names
+        assert "array_map_go" not in names
 
     def test_combinators_with_user_option(self) -> None:
         """Option combinators still injected when user defines standard Option."""

vera/codegen/modules.py

@@ -252,6 +252,10 @@ def _check_cross_module_calls(self, program: ast.Program) -> None:
         known.update({
             "array_length", "array_append", "array_range", "array_concat",
             "array_slice",
+            # Higher-order combinators — iterative WASM (#480).
+            # array_filter / array_fold still use the recursive prelude
+            # form until their own iterative migration lands.
+            "array_map",
             "apply_fn", "get", "put", "throw", "resume",
             "string_length", "string_concat", "string_slice",
             "string_char_code", "string_from_char_code", "string_repeat",