Handle rustc update

creusot-contracts-dummy/src/lib.rs

@@ -104,7 +104,7 @@ pub fn prusti_logic(_: TS1, _: TS1) -> TS1 {
 }
 
 #[proc_macro_attribute]
-pub fn prusti_ghost(_: TS1, _: TS1) -> TS1 {
+pub fn prusti_logic_prophetic(_: TS1, _: TS1) -> TS1 {
     TS1::new()
 }
 
@@ -113,6 +113,11 @@ pub fn prusti_predicate(_: TS1, _: TS1) -> TS1 {
     TS1::new()
 }
 
+#[proc_macro_attribute]
+pub fn prusti_predicate_prophetic(_: TS1, _: TS1) -> TS1 {
+    TS1::new()
+}
+
 #[proc_macro_attribute]
 pub fn prusti_law(_: TS1, _: TS1) -> TS1 {
     TS1::new()

creusot-contracts-proc/src/lib.rs

@@ -777,47 +777,39 @@ pub fn prusti_ensures_expiry(attr: TS1, tokens: TS1) -> TS1 {
     ensures_helper(rest.into(), tokens, prusti_info)
 }
 
-#[proc_macro_attribute]
-pub fn prusti_logic(attr: TS1, tokens: TS1) -> TS1 {
+fn prusti_logic_gen(attr: TS1, tokens: TS1, creusot_macro: TokenStream, allow_final: bool) -> TS1 {
     let attr = TokenStream::from(attr);
     let tokens = TokenStream::from(tokens);
     let sig = format!("{attr}");
     let sig = LitStr::new(&sig, attr.span());
+    let forbid = if allow_final { None } else { Some(quote!(#[forbid(creusot::prusti_final)])) };
     TS1::from(quote! {
+        #forbid
         #[creusot::prusti::ts="curr"]
         #[creusot::prusti::home_sig=#sig]
-        #[::creusot_contracts::logic]
+        #[::creusot_contracts::#creusot_macro]
         #tokens
     })
 }
 
 #[proc_macro_attribute]
-pub fn prusti_ghost(attr: TS1, tokens: TS1) -> TS1 {
-    let attr = TokenStream::from(attr);
-    let tokens = TokenStream::from(tokens);
-    let sig = format!("{attr}");
-    let sig = LitStr::new(&sig, attr.span());
-    TS1::from(quote! {
-        #[forbid(creusot::prusti_final)]
-        #[creusot::prusti::ts="curr"]
-        #[creusot::prusti::home_sig=#sig]
-        #[::creusot_contracts::ghost]
-        #tokens
-    })
+pub fn prusti_logic(attr: TS1, tokens: TS1) -> TS1 {
+    prusti_logic_gen(attr, tokens, quote!(logic), false)
+}
+
+#[proc_macro_attribute]
+pub fn prusti_logic_prophetic(attr: TS1, tokens: TS1) -> TS1 {
+    prusti_logic_gen(attr, tokens, quote!(logic(prophectic)), true)
 }
 
 #[proc_macro_attribute]
 pub fn prusti_predicate(attr: TS1, tokens: TS1) -> TS1 {
-    let attr = TokenStream::from(attr);
-    let tokens = TokenStream::from(tokens);
-    let sig = format!("{attr}");
-    let sig = LitStr::new(&sig, attr.span());
-    TS1::from(quote! {
-        #[creusot::prusti::ts="curr"]
-        #[creusot::prusti::home_sig=#sig]
-        #[::creusot_contracts::predicate]
-        #tokens
-    })
+    prusti_logic_gen(attr, tokens, quote!(predicate), false)
+}
+
+#[proc_macro_attribute]
+pub fn prusti_predicate_prophetic(attr: TS1, tokens: TS1) -> TS1 {
+    prusti_logic_gen(attr, tokens, quote!(predicate(prophectic)), true)
 }
 
 #[proc_macro_attribute]

creusot-contracts/src/lib.rs

@@ -104,15 +104,11 @@ mod macros {
 
     /// Allows the body of a logical definition to be made visible to provers. An optional visibility modifier can be
     /// provided to restrict the context in whcih the obdy is opened.
-    /// By default bodies are *opaque*: they are only visible to definitions in the same module (like `pub(self)` for visibility).
+    /// By default, bodies are *opaque*: they are only visible to definitions in the same module (like `pub(self)` for visibility).
     ///
     /// A body can only be visible in contexts where all the symbols used in the body are also visible.
     /// This means you cannot `#[open]` a body which refers to a `pub(crate)` symbol.
     pub use base_macros::open;
-
-    pub use base_macros::DeepModel;
-
-    pub use base_macros::Resolve;
 }
 
 #[cfg(creusot)]
@@ -193,8 +189,9 @@ mod base_prelude {
 pub mod prusti_macros {
     pub use base_macros::{
         invariant, open, pearlite, proof_assert, prusti_ensures as ensures,
-        prusti_ensures_expiry as after_expiry, prusti_law as law,
-        prusti_logic as logic, prusti_predicate as predicate, prusti_requires as requires, trusted,
+        prusti_ensures_expiry as after_expiry, prusti_law as law, prusti_logic as logic,
+        prusti_logic_prophetic as logic_prophetic, prusti_predicate as predicate,
+        prusti_predicate_prophetic as predicate_prophetic, prusti_requires as requires, trusted,
         variant,
     };
 }

creusot-contracts/src/prusti.rs

@@ -1,21 +1,21 @@
 use base_macros::*;
 
 /// Equivalent to `at::<'post>`
-#[ghost] // avoid triggering error since this is prusti specific
+#[logic] // avoid triggering error since this is prusti specific
 #[open]
 #[creusot::no_translate]
 #[rustc_diagnostic_item = "prusti_at_post"]
-pub fn at_post<T>(_: T) -> T {
-    absurd
+pub fn at_post<T>(t: T) -> T {
+    t
 }
 
 /// Evaluate an expression at a specific state eg `at::<'state>(exp)`
-#[ghost] // avoid triggering error since this is prusti specific
+#[logic] // avoid triggering error since this is prusti specific
 #[open]
 #[creusot::no_translate]
 #[rustc_diagnostic_item = "prusti_at"]
-pub fn at<'a: 'a, T>(_: T) -> T {
-    absurd
+pub fn at<'a: 'a, T>(t: T) -> T {
+    t
 }
 
 /// Types that do not depend on the program state (e.g. the heap) for validity
@@ -80,7 +80,7 @@ impl<T> Clone for Zombie<T> {
     }
 }
 
-#[ghost] // avoid triggering error since this is prusti specific
+#[logic] // avoid triggering error since this is prusti specific
 #[open]
 #[creusot::no_translate]
 #[rustc_diagnostic_item = "prusti_dbg_ty"]

creusot/Cargo.toml

@@ -20,7 +20,6 @@ tempdir = "0.3.7"
 serde_json = { version = "1.0" }
 lazy_static = "1.4.0"
 internal-iterator = "0.2.*"
-backtrace = "0.3.*"
 # Same as rustc
 smallvec = { version = "^1.8.1", features = [
     "const_generics",

creusot/src/backend/logic/vcgen.rs

@@ -325,7 +325,7 @@ impl<'a, 'tcx> VCGen<'a, 'tcx> {
             // Same as for tuples
             TermKind::Constructor { typ, variant, fields } => {
                 self.build_vc_slice(fields, &|args| {
-                    let TyKind::Adt(_, subst) = t.ty.kind() else { unreachable!() };
+                    let TyKind::Adt(_, subst) = t.creusot_ty().kind() else { unreachable!() };
 
                     let ctor = self.names.borrow_mut().constructor(
                         self.ctx.borrow().adt_def(typ).variants()[*variant].def_id,
@@ -366,7 +366,7 @@ impl<'a, 'tcx> VCGen<'a, 'tcx> {
             }),
             // VC(A.f, Q) = VC(A, |a| Q(a.f))
             TermKind::Projection { lhs, name } => {
-                let accessor = match lhs.ty.kind() {
+                let accessor = match lhs.creusot_ty().kind() {
                     TyKind::Closure(did, substs) => {
                         self.names.borrow_mut().accessor(*did, substs, 0, *name)
                     }
@@ -464,10 +464,10 @@ impl<'a, 'tcx> VCGen<'a, 'tcx> {
         let orig_variant = self.self_sig().contract.variant.remove(0);
         let mut rec_var_exp = orig_variant.clone();
         rec_var_exp.subst(&subst);
-        if is_int(self.ctx.borrow().tcx, variant.ty) {
+        if is_int(self.ctx.borrow().tcx, variant.creusot_ty()) {
             Ok(Exp::int(0).leq(orig_variant.clone()).log_and(rec_var_exp.lt(orig_variant)))
         } else {
-            Err(VCError::UnsupportedVariant(variant.ty, variant.span))
+            Err(VCError::UnsupportedVariant(variant.creusot_ty(), variant.span))
         }
     }
 

creusot/src/backend/term.rs

@@ -2,7 +2,7 @@ use super::{program::borrow_generated_id, Why3Generator};
 use crate::{
     backend::ty::{floatty_to_ty, intty_to_ty, translate_ty, uintty_to_ty},
     ctx::*,
-    pearlite::{self, prusti::strip_all_refs, Literal, Pattern, Term, TermKind},
+    pearlite::{self, Literal, Pattern, Term, TermKind},
     util,
     util::get_builtin,
 };
@@ -100,7 +100,7 @@ impl<'tcx, N: Namer<'tcx>> Lower<'_, 'tcx, N> {
             }
             TermKind::Constructor { typ, variant, fields } => {
                 self.ctx.translate(*typ);
-                let TyKind::Adt(_, subst) = strip_all_refs(term.ty).kind() else { unreachable!() };
+                let TyKind::Adt(_, subst) = term.creusot_ty().kind() else { unreachable!() };
                 let args = fields.into_iter().map(|f| self.lower_term(f)).collect();
 
                 let ctor = self
@@ -109,7 +109,7 @@ impl<'tcx, N: Namer<'tcx>> Lower<'_, 'tcx, N> {
                 Exp::Constructor { ctor, args }
             }
             TermKind::Cur { box term } => {
-                if strip_all_refs(term.ty).is_mutable_ptr() {
+                if term.creusot_ty().is_mutable_ptr() {
                     self.names.import_prelude_module(PreludeModule::Borrow);
                     Exp::Current(Box::new(self.lower_term(term)))
                 } else {
@@ -169,7 +169,7 @@ impl<'tcx, N: Namer<'tcx>> Lower<'_, 'tcx, N> {
                 Exp::qvar(accessor).app(vec![lhs])
             }
             TermKind::Closure { body } => {
-                let TyKind::Closure(id, subst) = strip_all_refs(term.ty).kind() else {
+                let TyKind::Closure(id, subst) = term.creusot_ty().kind() else {
                     unreachable!("closure has non closure type")
                 };
                 let body = self.lower_term(&*body);

creusot/src/prusti/ctx.rs

@@ -15,7 +15,9 @@ use rustc_infer::infer::region_constraints::Constraint;
 use rustc_lint::Lint;
 use rustc_middle::{
     bug, ty,
-    ty::{walk::TypeWalker, BoundRegionKind, ParamEnv, Region, TyCtxt, TypeFoldable},
+    ty::{
+        walk::TypeWalker, BoundRegionKind, GenericArgsRef, ParamEnv, Region, TyCtxt, TypeFoldable,
+    },
 };
 use rustc_span::{
     def_id::{DefId, LocalDefId, CRATE_DEF_ID},
@@ -113,7 +115,7 @@ impl<'a, 'tcx> Debug for BaseCtx<'a, 'tcx> {
 
 pub(super) fn dummy_region(tcx: TyCtxt<'_>, sym: Symbol) -> Region<'_> {
     let def_id = CRATE_DEF_ID.to_def_id();
-    Region::new_free(tcx, def_id, BoundRegionKind::BrNamed(def_id, sym))
+    Region::new_late_param(tcx, def_id, BoundRegionKind::BrNamed(def_id, sym))
 }
 
 fn try_index_of<I: Idx, T: Eq>(s: &IndexVec<I, T>, x: &T) -> Option<I> {
@@ -170,7 +172,7 @@ impl<'a, 'tcx> BaseCtx<'a, 'tcx> {
 
     pub(crate) fn lint(&self, lint: &'static Lint, span: Span, msg: impl Into<String>) {
         let hir_id = self.tcx.local_def_id_to_hir_id(self.owner_id);
-        self.tcx.struct_span_lint_hir(lint, hir_id, span, msg.into(), |x| x)
+        self.tcx.node_span_lint(lint, hir_id, span, msg.into(), |_| {});
     }
 
     fn new(
@@ -311,9 +313,7 @@ impl<'a, 'tcx> PreCtx<'a, 'tcx> {
 
     /// Fixes an external region by converting it into a singleton set
     fn fix_region(&self, r: Region<'tcx>) -> Region<'tcx> {
-        let Some(state) = try_index_of(&self.base_states, &r) else {
-            bug!()
-        };
+        let Some(state) = try_index_of(&self.base_states, &r) else { bug!() };
         self.state_to_reg(state)
     }
 
@@ -398,13 +398,15 @@ impl<'a, 'tcx> Ctx<'a, 'tcx> {
 
     /// Fixes an external region by converting it into a singleton set
     fn fix_region(&self, r: Region<'tcx>, or: impl Fn() -> Region<'tcx>) -> Region<'tcx> {
-        let Some(base_state) = try_index_of(&self.base_states, &r) else {
-            return or()
-        };
+        let Some(base_state) = try_index_of(&self.base_states, &r) else { return or() };
         let state = self.normalize_state(base_state);
         self.state_to_reg(state)
     }
 
+    pub fn fix_subst_with_erased(&self, subst: GenericArgsRef<'tcx>) -> GenericArgsRef<'tcx> {
+        self.fix_regions(subst, || self.tcx.lifetimes.re_erased)
+    }
+
     pub(super) fn fix_regions<T: TypeFoldable<TyCtxt<'tcx>>>(
         &self,
         t: T,

creusot/src/prusti/region_set.rs

@@ -2,7 +2,7 @@ use itertools::Itertools;
 use rustc_index::Idx;
 use rustc_middle::{
     bug,
-    ty::{EarlyBoundRegion, Region, RegionKind, TyCtxt},
+    ty::{EarlyParamRegion, Region, RegionKind, TyCtxt},
 };
 use rustc_span::{def_id::CRATE_DEF_ID, symbol::kw};
 use std::fmt::{Debug, Formatter};
@@ -54,8 +54,8 @@ impl StateSet {
 
     pub fn into_region(self, tcx: TyCtxt<'_>) -> Region<'_> {
         let reg =
-            EarlyBoundRegion { index: self.0, def_id: CRATE_DEF_ID.to_def_id(), name: kw::In };
-        Region::new_early_bound(tcx, reg)
+            EarlyParamRegion { index: self.0, def_id: CRATE_DEF_ID.to_def_id(), name: kw::In };
+        Region::new_early_param(tcx, reg)
     }
 
     pub fn try_into_singleton(self) -> Option<State> {
@@ -72,8 +72,8 @@ impl StateSet {
 impl<'tcx> From<Region<'tcx>> for StateSet {
     fn from(value: Region<'tcx>) -> Self {
         match value.kind() {
-            RegionKind::ReEarlyBound(EarlyBoundRegion { index, .. }) => StateSet(index),
-            _ => bug!(),
+            RegionKind::ReEarlyParam(EarlyParamRegion { index, .. }) => StateSet(index),
+            _ => bug!("{value:?} does not represent a state set"),
         }
     }
 }