Skip to content

Program

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

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

module Goose.Anoma.Program where

open import Foundation.BasicTypes hiding (ObjectId)
open import Goose.Anoma.Resource
open import Goose.Anoma.Transaction
open import Goose.Anoma.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: