Merge branch 'main' into update-rustc

Author: maximebuyse

.github/workflows/clippy_rust_engine.yml

@@ -0,0 +1,18 @@
+name: Linting for the Rust engine
+
+on:
+  pull_request:
+  merge_group:
+  workflow_dispatch:
+  push:
+    branches: [main]
+
+jobs:
+  clippy:
+    name: clippy
+    runs-on: linux
+    steps:
+    - uses: actions/checkout@v4
+    - name: Run clippy
+      run: |
+        cargo clippy -p rust-printer -- --no-deps

Cargo.lock

@@ -15,6 +15,7 @@ members = [
      "engine/names/extract",
      "hax-types",
      "rust-printer",
+     "rust-printer/macros",
 ]
 exclude = ["tests", "rustc-coverage-tests", "rust-printer/tests"]
 default-members = [

Cargo.toml

@@ -0,0 +1,48 @@
+---
+authors:
+  - maxime
+title: "This Month in Hax: May 2025"
+date: 2025-05-05
+---
+
+In May, we successfully merged **19 pull requests**!
+
+[@Nadrieril](https://github.com/Nadrieril) helped making the frontend more robust and complete with work on impl exprs ([#1431](https://github.com/cryspen/hax/pull/1431)), MIR extraction ([#1444](https://github.com/cryspen/hax/pull/1444), [#1457](https://github.com/cryspen/hax/pull/1457)) and `FnOnce` ([#1477](https://github.com/cryspen/hax/pull/1477)).
+
+[@W95Psp](https://github.com/W95Psp) worked on `hax-lib` with improved support for writing F* lemmas in Rust ([#1456](https://github.com/cryspen/hax/pull/1456)).
+
+[@cmester0](https://github.com/cmester0) improved the Coq and SSProve backends ([#1426](https://github.com/cryspen/hax/pull/1426) and [#1108](https://github.com/cryspen/hax/pull/1108))
+
+Apart from that, we contributed multiple F* [`core` library](https://doc.rust-lang.org/stable/core/) additions.
+
+Stay tuned for more updates next month!
+
+### Full list of PRs
+
+* \#1481: [Update owners metadata](https://github.com/cryspen/hax/pull/1481)
+* \#1477: [Provide the `FnOnce` shim for closures](https://github.com/cryspen/hax/pull/1477)
+* \#1476: [Release 0.3.1](https://github.com/cryspen/hax/pull/1476)
+* \#1473: [fix(proof-libs) Remove fields that shouldn't be in PartialOrd.](https://github.com/cryspen/hax/pull/1473)
+* \#1471: [fix(engine) Add InlineConst in concrete_idents.](https://github.com/cryspen/hax/pull/1471)
+* \#1465: [Release 0.3.0](https://github.com/cryspen/hax/pull/1465)
+* \#1458: [feat(proof-libs): add `rem_euclid` for every int types](https://github.com/cryspen/hax/pull/1458)
+* \#1457: [Simplify MIR place translation](https://github.com/cryspen/hax/pull/1457)
+* \#1456: [Fix unused in lemmas](https://github.com/cryspen/hax/pull/1456)
+* \#1455: [feat(proof-libs): F*: implement some wrapping operations on i64](https://github.com/cryspen/hax/pull/1455)
+* \#1454: [fix(engine/nix): pin ocamlgraph, waiting for https://github.com/NixOS/nixpkgs/pull/397883](https://github.com/cryspen/hax/pull/1454)
+* \#1451: [fix(engine): naming: items under closures](https://github.com/cryspen/hax/pull/1451)
+* \#1445: [Add interfaces to fstar core and rust_primitives](https://github.com/cryspen/hax/pull/1445)
+* \#1444: [Add missing unwind information in MIR](https://github.com/cryspen/hax/pull/1444)
+* \#1439: [Upstream evit changes up to Feb 21](https://github.com/cryspen/hax/pull/1439)
+* \#1438: [This month in hax April 2025.](https://github.com/cryspen/hax/pull/1438)
+* \#1431: [Consistently translate impl exprs for parent items](https://github.com/cryspen/hax/pull/1431)
+* \#1426: [Bertie ssprove](https://github.com/cryspen/hax/pull/1426)
+* \#1108: [Coq small fixes](https://github.com/cryspen/hax/pull/1108)
+
+### Contributors
+* [@Nadrieril](https://github.com/Nadrieril)
+* [@W95Psp](https://github.com/W95Psp)
+* [@clementblaudeau](https://github.com/clementblaudeau)
+* [@cmester0](https://github.com/cmester0)
+* [@franziskuskiefer](https://github.com/franziskuskiefer)
+* [@maximebuyse](https://github.com/maximebuyse)

docs/blog/posts/this-month-in-hax/2025-05.md

@@ -119,7 +119,7 @@ For the crates that successfully generated ASTs, we compared the time taken by `
 - On average, `cargo hax` is about 4–5 times slower than `cargo check`.
 - At the **10th decile**, the slowdown is only about 2×, indicating better scaling for larger crates.
 
-## Conclusion
+### Conclusion
 
 Our quantitative evaluation shows that the hax frontend successfully extracts ASTs for a large portion of the Rust ecosystem. Nevertheless, a small portion of crates reveal performance bottlenecks or outright failures that require further investigation and optimization.
 
@@ -131,3 +131,30 @@ These results also highlight a few **limitations** of this initial study:
 Overall, the hax frontend demonstrates capabilities for large-scale Rust code verification, but continued refinement is needed to handle edge cases and improve performance.
 
 [^1]: For a given crate, we normalize the times by dividing them by the total time.
+
+## Qualitative evaluation
+
+The qualitative evaluation aims at identifying what Rust patterns the frontend can handle. It also tests whether the information extracted from the frontend describes correctly the input Rust code.
+
+### Rustc coverage test suite
+
+The Rust compiler (rustc) has extensive test suites that describe various expectations of how it should handle Rust input. One of them is the [coverage test suite](https://rustc-dev-guide.rust-lang.org/tests/compiletest.html#coverage-tests) which contains a set of Rust inputs that is supposed to cover a wide range of Rust constructs. This test suite has been adapted to test hax.
+
+We use the following methodology:
+- The Rust inputs from the test suite have been copied to `rustc-coverage-tests/src/`, and can be updated using a script.
+- A Rust crate structure is built around these source files, to allow hax to handle them. The files that fail `cargo check` are excluded. There are currently 26 excluded (out of 81) tests, mostly because they contain asynchronous code, which requires a runtime file that is missing in our infrastructure.
+- To test hax frontend, we run `cargo hax json`. If the command succeeds, the test is considered successful.
+
+These tests aim at increasing the confidence in the ability of hax frontend to handle Rust inputs covering all of the language constructs. As of today, all tests are handled successfully by hax frontend. However we don't test any requirement on the output (see the following section for tests of hax frontend output quality).
+
+### Rust printer testing
+
+This method aims at testing the quality of hax frontend's output. It uses a tool that is under development that we call the Rust printer.
+
+This tool (written in Rust) takes the output of hax frontend (a json file describing the content of a Rust crate), it imports it as an AST (similar to the hax engine AST), and then prints this AST in Rust syntax. 
+
+If the Rust code we get out of this tool is equivalent to the Rust code it was given as input, then this means hax frontend correctly extracted the input code without losing or altering any information.
+
+There is no easy way of testing the full input/output equivalence so the methodology here is to test that the resulting code behaves the same as the input code with respect to relevant test cases.
+
+This work is available in the `rust-printer` folder. In the `tests` subfolder, an input file is available with tests for all Rust constructs supported by the printer (currently functions and expressions). For now these tests pass after extracting and printing the file with hax frontend and the Rust printer. This means that for the Rust constructs covered by the printer and the test file, hax frontend's extraction is correct. However this still needs to be extended to test more Rust constructs.

docs/frontend/evaluation.md

@@ -53,7 +53,7 @@ manager</a> <i>(with <a href="https://nixos.wiki/wiki/Flakes">flakes</a> enabled
   - or following [those steps](https://github.com/mschwaig/howto-install-nix-with-flake-support).
 
 + **Run hax on a crate directly** to get F\*/Coq/... (assuming you are in the crate's folder):
-   - `nix run github:hacspec/hax -- into fstar` extracts F*.
+   - `nix run github:hacspec/hax -- into fstar` extracts F\*.
 
 + **Install hax**:  `nix profile install github:hacspec/hax`, then run `cargo hax --help` anywhere
 + **Note**: in any of the Nix commands above, replace `github:hacspec/hax` by `./dir` to compile a local checkout of hax that lives in `./some-dir`

docs/manual/index.md

@@ -2,7 +2,7 @@
 weight: 0
 ---
 
-# Quick start with hax and F*
+# 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,7 +11,7 @@ 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) *(optional: only if want to run F\*)*
 
 ## Setup the crate you want to verify
 
@@ -34,7 +34,7 @@ what you are looking for!
 specific crate you want to extract.*
 
 Run the command `cargo hax into fstar` to extract every item of your
-crate as F* modules in the subfolder `proofs/fstar/extraction`.
+crate as F\* modules in the subfolder `proofs/fstar/extraction`.
 
 **What is critical? What is worth verifying?**  
 Probably, your Rust crate contains mixed kinds of code: some parts are
@@ -68,22 +68,22 @@ about the `-i` flag [in the FAQ](../faq/include-flags.md).
 
 
 
-## Start F* verification
+## 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
-`Makefile` in `proofs/fstar/extraction` will run F*.
+with various F\* modules in the `proofs/fstar/extraction` folder. The
+`Makefile` in `proofs/fstar/extraction` will run F\*.
 
 1. **Lax check:** the first step is to run `OTHERFLAGS="--lax" make`,
-   which will run F* in "lax" mode. The lax mode just makes sure basic
+   which will run F\* in "lax" mode. The lax mode just makes sure basic
    typechecking works: it is not proving anything. This first step is
-   important because there might be missing libraries. If F* is not
+   important because there might be missing libraries. If F\* is not
    able to find a definition, it is probably a `libcore` issue: you
-   probably need to edit the F* library, which lives in the
+   probably need to edit the F\* library, which lives in the
    `proofs-libs` directory in the root of the hax repo.
-2. **Typecheck:** the second step is to run `make`. This will ask F*
+2. **Typecheck:** the second step is to run `make`. This will ask F\*
    to typecheck fully your crate. This is very likely that you need to
    add preconditions and postconditions at this stage. Indeed, this
-   second step is about panic freedom: if F* can typecheck your crate,
+   second step is about panic freedom: if F\* can typecheck your crate,
    it means your code *never* panics, which already is an important
    property.
 

docs/manual/quick_start/index.md

@@ -94,7 +94,7 @@ impl Add for F {
 }
 ```
 
-Here, F* is able to prove automatically that (1) the addition doesn't
+Here, F\* is able to prove automatically that (1) the addition doesn't
 overflow and (2) that the invariant of `F` is preserved. The
-definition of type `F` in F* (named `t_F`) very explicitly requires
+definition of type `F` in F\* (named `t_F`) very explicitly requires
 the invariant as a refinement on `v`.

docs/manual/tutorial/data-invariants.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/) 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/).
+[F\* programming language](https://fstar-lang.org/).