Lib.rs

› Development tools › Cargo plugins
#formal-verification #hax #translation #specification #specification-language #ast #coq

hax-cli-options

hax cli options

by Franziskus Kiefer, Lucas Franceschino, karthikbhargavan, Lasse Letager Hansen, jschneider-bensch, Son HO and 11 contributors

1 unstable release

0.1.0-pre.1 Oct 23, 2023

#337 in Cargo plugins


Used in 2 crates

Apache-2.0

28KB
356 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 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.
  • The subcommand cargo hax takes options, list them with cargo hax --help.
  • The subcommand cargo hax into takes also options, list them with cargo 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 create fst modules in the directory hax/extraction/fstar.
      Note: replace fstar by your backend of choice

  • Install the tool: nix profile install github:hacspec/hacspec-v2

    • then run cargo hax --help anywhere
Using Docker
  1. Clone this repo: git clone git@github.com:hacspec/hacspec-v2.git && cd hacspec-v2
  2. Build the docker image: docker build -f .docker/Dockerfile . -t hacspec-v2
  3. Get a shell: docker run -it --rm -v /some/dir/with/a/crate:/work hacspec-v2 bash
  4. You can now run cargo-hax --help (notice here we use cargo-hax instead of cargo hax)
Manual installation
  1. Make sure to have the following installed on your system:
  • opam (opam switch create 4.14.1)
  • rustup
  • nodejs
  • jq
  1. Clone this repo: git clone git@github.com:hacspec/hacspec-v2.git && cd hacspec-v2
  2. Run the setup.sh script: ./setup.sh.
  3. 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 (see engine/backends/).
  • cli/: the hax 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 the TARGET part (TARGET is either rust or ocaml).

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.8–2.8MB
~54K SLoC