v0.0.196

Added

• examples/async_http_fanout.vera — the 37th example and the showcase for the v0.0.192 concurrent <Async>: two async(Http.get(url)) requests started back-to-back so network latency overlaps, then awaited and folded into a Z3-proved 0..3 status summary (4 obligations Tier-1 verified). examples/async_futures.vera and EXAMPLES.md's async section were reworded to stop teaching eager-only async: eager applies to non-whitelisted shapes, direct Http.get/Http.post calls run concurrently (#841).
• Two conformance programs pinning the apply_fn fix (suite now 106): ch05_apply_fn_typing (verify level — alias-typed application, variadic two-parameter application, deliberately non-commutative subtraction so a slot swap is caught) and ch05_apply_fn_arity (negative fixture, expected_error: E201 — a wrong-arity apply_fn must fail check).
• Spec completions after the server-effects sprint: §0.7 chapter index gains the Chapter 13 row; §7.7.6 documents the Async marker effect alongside its peers; §9.5.3 drops the stale "(future work)" framing on async Http composition; §9.3.4 scopes the Future<T> zero-overhead claim to eagerly-evaluated futures; §11.10.5 documents apply_fn's checker typing.
• wasmtime serve line-buffering caveat (spec §13.7 + TOOLCHAIN.md), empirically confirmed: under --world server a handler's IO.print without a trailing newline is held in the host's line buffer (flushed by the next newline, dropped at shutdown if none comes) — end log lines with \n; native vera serve does not buffer this way.
• veralang.dev surfaces the server/WASI work: two new Key-features cards (Verified HTTP handlers; WASI 0.2 components), a third Runs-Everywhere column with the --target wasi-p2 --world server → wasmtime serve command sequence, HttpServer in every effect list, and the 14-chapter/eight-effect counts — mirrored in the build_site.py literals that generate index.md/llms.txt/llms-full.txt (the hardcoded chapter list there gains Chapter 13).

Changed

• Documentation sweep after the server-effects sprint (v0.0.192–v0.0.195): HttpServer and the WASI targets are now surfaced in README (tagline, delivered-features), FAQ, and DESIGN.md's target/Async rows; KNOWN_ISSUES.md's WASI limitation row is rescoped from the closed #237 to the honest remainder tracked by #853 (wasi-p2 covers IO+Random only; the default target still uses ad-hoc vera.* imports), and the same rescope retitles vera/README's row to "Partial WASI support"; stale coverage-gap rows for the shipped #592/#645 removed; vera/README's module map gains codegen/wasi.py, runtime/wasi_host.py, runtime/server.py (plus tail_position.py, text.py) with recounted package totals (~65,000 lines of Python); CONTRIBUTING.md's branch-protection section now records enforce_admins and the actual review requirement; MUTATION.md documents the stale-.pyc purge step for hand-run mutation kills; ch10_float_predicates renamed ch09_float_predicates (its content, manifest chapter, and spec_ref were all chapter 9); counts refreshed everywhere (37 examples, 106 conformance programs, 14 spec chapters, live test totals). Scheduled limitation-state checking in CI is tracked by #852.

Fixed

• apply_fn is now typed by the checker — no more spurious E200, and misuse is a check-time error (#854). The documented primitive for applying a stored function value was unknown to the checker: every use fell into the unresolved-bare-call path, drawing a [E200] Unresolved function 'apply_fn' warning on green programs (vera check examples/closures.vera showed it) and typing the call as Unknown — so wrong arity or argument types passed check with exit 0 and only surfaced at compile time (a raw WAT assembler error at line 0,0, or a silently skipped function), and applying an effects(<IO>)-rowed fn value inside an effects(pure) function passed entirely (a reachable effect-soundness hole: the fn-typed parameter route was open even though constructing such a closure in a pure fn already tripped E122). apply_fn is variadic and effect-polymorphic — arity, argument types, result type, and effect row all come from the applied value's fn type — so it cannot be a fixed-signature registry row; it is now a checker special form typed structurally against the applied FunctionType: wrong arity → [E201], wrong argument type / non-function first argument → [E202], the applied row joins the caller's used effects and is checked against the declared row ([E122]/[E125]), and the result is the fn type's return type (a body returning an apply_fn result against the wrong declared return is now [E121]). TypeVar-parameterised fn-type aliases (the prelude combinator shape, e.g. @Mapper<A, B> params) check as before. Redefining fn apply_fn(...) — previously green at check time while codegen hijacked every 2+-argument call to call_indirect, silently skipping the caller — is now the same [E151] one-canonical-form error as any built-in redefinition. Mutation-validated four ways (special form disabled, effect-row join skipped, arity check skipped, E151 reject-set entry dropped — each flips exactly its discriminating tests RED).
• Prelude combinator skip-warnings no longer fire on every compile, and prelude diagnostics no longer misattribute to user source (#851). Every vera compile used to emit five [E602]/[E604] warnings about the generic Option/Result prelude combinators (option_unwrap_or, option_map, option_and_then, result_unwrap_or, result_map) being skipped — code the user didn't write and, in most programs, never calls — with locations that resolved the prelude buffer's line numbers against the user's file (a 5-line hello cited "line 61"; longer files rendered unrelated user source under the caret). Two fixes: (1) synthetic origin — diagnostics about prelude-injected declarations (and their mono clones, and nodes inside their bodies) now cite the synthetic file <prelude> and quote the actual prelude source line, in both text and --json output, so a prelude span can never render user code (inject_prelude returns the buffer it parsed; codegen's _warning/_error resolve prelude-origin nodes against it); (2) reachability suppression — E602/E604/E605 skip-warnings for prelude functions are dropped unless the program actually references them, via a transitive call-target scan rooted at every non-prelude declaration (including generic user fns the mono collector never visits, and imported module fns), so a minimal program compiles with zero warnings while a program that references a skipped combinator without a compilable instantiation keeps exactly that combinator's warning as the honest pre-runtime signal (now correctly attributed). A program that successfully calls option_map was already clean for the called fn via the #604 mono-compiled suppression; with the unreferenced four now silent too, it also compiles warning-free. User-defined unsupported functions warn exactly as before, with user-file locations (pinned by test). Mutation-validated four ways (suppression deleted, origin tag dropped, transitivity broken, body-node flag stuck false — each flips its discriminating test RED).