v0.0.187

Fixed

• Integer-overflow runtime traps now carry a precise overflow trap kind (#808). The #798 @Int / @Nat arithmetic-overflow guard trapped via a bare unreachable, so a dynamic overflow was classified kind="unreachable" and surfaced the generic non-exhaustive-match Fix paragraph — indistinguishable from an unrelated unreachable. The guard now calls a new vera.overflow_trap host import (mirroring vera.contract_fail) immediately before its unreachable; that signals an out-of-band channel _classify_trap checks before the str(exc) substring scan (which would otherwise match the trailing unreachable first), so the trap classifies kind="overflow" and carries the overflow Fix paragraph (the i64 / u64 range and the requires(...) remediation). Both runtimes provide the new import — the wasmtime host in execute() and the browser/Node runtime.mjs, whose dynamic import builder now binds vera.overflow_trap so a --target browser bundle still instantiates and surfaces "Integer overflow" rather than LinkError-ing on any arithmetic. The @Nat-subtraction underflow (#520) and @Nat → @Int widen (#813) guards are unchanged and still classify unreachable — tests/test_int_overflow_codegen.py::TestOverflowTrapKind808 pins the new overflow classification (all five + / - / * sites, both int_mul trap branches, plus the lifted-closure and ensures(...)-postcondition paths) and those two unchanged controls, and tests/test_browser.py pins the wasmtime↔Node parity.

• Host-import / allocation flags used only inside a requires(...) / ensures(...) contract are now declared (#823). A builtin or allocation reachable only through a contract predicate had its host-import / memory / GC flag set too late for module assembly, so the import / (memory …) / $gc_sp declaration was omitted and the orphaned call/global.get failed WAT compilation (unknown func: $vera.sin, unknown func: $vera.regex_match, unknown global: $gc_sp, …). Surfaced while wiring #808's vera.overflow_trap. Two fixes, by mechanism: (1) the per-function flag merge now runs after _compile_postconditions, covering every context-tracked family (sin/cos/pow math, json_*, html_*, map_*/set_*, decimal_*, http_*, inference_*, random_*) plus $alloc/$gc_sp and vera.overflow_trap; (2) the body host-import pre-scan now also walks the contract predicates, covering md_* and regex_*, which are registered only by that scan (they have no per-function set-site). Both changes are purely additive — nothing between the old and new positions reads these flags (they are consumed only at module assembly). Pinned by tests/test_codegen.py::TestPostconditionHostImportPropagation823 (math, allocation, regex, and Markdown builtins each in a postcondition over a scalar body).

Changed

• Documentation consistency pass (no code or behaviour change).
  • HISTORY.md restructured: the language-server stage (Stage 14) now ends at v0.0.170 and the verifier-soundness campaign is its own Stage 15; entries trimmed to one-liners with whole-sentence bold removed.
  • Removed the redundant defensive nat_to_int(@Nat.0) from three spec/09-standard-library.md reference examples — @Nat <: @Int is a first-class subtyping coercion (spec §2.2.1, "use a @Nat anywhere @Int is expected — no nat_to_int call"), so the explicit conversion was unnecessary.
  • Corrected stale counts and references across vera/README.md, AGENTS.md, SKILL.md, and examples/README.md: error-code range (E001–E702), ERROR_CODES count (123), test / conformance / example counts (5,442 / 103 / 35), the missing spec Chapter 8 row in SKILL's reference table, and the examples/README.md index completed to list all 35 examples (including the interactive read_char / inference ones, flagged for their stdin / API-key needs).
  • Synced the KNOWN_ISSUES.md Bugs table with the issue tracker's bug labels: added #775, labelled #766 bug, and relabelled #758 bug → limitation.