Skip to content

Program

Anoma program representation reifying the local domain, solver and controller.

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

module RM.Types.Program where

open import Foundation.BasicTypes
open import RM.Types.Resource
open import RM.Types.Transaction
open import RM.Types.Identities

Storage Types

StorageKey : Set
StorageKey = String

data StorageValue : Set where
  str   : String → StorageValue
  int   : ℕ → StorageValue
  bool  : Bool → StorageValue
  bytes : String → StorageValue

Resource Query

data ResourceQuery : Set where
  queryByObjectId : ObjectId → ResourceQuery

Program Error

data ProgramError : Set where
  networkError     : String → ProgramError
  engineError      : String → ProgramError
  decryptionError  : String → ProgramError
  commitmentError  : String → ProgramError
  identityError    : String → ProgramError
  storageError     : String → ProgramError
  typeError        : String → ProgramError
  userError        : ProgramError

Anoma Program

data Program : Set where
  skip : Program
  raise : ProgramError → Program
  tryCatch : Program → (ProgramError → Program) → Program → Program
  withRandomGen : (ℕ → Program × ℕ) → Program
  queryResource : ResourceQuery → (Resource → Program) → Program
  submitTransaction : Transaction → Program → Program
  decrypt : EngineId → Ciphertext → (Plaintext → Program) → Program
  requestCommitment : EngineId → Signable → (Commitment → Program) → Program
  generateIdentity : Backend → IDParams → Capabilities
    → (Maybe EngineId → Maybe EngineId → EngineId → Program) → Program
  connectIdentity : EngineId → Backend → Capabilities
    → (Maybe EngineId → Maybe EngineId → Program) → Program
  deleteIdentity : EngineId → Backend → Program → Program
  getValue : StorageKey → (Maybe StorageValue → Program) → Program
  setValue : StorageKey → StorageValue → Program → Program
  deleteValue : StorageKey → Program → Program

Generate Object ID

genObjectId : (ObjectId → Program) → Program
genObjectId next = withRandomGen (λ g → next g , g)
Module References

References

This module references: