Lean tutorial first version.

.github/workflows/clippy_rust_engine.yml

@@ -10,9 +10,12 @@ on:
 jobs:
   clippy:
     name: clippy
-    runs-on: linux
+    runs-on: ubuntu-latest
     steps:
     - uses: actions/checkout@v4
+    - name: Install clippy
+      run: |
+        rustup component add clippy
     - name: Run clippy
       run: |
         cargo clippy -p hax-rust-engine -- -D warnings --no-deps

.github/workflows/rustc-coverage-tests.yml

@@ -9,7 +9,7 @@ on:
 
 jobs:
     rustc-coverage-tests:
-      runs-on: linux
+      runs-on: ubuntu-latest
 
       steps:
         - uses: actions/checkout@v4

CHANGELOG.md

@@ -11,6 +11,9 @@ Change to the Rust Engine:
  - Add a resugaring `FunctionsToConstants` (#1559)
  - Drop the tuple nodes of the AST, add resugaring node for tuples (#1662)
 
+Miscellaneous:
+ - A lean tutorial has been added to the hax website.
+
 ## 0.3.4
 
 The release of `0.3.3` got troubles because of the new Rust Engine crates.

docs/default.nix

@@ -1,6 +1,6 @@
 { stdenv, buildPythonPackage, fetchPypi, setuptools, wheel, mkdocs
 , mkdocs-material, fetchFromGitHub, natsort, wcmatch, hax-frontend-docs
-, hax-engine-docs }:
+, hax-engine-docs, mkdocs-awesome-nav }:
 let
   mkdocs-glightbox = buildPythonPackage rec {
     pname = "mkdocs-glightbox";
@@ -34,7 +34,13 @@ let
 in stdenv.mkDerivation {
   name = "hax-docs";
   src = ./..;
-  buildInputs = [ mkdocs mkdocs-material mkdocs-glightbox mkdocs-nav-weight ];
+  buildInputs = [
+    mkdocs
+    mkdocs-material
+    mkdocs-glightbox
+    mkdocs-nav-weight
+    mkdocs-awesome-nav
+  ];
   buildPhase = ''
     mkdocs build
   '';

docs/javascripts/hax_playground.js

@@ -35,8 +35,9 @@ async function call_playground(result_block, query, text) {
     let ansi_up = new AnsiUp();
     let first = true;
     let logs = document.createElement('div');
-    logs.style = 'font-size: 80%; background: #00000010; padding: 3px;';
+    logs.style = 'font-size: 80%; background: #00000010; padding: 3px; white-space:pre-wrap;';
     let hax_version = await get_latest_hax_main();
+    let lean_backend = query.startsWith('lean');
     raw_query(
         PLAYGROUND_URL,
         hax_version,
@@ -62,7 +63,7 @@ async function call_playground(result_block, query, text) {
                     if (file.endsWith('.rs'))
                         continue;
                     let contents = json.Done.files[file];
-                    contents = contents.split('open FStar.Mul')[1].trim();
+                    contents = (contents.split(lean_backend?'set_option linter.unusedVariables false':'open FStar.Mul')[1] || contents).trim();
                     contents = contents.replace(/$/gm, ' ').trim();
                     out.push([file, contents]);
                 }
@@ -78,11 +79,11 @@ async function call_playground(result_block, query, text) {
                     result.textContent = out.map(([file, s]) => '(* File: ' + file + ' *) \n' + s).join('\n\n').trim();
                 }
                 result_block.appendChild(result);
+                hljs.highlightBlock(result);
+                result_block.innerHTML += `<br/><a style="float:right; font-family: 'Open Sans', sans-serif; font-size: 70%; cursor: pointer; color: gray; text-transform: uppercase; position: relative; top: -10px;" href='${PLAYGROUND_URL}/#${lean_backend?"lean":"fstar"}/${hax_version}/${LZString.compressToEncodedURIComponent(text)}'>Open in hax playground ↗</a>`;
                 if (json.Done.success && query.includes('+tc')) {
-                    result_block.innerHTML += '<div style="float: left; padding: 3px; padding-top: 8px; position: relative; top: 6px;"><span style="color: gray;">Status: </span><span style="color: green">✓ F* successfully typechecked!</span></div>';
+                    result_block.innerHTML += `<div style="float: left; padding: 3px; padding-top: 8px; position: relative; top: 6px;"><span style="color: gray;">Status: </span><span style="color: green">✓ ${lean_backend?"Lean":"F*"} successfully typechecked!</span></div>`;
                 }
-                hljs.highlightBlock(result);
-                result_block.innerHTML += `<br/><a style="float:right; font-family: 'Open Sans', sans-serif; font-size: 70%; cursor: pointer; color: gray; text-transform: uppercase; position: relative; top: -10px;" href='${PLAYGROUND_URL}/#fstar/${hax_version}/${LZString.compressToEncodedURIComponent(text)}'>Open in hax playground ↗</a>`;
             }
         },
     );
@@ -105,6 +106,7 @@ function setup_hax_playground() {
         let w = e.parentElement;
         if (!w.classList.contains("playable"))
             continue;
+        let backend = w.classList.contains("lean-backend")?'lean':'fstar';
 
         code.innerHTML = "<pre></pre>";
         let inner = code.children[0];
@@ -128,14 +130,15 @@ function setup_hax_playground() {
         let header = lines.filter(line => line.startsWith('# ')).map(line => line.slice(2)).join('\n');
         let getCode = () => header + '\n' + editor.state.doc.toString();
 
+
         let button_translate = document.createElement("button");
         button_translate.innerHTML = `<i class="fa-solid fa-play"></i>`;
         button_translate.classList.add('md-icon');
         button_translate.classList.add('md-clipboard');
         button_translate.classList.add('md-hax-playground');
         button_translate.style.right = "2.4em";
         button_translate.onclick = () => {
-            call_playground(result_block, 'fstar', getCode());
+            call_playground(result_block, backend, getCode());
         };
         e.prepend(button_translate);
 
@@ -146,13 +149,10 @@ function setup_hax_playground() {
         button_tc.classList.add('md-hax-playground');
         button_tc.style.right = "4.5em";
         button_tc.onclick = () => {
-            button_tc.onclick = () => {
-                call_playground(result_block, 'fstar+tc', getCode());
-            };
-            e.prepend(button_tc);
+            call_playground(result_block, backend + '+tc', getCode());
+        };
 
-            code.style.padding = "0 0.9em";
-        }
+        e.prepend(button_tc);
     }
 }
 

docs/manual/faq/index.md

@@ -1,5 +1,5 @@
 ---
-weight: 4
+weight: 200
 ---
 
 # Troubleshooting/FAQ

docs/manual/fstar/.nav.yml

@@ -0,0 +1 @@
+title: F*

docs/manual/fstar/index.md

@@ -0,0 +1 @@
+This section introduces the F\* backend of hax. It covers how to setup a project, and the basics of how to use the hax and F\* to verify Rust code.

docs/manual/quick_start/index.md → docs/manual/fstar/quick_start.md

@@ -2,7 +2,7 @@
 weight: 0
 ---
 
-# Quick start with hax and F\*
+# Quick start
 
 Do you want to try hax out on a Rust crate of yours? This chapter is
 what you are looking for!
@@ -11,18 +11,16 @@ what you are looking for!
 
  - <input type="checkbox" class="user-checkable"/> [Install the hax toolchain](https://github.com/hacspec/hax?tab=readme-ov-file#installation).  
    <span style="margin-right:30px;"></span>🪄 Running `cargo hax --version` should print some version info.
- - <input type="checkbox" class="user-checkable"/> [Install F\*](https://github.com/FStarLang/FStar/blob/master/INSTALL.md) *(optional: only if want to run F\*)*
+ - <input type="checkbox" class="user-checkable"/> [Install F\*](https://github.com/FStarLang/FStar/blob/master/INSTALL.md)
 
 ## Setup the crate you want to verify
 
 *Note: the instructions below assume you are in the folder of the specific crate (**not workspace!**) you want to extract.*
 
-*Note: this part is useful only if you want to run F\*.*
 
-
- - <input type="checkbox" class="user-checkable"/> Create the folder `proofs/fstar/extraction` folder, right next to the `Cargo.toml` of the crate you want to verify.  
+ - <input type="checkbox" class="user-checkable"/> Create the folder `proofs/fstar/extraction`folder, right next to the `Cargo.toml` of the crate you want to verify.  
    <span style="margin-right:30px;"></span>🪄 `mkdir -p proofs/fstar/extraction`
- - <input type="checkbox" class="user-checkable"/> Copy [this makefile](https://gist.github.com/W95Psp/4c304132a1f85c5af4e4959dd6b356c3) to `proofs/fstar/extraction/Makefile`.  
+ - <input type="checkbox" class="user-checkable"/> Copy [this makefile](https://gist.github.com/W95Psp/4c304132a1f85c5af4e4959dd6b356c3) to `proofs/fstar/extraction/Makefile`  
    <span style="margin-right:30px;"></span>🪄 `curl -o proofs/fstar/extraction/Makefile https://gist.githubusercontent.com/W95Psp/4c304132a1f85c5af4e4959dd6b356c3/raw/Makefile`
  - <input type="checkbox" class="user-checkable"/> Add `hax-lib` as a dependency to your crate, enabled only when using hax.  
    <span style="margin-right:30px;"></span>🪄 `cargo add --target 'cfg(hax)' --git https://github.com/hacspec/hax hax-lib`  
@@ -66,8 +64,6 @@ of your crate, say a function `my_crate::f`, is not handled by hax,
 you can append `-my_crate::f` to the `-i` flag. You can learn more
 about the `-i` flag [in the FAQ](../faq/include-flags.md).
 
-
-
 ## Start F\* verification
 After running the hax toolchain on your Rust code, you will end up
 with various F\* modules in the `proofs/fstar/extraction` folder. The

docs/manual/tutorial/data-invariants.md → docs/manual/fstar/tutorial/data-invariants.md

@@ -54,7 +54,7 @@ large enough provided by Rust is `u16`.
 Let's define `F` a
 ["newtype"](https://matklad.github.io/2018/06/04/newtype-index-pattern.html):
 a [struct](https://doc.rust-lang.org/book/ch05-00-structs.html) with
-one `u16` field `v`. Notice the refinment annotation on `v`: the
+one `u16` field `v`. Notice the refinement annotation on `v`: the
 extraction of this type `F` via hax will result in a type enforcing
 `v` small enough.
 

docs/manual/tutorial/index.md → docs/manual/fstar/tutorial/index.md

@@ -9,11 +9,11 @@ programs using the hax toolchain. hax is a tool that translates Rust
 programs to various formal programming languages.
 
 The formal programming languages we target are called *backends*. Some
-of them, e.g. [F\*](https://fstar-lang.org/) or
+of them, e.g. [F\*](https://fstar-lang.org/), [Lean](https://lean-lang.org/) or
 [Coq](https://coq.inria.fr/), are general purpose formal programming
 languages. Others are specialized tools:
 [ProVerif](https://bblanche.gitlabpages.inria.fr/proverif/) is
 dedicated to proving properties about protocols.
 
-This tutorial focuses on proving properties with the
-[F\* programming language](https://fstar-lang.org/).
+This tutorial focuses on proving properties with
+[F\*](https://fstar-lang.org/).

docs/manual/tutorial/panic-freedom.md → docs/manual/fstar/tutorial/panic-freedom.md

@@ -28,6 +28,7 @@ is just over `255`, the largest integer that fits `u8`. Rust does not
 ensure that functions are *total*: a function might panic at any
 point, or might never terminate.
 
+
 ## Rust and panicking code
 Quoting the chapter [To `panic!` or Not to
 `panic!`](https://doc.rust-lang.org/book/ch09-03-to-panic-or-not-to-panic.html)
@@ -91,9 +92,9 @@ erase your disk, or anything.
 
 The helper crate
 [hax-lib](https://github.com/hacspec/hax/tree/main/hax-lib)
-provdes the `requires`
+provides the `requires`
 [proc-macro](https://doc.rust-lang.org/reference/procedural-macros.html)
-which lets user writting pre-conditions directly in Rust.
+which lets user writing pre-conditions directly in Rust.
 
 ```{.rust .playable}
 #[hax_lib::requires(x < 16)]

docs/manual/tutorial/properties.md → docs/manual/fstar/tutorial/properties.md

@@ -123,7 +123,7 @@ In this situation, adding a pre- or a post-condition to either
 `encrypt` or `decrypt` is not useful: we want to state our inverse
 property about both of them. Better, we want this property to be
 stated directly in Rust: just as with pre and post-conditions, the
-Rust souces should clearly state what is to be proven.
+Rust sources should clearly state what is to be proven.
 
 To this end, Hax provides a macro `lemma`. Below, the Rust function
 `encrypt_decrypt_identity` takes a key and a plaintext, and then

docs/manual/index.md

@@ -5,19 +5,19 @@ weight: -5
 # Introduction
 
 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/).
+Rust into formal languages such as [F\*](https://www.fstar-lang.org/), [Lean](https://lean-lang.org/) or [Rocq](https://rocq-prover.org/).
 
 ## 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`).
+* **`into`** (`cargo hax into BACKEND`): translate a Rust crate to the backend `BACKEND` (e.g. `fstar`, `coq`, `lean`).
 * **`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`
+* `BACKEND` can be `fstar`, `coq`, `lean`, `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

docs/manual/lean/index.md

@@ -0,0 +1 @@
+This section introduces the Lean backend of hax. It shows the basic setup to use hax and Lean on a Rust crate, and gives an introduction to the basic features that can be used to make Lean proofs about Rust code.

docs/manual/lean/internals.md

@@ -0,0 +1,8 @@
+---
+weight: 102
+---
+
+
+# Internals
+
+

docs/manual/lean/quick_start.md

@@ -0,0 +1,80 @@
+---
+weight: 100
+---
+
+# Quick start
+
+## Setup the tools
+
+ - <input type="checkbox" class="user-checkable"/> [Install the hax toolchain](https://github.com/hacspec/hax?tab=readme-ov-file#installation).  
+   <span style="margin-right:30px;"></span>🪄 Running `cargo hax --version` should print some version info.
+ - <input type="checkbox" class="user-checkable"/> [Install Lean](https://lean-lang.org/install/)
+  - <input type="checkbox" class="user-checkable"/> Add `hax-lib` as a dependency to your crate, enabled only when using hax.  
+   <span style="margin-right:30px;"></span>🪄 `cargo add --target 'cfg(hax)' --git https://github.com/hacspec/hax hax-lib`  
+   <span style="margin-right:30px;"></span><span style="opacity: 0;">🪄</span> *(`hax-lib` is not mandatory, but this guide assumes it is present)*
+
+## Setup the crate you want to verify
+
+*Note: the instructions below assume you are in the folder of the specific crate (**not workspace!**) you want to extract.*
+
+
+ - <input type="checkbox" class="user-checkable"/> Create the folder `proofs/lean/extraction`folder, right next to the `Cargo.toml` of the crate you want to verify.  
+   <span style="margin-right:30px;"></span>🪄 `mkdir -p proofs/lean/extraction`
+ - <input type="checkbox" class="user-checkable"/> Create `proofs/lean/extraction/lakefile.toml`, and add the following content:  
+```toml
+name = "your_crate_name"
+version = "0.1.0"
+defaultTargets = ["your_crate_name"]
+
+[[lean_lib]]
+name = "your_crate_name"
+
+[[require]]
+name = "Hax"
+git.url = "https://github.com/cryspen/hax"
+git.subDir = "hax-lib/proof-libs/lean"
+rev = "main"
+``` 
+
+## Partial extraction
+
+*Note: the instructions below assume you are in the folder of the
+specific crate you want to extract.*
+
+Run the command `cargo hax into lean` to extract every item of your
+crate as F\* modules in the subfolder `proofs/lean/extraction`.
+
+**What is critical? What is worth verifying?**  
+Probably, your Rust crate contains mixed kinds of code: some parts are
+critical (e.g. the library functions at the core of your crate) while
+some others are not (e.g. the binary driver that wraps the
+library). In this case, you likely want to extract only partially your
+crate, so that you can focus on the important part.
+
+**Using the `-i` flag.**  
+If you want to extract a function
+`your_crate::some_module::my_function`, you need to tell `hax` to
+extract nothing but `my_function`:
+
+```bash
+cargo hax into -i '-** +your_crate::some_module::my_function' lean
+```
+
+This command will remove all items from extraction (`-**`) and add back `my_function`, along with all its dependencies (other functions, type definitions, etc.) from your crate. If you don't want the dependencies, you can use `+!` instead of `+`. See [the the FAQ](../faq/include-flags.md) or `cargo hax into --help` for more options for partial extraction.
+
+**Unsupported Rust code.**  
+hax [doesn't support every Rust
+constructs](https://github.com/hacspec/hax?tab=readme-ov-file#supported-subset-of-the-rust-language),
+`unsafe` code, or complicated mutation scheme. That is another reason
+for extracting only a part of your crate. When running hax, if an item
+of your crate, say a function `my_crate::f`, is not handled by hax,
+you can remove it from the extraction target by adding  `-my_crate::f` as an option to the `-i` flag. 
+
+## Start Lean verification
+After extracting your Rust code to Lean, the result is in the `proofs/lean/extraction` folder. The
+`lakefile.toml` allows you to run Lean on this folder by running `lake build` (or directly in the IDE 
+using the LSP). Contrarily to F\*, successfully building the code doesn't prove panic freedom, this
+happens only if the specification states that the code is panic-free. 
+
+### Current limitations
+The Lean backend of Hax is under active development, and extraction can *fail* even on supported Rust. This can come from a missing Rust feature (i.e. supported by the Hax engine but not yet by the Lean backend). Testing the same extraction target on the *F\** backend can be an easy way to check. If all the Rust features are supported, then the extracted code can fail to build if it uses definitions from Rust `core` and `std` libraries that are missing in our Lean model (in `hax-lib/proof-libs/lean`). We're actively extending it to support idiomatic code, but feel free to report it on [zulip](https://hacspec.zulipchat.com/) or [github](https://github.com/cryspen/hax/issues)

docs/manual/lean/tutorial/index.md

@@ -0,0 +1,8 @@
+---
+weight: 101
+---
+
+# Tutorial
+
+This tutorial focuses on proving properties with the hax toolchain and its
+[Lean](https://lean-lang.org/) backend.