Skip to the content.

🔗 GitHub | 📖 Book | 📝 Blog | 💬 Zulip | 🛠️ Internal docs | 🛝 Playground

Hax

hax is a tool for high assurance translations that translates a large subset of Rust into formal languages such as F* or Coq. This extends the scope of the hacspec project, which was previously a DSL embedded in Rust, to a usable tool for verifying Rust programs.

So what is hacspec now?

hacspec is the functional subset of Rust that can be used, together with a hacspec standard library, to write succinct, executable, and verifiable specifications in Rust. These specifications can be translated into formal languages with hax.

Try out hax online now!

Learn more

Here are some resources for learning more about hax:

Usage

Hax is a cargo subcommand. The command cargo hax accepts the following subcommands:

Note:

Installation

Manual installation
  1. Make sure to have the following installed on your system:
  1. Clone this repo: git clone git@github.com:hacspec/hax.git && cd hax
  2. Run the setup.sh script: ./setup.sh.
  3. Run cargo-hax --help
Nix

This should work on Linux, MacOS and Windows.

Prerequisites: Nix package manager (with flakes enabled)
  • Either using the Determinate Nix Installer, with the following bash one-liner:
    curl --proto '=https' --tlsv1.2 -sSf -L https://install.determinate.systems/nix | sh -s -- install
    
  • or following those steps.
Using Docker
  1. Clone this repo: git clone git@github.com:hacspec/hax.git && cd hax
  2. Build the docker image: docker build -f .docker/Dockerfile . -t hax
  3. Get a shell: docker run -it --rm -v /some/dir/with/a/crate:/work hax bash
  4. You can now run cargo-hax --help (notice here we use cargo-hax instead of cargo hax)

Supported Subset of the Rust Language

Hax intends to support full Rust, with the two following exceptions, promoting a functional style:

  1. no unsafe code (see https://github.com/hacspec/hax/issues/417);
  2. mutable references (aka &mut T) on return types or when aliasing (see https://github.com/hacspec/hax/issues/420).

Each unsupported Rust feature is documented as an issue labeled unsupported-rust. When the issue is labeled wontfix-v1, that means we don't plan on supporting that feature soon.

Quicklinks:

Hacking on Hax

The documentation of the internal crate of hax and its engine can be found here.

Edit the sources (Nix)

Just clone & cd into the repo, then run nix develop .. You can also just use direnv, with editor integration.

Structure of this repository

Compiling, formatting, and more

We use the just command runner. If you use Nix, the dev shell provides it automatically, if you don't use Nix, please install just on your system.

Anywhere within the repository, you can build and install in PATH (1) the Rust parts with just rust, (2) the OCaml parts with just ocaml or (3) both with just build. More commands (e.g. just fmt to format) are available, please run just or just --list to get all the commands.

Publications & Other material

Secondary literature, using hacspec:

Contributing

Before starting any work please join the Zulip chat, start a discussion on Github, or file an issue to discuss your contribution.

Acknowledgements

Zulip graciously provides the hacspec & hax community with a "Zulip Cloud Standard" tier.