Crates.io | hax-frontend-exporter-options |
lib.rs | hax-frontend-exporter-options |
version | 0.1.0-pre.1 |
source | src |
created_at | 2023-10-20 12:40:38.136875 |
updated_at | 2023-10-20 12:40:38.136875 |
description | hax frontend options |
homepage | https://github.com/hacspec/hax |
repository | https://github.com/hacspec/hax |
max_upload_size | |
id | 1008924 |
size | 8,301 |
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 backend BACKEND
(e.g. fstar
, coq
).json
(cargo hax json
): extract the typed AST of your crate as a JSON file.Note:
BACKEND
can be fstar
, coq
or easycrypt
. The list of
supported backends can be displayed running cargo hax into --help
.cargo hax
takes options, list them with cargo hax --help
.cargo hax into
takes also options, list them with cargo hax into --help
.This should work on Linux, MacOS and Windows.
curl --proto '=https' --tlsv1.2 -sSf -L https://install.determinate.systems/nix | sh -s -- install
Run hax on a crate to get F*/Coq/...:
cd path/to/your/crate
nix run github:hacspec/hacspec-v2 -- into fstar
fst
modules in the directory hax/extraction/fstar
.fstar
by your backend of choiceInstall the tool: nix profile install github:hacspec/hacspec-v2
cargo hax --help
anywheregit clone git@github.com:hacspec/hacspec-v2.git && cd hacspec-v2
docker build -f .docker/Dockerfile . -t hacspec-v2
docker run -it --rm -v /some/dir/with/a/crate:/work hacspec-v2 bash
cargo-hax --help
(notice here we use cargo-hax
instead of cargo hax
)opam
(opam switch create 4.14.1
)rustup
nodejs
jq
git clone git@github.com:hacspec/hacspec-v2.git && cd hacspec-v2
./setup.sh
.cargo-hax --help
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 (see engine/backends/
).cli/
: the hax
subcommand 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 the TARGET
part (TARGET
is either rust
or ocaml
).Before starting any work please join the Zulip chat, start a discussion on Github, or file an issue to discuss your contribution.