# Aver — Deep Documentation Index

> Start with [`llms.txt`](https://averlang.dev/llms.txt). This file is the deeper companion: the toolchain in full plus a routing index for language docs, examples, and implementation context.

## Recommended read order

1. [`llms.txt`](https://averlang.dev/llms.txt) for syntax guardrails and the minimal working shape of an Aver file
2. [Language Guide](https://github.com/jasisz/aver/blob/main/docs/language.md) for the full surface-language contract
3. [Services (stdlib)](https://github.com/jasisz/aver/blob/main/docs/services.md) for stdlib and effect namespaces
4. one or two raw `.av` examples close to your task
5. [`AGENTS.md`](https://github.com/jasisz/aver/blob/main/AGENTS.md) only if you need repository internals or implementation details

## Primary docs

- [Language Guide](https://github.com/jasisz/aver/blob/main/docs/language.md) — complete surface-language reference
- [Services (stdlib)](https://github.com/jasisz/aver/blob/main/docs/services.md) — every namespace and its API
- [Common Pushback](https://github.com/jasisz/aver/blob/main/docs/pushback.md) — questions, objections, honest answers

## Advanced topics

- [Independence (`?!`)](https://github.com/jasisz/aver/blob/main/docs/independence.md) — parallel products
- [Constructors](https://github.com/jasisz/aver/blob/main/docs/constructors.md) — constructor routing rules
- [Oracle](https://github.com/jasisz/aver/blob/main/docs/oracle.md) — proof export for classified effectful functions via `verify fn trace` + `given` stubs, plus `--hostile`
- [Lean proof export](https://github.com/jasisz/aver/blob/main/docs/lean.md) — verify blocks to Lean 4
- [Dafny verification](https://github.com/jasisz/aver/blob/main/docs/dafny.md) — verify laws to Dafny / Z3
- [WASM backend](https://github.com/jasisz/aver/blob/main/docs/wasm.md) — browser compilation

## Canonical examples

- [Hello](https://github.com/jasisz/aver/blob/main/examples/core/hello.av) — minimal pure file
- [Calculator](https://github.com/jasisz/aver/blob/main/examples/core/calculator.av) — verify on basic arithmetic
- [Independent Fan-out](https://github.com/jasisz/aver/blob/main/examples/core/independent_fanout.av) — `!` / `?!` independent products
- [Quicksort](https://github.com/jasisz/aver/blob/main/examples/data/quicksort.av) — recursion + verify on a recursive algorithm
- [Oracle Trace](https://github.com/jasisz/aver/blob/main/examples/formal/oracle_trace.av) — `verify fn trace` with `given` stubs for classified effects


## Toolchain

## Main commands

### Run

```bash
aver run file.av
aver run file.av --module-root .
aver run file.av -- arg1 arg2 arg3
```

- Aver program args are available through `Args.get()`
- `--record <dir>` records effect traces for replay

### Check

```bash
aver check file-or-dir --module-root . --deps
```

`check` handles static contract diagnostics:
- missing `intent =`
- missing `?` descriptions on relevant functions
- missing `verify` on pure, non-trivial, non-`main` functions
- coverage-style warnings for thin `verify` examples
- file size warnings

Warnings do not make `check` fail.

### Verify

```bash
aver verify file-or-dir --module-root . --deps
aver verify file-or-dir --wasm-gc
```

`verify` runs only declared `left => right` examples.
It fails on:
- mismatched examples
- parse/type errors
- execution errors

It is not a coverage tool.

`--wasm-gc` (0.17.3+) executes the same cases via the wasm-gc backend instead of the VM — cross-target check that catches divergence between VM and wasm-gc codegen on equality. The host decodes a single Bool per case (wasm-gc lowers `==` per-type via eq_helpers natively). Failure diagnostics show the actual runtime value for primitive return types (Int/Float/Bool/Str). Trace projections (`.trace.*`), classified-effect Oracle stubs (`given X: Time = stub`), and case bodies mentioning `BranchPath` are rejected upfront with a pointer back to VM verify — those features depend on namespace-value dispatch and runtime override that the wasm-gc backend doesn't have yet.

### Format

```bash
aver format .
aver format examples
aver format examples --check
```

`format` accepts files or directories and walks `.av` files recursively.

### Audit

```bash
aver audit file-or-dir --module-root . --deps
```

`audit` is the single-shot CI gate that runs all three axes at once:

1. static checks (same diagnostics as `check`)
2. `verify` execution (same as `verify`)
3. `format --check` (structural compliance)

Output is a flat list of `error[slug]:` / `warning[slug]:` lines plus a
summary footer: `N files | X check errors | Y verify failures | Z format`.
Any non-zero count fails the command.

- warnings (e.g. `independence-hazard`, `non-tail-recursion`) do not fail
  the audit — they are advisory
- errors come from the same machinery as `check` / `verify` / `format`, so
  slugs are stable and match `docs/diagnostics-slugs.md`
- prefer `aver audit` over chaining `check && verify && format --check` —
  it runs the pipeline once and reports everything in one place

Use it before showing a snippet to the user or committing docs examples;
it catches illegal `?!` usages, match-arm body-on-next-line parse errors,
and effect-type mismatches that a naked `aver run` can miss when the VM
short-circuits on the first failure.

`--hostile` (0.13+) layers adversarial worlds on top of every
`verify <fn> law` block — typed `given`s get type-boundary values,
classified effects get hostile profiles. Failures use the separate
slug `verify-hostile-mismatch` so CI can route declared-world vs
adversarial-world regressions to different channels.

### Context

```bash
aver context file.av --module-root .
```

Default:
- `--depth auto`
- `--budget 10kb`

This is the preferred AI discovery workflow:

1. start with a small budget
2. inspect the architecture map
3. look at selection metadata
4. zoom in only where needed

Examples:

```bash
aver context examples/modules/app.av --budget 10kb
aver context projects/workflow_engine/main.av --module-root projects/workflow_engine --budget 24kb
aver context projects/workflow_engine/main.av --module-root projects/workflow_engine --json --budget 24kb --output projects/workflow_engine/CONTEXT.json
```

Notes:
- `--depth N` and `--depth unlimited` bypass the auto-budget behavior
- `--decisions-only` exports only `decision` blocks
- selection metadata is printed to stdout and embedded in JSON output

### Compile

```bash
aver compile file.av -o /tmp/out --module-root .
aver compile file.av --target wasm-gc -o /tmp/out
aver compile file.av --target wasm-gc --optimize size -o /tmp/out
aver compile file.av --preset cloudflare --handler handler -o /tmp/out
aver compile file.av --emit-ir-after=PASS
aver compile file.av --explain-passes
```

- Default: Rust codegen, emits a modular Cargo project
- `--target wasm-gc`: native WebAssembly GC + tail-call output (recommended). Self-contained binary, engine handles GC/recursion, per-instantiation helpers DCE'd to what each program calls. Modern host baseline (Chrome 119+, Firefox 120+, Safari 18.2+, wasmtime 25+, Node 22+).
- `--target wasm`: legacy fallback for pre-2024 hosts. Bundles a custom NaN-boxed runtime via `wasm-merge`.
- `--optimize size|speed`: post-process with binaryen `-Oz` (size) or `-O3` (speed).
- `--preset cloudflare --handler <fn>`: Cloudflare Workers pack — `--target wasm-gc --pack cloudflare`, drops `worker.js` + `wrangler.toml` next to the wasm. `<fn>` must have signature `Fn(HttpRequest) -> HttpResponse`.
- `--emit-ir-after=PASS`: print the IR snapshot after the named pipeline stage and exit before codegen. PASS ∈ { `parse`, `tco`, `typecheck`, `interp_lower`, `buffer_build`, `resolve`, `last_use`, `analyze` }. `diff -u` between two stages shows exactly what each pass rewrote.
- `--explain-passes`: run the full pipeline (no codegen) and print a per-pass diagnostic report — tail-call conversions, interpolations lowered, fusion sites rewritten + sinks synthesized, slots resolved, last-use markers annotated, alloc/recursion facts. Drives failable-invariant CI checks ("fail if buffer_build no longer fires on the canonical shape", "fail if hot fn loses no-alloc status"). Pair with `--json` for typed-per-stage shape: `{schema_version: 1, passes: [{stage, data: {...stage-specific fields}}, ...]}` — buffer_build's `data` exposes `rewrites`, `synthesized`, `sinks`, `rewrites_by_sink`; analyze's exposes `total_fns`, `no_alloc_fns`, `recursive_fns`, `mutual_tco_members`. `jq '.passes[] | select(.stage=="buffer_build") | .data.rewrites'` instead of regex-parsing summary strings.

### Bench

```bash
aver bench foo.av                                            # ad-hoc, defaults (30 iter, 3 warmup)
aver bench foo.av --iterations=50 --warmup=5                 # ad-hoc with overrides
aver bench bench/scenarios/fib.toml                          # named manifest
aver bench bench/scenarios/fib.toml --json                   # structured report
aver bench bench/scenarios/                                  # directory mode (every *.toml)
aver bench bench/scenarios/ --json                           # NDJSON
aver bench bench/scenarios/fib.toml --target=wasm-local      # requires --features wasm
aver bench bench/scenarios/fib.toml --target=rust            # native binary, subprocess per iter
aver bench bench/scenarios/fib.toml --save-baseline base.json
aver bench bench/scenarios/fib.toml --compare base.json --fail-on-regression
aver bench bench/scenarios/ --save-baseline bench/baselines/<host>-<arch>-vm.json   # capture baseline (NDJSON)
aver bench bench/scenarios/ --baseline-dir bench/baselines/ --fail-on-regression   # CI gate
```

- Three input shapes: `.av` (ad-hoc, defaults + `--iterations` / `--warmup` overrides), `.toml` (named manifest with per-scenario tolerance + expected shape), directory (globs `*.toml`).
- Three targets: `vm` (default, in-process), `wasm-local` (wasmtime in-process), `rust` (native binary).
- Reports include `backend` (aver version, build, wasmtime version) and `host` (os/arch/cpus) so cross-machine runs disambiguate.
- `--save-baseline` works in both single-scenario (pretty JSON) and directory (NDJSON) mode. `--compare` is single-scenario only.
- `--baseline-dir DIR` auto-picks `<host.os>-<host.arch>-<backend.name>.json` from `DIR`. Silent skip when no matching baseline exists — single workflow gates wherever a baseline is pinned. CI uses this.
- See [docs/bench.md](docs/bench.md) for the full reference.

### Proof

```bash
aver proof file.av -o /tmp/proof --module-root . --verify-mode auto
```

Lean export modes:
- `auto`
- `sorry`
- `theorem-skeleton`

### Replay

```bash
aver replay recordings/ --test --diff
```

Use replay for effectful debugging and regression capture.

## Recommended workflows

### Logic bug

1. add or tighten a `verify`
2. run `aver verify ...`
3. fix code
4. keep the example

### Effect bug

1. run with `--record`
2. inspect replay artifact
3. run `aver replay ... --test --diff`

### Project discovery

1. `aver context <entry> --budget 10kb`
2. if needed, raise budget or target a specific module
3. only then open raw source files

## aver.toml

Project-level config (deployment guardrails + check tweaks):

```toml
[effects.Http]
hosts = ["api.example.com", "*.internal.corp"]

[effects.Disk]
paths = ["./data/**"]

[effects.Env]
keys = ["APP_*", "TOKEN"]

[[check.suppress]]
slug = "non-tail-recursion"
files = ["**/eval/**"]
reason = "Tree-walking interpreter — CPS would destroy correspondence."
```

Effect-host / path / key allowlists narrow which hosts, files, and env keys the runtime will admit. `[[check.suppress]]` lets a project waive specific lint slugs in specific paths with a reason.