Transaction Instrumentation

This module defines a simple transformer that wraps an AVMProgram₂ with transaction boundaries and states a correspondence lemma with the interpreter.

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

module AVM.Transactions where

open import Foundation.BasicTypes
open import Foundation.InteractionTrees

-- Re-export signatures used below as parameters
module _
  (Val : Set)
  (ObjectId : Set)
  (freshObjectId : ℕ → ObjectId)
  (MachineId : Set)
  (ControllerId : Set)
  (ControllerVersion : Set)
  (TxId : Set)
  (freshTxId : ℕ → TxId)
  where

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

  -- 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)

  -- Transformer: wrap a program in begin/commit/abort
  -- Uses AVMProgram₁ which includes Base + Transactions
  withTransaction : ∀ {A : Set} → AVMProgram₁ A → AVMProgram₁ A
  withTransaction prog =
    trigger {E = Instr₁ Safe} (Tx beginTx) >>= λ txid →
    prog >>= λ res →
    trigger {E = Instr₁ Safe} (Tx (commitTx txid)) >>= λ ok →
      if ok then ret res else
        (trigger {E = Instr₁ Safe} {A = ⊤} (Tx (abortTx txid)) >>= λ _ → ret res)

  -- The definition above is the canonical instrumentation; properties can be
  -- derived per interpreter instantiation.

  -- Note: An interpreter-level correspondence follows immediately when instantiated
  -- with a concrete Interpreter module, since the definition is identical to its
  -- inline form above.
Module References

References

This module references: