Merge pull request #21 from anoma/feature/refactoring

feature: add swap and refactor file structure

AnomaHelpers.juvix

@@ -101,6 +101,27 @@ InvalidLogicError-Show : Show InvalidLogicError :=
         ++str (e |> InvalidLogicError.actual |> Show.show)
         ++str "}"};
 
+instance
+Kind-Show : Show Kind := mkShow \ {k := natToString (Kind.unKind k)};
+
+type InvalidKindError :=
+  mkInvalidKindError {
+    expected : Kind;
+    actual : Kind
+  };
+
+instance
+InvalidKindError-Show : Show InvalidKindError :=
+  mkShow
+    \ {e :=
+      "InvalidLogicError:\n{"
+        ++str "expected : "
+        ++str (e |> InvalidKindError.expected |> Show.show)
+        ++str ", "
+        ++str "actual"
+        ++str (e |> InvalidKindError.actual |> Show.show)
+        ++str "}"};
+
 isCreated (r : Resource) (tx : Transaction) : Bool :=
   elem (==) r (ResourcePartition.created (partitionResources tx));
 
@@ -142,6 +163,17 @@ isSublist {A} {{Ord A}} (sub sup : List A) : Bool :=
   all (x in sub)
     Set.member? x (Set.fromList sup);
 
+module Kind;
+  toPair (kind : Kind) : Pair (Resource -> Transaction -> Bool) Nat :=
+    anomaDecode (Kind.unKind kind);
+
+  toLogic (kind : Kind) : Resource -> Transaction -> Bool := fst (toPair kind);
+
+  toLabel (kind : Kind) : Nat := snd (toPair kind);
+
+  open Kind public;
+end;
+
 commitmentSet (tx : Transaction) : Set Commitment := Set.fromList (Transaction.commitments tx);
 
 nullifierSet (tx : Transaction) : Set Nullifier := Set.fromList (Transaction.nullifiers tx);
@@ -183,3 +215,5 @@ compose (tx1 tx2 : Transaction) : Transaction :=
       in anomaEncode (Map.fromList (kvList1 ++ kvList2));
     preference := 0
   };
+
+rand : Nat := 0;

Authorization/Message.juvix

@@ -46,3 +46,23 @@ mkResourceRelationshipExtraData
     (map
       (mkResourceRelationshipExtraDataMapEntry nullifierKey mustBeConsumed mustBeCreated)
       origins);
+
+mkTxWithExtraData
+  (nk : PrivateKey) (consumed : List Resource) (created : List Resource) : Transaction :=
+  Transaction.mk@{
+    roots := [];
+    commitments := map commitment created;
+    nullifiers := map (r in consumed) nullifier r nk;
+    proofs := consumed ++ created;
+    complianceProofs := [];
+    delta := [];
+    extra :=
+      anomaEncode
+        mkResourceRelationshipExtraData@{
+          nullifierKey := nk;
+          origins := consumed;
+          mustBeConsumed := [];
+          mustBeCreated := created
+        };
+    preference := 0
+  };

Intent/Asset.juvix

@@ -0,0 +1,29 @@
+module Intent.Asset;
+
+import Stdlib.Prelude open;
+import Anoma open;
+
+type Asset :=
+  mkAsset {
+    quantity : Nat;
+    kind : Kind
+  };
+
+type Quantifier :=
+  | Any
+  | All;
+
+type QuantifiedAssets :=
+  mkQuantifiedAssets {
+    quantifier : Quantifier;
+    assets : List Asset
+  };
+
+--- Checks if an ;Asset; is included in a list of resources.
+--- The resource ;Kind; must match, the quantity must be
+--- greater or equal, and the `npk` must be the ;PublicKey; of the receiver.
+includesAsset (asset : Asset) (receiver : PublicKey) (resources : List Resource) : Bool :=
+  any (r in resources)
+    Asset.quantity asset <= Resource.quantity r
+      && Asset.kind asset == anomaKind r
+      && receiver == Resource.npk r;

