Aver 0.11.0

Effectful functions get verified now — bind an oracle with given, check the trace, or export the universal law to Lean & Dafny. Dafny caught up with Lean across every recursive shape.

Added

• Oracle law and trace docs/example — docs/oracle.md now separates proof-oriented verify <fn> law over explicit oracles from cases-form verify <fn> trace for .result / .trace.* assertions. Added examples/formal/oracle_trace.av as the short runnable example.
• Broader Oracle effect classification — Oracle now covers CLI input (Console.readLine), disk operation/result effects, one-shot TCP (Tcp.send / Tcp.ping), Time.sleep, and terminal trace/input calls that do not depend on modal terminal state.
• Dafny proof backend reaches feature parity with Lean on recursion. Shared recursion classifier (codegen::recursion::detect) + AST transform now feed both backends. Dafny emits mutual-recursion SCCs as fuel-guarded function fn__fuel(fuel: nat, …) decreases fuel { … } pairs with plan-specific metrics, parallel to Lean's def fn__fuel (fuel : Nat) …. Shapes that admit no total default or use ? that doesn't lower fall back to function {:axiom} — the Dafny analogue of Lean's partial def. Lemmas over opaque fns short-circuit to assume {:axiom} <ensures>;, the Dafny analogue of Lean's sorry. Across the 23 canonical examples: 12 are clean on both backends (full proof), 9 have matching proof gaps (Dafny axiom/assume vs. Lean sorry), 2 are pre-existing codegen gaps orthogonal to the recursion story.

Changed

• Effectful verification story — README, language guide, and proof-backend docs now distinguish Oracle verification for classified effects from record/replay for ambient state, persistent protocols, terminal modes, and server callbacks.
• codegen::recursion module — RecursionPlan enum, ProofModeIssue, recursion classifier, and rewrite_recursive_calls_{body,expr} AST transform pulled out of codegen::lean into the shared module. Lean and Dafny both consume it. RecursionPlan::IntAscending now holds the bound as an Aver AST node (Spanned<Expr>) instead of a Lean-rendered string — each backend renders it in its own idiom.

Aver 0.10.1

Added

• aver run --expr '<call>' / --input-file PATH — record or run any function, not just main. Pass a call like aver run src/tax.av -e 'loadTaxRate("PL")' --record dir/ and the recording's entry_fn and input are populated from the call; aver replay picks it up unchanged. Repeat -e to batch. Supports literal, list/tuple, and ADT-constructor arguments (Result.Ok(5), Shape.Circle(1.0), nested). Function calls / arithmetic / variables in arg position stay out of scope — wrap them in a helper function and call that instead. The same capability is exposed in the playground's Trace panel.

Aver 0.10.0 "Telltale"

Tooling now shows its work — parse errors point at the exact token with a repair, audit runs three axes in one shot, and every program can be recorded & replayed in the browser.

Added

• aver audit — one command that runs static checks, verify blocks, and format compliance together. CI-friendly exit code, --json for pipelines.
• aver format --check / aver format --check --json — non-mutating format verification. Every rewrite reports a structured FormatViolation with a stable rule slug: tab-indent, bad-function-header, effects-unsorted, effects-reshape, verify-misplaced, excess-blank, module-intent-reshape, decision-inline, trailing-whitespace, missing-final-newline. Agents and linters can key off specific rules instead of free-text diffs.
• Naming convention checker — flags non-camelCase functions / fields and non-PascalCase types / modules / variants as stable diagnostics (bad-fn-name, bad-type-name, bad-module-name, bad-variant-name, bad-field-name). Runs as part of aver check and aver audit.
• Canonical diagnostic bundle across every CLI command — aver check --json, aver verify --json, aver why --json, aver audit --json, aver format --check --json all emit AnalysisReport NDJSON now. One schema, schema_version: 1, documented in docs/diagnostics-schema.md.
• Reworked browser playground — multi-file editor, interactive record & replay, full parity with CLI audit / why / context / format. Go play.

Changed

• Format engine rewritten around structured violations — the formatter used to report "needs format" as opaque before/after diffs. Every normalization pass now tracks per-line rule violations with original source-line numbers, so --check output points at the exact line that needs the specific fix instead of dumping a reformatted file. needs-format stays as the aggregate marker; each FormatViolation rides alongside with its rule slug.
• Effects list in aver context — signature is now params + return type only; effects live on the sibling effects array. Lets renderers show them without duplicating ! [...] on screen.

Fixed

