diff --git a/.gitbook/assets/account-model.png b/.gitbook/assets/account-model.png new file mode 100644 index 0000000..5625083 Binary files /dev/null and b/.gitbook/assets/account-model.png differ diff --git a/.gitbook/assets/image (1).png b/.gitbook/assets/image (1).png new file mode 100644 index 0000000..e69de29 diff --git a/.gitbook/assets/image.png b/.gitbook/assets/image.png new file mode 100644 index 0000000..e69de29 diff --git a/.gitbook/assets/resource-model.png b/.gitbook/assets/resource-model.png new file mode 100644 index 0000000..1d076b1 Binary files /dev/null and b/.gitbook/assets/resource-model.png differ diff --git a/.gitbook/assets/state.png b/.gitbook/assets/state.png new file mode 100644 index 0000000..2d8211c Binary files /dev/null and b/.gitbook/assets/state.png differ diff --git a/.gitbook/assets/utxo-model.png b/.gitbook/assets/utxo-model.png new file mode 100644 index 0000000..01094e8 Binary files /dev/null and b/.gitbook/assets/utxo-model.png differ diff --git a/README.md b/README.md index fb17993..0350da2 100644 --- a/README.md +++ b/README.md @@ -1,7 +1,8 @@ --- icon: hand-wave +description: Welcome to the Anoma Developer Documentation! --- -# Anoma Overview +# Overview -Welcome to the Anoma Developer Documentation! +This documentation offers both practical and theoretical insights into Anoma. You can start with hands-on programming guides but also dive deeper into concepts that illustrate the necessary understanding for what's powering the Anoma protocol. diff --git a/SUMMARY.md b/SUMMARY.md index 969f0da..64acf58 100644 --- a/SUMMARY.md +++ b/SUMMARY.md @@ -1,10 +1,24 @@ # Table of contents -* [Anoma Overview](README.md) +* [Overview](README.md) + +## Build + +* [Getting Started](build/getting-started/README.md) + * [Install Juvix](build/getting-started/install-juvix.md) +* [Your First Anoma Application](build/your-first-anoma-application/README.md) + * [Write a Juvix Project](build/your-first-anoma-application/write-a-juvix-project.md) + * [Configure a Juvix Package](build/your-first-anoma-application/configure-a-juvix-package.md) +* [Anoma App Examples](build/anoma-app-examples/README.md) + * [SimpleCounter](build/anoma-app-examples/simplecounter.md) +* [Installation Steps](build/installation-steps.md) ## LEARN -* [Test](docs/test.juvix.md) +* [What is Anoma?](docs/test.juvix.md) +* [Page](learn/page.md) +* [Anoma's State Model](learn/anomas-state-model.md) +* [Resources](learn/resources.md) ## Advanced diff --git a/build/anoma-app-examples/README.md b/build/anoma-app-examples/README.md new file mode 100644 index 0000000..bb26498 --- /dev/null +++ b/build/anoma-app-examples/README.md @@ -0,0 +1,10 @@ +--- +icon: vial +--- + +# Anoma App Examples + +{% content-ref url="simplecounter.md" %} +[simplecounter.md](simplecounter.md) +{% endcontent-ref %} + diff --git a/build/anoma-app-examples/simplecounter.md b/build/anoma-app-examples/simplecounter.md new file mode 100644 index 0000000..3a3ae2e --- /dev/null +++ b/build/anoma-app-examples/simplecounter.md @@ -0,0 +1,351 @@ +--- +description: Learn how to build the SimpleCounter example application. +--- + +# SimpleCounter + +## Goal of this example + +The following outlines the basics of the SimpleCounter example application. The focus of this example is to highlight how resources can work with specific values and how additional functionality can access those resource values. + +## Prerequisites + +Before creating the SimpleCounter application, make sure to have [Juvix installed](../getting-started/install-juvix.md). Also consider looking at [Your First Anoma dApp](../your-first-anoma-application/) for some introductory explanations. + +## Let's write some SimpleCounter code + +#### Project setup + +Let's fly through the project setup by typing the following in our console / terminal. If you already have a project directory, you can skip ahead and just use `juvix init`. + +```bash +mkdir SimpleCounter +cd SimpleCounter +juvix init +# (1) Type 'simple-counter' for the project name +# (2) Press 'Enter' to choose the default version number +``` + +This allows us to get started with the first building block of our counter. + +#### SimpleCounter Resource + +We first build the Resource Object (link to Resource learn section) as it is at the very core of our Anoma dApp. We will continue in five steps - we begin with the Resource Object function, then the Logic, followed by Label, then Value, and lastly we're tying it back together in the Resource Object. + +{% stepper %} +{% step %} +### Building the Resource Object + +We start from the terminal and create a new `Resource` Juvix file. + +```bash +touch Resource.juvix +``` + +We start by sketching out the Resource Object function which we call `mkCounter`. + +{% code title="Resource.juvix" lineNumbers="true" %} +```agda +module Resource; + +-- Imports section +import Stdlib.Prelude open; +import Anoma open; +import Anoma.Builtin.System open; -- Import for `Reference.to` +import Applib open; + +-- Resource Object +mkCounter {count : Nat := 0} {ephemeral : Bool := false} : Resource := + mkResource@{ + logicRef := TODO; + labelRef := TODO; + valueRef := TODO; + quantity := 1; + ephemeral; + nullifierKeyCommitment := toNullifierKeyCommitment Universal.identity; + nonce := mkNonce rand; + randSeed := mkRandSeed rand; + }; +``` +{% endcode %} + +Importantly, `TODO` will lead to the IDE complaining `Symbol not in scope: TODO` as it's not defined. We can avoid this error by temporarily defining `TODO` before replacing it step-by-step over the next sections. Thus, we can add above `mkCounter`: + +```agda +axiom TODO : {A : Type} -> A; +``` + +Let's unpack what we just added in the Resource Object section line-by-line. + +```agda +mkCounter {count : Nat := 0} {ephemeral : Bool := false} : Resource := +``` + +We create a function `mkCounter` which takes in two arguments, `count` and `ephemeral`. `count` is of type `Nat` and has default value `0`, `ephemeral` is of type `Bool` and is `false` by default. Our `mkCounter` function passes back an object of type `Resource`. + +Next, we specify the constructor's arguments, please find more info on the `Resource` specification \[here]. + +```agda +mkResource@{...}; +``` + +First, we use the constructor of type `Resource` to instantiate the result of our `mkCounter` function. Now, we assign the individual arguments. + +{% code title="Resource.juvix" %} +```agda +mkCounter {count : Nat := 0} {ephemeral : Bool := false} : Resource := + mkResource@{ + logicRef := TODO; -- Will be added in next section + labelRef := TODO; -- Will be added in next section + valueRef := TODO; -- Will be added in next section + quantity := 1; -- We create one counter + ephemeral; -- We pass the mkCounter function argument + nullifierKeyCommitment := toNullifierKeyCommitment Universal.identity; -- To simplify, we use a univeral non-unique identifier + nonce := mkNonce rand; -- We assign a random nonce + randSeed := mkRandSeed rand; -- We assign a random seed + }; +``` +{% endcode %} + +{% hint style="info" %} +You can learn more about how to use the `nullifierKeyCommitment` in a more sophisticated scenario by looking at the `UniqueCounter` example in \[INSERT ANOMA-APPLIB UNIQUE COUNTER LINK]. +{% endhint %} + +Let's now get to the meat of it and specify our Resource further - we start with a simpel label. +{% endstep %} + +{% step %} +### Resource Label + +We start by creating a new file that will contain our Resource Label. + +{% code title="Project root" %} +```bash +touch Label.juvix +``` +{% endcode %} + +We add the following code in our new Label file. + +{% code title="Label.juvix" lineNumbers="true" %} +```agda +module Label; + +import Anoma open; +import Anoma.Builtin.System open; + +counterLabel : Label := mkLabel (anomaEncode ("SimpleCounter")) +``` +{% endcode %} + +The above simply creates a variable `counterLabel` of type `Label` which is assigned to the result of 1) running the `anomaEncode` function on "SimpleCounter" and 2) running `mkLabel` on the result of 1). + +{% hint style="info" %} +Throughout the documentation, we're trying to limit the ways we write Juvix code to a right-to-left evaluation. There are other ways though. For instance, instead of writing `mkLabel (anomaEncode ("SimpleCounter"))`, you can write `"SimpleCounter" |> anomaEncode |> mkLabel`, which results in the same but is written left-to-right. +{% endhint %} +{% endstep %} + +{% step %} +### Resource Logic + +Let's now write the most complex part of the Resource, the Resource Logic. + +{% hint style="info" %} +We're actively working on abstractions to reduce Logic boilerplate code. +{% endhint %} + +First and foremost, we can think about the code we're writing as logic that needs to evaluate to true in the case of a balanced transaction. What does that mean? It means our point-of-view is from the Anoma Resource Machine on a transaction with two resources, one consumed and one created resource. Now, in order for this transaction to balance, aka go through, we need both consumed and created resources' Resource Logics to evaluate true. Thus, when writing the following code, assume that the Anoma Resource Machine runs these logics and there are two resources present that the Anoma Resource Machine knows about. + +We start by creating the `Logic.juvix` file and adding the standard `module` and `import` code, as well as a dummy `counterLogic` function with two inputs, `publicInputs` and `privateInputs`. + +{% code title="Logic.juvix" lineNumbers="true" %} +```agda +module Logic; + +-- Imports +import Stdlib.Prelude open; +import Anoma open; +import Applib open; + +-- Helper +axiom TODO : {A : Type} -> A; + +-- Resource Logic +counterLogic + (publicInputs : Logic.Instance) (privateInputs : Logic.Witness) : Bool := + TODO; + +``` +{% endcode %} + +Here, `publicInputs` include `tag`, `commitments`, `nullifiers`, and `appData` and `privateInputs` include important information like the `Set` of consumed and created Resources. + +Our plan for the logic is now to evaluate to true in the two distinct cases that + +* 1\) the consumed resource is `Ephemeral` and the created resource is `NonEphemeral` which means that the counter is now getting created (i.e., it has not existed before) +* 2\) the consumed resource is `NonEphemeral` and the created resource is `NonEphemeral` which means that the counter exists and is now getting incremented. + +In all other cases, i.e. `NonEphemeral, Ephemeral` and `Ephemeral, Ephemeral`, we want the logic to evaluate `false`. + +Let's try to build that with the following pattern of two `case` evaluations. + +{% code title="" lineNumbers="true" %} +```agda +module Logic; + +-- Imports +import Stdlib.Prelude open; +import Stdlib.Data.Set as Set open using {Set}; +import Anoma open; +import Applib open; + +-- Resource Logic +counterLogic + (publicInputs : Logic.Instance) (privateInputs : Logic.Witness) : Bool := +let + consumed := privateInputs |> Logic.Witness.consumed |> Set.toList; + created := privateInputs |> Logic.Witness.created |> Set.toList; + in case consumed, created of + | [consumedCounter], [createdCounter] := + sameKindCheck@{ + consumedCounter; + createdCounter; + } + && case + both HasEphemerality.get (consumedCounter, createdCounter) + of { + | Ephemeral, NonEphemeral := + creationCheck@{ + createdCounter; + } + | NonEphemeral, NonEphemeral := + incrementationCheck@{ + consumedCounter; + createdCounter; + } + | _, _ := false + } + | _, _ := false; + +sameKindCheck (consumedCounter createdCounter : Resource) : Bool := + kind consumedCounter == kind createdCounter; + +creationCheck (createdCounter : Resource) : Bool := + getCount createdCounter == 0 && HasQuantity.get createdCounter == 1; + +incrementationCheck (consumedCounter createdCounter : Resource) : Bool := + let + expected := getCount consumedCounter + 1; + actual := getCount createdCounter; + in expected == actual; +``` +{% endcode %} + +\[BREAK DOWN IN MULTIPLE STEPS] + +\[^ PASTE NEW CODE ABOVE] + +In order to have this compile, we need to code the `getCount` function first. +{% endstep %} + +{% step %} +### Projection function + +We should be able to do this quickly after everything we've learned so far. `getCount` is a special type of function, a projection function. You can think of it as a read function and it lives within the interface \[LINK TO MODEL VIEW CONTROLLER VISUAL]. Thus, we create a separate folder, "Interface", and add our new projection function file in there. + +```bash +mkdir Interface +cd Interface +touch Projection.juvix +``` + +Let's create the `getCount` function. + +{% code title="Projection.juvix" lineNumbers="true" %} +```agda +module Interface.Projection; + +import Stdlib.Prelude open; +import Anoma open; +import Anoma.Builtin.System open; + +getCount (resource : Resource) : Nat := + Value.unValue (Reference.from (Resource.valueRef (resource))); +``` +{% endcode %} + +Essentially, `getCount` does exactly what you think it does, it accesses a resource which we pass into the function and reads the value. In our application and for resources we target here, the value field corresponds to the count. + +In order to make `Logic.juvix` work, let's not forget to import `getCount`: + +```agda +import Interface.Projection open using {getCount}; +``` + +Let's briefly circle back to `Resource.juvix` to finish our Resource Object. +{% endstep %} + +{% step %} +### Complete the Resource Object + +We can now pass the missing Resource Object parameters by importing what we've been coding in the above steps. + +```agda +module Resource; + +-- Imports +import Stdlib.Prelude open; +import Anoma open; +import Anoma.Builtin.System open; +import Applib open; + +import Logic open using {counterLogic}; +import Label open using {counterLabel}; + +-- Resource Object +mkCounter {count : Nat := 0} {ephemeral : Bool := false} : Resource := + mkResource@{ + logicRef := Reference.to (counterLogic); -- counterLogic from Logic.juvix + labelRef := Reference.to (counterLabel); -- counterLabel from Label.juvix + valueRef := Reference.to (mkValue (count)); -- count from function arguments + quantity := 1; + ephemeral; + nullifierKeyCommitment := toNullifierKeyCommitment Universal.identity; + nonce := mkNonce rand; + randSeed := mkRandSeed rand; + }; +``` + +In order to pass the correct type, we use the `Reference.to` function. Our `mkCounter` resource now uses `counterLogic`, `counterLabel`, and `count`. As you've correctly noticed, we could've specified `valueRef` in Step 1 as the `count` argument was already present. However, we decided to build up some of the Juvix knowledge, like why we write argument passing from right-to-left, and now put it all together. + +We can now face the final boss of our `SimpleCounter` Anoma dApp, the transaction function. Besides the projection function we've already tackled, this is another special function that is part of the `Interface`. As the name suggests, the transaction function handles transactions. + +Let's dive into creating our `SimpleCounter` transaction function! +{% endstep %} + +{% step %} +### Transaction function + +We first create `Transaction.juvix` inside our `Interface` directory (on the same level as `Projection.juvix`). +{% endstep %} +{% endstepper %} + + + +## Target structure + +The project we're building will have the following structure which we will start to build in the following: + +``` +counter +|- Interface +|-- Projection.juvix +|-- Transaction.juvix +|- Kind.juvix +|- Label.juvix +|- Logic.juvix +|- Resource.juvix +``` + + + diff --git a/build/getting-started/README.md b/build/getting-started/README.md new file mode 100644 index 0000000..1733c99 --- /dev/null +++ b/build/getting-started/README.md @@ -0,0 +1,43 @@ +--- +icon: screwdriver-wrench +description: The following helps you get started within less than 5 minutes. +--- + +# Getting Started + +## Prerequisites + +In order to get started, you need Clang / LLVM version 13 or later. + +On macOS the preinstalled clang does not support the wasm target. Get started by using: + +```bash +brew install llvm +``` + +## Install Juvix + +Use the following commands to install Juvix using Homebrew (macOS). + +To install the homebrew-juvix tap: + +```bash +brew tap anoma/juvix +``` + +To install Juvix: + +```bash +brew install juvix +``` + +You can also install Juvix from binaries or from source, as detailed on the [Install Juvix](install-juvix.md) page. + +## Juvix IDEs and plugins + +Using [Visual Studio Code](https://code.visualstudio.com/), install Juvix automatically with the [Juvix VSCode extension](https://marketplace.visualstudio.com/items?itemName=heliax.juvix-mode). + +{% hint style="info" %} +We will continuously add further IDE extensions and plugins. +{% endhint %} + diff --git a/build/getting-started/install-juvix.md b/build/getting-started/install-juvix.md new file mode 100644 index 0000000..9741d1e --- /dev/null +++ b/build/getting-started/install-juvix.md @@ -0,0 +1,3 @@ +# Install Juvix + +[https://docs.juvix.org/latest/howto/installing.html#prerequisites](https://docs.juvix.org/latest/howto/installing.html#prerequisites) diff --git a/build/installation-steps.md b/build/installation-steps.md new file mode 100644 index 0000000..df55cc8 --- /dev/null +++ b/build/installation-steps.md @@ -0,0 +1,108 @@ +--- +hidden: true +--- + +# Installation Steps + +First, macOS homebrew + +``` +brew tap anoma/juvix +``` + +``` +brew install juvix +``` + +Now, getting info with + +``` +juvix doctor +``` + +give me following output: + +``` +> Checking for clang... +> Checking clang version... +> Checking for wasm-ld... + ! Could not find the wasm-ld command + ! https://docs.juvix.org/0.6.6/reference/tooling/doctor/#could-not-find-the-wasm-ld-command +> Checking that clang supports wasm32... + ! Clang does not support the wasm32 target + ! https://docs.juvix.org/0.6.6/reference/tooling/doctor/#clang-does-not-support-the-wasm32-target +> Checking that clang supports wasm32-wasi... + ! Clang does not support the wasm32-wasi target + ! https://docs.juvix.org/0.6.6/reference/tooling/doctor/#clang-does-not-support-the-wasm32-wasi-target +> Checking that WASI_SYSROOT_PATH is set... + ! Environment variable WASI_SYSROOT_PATH is missing + ! https://docs.juvix.org/0.6.6/reference/tooling/doctor/#environment-variable-wasi_sysroot_path-is-not-set +> Checking for wasmer... + ! Could not find the wasmer command + ! https://docs.juvix.org/0.6.6/reference/tooling/doctor/#could-not-find-the-wasmer-command +> Checking latest Juvix release on Github... +``` + +^ Can we maybe make it clear if a step was successful? This look like just outputting when something is missing + +After installing dependencies for `wasi-sdk` , my `juvix doctor` output is the following: + +``` +> Checking for clang... +> Checking clang version... +> Checking for wasm-ld... + ! Could not find the wasm-ld command + ! https://docs.juvix.org/0.6.6/reference/tooling/doctor/#could-not-find-the-wasm-ld-command +> Checking that clang supports wasm32... + ! Clang does not support the wasm32 target + ! https://docs.juvix.org/0.6.6/reference/tooling/doctor/#clang-does-not-support-the-wasm32-target +> Checking that clang supports wasm32-wasi... + ! Clang does not support the wasm32-wasi target + ! https://docs.juvix.org/0.6.6/reference/tooling/doctor/#clang-does-not-support-the-wasm32-wasi-target +> Checking that WASI_SYSROOT_PATH is set... +> Checking for wasmer... + ! Could not find the wasmer command + ! https://docs.juvix.org/0.6.6/reference/tooling/doctor/#could-not-find-the-wasmer-command +> Checking latest Juvix release on Github... +``` + +Now I have installed dependencies but apparently, miss some dependencies. Seems like I'm required to separately install the prerequisites: + +For `wasmer`: + +``` +curl https://get.wasmer.io -sSfL | sh +``` + +That worked after closing and opening the terminal + +`juvix doctor` output: + +``` +> Checking for clang... +> Checking clang version... +> Checking for wasm-ld... + ! Could not find the wasm-ld command + ! https://docs.juvix.org/0.6.6/reference/tooling/doctor/#could-not-find-the-wasm-ld-command +> Checking that clang supports wasm32... + ! Clang does not support the wasm32 target + ! https://docs.juvix.org/0.6.6/reference/tooling/doctor/#clang-does-not-support-the-wasm32-target +> Checking that clang supports wasm32-wasi... + ! Clang does not support the wasm32-wasi target + ! https://docs.juvix.org/0.6.6/reference/tooling/doctor/#clang-does-not-support-the-wasm32-wasi-target +> Checking that WASI_SYSROOT_PATH is set... + ! Environment variable WASI_SYSROOT_PATH is missing + ! https://docs.juvix.org/0.6.6/reference/tooling/doctor/#environment-variable-wasi_sysroot_path-is-not-set +> Checking for wasmer... +> Checking latest Juvix release on Github... +``` + +*** + +According to Paul, for macOS, only `clang` is a prerequisite, followed by the homebrew installation steps + +^ added this to the docs + + + +Now trying to create first application with the installation steps from above. diff --git a/build/your-first-anoma-application/README.md b/build/your-first-anoma-application/README.md new file mode 100644 index 0000000..aa13204 --- /dev/null +++ b/build/your-first-anoma-application/README.md @@ -0,0 +1,225 @@ +--- +icon: rocket-launch +description: >- + The following sets you up to build, run, and test your first Anoma + application. +--- + +# Your First Anoma Application + +## Prerequisites + +Before creating your first Anoma dApp, make sure to have [Juvix installed](../getting-started/install-juvix.md). + +Additionally, you can learn how [write a Juvix project](write-a-juvix-project.md) to nail the very basics of coding in Juvix. + +## Anoma Client + +\[Section about connecting to Client] + +## Building the HelloWorld Application + +#### Project Outline + +The goal of this application is to create 1) _an Anoma Resource_ with 2) _a `label` "HelloWorld!"_ as well as 3) _a function to read_ _the_ `label` from the Resource Object. + +\[could insert more formal explainer of 1) Resource and 2) Label] + +#### Project Setup + +Let's fly through the project setup by typing the following in our console / terminal. If you already have a project directory, you can skip ahead and just use `juvix init`. + +```bash +mkdir HelloWorld +cd HelloWorld +juvix init +# (1) Next, type 'hello-world' for the project name +# (2) Finally, press 'Enter' to choose the default version number +``` + +{% stepper %} +{% step %} +### Building the HelloWorld Resource Object + +Let's start by creating a new file that will contain our Resource. + +{% code title="# Inside ~/HelloWorld# Inside ~/HelloWorld" %} +```bash +touch Resource.juvix +``` +{% endcode %} + +Next, we preface our `Resource.juvix` file with the standard `module` and imports. + +{% code title="Resource.juvix" %} +```agda +module Resource; + +-- IMPORTS +import Stdlib.Prelude open; +import Anoma open; +import Anoma.Builtin.System open; +import Applib open; +``` +{% endcode %} + +We now start contructing our Resource which we call `mkHelloWorld` by giving it values for `logicRef`, `labelRef`, `valueRef`, `quantity`, `ephemeral`, `nullifierKeyCommitment`, `nonce`, and `randSeed`. + +Let's start by putting default values for `logicRef` and `valueRef` while assigning `TODO` to `labelRef` for now. We will then branch out the `labelRef` code into a `Label.juvix` file to emphasize that we're not dealing with default values here. + +{% code title="Resource.juvix" lineNumbers="true" %} +```agda +-- ### Module and imports code ### + +-- HELPER +logic (publicInputs : Logic.Instance) (privateInputs : Logic.Witness) : Bool := + true; + +value : Value := mkValue 0; + +-- RESOURCE OBJECT +mkHelloWorld : Resource := + mkResource@{ + labelRef := TODO; + logicRef := Reference.to (logic); + valueRef := Reference.to (value); + }; +``` +{% endcode %} + +{% hint style="info" %} +Juvix will complain about the presence of `TODO` in the above code. You can get rid of the errors by adding `axiom TODO : {A : Type} -> A;` above the Resource Object. Keep in mind that you have to remove the `axiom` before compiling the code as it won't compile otherwise. +{% endhint %} + +What's happening here is that we assign `true` to the `logicRef`, implying that this Resource will not have any logic constraints. Similarly, we assign zero for `valueRef` which is an arbitrary default. + +Let's continue adding missing parameters before getting back to `labelRef`. + +{% code title="Resource.juvix" lineNumbers="true" %} +```agda +-- ### Module, imports, and helpers code ### + +-- RESOURCE OBJECT +mkHelloWorld : Resource := + mkResource@{ + labelRef := TODO; + logicRef := Reference.to (logic); + valueRef := Reference.to (value); + quantity := 1; + ephemeral := false; + nullifierKeyCommitment := toNullifierKeyCommitment Universal.identity; + nonce := mkNonce rand; + randSeed := mkRandSeed rand; + }; +``` +{% endcode %} + +In the above code, we + +* assign `quantity` of 1 (line 9) +* specify a non-emphemeral resource (in a sense, it can persist) (line 10) +* assign the universal identity to `nullifierKeyCommitment` which is equal to an Identity generated from a zero address (line 11) +* use builtin `rand` for our `nonce` (line 12) +* and finally use builtin `rand` again for the `randSeed` (line 13) + + +{% endstep %} + +{% step %} +### Add HelloWorld Label + +Let's add our `label` in a separate file. Although the `label` is not a complex piece of code in this case, it is good practice to have a separate file for non-default Resource components. + +{% code title="# Inside ~/HelloWorld# Inside ~/HelloWorld" %} +```bash +touch Label.juvix +``` +{% endcode %} + +We can now populate the `Label.juvix` file with our `Hello World!` label. + +{% code title="Label.juvix" %} +```agda +module Label; + +import Anoma open; +import Anoma.Builtin.System open; + +label : Label := mkLabel (anomaEncode "Hello World!"); +``` +{% endcode %} + +In the above code, we simply create a variable `label` of type `Label` which is the result of applying the function `mkLabel` to the result of the function `anomaEncode` of `Hello World!`. In other words, we encode "Hello World!" and then turn that into a label. + +Last step for our label is to tweak the `Resource.juvix` file slightly to accomodate our new code. The following should be our `Resource.juvix` file after integrating the label. + +{% code title="Resource.juvix" %} +```agda +module Resource; + +-- IMPORTS +import Stdlib.Prelude open; +import Anoma open; +import Anoma.Builtin.System open; +import Applib open; + +import Label open using {label}; + +-- HELPER +logic (publicInputs : Logic.Instance) (privateInputs : Logic.Witness) : Bool := + true; + +value : Value := mkValue 0; + +-- RESOURCE OBJECT +mkHelloWorld : Resource := + mkResource@{ + labelRef := Reference.to (label); + logicRef := Reference.to (logic); + valueRef := Reference.to (value); + quantity := 1; + ephemeral := false; + nullifierKeyCommitment := toNullifierKeyCommitment Universal.identity; + nonce := mkNonce rand; + randSeed := mkRandSeed rand; + }; + +``` +{% endcode %} +{% endstep %} + +{% step %} +### Add HelloWorld Projection Function + +Let's finish our HelloWorld application by adding functionality that allows us to read the label. To achieve this, we add `getLabel`, which is a special type of function, a projection function. You can think of it as a read function and it lives within the interface \[LINK TO MODEL VIEW CONTROLLER VISUAL]. Thus, we create a separate folder, "Interface", and add our new projection function file in there. + +{% code title="# Inside ~/HelloWorld" %} +```bash +mkdir Interface +cd Interface/ +touch Projection.juvix +``` +{% endcode %} + +We can now specify `getLabel`. It will take a parameter of type `Resource` and then access its label via `labelRef`. + +{% code title="Interface/Projection.juvix" %} +```agda +module Interface.Projection; + +import Stdlib.Prelude open; +import Anoma open; +import Anoma.Builtin.System open; + +getLabel (resource : Resource) : Nat := Label.unLabel (Reference.from (Resource.labelRef (resource))); +``` +{% endcode %} +{% endstep %} +{% endstepper %} + +## Runing the HelloWorld Application + +\[Continue section with progress from Paul's e2e integration work] + + + diff --git a/build/your-first-anoma-application/configure-a-juvix-package.md b/build/your-first-anoma-application/configure-a-juvix-package.md new file mode 100644 index 0000000..4fa1a30 --- /dev/null +++ b/build/your-first-anoma-application/configure-a-juvix-package.md @@ -0,0 +1,3 @@ +# Write a Juvix Package + +[https://docs.juvix.org/latest/howto/project.html](https://docs.juvix.org/latest/howto/project.html) diff --git a/build/your-first-anoma-application/write-a-juvix-project.md b/build/your-first-anoma-application/write-a-juvix-project.md new file mode 100644 index 0000000..0657ed0 --- /dev/null +++ b/build/your-first-anoma-application/write-a-juvix-project.md @@ -0,0 +1,84 @@ +# Write a Juvix Project + +## Prerequisites + +Before creating your first Anoma dApp, make sure to have [Juvix installed](../getting-started/install-juvix.md). + +## Setup a Juvix Project + +A Juvix project is a collection of Juvix modules and a `Package.juvix` file. You can find more detailed information on `Package.juvix` under [Write a Juvix Package](configure-a-juvix-package.md). + +Open your terminal and navigate to your project directory. Initialize your first project by running: + +```bash +juvix init +``` + +You will be prompted to enter the name of your project, let's go with `hello-world` and a version of your project, let's take the default `0.0.0` by pressing _Enter_. + +## Adding a Juvix Module + +To add functionality to our project, we need a new Juvix file. A Juvix file must declare a module with the same name as you gave the file. Let's create a new file in our terminal: + +```bash +touch HelloWorld.juvix +``` + +We will first add the module declaration according to the name of the file we have just created. + +{% code title="HelloWorld.juvix" %} +```agda +-- This is a comment +module HelloWorld; +``` +{% endcode %} + +Our `HelloWorld` program is supposed to output "Hello World!", of course. Thus, we first need to import the `String` type from the standard library prelude. + +{% code title="HelloWorld.juvix" fullWidth="false" %} +```agda +module HelloWorld; + +-- Importing the `String` type from the standard library prelude +import Stdlib.Prelude open; +``` +{% endcode %} + +Now that we have access to `String`, we can add our "Hello World!" output. + +{% code title="HelloWorld.juvix" %} +```agda +module HelloWorld; + +import Stdlib.Prelude open; + +main : String := "Hello world!"; +``` +{% endcode %} + +## Compiling Juvix Project + +To compile `HelloWorld.juvix`, go to your terminal and type: + +```bash +juvix compile native HelloWorld.juvix +``` + +This should result in the following project directory structure: + +``` +hello-world +|- HelloWorld -- compiled Unix Executable file +|- HelloWorld.juvix +|- Package.juvix +``` + +## Running Juvix Project + +Finally, we can run the compile Unix Executable file by typing the following in our terminal: + +```bash +juvix eval HelloWorld.juvix +``` + +This should now result in the expected output `"Hello world!"`. diff --git a/docs/test.juvix.md b/docs/test.juvix.md index 598c45e..13ce357 100644 --- a/docs/test.juvix.md +++ b/docs/test.juvix.md @@ -1,7 +1,12 @@ +# What is Anoma? + +TODO + # Test -```juvix +```agda module test; +mystring : String := "hello world"; ``` ## This is a test. diff --git a/learn/anomas-state-model.md b/learn/anomas-state-model.md new file mode 100644 index 0000000..d690e95 --- /dev/null +++ b/learn/anomas-state-model.md @@ -0,0 +1,57 @@ +# Anoma's State Model + +Anoma organizes state in a resource model. + +

Schematic depiction of state as resources.

+ + + +## Comparison to other State Models + +### 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. + +

Schematic depiction of the account model.

+ + + +### 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 + +

Schematic depiction of the UTXO model.

+ + + +### 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 + +

Schematic depiction of the resource model.

+ + + +## Affordances + +This enables[^1] + +* 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 + + + +[^1]: https://ethresear.ch/t/rfc-draft-anoma-as-the-universal-intent-machine-for-ethereum/19109. diff --git a/learn/page.md b/learn/page.md new file mode 100644 index 0000000..5c4b4d5 --- /dev/null +++ b/learn/page.md @@ -0,0 +1,2 @@ +# Page + diff --git a/learn/resources.md b/learn/resources.md new file mode 100644 index 0000000..fb992d0 --- /dev/null +++ b/learn/resources.md @@ -0,0 +1,83 @@ +# 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})$$ + +$$ +\texttt{kind} := h_\texttt{kind}(\texttt{logic},\,\texttt{label}) +$$ + +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.