Ghost Constraint Stabilization

docs/dev-guide/src/config/flags.md

@@ -23,7 +23,6 @@
 | [`DUMP_REBORROWING_DAG_IN_DEBUG_INFO`](#dump_reborrowing_dag_in_debug_info) | `bool` | `false` | A |
 | [`DUMP_VIPER_PROGRAM`](#dump_viper_program) | `bool` | `false` | A |
 | [`ENABLE_CACHE`](#enable_cache) | `bool` | `true` | A |
-| [`ENABLE_GHOST_CONSTRAINTS`](#enable_ghost_constraints) | `bool` | `false` | A |
 | [`ENABLE_PURIFICATION_OPTIMIZATION`](#enable_purification_optimization) | `bool` | `false` | A |
 | [`ENABLE_TYPE_INVARIANTS`](#enable_type_invariants) | `bool` | `false` | A |
 | [`ENABLE_VERIFY_ONLY_BASIC_BLOCK_PATH`](#enable_verify_only_basic_block_path) | `bool` | `false` | A |
@@ -179,15 +178,6 @@ When enabled, the encoded Viper program will be output.
 
 When enabled, verification requests (to verify individual `fn`s) are cached to improve future verification. By default the cache is only saved in memory (of the `prusti-server` if enabled). For long-running verification projects use [`CACHE_PATH`](#cache_path) to save to disk.
 
-## `ENABLE_GHOST_CONSTRAINTS`
-
-When enabled, ghost constraints can be used in Prusti specifications.
-
-Ghost constraints allow for specifications which are only active if a certain "constraint" (i.e. a trait bound
-on a generic type parameter) is satisfied.
-
-**This is an experimental feature**, because it is currently possible to introduce unsound verification behavior.
-
 ## `ENABLE_PURIFICATION_OPTIMIZATION`
 
 When enabled, impure methods are optimized using the purification optimization, which tries to convert heap operations to pure (snapshot-based) operations.

docs/user-guide/src/SUMMARY.md

@@ -26,7 +26,7 @@
   - [External specifications](verify/external.md)
   - [Loop body invariants](verify/loop.md)
   - [Pledges](verify/pledge.md)
-  - [Trait contract refinement](verify/traits.md)
+  - [Type-conditional spec refinements](verify/type_cond_spec.md)
   - [Closures](verify/closure.md)
   - [Specification entailments](verify/spec_ent.md)
   - [Type models](verify/type-models.md)

docs/user-guide/src/verify/summary.md

@@ -17,7 +17,7 @@ The following features are either currently supported or planned to be supported
 - [External specifications](external.md)
 - [Loop body invariants](loop.md)
 - [Pledges](pledge.md)
-- [Trait contract refinement](traits.md)
+- [Type-conditional spec refinements](type_cond_spec.md)
 - [Closures](closure.md)
 - [Specification entailments](spec_ent.md)
 - [Type models](type-models.md)

docs/user-guide/src/verify/type_cond_spec.md

@@ -0,0 +1,37 @@
+# Type-Conditional Spec Refinement
+
+When specifying trait methods or generic functions, there is often a special case that allows for more complete specification. In these cases, you can attach a type-conditional spec refinement attribute to the function in question, spelled e.g. `#[refine_spec(where T: A + B, U: C, [requires(true), pure])]`
+
+For example, one could use this to specify a function like `core::mem::size_of` by defining a trait for types whose size we'd like to specify:
+
+```rust
+#[pure]
+#[refine_spec(where T: KnownSize, [
+    ensures(result == T::size()),
+])]
+fn size_of<T>() -> usize;
+
+pub trait KnownSize {
+    #[pure]
+    fn size() -> usize;
+}
+```
+
+> Note that the involved functions are marked as `pure`, allowing them to be used within specifications. This is another common use case, because functions can only be `pure` if their parameters and result are `Copy`, so it is often useful to specify something like `#[refine_spec(where T: Copy, [pure])]`.
+
+There are some marker traits which simply modify the behavior of methods in their super-traits. For instance, consider the `PartialEq<T>` and `Eq` traits. In order to consider this additional behavior for verification, we can refine the contract of `PartialEq::eq` when the type is known to be marked `Eq`:
+
+```rust
+pub trait PartialEq<Rhs: ?Sized = Self> {
+    #[refine_spec(where Self: Eq, [
+        ensures(self == self), // reflexive
+        // we could write more specs here
+    ])]
+    #[ensures(/* partial equivalence formulas */)]
+    fn eq(&self, other: &Rhs) -> bool;
+}
+```
+
+Thus, any client implementing `Eq` on a custom type can take advantage of the additional semantics of the total equivalence.
+
+> Refinements like these are not scoped. Therefore, considering the previous example, implementing `Eq` on a type implies that the total equivalence contract is always considered on the type, irrespective of whether `Eq` is in scope or not.

prusti-contracts/prusti-contracts-proc-macros/src/lib.rs

@@ -90,7 +90,7 @@ pub fn model(_attr: TokenStream, _tokens: TokenStream) -> TokenStream {
 
 #[cfg(not(feature = "prusti"))]
 #[proc_macro_attribute]
-pub fn ghost_constraint(_attr: TokenStream, tokens: TokenStream) -> TokenStream {
+pub fn refine_spec(_attr: TokenStream, tokens: TokenStream) -> TokenStream {
     tokens
 }
 
@@ -221,13 +221,8 @@ pub fn model(_attr: TokenStream, tokens: TokenStream) -> TokenStream {
 
 #[cfg(feature = "prusti")]
 #[proc_macro_attribute]
-pub fn ghost_constraint(attr: TokenStream, tokens: TokenStream) -> TokenStream {
-    rewrite_prusti_attributes(
-        SpecAttributeKind::GhostConstraint,
-        attr.into(),
-        tokens.into(),
-    )
-    .into()
+pub fn refine_spec(attr: TokenStream, tokens: TokenStream) -> TokenStream {
+    rewrite_prusti_attributes(SpecAttributeKind::RefineSpec, attr.into(), tokens.into()).into()
 }
 
 #[cfg(feature = "prusti")]

prusti-contracts/prusti-contracts/src/lib.rs

@@ -45,7 +45,7 @@ pub use prusti_contracts_proc_macros::model;
 
 /// A macro to add trait bounds on a generic type parameter and specifications
 /// which are active only when these bounds are satisfied for a call.
-pub use prusti_contracts_proc_macros::ghost_constraint;
+pub use prusti_contracts_proc_macros::refine_spec;
 
 /// A macro for defining ghost blocks which will be left in for verification
 /// but omitted during compilation.

prusti-contracts/prusti-specs/src/common.rs

@@ -1,20 +1,20 @@
 //! Common code for spec-rewriting
 
-use std::borrow::BorrowMut;
-use std::collections::HashMap;
 use proc_macro2::Ident;
-use syn::{GenericParam, parse_quote, TypeParam};
-use syn::punctuated::Punctuated;
-use syn::spanned::Spanned;
-use uuid::Uuid;
-pub(crate) use syn_extensions::*;
-pub(crate) use self_type_rewriter::*;
 pub(crate) use receiver_rewriter::*;
+pub(crate) use self_type_rewriter::*;
+use std::{borrow::BorrowMut, collections::HashMap};
+use syn::{parse_quote, punctuated::Punctuated, spanned::Spanned, GenericParam, TypeParam};
+pub(crate) use syn_extensions::*;
+use uuid::Uuid;
 
 /// Module which provides various extension traits for syn types.
 /// These allow for writing of generic code over these types.
 mod syn_extensions {
-    use syn::{Attribute, Generics, ImplItemMacro, ImplItemMethod, ItemFn, ItemImpl, ItemStruct, ItemTrait, Macro, Signature, TraitItemMacro, TraitItemMethod};
+    use syn::{
+        Attribute, Generics, ImplItemMacro, ImplItemMethod, ItemFn, ItemImpl, ItemStruct,
+        ItemTrait, Macro, Signature, TraitItemMacro, TraitItemMethod,
+    };
 
     /// Trait which signals that the corresponding syn item contains generics
     pub(crate) trait HasGenerics {
@@ -26,28 +26,36 @@ mod syn_extensions {
         fn generics(&self) -> &Generics {
             self
         }
-        fn generics_mut(&mut self) -> &mut Generics { self }
+        fn generics_mut(&mut self) -> &mut Generics {
+            self
+        }
     }
 
     impl HasGenerics for ItemTrait {
         fn generics(&self) -> &Generics {
             &self.generics
         }
-        fn generics_mut(&mut self) -> &mut Generics { &mut self.generics }
+        fn generics_mut(&mut self) -> &mut Generics {
+            &mut self.generics
+        }
     }
 
     impl HasGenerics for ItemStruct {
         fn generics(&self) -> &Generics {
             &self.generics
         }
-        fn generics_mut(&mut self) -> &mut Generics { &mut self.generics }
+        fn generics_mut(&mut self) -> &mut Generics {
+            &mut self.generics
+        }
     }
 
     impl HasGenerics for ItemImpl {
         fn generics(&self) -> &syn::Generics {
             &self.generics
         }
-        fn generics_mut(&mut self) -> &mut Generics { &mut self.generics }
+        fn generics_mut(&mut self) -> &mut Generics {
+            &mut self.generics
+        }
     }
 
     /// Abstraction over everything that has a [syn::Signature]
@@ -129,7 +137,7 @@ mod syn_extensions {
             &self.attrs
         }
     }
-    
+
     impl HasAttributes for ItemFn {
         fn attrs(&self) -> &Vec<Attribute> {
             &self.attrs
@@ -241,9 +249,10 @@ mod self_type_rewriter {
 mod receiver_rewriter {
     use proc_macro2::{Ident, TokenStream, TokenTree};
     use quote::{quote, quote_spanned};
-    use syn::{FnArg, ImplItemMethod, ItemFn, Macro, parse_quote_spanned, Type};
-    use syn::spanned::Spanned;
-    use syn::visit_mut::VisitMut;
+    use syn::{
+        parse_quote_spanned, spanned::Spanned, visit_mut::VisitMut, FnArg, ImplItemMethod, ItemFn,
+        Macro, Type,
+    };
 
     /// Rewrites the receiver of a method-like item.
     /// This can be used to convert impl methods to free-standing functions.
@@ -267,14 +276,14 @@ mod receiver_rewriter {
 
     impl RewritableReceiver for ImplItemMethod {
         fn rewrite_receiver(&mut self, new_ty: &Type) {
-            let mut rewriter = Rewriter {new_ty};
+            let mut rewriter = Rewriter { new_ty };
             rewriter.rewrite_impl_item_method(self);
         }
     }
 
     impl RewritableReceiver for ItemFn {
         fn rewrite_receiver(&mut self, new_ty: &Type) {
-            let mut rewriter = Rewriter {new_ty};
+            let mut rewriter = Rewriter { new_ty };
             rewriter.rewrite_item_fn(self);
         }
     }
@@ -296,13 +305,15 @@ mod receiver_rewriter {
             let tokens_span = tokens.span();
             let rewritten = TokenStream::from_iter(tokens.into_iter().map(|token| match token {
                 TokenTree::Group(group) => {
-                    let new_group =
-                        proc_macro2::Group::new(group.delimiter(), Self::rewrite_tokens(group.stream()));
+                    let new_group = proc_macro2::Group::new(
+                        group.delimiter(),
+                        Self::rewrite_tokens(group.stream()),
+                    );
                     TokenTree::Group(new_group)
                 }
                 TokenTree::Ident(ident) if ident == "self" => {
                     TokenTree::Ident(proc_macro2::Ident::new("_self", ident.span()))
-                },
+                }
                 other => other,
             }));
             parse_quote_spanned! {tokens_span=>
@@ -316,17 +327,15 @@ mod receiver_rewriter {
             if let FnArg::Receiver(receiver) = fn_arg {
                 let span = receiver.span();
                 let and = match &receiver.reference {
-                    Some((_, Some(lifetime))) =>
-                        quote_spanned!{span => &#lifetime},
-                    Some((_, None)) =>
-                        quote_spanned!{span => &},
-                    None => quote! {}
+                    Some((_, Some(lifetime))) => quote_spanned! {span => &#lifetime},
+                    Some((_, None)) => quote_spanned! {span => &},
+                    None => quote! {},
                 };
                 let mutability = &receiver.mutability;
                 let new_ty = self.new_ty;
                 let new_fn_arg: FnArg = parse_quote_spanned! {span=>
-                _self : #and #mutability #new_ty
-            };
+                    _self : #and #mutability #new_ty
+                };
                 *fn_arg = new_fn_arg;
             } else {
                 syn::visit_mut::visit_fn_arg_mut(self, fn_arg);
@@ -380,9 +389,12 @@ pub(crate) fn merge_generics<T: HasGenerics>(target: &mut T, source: &T) {
         if let GenericParam::Type(type_param_source) = param_source {
             // We can remove the target type param here, because the source will not have the
             // same type param with the same identifiers
-            let maybe_type_param_source = existing_target_type_params.remove(&type_param_source.ident);
+            let maybe_type_param_source =
+                existing_target_type_params.remove(&type_param_source.ident);
             if let Some(type_param_target) = maybe_type_param_source {
-                type_param_target.bounds.extend(type_param_source.bounds.clone());
+                type_param_target
+                    .bounds
+                    .extend(type_param_source.bounds.clone());
             } else {
                 new_generic_params.push(GenericParam::Type(type_param_source.clone()));
             }
@@ -398,8 +410,13 @@ pub(crate) fn merge_generics<T: HasGenerics>(target: &mut T, source: &T) {
     }
 
     // Merge the where clause
-    match (generics_target.where_clause.as_mut(), generics_source.where_clause.as_ref()) {
-        (Some(target_where), Some(source_where)) => target_where.predicates.extend(source_where.predicates.clone()),
+    match (
+        generics_target.where_clause.as_mut(),
+        generics_source.where_clause.as_ref(),
+    ) {
+        (Some(target_where), Some(source_where)) => target_where
+            .predicates
+            .extend(source_where.predicates.clone()),
         (None, Some(source_where)) => generics_target.where_clause = Some(source_where.clone()),
         _ => (),
     }
@@ -487,8 +504,8 @@ mod tests {
     use super::*;
 
     mod merge_generics {
-        use syn::parse_quote;
         use crate::merge_generics;
+        use syn::parse_quote;
 
         macro_rules! test_merge {
             ([$($source:tt)+] into [$($target:tt)+] gives [$($expected:tt)+]) => {