V1.82

rust-toolchain.toml

@@ -1,4 +1,4 @@
 [toolchain]
-channel = "1.79.0"
+channel = "1.82.0"
 # channel = "nightly-2023-09-29" # TODO update to match 1.79.0 (not officially supported)
 components = [ "rustc", "rust-std", "cargo", "rustfmt", "rustc-dev", "llvm-tools" ]

source/builtin_macros/src/syntax.rs

@@ -662,7 +662,7 @@ impl Visitor {
                 self.inside_ghost += 1;
                 self.visit_expr_mut(&mut expr);
                 self.inside_ghost -= 1;
-                stmts.push(Stmt::Expr(Expr::Verbatim(quote_spanned!(con_span => #[verus::internal(verus_macro)] #[verus::internal(const_body)] fn __VERUS_CONST_BODY__() -> #con_ty { #expr } ))));
+                stmts.push(Stmt::Expr(Expr::Verbatim(quote_spanned!(con_span => #[allow(non_snake_case)]#[verus::internal(verus_macro)] #[verus::internal(const_body)] fn __VERUS_CONST_BODY__() -> #con_ty { #expr } ))));
                 stmts.push(Stmt::Expr(Expr::Verbatim(
                     quote_spanned!(con_span => unsafe { core::mem::zeroed() }),
                 )));

source/rust_verify/src/expand_errors_driver.rs

@@ -550,7 +550,8 @@ impl ExpandErrorsDriver {
         let s = if matches!(
             error_format,
             Some(rustc_session::config::ErrorOutputType::HumanReadable(
-                rustc_errors::emitter::HumanReadableErrorType::Short(_)
+                rustc_errors::emitter::HumanReadableErrorType::Short,
+                _
             ))
         ) {
             "diagnostics via expansion".into()

source/rust_verify/src/fn_call_to_vir.rs

@@ -196,9 +196,9 @@ pub(crate) fn fn_call_to_vir<'tcx>(
         let mut target_kind = vir::ast::CallTargetKind::Dynamic;
         let param_env = tcx.param_env(bctx.fun_id);
         let normalized_substs = tcx.normalize_erasing_regions(param_env, node_substs);
-        let inst = rustc_middle::ty::Instance::resolve(tcx, param_env, f, normalized_substs);
+        let inst = rustc_middle::ty::Instance::try_resolve(tcx, param_env, f, normalized_substs);
         if let Ok(Some(inst)) = inst {
-            if let rustc_middle::ty::InstanceDef::Item(did) = inst.def {
+            if let rustc_middle::ty::InstanceKind::Item(did) = inst.def {
                 let typs = mk_typ_args(bctx, &inst.args, did, expr.span)?;
                 let mut f =
                     Arc::new(FunX { path: def_id_to_vir_path(tcx, &bctx.ctxt.verus_items, did) });

source/rust_verify/src/lifetime.rs

@@ -205,6 +205,8 @@ pub(crate) fn check<'tcx>(queries: &'tcx rustc_interface::Queries<'tcx>) {
 }
 
 const PRELUDE: &str = "\
+#![feature(negative_impls)]
+#![feature(with_negative_coherence)]
 #![feature(box_patterns)]
 #![feature(ptr_metadata)]
 #![feature(never_type)]

source/rust_verify/src/lifetime_ast.rs

@@ -181,6 +181,7 @@ pub(crate) struct TraitImpl {
     pub(crate) generic_bounds: Vec<GenericBound>,
     // use Datatype(Id, Vec<Typ>) to represent (trait_path, trait_typ_args)
     pub(crate) trait_as_datatype: Typ,
+    pub(crate) trait_polarity: rustc_middle::ty::ImplPolarity,
     pub(crate) assoc_typs: Vec<(Id, Vec<GenericParam>, Typ)>,
 }
 

source/rust_verify/src/lifetime_emit.rs

@@ -1068,14 +1068,24 @@ pub(crate) fn emit_datatype_decl(state: &mut EmitState, d: &DatatypeDecl) {
 }
 
 pub(crate) fn emit_trait_impl(state: &mut EmitState, t: &TraitImpl) {
-    let TraitImpl { span, trait_as_datatype, self_typ, generic_params, generic_bounds, assoc_typs } =
-        t;
+    let TraitImpl {
+        span,
+        trait_as_datatype,
+        self_typ,
+        generic_params,
+        generic_bounds,
+        assoc_typs,
+        trait_polarity,
+    } = t;
     state.newdecl();
     state.newline();
     state.begin_span_opt(*span);
     state.write("impl");
     emit_generic_params(state, &generic_params);
     state.write(" ");
+    if trait_polarity == &rustc_middle::ty::ImplPolarity::Negative {
+        state.write("!");
+    }
     state.write(&trait_as_datatype.to_string());
     state.write(" for ");
     state.write(&self_typ.to_string());

source/rust_verify/src/lifetime_generate.rs

@@ -11,12 +11,12 @@ use rustc_hir::def::{CtorKind, DefKind, Res};
 use rustc_hir::{
     AssocItemKind, Block, BlockCheckMode, BodyId, Closure, Crate, Expr, ExprKind, FnSig, HirId,
     Impl, ImplItem, ImplItemKind, ItemKind, LetExpr, LetStmt, MaybeOwner, Node, OpaqueTy,
-    OpaqueTyOrigin, OwnerNode, Pat, PatKind, Stmt, StmtKind, TraitFn, TraitItem, TraitItemKind,
-    TraitItemRef, UnOp, Unsafety,
+    OpaqueTyOrigin, OwnerNode, Pat, PatKind, Safety, Stmt, StmtKind, TraitFn, TraitItem,
+    TraitItemKind, TraitItemRef, UnOp,
 };
 use rustc_middle::ty::{
     AdtDef, BoundRegionKind, BoundVariableKind, ClauseKind, Const, GenericArgKind,
-    GenericParamDefKind, RegionKind, Ty, TyCtxt, TyKind, TypeckResults, VariantDef,
+    GenericParamDefKind, RegionKind, TermKind, Ty, TyCtxt, TyKind, TypeckResults, VariantDef,
 };
 use rustc_span::def_id::DefId;
 use rustc_span::symbol::kw;
@@ -342,8 +342,8 @@ fn add_copy_type(ctxt: &mut Context, state: &mut State, id: DefId) {
                     let did = adt_def_data.did;
                     let generics = tcx.generics_of(id);
                     let mut copy_bounds: Vec<(Id, bool)> = Vec::new();
-                    if generics.params.len() == args.len() {
-                        for (param, arg) in generics.params.iter().zip(args.iter()) {
+                    if generics.own_params.len() == args.len() {
+                        for (param, arg) in generics.own_params.iter().zip(args.iter()) {
                             let name = state.typ_param(param.name.to_string(), Some(param.index));
                             copy_bounds.push((name, false));
                             if let GenericArgKind::Type(arg_ty) = arg.unpack() {
@@ -556,7 +556,7 @@ fn erase_ty<'tcx>(ctxt: &Context<'tcx>, state: &mut State, ty: &Ty<'tcx>) -> Typ
             };
             Box::new(TypX::Datatype(datatype_name, Vec::new(), typ_args))
         }
-        TyKind::Alias(rustc_middle::ty::AliasKind::Projection, t) => {
+        TyKind::Alias(rustc_middle::ty::AliasTyKind::Projection, t) => {
             // Note: even if rust_to_vir_base decides to normalize t,
             // we don't have to normalize t here, since we're generating Rust code, not VIR.
             // However, normalizing means we might reach less stuff so it's
@@ -597,7 +597,7 @@ fn erase_ty<'tcx>(ctxt: &Context<'tcx>, state: &mut State, ty: &Ty<'tcx>) -> Typ
             let projection_generics = ctxt.tcx.generics_of(t.def_id);
             let trait_def = projection_generics.parent;
             if let Some(trait_def) = trait_def {
-                let n = t.args.len() - projection_generics.params.len();
+                let n = t.args.len() - projection_generics.own_params.len();
                 let (trait_typ_args, self_typ) =
                     erase_generic_args(ctxt, state, &t.args[..n], true);
                 let (assoc_typ_args, _) = erase_generic_args(ctxt, state, &t.args[n..], false);
@@ -988,14 +988,14 @@ fn erase_call<'tcx>(
             );
 
             let normalized_substs = ctxt.tcx.normalize_erasing_regions(param_env, node_substs);
-            let inst = rustc_middle::ty::Instance::resolve(
+            let inst = rustc_middle::ty::Instance::try_resolve(
                 ctxt.tcx,
                 param_env,
                 fn_def_id,
                 normalized_substs,
             );
             if let Ok(Some(inst)) = inst {
-                if let rustc_middle::ty::InstanceDef::Item(did) = inst.def {
+                if let rustc_middle::ty::InstanceKind::Item(did) = inst.def {
                     node_substs = &inst.args;
                     fn_def_id = did;
                 }
@@ -1273,7 +1273,10 @@ fn erase_expr<'tcx>(
                         return mk_exp(ExpX::Call(fun_exp, vec![], vec![]));
                     }
                 }
-                Res::Def(DefKind::Static { mutability: Mutability::Not, nested: false }, id) => {
+                Res::Def(
+                    DefKind::Static { mutability: Mutability::Not, nested: false, .. },
+                    id,
+                ) => {
                     if expect_spec || ctxt.var_modes[&expr.hir_id] == Mode::Spec {
                         None
                     } else {
@@ -1876,35 +1879,39 @@ fn erase_mir_predicates<'a, 'tcx>(
                 }
             }
             ClauseKind::Projection(pred) => {
-                if Some(pred.projection_ty.def_id) == tcx.lang_items().fn_once_output() {
-                    assert!(pred.projection_ty.args.len() == 2);
-                    let typ = erase_ty(ctxt, state, &pred.projection_ty.args[0].expect_ty());
-                    let mut fn_params = match pred.projection_ty.args[1].unpack() {
+                if Some(pred.projection_term.def_id) == tcx.lang_items().fn_once_output() {
+                    assert!(pred.projection_term.args.len() == 2);
+                    let typ = erase_ty(ctxt, state, &pred.projection_term.args[0].expect_ty());
+                    let mut fn_params = match pred.projection_term.args[1].unpack() {
                         GenericArgKind::Type(ty) => erase_ty(ctxt, state, &ty),
                         _ => panic!("unexpected fn projection"),
                     };
                     if !matches!(*fn_params, TypX::Tuple(_)) {
                         fn_params = Box::new(TypX::Tuple(vec![fn_params]));
                     }
-                    let fn_ret = erase_ty(ctxt, state, &pred.term.ty().expect("fn_ret"));
+                    let fn_ret = if let TermKind::Ty(ty) = pred.term.unpack() {
+                        erase_ty(ctxt, state, &ty)
+                    } else {
+                        panic!("fn_ret");
+                    };
                     fn_projections.insert(typ, (fn_params, fn_ret)).map(|_| panic!("{:?}", pred));
                 } else {
-                    let typ0 = erase_ty(ctxt, state, &pred.projection_ty.args[0].expect_ty());
-                    let typ_eq = if let Some(ty) = pred.term.ty() {
+                    let typ0 = erase_ty(ctxt, state, &pred.projection_term.args[0].expect_ty());
+                    let typ_eq = if let TermKind::Ty(ty) = pred.term.unpack() {
                         erase_ty(ctxt, state, &ty)
                     } else {
                         panic!("should have been disallowed by rust_verify_base.rs");
                     };
-                    let trait_def_id = pred.projection_ty.trait_def_id(tcx);
-                    let item_def_id = pred.projection_ty.def_id;
+                    let trait_def_id = pred.projection_term.trait_def_id(tcx);
+                    let item_def_id = pred.projection_term.def_id;
                     let assoc_item = tcx.associated_item(item_def_id);
                     let projection_generics = ctxt.tcx.generics_of(item_def_id);
-                    let n = pred.projection_ty.args.len() - projection_generics.params.len();
+                    let n = pred.projection_term.args.len() - projection_generics.own_params.len();
                     let mut bound =
-                        erase_mir_bound(ctxt, state, trait_def_id, &pred.projection_ty.args[..n])
+                        erase_mir_bound(ctxt, state, trait_def_id, &pred.projection_term.args[..n])
                             .expect("bound");
                     let (x_args, _) =
-                        erase_generic_args(ctxt, state, &pred.projection_ty.args[n..], true);
+                        erase_generic_args(ctxt, state, &pred.projection_term.args[n..], true);
                     let x_args = x_args.into_iter().map(|a| a.as_lifetime()).collect();
                     if let Bound::Trait { trait_path: _, args: _, equality } = &mut bound {
                         assert!(equality.is_none());
@@ -1957,7 +1964,7 @@ fn erase_mir_generics<'tcx>(
             }
         }
     }
-    for gparam in &mir_generics.params {
+    for gparam in &mir_generics.own_params {
         match gparam.kind {
             GenericParamDefKind::Lifetime => {
                 let name = state.lifetime((gparam.name.to_string(), None));
@@ -1967,7 +1974,7 @@ fn erase_mir_generics<'tcx>(
                 let name = state.typ_param(gparam.name.to_string(), Some(gparam.index));
                 typ_params.push(GenericParam { name, const_typ: None });
             }
-            GenericParamDefKind::Const { has_default: _, is_host_effect: false } => {
+            GenericParamDefKind::Const { has_default: _, is_host_effect: false, .. } => {
                 let name = state.typ_param(gparam.name.to_string(), None);
                 let t = erase_ty(ctxt, state, &ctxt.tcx.type_of(gparam.def_id).skip_binder());
                 typ_params.push(GenericParam { name, const_typ: Some(t) });
@@ -2243,14 +2250,39 @@ fn erase_impl_assocs<'tcx>(ctxt: &Context<'tcx>, state: &mut State, impl_id: Def
         }
     }
 
+    let trait_polarity = ctxt.tcx.impl_polarity(impl_id);
     let trait_impl = TraitImpl {
         span: Some(span),
         generic_params,
         generic_bounds,
-        self_typ,
+        self_typ: self_typ.clone(),
+        trait_polarity,
         trait_as_datatype,
         assoc_typs,
     };
+
+    // v1.80 stablized Iterator and IntoIterator for Box.
+    // It needs to implement !Iterartor to avoid conflicts.
+    // The lifetime checking does not reserve polarity.
+    /*if matches!(name.raw_id.as_str(), "Iterator" | "IntoIterator") {
+        let skip = match self_typ.as_ref() {
+            // found both positive and negative implementation of trait `T55_Iterator` for type `&mut std::boxed::Box<[_], _>
+            TypX::Ref(r, ..) => {
+                if let TypX::Datatype(sid, ..) = r.as_ref() {
+                    sid.raw_id == "Box"
+                } else {
+                    false
+                }
+            }
+            TypX::Datatype(sid, ..) if sid.raw_id == "Box" => true,
+            _ => false,
+        };
+        if skip {
+            println!("skip  = {:?} {:?} {:?}", self_typ, trait_polarity, name);
+            return;
+        }
+    }*/
+
     state.trait_impls.push(trait_impl);
 }
 
@@ -2570,7 +2602,7 @@ fn erase_variant_data<'tcx>(
 fn erase_abstract_datatype<'tcx>(ctxt: &Context<'tcx>, state: &mut State, span: Span, id: DefId) {
     let mut fields: Vec<Typ> = Vec::new();
     let mir_generics = ctxt.tcx.generics_of(id);
-    for gparam in mir_generics.params.iter() {
+    for gparam in mir_generics.own_params.iter() {
         // Rust requires all lifetime/type variables to be mentioned in the fields,
         // so introduce a dummy field for each lifetime/type variable
         match gparam.kind {
@@ -2774,7 +2806,7 @@ pub(crate) fn gen_check_tracked_lifetimes<'tcx>(
                         }
                         ItemKind::Trait(
                             IsAuto::No,
-                            Unsafety::Normal,
+                            Safety::Safe,
                             _trait_generics,
                             _bounds,
                             _trait_items,
@@ -2879,7 +2911,7 @@ pub(crate) fn gen_check_tracked_lifetimes<'tcx>(
                         }
                         ItemKind::Trait(
                             IsAuto::No,
-                            Unsafety::Normal,
+                            Safety::Safe,
                             _trait_generics,
                             _bounds,
                             trait_items,
@@ -2915,7 +2947,6 @@ pub(crate) fn gen_check_tracked_lifetimes<'tcx>(
                             origin: OpaqueTyOrigin::AsyncFn(_),
                             in_trait: _,
                             lifetime_mapping: _,
-                            precise_capturing_args: None,
                         }) => {
                             continue;
                         }

source/rust_verify/src/rust_to_vir.rs

@@ -22,7 +22,7 @@ use std::collections::HashSet;
 use rustc_ast::IsAuto;
 use rustc_hir::{
     ForeignItem, ForeignItemId, ForeignItemKind, ImplItemKind, Item, ItemId, ItemKind, MaybeOwner,
-    Mutability, OpaqueTy, OpaqueTyOrigin, OwnerNode, Unsafety,
+    Mutability, OpaqueTy, OpaqueTyOrigin, OwnerNode, Safety,
 };
 use vir::def::Spanned;
 
@@ -290,7 +290,7 @@ fn check_item<'tcx>(
             unsupported_err!(item.span, "static mut");
         }
         ItemKind::Macro(_, _) => {}
-        ItemKind::Trait(IsAuto::No, Unsafety::Normal, trait_generics, _bounds, trait_items) => {
+        ItemKind::Trait(IsAuto::No, Safety::Safe, trait_generics, _bounds, trait_items) => {
             let trait_def_id = item.owner_id.to_def_id();
             crate::rust_to_vir_trait::translate_trait(
                 ctxt,
@@ -321,7 +321,6 @@ fn check_item<'tcx>(
             origin: OpaqueTyOrigin::AsyncFn(_),
             in_trait: _,
             lifetime_mapping: _,
-            precise_capturing_args: None,
         }) => {
             return Ok(());
         }
@@ -339,7 +338,7 @@ fn check_foreign_item<'tcx>(
     item: &'tcx ForeignItem<'tcx>,
 ) -> Result<(), VirErr> {
     match &item.kind {
-        ForeignItemKind::Fn(decl, idents, generics) => {
+        ForeignItemKind::Fn(rustc_hir::FnSig { decl, .. }, idents, generics) => {
             check_foreign_item_fn(
                 ctxt,
                 vir,

source/rust_verify/src/rust_to_vir_adts.rs

@@ -46,6 +46,10 @@ where
         Some(VariantData::Struct { fields, recovered }) => {
             // 'recovered' means that it was recovered from a syntactic error.
             // So we shouldn't get to this point if 'recovered' is true.
+            let recovered = match recovered {
+                rustc_ast::Recovered::No => false,
+                _ => true,
+            };
             unsupported_err_unless!(!recovered, span, "recovered_struct", variant_data_opt);
             Some(*fields)
         }