Non Prusti specific changes that are helpful for adding Prusi-ish syntax

creusot-contracts/src/lib.rs

@@ -13,121 +13,28 @@
 extern crate self as creusot_contracts;
 
 #[cfg(creusot)]
-mod macros {
-    /// A pre-condition of a function or trait item
-    pub use creusot_contracts_proc::requires;
-
-    /// A post-condition of a function or trait item
-    pub use creusot_contracts_proc::ensures;
-
-    pub use creusot_contracts_proc::snapshot;
-
-    /// A loop invariant
-    /// The first argument should be a name for the invariant
-    /// The second argument is the Pearlite expression for the loop invariant
-    pub use creusot_contracts_proc::invariant;
-
-    /// Declares a trait item as being a law which is autoloaded as soon another
-    /// trait item is used in a function
-    pub use creusot_contracts_proc::law;
-
-    /// Declare a function as being a logical function, this declaration must be pure and
-    /// total. It cannot be called from Rust programs, but in exchange it can use logical
-    /// operations and syntax with the help of the [`pearlite!`] macro.
-    ///
-    /// # `prophetic`
-    ///
-    /// If you wish to use the `^` operator on mutable borrows to get the final value, you need to
-    /// specify that the function is _prophetic_, like so:
-    /// ```ignore
-    /// #[logic(prophetic)]
-    /// fn uses_prophecies(x: &mut Int) -> Int {
-    ///     pearlite! { if ^x == 0 { 0 } else { 1 } }
-    /// }
-    /// ```
-    /// Such a logic function cannot be used in [`snapshot!`] anymore, and cannot be
-    /// called from a regular [`logic`] or [`predicate`] function.
-    pub use creusot_contracts_proc::logic;
-
-    /// Declare a function as being a logical function, this declaration must be pure and
-    /// total. It cannot be called from Rust programs as it is *ghost*, in exchange it can
-    /// use logical operations and syntax with the help of the [`pearlite!`] macro.
-    ///
-    /// It **must** return a boolean.
-    ///
-    /// # `prophetic`
-    ///
-    /// If you wish to use the `^` operator on mutable borrows to get the final value, you need to
-    /// specify that the function is _prophetic_, like so:
-    /// ```ignore
-    /// #[predicate(prophetic)]
-    /// fn uses_prophecies(x: &mut Int) -> bool {
-    ///     pearlite! { ^x == 0 }
-    /// }
-    /// ```
-    /// Such a predicate function cannot be used in [`snapshot!`] anymore, and cannot be
-    /// called from a regular [`logic`] or [`predicate`] function.
-    pub use creusot_contracts_proc::predicate;
-
-    /// Inserts a *logical* assertion into the code. This assertion will not be checked at runtime
-    /// but only during proofs. However, it has access to the ghost context and can use logical operations
-    /// and syntax.
-    pub use creusot_contracts_proc::proof_assert;
-
-    /// Instructs Pearlite to ignore the body of a declaration, assuming any contract the declaration has is
-    /// valid.
-    pub use creusot_contracts_proc::trusted;
-
-    /// Declares a variant for a function, this is primarily used in combination with logical functions
-    /// The variant must be an expression which returns a type implementing [WellFounded]
-    pub use creusot_contracts_proc::variant;
-
-    /// Enables Pearlite syntax, granting access to Pearlite specific operators and syntax
-    pub use creusot_contracts_proc::pearlite;
-
-    /// Allows specifications to be attached to functions coming from external crates
-    /// TODO: Document syntax
-    pub use creusot_contracts_proc::extern_spec;
-
-    /// Allows specifying both a pre- and post-condition in a single statement.
-    /// Expects an expression in either the form of a method or function call
-    /// Arguments to the call can be prefixed with `mut` to indicate that they are mutable borrows.
-    ///
-    /// Generates a `requires` and `ensures` clause in the shape of the input expression, with
-    /// `mut` replaced by `*` in the `requires` and `^` in the ensures.
-    pub use creusot_contracts_proc::maintains;
-
-    /// 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).
-    ///
-    /// 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 creusot_contracts_proc::open;
-
-    pub use creusot_contracts_proc::DeepModel;
-
-    pub use creusot_contracts_proc::Resolve;
-}
+extern crate creusot_contracts_proc as base_macros;
 
 #[cfg(not(creusot))]
