Skip to content

AVM Interpreter

This module defines the operational semantics of the AVM by specifying how each instruction transforms the VM state and generates log entries. The interpreter is parameterized by an abstract object model, making it independent of any specific object implementation.

{-# OPTIONS --exact-split --without-K --guardedness #-}

open import Foundation.BasicTypes using (ℕ; List; Maybe)

module AVM.Interpreter
  -- Base types
  (Val : Set)                          -- Values (data) - used for both Input and Output
  (ObjectId : Set)                      -- Object identifiers
  (freshObjectId : ℕ → ObjectId)       -- Fresh ID generation

  -- Machine/distribution types
  (MachineId : Set)                    -- Machine identifiers

  -- Controller/distribution types
  (ControllerId : Set)                 -- Controller identifiers
  (ControllerVersion : Set)            -- Version numbers

  -- Transaction types
  (TxId : Set)                         -- Transaction identifiers
  (freshTxId : ℕ → TxId)              -- Fresh transaction ID generation

  -- Object model (abstract)
  (Object : Set)                       -- Object type (abstract)
  (getBehavior : Object → (List Val → Maybe (List Val)))  -- Behavior: List Input → Maybe (List Output)
  where
-- Note: The I-O object model (φ : I* ⇀ O) permits distinct Input and Output types.
-- This implementation uses Val for both. The behavior function signature
-- (List Val → Maybe (List Val)) represents (List Input → Maybe (List Output))
-- where Input = Output = Val.

open import Foundation.BasicTypes hiding (ℕ)
open import Foundation.InteractionTrees

-- Import Runtime and Instruction modules (which use Object as parameter)
open import AVM.Instruction Val ObjectId freshObjectId MachineId ControllerId
                            ControllerVersion TxId freshTxId Object

Interpreter Implementation

The interpreter is parameterized by helper functions that provide platform-specific implementations:

module Interpreter
  -- Equality and comparison
  (_==_ : ∀ {A : Set} → A → A → Bool)
  (_≤v_ : ControllerVersion → ControllerVersion → Bool)

  -- State helpers
  (getFreshIdCounter : State → ℕ)
  (allObjectIds : State → List ObjectId)

  -- Object management
  (interpretValue : Val → Object)

  -- Distribution management
  (isReachableController : ControllerId → Bool)
  (isReachableMachine : MachineId → Bool)
  (sucVersion : ControllerVersion → ControllerVersion)
  where

Helper Functions

Object and Metadata Lookup

Retrieving an object with its metadata requires both components to be present.

  lookupObjectWithMeta : ObjectId → State → Maybe (Object × ObjectMeta)
  lookupObjectWithMeta oid st with Store.objects (State.store st) oid | Store.metadata (State.store st) oid
  ... | just obj | just meta = just (obj , meta)
  ... | just obj | nothing = nothing
  ... | nothing | just meta = nothing
  ... | nothing | nothing = nothing

Pending creates reside in the transactional overlay and are queried before the global store.

  lookupPendingCreate : ObjectId → State → Maybe (Object × ObjectMeta)
  lookupPendingCreate oid st = go (State.creates st)
    where
      go : List (ObjectId × Object × ObjectMeta) → Maybe (Object × ObjectMeta)
      go [] = nothing
      go ((oid' , obj , meta) ∷ rest) with oid == oid'
      ... | true = just (obj , meta)
      ... | false = go rest

Pending transfers track ownership changes scheduled within a transaction.

  lookupPendingTransfer : ObjectId → State → Maybe ControllerId
  lookupPendingTransfer oid st = go (State.pendingTransfers st)
    where
      go : List (ObjectId × ControllerId) → Maybe ControllerId
      go [] = nothing
      go ((oid' , cid) ∷ rest) with oid == oid'
      ... | true  = just cid
      ... | false = go rest

State Mutation

Metadata updates replace the metadata entry for a specific object.

  updateMeta : ObjectId → ObjectMeta → State → State
  updateMeta oid meta st =
    record st {
      store = record (State.store st) {
        metadata = λ oid' → if oid == oid' then just meta
                           else Store.metadata (State.store st) oid'
      }
    }

Creating an object with metadata installs both the object and its metadata in the store.

  createWithMeta : Object → ObjectMeta → State → State
  createWithMeta obj meta st =
    let oid = ObjectMeta.objectId meta in
    record st {
      store = record (State.store st) {
        objects = λ oid' → if oid == oid' then just obj
                           else Store.objects (State.store st) oid'
        ; metadata = λ oid' → if oid == oid' then just meta
                             else Store.metadata (State.store st) oid'
      }
    }

Metadata and Log Entry Construction

Initial metadata assigns a fresh object to a machine and controller at a specific version.

  initMeta : ObjectId → MachineId → ControllerId → ControllerVersion → ObjectMeta
  initMeta oid mid cid ver = mkMeta oid [] mid cid cid ver ver

Log entries record events with a sequence number, event type, and controller identifier.

  makeLogEntry : EventType → State → LogEntry
  makeLogEntry eventType st = mkLogEntry (getFreshIdCounter st) eventType (State.controllerId st)

Transaction Log Queries

Pending inputs accumulate all inputs directed to an object within the current transaction.

  pendingInputsFor : ObjectId → State → List Input
  pendingInputsFor oid st = collect (State.txLog st)
    where
      collect : List (ObjectId × Input) → List Input
      collect [] = []
      collect ((oid' , inp) ∷ rest) 
        with oid == oid'
      ...  | true  = inp ∷ collect rest
      ...  | false = collect rest

Adding a pending write appends an input to the transaction log.

  addPendingWrite : ObjectId → Input → State → State
  addPendingWrite oid inp st =
    record st { txLog = (State.txLog st) ++ ((oid , inp) ∷ []) }

Pending Transaction Operations

Pending creates are staged object creations committed at transaction end.

  addPendingCreate : ObjectId → Object → ObjectMeta → State → State
  addPendingCreate oid obj meta st =
    record st { creates = (State.creates st) ++ ((oid , obj , meta) ∷ []) }

Removing a pending create cancels a staged creation.

  removePendingCreate : ObjectId → State → State
  removePendingCreate oid st =
    record st { creates = remove (State.creates st) }
    where
      remove : List (ObjectId × Object × ObjectMeta) → List (ObjectId × Object × ObjectMeta)
      remove [] = []
      remove ((oid' , obj , meta) ∷ rest) with oid == oid'
      ... | true  = rest
      ... | false = (oid' , obj , meta) ∷ remove rest

Pending destroys mark objects for deletion at commit.

  addPendingDestroy : ObjectId → State → State
  addPendingDestroy oid st =
    record st { destroys = (State.destroys st) ++ (oid ∷ []) }

Pending transfers schedule ownership changes for commit.

  addPendingTransfer : ObjectId → ControllerId → State → State
  addPendingTransfer oid cid st =
    record st { pendingTransfers = (State.pendingTransfers st) ++ ((oid , cid) ∷ []) }

Read Set Management

Checking whether an object is observed determines if it is in the read set.

  containsObserved : ObjectId → List (ObjectId × ControllerVersion) → Bool
  containsObserved oid [] = false
  containsObserved oid ((oid' , _) ∷ rest) 
      with oid == oid'
  ... | true  = true
  ... | false = containsObserved oid rest

Ensuring an object is observed adds it to the read set if absent.

  ensureObserved : ObjectId → ObjectMeta → State → State
  ensureObserved oid meta st =
    if containsObserved oid (State.observed st)
    then st
    else record st { observed = (State.observed st) ++ ((oid , ObjectMeta.modifiedAtVersion meta) ∷ []) }

Membership in creates is checked during validation.

  inCreates : ObjectId → List (ObjectId × Object × ObjectMeta) → Bool
  inCreates oid [] = false
  inCreates oid ((oid' , _ , _) ∷ rest) with oid == oid'
  ... | true  = true
  ... | false = inCreates oid rest

Membership in destroys is checked during validation.

  inDestroys : ObjectId → List ObjectId → Bool
  inDestroys oid [] = false
  inDestroys oid (oid' ∷ rest) with oid == oid'
  ... | true  = true
  ... | false = inDestroys oid rest

Validation ensures observed versions match current store versions for all read objects.

  validateObserved : State → Bool
  validateObserved st = checkAll (State.observed st)
    where
      checkAll : List (ObjectId × ControllerVersion) → Bool
      checkAll [] = true
      checkAll ((oid , ver) ∷ rest) with inCreates oid (State.creates st)
      ... | true  = checkAll rest
      ... | false with Store.metadata (State.store st) oid
      ...   | nothing = false
      ...   | just meta with ObjectMeta.modifiedAtVersion meta == ver
      ...     | true  = checkAll rest
      ...     | false = false

Ownership checking validates that an object is owned by the current controller.

  checkOwnership : ObjectId → ObjectMeta → State → Bool
  checkOwnership oid meta st = ObjectMeta.currentController meta == State.controllerId st

Applying Transaction Overlays

Applying creates installs all pending object creations into the store.

  applyCreates : List (ObjectId × Object × ObjectMeta) → State → State
  applyCreates [] st = st
  applyCreates ((oid , obj , meta) ∷ rest) st =
    applyCreates rest (createWithMeta obj meta st)

Applying a write updates object metadata with the new input and version.

  applyWrite : ObjectId → Input → State → State
  applyWrite oid inp st with Store.metadata (State.store st) oid
  ... | nothing = st
  ... | just meta =
    let newHistory = ObjectMeta.history meta ++ (inp ∷ [])
        meta' = mkMeta oid newHistory
                  (ObjectMeta.machine meta)
                  (ObjectMeta.creatingController meta)
                  (ObjectMeta.currentController meta)
                  (ObjectMeta.createdAtVersion meta)
                  (State.currentVersion st)
    in updateMeta oid meta' st

Applying writes commits all pending inputs from the transaction log.

  applyWrites : List (ObjectId × Input) → State → State
  applyWrites [] st = st
  applyWrites ((oid , inp) ∷ rest) st =
    applyWrites rest (applyWrite oid inp st)

Destroying an object removes both the object and its metadata from the store.

  applyDestroy : ObjectId → State → State
  applyDestroy oid st =
    record st {
      store = record (State.store st) {
        objects = λ oid' → if oid == oid' then nothing
                          else Store.objects (State.store st) oid'
        ; metadata = λ oid' → if oid == oid' then nothing
                             else Store.metadata (State.store st) oid'
      }
    }

Applying destroys removes all pending object deletions.

  applyDestroys : List ObjectId → State → State
  applyDestroys [] st = st
  applyDestroys (oid ∷ rest) st = applyDestroys rest (applyDestroy oid st)

Applying a transfer updates the current controller field in object metadata.

  applyTransfer : (ObjectId × ControllerId) → State → State
  applyTransfer (oid , targetCid) st with lookupObjectWithMeta oid st
  ... | nothing = st
  ... | just (obj , meta) = updateMeta oid (record meta { currentController = targetCid }) st

Applying transfers commits all pending ownership changes.

  applyTransfers : List (ObjectId × ControllerId) → State → State
  applyTransfers [] st = st
  applyTransfers (x ∷ xs) st = applyTransfers xs (applyTransfer x st)

Object Call Handling

Handling a call invokes the object behavior with accumulated inputs and produces output.

  handleCall : ObjectId → Input → State → Object → ObjectMeta → AVMResult (Maybe Val)
  handleCall oid inp st obj meta with getBehavior obj ((ObjectMeta.history meta) ++ (pendingInputsFor oid st) ++ (inp ∷ []))
  ... | nothing = failure (err-invalid-input oid inp)
  ... | just outputs with State.tx st
  ...   | just _ =
      let output = (if null outputs then nothing else just (head outputs))
          entry = makeLogEntry (ObjectCalled oid inp output) st
          st' = addPendingWrite oid inp st
      in success (mkSuccess output st' (entry ∷ []))
  ...   | nothing =
      let output = (if null outputs then nothing else just (head outputs))
          entry = makeLogEntry (ObjectCalled oid inp output) st
          newHistory = ObjectMeta.history meta ++ (inp ∷ [])
          meta' = mkMeta oid newHistory
                      (ObjectMeta.machine meta)
                      (ObjectMeta.creatingController meta)
                      (ObjectMeta.currentController meta)
                      (ObjectMeta.createdAtVersion meta)
                      (State.currentVersion st)
          st' = updateMeta oid meta' st
      in success (mkSuccess output st' (entry ∷ []))

Instruction Interpreters

Object Instructions

Object creation generates a fresh identifier and installs the object in the store.

  callObjInTx : ObjectId → Input → State → Object → ObjectMeta → AVMResult (Maybe Output)
  callObjInTx oid inp st obj meta with checkOwnership oid meta st
  ... | false = failure (err-cross-controller-tx oid (ObjectMeta.currentController meta))
  ... | true = handleCall oid inp (ensureObserved oid meta st) obj meta

  transferObjInTx : ObjectId → ControllerId → ObjectMeta → State → AVMResult Bool
  transferObjInTx oid targetCid meta st with checkOwnership oid meta st
  ... | false = failure (err-cross-controller-tx oid (ObjectMeta.currentController meta))
  ... | true =
    let stObs = ensureObserved oid meta st
        st' = addPendingTransfer oid targetCid stObs
        entry = makeLogEntry (ObjectTransferred oid (State.controllerId st) targetCid) st
    in success (mkSuccess true st' (entry ∷ []))

  transferObjNoTx : ObjectId → ControllerId → ObjectMeta → State → AVMResult Bool
  transferObjNoTx oid targetCid meta st with checkOwnership oid meta st
  ... | false = failure (err-cross-controller-tx oid (ObjectMeta.currentController meta))
  ... | true =
    let meta' = record meta { currentController = targetCid }
        st' = updateMeta oid meta' st
        entry = makeLogEntry (ObjectTransferred oid (State.controllerId st) targetCid) st
    in success (mkSuccess true st' (entry ∷ []))

  destroyObjInTx : ObjectId → ObjectMeta → State → AVMResult Bool
  destroyObjInTx oid meta st with checkOwnership oid meta st
  ... | false = failure (err-cross-controller-tx oid (ObjectMeta.currentController meta))
  ... | true =
    let stObs = ensureObserved oid meta st
        st' = addPendingDestroy oid stObs
        entry = makeLogEntry (ObjectDestroyed oid) st
    in success (mkSuccess true st' (entry ∷ []))

  destroyObjNoTx : ObjectId → ObjectMeta → State → AVMResult Bool
  destroyObjNoTx oid meta st with checkOwnership oid meta st
  ... | false = failure (err-cross-controller-tx oid (ObjectMeta.currentController meta))
  ... | true =
    let st' = record st {
                store = record (State.store st) {
                  objects = λ oid' → if oid == oid' then nothing
                                    else Store.objects (State.store st) oid'
                  ; metadata = λ oid' → if oid == oid' then nothing
                                       else Store.metadata (State.store st) oid'
                }}
        entry = makeLogEntry (ObjectDestroyed oid) st
    in success (mkSuccess true st' (entry ∷ []))

  executeObj : ∀ {s A} → ObjInstruction s A → State → AVMResult A
  executeObj (createObj val) st with State.tx st
  ... | nothing =
    let oid = freshObjectId (getFreshIdCounter st) in
    let obj = interpretValue val in
    let meta = initMeta oid (State.machineId st) (State.controllerId st) (State.currentVersion st) in
    let entry = makeLogEntry (ObjectCreated oid val) st in
    let st' = createWithMeta obj meta st in
    success (mkSuccess oid st' (entry ∷ []))
  ... | just _ =
    let oid = freshObjectId (getFreshIdCounter st) in
    let obj = interpretValue val in
    let meta = initMeta oid (State.machineId st) (State.controllerId st) (State.currentVersion st) in
    let entry = makeLogEntry (ObjectCreated oid val) st in
    let st' = addPendingCreate oid obj meta st in
    success (mkSuccess oid st' (entry ∷ []))

Object destruction removes the object from the store or stages the removal in a transaction.

  executeObj (destroyObj oid) st with State.tx st | lookupPendingCreate oid st | Store.objects (State.store st) oid | Store.metadata (State.store st) oid
  ... | just _ | just _ | _         | _          =
    let st' = removePendingCreate oid st
        entry = makeLogEntry (ObjectDestroyed oid) st
    in success (mkSuccess true st' (entry ∷ []))
  ... | just _ | nothing | just _    | just meta  = destroyObjInTx oid meta st
  ... | just _ | nothing | just _    | nothing    = failure (err-metadata-corruption oid)
  ... | just _ | nothing | nothing   | _          = failure (err-object-not-found oid)
  ... | nothing | just _ | just _    | just meta = destroyObjNoTx oid meta st
  ... | nothing | just _ | just _    | nothing    = failure (err-metadata-corruption oid)
  ... | nothing | just _ | nothing   | _          = failure (err-object-not-found oid)
  ... | nothing | nothing | just _   | just meta  = destroyObjNoTx oid meta st
  ... | nothing | nothing | just _   | nothing    = failure (err-metadata-corruption oid)
  ... | nothing | nothing | nothing  | _          = failure (err-object-not-found oid)

Calling an object invokes its behavior function with the accumulated history and new input.

  executeObj (call oid inp) st with lookupPendingCreate oid st
  ... | just (obj , meta) = handleCall oid inp st obj meta
  ... | nothing with lookupObjectWithMeta oid st
  ...   | nothing = failure (err-object-not-found oid)
  ...   | just (obj , meta) with State.tx st
  ...     | just _ = callObjInTx oid inp st obj meta
  ...     | nothing = handleCall oid inp st obj meta

Introspection Instructions

The self instruction returns the current object identifier from the execution context.

  executeIntrospect : ∀ {s A} → IntrospectInstruction s A → State → AVMResult A
  executeIntrospect self st = success (mkSuccess (State.self st) st [])

The input instruction returns the current input value from the execution context.

  executeIntrospect input st = success (mkSuccess (State.input st) st [])

The getCurrentMachine instruction returns the physical machine identifier from the execution context.

  executeIntrospect getCurrentMachine st = success (mkSuccess (State.machineId st) st [])

Metadata scrying filters all objects by a predicate on their metadata.

  executeIntrospect (scryMeta pred) st =
    let results = foldr collectMatches [] (allObjectIds st)
    in success (mkSuccess results st [])
    where
      collectMatches : ObjectId → List (ObjectId × ObjectMeta) → List (ObjectId × ObjectMeta)
      collectMatches oid acc with Store.metadata (State.store st) oid
      ... | just meta = if pred meta then (oid , meta) ∷ acc else acc
      ... | nothing = acc

Deep scrying filters objects by a predicate on both the object and its metadata.

  executeIntrospect (scryDeep pred) st =
    let results = foldr collectMatches [] (allObjectIds st)
    in success (mkSuccess results st [])
    where
      collectMatches : ObjectId → List (ObjectId × Object × ObjectMeta) → List (ObjectId × Object × ObjectMeta)
      collectMatches oid acc with Store.objects (State.store st) oid | Store.metadata (State.store st) oid
      ... | just obj | just meta = if pred obj meta then (oid , obj , meta) ∷ acc else acc
      ... | just _ | nothing = acc
      ... | nothing | just _ = acc
      ... | nothing | nothing = acc

Reflection retrieves the metadata of a specific object.

  executeIntrospect (reflect oid) st =
    success (mkSuccess (Store.metadata (State.store st) oid) st [])

Transaction Instructions

Beginning a transaction allocates a fresh transaction identifier and initializes empty overlays.

  executeTx : ∀ {s A} → TxInstruction s A → State → AVMResult A
  executeTx beginTx st =
    let txid = freshTxId (getFreshIdCounter st)
        st' = record st { tx = just txid
                         ; txLog = []
                         ; creates = []
                         ; destroys = []
                         ; observed = []
                         }
        entry = makeLogEntry (TransactionStarted txid) st
    in success (mkSuccess txid st' (entry ∷ []))

Committing a transaction validates the read set and applies all pending changes atomically.

  executeTx (commitTx txid) st 
   with State.tx st
  ... | nothing = failure err-no-active-tx
  ... | just currentTx 
      with txid == currentTx
  ...    | false = failure (err-tx-conflict txid)
  ...    | true 
    with validateObserved st
  ...  | false = failure (err-tx-conflict txid)
  ...  | true =
    let stApplied = applyDestroys (State.destroys st)
                      (applyWrites (State.txLog st)
                        (applyTransfers (State.pendingTransfers st)
                          (applyCreates (State.creates st) st)))
        st' = record stApplied {
                tx = nothing
              ; txLog = []
              ; creates = []
              ; destroys = []
              ; observed = []
              ; pendingTransfers = []
              ; currentVersion = sucVersion (State.currentVersion st)
            }
        entry = makeLogEntry (TransactionCommitted txid) st
    in success (mkSuccess true st' (entry ∷ []))

Aborting a transaction discards all pending changes and clears the transaction state.

  executeTx (abortTx txid) st =
    let st' = record st {
              tx = nothing
              ; txLog = []
              ; creates = []
              ; destroys = []
              ; observed = []
              ; pendingTransfers = []
            }
        entry = makeLogEntry (TransactionAborted txid) st
    in success (mkSuccess tt st' (entry ∷ []))

Pure Computation Instructions

Calling a pure function looks up the function by name and applies it to the arguments.

  executePure : ∀ {s A} → PureInstruction s A → State → AVMResult A
  executePure (callPure name args) st 
   with State.pureFunctions st name
  ... | nothing = success (mkSuccess nothing st [])
  ... | just f = success (mkSuccess (f args) st [])

Registering a pure function adds it to the runtime registry.

  executePure (registerPure name f) st =
    let registry' = λ name' → if name == name' then just f
                              else State.pureFunctions st name'
        st' = record st { pureFunctions = registry' }
    in success (mkSuccess true st' [])

Machine Instructions

Machine instructions manage physical resource location and process migration.

Retrieving an object's machine returns its physical location from metadata.

  executeMachine : ∀ {s A} → MachineInstruction s A → State → AVMResult A
  executeMachine (getMachine oid) st with lookupPendingCreate oid st
  ... | just (_ , meta) = success (mkSuccess (just (ObjectMeta.machine meta)) st [])
  ... | nothing with Store.metadata (State.store st) oid
  ...   | nothing    = success (mkSuccess nothing st [])
  ...   | just meta  = success (mkSuccess (just (ObjectMeta.machine meta)) st [])

Teleporting migrates execution to a different physical machine if reachable. Safety constraint: teleportation is invalid during active transactions.

  executeMachine (teleport mid) st with State.tx st
  ... | just _ = failure (err-invalid-during-tx "teleport")
  ... | nothing =
    if isReachableMachine mid
    then (let st' = record st { machineId = mid }
              entry = makeLogEntry (ExecutionMoved mid (State.machineId st)) st
          in success (mkSuccess true st' (entry ∷ [])))
    else failure (err-machine-unreachable mid)

Moving an object migrates its data to a different physical machine if reachable.

  executeMachine (moveObject oid targetMid) st with lookupObjectWithMeta oid st
  ... | nothing = failure (err-object-not-found oid)
  ... | just (_ , meta) =
    if isReachableMachine targetMid
    then (let meta' = record meta { machine = targetMid }
              st' = updateMeta oid meta' st
              entry = makeLogEntry (ObjectMoved oid (ObjectMeta.machine meta) targetMid) st
          in success (mkSuccess true st' (entry ∷ [])))
    else failure (err-machine-unreachable targetMid)

Controller Instructions

Controller instructions manage logical authority and ownership.

Retrieving the current controller returns the controller identifier from the state.

  executeController : ∀ {s A} → ControllerInstruction s A → State → AVMResult A
  executeController getCurrentController st =
    success (mkSuccess (State.controllerId st) st [])

Retrieving an object's controller checks pending changes before querying the store.

  executeController (getController oid) st with lookupPendingCreate oid st
  ... | just (_ , meta) = success (mkSuccess (just (ObjectMeta.currentController meta)) st [])
  ... | nothing with lookupPendingTransfer oid st | Store.metadata (State.store st) oid | State.tx st
  ...   | just cid | _           | _        = success (mkSuccess (just cid) st [])
  ...   | nothing  | nothing     | _        = success (mkSuccess nothing st [])
  ...   | nothing  | just meta   | just _   = success (mkSuccess (just (ObjectMeta.currentController meta)) (ensureObserved oid meta st) [])
  ...   | nothing  | just meta   | nothing  = success (mkSuccess (just (ObjectMeta.currentController meta)) st [])

Transferring an object assigns it to a new controller immediately or schedules the change in a transaction. Authority requirement: proper authorization is checked via isReachableController.

  executeController (transferObject oid targetCid) st
    with State.tx st | isReachableController targetCid | lookupPendingCreate oid st | lookupObjectWithMeta oid st
  ... | just _ | false | _      | _              = failure (err-controller-unreachable targetCid)
  ... | just _ | true  | just (obj , meta) | _   =
    let st' = addPendingTransfer oid targetCid st
        entry = makeLogEntry (ObjectTransferred oid (State.controllerId st) targetCid) st
    in success (mkSuccess true st' (entry ∷ []))
  ... | just _ | true  | nothing | just (_ , meta) = transferObjInTx oid targetCid meta st
  ... | just _ | true  | nothing | nothing        = failure (err-object-not-found oid)
  ... | nothing | false | _      | _              = failure (err-controller-unreachable targetCid)
  ... | nothing | true  | _      | nothing        = failure (err-object-not-found oid)
  ... | nothing | true  | _      | just (obj , meta) = transferObjNoTx oid targetCid meta st

Retrieving the current version returns the controller's protocol version.

  executeController getCurrentVersion st =
    success (mkSuccess (State.currentVersion st) st [])

Switching versions updates the controller's protocol version if the target is compatible.

  executeController (switchVersion ver) st with State.tx st
  ... | just _ = failure (err-invalid-during-tx "switchVersion")
  ... | nothing =
    if ver ≤v State.currentVersion st
    then (let st' = record st { currentVersion = ver }
              entry = makeLogEntry (ControllerSwitched (State.controllerId st) ver) st
          in success (mkSuccess true st' (entry ∷ [])))
    else success (mkSuccess false st [])

Instruction Set Interpreters

Basic Instruction Set (Instr₀)

The basic instruction set dispatches object and introspection instructions.

  executeInstr₀ : ∀ {s A} → Instr₀ s A → State → AVMResult A
  executeInstr₀ (Obj instr) st = executeObj instr st
  executeInstr₀ (Introspect instr) st = executeIntrospect instr st

Transactional Instruction Set (Instr₁)

The transactional instruction set adds transaction support to basic operations.

  executeInstr₁ : ∀ {s A} → Instr₁ s A → State → AVMResult A
  executeInstr₁ instr st
    with instr
  ... | Obj instr = executeObj instr st
  ... | Introspect instr = executeIntrospect instr st
  ... | Tx instr = executeTx instr st

Extended Instruction Set (Instr₂)

The extended instruction set adds pure computation to transactional operations.

  executeInstr₂ : ∀ {s A} → Instr₂ s A → State → AVMResult A
  executeInstr₂ instr st
    with instr
  ... | Obj instr = executeObj instr st
  ... | Introspect instr = executeIntrospect instr st
  ... | Tx instr = executeTx instr st
  ... | Pure instr = executePure instr st

Full Instruction Set (Instruction)

The full instruction set combines all instruction types for complete AVM functionality.

  executeInstruction : ∀ {s A} → Instruction s A → State → AVMResult A
  executeInstruction instr st
    with instr
  ...  | Obj instr = executeObj instr st
  ...  | Introspect instr = executeIntrospect instr st
  ...  | Tx instr = executeTx instr st
  ...  | Pure instr = executePure instr st
  ...  | Machine instr = executeMachine instr st
  ...  | Controller instr = executeController instr st

Program Interpreters

Generic Interpreter Module

The interpretation logic is identical for all instruction sets. We parameterize the interpreter by the instruction type and execution function to avoid repetition.

  module GenericInterpreter
    (Instr : Safety → ISA)
    (execute : ∀ {s A} → Instr s A → State → AVMResult A)
    where

    {-# TERMINATING #-}
    interpretAux : ∀ {A} → ITree (Instr Safe) A → State → Trace → AVMResult A
    interpretAux prog st trace 
      with observe prog
    ...  | retF x = success (mkSuccess x st trace)
    ...  | tauF prog' = interpretAux prog' st trace
    ...  | visF B instr k 
         with execute instr st
    ...     | failure err = failure err
    ...     | success res =
                interpretAux
                  (k (Success.value res))
                  (Success.state res)
                  (trace ++ Success.trace res)

    interpret 
      : ∀ {A} → 
        ITree (Instr Safe) A → 
        State → 
        -----------
        AVMResult A
    interpret prog st = interpretAux prog st []

Basic Program Interpreter (Instr₀)

The basic program interpreter processes object and introspection instructions.

  open GenericInterpreter Instr₀ executeInstr₀
    renaming (interpret to interpretProgram; interpretAux to interpretProgramAux) public

Transactional Program Interpreter (Instr₁)

The transactional program interpreter handles transaction boundaries during execution.

  open GenericInterpreter Instr₁ executeInstr₁
    renaming (interpret to interpretProgram₁; interpretAux to interpretProgram₁Aux) public

Extended Program Interpreter (Instr₂)

The extended program interpreter processes pure computation alongside other operations.

  open GenericInterpreter Instr₂ executeInstr₂
    renaming (interpret to interpretProgram₂; interpretAux to interpretProgram₂Aux) public

Full AVM Program Interpreter

The full AVM program interpreter executes the complete instruction set including distribution operations.

  open GenericInterpreter Instruction executeInstruction
    renaming (interpret to interpretAVMProgram; interpretAux to interpretAVMProgramAux) public
Module References

Referenced By

This module is referenced by:

References

This module references: