Merge branch 'main' into fun-ty

Author: W95Psp

.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

@@ -71,6 +71,7 @@ impl From<ExtractionCallbacks> for hax_frontend_exporter_options::Options {
     fn from(opts: ExtractionCallbacks) -> hax_frontend_exporter_options::Options {
         hax_frontend_exporter_options::Options {
             inline_anon_consts: true,
+            resolve_drop_bounds: false,
         }
     }
 }

cli/driver/src/exporter.rs

@@ -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/).

docs/manual/tutorial/index.md

@@ -5,7 +5,7 @@ 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
+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.
 
@@ -18,8 +18,8 @@ fn square(x: u8) -> u8 {
 }
 ```
 
-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
+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!
 
@@ -70,7 +70,7 @@ fn square_option(x: u8) -> Option<u8> {
 }
 ```
 
-Here, F* is able to prove panic-freedom: calling `square` with any
+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
@@ -102,7 +102,7 @@ fn square_requires(x: u8) -> u8 {
 }
 ```
 
-With this precondition, F* is able to prove panic freedom. From now
+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.