Juvix empowers developers to write code in a high-level, functional language, compile it to gas-efficient output VM instructions, and formally verify the safety of their contracts prior to deployment and execution.
Juvix is a dependently functional programming language for writing efficient formally-verified validity predicates, which can be deployed to various distributed ledgers. Juvix addresses many issues that we have experienced while trying to write and deploy decentralised applications present in the ecosystem of smart-contracts:
The Juvix compiler synthesises a high-level frontend syntax with support for dependent-linearly types and several other cutting-edge research ideas from programming language design and type theory. For more details, see Juvix's documentation.
Install Stack:
apt install stack
apt install haskell-stack
pacman -S stack
brew install haskell-stack
It is required at least 8GB RAM for stack
installation.
You might need to install the following third-party libraries.
And run the following Nix commands:
nix-channel --add https://nixos.org/channels/nixpkgs-unstable
nix-channel --update
nix-env -u
Nix might install the following packages:
To install Juvix, you can download its sources using Git from the Github repository. Then, the program can be downloaded and installed with the following commands:
$ git clone https://github.com/anoma/juvix.git
$ cd juvix
$ make install
If the installation succeeds, you must be able to run the juvix command
from any location. To get the complete list of commands, please run juvix --help
.
$ juvix version
Juvix version 0.1.1.19-a2111a3
Branch: develop
Commit: a2111a389be0e17291f2903d1ec7d7b94bd60cf8
Date: Mon Sep 13 13:26:18 2021 -0500
For a more experienced user, after cloning Juvix into a local
directory, to build and install the binary to the local path, you
can run the following make commands: make
or for full optimisations
(but slower compile times): make build-prod
.
For Windows users, to use the command make, please visit this link.
.ju
contractTo write Juvix programs, you can use any text editor. However, we recommend to use VSCode with the Juvix syntax highlighting package. In the following example, we will code a validity predicate using the LLVM backend.
vp.ju
. The file content should be as follows.mod VP where
open Prelude
open Prelude.LLVM
type account = {
balance : nat
}
type transaction-type = {
account-from : account,
account-to : account
}
type storage = {
transaction : transaction-type,
}
sig accept-withdraws-from : key -> storage -> storage -> bool
let accept-withdraws-from key {transaction = initial} {transaction = final}
| key == final.account-to =
let difference = initial.account-from.balance - final.account-from.balance
in difference < 10
| else = false
To simply type-check your code:
$ juvix typecheck vp.ju -b llvm
To compile your code to a LLVM .ll
file, please run the following command:
$ juvix compile vp.ju vp.ll -b llvm
()
More examples of Juvix programs can be found in the examples
folder.
We have plenty of examples in the folder test
. To test Juvix against
these examples, please run the command:
$ make test
To open a REPL , you can run one the following commands:
$ make repl-lib # REPL with the library scoped
$ make repl-exe # REPL with the executable scoped
This is a software released for experimentation and research purposes only. Do not expect API stability. Expect divergence from canonical protocol implementations. No warranty is provided or implied.
We welcome contributions to the development of Juvix. See CONTRIBUTING.md for contribution guidelines.
We would love to hear what you think of Juvix! Join our community: