Merge pull request #11 from anoma/feature/fixed-supply

feat: implement fixed supply logic for `Token` and change message formats

AnomaHelpers.juvix

@@ -1,10 +1,12 @@
 module AnomaHelpers;
 
 import Stdlib.Prelude open;
+import Stdlib.Trait.Ord.Eq open using {fromOrdToEq};
+
 import Anoma open;
 
-import Data.Set open;
-import Data.Map open;
+import Data.Set as Set open using {Set};
+import Data.Map as Map open using {Map};
 
 -- Should be added to the `juvix-stdlib`
 type Either Error Result :=
@@ -24,18 +26,25 @@ find {A} (predicate : A → Bool) : List A → Maybe A
 type Bytes32 := mkBytes32 {unBytes32 : Nat};
 
 instance
-Bytes32Ord : Ord Bytes32 :=
+Bytes32-Ord : Ord Bytes32 :=
   mkOrd@{
     cmp : Bytes32 -> Bytes32 -> Ordering
       | (mkBytes32 b1) (mkBytes32 b2) := Ord.cmp b1 b2
   };
 
+instance
+Bytes32-Eq : Eq Bytes32 := Stdlib.Trait.Ord.Eq.fromOrdToEq;
+
+instance
+Bytes32-Show : Show Bytes32 :=
+  mkShow \ {b := natToString (Bytes32.unBytes32 b)};
+
 natToBytes32 : Nat -> Bytes32 := mkBytes32;
 
 type Bytes := mkBytes {unBytes : Nat};
 
 instance
