From ccb89284c2bc59dfc70ae8b9032af2180795df8b Mon Sep 17 00:00:00 2001
From: Maxime Buyse <maxime@cryspen.com>
Date: Tue, 26 Aug 2025 10:51:49 +0200
Subject: [PATCH 01/12] Lean tutorial first version.

---
 docs/manual/index.md                  |  6 +--
 docs/manual/quick_start/index.md      | 32 ++++++++++++--
 docs/manual/tutorial/index.md         |  6 +--
 docs/manual/tutorial/panic-freedom.md | 62 ++++++++++++++++++++++++++-
 docs/manual/tutorial/properties.md    | 27 ++++++++++++
 hax-lib/proof-libs/lean/Hax/Lib.lean  | 22 ++++++++++
 6 files changed, 144 insertions(+), 11 deletions(-)

diff --git a/docs/manual/index.md b/docs/manual/index.md
index a4b751254..c86d1d958 100644
--- a/docs/manual/index.md
+++ b/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
diff --git a/docs/manual/quick_start/index.md b/docs/manual/quick_start/index.md
index f5b8edfde..ce67c532a 100644
--- a/docs/manual/quick_start/index.md
+++ b/docs/manual/quick_start/index.md
@@ -2,7 +2,7 @@
 weight: 0
 ---
 
-# Quick start with hax and F\*
+# Quick start with hax and F\* (or Lean)
 
 Do you want to try hax out on a Rust crate of yours? This chapter is
 what you are looking for!
@@ -12,17 +12,33 @@ 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 Lean](https://lean-lang.org/install/) *(optional: only if want to run Lean)*
 
 ## 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\*.*
+*Note: this part is useful only if you want to run F\* or Lean.*
 
 
- - <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` (or `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/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"/> *Lean only step:* 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"
+``` 
+ - <input type="checkbox" class="user-checkable"/> *F\* only step* 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`  
@@ -87,4 +103,12 @@ with various F\* modules in the `proofs/fstar/extraction` folder. The
    it means your code *never* panics, which already is an important
    property.
 
+## 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 specifications states that the code is panic-free. However, trying to build without 
+specifications can fail if a definition is missing in our Lean model of the Rust core library. This lives 
+in the sub-directory `hax-lib/proof-libs/lean` of the hax repository. 
+
 To go further, please read the next chapter.
diff --git a/docs/manual/tutorial/index.md b/docs/manual/tutorial/index.md
index 4a20a4d3e..0e8d0e165 100644
--- a/docs/manual/tutorial/index.md
+++ b/docs/manual/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/) or [Lean](https://lean-lang.org/).
diff --git a/docs/manual/tutorial/panic-freedom.md b/docs/manual/tutorial/panic-freedom.md
index 8d4cfeacf..75565bcd5 100644
--- a/docs/manual/tutorial/panic-freedom.md
+++ b/docs/manual/tutorial/panic-freedom.md
@@ -2,7 +2,7 @@
 weight: 0
 ---
 
-# Panic freedom
+# Panic freedom with F\*
 
 Let's start with a simple example: a function that squares a `u8`
 integer. To extract this function to F\* using hax, we simply need to
@@ -28,6 +28,43 @@ 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.
 
+# Panic freedom with Lean
+
+Let's take the same `square` function and extract it to Lean using `cargo hax into lean`.
+If we run `lake build` on the result, we get a success, but this doesn't mean that the function is 
+panic-free. Indeed, our encoding of Rust code in Lean wraps everything in a result monad. And 
+functions that panic return an error in this monad. To try to prove panic-freedom, we have to 
+specify that the result of `square` is expected not to be an error in this result type. A way
+to do that is the following:
+```rust
+#[hax_lib::lean::after("
+theorem square_spec (value: u8) :
+  ⦃ __requires (value) = pure true ⦄
+  (square value)
+  ⦃ ⇓ result => __ensures value result = pure true ⦄
+  := by
+  mvcgen
+  simp [__requires, __ensures, square] at *
+  intros
+  rw [UInt8.HaxMul_spec_bv_rw] ; simp ;
+  bv_decide")]
+#[hax_lib::requires(true)]
+#[hax_lib::ensures(|res| true)]
+fn square(x: u8) -> u8 {
+    x * x
+}
+```
+The specification is extrinsic to the function, we state a theorem `square_spec` which uses a Hoare
+triple to specify properties on the output, assuming some other properties on the inputs. Here,
+we use the precondition and post-condition defined using the `hax_lib` macro, but we could write
+our specification entirely in the `square_spec` theorem. Here our post-condition is `true` which seems
+trivial, but `__ensures value result = pure true` is false if `result` (and thus `__ensures value result`) 
+is an error in the result monad. So this specification states that `square` should be panic-free. We also 
+have a small proof scripts applying a few tactics to try to prove our theorem. If we try running `lake build`
+after extracting this code, we get an error: 
+`The prover found a counterexample, consider the following assignment: value = 255`. Indeed `square(255)` 
+panics.
+
 ## 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)
@@ -107,6 +144,29 @@ on, it is the responsibility of the clients of `square` to respect the
 contact. The next step is thus be to verify, through hax extraction,
 that `square` is used correctly at every call site.
 
+### Lean version of solution B
+Let's try to add the precondition to the Lean version of the `square` function.
+We can modify the Rust precondition:
+```rust
+#[hax_lib::lean::after("
+theorem square_spec (value: u8) :
+  ⦃ __requires (value) = pure true ⦄
+  (square value)
+  ⦃ ⇓ result => __ensures value result = pure true ⦄
+  := by
+  mvcgen
+  simp [__requires, __ensures, square] at *
+  intros
+  rw [UInt8.HaxMul_spec_bv_rw] ; simp ;
+  bv_decide")]
+#[hax_lib::requires(x < 16)]
+#[hax_lib::ensures(|res| true)]
+fn square(x: u8) -> u8 {
+    x * x
+}
+```
+Now, extracting and then running Lean succeeds!
+
 ## Common panicking situations
 Multiplication is not the only panicking function provided by the Rust
 library: most of the other integer arithmetic operation have such
diff --git a/docs/manual/tutorial/properties.md b/docs/manual/tutorial/properties.md
index 91a053839..ea917ec4f 100644
--- a/docs/manual/tutorial/properties.md
+++ b/docs/manual/tutorial/properties.md
@@ -25,6 +25,29 @@ Such a simple post-condition is automatically proven by F\*. The
 properties of our `square` function are not fascinating. Let's study a
 more interesting example: [Barrett reduction](https://en.wikipedia.org/wiki/Barrett_reduction).
 
+# Proving properties in Lean
+
+Let's try the same in Lean:
+```rust
+#[hax_lib::lean::after("
+theorem square_spec (value: u8) :
+  ⦃ __requires (value) = pure true ⦄
+  (square value)
+  ⦃ ⇓ result => __ensures value result = pure true ⦄
+  := by
+  mvcgen
+  simp [__requires, __ensures, square] at *
+  intros
+  rw [UInt8.HaxMul_spec_bv_rw] ; simp ;
+  all_goals bv_decide")]
+#[hax_lib::requires(x < 16)]
+#[hax_lib::ensures(|res| res >= x)]
+fn square(x: u8) -> u8 {
+    x * x
+}
+```
+This works as well (note that the proof script is slightly modified to apply `bv_decide` to all goals).
+
 ## A concrete example of contract: Barrett reduction
 
 While the correctness of `square` is obvious, the Barrett reduction is
@@ -100,6 +123,10 @@ that the post-condition holds. The pre-condition and post-condition
 gives the function a formal specification, which is useful both for
 further formal verification and for documentation purposes.
 
+A Lean version of the Barrett example is available in the 
+[`examples`](https://github.com/cryspen/hax/tree/main/examples/lean_barrett) 
+section of hax. 
+
 ## Extrinsic properties with lemmas
 
 Consider the `encrypt` and `decrypt` functions below. Those functions
diff --git a/hax-lib/proof-libs/lean/Hax/Lib.lean b/hax-lib/proof-libs/lean/Hax/Lib.lean
index 2ca4c12d6..227b191d3 100644
--- a/hax-lib/proof-libs/lean/Hax/Lib.lean
+++ b/hax-lib/proof-libs/lean/Hax/Lib.lean
@@ -644,6 +644,28 @@ theorem HaxRem_spec_bv_rw (x y : i32) :
 
 end Int32
 
+
+
+namespace UInt8
+
+instance instHaxMul : HaxMul UInt8 where
+  mul x y :=
+    if (BitVec.umulOverflow x.toBitVec y.toBitVec) then .fail .integerOverflow
+    else pure (x * y)
+
+@[spec]
+theorem HaxMul_spec_bv (x y: u8) :
+  ⦃ ¬ (BitVec.umulOverflow x.toBitVec y.toBitVec) ⦄
+  (x *? y)
+  ⦃ ⇓ r => r = x * y ⦄ := by mvcgen [instHaxMul]
+
+theorem HaxMul_spec_bv_rw (x y: u8) :
+   ¬ (BitVec.umulOverflow x.toBitVec y.toBitVec) →
+   x *? y = Result.ok (x * y)
+:= by simp [instHaxMul]
+
+end UInt8
+
 /-
 
 # Wrapping operations

From 3afa2991c015d2a533883c4a66603d51abb1c111 Mon Sep 17 00:00:00 2001
From: Maxime Buyse <maxime@cryspen.com>
Date: Tue, 26 Aug 2025 15:59:00 +0200
Subject: [PATCH 02/12] Change titles for lean tutorial.

---
 docs/manual/tutorial/panic-freedom.md | 4 ++--
 1 file changed, 2 insertions(+), 2 deletions(-)

diff --git a/docs/manual/tutorial/panic-freedom.md b/docs/manual/tutorial/panic-freedom.md
index 75565bcd5..4070b29a9 100644
--- a/docs/manual/tutorial/panic-freedom.md
+++ b/docs/manual/tutorial/panic-freedom.md
@@ -2,7 +2,7 @@
 weight: 0
 ---
 
-# Panic freedom with F\*
+# Panic freedom
 
 Let's start with a simple example: a function that squares a `u8`
 integer. To extract this function to F\* using hax, we simply need to
@@ -28,7 +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.
 
-# Panic freedom with Lean
+## Panic freedom with Lean
 
 Let's take the same `square` function and extract it to Lean using `cargo hax into lean`.
 If we run `lake build` on the result, we get a success, but this doesn't mean that the function is 

From a0e3226c080ed6e8483bb001af6f948803a463f8 Mon Sep 17 00:00:00 2001
From: Maxime Buyse <maxime@cryspen.com>
Date: Tue, 26 Aug 2025 17:53:07 +0200
Subject: [PATCH 03/12] Playground integration in tutorial: small fixes + lean
 suport.

---
 docs/javascripts/hax_playground.js    | 24 ++++++++++++------------
 docs/manual/tutorial/panic-freedom.md |  4 ++--
 docs/manual/tutorial/properties.md    |  2 +-
 3 files changed, 15 insertions(+), 15 deletions(-)

diff --git a/docs/javascripts/hax_playground.js b/docs/javascripts/hax_playground.js
index 0d17d61c2..cd899ca12 100644
--- a/docs/javascripts/hax_playground.js
+++ b/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,6 +130,7 @@ 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');
@@ -135,7 +138,7 @@ function setup_hax_playground() {
         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);
     }
 }
 
diff --git a/docs/manual/tutorial/panic-freedom.md b/docs/manual/tutorial/panic-freedom.md
index 4070b29a9..afe78f9fb 100644
--- a/docs/manual/tutorial/panic-freedom.md
+++ b/docs/manual/tutorial/panic-freedom.md
@@ -36,7 +36,7 @@ panic-free. Indeed, our encoding of Rust code in Lean wraps everything in a resu
 functions that panic return an error in this monad. To try to prove panic-freedom, we have to 
 specify that the result of `square` is expected not to be an error in this result type. A way
 to do that is the following:
-```rust
+```{.rust .playable .lean-backend}
 #[hax_lib::lean::after("
 theorem square_spec (value: u8) :
   ⦃ __requires (value) = pure true ⦄
@@ -147,7 +147,7 @@ that `square` is used correctly at every call site.
 ### Lean version of solution B
 Let's try to add the precondition to the Lean version of the `square` function.
 We can modify the Rust precondition:
-```rust
+```{.rust .playable .lean-backend}
 #[hax_lib::lean::after("
 theorem square_spec (value: u8) :
   ⦃ __requires (value) = pure true ⦄
diff --git a/docs/manual/tutorial/properties.md b/docs/manual/tutorial/properties.md
index ea917ec4f..a97d65a56 100644
--- a/docs/manual/tutorial/properties.md
+++ b/docs/manual/tutorial/properties.md
@@ -28,7 +28,7 @@ more interesting example: [Barrett reduction](https://en.wikipedia.org/wiki/Barr
 # Proving properties in Lean
 
 Let's try the same in Lean:
-```rust
+```{.rust .playable .lean-backend}
 #[hax_lib::lean::after("
 theorem square_spec (value: u8) :
   ⦃ __requires (value) = pure true ⦄

From 48653ebb73b2d24404561602fedea4197f60348b Mon Sep 17 00:00:00 2001
From: Maxime Buyse <maxime@cryspen.com>
Date: Mon, 8 Sep 2025 11:58:07 +0200
Subject: [PATCH 04/12] Separate Lean and fstar tutorials.

---
 docs/manual/faq/index.md                      |   2 +-
 .../index.md                                  |  36 +----
 .../data-invariants.md                        |   0
 .../{tutorial => fstar_tutorial}/index.md     |   2 +-
 docs/manual/fstar_tutorial/panic-freedom.md   | 127 +++++++++++++++
 .../proofs/fstar/extraction/Makefile          |   0
 .../extraction/Tutorial_src.Math.Lemmas.fst   |   0
 .../proofs/fstar/extraction/Tutorial_src.fst  |   0
 docs/manual/fstar_tutorial/properties.md      | 152 ++++++++++++++++++
 docs/manual/lean_quick_start/index.md         |  83 ++++++++++
 docs/manual/lean_tutorial/index.md            |   8 +
 .../panic-freedom.md                          |  69 ++------
 .../{tutorial => lean_tutorial}/properties.md |   0
 13 files changed, 391 insertions(+), 88 deletions(-)
 rename docs/manual/{quick_start => fstar_quick_start}/index.md (70%)
 rename docs/manual/{tutorial => fstar_tutorial}/data-invariants.md (100%)
 rename docs/manual/{tutorial => fstar_tutorial}/index.md (90%)
 create mode 100644 docs/manual/fstar_tutorial/panic-freedom.md
 rename docs/manual/{tutorial => fstar_tutorial}/proofs/fstar/extraction/Makefile (100%)
 rename docs/manual/{tutorial => fstar_tutorial}/proofs/fstar/extraction/Tutorial_src.Math.Lemmas.fst (100%)
 rename docs/manual/{tutorial => fstar_tutorial}/proofs/fstar/extraction/Tutorial_src.fst (100%)
 create mode 100644 docs/manual/fstar_tutorial/properties.md
 create mode 100644 docs/manual/lean_quick_start/index.md
 create mode 100644 docs/manual/lean_tutorial/index.md
 rename docs/manual/{tutorial => lean_tutorial}/panic-freedom.md (67%)
 rename docs/manual/{tutorial => lean_tutorial}/properties.md (100%)

diff --git a/docs/manual/faq/index.md b/docs/manual/faq/index.md
index f561e2533..4736c8839 100644
--- a/docs/manual/faq/index.md
+++ b/docs/manual/faq/index.md
@@ -1,5 +1,5 @@
 ---
-weight: 4
+weight: 200
 ---
 
 # Troubleshooting/FAQ
diff --git a/docs/manual/quick_start/index.md b/docs/manual/fstar_quick_start/index.md
similarity index 70%
rename from docs/manual/quick_start/index.md
rename to docs/manual/fstar_quick_start/index.md
index ce67c532a..22394fe2d 100644
--- a/docs/manual/quick_start/index.md
+++ b/docs/manual/fstar_quick_start/index.md
@@ -2,7 +2,7 @@
 weight: 0
 ---
 
-# Quick start with hax and F\* (or Lean)
+# Quick start with hax and F\*
 
 Do you want to try hax out on a Rust crate of yours? This chapter is
 what you are looking for!
@@ -11,34 +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 Lean](https://lean-lang.org/install/) *(optional: only if want to run Lean)*
+ - <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\* or Lean.*
 
-
- - <input type="checkbox" class="user-checkable"/> Create the folder `proofs/fstar/extraction` (or `proofs/lean/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"/> *Lean only step:* 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"
-``` 
- - <input type="checkbox" class="user-checkable"/> *F\* only step* 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`  
@@ -82,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
@@ -103,12 +83,4 @@ with various F\* modules in the `proofs/fstar/extraction` folder. The
    it means your code *never* panics, which already is an important
    property.
 
-## 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 specifications states that the code is panic-free. However, trying to build without 
-specifications can fail if a definition is missing in our Lean model of the Rust core library. This lives 
-in the sub-directory `hax-lib/proof-libs/lean` of the hax repository. 
-
 To go further, please read the next chapter.
diff --git a/docs/manual/tutorial/data-invariants.md b/docs/manual/fstar_tutorial/data-invariants.md
similarity index 100%
rename from docs/manual/tutorial/data-invariants.md
rename to docs/manual/fstar_tutorial/data-invariants.md
diff --git a/docs/manual/tutorial/index.md b/docs/manual/fstar_tutorial/index.md
similarity index 90%
rename from docs/manual/tutorial/index.md
rename to docs/manual/fstar_tutorial/index.md
index 0e8d0e165..2bedd236f 100644
--- a/docs/manual/tutorial/index.md
+++ b/docs/manual/fstar_tutorial/index.md
@@ -16,4 +16,4 @@ languages. Others are specialized tools:
 dedicated to proving properties about protocols.
 
 This tutorial focuses on proving properties with
-[F\*](https://fstar-lang.org/) or [Lean](https://lean-lang.org/).
+[F\*](https://fstar-lang.org/).
diff --git a/docs/manual/fstar_tutorial/panic-freedom.md b/docs/manual/fstar_tutorial/panic-freedom.md
new file mode 100644
index 000000000..27fa5ecb8
--- /dev/null
+++ b/docs/manual/fstar_tutorial/panic-freedom.md
@@ -0,0 +1,127 @@
+---
+weight: 0
+---
+
+# Panic freedom
+
+Let's start with a simple example: a function that squares a `u8`
+integer. To extract this function to F\* using hax, we simply need to
+run the command `cargo hax into fstar` in the directory of the crate
+in which the function `square` is defined.
+
+*Note: throughout this tutorial, you can edit the snippets of code and
+extract to F\* by clicking the play button (:material-play:), or even typecheck it with the button (:material-check:).*
+
+```{.rust .playable }
+fn square(x: u8) -> u8 {
+    x * x
+}
+```
+
+Though, if we try to verify this function, F\* is complaining about a
+subtyping issue: F\* tells us that it is not able to prove that the
+result of the multiplication `x * x` fits the range of `u8`. The
+multiplication `x * x` might indeed be overflowing!
+
+For instance, running `square(16)` panics: `16 * 16` is `256`, which
+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)
+from the Rust book:
+
+> The `panic!` macro signals that your program is in a state it can't
+> handle and lets you tell the process to stop instead of trying to
+> proceed with invalid or incorrect values.
+
+A Rust program should panics only in a situation where an assumption
+or an invariant is broken: a panics models an *invalid* state. Formal
+verification is about proving such invalid state cannot occur, at all.
+
+From this observation emerges the urge of proving Rust programs to be
+panic-free!
+
+## Fixing our squaring function
+Let's come back to our example. There is an informal assumption to the
+multiplication operator in Rust: the inputs should be small enough so
+that the addition doesn't overflow.
+
+Note that Rust also provides `wrapping_mul`, a non-panicking variant
+of the multiplication on `u8` that wraps when the result is bigger
+than `255`. Replacing the common multiplication with `wrapping_mul` in
+`square` would fix the panic, but then, `square(256)` returns zero.
+Semantically, this is not what one would expect from `square`.
+
+Our problem is that our function `square` is well-defined only when
+its input is within `0` and `15`.
+
+### Solution A: reflect the partialness of the function in Rust
+A first solution is to make `square` return an `Option<u8>` instead of a `u8`:
+``` {.rust .playable}
+fn square_option(x: u8) -> Option<u8> {
+    if x >= 16 {
+        None
+    } else {
+        Some(x * x)
+    }
+}
+```
+
+Here, F\* is able to prove panic-freedom: calling `square` with any
+input is safe. Though, one may argue that `square`'s input being small
+enough should really be an assumption. Having to deal with the
+possible integer overflowing whenever squaring is a huge burden. Can
+we do better?
+
+### Solution B: add a precondition
+The type system of Rust doesn't allow the programmer to formalize the
+assumption that `square` expects a small `u8`. This becomes
+possible using hax: one can annotate a function with a pre-condition
+on its inputs.
+
+The pre-conditions and post-conditions on a function form a
+*contract*: "if you give me some inputs that satisfies a given formula
+(*the precondition*), I will produce a return value that satisfy
+another formula (*the postcondition*)". Outside this contracts,
+anything might happen: the function might panic, might run forever,
+erase your disk, or anything.
+
+The helper crate
+[hax-lib](https://github.com/hacspec/hax/tree/main/hax-lib)
+provdes the `requires`
+[proc-macro](https://doc.rust-lang.org/reference/procedural-macros.html)
+which lets user writting pre-conditions directly in Rust.
+
+```{.rust .playable}
+#[hax_lib::requires(x < 16)]
+fn square_requires(x: u8) -> u8 {
+    x * x
+}
+```
+
+With this precondition, F\* is able to prove panic freedom. From now
+on, it is the responsibility of the clients of `square` to respect the
+contact. The next step is thus be to verify, through hax extraction,
+that `square` is used correctly at every call site.
+
+## Common panicking situations
+Multiplication is not the only panicking function provided by the Rust
+library: most of the other integer arithmetic operation have such
+informal assumptions.
+
+Another source of panics is indexing. Indexing in an array, a slice or
+a vector is a partial operation: the index might be out of range.
+
+In the example folder of hax, you can find the [`chacha20`
+example](https://github.com/hacspec/hax/blob/main/examples/chacha20/src/lib.rs)
+that makes use of pre-conditions to prove panic freedom.
+
+Another solution for safe indexing is to use the [newtype index
+pattern](https://matklad.github.io/2018/06/04/newtype-index-pattern.html),
+which is [also supported by
+hax](https://github.com/hacspec/hax/blob/d668de4d17e5ddee3a613068dc30b71353a9db4f/tests/attributes/src/lib.rs#L98-L126). The [data invariants](data-invariants.md#newtype-and-refinements) chapter gives more details about this.
+
diff --git a/docs/manual/tutorial/proofs/fstar/extraction/Makefile b/docs/manual/fstar_tutorial/proofs/fstar/extraction/Makefile
similarity index 100%
rename from docs/manual/tutorial/proofs/fstar/extraction/Makefile
rename to docs/manual/fstar_tutorial/proofs/fstar/extraction/Makefile
diff --git a/docs/manual/tutorial/proofs/fstar/extraction/Tutorial_src.Math.Lemmas.fst b/docs/manual/fstar_tutorial/proofs/fstar/extraction/Tutorial_src.Math.Lemmas.fst
similarity index 100%
rename from docs/manual/tutorial/proofs/fstar/extraction/Tutorial_src.Math.Lemmas.fst
rename to docs/manual/fstar_tutorial/proofs/fstar/extraction/Tutorial_src.Math.Lemmas.fst
diff --git a/docs/manual/tutorial/proofs/fstar/extraction/Tutorial_src.fst b/docs/manual/fstar_tutorial/proofs/fstar/extraction/Tutorial_src.fst
similarity index 100%
rename from docs/manual/tutorial/proofs/fstar/extraction/Tutorial_src.fst
rename to docs/manual/fstar_tutorial/proofs/fstar/extraction/Tutorial_src.fst
diff --git a/docs/manual/fstar_tutorial/properties.md b/docs/manual/fstar_tutorial/properties.md
new file mode 100644
index 000000000..91a053839
--- /dev/null
+++ b/docs/manual/fstar_tutorial/properties.md
@@ -0,0 +1,152 @@
+---
+weight: 1
+---
+
+# Proving properties
+
+In the last chapter, we proved one property on the `square` function:
+panic freedom. After adding a precondition, the signature of the
+`square` function was `x:u8 -> Pure u8 (requires x <. 16uy) (ensures fun _ -> True)`.
+
+This contract stipulates that, given a small input, the function will
+_return a value_: it will not panic or diverge. We could enrich the
+contract of `square` with a post-condition about the fact it is a
+increasing function:
+
+``` {.rust .playable}
+#[hax_lib::requires(x < 16)]
+#[hax_lib::ensures(|result| result >= x)]
+fn square_ensures(x: u8) -> u8 {
+    x * x
+}
+```
+
+Such a simple post-condition is automatically proven by F\*. The
+properties of our `square` function are not fascinating. Let's study a
+more interesting example: [Barrett reduction](https://en.wikipedia.org/wiki/Barrett_reduction).
+
+## A concrete example of contract: Barrett reduction
+
+While the correctness of `square` is obvious, the Barrett reduction is
+not.
+
+Given `value` a field element (a `i32` whose absolute value is at most
+`BARRET_R`), the function `barrett_reduce` defined below computes
+`result` such that:
+
+- `result ≡ value (mod FIELD_MODULUS)`;
+- the absolute value of `result` is bound as follows:
+  `|result| < FIELD_MODULUS`.
+
+It is easy to write this contract directly as `hax::requires` and
+`hax::ensures` annotations, as shown in the snippet below.
+
+```{.rust .playable}
+type FieldElement = i32;
+const FIELD_MODULUS: i32 = 3329;
+const BARRETT_SHIFT: i64 = 26;
+const BARRETT_R: i64 = 0x4000000; // 2^26
+const BARRETT_MULTIPLIER: i64 = 20159; // ⌊(BARRETT_R / FIELD_MODULUS) + 1/2⌋
+
+#[hax_lib::fstar::options("--z3rlimit 100")]
+#[hax_lib::requires((i64::from(value) >= -BARRETT_R && i64::from(value) <= BARRETT_R))]
+#[hax_lib::ensures(|result| result > -FIELD_MODULUS && result < FIELD_MODULUS
+                     && result %  FIELD_MODULUS ==  value % FIELD_MODULUS)]
+fn barrett_reduce(value: i32) -> i32 {
+    let t = i64::from(value) * BARRETT_MULTIPLIER;
+    let t = t + (BARRETT_R >> 1);
+
+    let quotient = t >> BARRETT_SHIFT;
+    let quotient = quotient as i32;
+
+    let sub = quotient * FIELD_MODULUS;
+
+    value - sub
+}
+```
+
+<!-- Note that we call to `cancel_mul_mod`, a lemma: in Rust, this have no
+effect, but in F\*, that establishes that `(quotient * 3329) % 3329` is
+zero. -->
+
+The proof for the code above uses the Z3 SMT solver to prove the
+post-condition.  Since the SMT solver needs to reason about non-linear
+arithmetic (multiplication, modulus, division) it needs more
+resources, hence we bump up the `rlimit` to 100 in an annotation above
+the function. With this annotation F\* and Z3 are able to automatically
+verify this function. However, it is worth noting that the heuristic
+strategies used by Z3 for non-linear arithmetic may sometimes fail to
+complete in the given `rlimit` depending on the solver version or random
+number generator, so we often give Z3 a generous resource limit.
+
+Conversely, instead of relying on the SMT solver, we can also
+elaborate the proof of this function by hand to make it more
+predictable.  For example, before the final line of the function, 
+we could call a mathematical lemma may have to help F\* prove
+the correctness of the reduction.  The lemma call would be:
+```
+    fstar!("Math.Lemmas.cancel_mul_mod (v quotient) 3329");
+```
+This lemma establishes that `(quotient * 3329) % 3329` is zero. We often use lemmas like
+these to limit our dependence on Z3. 
+
+This Barrett reduction examples is taken from
+[libcrux](https://github.com/cryspen/libcrux/tree/main)'s proof of
+Kyber which is using hax and F\*.
+
+This example showcases an **intrinsic proof**: the function
+`barrett_reduce` not only computes a value, but it also ship a proof
+that the post-condition holds. The pre-condition and post-condition
+gives the function a formal specification, which is useful both for
+further formal verification and for documentation purposes.
+
+## Extrinsic properties with lemmas
+
+Consider the `encrypt` and `decrypt` functions below. Those functions
+have no precondition, don't have particularly interesting properties
+individually. However, the composition of the two yields an useful
+property: encrypting a ciphertext and decrypting the result with a
+same key produces the ciphertext again. `|c| decrypt(c, key)` is the
+inverse of `|p| encrypt(p, key)`.
+
+```{.rust .playable}
+fn encrypt(plaintext: u32, key: u32) -> u32 {
+    plaintext ^ key
+}
+
+fn decrypt(ciphertext: u32, key: u32) -> u32 {
+    ciphertext ^ key
+}
+```
+
+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.
+
+To this end, Hax provides a macro `lemma`. Below, the Rust function
+`encrypt_decrypt_identity` takes a key and a plaintext, and then
+states the inverse property. The body is empty: the details of the
+proof itself are not relevant, at this stage, we only care about the
+statement. The proof will be completed manually in the proof
+assistant.
+
+```{.rust .playable}
+# fn encrypt(plaintext: u32, key: u32) -> u32 {
+#     plaintext ^ key
+# }
+# 
+# fn decrypt(ciphertext: u32, key: u32) -> u32 {
+#     ciphertext ^ key
+# }
+# 
+#[hax_lib::lemma]
+#[hax_lib::requires(true)]
+
+fn encrypt_decrypt_identity(
+    key: u32,
+    plaintext: u32,
+) -> Proof<{ decrypt(encrypt(plaintext, key), key) == plaintext }> {
+}
+```
diff --git a/docs/manual/lean_quick_start/index.md b/docs/manual/lean_quick_start/index.md
new file mode 100644
index 000000000..9c928ce48
--- /dev/null
+++ b/docs/manual/lean_quick_start/index.md
@@ -0,0 +1,83 @@
+---
+weight: 100
+---
+
+# Quick start with hax and Lean
+
+## 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.
+
+**Partial extraction.**  
+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
+```
+
+Note this command will extract `my_function` but also any item
+(function, type, etc.) from your crate which is used directly or
+indirectly by `my_function`. If you don't want the dependency, use
+`+!` instead of `+` in the `-i` flag.
+
+**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 append `-my_crate::f` to the `-i` flag. You can learn more
+about the `-i` flag [in the FAQ](../faq/include-flags.md).
+
+## 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 specifications states that the code is panic-free. However, trying to build without 
+specifications can fail if a definition is missing in our Lean model of the Rust core library. This lives 
+in the sub-directory `hax-lib/proof-libs/lean` of the hax repository. 
diff --git a/docs/manual/lean_tutorial/index.md b/docs/manual/lean_tutorial/index.md
new file mode 100644
index 000000000..404ab7e59
--- /dev/null
+++ b/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.
diff --git a/docs/manual/tutorial/panic-freedom.md b/docs/manual/lean_tutorial/panic-freedom.md
similarity index 67%
rename from docs/manual/tutorial/panic-freedom.md
rename to docs/manual/lean_tutorial/panic-freedom.md
index afe78f9fb..505b4d1f3 100644
--- a/docs/manual/tutorial/panic-freedom.md
+++ b/docs/manual/lean_tutorial/panic-freedom.md
@@ -5,33 +5,20 @@ weight: 0
 # Panic freedom
 
 Let's start with a simple example: a function that squares a `u8`
-integer. To extract this function to F\* using hax, we simply need to
-run the command `cargo hax into fstar` in the directory of the crate
+integer. To extract this function to Lean using hax, we simply need to
+run the command `cargo hax into lean` in the directory of the crate
 in which the function `square` is defined.
 
 *Note: throughout this tutorial, you can edit the snippets of code and
-extract to F\* by clicking the play button (:material-play:), or even typecheck it with the button (:material-check:).*
+extract to Lean by clicking the play button (:material-play:), or even typecheck it with the button (:material-check:).*
 
-```{.rust .playable }
+```{.rust .playable .lean-backend}
 fn square(x: u8) -> u8 {
     x * x
 }
 ```
 
-Though, if we try to verify this function, F\* is complaining about a
-subtyping issue: F\* tells us that it is not able to prove that the
-result of the multiplication `x * x` fits the range of `u8`. The
-multiplication `x * x` might indeed be overflowing!
-
-For instance, running `square(16)` panics: `16 * 16` is `256`, which
-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.
-
-## Panic freedom with Lean
-
-Let's take the same `square` function and extract it to Lean using `cargo hax into lean`.
-If we run `lake build` on the result, we get a success, but this doesn't mean that the function is 
+If we run `lake build` on the result (or type-check using the playground), we get a success. If you followed the F\* tutorial, this might be a surprise because the function is not 
 panic-free. Indeed, our encoding of Rust code in Lean wraps everything in a result monad. And 
 functions that panic return an error in this monad. To try to prove panic-freedom, we have to 
 specify that the result of `square` is expected not to be an error in this result type. A way
@@ -58,12 +45,12 @@ The specification is extrinsic to the function, we state a theorem `square_spec`
 triple to specify properties on the output, assuming some other properties on the inputs. Here,
 we use the precondition and post-condition defined using the `hax_lib` macro, but we could write
 our specification entirely in the `square_spec` theorem. Here our post-condition is `true` which seems
-trivial, but `__ensures value result = pure true` is false if `result` (and thus `__ensures value result`) 
+trivial, but the condition `__ensures value result = pure true` is false if `result` (and thus `__ensures value result`) 
 is an error in the result monad. So this specification states that `square` should be panic-free. We also 
-have a small proof scripts applying a few tactics to try to prove our theorem. If we try running `lake build`
+have a small proof script applying a few tactics to try to prove our theorem. If we try running `lake build`
 after extracting this code, we get an error: 
 `The prover found a counterexample, consider the following assignment: value = 255`. Indeed `square(255)` 
-panics.
+panics because the multiplication overflows.
 
 ## Rust and panicking code
 Quoting the chapter [To `panic!` or Not to
@@ -97,7 +84,7 @@ its input is within `0` and `15`.
 
 ### Solution A: reflect the partialness of the function in Rust
 A first solution is to make `square` return an `Option<u8>` instead of a `u8`:
-``` {.rust .playable}
+``` {.rust .playable .lean-backend}
 fn square_option(x: u8) -> Option<u8> {
     if x >= 16 {
         None
@@ -114,39 +101,9 @@ possible integer overflowing whenever squaring is a huge burden. Can
 we do better?
 
 ### Solution B: add a precondition
-The type system of Rust doesn't allow the programmer to formalize the
-assumption that `square` expects a small `u8`. This becomes
-possible using hax: one can annotate a function with a pre-condition
-on its inputs.
-
-The pre-conditions and post-conditions on a function form a
-*contract*: "if you give me some inputs that satisfies a given formula
-(*the precondition*), I will produce a return value that satisfy
-another formula (*the postcondition*)". Outside this contracts,
-anything might happen: the function might panic, might run forever,
-erase your disk, or anything.
-
-The helper crate
-[hax-lib](https://github.com/hacspec/hax/tree/main/hax-lib)
-provdes the `requires`
-[proc-macro](https://doc.rust-lang.org/reference/procedural-macros.html)
-which lets user writting pre-conditions directly in Rust.
-
-```{.rust .playable}
-#[hax_lib::requires(x < 16)]
-fn square_requires(x: u8) -> u8 {
-    x * x
-}
-```
 
-With this precondition, F\* is able to prove panic freedom. From now
-on, it is the responsibility of the clients of `square` to respect the
-contact. The next step is thus be to verify, through hax extraction,
-that `square` is used correctly at every call site.
+We already added a pre-condition to specify panic-freedom but we can turn it into a more interesting pre-condition to restrict the inputs and stay in the domain where the multiplication fits in a `u8`. We only need to modify the Rust condition that is passed to the `hax_lib::requires` macro: 
 
-### Lean version of solution B
-Let's try to add the precondition to the Lean version of the `square` function.
-We can modify the Rust precondition:
 ```{.rust .playable .lean-backend}
 #[hax_lib::lean::after("
 theorem square_spec (value: u8) :
@@ -165,7 +122,11 @@ fn square(x: u8) -> u8 {
     x * x
 }
 ```
-Now, extracting and then running Lean succeeds!
+
+With this precondition, Lean is able to prove panic freedom. From now
+on, it is the responsibility of the clients of `square` to respect the
+contact. The next step is thus be to verify, through hax extraction,
+that `square` is used correctly at every call site.\
 
 ## Common panicking situations
 Multiplication is not the only panicking function provided by the Rust
diff --git a/docs/manual/tutorial/properties.md b/docs/manual/lean_tutorial/properties.md
similarity index 100%
rename from docs/manual/tutorial/properties.md
rename to docs/manual/lean_tutorial/properties.md

From 99abdfb0623471c2644a85a5509ccae8d94f0dc9 Mon Sep 17 00:00:00 2001
From: Maxime Buyse <maxime@cryspen.com>
Date: Mon, 8 Sep 2025 12:26:31 +0200
Subject: [PATCH 05/12] Lean tutorial for properties.

---
 docs/manual/lean_tutorial/panic-freedom.md |  20 +--
 docs/manual/lean_tutorial/properties.md    | 147 +--------------------
 2 files changed, 4 insertions(+), 163 deletions(-)

diff --git a/docs/manual/lean_tutorial/panic-freedom.md b/docs/manual/lean_tutorial/panic-freedom.md
index 505b4d1f3..c8b5bcafa 100644
--- a/docs/manual/lean_tutorial/panic-freedom.md
+++ b/docs/manual/lean_tutorial/panic-freedom.md
@@ -82,25 +82,7 @@ Semantically, this is not what one would expect from `square`.
 Our problem is that our function `square` is well-defined only when
 its input is within `0` and `15`.
 
-### Solution A: reflect the partialness of the function in Rust
-A first solution is to make `square` return an `Option<u8>` instead of a `u8`:
-``` {.rust .playable .lean-backend}
-fn square_option(x: u8) -> Option<u8> {
-    if x >= 16 {
-        None
-    } else {
-        Some(x * x)
-    }
-}
-```
-
-Here, F\* is able to prove panic-freedom: calling `square` with any
-input is safe. Though, one may argue that `square`'s input being small
-enough should really be an assumption. Having to deal with the
-possible integer overflowing whenever squaring is a huge burden. Can
-we do better?
-
-### Solution B: add a precondition
+### Solution: add a precondition
 
 We already added a pre-condition to specify panic-freedom but we can turn it into a more interesting pre-condition to restrict the inputs and stay in the domain where the multiplication fits in a `u8`. We only need to modify the Rust condition that is passed to the `hax_lib::requires` macro: 
 
diff --git a/docs/manual/lean_tutorial/properties.md b/docs/manual/lean_tutorial/properties.md
index a97d65a56..eafa4cafb 100644
--- a/docs/manual/lean_tutorial/properties.md
+++ b/docs/manual/lean_tutorial/properties.md
@@ -5,29 +5,12 @@ weight: 1
 # Proving properties
 
 In the last chapter, we proved one property on the `square` function:
-panic freedom. After adding a precondition, the signature of the
-`square` function was `x:u8 -> Pure u8 (requires x <. 16uy) (ensures fun _ -> True)`.
+panic freedom.
 
 This contract stipulates that, given a small input, the function will
 _return a value_: it will not panic or diverge. We could enrich the
-contract of `square` with a post-condition about the fact it is a
+contract of `square` with a post-condition about the fact it is an
 increasing function:
-
-``` {.rust .playable}
-#[hax_lib::requires(x < 16)]
-#[hax_lib::ensures(|result| result >= x)]
-fn square_ensures(x: u8) -> u8 {
-    x * x
-}
-```
-
-Such a simple post-condition is automatically proven by F\*. The
-properties of our `square` function are not fascinating. Let's study a
-more interesting example: [Barrett reduction](https://en.wikipedia.org/wiki/Barrett_reduction).
-
-# Proving properties in Lean
-
-Let's try the same in Lean:
 ```{.rust .playable .lean-backend}
 #[hax_lib::lean::after("
 theorem square_spec (value: u8) :
@@ -48,132 +31,8 @@ fn square(x: u8) -> u8 {
 ```
 This works as well (note that the proof script is slightly modified to apply `bv_decide` to all goals).
 
-## A concrete example of contract: Barrett reduction
-
-While the correctness of `square` is obvious, the Barrett reduction is
-not.
-
-Given `value` a field element (a `i32` whose absolute value is at most
-`BARRET_R`), the function `barrett_reduce` defined below computes
-`result` such that:
-
-- `result ≡ value (mod FIELD_MODULUS)`;
-- the absolute value of `result` is bound as follows:
-  `|result| < FIELD_MODULUS`.
-
-It is easy to write this contract directly as `hax::requires` and
-`hax::ensures` annotations, as shown in the snippet below.
-
-```{.rust .playable}
-type FieldElement = i32;
-const FIELD_MODULUS: i32 = 3329;
-const BARRETT_SHIFT: i64 = 26;
-const BARRETT_R: i64 = 0x4000000; // 2^26
-const BARRETT_MULTIPLIER: i64 = 20159; // ⌊(BARRETT_R / FIELD_MODULUS) + 1/2⌋
-
-#[hax_lib::fstar::options("--z3rlimit 100")]
-#[hax_lib::requires((i64::from(value) >= -BARRETT_R && i64::from(value) <= BARRETT_R))]
-#[hax_lib::ensures(|result| result > -FIELD_MODULUS && result < FIELD_MODULUS
-                     && result %  FIELD_MODULUS ==  value % FIELD_MODULUS)]
-fn barrett_reduce(value: i32) -> i32 {
-    let t = i64::from(value) * BARRETT_MULTIPLIER;
-    let t = t + (BARRETT_R >> 1);
-
-    let quotient = t >> BARRETT_SHIFT;
-    let quotient = quotient as i32;
-
-    let sub = quotient * FIELD_MODULUS;
-
-    value - sub
-}
-```
-
-<!-- Note that we call to `cancel_mul_mod`, a lemma: in Rust, this have no
-effect, but in F\*, that establishes that `(quotient * 3329) % 3329` is
-zero. -->
-
-The proof for the code above uses the Z3 SMT solver to prove the
-post-condition.  Since the SMT solver needs to reason about non-linear
-arithmetic (multiplication, modulus, division) it needs more
-resources, hence we bump up the `rlimit` to 100 in an annotation above
-the function. With this annotation F\* and Z3 are able to automatically
-verify this function. However, it is worth noting that the heuristic
-strategies used by Z3 for non-linear arithmetic may sometimes fail to
-complete in the given `rlimit` depending on the solver version or random
-number generator, so we often give Z3 a generous resource limit.
-
-Conversely, instead of relying on the SMT solver, we can also
-elaborate the proof of this function by hand to make it more
-predictable.  For example, before the final line of the function, 
-we could call a mathematical lemma may have to help F\* prove
-the correctness of the reduction.  The lemma call would be:
-```
-    fstar!("Math.Lemmas.cancel_mul_mod (v quotient) 3329");
-```
-This lemma establishes that `(quotient * 3329) % 3329` is zero. We often use lemmas like
-these to limit our dependence on Z3. 
-
-This Barrett reduction examples is taken from
-[libcrux](https://github.com/cryspen/libcrux/tree/main)'s proof of
-Kyber which is using hax and F\*.
-
-This example showcases an **intrinsic proof**: the function
-`barrett_reduce` not only computes a value, but it also ship a proof
-that the post-condition holds. The pre-condition and post-condition
-gives the function a formal specification, which is useful both for
-further formal verification and for documentation purposes.
-
-A Lean version of the Barrett example is available in the 
+The property that we prove above demonstrates a very simple case of a proof using hax and Lean. For a more complex example, a version of the Barrett example is available in the 
 [`examples`](https://github.com/cryspen/hax/tree/main/examples/lean_barrett) 
 section of hax. 
 
-## Extrinsic properties with lemmas
 
-Consider the `encrypt` and `decrypt` functions below. Those functions
-have no precondition, don't have particularly interesting properties
-individually. However, the composition of the two yields an useful
-property: encrypting a ciphertext and decrypting the result with a
-same key produces the ciphertext again. `|c| decrypt(c, key)` is the
-inverse of `|p| encrypt(p, key)`.
-
-```{.rust .playable}
-fn encrypt(plaintext: u32, key: u32) -> u32 {
-    plaintext ^ key
-}
-
-fn decrypt(ciphertext: u32, key: u32) -> u32 {
-    ciphertext ^ key
-}
-```
-
-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.
-
-To this end, Hax provides a macro `lemma`. Below, the Rust function
-`encrypt_decrypt_identity` takes a key and a plaintext, and then
-states the inverse property. The body is empty: the details of the
-proof itself are not relevant, at this stage, we only care about the
-statement. The proof will be completed manually in the proof
-assistant.
-
-```{.rust .playable}
-# fn encrypt(plaintext: u32, key: u32) -> u32 {
-#     plaintext ^ key
-# }
-# 
-# fn decrypt(ciphertext: u32, key: u32) -> u32 {
-#     ciphertext ^ key
-# }
-# 
-#[hax_lib::lemma]
-#[hax_lib::requires(true)]
-
-fn encrypt_decrypt_identity(
-    key: u32,
-    plaintext: u32,
-) -> Proof<{ decrypt(encrypt(plaintext, key), key) == plaintext }> {
-}
-```

From 53a6b60e8ecd1e12b7c36cd8e98a85e35ebd4e2e Mon Sep 17 00:00:00 2001
From: Maxime Buyse <maxime@cryspen.com>
Date: Mon, 8 Sep 2025 12:29:49 +0200
Subject: [PATCH 06/12] Update changelog.

---
 CHANGELOG.md | 2 ++
 1 file changed, 2 insertions(+)

diff --git a/CHANGELOG.md b/CHANGELOG.md
index c4ac36eda..95347e408 100644
--- a/CHANGELOG.md
+++ b/CHANGELOG.md
@@ -7,6 +7,8 @@ and this project adheres to [Semantic Versioning](https://semver.org/spec/v2.0.0
 
 ## [Unreleased]
 
+- 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.

From df54831fd0898f168ec2d0bae22745d47f97ceb5 Mon Sep 17 00:00:00 2001
From: maximebuyse <45398004+maximebuyse@users.noreply.github.com>
Date: Mon, 8 Sep 2025 14:57:24 +0200
Subject: [PATCH 07/12] Apply suggestions from code review
MIME-Version: 1.0
Content-Type: text/plain; charset=UTF-8
Content-Transfer-Encoding: 8bit

Co-authored-by: Clément Blaudeau <40171892+clementblaudeau@users.noreply.github.com>
---
 docs/manual/lean_quick_start/index.md | 17 +++++++----------
 1 file changed, 7 insertions(+), 10 deletions(-)

diff --git a/docs/manual/lean_quick_start/index.md b/docs/manual/lean_quick_start/index.md
index 9c928ce48..899cb9572 100644
--- a/docs/manual/lean_quick_start/index.md
+++ b/docs/manual/lean_quick_start/index.md
@@ -51,7 +51,7 @@ 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.
 
-**Partial extraction.**  
+**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`:
@@ -60,10 +60,7 @@ extract nothing but `my_function`:
 cargo hax into -i '-** +your_crate::some_module::my_function' lean
 ```
 
-Note this command will extract `my_function` but also any item
-(function, type, etc.) from your crate which is used directly or
-indirectly by `my_function`. If you don't want the dependency, use
-`+!` instead of `+` in the `-i` flag.
+This command will remove all items from extraction (`-**`) and add back `my_function`, along with all its dependencies (other function, 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
@@ -71,13 +68,13 @@ constructs](https://github.com/hacspec/hax?tab=readme-ov-file#supported-subset-o
 `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 append `-my_crate::f` to the `-i` flag. You can learn more
-about the `-i` flag [in the FAQ](../faq/include-flags.md).
+you can have 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 specifications states that the code is panic-free. However, trying to build without 
-specifications can fail if a definition is missing in our Lean model of the Rust core library. This lives 
-in the sub-directory `hax-lib/proof-libs/lean` of the hax repository. 
+happens only if the specifications 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` librairies 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)

From abf8b6ff395ae6ef7305059d7c75c01ca800e7ef Mon Sep 17 00:00:00 2001
From: Lucas Franceschino <lucas@cryspen.com>
Date: Mon, 8 Sep 2025 15:24:12 +0200
Subject: [PATCH 08/12] feat(mkdocs): use `awesome-nav`

To rename a title without renaming the folder itself, create a `.nav.yml` with:
```
title: whatever
```
---
 docs/default.nix | 10 ++++++++--
 mkdocs.yml       |  1 +
 2 files changed, 9 insertions(+), 2 deletions(-)

diff --git a/docs/default.nix b/docs/default.nix
index dfb80986a..ff42bd6e8 100644
--- a/docs/default.nix
+++ b/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
   '';
diff --git a/mkdocs.yml b/mkdocs.yml
index af9faf90f..5df17e9a4 100644
--- a/mkdocs.yml
+++ b/mkdocs.yml
@@ -81,6 +81,7 @@ plugins:
   - glightbox
   - search
   - blog
+  - awesome-nav
   - mkdocs-nav-weight
   - tags:
       tags_file: RFCs/index.md

From 52c55eaedec59922bdc6ab8dd2fe7fa95adb9d7b Mon Sep 17 00:00:00 2001
From: Maxime Buyse <maxime@cryspen.com>
Date: Mon, 8 Sep 2025 15:55:48 +0200
Subject: [PATCH 09/12] Reorganize tutorial with a Lean section and an F*
 section.

---
 docs/manual/fstar/.nav.yml                                | 1 +
 docs/manual/fstar/fstar_tutorial/.nav.yml                 | 1 +
 docs/manual/{ => fstar}/fstar_tutorial/data-invariants.md | 2 +-
 docs/manual/{ => fstar}/fstar_tutorial/index.md           | 0
 docs/manual/{ => fstar}/fstar_tutorial/panic-freedom.md   | 4 ++--
 .../fstar_tutorial/proofs/fstar/extraction/Makefile       | 0
 .../proofs/fstar/extraction/Tutorial_src.Math.Lemmas.fst  | 0
 .../proofs/fstar/extraction/Tutorial_src.fst              | 0
 docs/manual/{ => fstar}/fstar_tutorial/properties.md      | 2 +-
 .../{fstar_quick_start/index.md => fstar/quick_start.md}  | 0
 docs/manual/lean/lean_internals.md                        | 8 ++++++++
 docs/manual/{ => lean}/lean_tutorial/index.md             | 0
 docs/manual/{ => lean}/lean_tutorial/panic-freedom.md     | 0
 docs/manual/{ => lean}/lean_tutorial/properties.md        | 0
 .../{lean_quick_start/index.md => lean/quick_start.md}    | 8 ++++----
 15 files changed, 18 insertions(+), 8 deletions(-)
 create mode 100644 docs/manual/fstar/.nav.yml
 create mode 100644 docs/manual/fstar/fstar_tutorial/.nav.yml
 rename docs/manual/{ => fstar}/fstar_tutorial/data-invariants.md (98%)
 rename docs/manual/{ => fstar}/fstar_tutorial/index.md (100%)
 rename docs/manual/{ => fstar}/fstar_tutorial/panic-freedom.md (98%)
 rename docs/manual/{ => fstar}/fstar_tutorial/proofs/fstar/extraction/Makefile (100%)
 rename docs/manual/{ => fstar}/fstar_tutorial/proofs/fstar/extraction/Tutorial_src.Math.Lemmas.fst (100%)
 rename docs/manual/{ => fstar}/fstar_tutorial/proofs/fstar/extraction/Tutorial_src.fst (100%)
 rename docs/manual/{ => fstar}/fstar_tutorial/properties.md (98%)
 rename docs/manual/{fstar_quick_start/index.md => fstar/quick_start.md} (100%)
 create mode 100644 docs/manual/lean/lean_internals.md
 rename docs/manual/{ => lean}/lean_tutorial/index.md (100%)
 rename docs/manual/{ => lean}/lean_tutorial/panic-freedom.md (100%)
 rename docs/manual/{ => lean}/lean_tutorial/properties.md (100%)
 rename docs/manual/{lean_quick_start/index.md => lean/quick_start.md} (84%)

diff --git a/docs/manual/fstar/.nav.yml b/docs/manual/fstar/.nav.yml
new file mode 100644
index 000000000..5233ab9f9
--- /dev/null
+++ b/docs/manual/fstar/.nav.yml
@@ -0,0 +1 @@
+title: F*
\ No newline at end of file
diff --git a/docs/manual/fstar/fstar_tutorial/.nav.yml b/docs/manual/fstar/fstar_tutorial/.nav.yml
new file mode 100644
index 000000000..3a02279c1
--- /dev/null
+++ b/docs/manual/fstar/fstar_tutorial/.nav.yml
@@ -0,0 +1 @@
+title: F* tutorial
\ No newline at end of file
diff --git a/docs/manual/fstar_tutorial/data-invariants.md b/docs/manual/fstar/fstar_tutorial/data-invariants.md
similarity index 98%
rename from docs/manual/fstar_tutorial/data-invariants.md
rename to docs/manual/fstar/fstar_tutorial/data-invariants.md
index ad9367ad3..356297278 100644
--- a/docs/manual/fstar_tutorial/data-invariants.md
+++ b/docs/manual/fstar/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.
 
diff --git a/docs/manual/fstar_tutorial/index.md b/docs/manual/fstar/fstar_tutorial/index.md
similarity index 100%
rename from docs/manual/fstar_tutorial/index.md
rename to docs/manual/fstar/fstar_tutorial/index.md
diff --git a/docs/manual/fstar_tutorial/panic-freedom.md b/docs/manual/fstar/fstar_tutorial/panic-freedom.md
similarity index 98%
rename from docs/manual/fstar_tutorial/panic-freedom.md
rename to docs/manual/fstar/fstar_tutorial/panic-freedom.md
index 27fa5ecb8..79becc2a4 100644
--- a/docs/manual/fstar_tutorial/panic-freedom.md
+++ b/docs/manual/fstar/fstar_tutorial/panic-freedom.md
@@ -92,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)]
diff --git a/docs/manual/fstar_tutorial/proofs/fstar/extraction/Makefile b/docs/manual/fstar/fstar_tutorial/proofs/fstar/extraction/Makefile
similarity index 100%
rename from docs/manual/fstar_tutorial/proofs/fstar/extraction/Makefile
rename to docs/manual/fstar/fstar_tutorial/proofs/fstar/extraction/Makefile
diff --git a/docs/manual/fstar_tutorial/proofs/fstar/extraction/Tutorial_src.Math.Lemmas.fst b/docs/manual/fstar/fstar_tutorial/proofs/fstar/extraction/Tutorial_src.Math.Lemmas.fst
similarity index 100%
rename from docs/manual/fstar_tutorial/proofs/fstar/extraction/Tutorial_src.Math.Lemmas.fst
rename to docs/manual/fstar/fstar_tutorial/proofs/fstar/extraction/Tutorial_src.Math.Lemmas.fst
diff --git a/docs/manual/fstar_tutorial/proofs/fstar/extraction/Tutorial_src.fst b/docs/manual/fstar/fstar_tutorial/proofs/fstar/extraction/Tutorial_src.fst
similarity index 100%
rename from docs/manual/fstar_tutorial/proofs/fstar/extraction/Tutorial_src.fst
rename to docs/manual/fstar/fstar_tutorial/proofs/fstar/extraction/Tutorial_src.fst
diff --git a/docs/manual/fstar_tutorial/properties.md b/docs/manual/fstar/fstar_tutorial/properties.md
similarity index 98%
rename from docs/manual/fstar_tutorial/properties.md
rename to docs/manual/fstar/fstar_tutorial/properties.md
index 91a053839..e1edb34e6 100644
--- a/docs/manual/fstar_tutorial/properties.md
+++ b/docs/manual/fstar/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
diff --git a/docs/manual/fstar_quick_start/index.md b/docs/manual/fstar/quick_start.md
similarity index 100%
rename from docs/manual/fstar_quick_start/index.md
rename to docs/manual/fstar/quick_start.md
diff --git a/docs/manual/lean/lean_internals.md b/docs/manual/lean/lean_internals.md
new file mode 100644
index 000000000..15dadbf33
--- /dev/null
+++ b/docs/manual/lean/lean_internals.md
@@ -0,0 +1,8 @@
+---
+weight: 102
+---
+
+
+# Lean internals
+
+
diff --git a/docs/manual/lean_tutorial/index.md b/docs/manual/lean/lean_tutorial/index.md
similarity index 100%
rename from docs/manual/lean_tutorial/index.md
rename to docs/manual/lean/lean_tutorial/index.md
diff --git a/docs/manual/lean_tutorial/panic-freedom.md b/docs/manual/lean/lean_tutorial/panic-freedom.md
similarity index 100%
rename from docs/manual/lean_tutorial/panic-freedom.md
rename to docs/manual/lean/lean_tutorial/panic-freedom.md
diff --git a/docs/manual/lean_tutorial/properties.md b/docs/manual/lean/lean_tutorial/properties.md
similarity index 100%
rename from docs/manual/lean_tutorial/properties.md
rename to docs/manual/lean/lean_tutorial/properties.md
diff --git a/docs/manual/lean_quick_start/index.md b/docs/manual/lean/quick_start.md
similarity index 84%
rename from docs/manual/lean_quick_start/index.md
rename to docs/manual/lean/quick_start.md
index 899cb9572..4f81d894c 100644
--- a/docs/manual/lean_quick_start/index.md
+++ b/docs/manual/lean/quick_start.md
@@ -60,7 +60,7 @@ extract nothing but `my_function`:
 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 function, 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.
+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
@@ -68,13 +68,13 @@ constructs](https://github.com/hacspec/hax?tab=readme-ov-file#supported-subset-o
 `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 have remove it from the extraction target by adding  `-my_crate::f` as an option to the `-i` flag. 
+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 specifications states that the code is panic-free. 
+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` librairies 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)
+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)

From a92257389f98b99e122bd513e6e2e3bd959ed718 Mon Sep 17 00:00:00 2001
From: Maxime Buyse <maxime@cryspen.com>
Date: Mon, 8 Sep 2025 16:37:12 +0200
Subject: [PATCH 10/12] Use github runners instead of self-hosted.

---
 .github/workflows/clippy_rust_engine.yml   | 2 +-
 .github/workflows/rustc-coverage-tests.yml | 2 +-
 2 files changed, 2 insertions(+), 2 deletions(-)

diff --git a/.github/workflows/clippy_rust_engine.yml b/.github/workflows/clippy_rust_engine.yml
index 34044319c..650d6f7a5 100644
--- a/.github/workflows/clippy_rust_engine.yml
+++ b/.github/workflows/clippy_rust_engine.yml
@@ -10,7 +10,7 @@ on:
 jobs:
   clippy:
     name: clippy
-    runs-on: linux
+    runs-on: ubuntu-latest
     steps:
     - uses: actions/checkout@v4
     - name: Run clippy
diff --git a/.github/workflows/rustc-coverage-tests.yml b/.github/workflows/rustc-coverage-tests.yml
index f9dfd1e83..f5f7d9736 100644
--- a/.github/workflows/rustc-coverage-tests.yml
+++ b/.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

From d9dd622612981f4bc0b448e551383f85d8402ca4 Mon Sep 17 00:00:00 2001
From: Maxime Buyse <maxime@cryspen.com>
Date: Mon, 8 Sep 2025 16:42:40 +0200
Subject: [PATCH 11/12] Add step to install clippy.

---
 .github/workflows/clippy_rust_engine.yml | 3 +++
 1 file changed, 3 insertions(+)

diff --git a/.github/workflows/clippy_rust_engine.yml b/.github/workflows/clippy_rust_engine.yml
index 650d6f7a5..aba685473 100644
--- a/.github/workflows/clippy_rust_engine.yml
+++ b/.github/workflows/clippy_rust_engine.yml
@@ -13,6 +13,9 @@ jobs:
     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

From 5127f362a3897d0fefaac710ea246df364f3fc43 Mon Sep 17 00:00:00 2001
From: Maxime Buyse <maxime@cryspen.com>
Date: Mon, 8 Sep 2025 17:54:50 +0200
Subject: [PATCH 12/12] Rename some parts of the manual.

---
 docs/manual/fstar/fstar_tutorial/.nav.yml                       | 1 -
 docs/manual/fstar/index.md                                      | 1 +
 docs/manual/fstar/quick_start.md                                | 2 +-
 .../fstar/{fstar_tutorial => tutorial}/data-invariants.md       | 0
 docs/manual/fstar/{fstar_tutorial => tutorial}/index.md         | 0
 docs/manual/fstar/{fstar_tutorial => tutorial}/panic-freedom.md | 0
 .../proofs/fstar/extraction/Makefile                            | 0
 .../proofs/fstar/extraction/Tutorial_src.Math.Lemmas.fst        | 0
 .../proofs/fstar/extraction/Tutorial_src.fst                    | 0
 docs/manual/fstar/{fstar_tutorial => tutorial}/properties.md    | 0
 docs/manual/lean/index.md                                       | 1 +
 docs/manual/lean/{lean_internals.md => internals.md}            | 2 +-
 docs/manual/lean/quick_start.md                                 | 2 +-
 docs/manual/lean/{lean_tutorial => tutorial}/index.md           | 0
 docs/manual/lean/{lean_tutorial => tutorial}/panic-freedom.md   | 0
 docs/manual/lean/{lean_tutorial => tutorial}/properties.md      | 0
 16 files changed, 5 insertions(+), 4 deletions(-)
 delete mode 100644 docs/manual/fstar/fstar_tutorial/.nav.yml
 create mode 100644 docs/manual/fstar/index.md
 rename docs/manual/fstar/{fstar_tutorial => tutorial}/data-invariants.md (100%)
 rename docs/manual/fstar/{fstar_tutorial => tutorial}/index.md (100%)
 rename docs/manual/fstar/{fstar_tutorial => tutorial}/panic-freedom.md (100%)
 rename docs/manual/fstar/{fstar_tutorial => tutorial}/proofs/fstar/extraction/Makefile (100%)
 rename docs/manual/fstar/{fstar_tutorial => tutorial}/proofs/fstar/extraction/Tutorial_src.Math.Lemmas.fst (100%)
 rename docs/manual/fstar/{fstar_tutorial => tutorial}/proofs/fstar/extraction/Tutorial_src.fst (100%)
 rename docs/manual/fstar/{fstar_tutorial => tutorial}/properties.md (100%)
 create mode 100644 docs/manual/lean/index.md
 rename docs/manual/lean/{lean_internals.md => internals.md} (58%)
 rename docs/manual/lean/{lean_tutorial => tutorial}/index.md (100%)
 rename docs/manual/lean/{lean_tutorial => tutorial}/panic-freedom.md (100%)
 rename docs/manual/lean/{lean_tutorial => tutorial}/properties.md (100%)

diff --git a/docs/manual/fstar/fstar_tutorial/.nav.yml b/docs/manual/fstar/fstar_tutorial/.nav.yml
deleted file mode 100644
index 3a02279c1..000000000
--- a/docs/manual/fstar/fstar_tutorial/.nav.yml
+++ /dev/null
@@ -1 +0,0 @@
-title: F* tutorial
\ No newline at end of file
diff --git a/docs/manual/fstar/index.md b/docs/manual/fstar/index.md
new file mode 100644
index 000000000..e8caab9bc
--- /dev/null
+++ b/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.
\ No newline at end of file
diff --git a/docs/manual/fstar/quick_start.md b/docs/manual/fstar/quick_start.md
index 22394fe2d..02111a988 100644
--- a/docs/manual/fstar/quick_start.md
+++ b/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!
diff --git a/docs/manual/fstar/fstar_tutorial/data-invariants.md b/docs/manual/fstar/tutorial/data-invariants.md
similarity index 100%
rename from docs/manual/fstar/fstar_tutorial/data-invariants.md
rename to docs/manual/fstar/tutorial/data-invariants.md
diff --git a/docs/manual/fstar/fstar_tutorial/index.md b/docs/manual/fstar/tutorial/index.md
similarity index 100%
rename from docs/manual/fstar/fstar_tutorial/index.md
rename to docs/manual/fstar/tutorial/index.md
diff --git a/docs/manual/fstar/fstar_tutorial/panic-freedom.md b/docs/manual/fstar/tutorial/panic-freedom.md
similarity index 100%
rename from docs/manual/fstar/fstar_tutorial/panic-freedom.md
rename to docs/manual/fstar/tutorial/panic-freedom.md
diff --git a/docs/manual/fstar/fstar_tutorial/proofs/fstar/extraction/Makefile b/docs/manual/fstar/tutorial/proofs/fstar/extraction/Makefile
similarity index 100%
rename from docs/manual/fstar/fstar_tutorial/proofs/fstar/extraction/Makefile
rename to docs/manual/fstar/tutorial/proofs/fstar/extraction/Makefile
diff --git a/docs/manual/fstar/fstar_tutorial/proofs/fstar/extraction/Tutorial_src.Math.Lemmas.fst b/docs/manual/fstar/tutorial/proofs/fstar/extraction/Tutorial_src.Math.Lemmas.fst
similarity index 100%
rename from docs/manual/fstar/fstar_tutorial/proofs/fstar/extraction/Tutorial_src.Math.Lemmas.fst
rename to docs/manual/fstar/tutorial/proofs/fstar/extraction/Tutorial_src.Math.Lemmas.fst
diff --git a/docs/manual/fstar/fstar_tutorial/proofs/fstar/extraction/Tutorial_src.fst b/docs/manual/fstar/tutorial/proofs/fstar/extraction/Tutorial_src.fst
similarity index 100%
rename from docs/manual/fstar/fstar_tutorial/proofs/fstar/extraction/Tutorial_src.fst
rename to docs/manual/fstar/tutorial/proofs/fstar/extraction/Tutorial_src.fst
diff --git a/docs/manual/fstar/fstar_tutorial/properties.md b/docs/manual/fstar/tutorial/properties.md
similarity index 100%
rename from docs/manual/fstar/fstar_tutorial/properties.md
rename to docs/manual/fstar/tutorial/properties.md
diff --git a/docs/manual/lean/index.md b/docs/manual/lean/index.md
new file mode 100644
index 000000000..83929d92e
--- /dev/null
+++ b/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.
\ No newline at end of file
diff --git a/docs/manual/lean/lean_internals.md b/docs/manual/lean/internals.md
similarity index 58%
rename from docs/manual/lean/lean_internals.md
rename to docs/manual/lean/internals.md
index 15dadbf33..3b4ea044d 100644
--- a/docs/manual/lean/lean_internals.md
+++ b/docs/manual/lean/internals.md
@@ -3,6 +3,6 @@ weight: 102
 ---
 
 
-# Lean internals
+# Internals
 
 
diff --git a/docs/manual/lean/quick_start.md b/docs/manual/lean/quick_start.md
index 4f81d894c..a6fe3c6d9 100644
--- a/docs/manual/lean/quick_start.md
+++ b/docs/manual/lean/quick_start.md
@@ -2,7 +2,7 @@
 weight: 100
 ---
 
-# Quick start with hax and Lean
+# Quick start
 
 ## Setup the tools
 
diff --git a/docs/manual/lean/lean_tutorial/index.md b/docs/manual/lean/tutorial/index.md
similarity index 100%
rename from docs/manual/lean/lean_tutorial/index.md
rename to docs/manual/lean/tutorial/index.md
diff --git a/docs/manual/lean/lean_tutorial/panic-freedom.md b/docs/manual/lean/tutorial/panic-freedom.md
similarity index 100%
rename from docs/manual/lean/lean_tutorial/panic-freedom.md
rename to docs/manual/lean/tutorial/panic-freedom.md
diff --git a/docs/manual/lean/lean_tutorial/properties.md b/docs/manual/lean/tutorial/properties.md
similarity index 100%
rename from docs/manual/lean/lean_tutorial/properties.md
rename to docs/manual/lean/tutorial/properties.md