Ghost Constraint Stabilization (#1271)

* recognize and reject extern specs which define bodies for their methods

* support multiple constraints in ghost constraints

* correctly support purity ghost constraints

turns out the previous implementation was flawed in that it made the function pure whether or not the constraint held

* require at least one bound for ghost constraints

* report example structure only when it makes sense

* add compiletests for ghost constraint purity

* auto-format prusti-specs crate

* unify handling of bodies in extern specs and check more places

* add unit test for bodies in extern specs

* update unit tests

* parse new syntax for ghost constraints/conditional spec refinements

* add failing test for extraneous comma before specs

* update example in error note

* remove ghost constraint feature flag

you can still introduce unsound behavior with them, but they're far from the only way to do so, and absolutely necessary for prusti std

* rename ghost constraints to conditional spec refinements in user-facing strings & comments

* formatting

* address clippy's concerns

* add unit test for trait impls with generic arguments

removed a check preventing use of this feature previously; this effectively formalizes it as working

* improve test

* desugaring fixes

expressions are not implicitly in parentheses, creating very strange errors when desugaring e.g. a + b to &a + b

* conditional spec refinements -> type-conditional spec refinements

* rename ghost constraints to type-conditional spec refinements everywhere

* update test to reflect that generics are supported

not thoroughly tested, but let's not let perfect be the enemy of good enough

* update test to reflect that generics are supported

not thoroughly tested, but let's not let perfect be the enemy of good enough

* adjust join_spans testing-specific behavior

testing-specific workaround is now only present when cfg(test) is active

* make typecondspec parser more robust, require comma again

* update overlooked holdover of old ghost constraint term

* fix typo

* update compiletests to new typecondspec syntax

* update preparser tests to include the new parentheses

* update cargo test

* update more compiletests

* update more compiletests

* allow merge clauses for extern trait specs

implemented by simply tacking on our bound to the existing clause

* allow extern_spec to take a module argument & apply to free functions

the module argument is not valid on impls, since those already work with qualified type paths

* update tests

* allow trailing commas in where clauses on extern specs on traits

* ignore lifetimes in pure function substs

* ignore lifetimes in extern spec sanity check too

* always use lifetimes from args instead of generics

generic lifetimes are erased during trait impl resolution

* clippy

* update user guide with new typecondspec syntax

* add regression test for trait resolution with references

* update broken link

* use lifetimes from substs when possible

* erase lifetimes only when resolved method differs

* tiny fix

got lost in the refactor; i blame copilot lol

* fix some test indentation

* remove unnecessary derive

* rename missed test folders

* improve generic trait tests

* update comment

* drop unhelpful comment

* remove outdated comment

better no information than inaccurate information!

* fix spans for binary ops

while preserving the safety of parenthesizing incoming LHS/RHS

* obsolete #[generic]/#[concrete] for traits

the latter didn't work anyway, and now that we have type-cond-specs, we know we won't need it, so we can drop the annotations entirely.

* update tests for trait parameter attribute removal

* update preparser cfg tests

* rewrite self type in newly-allowed where clauses

where clauses on traits

* bump cache version

we were getting spurious failures for the core proof tests from old data

* mangle function names for extern specs

* flatten extern spec modules

it's like they were never there! no more use crate::*;

* update tests

* only mangle free functions

keep the changes to a minimum

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 |
@@ -180,15 +179,6 @@ You can find them either in `log/viper_program` or `target/verify/log/viper_prog
 
 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,35 @@
+# 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.

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
@@ -141,7 +149,7 @@ mod syn_extensions {
 mod self_type_rewriter {
     use syn::{
         parse_quote_spanned, spanned::Spanned, visit_mut::VisitMut, ImplItemMethod, ItemFn, Type,
-        TypePath,
+        TypePath, WhereClause,
     };
 
     /// Given a replacement for the `Self` type and the trait it should fulfill,
@@ -185,6 +193,16 @@ mod self_type_rewriter {
         }
     }
 
+    impl SelfTypeRewriter for WhereClause {
+        fn rewrite_self_type(&mut self, self_type: &Type, self_type_trait: Option<&TypePath>) {
+            let mut rewriter = Rewriter {
+                self_type,
+                self_type_trait,
+            };
+            rewriter.rewrite_where_clause(self);
+        }
+    }
+
     struct Rewriter<'a> {
         self_type: &'a Type,
         self_type_trait: Option<&'a TypePath>,
@@ -198,6 +216,10 @@ mod self_type_rewriter {
         pub fn rewrite_item_fn(&mut self, item: &mut syn::ItemFn) {
             syn::visit_mut::visit_item_fn_mut(self, item);
         }
+
+        pub fn rewrite_where_clause(&mut self, where_clause: &mut WhereClause) {
+            syn::visit_mut::visit_where_clause_mut(self, where_clause);
+        }
     }
 
     impl<'a> VisitMut for Rewriter<'a> {
@@ -241,9 +263,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 +290,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 +319,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 +341,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 +403,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 +424,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 +518,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)+]) => {