Introduction
hax is a tool for high assurance translations of a large subset of Rust into formal languages such as F* or Rocq.
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
andcargo hax into <BACKEND>
takes options. For instance, you cancargo hax into fstar --z3rlimit 100
. Use--help
on those subcommands to list all options.
Installation
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:
-
or following those steps.
-
Run hax on a crate directly to get F*/Coq/... (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 runcargo 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
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-hax
instead ofcargo hax
)
Note: Please make sure that $HOME/.cargo/bin
is in your $PATH
, as
that is where setup.sh
will install hax.