Skip to content

Resource

Representation of Anoma Resource data.

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

module RM.Types.Resource where

open import Foundation.BasicTypes
open import RM.Types.ConsumedCreated
open import RM.Types.Nullifier
open import RM.Types.Nonce
open import RM.Types.NullifierKey
open import RM.Types.Crypto
open import RM.Types.Identities

Logic Reference

record LogicRef : Set where
  field
    ref : String

open LogicRef public

Resource Structure

record Resource : Set where
  field
    Val   : Set
    Label : Set
    label : Label
    logicRef : LogicRef
    quantity : ℕ
    value : Val
    ephemeral : Bool
    nonce : Nonce
    nullifierKeyCommitment : NullifierKeyCommitment

open Resource public

Resource Predicates

isEphemeral : Resource → Bool
isEphemeral r = r .ephemeral

isPersistent : Resource → Bool
isPersistent r = not (isEphemeral r)

Can Nullify Resource

Proof that a key can nullify a resource.

record CanNullifyResource (key : NullifierKey) (res : Resource) : Set where
  field
    proof : NullifierKeyMatchesCommitment key (res .nullifierKeyCommitment)

open CanNullifyResource public

Nullifier from Proof

nullifier : {key : NullifierKey} {res : Resource} → CanNullifyResource key res → Nullifier
nullifier _ = privateMk

Resource Commitment

Computes the commitment of a resource.

postulate
  resourceCommitment : Resource → Commitment

Note: Placeholder implementation. Should use proper serialization and hashing.

Module References

Referenced By

This module is referenced by:

References

This module references: