Skip to content

Instruction Set

The AVM instruction set architecture (ISA) defines the primitive operations available to AVM programs. The instruction taxonomy is organized into distinct instruction sets, each characterized by specific safety levels and operational capabilities.

Instruction Set Description
Object layer
createObj Create new object by referencing behavior name
destroyObj Mark object for destruction
call Send message to object, receive output synchronously
receive Receive next available message asynchronously
Introspection layer
self Return current object's ID
input Return current input message
getCurrentMachine Return current physical machine ID
getState Return current object's internal state
setState Update current object's internal state
sender Return calling object's ID
Reflection layer
reflect Retrieve object metadata (unsafe)
scryMeta Query objects by metadata predicate (unsafe)
scryDeep Query objects by internals and metadata (unsafe)
Reification layer
reifyContext Capture current execution context as data
reifyTxState Capture transaction state as data (unsafe)
reifyConstraints Capture constraint store as data (unsafe)
Transaction layer
beginTx Start new atomic transaction context
commitTx Commit transaction changes to store
abortTx Abort transaction, discard changes
Pure function layer
callPure Invoke registered pure function
registerPure Register new pure function (unsafe)
updatePure Update existing pure function definition
Machine layer
getMachine Query physical machine location of object
teleport Move execution context to another machine
moveObject Move object data to another machine
fetch Bring object replica to local machine
Controller layer
getCurrentController Return current controller ID
getController Query object's controller
transferObject Transfer object ownership to another controller
freeze Synchronize object replicas for strong consistency
FD constraint layer
newVar Create fresh constraint variable with finite domain
narrow Narrow variable domain by intersection
post Post relational constraint to constraint store
label Select value from variable's domain (search step)
Nondeterminism layer
choose Select value from preference distribution
require Assert constraint for transaction
AVM Instruction Set Architecture

The instruction architecture exhibits hierarchical organization, wherein each successive layer extends the previous layer with additional operational capabilities. While individual instruction families (e.g., ObjInstruction, TxInstruction) are defined independently, the numbered instruction sets (Instr₀, Instr₁, etc.) compose these families in a cumulative layered hierarchy where each level subsumes all capabilities from previous layers.

AVM Instruction Set Module Parameters

This module exhibits parametric polymorphism over types representing values, object behaviours, transactions, and distributed execution infrastructure (encompassing both physical machines and logical controllers).

Module Parameters 
module AVM.Instruction
    -- Core types
    (Val : Set)                      -- Used for both Input and Output currently
    (ObjectId : Set)

    -- Machine/distribution types
    (MachineId : Set)

    -- Controller/distribution types
    (ControllerId : Set)

    -- Transaction types
    (TxId : Set)

    -- Object behaviour type
    -- In concrete instantiations, this is AVMProgram (List Val)
    (ObjectBehaviour : Set)
  where

open import AVM.Context
  Val
  ObjectId
  MachineId
  ControllerId
  TxId
  ObjectBehaviour
  public

AVM Instruction Set Algebraic Datatypes

The instruction sets are formalised as inductive algebraic datatypes, wherein each data constructor represents a distinct instruction within the corresponding instruction set family.

Each instruction set datatype is indexed by a safety level parameter that characterises the security properties of instructions within the set. The safety level indexing enables compile-time enforcement of the invariant that safe programs cannot invoke unsafe operations, thereby providing static safety guarantees.

The instruction set architecture uses the following type-level signature:

ISA : Set
ISA = Set -> Set

The ISA type represents an instruction signature family wherein each instruction is indexed by its return type ISA, thereby establishing ISA as a parameterised type family.

Safety Datatype

The specification defines two distinct safety levels: Safe and Unsafe. Instructions are classified as unsafe when their execution violates foundational principles of the object model encapsulation properties or introduces systemic security risks to the virtual machine execution environment.

data Safety : Set where
  Safe   : Safety
  Unsafe : Safety

Object Lifecycle and Communication Instructions

The object instruction family constitutes the foundational layer of the AVM ISA hierarchy. This layer provides primitive object-oriented operations encompassing object lifecycle management (creation and destruction) and inter-object communication realized through message-passing semantics.

ObjInstruction datatype

