Skip to content

Action

Action structures for the Anoma Resource Machine.

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

module Goose.Anoma.Action where

open import Foundation.BasicTypes 
open import Goose.Anoma.Compliance
open import Goose.Anoma.ConsumedCreated
open import Goose.Anoma.Identities

Tag

data Tag : Set where
  Created  : Commitment  Tag
  Consumed : String  Tag

Logic Verifier Key Outer Hash

LogicVKOuterHash : Set
LogicVKOuterHash = String

Deletion Criterion

data DeletionCriterion : Set where
  DeleteImmediately : DeletionCriterion
  StoreForever      : DeletionCriterion

Logic Verifier Input

record LogicVerifierInput : Set where
  field
    status : ConsumedCreated
    Data : Set
    appData : Data
    logicVKOuter : LogicVKOuterHash
    proof : String
open LogicVerifierInput public

Action Structure

record Action : Set where
  field
    complianceUnits : List ComplianceUnit
    logicVerifierInputs : List (Tag × LogicVerifierInput)
open Action public

Module References

Referenced By

This module is referenced by:

  • Goose.Anoma.Transaction

References

This module references: