module arch.system.types.action; import prelude open; import arch.system.types.nullifier open; import arch.system.types.commitment open; type Action A := mkAction@{ created : Set (Commitment A); consumed : Set Nullifier; -- resourceLogicProofs : Map Tag (LogicRefHash, PS.Proof); -- complianceUnits : Set ComplianceUnit; -- applicationData : Map Tag (BitString, DeletionCriterion); }; deriving instance eqAction {A} {{Eq A}} : Eq (Action A); deriving instance ordAction {A} {{Ord A}} : Ord (Action A); -- axiom -- create -- (nfs : Set (NullifierKey, Resource)) -- (created : Set Resource) -- (applicationData : ApplicationData) -> Action; -- axiom -- delta (action : Action) -> DeltaHash; -- axiom -- verify (action : Action) -> Bool;