Juvix imports

module arch.system.types.action;

import prelude open;
import arch.system.types.nullifier open;
import arch.system.types.commitment open;

Actions¶

An action is a term of type Action that represent atomic transactions or state changes.

Purpose¶

Actions are atomic units of state change within a transaction. They serve the following main purposes.

State Change Organization: Actions partition a transaction's overall state change into smaller, focused units. Each action clearly specifies which resources are being created and consumed by the associated transaction.
Proof Context Isolation: Actions provide an isolated context for resource logic proofs. When evaluating proofs for a resource, only the resources associated with that action are accessible. This isolation helps manage complexity and ensures proper resource handling.

We also need to discuss how resources are associated with actions.

A resource can be associated with an action in two ways:

Through its corresponding commitment in the action's created field, indicating it is being created

Through its corresponding nullifier in the action's consumed field, indicating it is being consumed

Important properties of this resource association:

Resources listed in consumed are considered "consumed in the action".
Resources listed in created are considered "created in the action".
Each resource is associated with exactly one action in case it is created or consumed in the action.

Now we can define the Action type.

A transaction action or simply action is a term of type Action.

type Action A :=
  mkAction@{
    created : Set (Commitment A);
    consumed : Set Nullifier;
  };

Arguments

created: contains commitments of resources created in this action
consumed: contains nullifiers of resources consumed in this action
resourceLogicProofs: contains a map of resource logic proofs associated with this action. The key is the self resource for which the proof is computed, the first parameter of the value opens to the required verifying key, the second one is the corresponding proof
complianceUnits: The set of transaction's compliance units
applicationData: maps tags to relevant application data needed to verify resource logic proofs. The deletion criterion field is described here. The openings are expected to be ordered.

Auxiliary Juvix code: Instances

deriving instance
eqAction {A} {{Eq A}} : Eq (Action A);

deriving instance
ordAction {A} {{Ord A}} : Ord (Action A);

created