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 Taiga 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 using VampIR or Geb, 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.
flowchart LR
A((Alice)) -- "Intent 1:\ntrade 1 A or 2 B for 1 Dolphin" ---> B[Taiga]
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/taiga-simulator
¶
module Alice;
-- Alice is willing to exchange either 2 B or 1 A for 1 Dolphin.
partialTransaction : PartialTx :=
mkPartialTx
(consumedPair := A.mkResource 1, B.mkResource 2;
createdPair := AliceIntent.mkResource 1, dummyResource);
end;
module Bob;
partialTransaction : PartialTx :=
mkPartialTx
(consumedPair := Dolphin.mkResource 1, dummyResource;
createdPair := A.mkResource 1, dummyResource);
end;
module Solver;
partialTransaction : PartialTx :=
mkPartialTx
(consumedPair := AliceIntent.mkResource 1, dummyResource;
createdPair := Dolphin.mkResource 1, B.mkResource 2);
end;
module AliceIntent;
logicFunction : ResourceKind -> PartialTx -> Bool
| kind tx :=
let
createdRs : List Resource := createdResources tx;
createdHashes : List LogicHash :=
map Resource.logicHash createdRs;
in isCreated kind
|| (quantityOfDenom Dolphin.denomination createdRs
== ofNat 1
&& quantityOfDenom A.denomination createdRs == ofNat 1)
|| quantityOfDenom Dolphin.denomination createdRs == ofNat 1
&& quantityOfDenom B.denomination createdRs == ofNat 2;
--- This will be computed from the logic function
logicHash : LogicHash := 1;
staticData : ByteString := 3 :: nil;
denomination : Denomination := 1 :: staticData;
mkResource (n : Int) : Resource :=
mkResource'
(logicHash := logicHash;
staticData := staticData;
dynamicData := nil;
quantity := n);
end;
logicFunctions : Map LogicHash LogicFunction :=
mkLogicFunctionMap
((AliceIntent.logicHash, AliceIntent.logicFunction) :: nil);
twoPartyExchange : Test :=
let
txs : List PartialTx :=
Alice.partialTransaction
:: Bob.partialTransaction
:: Solver.partialTransaction
:: nil;
in testCase
"two party exchange"
(assertTrue
"expected two-party exchange transactions to validate"
(checkTransaction logicFunctions txs));
How to write intents in Juvix to validate transactions in Anoma is further elaborated in both the Taiga Simulator repository and the Juvix Workshop.
sequenceDiagram
UserWallet ->>Taiga API: use intent to create ptxs
Taiga API -->>UserWallet: returns ptxs
UserWallet ->>Solvers: send a ptxs
Solvers ->>Solvers: match/broadcast ptxs
Solvers -->>Taiga API: create helper ptxs
Taiga API -->>Solvers: gives helper ptxs
Solvers ->>Taiga API: create a tx
Taiga API -->>Solvers: returns a finalized tx
Solvers ->>Finaliser : submit finalized transaction
Finaliser ->> Taiga API: verify the finalized transaction
Taiga API ->> Finaliser: return the result (valid/invalid)
Finaliser -->> Blockchain: commit a (balanced) tx
Blockchain ->> Blockchain: run consensus Typhon alg.
Blockchain ->> Taiga API: verify the transaction
Taiga 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 -t 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
¶
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;
{
"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.
-
Tutorials
Master the essentials of Juvix through a series of tailored examples, tutorials and technical explanations.
-
Talks and Workshops
A collection of talks and workshop videos showcasing Juvix. Gain valuable insights and inspiration from our presentations at various conferences.
-
Reference
Explore the Language reference, milestone examples, and tooling documentation!
-
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.
-
Open Source, GPL3.0
Juvix is licensed under GPL3 and available on GitHub.