Refactor main page and many other fixes

anoma · Sep 16, 2023 · 6f6de62 · 6f6de62
1 parent f1f6259
commit 6f6de62
Show file tree

Hide file tree

Showing 13 changed files with 13,995 additions and 159 deletions.
diff --git a/MidSquareHash.lisp b/MidSquareHash.lisp
diff --git a/docs/howto/installing.md b/docs/howto/installing.md
@@ -35,6 +35,11 @@ Copy and paste the following command into your terminal to install Juvix.
     curl --proto '=https' --tlsv1.2 -sSfL https://get.juvix.org | sh
     ```
 
+!!! tip ""
+
+      In VSCode, install Juvix automatically with the [Juvix VSCode
+      extension](https://marketplace.visualstudio.com/items?itemName=heliax.juvix-mode).
+
 ## MacOS
 
 The easiest way to install Juvix on MacOS is by using

diff --git a/docs/index.juvix b/docs/index.juvix
@@ -1,23 +1,55 @@
 module index;
 
-import Stdlib.Prelude open;
-import Stdlib.Data.Nat.Ord open;
+--8<-- [start:hash]
+module Hash;
+  import Stdlib.Prelude open;
+  import Stdlib.Data.Nat.Ord open;
 
---8<-- [start:exponentiation]
-module FastExponentiation;
-
   {-# unroll: 30 #-}
   terminating
   power' (acc a b : Nat) : Nat :=
     let
       acc' : Nat := if (mod b 2 == 0) acc (acc * a);
     in if (b == 0) acc (power' acc' (a * a) (div b 2));
 
-  power : Nat → Nat → Nat := power' 1;
+  power : Nat → Nat := power' 1 2;
 
+  hash' : Nat -> Nat -> Nat
+    | (suc n@(suc (suc m))) x :=
+      if
+        (x < power n)
+        (hash' n x)
+        (mod (div (x * x) (power m)) (power 6))
+    | _ x := x * x;
+
+  hash : Nat -> Nat := hash' 16;
+
+  -- result: 3
+  main : Nat := hash 1367;
 end;
---8<-- [end:exponentiation]
+--8<-- [end:hash]
 
+{-
 --8<-- [start:intent]
--- ss
+...
+-- Alice is willing to exchange either 2 B or 1 A for 1 Dolphin.
+module Apps.TwoPartyExchange;
+--- Definitions related to Alice's intent
+module AliceIntent;
+  logicFunction : LogicFunction
+    | kind tx :=
+        let
+            {- check if the resource associated to
+            this logic function is among the created (output) resources.
+            Then check if alice's intent is satisfied. -}
+            createdRs : List Resource := createdResources tx;
+            createdHashes : List LogicHash :=
+                map logicHash createdRs;
+        in isCreated kind
+      || quantityOfDenom Dolphin.denomination createdRs == 1
+      && quantityOfDenom A.denomination createdRs == 1
+      || quantityOfDenom Dolphin.denomination createdRs == 1
+      && quantityOfDenom B.denomination createdRs == 2;
+ ...
 --8<-- [end:intent]
+-}
diff --git a/docs/index.md b/docs/index.md
@@ -1,116 +1,174 @@
 ---
 nobuttons: true
-title: Home
+title: Juvix Docs
 description: Juvix is a high-level programming language for writing privacy-preserving decentralised applications.
 hide:
   - navigation
   - toc
 ---
 
-# Welcome to the Juvix documentation!
+
+# Juvix: a language for intent-centric and declarative decentralized applications
+
 
 <div class="grid cards" markdown>
 
-Juvix is an open-source, ever-evolving functional language for creating
-privacy-focused decentralized apps. It allows developers to write high-level
-programs that compile to WASM or, via [VampIR][vampir], to circuits for private
-execution using [Taiga][taiga] on [Anoma][anoma] or Ethereum.
+<div style="text-align:center" markdown>
+
+<div style="text-align:center">
+  <img src="assets/images/tara-smiling.svg" width="220" />
 </div>
 
+[Install Juvix on your machine](http://localhost:8000/howto/installing/#shell-script){ .md-button .md-button--primary}
 
-<div class="grid cards" markdown>
+[Try Juvix now on Codespaces](https://github.com/codespaces/new?hide_repo_select=true&ref=main&repo=102404734&machine=standardLinux32gb&location=WestEurope){ .md-button  }
+
+</div>
 
 <div markdown>
 
-## :material-content-duplicate: Intents in Juvix for Anoma
+Juvix is an open-source functional language with static typing and strict
+semantics. It is the programming language for the [Anoma][anoma]'s blockchain. The
+primary purpose of this language is to encode [Anoma's intents][anoma], enabling
+private or transparent execution through [Taiga][taiga] on the Anoma
+blockchain.
 
-An intent is a high-level description of a transaction the user wants to
-perform. It is a program that describes the conditions under which a transaction
-is valid. For example, Alice wants to exchange 2 B or 1 A for 1 Dolphin.
+Juvix, while designed for Anoma, offers capabilities that surpass it. It can
+compile programs into WASM and arithmetic circuits using [VampIR][vampir] or
+[Geb][geb], providing features expected in any other high-level programming
+language.
 
-Read more on Anoma's intents [here](https://anoma.net/blog/intents-arent-real).
+Stay tuned for Juvix updates! Follow us on [:material-twitter: Twitter][twitter]
+and join our [:fontawesome-brands-discord: Discord][Discord] community.
 
-<div style="text-align:center" markdown>
+<!-- To follow the development of Anoma, follow [:material-twitter: Anoma
+Twitter][anomaTwitter] and join [:fontawesome-brands-discord: Anoma
+Discord][anomaDiscord]. -->
 
-<div style="text-align:center">
-  <img src="assets/images/tara-smiling.svg" width="250" />
 </div>
 
+</div>
+
+<div style="text-align:center" markdown>
 
-[Try Juvix now on Codespaces](https://github.com/codespaces/new?hide_repo_select=true&ref=main&repo=102404734&machine=standardLinux32gb&location=WestEurope){ .md-button .md-button--primary }
+## ... a brief of what Juvix is about
 
 </div>
 
 
-</div>
+<div class="grid cards" markdown>
+
+<div markdown>
 
-<div style="padding: 1rem 0 0 0" markdown>
+## :material-content-duplicate: Intents in Juvix for Anoma's dApps
 
+What is an [intent](https://anoma.net/blog/intents-arent-real)? An intent, in
+essence, is a high-level description of a user's desired transaction. It can be
+written in Juvix as a program detailing the conditions that validate the
+transaction in relation to the user's resources.
 
-:octicons-mark-github-16: [`anoma/juvix-workshop`](https://github.com/anoma/taiga-simulator)
+Take for instance, Alice's intent. Her intent is to trade either two units of
+resource `B` or one unit of resource `A` for a unit of `C`. Bob, on the other
+hand, is willing to exchange one unit of resource `A` for 1 `C`. How can we
+write these intents in Juvix? The conditions for Alice's intent is presented in
+Juvix on the right, a **logic function** that validates the transaction.
 
-```juvix
-...
--- Alice is willing to exchange either 2 B or 1 A for 1 Dolphin.
-module Apps.TwoPartyExchange;
---- Definitions related to Alice's intent
-module AliceIntent;
-  logicFunction : LogicFunction
-    | kind tx :=
-        let
-            {- check if the resource associated to
-            this logic function is among the created (output) resources.
-            Then check if alice's intent is satisfied. -}
-            createdRs : List Resource := createdResources tx;
-            createdHashes : List LogicHash :=
-                map logicHash createdRs;
-        in isCreated kind
-      || quantityOfDenom Dolphin.denomination createdRs == 1
-      && quantityOfDenom A.denomination createdRs == 1
-      || quantityOfDenom Dolphin.denomination createdRs == 1
-      && quantityOfDenom B.denomination createdRs == 2;
- ...
+See [here](https://anoma.github.io/taiga-simulator/Apps.TwoPartyExchange-src.html#1184) the full Juvix code for this example.
+
+<div class="grid cards" style="text-align:center" markdown>
+
+```mermaid
+flowchart LR
+    A[Alice] -- "Intent #1: has 2 B, wants 1 C" ----> B[Anoma]
+    A -- "Intent #2: has 1 A, wants 1 C" ----> B
+    X[Bob] -- "Intent #3: has 1 C, wants 1 A" ----> B
 ```
 
 </div>
 
+How to write intents in Juvix to validate transactions in Anoma is futher
+elaborated in both the [Taiga
+Simulator](https://github.com/anoma/taiga-simulator) repository and the [Juvix
+Workshop](https://github.com/anoma/juvix-workshop).
+
 </div>
 
+<div markdown>
+
+## :octicons-mark-github-16: [`anoma/juvix-workshop`](https://github.com/anoma/taiga-simulator)
+
+```juvix
+--8<------ "docs/index.juvix:intent"
+```
+
+</div>
+</div>
 
-## :material-graph-outline: Juvix Compilation to Arithmetic Circuits
 
 <div class="grid cards" markdown>
 
 <div markdown>
 
-A significant feature of Juvix includes compiling programs into arithmetic circuits for confidential execution, achieved via the in-house [VampIR][vampir] compiler. Arithmetic circuits model the computation of Juvix programs by representing polynomial computations. These circuits can be executed privately using [Taiga][taiga]. Essentially, arithmetic circuits are systematic polynomial equations expressed in a universal, canonical form.
+## :material-graph-outline: Arithmetic Circuits / Zero-knowledge Proofs
+
+An arithmetic circuit is an algebraic representation, essentially expressing a
+system of polynomial equations in a universal, canonical form that model the
+computation of a program. Arithmetic circuits are used in zero-knowledge proofs
+and Juvix can compile programs into these representations via [VampIR][vampir].
+
+```mermaid
+flowchart LR
+    A[Juvix file]  -- Juvix --> B[VampIR circuit]
+    B -- VampIR --> C[PLONK or Halo2 circuit]
+```
+
+``` shell
+juvix compile -t vampir Hash.juvix
+```
+
+The VampIR file can then be compiled to a PLONK circuit:
+
+``` shell
+vamp-ir plonk setup -m 10 -o input.pp
+vamp-ir plonk compile -u input.pp -s Hash.pir -o c.plonk
+```
+
+A zero-knowledge proof that `hash 1367` is equal to `3` can then be generated
+from the circuit:
+
+``` shell
+vamp-ir plonk prove -u input.pp -c c.plonk -o proof.plonk -i Hash.json
+```
+
+This proof can then be verified:
 
-See more [Compiling Juvix programs to arithmetic circuits via Vamp-IR](./blog/posts/vampir-circuits.md).
+``` shell
+vamp-ir plonk verify -u input.pp -c c.plonk -p proof.plonk
+```
 
 </div>
 
 <div markdown>
 
-```juvix
-module FastExponentiation;
-
-{-# unroll: 30 #-}
-terminating
-power' (acc a b : Nat) : Nat :=
-  let acc' : Nat := if (mod b 2 == 0) acc (acc * a);
-  in if (b == 0) acc (power' acc' (a * a) (div b 2));
-power : Nat → Nat → Nat := power' 1;
+## :octicons-mark-github-16: [`anoma/juvix-workshop`](https://github.com/anoma/juvix-workshop/blob/main/arithmetic-circuits/README.md)
 
-end;
+```juvix
+--8<------ "docs/index.juvix:hash"
 ```
 
+For further details, refer to [Compiling Juvix programs to
+arithmetic circuits via Vamp-IR](./blog/posts/vampir-circuits.md).
+
 </div>
 
 </div>
 
+<div style="text-align:center" markdown>
 
 ## :material-firework: Juvix is growing fast!
 
+</div>
+
 <div class="grid cards" markdown>
 
 -   :fontawesome-solid-computer:{ .lg .middle } __How-to guides__
@@ -184,6 +242,7 @@ end;
 [anoma]: https://anoma.net
 [changelog]: https://docs.juvix.org/changelog.html
 [Discord]: https://discord.gg/jwzaMZ2Sct
+[anomaDiscord]: https://discord.gg/jwzaMZ2Sct
 [geb]: https://github.com/anoma/geb
 [GitHub]: https://github.com/anoma/juvix
 [homebrew]: https://brew.sh
@@ -198,6 +257,7 @@ end;
 [stdlib]: https://github.com/anoma/juvix-stdlib
 [taiga]: https://github.com/anoma/taiga
 [twitter]: https://twitter.com/juvixlang
+[anomaTwitter]: https://twitter.com/anoma
 [vampir]: https://github.com/anoma/vamp-ir
 [vscode-plugin]: https://github.com/anoma/vscode-juvix
 [website]: https://juvix.org
diff --git a/docs/reference/language/datatypes.juvix b/docs/reference/language/datatypes.juvix
@@ -2,6 +2,30 @@ module datatypes;
 
 import Stdlib.Data.Fixity open;
 
+--8<-- [start:unit]
+type Unit := unit : Unit;
+--8<-- [end:unit]
+
+--8<-- [start:typeBool]
+type Bool :=
+  | true : Bool
+  | false : Bool;
+--8<-- [end:typeBool]
+
+module ADT;
+  --8<-- [start:natADT]
+  type Nat :=
+    | Z
+    | S Nat;
+  --8<-- [end:natADT]
+
+  --8<-- [start:listADT]
+  type List A :=
+    | Nil
+    | Cons A (List A);
+--8<-- [end:listADT]
+end;
+
 --8<-- [start:typeNat]
 type Nat :=
   | zero : Nat