• MiniJuvix
  • Description
  • Quick Start
  • Testing
    • Dependencies
    • Running
  • Usage Example
  • Other Documentation
  • Community

MiniJuvix

<a href="https://github.com/heliaxdev/minijuvix/blob/main/LICENSE"> <img alt="LICENSE" src="" /> </a>

<a href="https://github.com/heliaxdev/MiniJuvix/actions/workflows/ci.yml"> <img alt="CI status" src="" /> </a>

<a href="https://github.com/heliaxdev/minijuvix/tags"> <img alt="" src="https://img.shields.io/github/v/release/heliaxdev/minijuvix?include_prereleases" /> </a>

Description

MiniJuvix is a programming language for writing efficient formally-verified validity predicates, which can be deployed to various distributed ledgers. This is software released for experimentation and research purposes only. No warranty is provided or implied.

MiniJuvix addresses many issues that we have experienced while trying to write and deploy decentralized applications present in the ecosystem of smart-contracts:

• the difficulty of adequate program verification,
• the ceiling of compositional complexity,
• the illegibility of execution costs, and
• the lock-in to particular backends.

Quick Start

To install MiniJuvix, you can download its sources using Git from the Github repository. Then, the program can be downloaded and installed with the following commands. You will need to have Stack installed.

git clone https://github.com/heliaxdev/minijuvix.git
cd minijuvix
stack install

If the installation succeeds, you must be able to run the minijuvix command from any location. To get the complete list of commands, please run minijuvix --help.

Testing

Dependencies

The following dependencies are required for the WASM compiler tests.

• wasmer
• Clang / LLVM (NB: On macOS the preinstalled clang does not support the wasm target so use brew install llvm instead for example)
• wasi-sdk
• wasm-ld - the LLVM linker for WASM (NB: On linux you may need to install the lld package, on macOS this is installed as part of llvm).

To install wasi-sdk you need to download libclang_rt and wasi-sysroot precompiled archives from the wasi-sdk release page and:

1. Extract the libclang_rt.builtins-wasm32-wasi-*.tar.gz archive in the clang installation root (for example /usr/lib/clang/13 on Ubuntu or `brew --prefix llvm` on macos).

   For example on macos with homebrew clang:

   cd `brew --prefix llvm`
   curl https://github.com/WebAssembly/wasi-sdk/releases/download/wasi-sdk-15/libclang_rt.builtins-wasm32-wasi-15.0.tar.gz -OL
   tar xf libclang_rt.builtins-wasm32-wasi-15.0.tar.gz

2. Extract the wasi-sysroot-*.tar.gz archive on your local system and set WASI_SYSROOT_PATH to its path.

   For example:

   cd ~
   curl https://github.com/WebAssembly/wasi-sdk/releases/download/wasi-sdk-15/wasi-sysroot-15.0.tar.gz -OL
   tar xf wasi-sysroot-15.0.tar.gz
   export WASI_SYSROOT_PATH=~/wasi-sysroot

Running

Run tests using:

stack test

To run tests, ignoring all the WASM tests:

stack test --ta '-p "! /slow tests/"'

Usage Example

In the following example a MiniJuvix file is compiled using the C backend. The result is compiled to WASM using Clang and then executed using wasmer.

NB: Set the WASI_SYSROOT_PATH environment variable to the root of the WASI sysroot. See Dependencies for instructions on how to install the sysroot.

cd tests/positive/MiniC/HelloWorld
minijuvix minic Input.mjuvix | clang --target=wasm32-wasi -nodefaultlibs -lc --sysroot $WASI_SYSROOT_PATH -I../../../../minic-runtime/libc -x c - -o out.wasm && wasmer out.wasm

hello world!

Other Documentation

Developer Tooling

Community

We would love to hear what you think of MiniJuvix! Join us on Discord