The AVM ISA is currently specified in a series of entries in my notes. The following contains some thoughts and updates on what I’ve been working on during the last couple of days, based on discussions with @cwgoes and @graphomath
Related:
- #desiderata
- Outdated but still AVM Instruction Set - Instr₀ - #4 by cwgoes
What is the AVM, right now?
The Anoma Virtual Machine (AVM) is an architecture for executing distributed, non-deterministic programs. This post sheds light on what the AVM aims to be, what sets it apart from other virtual machines, what already works/is implemented, and what challenges are ahead. We’ll focus on the high-level concepts, avoiding compilation targets and resource machine details for now.
Why another virtual machine?
To run smart contracts on a blockchain, there is the EVM. For running sandboxed
code in browsers, there is WebAssembly. For running Java programs on your
laptop, there is the JVM. Want to do metaprogramming and introspection? There is
Lisp, its own VM. Each VM solves a specific problem—what is our problem then?
The AVM aims to enable programs where multiple independent parties coordinate
operations on objects. These objects communicate through messages, and programs
may express preferences rather than explicit state transitions. And, here, we
are not mentioning privacy matters yet.
What the AVM must do, so we design an ISA that makes sense
The AVM is fundamentally different from stack or register machines. It works as
a message-passing actor-like model—Erlang is the closest existing artefact?—No
existing VM combines all these features: message-driven objects, multi-party
transaction coordination, distributed execution and location transparency, and
intent matching. Let’s review the core requirements in detail.
-
Message-passing objects with execution traces: Objects are black boxes. You send messages and get responses, but you cannot peek inside. Like calling a web API, you know the endpoints but not the server’s internal code. The runtime records all messages sent during execution (message sequence chart) to enable multi-party constraint checking.
-
Purely functional objects with optional determinism: Objects behave as pure
functions from input histories to outputs, enabling replay and verification when
deterministic behaviour is desired. Programs can request nondeterministic choices
throughchoose(pick a value from the domain) and enforce constraints through
require(transaction fails if the constraint is unsatisfied). The AVM runtime
symbolically executes programs to extract constraint satisfaction problems for
intent matching via SAT solvers. -
Multi-party transactions: Alice’s and Bob’s resources are each controlled by
different controllers (independent transaction ordering authorities). Controllers
order transactions and prevent double-spends by ensuring each resource has one
terminal controller that determines when it can be consumed. Alice and Bob trade
atomically through transaction composition. Programs can compose non-conflicting executions (parallel) or sequentially dependent executions (Bob reads Alice’s writes). Programs check constraints on other programs’ message sequences. Linear constraints enforce use-once guarantees (“I offer A only in exchange for B”). -
Intent matching: Programs can express transition preferences through
nondeterministic choice and constraints. “I want asset X, I’ll give Y, as long
as condition Z holds.” The runtime extracts constraint satisfaction problems
into an intermediate representation suitable for SAT solvers. Solutions satisfy
all constraints across all composed programs or report no solution exists. -
Distribution: Programs run across multiple physical machines with location
transparency. Programs can be written as if running on a single machine; the
system handles distribution transparently. Objects may be on different physical
machines, controlled by different parties, and executed in different runtimes. The AVM also supports teleportation: moving a process from one
machine to another while maintaining the same transaction state. -
Transactions use optimistic concurrency. Transactions only operate on objects
owned by the same controller. Transactions are atomic and non-nested. Commit and abort are the only ways to end a transaction.
Currrent progress
- There is an initial (Agda) specification of the AVM ISA.
- The ISA is a layered architecture, with each layer addressing a different
concern. AVM ISA layers can be composed to form custom instruction sets. - For the instruction set, we have defined six instruction families so far (objects, introspection, transactions, pure functions, machine and controller).
- An object model. An object is a pair of a behaviour function from input sequences to outputs and a history of input sequences. Well-formedness properties proven (prefix closure, optional determinism). Counter and echo examples demonstrate the model.
- A runtime infrastructure. State representation, error handling, and event logging are all specified.
- An interpreter, actually an interpreter for each instruction family. That gives us a formal operational semantics for each instruction family. A few runtime checks at the moment, such as checking that no nested transactions are started while a transaction is already active, and transactions only talk about objects owned by the same controller. These checks can be lifted to static checks in the future.
What’s missing or incomplete I can see right now
-
The current semantics is a presentation in terms of interaction trees. However, there are a few challenges. Do we want terminating or non-terminating programs? resolve branching (if-then-else vs explicit jumps). Do we also need to describe the compilation to a lower executable bytecode (RM-based, for example)?
-
Distributed transactions: Single-controller transactions work on paper.
Multi-controller coordination requires something more involved; this is research
territory. -
Intent matching and symbolic execution: How do
chooseandrequireintegrate
with transaction commit? The runtime must symbolically execute programs to
extract constraint satisfaction problems. Constraint solving is potentially
expensive (NP-hard for general constraints). How do we handle linear versus
non-linear constraints on message sequence charts? -
Cost model: Unsafe operations (scryMeta, scryDeep) can force complete store
traversal. Need upper bounds and quota mechanisms to prevent abuse.
We want a formal specification that can tell us properties such as atomicity,
location transparency, optional determinism, object model’s properties as
highlighted in the green paper. -
The surface language is not really a concern of the AVM ISA. However, we need
One that shares the functionality of the AVM ISA and can be compiled to the AVM ISA.
What syntax do programmers write? The examples in the current specification use
Agda as a metalanguage, but that’s not the user-facing language, and it should
not be. Scheme/Racket is a strong candidate, yes, it’s simple. S-expressions map
naturally to the instruction tree structure, simple grammar, and proven compilation
techniques. A Scheme-based language could be the canonical syntax with room for
alternatives (imperative, declarative) later. Python, Rust, whatever works.
More questions I have
-
Should the “official” VM programs have access to unsafe operations (in particular, scry)? Debuggers need to inspect object state without triggering behaviour. The type system marks these operations “unsafe” but doesn’t prevent their use. Should we forbid them entirely, add runtime permissions, or trust developers to use them responsibly?
-
How should execution migration (teleport) interact with active transactions?
Currently forbidden to maintain transaction integrity. Alternative: allow
migration, but track it in the transaction overlay.