Aver 0.15.2 "Traversal"

Every pipeline pass exposes its decisions through one typed shape; bench reports gain the metrics that make regressions catchable; CI gates them per-host without per-runner branching.

Added

• aver compile --explain-passes [--json] — typed per-pass diagnostic report (TCO conversions, interpolations lowered, fusion sites + sinks fired, slots resolved, alloc/recursion facts). JSON shape is one {stage, data} block per pass with stage-specific fields; schema_version: 1 pins the contract for CI gates (tests/explain_passes_spec.rs).
• aver bench populates compiler_visible_allocs (IR-level via NeutralAllocPolicy, same across all three targets) and response_bytes (vm: rendered return value via aver_display; wasm-local: fd_write iovec sum; rust: subprocess stdout). --compare gates both as exact-match alongside p50/p95.
• aver bench --baseline-dir DIR auto-picks <host.os>-<host.arch>-<backend.name>.json; silent skip when no match. Directory mode supports --save-baseline (NDJSON, same shape --baseline-dir reads) — bench/baselines/macos-aarch64-vm.json ships as the reference.
• GitHub Actions Bench Gate job runs aver bench bench/scenarios/ --target=vm --baseline-dir bench/baselines/ --fail-on-regression on every PR; results upload as 30-day artifact.

Changed

• PipelineResult.buffer_build is now a typed BufferBuildPassReport (sinks, synthesized fns, per-sink rewrite counts) instead of an opaque (usize, usize) tuple.
• aver check no longer prints the ↻ N buffer-build sink(s) […] summary — same data with richer detail is now in aver compile --explain-passes.

Aver 0.15.1 "Traversal"

The compiler grew a real pipeline. Every IR transform is a named ordered stage, every consumer reads derived facts from one place, every backend's relationship to the IR is a documented contract.

Added

• Ordered 7-stage pipeline (tco → typecheck → interp_lower → buffer_build → resolve → last_use → analyze) as the single source of truth, with per-stage public functions and per-stage PipelineConfig flags.
• Analyze stage centralises five ad-hoc IR analyses (alloc info, mutual-TCO membership, recursive fns, callsite counts, body classification) into one PipelineResult.analysis codegen reads from.
• LastUse stage split out of the resolver — <name:last> markers in IR dump show which slots VM/Rust/WASM MOVE instead of COPY.
• aver compile --emit-ir-after=PASS prints the IR snapshot after any pipeline stage; diff -u between two stages shows exactly what each pass rewrote.
• aver bench scenario harness with three targets (vm / wasm-local / rust), TOML manifests, NDJSON for batch runs, --save-baseline / --compare / --fail-on-regression, and backend + host identity blocks in every report. Thirteen scenarios shared with cargo bench via include_str!. See docs/bench.md.

Fixed

• Proof export traversal leak. Dep modules ignored the proof-export flag and ran deforestation anyway, leaking synthesized <fn>__buffered variants into Lean/Dafny output.
• Playground bypassed deforestation. Browser-compiled WASM/Rust artifacts were measurably slower than equivalent CLI compiles. All playground compile / replay / record paths now use the canonical pipeline.

Changed

• PipelineConfig is per-stage booleans. No bundled apply_traversal_lowering knob; stop_after removed. Caller-level proof-vs-runtime distinction translates to per-stage flags at the CLI boundary.
• pipeline::* is the single entry point for IR transforms and analyses — direct calls to tco::transform_program / resolver::resolve_program / run_type_check_full etc. are gone from production and tests.
• Codegen consumers read derived facts from PipelineResult.analysis / CodegenContext instead of recomputing. Aver's module DAG makes per-module unions sound (cross-module SCCs are mathematically impossible — pinned in src/ir/analyze.rs doc and memory).
• VM compile API consolidated. All three entry points take analysis: Option<&AnalysisResult> as a peer parameter; no _and_analysis variant.

Pipeline contract (new)

• WASM and Rust codegen no longer handle Expr::InterpolatedStr — interp_lower is now a mandatory predecessor stage. ~100 lines of dead code + helper enums deleted, replaced with unreachable!() + contract comments.
• VM keeps its compile_interpolated_str — the REPL is the only legitimate consumer of pre-lower IR.

