diff --git a/README.md b/README.md index 7984d4c6a..56fdeb0a1 100644 --- a/README.md +++ b/README.md @@ -3,27 +3,25 @@

- 🌐 Website | - 📖 Book | - 📝 Blog | + 🌐 Website | + 📝 Blog | 💬 Zulip | - 🛠️ Internal docs | 🛝 Playground

# Hax -hax is a tool for high assurance translations that translates a large subset of -Rust into formal languages such as [F\*](https://www.fstar-lang.org/) or [Coq](https://coq.inria.fr/). -This extends the scope of the hacspec project, which was previously a DSL embedded in Rust, -to a usable tool for verifying Rust programs. +hax is a tool for high assurance translations of a large subset of +Rust into formal languages such as [F\*](https://www.fstar-lang.org/) or [Rocq](https://rocq-prover.org/). -> So what is hacspec now? +
+ 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. +

@@ -34,9 +32,9 @@ These specifications can be translated into formal languages with hax. ## Learn more Here are some resources for learning more about hax: - - [Book](https://hacspec.org/book) (work in progress) - + [Quick start](https://hacspec.org/book/quick_start/intro.html) - + [Tutorial](https://hacspec.org/book/tutorial/index.html) + - [Manual](https://hax.cryspen.com/manual/index.html) (work in progress) + + [Quick start](https://hax.cryspen.com/manual/quick_start/index.html) + + [Tutorial](https://hax.cryspen.com/manual/tutorial/index.html) - [Examples](./examples/): the [examples directory](./examples/) contains a set of examples that show what hax can do for you. - Other [specifications](https://github.com/hacspec/specs) of cryptographic protocols. @@ -123,7 +121,8 @@ Quicklinks: ## Hacking on Hax The documentation of the internal crate of hax and its engine can be -found [here](https://hacspec.org/hax/). +found [here for the engine](https://hax.cryspen.com/engine/index.html) +and [here for the frontent](https://hax.cryspen.com/frontend/index.html). ### Edit the sources (Nix) diff --git a/docs/index.md b/docs/index.md index 824e07f98..2bf6412cd 100644 --- a/docs/index.md +++ b/docs/index.md @@ -2,3 +2,5 @@ hax is a tool for high assurance translations of a large subset of Rust into formal languages such as [F\*](https://www.fstar-lang.org/) or [Rocq](https://rocq-prover.org/). + +Head over to the [Manual](./manual/index.md) to get started! diff --git a/docs/manual/index.md b/docs/manual/index.md index 2c29acec3..eacda1c2f 100644 --- a/docs/manual/index.md +++ b/docs/manual/index.md @@ -4,15 +4,68 @@ weight: -5 # Introduction -hax is a tool for high assurance translations that translates a large subset of -Rust into formal languages such as [F\*](https://www.fstar-lang.org/) or [Coq](https://coq.inria.fr/). -This extends the scope of the hacspec project, which was previously a DSL embedded in Rust, -to a usable tool for verifying Rust programs. +hax is a tool for high assurance translations of a large subset of +Rust into formal languages such as [F\*](https://www.fstar-lang.org/) or [Rocq](https://rocq-prover.org/). -> So what is **hacspec** now? +## Usage -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`, `easycrypt` or `pro-verif`. `cargo hax into --help` + gives the full list of supported backends. +* The subcommands `cargo hax`, `cargo hax into` and `cargo hax into + ` takes options. For instance, you can `cargo hax into + fstar --z3rlimit 100`. Use `--help` on those subcommands to list + all options. + +## Installation + +### Manual installation + +1. Make sure to have the following installed on your system: + + - [`opam`](https://opam.ocaml.org/) (`opam switch create 5.1.1`) + - [`rustup`](https://rustup.rs/) + - [`nodejs`](https://nodejs.org/) + - [`jq`](https://jqlang.github.io/jq/) + +2. Clone this repo: `git clone git@github.com:hacspec/hax.git && cd hax` +3. Run the [setup.sh](./setup.sh) script: `./setup.sh`. +4. Run `cargo-hax --help` + +### Nix + +This should work on [Linux](https://nixos.org/download.html#nix-install-linux), [MacOS](https://nixos.org/download.html#nix-install-macos) and [Windows](https://nixos.org/download.html#nix-install-windows). + +Prerequisites: Nix package +manager (with flakes enabled) + + - Either using the [Determinate Nix Installer](https://github.com/DeterminateSystems/nix-installer), with the following bash one-liner: + ```bash + curl --proto '=https' --tlsv1.2 -sSf -L https://install.determinate.systems/nix | sh -s -- install + ``` + - or following [those steps](https://github.com/mschwaig/howto-install-nix-with-flake-support). + ++ **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 run `cargo 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](https://app.cachix.org/cache/hax), just `cachix use hax` + +### Docker + +1. Clone this repo: `git clone git@github.com:hacspec/hax.git && cd hax` +2. Build the docker image: `docker build -f .docker/Dockerfile . -t hax` +3. Get a shell: `docker run -it --rm -v /some/dir/with/a/crate:/work hax bash` +4. You can now run `cargo-hax --help` (notice here we use `cargo-hax` instead of `cargo hax`) + +Note: Please make sure that `$HOME/.cargo/bin` is in your `$PATH`, as +that is where `setup.sh` will install hax. diff --git a/docs/publications.md b/docs/publications.md new file mode 100644 index 000000000..bfcd23a56 --- /dev/null +++ b/docs/publications.md @@ -0,0 +1,16 @@ +--- +weight: 5 +--- + +# Publications + +* [📕 hacspec Tech report](https://hal.inria.fr/hal-03176482) +* [📕 HACSpec: A gateway to high-assurance cryptography](https://github.com/hacspec/hacspec/blob/master/rwc2023-abstract.pdf) +* [📕 Original hacspec paper](https://www.franziskuskiefer.de/publications/hacspec-ssr18-paper.pdf) + +### Secondary literature, using hacspec & hax: +* [📕 Last yard](https://eprint.iacr.org/2023/185) +* [📕 A Verified Pipeline from a Specification Language to Optimized, Safe Rust](https://github.com/hacspec/hacspec.github.io/blob/master/coqpl22-final61.pdf) at [CoqPL'22](https://popl22.sigplan.org/details/CoqPL-2022-papers/5/A-Verified-Pipeline-from-a-Specification-Language-to-Optimized-Safe-Rust) +* [📕 Hax - Enabling High Assurance Cryptographic Software](https://github.com/hacspec/hacspec.github.io/blob/master/RustVerify24.pdf) at [RustVerify24](https://sites.google.com/view/rustverify2024) +* [📕 A formal security analysis of Blockchain voting](https://github.com/hacspec/hacspec.github.io/blob/master/coqpl24-paper8-2.pdf) at [CoqPL'24](https://popl24.sigplan.org/details/CoqPL-2024-papers/8/A-formal-security-analysis-of-Blockchain-voting) +* [📕 Specifying Smart Contract with Hax and ConCert](https://github.com/hacspec/hacspec.github.io/blob/master/coqpl24-paper9-13.pdf) at [CoqPL'24](https://popl24.sigplan.org/details/CoqPL-2024-papers/9/Specifying-Smart-Contract-with-Hax-and-ConCert)