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.
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:
BACKENDcan befstar,coqoreasycrypt.cargo hax into --helpgives the full list of supported backends.- The subcommands
cargo hax,cargo hax intoandcargo hax into <BACKEND>takes options. For instance, you cancargo hax into fstar --z3rlimit 100. Use--helpon those subcommands to list all options.
Manual installation
- Make sure to have the following installed on your system:
- Clone this repo:
git clone git@github.com:hacspec/hax.git && cd hax - Run the setup.sh script:
./setup.sh. - 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.
-
Run hax on a crate to get F*/Coq/...:
cd path/to/your/cratenix run github:hacspec/hax -- into fstarwill createfstmodules in the directoryhax/extraction/fstar. Note: replacefstarby your backend of choice
-
Install the tool:
nix profile install github:hacspec/hax- then run
cargo hax --helpanywhere
- then run
Using Docker
- 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 usecargo-haxinstead ofcargo hax)
There's a set of examples that show what hax can do for you. Please check out the examples directory
Just clone & cd into the repo, then run nix develop ..
You can also just use direnv, with editor integration.
rust-frontend/: Rust library that hooks in the rust compiler and extract its internal typed abstract syntax tree THIR as JSON.engine/: the simplication and elaboration engine that translate programs from the Rust language to various backends (seeengine/backends/).cli/: thehaxsubcommand for Cargo.
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 theTARGETpart (TARGETis eitherrustorocaml).
Before starting any work please join the Zulip chat, start a discussion on Github, or file an issue to discuss your contribution.