Skip to content

title: AVM Controller Instructions tags: - AVM green paper - cross-chain integrity - instruction set

Controller Instruction Set

This module defines instructions for cross-controller operations based on the protocol in Sheff et al. (2024)1. These instructions operate on controller state and enable resource transfers, endorsement, and DAG reduction.

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

Module Parameters

module AVM.ControllerInstruction
    (Val : Set)
    (ObjectId : Set)
    (ControllerId : Set)
    (ControllerVersion : Set)
    (ResourceId : Set)
  where

open import Foundation.BasicTypes
open import AVM.Controller ControllerId ControllerVersion ObjectId ResourceId

Controller Query Instructions

Basic operations for querying controller state (maps to Paper Section 3.1).

data ControllerQuery : Set → Set where
  -- Get the current controller executing this transaction
  getCurrentController : ControllerQuery ControllerId

  -- Get the controller responsible for an object/resource
  getController : ObjectId → ControllerQuery (Maybe ControllerId)

  -- Get current controller version
  getCurrentVersion : ControllerQuery ControllerVersion

  -- Get current state root (for endorsement)
  getStateRoot : ControllerQuery StateRoot

  -- Check if a controller is halted (Section 3.4.4)
  isHalted : ControllerId → ControllerQuery Bool

Transfer Protocol Instructions

Instructions implementing the two-phase transfer protocol (Paper Section 3.3.1):

  1. Sender initiates transfer and creates send record
  2. Receiver endorses sender's state and creates receive record
data TransferInstruction : Set → Set where
  -- Sender side: initiate transfer
  -- Creates send record and marks resource as sent
  -- Returns send identifier for tracking
  initiateSend : ObjectId → ControllerId → TransferInstruction SendId

  -- Receiver side: complete transfer
  -- Creates receive record after endorsing sender's state
  -- Returns the received object ID if successful
  completeReceive : SendId → TransferInstruction (Maybe ObjectId)

  -- Query send record (for building reduce proofs)
  getSendRecord : SendId → TransferInstruction (Maybe SendRecord)

  -- Query receive record (for building reduce proofs)
  getReceiveRecord : ReceiveId → TransferInstruction (Maybe ReceiveRecord)

  -- Update send record (marks as non-updatable during reduction)
  updateSendRecord : SendRecord → TransferInstruction Bool

  -- Update receive record (modifies incoming during reduction)
  updateReceiveRecord : ReceiveRecord → TransferInstruction Bool

  -- Query transfer status
  getTransferStatus : SendId → TransferInstruction TransferStatus

Endorsement Instructions

Instructions for endorsement-based DAG reduction (Paper Section 3.4).

data EndorsementInstruction : Set → Set where
  -- Update endorsement map entry (Section 3.1)
  -- Controller endorses another controller's state root
  -- Requires proofs:
  --   1. New state provably after old state
  --   2. If endorsed controller endorses us, it's a consistent state
  endorseController : ControllerId → StateRoot → EndorsementInstruction Bool

  -- Query what state this controller has endorsed for another
  queryEndorsement : ControllerId → EndorsementInstruction (Maybe StateRoot)

  -- Query what state another controller has endorsed for us
  queryEndorsedBy : ControllerId → EndorsementInstruction (Maybe StateRoot)

  -- Create reduce proof for a set of sends (Section 3.4.2)
  -- Returns proof if all conditions satisfied:
  --   1. All sends have removable=true
  --   2. All parent and child controllers have appropriate endorsements
  --   3. Receive records updated to reference parents directly
  createReduceProof : List SendId → EndorsementInstruction (Maybe ReduceProof)

  -- Verify a reduce proof is valid
  verifyReduceProof : ReduceProof → EndorsementInstruction Bool

Resource History Instructions

Instructions for checking and manipulating resource history properties (Paper Section 2, 3.5).

data HistoryInstruction : Set → Set where
  -- Check if resource has Causal Resource History (Section 2.1)
  checkCRH : ObjectId → HistoryInstruction Bool

  -- Check if resources have Serializable Resource History (Section 2.2)
  -- Takes multiple resources to check they don't conflict
  checkSRH : List ObjectId → HistoryInstruction Bool

  -- Get the controller DAG for a resource
  getControllerDAG : ObjectId → HistoryInstruction ControllerDAG

  -- Get affecting controllers (all controllers in DAG)
  getAffectingControllers : ObjectId → HistoryInstruction (List ControllerId)

  -- Reduce controller DAG by removing a node (Section 3.4.3)
  -- Requires a valid reduce proof
  -- Removes node and connects parents to children
  reduceDAG : ObjectId → ReduceProof → HistoryInstruction Bool

  -- Remove specific node from controller DAG
  -- Requires reduce proof for that node's send
  removeNode : ObjectId → SendId → ReduceProof → HistoryInstruction Bool

Resource Label Instructions

Instructions for managing resource labels.

data LabelInstruction : Set → Set where
  -- Get complete label for a resource
  getResourceLabel : ObjectId → LabelInstruction (Maybe ResourceLabel)

  -- Update terminal controller (transfer control)
  updateTerminalController : ObjectId → ControllerId → LabelInstruction Bool

  -- Register backup controllers (Section 3.4.5)
  registerBackup : ObjectId → List ControllerId → LabelInstruction Bool

  -- Update receives field when resource is used as input
  updateReceives : ObjectId → List ReceiveId → LabelInstruction Bool

  -- Get resource lifecycle state
  getResourceState : ObjectId → LabelInstruction (Maybe ResourceState)

  -- Mark resource as consumed
  consumeResource : ObjectId → LabelInstruction Bool

Fault Tolerance Instructions

Instructions for handling controller failures (Paper Section 3.4.4, 3.4.5).