• Parse errors landed on line 1:1 with no hint — the formatter stripped the real span and emitted a single red line that didn't tell you where or why. Now: real line/col pulled from the parser, source snippet with ^^^ caret under the offending token (clamped to the last char for EOL errors like Unterminated string), and repair hints for common shapes (Expected '[' after '!' → ! [Console.print, ...], missing module <Name>, map => syntax, tuple-needs-2-elements, …).
• Time.sleep on wasm32-unknown-unknown panicked ("can't sleep") — the browser runtime now makes it a no-op; native builds keep real blocking sleep.

Aver 0.9.7

Changed

• Pre-compiled self-host — --self-host no longer generates Rust code and runs cargo build at runtime. The self-host interpreter is compiled as a [[bin]] target alongside aver, so cargo install aver-lang provides both binaries out of the box. No Rust toolchain needed at runtime.
• Cargo package cleanup — published crate excludes self_hosted/, examples/, tools/, editors/, etc. Only src/ and essentials ship. Self-host generated code lives in src/self_host/.

Added

• Release script (tools/release.py) — automates version bumps, self-host regeneration, playground rebuild, crates.io publish, and GitHub release creation.

Fixed

• --self-host crash from crates.io install — the runtime codegen tried to read aver-rt/Cargo.toml relative to the installed crate source, which doesn't exist. Eliminated by removing runtime codegen entirely.
• Rust codegen: TCO invariant hoisting of variant constructors — enum variant constructors (e.g., Val::ValStr) were hoisted as loop invariants, causing move errors in generated Rust. Now excluded alongside builtins.

Removed

• Runtime codegen pipeline for self-host (build_self_host_binary, fingerprinting, cargo build --offline invocation).

Aver 0.9.6

Performance

• VECTOR_SET_OR_KEEP in-place mutation — fused Option.withDefault(Vector.set(v, i, val), v) always has sole ownership; the opcode now mutates the vector directly at its arena slot. Vector get/set 5k: 17ms → 816µs (20× faster).
• Skip promotion rewrite for bulk types without young refs — vectors/maps/tuples of inline ints skip O(n) per-element rewrite during young→yard promotion. Vector get/set 5k: 17ms → 12.6ms (−26%).
• VM arena in-place map rewrite — map promotion rewrites NanValue pairs in-place via Rc::make_mut instead of rebuilding the HashMap. Map build 5k: 24ms → 1.3ms (18.9×). COW ops inherit source allocation space, skipping redundant promotion.

Changed

• Unified symbol resolution for uppercase dotted paths — classify_leaf_op now classifies uppercase Expr::Attr paths (Option.None, variant constructors, module function refs) via three new LeafOp variants instead of returning None. Eliminates duplicate resolution logic from Rust and WASM backends. WASM backend now routes Expr::Attr through the shared IR layer.

Added

• WASM Option.toResult builtin — Some(v) → Ok(v), None → Err(err_value).

Fixed

• WASM cross-module variant constructor resolution — hierarchical module paths like Domain.Types.TaskStatus.Blocked now resolve correctly (previously only single-level bases worked).
• Rust codegen: TCO invariant hoisting of builtin callees — List.prepend and similar builtin namespace refs were hoisted as standalone value expressions, generating invalid Rust. Now excluded from hoisting since they're compile-time constants.

Removed

• Dead entry_has_young_refs function.

0.9.5

Changed

• Shared symbol layer — module visibility, type registration, and symbol resolution now go through a single shared layer (src/visibility.rs). All backends consume the same ModuleExports and SymbolRegistry instead of building their own views.
• Unified module loader — load_module_tree() replaces independent loaders in the VM compiler and type checker. Proper circular-import detection and module-name validation everywhere.

Fixed

• WASM codegen wrong types for private module helpers — dependency modules with private functions returning non-Int types (e.g. padTwo returning String) caused invalid WASM. Codegen now has full signatures for all emitted functions.
• Rust codegen missing Arc::new() for cross-module recursive types — self-host binary failed to compile from a clean cache (175 type errors). Constructor boxed-position lookup now handles qualified names.

Removed

• Suffix-matching heuristic in VM type resolution
• Dual-key registration in type checker (replaced by alias-based lookup)
• Checker's ModuleSigCache and cycle-detection stack (handled by shared loader)

v0.9.4 — Fix Rust codegen forwarded argument crash

Fixed

• Rust codegen crash with forwarded arguments — aver compile and aver run --self-host failed on programs with forwarded local variables after the unified resolver change in 0.9.3.

v0.9.2 — WASM mutual TCO memory fix

Fixed

• WASM mutual TCO memory leak — dead temporaries accumulated across iterations in mutual tail-call loops. Replaced per-iteration skip threshold with watermark-based adaptive compaction. Game of Life editor loop now stable at ~15KB instead of growing to 10+ MB.

Added

• $heap_ptr WASM export — modules export the bump allocator position for host-side memory inspection.
• Playground memory display — live heap usage shown in status bar.
• Playground rogue touch controls — added descend stairs (>) button.

v0.9.1 — Aver Playground

Added

• Aver Playground — write and run Aver in the browser at averlang.dev. In-browser compiler, 7 playable games, source viewer, syntax highlighting.

Fixed

• WASM variant equality — nullary variants compare correctly.
• WASM variant display — shows type names instead of Variant#0.
• WASM Console.readLine — properly wrapped in Result.Ok, blocking via SharedArrayBuffer.

v0.9.0 — VM-only backend

Changed

• VM is the default backend — aver run, verify, replay, and repl now use the bytecode VM directly. The --vm flag is no longer needed and has been removed.

Removed

• Tree-walking interpreter — ~7500 lines removed. The VM covers all use cases the interpreter handled.

Added

• WASM backend — aver compile --target wasm and aver run --wasm. Own aver/* import ABI with --adapter wasi for standalone wasmtime. Works with built-in host, browser JS shim, or custom host.
• Browser WASM runner — tools/wasm-runner/ with terminal canvas rendering and keyboard input.
• aver-memory crate — standalone NaN-boxed value representation and arena allocator.