Aver 0.15.0 "Traversal"

The compiler now eliminates intermediate list traversals it can prove are consumed once — String.join builders, interpolation chains, and external-reverse pipelines fuse to direct buffer writes across all three execution backends.

Added

• Buffer-build deforestation across VM, WASM, and Rust. String.join(<recursive_prepend_builder>(args, []), sep) no longer materialises the intermediate List<String>. The IR-level pass detects the canonical sink shape (match cond { true -> List.reverse(acc); false -> recurse(... List.prepend(elem, acc)) }), synthesizes a <sink>__buffered variant that threads a mutable Buffer through the tail-call chain, and rewrites matching call sites to __buf_finalize(<sink>__buffered(args.., __buf_new(8192), sep)). Each backend then lowers the four __buf_* intrinsics: VM dispatches to dedicated bytecode opcodes (BUFFER_NEW/APPEND_STR/APPEND_SEP_UNLESS_FIRST/FINALIZE) backed by a Vec<Option<String>> pool on the VM struct; Rust uses String::with_capacity + push_str (with Buffer = String aliased in aver-rt); WASM uses an OBJ_BUFFER heap object and rt_buffer_* runtime helpers. Local benches: 8× speedup on Rust (buildLines(500_000, []) → String.join), 2.7× on VM, 24% on WASM under workerd.
• String interpolation lowers through the same buffer pipeline. "a${x}b${y}c" no longer chains str_concat calls — every interpolation goes through a new IR pass (src/ir/interp_lower.rs) that desugars to __buf_finalize(__buf_append(... __buf_new(N), __to_str(x))). Coercion of non-string parts uses a new __to_str intrinsic (VM: CONCAT against empty, Rust: aver_rt::aver_display, WASM: existing emit_value_to_str host bridge). Universal speedup — every Aver program with f-strings benefits, not just the niche of recursive String.join builders. Old O(N²) chained-concat shape (each step allocates a string of cumulative length) becomes O(N + total_len) buffer-write.
• External-reverse builder shape. The buffer-build detector now also matches sinks shaped match list { [] -> acc; [head, ..rest] -> recurse(rest, List.prepend(elem, acc)) } — common in payment_ops / workflow_engine codebases under the *Into naming convention (serializeEntriesInto, filterSubjectInto, renderEventItemsInto). Call sites spelled String.join(List.reverse(<sink>(args, [])), sep) fuse against these. Per-shape kind alignment + acc-position empty-list precondition checked the same way in detection and rewrite, so aver check can't over-report sites the rewrite would refuse.
• Antipattern lints (aver check traversal warnings). Three patterns the deforestation pass deliberately doesn't fuse get surfaced as warnings instead — the fuse-vs-warn split says: silently fuse only when Aver has no idiomatic alternative; warn when it does. Flagged: Vector.fromList(<sink>(args, [])) (suggest Vector.new(N, default) + Option.withDefault(Vector.set(v, i, x), v) owned-mutate fast path), Map.fromList(<sink>(args, [])) (suggest Map.empty() + Map.set chain), and standalone List.reverse(<sink>(args, [])) whose result isn't fed straight into a String.join (the fusion path covers that case; the lint catches sites where the wrapper is something else like renderLines and fusion can't chain through). Acc-position-empty-list precondition checked the same way the rewrite checks it, so the warning never offers broken advice.

Fixed

• Dead HAMT pointer walk in WASM boundary GC. The HAMT runtime was replaced by the flat OBJ_MAP (kind=12) earlier, but the kind=13/15 pointer-walks for HAMT_NODE/HAMT_COLLISION stayed in collect_end and retain_i32. They never fired on main because no live object used those kinds — but Phase 2c reuses kind=13 for OBJ_BUFFER, and the stale walk was treating buffer payload bytes as inner pointers, calling rt_retain_i32/rt_rebase_i32 on garbage. On wasmtime the pseudo-pointers happened to land outside the collect range and were silently passed through; on Cloudflare Workers v8 the layout differed and they corrupted memory mid-collect, surfacing as aver_http_handle threw: RuntimeError: memory access out of bounds. Removing the dead walks fixes it.
• Result.withDefault / Option.withDefault / Option.toResult first-arg validation. All three combinators were registered with Type::Unknown parameters in src/types/checker/builtins.rs, so Result.withDefault(Vector.get(v, i), 0) (Vector.get returns Option<T>, not Result<T, E>) compiled cleanly through aver check and silently returned the default at runtime — every lookup folded to the fallback value with no error surfaced. The special-case handlers in infer/expr.rs already had the right return-type inference but skipped argument validation; they now emit a real type error when the first argument is not the expected wrapper. Type::Unknown still flows through as escape hatch for genuinely polymorphic returns.
• HttpServer.listenWith context-handler type linkage. The second argument (user-defined context) and the handler's first parameter must share the same type — in the weather.av style, both are WeatherContext. The builtin sig leaves context as Type::Unknown (Aver builtins don't carry parametric polymorphism), so the linkage is enforced as a cross-arg check after the standard sig-based validation: extract the handler's Type::Fn first param, compare with the inferred type of the context arg, emit a type error on mismatch. Same logic covers SelfHostRuntime.httpServerListenWith.
• SelfHostRuntime.httpServerListen{,With} handler typing. Both aliases declared their handler parameter as Type::Unknown, so callers could pass an Int where a Fn(HttpRequest) -> HttpResponse was expected and the compile would proceed past type-check. Tightened to http_handler() / http_handler_with_context() to mirror the public HttpServer.listen{,With} shape.

