feat(wasi): experimental WASI Preview 2 target — vera compile/run --target wasi-p2 — v0.0.194

CHANGELOG.md

@@ -6,10 +6,16 @@ The format is based on [Keep a Changelog](https://keepachangelog.com/en/1.1.0/).
 
 ## [Unreleased]
 
+## [0.0.194] - 2026-07-02
+
+### Added
+
+- **Experimental WASI Preview 2 target — `vera compile/run --target wasi-p2`** ([#237](https://github.com/aallan/vera/issues/237)).  `vera compile --target wasi-p2` emits a **binary WebAssembly component** whose `vera.*` IO + Random host imports are implemented on top of WASI 0.2 interfaces, runnable by any stock wasip2 host — `wasmtime run` works with no flags and no Vera bindings (`wasmtime.wat2wasm` accepts component text, so no external componentizer and no new dependency).  The component wraps the **unchanged core module** (the default `--target wasm` emission is untouched, pinned by test): each `(import "vera" "op")` becomes a same-named `call_indirect` shim through a funcref dispatch table the main module defines and exports, and a compiler-generated adapter core module implements all 14 IO/Random ops (plus the `contract_fail`/`overflow_trap` channels) over canon-lowered WASI imports, planting itself into the table via active elem segments strictly before any lifted export can run — the naive main↔adapter import topology is an instantiation cycle, which the component model forbids.  `cabi_realloc` is a bump allocator over a **GC-exempt 64 KiB scratch arena** below `gc_heap_start` (host-written data needs no rooting and a collection can never move a half-written block — the #593/#695 UAF class, host-side); data crossing back into Vera is copied into GC-heap blocks under explicit shadow-stack rooting, and a 500-arg GC-pressure stress pins it.  Canonical-ABI variant discriminants are read `i32.load8_u` (they are u8; retptr-slab reuse leaves garbage in the padding — found live as an EOF misread as `last-operation-failed` with a stale list length as a "handle").  `vera run --target wasi-p2` executes the component under wasmtime-py's built-in `add_wasip2()` host (new `vera/runtime/wasi_host.py`) with the core path's `ExecuteResult` contract: stdout/stderr capture (+ the #543 live tee), `os.environ` snapshot, cwd preopen for file ops, argv, `IO.read_line` CRLF handling matching the core host's universal-newlines behavior (a lone `\r` separator stays content — spec chapter 13), and the #516 trap-kind taxonomy — a contract violation classifies as `contract_violation` with the full violation text recovered from the WASI stderr channel (structured frames do not cross the component boundary; the JSON envelope's `frames` is empty — spike check 5's documented degradation).  A program using any host family beyond IO/Random gets a **diagnostic naming the family** — never a silent fallback to the core target.  Both entry worlds are exported: `wasi:cli/run@0.2.0` (what stock `wasmtime run` invokes) and a plain lifted `main` for scalar returns (`Int`/`Nat` as `s64`, `Float64`, `Unit`); a `String`/heap-returning `main` runs via `wasi:cli/run` and reports no value.  Inherent WASI 0.2 divergences are documented in the new **spec chapter 13** and pinned by tests: `wasi:cli/exit@0.2.0` carries ok/err only, so `IO.exit(n)` degrades to exit status 0/1 under *every* wasip2 host.  Validation is live, not parse-only (the design study caught a mis-spelled filesystem `error-code` case — `quota`, not `disk-quota` — only at `add_wasip2` instantiation): the suite instantiates and executes every artifact, a **dual-target conformance differential** runs all 88 run-level conformance programs under both targets and requires byte-identical stdout/stderr (71 execute identically; the rest are family-gated, `main`-less, or wall-clock-dependent — the sweep also surfaced that `handle[Exn]` programs need the wasip2 runner to enable the exceptions proposal like the core engine does), and a stock-`wasmtime`-CLI smoke test runs where the CLI is installed.  This closes #237 as written (its listed ops are exactly the IO family) as an **experimental WASI Preview 2 target (IO + Random surface)** — not a blanket "WASI 0.2 compliant" claim; the remaining `vera.*` families (Map, Set, Decimal, Json, Html, Md, Regex, Math, Http, Inference, State, Async) stay host-bound on the core target.  Also: the doc-builtin-shadowing scanner now skips `.claude/` (session-tooling worktrees carry full repo copies that re-flagged every spec chapter).
+
 ### Fixed
 
 - **GC use-after-free: pair-typed `let` bindings (`String` / `Array<T>`) were never shadow-rooted** ([#847](https://github.com/aallan/vera/issues/847), fixed by [#846](https://github.com/aallan/vera/pull/846)).  The plain-`let` pair branch in `translate_block` (`vera/wasm/context.py`) stored the (ptr, len) pair into WASM locals without pushing the pointer onto the GC shadow stack — the last unrooted sibling of the [#705](https://github.com/aallan/vera/issues/705) scalar-i32 let fix and the [#707](https://github.com/aallan/vera/pull/707) let-destruct pair fix (whose review comment had already named this gap class).  Unobservable for Vera-side producers — an array literal or string builtin shadow-pushes its own freshly-allocated block at the alloc site, and that push survives to the function epilogue, masking the missing let root — but a **host-import** pair (`IO.args` → `Array<String>`, `IO.read_line` → `String`) is rooted only host-side during construction (`_ShadowGuard`, popped on return), so the first Vera-side allocation after the `let` could collect the block while the locals still pointed at it: the free list overwrites the payload's first words and reads through the binding see reclaimed bytes (`IO.print` of an `IO.args` element after a `nat_to_string` call printed `2::++2@` instead of `2:aa+bb`; `string_join` over the swept backing chased overwritten element pointers).  Found stress-testing [#237](https://github.com/aallan/vera/issues/237) under `VERA_EAGER_GC=1`; no WASI code involved, and reachable under ordinary collection pressure.  Pair lets are now rooted unconditionally — static and null pointers are ignored by the conservative scan's heap range check, so the push is harmless for non-heap values.  New targeted eager-GC tests pin the fix (args / read_line reproducers) and confirm the neighbouring host-import ADT paths (`IO.read_file` → `Result<String, String>`, `IO.get_env` → `Option<String>`) were already rooted by the #705/#707-era fixes.
-- **De-flaked the #841 live-interrupt test; one red combo no longer cancels the CI matrix** ([#848](https://github.com/aallan/vera/issues/848)).  `test_async_await_keyboard_interrupt_live_request` printed its progress marker *between* `async(...)` and `await`, racing the worker thread's request — whose arrival gates the test's interrupt — against the guest reaching the print: a lost race yields the correct exit 130 with empty stdout and failed the stdout assertion (twice on macos-26 runners across PR [#846](https://github.com/aallan/vera/pull/846)'s matrices, each time cancelling the other 11 fail-fast jobs).  The print now precedes the `async(...)`, so program order supplies a real happens-before (buffer write → request issuance → arrival → interrupt) and the assertion strengthens from `in` to `==`; prompt issuance at the `async` point stays pinned by the #841 request-ordering and operand-stack tests, so the reorder loses nothing.  The test matrix also sets `fail-fast: false`, so a single red combo reports alone instead of cancelling eleven healthy jobs.
+- **De-flaked the #841 live-interrupt test; one red combo no longer cancels the CI matrix** ([#848](https://github.com/aallan/vera/issues/848)).  `test_async_await_keyboard_interrupt_live_request` printed its progress marker *between* `async(...)` and `await`, racing the worker thread's request — whose arrival gates the test's interrupt — against the guest reaching the print: a lost race yields the correct exit 130 with empty stdout and failed the stdout assertion (twice on macos-26 runners across PR [#846](https://github.com/aallan/vera/pull/846)'s matrices, each time cancelling the other 11 fail-fast jobs).  The print now precedes the `async(...)`, so program order supplies a real happens-before (buffer write → request issuance → arrival → interrupt) and the assertion strengthens from `in` to `==`; prompt issuance at the `async` point stays pinned by the #841 request-ordering and operand-stack tests, so the reorder loses nothing.  The test matrix also sets `fail-fast: false`, so a single red combo reports alone instead of cancelling eleven healthy jobs.  **Round 2 (PR #849, closes #848):** the reorder alone proved insufficient — server arrival is produced by the executor worker thread and says nothing about the main thread's position, so `interrupt_main()`'s pending flag could materialize outside `execute()`'s protected region on slow runners (an xdist worker crash on two macOS jobs, a completed run with `exit_code=None` on ubuntu — 3/12 jobs at one head).  The interrupter now also polls `sys._current_frames()` until the main thread is verifiably parked in `host_async_await` → `Future.result` — the interruptible wait the #595-class machinery intercepts — before firing, with a bounded deadline so the test can never hang.
 
 ## [0.0.193] - 2026-07-02
 
@@ -2733,7 +2739,8 @@ Small docs sweep — closes six aging documentation issues in one PR.  No code c
 - Grammar: handler body simplified to avoid LALR reduce/reduce conflict
 - `pyproject.toml`: corrected build backend, package discovery, PEP 639 compliance
 
-[Unreleased]: https://github.com/aallan/vera/compare/v0.0.193...HEAD
+[Unreleased]: https://github.com/aallan/vera/compare/v0.0.194...HEAD
+[0.0.194]: https://github.com/aallan/vera/compare/v0.0.193...v0.0.194
 [0.0.193]: https://github.com/aallan/vera/compare/v0.0.192...v0.0.193
 [0.0.192]: https://github.com/aallan/vera/compare/v0.0.191...v0.0.192
 [0.0.191]: https://github.com/aallan/vera/compare/v0.0.190...v0.0.191

CLAUDE.md

@@ -31,8 +31,10 @@ vera verify --quiet file.vera     # Verify, suppress success output
 vera compile file.vera                    # Compile to .wasm binary
 vera compile --wat file.vera              # Print WAT text (human-readable WASM)
 vera compile --target browser file.vera   # Compile + emit browser bundle
+vera compile --target wasi-p2 file.vera   # Emit a WASI Preview 2 component (experimental, IO+Random; #237)
 vera run file.vera                # Compile and execute (calls main)
 vera run file.vera --fn f -- 42   # Call function f with argument 42
+vera run --target wasi-p2 file.vera  # Execute under the built-in WASI 0.2 host (spec/13-wasi.md)
 vera serve file.vera              # Serve handle(Request -> Response) over HTTP (#305)
 vera serve --port 8080 file.vera  # Serve on a specific port (default 8000)
 vera test file.vera               # Contract-driven testing via Z3 + WASM
@@ -83,7 +85,7 @@ See [`TOOLCHAIN.md`](TOOLCHAIN.md) for the CLI cookbook — driving the toolchai
 
 ## Project layout
 
-- `spec/` — Language specification (Chapters 0-12)
+- `spec/` — Language specification (Chapters 0-13)
 - `vera/` — Reference compiler: grammar, parser, AST, transformer, type checker, verifier, codegen, CLI
 - `examples/` — 36 example Vera programs (all must pass `vera check` and `vera verify`)
 - `tests/` — Test suite (unit tests + conformance suite)

HISTORY.md

@@ -427,22 +427,23 @@ Demo-first: each stage ships a working capability, cut as its own release, on th
 |---------|------|-------------|
 | v0.0.192 | 2 Jul | Concurrent `<Async>`: `async(Http.get/post)` runs on a host worker thread, `await` blocks for it, `W002` marks the eager remainder ([#841](https://github.com/aallan/vera/issues/841)); rides with the #420/#419/#839 test-oracle splits. |
 | v0.0.193 | 2 Jul | `<HttpServer>`: total contract-checked handlers served over HTTP by `vera serve` with instance-per-request isolation ([#305](https://github.com/aallan/vera/issues/305)). |
+| v0.0.194 | 2 Jul | Experimental WASI Preview 2 target: `--target wasi-p2` emits a binary component that runs IO+Random programs under any stock wasip2 host ([#237](https://github.com/aallan/vera/issues/237)). |
 
 ---
 
 ## By the numbers
 
-Six releases, chosen for the capability each one unlocked rather than even spacing.
+Eight releases, chosen for the capability each one unlocked rather than even spacing.
 
-| Metric | v0.0.1 (23 Feb) | v0.0.9 (23 Feb) | v0.0.65 (4 Mar) | v0.0.101 (27 Mar) | v0.0.170 (12 Jun) | v0.0.191 (1 Jul) | v0.0.193 (2 Jul) |
-|--------|:---:|:---:|:---:|:---:|:---:|:---:|:---:|
-| Milestone | First release | Runs end-to-end | GC + maturity | Inference effect | Language server | Soundness campaign | HttpServer effect |
-| Compiler layers | Parser | 5 (full pipeline) | 5 + modules + GC | 5 + modules + GC + browser | 5 + modules + GC + browser + LSP | 5 + modules + GC + browser + LSP | 5 + modules + GC + browser + LSP |
-| Tests | ~50 | ~300 | ~1,400 | 3,095 | 4,342 | 5,559 | 5,615 |
-| Examples | 13 | 15 | 18 | 30 | 35 | 35 | 36 |
-| Built-in functions | 0 | 0 | ~30 | 122 | 164 | 164 | 164 |
-| Conformance programs | 0 | 0 | 0 | 64 | 89 | 103 | 104 |
-| Spec chapters | 7 | 10 | 12 | 13 | 13 | 13 | 13 |
-| Code coverage | — | — | 90% | 96% | 95% | 95% | 95% |
+| Metric | v0.0.1 (23 Feb) | v0.0.9 (23 Feb) | v0.0.65 (4 Mar) | v0.0.101 (27 Mar) | v0.0.170 (12 Jun) | v0.0.191 (1 Jul) | v0.0.193 (2 Jul) | v0.0.194 (2 Jul) |
+|--------|:---:|:---:|:---:|:---:|:---:|:---:|:---:|:---:|
+| Milestone | First release | Runs end-to-end | GC + maturity | Inference effect | Language server | Soundness campaign | HttpServer effect | WASI 0.2 target |
+| Compiler layers | Parser | 5 (full pipeline) | 5 + modules + GC | 5 + modules + GC + browser | 5 + modules + GC + browser + LSP | 5 + modules + GC + browser + LSP | 5 + modules + GC + browser + LSP | 5 + modules + GC + browser + LSP + WASI |
+| Tests | ~50 | ~300 | ~1,400 | 3,095 | 4,342 | 5,559 | 5,615 | 5,768 |
+| Examples | 13 | 15 | 18 | 30 | 35 | 35 | 36 | 36 |
+| Built-in functions | 0 | 0 | ~30 | 122 | 164 | 164 | 164 | 164 |
+| Conformance programs | 0 | 0 | 0 | 64 | 89 | 103 | 104 | 104 |
+| Spec chapters | 7 | 10 | 12 | 13 | 13 | 13 | 13 | 14 |
+| Code coverage | — | — | 90% | 96% | 95% | 95% | 95% | 95% |
 
-Total: **1,800+ commits, 193 tagged releases, 92 active development days.**
+Total: **1,800+ commits, 194 tagged releases, 92 active development days.**

README.md

@@ -166,6 +166,8 @@ Hello, World!
 ```bash
 vera run file.vera --fn f -- 42           # call function f with argument 42
 vera compile --target browser file.vera   # emit browser bundle
+vera compile --target wasi-p2 file.vera   # emit a WASI Preview 2 component (experimental)
+vera run --target wasi-p2 file.vera       # execute under the built-in WASI 0.2 host
 vera test file.vera                       # contract-driven testing via Z3 + WASM
 vera fmt file.vera                        # format to canonical form
 vera verify --json file.vera              # JSON diagnostics for agent feedback loops
@@ -179,6 +181,8 @@ vera errors --json                       # list the diagnostic error-code regist
 
 `vera compile --target browser` produces a self-contained bundle (wasm + JS runtime + HTML) that runs in any browser — no build step, no bundler. Mandatory parity tests ensure identical behaviour between the command-line and browser runtimes for the pure-language surface (arithmetic, ADTs, pattern matching, closures, contracts, effects-as-host-imports, etc.).  The IO surface is the documented exception: terminal Vera programs that rely on `IO.sleep` for animation pacing or ANSI escape codes for cursor control compile cleanly to `--target browser` but render the escapes as literal text and freeze the tab while sleeping — the browser target expects Vera to be the pure simulation core and JavaScript to drive timing and rendering ([SKILL.md §Browser compilation](SKILL.md#browser-compilation) has the recommended pattern).
 
+`vera compile --target wasi-p2` emits an **experimental WASI Preview 2 target (IO and Random surface)**: a binary WebAssembly component whose host imports are implemented over WASI 0.2 interfaces, runnable by any stock wasip2 host (`wasmtime run` needs no flags and no Vera bindings). Programs using host families beyond IO/Random are rejected with a diagnostic naming the family — never silently compiled against the core target. See [spec chapter 13](spec/13-wasi.md) for the architecture, the supported surface, and the documented divergences (WASI 0.2's ok/err-only exit codes, no structured trap frames across the component boundary).
+
 ### Editor support
 
 Vera ships a [language server](LSP_SERVER.md) (`vera lsp`, via the optional `[lsp]` extra) that keeps a warm incremental Z3 session between keystrokes — diagnostics, proofs, hover, slot go-to-definition, and typed-hole completion at editor latency, plus custom proof-delta methods for coding agents. See **[LSP_SERVER.md](LSP_SERVER.md)** for setup and the full protocol surface.
@@ -215,9 +219,9 @@ cp /path/to/vera/SKILL.md ~/.claude/skills/vera-language/SKILL.md
 
 ## Project status
 
-Vera is in **active development** at v0.0.193 — 1,800+ commits, 193 releases, 5,620 tests, 91% code coverage, 104 conformance programs, 36 examples, and a 13-chapter specification. See **[HISTORY.md](HISTORY.md)** for how the compiler was built.
+Vera is in **active development** at v0.0.194 — 1,800+ commits, 194 releases, 5,768 tests, 91% code coverage, 104 conformance programs, 36 examples, and a 14-chapter specification. See **[HISTORY.md](HISTORY.md)** for how the compiler was built.
 
-The reference compiler — parser, AST, type checker, contract verifier (Z3), WASM code generator, module system, browser runtime, and runtime contract insertion — is working. The language specification is in draft across [13 chapters](spec/).
+The reference compiler — parser, AST, type checker, contract verifier (Z3), WASM code generator, module system, browser runtime, and runtime contract insertion — is working. The language specification is in draft across [14 chapters](spec/).
 
 **Key features delivered:** [typed De Bruijn indices](DE_BRUIJN.md) (`@T.n`), mandatory contracts, algebraic effects (IO, Http, State, Exceptions, Async, Inference, Random), refinement types, constrained generics (Eq, Ord, Hash, Show), algebraic data types, pattern matching, modules, 164 built-in functions (strings, arrays, maps, sets, decimals, math, JSON, HTML, Markdown, regex, base64, URL), contract-driven testing, canonical formatter, browser runtime, three-tier verification (Z3 static, guided, runtime fallback), and a [language server](LSP_SERVER.md) with warm incremental verification and agent-facing proof-delta methods.
 
@@ -243,7 +247,7 @@ vera/
 ├── CONTRIBUTING.md                # Contributor guidelines
 ├── CHANGELOG.md                   # Version history
 ├── LICENSE                        # MIT licence
-├── spec/                          # Language specification (13 chapters)
+├── spec/                          # Language specification (14 chapters)
 ├── vera/                          # Reference compiler (Python)
 │   ├── grammar.lark               #   Lark LALR(1) grammar
 │   ├── parser.py                  #   Parser module