data FaultToleranceInstruction : Set → Set where
  -- Halt this controller (Section 3.4.4)
  -- Creates implicit send records for all unconsumed resources
  haltController : FaultToleranceInstruction Bool

  -- Activate backup controller for an orphaned resource (Section 3.4.5)
  -- Checks if terminal controller is halted, then transfers to next backup
  activateBackup : ObjectId → FaultToleranceInstruction (Maybe ControllerId)

  -- Remove halted controller subgraph from DAG
  -- Requires all parents and children endorse the halted nodes
  removeHaltedSubgraph : ObjectId → List ControllerId → FaultToleranceInstruction Bool

  -- Register emergency override condition (Section 3.4.6)
  -- Modifies controller's halt conditions
  registerEmergencyOverride : EmergencyOverride → FaultToleranceInstruction Bool

State Proof Instructions

Instructions for proving causal ordering of controller states.

data StateProofInstruction : Set → Set where
  -- Prove one state root is provably after another
  -- Used in endorsement validation and transfer protocol
  proveAfter : (c : ControllerId) → (s₁ s₂ : StateRoot) → StateProofInstruction (Maybe (c ⊢ s₁ ≼ s₂))

  -- Get list of state transitions between two roots
  getStateTransitions : ControllerId → StateRoot → StateRoot → StateProofInstruction (List StateRoot)

Garbage Collection Instructions

Instructions for cleaning up obsolete send/receive records (Paper Section 3.4.2, end).

data GarbageCollectionInstruction : Set → Set where
  -- Remove controller from send record's outgoing field
  -- When all receives from that controller have empty live sets
  -- and reduce proofs exist for all their outgoing sends
  gcSendOutgoing : SendId → ControllerId → GarbageCollectionInstruction Bool

  -- Garbage collect receive record
  -- When all incoming sends have removed this controller from outgoing
  gcReceiveRecord : ReceiveId → GarbageCollectionInstruction Bool

  -- Garbage collect send record
  -- When removable=true and all incoming receives are garbage collected
  gcSendRecord : SendId → GarbageCollectionInstruction Bool

Combined Controller Instruction Set

All controller instructions unified under a single type.

data ControllerInstruction : Set → Set where
  query : ∀ {A} → ControllerQuery A → ControllerInstruction A
  transfer : ∀ {A} → TransferInstruction A → ControllerInstruction A
  endorse : ∀ {A} → EndorsementInstruction A → ControllerInstruction A
  history : ∀ {A} → HistoryInstruction A → ControllerInstruction A
  label : ∀ {A} → LabelInstruction A → ControllerInstruction A
  fault : ∀ {A} → FaultToleranceInstruction A → ControllerInstruction A
  stateProof : ∀ {A} → StateProofInstruction A → ControllerInstruction A
  gc : ∀ {A} → GarbageCollectionInstruction A → ControllerInstruction A

Mapping from DistribInstruction

The interpreter can map the simple DistribInstruction operations to these richer controller operations:

  • getCurrentController → query getCurrentController
  • getController obj → query (getController obj)
  • teleport ctrl → Execute transfer sequence and reduce DAG
  • transferObject obj ctrl → transfer (initiateSend obj ctrl) then transfer (completeReceive ...)
  • getCurrentVersion → query getCurrentVersion
  • switchVersion v → Update controller version in state

The teleport operation is particularly interesting: it represents a high-level operation that internally:

  1. Transfers all resources to target controller
  2. Creates reduce proofs for the transferring controller
  3. Allows target controller to remove the intermediate node from DAGs

Instruction Semantics

The semantics of these instructions are defined by state transformers in the interpreter module. Key invariants maintained:

  1. Transfer Safety: Send/receive records always paired correctly
  2. Endorsement Monotonicity: Once endorsed, can't endorse contradictory state
  3. CCL Preservation: DAG reduction preserves Consistent Controller Labels (Theorem 3)
  4. CRH Propagation: Resource creation propagates Causal Resource History
  5. Halting Finality: Halted controllers accept no new transitions

Usage Examples

Basic Transfer

-- On sender (controller A):
sendId ← initiateSend objectId controllerB

-- On receiver (controller B):
-- First endorse sender's current state
endorseController controllerA stateRoot
-- Then complete transfer
objId ← completeReceive sendId

Endorsement and Reduction

-- Controller A sends resource to B, B sends to C, C sends back to A
-- A can now reduce B's node from the DAG:

-- 1. A endorses B's state (containing the send to C)
endorseController B stateRootB

-- 2. A endorses C's state (containing the receive from B)
endorseController C stateRootC

-- 3. C updates receive to point to A's original send
proof ← createReduceProof [sendB]

-- 4. A can now remove B from the resource's DAG
reduceDAG resourceId proof

Checking Resource Consistency

-- Before combining resources from different controllers:
consistent ← checkSRH [resource1, resource2, resource3]

if consistent then
  -- Safe to use all resources in same transaction
  proceed
else
  -- Resources may reflect double-spend, check affecting controllers
  controllers1 ← getAffectingControllers resource1
  controllers2 ← getAffectingControllers resource2
  -- Identify which controller forked

Next Steps

The interpreter will implement the operational semantics for these instructions, maintaining the invariants described in the paper. Key implementation challenges:

  1. Efficient DAG representation and manipulation
  2. Proof generation and verification for endorsements
  3. Garbage collection of obsolete records
  4. Detecting and handling controller forks
  5. Backup controller activation logic

See AVM Interpreter for the operational semantics.

  1. Sheff Isaac. Cross-Chain Integrity with Controller Labels and Endorsement. Anoma Research Topics, Jun 2024. URL: https://doi.org/10.5281/zenodo.10498996, doi:10.5281/zenodo.10498997. ↩