Merge pull request #1263 from cryspen/franziskus/website-update2

updatge readme and docs

README.md

@@ -3,27 +3,25 @@
 </p>
 
 <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://hax.cryspen.com/">🌐 Website</a> |
+  <a href="https://hax.cryspen.com/blog">📝 Blog</a> |
   <a href="https://hacspec.zulipchat.com/">💬 Zulip</a> |
-  <a href="https://hacspec.org/hax/">🛠️ Internal docs</a> |
   <a href="https://hax-playground.cryspen.com/">🛝 Playground</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/).
-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?
+<details>
+<summary> So what is hacspec now?</summary>
 
 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.
+</details>
 
 <p align="center">
     <a href="https://hax-playground.cryspen.com/#fstar+tc/latest-main/gist=5252f86237adbca7fdeb7a8fea0b1648">
@@ -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)
 

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!

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
+   <BACKEND>` 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 [email protected]: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).
+
+<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>
+
+  - 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 [email protected]: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.
 

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)