Intent/DSL.juvix

@@ -4,24 +4,7 @@ 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;
+import Intent.Asset open;
 
 type Intention :=
   | Want
@@ -33,20 +16,24 @@ type Clause :=
     rhs : QuantifiedAssets
   };
 
+syntax operator of_ additive;
+
+syntax alias of_ := mkAsset;
+
 any (as : List Asset) : QuantifiedAssets :=
-  mkAssets@{
+  mkQuantifiedAssets@{
     quantifier := Any;
     assets := as
   };
 
 all (as : List Asset) : QuantifiedAssets :=
-  mkAssets@{
+  mkQuantifiedAssets@{
     quantifier := All;
     assets := as
   };
 
 exactly (a : Asset) : QuantifiedAssets :=
-  mkAssets@{
+  mkQuantifiedAssets@{
     quantifier := All;
     assets := [a]
   };
@@ -66,3 +53,9 @@ for (l : Pair Intention QuantifiedAssets) (qs : QuantifiedAssets) : Clause :=
 intent (clauses : List Clause) : Resource := mkIntent clauses;
 
 axiom mkIntent : List Clause -> Resource;
+
+A : Kind := Kind.mk 1;
+
+B : Kind := Kind.mk 1;
+
+aliceIntentClause : QuantifiedAssets := any [5 of_ A; 3 of_ B];

Token/Error.juvix

@@ -12,6 +12,7 @@ type TokenError :=
   | ErrTokenInsufficientQuantity InsufficientQuantityError
   | ErrTokenInvalidLabel InvalidLabelError
   | ErrTokenInvalidLogic InvalidLogicError
+  | ErrTokenInvalidKind InvalidKindError
   | ErrNonTransferable NonTransferableError
   | ErrTokenInsufficientElements InsufficientElementsError
   | ErrTokenDefault Error;
@@ -54,6 +55,12 @@ InvalidLogicThrowable {A} : TokenThrowable InvalidLogicError A :=
     throw (e : InvalidLogicError) : Result TokenError A := error {_} {A} (ErrTokenInvalidLogic e)
   };
 
+instance
+InvalidKindThrowable {A} : TokenThrowable InvalidKindError A :=
+  mkTokenThrowable@{
+    throw (e : InvalidKindError) : Result TokenError A := error {_} {A} (ErrTokenInvalidKind e)
+  };
+
 instance
 NonTransferableThrowable {A} : TokenThrowable NonTransferableError A :=
   mkTokenThrowable@{

Token/Label.juvix

@@ -63,15 +63,6 @@ isTransferable (r : Resource) : Bool := Label.transferable (getLabel r);
 
 getOriginator (r : Resource) : PublicKey := Label.originator (getLabel r);
 
-terminating
-containsWrongLabel (labels : List Label) (label : Label) : Maybe Label :=
-  case labels of
-    | nil := nothing
-    | l :: ls :=
-      if
-        | l /= label := just l
-        | else := containsWrongLabel ls label;
-
 type InvalidLabelError :=
   mkInvalidLabelError {
     expected : Label;

Token/Logic.juvix

@@ -16,24 +16,27 @@ tokenLogic (supply : Supply) : Resource -> Transaction -> Bool :=
 
 unboundSupplyLogic (self : Resource) (tx : Transaction) : Bool :=
   case lifecycle self tx, ephemerality self of
-    | Consumed, Ephemeral := isAuthorizedBy (getOriginator self) self tx
+    | Consumed, Ephemeral := unboundSupplyInitializationLogic self tx
     | Consumed, NonEphemeral := transferLogic self tx
-    | Created, _ := true
+    | Created, Ephemeral := true
+    | Created, NonEphemeral := true
     | Unknown, _ := false;
 
+unboundSupplyInitializationLogic (self : Resource) (tx : Transaction) : Bool :=
+  isAuthorizedBy (getOriginator self) self tx;
+
 fixedSupplyLogic (nf : Nullifier) (self : Resource) (tx : Transaction) : Bool :=
   case lifecycle self tx, ephemerality self of
-    | Consumed, Ephemeral := isAuthorizedBy (getOriginator self) self tx && isNullifierPresent nf tx
+    | Consumed, Ephemeral := fixedSupplyInitializationLogic nf self tx
     | Consumed, NonEphemeral := transferLogic self tx
     | Created, Ephemeral := false
     | Created, NonEphemeral := true
     | Unknown, _ := false;
 
+fixedSupplyInitializationLogic (nf : Nullifier) (self : Resource) (tx : Transaction) : Bool :=
+  isNullifierPresent nf tx && isAuthorizedBy (getOriginator self) self tx;
+
 axiom cappedSupplyLogic : Resource -> Transaction -> Bool;
 
 transferLogic (self : Resource) (tx : Transaction) : Bool :=
-  case isTransferable self of
-    | true := isAuthorizedBy (getOwner self) self tx
-    | false := false;
-
-getOwner (r : Resource) : PublicKey := Resource.npk r;
+  isTransferable self && isAuthorizedBy (Resource.npk self) self tx;

Token/Projection.juvix

@@ -1,24 +1,3 @@
 module Token.Projection;
 
-import Stdlib.Prelude open;
-import Data.Set as Set open using {Set};
-import Data.Map as Map open using {Map};
-
-import Anoma open;
-
---- Returns the total quantity of all resources  ;Kind; by looking up
---- a ;Set; of ;Commitment;s associated with an account's ;PublicKey;
---- from the key-value storage.
---- This assume that the set is is up-to-date an no ;Commitment;s of
---- consumed ;Resource;s are present.
-getBalance (kind : Kind) (account : PublicKey) : Nat :=
-  let
-    ledger : Map PublicKey (Set Commitment) := anomaGet (anomaEncode (kind));
-    result := Map.lookup account ledger;
-  in case result of
-       | nothing := 0
-       | just ledger :=
-         for (sum := 0) (cm in Set.toList ledger)
-           {let
-             q := Resource.quantity (commitmentResource cm);
-           in q + sum};
+import Token.Projection.Balance open public;

Token/Projection/Balance.juvix

@@ -0,0 +1,18 @@
+module Token.Projection.Balance;
+
+import Stdlib.Prelude open;
+import Data.Set as Set open using {Set};
+import Anoma open;
+
+--- Returns the total quantity of all resources  ;Kind; by looking up
+--- a ;Set; of ;Commitment;s associated with an account's ;PublicKey;
+--- from the key-value storage.
+--- This assume that the set is is up-to-date an no ;Commitment;s of
+--- consumed ;Resource;s are present.
+balance (kind : Kind) (account : PublicKey) : Nat :=
+  let
+    ownedResources : Set Commitment := anomaGet (kind, account);
+  in for (sum := 0) (cm in Set.toList ownedResources)
+       {let
+         q := Resource.quantity (commitmentResource cm);
+       in q + sum};

Token/Resource.juvix

@@ -2,20 +2,19 @@ module Token.Resource;
 
 import Stdlib.Prelude open;
 import Anoma open;
+import AnomaHelpers open;
 
 import Token.Label open;
 import Token.Logic open;
 
-mkToken (eph : Bool) (quantity : Nat) (tokenLabel : Label) (owner : PublicKey) : Resource :=
+mkToken (quantity : Nat) (tokenLabel : Label) (npk : PublicKey) {eph : Bool := false} : Resource :=
   Resource.mk@{
     logic := tokenLogic (Label.supply tokenLabel);
     label := anomaEncode (tokenLabel);
     quantity;
     data := 0;
     eph;
-    npk := owner;
-    nonce := 0;
-    rseed := 0
+    npk;
+    nonce := rand;
+    rseed := rand
   };
-
-