Skip to content

AVM Verification Architecture

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
open import AVM.Instruction
open import AVM.Objects
open import Goose.Anoma

Compilation Pipeline

The AVM verification effort centers on a compilation pipeline that transforms high-level intent programs called AVM programs into executable resource machine code.

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

The compilation process must preserve semantic correctness through a formal translation function that maintains behavioral equivalence between abstraction levels. For proving this, we need to define a notion of semantic equivalence between AVM programs and resource machine programs.

Denotational Semantics

Each language in the compilation pipeline receives a denotational semantics via interaction trees, enabling precise reasoning about program behavior and compiler correctness. In other words, we denote AVM programs as interaction trees and resource machine programs as interaction trees. With the right notion of semantic equivalence, weak bisimulation, we can prove that the compilation process preserves semantic correctness. 

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

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

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

    AVM_IT -.->|translate| TRANS_IT
    TRANS_IT ==>|"≈ (notion of equiv.)"| 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, the compilation preserves semantics up to a notion of semantic equivalence (≈, weak bisimulation) after event translation:

\[ \texttt{translate}(⟦ p ⟧_{\mathsf{AVM}}) ≈ ⟦ \texttt{compile}(p) ⟧_{\mathsf{RM}} \]

The semantic domains are stratified by event types E_AVM and E_RM. The translate function maps high-level AVM events to resource machine events, preserving the computational structure.

Event Interpretation Architecture

The interpretation of interaction trees proceeds through event translation and handlers that bridge abstract program semantics with concrete computational effects.

graph LR
    AVM_IT["ITree E_AVM A"]
    RM_IT["ITree E_RM A"]
    Result["M A"]

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

    subgraph handler["Handler: h : E_RM ~> 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

The event translation maps high-level AVM operations into resource machine primitives, while the RM handler interprets those primitives into concrete effects: state management for resource tracking, error handling for validation failures, and IO for external system interactions.