Aver 0.30.0 "Turn"

Programs wait, work and answer in turns written in plain Aver, and more of what they compile to is certified on the exact bytes.

Highlights

• Concurrency is data plus effects. A function that requests something your program answers (answers [Cap], now or later) is a process; nothing marks it, and aver check lists each one with the reason. The compiler cuts it into plain state, request and answer functions and generates the loop that runs it (Run.all()). Run.turn() hands the turn back without a request. See "The coordinator" in docs/language.md.
• Jobs and one wait. A job is a request answered by a pure function bound in aver.toml. Wait.poll waits on sockets and jobs together. Jobs run in parallel on the VM, Rust and wasm-gc, and a recording replays on any of them.
• Non-blocking TCP. Tcp.readNow, Tcp.writeNow and Tcp.Socket.Sending.
• Certificates cover much more of a real program. Int arithmetic, lists, Bytes, ? and string interpolation are certified on the bytes, and laws about certified functions hold on the bytes. On btc-listener: 1,450 functions, 74 laws, aver cert check in under ten minutes on a laptop.
• Proofs are Lean only. Dafny is gone. A law can explain itself with because and using, and more shapes close for every input. Lean 4.34.0.
• Patterns at any depth: Option.Some(0), Shape.Rect(0, h), [a, b, ..rest], checked for what they miss on every backend.
• No copies when a Map or Vector inside a record is updated and nothing else holds it.
• Tooling: aver effects --write, aver agent-connect, --pack wasmtime, Disk.sync, Int.toBigEndian.
• projects/song: a short piece played by six processes and synthesised by the program itself; its sound functions are certified on the bytes, and a recording replays to the same WAV on the VM and wasm-gc.

The cut of a process is checked on the compiler's own programs; a proof for every program is still open (#1376).

Migration

Before	Now
aver proof --backend dafny, --error-budget	Lean only; --sorry-budget, --declined-budget
--check-json keys errors, timeouts, axioms, axiom_budget, omitted	build_errors, sorries
proof sidecars	because / using in the law
aver proof and --certify covering every verify example	laws by default; --examples for the examples
match on Tcp.Socket	add a Tcp.Socket.Sending(connection) arm
a function of a recursion group not declaring the group's effects	every function declares them
any bare name in ! [...]	only _ or a capability namespace
dial, listen or peerAddress on --target wasip2	refused at compile time

Certificates from earlier versions must be produced again. If you pinned main between 0.29 and 0.30: answer =, the job keys and [run] in aver.toml are refused with the repair, reply sums and Wait.Wake became Result and Run.Wake, yield is gone (a function is a process when it requests something its module's dependencies answer; a loop that only hands the turn back calls Run.turn()), a program can no longer call generated __ names, and wasm-gc recordings of Wait.poll have to be made again.

Fixed

• aver proof no longer proves laws that are false at run time, such as 0 - 1 read as 0 or a negative Vector index.
• aver-cert checks that a wasip2 component runs the core it certifies, and a package can no longer forge a verdict line.
• wasm-gc and Rust agree with the VM on non-ASCII case mapping (#1185) and on several match shapes.
• Record fields run in the order written (#1240), Disk.sync on a directory works on Windows (#1238), and aver-memory builds without std (#1460).