Initial commit

.devcontainer/Dockerfile

@@ -0,0 +1,29 @@
+# OS
+ARG VARIANT="ubuntu-22.04"
+
+FROM mcr.microsoft.com/vscode/devcontainers/base:0-${VARIANT}
+ENV DEBIAN_FRONTEND=noninteractive
+
+RUN apt-get update && \
+    apt-get -y install --no-install-recommends \
+    curl \
+    sudo \
+    wget \
+    git \
+    && apt-get clean
+
+ENV PATH=${PATH}:/home/vscode/.local/bin
+RUN sudo bash -c 'mkdir -p /home/vscode/.local/bin'
+RUN sudo bash -c "chown -R vscode /home/vscode/.local/"
+RUN sudo bash -c 'chmod -R a+rXw /home/vscode/.local'
+
+# to be used by the juvix extension
+RUN sudo bash -c 'mkdir -p /home/vscode/.local/juvix'
+
+RUN sudo bash -c 'curl -s https://api.github.com/repos/anoma/juvix/releases/tags/v0.6.8 \
+       | grep -a "browser_download_url.*linux" \
+       | cut -d : -f 2,3 \
+       | tr -d \" \
+       | head -n 1 \
+       | wget --output-document juvix.tar.gz -qi - \
+      && tar xfv juvix.tar.gz --directory=/home/vscode/.local/bin/'

.devcontainer/devcontainer.json

@@ -0,0 +1,33 @@
+{
+  "name": "Ubuntu",
+  "build": {
+    "dockerfile": "Dockerfile",
+    "args": {
+      "USERNAME": "vscode",
+      "VARIANT": "ubuntu-22.04"
+    }
+  },
+  "customizations": {
+    "vscode": {
+      "settings": {
+        "workbench.colorTheme": "Default Dark+",
+        "editor.formatOnSave": false,
+        "editor.tabSize": 2,
+        "editor.renderWhitespace": "trailing",
+        "files.trimTrailingWhitespace": true,
+        "extensions.ignoreRecommendations": true,
+        "terminal.integrated.confirmOnKill": "never",
+        "juvix-mode.opts": {
+          "internalBuildDir": "/workspaces/applications-workshop/.juvix-build"
+        },
+        "juvix-mode.juvixBinPath": "/home/vscode/.local/bin/",
+        "juvix-mode.juvixBinName": "juvix",
+        "juvix-mode.input.languages": ["Juvix", "JuvixCore"],
+        "juvix-mode.reloadReplOnSave": true,
+        "juvix-mode.typecheckOn": "none"
+      },
+      "extensions": ["Heliax.juvix-mode"]
+    }
+  },
+  "remoteUser": "vscode"
+}

.github/workflows/tests.yaml

@@ -0,0 +1,29 @@
+name: Test anoma-applib
+
+on:
+  push:
+    branches: [ main ]
+  pull_request:
+  workflow_dispatch:
+
+jobs:
+  test:
+    name: Run test suite
+    runs-on: ubuntu-latest
+    defaults:
+      run:
+        working-directory: HelloWorld
+    steps:
+      - name: checkout code
+        uses: actions/checkout@v3
+      - name: Download the Juvix binary
+        uses: jaxxstorm/[email protected]
+        with:
+          repo: anoma/juvix
+          cache: enable
+      - name: Clean
+        run: juvix clean --global && juvix dependencies update 
+      - name: Type Check
+        run: juvix typecheck
+      - name: Format Check
+        run: juvix format

.gitignore

@@ -0,0 +1,5 @@
+.juvix-build
+.history
+*.nockma
+.DS_Store
+.vscode

.prettierignore

@@ -0,0 +1,5 @@
+# directories
+.juvix-build
+
+# files
+.DS_Store

.prettierrc

@@ -0,0 +1,4 @@
+{
+  "tabWidth": 2,
+  "singleQuote": true
+}

HelloWorld/Exercise_1/README.md

@@ -0,0 +1,3 @@
+# Exercise 1
+
+Write your first resource constructor.

HelloWorld/Exercise_1/Resource.juvix

@@ -0,0 +1,30 @@
+module Exercise_1.Resource;
+
+import Anoma open;
+import Applib open;
+import WorkshopUtils open;
+
+--- A dummy logic function that always returns true.
+logic (publicInputs : Logic.Instance) (privateInputs : Logic.Witness) : Bool :=
+  true;
+
+--- A label containing the string "Hello world!".
+labelRef : LabelRef := toLabelRef "Hello world!";
+
+{-
+  TODO: Write the constructor of your Hello World resource.
+  You can use the definitions from above.
+  Check for errors with `juvix typecheck Exercise_1/Resource.juvix`
+-}
+mkLabelledResource (owner : ExternalIdentity) (nonce : Nonce) : Resource :=
+  mkResource@{
+    labelRef := TODO;
+    logicRef := TODO;
+    valueRef := TODO;
+    quantity := TODO;
+    nonce;
+    -- NOTE: In this workshop, we don't bother about the fields below.
+    ephemeral := false;
+    randSeed := UnusedRandSeed;
+    nullifierKeyCommitment := Universal.nullifierKeyCommitment;
+  };

HelloWorld/Exercise_2/Resource.juvix

@@ -0,0 +1,39 @@
+module Exercise_2.Resource;
+
+import Anoma open;
+import Applib open;
+import WorkshopUtils open;
+
+{-
+  TODO: Write a logic function checkiong that the consumption of the resource was authorized by the owner.
+  As a bonus, ensure that the quantity is 1.
+-}
+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 := TODO;
+               origin := TODO;
+               publicInputs;
+             }
+         }
+       | Created commitment := true;
+
+mkHelloWorldResource (owner : ExternalIdentity) (nonce : Nonce) : Resource :=
+  mkResource@{
+    labelRef := toLabelRef "Hello world!";
+    logicRef := toLogicRef logic;
+    valueRef := toValueRef owner;
+    quantity := 1;
+    -- NOTE: In this workshop, we don't bother about the fields below.
+    ephemeral := false;
+    nonce;
+    randSeed := UnusedRandSeed;
+    nullifierKeyCommitment := Universal.nullifierKeyCommitment;
+  };

HelloWorld/Exercise_3/Resource.juvix

@@ -0,0 +1,37 @@
+module Exercise_3.Resource;
+
+import Anoma open;
+import Applib open;
+import WorkshopUtils open;
+
+-- NOTE: You don't need to change anything in this file.
+
+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 := fromValueRef self;
+               origin := tag;
+               publicInputs;
+             }
+               && Resource.quantity self == 1
+         }
+       | Created commitment := true;
+
+mkHelloWorldResource (owner : ExternalIdentity) (nonce : Nonce) : Resource :=
+  mkResource@{
+    labelRef := toLabelRef "Hello world!";
+    logicRef := toLogicRef logic;
+    valueRef := toValueRef owner;
+    quantity := 1;
+    ephemeral := false;
+    nonce;
+    randSeed := UnusedRandSeed;
+    nullifierKeyCommitment := Universal.nullifierKeyCommitment;
+  };

HelloWorld/Exercise_3/Transaction.juvix

@@ -0,0 +1,20 @@
+module Exercise_3.Transaction;
+
+import Anoma open;
+import Applib open;
+import WorkshopUtils open;
+import Exercise_3.Resource open;
+
+-- TODO
+transferHelloWorld
+  (standardInputs : StandardInputs)
+  (existingHello : Resource)
+  (receiver : ExternalIdentity)
+  : Transaction :=
+  let
+    nonce := generateNonce (StandardInputs.randSeed standardInputs);
+  in prepareTransaction@{
+       standardInputs;
+       consumed := Set.singleton existingHello;
+       created := TODO;
+     };

HelloWorld/Intent/Resource.juvix

@@ -0,0 +1,54 @@
+module Intent.Resource;
+
+import Anoma open;
+import Applib open;
+import WorkshopUtils open;
+
+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 := fromValueRef 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 := toLogicRef logic;
+    labelRef := toLabelRef label;
+    valueRef := toValueRef 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;
+  };

HelloWorld/Intent/Transaction.juvix

@@ -0,0 +1,40 @@
+module Intent.Transaction;
+
+import Anoma open;
+import Applib open;
+import WorkshopUtils open;
+import Intent.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);
+        };
+  };

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";
+      ];
+  };