---
title: Resource
tags:
  - anoma
  - resource
  - resource machine
---

Representation of Anoma Resource data.

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

module Goose.Anoma.Resource where

open import Foundation.BasicTypes
open import Goose.Anoma.ConsumedCreated
open import Goose.Anoma.Nullifier
open import Goose.Anoma.Nonce
open import Goose.Anoma.NullifierKey
open import Goose.Anoma.Crypto
open import Goose.Anoma.Identities
```

## Logic Reference

```agda
record LogicRef : Set where
  field
    ref : String
```

```agda
open LogicRef public
```

## Resource Structure

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

```agda
open Resource public
```

## Resource Predicates

```agda
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.

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

```agda
open CanNullifyResource public
```

## Nullifier from Proof

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

## Resource Commitment

Computes the commitment of a resource.

```agda
postulate
  resourceCommitment : Resource → Commitment
```

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

