Skip to content

AVM Specification

This document presents the formal verification architecture planned for the Anoma Virtual Machine (AVM) compilation pipeline using (a version of) interaction trees and weak bisimulation-based correctness proofs.

{-# OPTIONS --without-K --type-in-type --guardedness --exact-split #-}
module AVM.README where

Module Architecture

The AVM formalization uses four layers with clear separation of concerns:

graph TB
    Objects["Objects<br/>(Object Behavior Model)"]
    Runtime["Runtime<br/>(Execution Context)"]
    Instruction["Instruction<br/>(Instruction Syntax)"]
    Interpreter["Interpreter<br/>(Instruction Semantics)"]

    Objects --> Runtime
    Runtime --> Instruction
    Instruction --> Interpreter

    style Objects fill:#e1f5ff,stroke:#0288d1
    style Runtime fill:#fff9c4,stroke:#f57f17
    style Instruction fill:#f3e5f5,stroke:#7b1fa2
    style Interpreter fill:#e8f5e9,stroke:#388e3c

Objects defines the abstract object model. An object φ : I* ⇀ O maps input sequences to output sequences. Objects may be deterministic or nondeterministic (using choose for intent matching).

Runtime provides the execution environment: global state (object store, transaction overlays, controller context), error types (layered by instruction family), result types (success/failure with state and trace), and observability (events, logs, traces).

Instruction defines the instruction set syntax organized into composable layers: base, transactional, pure computation, and distribution.

Interpreter implements operational semantics. Each instruction transforms state, generates events, and produces results (success with updated state and trace, or failure with error).

Compilation Pipeline

The compiler transforms high-level AVM programs into resource machine code:

graph LR
    AVM["AVM Program<br/>(High-level DSL)"]
    RM["Resource Machine Program<br/>(Low-level Execution)"]
    AVM -->|compile| RM

Correctness requires behavioral equivalence between abstraction levels via weak bisimulation.

Denotational Semantics

Both AVM and resource machine programs denote interaction trees. Compiler correctness uses weak bisimulation to relate these denotations.

graph TB
    subgraph syntax["Syntax"]
        AVM_P["p : AVM"]
        RM_P["compile(p) : RM"]
    end

    subgraph semantics["Denotational Semantics"]
        AVM_IT["⟦ p ⟧ : ITree (Instr₂ Safe) A"]
        TRANS_IT["translate(⟦ p ⟧) : ITree (Instr₂ Safe) A"]
        RM_IT["⟦ compile(p) ⟧ : ITree (Instr₂ Safe) A"]
    end

    AVM_P -->|compile| RM_P
    AVM_P -.->|⟦·⟧_AVM| AVM_IT
    RM_P -.->|⟦·⟧_RM| RM_IT

    AVM_IT -.->|translate| TRANS_IT
    TRANS_IT ==>|"≈ (weak bisim)"| RM_IT

    style syntax fill:#f0f0f0,stroke:#666,stroke-width:2px
    style semantics fill:#f0f0f0,stroke:#666,stroke-width:2px

Compiler Correctness. For any AVM program p, compilation preserves semantics: translate(⟦ p ⟧) ≈ ⟦ compile(p) ⟧.

The translate function maps AVM events (E_AVM) to resource machine events (E_RM), preserving computational structure.

Event Interpretation Architecture

Interaction trees interpret via event translation and handlers:

graph LR
    AVM_IT["ITree (Instr₂ Safe) A"]
    RM_IT["ITree (Instr₂ Safe) A"]
    Result["M A"]

    AVM_IT -->|"translate<br/>(event morphism)"| RM_IT
    RM_IT -->|"interpret h<br/>(handler)"| Result

    subgraph handler["Handler: h : (Instr₂ Safe) ~> M"]
        direction TB
        State["State<br/>(Resource State)"]
        Error["Error<br/>(Validation)"]
        IO["IO<br/>(External Effects)"]
    end

    RM_IT -.->|uses| handler

    style handler fill:#f0f0f0,stroke:#666,stroke-width:2px

Event translation maps AVM operations to resource machine primitives. The handler interprets primitives as concrete effects: state management, error handling, and IO.