module arch.system.types.resource_machine; import prelude open; import arch.system.types.transaction open; trait type ResourceMachine A := mkResourceMachine@{ createTransaction : -- CMTreeRoots : Set CMtree.Value; -- actions : Set Action; -- deltaProof : DeltaProvingSystem.Proof; Unit -> Transaction A; -- which is the mkTransaction function composeTransactions : Transaction A -> Transaction A -> Transaction A; verifyTransaction : Transaction A -> Bool; -- read nullifier set? -- append to nullifier set? -- read commitment tree? -- add data to commitment tree? };