Merge branch 'main' into fix-1177

Cargo.toml

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

PUBLISHING.md

@@ -58,3 +58,9 @@ Note: for now, we are not publishing to Opam. Instead, let's just advertise the
 opam pin hax-engine https://github.com/hacspec/hax.git#the-release-tag
 opam install hax-engine
 ```
+
+## Notes
+`cargo release` reads the `Cargo.toml` of each crates of the workspace.
+Some creates are excluded from releasing: in their `Cargo.toml` manifest, they have `package.metadata.release.release` set to `false`.
+
+Also, `cli/subcommands/Cargo.toml` specifies pre-release replacements for the engine: the version of the engine is bumped automatically by `cargo release`.

engine/dune-project

@@ -2,7 +2,7 @@
 
 (name hax-engine)
 
-(version 0.1.0-rc.1)
+(version 0.1.0)
 
 (generate_opam_files true)
 

engine/hax-engine.opam

@@ -1,6 +1,6 @@
 # This file is generated by dune, edit dune-project instead
 opam-version: "2.0"
-version: "0.1.0-rc.1"
+version: "0.1.0"
 synopsis: "The engine of hax, a Rust verification tool"
 description:
   "Hax is divided in two: a frontend (written in Rust) and an engine (written in OCaml). This is the engine."

engine/lib/import_thir.ml

@@ -1099,11 +1099,12 @@ end) : EXPR = struct
   and c_impl_expr (span : Thir.span) (ie : Thir.impl_expr) : impl_expr =
     let goal = c_trait_ref span ie.trait.value in
     let impl = { kind = c_impl_expr_atom span ie.impl; goal } in
-    match ie.args with
-    | [] -> impl
-    | args ->
-        let args = List.map ~f:(c_impl_expr span) args in
+    match ie.impl with
+    | Concrete { impl_exprs = []; _ } -> impl
+    | Concrete { impl_exprs; _ } ->
+        let args = List.map ~f:(c_impl_expr span) impl_exprs in
         { kind = ImplApp { impl; args }; goal }
+    | _ -> impl
 
   and c_trait_ref span (tr : Thir.trait_ref) : trait_goal =
     let trait = Concrete_ident.of_def_id Trait tr.def_id in
@@ -1137,7 +1138,7 @@ end) : EXPR = struct
           Parent { impl = { kind = item_kind; goal = trait_ref }; ident }
     in
     match ie with
-    | Concrete { id; generics } ->
+    | Concrete { id; generics; _ } ->
         let trait = Concrete_ident.of_def_id Impl id in
         let args = List.map ~f:(c_generic_value span) generics in
         Concrete { trait; args }
@@ -1146,7 +1147,7 @@ end) : EXPR = struct
         List.fold ~init ~f:browse_path path
     | Dyn -> Dyn
     | SelfImpl { path; _ } -> List.fold ~init:Self ~f:browse_path path
-    | Builtin { trait } -> Builtin (c_trait_ref span trait.value)
+    | Builtin { trait; _ } -> Builtin (c_trait_ref span trait.value)
     | Error str -> failwith @@ "impl_expr_atom: Error " ^ str
 
   and c_generic_value (span : Thir.span) (ty : Thir.generic_arg) : generic_value

frontend/exporter/src/traits.rs

@@ -62,6 +62,8 @@ pub enum ImplExprAtom {
         #[from(def_id)]
         id: GlobalIdent,
         generics: Vec<GenericArg>,
+        /// The impl exprs that prove the clauses on the impl.
+        impl_exprs: Vec<ImplExpr>,
     },
     /// A context-bound clause like `where T: Trait`.
     LocalBound {
@@ -90,8 +92,18 @@ pub enum ImplExprAtom {
     /// `dyn Trait` implements `Trait` using a built-in implementation; this refers to that
     /// built-in implementation.
     Dyn,
-    /// A built-in trait whose implementation is computed by the compiler, such as `Sync`.
-    Builtin { r#trait: Binder<TraitRef> },
+    /// A built-in trait whose implementation is computed by the compiler, such as `FnMut`. This
+    /// morally points to an invisible `impl` block; as such it contains the information we may
+    /// need from one.
+    Builtin {
+        r#trait: Binder<TraitRef>,
+        /// The `ImplExpr`s required to satisfy the implied predicates on the trait declaration.
+        /// E.g. since `FnMut: FnOnce`, a built-in `T: FnMut` impl would have an `ImplExpr` for `T:
+        /// FnOnce`.
+        impl_exprs: Vec<ImplExpr>,
+        /// The values of the associated types for this trait.
+        types: Vec<(DefId, Ty)>,
+    },
     /// An error happened while resolving traits.
     Error(String),
 }
@@ -108,8 +120,6 @@ pub struct ImplExpr {
     pub r#trait: Binder<TraitRef>,
     /// The kind of implemention of the root of the tree.
     pub r#impl: ImplExprAtom,
-    /// A list of `ImplExpr`s required to fully specify the trait references in `impl`.
-    pub args: Vec<ImplExpr>,
 }
 
 /// Given a clause `clause` in the context of some impl block `impl_did`, susbts correctly `Self`