# Chapter 9: Standard Library

## 9.1 Overview

Vera's standard library provides built-in types, effects, and functions that are available in every Vera program without explicit import. The library is deliberately small — it includes only the types and operations that are universally needed and cannot be expressed purely in user code.

The standard library comprises:

- **Built-in ADTs**: `Option<T>` and `Result<T, E>` for representing partiality and fallibility.
- **Built-in collections**: `Array<T>` for fixed-size homogeneous sequences, `Set<T>` for unordered unique elements, and `Map<K, V>` for key-value mappings.
- **Built-in effects**: `IO` for output, `State<T>` for mutable state, `Http` for network I/O (`get` and `post`), `Async` for concurrency, `Inference` for LLM calls, `HttpServer` for verified HTTP handling, and `DB` for SQL database access (see §9.5 for each).
- **Built-in functions**: `array_length`, `array_append`, `array_range`, and `array_concat` for arrays, numeric operations (`abs`, `min`, `max`, `floor`, `ceil`, `round`, `sqrt`, `pow`), type conversions (`int_to_float`, `float_to_int`, `nat_to_int`, `int_to_nat`, `byte_to_int`, `int_to_byte`), Float64 predicates (`float_is_nan`, `float_is_infinite`, `nan`, `infinity`), string search (`string_contains`, `string_starts_with`, `string_ends_with`, `string_index_of`), string transformation (`string_strip`, `string_upper`, `string_lower`, `string_replace`, `string_split`, `string_join`, `string_char_code`, `string_from_char_code`), regular expressions (`regex_match`, `regex_find`, `regex_find_all`, `regex_replace`), plus future functions for vector similarity.
- **Decimal type**: `Decimal` for exact decimal arithmetic via host imports (see §9.7.2). Exact in both the Python runtime (`decimal.Decimal`) and the browser runtime (scaled-BigInt engine), which mirror each other operation-for-operation over finite decimal values.
- **Json type**: `Json` ADT for structured data interchange — parse, query, and serialize JSON via 8 built-in functions (see §9.7.1).
- **Markdown type**: `MdBlock` and `MdInline` ADTs for agent-oriented document structure — parse, render, and query Markdown via pure host-import functions (see §9.7.3).
- **Html type**: `HtmlNode` ADT for parsing and querying HTML documents — parse, serialize, query, and extract text via 5 built-in functions (see §9.7.4).
- **Built-in abilities**: `Eq`, `Ord`, `Hash`, `Show` — type constraints for generic programming. The `Ordering` ADT (`Less`, `Equal`, `Greater`) supports `Ord`'s `compare` operation.

All built-in types participate fully in the type system: they can appear in contracts, be verified by the SMT solver, and be used with refinement types and pattern matching. Built-in effects follow the same algebraic effect semantics as user-defined effects (see Chapter 7).

### 9.1.1 Naming Convention

Built-in function names follow a consistent `domain_verb` convention to make names predictable and reduce LLM hallucination errors:

| Pattern | When to use | Examples |
|---------|-------------|----------|
| `domain_verb` | Most functions — domain prefix identifies the type or module | `string_length`, `array_append`, `regex_match`, `md_parse` |
| `source_to_target` | Type conversions — source and target types in the name | `int_to_float`, `float_to_int`, `nat_to_int`, `int_to_byte` |
| `domain_is_predicate` | Boolean predicates — domain prefix + `is_` + property | `float_is_nan`, `float_is_infinite` |
| Prefix-less | Math universals only — names understood across all languages | `abs`, `min`, `max`, `floor`, `ceil`, `round`, `sqrt`, `pow` |

**Key rules:**

1. **String operations always use `string_` prefix**: `string_contains`, `string_starts_with`, `string_split`, `string_join`, `string_strip`, `string_upper`, `string_lower`, `string_replace`, `string_index_of`, `string_char_code`, `string_from_char_code`.
2. **Float64 predicates use `float_` prefix**: `float_is_nan`, `float_is_infinite`.
3. **Type conversions use `source_to_target`**: `int_to_float` (not `to_float`), `float_to_int`, `int_to_nat`.
4. **Math functions and float constants are the only exceptions** to domain prefixing — `abs`, `min`, `max`, `floor`, `ceil`, `round`, `sqrt`, `pow`, `nan`, and `infinity` need no prefix because they are universally understood mathematical names.
5. **New functions MUST follow these patterns.** When adding a function, choose the pattern that matches its category. If uncertain, use `domain_verb`.

### 9.1.2 Standard Prelude

Every Vera program implicitly has access to a **standard prelude** that provides commonly used ADTs and their associated operations without requiring explicit `data` declarations:

- **`Option<T>`** — `Some(T)`, `None` constructors.
- **`Result<T, E>`** — `Ok(T)`, `Err(E)` constructors.
- **`Ordering`** — `Less`, `Equal`, `Greater` constructors (for `Ord`'s `compare` operation).
- **`UrlParts`** — `UrlParts(String, String, String, String, String)` constructor (RFC 3986 decomposition).

In addition, Option/Result combinators (`option_unwrap_or`, `option_map`, `option_and_then`, `result_unwrap_or`, `result_map`) and array operations (`array_slice`, `array_map`, `array_filter`, `array_fold`) are automatically available.

User-defined `data` declarations with the same name **shadow** the prelude definition. If a user defines a non-standard variant (e.g. `data Option<T> { None, Just(T) }` instead of the standard `None, Some(T)`), the related combinators are suppressed — they rely on the standard constructor names.

## 9.2 Primitive Types

The primitive types (`Int`, `Nat`, `Bool`, `Byte`, `Float64`, `String`, `Unit`, `Never`) are documented in Chapter 2, Section 2.2. They are not part of the standard library per se — they are built into the language core.

## 9.3 Built-in ADTs

### 9.3.1 Option\<T\>

```
public data Option<T> {
  Some(T),
  None
}
```

`Option<T>` represents a value that may or may not be present. It is the standard way to express partiality in Vera — functions that might not produce a result return `Option<T>` rather than using null pointers or sentinel values.

Constructors:
- `Some(@T)` — wraps a present value.
- `None` — represents absence.

Pattern matching on `Option<T>` is exhaustive: both `Some` and `None` must be handled.

```
private fn safe_head(@Array<Int> -> @Option<Int>)
  requires(true)
  ensures(true)
  effects(pure)
{
  if array_length(@Array<Int>.0) > 0 then {
    Some(@Array<Int>.0[0])
  } else {
    None
  }
}
```

### 9.3.2 Result\<T, E\>

```
public data Result<T, E> {
  Ok(T),
  Err(E)
}
```

`Result<T, E>` represents a computation that may succeed with a value of type `T` or fail with an error of type `E`. It is the standard way to express fallible operations without using exceptions.

Constructors:
- `Ok(@T)` — wraps a successful result.
- `Err(@E)` — wraps an error value.

Pattern matching on `Result<T, E>` is exhaustive: both `Ok` and `Err` must be handled.

```
private fn checked_nat(@Int -> @Result<Nat, String>)
  requires(true)
  ensures(true)
  effects(pure)
{
  if @Int.0 >= 0 then {
    Ok(@Int.0)
  } else {
    Err("negative")
  }
}
```

### 9.3.3 UrlParts

<!-- vera:skip-check category="INCOMPLETE" reason="data UrlParts (no visibility keyword)" -->
```
data UrlParts {
  UrlParts(String, String, String, String, String)
}
```

`UrlParts` is a built-in ADT representing the five components of a URL per RFC 3986: scheme, authority, path, query, and fragment. It is provided by the standard prelude (see §9.1.2) and available in every program without an explicit `data` declaration.

Constructors:
- `UrlParts(@String, @String, @String, @String, @String)` — scheme, authority, path, query, fragment.

See §9.6.18 for the `url_parse` and `url_join` function specifications.

### 9.3.4 Future\<T\>

<!-- vera:skip-check category="INCOMPLETE" reason="data Future<T> (no visibility keyword)" -->
```
data Future<T> { Future(T) }
```

`Future<T>` represents the result of an asynchronous computation. An eagerly-evaluated future is WASM-transparent — it has the same runtime representation as `T`, with no overhead; a concurrently-evaluated future is an opaque pending handle with the same WASM value type (see §9.5.4).

Constructors:
- `Future(@T)` — wraps a value.

See §9.5.4 for the `async` and `await` function specifications.

### 9.3.5 MdInline

```
public data MdInline {
  MdText(String),
  MdCode(String),
  MdEmph(Array<MdInline>),
  MdStrong(Array<MdInline>),
  MdLink(Array<MdInline>, String),
  MdImage(String, String)
}
```

`MdInline` represents inline-level Markdown content. It is one of two mutually defined ADTs (with `MdBlock`) that make illegal states unrepresentable — a heading cannot contain another heading at the type level.

Constructors:
- `MdText(@String)` — plain text run.
- `MdCode(@String)` — inline code span.
- `MdEmph(@Array<MdInline>)` — emphasis (italic).
- `MdStrong(@Array<MdInline>)` — strong emphasis (bold).
- `MdLink(@Array<MdInline>, @String)` — hyperlink: display text and URL.
- `MdImage(@String, @String)` — image: alt text and source URL.

See §9.7.3 for the Markdown function specifications.

### 9.3.6 MdBlock

```
public data MdBlock {
  MdParagraph(Array<MdInline>),
  MdHeading(Nat, Array<MdInline>),
  MdCodeBlock(String, String),
  MdBlockQuote(Array<MdBlock>),
  MdList(Bool, Array<Array<MdBlock>>),
  MdThematicBreak,
  MdTable(Array<Array<Array<MdInline>>>),
  MdDocument(Array<MdBlock>)
}
```

`MdBlock` represents block-level Markdown elements.

Constructors:
- `MdParagraph(@Array<MdInline>)` — paragraph.
- `MdHeading(@Nat, @Array<MdInline>)` — heading: level (1--6) and content.
- `MdCodeBlock(@String, @String)` — fenced code block: language and code body.
- `MdBlockQuote(@Array<MdBlock>)` — block quote.
- `MdList(@Bool, @Array<Array<MdBlock>>)` — list: ordered/unordered, with items.
- `MdThematicBreak` — horizontal rule (nullary).
- `MdTable(@Array<Array<Array<MdInline>>>)` — table: rows of cells of inlines.
- `MdDocument(@Array<MdBlock>)` — top-level document.

See §9.7.3 for the Markdown function specifications.

### 9.3.7 Option and Result Combinators

The standard prelude (§9.1.2) provides combinator functions that eliminate common match boilerplate for `Option<T>` and `Result<T, E>`. These are injected automatically unless the user defines a non-standard variant (different constructors or arities) or shadows the function names.

**Option combinators:**

| Function | Signature | Description |
|----------|-----------|-------------|
| `option_unwrap_or` | `forall<T> (Option<T>, T) -> T` | Extract `Some` value or return default |
| `option_map` | `forall<A, B> (Option<A>, fn(A -> B)) -> Option<B>` | Transform the value inside `Some` |
| `option_and_then` | `forall<A, B> (Option<A>, fn(A -> Option<B>)) -> Option<B>` | Chain fallible operations |

**Result combinators:**

| Function | Signature | Description |
|----------|-----------|-------------|
| `result_unwrap_or` | `forall<T, E> (Result<T, E>, T) -> T` | Extract `Ok` value or return default |
| `result_map` | `forall<A, B, E> (Result<A, E>, fn(A -> B)) -> Result<B, E>` | Transform the `Ok` value |

Combinators follow the `domain_verb` naming convention (see §5). They are injected as private generic functions before compilation and undergo normal monomorphization. A combinator is not injected if the user defines a function with the same name.

## 9.4 Built-in Collections

### 9.4.1 Array\<T\>

`Array<T>` is a fixed-size, homogeneous, immutable ordered collection. Arrays are created with array literal syntax and accessed by integer index.

**Syntax:**

```
let @Array<Int> = [1, 2, 3];
@Array<Int>.0[0]
```

**Properties:**
- Fixed size: the length is determined at creation and cannot change.
- Immutable: elements cannot be modified after creation.
- Zero-indexed: the first element is at index 0.
- Bounds-checked: indexing with an out-of-range index causes a runtime trap (see Chapter 12).

**Element types:** Arrays can contain any type for which a WASM representation exists, including primitives (`Int`, `Nat`, `Bool`, `Byte`, `Float64`), ADT types (`Option<Int>`, `Result<Nat, String>`), `String`, and nested arrays (`Array<Array<Int>>`).

**Length:** The `array_length` built-in function returns the number of elements (see Section 9.6.1).

For the compilation model of arrays, see Chapter 11, Section 11.12.

### 9.4.2 Set\<T\>

`Set<T>` is an unordered collection of unique elements. It requires the `Eq` and `Hash` abilities on `T` (see Section 9.8). Element types must be hashable primitives: `Int`, `Nat`, `Bool`, `Float64`, `String`, or `Byte`.

Set is an opaque built-in type implemented via host imports. The runtime maintains the underlying set; WASM code interacts with sets through `i32` handles. All operations are pure — `set_add` and `set_remove` return new sets (functional semantics).

**Operations:**

| Function | Signature | Description |
|----------|-----------|-------------|
| `set_new()` | `forall<T> () → Set<T>` | Create an empty set |
| `set_add(s, t)` | `forall<T> (Set<T>, T) → Set<T>` | Return a new set with the element added |
| `set_contains(s, t)` | `forall<T> (Set<T>, T) → Bool` | Test whether an element is present |
| `set_remove(s, t)` | `forall<T> (Set<T>, T) → Set<T>` | Return a new set without the element |
| `set_size(s)` | `forall<T> (Set<T>) → Int` | Number of elements |
| `set_to_array(s)` | `forall<T> (Set<T>) → Array<T>` | All elements as an array |

```
private fn set_demo(-> @Int)
  requires(true)
  ensures(@Int.result == 2)
  effects(pure)
{
  set_size(set_add(set_add(set_new(), "hello"), "world"))
}
```

`Set` and `Map` (Section 9.4.3) together provide the standard collection types needed for structured data handling.

### 9.4.3 Map\<K, V\>

`Map<K, V>` is a key-value mapping. It requires the `Eq` and `Hash` abilities on `K` (see Section 9.8). Keys must be hashable primitive types: `Int`, `Nat`, `Bool`, `Float64`, `String`, or `Byte`. Values must be primitives (`Int`, `Nat`, `Bool`, `Byte`, `Float64`, `String`), ADT heap-pointer types (`Option<T>`, `Result<T, E>`), or other `Map` handles. `Array<T>` values are not yet supported as Map values (tracked as a future enhancement).

Map is an opaque built-in type implemented via host imports. The runtime maintains the underlying hash table; WASM code interacts with maps through `i32` handles. All operations are pure — `map_insert` and `map_remove` return new maps (functional semantics).

**Operations:**

| Function | Signature | Description |
|----------|-----------|-------------|
| `map_new()` | `forall<K, V> () -> Map<K, V>` | Create an empty map |
| `map_insert(m, k, v)` | `forall<K, V> (Map<K, V>, K, V) -> Map<K, V>` | Return a new map with the entry added |
| `map_get(m, k)` | `forall<K, V> (Map<K, V>, K) -> Option<V>` | Look up a key; `Some(v)` if present, `None` if absent |
| `map_contains(m, k)` | `forall<K, V> (Map<K, V>, K) -> Bool` | Test whether a key is present |
| `map_remove(m, k)` | `forall<K, V> (Map<K, V>, K) -> Map<K, V>` | Return a new map without the key |
| `map_size(m)` | `forall<K, V> (Map<K, V>) -> Int` | Number of entries |
| `map_keys(m)` | `forall<K, V> (Map<K, V>) -> Array<K>` | All keys as an array |
| `map_values(m)` | `forall<K, V> (Map<K, V>) -> Array<V>` | All values as an array |

All Map operations require `Eq<K>` and `Hash<K>` ability constraints.

**Example:**

```vera
private fn map_demo(-> @Int)
  requires(true)
  ensures(@Int.result == 42)
  effects(pure)
{
  option_unwrap_or(map_get(map_insert(map_new(), "answer", 42), "answer"), 0)
}
```

`Map` is needed by the proposed `Json` ADT (Section 9.7.1), where `JObject` wraps a `Map<String, Json>`.

## 9.5 Built-in Effects

### 9.5.1 IO

The `IO` effect provides input/output operations. Functions that perform IO must declare `effects(<IO>)`.

The `IO` effect has no type parameters. All IO operations are invoked as qualified calls (`IO.print(...)`, `IO.read_line(())`, etc.).

**Operations:**

| Operation | Signature | Description |
|-----------|-----------|-------------|
| `print` | `String -> Unit` | Write a UTF-8 string to stdout |
| `read_line` | `Unit -> String` | Read one line from stdin (trailing newline stripped) |
| `read_char` | `Unit -> Result<String, String>` | Read one character from stdin — cbreak mode on a Unix TTY, where Ctrl-D gives `Err("EOF")`; redirected input reads one character from the stdin stream and gives `Err("EOF")` at end of input |
| `read_file` | `String -> Result<String, String>` | Read file contents; returns `Ok(contents)` or `Err(message)` |
| `write_file` | `String, String -> Result<Unit, String>` | Write string to file; returns `Ok(())` or `Err(message)` |
| `args` | `Unit -> Array<String>` | Command-line arguments |
| `exit` | `Int -> Never` | Terminate with exit code (never returns) |
| `get_env` | `String -> Option<String>` | Look up environment variable; returns `Some(value)` or `None` |
| `sleep` | `Nat -> Unit` | Pause execution for N milliseconds |
| `time` | `Unit -> Nat` | Current Unix time in milliseconds |
| `stderr` | `String -> Unit` | Write a UTF-8 string to stderr |

The `IO` effect is registered as a built-in: the operations above are in scope for any function whose effect row names `IO`, and no declaration brings them there. An `effect IO { ... }` block in a program is a compile error (`E152`) — the same one-canonical-form rule that forbids redefining a built-in function (`E151`, Section 9.6). The rule is name-keyed and unconditional: a block whose operation signatures agree with the built-in is rejected too, because it is a second textual spelling of the same program (Chapter 0, Section 0.2, design goal 3). It also cannot be honoured — code generation lowers every qualified `IO.op(...)` call to the fixed host import selected by the qualifier and never reads the declaration, so a block whose signatures diverge from the built-in would compile to structurally invalid WebAssembly.

The same rule holds for every built-in effect, marker effects included. Chapter 7, Section 7.7 states it once for the whole registered set rather than naming them here, so the rule cannot fall out of step with the registry as effects are added.

```
private fn hello(-> @Unit)
  requires(true)
  ensures(true)
  effects(<IO>)
{
  IO.print("hello, world")
}
```

File operations return `Result` types for error handling:

```
public fn main(-> @Unit)
  requires(true)
  ensures(true)
  effects(<IO>)
{
  match IO.read_file("data.txt") {
    Ok(@String) -> IO.print(@String.0),
    Err(@String) -> IO.print(@String.0)
  };
  ()
}
```

For the runtime implementation of IO operations, see Chapter 12, Section 12.4.1.

### 9.5.2 State\<T\>

The `State<T>` effect provides mutable state operations. Functions that read or write state must declare the specific state type in their effect row: `effects(<State<Int>>)`. Like `IO`, `State<T>` is built-in — no `effect State<T> { ... }` declaration is needed (and one is `E152`).

| Operation | Signature | Description |
|-----------|-----------|-------------|
| `get` | `Unit -> T` | Reads the current state value; the `Unit` argument is written out, as `get(())` |
| `put` | `T -> Unit` | Writes a new state value |

Multiple independent state types can be used in the same function by declaring them in the effect row. State operations (`get`, `put`) are called without qualification — the type checker resolves which state cell is targeted from the types:

```
private fn increment(-> @Unit)
  requires(true)
  ensures(new(State<Int>) == old(State<Int>) + 1)
  effects(<State<Int>>)
{
  let @Int = get(());
  put(@Int.0 + 1);
  ()
}
```

State is handled by providing an initial value and a handler that manages the mutable cell:

```
private fn run_increment(@Unit -> @Int)
  requires(true)
  ensures(true)
  effects(pure)
{
  handle[State<Int>](@Int = 0) {
    get(@Unit) -> { resume(@Int.0) },
    put(@Int) -> { resume(()) }
  } in {
    let @Int = get(());
    put(@Int.0 + 1);
    get(())
  }
}
```

For the runtime implementation of `State<T>`, see Chapter 12, Section 12.4.2.

### 9.5.3 Http

> **Status: Implemented.** Tracked in [#57](https://github.com/aallan/vera/issues/57). `Http.get` and `Http.post` are fully compilable and execute via host imports (Python `urllib` / JavaScript `fetch`). Returns `Result<String, String>` — `Ok` with the response body, `Err` with the error message. New conformance test `ch09_http` (62 programs, was 61). New example `http.vera`.

Network I/O is modelled as a built-in algebraic effect with two operations: `get` and `post`. Functions performing network access declare `effects(<Http>)`. The effect is built-in — no `effect Http { ... }` declaration is needed (and one is `E152`).

**Operations:**

| Operation | Signature | Description |
|-----------|-----------|-------------|
| `get` | `String -> Result<String, String>` | Performs an HTTP GET request; `Ok(body)` on success, `Err(message)` on failure |
| `post` | `String, String -> Result<String, String>` | Performs an HTTP POST request with the given body (sent as `application/json`); `Ok(body)` on success, `Err(message)` on failure |

This fits naturally with Vera's algebraic effect system and makes network I/O explicit and testable.

**Composition with JSON:**

`Http.get` returns a string. To get typed data, compose with `json_parse`:

```
public fn fetch_json(@String -> @Result<Json, String>)
  requires(string_length(@String.0) > 0)
  ensures(true)
  effects(<Http>)
{
  let @Result<String, String> = Http.get(@String.0);
  match @Result<String, String>.0 {
    Ok(@String) -> json_parse(@String.0),
    Err(@String) -> Err(@String.0)
  }
}
```

This follows the same pattern as Markdown: `json_parse(Http.get(url))`, not a dedicated `get_json` operation. One way to do things (§0.2.3).

**Implementation notes:**

- The Python runtime uses `urllib.request.urlopen` (stdlib, no external dependencies).
- The browser/Node.js runtime uses the `fetch` API.
- `Http.post` sends the body with `Content-Type: application/json`.
- Responses are returned as the full response body string. Status codes are not currently exposed — non-2xx responses produce `Err`.
- HTTPS is supported. Certificate verification follows the platform default.

**Known limitations:**

- No custom headers ([#351](https://github.com/aallan/vera/issues/351)).
- No HTTP status code access ([#352](https://github.com/aallan/vera/issues/352)).
- No request timeout control ([#353](https://github.com/aallan/vera/issues/353)).
- Browser runtime uses deprecated synchronous XMLHttpRequest ([#355](https://github.com/aallan/vera/issues/355)).
- No PUT, PATCH, DELETE methods ([#356](https://github.com/aallan/vera/issues/356)).

**Async composition:**

Http composes with the `<Async>` effect for concurrent requests:

```
private fn fetch_both(@String, @String -> @Tuple<Result<String, String>, Result<String, String>>)
  requires(true)
  ensures(true)
  effects(<Http, Async>)
{
  let @Future<Result<String, String>> = async(Http.get(@String.0));
  let @Future<Result<String, String>> = async(Http.get(@String.1));
  let @Result<String, String> = await(@Future<Result<String, String>>.1);
  let @Result<String, String> = await(@Future<Result<String, String>>.0);
  Tuple(@Result<String, String>.1, @Result<String, String>.0)
}
```

> **Note:** As of #841 the reference implementation executes this shape concurrently: `async(Http.get(url))` submits the request to a host worker thread at the `async(...)` point, and `await` blocks for the response. See §9.5.4 for exactly which shapes are concurrent.

### 9.5.4 Async

The `<Async>` effect enables asynchronous computation via `async(expr)` and `await(future)` operations with a `Future<T>` type (see §9.3.4 for the ADT definition).

**Built-in functions:**

<!-- vera:skip-parse category="FRAGMENT" reason="async/await signatures (no body)" -->
```
fn async<T>(@T.0 -> @Future<T>) effects(<Async>)
fn await<T>(@Future<T>.0 -> @T) effects(<Async>)
```

**Example:**

```
private fn compute(@Nat, @Nat -> @Int)
  requires(true)
  ensures(true)
  effects(<Async>)
{
  let @Future<Int> = async(@Nat.1 * 2);
  let @Future<Int> = async(@Nat.0 * 3);
  await(@Future<Int>.0) + await(@Future<Int>.1)
}
```

![The async model: async(e) evaluates concurrently when e's effect row is commutative — Http requests issue on a host worker thread at the async point and await blocks for the response — while every other shape evaluates eagerly with a W002 warning; Future of T is WASM-transparent either way.](../assets/diagrams/async-model.svg)

Key design points:
- `async(expr)` evaluates `expr` and wraps the result in `Future<T>`.
- `await(@Future<T>.n)` unwraps the future, yielding the result of type `T`.
- The `<Async>` effect must be declared, making concurrency explicit and trackable.
- `Async` is a marker effect with no operations — `async` and `await` are built-in generic functions that require `effects(<Async>)`.
- `Future<T>` is WASM-transparent: an eagerly-evaluated future has the same runtime representation as `T`, with no overhead.  (A concurrently-evaluated future is an opaque pending handle with the same WASM value type; `await` resolves it.)
- **Concurrency (#841):** an implementation MAY evaluate `async(e)` concurrently when `e`'s effect row is commutative — value semantics are unchanged, and all other effects retain program order.  The reference implementation evaluates `async(Http.get(...))` and `async(Http.post(...))` (with call-free argument expressions) concurrently: the request is issued on a host worker thread at the `async(...)` point (so request *issuance* keeps program order), and `await` blocks for the response.  Every other shape evaluates eagerly (sequential execution); the checker warns (`W002`) when the argument's effect row is not within the commutative whitelist (`{Http, Async}`), documenting exactly where eager evaluation is semantically forced rather than merely unoptimized.
- The concurrent lowering keys the `await` handle-check on the type `Future<Result<String, String>>`, covering slots, parameters, direct compositions, and calls (bare, imported, or module-qualified) whose declared return is that type — with type aliases resolved transitively, here as everywhere else ([#1109](https://github.com/aallan/vera/issues/1109)).  An **indirectly-called closure** (`await(apply_fn(closure, …))`) returning this future type is classified by the closure's *declared* return type — a fn-typed slot resolved through its `FnType` alias, following the alias chain **transitively** to the terminal `FnType` (`type Fetcher = Inner;` where `Inner` aliases the fn type, [#867](https://github.com/aallan/vera/issues/867)) and substituting each generic alias's type params (so `Producer<Future<Result<String, String>>>` classifies), or an inline closure literal — so the await lowers correctly ([#843](https://github.com/aallan/vera/issues/843)).  A closure whose declared return type is not statically resolvable falls back to the identity lowering, with a loud backstop: a closure *argument produced by a nested call* (`apply_fn(make_fn(), …)`) is rejected by the `apply_fn` translation with `[E616]` (the function is skipped), so no fused wrapper is silently read as the ADT.
- The browser runtime evaluates all futures eagerly — spec-conformant under the MAY above: only the evaluation strategy differs, the underlying value is preserved whenever the two hosts' results are comparable, and any difference that remains comes from the `Http` outcome underneath rather than from `async` itself (documented in §12).
- True multi-await suspension and custom scheduling strategies (thread pool, event loop) via `handle[Async]` handlers remain future work ([#406](https://github.com/aallan/vera/issues/406), [#270](https://github.com/aallan/vera/issues/270)).
- This avoids coloured-function problems because algebraic effects already separate the description of an operation from its execution.

### 9.5.5 Inference

The `Inference` effect models LLM calls as algebraic effects, making them explicit in the type system and contract-verifiable. Functions that call language models must declare `effects(<Inference>)`; pure functions cannot secretly call models.

| Operation | Signature | Description |
|-----------|-----------|-------------|
| `Inference.complete` | `String -> Result<String, String>` | Send a prompt to the configured LLM provider; returns `Ok(completion)` or `Err(message)` |

`Inference` is a built-in effect — no `effect Inference { ... }` declaration is needed in source files (and one is `E152`).

```vera
private fn classify(@String -> @Result<String, String>)
  requires(string_length(@String.0) > 0)
  ensures(true)
  effects(<Inference>)
{
  let @String = string_concat("Classify as Spam or Ham: ", @String.0);
  Inference.complete(@String.0)
}
```

**Effect composition:** `effects(<Inference, IO>)` for LLM + console output; `effects(<Http, Inference>)` for fetching + LLM.

**Runtime:** In the reference implementation, `Inference` is host-backed — the runtime dispatches to the provider specified by environment variable:

| Variable | Purpose |
|----------|---------|
| `VERA_ANTHROPIC_API_KEY` | Anthropic API key (Claude models) |
| `VERA_OPENAI_API_KEY` | OpenAI API key (GPT models) |
| `VERA_MOONSHOT_API_KEY` | Kimi (Moonshot) API key — developer portal at [platform.kimi.ai](https://platform.kimi.ai) |
| `VERA_MISTRAL_API_KEY` | Mistral AI API key |
| `VERA_XAI_API_KEY` | xAI (Grok) API key |
| `VERA_DEEPSEEK_API_KEY` | DeepSeek API key |
| `VERA_INFERENCE_PROVIDER` | Force a provider (`anthropic`, `openai`, `moonshot`, `mistral`, `xai`, `deepseek`).  When unset, the provider is the **first** of those whose key is set to a non-empty value, in that order — so several keys at once resolve to the earliest rather than to the one most recently exported.  Every provider-backed `Err` names the **selected** provider and model associated with the request — including the failures raised before any response arrives, such as a DNS or timeout failure, where no provider answered at all — so a run can always be attributed (the browser `Err` below reaches no provider to name) |
| `VERA_INFERENCE_MODEL` | Override the model.  Each provider's default is its flagship general-chat model: `claude-opus-5`, `gpt-5.6-sol`, `kimi-k3`, `mistral-large-latest`, `grok-4.6`, `deepseek-v4-pro`.  A cheaper tier is reached by setting this variable |

**Browser:** the browser runtime binds `Inference.complete` but never calls a provider — every invocation returns an explanatory `Err`, so a program compiled with `<Inference>` still loads and runs in the browser and handles the refusal through the same `Result` it already matches on. Embedding API keys in client-side JavaScript would expose them in page source and network traffic; route inference through a server-side proxy called with the `Http` effect.

**Error text from the provider.** When a provider rejects a request, its own message is surfaced in the `Err` rather than only the HTTP status line. That text — and every other provider-supplied fragment an `Err` quotes, including a response body that is not JSON, a `stop_reason` or `finish_reason`, a refusal, and the key and type names a shape report lists — is bounded and **redacted**: the configured API key and any credential-shaped token — `sk-`, `sk_`, `key-`, `key_`, `token-`, `token_`, `xai-` or `xai_` followed by eight or more of `[A-Za-z0-9_-]` — are replaced with `[redacted]`. The configured key is matched literally and unconditionally: there is no minimum length, so a very short key also redacts incidental occurrences of its characters. That is deliberate — a length floor would stop redacting short real tokens, which gateways and proxies do issue, and redaction never trades coverage for tidiness. The prefix pattern cannot cover every provider either: a key with no recognisable prefix, such as Mistral's bare alphanumeric form, is matched only by the configured-key rule, which is why the two rules exist together. Providers quote the key they rejected (`Incorrect API key provided: sk-…`), and an `Err` is an ordinary Vera value that a program may print, log, or send onward.

**Accepted response shapes.** On the Anthropic branch the completion is every `content` block whose `type` is `"text"`, joined in order. On the OpenAI-compatible branch it is `message.content` when that is a string; when it is a list, the parts are taken by discriminator in PREFERENCE order — every `"text"` part joined in order if any yields text, and otherwise every `"output_text"` part. The two are never merged, and parts under the discriminator not selected are neither joined nor validated: a gateway mirroring one reply under both spellings must not have it returned twice. A block or part **of the selected type** that carries no `text` field, or whose `text` is not a string, is an error rather than a value to coerce. Blocks and parts of any other type — `thinking`, `tool_use`, `reasoning` — are skipped, not errors. If that leaves NO block or part of the selected type at all — a `content` of only `thinking` blocks, a parts list with neither `text` nor `output_text`, an empty list — the response is an `Err` naming the block or part types that were present and, when the provider sent one, its `stop_reason` or `finish_reason`. That is distinct from a selected block that IS present but empty, which is `Ok("")` unless the turn was refused or truncated. `message.refusal` is surfaced when the model declined — including when the content beside it is empty, where returning the empty completion would discard the reason. An empty or whitespace-only completion is an error whenever the provider itself explained it: on the Anthropic branch when `stop_reason` is `refusal` or `max_tokens`, and on the OpenAI-compatible branch when `message.refusal` is present or `finish_reason` is `length`. The reason is matched case-insensitively, so a gateway normalising it to `MAX_TOKENS` is treated the same as `max_tokens`, while the diagnostic carries the token exactly as received — `stop_reason=refusal`, `finish_reason=length` — so a caller can tell a declined request from a truncated one and can see what the provider actually sent. Under any other reason, or none at all, an empty completion remains `Ok("")`: a model may legitimately answer with nothing. A NON-empty reply is returned unchanged whatever the reason, truncated output still being the model's answer.

**Limitations in this release:**
- `complete` only — `embed` (returning `Array<Float64>`) is deferred ([#371](https://github.com/aallan/vera/issues/371))
- No streaming — full response only
- No system prompt — single `complete(user_prompt)` call; structured prompting via `string_concat`
- User-defined `handle[Inference]` handlers (for mocking, local models, replay) are planned for a future release ([#372](https://github.com/aallan/vera/issues/372))

### 9.5.6 HttpServer

The `HttpServer` effect (a marker, §7.7.5 — no operations) enables **verified HTTP request handling** (#305, since v0.0.193).  A server program defines a total, contract-checked handler:

```vera
public fn handle(@Request -> @Response)
  requires(true)
  ensures(true)
  effects(<HttpServer>)
{
  match @Request.0 {
    Request(@String, @String, @Map<String, String>, @String) ->
      Response(200, map_new(), @String.0)
  }
}
```

**Built-in types** (prelude ADTs, injected when referenced; user definitions shadow them):

<!-- vera:skip-check category="ILLUSTRATIVE" reason="prelude-injected Request/Response decls shown without visibility (#305)" -->
```
data Request { Request(String, String, Map<String, String>, String) }
data Response { Response(Int, Map<String, String>, String) }
```

`Request` fields are method, path, headers, body; `Response` fields are status, headers, body.

**Execution model.**  `vera serve prog.vera [--port N]` hosts the accept loop: each incoming request is marshalled into a `Request` value, the handler is called on a **fresh module instance** (per-request isolation — `State<T>` mutations cannot leak between requests), and the returned `Response` becomes the HTTP response.  Because the loop lives in the host, handlers are ordinary total functions — no `Diverge`, and every contract on the handler (or its helpers) is an ordinary Tier-1/Tier-3 obligation.  A runtime contract violation (or any trap) inside a handler answers **500** with the trap diagnostic in a JSON body; the connection is always answered.

![The vera serve request lifecycle: the host owns the accept loop, marshals each request into a Request value, calls the contract-checked handler on a fresh module instance, and turns the returned Response into the HTTP response — traps answer 500 with the diagnostic.](../assets/diagrams/httpserver-lifecycle.svg)

- Routing is ordinary pattern matching on the request fields.
- Per-request effects compose in the row: `effects(<HttpServer, State<Int>>)`.
- Request handling is sequential in v1; concurrent handling is future work (#406).
- Native-only: the serve driver is part of the reference (wasmtime) runtime; the browser runtime does not serve HTTP (documented divergence, §12).

### 9.5.7 DB

The `DB` effect (a built-in, §7.7.7) executes SQL through the host (#229, since v0.1.7). `execute` runs writes and returns the affected-row count; `query` runs reads and returns a grid of cells:

```vera
public fn seed_and_count(-> @Int)
  requires(true)
  ensures(true)
  effects(<DB>)
{
  match DB.execute("CREATE TABLE users (id INTEGER PRIMARY KEY, name TEXT, nickname TEXT)", []) {
    Err(@String) -> -1,
    Ok(@Int) -> match DB.execute("INSERT INTO users (name, nickname) VALUES (?, ?)", [Some("Ada"), None]) {
      Err(@String) -> -1,
      Ok(@Int) -> match DB.query("SELECT name, nickname FROM users", []) {
        Err(@String) -> -1,
        Ok(@Array<Array<Option<String>>>) -> array_length(@Array<Array<Option<String>>>.0)
      }
    }
  }
}
```

**Row and parameter marshalling.**  A query result is an `Array<Array<Option<String>>>`: the outer array is the rows, each row is an array of cells, and each cell is an `Option<String>`.  A cell that is SQL `NULL` marshals to `None`; a present value marshals to `Some(text)`.  `NULL` and the empty string `""` therefore stay distinct — the effect never collapses one into the other (DESIGN principle 2, no implicit behaviour).  A `NOT NULL` column is read with `option_unwrap_or(cell, "")`, or matched explicitly when the caller must handle absence.

Parameters travel the same shape one level down: the `Array<Option<String>>` second argument binds positionally to the `?` placeholders — `Some(v)` for a value, `None` for `NULL`.  All values cross the host boundary as UTF-8 strings; a non-text SQLite column is rendered to its text form on the way out.

**SQL literal provenance (injection prevention).**  The SQL argument of `query` / `execute` must be *literal-provenance*: a string literal, a `string_concat` of literals, or a `let` chain of those.  A SQL string that embeds a runtime value — a function result, a parameter, or a `\(expr)` interpolation of one — is the SQL injection vector, so Vera rejects it at **compile time** (`E207`); an interpolation, concatenation, or `let`-bound slot whose embedded expressions are themselves literals stays literal-provenance and is accepted.  Runtime data reaches the query only through the `?` placeholders and the params array.  The guarantee is a deterministic type error, not an SMT obligation — it needs no solver and holds even inside handled code where solver-based claims cannot reach.  When both the SQL and the params array are statically sized, a placeholder/parameter count mismatch is also a compile-time error (`E208`); a dynamically-sized params array defers that arity check to the driver at run time.  Only anonymous `?` placeholders are supported: because parameters bind positionally through the `Array<Option<String>>` argument, a numbered (`?NNN`) or named (`:name` / `@name` / `$name`) placeholder has no well-defined binding and is a compile-time error (`E209`).  The gate keys on the call reaching the host database — the `DB.query` / `DB.execute` spelling codegen routes to the host — rather than on the identity of the resolved operation, so no runtime SQL slips through an unusual declaration; an imported library body carrying a non-literal query is rejected on the compile path as well. A program cannot redeclare `effect DB` at all (`E152`, Section 9.5.1), so that route is closed twice over.

- **Failure is a value.**  Both operations return `Result<_, String>`; a driver error is the `Err(msg)` arm, never a trap, so a database call is checked like any other `Result`.
- **Connection.**  `VERA_DB_URL` selects the database — `sqlite::memory:` by default, or `sqlite:///path/to/file.db` for a file.  One connection is used per program run.
- **Portability.**  Native only: the browser runtime returns `Err` for every `DB` operation (documented divergence, §12), and `vera compile --target wasi-p2` rejects a program that uses `<DB>`.

## 9.6 Built-in Functions

Built-in functions are always in scope as the single canonical definition of each operation. A user or module function whose name matches a built-in is a compile error (**E151**): there is one canonical form, so a second definition is redundant, and for the verifier-modelled built-ins it is silently unsound — the verifier would reason with the built-in's idealized model while code generation runs the user's body, letting a postcondition be *proved* against the built-in yet *violated at runtime*. Call the built-in directly (no import is needed) or choose a distinct name for genuinely different behaviour. The Option/Result/Json/Html combinators listed in the standard prelude (Section 9.1.2) are the exception: they are ordinary Vera functions the prelude injects, so a same-named user definition soundly replaces them.

### 9.6.1 array\_length

<!-- vera:skip-parse category="FRAGMENT" reason="array_length signature (no body)" -->
```
public forall<T> fn array_length(@Array<T> -> @Int)
  requires(true)
  ensures(@Int.result >= 0)
  effects(pure)
```

Returns the number of elements in an array. The result is always non-negative. `array_length` is generic over the element type.

```
let @Array<Int> = [10, 20, 30];
array_length(@Array<Int>.0)
```

This expression evaluates to `3`.

For the compilation of `array_length`, see Chapter 11, Section 11.12.

### 9.6.2 array\_append

<!-- vera:skip-parse category="FRAGMENT" reason="array_append signature (no body)" -->
```
public forall<T> fn array_append(@Array<T>, @T -> @Array<T>)
  requires(true)
  ensures(true)
  effects(pure)
```

Returns a new array with the element appended at the end. The returned array has length `array_length(input) + 1`, with the new element at the last index. The original array is unchanged (arrays are immutable values). `array_append` is generic over the element type.

```
let @Array<Int> = array_append([10, 20, 30], 40);
array_length(@Array<Int>.0)
```

This expression evaluates to `4`.

### 9.6.3 array\_range

<!-- vera:skip-parse category="FRAGMENT" reason="array_range signature (no body)" -->
```vera
public fn array_range(@Int, @Int -> @Array<Int>)
  requires(true)
  ensures(true)
  effects(pure)
```

Produces an array of integers over the half-open interval `[start, end)`. The first argument is the start (inclusive) and the second is the end (exclusive). If `start >= end`, the result is an empty array. The elements are consecutive integers from `start` to `end - 1`.

```vera
array_range(0, 5)       -- [0, 1, 2, 3, 4]
array_range(3, 7)       -- [3, 4, 5, 6]
array_range(5, 5)       -- [] (empty, start == end)
array_range(10, 3)      -- [] (empty, start > end)
```

### 9.6.4 array\_concat

<!-- vera:skip-parse category="FRAGMENT" reason="array_concat signature (no body)" -->
```vera
public forall<T> fn array_concat(@Array<T>, @Array<T> -> @Array<T>)
  requires(true)
  ensures(true)
  effects(pure)
```

Merges two arrays into a single array. The elements of the first array appear before the elements of the second. The result has length `array_length(first) + array_length(second)`. Both input arrays are unchanged (arrays are immutable values). `array_concat` is generic over the element type.

```vera
array_concat([1, 2, 3], [4, 5])       -- [1, 2, 3, 4, 5]
array_concat([], [1, 2])               -- [1, 2]
array_concat([1, 2], [])               -- [1, 2]
array_concat([], [])                   -- [] (empty)
```

### 9.6.5 array\_slice

<!-- vera:skip-parse category="FRAGMENT" reason="array_slice signature (no body)" -->
```vera
public forall<T> fn array_slice(@Array<T>, @Int, @Int -> @Array<T>)
  requires(true)
  ensures(true)
  effects(pure)
```

Returns a new array containing elements from index `start` (inclusive) to `end` (exclusive). Indices are clamped to `[0, array_length(input)]`, so out-of-range values produce shorter slices rather than traps. If `start >= end` after clamping, returns an empty array. The original array is unchanged.

```vera
array_slice([10, 20, 30, 40, 50], 1, 4)  -- [20, 30, 40]
array_slice([10, 20, 30], 0, 2)          -- [10, 20]
array_slice([10, 20, 30], 5, 10)         -- [] (clamped, empty)
array_slice([10, 20, 30], 2, 1)          -- [] (start >= end)
```

### 9.6.6 array\_map

<!-- vera:skip-parse category="FRAGMENT" reason="array_map signature (no body)" -->
```vera
public forall<A, B> fn array_map(@Array<A>, fn(A -> B) effects(pure) -> @Array<B>)
  requires(true)
  ensures(true)
  effects(pure)
```

Applies a function to each element of the array and returns a new array of the results. The result has the same length as the input. The element type may change (e.g. mapping `Int` to `String`).

```vera
array_map([1, 2, 3], fn(@Int -> @Int) effects(pure) { @Int.0 * 10 })
-- [10, 20, 30]
```

### 9.6.7 array\_filter

<!-- vera:skip-parse category="FRAGMENT" reason="array_filter signature (no body)" -->
```vera
public forall<T> fn array_filter(@Array<T>, fn(T -> Bool) effects(pure) -> @Array<T>)
  requires(true)
  ensures(true)
  effects(pure)
```

Returns a new array containing only the elements for which the predicate returns `true`. The result length is between 0 and the input length. Element order is preserved.

```vera
array_filter([1, 2, 3, 4, 5, 6], fn(@Int -> @Bool) effects(pure) { @Int.0 > 3 })
-- [4, 5, 6]
```

### 9.6.8 array\_fold

<!-- vera:skip-parse category="FRAGMENT" reason="array_fold signature (no body)" -->
```vera
public forall<T, U> fn array_fold(@Array<T>, @U, fn(U, T -> U) effects(pure) -> @U)
  requires(true)
  ensures(true)
  effects(pure)
```

Reduces an array to a single value by applying a function to an accumulator and each element, left to right. The second argument is the initial accumulator value. The accumulator type may differ from the element type.

```vera
array_fold([1, 2, 3, 4], 0, fn(@Int, @Int -> @Int) effects(pure) { @Int.1 + @Int.0 })
-- 10 (0 + 1 + 2 + 3 + 4)
```

### 9.6.9 Numeric Operations

Vera provides eight built-in numeric functions for common mathematical operations. The integer functions (`abs`, `min`, `max`) operate on `Int` values and are pure — they perform no effects and are fully verifiable by the SMT solver (Tier 1). The floating-point functions (`floor`, `ceil`, `round`, `sqrt`, `pow`) use IEEE 754 semantics via WebAssembly's native instructions.

#### abs

<!-- vera:skip-parse category="FRAGMENT" reason="abs signature (no body)" -->
```
public fn abs(@Int -> @Nat)
  requires(true)
  ensures(@Nat.result >= 0)
  effects(pure)
```

Returns the absolute value of an integer. The result type is `Nat` because absolute values are always non-negative. Both `Nat` and `Int` are `i64` at the WASM level, so this involves no runtime conversion.

```
abs(-42)
```

This expression evaluates to `42`.

#### min

<!-- vera:skip-parse category="FRAGMENT" reason="min signature (no body)" -->
```
public fn min(@Int, @Int -> @Int)
  requires(true)
  ensures(@Int.result <= @Int.0 && @Int.result <= @Int.1)
  effects(pure)
```

Returns the smaller of two integers.

```
min(3, 7)
```

This expression evaluates to `3`.

#### max

<!-- vera:skip-parse category="FRAGMENT" reason="max signature (no body)" -->
```
public fn max(@Int, @Int -> @Int)
  requires(true)
  ensures(@Int.result >= @Int.0 && @Int.result >= @Int.1)
  effects(pure)
```

Returns the larger of two integers.

```
max(3, 7)
```

This expression evaluates to `7`.

#### floor

<!-- vera:skip-parse category="FRAGMENT" reason="floor signature (no body)" -->
```
public fn floor(@Float64 -> @Int)
  requires(true)
  ensures(true)
  effects(pure)
```

Returns the largest integer less than or equal to the input. Compiles to `f64.floor` followed by `i64.trunc_f64_s`. Traps on NaN or out-of-range values (WASM semantics).

```
floor(3.7)
```

This expression evaluates to `3`.

#### ceil

<!-- vera:skip-parse category="FRAGMENT" reason="ceil signature (no body)" -->
```
public fn ceil(@Float64 -> @Int)
  requires(true)
  ensures(true)
  effects(pure)
```

Returns the smallest integer greater than or equal to the input. Compiles to `f64.ceil` followed by `i64.trunc_f64_s`. Traps on NaN or out-of-range values (WASM semantics).

```
ceil(3.2)
```

This expression evaluates to `4`.

#### round

<!-- vera:skip-parse category="FRAGMENT" reason="round signature (no body)" -->
```
public fn round(@Float64 -> @Int)
  requires(true)
  ensures(true)
  effects(pure)
```

Rounds to the nearest integer using banker's rounding (IEEE 754 roundTiesToEven). This means `round(2.5)` evaluates to `2`, not `3` — ties round to the nearest even integer. Compiles to `f64.nearest` followed by `i64.trunc_f64_s`. Traps on NaN or out-of-range values (WASM semantics).

```
round(3.7)
```

This expression evaluates to `4`.

#### sqrt

<!-- vera:skip-parse category="FRAGMENT" reason="sqrt signature (no body)" -->
```
public fn sqrt(@Float64 -> @Float64)
  requires(true)
  ensures(true)
  effects(pure)
```

Returns the square root of a floating-point number. Compiles directly to the WASM `f64.sqrt` instruction.

```
sqrt(4.0)
```

This expression evaluates to `2.0`.

#### pow

<!-- vera:skip-parse category="FRAGMENT" reason="pow signature (no body)" -->
```
public fn pow(@Float64, @Int -> @Float64)
  requires(true)
  ensures(true)
  effects(pure)
```

Raises a floating-point base to an integer exponent. The exponent is `Int`, not `Float64` — this avoids silent truncation of fractional exponents. Negative exponents produce reciprocals (`pow(2.0, -1)` evaluates to `0.5`). Implemented via exponentiation by squaring for efficiency.

```
pow(2.0, 10)
```

This expression evaluates to `1024.0`.

### 9.6.10 Logarithmic, Trigonometric, and Numeric Utility Functions

Fifteen additional math functions cover common scientific computing needs: three logarithms, seven trigonometric functions, two constants, and three numeric utilities. All are pure and (where applicable) defer to IEEE 754 semantics — returning `NaN` for out-of-domain inputs (`log(-1.0)`, `asin(2.0)`) and `±Infinity` for overflow. The logarithms' zero pole is not a domain error: `log(0.0)`, `log2(0.0)`, and `log10(0.0)` (including `-0.0`) return `-Infinity`, matching IEEE 754 and JS `Math.log` in both runtimes (#790).

Most log and trig functions are uninterpreted in Z3's real-arithmetic fragment, so contracts that depend on their specific values fall to Tier 3 (runtime check). Call-site type checking and effect inference still apply.

| Function | Signature | Description |
|---|---|---|
| `log` | `Float64 -> Float64` | Natural logarithm (base *e*) |
| `log2` | `Float64 -> Float64` | Base-2 logarithm |
| `log10` | `Float64 -> Float64` | Base-10 logarithm |
| `sin` | `Float64 -> Float64` | Sine (radians) |
| `cos` | `Float64 -> Float64` | Cosine (radians) |
| `tan` | `Float64 -> Float64` | Tangent (radians) |
| `asin` | `Float64 -> Float64` | Inverse sine, returns `[-π/2, π/2]` |
| `acos` | `Float64 -> Float64` | Inverse cosine, returns `[0, π]` |
| `atan` | `Float64 -> Float64` | Inverse tangent, returns `(-π/2, π/2)` |
| `atan2` | `Float64, Float64 -> Float64` | Quadrant-correct angle from `(y, x)` — returns `[-π, π]` |
| `pi` | `() -> Float64` | `3.141592653589793` |
| `e` | `() -> Float64` | `2.718281828459045` |
| `sign` | `Int -> Int` | `-1` for negative, `0` for zero, `1` for positive |
| `clamp` | `Int, Int, Int -> Int` | `clamp(v, lo, hi)` restricts `v` to `[lo, hi]` |
| `float_clamp` | `Float64, Float64, Float64 -> Float64` | Float64 variant of `clamp` |

The argument order for `atan2` is `(y, x)`, matching POSIX, Python's `math.atan2`, and JavaScript's `Math.atan2` — `atan2(1.0, 1.0)` is `π/4`, `atan2(1.0, -1.0)` is `3π/4`.

```vera
let @Float64 = log(e())          -- evaluates to 1.0
let @Float64 = atan2(1.0, 1.0)   -- evaluates to π/4 ≈ 0.785
let @Int = sign(-42)              -- evaluates to -1
let @Int = clamp(15, 0, 10)       -- evaluates to 10
```

Clamp is defined as `min(max(v, lo), hi)`; when `lo > hi` the outer `min` dominates and the result equals `hi`. This is intentional — callers with strict ordering expectations should pre-check their bounds.

### 9.6.11 Type Conversions

Vera has no implicit numeric conversions. The following built-in functions provide explicit conversions between numeric types.

#### Widening conversions (always succeed)

<!-- vera:skip-parse category="FRAGMENT" reason="int_to_float signature (no body)" -->
```
public fn int_to_float(@Int -> @Float64)
  requires(true)
  ensures(true)
  effects(pure)
```

Converts an integer to a floating-point number. Compiled to `f64.convert_i64_s`.

```
int_to_float(42)
```

This expression evaluates to `42.0`.

<!-- vera:skip-parse category="FRAGMENT" reason="nat_to_int signature (no body)" -->
```
public fn nat_to_int(@Nat -> @Int)
  requires(true)
  ensures(@Int.result >= 0)
  effects(pure)
```

Converts a natural number to a signed integer. This is a no-op at runtime — both types share the same representation (i64). The postcondition captures the invariant that the result is non-negative.

```
nat_to_int(abs(42))
```

This expression evaluates to `42`.

<!-- vera:skip-parse category="FRAGMENT" reason="byte_to_int signature (no body)" -->
```
public fn byte_to_int(@Byte -> @Int)
  requires(true)
  ensures(@Int.result >= 0)
  effects(pure)
```

Converts a byte (0–255) to a signed integer. Compiled to `i64.extend_i32_u` (unsigned zero-extension from i32 to i64).

```
byte_to_int(@Byte.0)
```

#### Narrowing conversions (may fail)

<!-- vera:skip-parse category="FRAGMENT" reason="float_to_int signature (no body)" -->
```
public fn float_to_int(@Float64 -> @Int)
  requires(true)
  ensures(true)
  effects(pure)
```

Truncates a floating-point number toward zero. Traps on NaN or Infinity (consistent with `floor`, `ceil`, and `round`). Compiled to `i64.trunc_f64_s`.

```
float_to_int(3.9)
```

This expression evaluates to `3` (truncation toward zero, not rounding).

<!-- vera:skip-parse category="FRAGMENT" reason="int_to_nat signature (no body)" -->
```
public fn int_to_nat(@Int -> @Option<Nat>)
  requires(true)
  ensures(true)
  effects(pure)
```

Checked narrowing from signed integer to natural number. Returns `Some(n)` if the input is non-negative, `None` otherwise.

```
match int_to_nat(42) {
  Some(@Nat) -> @Nat.0,
  None -> 0 - 1
}
```

This expression evaluates to `42`.

<!-- vera:skip-parse category="FRAGMENT" reason="int_to_byte signature (no body)" -->
```
public fn int_to_byte(@Int -> @Option<Byte>)
  requires(true)
  ensures(true)
  effects(pure)
```

Checked narrowing from signed integer to byte. Returns `Some(b)` if the input is in the range 0–255, `None` otherwise.

```
match int_to_byte(65) {
  Some(@Byte) -> byte_to_int(@Byte.0),
  None -> 0 - 1
}
```

This expression evaluates to `65`.

#### float_to_string (total over all Float64 values)

<!-- vera:skip-parse category="FRAGMENT" reason="float_to_string signature (no body)" -->
```
public fn float_to_string(@Float64 -> @String)
  requires(true)
  ensures(true)
  effects(pure)
```

Renders a `Float64` as its decimal string (up to six fractional digits, trailing zeros trimmed but at least one kept, so `42.0` stays `"42.0"`). This function is **total**: it is defined for every `Float64` value, including the three IEEE 754 non-finite classes, which render as fixed ASCII spellings:

| Input | Output |
|-------|--------|
| `NaN` (e.g. `nan()`, `log(-1.0)`) | `"nan"` |
| `+∞` (e.g. `infinity()`) | `"inf"` |
| `-∞` (e.g. `log(0.0)`, `0.0 - infinity()`) | `"-inf"` |

These spellings are chosen for cross-runtime parity: `float_to_string` compiles to inline WASM (no host import), so the Python host runtime and the browser runtime execute the same module and emit these bytes identically by construction. Because the math built-ins commit to IEEE 754 semantics — `log(0.0)` returns `-∞` and out-of-domain inputs return `NaN` (§9.6.10) — these are ordinary, reachable values, not errors; rendering them never traps ([#857](https://github.com/aallan/vera/issues/857)).

```
float_to_string(log(0.0))
```

This expression evaluates to `"-inf"`.

### 9.6.12 Float64 Predicates

Vera provides built-in functions for testing and constructing IEEE 754 special float values (NaN and infinity).

#### Predicates

<!-- vera:skip-parse category="FRAGMENT" reason="float_is_nan signature (no body)" -->
```
public fn float_is_nan(@Float64 -> @Bool)
  requires(true)
  ensures(true)
  effects(pure)
```

Tests whether a Float64 value is NaN (not a number). NaN is the only value that is not equal to itself. Compiled to `f64.ne(x, x)`.

```vera
public fn test_is_nan(@Unit -> @Int)
  requires(true) ensures(true) effects(pure)
{ if float_is_nan(nan()) then { 1 } else { 0 } }
```

This expression evaluates to `1`.

<!-- vera:skip-parse category="FRAGMENT" reason="float_is_infinite signature (no body)" -->
```
public fn float_is_infinite(@Float64 -> @Bool)
  requires(true)
  ensures(true)
  effects(pure)
```

Tests whether a Float64 value is positive or negative infinity. Compiled to `f64.eq(f64.abs(x), inf)`. Returns `false` for NaN.

```vera
public fn test_is_infinite(@Unit -> @Int)
  requires(true) ensures(true) effects(pure)
{ if float_is_infinite(infinity()) then { 1 } else { 0 } }
```

This expression evaluates to `1`.

#### Constants

<!-- vera:skip-parse category="FRAGMENT" reason="nan signature (no body)" -->
```
public fn nan(-> @Float64)
  requires(true)
  ensures(true)
  effects(pure)
```

Returns a quiet NaN value. Compiled to `f64.const nan`.

```vera
public fn test_nan(@Unit -> @Float64)
  requires(true) ensures(true) effects(pure)
{ nan() }
```

<!-- vera:skip-parse category="FRAGMENT" reason="infinity signature (no body)" -->
```vera
public fn infinity(-> @Float64)
  requires(true)
  ensures(true)
  effects(pure)
```

Returns positive infinity. Negative infinity can be obtained via `0.0 - infinity()`. Compiled to `f64.const inf`.

```vera
public fn test_infinity(@Unit -> @Float64)
  requires(true) ensures(true) effects(pure)
{ infinity() }
```

### 9.6.13 String Search

String search functions test for the presence or position of substrings. All are pure, take `String` arguments, and operate on raw bytes (ASCII). All are Tier 3 for verification (String is not modeled in Z3).

#### string_contains

<!-- vera:skip-parse category="FRAGMENT" reason="string_contains signature (no body)" -->
```vera
public fn string_contains(@String, @String -> @Bool)
  requires(true) ensures(true) effects(pure)
```

Returns `true` if the second argument (needle) appears as a contiguous substring of the first (haystack). An empty needle always matches. Uses a naive O(n×m) byte comparison.

```vera
string_contains("hello world", "world")  -- true
string_contains("hello", "xyz")          -- false
string_contains("hello", "")             -- true
```

#### string_starts_with

<!-- vera:skip-parse category="FRAGMENT" reason="string_starts_with signature (no body)" -->
```vera
public fn string_starts_with(@String, @String -> @Bool)
  requires(true) ensures(true) effects(pure)
```

Returns `true` if the haystack begins with the given prefix. An empty prefix always matches. If the prefix is longer than the haystack, returns `false`.

```vera
string_starts_with("hello world", "hello")  -- true
string_starts_with("hello", "world")        -- false
string_starts_with("hello", "")             -- true
```

#### string_ends_with

<!-- vera:skip-parse category="FRAGMENT" reason="string_ends_with signature (no body)" -->
```vera
public fn string_ends_with(@String, @String -> @Bool)
  requires(true) ensures(true) effects(pure)
```

Returns `true` if the haystack ends with the given suffix. An empty suffix always matches. If the suffix is longer than the haystack, returns `false`.

```vera
string_ends_with("hello world", "world")  -- true
string_ends_with("hello", "world")        -- false
string_ends_with("hello", "")             -- true
```

#### string_index_of

<!-- vera:skip-parse category="FRAGMENT" reason="string_index_of signature (no body)" -->
```vera
public fn string_index_of(@String, @String -> @Option<Nat>)
  requires(true) ensures(true) effects(pure)
```

Returns `Some(i)` where `i` is the byte offset of the first occurrence of the needle in the haystack, or `None` if not found. An empty needle matches at position 0. The returned index is a `Nat` (natural number).

```vera
match string_index_of("hello world", "world") {
  Some(@Nat) -> @Nat.0,
  None -> 0 - 1
}
-- evaluates to 6
```

### 9.6.14 String Transformation

String transformation functions produce new strings by modifying characters or structure. All allocate heap memory for the result and register it with the GC shadow stack. All are pure and Tier 3.

#### string\_strip

<!-- vera:skip-parse category="FRAGMENT" reason="string_strip signature (no body)" -->
```
public fn string_strip(@String -> @String)
  requires(true) ensures(true) effects(pure)
```

Returns a new string with leading and trailing ASCII whitespace removed. Whitespace bytes are: space (32), tab (9), carriage return (13), and newline (10). Interior whitespace is preserved.

```vera
string_strip("  hello  ")   -- "hello"
string_strip("\thello\n")    -- "hello"
string_strip("hello")        -- "hello" (no change)
string_strip("  ")           -- "" (empty)
```

#### string\_char\_code

<!-- vera:skip-parse category="FRAGMENT" reason="string_char_code signature (no body)" -->
```
public fn string_char_code(@String, @Int -> @Nat)
  requires(true) ensures(true) effects(pure)
```

Returns the ASCII code point (as a `Nat`) of the byte at the given index in the string. The index is zero-based. Traps if the index is out of bounds.

```vera
string_char_code("A", 0)     -- 65
string_char_code("hello", 1) -- 101 (ASCII 'e')
string_char_code("ABC", 2)   -- 67 (ASCII 'C')
```

#### string_upper

<!-- vera:skip-parse category="FRAGMENT" reason="string_upper signature (no body)" -->
```vera
public fn string_upper(@String -> @String)
  requires(true) ensures(true) effects(pure)
```

Returns a new string with all ASCII lowercase letters (a–z, bytes 97–122) converted to uppercase (A–Z, bytes 65–90). Non-ASCII bytes and non-letter bytes are unchanged.

```vera
string_upper("hello")   -- "HELLO"
string_upper("Hello!")   -- "HELLO!"
string_upper("123")      -- "123"
```

#### string_lower

<!-- vera:skip-parse category="FRAGMENT" reason="string_lower signature (no body)" -->
```vera
public fn string_lower(@String -> @String)
  requires(true) ensures(true) effects(pure)
```

Returns a new string with all ASCII uppercase letters (A–Z, bytes 65–90) converted to lowercase (a–z, bytes 97–122). Non-ASCII bytes and non-letter bytes are unchanged.

```vera
string_lower("HELLO")   -- "hello"
string_lower("Hello!")   -- "hello!"
string_lower("123")      -- "123"
```

#### string_replace

<!-- vera:skip-parse category="FRAGMENT" reason="string_replace signature (no body)" -->
```vera
public fn string_replace(@String, @String, @String -> @String)
  requires(true) ensures(true) effects(pure)
```

Replaces all non-overlapping occurrences of the needle (second argument) in the haystack (first argument) with the replacement (third argument). If the needle is empty, returns a copy of the haystack. Uses a two-pass algorithm: pass 1 counts occurrences, then allocates the output buffer; pass 2 copies bytes with substitutions.

```vera
string_replace("hello world", "world", "vera")  -- "hello vera"
string_replace("aaa", "a", "bb")                -- "bbbbbb"
string_replace("hello", "xyz", "abc")           -- "hello"
string_replace("hello", "", "x")                -- "hello"
```

#### string_split

<!-- vera:skip-parse category="FRAGMENT" reason="string_split signature (no body)" -->
```vera
public fn string_split(@String, @String -> @Array<String>)
  requires(true) ensures(true) effects(pure)
```

Splits the string at each non-overlapping occurrence of the delimiter, returning an `Array<String>`. If the delimiter is empty, returns a single-element array containing the original string. Consecutive delimiters produce empty string segments. Uses a two-pass algorithm: pass 1 counts delimiters, then allocates the array and segment buffers in pass 2.

```vera
string_split("a,b,c", ",")     -- Array with 3 elements: "a", "b", "c"
string_split("hello", ",")     -- Array with 1 element: "hello"
string_split("a,,b", ",")      -- Array with 3 elements: "a", "", "b"
```

#### string_join

<!-- vera:skip-parse category="FRAGMENT" reason="string_join signature (no body)" -->
```vera
public fn string_join(@Array<String>, @String -> @String)
  requires(true) ensures(true) effects(pure)
```

Joins an array of strings with the given separator between each pair of elements. An empty array produces an empty string. Uses a two-pass algorithm: pass 1 sums the total length, pass 2 copies bytes.

```vera
string_join(string_split("a,b,c", ","), "-")  -- "a-b-c"
string_join(string_split("hello", ","), "-")  -- "hello"
```

#### string_from_char_code

<!-- vera:skip-parse category="FRAGMENT" reason="string_from_char_code signature (no body)" -->
```vera
public fn string_from_char_code(@Nat -> @String)
  requires(true) ensures(true) effects(pure)
```

Creates a single-character (1-byte) string from an ASCII code point. Inverse of `string_char_code`. Allocates 1 byte of heap memory for the result.

```vera
string_from_char_code(65)                        -- "A"
string_char_code(string_from_char_code(65), 0)          -- 65 (roundtrip)
string_concat(string_from_char_code(72), string_from_char_code(105))  -- "Hi"
```

#### string_repeat

<!-- vera:skip-parse category="FRAGMENT" reason="string_repeat signature (no body)" -->
```vera
public fn string_repeat(@String, @Nat -> @String)
  requires(true) ensures(true) effects(pure)
```

Repeats a string a given number of times. Allocates `length(s) × n` bytes of heap memory and fills the result by cycling through the source bytes.

```vera
string_repeat("ab", 3)                   -- "ababab"
string_repeat("x", 5)                    -- "xxxxx"
string_repeat("hello", 0)                -- "" (empty)
string_repeat("", 100)                   -- "" (empty)
```

### 9.6.15 Parsing Functions

Parsing functions convert strings to typed values, returning `Result<T, String>` to represent success or failure. All strip leading and trailing ASCII whitespace (spaces, tabs, `\r`, `\n`) before parsing. All are pure and Tier 3 for verification.

The `Result` type used by parsing functions is the standard ADT:

```vera
private data Result<T, E> { Ok(T), Err(E) }
```

On success, the `Ok` variant contains the parsed value. On failure, the `Err` variant contains a descriptive error message string.

#### parse_nat

<!-- vera:skip-parse category="FRAGMENT" reason="parse_nat signature (no body)" -->
```vera
public fn parse_nat(@String -> @Result<Nat, String>)
  requires(true) ensures(true) effects(pure)
```

Parses a non-negative integer from a string. After stripping whitespace, the remaining characters must all be ASCII digits (`0`–`9`). Leading zeros are permitted (e.g., `"007"` parses as `7`).

Error messages:
- `"empty string"` — the input is empty or contains only whitespace
- `"invalid digit"` — a non-digit character was encountered

```vera
parse_nat("42")        -- Ok(42)
parse_nat("  7  ")     -- Ok(7)   (whitespace stripped)
parse_nat("007")       -- Ok(7)   (leading zeros allowed)
parse_nat("abc")       -- Err("invalid digit")
parse_nat("")          -- Err("empty string")
parse_nat("  ")        -- Err("empty string")
```

#### parse_int

<!-- vera:skip-parse category="FRAGMENT" reason="parse_int signature (no body)" -->
```vera
public fn parse_int(@String -> @Result<Int, String>)
  requires(true) ensures(true) effects(pure)
```

Parses a signed integer from a string. After stripping whitespace, an optional leading `+` or `-` sign is consumed. The remaining characters must all be ASCII digits (`0`–`9`). A bare sign with no digits (e.g., `"-"`) is an error.

Error messages:
- `"empty string"` — the input is empty or contains only whitespace
- `"invalid character"` — a non-digit character was encountered (after any sign)

```vera
parse_int("42")        -- Ok(42)
parse_int("-7")        -- Ok(-7)
parse_int("+3")        -- Ok(3)
parse_int("  -42  ")   -- Ok(-42) (whitespace stripped)
parse_int("abc")       -- Err("invalid character")
parse_int("-")         -- Err("invalid character")
parse_int("")          -- Err("empty string")
```

#### parse_float64

<!-- vera:skip-parse category="FRAGMENT" reason="parse_float64 signature (no body)" -->
```vera
public fn parse_float64(@String -> @Result<Float64, String>)
  requires(true) ensures(true) effects(pure)
```

Parses a 64-bit floating-point number from a string. After stripping whitespace, an optional leading `-` sign is consumed, followed by one or more digits, an optional decimal point with additional digits, and an optional exponent (`e` or `E` followed by an optional sign and digits). At least one digit must appear in the integer part.

Error messages:
- `"empty string"` — the input is empty or contains only whitespace
- `"invalid character"` — a non-digit, non-`.`, non-`e`/`E` character was encountered

```vera
parse_float64("3.14")      -- Ok(3.14)
parse_float64("-2.5")      -- Ok(-2.5)
parse_float64("42")        -- Ok(42.0)
parse_float64("  1.0  ")   -- Ok(1.0) (whitespace stripped)
parse_float64("abc")       -- Err("invalid character")
parse_float64("")          -- Err("empty string")
```

#### parse_bool

<!-- vera:skip-parse category="FRAGMENT" reason="parse_bool signature (no body)" -->
```vera
public fn parse_bool(@String -> @Result<Bool, String>)
  requires(true) ensures(true) effects(pure)
```

Parses a boolean from a string. After stripping whitespace, the remaining content must be exactly `"true"` or `"false"` (strict lowercase). No other forms are accepted — `"True"`, `"TRUE"`, `"yes"`, `"1"`, etc. all produce errors. This strictness prevents ambiguity when models generate boolean values.

Error messages:
- `"expected true or false"` — the input does not match `"true"` or `"false"` after whitespace stripping

```vera
parse_bool("true")         -- Ok(true)
parse_bool("false")        -- Ok(false)
parse_bool("  true  ")     -- Ok(true) (whitespace stripped)
parse_bool("True")         -- Err("expected true or false")
parse_bool("yes")          -- Err("expected true or false")
parse_bool("")             -- Err("expected true or false")
```

### 9.6.16 Base64

#### base64\_encode

<!-- vera:skip-parse category="FRAGMENT" reason="base64_encode signature (no body)" -->
```
public fn base64_encode(@String -> @String)
  requires(true)
  ensures(string_length(@String.result) == ((string_length(@String.0) + 2) / 3) * 4
          || string_length(@String.0) == 0 && string_length(@String.result) == 0)
  effects(pure)
```

Encodes a UTF-8 string to standard Base64 (RFC 4648). Every 3 input bytes produce 4 output characters from the alphabet `A`–`Z`, `a`–`z`, `0`–`9`, `+`, `/`. Remaining 1–2 bytes are padded with `=`. An empty input produces an empty string.

```vera
base64_encode("Hello, World!")   -- "SGVsbG8sIFdvcmxkIQ=="
base64_encode("ABC")             -- "QUJD"
base64_encode("A")               -- "QQ=="
base64_encode("")                 -- ""
```

#### base64\_decode

<!-- vera:skip-parse category="FRAGMENT" reason="base64_decode signature (no body)" -->
```
public fn base64_decode(@String -> @Result<String, String>)
  requires(true)
  ensures(true)
  effects(pure)
```

Decodes a standard Base64 string (RFC 4648) to its original UTF-8 bytes. Returns `Ok(String)` on success or `Err(String)` with an error message on failure.

**Error conditions:**

- `"invalid base64 length"` — the input length is not a multiple of 4
- `"invalid base64"` — the input contains characters outside the Base64 alphabet

```vera
base64_decode("QUJD")                  -- Ok("ABC")
base64_decode("SGVsbG8sIFdvcmxkIQ==")  -- Ok("Hello, World!")
base64_decode("QQ==")                  -- Ok("A")
base64_decode("")                      -- Ok("")
base64_decode("ABC")                   -- Err("invalid base64 length")
base64_decode("QQ!!")                  -- Err("invalid base64")
```

### 9.6.17 URL Encoding

#### url\_encode

<!-- vera:skip-parse category="FRAGMENT" reason="url_encode signature (no body)" -->
```
public fn url_encode(@String -> @String)
  requires(true)
  ensures(true)
  effects(pure)
```

Percent-encodes a string for use in URLs (RFC 3986). Unreserved characters (`A`–`Z`, `a`–`z`, `0`–`9`, `-`, `_`, `.`, `~`) pass through unchanged. All other bytes are encoded as `%XX` where `XX` is the uppercase hexadecimal representation of the byte value.

```vera
url_encode("Hello, World!")     -- "Hello%2C%20World%21"
url_encode("foo@bar.com")       -- "foo%40bar.com"
url_encode("a b c")             -- "a%20b%20c"
url_encode("safe-text_123.~")   -- "safe-text_123.~"
url_encode("")                  -- ""
```

#### url\_decode

<!-- vera:skip-parse category="FRAGMENT" reason="url_decode signature (no body)" -->
```
public fn url_decode(@String -> @Result<String, String>)
  requires(true)
  ensures(true)
  effects(pure)
```

Decodes a percent-encoded string (RFC 3986). Each `%XX` sequence is converted to the byte with that hexadecimal value. Both uppercase and lowercase hex digits are accepted. Returns `Ok(String)` on success or `Err(String)` with an error message on failure.

**Error conditions:**

- `"invalid percent-encoding"` — truncated `%` sequence (fewer than 2 hex digits following `%`) or invalid hex digits

```vera
url_decode("Hello%2C%20World%21")  -- Ok("Hello, World!")
url_decode("%41%42%43")            -- Ok("ABC")
url_decode("hello")               -- Ok("hello")
url_decode("")                     -- Ok("")
url_decode("%ZZ")                  -- Err("invalid percent-encoding")
url_decode("%4")                   -- Err("invalid percent-encoding")
```

### 9.6.18 URL Parsing

The `UrlParts` ADT is defined in §9.3.3 and injected by the standard prelude (§9.1.2).

<!-- vera:skip-parse category="FRAGMENT" reason="url_parse signature (no body)" -->
```
public fn url_parse(@String -> @Result<UrlParts, String>)
  requires(true)
  ensures(true)
  effects(pure)
```

Decomposes a URL string into its RFC 3986 components. Returns `Ok(UrlParts(scheme, authority, path, query, fragment))` on success, or `Err("missing scheme")` if no `:` delimiter is found. Missing optional components (authority, query, fragment) are represented as empty strings.

```
url_parse("https://example.com/path?q=1#frag")
  -- Ok(UrlParts("https", "example.com", "/path", "q=1", "frag"))
url_parse("http:")
  -- Ok(UrlParts("http", "", "", "", ""))
url_parse("file:///path")
  -- Ok(UrlParts("file", "", "/path", "", ""))
url_parse("no-scheme")
  -- Err("missing scheme")
```

<!-- vera:skip-parse category="FRAGMENT" reason="url_join signature (no body)" -->
```
public fn url_join(@UrlParts -> @String)
  requires(true)
  ensures(true)
  effects(pure)
```

Reassembles a `UrlParts` value into a URL string. If the scheme is non-empty, the `://` separator is inserted. The `?` and `#` delimiters are only included when their respective components are non-empty.

```
url_join(UrlParts("https", "example.com", "/path", "q=1", "frag"))
  -- "https://example.com/path?q=1#frag"
url_join(UrlParts("", "", "", "", ""))
  -- ""
```

### 9.6.19 similarity (Future)

> **Status: Not yet implemented.** Requires `Inference.embed` (returning `Array<Float64>`) which is deferred to a follow-up release. `Inference.complete` was implemented in v0.0.101 ([#61](https://github.com/aallan/vera/issues/61)); `embed` is tracked separately ([#371](https://github.com/aallan/vera/issues/371)).

<!-- vera:skip-parse category="FRAGMENT" reason="similarity signature (no body)" -->
```
public fn similarity(@Array<Float64>, @Array<Float64> -> @Float64)
  requires(array_length(@Array<Float64>.0) == array_length(@Array<Float64>.1))
  ensures(@Float64.result >= -1.0 && @Float64.result <= 1.0)
  effects(pure)
```

Computes the cosine similarity between two vectors (embeddings). The arrays must have equal length (enforced by precondition). The result is in the range \[-1, 1\], where 1 indicates identical direction, 0 indicates orthogonality, and -1 indicates opposite direction.

This function is pure — it performs no effects. It is intended for use with the `Inference.embed` operation to compare semantic similarity of text.

### 9.6.20 Regular Expressions

Four pure functions for pattern matching on strings using regular expressions. All accept patterns in standard regex syntax and return `Result` types to safely handle invalid patterns.

#### regex\_match

<!-- vera:skip-parse category="FRAGMENT" reason="regex_match signature (no body)" -->
```
public fn regex_match(@String, @String -> @Result<Bool, String>)
  requires(true)
  ensures(true)
  effects(pure)
```

Tests whether the input string (first argument) contains a substring matching the regex pattern (second argument). Returns `Ok(true)` if a match is found, `Ok(false)` otherwise, or `Err(msg)` if the pattern is invalid.

```vera
let @Result<Bool, String> = regex_match("hello123", "\\d+");
-- Ok(true) — digits found
```

#### regex\_find

<!-- vera:skip-parse category="FRAGMENT" reason="regex_find signature (no body)" -->
```
public fn regex_find(@String, @String -> @Result<Option<String>, String>)
  requires(true)
  ensures(true)
  effects(pure)
```

Returns the first substring of the input that matches the pattern. Returns `Ok(Some(match))` if found, `Ok(None)` if not found, or `Err(msg)` for invalid patterns.

```vera
let @Result<Option<String>, String> = regex_find("abc123def", "\\d+");
-- Ok(Some("123"))
```

#### regex\_find\_all

<!-- vera:skip-parse category="FRAGMENT" reason="regex_find_all signature (no body)" -->
```
public fn regex_find_all(@String, @String -> @Result<Array<String>, String>)
  requires(true)
  ensures(true)
  effects(pure)
```

Returns all non-overlapping substrings of the input that match the pattern. Always returns full match strings (group 0), even when the pattern contains capture groups. Returns `Ok([])` (empty array) if no matches are found, or `Err(msg)` for invalid patterns.

```vera
let @Result<Array<String>, String> = regex_find_all("a1b2c3", "\\d");
-- Ok(["1", "2", "3"])
```

#### regex\_replace

<!-- vera:skip-parse category="FRAGMENT" reason="regex_replace signature (no body)" -->
```
public fn regex_replace(@String, @String, @String -> @Result<String, String>)
  requires(true)
  ensures(true)
  effects(pure)
```

Replaces the **first** occurrence of the pattern in the input string with the replacement string (third argument). Returns the modified string, or the original string unchanged if no match is found. Returns `Err(msg)` for invalid patterns.

```vera
let @Result<String, String> = regex_replace("hello world", "world", "vera");
-- Ok("hello vera")
```

**Implementation note:** These functions are implemented as host imports — they delegate to the runtime's native regex engine (Python's `re` module for wasmtime, JavaScript's `RegExp` for the browser runtime). This avoids embedding a regex engine in WASM while providing access to mature, well-tested implementations.

### 9.6.21 Array Utilities

Vera provides seven additional array combinators beyond `array_map` / `array_filter` / `array_fold`. All are implemented as iterative WASM loops with O(1) shadow-stack depth, mirroring the architecture established by [#480](https://github.com/aallan/vera/issues/480). None require ability dispatch on the polymorphic element type — `array_sort`, `array_contains`, and `array_index_of` (which would need to invoke `compare<T>` / `eq<T>` from inside the loop) are tracked separately and implemented in a future release.

<!-- vera:skip-parse category="FRAGMENT" reason="array_mapi signature (no body)" -->
```vera
public forall<A, B> fn array_mapi(@Array<A>, fn(A, Nat -> B) effects(pure) -> @Array<B>)
  requires(true) ensures(true) effects(pure)
```

`array_mapi` maps a function over the array, passing each element along with its zero-based position as the second argument. Same return shape as `array_map`; the index is provided so the caller can avoid the recursive-accumulator-with-index pattern that has historically been a leading source of De Bruijn indexing mistakes. Matches `mapi` from OCaml's `List`, `enumerate().map()` from Rust, and `arr.map((x, i) => ...)` from JavaScript.

```vera
array_mapi([10, 20, 30], fn(@Int, @Nat -> @Int) effects(pure) {
  @Int.0 + @Nat.0
})
-- [10, 21, 32]
```

<!-- vera:skip-parse category="FRAGMENT" reason="array_reverse signature (no body)" -->
```vera
public forall<T> fn array_reverse(@Array<T> -> @Array<T>)
  requires(true) ensures(true) effects(pure)
```

`array_reverse` returns a new array with the elements in reverse order. Length and element values are preserved. Single-pass O(n).

```vera
array_reverse([1, 2, 3, 4, 5])  -- [5, 4, 3, 2, 1]
```

<!-- vera:skip-parse category="FRAGMENT" reason="array_find signature (no body)" -->
```vera
public forall<T> fn array_find(@Array<T>, fn(T -> Bool) effects(pure) -> @Option<T>)
  requires(true) ensures(true) effects(pure)
```

`array_find` returns `Some(x)` for the first element where the predicate is `true`, or `None` if no element matches. Short-circuits on the first match — the predicate is not invoked for elements past the match.

```vera
array_find([1, 3, 5, 7, 9], fn(@Int -> @Bool) effects(pure) { @Int.0 > 4 })
-- Some(5)
```

<!-- vera:skip-parse category="FRAGMENT" reason="array_any + array_all signatures (no body)" -->
```vera
public forall<T> fn array_any(@Array<T>, fn(T -> Bool) effects(pure) -> @Bool)
  requires(true) ensures(true) effects(pure)

public forall<T> fn array_all(@Array<T>, fn(T -> Bool) effects(pure) -> @Bool)
  requires(true) ensures(true) effects(pure)
```

`array_any` returns `true` if at least one element satisfies the predicate, `false` otherwise. `array_all` returns `true` only when every element satisfies the predicate. Both short-circuit: `array_any` exits on the first true result, `array_all` exits on the first false. Empty-array convention follows the standard mathematical reading: `array_any([], _) == false` (no element to satisfy), `array_all([], _) == true` (vacuously true).

```vera
array_any([1, 2, 3], fn(@Int -> @Bool) effects(pure) { @Int.0 > 2 })  -- true
array_all([1, 2, 3], fn(@Int -> @Bool) effects(pure) { @Int.0 > 0 })  -- true
array_all([1, 2, 3], fn(@Int -> @Bool) effects(pure) { @Int.0 > 2 })  -- false
```

<!-- vera:skip-parse category="FRAGMENT" reason="array_flatten signature (no body)" -->
```vera
public forall<T> fn array_flatten(@Array<Array<T>> -> @Array<T>)
  requires(true) ensures(true) effects(pure)
```

`array_flatten` concatenates one level of nested arrays. Two-pass: the first pass sums the inner lengths to size the destination, the second pass copies each inner array contiguously. Empty inner arrays are skipped without overhead.

```vera
array_flatten([[1, 2], [3, 4], [5, 6]])  -- [1, 2, 3, 4, 5, 6]
array_flatten([[1, 2], [], [3]])         -- [1, 2, 3]
```

<!-- vera:skip-parse category="FRAGMENT" reason="array_sort_by signature (no body)" -->
```vera
public forall<T> fn array_sort_by(@Array<T>, fn(T, T -> Ordering) effects(pure) -> @Array<T>)
  requires(true) ensures(true) effects(pure)
```

`array_sort_by` returns a new array sorted using a caller-supplied comparator. The comparator receives two elements and returns an `@Ordering` value (`Less`, `Equal`, or `Greater`); the convention `cmp(a, b) == Less when a < b` produces ascending order. Implementation is insertion sort — stable, O(n²) worst-case, well-suited to the small-to-medium arrays Vera programs typically handle. A future release will add `array_sort<T> where Ord<T>` so the comparator can be inferred from the element type's `Ord` ability rather than supplied explicitly.

```vera
array_sort_by(
  [3, 1, 4, 1, 5, 9, 2, 6],
  fn(@Int, @Int -> @Ordering) effects(pure) {
    if @Int.1 < @Int.0 then { Less } else {
      if @Int.1 > @Int.0 then { Greater } else { Equal }
    }
  }
)
-- [1, 1, 2, 3, 4, 5, 6, 9]
```

**Verification:** all seven utilities have signatures verifiable by the type checker; their bodies fall to Tier 3 (runtime) verification, but for two distinct reasons.

The callback-based combinators — `array_mapi`, `array_find`, `array_any`, `array_all`, and `array_sort_by` — are Tier 3 because their semantics iterate a user-supplied closure whose effects, returns, and termination behaviour are not statically modelled in the verifier's encoding. This category cannot move to Tier 1 without a substantial extension to the SMT translation that reasons about higher-order functions.

`array_reverse` and `array_flatten` are Tier 3 for a different and narrower reason: they have no closure callback at all and their behaviour is entirely structural (length-preserving / length-summing respectively). They could in principle support stronger Tier 1 contracts such as `ensures(array_length(@result) == array_length(@input))` for `array_reverse` or `ensures(array_length(@result) == sum_inner_lengths(@input))` for `array_flatten`. The underlying SMT encoding for those properties is not yet implemented; once it is, both functions become candidates for Tier 1 promotion without any change to their signatures.

### 9.6.22 String Utilities and Character Classification

Vera provides eight additional string utilities and eight character classification primitives. All sixteen are implemented as inline WAT — no host imports — so they execute identically under the Python (`wasmtime`) and browser (Node.js / web) runtimes. Tracked in [#470](https://github.com/aallan/vera/issues/470) (utilities) and [#471](https://github.com/aallan/vera/issues/471) (classifiers).

All operations use **ASCII byte semantics**: classifiers test the first byte of the input string; case-conversion functions transform the first byte and pass remaining bytes through unchanged; structural splits work at the byte level. Unicode-aware variants are tracked separately and intentionally deferred.

#### String splits — bridges to the array combinators

<!-- vera:skip-parse category="FRAGMENT" reason="string_chars/lines/words signatures (no bodies)" -->
```vera
public fn string_chars(@String -> @Array<String>)
  requires(true) ensures(true) effects(pure)

public fn string_lines(@String -> @Array<String>)
  requires(true) ensures(true) effects(pure)

public fn string_words(@String -> @Array<String>)
  requires(true) ensures(true) effects(pure)
```

`string_chars` returns one 1-byte string per byte of the input, in order. This is the canonical bridge from string to array: combine with `array_map`, `array_filter`, `array_fold`, etc. to thread per-byte logic through the array combinators.

`string_lines` follows Python's `str.splitlines()`: splits on `\n`, `\r\n`, and `\r` line terminators. A trailing line terminator does **not** produce an empty trailing segment.

`string_words` follows Python's `str.split()` with no arguments: splits on runs of ASCII whitespace (the same set as `is_whitespace` — space, tab, `\n`, `\v`, `\f`, `\r`), and discards empty segments. `string_words("  ")` returns the empty array.

```vera
string_chars("abc")           -- ["a", "b", "c"]
string_lines("a\nb\r\nc\rd")  -- ["a", "b", "c", "d"]
string_lines("a\n")           -- ["a"]      -- not ["a", ""]
string_words("  foo  bar ")   -- ["foo", "bar"]
string_words("   ")           -- []
```

All three return a fresh `@Array<String>` whose elements are each independently allocated and copied. (The implementation does not share a backing buffer between elements: the GC mark phase rejects interior pointers — see `_emit_gc_collect` in `vera/codegen/assembly.py` — so a shared-buffer scheme cannot keep the elements rooted across a collection triggered after the function returns.)

#### String transformations

<!-- vera:skip-parse category="FRAGMENT" reason="string_reverse/trim_start/trim_end signatures (no body, #470)" -->
```vera
public fn string_reverse(@String -> @String)
  requires(true) ensures(true) effects(pure)

public fn string_trim_start(@String -> @String)
  requires(true) ensures(true) effects(pure)

public fn string_trim_end(@String -> @String)
  requires(true) ensures(true) effects(pure)
```

`string_reverse` reverses the byte order of the input. ASCII-safe; for multi-byte UTF-8 sequences the result is not a valid UTF-8 string. The empty string round-trips.

`string_trim_start` strips leading ASCII whitespace (the same set as `is_whitespace` — space, tab, `\n`, `\v`, `\f`, `\r`); `string_trim_end` strips trailing whitespace. Each preserves the opposite end exactly. The all-whitespace input returns the empty string.

```vera
string_reverse("hello")       -- "olleh"
string_trim_start("  hi  ")   -- "hi  "
string_trim_end("  hi  ")     -- "  hi"
```

#### Padding

<!-- vera:skip-parse category="FRAGMENT" reason="string_pad_start/pad_end signatures (no body, #470)" -->
```vera
public fn string_pad_start(@String, @Nat, @String -> @String)
  requires(true) ensures(true) effects(pure)

public fn string_pad_end(@String, @Nat, @String -> @String)
  requires(true) ensures(true) effects(pure)
```

`string_pad_start(s, n, fill)` returns `s` left-padded with `fill` so the result has length at least `n` bytes. `string_pad_end(s, n, fill)` pads on the right. Semantics match JavaScript's `padStart` / `padEnd`:

- If `string_length(s) >= n` the input is returned unchanged.
- The fill cycles left-to-right and is truncated to exactly the padding length, not the next multiple of `string_length(fill)`.
- An empty `fill` is a no-op (returns the input unchanged) — `pad_start` cannot infinitely loop.

```vera
string_pad_start("7", 5, "0")     -- "00007"
string_pad_end("ok", 8, ".")      -- "ok......"
string_pad_start("x", 7, "ab")    -- "abababx"
string_pad_start("hello", 3, "*") -- "hello"
```

#### Case conversion

<!-- vera:skip-parse category="FRAGMENT" reason="char_to_upper/char_to_lower signatures (no body, #471)" -->
```vera
public fn char_to_upper(@String -> @String)
  requires(true) ensures(true) effects(pure)

public fn char_to_lower(@String -> @String)
  requires(true) ensures(true) effects(pure)
```

`char_to_upper` converts the first byte of the input to uppercase if it is an ASCII lowercase letter (`a..z`); other bytes pass through unchanged. `char_to_lower` is the dual. Only the first byte is transformed — these are deliberately first-character operations, useful for title-casing tokens.

```vera
char_to_upper("alice")  -- "Alice"
char_to_upper("5xyz")   -- "5xyz"
char_to_lower("ALICE")  -- "aLICE"
char_to_upper("")       -- ""
```

For whole-string ASCII case conversion, see `string_upper` / `string_lower` in §9.6.14. Unicode-aware variants of all four operations are tracked alongside Unicode handling.

#### Character classifiers

<!-- vera:skip-parse category="FRAGMENT" reason="is_digit/alpha/... signatures (no body, #471)" -->
```vera
public fn is_digit(@String -> @Bool)         requires(true) ensures(true) effects(pure)
public fn is_alpha(@String -> @Bool)         requires(true) ensures(true) effects(pure)
public fn is_alphanumeric(@String -> @Bool)  requires(true) ensures(true) effects(pure)
public fn is_whitespace(@String -> @Bool)    requires(true) ensures(true) effects(pure)
public fn is_upper(@String -> @Bool)         requires(true) ensures(true) effects(pure)
public fn is_lower(@String -> @Bool)         requires(true) ensures(true) effects(pure)
```

Each classifier inspects the **first byte** of the input string and returns a `@Bool`. ASCII range definitions:

| Predicate | Returns true for byte values |
|---|---|
| `is_digit` | `0x30..0x39` (`'0'..'9'`) |
| `is_alpha` | `0x41..0x5A` or `0x61..0x7A` (`'A'..'Z'`, `'a'..'z'`) |
| `is_alphanumeric` | union of `is_digit` and `is_alpha` |
| `is_whitespace` | `0x09` (tab), `0x0A` (`\n`), `0x0B` (`\v`), `0x0C` (`\f`), `0x0D` (`\r`), `0x20` (space) — Python `str.isspace()` ASCII set |
| `is_upper` | `0x41..0x5A` (`'A'..'Z'`) |
| `is_lower` | `0x61..0x7A` (`'a'..'z'`) |

Every classifier returns `false` for the empty string — there is no first byte to inspect, so no predicate can hold.

```vera
is_digit("5")   -- true
is_digit("x")   -- false
is_digit("")    -- false
is_alpha("A")   -- true
is_alpha("9")   -- false
is_whitespace("\t")  -- true
```

**Verification:** all sixteen functions have Tier-1-verifiable signatures; their bodies fall to Tier 3 (runtime) verification because the SMT encoding does not yet model byte-level string operations. Their `requires(true)` / `ensures(true)` contracts are total, so Tier 3 reduces to runtime trap-freedom — every input is accepted.

### 9.6.23 JSON Typed Accessors

Vera provides eleven additional JSON accessor functions that eliminate the two-level pattern-match boilerplate (`match option ... { Some(@Json) -> match @Json.0 { JNumber(@Float64) -> ... } }`) that every JSON API consumer would otherwise write. Tracked in [#366](https://github.com/aallan/vera/issues/366).

Unlike the rest of the chapter-9 built-ins, these are **pure-Vera prelude functions**, not WASM translators. The compiler injects them into every module that references `Json` values, alongside the existing `json_get` / `json_keys` / `json_type` combinators. No new host imports and no dedicated WASM translator paths — but the accessors are still compiled as ordinary WASM functions (via the standard AST-to-WAT pipeline) whenever a module actually references them. A module that never calls any of the eleven accessors pays zero compiled-WASM cost for them.

#### Layer 1 — type-coercion accessors

<!-- vera:skip-parse category="FRAGMENT" reason="json_as_* Layer-1 signatures (no body, #366)" -->
```vera
public fn json_as_string(@Json -> @Option<String>)
  requires(true) ensures(true) effects(pure)

public fn json_as_number(@Json -> @Option<Float64>)
  requires(true) ensures(true) effects(pure)

public fn json_as_bool(@Json -> @Option<Bool>)
  requires(true) ensures(true) effects(pure)

public fn json_as_int(@Json -> @Option<Int>)
  requires(true) ensures(true) effects(pure)

public fn json_as_array(@Json -> @Option<Array<Json>>)
  requires(true) ensures(true) effects(pure)

public fn json_as_object(@Json -> @Option<Map<String, Json>>)
  requires(true) ensures(true) effects(pure)
```

Each `json_as_*` returns `Some(value)` when the Json's constructor matches the requested type, `None` otherwise. The accessors are disjoint — at most one returns `Some` for any given Json value.

`json_as_int` is the one asymmetric case: it applies `float_to_int` to the underlying `Float64`, truncating toward zero. `float_to_int` (aka WASM's `i64.trunc_f64_s`) traps on NaN, ±infinity, and any finite float outside the closed-open i64 range `[-2^63, 2^63)` — that is, `f < -2^63` or `f >= 2^63`. The range is asymmetric because two's-complement i64 can represent `-2^63 = INT64_MIN` exactly but not `+2^63`. `json_as_int` guards all four trap paths (`float_is_nan`, `float_is_infinite`, plus explicit bounds `f >= 9223372036854775808.0` and `f < -9223372036854775808.0`) and returns `None` for every non-representable-as-Int input. At the inclusive lower bound, `json_as_int(JNumber(-9223372036854775808.0))` correctly returns `Some(INT64_MIN)`.

```vera
json_as_string(JString("hi"))              -- Some("hi")
json_as_string(JNumber(1.0))               -- None
json_as_int(JNumber(42.7))                 -- Some(42)
json_as_int(JNumber(-3.9))                 -- Some(-3)   -- toward-zero truncation
json_as_int(JNumber(0.0 / 0.0))            -- None       -- NaN guard
json_as_int(JNumber(infinity()))           -- None       -- infinity guard
```

#### Layer 2 — compound field accessors

<!-- vera:skip-parse category="FRAGMENT" reason="json_get_* Layer-2 signatures (no body, #366)" -->
```vera
public fn json_get_string(@Json, @String -> @Option<String>)
  requires(true) ensures(true) effects(pure)

public fn json_get_number(@Json, @String -> @Option<Float64>)
  requires(true) ensures(true) effects(pure)

public fn json_get_bool(@Json, @String -> @Option<Bool>)
  requires(true) ensures(true) effects(pure)

public fn json_get_int(@Json, @String -> @Option<Int>)
  requires(true) ensures(true) effects(pure)

public fn json_get_array(@Json, @String -> @Option<Array<Json>>)
  requires(true) ensures(true) effects(pure)
```

Each `json_get_X(j, key)` is definitionally equivalent to chaining `json_get(j, key)` with the matching `json_as_X` coercion: it returns `None` both when the field is missing and when the field is present but of the wrong type. This is the accessor shape that 90% of real API-consuming code wants — field lookup and type coercion collapsed into one call.

There is no `json_get_object` — chained field access is handled by `json_get` returning `Option<Json>`, then letting the caller recurse.

```vera
-- Assume parsed: {"name":"Alice","age":30,"active":true,"tags":[1,2,3]}
json_get_string(obj, "name")               -- Some("Alice")
json_get_int(obj, "age")                   -- Some(30)
json_get_bool(obj, "active")               -- Some(true)
json_get_array(obj, "tags")                -- Some([JNumber(1), ...])
json_get_int(obj, "nope")                  -- None (missing)
json_get_int(obj, "name")                  -- None (wrong type)
```

**Verification:** all eleven functions have Tier-1-verifiable signatures; their bodies fall to Tier 3 runtime verification because the SMT encoding does not yet model the `Json` ADT match expressions or `Map<String, Json>` operations.

## 9.7 Built-in Types

### 9.7.1 Json

`Json` is a standard library ADT for structured data interchange. Tracked in [#58](https://github.com/aallan/vera/issues/58).

```vera
public data Json {
  JNull,
  JBool(Bool),
  JNumber(Float64),
  JString(String),
  JArray(Array<Json>),
  JObject(Map<String, Json>)
}
```

The `Json` type is provided by the standard prelude — no explicit `data` declaration is required. JSON values are constructed with the six variant constructors and destructured via `match`.

**Parsing and serialization:**

| Function | Signature | Description |
|----------|-----------|-------------|
| `json_parse(s)` | `(String) → Result<Json, String>` | Parse JSON text; `Err` outside the accepted domain below |
| `json_stringify(j)` | `(Json) → String` | Serialize a Json value to its canonical JSON string |

**`json_parse`'s accepted domain.** Both runtimes accept exactly RFC 8259-valid text that decodes to finite numbers and to strings that are sequences of Unicode scalar values. Text outside that domain MUST produce `Err` at the parse rather than a value, and for the two exclusions below the message MUST be the same on every runtime. The domain is defined here rather than inherited from whatever the host parser happens to accept (DESIGN.md: explicit over implicit) — the two exclusions are precisely where the host parsers disagree:

- **A non-finite number, however it is written.** RFC 8259 has no literal for one, so the JavaScript constants `NaN`, `Infinity` and `-Infinity` are refused wherever a value may appear, nested or at the top level. A *syntactically valid* number whose magnitude overflows the `Float64` a `JNumber` holds is refused too, whether it is written with an exponent (`1e999`) or as plain digits (`1` followed by 309 zeros) — the distinction matters to a host whose parser decodes the two to different types, and not at all to the domain: RFC 8259 §6 sets no limit on a number's range but says an implementation may set one, and Vera's accepted range is the finite `Float64` values, which is exactly what `json_stringify` can write back. The bound is the point at which the nearest `Float64` becomes infinite, so a magnitude above the largest finite double that still *rounds* to it is accepted. Underflow is a different question and is *not* refused either: `1e-999` decodes to `0`, which is finite and in the domain. This is the input-side counterpart of the serialization rule below — a non-finite number has no JSON representation in either direction — and with both entry routes closed, the only way to reach the output-side refusal is to construct a `JNumber` from `nan()` or `infinity()`.
- **A lone surrogate** — a `\uXXXX` escape in D800–DFFF with no matching partner. The text is grammatically legal, but its decoded value is not a sequence of scalar values, and a Vera `String` is. The alternatives are substituting U+FFFD, which silently yields a value the text did not encode, and admitting strings the rest of the language cannot represent (§0.2.6). A *matched* high-then-low pair is ordinary and is accepted: it denotes one astral scalar value.

Text malformed for any other reason also produces `Err`, but that message is the host parser's own and is not pinned.

**Canonical serialization.** `json_stringify` has exactly one output form, per the one-canonical-form principle (§0.2.3), and every runtime produces it byte for byte (§12.9.3):

- **Separators.** `,` between elements and members, `:` between a key and its value, with no surrounding whitespace. No indentation, no trailing newline.
- **Object members.** Emitted in the insertion order of the underlying `Map<String, Json>`, not sorted.
- **Strings.** Escaped per RFC 8259, with non-ASCII characters emitted literally rather than as `\uXXXX` escapes.
- **Numbers.** Rendered by ECMAScript's `Number::toString` with radix 10 ([ECMA-262 §6.1.6.1.20](https://tc39.es/ecma262/#sec-numeric-types-number-tostring)). A `JNumber` wraps a `Float64`, so this is the rendering rule that matters most: an integral value carries no fractional part (`1`, not `1.0`), the notation switches to exponential at and above `1e21` and below `1e-6`, the exponent is signed and unpadded (`1e-7`, not `1e-07`), and negative zero renders `0`.

The number rule is what makes serialization non-destructive: a document containing `1` re-serializes as `1`. A form that wrote `1.0` would silently alter integral values in transit, which §0.2.2 (explicitness, no implicit behaviour) rules out.

`NaN` and infinities have no JSON representation. `json_stringify` on a `JNumber` holding one **fails** rather than substituting `null` — substituting would turn a value the format cannot carry into a different, valid one that no consumer could distinguish from a genuine `JNull`. Guard with `float_is_nan` / `float_is_infinite` (§9.6.12) before serializing.

**Object access:**

| Function | Signature | Description |
|----------|-----------|-------------|
| `json_get(j, key)` | `(Json, String) → Option<Json>` | Get a field from a JObject; `None` if absent or not an object |
| `json_has_field(j, key)` | `(Json, String) → Bool` | Check whether a JObject has a field |
| `json_keys(j)` | `(Json) → Array<String>` | Get all keys from a JObject; empty array if not an object |

**Array access:**

| Function | Signature | Description |
|----------|-----------|-------------|
| `json_array_get(j, i)` | `(Json, Int) → Option<Json>` | Get element at index from a JArray; `None` if out of bounds or not an array |
| `json_array_length(j)` | `(Json) → Int` | Get length of a JArray; 0 if not an array |

**Type inspection:**

| Function | Signature | Description |
|----------|-----------|-------------|
| `json_type(j)` | `(Json) → String` | Returns `"null"`, `"bool"`, `"number"`, `"string"`, `"array"`, or `"object"` |

All JSON functions are pure. The `Json` type is a heap-allocated ADT — values are `i32` pointers into WASM linear memory with a tag + payload layout (like all Vera ADTs). Only `json_parse` and `json_stringify` are host imports (Python `json` / JavaScript `JSON`); the remaining utility functions (`json_get`, `json_has_field`, `json_type`, `json_keys`, `json_array_get`, `json_array_length`) are injected as Vera source from the standard prelude.

**Example:**

```vera
private fn get_name(@String -> @Result<String, String>)
  requires(true)
  ensures(true)
  effects(pure)
{
  match json_parse(@String.0) {
    Err(@String) -> Err(@String.0),
    Ok(@Json) -> match json_get(@Json.0, "name") {
      None -> Err("missing name"),
      Some(@Json) -> match @Json.0 {
        JString(@String) -> Ok(@String.0),
        _ -> Err("name is not a string")
      }
    }
  }
}
```

Refinement types can express JSON schemas:

```
type ApiResponse = { @Json | json_has_field(@Json.0, "status") };
```

### 9.7.2 Decimal

`Decimal` provides exact decimal arithmetic for financial and precision-sensitive applications. Tracked in [#333](https://github.com/aallan/vera/issues/333).

Decimal is an opaque built-in type implemented via host imports, following the same pattern as `Map<K, V>` and `Set<T>`. The runtime maintains `decimal.Decimal` values (Python) or exact scaled-BigInt values (JavaScript); WASM code interacts with decimals through `i32` handles. All operations are pure.

**Construction and conversion:**

| Function | Signature | Description |
|----------|-----------|-------------|
| `decimal_from_int(n)` | `(Int) → Decimal` | Exact conversion from integer |
| `decimal_from_float(f)` | `(Float64) → Decimal` | Conversion via Python's `str(v)` float repr (may not be exact) |
| `decimal_from_string(s)` | `(String) → Option<Decimal>` | Parse a decimal string per the grammar below; `None` on failure |
| `decimal_to_string(d)` | `(Decimal) → String` | String representation |
| `decimal_to_float(d)` | `(Decimal) → Float64` | Potentially lossy conversion to float |

**`decimal_from_string` grammar:** both runtimes accept exactly the language `[+-]? ( digits ( "." digits? )? | "." digits ) ( ("e" | "E") [+-]? digits )?` where `digits` is one or more ASCII `0`–`9`, applied after ignoring surrounding whitespace — the six code points `is_whitespace` names (`0x09`, `0x0A`, `0x0B`, `0x0C`, `0x0D`, `0x20`) and no others, stated here because the two host libraries' own trim functions disagree about the rest in both directions, and the exponent token (when present) MUST satisfy `|exp| <= 999999` — the default context's exponent floor, cited by the `decimal_round` fallback below and chosen to keep operand magnitudes bounded and the exponent-token check exact. Only finite decimals are accepted: special values (`NaN`, `sNaN`, `Infinity`), digit-group underscores (`1_000`), non-ASCII digits, and out-of-range exponent tokens are all rejected with `None`, even where a host decimal library would accept them. The accepted domain is defined by this grammar rather than inherited from whatever the host library parses (DESIGN.md: explicit over implicit) — the Python host pre-validates with this grammar before constructing a `decimal.Decimal`, and the browser runtime's parser recognises the same language, checking the exponent token as a string before any numeric conversion (an unbounded token would otherwise round silently above 2^53). This `|exp| <= 999999` bound constrains **input literals** only; exact arithmetic on accepted operands can grow the exponent past it, as squaring the largest accepted literal shows, and such results are computed and rendered identically in both runtimes (the Python host runs the binary operations in a context whose exponent range is widened to the library maximum, `±10^18`, so a finite result never overflows and matches the browser's unbounded engine).

```
-- The |exp| <= 999999 bound constrains input LITERALS.  Exact
-- arithmetic on accepted operands can carry the exponent past it.
public fn square_of_the_largest_literal(@Unit -> @String)
  requires(true)
  ensures(true)
  effects(pure)
{
  match decimal_from_string("1e999999") {
    Some(@Decimal) -> decimal_to_string(decimal_mul(@Decimal.0, @Decimal.0)),
    None -> "unreachable: 1e999999 is inside the grammar"
  }
}
```

Returns `1E+1999998` on both runtimes. `decimal_from_string` yields an
`Option<Decimal>`, so the operand is unwrapped before it reaches
`decimal_mul`, which takes two `Decimal`\ s.

**Arithmetic:**

| Function | Signature | Description |
|----------|-----------|-------------|
| `decimal_add(a, b)` | `(Decimal, Decimal) → Decimal` | Addition |
| `decimal_sub(a, b)` | `(Decimal, Decimal) → Decimal` | Subtraction |
| `decimal_mul(a, b)` | `(Decimal, Decimal) → Decimal` | Multiplication |
| `decimal_div(a, b)` | `(Decimal, Decimal) → Option<Decimal>` | Division; `None` on division by zero |
| `decimal_neg(d)` | `(Decimal) → Decimal` | Negation |
| `decimal_abs(d)` | `(Decimal) → Decimal` | Absolute value |
| `decimal_round(d, n)` | `(Decimal, Int) → Decimal` | Round to `n` decimal places |

**Comparison:**

| Function | Signature | Description |
|----------|-----------|-------------|
| `decimal_compare(a, b)` | `(Decimal, Decimal) → Ordering` | Returns `Less`, `Equal`, or `Greater` |
| `decimal_eq(a, b)` | `(Decimal, Decimal) → Bool` | Equality test |

**Example:**

```vera
private fn decimal_demo(-> @Int)
  requires(true)
  ensures(@Int.result == 1)
  effects(pure)
{
  let @Decimal = decimal_add(decimal_from_int(100), decimal_from_int(3));
  if decimal_eq(@Decimal.0, decimal_from_int(103)) then { 1 } else { 0 }
}
```

**Runtime parity:** Both runtimes provide exact decimal arithmetic and comparison over finite decimal values. The Python runtime uses `decimal.Decimal`; the browser runtime uses a scaled-BigInt engine that mirrors `decimal.Decimal`'s default context (28 significant digits, `ROUND_HALF_EVEN`) operation-for-operation: construction (`decimal_from_int`; `decimal_from_float` including Python's float-repr formatting, so `decimal_from_float(100.0)` renders `"100.0"` in both runtimes and the implied exponent carries through arithmetic; `decimal_from_string` under the grammar above), addition, subtraction, multiplication, division (ideal-exponent trailing-zero trimming; the Python host runs these four binary operations in an exponent-widened context, `Emax`/`Emin` = `±10^18`, so a finite result whose exponent exceeds the default `±999999` returns the same exact value as the browser's unbounded engine rather than raising), rounding (quantize semantics, including negative `places`, whose quantum exponent is `max(0, -places - 27)` because the quantum itself is context-rounded; `places` below the context's exponent floor of `-999999` leave the value unchanged in both runtimes, extending the same unchanged-value fallback that covers unrepresentable quantize results), negation and absolute value (which apply the context, rounding to 28 significant digits like Python's unary operators), comparison, equality, and the canonical string form all agree byte-for-byte across the two runtimes — enforced by the compile-once, compare-stdout-byte-exact parity tests in `tests/test_browser.py` (`TestBrowserDecimalExact856`). `decimal_compare` and `decimal_eq` share one exact numeric comparison in each runtime, so `decimal_from_string("1.0")` and `decimal_from_string("1")` compare `Equal` **and** `eq` in both. The one exclusion is non-finite floats through `decimal_from_float` (NaN, ±infinity): `decimal_to_string` and `decimal_to_float` round-trip them identically in both runtimes (`NaN` / `Infinity` / `-Infinity`), but arithmetic and comparison on such values are defined only on the Python runtime — the browser runtime rejects them with a loud runtime error naming this section. This closed [#856](https://github.com/aallan/vera/issues/856) (was: the browser runtime routed the family through JavaScript `Number`, losing precision and contradicting itself); see the CHANGELOG.

### 9.7.3 Markdown

Markdown is the lingua franca of large language models — they understand it natively and generate it naturally. A typed Markdown ADT makes document structure visible to the type system, enabling contracts that verify the structural properties of agent output.

Markdown is represented as two mutually defined ADTs: `MdBlock` for block-level elements (§9.3.6) and `MdInline` for inline-level content (§9.3.5). The two-level design makes illegal states unrepresentable — a heading cannot contain another heading at the type level.

```
public data MdInline {
  MdText(String),
  MdCode(String),
  MdEmph(Array<MdInline>),
  MdStrong(Array<MdInline>),
  MdLink(Array<MdInline>, String),
  MdImage(String, String)
}
```

`MdInline` constructors:
- `MdText(@String)` — plain text run. The leaf node of all inline content.
- `MdCode(@String)` — inline code span. Essential for agent communication about code.
- `MdEmph(@Array<MdInline>)` — emphasis (italic). Contains recursive inline content.
- `MdStrong(@Array<MdInline>)` — strong emphasis (bold). Contains recursive inline content.
- `MdLink(@Array<MdInline>, @String)` — hyperlink: display text (inline content) and target URL.
- `MdImage(@String, @String)` — image: alt text and source URL.

```
public data MdBlock {
  MdParagraph(Array<MdInline>),
  MdHeading(Nat, Array<MdInline>),
  MdCodeBlock(String, String),
  MdBlockQuote(Array<MdBlock>),
  MdList(Bool, Array<Array<MdBlock>>),
  MdThematicBreak,
  MdTable(Array<Array<Array<MdInline>>>),
  MdDocument(Array<MdBlock>)
}
```

`MdBlock` constructors:
- `MdParagraph(@Array<MdInline>)` — paragraph: a sequence of inline content.
- `MdHeading(@Nat, @Array<MdInline>)` — heading: level (1--6) as `Nat`, plus inline content. The level is a number rather than six separate constructors, allowing contracts like `@Nat.0 >= 1 && @Nat.0 <= 6`.
- `MdCodeBlock(@String, @String)` — fenced code block: language tag and code body. Critical for agents working with source code.
- `MdBlockQuote(@Array<MdBlock>)` — block quote: contains recursive block content.
- `MdList(@Bool, @Array<Array<MdBlock>>)` — list: ordered (`true`) or unordered (`false`), with each item containing block content.
- `MdThematicBreak` — horizontal rule. Nullary constructor.
- `MdTable(@Array<Array<Array<MdInline>>>)` — table: rows of cells, each cell containing inline content. Tables are a GitHub Flavored Markdown extension, not strict CommonMark, but they are ubiquitous in agent communication and document conversion output.
- `MdDocument(@Array<MdBlock>)` — top-level document: a sequence of blocks.

**Design note.** The following Markdown constructs are intentionally excluded per the one-canonical-form principle (§0.2.3). Each has a canonical equivalent in the ADT:

- **Raw HTML** (block and inline) — not safe for verification, not appropriate for agent-to-agent communication.
- **Link reference definitions** — resolved to inline `MdLink` during parsing. The parsed ADT has no reference indirection.
- **Setext headings** — merged with ATX headings into `MdHeading`. Both surface syntaxes parse to the same constructor.
- **Indented code blocks** — merged with fenced code blocks into `MdCodeBlock` (with an empty language string).
- **Hard and soft line breaks** — collapsed into paragraph text. Not structurally significant for agent communication.

**Parse and render operations:**

<!-- vera:skip-parse category="FUTURE" reason="md_parse signature (no body)" -->
```
public fn md_parse(@String -> @Result<MdBlock, String>)
  requires(true)
  ensures(true)
  effects(pure)
```

Parses a Markdown string into an `MdDocument`. Returns `Err` if parsing fails. This is pure — it transforms one value to another with no side effects.

<!-- vera:skip-parse category="FUTURE" reason="md_render" -->
```
public fn md_render(@MdBlock -> @String)
  requires(true)
  ensures(true)
  effects(pure)
```

Renders an `MdBlock` to a canonical Markdown string. Always succeeds. For every block the subset can write back, the round-trip property `md_parse(md_render(b)) == Ok(b)` MUST hold: rendering then re-parsing preserves structure. Two families are outside it, both because the subset has no text for them: the two code-span shapes named below, and a container with nothing in it to write — an `MdList` with no items or an `MdTable` with no rows renders to no lines, so it re-parses to no block. (An empty `MdBlockQuote` and an empty list *item* are inside the property: each has a form, given below.) Every runtime produces the same string (§12.9.3).

Four rules carry that property. The first two follow from the ADT having no line-break node (see the design note above); the last two from a container needing to be readable back as one block:

- **A paragraph is one line.** Its inline content is rendered without internal newlines. A parser collapses a paragraph's soft line breaks to spaces on the way in, so nothing survives to be re-emitted.
- **A container prefixes every line of every child.** A block quote writes `>` and a space before each rendered line, and a bare `>` for a blank one; a list item writes its marker before the first line and an equal-width indent before the rest. Prefixing only a child's first line would leave a fenced block's body — or a nested block's continuation — outside its container, and the next `md_parse` would read it as a sibling.
- **A container separates its children.** A block quote writes a bare `>` between adjacent children, as a document writes a blank line between its own. Without it two quoted paragraphs render as two adjacent quoted lines, which re-parse as one paragraph. An empty child still occupies its line: a `MdBlockQuote` with no children renders `>`, and a list item with no blocks renders its marker followed by a space, which is what the item patterns read back — a bare `-` is a paragraph. Rendering either as nothing deletes it, and in an ordered list renumbers every item after it. A container with nothing to render at all — a list with no items, a table with no rows — contributes no lines **and** no separator, because a separator standing for an absent block is a blank line the next parse cannot attribute to anything.
- **A code span is fenced longer than its content.** The fence is one backtick more than the longest backtick run inside the span, with a single padding space on each side when the content itself starts or ends with a backtick, or when it both starts and ends with a space — a parser strips one such pair, so the pad is what it removes instead of the content's own spaces. A fixed-width fence terminates on a run inside the content.

Together these MUST make `md_render` a fixed point: re-parsing and re-rendering its output returns the same bytes. Unlike the round-trip property this one has no exceptions — a block with no text renders to no lines, which re-renders to no lines.

Two code-span shapes are outside the **round-trip** property — not the fixed point, which has no exceptions. They are the two that property defers to above, and they are lost identically on every runtime rather than differently, because the subset has no escape syntax to write them another way: a span needing three or more backticks, at the start of a line, where that run is a fenced-code-block opener; and an empty span, whose rendering reads back as literal text.

The rules are visible from a value a program builds, which is where they
bite: a parser cannot produce an empty list item or a space-bounded code
span, so only a constructed `MdBlock` reaches them.

```
-- A container prefixes every line of every child, separates adjacent
-- children with a bare '>', and still writes a line for an empty one.
public fn quote_rules(@Unit -> @String)
  requires(true)
  ensures(true)
  effects(pure)
{
  md_render(MdDocument([MdBlockQuote([MdParagraph([MdText("one")]), MdCodeBlock("sh", "a\nb")]), MdBlockQuote([])]))
}
```

Renders `> one`, `>`, `> ```sh`, `> a`, `> b`, `> ``` `, a blank line, and
`>` — the fenced block's body carries the prefix on every line, the bare
`>` separates the quote's two children, and the empty quote still occupies
its own line.

```
-- A code span is fenced longer than its content, and padded when the
-- content would otherwise merge with the fence or lose its own spaces.
public fn span_rules(@Unit -> @String)
  requires(true)
  ensures(true)
  effects(pure)
{
  md_render(MdDocument([MdParagraph([MdCode("a`b"), MdText(" "), MdCode(" x ")]), MdList(false, [[]])]))
}
```

Renders ``` ``a`b`` `  x  ` ``` and then `- `: the first span's fence is
one backtick longer than the run inside it, the second is padded so the
parser's strip removes the pad rather than the content's own spaces, and
the empty item keeps its place as a marker and a space.

**Accessor functions for contracts:**

<!-- vera:skip-parse category="FUTURE" reason="md_has_heading" -->
```
public fn md_has_heading(@MdBlock, @Nat -> @Bool)
  requires(@Nat.0 >= 1 && @Nat.0 <= 6)
  ensures(true)
  effects(pure)
```

Returns `true` if the document contains a heading of the given level.

<!-- vera:skip-parse category="FUTURE" reason="md_has_code_block" -->
```
public fn md_has_code_block(@MdBlock, @String -> @Bool)
  requires(true)
  ensures(true)
  effects(pure)
```

Returns `true` if the document contains a code block with the given language tag.

<!-- vera:skip-parse category="FUTURE" reason="md_extract_code_blocks" -->
```
public fn md_extract_code_blocks(@MdBlock, @String -> @Array<String>)
  requires(true)
  ensures(true)
  effects(pure)
```

Extracts the code content from all code blocks with the given language tag. This is the key agent operation: extract code from documentation.

**Refinement type examples:**

Refinement types can express structural requirements on Markdown documents:

```
type HasTitle = { @MdBlock | md_has_heading(@MdBlock.0, 1) };
type HasVeraCode = { @MdBlock | md_has_code_block(@MdBlock.0, "vera") };
```

These predicates call pure functions, placing them in Tier 2 (extended, function calls in contracts). For small documents they may be verifiable by Z3 with function unrolling; for larger documents they fall to Tier 3 (runtime checks).

**Document conversion:**

Document conversion (PDF, Word, HTML, etc. to Markdown) is not part of the language specification. Vera provides the types; conversion uses the `IO` effect with host bindings that delegate to external tools:

<!-- vera:skip-parse category="FUTURE" reason="convert_to_markdown" -->
```
public fn convert_to_markdown(@String -> @Result<MdBlock, String>)
  requires(true)
  ensures(true)
  effects(<IO>)
```

The host runtime can import tools like MarkItDown or pandoc. The WASM module receives a clean `MdBlock` value through the host binding.

**Connection to the Inference effect:**

`Inference.complete()` (Section 9.5.5) returns `Result<String, String>`. Callers compose explicitly to get Markdown:

```
let @Result<String, String> = Inference.complete(
  string_concat("Write a report about: ", @String.0)
);
match @Result<String, String>.0 {
  Ok(@String) -> match md_parse(@String.0) {
    Ok(@MdBlock) -> @MdBlock.0,
    Err(@String) -> MdDocument([MdParagraph([MdText(@String.0)])])
  },
  Err(@String) -> MdDocument([MdParagraph([MdText(@String.0)])])
}
```

This follows the same pattern as JSON: `json_parse(Http.get(url))`, not a dedicated `get_json` operation. One way to do things (§0.2.3).

### 9.7.4 Html

HTML is the primary output format of web applications and the most common document format encountered by agents browsing the web. A typed HTML ADT makes document structure visible to the type system, enabling contracts that verify the structural properties of parsed web pages.

HTML is represented as a single ADT `HtmlNode` with three constructors:

```
public data HtmlNode {
  HtmlElement(String, Map<String, String>, Array<HtmlNode>),
  HtmlText(String),
  HtmlComment(String)
}
```

`HtmlNode` constructors:
- `HtmlElement(@String, @Map<String, String>, @Array<HtmlNode>)` — an HTML element: tag name, attribute map, and child nodes.
- `HtmlText(@String)` — text content within an element.
- `HtmlComment(@String)` — an HTML comment.

**Parse and serialize operations:**

<!-- vera:skip-parse category="FUTURE" reason="html_parse" -->
```
public fn html_parse(@String -> @Result<HtmlNode, String>)
  requires(true)
  ensures(true)
  effects(pure)
```

Parses an HTML string into an `HtmlNode` tree. The parser is lenient (like browsers) — malformed HTML produces a best-effort tree rather than an error. Returns `Err` only on catastrophic parse failures.

<!-- vera:skip-parse category="FUTURE" reason="html_to_string" -->
```
public fn html_to_string(@HtmlNode -> @String)
  requires(true)
  ensures(true)
  effects(pure)
```

Serializes an `HtmlNode` tree back to an HTML string.

**Query and extraction operations:**

<!-- vera:skip-parse category="FUTURE" reason="html_query" -->
```
public fn html_query(@HtmlNode, @String -> @Array<HtmlNode>)
  requires(true)
  ensures(true)
  effects(pure)
```

Queries the tree using a simple CSS selector subset. Returns all matching elements. Supported selectors: tag name (`div`), class (`.classname`), ID (`#id`), attribute presence (`[href]`), and descendant combinator (`div p`).

<!-- vera:skip-parse category="FUTURE" reason="html_text" -->
```
public fn html_text(@HtmlNode -> @String)
  requires(true)
  ensures(true)
  effects(pure)
```

Extracts all text content from the node and its descendants, recursively concatenated. Comments are excluded.

<!-- vera:skip-parse category="FUTURE" reason="html_attr" -->
```
public fn html_attr(@HtmlNode, @String -> @Option<String>)
  requires(true)
  ensures(true)
  effects(pure)
```

Returns the value of the named attribute if the node is an `HtmlElement` with that attribute present. Returns `None` for `HtmlText`, `HtmlComment`, or missing attributes. This is a pure Vera function (prelude-injected), not a host import.

**Design note.** The `HtmlNode` ADT is intentionally simple compared to a full DOM. It captures the structural essence of HTML documents without modeling CSS, JavaScript, or DOM events. This matches the agent use case: extract structured information from web pages.

## 9.8 Abilities

> **Status: Implemented.** Tracked in [#60](https://github.com/aallan/vera/issues/60). Four built-in abilities (`Eq`, `Ord`, `Hash`, `Show`) are fully compilable. Supported types: Int, Nat, Bool, Float64, String, Byte, Unit. `Eq` derivation is **structural** ([#773](https://github.com/aallan/vera/issues/773)): a simple enum, or an ADT every field of which is itself `Eq` — an `Eq` primitive (`String` included, compared by content) or a nested `Eq` ADT (compared recursively, including recursive types) — supports `Eq` automatically. Fields with no `Eq` semantics (`Array`, `Map`, host handles) make the ADT non-derivable. `Show` and `Hash` derive **structurally** for composite types too ([#911](https://github.com/aallan/vera/issues/911)) — ADT, `Tuple`, `Option`, `Result`, and `Array`, recursing into each field/element by its own `show`/`hash` (see §9.8.2) — including directly-recursive ADTs (`List<T>`, `Tree<T>`), which lower to a generated self-calling helper ([#924](https://github.com/aallan/vera/issues/924)). The built-in `Ordering` ADT (`Less`, `Equal`, `Greater`) is available for `Ord`'s `compare` operation.

Vera supports restricted abilities for constraining type variables in generic functions. To support practical generic programming — sorting, hashing, serialisation — type variables need constraints. Vera adopts restricted abilities rather than full typeclasses:

```
ability Eq<T> {
  op eq(T, T -> Bool);
}

ability Ord<T> {
  op compare(T, T -> Ordering);
}

public forall<T where Eq<T>> fn contains(@Array<T>, @T -> @Bool)
  requires(true)
  ensures(true)
  effects(pure)
{
  exists(@Nat, array_length(@Array<T>.0), fn(@Nat -> @Bool) effects(pure) {
    eq(@Array<T>.0[@Nat.0], @T.0)
  })
}
```

Key design points:

1. **No higher-kinded types.** No `Functor`, `Monad`, or `Applicative`. Abilities are first-order only: `Eq<T>`, not `Mappable<F>` where `F` is a type constructor. This preserves decidable type checking and prevents the abstraction hierarchy that makes code harder for LLMs to generate correctly.

2. **Built-in abilities** are auto-derivable for ADTs composed of types that already support them: `Eq`, `Ord`, `Hash`, `Encode`, `Decode`, `Show`. If all fields of an ADT support `Eq`, the ADT supports `Eq` automatically. Four abilities are currently built-in: `Eq`, `Ord`, `Hash`, and `Show`.

3. **User-defined abilities** are permitted but restricted to first-order type parameters. This allows library authors to define domain-specific abilities without the complexity of higher-kinded polymorphism.

4. **`ability` declarations** look like `effect` declarations (using `op` for operations), keeping the language syntactically consistent.

5. **Constraint syntax** uses `forall<T where Ability<T>>`, consistent with the placeholder noted in Chapter 2, Section 2.7.1.

This design draws on Roc's abilities (deliberately no HKTs, auto-derivable) and Gleam's validation that useful languages need not have typeclasses.

### 9.8.1 Built-in Abilities

Four abilities are built into the language. Each is auto-satisfied for primitive types and (where noted) for ADTs composed of satisfying types.

**Eq\<T\>** — Equality comparison.

```
ability Eq<T> {
  op eq(T, T -> Bool);
}
```

Operation: `eq(@T, @T -> @Bool)`. Returns `true` if the two values are structurally equal.

Satisfied by: Int, Nat, Bool, Float64, String, Byte, Unit, and ADTs whose constructors contain only Eq-satisfying field types (auto-derivation). Simple enums (all-nullary constructors) always satisfy Eq.

**Ord\<T\>** — Ordering comparison.

```
ability Ord<T> {
  op compare(T, T -> Ordering);
}
```

Operation: `compare(@T, @T -> @Ordering)`. Returns `Less`, `Equal`, or `Greater`.

The `Ordering` ADT is a built-in type:

```
public data Ordering {
  Less,
  Equal,
  Greater
}
```

Satisfied by: Int, Nat, Float64, Byte, String — exactly the orderable types on which the ordering operators `<` / `>` / `<=` / `>=` are defined (Chapter 4, Section 4.5). `compare` is the ability spelling of the three-way if-chain `a < b ? Less : (a == b ? Equal : Greater)` (Chapter 6, Section 6.4), so it shares that domain. A user-defined ADT is **not** Ord-derivable (unlike `Eq` / `Hash` / `Show`, which derive structurally for composite types) — it has no defined total order, and neither does `Bool`. `compare` on a non-orderable operand (any ADT, or `Bool`) is rejected at check time with E242, mirroring the E143 rejection of a direct `<` on the same operand ([#921](https://github.com/aallan/vera/issues/921)).

**Hash\<T\>** — Hashing.

```
ability Hash<T> {
  op hash(T -> Int);
}
```

Operation: `hash(@T -> @Int)`. Returns a deterministic integer hash of the value.

Satisfied by: Int, Nat, Bool, Float64, String, Byte, Unit, and composite types — ADTs, `Tuple`, `Option`, `Result`, and `Array` — whose fields/elements are themselves `Hash`-satisfying (structural auto-derivation, §9.8.2).

**Show\<T\>** — String representation.

```
ability Show<T> {
  op show(T -> String);
}
```

Operation: `show(@T -> @String)`. Returns a human-readable string representation.

Satisfied by: Int, Nat, Bool, Float64, String, Byte, Unit, and composite types — ADTs, `Tuple`, `Option`, `Result`, and `Array` — whose fields/elements are themselves `Show`-satisfying (structural auto-derivation, §9.8.2).

`show(@Float64)` is backed by `float_to_string` and is therefore **total** over all `Float64` values: the non-finite classes render as `"nan"`, `"inf"`, and `"-inf"` (§9.6.11, [#857](https://github.com/aallan/vera/issues/857)), with the same spellings in both the Python and browser runtimes.

### 9.8.2 ADT Auto-Derivation

For `Eq`, ADTs are automatically derivable when all constructor fields are Eq-satisfying types. The compiler generates structural equality: compare tags first, then compare fields pairwise.

Simple enums (ADTs with only nullary constructors) always satisfy `Eq` — equality reduces to tag comparison.

ADTs with `String` fields derive `Eq` by content, and nested-ADT fields recurse into the nested ADT's own equality — including recursive and mutually-recursive types ([#773](https://github.com/aallan/vera/issues/773)). `Array`, `Map`, `Set`, host-handle, function, and tuple fields remain non-derivable. `==` / `!=` (and the `eq` ability operation) is the surface spelling of `Eq`, so a non-Eq-derivable operand — a function value, an `Array` / `Map` / `Set` / `Tuple`, or a composite carrying such a field — is rejected at check time with E243 ([#928](https://github.com/aallan/vera/issues/928)), mirroring the E242 rejection of `compare` / ordering on a non-orderable operand. An `Eq` constraint over a non-derivable type on the generic path is likewise rejected, with E613 at monomorphization.

`Show` and `Hash` also derive **structurally** for composite types ([#911](https://github.com/aallan/vera/issues/911)) — user ADTs, `Tuple`, `Option`, `Result`, and `Array` — recursing into each field/element by its own `show`/`hash`.

`show` renders a composite value using its constructor syntax:

| Type | Rendering |
|------|-----------|
| ADT nullary constructor | `Ctor` (bare name) |
| ADT with fields | `Ctor(f0, f1, …)` — each field by its own `show` |
| `Tuple` | `(a, b, …)` |
| `Option` | `Some(x)` / `None` |
| `Result` | `Ok(x)` / `Err(e)` |
| `Array` | `[e0, e1, …]` (empty: `[]`) |

Fields are separated by `, ` (comma + space). A `String` field renders as its raw content (no surrounding quotes), consistent with `show` on a `String` being the identity. Nesting recurses to arbitrary finite depth (ADT-of-ADT, `Option`-of-`Tuple`, `Array`-of-composite).

`hash` on a composite is deterministic: it seeds with the constructor tag (or, for an `Array`, its length) and folds each field/element hash in FNV-style, so distinct constructors and distinct field values hash differently.

A directly self-referential recursive ADT (`List<T>`, `Tree<T>`) `show`/`hash`es via a **generated self-calling helper function** ([#924](https://github.com/aallan/vera/issues/924)) — one `$show_<type>` / `$hash_<type>` per recursive type, recursing over the finite value at run time (mirroring how structural `Eq` derives one `$eq_<type>` helper). A composite whose element/field types still cannot be resolved at the `show`/`hash` site — e.g. a *generic* mutually-recursive ADT whose type argument is buried in a nested generic field (`Grove(Rose<T>, Forest<T>)`), the same type-argument-recovery limitation `Eq` shares — is skipped rather than mis-rendered.

### 9.8.3 Compilation Strategy

Ability operations are compiled via two mechanisms:

1. **AST-level rewriting** (Pass 1.6): `eq(a, b)` is rewritten to `a == b`, and `compare(a, b)` is rewritten to `if a < b then Less else if a == b then Equal else Greater`. This reuses existing comparison codegen.

2. **WASM-level dispatch**: `show(x)` and `hash(x)` are dispatched at WASM generation time based on the inferred type of the argument, routing to type-specific implementations (e.g., `to_string` for Int, FNV-1a for String hashing). For a composite argument the dispatch recurses over the value's layout — tag at offset 0, then each field at its concrete offset — rendering / folding each field by its own `show`/`hash`, the same structural traversal `Eq` uses.

## 9.9 Limitations

The standard library and built-in effects have the following limitations, each tracked as a GitHub issue:

| Limitation | Issue |
|-----------|-------|
| No date or time handling beyond `IO.time` — no ISO 8601 parsing, formatting, or arithmetic | [#233](https://github.com/aallan/vera/issues/233) |
| No cryptographic primitives (hashing, HMAC) | [#235](https://github.com/aallan/vera/issues/235) |
| No CSV parsing or generation | [#236](https://github.com/aallan/vera/issues/236) |
| `Http`: fixed request headers — no custom header support | [#351](https://github.com/aallan/vera/issues/351) |
| `Http`: response status codes are not accessible | [#352](https://github.com/aallan/vera/issues/352) |
| `Http`: no per-request timeout control | [#353](https://github.com/aallan/vera/issues/353) |
| `Http`: browser runtime uses deprecated synchronous XMLHttpRequest | [#355](https://github.com/aallan/vera/issues/355) |
| `Http`: GET and POST only — no PUT, PATCH, or DELETE | [#356](https://github.com/aallan/vera/issues/356) |
| `Inference.complete`: `max_tokens` and `temperature` are not configurable | [#370](https://github.com/aallan/vera/issues/370) |
| `Inference`: no `embed` operation (vector embeddings) | [#371](https://github.com/aallan/vera/issues/371) |
| `Inference`: no user-defined handlers — `handle[Inference]` is rejected | [#372](https://github.com/aallan/vera/issues/372) |
| Host imports cannot return `Array<Float64>` (`alloc_result_ok_float_array` infrastructure) | [#373](https://github.com/aallan/vera/issues/373) |