1 unstable release
0.1.0-pre.1 | Oct 23, 2023 |
---|
#335 in Cargo plugins
Used in 2 crates
19KB
332 lines
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.
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
oreasycrypt
. The list of supported backends can be displayed runningcargo hax into --help
.- The subcommand
cargo hax
takes options, list them withcargo hax --help
. - The subcommand
cargo hax into
takes also options, list them withcargo hax into --help
.
Installation
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/crate
nix run github:hacspec/hacspec-v2 -- into fstar
will createfst
modules in the directoryhax/extraction/fstar
.
Note: replacefstar
by your backend of choice
-
Install the tool:
nix profile install github:hacspec/hacspec-v2
- then run
cargo hax --help
anywhere
- then run
Using Docker
- Clone this repo:
git clone git@github.com:hacspec/hacspec-v2.git && cd hacspec-v2
- Build the docker image:
docker build -f .docker/Dockerfile . -t hacspec-v2
- Get a shell:
docker run -it --rm -v /some/dir/with/a/crate:/work hacspec-v2 bash
- You can now run
cargo-hax --help
(notice here we usecargo-hax
instead ofcargo hax
)
Manual installation
- Make sure to have the following installed on your system:
opam
(opam switch create 4.14.1
)rustup
nodejs
jq
- Clone this repo:
git clone git@github.com:hacspec/hacspec-v2.git && cd hacspec-v2
- Run the setup.sh script:
./setup.sh
. - Run
cargo-hax --help
Examples
There's a set of examples that show what hax can do for you. Please check out the examples directory
Hacking on Hax
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 simplication and elaboration engine that translate 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:
Contributing
Before starting any work please join the Zulip chat, start a discussion on Github, or file an issue to discuss your contribution.
Dependencies
~1–11MB
~80K SLoC