Use the new trait solver.

creusot-args/src/lib.rs

@@ -11,6 +11,7 @@ pub const CREUSOT_RUSTC_ARGS: &[&str] = &[
     "-Zcrate-attr=feature(proc_macro_hygiene)",
     "-Zcrate-attr=feature(rustc_attrs)",
     "-Zcrate-attr=feature(unsized_fn_params)",
+    "-Znext-solver=globally",
     "--allow=internal_features",
     "--cfg",
     "creusot",

creusot-contracts/src/std/ops.rs

@@ -5,7 +5,9 @@ pub use ::std::ops::*;
 /// `FnOnceExt` is an extension trait for the `FnOnce` trait, used for
 /// adding a specification to closures. It should not be used directly.
 #[rustc_diagnostic_item = "fn_once_spec"]
-pub trait FnOnceExt<Args: Tuple>: FnOnce<Args> {
+pub trait FnOnceExt<Args: Tuple> {
+    type Output;
+
     #[predicate]
     fn precondition(self, a: Args) -> bool;
 
@@ -16,7 +18,7 @@ pub trait FnOnceExt<Args: Tuple>: FnOnce<Args> {
 /// `FnMutExt` is an extension trait for the `FnMut` trait, used for
 /// adding a specification to closures. It should not be used directly.
 #[rustc_diagnostic_item = "fn_mut_spec"]
-pub trait FnMutExt<Args: Tuple>: FnMut<Args> + FnOnceExt<Args> {
+pub trait FnMutExt<Args: Tuple>: FnOnceExt<Args> {
     #[predicate]
     fn postcondition_mut(&mut self, _: Args, _: Self::Output) -> bool;
 
@@ -48,7 +50,7 @@ pub trait FnMutExt<Args: Tuple>: FnMut<Args> + FnOnceExt<Args> {
 /// `FnExt` is an extension trait for the `Fn` trait, used for
 /// adding a specification to closures. It should not be used directly.
 #[rustc_diagnostic_item = "fn_spec"]
-pub trait FnExt<Args: Tuple>: Fn<Args> + FnMutExt<Args> {
+pub trait FnExt<Args: Tuple>: FnMutExt<Args> {
     #[predicate]
     fn postcondition(&self, _: Args, _: Self::Output) -> bool;
 
@@ -64,6 +66,8 @@ pub trait FnExt<Args: Tuple>: Fn<Args> + FnMutExt<Args> {
 }
 
 impl<Args: Tuple, F: FnOnce<Args>> FnOnceExt<Args> for F {
+    type Output = <Self as FnOnce<Args>>::Output;
+
     #[predicate]
     #[trusted]
     #[rustc_diagnostic_item = "fn_once_impl_precond"]
@@ -140,21 +144,19 @@ impl<Args: Tuple, F: Fn<Args>> FnExt<Args> for F {
 extern_spec! {
     mod std {
         mod ops {
-            // FIXME: we should not need the `Self :` bounds, because they are implied by the main trait bound.
-            // But if we remove them, some test fail.
-            trait FnOnce<Args> where Self : FnOnceExt<Args>, Args : Tuple {
+            trait FnOnce<Args> where Args : Tuple {
                 #[requires(self.precondition(arg))]
                 #[ensures(self.postcondition_once(arg, result))]
                 fn call_once(self, arg: Args) -> Self::Output;
             }
 
-            trait FnMut<Args> where Self : FnMutExt<Args>, Args : Tuple {
+            trait FnMut<Args> where Args : Tuple {
                 #[requires((*self).precondition(arg))]
                 #[ensures(self.postcondition_mut(arg, result))]
                 fn call_mut(&mut self, arg: Args) -> Self::Output;
             }
 
-            trait Fn<Args> where Self : FnExt<Args>, Args : Tuple {
+            trait Fn<Args> where Args : Tuple {
                 #[requires((*self).precondition(arg))]
                 #[ensures(self.postcondition(arg, result))]
                 fn call(&self, arg: Args) -> Self::Output;

creusot/src/backend/clone_map/elaborator.rs

@@ -498,8 +498,8 @@ pub fn term<'tcx>(
             } else if is_resolve_function(ctx.tcx, def_id) {
                 resolve_term(ctx, param_env, def_id, subst)
             } else if is_structural_resolve(ctx.tcx, def_id) {
-                let sig = ctx.sig(def_id).clone();
-                structural_resolve(ctx, sig.inputs[0].0, subst.type_at(0))
+                let subj = ctx.sig(def_id).inputs[0].0;
+                structural_resolve(ctx, subj, subst.type_at(0))
             } else {
                 let term = ctx.ctx.term(def_id).unwrap().clone();
                 let term = normalize(

creusot/src/backend/logic/vcgen.rs

@@ -345,9 +345,7 @@ impl<'a, 'tcx> VCGen<'a, 'tcx> {
             TermKind::Tuple { fields } => self.build_vc_slice(fields, &|flds| k(Exp::Tuple(flds))),
             // Same as for tuples
             TermKind::Constructor { variant, fields, .. } => {
-                let ty =
-                    self.ctx.borrow().normalize_erasing_regions(self.param_env, t.creusot_ty());
-                let TyKind::Adt(adt, subst) = ty.kind() else { unreachable!() };
+                let TyKind::Adt(adt, subst) = t.creusot_ty().kind() else { unreachable!() };
                 self.build_vc_slice(fields, &|fields| {
                     let ctor = constructor(
                         *self.names.borrow_mut(),
@@ -406,9 +404,7 @@ impl<'a, 'tcx> VCGen<'a, 'tcx> {
             }),
             // VC(A.f, Q) = VC(A, |a| Q(a.f))
             TermKind::Projection { lhs, name } => {
-                let ty =
-                    self.ctx.borrow().normalize_erasing_regions(self.param_env, lhs.creusot_ty());
-                let field = match ty.kind() {
+                let field = match lhs.creusot_ty().kind() {
                     TyKind::Closure(did, substs) => {
                         self.names.borrow_mut().field(*did, substs, *name).as_ident()
                     }
@@ -462,9 +458,8 @@ impl<'a, 'tcx> VCGen<'a, 'tcx> {
             Pattern::Constructor { variant, fields, substs } => {
                 let fields =
                     fields.into_iter().map(|pat| self.build_pattern_inner(bounds, pat)).collect();
-                let substs = self.ctx.borrow().normalize_erasing_regions(self.param_env, *substs);
                 if self.ctx.borrow().def_kind(variant) == DefKind::Variant {
-                    Pat::ConsP(self.names.borrow_mut().constructor(*variant, substs), fields)
+                    Pat::ConsP(self.names.borrow_mut().constructor(*variant, *substs), fields)
                 } else if fields.len() == 0 {
                     Pat::TupleP(vec![])
                 } else {

creusot/src/backend/term.rs

@@ -122,8 +122,7 @@ impl<'tcx, N: Namer<'tcx>> Lower<'_, 'tcx, N> {
                 }
             }
             TermKind::Constructor { variant, fields, .. } => {
-                let ty = self.names.normalize(self.ctx, term.creusot_ty());
-                let TyKind::Adt(adt, subst) = ty.kind() else { unreachable!() };
+                let TyKind::Adt(adt, subst) = term.creusot_ty().kind() else { unreachable!() };
                 let fields = fields.into_iter().map(|f| self.lower_term(f)).collect();
                 constructor(self.names, fields, adt.variant(*variant).def_id, subst)
             }
@@ -173,10 +172,9 @@ impl<'tcx, N: Namer<'tcx>> Lower<'_, 'tcx, N> {
                 Exp::Tuple(fields.into_iter().map(|f| self.lower_term(f)).collect())
             }
             TermKind::Projection { box lhs, name } => {
-                let base_ty = self.names.normalize(self.ctx, lhs.creusot_ty());
-                let lhs = self.lower_term(lhs);
+                let lhs_low = self.lower_term(lhs);
 
-                let field = match base_ty.kind() {
+                let field = match lhs.creusot_ty().kind() {
                     TyKind::Closure(did, substs) => self.names.field(*did, substs, *name),
                     TyKind::Adt(def, substs) => self.names.field(def.did(), substs, *name),
                     TyKind::Tuple(f) => {
@@ -185,14 +183,14 @@ impl<'tcx, N: Namer<'tcx>> Lower<'_, 'tcx, N> {
 
                         return Exp::Let {
                             pattern: Pat::TupleP(fields),
-                            arg: Box::new(lhs),
+                            arg: Box::new(lhs_low),
                             body: Box::new(Exp::var("a")),
                         };
                     }
                     k => unreachable!("Projection from {k:?}"),
                 };
 
-                lhs.field(&field.as_ident())
+                lhs_low.field(&field.as_ident())
             }
             TermKind::Closure { body, .. } => {
                 let TyKind::Closure(id, subst) = term.creusot_ty().kind() else {
@@ -203,10 +201,10 @@ impl<'tcx, N: Namer<'tcx>> Lower<'_, 'tcx, N> {
                 let mut binders = Vec::new();
                 let sig = self.ctx.sig(*id).clone();
                 let sig = EarlyBinder::bind(sig).instantiate(self.ctx.tcx, subst);
-                // FIXME: normalize sig
                 for arg in sig.inputs.iter().skip(1) {
-                    binders
-                        .push(Binder::typed(Ident::build(&arg.0.to_string()), self.lower_ty(arg.2)))
+                    let nm = Ident::build(&arg.0.to_string());
+                    let ty = self.names.normalize(self.ctx, arg.2);
+                    binders.push(Binder::typed(nm, self.lower_ty(ty)))
                 }
 
                 Exp::Abs(binders, Box::new(body))
@@ -232,9 +230,8 @@ impl<'tcx, N: Namer<'tcx>> Lower<'_, 'tcx, N> {
         match pat {
             Pattern::Constructor { variant, fields, substs } => {
                 let fields = fields.into_iter().map(|pat| self.lower_pat(pat)).collect();
-                let substs = self.names.normalize(self.ctx, *substs);
                 if self.ctx.def_kind(variant) == DefKind::Variant {
-                    Pat::ConsP(self.names.constructor(*variant, substs), fields)
+                    Pat::ConsP(self.names.constructor(*variant, *substs), fields)
                 } else if fields.len() == 0 {
                     Pat::TupleP(vec![])
                 } else {

creusot/src/ctx.rs

@@ -32,6 +32,7 @@ use rustc_hir::{
     def::DefKind,
     def_id::{DefId, LocalDefId},
 };
+use rustc_infer::traits::ObligationCause;
 use rustc_macros::{TypeFoldable, TypeVisitable};
 use rustc_middle::{
     mir::{Body, Promoted, TerminatorKind},
@@ -41,6 +42,7 @@ use rustc_middle::{
     },
 };
 use rustc_span::{Span, Symbol};
+use rustc_trait_selection::traits::normalize_param_env_or_error;
 use std::{collections::HashMap, ops::Deref};
 
 pub(crate) use crate::{backend::clone_map::*, translated_item::*};
@@ -398,15 +400,7 @@ impl<'tcx, 'sess> TranslationCtx<'tcx> {
                 .collect::<Vec<_>>();
             let res =
                 ParamEnv::new(self.mk_clauses(&clauses), rustc_infer::traits::Reveal::UserFacing);
-            // FIXME: param envs should be normalized (this is an invariant of the trait solver),
-            // but calling this function here causes an overflow in the handling of PartialEq::eq
-            // I see two solutions:
-            //    1- Wait for the next trait solver that does not need this (I think).
-            //    2- Allow adding new generic type variables in extern specs, so that we could write
-            //             Self: DeepModel<DeepModelTy = T>,
-            //             Rhs: DeepModel<DeepModelTy = T>;
-            //
-            // let res = normalize_param_env_or_error(self.tcx, res, ObligationCause::dummy());
+            let res = normalize_param_env_or_error(self.tcx, res, ObligationCause::dummy());
             res
         } else {
             self.tcx.param_env(def_id)

creusot/src/translation/function/terminator.rs

@@ -335,7 +335,6 @@ impl<'tcx> BodyTranslator<'_, 'tcx> {
             return;
         }
         // We are indeed in program code.
-        let func_param_env = self.ctx.param_env(fun_def_id);
 
         // Check that we do not call `GhostBox::into_inner` in normal code
         if is_ghost_into_inner(self.ctx.tcx, fun_def_id) {
@@ -379,6 +378,7 @@ impl<'tcx> BodyTranslator<'_, 'tcx> {
                 )
                 .emit();
         } else {
+            let func_param_env = self.ctx.param_env(fun_def_id);
             // Check and reject instantiation of a <T: Deref> with a ghost parameter.
             let deref_trait_id = self.ctx.require_lang_item(rustc_hir::LangItem::Deref, None);
             let infer_ctx = self.ctx.infer_ctxt().build();

creusot/src/translation/pearlite/normalize.rs

@@ -14,8 +14,7 @@ pub(crate) fn normalize<'tcx>(
     mut term: Term<'tcx>,
 ) -> Term<'tcx> {
     NormalizeTerm { param_env, tcx }.visit_mut_term(&mut term);
-    // FIXME: we should normalize here, but it diverges when normalizing specification of partial_eq
-    // let term = tcx.normalize_erasing_regions(param_env, term);
+    let term = tcx.normalize_erasing_regions(param_env, term);
     term
 }
 
@@ -38,7 +37,6 @@ impl<'tcx> TermVisitorMut<'tcx> for NormalizeTerm<'tcx> {
                     *id = method.0;
                     *subst = method.1;
                 }
-                *subst = self.tcx.normalize_erasing_regions(self.param_env, *subst);
 
                 if is_box_new(self.tcx, *id) {
                     let arg = args.remove(0);

creusot/src/translation/specification.rs

@@ -377,12 +377,17 @@ pub(crate) fn contract_of<'tcx>(
         let mut contract =
             extern_spec.contract.get_pre(ctx, fn_name).instantiate(ctx.tcx, extern_spec.subst);
         contract.subst(&extern_spec.arg_subst.iter().cloned().collect());
-        contract.normalize(ctx.tcx, ctx.param_env(def_id))
+        // We do NOT normalize the contract here. See below.
+        contract
     } else if let Some((parent_id, subst)) = inherited_extern_spec(ctx, def_id) {
         let spec = ctx.extern_spec(parent_id).cloned().unwrap();
         let mut contract = spec.contract.get_pre(ctx, fn_name).instantiate(ctx.tcx, subst);
         contract.subst(&spec.arg_subst.iter().cloned().collect());
-        contract.normalize(ctx.tcx, ctx.param_env(def_id))
+        // We do NOT normalize the contract here: indeed, we do not have a valid non-redundant param
+        // env for doing this. This is still valid because this contract is going to be substituted
+        // and normalized in the caller context (such extern specs are only evaluated in the context
+        // of a specific call).
+        contract
     } else {
         let subst = erased_identity_for_item(ctx.tcx, def_id);
         let mut contract = contract_clauses_of(ctx, def_id)
@@ -427,7 +432,6 @@ pub(crate) fn pre_sig_of<'tcx>(
     ctx: &mut TranslationCtx<'tcx>,
     def_id: DefId,
 ) -> PreSignature<'tcx> {
-    let param_env = ctx.param_env(def_id);
     let (inputs, output) = inputs_and_output(ctx.tcx, def_id);
 
     let mut contract = crate::specification::contract_of(ctx, def_id);
@@ -461,7 +465,7 @@ pub(crate) fn pre_sig_of<'tcx>(
 
             let term = Term::call(
                 ctx.tcx,
-                param_env,
+                ctx.param_env(def_id),
                 unnest_id,
                 unnest_subst,
                 vec![Term::var(self_, env_ty).cur(), Term::var(self_, env_ty).fin()],
@@ -546,7 +550,7 @@ pub(crate) fn pre_sig_of<'tcx>(
         }
     }
 
-    PreSignature { inputs, output, contract }.normalize(ctx.tcx, param_env)
+    PreSignature { inputs, output, contract }
 }
 
 fn inputs_and_output<'tcx>(