Juvix a language for intent-centric and declarative decentralized applications¶

Juvix is an open-source functional language with static typing and strict semantics. It is the programming language for the Anoma's blockchain. The primary purpose of this language is to encode Anoma's intents, enabling private and transparent execution through the Abstract Resource Machine on the Anoma blockchain.

Juvix, initially designed for Anoma, provides features typical of any high-level programming language with many more on the horizon. It can compile programs into native executable, WASM, and arithmetic circuits facilitating zero-knowledge proofs.

Stay tuned for Juvix updates! Follow us on Twitter and join our Discord community.

... a brief of what Juvix is about¶

Intents in Juvix for Anoma's dApps¶

What is an intent? An intent, in essence, is a high-level description, a message sent by programs to indicate changes of a desired state.

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 Dolphin. Bob, on the other hand, is willing to exchange one unit of resource A for 1 Dolphin. 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.

See here the full Juvix code for this example.

Two-party exchange

flowchart LR
    A((Alice)) -- "Intent 1:\ntrade 1 A or 2 B for 1 Dolphin" ---> B[RM]
    X((Bob)) -- "Intent 2:\ntrade 1 Dolphin for 1 A" ---> B
    B --> P[Pool]
    S((Solver)) <----> P
    P -- "Intent solving" --> Z("Finalized\nTransaction")
    Z --> O[(Anoma)]

`anoma/abstract-resource-machine-simulator`¶

Alice Intent

module Exchange;
  import Anoma open;
  import Anoma.Prelude open hiding {for; any; all};
  import Anoma.IntentDsl open;
  import Apps.TwoPartyExchange.Asset open;
  
  aliceIntent : PartialTx :=
    exchangeIntent@{
      ownedAssets := [1 of_ a; 2 of_ b];
      clauses := [want (1 of_ dolphin) for any ownedAssets]
    };
  
  bobIntent : PartialTx :=
    exchangeIntent@{
      ownedAssets := [1 of_ dolphin];
      clauses := [want (1 of_ a) for exactly (1 of_ dolphin)]
    };
end;

Abstract Resource Machine SimulatorTransaction lifecycle

How to write intents in Juvix to validate transactions in Anoma is further elaborated in both the RM Simulator repository and the Juvix Workshop.

sequenceDiagram
    UserWallet ->>RM API: use intent to create ptxs
    RM API  -->>UserWallet: returns ptxs
    UserWallet  ->>Solvers: send a ptxs
    Solvers   ->>Solvers: match/broadcast ptxs
    Solvers  -->>RM API: create helper ptxs
    RM API  -->>Solvers: gives helper ptxs
    Solvers   ->>RM API: create a tx
    RM API  -->>Solvers: returns a finalized tx
    Solvers  ->>Finaliser : submit finalized transaction
        Finaliser ->> RM API: verify the finalized transaction
    RM API ->> Finaliser: return the result (valid/invalid)
    Finaliser -->> Blockchain: commit a (balanced) tx
    Blockchain ->> Blockchain: run consensus Typhon alg.
    Blockchain ->> RM API: verify the transaction
    RM API -->> Blockchain: return the result (valid/invalid)

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 our in-house compiler VampIR.

flowchart LR
    A[Juvix file]  -- Juvix --> B[VampIR circuit]
    B -- VampIR --> C[PLONK or Halo2 circuit]

juvix compile vampir Hash.juvix

The VampIR file can then be compiled to a PLONK circuit:

vamp-ir plonk setup -m 14 -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:

vamp-ir plonk prove -u input.pp \
                    -c c.plonk \
                    -o proof.plonk -i Hash.json

This proof can then be verified:

vamp-ir plonk verify -u input.pp -c c.plonk -p proof.plonk

`anoma/juvix-workshop`¶

Hash.juvixHash.json

module Hash;
  import Stdlib.Prelude open;

  {-# 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 := 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;
  
  main : Nat -> Nat := hash;
end;

{
"in": "1367",
"out": "3"
}

Note

For further details, refer to Compiling Juvix programs to arithmetic circuits via Vamp-IR.

Juvix is growing fast!¶

How-to guides

Learn how to install Juvix on macOS or Linux, as well as compile and document your Juvix projects.

Quick start

How-to guides
Tutorials

Master the essentials of Juvix through a series of tailored examples, tutorials and technical explanations.

Learn Juvix in 5 minutes

Talks and Workshops

A collection of talks and workshop videos showcasing Juvix. Gain valuable insights and inspiration from our presentations at various conferences.

Juvix videos
Reference

Explore the Language reference, milestone examples, and tooling documentation!

Reference
Blog

Check out our blog to discover new features in the upcoming release, along with helpful examples and more. And, don't forget to join us on Discord.

Blog

Join us
Open Source, GPL3.0

Juvix is licensed under GPL3 and available on GitHub.

License