-- Object lifecycle and communication
data ObjInstruction : Safety → ISA where
  -- Object lifecycle
  createObj : String → Maybe ControllerId → ObjInstruction Safe ObjectId
  destroyObj : ObjectId → ObjInstruction Safe Bool  -- May fail if object doesn't exist

  -- Message passing (may fail if object doesn't exist or rejects input)
  call : ObjectId → Input → ObjInstruction Safe (Maybe Output)

  -- Asynchronous message reception (waits for next message)
  receive : ObjInstruction Safe (Maybe Input)

These instructions realise the fundamental object-oriented programming model within the AVM. Objects are created through createObj, terminated via destroyObj, and interact through synchronous message-passing using the call instruction. The receive instruction allows objects to wait for incoming messages from other objects or the runtime environment and pattern match on the received message.

Runtime Introspection Instructions

The introspection instruction family constitutes the second layer of the AVM ISA hierarchy. This layer provides primitive introspection operations enabling programs to query their own execution context—the current object's identity, input, internal state, and caller information.

Introspection is distinguished from reflection: introspection examines the self (current execution context), while reflection examines others (external objects' metadata and internals).

IntrospectInstruction Datatype

Introspection instructions provide capabilities for querying and updating the current object's own execution context. All introspection operations are safe because they only access information the executing object legitimately owns.

data IntrospectInstruction : Safety → ISA where
  self : IntrospectInstruction Safe ObjectId
  input : IntrospectInstruction Safe Input
  getCurrentMachine : IntrospectInstruction Safe MachineId
  getState : IntrospectInstruction Safe (List Val)
  setState : List Val → IntrospectInstruction Safe ⊤
  sender : IntrospectInstruction Safe (Maybe ObjectId)

Runtime Reflection Instructions

The reflection instruction family provides capabilities for examining other objects' metadata and internal state without invoking their message-passing interface. Reflection breaks object encapsulation by exposing information that objects do not voluntarily reveal through their public interface.

All reflection operations are unsafe because they violate the encapsulation principle that objects exclusively control what information they expose to external observers.

ReflectInstruction Datatype

data ReflectInstruction : Safety → ISA where
  reflect : ObjectId → ReflectInstruction Unsafe (Maybe ObjectMeta)

  scryMeta
    : (ObjectMeta → Bool) →
      ReflectInstruction Unsafe (List (ObjectId × ObjectMeta))

  scryDeep
    : (ObjectBehaviour → ObjectMeta → Bool) →
      ReflectInstruction Unsafe (List RuntimeObjectWithId)

The reflect instruction retrieves metadata for a specified object identifier without invoking the object's message-passing interface. This operation violates the encapsulation principle that objects exclusively control the information they expose to external observers.

The scryMeta instruction performs predicate-based queries over the object store, selecting objects whose metadata satisfies a specified boolean predicate. The instruction returns pairs of object identifiers and corresponding metadata for all matching entities.

The scryDeep instruction extends this capability by enabling predicate evaluation over both object internal state and metadata, returning the complete object representation. Both instructions require complete store traversal, introducing computational complexity risks scaling linearly with the total object population.

Reification Instructions

Reification is the mechanism for encoding execution state as first-class data. While introspection queries the current context and reflection examines other objects, reification captures runtime state structures as values that can be stored, transmitted, or later analyzed.

Reification enables:

  • Debugging: Capturing execution snapshots for post-mortem analysis
  • Migration: Serializing execution state for process migration
  • Checkpointing: Creating restorable execution snapshots
  • Auditing: Recording execution state for compliance verification

ReifyInstruction Datatype

  • Reified execution context (safe subset of State)
record ReifiedContext : Set where
  constructor mkReifiedContext
  field
    contextSelf : ObjectId
    contextInput : Input
    contextSender : Maybe ObjectId
    contextMachine : MachineId
    contextController : ControllerId
  • Reified transaction state
record ReifiedTxState : Set where
  constructor mkReifiedTxState
  field
    txStateId : Maybe TxId
    txStateWrites : List (ObjectId × Input)
    txStateCreates : List ObjectId
    txStateDestroys : List ObjectId
    txStateObserved : List ObjectId
  • Reified constraint store (for FD layer)
record ReifiedConstraints : Set where
  constructor mkReifiedConstraints
  field
    -- Variable domains: list of (variable id, current domain values)
    constraintVars : List (ℕ × List Val)
    -- Posted constraints (simplified representation)
    constraintCount : ℕ

data ReifyInstruction : Safety → ISA where
  -- Safe: reify own execution context
  reifyContext : ReifyInstruction Safe ReifiedContext

  -- Unsafe: reify transaction state (exposes pending writes)
  reifyTxState : ReifyInstruction Unsafe (Maybe ReifiedTxState)

  -- Unsafe: reify constraint store (exposes solver state)
  reifyConstraints : ReifyInstruction Unsafe ReifiedConstraints

The reifyContext instruction captures the current execution frame as a first-class value. This is safe because it only accesses information already available through individual introspection instructions.

The reifyTxState instruction captures the current transaction's pending state including uncommitted writes, creates, and destroys. This is unsafe because it exposes tentative state that may be rolled back.

The reifyConstraints instruction captures the constraint solver's internal state including variable domains and constraint counts. This is unsafe because it exposes solver internals that programs should not depend on.

Instr₀: The Minimal Instruction Set

The foundational instruction layers are composed to form the minimal instruction set, designated Instr₀.

This constitutes the foundational instruction set in the AVM ISA hierarchy, encompassing the base object lifecycle operations, runtime introspection, reflection, and reification capabilities.

data Instr₀ : Safety → ISA where
  Obj : ∀ {s A} → ObjInstruction s A → Instr₀ s A
  Introspect : ∀ {s A} → IntrospectInstruction s A → Instr₀ s A
  Reflect : ∀ {s A} → ReflectInstruction s A → Instr₀ s A
  Reify : ∀ {s A} → ReifyInstruction s A → Instr₀ s A

open import Background.InteractionTrees

TxInstruction datatype

This is the third layer of the AVM ISA. It provides the fundamental transactional operations for managing atomic execution contexts.

data TxInstruction : Safety → ISA where
  beginTx : Maybe ControllerId → TxInstruction Safe TxId
  commitTx : TxId → TxInstruction Safe Bool      -- May fail if conflicts
  abortTx : TxId → TxInstruction Safe ⊤

Instr₁ instruction set, adds transactional support

Programs that can roll back changes are possible via TxInstruction. With this feature, we can define our second instruction set, Instr₁:

data Instr₁ : Safety → ISA where
  Obj : ∀ {s A} → ObjInstruction s A → Instr₁ s A
  Introspect : ∀ {s A} → IntrospectInstruction s A → Instr₁ s A
  Reflect : ∀ {s A} → ReflectInstruction s A → Instr₁ s A
  Reify : ∀ {s A} → ReifyInstruction s A → Instr₁ s A
  Tx : ∀ {s A} → TxInstruction s A → Instr₁ s A

PureInstruction datatype

This is the fourth layer of the AVM ISA. This step adds means to call pure functions, register new pure functions, and update existing pure functions. Thus, think of this as a capability to extend the any instruction set with deterministic computation. For example adding arbitrary arithmetic operations to the instruction set.

data PureInstruction : Safety → ISA where
  -- Call a registered pure function by identifier
  callPure : String → List Val → PureInstruction Safe (Maybe Val)

  -- Register new pure function (unsafe - extends the function set)
  registerPure : String → (List Val → Maybe Val) → PureInstruction Unsafe Bool

  -- Update function definition for a given function identifier
  updatePure : String → (List Val → Maybe Val) → PureInstruction Safe Bool

Instr₂ instruction set, adds pure function computation

With the ability to call pure functions, we can define our third instruction set, Instr₂, which adds pure function computation to the transactional instruction set:

data Instr₂ : Safety → ISA where
  Obj : ∀ {s A} → ObjInstruction s A → Instr₂ s A
  Introspect : ∀ {s A} → IntrospectInstruction s A → Instr₂ s A
  Reflect : ∀ {s A} → ReflectInstruction s A → Instr₂ s A
  Reify : ∀ {s A} → ReifyInstruction s A → Instr₂ s A
  Tx : ∀ {s A} → TxInstruction s A → Instr₂ s A
  Pure : ∀ {s A} → PureInstruction s A → Instr₂ s A

Distribution Layer: Machine and Controller Instructions

This is the fifth layer of the AVM ISA, which provides instructions for managing distributed execution across physical machines and logical controllers.

AVM programs execute in a distributed environment with two orthogonal concepts: physical machines (where computation and storage occur) and logical controllers (who order transactions and own objects). This separation enables independent reasoning about data consistency, locality, and authority.

We split the distribution layer into two instruction families to maintain clear separation of concerns, enable independent testing, and support distinct policy enforcement for physical versus logical operations.

MachineInstruction datatype

Machines are physical nodes that host computation and object data. Programs can query which machine holds an object's data and move execution or data objects between machines. Machine operations deal with physical resource location and object data migration.

data MachineInstruction : Safety → ISA where
  -- Query physical machine location of object data
  getMachine : ObjectId → MachineInstruction Safe (Maybe MachineId)

  -- Move execution context (process) to another machine
  teleport : MachineId → MachineInstruction Safe Bool

  -- Move object data to another machine (changes physical location)
  moveObject : ObjectId → MachineId → MachineInstruction Safe Bool

  -- Bring object replica to local machine for local access
  fetch : ObjectId → MachineInstruction Safe Bool

Safety constraints: teleport is invalid during active transactions. Attempting to teleport while a transaction is in progress should result in an error.

ControllerInstruction datatype

Controllers are logical authorities that order transactions and own object consistent state. Each object records which controller created it, which controller currently owns it. Programs can query controller ownership and transfer objects between controllers without moving their physical location. Controller operations deal with logical resource location and object data consistency.

data ControllerInstruction : Safety → ISA where
  -- Query controller identity and ownership
  getCurrentController : ControllerInstruction Safe (Maybe ControllerId)
  getController : ObjectId → ControllerInstruction Safe (Maybe ControllerId)

  -- Transfer object ownership to another controller (changes logical authority)
  transferObject : ObjectId → ControllerId → ControllerInstruction Safe Bool

  -- Freeze: synchronize all replicas through the controller for strong consistency
  -- When multiple machines have fetched the same object, freeze reconciles their state
  -- Returns: nothing (no controller), just true (success), just false (object missing/unreachable)
  freeze : ObjectId → ControllerInstruction Safe (Maybe Bool)

Authority requirements: transferObject requires proper authorization. The current controller must have authority to transfer the object.

Instr₃ instruction set, adds distributed operations

With machine and controller instructions, we can now define our fourth instruction set, Instr₃. This instruction set adds distributed computing capabilities to the pure function instruction set.

data Instr₃ : Safety → ISA where
  Obj : ∀ {s A} → ObjInstruction s A → Instr₃ s A
  Introspect : ∀ {s A} → IntrospectInstruction s A → Instr₃ s A
  Reflect : ∀ {s A} → ReflectInstruction s A → Instr₃ s A
  Reify : ∀ {s A} → ReifyInstruction s A → Instr₃ s A
  Tx : ∀ {s A} → TxInstruction s A → Instr₃ s A
  Pure : ∀ {s A} → PureInstruction s A → Instr₃ s A
  Machine : ∀ {s A} → MachineInstruction s A → Instr₃ s A
  Controller : ∀ {s A} → ControllerInstruction s A → Instr₃ s A

Finite Domain Constraint Programming Layer

This is the sixth layer of the AVM ISA, which introduces finite domain (FD) instructions that enable constraint-based programming where computation proceeds through constraint propagation and search over symbolic variables with call-time choice semantics.

Variables are created with finite domains, domains are narrowed through constraint propagation, and search proceeds by labeling variables with concrete values. When labeling leads to constraint failure (domain emptying), transaction rollback (abortTx) provides the backtracking mechanism to explore alternative search paths.

Supporting Types for Constraint Programming

  • Variable identifiers for constraint variables
record VarId : Set where
  constructor mkVarId
  field
    varId : ℕ
  • Finite domain: a set of possible values
Domain : Set
Domain = List Val
  • Relational constraints between variables and values
data Constraint : Set where
  -- Equality: var₁ = var₂
  Eq : VarId → VarId → Constraint

  -- Inequality: var₁ ≠ var₂
  Neq : VarId → VarId → Constraint

  -- Ordering constraints between variables
  -- Less than or equal: var₁ ≤ var₂
  Leq : VarId → VarId → Constraint

  -- Less than: var₁ < var₂
  Lt : VarId → VarId → Constraint

  -- Greater than or equal: var₁ ≥ var₂
  Geq : VarId → VarId → Constraint

  -- Greater than: var₁ > var₂
  Gt : VarId → VarId → Constraint

  -- All-different: all variables must take distinct values
  AllDiff : List VarId → Constraint

  -- Value constraints: compare a variable to a concrete value
  -- var = value
  ValEq : VarId → Val → Constraint

  -- var ≤ value
  ValLeq : VarId → Val → Constraint

  -- var < value
  ValLt : VarId → Val → Constraint

  -- var ≥ value
  ValGeq : VarId → Val → Constraint

  -- var > value
  ValGt : VarId → Val → Constraint

FDInstruction datatype

The FD instruction family provides instructions for creating, narrowing, and posting constraints on constraint variables.

data FDInstruction : Safety → ISA where
  -- Create a fresh symbolic variable with an initial finite domain
  newVar : Domain → FDInstruction Safe VarId

  -- Narrow the domain of an existing variable (intersection); false if emptied
  -- TODO: investigate if this is really needed.
  narrow : VarId → Domain → FDInstruction Safe Bool

  -- Post a relational constraint (e.g., equality/inequality/distinctness)
  -- Triggers constraint propagation to narrow related variable domains
  post : Constraint → FDInstruction Safe Bool

  -- Labeling: select value from variable's domain (search step with call-time choice)
  -- Transaction abort (abortTx) provides backtracking when constraints fail
  label : VarId → FDInstruction Safe Val

Experimental Instruction Families

The following instruction families support intent-based programming and multi-party coordination. These are experimental features for prototyping advanced AVM capabilities.

Nondeterminism Instructions

Nondeterminism instructions enable preference-directed selection and constraint validation at transaction commit time. These instructions are suited for multi-party intent matching where constraints accumulate during execution and are evaluated atomically when the transaction commits.

Nondeterministic constraints (NondetConstraint) differ from finite domain constraints (Constraint) in their evaluation semantics: nondeterministic constraints represent assertions validated atomically at commit time, whereas finite domain constraints are symbolic relations between variables that trigger incremental propagation.

data NondetConstraint : Set where
  -- Assert that a boolean condition must hold at transaction commit
  Assert : Bool → NondetConstraint

data NondetInstruction : Safety → ISA where
  -- Choose a value nondeterministically from available options
  -- Runtime may use preferences, weights, or solver guidance
  choose : List Val → NondetInstruction Safe Val

  -- Assert constraint that must hold at transaction commit
  -- All accumulated constraints are validated atomically when commitTx executes
  require : NondetConstraint → NondetInstruction Safe ⊤

Choosing Between FD and NonDet Layers

The FD and NonDet layers serve complementary purposes with incompatible execution models.

Finite Domain (Call-Time Choice)

  1. Execution Model:

    1. Values selected immediately when label executes
    2. Constraint propagation occurs incrementally after each post
    3. Transaction rollback, via abortTx, provides backtracking for search
    4. Domains narrow eagerly as constraints are posted

  2. Suitable for:

    1. Single-agent CSP solving (TODO: add examples of N-Queens, Sudoku, scheduling)
    2. Search algorithms requiring systematic exploration
    3. Problems benefiting from incremental constraint propagation
    4. Resource allocation with backtracking

Nondeterminism (Commit-Time Validation)

  1. Execution Model:

    1. Choices recorded but deferred until transaction commit, via choose
    2. Constraints accumulate and validate atomically at transaction commit, via commitTx
    3. Enables composition of multiple parties' preferences
    4. Solver considers all constraints simultaneously

  2. Suitable for:

    1. Intent matching and multi-party coordination
    2. Preference-directed selection with solver guidance

The Instruction datatype

The Instruction datatype combines all instructions so far defined, including experimental ones, and provides ergonomic pattern synonyms for a flat instruction namespace.

-- Union datatype combining all instruction families
data Instruction : Safety → ISA where
  Obj : ∀ {s A} → ObjInstruction s A → Instruction s A
  Introspect : ∀ {s A} → IntrospectInstruction s A → Instruction s A
  Reflect : ∀ {s A} → ReflectInstruction s A → Instruction s A
  Reify : ∀ {s A} → ReifyInstruction s A → Instruction s A
  Tx : ∀ {s A} → TxInstruction s A → Instruction s A
  Pure : ∀ {s A} → PureInstruction s A → Instruction s A
  Machine : ∀ {s A} → MachineInstruction s A → Instruction s A
  Controller : ∀ {s A} → ControllerInstruction s A → Instruction s A
  FD : ∀ {s A} → FDInstruction s A → Instruction s A
  Nondet : ∀ {s A} → NondetInstruction s A → Instruction s A

Pattern Synonyms for convenience

Pattern synonyms provide a flat namespace for common instructions, eliminating the need for nested constructors when writing AVM programs. These patterns can also be used for pattern matching on instructions. It is a matter of using Agda here to describe the instruction set and pattern matching on it.

Also, it can be seen as the list of all instructions in the instruction set.

-- Object instruction patterns
pattern obj-create behaviorName mcid = Obj (createObj behaviorName mcid)
pattern obj-destroy oid = Obj (destroyObj oid)
pattern obj-call oid inp = Obj (call oid inp)
pattern obj-receive = Obj receive

-- Introspection instruction patterns (self-examination)
pattern get-self = Introspect self
pattern get-input = Introspect input
pattern get-current-machine = Introspect getCurrentMachine
pattern get-state = Introspect getState
pattern set-state newState = Introspect (setState newState)
pattern get-sender = Introspect sender

-- Reflection instruction patterns (examining others - unsafe)
pattern obj-reflect oid = Reflect (reflect oid)
pattern obj-scry-meta pred = Reflect (scryMeta pred)
pattern obj-scry-deep pred = Reflect (scryDeep pred)

-- Reification instruction patterns (capturing state as data)
pattern do-reify-context = Reify reifyContext
pattern do-reify-tx-state = Reify reifyTxState
pattern do-reify-constraints = Reify reifyConstraints

-- Transaction instruction patterns
pattern tx-begin mcid = Tx (beginTx mcid)
pattern tx-commit tid = Tx (commitTx tid)
pattern tx-abort tid = Tx (abortTx tid)

-- Pure function instruction patterns
pattern call-pure name args = Pure (callPure name args)
pattern register-pure name fn = Pure (registerPure name fn)
pattern pure-update-pure name fn = Pure (updatePure name fn)

-- Machine instruction patterns (physical location and process migration)
pattern get-machine oid = Machine (getMachine oid)
pattern do-teleport mid = Machine (teleport mid)
pattern move-object oid mid = Machine (moveObject oid mid)
pattern fetch-object oid = Machine (fetch oid)

-- Controller instruction patterns (logical authority and ownership)
pattern get-current-controller = Controller getCurrentController
pattern get-controller oid = Controller (getController oid)
pattern transfer-object oid cid = Controller (transferObject oid cid)
pattern freeze-object oid = Controller (freeze oid)

The Instruction type provides the full AVM instruction set in a single datatype:

AVMProgram : Set → Set
AVMProgram = ITree (Instruction Safe)

Object Behaviour Instantiation Note

In the AVM operational model, the ObjectBehaviour module parameter is concretely instantiated as AVMProgram (List Val) in implementations. This establishes that runtime objects are pairs of (ObjectBehaviour × ObjectMeta) - executable AVM programs paired with runtime metadata.

This design combines compositionality (instruction families as separate types) with ergonomics (pattern synonyms for flat naming). Programs can use either the layered approach (Instr₀, Instr₁, etc.) for compositional reasoning or the unified Instruction type for convenience.

Instruction Set Operational Semantics

The AVM specification provides multiple instruction sets, systematically organized by operational capability and safety classification. This section establishes comprehensive operational semantics for all instruction types within the ISA hierarchy. Each instruction specification includes its associated safety level classification and return type signature.

The instruction set organization by instruction family follows this taxonomy:

  1. ObjInstruction: Object instructions: Object lifecycle and communication
  2. IntrospectInstruction: Introspection instructions: Self-examination of current execution context
  3. ReflectInstruction: Reflection instructions: Examining other objects' metadata and internals (unsafe)
  4. ReifyInstruction: Reification instructions: Capturing execution state as first-class data
  5. TxInstruction: Transaction instructions: Atomic execution contexts
  6. PureInstruction: Pure function instructions: Deterministic computation via function registry
  7. MachineInstruction: Machine instructions: Physical location and process migration
  8. ControllerInstruction: Controller instructions: Logical authority and ownership transfer

Object Lifecycle Operations

Object lifecycle instructions provide primitive operations for managing object creation and destruction within the persistent object store.

createObj

createObj : String → Maybe ControllerId → ObjInstruction Safe ObjectId

Creates a new runtime object within the persistent store by referencing a behavior name. The first eqString parameter specifies the behavior name that will be resolved by the interpreter to an ObjectBehaviour (an AVM program). The second Maybe ControllerId parameter optionally specifies the controller that should own the object:

  • just controllerId: The object is created with the specified controller as both creatingController and currentController fields in ObjectMeta
  • nothing: If within a transaction, the object is created with the transaction's controller. If outside a transaction, the object is created without a controller (both controller fields are nothing)

The instruction returns a fresh ObjectId that uniquely identifies the newly created runtime object within the global object namespace. Object creation exhibits transactional semantics: if the enclosing transaction context aborts, the object creation is rolled back and the runtime object does not persist to the store.

destroyObj

destroyObj : ObjectId → ObjInstruction Safe Bool

Marks the runtime object identified by the given ObjectId for destruction. Returns true if destruction succeeds, false if the runtime object does not exist. The runtime object (both behavior and metadata) is removed from the store, and subsequent references to this ObjectId will fail. Destruction is transactional: the object remains accessible within the current transaction until committed.

Object Interaction

Object interaction is achieved through pure message-passing, preserving object encapsulation. Message passing is the only way to interact with objects in the AVM.

call

call : ObjectId → Input → ObjInstruction Safe (Maybe Output)

Performs synchronous message passing to the object identified by the given ObjectId. Sends the input and blocks until the target object produces an output. Returns nothing if the object does not exist or rejects the input, otherwise returns just the output produced by the target object.

receive

receive : ObjInstruction Safe (Maybe Input)

Receives the next available message for the current object. This instruction enables asynchronous message reception, allowing objects to retrieve incoming messages from other objects or the runtime system.

The blocking behavior is platform-specific: runtime implementations may choose to make this instruction blocking (waiting until a message arrives) or non-blocking (returning immediately). The return type Maybe Input accommodates both: - Blocking implementations: always return just a message (blocking until one arrives) - Non-blocking implementations: return just a message if available, or nothing if the message queue is empty

Consult your runtime's documentation for its specific message reception semantics.

This differs from input (see introspection below), which only exposes the message that triggered the current activation. receive dequeues the next message (and may block waiting), while input is a pure read of the current call context that neither waits nor consumes the queue.

Introspection (Self-Examination)

Introspection instructions query the current object's own execution context. These are safe operations because they only access information the executing object legitimately owns.

self

self : IntrospectInstruction Safe ObjectId

Returns the ObjectId of the currently executing object. This instruction is essential for recursion and self-reference, allowing an object to pass its own identifier to other objects or invoke itself.

input

input : IntrospectInstruction Safe Input

Returns the input being processed by the current object. This instruction provides access to the message sent to the current object.

getCurrentMachine

getCurrentMachine : IntrospectInstruction Safe MachineId

Returns the identifier of the physical machine currently executing this program. This instruction enables programs to reason about their execution location, which is independent of controller identity. Machine information is useful for data locality optimizations and understanding cross-machine communication costs.

getState

getState : IntrospectInstruction Safe (List Val)

Returns the current internal state of the executing object. The state is a list of values that the object maintains across invocations. Initially, all objects have an empty state []. Objects update their state using the setState instruction. This enables objects to maintain explicit state rather than deriving state from input history.

setState

setState : List Val → IntrospectInstruction Safe ⊤

Updates the internal state of the currently executing object. The provided list of values replaces the current state entirely. State changes are persisted when the enclosing transaction commits (if within a transaction) or immediately (if outside a transaction). This instruction allows objects to maintain and evolve their internal state explicitly.

sender

sender : IntrospectInstruction Safe (Maybe ObjectId)

Returns the ObjectId of the calling object when invoked from within a call instruction. Returns nothing for top-level execution contexts or when no caller exists. This instruction enables objects to verify the origin of received messages and implement access control policies based on caller identity.

Reflection (Examining Others)

Reflection instructions examine other objects' metadata and internal state, breaking object encapsulation. All reflection operations are unsafe because they violate the principle that objects exclusively control what information they expose.

reflect (Unsafe)

reflect : ObjectId → ReflectInstruction Unsafe (Maybe ObjectMeta)

Retrieves metadata about the object identified by the given ObjectId. Returns nothing if the object does not exist, otherwise returns just the object's metadata. Marked as unsafe because it bypasses object encapsulation.

scryMeta (Unsafe)

scryMeta : (ObjectMeta → Bool) → ReflectInstruction Unsafe (List (ObjectId × ObjectMeta))

Queries the store for objects whose metadata satisfies the given predicate. Returns pairs of object identifiers and metadata for all matching objects. This instruction traverses the entire store, applying the predicate to each object's metadata. Typical queries include finding all objects created by a specific controller, objects on a particular machine, or objects with a specific current controller. Marked unsafe because enumeration scales with total object count.

scryDeep (Unsafe)

scryDeep : (ObjectBehaviour → ObjectMeta → Bool) → ReflectInstruction Unsafe (List RuntimeObjectWithId)

Queries the store for runtime objects (object behaviours paired with metadata) that satisfy the given predicate. Returns complete runtime object data for all matches. This instruction breaks encapsulation by exposing raw ObjectBehaviour values. Use cases include deep inspection for debugging, auditing, or migration. Marked unsafe for both encapsulation violation and unbounded computation.

Reification (Capturing State as Data)

Reification instructions encode execution state as first-class data values that can be stored, transmitted, or analyzed. While introspection queries context and reflection examines others, reification captures runtime structures as values.

reifyContext

reifyContext : ReifyInstruction Safe ReifiedContext

Captures the current execution frame as a first-class value containing the current object ID, input, sender, machine, and controller. This is safe because it only packages information already available through individual introspection instructions.

reifyTxState (Unsafe)

reifyTxState : ReifyInstruction Unsafe (Maybe ReifiedTxState)

Captures the current transaction's pending state as a first-class value, including the transaction ID, uncommitted writes, pending creates and destroys, and observed objects. Returns nothing if no transaction is active. Marked unsafe because it exposes tentative state that may be rolled back, potentially leaking information about uncommitted operations.

reifyConstraints (Unsafe)

reifyConstraints : ReifyInstruction Unsafe ReifiedConstraints

Captures the constraint solver's internal state as a first-class value, including variable domains and constraint counts. Marked unsafe because it exposes solver internals that programs should not depend upon for correctness.

Transaction Control

Transaction control instructions manage atomic execution contexts. All state modifications within a transaction are tentative until committed.

beginTx

beginTx : Maybe ControllerId → TxInstruction Safe TxId

Initiates a new transactional context with an optional controller parameter and returns a fresh transaction identifier. The controller determines the execution context for the transaction:

  • just controllerId: Immediately locks the transaction to the specified controller. All objects accessed must belong to this controller.
  • nothing: Defers controller selection. The transaction controller is resolved from the first object accessed (via operations like call, destroyObj, transferObject, etc.).

All subsequent state modifications are logged to the transaction's write-set until the transaction is either committed or aborted. Transactions provide atomicity: either all changes succeed or none do. The single-controller invariant ensures all objects in a transaction belong to the same controller.

commitTx

commitTx : TxId → TxInstruction Safe Bool

Attempts to commit the transaction identified by the given TxId. Returns true if the commit succeeds, persisting all logged changes to the store. Returns false if the transaction cannot be committed due to conflicts with concurrent transactions or if the transaction was already finalized.

abortTx

abortTx : TxId → TxInstruction Safe ⊤

Aborts the transaction identified by the given TxId, discarding all tentative state changes in its write-set. The store reverts to its state before beginTx was called. This operation always succeeds and returns unit.

Pure Function Instructions

Pure function instructions provide deterministic computation capabilities through an extensible function registry.

callPure

callPure : String → List Val → PureInstruction Safe (Maybe Val)

Invokes a registered pure function by identifier with the given arguments. Returns the function result or nothing if the function doesn't exist or the arguments don't match the expected arity.

registerPure (Unsafe)

registerPure : String → (List Val → Maybe Val) → PureInstruction Unsafe Bool

Registers a new pure function in the function registry. Marked as unsafe because it extends the global function set, potentially affecting system-wide computation.

updatePure

updatePure : String → (List Val → Maybe Val) → PureInstruction Safe Bool

Updates the function definition of a registered pure function identified by the given string name. This instruction replaces the existing function definition in the pure function registry with the new function provided. The first parameter is the function identifier (name), and the second parameter is the new function definition. Returns true if the update succeeds (the function exists and was updated), false if the function does not exist in the registry or the update fails. This instruction enables dynamic modification of pure function implementations while maintaining deterministic computation semantics.

Pure function instructions modify the execution environment (the pureFunctions field of State), not the object store. These changes take effect immediately and affect all subsequent execution system-wide.

Machine Instructions

Machine instructions manage physical resource location and process migration in distributed AVM deployments. These operations deal with where computation executes and where object data physically resides.

getMachine

getMachine : ObjectId → MachineInstruction Safe (Maybe MachineId)

Returns the physical machine where the specified object's data resides, or nothing if the object doesn't exist. The machine location is independent of controller ownership. This information is useful for data locality optimization and understanding cross-machine communication costs.

teleport

teleport : MachineId → MachineInstruction Safe Bool

Moves the execution context (process) to the specified physical machine. Returns true if teleportation succeeds, false if the target machine is unreachable. This changes where computation happens, but does not change the controller identity or object ownership.

Safety constraint: This instruction is invalid during active transactions. The interpreter must reject teleportation attempts within a transaction boundary to maintain transaction integrity. This is to preserve the transactional atomicity guarantees.

moveObject

moveObject : ObjectId → MachineId → MachineInstruction Safe Bool

Moves an object's data to a different physical machine. Returns true if the move succeeds, false if the target machine is unreachable. This changes the object's physical storage location but does not change its controller ownership. Machine migration enables room for data locality optimisation and load balancing.

fetch

fetch : ObjectId → MachineInstruction Safe Bool

Brings a replica of the specified object to the local machine for local access. The object retains its original identity (same ObjectId) and remains opaque—interaction still occurs through the call instruction. Returns true if the replica is successfully created or updated locally, false if the object does not exist.

Multiple AVM programs on different machines can fetch the same object, creating independent replicas. These replicas may diverge (eventual consistency) until reconciled via freeze. The fetch operation does not change the object's controller ownership or its authoritative location—it creates a local working copy for efficient access.

Controller Instructions

Controller instructions manage logical authority and ownership for distributed AVM deployments. Controllers order transactions and own objects. These operations deal with which controller has authority over objects and transaction ordering. These operations are independent of the physical machine executing the code.

getCurrentController

getCurrentController : ControllerInstruction Safe (Maybe ControllerId)

Returns the transaction controller identifier if executing within a transaction, or nothing if executing outside transaction scope.

getController

getController : ObjectId → ControllerInstruction Safe (Maybe ControllerId)

Returns the controller responsible for the specified object, or nothing if the object doesn't exist. This queries the object's logical ownership, not its physical location. The controller determines transaction ordering for the object.

transferObject

transferObject : ObjectId → ControllerId → ControllerInstruction Safe Bool

Transfers logical ownership of an object to another controller. This changes which controller orders transactions for the object but does not move the object's data between machines. Returns true if the transfer succeeds, false if the transfer is unauthorized or the target controller is unreachable.

Safety constraint: The current controller must have authority to transfer the object.

freeze

freeze : ObjectId → ControllerInstruction Safe (Maybe Bool)

Synchronizes all replicas of an object through the controller for strong consistency. When multiple machines have fetched the same object (creating local replicas), their states may diverge. The freeze operation reconciles these divergent replicas by pushing all pending changes to the controller and ensuring all replicas see a consistent view.

Returns: - nothing if the object has no controller assigned (cannot freeze) - just true if the freeze operation succeeds and replicas are synchronized - just false if the object does not exist or the controller is unreachable

After freeze completes, all replicas are synchronized. Subsequent fetch operations on other machines will naturally create new replicas that may again diverge, maintaining the eventually consistent model until the next freeze.

Finite Domain Constraint Programming Instructions

Finite domain (FD) instructions enable constraint-based programming where computation proceeds through constraint propagation and search over symbolic variables. These instructions support declarative problem-solving where solutions emerge from posting constraints and labeling variables.

newVar

newVar : Domain → FDInstruction Safe VarId

Creates a fresh constraint variable with the specified finite domain. The Domain is a list of possible values the variable can take. Returns a unique variable identifier for use in subsequent constraint operations. Variables created within a transaction are local to that transaction's constraint store.

narrow

narrow : VarId → Domain → FDInstruction Safe Bool

Narrows the domain of an existing constraint variable by intersecting it with the provided domain. Returns true if the narrowing succeeds (the intersection is non-empty), false if the intersection would empty the domain (constraint failure). Domain narrowing is a fundamental operation in constraint propagation.

post

post : Constraint → FDInstruction Safe Bool

Posts a relational constraint to the constraint store. Constraints relate variables through:

Returns true if the constraint is consistent with the current constraint store, false if posting the constraint would lead to immediate failure. Constraint posting triggers propagation to narrow the variable domains.

label

label : VarId → FDInstruction Safe Val

Selects a value from the variable's current domain using call-time choice—the value is chosen immediately when label executes. This is the search step in constraint solving. If subsequent constraint propagation fails, transaction rollback (abortTx) backtracks to explore alternative values. Returns the selected value, or fails immediately if the domain is empty.

References to other modules

This page references the following modules:

Symbol disambiguation log

The following references had multiple matches and were disambiguated:

  • String: chose examples.Common.Equality.eqString from ['examples.Common.Equality.eqString', 'examples.PingPong.Main.VString']

Module References

Referenced By

This module is referenced by:

References

This module references:

?>