-BytesOrd : Ord Bytes :=
+Bytes-Ord : Ord Bytes :=
   mkOrd@{
     cmp : Bytes -> Bytes -> Ordering
       | (mkBytes b1) (mkBytes b2) := Ord.cmp b1 b2
@@ -116,25 +125,49 @@ isConsumed (r : Resource) (tx : Transaction) : Bool :=
     r
     (ResourcePartition.consumed (partitionResources tx));
 
+type Lifecycle :=
+  | Consumed
+  | Created
+  | Unknown;
+
+lifecycle (r : Resource) (tx : Transaction) : Lifecycle :=
+  let
+    rs := partitionResources tx;
+    consumed := ResourcePartition.consumed rs;
+    created := ResourcePartition.created rs;
+  in if
+    | elem (==) r consumed := Consumed
+    | elem (==) r created := Created
+    | else := Unknown;
+
 isEphemeral (r : Resource) : Bool := Resource.eph r;
 
+type Ephemerality :=
+  | NonEphemeral
+  | Ephemeral;
+
+ephemerality (r : Resource) : Ephemerality :=
+  if
+    | isEphemeral r := Ephemeral
+    | else := NonEphemeral;
+
 isNullifierPresent
   (nf : Helper.Nullifier) (tx : Transaction) : Bool :=
   elem (==) nf (Transaction.nullifiers tx);
 
 isSubset {A} {{Ord A}} (sub sup : Set A) : Bool :=
-  all (x in Data.Set.toList sub)
-    member? x sup;
+  all (x in Set.toList sub)
+    Set.member? x sup;
 
 isSublist {A} {{Ord A}} (sub sup : List A) : Bool :=
   all (x in sub)
-    member? x (Data.Set.fromList sup);
+    Set.member? x (Set.fromList sup);
 
 commitmentSet (tx : Transaction) : Set Helper.Commitment :=
-  Data.Set.fromList (Transaction.commitments tx);
+  Set.fromList (Transaction.commitments tx);
 
 nullifierSet (tx : Transaction) : Set Helper.Nullifier :=
-  Data.Set.fromList (Transaction.nullifiers tx);
+  Set.fromList (Transaction.nullifiers tx);
 
 lookupExtraData
   {Value : Type}
@@ -144,20 +177,41 @@ lookupExtraData
   let
     keyValueMap : Map Bytes32 Value :=
       anomaDecode (Transaction.extra tx);
-  in lookup key keyValueMap;
+  in Map.lookup key keyValueMap;
 
 mkTransaction
-  (self : PrivateKey)
+  (nullifierKey : PrivateKey)
   (consumed : List Resource)
   (created : List Resource)
   (extraData : Map Bytes32 Bytes)
   : Transaction :=
   Transaction.mk@{
     roots := [];
     commitments := map commitment created;
-    nullifiers := map (r in consumed) nullifier r self;
+    nullifiers := map (r in consumed) nullifier r nullifierKey;
     proofs := consumed ++ created;
     delta := [];
     extra := anomaEncode (extraData);
     preference := 0
   };
+
+composeTransactions (tx1 tx2 : Transaction) : Transaction :=
+  Transaction.mk@{
+    roots := Transaction.roots tx1 ++ Transaction.roots tx2;
+    commitments :=
+      Transaction.commitments tx1
+        ++ Transaction.commitments tx2;
+    nullifiers :=
+      Transaction.nullifiers tx1 ++ Transaction.nullifiers tx2;
+    proofs := Transaction.proofs tx1 ++ Transaction.proofs tx2;
+    delta := Transaction.delta tx1 ++ Transaction.delta tx2;
+    extra :=
+      let
+        kvList1 : List (Pair Bytes32 Bytes) :=
+          Map.toList (anomaDecode (Transaction.extra tx1));
+        kvList2 : List (Pair Bytes32 Bytes) :=
+          Map.toList (anomaDecode (Transaction.extra tx2));
+      in anomaEncode (Map.fromList (kvList1 ++ kvList2));
+
+    preference := 0
+  };

Authorization/Message.juvix

@@ -1,83 +1,56 @@
 module Authorization.Message;
 
 import Stdlib.Prelude open;
-import Data.Map open;
-import Data.Set open;
+import Data.Map as Map open using {Map};
+import Data.Set as Set open using {Set};
 import Anoma open;
 import AnomaHelpers open;
 
--- TODO: Use nullifier once v2 specs are implemented.
-type LinkedCommitmentMessage :=
-  mkLinkedCommitmentMessage {
-    consumed : Helper.Commitment;
-    created : Helper.Commitment
+-- TODO use Helper.Nullifier once we comply with v2 specs
+type ResourceRelationship :=
+  mkResourceRelationship {
+    origin : Helper.Commitment;
+    mustBeCreated : Set Helper.Commitment;
+    mustBeConsumed : Set Helper.Commitment
   };
 
-type LinkedCommitmentSetMessage :=
-  mkLinkedCommitmentSetMessage {
-    consumed : Helper.Commitment;
-    createdSet : Set Helper.Commitment
-  };
-
--- TODO make signing optional
-mkLinkedCommitmentExtraDataMapEntry
-  (self : PrivateKey)
-  (created : Resource)
-  (consumed : Resource)
-  : Pair Bytes32 Bytes :=
-  let
-    consumedCm : Helper.Commitment := commitment consumed;
-    createdCm : Helper.Commitment := commitment created;
-    msg : LinkedCommitmentMessage :=
-      mkLinkedCommitmentMessage@{
-        consumed := consumedCm;
-        created := createdCm
-      };
-
-    k : Bytes32 := natToBytes32 consumedCm;
-    v : Bytes :=
-      natToBytes
-        (anomaEncode (msg, anomaSignDetached msg self));
-  in k, v;
-
 -- TODO make signing optional
-mkLinkedCommitmentSetExtraDataMapEntry
-  (self : PrivateKey)
-  (created : List Resource)
-  (consumed : Resource)
+mkResourceRelationshipExtraDataMapEntry
+  (nullifierKey : PrivateKey)
+  (mustBeConsumed : List Resource)
+  (mustBeCreated : List Resource)
+  (origin : Resource)
   : Pair Bytes32 Bytes :=
   let
-    consumedCm : Helper.Commitment := commitment consumed;
+    originCm : Helper.Commitment := commitment origin;
+    consumedNfs : Set Helper.Nullifier :=
+      Set.fromList
+        (map \ {r := nullifier r nullifierKey} mustBeConsumed);
     createdCms : Set Helper.Commitment :=
-      Data.Set.fromList (map commitment created);
-    msg : LinkedCommitmentSetMessage :=
-      mkLinkedCommitmentSetMessage@{
-        consumed := consumedCm;
-        createdSet := createdCms
+      Set.fromList (map commitment mustBeCreated);
+    msg : ResourceRelationship :=
+      mkResourceRelationship@{
+        origin := originCm;
+        mustBeConsumed := consumedNfs;
+        mustBeCreated := createdCms
       };
 
-    k : Bytes32 := natToBytes32 consumedCm;
+    k : Bytes32 := natToBytes32 originCm;
     v : Bytes :=
       natToBytes
-        (anomaEncode (msg, anomaSignDetached msg self));
+        (anomaEncode (msg, anomaSignDetached msg nullifierKey));
   in k, v;
 
-mkLinkedCommitmentExtraData
-  (self : PrivateKey)
-  (consumed : List Resource)
-  (created : Resource)
-  : Map Bytes32 Bytes :=
-  Data.Map.fromList
-    (map
-      (mkLinkedCommitmentExtraDataMapEntry self created)
-      consumed);
-
-mkLinkedCommitmentSetExtraData
-  (self : PrivateKey)
-  (consumed : List Resource)
-  (created : List Resource)
+mkResourceRelationshipExtraData
+  (nullifierKey : PrivateKey)
+  (origins : List Resource)
+  (mustBeConsumed : List Resource)
+  (mustBeCreated : List Resource)
   : Map Bytes32 Bytes :=
-  Data.Map.fromList
+  Map.fromList
     (map
-      (mkLinkedCommitmentSetExtraDataMapEntry self created)
-      consumed);
+      (mkResourceRelationshipExtraDataMapEntry
+        nullifierKey
+        mustBeConsumed
+        mustBeCreated)
+      origins);

Authorization/Owner.juvix

@@ -41,13 +41,16 @@ isAuthorizedByOwner
   let
     selfCm : Helper.Commitment := commitment self;
     lookupResult
-      : Maybe (Pair LinkedCommitmentSetMessage Signature) :=
+      : Maybe (Pair ResourceRelationship Signature) :=
       lookupExtraData (natToBytes32 selfCm) tx;
   in case lookupResult of
        | nothing := false
        | just (msg, sig) :=
-         LinkedCommitmentSetMessage.consumed msg == selfCm
+         ResourceRelationship.origin msg == selfCm
            && anomaVerifyDetached sig msg (getOwner self)
            && isSubset
-             (LinkedCommitmentSetMessage.createdSet msg)
+             (ResourceRelationship.mustBeConsumed msg)
+             (nullifierSet tx)
+           && isSubset
+             (ResourceRelationship.mustBeCreated msg)
              (commitmentSet tx);

Token/Logic.juvix

@@ -6,21 +6,32 @@ import AnomaHelpers open;
 
 import Authorization.Owner open;
 import Token.Supply open;
+import Token.Label open;
 
 tokenLogic
   (supply : Supply) : Resource -> Transaction -> Bool :=
   case supply of
     | Unbound := unboundSupplyLogic
-    | Fixed := fixedSupplyLogic
-    | Capped := cappedSupplyLogic;
+    | Capped := cappedSupplyLogic
+    | Fixed f := fixedSupplyLogic (FixingNullifier.nf f);
 
 unboundSupplyLogic
   (self : Resource) (tx : Transaction) : Bool :=
-  if
-    | isConsumed self tx := isAuthorizedByOwner self tx
-    | isCreated self tx := true
-    | else := false;
+  case lifecycle self tx of
+    | Consumed := isAuthorizedByOwner self tx
+    | Created := true
+    | Unknown := false;
 
-axiom fixedSupplyLogic : Resource -> Transaction -> Bool;
+fixedSupplyLogic
+  (nf : Helper.Nullifier)
+  (self : Resource)
+  (tx : Transaction)
+  : Bool :=
+  case ephemerality self of
+    | NonEphemeral := unboundSupplyLogic self tx
+    | Ephemeral :=
+      case lifecycle self tx of
+        | Consumed := isNullifierPresent nf tx
+        | _ := false;
 
 axiom cappedSupplyLogic : Resource -> Transaction -> Bool;

Token/Projection.juvix

@@ -1,8 +1,8 @@
 module Token.Projection;
 
 import Stdlib.Prelude open;
-import Data.Map open;
-import Data.Set open;
+import Data.Set as Set open using {Set};
+import Data.Map as Map open using {Map};
 
 import Anoma open;
 
@@ -13,12 +13,12 @@ import Anoma open;
 --- consumed ;Resource;s are present.
 getBalance (kind : Kind) (account : PublicKey) : Nat :=
   let
-    ledgers : Map PublicKey (Set Helper.Commitment) :=
+    ledger : Map PublicKey (Set Helper.Commitment) :=
       anomaGet (anomaEncode (kind));
-    result := lookup account ledgers;
+    result := Map.lookup account ledger;
   in case result of
        | just ledger :=
-         for (sum := 0) (cm in Data.Set.toList ledger)
+         for (sum := 0) (cm in Set.toList ledger)
            {let
              q := Resource.quantity (commitmentResource cm);
            in q + sum}

Token/Supply.juvix

@@ -1,19 +1,24 @@
 module Token.Supply;
 
 import Stdlib.Prelude open;
+import Anoma open;
+
+type FixingNullifier :=
+  mkFixingNullifier {nf : Helper.Nullifier};
 
 type Supply :=
   | Unbound
   | Capped
-  | Fixed;
+  | Fixed FixingNullifier;
 
 instance
 Supply-Eq : Eq Supply :=
   mkEq@{
     eq : Supply -> Supply -> Bool
       | Unbound Unbound := true
       | Capped Capped := true
-      | Fixed Fixed := true
+      | (Fixed f1) (Fixed f2) :=
+        FixingNullifier.nf f1 == FixingNullifier.nf f2
       | _ _ := false
   };
 
@@ -23,5 +28,8 @@ Supply-Show : Show Supply :=
     \ {
       | Unbound := "Unbound"
       | Capped := "Capped"
-      | Fixed := "Fixed"
+      | (Fixed f) :=
+        "Fixed (nf: "
+          ++str natToString (FixingNullifier.nf f)
+          ++str ")"
     };