feat: implement initial version

.gitignore

@@ -0,0 +1,4 @@
+.juvix-build
+.history
+*.nockma
+.DS_Store

AnomaHelpers.juvix

@@ -0,0 +1,63 @@
+module AnomaHelpers;
+
+import Stdlib.Prelude open;
+import Data.Map open;
+import Data.Set open;
+import Anoma open;
+
+
+-- TODO all these helpers should be in `juvix-anoma-stdlib`
+
+syntax alias Bytes32 := Nat;
+syntax alias Bytes := Nat;
+
+isCreated (r : Resource) (tx : Transaction) : Bool :=
+  elem (==) r (ResourcePartition.created (partitionResources tx));
+
+isConsumed (r : Resource) (tx : Transaction) : Bool :=
+  elem (==) r (ResourcePartition.consumed (partitionResources tx));
+
+
+isPresent (cms : List Helper.Commitment) (cm : Helper.Commitment) : Bool :=
+  elem (==) cm cms;
+
+isSublist (sub sup : List Helper.Commitment) : Bool :=
+  all (isPresent sup) sub;
+
+isSubset {A} {{Ord A}} (sub sup : Set A) : Bool :=
+  all (x in Data.Set.toList sub)
+    member? x sup;
+
+
+isSubsetOfCreatedResources (sub : Set Helper.Commitment) (tx : Transaction) : Bool :=
+  let
+    sup : Set Helper.Commitment := Data.Set.fromList (map commitment (ResourcePartition.created (partitionResources tx)));
+  in
+    isSubset sub sup;
+
+lookupExtraData {Value : Type} (key : Bytes32) (tx : Transaction) : Maybe Value :=
+  let
+    keyValueMap : Map Bytes32 Value := anomaDecode (Transaction.extra tx);
+  in
+    lookup key keyValueMap;
+
+
+-- This helper replicates the private key to compute the nullifiers. TODO
+mkTransaction
+  (self : PrivateKey)
+  (consumed : List Resource)
+  (created : List Resource)
+  (extraData : Map Bytes32 Bytes)
+  : Transaction :=
+    let
+      replicatedPrivKey : List PrivateKey := replicate (length consumed) self;
+    in
+      Transaction.mk@{
+        roots := [];
+        commitments := map commitment created;
+        nullifiers := zipWith nullifier consumed replicatedPrivKey;
+        proofs := consumed ++ created;
+        delta := [];
+        extra := anomaEncode (extraData);
+        preference := 0
+      };

Authorization/Owner.juvix

@@ -0,0 +1,58 @@
+module Authorization.Owner;
+
+import Stdlib.Prelude open;
+import Data.Map open;
+import Data.Set open;
+import Anoma open;
+
+import AnomaHelpers open;
+
+type Owner :=
+  mkOwner {
+    owner : PublicKey;
+  };
+
+instance
+Owner-Eq : Eq Owner :=
+  mkEq@{
+    eq (d1 d2 : Owner) : Bool :=
+      Owner.owner d1 == Owner.owner d2
+  };
+
+getOwner (r : Resource) : PublicKey :=
+  Owner.owner (anomaDecode (Resource.data r));
+
+type AuthMessage :=
+  mkAuthMessage {
+    consumed : Helper.Nullifier;
+    mustBeCreated : Set Helper.Commitment;
+  };
+
+ mkAuthExtraDataMapEntry (self : PrivateKey) (created : List Resource) (consumed : Resource) : Pair Bytes32 Bytes :=
+  let
+    consumedNk : Helper.Nullifier := nullifier consumed self;
+    createdCms : Set Helper.Commitment := Data.Set.fromList (map commitment created);
+    msg : AuthMessage := mkAuthMessage@{consumed := consumedNk; mustBeCreated := createdCms;};
+
+    k := consumedNk;
+    v := anomaEncode(msg, anomaSignDetached msg self);
+  in
+    (k, v);
+
+ mkAuthExtraData (self : PrivateKey) (consumed : List Resource) (created : List Resource) : Map Bytes32 Bytes :=
+   Data.Map.fromList (map (mkAuthExtraDataMapEntry self created) consumed);
+
+
+isAuthorizedByOwner (self : Resource)  (tx : Transaction) : Bool :=
+  let
+    owner : PublicKey := getOwner self;
+    selfNk : Helper.Commitment := commitment self;
+    lookupResult : Maybe (Pair AuthMessage Signature) := lookupExtraData selfNk tx ;
+  in
+    case lookupResult of
+      | nothing := false
+      | just (msg, sig) :=
+        AuthMessage.consumed msg == selfNk
+        && anomaVerifyDetached sig msg owner
+        && isSubsetOfCreatedResources (AuthMessage.mustBeCreated msg) tx
+  ;