+extern crate creusot_contracts_dummy as base_macros;
+
 mod macros {
     /// A pre-condition of a function or trait item
-    pub use creusot_contracts_dummy::requires;
+    pub use base_macros::requires;
 
     /// A post-condition of a function or trait item
-    pub use creusot_contracts_dummy::ensures;
+    pub use base_macros::ensures;
 
-    pub use creusot_contracts_dummy::snapshot;
+    pub use base_macros::snapshot;
 
     /// A loop invariant
     /// The first argument should be a name for the invariant
     /// The second argument is the Pearlite expression for the loop invariant
-    pub use creusot_contracts_dummy::invariant;
+    pub use base_macros::invariant;
 
     /// Declares a trait item as being a law which is autoloaded as soon another
     /// trait item is used in a function
-    pub use creusot_contracts_dummy::law;
+    pub use base_macros::law;
 
     /// Declare a function as being a logical function, this declaration must be pure and
     /// total. It cannot be called from Rust programs, but in exchange it can use logical
@@ -145,7 +52,7 @@ mod macros {
     /// ```
     /// Such a logic function cannot be used in [`snapshot!`] anymore, and cannot be
     /// called from a regular [`logic`] or [`predicate`] function.
-    pub use creusot_contracts_dummy::logic;
+    pub use base_macros::logic;
 
     /// Declare a function as being a logical function, this declaration must be pure and
     /// total. It cannot be called from Rust programs as it is *ghost*, in exchange it can
@@ -165,47 +72,43 @@ mod macros {
     /// ```
     /// Such a predicate function cannot be used in [`snapshot!`] anymore, and cannot be
     /// called from a regular [`logic`] or [`predicate`] function.
-    pub use creusot_contracts_dummy::predicate;
+    pub use base_macros::predicate;
 
     /// Inserts a *logical* assertion into the code. This assertion will not be checked at runtime
     /// but only during proofs. However, it has access to the ghost context and can use logical operations
     /// and syntax.
-    pub use creusot_contracts_dummy::proof_assert;
+    pub use base_macros::proof_assert;
 
     /// Instructs Pearlite to ignore the body of a declaration, assuming any contract the declaration has is
     /// valid.
-    pub use creusot_contracts_dummy::trusted;
+    pub use base_macros::trusted;
 
     /// Declares a variant for a function, this is primarily used in combination with logical functions
     /// The variant must be an expression which returns a type implementing [WellFounded]
-    pub use creusot_contracts_dummy::variant;
+    pub use base_macros::variant;
 
     /// Enables Pearlite syntax, granting access to Pearlite specific operators and syntax
-    pub use creusot_contracts_dummy::pearlite;
+    pub use base_macros::pearlite;
 
     /// Allows specifications to be attached to functions coming from external crates
     /// TODO: Document syntax
-    pub use creusot_contracts_dummy::extern_spec;
+    pub use base_macros::extern_spec;
 
     /// Allows specifying both a pre- and post-condition in a single statement.
     /// Expects an expression in either the form of a method or function call
     /// Arguments to the call can be prefixed with `mut` to indicate that they are mutable borrows.
     ///
     /// Generates a `requires` and `ensures` clause in the shape of the input expression, with
     /// `mut` replaced by `*` in the `requires` and `^` in the ensures.
-    pub use creusot_contracts_dummy::maintains;
+    pub use base_macros::maintains;
 
     /// 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 creusot_contracts_dummy::open;
-
-    pub use creusot_contracts_dummy::DeepModel;
-
-    pub use creusot_contracts_dummy::Resolve;
+    pub use base_macros::open;
 }
 
 #[cfg(creusot)]
@@ -252,34 +155,40 @@ pub mod util;
 pub mod well_founded;
 
 // We add some common things at the root of the creusot-contracts library
-pub use crate::{
-    logic::{IndexLogic as _, Int, OrdLogic, Seq},
-    macros::*,
-    model::{DeepModel, ShallowModel},
-    resolve::Resolve,
-    snapshot::Snapshot,
-    std::{
-        // Shadow std::prelude by our version.
-        // For Clone and PartialEq, this is important for the derive macro.
-        // If the user write the glob pattern "use creusot_contracts::*", then
-        // rustc will either shadow the old identifier or complain about the
-        // ambiguïty (ex: for the derive macros Clone and PartialEq, a glob
-        // pattern is not enough to force rustc to use our version, but at least
-        // we get an error message).
-        clone::Clone,
-        cmp::PartialEq,
-        default::Default,
-        iter::{FromIterator, IntoIterator, Iterator},
-    },
-    well_founded::WellFounded,
-};
+mod base_prelude {
+    pub use crate::{
+        logic::{IndexLogic as _, Int, OrdLogic, Seq},
+        model::{DeepModel, ShallowModel},
+        resolve::Resolve,
+        snapshot::Snapshot,
+        std::{
+            // Shadow std::prelude by our version.
+            // For Clone and PartialEq, this is important for the derive macro.
+            // If the user write the glob pattern "use creusot_contracts::*", then
+            // rustc will either shadow the old identifier or complain about the
+            // ambiguïty (ex: for the derive macros Clone and PartialEq, a glob
+            // pattern is not enough to force rustc to use our version, but at least
+            // we get an error message).
+            clone::Clone,
+            cmp::PartialEq,
+            default::Default,
+            iter::{FromIterator, IntoIterator, Iterator},
+        },
+        well_founded::WellFounded,
+    };
+
+    // Export extension traits anonymously
+    pub use crate::std::{
+        iter::{SkipExt as _, TakeExt as _},
+        ops::{FnExt as _, FnMutExt as _, FnOnceExt as _, RangeInclusiveExt as _},
+        slice::SliceExt as _,
+    };
+}
+pub mod prelude {
+    pub use crate::{base_prelude::*, macros::*};
+}
 
-// Export extension traits anonymously
-pub use crate::std::{
-    iter::{SkipExt as _, TakeExt as _},
-    ops::{FnExt as _, FnMutExt as _, FnOnceExt as _, RangeInclusiveExt as _},
-    slice::SliceExt as _,
-};
+pub use prelude::*;
 
 // The std vec macro uses special magic to construct the array argument
 // to Box::new directly on the heap. Because the generated MIR is hard

creusot-contracts/src/model.rs

@@ -12,11 +12,7 @@ pub trait ShallowModel {
     fn shallow_model(self) -> Self::ShallowModelTy;
 }
 
-#[cfg(creusot)]
-pub use creusot_contracts_proc::DeepModel;
-
-#[cfg(not(creusot))]
-pub use creusot_contracts_dummy::DeepModel;
+pub use crate::base_macros::DeepModel;
 
 /// The deep model corresponds to the model used for specifying
 /// operations such as equality, hash function or ordering, which are

creusot-contracts/src/resolve.rs

@@ -1,3 +1,4 @@
+pub use crate::base_macros::Resolve;
 use crate::*;
 
 #[cfg_attr(creusot, rustc_diagnostic_item = "creusot_resolve")]

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

@@ -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) = 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 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) = 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);