Merge branch 'develop'

.github/workflows/tests.yaml

@@ -13,19 +13,14 @@ jobs:
     steps:
       - name: checkout code
         uses: actions/checkout@v3
-
-      - name: Download latest nightly Juvix binary
+      - name: Download the Juvix binary
         uses: jaxxstorm/[email protected]
         with:
-          repo: anoma/juvix-nightly-builds
+          repo: anoma/juvix
           cache: enable
-
       - name: Clean
         run: juvix clean --global && juvix dependencies update 
-
-      - name: Run TokenLogic Test
-        run: juvix eval Token/Tests/TokenLogic.juvix
-
-      # NOTE: Skipped because of performance issues of `anomaDecode`
-      #- name: Run Swap Test
-      #  run: juvix eval Token/Tests/Swap.juvix
+      - name: Type Check
+        run: juvix typecheck
+      - name: Format Check
+        run: juvix format

Applib.juvix

@@ -0,0 +1,12 @@
+module Applib;
+
+import Applib.Resource open public;
+import Applib.Helpers open public;
+import Applib.Identities open public;
+
+import Applib.Transaction as Transaction public;
+import Applib.Projection as Projection public;
+import Applib.Authorization as Authorization public;
+import Applib.Intent as Intent public;
+import Applib.Token as Token public;
+import Applib.Utils as Utils public;

Applib/Authorization.juvix

@@ -0,0 +1,5 @@
+module Applib.Authorization;
+
+import Applib.Authorization.Check as Check open public;
+import Applib.Identities as Identities open public;
+import Applib.Authorization.Message as Message open public;

Applib/Authorization/Check.juvix

@@ -0,0 +1,41 @@
+module Applib.Authorization.Check;
+
+import Stdlib.Prelude open;
+
+import Anoma open;
+import Applib.Authorization.Message open;
+import Applib.Helpers open;
+import Stdlib.Data.Set as Set open using {Set};
+
+--- Checks if an ;ExternalIdentity; has authorized the creation and consumption of ;Resource;s within the same ;Action; as the resource logic performing this check.
+--- The check proceeds in five steps:
+--- 1. The ;ResourceRelationship; message and corresponding ;Signature; are looked up in ;AppData; with the ;Tag; of the checking resource as the lookup key.
+--- 3. The ;ResourceRelationship; message and corresponding ;Signature; are verified to be authored by the `signer` ;ExternalIdentity;.
+--- @param signer The external identity that has authorized the consumption and creation of resources.
+--- @param origin The ;Tag; referencing the resource that must perform the check.
+--- @param publicInputs The public inputs of the resource logic function.
+isAuthorizedBy
+  (signer : ExternalIdentity)
+  (origin : Tag)
+  (publicInputs : Logic.Instance)
+  : Bool :=
+  case
+    lookupAppData@{
+      key := origin;
+      Value := Pair ResourceRelationship Signature;
+      appData := Logic.Instance.appData publicInputs;
+    }
+  of
+    | nothing := false
+    | just (message, signature) :=
+      verify@{
+        signature;
+        message;
+        signer;
+      }
+        && checkResourceRelationship@{
+             message;
+             origin;
+             nullifiers := Logic.Instance.nullifiers publicInputs;
+             commitments := Logic.Instance.commitments publicInputs;
+           };

Applib/Authorization/Message.juvix

@@ -0,0 +1,142 @@
+module Applib.Authorization.Message;
+
+import Stdlib.Prelude open;
+import Stdlib.Data.Set as Set open using {Set};
+import Stdlib.Data.Map as Map;
+import Anoma open;
+import Anoma.Builtin.System open;
+
+import Applib.Helpers open;
+import Applib.Identities open;
+
+--- A message format specifiying resources that must be created and consumed within an ;Action;.
+--- @param origin The reference to the resource performing the check.
+--- @param mustBeConsumed The resources that must be consumed.
+--- @param mustBeCreated The resources that must be created.
+type ResourceRelationship :=
+  mkResourceRelationship@{
+    origin : Tag;
+    mustBeConsumed : Set Nullifier;
+    mustBeCreated : Set Commitment;
+  };
+
+--- Checks that a ;ResourceRelationship; message has the expected values.
+--- @param message The resource relationship message to check.
+--- @param origin The expected origin.
+--- @param nullifiers The nullifier set that must contain the `mustBeConsumed` nullifiers as a subset.
+--- @param commitments The commitment set that must contain the `mustBeCreated` commitments as a subset.
+--- @return The check result.
+checkResourceRelationship
+  (message : ResourceRelationship)
+  (origin : Tag)
+  (nullifiers : Set Nullifier)
+  (commitments : Set Commitment)
+  : Bool :=
+  ResourceRelationship.origin message == origin
+    && Set.isSubset (ResourceRelationship.mustBeConsumed message) nullifiers
+    && Set.isSubset (ResourceRelationship.mustBeCreated message) commitments;
+
+--- Creates an ;AppData; entry consisting of a ;ResourceRelationship; message and corresponding ;Signature; as the ;AppDataValue; and the resource ;Tag; value as the ;AppDataKey;.
+--- @param identity The identity to derive the nullifier key from.
+--- @param origin The resource performing the check.
+--- @param mustBeConsumed The resources that must be consumed.
+--- @param mustBeCreated The resources that must be created.
+--- @return The app data entry.
+mkResourceRelationshipAppDataEntry
+  (signer : InternalIdentity)
+  (origin : Tag)
+  (mustBeConsumed : Set Nullifier)
+  (mustBeCreated : Set Commitment)
+  : Pair AppDataKey AppDataValue :=
+  let
+    message : ResourceRelationship :=
+      mkResourceRelationship@{
+        origin;
+        mustBeConsumed;
+        mustBeCreated;
+      };
+    signature : Signature :=
+      sign@{
+        message;
+        signer;
+      };
+  in case origin of
+       | Created commitment :=
+         toAppDataEntry@{
+           key := commitment;
+           data := message, signature;
+         }
+       | Consumed nullifier :=
+         toAppDataEntry@{
+           key := nullifier;
+           data := message, signature;
+         };
+
+module ActionFromConvertable;
+  import Applib.Resource.Traits.Convertable open;
+  import Applib.Transaction.Traits open;
+
+  --- Instantiates the ;ActionConvertable; trait with a parametrized function accepting `ConsumedTypedResource` and `CreatedTypedResource` being required to implement the ;Ord; and ;Convertable; traits.
+  --- The underlying inmplementation converts the typed resources to standard ;Resource;s and creates an ;Action; with
+  --- - authorization ;AppData; containing an ;AppData; entry for every consumed ;Resource;.
+  --- - custom inputs (;CustomInputs;) containing entries mapping nullifiers to consumed resources and commitments to created resources.
+  actionWithAuthorizationAppData
+    {ConsumedTypedResource CreatedTypedResource}
+    {{Ord ConsumedTypedResource}}
+    {{Ord CreatedTypedResource}}
+    {{Convertable ConsumedTypedResource}}
+    {{Convertable CreatedTypedResource}}
+    : ActionConvertable ConsumedTypedResource CreatedTypedResource :=
+    mkActionConvertable@{
+      toAction
+        (standardInputs : StandardInputs)
+        (consumedResources : Set ConsumedTypedResource)
+        (createdResources : Set CreatedTypedResource)
+        : Action :=
+        let
+          -- Convert typed resources to resources.
+          consumed :=
+            Set.map (r in consumedResources) {
+              Convertable.toResource r
+            };
+          created :=
+            Set.map (r in createdResources) {
+              Convertable.toResource r
+            };
+
+          -- Put maps into the custom inputs that map:
+          -- - nullifiers to consumed resources
+          -- - commitments to created resources
+          tagsAndCustomInputs :=
+            computeTagsAndCustomInputs@{
+              consumed;
+              created;
+            };
+          tags := TagsAndCustomInputs.tags tagsAndCustomInputs;
+          pair := tagsToPair tags;
+          nullifiers := fst pair;
+          commitments := snd pair;
+
+          -- Put signed messages and signatures by the owner in the app data.
+          -- The signed messages link back to the original consumed resources, where the signature verification is part of the resource logic requiring the commitments of created resources to be part of the action.
+          appData :=
+            Set.map (nullifier in nullifiers) {
+                mkResourceRelationshipAppDataEntry@{
+                  signer :=
+                    Identity.internal (StandardInputs.caller standardInputs);
+                  origin := Consumed nullifier;
+                  mustBeConsumed := Set.empty;
+                  mustBeCreated := commitments;
+                }
+              }
+              |> Map.fromSet;
+        in mkActionHelper@{
+             consumed;
+             created;
+             appData;
+             customInputs :=
+               TagsAndCustomInputs.customInputs tagsAndCustomInputs;
+             tags;
+           };
+    };
+end;