Readme update

README.md

@@ -1,4 +1,14 @@
-# Hax 
+<!-- WARNING: a GitHub action periodically replaces this file with https://github.com/hacspec/hax/blob/main/README.md. Do not make any modification to this file, instead make a PR to https://github.com/hacspec/hax/blob/main/README.md -->
+
+<p align="center">
+  <a href="https://hacspec.org/">🌐 Website</a> |
+  <a href="https://hacspec.org/book">📖 Book</a> |
+  <a href="https://hacspec.org/blog">📝 Blog</a> |
+  <a href="https://hacspec.zulipchat.com/">💬 Zulip</a> |
+  <a href="https://hacspec.org/hax/">🛠️ Internal docs</a>
+</p>
+
+# 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/).
@@ -12,7 +22,14 @@ standard library, to write succinct, executable, and verifiable specifications i
 Rust.
 These specifications can be translated into formal languages with hax.
 
-[![GitHub](https://img.shields.io/badge/Github-Repository-blue.svg?style=for-the-badge&logo=github)](https://github.com/hacspec/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)
+ - [Examples](examples/): the [examples directory](examples/) contains
+   a set of examples that show what hax can do for you.
 
 ## Usage
 Hax is a cargo subcommand. 
@@ -21,60 +38,82 @@ The command `cargo hax` accepts the following subcommands:
  * **`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`.
+ * `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
+   <BACKEND>` takes options. For instance, you can `cargo hax into
+   fstar --z3rlimit 100`. Use `--help` on those subcommands to list
+   all options.
 
 ## Installation
-### Nix
+<details>
+  <summary><b>Manual installation</b></summary>
+
+1. Make sure to have the following installed on your system:
+
+- [`opam`](https://opam.ocaml.org/) (`opam switch create 4.14.1`)
+- [`rustup`](https://rustup.rs/)
+- [`nodejs`](https://nodejs.org/)
+- [`jq`](https://jqlang.github.io/jq/)
+
+2. Clone this repo: `git clone [email protected]:hacspec/hax.git && cd hax`
+3. Run the [setup.sh](./setup.sh) script: `./setup.sh`.
+4. Run `cargo-hax --help`
+
+</details>
+
+<details>
+  <summary><b>Nix</b></summary>
 
  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](https://nixos.org) _(with [flakes](https://nixos.wiki/wiki/Flakes) enabled)_
+<details>
+  <summary><b>Prerequisites:</b> <a href="https://nixos.org/">Nix package
+manager</a> <i>(with <a href="https://nixos.wiki/wiki/Flakes">flakes</a> enabled)</i></summary>
 
   - 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 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*
+</details>
 
-+ Install the tool:  `nix profile install github:hacspec/hacspec-v2`
-   - then run `cargo hax --help` anywhere
++ **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*.
 
-### Using Docker
++ **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`
 
-1. Clone this repo: `git clone [email protected]:hacspec/hacspec-v2.git && cd hacspec-v2`
-3. Build the docker image: `docker build -f .docker/Dockerfile . -t hacspec-v2`
-4. Get a shell: `docker run -it --rm -v /some/dir/with/a/crate:/work hacspec-v2 bash`
-5. You can now run `cargo-hax --help` (notice here we use `cargo-hax` instead of `cargo hax`)
+</details>
 
-### Manual installation
+<details>
+  <summary><b>Using Docker</b></summary>
 
-1. Make sure to have the following installed on your system:
+1. Clone this repo: `git clone [email protected]:hacspec/hax.git && cd hax`
+3. Build the docker image: `docker build -f .docker/Dockerfile . -t hax`
+4. Get a shell: `docker run -it --rm -v /some/dir/with/a/crate:/work hax bash`
+5. You can now run `cargo-hax --help` (notice here we use `cargo-hax` instead of `cargo hax`)
 
-- `opam` (`opam switch create 4.14.1`)
-- `rustup`
-- `nodejs`
-- `jq`
+</details>
 
-2. Clone this repo: `git clone [email protected]:hacspec/hacspec-v2.git && cd hacspec-v2`
-3. Run the [setup.sh](./setup.sh) script: `./setup.sh`.
-4. Run `cargo-hax --help`
+## Supported Subset of the Rust Language
+
+Hax intends to support full Rust, with the two following exceptions, promoting a functional style:
+ 1. no `unsafe` code (see https://github.com/hacspec/hax/issues/417);
+ 2. mutable references (aka `&mut T`) on return types or when aliasing (see https://github.com/hacspec/hax/issues/420).
 
-## Examples
+Each unsupported Rust feature is documented as an issue labeled [`unsupported-rust`](https://github.com/hacspec/hax/issues?q=is%3Aissue+is%3Aopen+label%3Aunsupported-rust). When the issue is labeled [`wontfix-v1`](https://github.com/hacspec/hax/issues?q=is%3Aissue+is%3Aopen+label%3Aunsupported-rust+label%3Awontfix%2Cwontfix-v1), that means we don't plan on supporting that feature soon.
 
-There's a set of examples that show what hax can do for you.
-Please check out the [examples directory](https://github.com/hacspec/hax/tree/main/examples)
+Quicklinks:
+ - [🔨 Rejected rust we want to support](https://github.com/hacspec/hax/issues?q=is%3Aissue+is%3Aopen+label%3Aunsupported-rust+-label%3Awontfix%2Cwontfix-v1);
+ - [💭 Rejected rust we don't plan to support in v1](https://github.com/hacspec/hax/issues?q=is%3Aissue+is%3Aopen+label%3Aunsupported-rust+label%3Awontfix%2Cwontfix-v1).
 
 ## Hacking on Hax
+The documentation of the internal crate of hax and its engine can be
+found [here](https://hacspec.org/hax/).
+
 ### Edit the sources (Nix)
 
 Just clone & `cd` into the repo, then run `nix develop .`.
@@ -85,23 +124,23 @@ You can also just use [direnv](https://github.com/nix-community/nix-direnv), wit
 - `rust-frontend/`: Rust library that hooks in the rust compiler and
   extract its internal typed abstract syntax tree
   [**THIR**](https://rustc-dev-guide.rust-lang.org/thir.html) as JSON.
-- `engine/`: the simplication and elaboration engine that translate
+- `engine/`: the simplification and elaboration engine that translates
   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`](https://github.com/hacspec/hax/tree/main/.utils/rebuild.sh) script (which is available automatically as the command `rebuild` when using the Nix devshell):
+You can use the [`.utils/rebuild.sh`](./.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
 
 * [📕 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)
-* [📕 Hax - Enabling High Assurance Cryptographic Software](https://github.com/hacspec/hacspec.github.io/blob/master/RustVerify24.pdf) at [RustVerify'24](https://sites.google.com/view/rustverify2024)
-* [📕 Original hacspec paper](https://www.franziskuskiefer.de/publications/hacspec-ssr18-paper.pdf)  
+* [📕 Original hacspec paper](https://www.franziskuskiefer.de/publications/hacspec-ssr18-paper.pdf)
 
 ### Secondary literature, using hacspec:
+* [📕 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)
 * [📕 Last yard](https://eprint.iacr.org/2023/185)
 * [📕 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)
@@ -113,3 +152,10 @@ Before starting any work please join the [Zulip chat][chat-link], start a [discu
 
 
 [chat-link]: https://hacspec.zulipchat.com
+
+## Acknowledgements
+
+[Zulip] graciously provides the hacspec & hax community with a "Zulip Cloud Standard" tier.
+
+
+[Zulip]: https://zulip.com/