Small Staged Transfer Example

This small example demonstrates how transferObject is staged inside a transaction (overlay) and how the interpreter forbids teleport during an active transaction. It uses the interpretAVMProgram runner from the interpreter.

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

module AVM.SmallExample where

open import Foundation.BasicTypes

-- Minimal concrete instantiation for the interpreter
-- Values and identifiers are naturals for simplicity

Val : Set
Val = ℕ

ObjectId : Set
ObjectId = ℕ

MachineId : Set
MachineId = ℕ

ControllerId : Set
ControllerId = ℕ

ControllerVersion : Set
ControllerVersion = ℕ

TxId : Set
TxId = ℕ

freshObjectId : ℕ → ObjectId
freshObjectId n = n

freshTxId : ℕ → TxId
freshTxId n = n

-- Import Objects module to get Object
open import AVM.Objects Val ObjectId freshObjectId MachineId ControllerId ControllerVersion TxId freshTxId
  using (Object; mkObjType)

-- Import Instruction and Interpreter with Object
open import AVM.Instruction Val ObjectId freshObjectId MachineId ControllerId ControllerVersion TxId freshTxId Object
open import AVM.Interpreter Val ObjectId freshObjectId MachineId ControllerId ControllerVersion TxId freshTxId
                            Object (λ obj → Object.behavior obj)
open import Foundation.InteractionTrees

-- A trivial object type that always succeeds and returns no outputs
simpleObj : Object
simpleObj = mkObjType (λ _ → just ([]))

-- Helpers required by the interpreter

eqNat : ∀ {A : Set} → A → A → Bool
eqNat {A} x y = true

_≤v_ : ControllerVersion → ControllerVersion → Bool
_≤v_ = λ m n → true

getFreshIdCounter : State → ℕ
getFreshIdCounter _ = 0

allObjectIds : State → List ObjectId
allObjectIds _ = []

interpretValue : Val → Object
interpretValue _ = simpleObj

isReachableController : ControllerId → Bool
isReachableController _ = true

isReachableMachine : MachineId → Bool
isReachableMachine _ = true

sucVersion : ControllerVersion → ControllerVersion
sucVersion = suc

-- Instantiate the interpreter with our helpers
module Run = Interpreter eqNat _≤v_ getFreshIdCounter allObjectIds interpretValue isReachableController isReachableMachine sucVersion

open Run

-- Initial state with a single object (id 1) controlled by controller 10

exOid : ObjectId
exOid = 1

exMachine : MachineId
exMachine = 1

exCtrl : ControllerId
exCtrl = 10

meta0 : ObjectMeta
meta0 = mkMeta exOid [] exMachine exCtrl exCtrl 0 0

initStore : Store
initStore = mkStore
  (λ _ → just simpleObj)      -- every id maps to our simple object (for simplicity)
  (λ _ → just meta0)          -- every id maps to the same metadata (for simplicity)

emptyFuns : PureFunctions
emptyFuns _ = nothing

initState : State
initState = record
  { machineId       = exMachine
  ; controllerId    = exCtrl
  ; currentVersion  = 0
  ; store           = initStore
  ; pureFunctions   = emptyFuns
  ; txLog           = []
  ; creates         = []
  ; destroys        = []
  ; observed        = []
  ; pendingTransfers = []
  ; tx              = nothing
  ; self            = exOid
  ; input           = 0
  ; traceMode       = false
  }

-- Program 1: Stage a transfer inside a transaction and observe getController

targetCtrl : ControllerId
targetCtrl = 20

stagedTransferProg : AVMProgram (Maybe ControllerId)
stagedTransferProg =
  trigger (Tx beginTx) >>= λ txid →
  trigger (Controller (transferObject exOid targetCtrl)) >>= λ moved →
  -- Should reflect pending move while in-transaction
  trigger (Controller (getController exOid))

stagedResult : AVMResult (Maybe ControllerId)
stagedResult = interpretAVMProgram stagedTransferProg initState

-- Program 2: Attempt teleport during an active transaction (guarded)

invalidTeleportProg : AVMProgram Bool
invalidTeleportProg =
  trigger (Tx beginTx) >>= λ txid →
  trigger (Machine (teleport targetCtrl))

invalidTeleportResult : AVMResult Bool
invalidTeleportResult = interpretAVMProgram invalidTeleportProg initState

The first program stages a transferObject and queries getController before commit. The interpreter overlays this intent via pendingTransfers, so the query returns the staged target controller. The second program shows that teleport is rejected during an active transaction and yields an ErrInvalidDuringTx error when interpreted.

Module References

References

This module references: