About the AVM

The Anoma Virtual Machine (AVM) is a transactional virtual machine architecture designed for message-driven object-oriented computation. The system provides a set of primitives to support pure functional programming, distributed computation primitives, and nondeterministic choice mechanisms enabling intent-based transaction matching.

Specification Scope

The AVM specification establishes denotational semantics for programs, defining what programs signify rather than dictating execution strategies. Programs are typed as AVMProgram, with operational semantics defined through interaction trees. This coinductive formalization separates effectful operations instructions from pure computation. The semantics form a small-step transition system over a global state of live objects and metadata.

The specification covers instruction semantics, state transitions, runtime context (including error handling and event tracing), and system model assumptions addressing network behavior, failure modes, and trust boundaries. Althought, not complete, we include a rundimentary interpreter section to guide implementation.

The specification does not dictate platform implementation choices—scheduling, persistence, network protocols, or resource management remain platform concerns. This separation allows different implementations to target varied deployments while conforming to one semantic specification.

Design Commitments

The following commitments guide runtime implementations while remaining independent from the formal semantics presented in this specification. The instruction set reflects these commitments, and the system model assumes these commitments are realised.

1. Object-Centric Computation Model: Objects maintain immutable input histories that grow monotonically.

2. Objects are created and destroyed exactly once in their lifecycle.

3. Code objects execute when invoked by a message.

4. At any moment, execution is localised to a single object context. That is, execution occurs within a single object.

5. Distributed Execution Model: Program execution may migrate across machine boundaries.

6. Each object is associated with exactly one controller authority at any time.

7. Programs can inspect the current history identifier and move to specific target history identifiers.

8. Transactional Semantics: Transaction boundaries use beginTx, commitTx, and abortTx to provide atomic commit semantics. Current implementations use single-controller coordination; multi-party composition remains an active goal.

9. Constraint Programming and Nondeterminism: The instruction set provides two constraint layers with distinct execution models. Finite domain instructions (newVar, narrow, post, label) enable constraint propagation and search with call-time choice. Nondeterminism instructions (choose, require) support commit-time choice where selections and constraints accumulate during execution and are validated atomically at transaction commit.

10. Intent Composition: The architecture supports composing multiple transactional segments into a unified atomic transaction.

11. Message Sequence Constraints: Programs may specify constraints over message ordering when composing multi-party intents/programs.

12. Pure Computation Representation: The AVM architecture does not prescribe a fixed representation for pure functions. The admissible function set can grow without altering the virtual machine semantics.

These design commitments guide the architecture and link user-facing features with the formal specification. They are realized through the system model assumptions detailed in AVM System Model, which specifies the network model, failure semantics, transaction isolation guarantees, and other normative requirements that runtime implementations must satisfy.

---

References to other modules

This page references the following modules:

• AVM.Instruction
  • Symbols: Safety, ObjInstruction, IntrospectInstruction, ReflectInstruction, ReifyInstruction, Instr₀, TxInstruction, Instr₁, PureInstruction, Instr₂, MachineInstruction, ControllerInstruction, Instr₃, Constraint, FDInstruction, NondetConstraint, NondetInstruction, Instruction, ReifiedContext, ReifiedTxState, ReifiedConstraints, VarId, Safe, Unsafe, createObj, destroyObj, call, self, input, getCurrentMachine, getState, setState, sender, reflect, scryMeta, scryDeep, mkReifiedContext, mkReifiedTxState, mkReifiedConstraints, reifyContext, reifyTxState, reifyConstraints, Obj, Introspect, Reflect, Reify, beginTx, commitTx, abortTx, Tx, callPure, registerPure, updatePure, Pure, getMachine, teleport, moveObject, fetch, getCurrentController, getController, transferObject, freeze, Machine, Controller, mkVarId, Eq, Neq, Leq, Lt, Geq, Gt, AllDiff, ValEq, ValLeq, ValLt, ValGeq, ValGt, newVar, narrow, post, label, Assert, choose, require, FD, Nondet, obj-create, obj-destroy, obj-call, obj-receive, get-self, get-input, get-current-machine, get-state, set-state, get-sender, obj-reflect, obj-scry-meta, obj-scry-deep, do-reify-context, do-reify-tx-state, do-reify-constraints, tx-begin, tx-commit, tx-abort, call-pure, register-pure, pure-update-pure, get-machine, do-teleport, move-object, fetch-object, get-current-controller, get-controller, transfer-object, freeze-object, ISA, Domain, AVMProgram