Skip to content

Object Composition

This module formalises object composition mechanisms from the AVM green paper (§4.2-4.4), including coproducts of object types (horizontal composition), objects with interfaces (vertical composition), and nested method invocations.

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

module AVM.Composition where

open import Foundation.BasicTypes
open import Foundation.InteractionTrees
open import AVM.Instruction
open import AVM.Objects

Motivation

Sequential objects (see SequentialObject) are composed horizontally via coproducts and vertically via nesting.

  1. Horizontal composition allows independent objects to coexist, while

  2. vertical composition enables objects to invoke methods on nested sub-objects, creating hierarchical structures.

Horizontal Composition

Coproducts model horizontal composition, where multiple object types can be used interchangeably through a common interface.

Tagged Object Types

A coproduct of two object types accepts inputs tagged with a choice indicator.

data Tag : Set where
  left  : Tag
  right : Tag

TaggedInput : Set
TaggedInput = Tag × Input

postulate string-to-tag : String → Maybe Tag

Coproduct Object Type

The coproduct combines two object types (see ObjectType), partial functions that route inputs based on tags.

_⊕_ : ObjectType → ObjectType → ObjectType
(φ₁ ⊕ φ₂) [] = φ₁ []  -- Initial output from left component
(φ₁ ⊕ φ₂) inputs@(_ ∷ _) = helper inputs []
  where
    helper : InputSequence → InputSequence → Maybe Output
    helper [] acc = nothing  -- Should not happen
    helper (input ∷ rest) acc 
      with string-to-tag input
    ...  | nothing = nothing  -- Invalid tag
    ...  | just left  = φ₁ (acc ++ rest)
    ...  | just right = φ₂ (acc ++ rest)

infixr 6 _⊕_

Lemma. Horizontal composition preserves well-formedness

Horizontal composition preserves well-formedness (see WellFormedObjectType) when components are well-formed.

⊕-preserves-wf : (φ₁ φ₂ : ObjectType) →
  WellFormedObjectType φ₁ →
  WellFormedObjectType φ₂ →
  ---------------------------------------
  WellFormedObjectType (φ₁ ⊕ φ₂)
⊕-preserves-wf φ₁ φ₂ wf₁ wf₂ = record
  { empty-defined = postulate-empty
  ; prefix-closed = postulate-prefix
  ; deterministic = postulate-det
  }
  where
    postulate
      postulate-empty : is-defined (φ₁ ⊕ φ₂) ε
      postulate-prefix : ∀ xs x →
        is-defined (φ₁ ⊕ φ₂) (xs · x) →
        is-defined (φ₁ ⊕ φ₂) xs
      postulate-det : ∀ xs o₁ o₂ →
        (φ₁ ⊕ φ₂) xs ≡ just o₁ →
        (φ₁ ⊕ φ₂) xs ≡ just o₂ →
        o₁ ≡ o₂

Objects with Interfaces

Following §4.4 of the green paper, objects can expose interfaces that abstract their internal implementation, supporting vertical composition through nesting.

Interface Specification

An interface declares the methods an object must implement.

record AVMInterface : Set where
  field
    methods : List MethodId
    method-signature : MethodId → (Args → Set) × (Result → Set)

open AVMInterface public

Implementation Map

An implementation map defines how an object type realizes an interface.

record ImplementationMap (I : AVMInterface) : Set where
  field
    impl-type : ObjectType
    well-formed : WellFormedObjectType impl-type

    -- Each interface method maps to a sequence of object inputs
    method-impl : (m : MethodId) →
      m ∈ methods I →
      Args → InputSequence

open ImplementationMap public

Object with Interface

An object equipped with an interface and implementation map.

record ObjectWithInterface : Set where
  field
    interface : AVMInterface
    impl-map : ImplementationMap interface
    state : SequentialObject

    -- State type matches implementation
    state-compatible :
      object-type state ≡ impl-type impl-map

open ObjectWithInterface public

Nested Objects and Object Identifiers

Objects can contain other objects as components, creating hierarchical structures. This requires a systematic approach to object identification.

Object Identifier System

We define a hierarchical identifier system following §4.4 of the green paper.

data ObjId : Set where
  root : ObjId
  child : ObjId → ℕ → ObjId

-- Path from root to object
id-path : ObjId → List ℕ
id-path root = []
id-path (child parent n) = id-path parent ++ (n ∷ [])

-- Parent of an identifier
parent-id : ObjId → Maybe ObjId
parent-id root = nothing
parent-id (child p _) = just p

Nested Object Structure

A nested object contains a map from identifiers to sub-objects.

record NestedObject : Set where
  coinductive
  field
    obj-id : ObjId
    local-state : SequentialObject
    children : List (ℕ × NestedObject)

  -- Lookup child by index
  get-child : ℕ → Maybe NestedObject
  get-child n with lookup-child n children
    where
      lookup-child : {A : Set} → ℕ → List (ℕ × A) → Maybe A
      lookup-child n [] = nothing
      lookup-child n ((m , obj) ∷ rest) with nat-eq n m
        where postulate nat-eq : ℕ → ℕ → Bool
      ... | true = just obj
      ... | false = lookup-child n rest
  ... | result = result

open NestedObject public

Nested Method Invocation

Method calls can target nested sub-objects via their identifiers.

data NestedMethodCall : Set where
  local-call : MethodId → Args → NestedMethodCall
  nested-call : ObjId → MethodId → Args → NestedMethodCall

postulate
  get-local-id : NestedObject → ObjectId
  _≟-id_ : ObjId → ObjId → Bool
  error-result : String → Result

-- Find nested object by identifier
{-# TERMINATING #-}
find-object : NestedObject → ObjId → Maybe NestedObject
find-object obj target with obj-id obj ≟-id target
... | true = just obj
... | false = search-children (children obj)
  where
    search-children : List (ℕ × NestedObject) → Maybe NestedObject
    search-children [] = nothing
    search-children ((n , c) ∷ rest)
      with find-object c target
    ... | just found = just found
    ... | nothing = search-children rest

-- Execute a nested method call
execute-nested-call :
  NestedObject →
  NestedMethodCall →
  AVMProgram Result
execute-nested-call obj (local-call method args) =
  -- Invoke method on local state
  trigger (callMethod (get-local-id obj) method args)

execute-nested-call obj (nested-call target-id method args)
  with find-object obj target-id
... | nothing = ret (error-result "Object not found")
... | just target = trigger (callMethod (get-local-id target) method args)

Canonical Decomposition

Every nested object structure admits a canonical decomposition into a flat collection with unique identifiers (§4.4).

Flattened Object Collection

Decompose nested structure into flat map.

record FlatObjectCollection : Set where
  field
    objects : List (ObjId × SequentialObject)

  -- Lookup by identifier
  lookup : ObjId → Maybe SequentialObject
  lookup id = helper objects
    where
      helper : List (ObjId × SequentialObject) → Maybe SequentialObject
      helper [] = nothing
      helper ((oid , obj) ∷ rest) with oid ≟-id id
      ... | true = just obj
      ... | false = helper rest

open FlatObjectCollection public

Flattening Transformation

Flatten nested objects into collection.

{-# TERMINATING #-}
flatten : NestedObject → FlatObjectCollection
flatten obj = record
  { objects = collect obj
  }
  where
    collect : NestedObject → List (ObjId × SequentialObject)
    collect obj =
      (obj-id obj , local-state obj) ∷
      concat-map (λ { (n , c) → collect c }) (children obj)
      where
        concat-map : {A B : Set} → (A → List B) → List A → List B
        concat-map f [] = []
        concat-map f (x ∷ xs) = f x ++ concat-map f xs

Decomposition Properties

Lemma. Flattening Preserves State

The flattening transformation preserves child object states.

postulate
  flatten-preserves-state :
    (obj : NestedObject) →
    (n : ℕ) →
    (child-obj : NestedObject) →
    get-child obj n ≡ just child-obj →
    lookup (flatten obj) (child (obj-id obj) n) ≡ just (local-state child-obj)

Lemma. Flattening Creates Unique Identifiers

The flattening transformation ensures distinct identifiers map to distinct states.

postulate
  flatten-unique-ids :
    (obj : NestedObject) →
    ∀ id₁ id₂ →
    id₁ ≢ id₂ →
    lookup (flatten obj) id₁ ≢ lookup (flatten obj) id₂

Vertical Composition

Objects compose vertically by delegation: outer objects invoke methods on nested objects to implement their own behavior.

Delegating Object

An object that implements methods by delegating to sub-objects.

record DelegatingObject : Set where
  field
    interface : AVMInterface
    nested : NestedObject

    -- Map interface methods to nested calls
    delegation-map :
      (m : MethodId) →
      m ∈ methods interface →
      Args → NestedMethodCall

open DelegatingObject public

Delegation Semantics

Execute delegating object method.

execute-delegating-method :
  DelegatingObject →
  MethodId →
  Args →
  AVMProgram Result
execute-delegating-method obj method args with method-in-interface method
  where
    postulate method-in-interface : MethodId → Maybe (method ∈ methods (interface obj))
... | nothing = ret (error-result "Method not in interface")
... | just proof =
    let call = delegation-map obj method proof args
    in execute-nested-call (nested obj) call

Example: Composite Counter

A composite counter built from two nested counters using vertical composition.

module CompositeCounterExample where
  postulate
    counter-interface : AVMInterface
    make-counter : ℕ → SequentialObject
    increment-method : MethodId
    get-value-method : MethodId

  -- Two counters nested in composite
  composite-counter : NestedObject
  composite-counter = record
    { obj-id = root
    ; local-state = make-counter 0
    ; children =
        (0 , record { obj-id = child root 0
                    ; local-state = make-counter 0
                    ; children = [] }) ∷
        (1 , record { obj-id = child root 1
                    ; local-state = make-counter 0
                    ; children = [] }) ∷
        []
    }

  -- Increment both sub-counters
  increment-both : AVMProgram Result
  increment-both =
    execute-nested-call composite-counter
      (nested-call (child root 0) increment-method unit-args) >>= λ _ →
    execute-nested-call composite-counter
      (nested-call (child root 1) increment-method unit-args)
    where
      postulate unit-args : Args

Conclusion

This formalization establishes the compositional mechanisms for AVM objects, enabling construction of complex systems from simple sequential components. The development comprises three main composition strategies:

  • Horizontal Composition. Coproducts enable independent object types to coexist through tagged routing, preserving well-formedness properties while allowing flexible component selection.
  • Vertical Composition. Nested objects with interfaces support hierarchical structures through delegation, where outer objects implement behavior by invoking methods on sub-objects.
  • Canonical Decomposition. The flattening transformation systematically converts hierarchical nested structures into flat collections with unique identifiers, essential for transaction processing and state management.

These mechanisms directly realize the compositional vision of the AVM green paper (§4.2-4.4), providing the basis for the AVM message-passing object system.

References to other modules

This page references the following modules: