feat: add hello world app (#19)

* bug: sync to fix * chore: update deps * feat: HelloWorld Resource Object * chore: update deps * ci: add test and format check workflow * style: format * ci: rename tests * chore: update deps * feat: finish hello world and use latest compiler * fix: wrong import * style: formatting --------- Co-authored-by: Michael Heuer <[email protected]>
anoma · Nov 12, 2024 · c234aa7 · c234aa7
1 parent 597644a
commit c234aa7
Show file tree

Hide file tree

Showing 10 changed files with 260 additions and 63 deletions.
diff --git a/.github/workflows/tests.yaml b/.github/workflows/tests.yaml
@@ -7,8 +7,8 @@ on:
   workflow_dispatch:
 
 jobs:
-  tests:
-    name: Run test suite
+  kudos-tests:
+    name: Kudos
     runs-on: ubuntu-latest
     defaults:
       run:
@@ -19,13 +19,34 @@ jobs:
       - name: Download latest nightly Juvix binary
         uses: jaxxstorm/[email protected]
         with:
-          repo: anoma/juvix-nightly-builds
+          repo: anoma/juvix
+          cache: enable
+      - name: Clean
+        run: juvix clean --global && juvix clean && juvix dependencies update
+      - name: Type Check
+        run: juvix typecheck
+      - name: Format Check
+        run: juvix format
+      #- name: Run Example
+      #  run: juvix eval Example.juvix
+
+  hello-world-tests:
+    name: Hello World
+    runs-on: ubuntu-latest
+    defaults:
+      run:
+        working-directory: HelloWorld
+    steps:
+      - name: checkout code
+        uses: actions/checkout@v3
+      - name: Download latest nightly Juvix binary
+        uses: jaxxstorm/[email protected]
+        with:
+          repo: anoma/juvix
           cache: enable
       - name: Clean
         run: juvix clean --global && juvix clean && juvix dependencies update
       - name: Type Check
         run: juvix typecheck
       - name: Format Check
         run: juvix format
-      - name: Run Example
-        run: juvix eval Example.juvix
diff --git a/.gitignore b/.gitignore
@@ -2,3 +2,6 @@
 .history
 *.nockma
 .DS_Store
+
+
+.vscode
diff --git a/HelloWorld/Interface/Transaction.juvix b/HelloWorld/Interface/Transaction.juvix
@@ -0,0 +1,87 @@
+module Interface.Transaction;
+
+import Stdlib.Prelude open;
+import Stdlib.Data.Set as Set open using {Set};
+import Stdlib.Data.Map as Map open using {Map};
+import Anoma open;
+import Applib open;
+import Resource open;
+
+transferHello
+  (standardInputs : StandardInputs)
+  (existingHello : Resource)
+  (receiver : ExternalIdentity)
+  : Transaction :=
+  let
+    nonce := generateNonce (StandardInputs.randSeed standardInputs);
+  in prepareTransaction@{
+       standardInputs;
+       consumed := Set.singleton existingHello;
+       created :=
+         Set.singleton
+           mkHelloResource@{
+             owner := receiver;
+             nonce;
+           };
+     };
+
+helloWorldIntent
+  (standardInputs : StandardInputs)
+  (existingHello : Resource)
+  (receiver : ExternalIdentity)
+  : Transaction :=
+  prepareTransaction@{
+    standardInputs;
+    consumed := Set.singleton existingHello;
+    created :=
+      Set.singleton
+        mkWorldResource@{
+          owner := Identity.external (StandardInputs.caller standardInputs);
+          nonce := generateNonce (StandardInputs.randSeed standardInputs);
+        };
+  };
+
+prepareTransaction
+  (standardInputs : StandardInputs)
+  (consumed created : Set Resource)
+  : Transaction :=
+  let
+    -- 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 from the caller 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 mkTransactionHelper@{
+       roots := Set.singleton (StandardInputs.currentRoot standardInputs);
+       actions :=
+         Set.singleton
+           mkActionHelper@{
+             consumed;
+             created;
+             tags := TagsAndCustomInputs.tags tagsAndCustomInputs;
+             appData;
+             customInputs :=
+               TagsAndCustomInputs.customInputs tagsAndCustomInputs;
+           };
+     };
diff --git a/HelloWorld/Package.juvix b/HelloWorld/Package.juvix
@@ -0,0 +1,14 @@
+module Package;
+
+import PackageDescription.V2 open;
+
+package : Package :=
+  defaultPackage@?{
+    name := "hello-world";
+    dependencies :=
+      [
+        github "anoma" "juvix-stdlib" "v0.8.0";
+        github "anoma" "juvix-arm-specs" "v2.0.0-transparent-alpha.1";
+        github "anoma" "anoma-app-lib" "v0.6.1";
+      ];
+  };
diff --git a/HelloWorld/Resource.juvix b/HelloWorld/Resource.juvix
@@ -0,0 +1,58 @@
+module Resource;
+
+import Stdlib.Prelude open;
+import Anoma open;
+import Anoma.Builtin.System open;
+import Applib open;
+import Applib.Authorization.Check open public;
+import Applib.Authorization.Check open public;
+import Applib.Authorization.Message open public;
+
+logic (publicInputs : Logic.Instance) (privateInputs : Logic.Witness) : Bool :=
+  let
+    tag := Logic.Instance.tag publicInputs;
+    customInputs := Logic.Witness.customInputs privateInputs;
+  in case tag of
+       | Consumed nullifier :=
+         case lookupResource nullifier customInputs of {
+           | nothing := false
+           | just self :=
+             isAuthorizedBy@{
+               signer := HasOwner.get self;
+               origin := tag;
+               publicInputs;
+             }
+         }
+       | Created commitment := true;
+
+-- You don't need to change anything below this point.
+mkLabelledResource
+  (label : String)
+  (owner : ExternalIdentity)
+  (nonce : Nonce)
+  {ephemeral : Bool := false}
+  : Resource :=
+  mkResource@{
+    logicRef := BindingReference.compute logic;
+    labelRef := BindingReference.compute (mkLabel (anomaEncode label));
+    valueRef := BindingReference.compute (mkValue (anomaEncode owner));
+    quantity := 1;
+    nonce;
+    ephemeral;
+    randSeed := UnusedRandSeed;
+    nullifierKeyCommitment := Universal.nullifierKeyCommitment;
+  };
+
+mkHelloResource (owner : ExternalIdentity) (nonce : Nonce) : Resource :=
+  mkLabelledResource@{
+    label := "Hello";
+    owner;
+    nonce;
+  };
+
+mkWorldResource (owner : ExternalIdentity) (nonce : Nonce) : Resource :=
+  mkLabelledResource@{
+    label := "World";
+    owner;
+    nonce;
+  };
diff --git a/HelloWorld/juvix.lock.yaml b/HelloWorld/juvix.lock.yaml
@@ -0,0 +1,41 @@
+# This file was autogenerated by Juvix version 0.6.8.
+# Do not edit this file manually.
+
+version: 2
+checksum: 7e1503c9e6c5f62bedadd6b6637bc55e25372a26fe9628bbf5f4026fd1ad34a5
+dependencies:
+- git:
+    name: anoma_juvix-stdlib
+    ref: 0080b1183ab55e5180e69bfc3987e4cd6edbc230
+    url: https://github.com/anoma/juvix-stdlib
+  dependencies: []
+- git:
+    name: anoma_juvix-arm-specs
+    ref: dc691b9e17b4b8136296904d433c946f81588157
+    url: https://github.com/anoma/juvix-arm-specs
+  dependencies:
+  - git:
+      name: anoma_juvix-stdlib
+      ref: 0080b1183ab55e5180e69bfc3987e4cd6edbc230
+      url: https://github.com/anoma/juvix-stdlib
+    dependencies: []
+- git:
+    name: anoma_anoma-app-lib
+    ref: a6c4993f203d759051ef4a31c0c6c7fde0a9e9a2
+    url: https://github.com/anoma/anoma-app-lib
+  dependencies:
+  - git:
+      name: anoma_juvix-stdlib
+      ref: 0080b1183ab55e5180e69bfc3987e4cd6edbc230
+      url: https://github.com/anoma/juvix-stdlib
+    dependencies: []
+  - git:
+      name: anoma_juvix-arm-specs
+      ref: dc691b9e17b4b8136296904d433c946f81588157
+      url: https://github.com/anoma/juvix-arm-specs
+    dependencies:
+    - git:
+        name: anoma_juvix-stdlib
+        ref: 0080b1183ab55e5180e69bfc3987e4cd6edbc230
+        url: https://github.com/anoma/juvix-stdlib
+      dependencies: []
diff --git a/Kudos/Example.juvix b/Kudos/Example.juvix
@@ -4,6 +4,7 @@ import Stdlib.Prelude open;
 import Stdlib.Debug.Fail open using {failwith};
 
 import Anoma open;
+import Anoma.Builtin.ByteArray open;
 import Anoma.State.CommitmentTree open;
 
 import Applib open;
@@ -16,8 +17,9 @@ bob : ExternalIdentity := Zero.externalIdentity;
 
 standardInputs : StandardInputs :=
   mkStandardInputs@{
-    identity := alice;
+    caller := alice;
     currentRoot := mkRoot 0;
+    randSeed := mkRandSeed (mkByteArray (replicate 32 0x0));
   };
 
 --- Create 10 Kudo tokens as Alice (the originator) for Bob (the owner).

diff --git a/Kudos/Interface.juvix b/Kudos/Interface.juvix
@@ -1,6 +1,7 @@
 module Interface;
 
 import Stdlib.Prelude open;
+import Stdlib.Data.Set as Set open using {Set};
 
 import Anoma open;
 import Applib open;
@@ -22,9 +23,11 @@ initialize
   (receiver : ExternalIdentity)
   : Result StandardError Transaction :=
   let
-    self := standardInputs |> StandardInputs.identity |> Identity.external;
+    self := Identity.external (StandardInputs.caller standardInputs);
+    nonce := generateNonce (StandardInputs.randSeed standardInputs);
     token :=
       Token.create@{
+        nonce;
         quantity;
         tokenLabel := mkKudoLabel self;
         owner := receiver;
@@ -40,8 +43,7 @@ finalize
   (token : Token)
   : Result StandardError Transaction :=
   let
-    self : ExternalIdentity :=
-      standardInputs |> StandardInputs.identity |> Identity.external;
+    self := Identity.external (StandardInputs.caller standardInputs);
   in case isKudo (self) token of
        | false := throw notKudoError
        | true :=
@@ -57,8 +59,7 @@ send
   (receiver : ExternalIdentity)
   : Result StandardError Transaction :=
   let
-    self : ExternalIdentity :=
-      standardInputs |> StandardInputs.identity |> Identity.external;
+    self := Identity.external (StandardInputs.caller standardInputs);
   in case isKudo self token of
        | false := throw notKudoError
        | true :=
@@ -75,8 +76,7 @@ transfer
   (receiver : ExternalIdentity)
   : Result StandardError Transaction :=
   let
-    self : ExternalIdentity :=
-      standardInputs |> StandardInputs.identity |> Identity.external;
+    self := Identity.external (StandardInputs.caller standardInputs);
   in case isKudo (self) token of
        | false := throw notKudoError
        | true :=
@@ -93,8 +93,7 @@ split
   (quantitiesAndReceivers : List (Pair Quantity ExternalIdentity))
   : Result StandardError Transaction :=
   let
-    self : ExternalIdentity :=
-      standardInputs |> StandardInputs.identity |> Identity.external;
+    self := Identity.external (StandardInputs.caller standardInputs);
   in case isKudo self token of
        | false := throw notKudoError
        | true :=
@@ -110,7 +109,7 @@ merge
   (receiver : ExternalIdentity)
   : Result StandardError Transaction :=
   let
-    self := standardInputs |> StandardInputs.identity |> Identity.external;
+    self := Identity.external (StandardInputs.caller standardInputs);
   in case
        all (t in tokens) {
          isKudo self t
@@ -126,14 +125,15 @@ merge
 
 swap
   (standardInputs : StandardInputs)
-  (toSwap : List Token)
+  (toSwap : Set Token)
   (want : Asset.QuantifiedAssets)
   (solver : ExternalIdentity)
   : Result StandardError Transaction :=
   let
-    self := standardInputs |> StandardInputs.identity |> Identity.external;
+    self := Identity.external (StandardInputs.caller standardInputs);
+    nonce := generateNonce (StandardInputs.randSeed standardInputs);
   in case
-       all (t in toSwap) {
+       all (t in Set.toList toSwap) {
          isKudo self t
        }
      of
@@ -144,6 +144,7 @@ swap
            toSwap;
            intent :=
              Swap.SwapIntent.create@{
+               nonce;
                want;
                receiver := self;
                solver;
@@ -152,8 +153,8 @@ swap
 
 settle
   (standardInputs : StandardInputs)
-  (transactions : List Transaction)
-  (solutions : List Swap.Solution)
+  (transactions : Set Transaction)
+  (solutions : Set Swap.Solution)
   : Result StandardError Transaction :=
   Transaction.settle@{
     standardInputs;