AVM Instruction Examples

view source: Examples.lagda.md

{-# OPTIONS --without-K --type-in-type --guardedness --exact-split #-}
-- (no extra warning flags)
module AVM.Examples where

open import Foundation.BasicTypes
open import Foundation.InteractionTrees

Overview

This module provides concrete examples demonstrating the AVM instruction set defined in AVM.Instruction. We instantiate the parametrized instruction module with:

A canonical S-expression type for values
Object identifiers as pairs of node IDs and strings
A simple oracle for generating fresh object identifiers

Value Type Instantiation

We define a concrete value type for messages in our examples:

data Val : Set where
  VInt : ℕ → Val
  VBool : Bool → Val
  VString : String → Val
  VPair : Val → Val → Val
  VNil : Val
  VList : List Val → Val

Object Identifier Instantiation

We define object identifiers as pairs of node identifiers and local names:

NodeId : Set
NodeId = String

ObjectId : Set
ObjectId = NodeId × String

Fresh ObjectId Oracle

We provide a simple oracle that generates fresh object identifiers by converting a natural number to a string and pairing it with a default node:

freshObjectId : ℕ → ObjectId
freshObjectId n = ("default-node" , nat-to-string n)

MachineId : Set
MachineId = String

ControllerId : Set
ControllerId = String

ControllerVersion : Set
ControllerVersion = ℕ

TxId : Set
TxId = String

freshTxId : ℕ → TxId
freshTxId n = nat-to-string n

This oracle ensures uniqueness by using the counter value directly. In a real implementation, this would need to be replaced with a more sophisticated mechanism that accounts for concurrent object creation and distributed systems.

Module Instantiation

Now we instantiate the object model and instruction set with our concrete types. Both modules are parameterized by the same core types:

-- First instantiate the Objects module with our concrete types
open import AVM.Objects Val ObjectId freshObjectId MachineId ControllerId ControllerVersion TxId freshTxId
  using (Object; Input; Output; InputSequence; mkObjType)

-- Define Message as alias for Val (since Instruction's Message is hidden)
Message : Set
Message = Val

-- Then instantiate the Instruction module, passing Object from Objects
-- Hide Input/Output/Message to avoid name collision since Objects already exports them
open import AVM.Instruction Val ObjectId freshObjectId MachineId ControllerId ControllerVersion TxId freshTxId Object public
  hiding (Input; Output; Message)

Helper Functions

We define helper functions for creating messages and validating responses:

withdraw : ℕ → Message
withdraw n = VList (VString "withdraw" ∷ VInt n ∷ [])

deposit : ℕ → Message
deposit n = VList (VString "deposit" ∷ VInt n ∷ [])

ok? : Val → Bool
ok? (VString "ok") = true
ok? (VString _) = false  -- Any other string
ok? (VInt _) = false
ok? (VBool _) = false
ok? (VPair _ _) = false
ok? VNil = false
ok? (VList _) = false

Transfer Example

This example demonstrates an atomic transfer operation between two account objects. We assume:

An Account object type is defined
Account objects support withdraw and deposit methods that modify a balance field
Two Account objects are identified by fromAcc and toAcc

Given two object identifiers and an amount, we define a transfer function:

kudosTransfer : ObjectId → ObjectId → ℕ → AVMProgram₁ Val
kudosTransfer fromAcc toAcc amount =
  trigger (Tx beginTx) >>= λ txId →
  trigger (Obj(call fromAcc (withdraw amount))) >>= λ mr₁ →
  handleWithdraw txId mr₁
  where
    abortWithMsg : TxId → String → AVMProgram₁ Val
    abortWithMsg txId msg =
      trigger (Tx(abortTx txId)) >>= λ _ →
      ret (VString msg)

    commitWithResult : TxId → AVMProgram₁ Val
    commitWithResult txId =
      trigger (Tx(commitTx txId)) >>= λ success →
      if success then
        ret (VString "transfer-complete")
      else
        ret (VString "commit-failed")

    handleDeposit : TxId → Maybe Val → AVMProgram₁ Val
    handleDeposit txId nothing = abortWithMsg txId "deposit-call-failed"
    handleDeposit txId (just r₂) =
      if ok? r₂ then
        commitWithResult txId
      else
        abortWithMsg txId "deposit-failed"

    handleWithdraw : TxId → Maybe Val → AVMProgram₁ Val
    handleWithdraw txId nothing = abortWithMsg txId "withdraw-call-failed"
    handleWithdraw txId (just r₁) =
      if ok? r₁ then
        (trigger (Obj(call toAcc (deposit amount))) >>= λ mr₂ →
         handleDeposit txId mr₂)
      else
        abortWithMsg txId "insufficient-funds"

The transfer operation is atomic: either both the withdrawal and deposit succeed and are committed, or the transaction is aborted and no state changes occur.

Object Creation and Initialization

Creating a new counter object and performing initial operations:

createCounter : Val → AVMProgram₁ ObjectId
createCounter initialValue =
  trigger (Obj(createObj (VList (VString "counter" ∷ initialValue ∷ [])))) >>= λ counterId →
  trigger (Obj(call counterId (VString "increment"))) >>= λ _ →
  ret counterId

-- Using the counter
counterExample : AVMProgram₁ Val
counterExample =
  createCounter (VInt 0) >>= λ ctr →
  trigger (Obj(call ctr (VString "increment"))) >>= λ _ →
  trigger (Obj(call ctr (VString "increment"))) >>= λ _ →
  trigger (Obj(call ctr (VString "get"))) >>= λ mv₃ →
  handleResult mv₃
  where
    handleResult : Maybe Val → AVMProgram₁ Val
    handleResult nothing = ret (VString "call-failed")
    handleResult (just v₃) = ret v₃  -- Returns VInt 3

The counter maintains its state across calls, demonstrating the stateful nature of objects created through createObj.

Balance Update with Validation

Updating an account balance through message-passing with validation:

updateBalance : ObjectId → Val → AVMProgram₁ Val
updateBalance account v = helper v
  where
    invalidMsg : Val
    invalidMsg = VString "invalid-value-type"

    helper : Val → AVMProgram₁ Val
    helper (VInt n) = updateHelper n
      where
        handleUpdateResult : Maybe Val → AVMProgram₁ Val
        handleUpdateResult nothing = ret (VString "update-call-failed")
        handleUpdateResult (just result) =
          if ok? result then
            ret (VString "balance-updated")
          else
            ret (VString "update-failed")

        updateHelper : ℕ → AVMProgram₁ Val
        updateHelper n =
          if 0 ≤? n then
            -- Get current balance via message
            (trigger (Obj(call account (VString "get-balance"))) >>= λ mOldValue →
             -- Update via message
             trigger (Obj(call account (VList (VString "set-balance" ∷ VInt n ∷ [])))) >>= λ mResult →
             handleUpdateResult mResult)
          else
            ret (VString "invalid-balance")
    helper (VBool _) = ret invalidMsg
    helper (VString _) = ret invalidMsg
    helper (VPair _ _) = ret invalidMsg
    helper VNil = ret invalidMsg
    helper (VList _) = ret invalidMsg

Balance updates are validated before being applied through the object's message interface.

Batch Transfer

Calling a multi-method that operates on multiple objects simultaneously:

transferBatch : List (ObjectId × ObjectId × ℕ) → AVMProgram₁ Val
transferBatch transfers =
  processTransfers transfers
  where
    processTransfers : List (ObjectId × ObjectId × ℕ) → AVMProgram₁ Val
    processTransfers [] = ret (VString "batch-complete")
    processTransfers ((from , to , amount) ∷ rest) =
      kudosTransfer from to amount >>= λ result →
      (if ok? result then
        processTransfers rest
      else
        ret (VString "batch-failed"))

Batch operations can be made atomic by wrapping them in appropriate transaction boundaries.

Object Destruction with Cleanup

Destroying an object after transferring its remaining balance:

closeAccount : ObjectId → ObjectId → AVMProgram₁ Val
closeAccount accountToClose beneficiary =
  -- Get final balance
  trigger (Obj(call accountToClose (VString "get-balance"))) >>= λ mBalance →
  handleBalance mBalance
  where
    closeWithBalance : Val → AVMProgram₁ Val
    closeWithBalance (VInt n) =
      if 0 <? n then
        -- Transfer remaining funds
        (trigger (Obj(call accountToClose (withdraw n))) >>= λ _ →
         trigger (Obj(call beneficiary (deposit n))) >>= λ _ →
         -- Destroy the account
         trigger (Obj(destroyObj accountToClose)) >>= λ _ →
         ret (VString "account-closed"))
      else
        -- No balance, just destroy
        (trigger (Obj(destroyObj accountToClose)) >>= λ _ →
         ret (VString "account-closed-empty"))
    closeWithBalance (VString _) = ret (VString "invalid-balance")
    closeWithBalance (VBool _) = ret (VString "invalid-balance")
    closeWithBalance (VPair _ _) = ret (VString "invalid-balance")
    closeWithBalance VNil = ret (VString "invalid-balance")
    closeWithBalance (VList _) = ret (VString "invalid-balance")

    handleBalance : Maybe Val → AVMProgram₁ Val
    handleBalance nothing = ret (VString "get-balance-failed")
    handleBalance (just balance) = closeWithBalance balance

This ensures no funds are lost when an account is closed - the remaining balance is transferred before destruction using destroyObj.

Stateless Object Examples

This section demonstrates stateless objects as pure functions from input histories to outputs, following the pattern φ : I* ⇀ O from the AVM green paper. These examples illustrate the relationship between the mathematical specification (denotational semantics) and executable implementation (operational semantics).

Each example follows the same structure:

Define message types (Input)
Define a replay function that derives state from history
Define φ as a total function History → Maybe Output
Define step as the operational form: (History × Input) → Maybe (Output × History)

Counter Object (Stateless)

The counter maintains a count by processing increment and decrement messages. The state (current count) is derived entirely from the input history.

Input messages:

data CounterMsg : Set where
  inc : CounterMsg
  dec : CounterMsg

The replay function derives the current count from history:

replay-counter : List CounterMsg → ℕ
replay-counter [] = 0
replay-counter (inc ∷ ms) = suc (replay-counter ms)
replay-counter (dec ∷ ms) with replay-counter ms
... | zero = zero  -- Cannot go below zero
... | suc n = n

The φ function maps complete histories to observable outputs:

φ-counter : List CounterMsg → Maybe ℕ
φ-counter history = just (replay-counter history)

The operational step function processes one input at a time:

step-counter : List CounterMsg → CounterMsg → Maybe (ℕ × List CounterMsg)
step-counter history msg with φ-counter (history ++ (msg ∷ []))
... | just count = just (count , history ++ (msg ∷ []))
... | nothing = nothing

The counter is always defined (total function), demonstrating that not all objects need partiality.

Key-Value Store Object (Stateless)

The KV store supports put, delete, and get operations. The store state is derived from the event history.

Input messages:

data Key : Set where
  key : String → Key

data KVMsg : Set where
  put : Key → Val → KVMsg
  del : Key → KVMsg
  get : Key → KVMsg

Event type for state reconstruction:

data KVEvent : Set where
  put-event : Key → Val → KVEvent
  del-event : Key → KVEvent

-- Store represented as association list
KVStore : Set
KVStore = List (Key × Val)

Helper functions:

postulate
  _≟key_ : Key → Key → Bool
  lookup-kv : Key → KVStore → Maybe Val
  last : {A : Set} → List A → Maybe A
  filter-map : {A B : Set} → (A → Maybe B) → List A → List B

The replay function derives the current store from history:


apply-kv-event : KVStore → KVEvent → KVStore
apply-kv-event store (put-event k v) = (k , v) ∷ filter (λ { (k' , _) → not (k ≟key k') }) store
apply-kv-event store (del-event k) = filter (λ { (k' , _) → not (k ≟key k') }) store

replay-kv : List KVEvent → KVStore
replay-kv [] = []
replay-kv (e ∷ es) = apply-kv-event (replay-kv es) e

The φ function maps histories to outputs (partiality arises from get on missing keys):

-- Convert messages to events and outputs
msg-to-event : KVMsg → Maybe KVEvent
msg-to-event (put k v) = just (put-event k v)
msg-to-event (del k) = just (del-event k)
msg-to-event (get k) = nothing  -- get produces no event

φ-kv-aux : List KVMsg → Maybe KVMsg → Maybe Val
φ-kv-aux history nothing = nothing
φ-kv-aux history (just (put k v)) = just (VString "ok")
φ-kv-aux history (just (del k)) = just (VString "ok")
φ-kv-aux history (just (get k)) =
  let events = filter-map msg-to-event history in
  let store = replay-kv events in
  lookup-kv k store

φ-kv : List KVMsg → Maybe Val
φ-kv [] = nothing  -- Empty history: no output
φ-kv (x ∷ xs) = φ-kv-aux (x ∷ xs) (last (x ∷ xs))

The operational step function:

step-kv : List KVMsg → KVMsg → Maybe (Val × List KVMsg)
step-kv history msg with φ-kv (history ++ (msg ∷ []))
... | just output = just (output , history ++ (msg ∷ []))
... | nothing = nothing  -- get on missing key

The KV store is partial: get operations on missing keys are undefined.

Bank Account Object (Stateless)

The bank account supports deposit, withdraw, and balance query operations. Withdrawals that would result in negative balance are undefined.

Input messages:

data AccountMsg : Set where
  depositMsg : ℕ → AccountMsg
  withdrawMsg : ℕ → AccountMsg
  balanceMsg : AccountMsg

Helper functions:

postulate
  _≥ℕ_ : ℕ → ℕ → Bool
  _-ℕ_ : ℕ → ℕ → ℕ
  init : {A : Set} → List A → List A  -- All but last

The replay function derives current balance from history:

replay-account : List AccountMsg → ℕ
replay-account [] = 0  -- Initial balance
replay-account (depositMsg x ∷ ms) =
  let prev-bal = replay-account ms in
  x +ℕ prev-bal
replay-account (withdrawMsg x ∷ ms) =
  let prev-bal = replay-account ms in
  if prev-bal ≥ℕ x then prev-bal -ℕ x else prev-bal  -- Reject if insufficient
replay-account (balanceMsg ∷ ms) = replay-account ms  -- Query doesn't change state

The φ function maps histories to outputs:

data AccountOutput : Set where
  ok : AccountOutput
  error-insufficient : AccountOutput
  balance-val : ℕ → AccountOutput

φ-account-aux : List AccountMsg → Maybe AccountMsg → Maybe AccountOutput
φ-account-aux history nothing = nothing
φ-account-aux history (just (depositMsg x)) = just ok
φ-account-aux history (just (withdrawMsg x)) =
  let prev-history = init history in
  let bal = replay-account prev-history in
  if bal ≥ℕ x then just ok else nothing  -- undefined if insufficient
φ-account-aux history (just balanceMsg) = just (balance-val (replay-account history))

φ-account : List AccountMsg → Maybe AccountOutput
φ-account [] = nothing  -- No output for empty history
φ-account (x ∷ xs) = φ-account-aux (x ∷ xs) (last (x ∷ xs))

The operational step function:

step-account : List AccountMsg → AccountMsg → Maybe (AccountOutput × List AccountMsg)
step-account history msg with φ-account (history ++ (msg ∷ []))
... | just output = just (output , history ++ (msg ∷ []))
... | nothing = nothing  -- withdrawal with insufficient funds

The bank account is partial: withdrawals exceeding the current balance are undefined.

Properties Demonstrated

These examples illustrate key properties of the AVM object model:

Statelessness. No mutable state exists. State is the equivalence class of input histories inducing identical future behavior.

Behavioral equivalence. Two histories are equivalent if they produce the same future behavior. For the counter, histories [inc, inc, inc] and [inc, inc, inc, inc, dec] are equivalent (both yield count 3).

Prefix closure. All examples satisfy prefix closure: if φ is defined on a history, it is defined on all prefixes.

Partiality. The KV store (get on missing key) and bank account (withdraw exceeding balance) demonstrate undefined behavior.

Denotational-operational correspondence. Each example shows both the denotational form (φ mapping complete histories to outputs) and the operational form (step processing one input at a time). They are equivalent up to currying and totality translation.

Module References

References

This module references:

AVM.Instruction
- Imports: AVMProgram₁, abortTx, beginTx, call, commitTx, createObj, destroyObj
AVM.Objects
- Imports: InputSequence, Object, mkObjType
AVM.Runtime
- Imports: Input, Message, Output
Foundation.BasicTypes
- Imports: Bool, List, Maybe, [], ++, +ℕ, ,, <?, ×, ∷, ≤?, false, filter, if_then_else_, just, not, nothing, suc, true, zero, ℕ
Foundation.InteractionTrees
- Imports: >>=, ret, trigger

?>