Merge pull request #650 from Nadrieril/update-rustc

Bump rustc version by a few weeks

engine/lib/ast.ml

@@ -143,11 +143,8 @@ functor
           ident : impl_ident;
         }
       | ImplApp of { impl : impl_expr; args : impl_expr list }
-      | Dyn of trait_goal
+      | Dyn
       | Builtin of trait_goal
-      | FnPointer of ty
-      (* The `IE` suffix is there because visitors conflicts...... *)
-      | ClosureIE of todo
 
     and trait_goal = { trait : concrete_ident; args : generic_value list }
     (** A fully applied trait: [Foo<SomeTy, T0, ..., Tn>] (or

engine/lib/ast_visitors.ml

@@ -172,18 +172,10 @@ functor
                 self#visit_list self#visit_impl_expr env record_payload.args
               in
               ImplApp { impl; args }
-          | Dyn x0 ->
-              let x0 = self#visit_trait_goal env x0 in
-              Dyn x0
+          | Dyn -> Dyn
           | Builtin x0 ->
               let x0 = self#visit_trait_goal env x0 in
               Builtin x0
-          | FnPointer x0 ->
-              let x0 = self#visit_ty env x0 in
-              FnPointer x0
-          | ClosureIE x0 ->
-              let x0 = self#visit_todo env x0 in
-              ClosureIE x0
 
         method visit_trait_goal (env : 'env) (this : trait_goal) : trait_goal =
           let trait = self#visit_concrete_ident env this.trait in
@@ -1113,18 +1105,10 @@ functor
               in
               let reduce_acc = self#plus reduce_acc reduce_acc' in
               (ImplApp { impl; args }, reduce_acc)
-          | Dyn x0 ->
-              let x0, reduce_acc = self#visit_trait_goal env x0 in
-              (Dyn x0, reduce_acc)
+          | Dyn -> (Dyn, self#zero)
           | Builtin x0 ->
               let x0, reduce_acc = self#visit_trait_goal env x0 in
               (Builtin x0, reduce_acc)
-          | FnPointer x0 ->
-              let x0, reduce_acc = self#visit_ty env x0 in
-              (FnPointer x0, reduce_acc)
-          | ClosureIE x0 ->
-              let x0, reduce_acc = self#visit_todo env x0 in
-              (ClosureIE x0, reduce_acc)
 
         method visit_trait_goal (env : 'env) (this : trait_goal)
             : trait_goal * 'acc =
@@ -2301,18 +2285,10 @@ functor
               in
               let reduce_acc = self#plus reduce_acc reduce_acc' in
               reduce_acc
-          | Dyn x0 ->
-              let reduce_acc = self#visit_trait_goal env x0 in
-              reduce_acc
+          | Dyn -> self#zero
           | Builtin x0 ->
               let reduce_acc = self#visit_trait_goal env x0 in
               reduce_acc
-          | FnPointer x0 ->
-              let reduce_acc = self#visit_ty env x0 in
-              reduce_acc
-          | ClosureIE x0 ->
-              let reduce_acc = self#visit_todo env x0 in
-              reduce_acc
 
         method visit_trait_goal (env : 'env) (this : trait_goal) : 'acc =
           let reduce_acc = self#visit_concrete_ident env this.trait in

engine/lib/import_thir.ml

@@ -938,6 +938,7 @@ end) : EXPR = struct
         TOpaque (Concrete_ident.of_def_id Type def_id)
     | Alias { kind = Inherent; _ } ->
         unimplemented [ span ] "type Alias::Inherent"
+    | Alias { kind = Weak; _ } -> unimplemented [ span ] "type Alias::Weak"
     | Param { index; name } ->
         (* TODO: [id] might not unique *)
         TParam { name; id = Local_ident.mk_id Typ (MyInt64.to_int_exn index) }
@@ -987,11 +988,9 @@ end) : EXPR = struct
     | LocalBound { clause_id; path; _ } ->
         let init = LocalBound { id = clause_id } in
         List.fold ~init ~f:browse_path path
-    | Dyn { trait } -> Dyn (c_trait_ref span trait)
+    | Dyn -> Dyn
     | SelfImpl { path; _ } -> List.fold ~init:Self ~f:browse_path path
     | Builtin { trait } -> Builtin (c_trait_ref span trait)
-    | FnPointer { fn_ty } -> FnPointer (c_ty span fn_ty)
-    | Closure _ as x -> ClosureIE ([%show: Thir.impl_expr_atom] x)
     | Todo str -> failwith @@ "impl_expr_atom: Todo " ^ str
 
   and c_generic_value (span : Thir.span) (ty : Thir.generic_arg) : generic_value

engine/lib/subtype.ml

@@ -70,10 +70,8 @@ struct
             impl = dimpl_expr span impl;
             args = List.map ~f:(dimpl_expr span) args;
           }
-    | Dyn tr -> Dyn (dtrait_goal span tr)
+    | Dyn -> Dyn
     | Builtin tr -> Builtin (dtrait_goal span tr)
-    | ClosureIE todo -> ClosureIE todo
-    | FnPointer ty -> FnPointer (dty span ty)
 
   and dgeneric_value (span : span) (generic_value : A.generic_value) :
       B.generic_value =

frontend/exporter/src/traits.rs

@@ -19,51 +19,55 @@ pub enum ImplExprPathChunk {
     },
 }
 
+/// The source of a particular trait implementation. Most often this is either `Concrete` for a
+/// concrete `impl Trait for Type {}` item, or `LocalBound` for a context-bound `where T: Trait`.
 #[derive(
     Clone, Debug, Hash, PartialEq, Eq, PartialOrd, Ord, Serialize, Deserialize, JsonSchema,
 )]
 pub enum ImplExprAtom {
+    /// A concrete `impl Trait for Type {}` item.
     Concrete {
         id: GlobalIdent,
         generics: Vec<GenericArg>,
     },
+    /// A context-bound clause like `where T: Trait`.
     LocalBound {
         clause_id: u64,
         r#trait: Binder<TraitRef>,
         path: Vec<ImplExprPathChunk>,
     },
+    /// The automatic clause `Self: Trait` present inside a `impl Trait for Type {}` item.
     SelfImpl {
         r#trait: Binder<TraitRef>,
         path: Vec<ImplExprPathChunk>,
     },
-    /// `dyn TRAIT` is a wrapped value with a virtual table for trait
-    /// `TRAIT`.  In other words, a value `dyn TRAIT` is a dependent
+    /// `dyn Trait` is a wrapped value with a virtual table for trait
+    /// `Trait`.  In other words, a value `dyn Trait` is a dependent
     /// triple that gathers a type τ, a value of type τ and an
-    /// instance of type `TRAIT`.
-    Dyn {
-        r#trait: TraitRef,
-    },
-    Builtin {
-        r#trait: TraitRef,
-    },
-    FnPointer {
-        fn_ty: Box<Ty>,
-    },
-    Closure {
-        closure_def_id: DefId,
-        parent_substs: Vec<GenericArg>,
-        signature: Box<PolyFnSig>,
-    },
+    /// instance of type `Trait`.
+    /// `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: TraitRef },
+    /// Anything else. Currently used for trait upcasting and trait aliases.
     Todo(String),
 }
 
+/// An `ImplExpr` describes the full data of a trait implementation. Because of generics, this may
+/// need to combine several concrete trait implementation items. For example, `((1u8, 2u8),
+/// "hello").clone()` combines the generic implementation of `Clone` for `(A, B)` with the
+/// concrete implementations for `u8` and `&str`, represented as a tree.
 #[derive(
     Clone, Debug, Hash, PartialEq, Eq, PartialOrd, Ord, Serialize, Deserialize, JsonSchema,
 )]
 pub struct ImplExpr {
-    pub r#impl: ImplExprAtom,
-    pub args: Box<Vec<ImplExpr>>,
+    /// The trait this is an impl for.
     pub r#trait: 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>,
 }
 
 mod search_clause {
@@ -265,7 +269,7 @@ impl ImplExprAtom {
     fn with_args(self, args: Vec<ImplExpr>, r#trait: TraitRef) -> ImplExpr {
         ImplExpr {
             r#impl: self,
-            args: Box::new(args),
+            args,
             r#trait,
         }
     }
@@ -377,38 +381,13 @@ impl<'tcx> IntoImplExpr<'tcx> for rustc_middle::ty::PolyTraitRef<'tcx> {
                     .with_args(impl_exprs(s, &nested), trait_ref)
                 }
             }
-            // Happens when we use a function pointer as an object implementing
-            // a trait like `FnMut`
-            ImplSource::FnPointer(rustc_trait_selection::traits::ImplSourceFnPointerData {
-                fn_ty,
-                nested,
-            }) => ImplExprAtom::FnPointer {
-                fn_ty: fn_ty.sinto(s),
-            }
-            .with_args(impl_exprs(s, &nested), trait_ref),
-            ImplSource::Closure(rustc_trait_selection::traits::ImplSourceClosureData {
-                closure_def_id,
-                substs,
-                nested,
-            }) => {
-                let substs = substs.as_closure();
-                let parent_substs = substs.parent_substs().sinto(s);
-                let signature = Box::new(substs.sig().sinto(s));
-                ImplExprAtom::Closure {
-                    closure_def_id: closure_def_id.sinto(s),
-                    parent_substs,
-                    signature,
-                }
-                .with_args(impl_exprs(s, &nested), trait_ref)
-            }
-            ImplSource::Object(data) => ImplExprAtom::Dyn {
-                r#trait: data.upcast_trait_ref.skip_binder().sinto(s),
+            ImplSource::Object(data) => {
+                ImplExprAtom::Dyn.with_args(impl_exprs(s, &data.nested), trait_ref)
             }
-            .with_args(impl_exprs(s, &data.nested), trait_ref),
-            ImplSource::Builtin(x) => ImplExprAtom::Builtin {
+            ImplSource::Builtin(nested) => ImplExprAtom::Builtin {
                 r#trait: self.skip_binder().sinto(s),
             }
-            .with_args(impl_exprs(s, &x.nested), trait_ref),
+            .with_args(impl_exprs(s, &nested), trait_ref),
             x => ImplExprAtom::Todo(format!(
                 "ImplExprAtom::Todo(see https://github.com/hacspec/hax/issues/381) {:#?}\n\n{:#?}",
                 x, self
@@ -555,7 +534,7 @@ pub mod copy_paste_from_rustc {
         // Currently, we use a fulfillment context to completely resolve
         // all nested obligations. This is because they can inform the
         // inference of the impl's type parameters.
-        let mut fulfill_cx = <dyn TraitEngine<'tcx>>::new(tcx);
+        let mut fulfill_cx = <dyn TraitEngine<'tcx>>::new(&infcx);
         let impl_source = selection.map(|predicate| {
             fulfill_cx.register_predicate_obligation(&infcx, predicate.clone());
             predicate

frontend/exporter/src/types/copied.rs

@@ -177,15 +177,31 @@ pub enum UnOp {
 #[derive(AdtInto, Copy, Clone, Debug, Serialize, Deserialize, JsonSchema)]
 #[args(<'slt, S: UnderOwnerState<'slt>>, from: rustc_middle::mir::BinOp, state: S as _s)]
 pub enum BinOp {
+    // We merge the checked and unchecked variants because in either case overflow is failure.
+    #[custom_arm(
+        rustc_middle::mir::BinOp::Add | rustc_middle::mir::BinOp::AddUnchecked => BinOp::Add,
+    )]
     Add,
+    #[custom_arm(
+        rustc_middle::mir::BinOp::Sub | rustc_middle::mir::BinOp::SubUnchecked => BinOp::Sub,
+    )]
     Sub,
+    #[custom_arm(
+        rustc_middle::mir::BinOp::Mul | rustc_middle::mir::BinOp::MulUnchecked => BinOp::Mul,
+    )]
     Mul,
     Div,
     Rem,
     BitXor,
     BitAnd,
     BitOr,
+    #[custom_arm(
+        rustc_middle::mir::BinOp::Shl | rustc_middle::mir::BinOp::ShlUnchecked => BinOp::Shl,
+    )]
     Shl,
+    #[custom_arm(
+        rustc_middle::mir::BinOp::Shr | rustc_middle::mir::BinOp::ShrUnchecked => BinOp::Shr,
+    )]
     Shr,
     Eq,
     Lt,
@@ -1546,6 +1562,7 @@ pub struct Alias {
     pub def_id: DefId,
 }
 
+/// Reflects [`rustc_middle::ty::AliasKind`]
 #[derive(
     Clone, Debug, Serialize, Deserialize, JsonSchema, Hash, PartialEq, Eq, PartialOrd, Ord,
 )]
@@ -1557,8 +1574,12 @@ pub enum AliasKind {
         /// The `Type` in `Ty: Trait<..., Type = U>`.
         assoc_item: AssocItem,
     },
+    /// An associated type in an inherent impl.
     Inherent,
+    /// An `impl Trait` opaque type.
     Opaque,
+    /// A type alias that references opaque types. Likely to always be normalized away.
+    Weak,
 }
 
 impl Alias {
@@ -1578,6 +1599,7 @@ impl Alias {
             }
             RustAliasKind::Inherent => AliasKind::Inherent,
             RustAliasKind::Opaque => AliasKind::Opaque,
+            RustAliasKind::Weak => AliasKind::Weak,
         };
         Alias {
             kind,
@@ -3234,6 +3256,8 @@ pub enum ClauseKind {
     TypeOutlives(TypeOutlivesPredicate),
     Projection(ProjectionPredicate),
     ConstArgHasType(ConstantExpr, Ty),
+    WellFormed(GenericArg),
+    ConstEvaluatable(ConstantExpr),
 }
 
 /// Reflects [`rustc_middle::ty::Clause`]
@@ -3362,12 +3386,10 @@ pub enum ClosureKind {
 )]
 pub enum PredicateKind {
     Clause(Clause),
-    WellFormed(GenericArg),
     ObjectSafe(DefId),
     ClosureKind(DefId, Vec<GenericArg>, ClosureKind),
     Subtype(SubtypePredicate),
     Coerce(CoercePredicate),
-    ConstEvaluatable(ConstantExpr),
     ConstEquate(ConstantExpr, ConstantExpr),
     TypeWellFormedFromEnv(Ty),
     Ambiguous,

proof-libs/fstar/core/Alloc.Collections.Binary_heap.fsti

@@ -1,28 +1,27 @@
 module Alloc.Collections.Binary_heap
 open Rust_primitives
 
-val t_BinaryHeap: Type -> eqtype
+val t_BinaryHeap: Type -> unit -> eqtype
 
-val impl_9__new: #t:Type -> t_BinaryHeap t
-val impl_9__push: #t:Type -> t_BinaryHeap t -> t -> t_BinaryHeap t
-val impl_10__len: #t:Type -> t_BinaryHeap t -> usize
-val impl_10__iter: #t:Type -> t_BinaryHeap t -> t_Slice t
+val impl_10__new: #t:Type -> t_BinaryHeap t ()
+val impl_10__push: #t:Type -> t_BinaryHeap t () -> t -> t_BinaryHeap t ()
+val impl_11__len: #t:Type -> t_BinaryHeap t () -> usize
+val impl_11__iter: #t:Type -> t_BinaryHeap t () -> t_Slice t
 
 open Core.Option
 
-val impl_10__peek: #t:Type -> t_BinaryHeap t -> t_Option t
-val impl_9__pop: #t:Type -> t_BinaryHeap t -> t_BinaryHeap t & t_Option t
+val impl_11__peek: #t:Type -> t_BinaryHeap t () -> t_Option t
+val impl_10__pop: #t:Type -> t_BinaryHeap t () -> t_BinaryHeap t () & t_Option t
 
 unfold
-let nonempty h = v (impl_10__len h) > 0
+let nonempty h = v (impl_11__len h) > 0
 
-val lemma_peek_len: #t:Type -> h: t_BinaryHeap t 
-  -> Lemma (Option_Some? (impl_10__peek h) <==> nonempty h)
+val lemma_peek_len: #t:Type -> h: t_BinaryHeap t ()
+  -> Lemma (Option_Some? (impl_11__peek h) <==> nonempty h)
 
-val lemma_pop_len: #t:Type -> h: t_BinaryHeap t 
-  -> Lemma (Option_Some? (snd (impl_9__pop h)) <==> nonempty h)
-
-val lemma_peek_pop: #t:Type -> h: t_BinaryHeap t 
-  -> Lemma (impl_10__peek h == snd (impl_9__pop h))
-          [SMTPat (impl_10__peek h)]
+val lemma_pop_len: #t:Type -> h: t_BinaryHeap t ()
+  -> Lemma (Option_Some? (snd (impl_10__pop h)) <==> nonempty h)
 
+val lemma_peek_pop: #t:Type -> h: t_BinaryHeap t ()
+  -> Lemma (impl_11__peek h == snd (impl_10__pop h))
+          [SMTPat (impl_11__peek h)]

rust-toolchain.toml

@@ -1,3 +1,3 @@
 [toolchain]
-channel = "nightly-2023-06-02"
+channel = "nightly-2023-06-20"
 components = [ "rustc-dev", "llvm-tools-preview" , "rust-analysis" , "rust-src" , "rustfmt" ]

test-harness/src/snapshots/toolchain__traits into-fstar.snap

@@ -82,8 +82,8 @@ let impl_SuperTrait_for_i32: t_SuperTrait i32 =
 
 class t_Foo (v_Self: Type) = {
   f_AssocType:Type;
-  f_AssocType_14574884306673035349:t_SuperTrait f_AssocType;
-  f_AssocType_15671956332092790358:Core.Clone.t_Clone f_AssocType;
+  f_AssocType_7709027004138830043:t_SuperTrait f_AssocType;
+  f_AssocType_11415341696577095690:Core.Clone.t_Clone f_AssocType;
   f_N:usize;
   f_assoc_f_pre:Prims.unit -> bool;
   f_assoc_f_post:Prims.unit -> Prims.unit -> bool;
@@ -130,7 +130,7 @@ let g (#v_T: Type) (#[FStar.Tactics.Typeclasses.tcresolve ()] i1: t_Foo v_T) (x:
 let impl_Foo_for_tuple_: t_Foo Prims.unit =
   {
     f_AssocType = i32;
-    f_AssocType_14574884306673035349 = FStar.Tactics.Typeclasses.solve;
+    f_AssocType_7709027004138830043 = FStar.Tactics.Typeclasses.solve;
     f_N = sz 32;
     f_assoc_f_pre = (fun (_: Prims.unit) -> true);
     f_assoc_f_post = (fun (_: Prims.unit) (out: Prims.unit) -> true);