Update hax

charon-ml/src/CharonVersion.ml

@@ -1,3 +1,3 @@
 (* This is an automatically generated file, generated from `charon/Cargo.toml`. *)
 (* To re-generate this file, rune `make` in the root directory *)
-let supported_charon_version = "0.1.62"
+let supported_charon_version = "0.1.63"

charon-ml/src/PrintTypes.ml

@@ -302,7 +302,7 @@ and trait_instance_id_to_string (env : 'a fmt_env) (id : trait_instance_id) :
       let impl = trait_impl_id_to_string env id in
       let generics = generic_args_to_string env generics in
       impl ^ generics
-  | BuiltinOrAuto trait ->
+  | BuiltinOrAuto (trait, _, _) ->
       region_binder_to_string trait_decl_ref_to_string env trait
   | Clause id -> trait_db_var_to_string env id
   | ParentClause (inst_id, _decl_id, clause_id) ->

charon-ml/src/generated/Generated_GAstOfJson.ml

@@ -984,11 +984,29 @@ and trait_instance_id_of_json (ctx : of_json_ctx) (js : json) :
         let* x_2 = trait_clause_id_of_json ctx x_2 in
         Ok (ParentClause (x_0, x_1, x_2))
     | `String "SelfId" -> Ok Self
-    | `Assoc [ ("BuiltinOrAuto", builtin_or_auto) ] ->
-        let* builtin_or_auto =
-          region_binder_of_json trait_decl_ref_of_json ctx builtin_or_auto
+    | `Assoc
+        [
+          ( "BuiltinOrAuto",
+            `Assoc
+              [
+                ("trait_decl_ref", trait_decl_ref);
+                ("parent_trait_refs", parent_trait_refs);
+                ("types", types);
+              ] );
+        ] ->
+        let* trait_decl_ref =
+          region_binder_of_json trait_decl_ref_of_json ctx trait_decl_ref
+        in
+        let* parent_trait_refs =
+          vector_of_json trait_clause_id_of_json trait_ref_of_json ctx
+            parent_trait_refs
+        in
+        let* types =
+          list_of_json
+            (pair_of_json trait_item_name_of_json ty_of_json)
+            ctx types
         in
-        Ok (BuiltinOrAuto builtin_or_auto)
+        Ok (BuiltinOrAuto (trait_decl_ref, parent_trait_refs, types))
     | `Assoc [ ("Dyn", dyn) ] ->
         let* dyn = region_binder_of_json trait_decl_ref_of_json ctx dyn in
         Ok (Dyn dyn)

charon-ml/src/generated/Generated_Types.ml

@@ -263,9 +263,20 @@ and trait_instance_id =
           is useful to give priority to the local clauses when solving the trait
           obligations which are fullfilled by the trait parameters.
        *)
-  | BuiltinOrAuto of trait_decl_ref region_binder
-      (** A specific builtin trait implementation like [core::marker::Sized] or
-          auto trait implementation like [core::marker::Syn].
+  | BuiltinOrAuto of
+      trait_decl_ref region_binder
+      * trait_ref list
+      * (trait_item_name * ty) list
+      (** A trait implementation that is computed by the compiler, such as for built-in traits
+          `Sized` or `FnMut`. This morally points to an invisible `impl` block; as such it contains
+          the information we may need from one.
+
+          Fields:
+          - [trait_decl_ref]
+          - [parent_trait_refs]:  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`.
+          - [types]:  The values of the associated types for this trait.
        *)
   | Dyn of trait_decl_ref region_binder
       (** The automatically-generated implementation for `dyn Trait`. *)

charon/Cargo.toml

@@ -1,6 +1,6 @@
 [package]
 name = "charon"
-version = "0.1.62"
+version = "0.1.63"
 authors = ["Son Ho <hosonmarc@gmail.com>"]
 edition = "2021"
 license = "Apache-2.0"
@@ -78,8 +78,7 @@ tracing = { version = "0.1", features = [ "max_level_trace" ] }
 wait-timeout = { version = "0.2.0", optional = true }
 which = "7.0"
 
-# hax-frontend-exporter = { git = "https://github.com/cryspen/hax", branch = "main", optional = true }
-hax-frontend-exporter = { git = "https://github.com/Nadrieril/hax", branch = "fix-clause-order", optional = true }
+hax-frontend-exporter = { git = "https://github.com/cryspen/hax", branch = "main", optional = true }
 # hax-frontend-exporter = { path = "../../hax/frontend/exporter", optional = true }
 macros = { path = "./macros" }
 

charon/src/ast/types.rs

@@ -124,9 +124,18 @@ pub enum TraitRefKind {
     #[charon::rename("Self")]
     SelfId,
 
-    /// A specific builtin trait implementation like [core::marker::Sized] or
-    /// auto trait implementation like [core::marker::Syn].
-    BuiltinOrAuto(PolyTraitDeclRef),
+    /// A trait implementation that is computed by the compiler, such as for built-in traits
+    /// `Sized` or `FnMut`. This morally points to an invisible `impl` block; as such it contains
+    /// the information we may need from one.
+    BuiltinOrAuto {
+        trait_decl_ref: PolyTraitDeclRef,
+        /// 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`.
+        parent_trait_refs: Vector<TraitClauseId, TraitRef>,
+        /// The values of the associated types for this trait.
+        types: Vec<(TraitItemName, Ty)>,
+    },
 
     /// The automatically-generated implementation for `dyn Trait`.
     Dyn(PolyTraitDeclRef),

charon/src/bin/charon-driver/translate/translate_ctx.rs

@@ -1008,6 +1008,10 @@ impl<'tcx, 'ctx> BodyTransCtx<'tcx, 'ctx> {
         self.t_ctx.translate_span_from_hax(rspan)
     }
 
+    pub(crate) fn hax_def(&mut self, def_id: impl Into<DefId>) -> Result<Arc<hax::FullDef>, Error> {
+        self.t_ctx.hax_def(def_id.into())
+    }
+
     pub(crate) fn def_span(&mut self, def_id: impl Into<DefId>) -> Span {
         self.t_ctx.def_span(def_id)
     }

charon/src/bin/charon-driver/translate/translate_predicates.rs

@@ -211,17 +211,17 @@ impl<'tcx, 'ctx> BodyTransCtx<'tcx, 'ctx> {
         trace!("impl_expr: {:#?}", impl_source);
         use hax::ImplExprAtom;
 
-        let nested = &impl_source.args;
         let trait_ref = match &impl_source.r#impl {
             ImplExprAtom::Concrete {
                 id: impl_def_id,
                 generics,
+                impl_exprs,
             } => {
                 let impl_id = self.register_trait_impl_id(span, impl_def_id);
                 let generics = self.translate_generic_args(
                     span,
                     generics,
-                    nested,
+                    impl_exprs,
                     None,
                     GenericsSource::item(impl_id),
                 )?;
@@ -240,7 +240,6 @@ impl<'tcx, 'ctx> BodyTransCtx<'tcx, 'ctx> {
                 path,
                 ..
             } => {
-                assert!(nested.is_empty());
                 trace!(
                     "impl source (self or clause): param:\n- trait_ref: {:?}\n- path: {:?}",
                     trait_ref,
@@ -318,10 +317,34 @@ impl<'tcx, 'ctx> BodyTransCtx<'tcx, 'ctx> {
                 kind: TraitRefKind::Dyn(trait_decl_ref.clone()),
                 trait_decl_ref,
             },
-            ImplExprAtom::Builtin { .. } => TraitRef {
-                kind: TraitRefKind::BuiltinOrAuto(trait_decl_ref.clone()),
-                trait_decl_ref,
-            },
+            ImplExprAtom::Builtin {
+                impl_exprs, types, ..
+            } => {
+                let parent_trait_refs = self.translate_trait_impl_exprs(span, &impl_exprs)?;
+                let types = types
+                    .iter()
+                    .map(|(def_id, ty)| {
+                        let item_def = self.hax_def(def_id)?;
+                        let ty = self.translate_ty(span, ty)?;
+                        let hax::FullDefKind::AssocTy {
+                            associated_item, ..
+                        } = item_def.kind()
+                        else {
+                            unreachable!()
+                        };
+                        let name = TraitItemName(associated_item.name.clone());
+                        Ok((name, ty))
+                    })
+                    .try_collect()?;
+                TraitRef {
+                    kind: TraitRefKind::BuiltinOrAuto {
+                        trait_decl_ref: trait_decl_ref.clone(),
+                        parent_trait_refs,
+                        types,
+                    },
+                    trait_decl_ref,
+                }
+            }
             ImplExprAtom::Error(msg) => {
                 let trait_ref = TraitRef {
                     kind: TraitRefKind::Unknown(msg.clone()),

charon/src/pretty/fmt_with_ctx.rs

@@ -1302,7 +1302,27 @@ impl<C: AstFormatter> FmtWithCtx<C> for TraitRefKind {
                 format!("{impl_}{args}")
             }
             TraitRefKind::Clause(id) => ctx.format_object(*id),
-            TraitRefKind::BuiltinOrAuto(tr) | TraitRefKind::Dyn(tr) => tr.fmt_with_ctx(ctx),
+            TraitRefKind::BuiltinOrAuto {
+                trait_decl_ref: tr,
+                types,
+                ..
+            } => {
+                let tr = tr.fmt_with_ctx(ctx);
+                let types = if types.is_empty() {
+                    String::new()
+                } else {
+                    let types = types
+                        .iter()
+                        .map(|(name, ty)| {
+                            let ty = ty.fmt_with_ctx(ctx);
+                            format!("{name}  = {ty}")
+                        })
+                        .join(", ");
+                    format!(" where {types}")
+                };
+                format!("{tr}{types}")
+            }
+            TraitRefKind::Dyn(tr) => tr.fmt_with_ctx(ctx),
             TraitRefKind::Unknown(msg) => format!("UNKNOWN({msg})"),
         }
     }

charon/tests/cargo/dependencies.out

@@ -44,7 +44,7 @@ fn test_cargo_dependencies::silly_incr<'_0>(@1: &'_0 mut (u32))
 
     @3 := &two-phase-mut *(x@1)
     @4 := {test_cargo_dependencies::silly_incr::closure} {}
-    @2 := take_mut::take<'_, u32, fn(u32) -> u32>[core::marker::Sized<u32>, core::marker::Sized<fn(u32) -> u32>, core::ops::function::FnOnce<fn(u32) -> u32, (u32)>](move (@3), move (@4))
+    @2 := take_mut::take<'_, u32, fn(u32) -> u32>[core::marker::Sized<u32>, core::marker::Sized<fn(u32) -> u32>, core::ops::function::FnOnce<fn(u32) -> u32, (u32)> where Output  = u32](move (@3), move (@4))
     drop @4
     drop @3
     drop @2

charon/tests/ui/impl-trait.out

@@ -233,7 +233,7 @@ fn test_crate::use_wrap()
     @6 := &@7
     @5 := &*(@6)
     @4 := (move (@5))
-    @2 := core::ops::function::FnOnce<fn<'_0>(&'_0_0 (u32)) -> test_crate::WrapClone<&'_0_0 (u32)>[core::marker::Sized<&'_1_0 (u32)>, core::clone::impls::{impl core::clone::Clone for &'_0 (T)}#3<'_, u32>], (&'_ (u32))>::call_once(move (@3), move (@4))
+    @2 := core::ops::function::FnOnce<fn<'_0>(&'_0_0 (u32)) -> test_crate::WrapClone<&'_0_0 (u32)>[core::marker::Sized<&'_1_0 (u32)>, core::clone::impls::{impl core::clone::Clone for &'_0 (T)}#3<'_, u32>], (&'_ (u32))> where Output  = test_crate::WrapClone<&'_ (u32)>[core::marker::Sized<&'_ (u32)>, core::clone::impls::{impl core::clone::Clone for &'_0 (T)}#3<'_, u32>]::call_once(move (@3), move (@4))
     drop @5
     drop @4
     drop @3

charon/tests/ui/unsupported/advanced-const-generics.out

@@ -43,6 +43,20 @@ error: Item `test_crate::foo` caused errors; ignoring.
    | ^^^^^^^^^^^^^^^^^^^^^^^^^^^^^
    |
 
-error: aborting due to 1 previous error
+disabled backtrace
+warning[E9999]: Failed to compute associated type <T as std::marker::DiscriminantKind>::Discriminant
+ --> /rustc/86d69c705a552236a622eee3fdea94bf13c5f102/library/core/src/intrinsics.rs:2556:5
+  |
+  = note: ⚠️ This is a bug in Hax's frontend.
+          Please report this error to https://github.com/hacspec/hax/issues with some context (e.g. the current crate)!
+
+disabled backtrace
+warning[E9999]: Failed to compute associated type <Self as std::marker::DiscriminantKind>::Discriminant
+ --> /rustc/86d69c705a552236a622eee3fdea94bf13c5f102/library/core/src/marker.rs:823:5
+  |
+  = note: ⚠️ This is a bug in Hax's frontend.
+          Please report this error to https://github.com/hacspec/hax/issues with some context (e.g. the current crate)!
+
+error: aborting due to 1 previous error; 2 warnings emitted
 
 ERROR Compilation encountered 3 errors