title: AVM Controller Model tags: - cross-chain integrity - distributed systems
Controller Model for Cross-Chain Integrity
This module defines the controller abstraction for the AVM, based on the cross-chain integrity protocol described in Sheff et al. (2024). Controllers are state machines that order transactions and maintain authoritative state for resources.
References
- Cross-Chain Integrity with Controller Labels and Endorsement
- Sections referenced throughout this module refer to that paper
{-# OPTIONS --without-K --type-in-type --exact-split #-}
Module Parameters
module AVM.Controller (ControllerId : Set) (ControllerVersion : Set) (ObjectId : Set) (ResourceId : Set) where open import Foundation.BasicTypes
State Roots and Causal Ordering
Controllers maintain state that can be uniquely identified by a state root (typically a cryptographic hash or Merkle root). The paper (Section 3.1) requires proving causal ordering between states.
StateRoot : Set StateRoot = ℕ -- Placeholder: in practice this would be a cryptographic hash
The provably-after relation captures when one state is the result of valid state transitions from another state.
-- Placeholder for proof that one state follows another -- In practice: proof that stateAfter results from applying transactions to stateBefore data _⊢_≼_ : ControllerId → StateRoot → StateRoot → Set where -- Would be defined by the specific controller implementation -- Could be a chain of block headers, consensus proofs, etc.
Resource Lifecycle
Resources have three lifecycle states (Paper Section 1.2):
data ResourceState : Set where NotCreated : ResourceState Created : ResourceState Consumed : ResourceState
Send Records
Send records track outgoing resource transfers from one controller to another (Paper Section 3.1.1, Table 2). When a resource is transferred, the sending controller creates a send record representing a promise to accept the resource back (or its descendants) in future transfers.
SendId : Set SendId = ℕ × ControllerId -- Unique identifier: (counter, sender) ReceiveId : Set ReceiveId = ℕ × ControllerId -- Forward declaration for mutual reference
Send Record Structure
record SendRecord : Set where constructor mkSend field id : SendId resource : ResourceId -- Can this send be removed via reduction? -- False for sends with no incoming (root sends) removable : Bool -- Can this send's fields be updated? -- Set to false during reduce proof generation updatable : Bool -- Receive records on which this send depends -- Empty for resources created on this controller incoming : List ReceiveId -- Controllers to which the resource was sent -- Updated during DAG reduction outgoing : List ControllerId
Receive Records
Receive records track incoming resource transfers (Paper Section 3.1.2, Table 3). A receive record is created when a controller accepts a resource sent from another controller.
record ReceiveRecord : Set where constructor mkReceive field id : ReceiveId resource : ResourceId -- Send records on other controllers that this receive accepts -- Must be non-empty incoming : List SendId -- Resources currently alive on this controller that depend on this receive live : List ResourceId -- Sends created when resources dependent on this receive were sent elsewhere outgoing : List SendId
Endorsement
Endorsement maps track which other controllers' states this controller has reviewed and accepted (Paper Section 3.1). Endorsement enables DAG reduction by allowing controllers to vouch for history that occurred elsewhere.
Endorsement Map
EndorsementMap : Set EndorsementMap = ControllerId → Maybe StateRoot
Each controller maintains an endorsement map where:
- The entry for itself points to its current state
- Entries for other controllers indicate endorsed state roots
- An endorsed state means this controller has verified the history up to that state
Controller State
The complete state of a controller (Paper Section 3.1, Table 1).
record ControllerState : Set where constructor mkControllerState field controllerId : ControllerId currentVersion : ControllerVersion -- Is this controller halted? (Section 3.4.4) -- Once true, no further state transitions are valid halted : Bool -- Endorsement tracking (Section 3.1) -- Maps controller IDs to the state roots this controller has endorsed endorsements : EndorsementMap -- Transfer tracking sends : List SendRecord -- Outgoing transfers receives : List ReceiveRecord -- Incoming transfers -- Resource tracking (Section 1.2) -- In practice: Merkle accumulators (line 94) created : List ResourceId -- Resources created by this controller consumed : List ResourceId -- Resources consumed by this controller
Resource Labels
Each resource carries a label tracking which controllers have affected its history (Paper Section 3.2, Table 4). The label includes a DAG of controller nodes representing the resource's provenance.
Controller DAG Node
record NodeLabel : Set where constructor mkNode field controller : ControllerId send : SendId state : StateRoot -- State of this controller after the send
Controller DAG
The controller DAG is represented as a list of nodes with implicit edges. An edge exists from node A to node B when there is a receive record in B's controller that has A's send in its incoming set (Paper Section 3.2).
ControllerDAG : Set ControllerDAG = List NodeLabel
Resource Label Structure
record ResourceLabel : Set where constructor mkLabel field -- Which controller created this resource? creating : ControllerId -- Which controller can consume this resource? -- This controller orders transactions that use this resource as input terminal : ControllerId -- Backup controllers for fault tolerance (Section 3.4.5) -- If terminal controller halts, control transfers to first available backup backup : List ControllerId -- Receive records on the terminal controller that this resource depends on receives : List ReceiveId -- Controller DAG tracking affecting controllers dag : ControllerDAG
The affecting controllers of a resource are all the controllers appearing in its DAG nodes. By property CCL (Consistent Controller Labels), if a resource lacks SRH (Serializable Resource History), it must have an unsafe controller in this set.
Transfer Protocol Types
Transfer status tracking for cross-controller operations.
data TransferStatus : Set where Initiated : TransferStatus Received : TransferStatus Failed : String → TransferStatus
Endorsement and DAG Reduction
Reduce proofs enable removing intermediate controllers from a resource's DAG by proving that neighboring controllers have endorsed the intermediate history (Paper Section 3.4.2).
record ReduceProof : Set where constructor mkReduceProof field -- Set of sends being reduced (all must have removable=true) sendSet : List SendId -- State roots of parent controllers (X in paper) parentStates : List (ControllerId × StateRoot) -- State roots of child controllers (Z in paper) childStates : List (ControllerId × StateRoot) -- Proofs that required endorsements occurred -- Shows all controllers in X, Y, Z endorsed appropriate states endorsementProofs : List (ControllerId × StateRoot)
Reduce Proof Validity
A reduce proof is valid when (Paper Section 3.4.2):
- All sends in sendSet have updatable=false
- All parent controllers have endorsed child and intermediate states
- All child controllers have endorsed parent and intermediate states
- Receive records have been updated to reference parent sends directly
Resource History Properties
The paper defines three key properties for resource history (Section 2).
Causal Resource History (CRH)
A resource has CRH if it was created in a valid transaction whose inputs also have CRH (Paper Section 2.1). This is a recursive property maintained through resource creation.
-- Placeholder: proof that a resource has causal resource history data HasCRH : ResourceId → Set where -- Would prove: resource created in valid transaction with CRH inputs
Serializable Resource History (SRH)
A resource has SRH if its complete history reflects a fully serializable execution with no double-consumes (Paper Section 2.2). This is the stronger consistency property users typically want.
-- Placeholder: proof that resources have serializable history data HasSRH : List ResourceId → Set where -- Would prove: no resource in history consumed more than once
Consistent Controller Labels (CCL)
A resource has CCL if whenever it lacks SRH, it has an unsafe controller in its affecting controllers set (Paper Section 2.3). The protocol maintains CCL through careful management of controller DAG reduction.
-- Placeholder: proof that label correctly tracks unsafe controllers data HasCCL : ResourceLabel → Set where -- Would prove: ¬(HasSRH r) → unsafe-controller ∈ affecting-controllers
Emergency Override Condition
Controllers can specify an Emergency Override Condition (EOC) - a special procedure that can only halt the controller (Paper Section 3.4.6). This enables high-integrity oversight without normal operational control.
record EmergencyOverride : Set where field -- Condition under which emergency halt is triggered -- E.g., signature from supervisor, consensus failure detection condition : ControllerState → Bool -- Identity of the override authority authority : String -- Could be a public key, committee ID, etc.
Utilities
Helper functions for working with controller structures.
Affecting Controllers
Extract the set of affecting controllers from a resource label.
affectingControllers : ResourceLabel → List ControllerId affectingControllers label = let open ResourceLabel label in creating ∷ terminal ∷ map NodeLabel.controller dag
DAG Parents
Find parent nodes of a given node in a controller DAG. This operation is used during DAG reduction to identify which controllers must participate in endorsement (Paper Section 3.4.2).
-- Note: Implementation left as postulate for now -- In practice: returns send IDs that are incoming to receives referencing this send postulate dagParents : SendRecord → List ReceiveRecord → List SendId
Next Steps
This module provides the foundational types for controller operations. The instruction set for manipulating these structures is defined in ControllerInstruction.
Key properties to prove:
- Endorsement-based reduction preserves CCL (Theorem 3 in paper)
- Transfer protocol maintains CRH
- Valid reduce proofs enable safe node removal from DAG