Merge pull request #15 from anoma/feature/transferable

feat: add non-transferability property

Author: heueristik

Token/Error.juvix

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

Token/Label.juvix

@@ -12,6 +12,7 @@ type Label :=
     symbol : String;
     decimals : Nat;
     supply : Supply;
+    transferable : Bool;
     originator : PublicKey
   };
 
@@ -41,6 +42,9 @@ Label-Show : Show Label :=
         ++str "supply : "
         ++str (l |> Label.supply |> Show.show)
         ++str ", "
+        ++str "transferable : "
+        ++str (l |> Label.transferable |> Show.show)
+        ++str ", "
         ++str "originator : "
         ++str (l |> Label.supply |> Show.show)
         ++str "}"};
@@ -55,6 +59,8 @@ getDecimals (r : Resource) : Nat := Label.decimals (getLabel r);
 
 getSupply (r : Resource) : Supply := Label.supply (getLabel r);
 
+isTransferable (r : Resource) : Bool := Label.transferable (getLabel r);
+
 getOriginator (r : Resource) : PublicKey := Label.originator (getLabel r);
 
 terminating
@@ -83,3 +89,8 @@ InvalidLabelError-Show : Show InvalidLabelError :=
         ++str "actual"
         ++str (e |> InvalidLabelError.actual |> Show.show)
         ++str "}"};
+
+type NonTransferableError := mkNonTransferableError;
+
+instance
+NonTransferableError-Show : Show NonTransferableError := mkShow \ {e := "NonTransferableError"};

Token/Logic.juvix

@@ -18,16 +18,21 @@ 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, NonEphemeral := isAuthorizedBy (getOwner self) self tx
+    | Consumed, NonEphemeral := transferLogic self tx
     | Created, _ := true
     | Unknown, _ := false;
 
 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, NonEphemeral := isAuthorizedBy (getOwner self) self tx
+    | Consumed, NonEphemeral := transferLogic self tx
     | Created, Ephemeral := false
     | Created, NonEphemeral := true
     | Unknown, _ := false;
 
 axiom cappedSupplyLogic : Resource -> Transaction -> Bool;
+
+transferLogic (self : Resource) (tx : Transaction) : Bool :=
+  case isTransferable self of
+    | true := isAuthorizedBy (getOwner self) self tx
+    | false := false;

Token/Transaction.juvix

@@ -95,6 +95,7 @@ transfer (self : KeyPair) (token : Resource) (receiver : PublicKey)
       mustBeCreated := createdRs
     };
   in if
+    | not (isTransferable token) := throw mkNonTransferableError
     | owner /= myself := throw mkUnauthorizedError@{expected := myself; actual := owner}
     | else := ok (mkTransaction mySecret consumedRs createdRs extraData);
 
@@ -123,6 +124,7 @@ split (self : KeyPair) (token : Resource) (amountsAndReceivers : List (Pair Nat
       mustBeCreated := createdRs
     };
   in if
+    | not (isTransferable token) := throw mkNonTransferableError
     | owner /= myself := throw mkUnauthorizedError@{expected := myself; actual := owner}
     | balance /= sum := throw mkInsufficientQuantityError@{limit := balance; actual := sum}
     | else := ok (mkTransaction mySecret consumedRs createdRs extraData);
@@ -139,15 +141,14 @@ send (self : KeyPair) (token : Resource) (amount : Nat) (receiver : PublicKey)
   let
     myself : PublicKey := KeyPair.pubKey self;
     availableAmount : Nat := Resource.quantity token;
-  in
-    case (compare availableAmount amount) of
-    | LT := throw mkInsufficientQuantityError@{limit := availableAmount; actual := amount}
-    | EQ := transfer self token receiver
-    | GT :=
-      let
-        remainder : Nat := toNat (intSubNat availableAmount amount);
-      in
-        split self token [(amount, receiver); (remainder, myself)];
+  in case (compare availableAmount amount) of
+      | LT := throw mkInsufficientQuantityError@{limit := availableAmount; actual := amount}
+      | EQ := transfer self token receiver
+      | GT :=
+        let
+          remainder : Nat := toNat (intSubNat availableAmount amount);
+        in
+          split self token [(amount, receiver); (remainder, myself)];
 
 --- Merges token ;Resource;s, if the calling ;KeyPair; is the owner of all
 --- of them and the ;Label;s match.
@@ -178,12 +179,15 @@ merge (self : KeyPair) (tokens : List Resource) (receiver : PublicKey)
         mustBeConsumed := [];
         mustBeCreated := createdRs
       };
-      in case find ((/=) owner) (map getOwner tokens) of
-        | just wrongOwner := throw mkUnauthorizedError@{expected := myself; actual := wrongOwner}
-        | nothing :=
-          case find ((/=) label) (map getLabel tokens) of
-          | just wrongLabel := throw mkInvalidLabelError@{expected := label; actual := wrongLabel}
-          | nothing :=
-            case find ((/=) logic) (map getLogic tokens) of
-            | just wrongLogic := throw mkInvalidLogicError@{expected := logic; actual := wrongLogic}
-            | nothing := ok (mkTransaction mySecret consumedRs createdRs extraData);
+      in if 
+        | not (isTransferable t) := throw mkNonTransferableError
+        | else :=
+          case find ((/=) owner) (map getOwner tokens) of
+            | just wrongOwner := throw mkUnauthorizedError@{expected := myself; actual := wrongOwner}
+            | nothing :=
+              case find ((/=) label) (map getLabel tokens) of
+              | just wrongLabel := throw mkInvalidLabelError@{expected := label; actual := wrongLabel}
+              | nothing :=
+                case find ((/=) logic) (map getLogic tokens) of
+                | just wrongLogic := throw mkInvalidLogicError@{expected := logic; actual := wrongLogic}
+                | nothing := ok (mkTransaction mySecret consumedRs createdRs extraData);