Skip to content

AVM Runtime

This module defines the execution environment and runtime infrastructure for the AVM. It provides the state representation, error types, result types, and observability mechanisms used by the interpreter.

{-# OPTIONS --without-K --type-in-type --guardedness --exact-split #-}
open import Foundation.BasicTypes

Module Parameters

module AVM.Runtime
    -- Core types
    (Val : Set)
    (ObjectId : Set)
    (freshObjectId : ℕ → ObjectId)

    -- Machine/distribution types
    (MachineId : Set)

    -- Controller/distribution types
    (ControllerId : Set)
    (ControllerVersion : Set)

    -- Transaction types
    (TxId : Set)
    (freshTxId : ℕ → TxId)

    -- Object model type
    (Object : Set)
  where

Message Types

Message passing is the only way to communicate between objects. The representation of messages is left abstract by design.

The general I-O object model (φ : I* ⇀ O) permits distinct input type I and output type O. The current implementation uses the same type (Val) for both Input and Output for simplicity. Future refinements may parameterize modules by separate Input and Output types to support heterogeneous communication (e.g., Input = Command, Output = Response).

Message : Set
Message = Val

Input : Set
Input = Message

Output : Set
Output = Message

Object Metadata

Extrinsic metadata managed by the AVM includes the object's identifier, accumulated input history, physical location, and controller assignments. Objects reside on machines (physical nodes) and are owned by controllers (logical authorities that order transactions). Each object tracks its current machine location, which controller created it, which controller currently owns it, and version numbers for distributed consistency.

record ObjectMeta : Set where
  constructor mkMeta
  field
    objectId : ObjectId
    history : List Input                 -- Accumulated inputs

    -- Physical location
    machine : MachineId                  -- Where object data resides

    -- Simplified controller tracking
    creatingController : ControllerId    -- Who created (immutable)
    currentController : ControllerId     -- Who controls now

    -- Version tracking for distribution
    createdAtVersion : ControllerVersion
    modifiedAtVersion : ControllerVersion

Store: Persistent Object Database

The AVM provides a view of the store of all objects. The store separates intrinsic object behaviors from their runtime metadata. This view is partial because an object may not yet exist in the store or may not be available.

ObjectStore

ObjectStore : Set
ObjectStore = ObjectId → Maybe Object

MetaStore

MetaStore : Set
MetaStore = ObjectId → Maybe ObjectMeta

Store Record

record Store : Set where
  constructor mkStore
  field
    objects : ObjectStore    -- Immutable behaviors
    metadata : MetaStore     -- Mutable runtime state

The Store abstraction separates the persistent object database from ephemeral execution state. This separation distinguishes what persists across transactions (the store) from what exists only during execution (transaction overlays and execution context).

Transactional Semantics

Transactions provide atomicity. State modifications within a transaction remain tentative until committed; abortion discards all changes. The AVM maintains a transaction log recording pending object writes, creations, destructions, and cross-controller transfers.

TxWrite

A transaction write pairs an object identifier with an input message. The transaction log accumulates these pairs in order. Multiple writes to the same object within a transaction preserve ordering, enabling sequential object behavior within atomic boundaries.

TxWrite : Set
TxWrite = ObjectId × Input

Pure Functions

A collection of pure functions indexed by name. Each function takes a list of arguments and may return a value (or fail with nothing if the arguments are invalid).

PureFunctions : Set
PureFunctions =
  String  -- function name
  -> Maybe ( -- lookup result
         List Val  -- fun. arguments
      -> Maybe Val  -- fun. result
   )

Execution State

The AVM maintains a global execution state that captures all information needed for transactional computation. Each instruction execution operates as a state transition: given the current state and an instruction, the interpreter produces a result value, an updated state, and an execution trace.

record State : Set where
  field
    -- Current execution location
    machineId : MachineId          -- Physical machine executing this program

    -- Current controller identity
    controllerId : ControllerId
    currentVersion : ControllerVersion

    -- Object storage (separated)
    store : Store          -- Combined store with objects and metadata

    -- Pure function collection (can be extended over time)
    -- Think of this as a library for programs to use.
    pureFunctions : PureFunctions

    -- Transaction context (overlay)
    txLog : List TxWrite      -- Tentative writes: (objectId , input)
    creates : List (ObjectId × Object × ObjectMeta)  -- Pending creates
    destroys : List ObjectId                          -- Pending destroys
    observed : List (ObjectId × ControllerVersion)    -- Observed versions (for commit-time validation)
    pendingTransfers : List (ObjectId × ControllerId) -- Pending object moves
    tx : Maybe TxId                                   -- Active transaction id (if any)

    -- Current execution frame
    self : ObjectId           -- Current object being processed
    input : Input             -- Current input being processed
    traceMode : Bool          -- Debug tracing flag

The State record organizes fields into five logical groups:

  • Physical execution context: machineId identifies the physical machine where this program is currently executing. This is independent of logical controller identity and enables reasoning about data locality and cross-machine communication costs.
  • Controller context: controllerId identifies the executing controller (logical authority), and currentVersion tracks its protocol version. These fields enable distributed consistency checking across controller boundaries.
  • Persistent storage: store holds the object database (both behaviors and metadata), and pureFunctions maintains the extensible pure function registry. These components persist across instruction executions.
  • Transactional overlay: txLog accumulates uncommitted writes (object-input pairs), creates and destroys track pending object lifecycle changes, observed records object versions for conflict detection, pendingTransfers queues cross-controller object moves, and tx holds the active transaction identifier (or nothing if no transaction is active).
  • Execution frame: self identifies the currently executing object, input holds the message being processed, and traceMode enables debug logging when set to true.

Layered Error Types

Instructions may fail during execution. Each instruction family defines its own error domain, and these domains compose to form layered error types matching the instruction set hierarchy. This design provides type-level guarantees about which errors can occur at each layer.

Object Errors

Object lifecycle and interaction operations fail when objects are missing, destroyed, or reject inputs.

data ObjError : Set where
  ErrObjectNotFound : ObjectId → ObjError
  ErrObjectAlreadyDestroyed : ObjectId → ObjError
  ErrObjectAlreadyExists : ObjectId → ObjError
  ErrInvalidInput : ObjectId → Input → ObjError
  ErrObjectRejectedCall : ObjectId → Input → ObjError
  ErrMetadataCorruption : ObjectId → ObjError

Introspection Errors

Introspection operations fail when the object store is corrupted.

data IntrospectError : Set where
  ErrStoreCorruption : String → IntrospectError

Transaction Errors

Transaction operations fail due to conflicts, missing transactions, or invalid nesting.

data TxError : Set where
  ErrTxConflict : TxId → TxError
  ErrTxNotFound : TxId → TxError
  ErrTxAlreadyCommitted : TxId → TxError
  ErrTxAlreadyAborted : TxId → TxError
  ErrNoActiveTx : TxError
  ErrInvalidDuringTx : String → TxError

Distribution Errors

Distribution operations fail when controllers or machines are unreachable, transfers are unauthorized, or version mismatches occur.

data DistribError : Set where
  -- Controller errors
  ErrControllerUnreachable : ControllerId → DistribError
  ErrUnauthorizedTransfer : ObjectId → ControllerId → DistribError
  ErrVersionMismatch : ControllerVersion → ControllerVersion → DistribError
  ErrCrossControllerTx : ObjectId → ControllerId → DistribError

  -- Machine errors
  ErrMachineUnreachable : MachineId → DistribError
  ErrInvalidMachineTransfer : ObjectId → MachineId → DistribError

Pure Function Errors

Pure function operations fail when functions are missing or already registered.

data PureError : Set where
  ErrFunctionNotFound : String → PureError
  ErrFunctionAlreadyRegistered : String → PureError

Composed Error Types

Error types compose in layers matching the instruction set hierarchy. Each layer includes errors from previous layers plus domain-specific errors.

Base Layer Error (Instr₀)

The base layer combines object and introspection errors.

data BaseError : Set where
  obj-error : ObjError → BaseError
  introspect-error : IntrospectError → BaseError

Transaction Layer Error (Instr₁)

The transaction layer adds transaction errors to base errors.

data TxLayerError : Set where
  base-error : BaseError → TxLayerError
  tx-error : TxError → TxLayerError

Pure Function Layer Error (Instr₂)

The pure function layer adds pure computation errors to transactional errors.

data PureLayerError : Set where
  tx-layer-error : TxLayerError → PureLayerError
  pure-error : PureError → PureLayerError

Full AVM Error

The full error type includes all instruction errors plus distribution errors.

data AVMError : Set where
  pure-layer-error : PureLayerError → AVMError
  distrib-error : DistribError → AVMError

Error Pattern Synonyms

Pattern synonyms eliminate verbose nested constructor applications when constructing or matching errors.

Object Error Patterns

pattern err-object-not-found oid =
  pure-layer-error (tx-layer-error (base-error (obj-error (ErrObjectNotFound oid))))

pattern err-object-destroyed oid =
  pure-layer-error (tx-layer-error (base-error (obj-error (ErrObjectAlreadyDestroyed oid))))

pattern err-object-exists oid =
  pure-layer-error (tx-layer-error (base-error (obj-error (ErrObjectAlreadyExists oid))))

pattern err-invalid-input oid inp =
  pure-layer-error (tx-layer-error (base-error (obj-error (ErrInvalidInput oid inp))))

pattern err-object-rejected oid inp =
  pure-layer-error (tx-layer-error (base-error (obj-error (ErrObjectRejectedCall oid inp))))

pattern err-metadata-corruption oid =
  pure-layer-error (tx-layer-error (base-error (obj-error (ErrMetadataCorruption oid))))

Introspection Error Patterns

pattern err-store-corruption msg =
  pure-layer-error (tx-layer-error (base-error (introspect-error (ErrStoreCorruption msg))))

Transaction Error Patterns

pattern err-tx-conflict tid =
  pure-layer-error (tx-layer-error (tx-error (ErrTxConflict tid)))

pattern err-tx-not-found tid =
  pure-layer-error (tx-layer-error (tx-error (ErrTxNotFound tid)))

pattern err-tx-committed tid =
  pure-layer-error (tx-layer-error (tx-error (ErrTxAlreadyCommitted tid)))

pattern err-tx-aborted tid =
  pure-layer-error (tx-layer-error (tx-error (ErrTxAlreadyAborted tid)))

pattern err-no-active-tx =
  pure-layer-error (tx-layer-error (tx-error ErrNoActiveTx))

pattern err-invalid-during-tx msg =
  pure-layer-error (tx-layer-error (tx-error (ErrInvalidDuringTx msg)))

Pure Function Error Patterns

pattern err-function-not-found name =
  pure-layer-error (pure-error (ErrFunctionNotFound name))

pattern err-function-registered name =
  pure-layer-error (pure-error (ErrFunctionAlreadyRegistered name))

Distribution Error Patterns

-- Controller error patterns
pattern err-controller-unreachable cid =
  distrib-error (ErrControllerUnreachable cid)

pattern err-unauthorized-transfer oid cid =
  distrib-error (ErrUnauthorizedTransfer oid cid)

pattern err-version-mismatch v1 v2 =
  distrib-error (ErrVersionMismatch v1 v2)

pattern err-cross-controller-tx oid cid =
  distrib-error (ErrCrossControllerTx oid cid)

-- Machine error patterns
pattern err-machine-unreachable mid =
  distrib-error (ErrMachineUnreachable mid)

pattern err-invalid-machine-transfer oid mid =
  distrib-error (ErrInvalidMachineTransfer oid mid)

Observability and Tracing

State transitions generate observable events. The interpreter records object creation, destruction, message passing, transaction boundaries, and controller operations in a chronological log. Each log entry pairs an event type with a timestamp and executing controller identifier. This mechanism supports debugging, auditing, and formal verification of execution histories.

EventType

data EventType : Set where
  -- Object lifecycle events
  ObjectCreated : ObjectId → Val → EventType
  ObjectDestroyed : ObjectId → EventType

  -- Object interaction events
  ObjectCalled : ObjectId → Input → Maybe Output → EventType

  -- Machine events
  ObjectMoved : ObjectId → MachineId → MachineId → EventType
  ExecutionMoved : MachineId → MachineId → EventType

  -- Controller events (ownership changes)
  ObjectTransferred : ObjectId → ControllerId → ControllerId → EventType
  ControllerSwitched : ControllerId → ControllerVersion → EventType

  -- Transaction events
  TransactionStarted : TxId → EventType
  TransactionCommitted : TxId → EventType
  TransactionAborted : TxId → EventType

  -- Error events
  ErrorOccurred : AVMError → EventType

LogEntry

record LogEntry : Set where
  constructor mkLogEntry
  field
    timestamp : ℕ
    eventType : EventType
    executingController : ControllerId

Trace

Trace : Set
Trace = List LogEntry

Result Types

Instruction execution produces either success or failure. The Result type encodes this dichotomy: successful executions yield a value, updated state, and trace; failures yield only an error. This design threads state and trace information through the interpreter while enabling early termination on errors.

Success Record

Successful execution returns three components: the instruction's result value, the modified execution state, and the trace of events generated. A record structure provides named field access, eliminating tuple projections.

record Success (A : Set) : Set where
  constructor mkSuccess
  field
    value : A
    state : State
    trace : Trace

open Success public

Result Datatype

A polymorphic sum type distinguishes success from failure. The type parameter A specifies the result value type, while parameter E specifies the error type. The success constructor wraps a Success record; the failure constructor wraps an error value.

data Result (A : Set) (E : Set) : Set where
  success : Success A → Result A E
  failure : E → Result A E

Layer-Specific Result Types

Each instruction layer has a precise result type reflecting its error domain.

BaseResult : Set → Set
BaseResult A = Result A BaseError

TxResult : Set → Set
TxResult A = Result A TxLayerError

PureResult : Set → Set
PureResult A = Result A PureLayerError

AVMResult : Set → Set
AVMResult A = Result A AVMError

The Result type makes explicit that:

  • Success returns a record with named fields: value, state, and trace
  • Failure returns only an error value of the specified error type
  • Named fields eliminate nested tuple projections and improve code clarity
Module References

Referenced By

This module is referenced by:

References

This module references: