Merge branch 'main' into AST-EBNF-documentation

.github/workflows/mlkem.yml

@@ -33,7 +33,7 @@ jobs:
           nix profile install ./hax
 
       - name: ⤵ Install FStar
-        run: nix profile install github:FStarLang/FStar/v2024.01.13
+        run: nix profile install github:FStarLang/FStar/v2024.12.03
 
       - name: ⤵ Clone HACL-star repository
         uses: actions/checkout@v4

.github/workflows/stale.yml

@@ -1,7 +1,7 @@
 name: 'Triage stale issues and PRs'
 on:
   schedule:
-    - cron: '00 1 * * *'
+    - cron: '00 00 * * 4'
   workflow_dispatch:
 
 jobs:

Cargo.toml

@@ -32,7 +32,7 @@ default-members = [
 resolver = "2"
 
 [workspace.package]
-version = "0.1.0-alpha.1"
+version = "0.1.0-rc.1"
 authors = ["hax Authors"]
 license = "Apache-2.0"
 homepage = "https://github.com/hacspec/hax"
@@ -71,15 +71,14 @@ colored = "2"
 annotate-snippets = "0.11"
 
 # Crates in this repository
-hax-frontend-exporter = { path = "frontend/exporter", version = "=0.1.0-alpha.1", default-features = false }
-hax-adt-into = { path = "frontend/exporter/adt-into", version = "=0.1.0-alpha.1" }
-hax-frontend-exporter-options = { path = "frontend/exporter/options", version = "=0.1.0-alpha.1" }
-hax-lib-macros = { path = "hax-lib/macros", version = "=0.1.0-alpha.1" }
-hax-lib-macros-types = { path = "hax-lib/macros/types", version = "=0.1.0-alpha.1" }
-hax-lib = { path = "hax-lib", version = "=0.1.0-alpha.1" }
-hax-engine-names = { path = "engine/names", version = "=0.1.0-alpha.1" }
-hax-types = { path = "hax-types", version = "=0.1.0-alpha.1" }
+hax-frontend-exporter = { path = "frontend/exporter", version = "=0.1.0-rc.1", default-features = false }
+hax-adt-into = { path = "frontend/exporter/adt-into", version = "=0.1.0-rc.1" }
+hax-frontend-exporter-options = { path = "frontend/exporter/options", version = "=0.1.0-rc.1" }
+hax-lib-macros = { path = "hax-lib/macros", version = "=0.1.0-rc.1" }
+hax-lib-macros-types = { path = "hax-lib/macros/types", version = "=0.1.0-rc.1" }
+hax-lib = { path = "hax-lib", version = "=0.1.0-rc.1" }
+hax-engine-names = { path = "engine/names", version = "=0.1.0-rc.1" }
+hax-types = { path = "hax-types", version = "=0.1.0-rc.1" }
 
 [workspace.metadata.release]
-owners = ["github:hacspec:crates"]
-
+owners = ["github:hacspec:crates"]

PUBLISHING.md

@@ -49,7 +49,7 @@ engine. Those should not be published on `crate.io`.
 2. `cargo-hax-engine-names-extract`
 
 ## Procedure
- 1. Bump the version number with `cargo release LEVEL --no-publish --execute` (`cargo release --help` for more details on `LEVEL`). This will bump the version of every Rust crate, but also the version in `engine/dune-project`. This will also regenerate `engine/hax-engine.opam`. Note this will *not* publish the crate.
+ 1. Bump the version number with `cargo release LEVEL --no-publish --no-tag --execute` (`cargo release --help` for more details on `LEVEL`). This will bump the version of every Rust crate, but also the version in `engine/dune-project`. This will also regenerate `engine/hax-engine.opam`. Note this will *not* publish the crate.
  2. PR the change
  3. when the PR is merged in main, checkout `main` and run `cargo release --execute`
 

README.md

@@ -106,13 +106,14 @@ manager</a> <i>(with <a href="https://nixos.wiki/wiki/Flakes">flakes</a> enabled
 4. Get a shell: `docker run -it --rm -v /some/dir/with/a/crate:/work hax bash`
 5. You can now run `cargo-hax --help` (notice here we use `cargo-hax` instead of `cargo hax`)
 
+Note: Please make sure that `$HOME/.cargo/bin` is in your `$PATH`, as
+that is where `setup.sh` will install hax.
+
 </details>
 
 ## Supported Subset of the Rust Language
 
-Hax intends to support full Rust, with the two following exceptions, promoting a functional style:
- 1. no `unsafe` code (see https://github.com/hacspec/hax/issues/417);
- 2. mutable references (aka `&mut T`) on return types or when aliasing (see https://github.com/hacspec/hax/issues/420).
+Hax intends to support full Rust, with the one exception, promoting a functional style: mutable references (aka `&mut T`) on return types or when aliasing (see https://github.com/hacspec/hax/issues/420) are forbidden.
 
 Each unsupported Rust feature is documented as an issue labeled [`unsupported-rust`](https://github.com/hacspec/hax/issues?q=is%3Aissue+is%3Aopen+label%3Aunsupported-rust). When the issue is labeled [`wontfix-v1`](https://github.com/hacspec/hax/issues?q=is%3Aissue+is%3Aopen+label%3Aunsupported-rust+label%3Awontfix%2Cwontfix-v1), that means we don't plan on supporting that feature soon.
 

book/src/contributing/intro.md

@@ -0,0 +1,4 @@
+# Contributing
+This chapter contains information about internals of hax.
+
+Please read the [`CONTRIBUTING.md`](https://github.com/hacspec/hax/blob/main/CONTRIBUTING.md) before opening a pull request.

cli/driver/src/exporter.rs

@@ -286,6 +286,7 @@ impl Callbacks for ExtractionCallbacks {
                             .flatten()
                             .collect(),
                         def_ids,
+                        hax_version: hax_types::HAX_VERSION.into(),
                     };
                     haxmeta.write(&mut file, cache_map);
                 }

cli/subcommands/build.rs

@@ -14,7 +14,7 @@ fn rustc_version_env_var() {
 }
 
 fn json_schema_static_asset() {
-    let schema = schemars::schema_for!((
+    let mut schema = schemars::schema_for!((
         hax_frontend_exporter::Item<hax_frontend_exporter::ThirBody>,
         hax_types::cli_options::Options,
         hax_types::diagnostics::Diagnostics,
@@ -25,6 +25,7 @@ fn json_schema_static_asset() {
         hax_types::engine_api::protocol::ToEngine,
         hax_lib_macros_types::AttrPayload,
     ));
+    schema.schema.metadata.get_or_insert_default().id = Some(hax_types::HAX_VERSION.into());
     serde_json::to_writer(
         std::fs::File::create(format!("{}/schema.json", std::env::var("OUT_DIR").unwrap()))
             .unwrap(),

cli/subcommands/src/cargo_hax.rs

@@ -240,6 +240,7 @@ fn run_engine(
     message_format: MessageFormat,
 ) -> bool {
     let engine_options = EngineOptions {
+        hax_version: haxmeta.hax_version,
         backend: backend.clone(),
         input: haxmeta.items,
         impl_infos: haxmeta.impl_infos,
@@ -532,6 +533,7 @@ fn compute_haxmeta_files(options: &Options) -> (Vec<EmitHaxMetaMessage>, i32) {
     } else {
         0
     };
+
     (haxmeta_files, exit_code)
 }
 

engine/backends/coq/coq/coq_backend.ml

@@ -407,14 +407,19 @@ struct
       method item'_Impl ~super ~generics ~self_ty ~of_trait ~items
           ~parent_bounds:_ ~safety:_ =
         let name, args = of_trait#v in
-        CoqNotation.instance
-          (name#p ^^ string "_" ^^ string (Int.to_string ([%hash: item] super)))
-          generics#p []
-          (name#p ^^ concat_map (fun x -> space ^^ parens x#p) args)
-          (braces
-             (nest 2
-                (concat_map (fun x -> break 1 ^^ name#p ^^ !^"_" ^^ x#p) items)
-             ^^ break 1))
+        if Attrs.is_erased super.attrs then empty
+        else
+          CoqNotation.instance
+            (name#p ^^ string "_"
+            ^^ string (Int.to_string ([%hash: item] super)))
+            generics#p []
+            (name#p ^^ concat_map (fun x -> space ^^ parens x#p) args)
+            (braces
+               (nest 2
+                  (concat_map
+                     (fun x -> break 1 ^^ name#p ^^ !^"_" ^^ x#p)
+                     items)
+               ^^ break 1))
 
       method item'_NotImplementedYet = string "(* NotImplementedYet *)"
 

engine/backends/fstar/fstar_ast.ml

@@ -9,6 +9,7 @@ module Ident = FStar_Ident
 
 let dummyRange = Range.dummyRange
 let id ident = Ident.mk_ident (ident, dummyRange)
+let id_prime (ident : Ident.ident) = id (ident.idText ^ "'")
 
 let lid path =
   let init, last = List.(drop_last_exn path, last_exn path) in
@@ -87,6 +88,7 @@ let mk_refined (x : string) (typ : AST.term) (phi : x:AST.term -> AST.term) =
   term @@ AST.Refine (x_bd, phi (term @@ AST.Var (lid_of_id x)))
 
 let type0_term = AST.Name (lid [ "Type0" ]) |> term
+let eqtype_term = AST.Name (lid [ "eqtype" ]) |> term
 
 let parse_string f s =
   let open FStar_Parser_ParseIt in