Hax

hax is a tool for high assurance translations of a large subset of Rust into formal languages such as F* or Rocq.

<a href="https://hax-playground.cryspen.com/#fstar+tc/latest-main/gist=5252f86237adbca7fdeb7a8fea0b1648"> Try out hax online now! </a>

Supported Backends

<table align="center"> <tr> <td align="center" colspan="3"> General purpose proof assistants </td> <td align="center" colspan="2"> Cryptography & protocols </td> </tr> <tr> <td align="center"> <a href="https://www.fstar-lang.org/"> F*  </a> </td> <td align="center"> <a href="https://rocq-prover.org/"> <picture> <source srcset=".github/assets/rocq-dark.svg" media="(prefers-color-scheme: dark)"> <source srcset=".github/assets/rocq-light.svg" media="(prefers-color-scheme: light)"> <img src=".github/assets/rocq-light.svg" height="18" alt="Rocq"> </picture> </a> </td> <td align="center" style="vertical-align: center; "> <a href="https://lean-lang.org/"> <picture> <source srcset=".github/assets/lean-dark.svg" media="(prefers-color-scheme: dark)"> <source srcset=".github/assets/lean-light.svg" media="(prefers-color-scheme: light)"> <img src=".github/assets/lean-light.svg" height="18" alt="Lean"> </picture> </a> </td> <td align="center"> <a href="https://github.com/SSProve/ssprove"> <picture> <source srcset=".github/assets/ssprove-dark.svg" media="(prefers-color-scheme: dark)"> <source srcset=".github/assets/ssprove-light.svg" media="(prefers-color-scheme: light)"> <img src=".github/assets/ssprove-light.svg" height="18" alt="SSProve"> </picture> </a> </td> <td align="center"> <a href="https://proverif.inria.fr/"> ProVerif </a> </td> </tr> <tr>  <td align="center">🟢 stable</td> <td align="center">🟡 partial</td> <td align="center">🚀 active dev.</td> <td align="center">🟡 partial</td> <td align="center">🟠 PoC</td> </tr> </table>

Learn more

Here are some resources for learning more about hax:

Manual (work in progress)
- Quick start: F*, Lean
- Tutorial: F*, Lean
Examples: the examples directory contains a set of examples that show what hax can do for you.
Other specifications of cryptographic protocols.

Questions? Join us on Zulip or open a GitHub Discussion. For bugs, file an Issue.

Usage

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

into (cargo hax into BACKEND): translate a Rust crate to the backend BACKEND (e.g. fstar, coq, lean).
json (cargo hax json): extract the typed AST of your crate as a JSON file.

Note:

BACKEND can be fstar, lean, coq, easycrypt or pro-verif. cargo hax into --help gives the full list of supported backends.
The subcommands cargo hax, cargo hax into and cargo hax into <BACKEND> takes options. For instance, you can cargo hax into fstar --z3rlimit 100. Use --help on those subcommands to list all options.

Installation

<details> <summary>Manual installation</summary>

Make sure to have the following installed on your system:

opam (opam switch create 5.1.1)
rustup
nodejs
jq

Clone this repo: git clone git@github.com:cryspen/hax.git && cd hax
Run the setup.sh script: ./setup.sh.
Run cargo-hax --help

</details> <details> <summary>Nix</summary>

This should work on Linux, MacOS and Windows.

<details> <summary>Prerequisites: <a href="https://nixos.org/">Nix package manager</a> (with <a href="https://nixos.wiki/wiki/Flakes">flakes</a> enabled)</summary>

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.

</details>

Run hax on a crate directly to get F*/Coq/Lean/... (assuming you are in the crate's folder):
- nix run github:hacspec/hax -- into fstar extracts F*.
Install hax: nix profile install github:hacspec/hax, then run cargo hax --help anywhere
Note: in any of the Nix commands above, replace github:hacspec/hax by ./dir to compile a local checkout of hax that lives in ./some-dir
Setup binary cache: using Cachix, just cachix use hax

</details> <details> <summary>Using Docker</summary>

Clone this repo: git clone git@github.com:hacspec/hax.git && cd hax
Build the docker image: docker build -f .docker/Dockerfile . -t hax
Get a shell: docker run -it --rm -v /some/dir/with/a/crate:/work hax bash
You can now run cargo-hax --help (notice here we use cargo-hax instead of cargo hax)

Note: Please make sure that $HOME/.cargo/bin is in your $PATH, as that is where setup.sh will install hax.

</details>

Supported Subset of the Rust Language

Hax intends to support full Rust, with the one exception, promoting a functional style: mutable references (aka &mut T) on return types or when aliasing (see https://github.com/hacspec/hax/issues/420) are forbidden.

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 for the engine and here for the frontend.

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

rust-frontend/: Rust library that hooks in the rust compiler and extract its internal typed abstract syntax tree THIR as JSON.
engine/: the simplification and elaboration engine that translates programs from the Rust language to various backends (see engine/backends/). Written in OCaml.
rust-engine/: an on-going rewrite of our engine from OCaml to Rust.
cli/: the hax subcommand for Cargo.

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.

Hax

Install / Use

README

Hax