diff --git a/.assets/account-model.png b/.assets/account-model.png new file mode 100644 index 0000000..5625083 Binary files /dev/null and b/.assets/account-model.png differ diff --git a/.assets/anoma-logo.png b/.assets/anoma-logo.png new file mode 100644 index 0000000..9042402 Binary files /dev/null and b/.assets/anoma-logo.png differ diff --git a/.assets/resource-model.png b/.assets/resource-model.png new file mode 100644 index 0000000..1d076b1 Binary files /dev/null and b/.assets/resource-model.png differ diff --git a/.assets/state.png b/.assets/state.png new file mode 100644 index 0000000..2d8211c Binary files /dev/null and b/.assets/state.png differ diff --git a/.assets/tara-smiling.png b/.assets/tara-smiling.png new file mode 100644 index 0000000..a37360a Binary files /dev/null and b/.assets/tara-smiling.png differ diff --git a/.assets/utxo-model.png b/.assets/utxo-model.png new file mode 100644 index 0000000..01094e8 Binary files /dev/null and b/.assets/utxo-model.png differ diff --git a/.devcontainer/Dockerfile b/.devcontainer/Dockerfile new file mode 100644 index 0000000..63a553d --- /dev/null +++ b/.devcontainer/Dockerfile @@ -0,0 +1,53 @@ +# 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 \ + make \ + cmake \ + clang \ + lldb \ + lld \ + llvm \ + rsync \ + build-essential \ + lsb-release \ + pkg-config \ + software-properties-common \ + autoconf && 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' + +RUN sudo bash -c 'curl https://get.wasmer.io -sSfL | sudo WASMER_DIR=/home/vscode/.local sh' + +# 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/' + +RUN sudo bash -c 'mkdir -p /home/vscode/.local/wasi-sysroot' +RUN sudo bash -c 'curl -s https://api.github.com/repos/WebAssembly/wasi-sdk/releases/tags/wasi-sdk-16 \ + | grep -a "browser_download_url.*wasi-sysroot-16.*tar.gz" \ + | cut -d : -f 2,3 \ + | tr -d \" \ + | wget --output-document wasi-sysroot.tar.gz -qi - \ + && tar xvf wasi-sysroot.tar.gz --directory /home/vscode/.local/wasi-sysroot/' +ENV WASI_SYSROOT_PATH=/home/vscode/.local/wasi-sysroot/ + + diff --git a/.devcontainer/devcontainer.json b/.devcontainer/devcontainer.json new file mode 100644 index 0000000..9e97fdb --- /dev/null +++ b/.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" +} diff --git a/.github/workflows/tests.yaml b/.github/workflows/tests.yaml new file mode 100644 index 0000000..07438cd --- /dev/null +++ b/.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/action-install-gh-release@v1.10.0 + 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 diff --git a/.gitignore b/.gitignore new file mode 100644 index 0000000..192480b --- /dev/null +++ b/.gitignore @@ -0,0 +1,5 @@ +.juvix-build +.history +*.nockma +.DS_Store +.vscode \ No newline at end of file diff --git a/.prettierignore b/.prettierignore new file mode 100644 index 0000000..95ebbe8 --- /dev/null +++ b/.prettierignore @@ -0,0 +1,5 @@ +# directories +.juvix-build + +# files +.DS_Store diff --git a/.prettierrc b/.prettierrc new file mode 100644 index 0000000..1fb73bc --- /dev/null +++ b/.prettierrc @@ -0,0 +1,4 @@ +{ + "tabWidth": 2, + "singleQuote": true +} diff --git a/HelloWorld/Exercise_1/Resource.juvix b/HelloWorld/Exercise_1/Resource.juvix new file mode 100644 index 0000000..27dffbc --- /dev/null +++ b/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; + }; diff --git a/HelloWorld/Exercise_2/Resource.juvix b/HelloWorld/Exercise_2/Resource.juvix new file mode 100644 index 0000000..7644c45 --- /dev/null +++ b/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 checking 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; + }; diff --git a/HelloWorld/Exercise_3/Resource.juvix b/HelloWorld/Exercise_3/Resource.juvix new file mode 100644 index 0000000..f485a10 --- /dev/null +++ b/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; + }; diff --git a/HelloWorld/Exercise_3/Transaction.juvix b/HelloWorld/Exercise_3/Transaction.juvix new file mode 100644 index 0000000..d0b8629 --- /dev/null +++ b/HelloWorld/Exercise_3/Transaction.juvix @@ -0,0 +1,22 @@ +module Exercise_3.Transaction; + +import Anoma open; +import Applib open; +import WorkshopUtils open; +import Exercise_3.Resource open; + +{- + TODO: Write a function that transfers the `existingHelloWorld` resource to the `receiver`. +-} +transferHelloWorld + (standardInputs : StandardInputs) + (existingHelloWorld : Resource) + (receiver : ExternalIdentity) + : Transaction := + let + nonce := generateNonce (StandardInputs.randSeed standardInputs); + in prepareTransaction@{ + standardInputs; + consumed := TODO; + created := TODO; + }; diff --git a/HelloWorld/Intent/Resource.juvix b/HelloWorld/Intent/Resource.juvix new file mode 100644 index 0000000..461a1a9 --- /dev/null +++ b/HelloWorld/Intent/Resource.juvix @@ -0,0 +1,56 @@ +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; + +--- Constructs a resource with a specified label. +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; + }; + +--- Constructs a resource with the label "Hello". +mkHelloResource (owner : ExternalIdentity) (nonce : Nonce) : Resource := + mkLabelledResource@{ + label := "Hello"; + owner; + nonce; + }; + +--- Constructs a resource with the label "World". +mkWorldResource (owner : ExternalIdentity) (nonce : Nonce) : Resource := + mkLabelledResource@{ + label := "World"; + owner; + nonce; + }; diff --git a/HelloWorld/Intent/Transaction.juvix b/HelloWorld/Intent/Transaction.juvix new file mode 100644 index 0000000..8a65171 --- /dev/null +++ b/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); + }; + }; diff --git a/HelloWorld/Package.juvix b/HelloWorld/Package.juvix new file mode 100644 index 0000000..5145faf --- /dev/null +++ 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/WorkshopUtils.juvix b/HelloWorld/WorkshopUtils.juvix new file mode 100644 index 0000000..2138b5f --- /dev/null +++ b/HelloWorld/WorkshopUtils.juvix @@ -0,0 +1,85 @@ +module WorkshopUtils; + +import Stdlib.Prelude open public; +import Stdlib.Data.Set as Set public; + +open Set using {Set} public; + +import Stdlib.Data.Map as Map public; +import Anoma open; +import Anoma.Builtin.System open public; +import Applib open; +import Applib.Authorization.Check open public; +import Applib.Authorization.Message open public; + +axiom TODO : {A : Type} -> A; + +toLabelRef {T} (data : T) : LabelRef := + BindingReference.compute (mkLabel (anomaEncode data)); + +fromLabelRef {T} (resource : Resource) : T := + resource + |> Resource.labelRef + |> lookupFromReferenceChecked + |> Label.unLabel + |> anomaDecode; + +toValueRef {T} (data : T) : ValueRef := + BindingReference.compute (mkValue (anomaEncode data)); + +fromValueRef {T} (resource : Resource) : T := + resource + |> Resource.valueRef + |> lookupFromReferenceChecked + |> Value.unValue + |> anomaDecode; + +toLogicRef (func : Logic) : LogicRef := BindingReference.compute (func); + +fromLogicRef (resource : Resource) : Logic := + resource |> Resource.logicRef |> lookupFromReferenceChecked; + +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/juvix.lock.yaml b/HelloWorld/juvix.lock.yaml new file mode 100644 index 0000000..18081ba --- /dev/null +++ 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/Material/1_Learn-Anoma-Apps.md b/Material/1_Learn-Anoma-Apps.md new file mode 100644 index 0000000..1f3aeae --- /dev/null +++ b/Material/1_Learn-Anoma-Apps.md @@ -0,0 +1,247 @@ +# Anoma Applications Primer + +Anoma is a distributed operating system for intent-centric applications. + +In the beginning, we introduce some of Anoma's mechanisms with a focus on app development. + +- [Anoma's State Model](#anomas-state-model) +- [Resources](#resources) +- [Transactions](#transactions) +- [Anoma Resource Machine](#anoma-resource-machine) + - [Concepts](#concepts) + - [Valididty](#validity) +- [Applications](#applications) + +## Anoma's State Model + +Anoma organizes state in a resource model. + +

+schematic depiction of state as resources +

+

+ +Credit to Yulia Khalniyazova for all graphics in this document. + +

+ +
Comparison to other State Models + +Comparing the resource model to other state models, the advantages become clear. + +#### Account Model + +

+schematic depiction of the account model +

+ +- State is explict and global +- Example: An Ethereum smart contract containing value (e.g., `uint256 count`) or a account balance mapping (`mapping(address => uint256) balanceOf`). +- An application must be deployed to each chain specifically. +- Cross-chain apps require sophisticated bridging and code changes. + +#### UTXO Model + +

+schematic depiction of the UTXO model +

+ +- State is implicit and comprised of all unspent transaction outputs (UTXOs) +- Examples: Bitcoin or Zcash transactions +- The predicate determining if it is allowed to spent an UTXO is always the same +- Arbitrary applications are difficult/not possible + +#### Resource Model + +

+schematic depiction of the resource model +

+ +- State is implicit and comprised of all unspent resources +- Predicates and data attached to resources can be arbitrary +- Arbitrary applications and general intents are enabled + +
+ +### Affordances + +This enables[^cwgoes] + +[^cwgoes]: https://ethresear.ch/t/rfc-draft-anoma-as-the-universal-intent-machine-for-ethereum/19109. + +- Heterogeneous trust + - Resources can live on different controllers (e.g., L1's, L2's, three friends in a LAN). + - A transaction can consume a resource on controller A and create it on controller B. +- Information flow control + - Transactions can be sent transparent, shielded, or private just by setting a flag +- Intent-level Composability + - Intents (unbalanced transactions) can be composed and settled across different applications and chains + +## Resources + +**Resources** are atomic units of application state and logic. They have + +- a quantity, label, and specific kind +- data (e.g, owner, diameter, etc.) + | 5 🐚 `{diameter : 1.4}` | 2 🍏 `{fruitiness : 8 / 10}` | 1 💌 `{text : "I ❤️ u"}` | + |:--------------------------------:|:-----------------------------:|:---------------------------------:| + | `5 Shell` resource | `2 GreenApple` resource | `1 Message` Resource | +- a lifecycle with three stages, + ```mermaid + flowchart LR + Non-existent --> Created --> Consumed + ``` +- a logic function enforcing predicates (that check data, e.g., in itself, the transaction or other resources) + +
The Resource object in detail + +```haskell +type Resource := + mkResource@{ + logic : LogicRef; + label : LabelRef; + value : ValueRef; + quantity : Quantity; + ephemeral : Bool; + nonce : Nonce; + randSeed : RandSeed; + nullifierKeyCommitment : NullifierKeyCommitment; + }; +``` + +- **`logic`:** A boolean-valued function enforcing predicates required to create and consume the resource. +- **`label`:** Arbitrary data describing the resource and determining its kind (e.g., the name or symbol). +- **`value`:** Arbitrary data associated with the resource (e.g., the owner). +- **`quantity`:** The number of units that this resource describes. +- **`ephemeral`** A boolean expressing whether this resource is ephemeral or not, i.e., exists only during a transaction. +- **`nonce`:** A number ensuring the uniqueness of the resource. +- **`randSeed:`** A number to derive (pseudo)-randomness from. +- **`nullifierKeyCommitment`** A commitment to a secret nullfier key. + +*Types named `*Ref` are binding references to objects in BLOB storage. + +
+

+ +**Creation:** To create a resource its _commitment_ must be computed by hashing the resource object. +$$\texttt{commitment} := h_\texttt{cm}(\texttt{resource})$$ +After execution, the commitment is added to a Merkle tree. + +**Consumption:** To consume a resource its _nullifier_ must be computed by hashing the resource object and a secret called the _nullifier key_. +$$\texttt{nullifier} := h_\texttt{nf}(\texttt{resource},\,\texttt{nullifierKey})$$ +After execution, the nullifier is added into a nullifier set. + +**Kind:** The _kind_ of a resource determines its fungibility and is computed as the hash of its _logic_ and _label_. +$$\texttt{kind} := h_\texttt{kind}(\texttt{logic},\,\texttt{label})$$ +The kind is used to check if transactions are balanced. + +## Transactions + +**Transactions** consume and create resources. + +- Transactions with equal quantities of created and consumed resources of the same kind are **balanced**. +- If all resource logics are + +- An unbalanced transaction is called **intent**. +- Only balanced and transactions can be executed + + | Consumed | Created | Balanced? ✅/❌ | + | :-------------------: | :-------------------: | :-------------: | + | 2🍏 | 2🍏 | | + | 2🍏 | 1🍏 + 1🍏 | | + | 2🍏 + 1🐚 | 1🍏 + 2🐚 | | + | 2🍏 + 1🐚 | 1🍏 + 1🍎 + 1🐚 | | + | 1🍏 + 2🍎 + 2🍎 + 3🐚 | 1🍏 + 4🍎 + 1🐚 + 2🐚 | | + +- contain **actions** for context separation. + +
The Transaction object + +```haskell +type Transaction := + mkTransaction@{ + actions : Set Action; + roots : Set CommitmentTree.Root; + delta : Delta; + deltaProof : Delta.Proof; + }; + +- **`actions`:** Contains +- **`roots`:** Computed for each consumed resource. +- **`delta`:** Computed for each consumed resource. +- **`deltaProof`:** Computed for each consumed resource. + +type Action := + mkAction@{ + commitments : Set Commitment; + nullifiers : Set Nullifier; + proofs : Set Proofs; + appData : AppData; + }; +``` + +- **`commitments`:** Computed for each created resource. +- **`nullifiers`:** Computed for each consumed resource. +- **`proof`:** Logic and compliance proofs +- **`appData`:** A mapping containing arbitrary, application-specific data. +
+ +## Anoma Resource Machine + +The [**Anoma Resource Machine** (ARM)](#resource-machine) is a virtual machine being part of the Anoma Protocol and checks if transactions are adhering to its rules and are therefore [valid](#validity). + +### Validity + +1. **Balance check:** The number of consumed and created resources of the same kind must balance in a transaction. +2. **Resource Logic Checks:** For each resource in the transaction, the corresponding resource logic function must return `true`. +3. **Compliance Checks:** Ensures the RM rules are met. + - Created resources + - Commitments can not exist already. + - Consumed resources + - Commitment must exist already + - Nullifier can not exist + - Ephemeral resources (created and consumed) + - existence checks are skipped + +## Applications + +Applications consist of application state and logic. + +- State is modelled as resources and the data they contain +- Logic is modelled as resource logic functions expressing the predicates required for a resource to be created and consumed + +Accordingly, resources and corresponding **resource logic functions** constitute the **application backend**. + +Instead of creating and consuming resources and providing all data required in the transaction object directly and manually, users interact with an **application interface**. + +
Interface details + +The interface consists of + +- Projection functions (the application **read interface**) + - Outputs meaningful data projected from the state + - Example: The total quantity of resources of specific kind owned by an identity +- Transaction function (the application **write interface**) + - Outputs a transaction object + - Example: Transfer of a resource to a new owner. + + +```mermaid +flowchart TB + subgraph Application + direction BT + subgraph Interface + direction LR + tf("Projection functions") --> pf("Transaction functions") + end + subgraph Backend + direction BT + rlf("Logic functions") + end + end + human(("Human")) --> Application --> machine(("Machine")) + Backend --"read"--> Interface + Interface --"write"--> Backend +``` + +
diff --git a/Material/2_Install-Juvix.md b/Material/2_Install-Juvix.md new file mode 100644 index 0000000..251f6dd --- /dev/null +++ b/Material/2_Install-Juvix.md @@ -0,0 +1,84 @@ +