Aver 0.14.2

Added

• Pure no-alloc fast path on both WASM and VM. New shared compute_alloc_info analyzer (src/ir/alloc_info.rs) parametrised by a backend-specific AllocPolicy trait classifies every user fn as allocating or not, walking the call graph to fixpoint. The WASM emitter then skips the prologue heap_ptr save and epilogue rt_truncate for no-alloc bodies; the mutual-TCO trampoline drops its watermark check, per-iter heap_ptr save, and adaptive compaction when every member is no-alloc. The VM compiler tags qualifying chunks so TAIL_CALL_KNOWN / TAIL_CALL_SELF skip finalize_frame_locals_for_tail_call, CALL_KNOWN parks dummy zero marks, and RETURN short-circuits the standard fast-return path. Mandelbrot bench (160×96 × 100 reps × 80 iter, mutual-TCO mandelStep ↔ mandelIter with cardioid + period-2 bulb pre-tests) runs ~4× faster on WASM and ~22% faster on VM. Closes the bulk of the float-tight-loop gap with peer typed-wasm + Cranelift toolchains (down from ~3× slower to ~1.07× slower, apples-to-apples).
• HttpRequest.query: String field for the fetch bridge. req.query returns the URL search string without the leading ? (previously dropped silently — req.body worked but req.query was simply absent from the builtin record). Plumbed through builtin_records.rs, abi.rs (Request.query → request_query), the fetch-bridge field-emit map, the cloudflare worker.js template, and the type-checker's net-request field list. Enables URL-driven server-side state without an extra parser layer.
• Friendly compile-time error for HTTP types under non-fetch bridges. aver compile … --target wasm (no bridge) on a program declaring fn handler(req: HttpRequest) -> HttpResponse previously produced invalid bytecode (type mismatch: expected i64, found i32 deep in the record-shape codegen). The emitter now rejects HttpRequest/HttpResponse parameters/returns under any non-fetch adapter before emit, naming the offending fn and pointing at --preset cloudflare / --bridge fetch.
• /fractal on edge.averlang.dev becomes interactive. Replaces the previous static Braille pair with a single-panel 200×120 half-block Mandelbrot driven by URL query params (cx, cy, w). Per-pixel 16-step colour palette (each cell <i c=XX>▀</i> packs top/bot palette indices into one 2-hex attribute, ~38% smaller HTML than per-cell two-class form). Pan / zoom / reset buttons + six landmark presets (seahorse, mini-Mandelbrot, double spiral, elephant valley, tendrils, eastern bulb) all encode their target view in the URL — every navigation fires a fresh handler invocation with cache-control: no-store, no precomputed images. Iter cap auto-scales (100 / 150 / 250) so deep zooms stay sharp at modest extra compute. Production warm TTFB ~35-40 ms (keep-alive); first hit ~70 ms with TLS handshake.

