๐ GitHub | ๐ Book | ๐ Blog | ๐ฌ Zulip | ๐ ๏ธ Internal docs
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.
Learn more
Here are some resources for learning more about hax:
- Book (work in progress)
- Examples: the examples directory contains a set of examples that show what hax can do for you.
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 backendBACKEND
(e.g.fstar
,coq
).json
(cargo hax json
): extract the typed AST of your crate as a JSON file.
Note:
BACKEND
can befstar
,coq
,easycrypt
orpro-verif
.cargo hax into --help
gives the full list of supported backends.- The subcommands
cargo hax
,cargo hax into
and `cargo hax into` takes options. For instance, you can `cargo hax into fstar --z3rlimit 100`. Use `--help` on those subcommands to list all options.
Installation
Manual installation
1. Make sure to have the following installed on your system: - [`opam`](https://opam.ocaml.org/) (`opam switch create 4.14.1`) - [`rustup`](https://rustup.rs/) - [`nodejs`](https://nodejs.org/) - [`jq`](https://jqlang.github.io/jq/) 2. Clone this repo: `git clone git@github.com:hacspec/hax.git && cd hax` 3. Run the [setup.sh](./setup.sh) script: `./setup.sh`. 4. Run `cargo-hax --help`Nix
This should work on [Linux](https://nixos.org/download.html#nix-install-linux), [MacOS](https://nixos.org/download.html#nix-install-macos) and [Windows](https://nixos.org/download.html#nix-install-windows).Prerequisites: Nix package manager (with flakes enabled)
- Either using the [Determinate Nix Installer](https://github.com/DeterminateSystems/nix-installer), with the following bash one-liner: ```bash curl --proto '=https' --tlsv1.2 -sSf -L https://install.determinate.systems/nix | sh -s -- install ``` - or following [those steps](https://github.com/mschwaig/howto-install-nix-with-flake-support).Using Docker
1. Clone this repo: `git clone git@github.com:hacspec/hax.git && cd hax` 3. Build the docker image: `docker build -f .docker/Dockerfile . -t hax` 4. Get a shell: `docker run -it --rm -v /some/dir/with/a/crate:/work hax bash` 5. 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:
- no
unsafe
code (see https://github.com/hacspec/hax/issues/417); - 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
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 (seeengine/backends/
).cli/
: thehax
subcommand for Cargo.
Recompiling
You can use the .utils/rebuild.sh
script (which is available automatically as the command rebuild
when using the Nix devshell):
rebuild
: rebuild the Rust then the OCaml part;rebuild TARGET
: rebuild theTARGET
part (TARGET
is eitherrust
orocaml
).
Publications & Other material
Secondary literature, using hacspec:
- ๐ Last yard
- ๐ A Verified Pipeline from a Specification Language to Optimized, Safe Rust at CoqPLโ22
- ๐ Last yard
- ๐ A formal security analysis of Blockchain voting at CoqPLโ24
- ๐ Specifying Smart Contract with Hax and ConCert at CoqPLโ24
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.