+tara mascot smiling +

+

Install Juvix

+ +Welcome to Juvix, a language for intent-centric and declarative decentralized apps! + +## Table of Contents + +- [Installing Juvix](#installing-juvix) +- [IDE Setup](#ide-setup) + - [VSCode](#vscode) + - [Emacs](#emacs) +- [Juvix Documentation](#juvix-documentation) + +## Installing Juvix + +Please use one of the following options to install the Juvix compiler. Juvix is supported on + +- Linux `x86_64` +- macOS `x86_64` or `aarch64 (M1/M2)` + +### Prerequisites + +The Juvix compiler requires [the LLVM/clang compiler](https://llvm.org) to be available on your system PATH in order to build native binaries. + +### macOS homebrew + +If you use the [Homebrew package manager](https://brew.sh) you can use our tap: + +```shell +brew update +brew tap anoma/juvix +brew install juvix +``` + +### Linux / macOS automatic installer + +To install for linux or macOS run the following in a terminal (as a non-root user): + +```shell +curl --proto '=https' --tlsv1.2 -sSfL https://get.juvix.org | sh +``` + +### Manual installation + +There are also binaries for the Juvix compiler available to download + +| OS / Architecture | +| ----------------------------------------------------------------------------------------------------------- | +| [Linux x86_64](https://github.com/anoma/juvix/releases/latest/download/juvix-linux-x86_64.tar.gz) | +| [macOS x86_64](https://github.com/anoma/juvix/releases/latest/download/juvix-macos-x86_64.tar.gz) | +| [macOS aarch64 (M1/M2)](https://github.com/anoma/juvix/releases/latest/download/juvix-macos-aarch64.tar.gz) | + +## IDE Setup + +### Visual Studio Code + +First install visual studio code from the Microsoft website https://code.visualstudio.com/download + +In the extension tab search for `juvix` and install the extension that features the Tara logo. + +See the [vscode-juvix repository](https://github.com/anoma/vscode-juvix) for usage information. + +### Emacs + +To get started, clone the [juvix-mode repository](https://github.com/anoma/juvix-mode.git) + +```shell +git clone https://github.com/anoma/juvix-mode.git +``` + +And add the following lines to your Emacs configuration file: + +```emacs-lisp +(push "/path/to/juvix-mode/" load-path) +(require 'juvix-mode) +``` + +See the [juvix-mode repository](https://github.com/anoma/juvix-mode.git) for usage information. + +## Juvix Documentation + +The full documentation for Juvix is available at https://docs.juvix.org diff --git a/Material/3_Write-Applications.md b/Material/3_Write-Applications.md new file mode 100644 index 0000000..09dd315 --- /dev/null +++ b/Material/3_Write-Applications.md @@ -0,0 +1,60 @@ +# Write & Explore Applications + +## Write your first Application + +If you [installed Juvix](./2_Install-Juvix.md) on you machine, clone this repo + +```sh +git clone https://github.com/anoma/applications-workshop.git +``` + +and open it in your preferred IDE. + +Alternatively, you can use our GitHub Codespace by clicking + +[![Open in GitHub Codespaces](https://github.com/codespaces/badge.svg)](https://codespaces.new/anoma/applications-workshop?quickstart=1) + +or go to [github.com/anoma/applications-workshop](https://github.com/anoma/applications-workshop). + +Go through the folders `Excercise_X` and find the assignments as comments inside the `.juvix` files. + +| Command | Description | +| :-------------------------- | :-------------------------------------------------------------------- | +| `juvix clean --global` | Delete your juvix dependencies | +| `juvix clean` | Delete build artifacts | +| `juvix dependencies update` | Fetch & update the dependencies specified in the `Package.juvix` file | +| `juvix typecheck` | Check your app for type errors. | +| `juvix format --in-place` | Format your files | + +Do it all at once with + +```sh +juvix clean --global && juvix clean && juvix dependencies update && juvix typecheck && juvix format --in-place +``` + +## Explore the Kudos Token + +Kudos is an accounting primitive for Anoma. Kudos intents can embody trust relationships between identities. + +### Feature Set + +- Identifiers (name, symbol, decimals) +- Originator + - Can initially create new quantities of this kind/ +- Supply + - Fixed: The total quantity of resources of this kind is fixed. Resources can still be split and merged. + - Capped: Upper bound on the total quantity. Originator cannot create more than this limit. Owners can burn tokens, + - Unbound: Originator can inflate the supply. +- Transferability + - Transferable: Your normal token (ERC-20, NFT) + - Non-transferable: Soulbound token (SBT) +- Interface + - mint, burn, transfer, split, merge (no counterparty required) + - swap intent (counterparty required) + +### `Token` Implementation + +- Resource Label: [1](https://github.com/anoma/anoma-applib/blob/a6c4993f203d759051ef4a31c0c6c7fde0a9e9a2/Applib/Token/Label.juvix#L8-L16),[2](../HelloWorld/.juvix-build/0.6.8/deps/c4c0b1e74196bd1135c8ea27b48f6756d7ec7aa8f5388511e02d6401d1f1c407/Applib/Token/Label.juvix) +- Resource Logic Function: [1](https://github.com/anoma/anoma-applib/blob/a6c4993f203d759051ef4a31c0c6c7fde0a9e9a2/Applib/Token/Logic.juvix#L13-L23),[2](../HelloWorld/.juvix-build/0.6.8/deps/c4c0b1e74196bd1135c8ea27b48f6756d7ec7aa8f5388511e02d6401d1f1c407/Applib/Token/Logic.juvix) +- Transaction functions (write interface): [1](https://github.com/anoma/anoma-applib/blob/a6c4993f203d759051ef4a31c0c6c7fde0a9e9a2/Applib/Transaction),[2](../HelloWorld/.juvix-build/0.6.8/deps/c4c0b1e74196bd1135c8ea27b48f6756d7ec7aa8f5388511e02d6401d1f1c407/Applib/Transaction) +- Projection functions (read interface): [1](https://github.com/anoma/anoma-applib/blob/a6c4993f203d759051ef4a31c0c6c7fde0a9e9a2/Applib/Projection/TotalQuantity.juvix#L9-L12),[2](../HelloWorld/.juvix-build/0.6.8/deps/c4c0b1e74196bd1135c8ea27b48f6756d7ec7aa8f5388511e02d6401d1f1c407/Applib/Projection/TotalQuantity.juvix) diff --git a/README.md b/README.md new file mode 100644 index 0000000..57ff13e --- /dev/null +++ b/README.md @@ -0,0 +1,14 @@ +

+anoma logo +

+

Applications Workshop

+ +Welcome to the Anoma Applications Workshop! + +[![Open in GitHub Codespaces](https://github.com/codespaces/badge.svg)](https://codespaces.new/anoma/applications-workshop?quickstart=1) + +In this workshop we will + +1. [Learn](./Material/1_Learn-Anoma-Apps.md) about [Anoma](https://anoma.net/) and intent-centric apps. +2. [Install](./Material/2_Install-Juvix.md) the [Juvix](https://juvix.org/) language (**optional**), a language for intent-centric and declarative decentralized apps. +3. [Write](./Material/3_Write-Applications.md#write-your-first-application) & [explore](./Material/3_Write-Applications.md#explore-the-kudos-tokens) Anoma apps.