Changed

• WASM mutual-TCO trampoline collapses to a flat shared slot row when every member has an identical typed signature and is no-alloc (mandelStep ↔ mandelIter style). Per-tail-call args reshape skips its eval → tmp → target double-copy under those conditions and writes args directly into target slots in reverse stack order. Eliminates ~10 local.set per iter from the trampoline hot loop.

Docs

• docs/wasm.md — reframed aver.toml policy as a deliberate host concern, not a missing feature. New "Policy is the Host's Job" section cites wasmtime/WASI --allow-net, Cloudflare Workers services/fetch bindings, browser CSP connect-src, and Fastly Compute backend whitelists as the actual enforcement layers; build-time concerns (effect declarations, deterministic mocks, independence invariants) stay with us.

Tooling

• tools/release.py — GitHub release titles now carry the codename for thematic releases (Aver 0.14.0 "Edge"); patches stay plain. Cascade-bump logic tightened to fire only for genuine publish-blockers (aver-rt → aver-memory); aver-lsp no longer auto-bumps just because aver-lang does.

Aver 0.14.1

Removed

• Header record. 0.14 standardised HTTP headers as Map<String, List<String>> across every backend; the per-entry Header { name, value } record left over from the old List<Header> shape was unreachable from any built-in HTTP type and is now retired. User code that constructed Header literals must now build a Map<String, List<String>> directly.

Fixed

• Http.post / Http.put / Http.patch oracle signature now reports the headers parameter as Map<String, List<String>> instead of the stale List<Header> from the pre-0.14 shape. Verify-mode mocks and effect classification see the correct type.
• Self-host codegen template (--with-self-host-support) emitted headers: AverList<Header> for HTTP request/response handling. Now emits headers: HttpHeaders (= AverMap<AverStr, AverList<AverStr>>), matching the runtime shape every other backend already used.

Docs

• docs/services.md: Http.* signatures and HttpRequest / HttpResponse records updated to the Map<String, List<String>> headers shape.

Aver 0.14.0 "Edge"

Aver's WASM backend becomes a deployable edge target: small user modules, a shared runtime, and explicit host bridges.

Added