Intent/DSL.juvix

@@ -0,0 +1,76 @@
+--- A DSL for constructing intents
+module Intent.DSL;
+
+import Stdlib.Prelude open hiding {for; any; all};
+import Anoma open public;
+
+type Asset :=
+  mkAsset {
+    quantity : Nat;
+    kind : Kind
+  };
+
+type Quantifier :=
+  | Any
+  | All;
+
+type QuantifiedAssets :=
+  mkAssets {
+    quantifier : Quantifier;
+    assets : List Asset
+  };
+
+syntax operator of_ additive;
+syntax alias of_ := mkAsset;
+
+type Intention :=
+  | Want
+  | Give;
+
+type Clause :=
+  mkClause {
+    lhs : Pair Intention QuantifiedAssets;
+    rhs : QuantifiedAssets
+  };
+
+any (as : List Asset) : QuantifiedAssets :=
+  mkAssets@{
+    quantifier := Any;
+    assets := as
+  };
+
+all (as : List Asset) : QuantifiedAssets :=
+  mkAssets@{
+    quantifier := All;
+    assets := as
+  };
+
+exactly (a : Asset) : QuantifiedAssets :=
+  mkAssets@{
+    quantifier := All;
+    assets := [a]
+  };
+
+want
+  (a : QuantifiedAssets) : Pair Intention QuantifiedAssets :=
+  Want, a;
+
+give
+  (a : QuantifiedAssets) : Pair Intention QuantifiedAssets :=
+  Give, a;
+
+syntax operator for pair;
+
+for
+  (l : Pair Intention QuantifiedAssets)
+  (qs : QuantifiedAssets)
+  : Clause :=
+  mkClause@{
+    lhs := l;
+    rhs := qs
+  };
+
+intent (clauses : List Clause) : Resource :=
+  mkIntent clauses;
+
+axiom mkIntent : List Clause -> Resource;

Package.juvix

@@ -0,0 +1,12 @@
+module Package;
+
+import PackageDescription.V2 open;
+
+package : Package :=
+  defaultPackage
+    {name := "anoma-app-patterns";
+     version := mkVersion 0 0 1;
+     dependencies := [ github "anoma" "juvix-anoma-stdlib" "v0.1.0"
+                     ; github "anoma" "juvix-stdlib" "v0.4.0"
+                     ; github "anoma" "juvix-containers" "v0.12.1"
+                     ]};

README.md

@@ -1,3 +1,3 @@
-# Nomine 
+# Anoma App Patterns 
 
-Nomine is a library for intent-centric application development.
+A library for intent-centric application development.

Token/Label.juvix

@@ -0,0 +1,23 @@
+module Token.Label;
+
+import Stdlib.Prelude open;
+import Anoma open;
+
+type Label :=
+  mkLabel {
+    name : Nat;
+    symbol : String;
+    decimals : Nat
+  };
+
+instance
+Label-Eq : Eq Label :=
+  mkEq@{
+    eq (d1 d2 : Label) : Bool :=
+      Label.name d1 == Label.name d2
+        && Label.symbol d1 == Label.symbol d2
+        && Label.decimals d1 == Label.decimals d2
+  };
+
+getLabel (r : Resource) : Label :=
+  anomaDecode (Resource.label r);

Token/Logic.juvix

@@ -0,0 +1,16 @@
+module Token.Logic;
+
+import Stdlib.Prelude open;
+import Anoma open;
+import AnomaHelpers open;
+
+import Authorization.Owner open;
+
+tokenLogic (self : Resource) (tx : Transaction) : Bool :=
+  if
+    | isConsumed self tx := isAuthorizedByOwner self tx
+    | isCreated self tx := true
+    | else := false;
+
+
+-- TODO Implement fixed supply

Token/Resource.juvix

@@ -0,0 +1,25 @@
+module Token.Resource;
+
+import Stdlib.Prelude open;
+import Anoma open;
+
+import Token.Label open;
+import Token.Logic open;
+import Authorization.Owner open;
+
+mkToken
+  (ephemeral : Bool)
+  (amount : Nat)
+  (tokenLabel : Label)
+  (ownerData : Owner)
+  : Resource :=
+  Resource.mk@{
+    logic := tokenLogic;
+    label := anomaEncode tokenLabel;
+    quantity := amount;
+    data := anomaEncode ownerData;
+    eph := ephemeral;
+    npk := Owner.owner ownerData;
+    nonce := 0;
+    rseed := 0
+  };