Merge pull request #14 from anoma/feature/deps-update

feat: update dependencies

Author: heueristik

.gitignore

@@ -2,3 +2,4 @@
 .history
 *.nockma
 .DS_Store
+.vscode/*

AnomaHelpers.juvix

@@ -8,21 +8,13 @@ import Anoma 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 :=
-  | left Error
-  | right Result;
-
---- Returns the leftmost element of the list satisfying the predicate or
---- nothing if there's no such element.
-find {A} (predicate : A → Bool) : List A → Maybe A
-  | nil := nothing
-  | (x :: xs) :=
-    if
-      | predicate x := just x
-      | else := find predicate xs;
-
 -- Should be added to the `juvix-anoma-stdlib`
+instance
+PublicKey-Show : Show PublicKey := mkShow \ {k := natToString (PublicKey.unPublicKey k)};
+
+instance
+PrivateKey-Show : Show PrivateKey := mkShow \ {k := natToString (PrivateKey.unPrivateKey k)};
+
 type Bytes32 := mkBytes32 {unBytes32 : Nat};
 
 instance
@@ -36,8 +28,7 @@ instance
 Bytes32-Eq : Eq Bytes32 := Stdlib.Trait.Ord.Eq.fromOrdToEq;
 
 instance
-Bytes32-Show : Show Bytes32 :=
-  mkShow \ {b := natToString (Bytes32.unBytes32 b)};
+Bytes32-Show : Show Bytes32 := mkShow \ {b := natToString (Bytes32.unBytes32 b)};
 
 natToBytes32 : Nat -> Bytes32 := mkBytes32;
 
@@ -52,8 +43,7 @@ Bytes-Ord : Ord Bytes :=
 
 natToBytes : Nat -> Bytes := mkBytes;
 
-getLogic (r : Resource) : Nat :=
-  anomaEncode (Resource.logic r);
+getLogic (r : Resource) : Nat := anomaEncode (Resource.logic r);
 
 type Error := mkError {msg : String};
 
@@ -64,8 +54,7 @@ type InsufficientElementsError :=
   };
 
 instance
-InsufficientElementsError-Show
-  : Show InsufficientElementsError :=
+InsufficientElementsError-Show : Show InsufficientElementsError :=
   mkShow
     \ {e :=
       "InsufficientElementsError:\n{"
@@ -83,8 +72,7 @@ type InsufficientQuantityError :=
   };
 
 instance
-InsufficientQuantityError-Show
-  : Show InsufficientQuantityError :=
+InsufficientQuantityError-Show : Show InsufficientQuantityError :=
   mkShow
     \ {e :=
       "InsufficientQuantityError:\n{"
@@ -114,16 +102,10 @@ InvalidLogicError-Show : Show InvalidLogicError :=
         ++str "}"};
 
 isCreated (r : Resource) (tx : Transaction) : Bool :=
-  elem
-    (==)
-    r
-    (ResourcePartition.created (partitionResources tx));
+  elem (==) r (ResourcePartition.created (partitionResources tx));
 
 isConsumed (r : Resource) (tx : Transaction) : Bool :=
-  elem
-    (==)
-    r
-    (ResourcePartition.consumed (partitionResources tx));
+  elem (==) r (ResourcePartition.consumed (partitionResources tx));
 
 type Lifecycle :=
   | Consumed
@@ -151,32 +133,22 @@ ephemerality (r : Resource) : Ephemerality :=
     | isEphemeral r := Ephemeral
     | else := NonEphemeral;
 
-isNullifierPresent
-  (nf : Helper.Nullifier) (tx : Transaction) : Bool :=
+isNullifierPresent (nf : Nullifier) (tx : Transaction) : Bool :=
   elem (==) nf (Transaction.nullifiers tx);
 
-isSubset {A} {{Ord A}} (sub sup : Set A) : Bool :=
-  all (x in Set.toList sub)
-    Set.member? x sup;
+isSubset {A} {{Ord A}} (sub sup : Set A) : Bool := all (x in Set.toList sub) Set.member? x sup;
 
 isSublist {A} {{Ord A}} (sub sup : List A) : Bool :=
   all (x in sub)
     Set.member? x (Set.fromList sup);
 
-commitmentSet (tx : Transaction) : Set Helper.Commitment :=
-  Set.fromList (Transaction.commitments tx);
+commitmentSet (tx : Transaction) : Set Commitment := Set.fromList (Transaction.commitments tx);
 
-nullifierSet (tx : Transaction) : Set Helper.Nullifier :=
-  Set.fromList (Transaction.nullifiers tx);
+nullifierSet (tx : Transaction) : Set Nullifier := Set.fromList (Transaction.nullifiers tx);
 
-lookupExtraData
-  {Value : Type}
-  (key : Bytes32)
-  (tx : Transaction)
-  : Maybe Value :=
+lookupExtraData {Value : Type} (key : Bytes32) (tx : Transaction) : Maybe Value :=
   let
-    keyValueMap : Map Bytes32 Value :=
-      anomaDecode (Transaction.extra tx);
+    keyValueMap : Map Bytes32 Value := anomaDecode (Transaction.extra tx);
   in Map.lookup key keyValueMap;
 
 mkTransaction
@@ -190,28 +162,24 @@ mkTransaction
     commitments := map commitment created;
     nullifiers := map (r in consumed) nullifier r nullifierKey;
     proofs := consumed ++ created;
+    complianceProofs := [];
     delta := [];
     extra := anomaEncode (extraData);
     preference := 0
   };
 
-composeTransactions (tx1 tx2 : Transaction) : Transaction :=
+compose (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;
+    commitments := Transaction.commitments tx1 ++ Transaction.commitments tx2;
+    nullifiers := Transaction.nullifiers tx1 ++ Transaction.nullifiers tx2;
     proofs := Transaction.proofs tx1 ++ Transaction.proofs tx2;
+    complianceProofs := Transaction.complianceProofs tx1 ++ Transaction.complianceProofs 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));
+        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/Check.juvix

@@ -7,30 +7,22 @@ import AnomaHelpers open;
 import Authorization.Message open;
 
 -- TODO use nullifer instead of commitment
-isAuthorizedBy
-  (signer : PublicKey)
-  (self : Resource)
-  (_tx : Transaction)
-  : Bool :=
+isAuthorizedBy (signer : PublicKey) (self : Resource) (tx : Transaction) : Bool :=
   let
     cm := commitment self;
   in case
        lookupExtraData@{
-         key := natToBytes32 cm;
+         key := natToBytes32 (anomaEncode cm);
          Value := Pair ResourceRelationship Signature;
-         tx := _tx
+         tx
        }
      of
        | nothing := false
        | just (msg, sig) :=
          ResourceRelationship.origin msg == cm
            && anomaVerifyDetached sig msg signer
-           && isSubset
-             (ResourceRelationship.mustBeConsumed msg)
-             (nullifierSet _tx)
-           && isSubset
-             (ResourceRelationship.mustBeCreated msg)
-             (commitmentSet _tx);
+           && isSubset (ResourceRelationship.mustBeConsumed msg) (nullifierSet tx)
+           && isSubset (ResourceRelationship.mustBeCreated msg) (commitmentSet tx);
 
 type UnauthorizedError :=
   mkUnauthorizedError {

Authorization/Identities.juvix

@@ -2,16 +2,24 @@ module Authorization.Identities;
 
 import Anoma open;
 
---- The keypair generated from the seed `0x0000000000000000000000000000000000000000000000000000000000000000`
+--- The ;KeyPair; generated from the seed `0x0000000000000000000000000000000000000000000000000000000000000000`
 --- (see, e.g., https://cyphr.me/ed25519_tool/ed.html) in little-endian byte order.
-universal : KeyPair :=
-  mkKeyPair@{
-    pubKey :=
-      0x29da598ba148c03aa643e21d77153265730d6f2ad0a8a3622da4b6cebc276a3b;
-    privKey :=
-      0x29da598ba148c03aa643e21d77153265730d6f2ad0a8a3622da4b6cebc276a3b0000000000000000000000000000000000000000000000000000000000000000
-  };
+module Universal;
+  keyPair : KeyPair :=
+    KeyPair.mk@{
+      pubKey := PublicKey.mk 0x29da598ba148c03aa643e21d77153265730d6f2ad0a8a3622da4b6cebc276a3b;
+      privKey :=
+        PrivateKey.mk
+          0x29da598ba148c03aa643e21d77153265730d6f2ad0a8a3622da4b6cebc276a3b0000000000000000000000000000000000000000000000000000000000000000
+    };
 
-universalPubKey : PublicKey := KeyPair.pubKey universal;
+  pubKey : PublicKey := KeyPair.pubKey keyPair;
 
-universalPrivKey : PublicKey := KeyPair.privKey universal;
+  privKey : PrivateKey := KeyPair.privKey keyPair;
+end;
+
+--- The zero ;PublicKey; `0x0000000000000000000000000000000000000000000000000000000000000000`
+--- for which the ;PrivateKey; is not known.
+module Zero;
+  pubKey : PublicKey := PublicKey.mk 0x0;
+end;

Authorization/Message.juvix

@@ -6,12 +6,12 @@ import Data.Set as Set open using {Set};
 import Anoma open;
 import AnomaHelpers open;
 
--- TODO use Helper.Nullifier once we comply with v2 specs
+-- TODO use Nullifier once we comply with v2 specs
 type ResourceRelationship :=
   mkResourceRelationship {
-    origin : Helper.Commitment;
-    mustBeCreated : Set Helper.Commitment;
-    mustBeConsumed : Set Helper.Commitment
+    origin : Commitment;
+    mustBeCreated : Set Commitment;
+    mustBeConsumed : Set Nullifier
   };
 
 -- TODO make signing optional
@@ -22,23 +22,18 @@ mkResourceRelationshipExtraDataMapEntry
   (origin : Resource)
   : Pair Bytes32 Bytes :=
   let
-    originCm : Helper.Commitment := commitment origin;
-    consumedNfs : Set Helper.Nullifier :=
-      Set.fromList
-        (map \ {r := nullifier r nullifierKey} mustBeConsumed);
-    createdCms : Set Helper.Commitment :=
-      Set.fromList (map commitment mustBeCreated);
+    originCm : Commitment := commitment origin;
+    consumedNfs : Set Nullifier :=
+      Set.fromList (map \ {r := nullifier r nullifierKey} mustBeConsumed);
+    createdCms : Set Commitment := Set.fromList (map commitment mustBeCreated);
     msg : ResourceRelationship :=
       mkResourceRelationship@{
         origin := originCm;
         mustBeConsumed := consumedNfs;
         mustBeCreated := createdCms
       };
-
-    k : Bytes32 := natToBytes32 originCm;
-    v : Bytes :=
-      natToBytes
-        (anomaEncode (msg, anomaSignDetached msg nullifierKey));
+    k : Bytes32 := natToBytes32 (anomaEncode originCm);
+    v : Bytes := natToBytes (anomaEncode (msg, anomaSignDetached msg nullifierKey));
   in k, v;
 
 mkResourceRelationshipExtraData
@@ -49,8 +44,5 @@ mkResourceRelationshipExtraData
   : Map Bytes32 Bytes :=
   Map.fromList
     (map
-      (mkResourceRelationshipExtraDataMapEntry
-        nullifierKey
-        mustBeConsumed
-        mustBeCreated)
+      (mkResourceRelationshipExtraDataMapEntry nullifierKey mustBeConsumed mustBeCreated)
       origins);

Authorization/Owner.juvix

@@ -8,9 +8,7 @@ type Owner := mkOwner {owner : PublicKey};
 instance
 Owner-Eq : Eq Owner :=
   mkEq@{
-    eq (d1 d2 : Owner) : Bool :=
-      Owner.owner d1 == Owner.owner d2
+    eq (d1 d2 : Owner) : Bool := Owner.owner d1 == Owner.owner d2
   };
 
-getOwner (r : Resource) : PublicKey :=
-  Owner.owner (anomaDecode (Resource.data r));
+getOwner (r : Resource) : PublicKey := Owner.owner (anomaDecode (Resource.data r));

Intent/DSL.juvix

@@ -51,26 +51,18 @@ exactly (a : Asset) : QuantifiedAssets :=
     assets := [a]
   };
 
-want
-  (a : QuantifiedAssets) : Pair Intention QuantifiedAssets :=
-  Want, a;
+want (a : QuantifiedAssets) : Pair Intention QuantifiedAssets := Want, a;
 
-give
-  (a : QuantifiedAssets) : Pair Intention QuantifiedAssets :=
-  Give, a;
+give (a : QuantifiedAssets) : Pair Intention QuantifiedAssets := Give, a;
 
 syntax operator for pair;
 
-for
-  (l : Pair Intention QuantifiedAssets)
-  (qs : QuantifiedAssets)
-  : Clause :=
+for (l : Pair Intention QuantifiedAssets) (qs : QuantifiedAssets) : Clause :=
   mkClause@{
     lhs := l;
     rhs := qs
   };
 
-intent (clauses : List Clause) : Resource :=
-  mkIntent clauses;
+intent (clauses : List Clause) : Resource := mkIntent clauses;
 
 axiom mkIntent : List Clause -> Resource;

Package.juvix

@@ -3,10 +3,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"
-                     ]};
+  defaultPackage@?{
+    name := "anoma-app-patterns";
+    version := mkVersion 0 0 1;
+    dependencies :=
+      [ github "anoma" "juvix-anoma-stdlib" "v0.4.0"
+      ; github "anoma" "juvix-stdlib" "v0.5.0"
+      ; github "anoma" "juvix-containers" "v0.13.0"
+      ]
+  };