• --target edge-wasm emits a thin user.wasm that imports a separately hosted aver_runtime, so browser and edge deployments can cache the runtime once.
• Host bridges: --bridge fetch for JS/Workers-style hosts and --bridge wasip1 for standalone WASI preview 1 execution.
• Cloudflare Workers pack output (--preset cloudflare) — drops worker.js (ES-module bootstrap that wires aver/* host imports against console.* / Date.now() / Math.random() / Fetch + JSPI for Http.*) and wrangler.toml next to a single bundled user.wasm. Cloudflare Workers reject WebAssembly.instantiate(bytes, …) from runtime-fetched bytes, so the preset uses --target wasm (runtime inlined via wasm-merge) for static-import shape; --target edge-wasm stays for browsers / Deno / Bun where the runtime CDN at averlang.dev/runtime/ works. Runtime artifacts, checksums, and manifest are published independently under /runtime/.
• WASM host coverage for Env.*, Console.warn, Http.*, request/response headers, and multi-value header flow.
• WASM Map runtime — flat hashtable with structural hashing/equality across all hashable key types (Int, Float, Bool, String, heap), O(1) Map.len, owned-mutate fast path on Map.set when last-use analysis proves sole ownership. map build 5k bench: WASM 963 µs vs VM 1.33 ms. Replaces the prior placeholder linked-list shape that was O(N²) on TCO build patterns.
• --optimize size|speed for the WASM optimization pipeline.
• Runtime artifacts at /runtime/: aver_runtime.wasm, aver_to_wasi.wasm, WAT companions, checksums, versioned URLs, and latest/.

Changed

• HTTP headers are Map<String, List<String>> across request/response records and Http.post / Http.put / Http.patch.
• WASM map ABI is polymorphic, with key kind and value pointer flags passed explicitly.
• WAT is the source of truth for the standalone runtime, and emit-time WASM validation is part of the compile path.
• WASM Vector.set is O(1) in TCO build loops via owned-mutate dispatch — fused Option.withDefault(Vector.set(v, i, x), v) where v is a last-use slot lowers to an inline bounds check + i64.store. Same trick the VM uses; matches its perf profile on vector get/set 5k.

Removed

• --adapter → --bridge and --wasm-opt oz|o3 → --optimize size|speed.
• --target wat and --target wasm+wat; use standard WASM tooling for WAT output.

Fixed

• WASM Map<Int|Float|Bool, V> validation and lookup issues.
• VM map structural equality for heap keys.
• Cloudflare/fetch bridge response headers no longer get dropped.

Known limitations

• Http.* under --bridge wasip1 returns a transport error; real WASI HTTP belongs in a later Component Model target.

Aver 0.13.0 "Limit"

Pure core. Explicit shell. Auditable boundary. Aver learns to say no — at the module's edge, to extra calls, to hostile worlds.

Added

• aver verify --hostile / aver audit --hostile — runs every verify <fn> law <name> block under an adversarial expansion of its given clauses. Typed value domains (given x: Int = [3]) get augmented with the per-type boundary set (0, 1, -1, i64::MIN, i64::MAX; for Float add ±Inf and NaN; for Str add empty / NUL-embedded / multi-byte / 1024-char). On top of that, classified effects get multiplied by adversarial profiles (frozen / fast-forward / backward clocks, always-min / always-max / alternating random, network-down responses, empty / always-error filesystem, …) — given for an effect is just the worlds you listed, hostile mode adds more on top, and law form already quantifies universally over every stub. Failures that surface only here mean the law isn't universal — either weaken it with when <precondition> to scope it to the worlds where it actually holds, downgrade from law to verify <fn> cases-form when the claim is really stub-specific, or accept the profile as a real production world the impl should handle.
• Module-level effect boundary — effects [...] declaration on the module header. Every function's ! [Effect] must be covered by the module's declared surface, enforced at type-check. A namespace entry like Disk admits any Disk.* method; method-level Disk.readText admits only that one. Modules with functions but no effects [...] get a soft warning nudging them to declare the boundary; you opt in when you want the enforcement.
• when over oracle stubs (oracle assumptions). In verify <fn> trace law <name>, the when predicate may now reference an effect-given oracle directly: when clock(BranchPath.Root, 1) > clock(BranchPath.Root, 0) declares "this law assumes a monotonic clock". Hostile profiles that violate the assumption are skipped; profiles that respect it run normally. Read-your-writes, conservation, idempotent fetch, protocol order — invariants you used to leave in comments now live in source. Skipped count is shown alongside passed / failed; if every adversarial profile is skipped, you get a vacuous-under-hostile warning so the law isn't silently uncovered.
• .trace.count(method) — quantitative trace assertion. Returns the number of trace events whose method matches the argument (Console.print, Http.get(...), etc.). Complements .contains (boolean any-match) with the count form so laws can pin "this fn calls the API exactly once" or "no extra disk reads under hostile profiles".
• verify-hostile-mismatch diagnostic slug — distinct from the regular verify-mismatch, so CI gates can route declared-world regressions and adversarial-world surfacings to separate channels: jq '.diagnostics[] | select(.slug == "verify-hostile-mismatch")'. Each carries from_hostile: true and an origin field with the profile label (hostile effect profile: Time.unixMs/saturated, hostile boundary expansion).
• Oracle invariants in proof export — documented and enforced. The trust header in every aver proof --backend lean / --backend dafny artifact spells out the per-effect bounds the runtime guarantees: Random.int stays in [min, max], Random.float in [0.0, 1.0], Time.unixMs ≥ 0, Disk.exists is total. Lifted theorems quantify over subtype-encoded oracle types (RandomIntInBounds, RandomFloatInUnit, TimeUnixMsNonneg) — the bound is a constrained quantifier at the lemma level, not a free side-condition you have to discharge separately.
• Playground hostile toggle — checkbox next to the Audit button. When checked, audit runs the hostile pipeline; the Verify panel and the structured JSON output carry the same dual-run breakdown (declared vs hostile, with the per-block scorecard).
• Showcase example: hostile clock. examples/formal/hostile_clock.av (and the Oracle dropdown in the playground): a deadline check that passes under real time and breaks under the saturated-clock profile — concrete demo of what --hostile finds that plain verify misses.
• Dual-run breakdown in TTY and JSON. Per-block summary line shows (1/1 declared, 11/35 hostile, 3 skipped by when) so you can see at a glance whether a regression is in the declared world or only surfaces under adversarial profiles. JSON output adds four counters on verify_summary.blocks[] — declared_passed, declared_failed, hostile_passed, hostile_failed — for tooling that wants to split "law regression" from "hostile coverage gap".
• Cartesian cap. Hostile expansion stops at 10,000 cases per block (same ceiling the parser uses for declared given ranges). Over-budget blocks get a clear error pointing at the law and listing the projected size; tighten the given, add a when, or run that block without --hostile.

Aver 0.12.0 "Atlas"

Multi-module Aver projects export to Lean and Dafny end-to-end. Generated proofs shrank by ~85% on pure-math examples. All 42 canonical examples now pass both proof backends.

Added

• Multi-module proof export. Projects with depends [...] produce one .lean / .dfy file per module, plus a shared AverCommon library carrying only the helpers your code actually references. Submodule paths like Models.User land at Models/User.{lean,dfy}. Works on rogue, doom, tetris, checkers, notepad — every multi-module example in the repo, including those mixing same-named fns across modules and modules sharing a name with a record.
• ? operator now works in pure proof export. Previously cmd = parseCommand(x)?; <rest> produced uncompilable proof code; now correctly lowers to match … { Result.Ok(cmd) -> <rest>; Result.Err(e) -> Result.Err(e) } before reaching Lean / Dafny. Fixes mission_control.
• Concrete Float evaluation in Lean proofs. Float.floor, Float.round, Float.ceil, Float.toInt now match the runtime exactly (IEEE 754 + saturating cast, including NaN → 0 and ±∞ → i64 bounds). verify cases over Float values get real native_decide evaluation in Lean instead of opaque stubs. Edge-case behaviour is asserted by native_decide proofs that re-run on every Lake build.
• Float.sin, Float.cos, Float.atan2 are now proof-exportable across both backends, not just runtime. doom's raycaster compiles to Lean / Dafny.
• Terminal.size is now a verifiable effect. Oracle signature () -> Terminal.Size, same shape as Args.get / Env.get. Example: examples/formal/terminal_size_snapshot.av.
• Playground download menu. The ⬇ button now expands into Aver source / WASM binary / Rust project / Lean 4 proof / Dafny proof — your in-browser source compiles and ships as .av / .wasm / .zip.

Changed

• Generated proof files shrank dramatically. Lean and Dafny now emit only the helpers, records, and trust-assumption headers your code actually references — no more 1500-line preamble for a 20-line pure-math file. Calculator and pure-laws examples shrank ~85-90% in Lean, ~70-90% in Dafny; effectful examples 25-40%.
• Shared backend infrastructure. Built-in records, helpers, and per-module emission logic live in single shared modules consumed by Lean / Dafny / WASM. Adding a new built-in record shape is one line in codegen::builtin_records.
• aver context output is denser (schema_version: 7, breaking). Markdown signatures now use the Aver source form name(args) -> Ret ! [Effects] instead of a separate effects: line. JSON records.fields and types.variants are pre-formatted strings (["id: String", ...], ["IngestWebhooks(String, String)", ...]) instead of nested objects, and arrays are rendered inline ([a, b, c]) while objects stay multi-line. Net effect on the showcase projects: workflow_engine fits 78/131 elements at 24kb (was 47/131); payment_ops fits 98/98 at 32kb with room to spare. Anything parsing CONTEXT.json should switch from fields[i].name / fields[i].type access to split(": ") on the string.

Aver 0.11.0 "Oracle"

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.