Termination check: handle recursion through proof trees and add recursive types check

creusot-std-proc/Cargo.toml

@@ -28,7 +28,7 @@ creusot = ["dep:uuid", "dep:pearlite-syn", "proc-macro2/span-locations"]
 quote = "1.0"
 uuid = { version = "1.12", features = ["v4"], optional = true }
 pearlite-syn = { version = "0.12.0-dev", path = "../pearlite-syn", features = ["full"], optional = true }
-syn = { version = "2.0", features = ["full", "visit", "visit-mut"] }
+syn = { version = "2.0", features = ["parsing", "full", "visit", "visit-mut"] }
 proc-macro2 = { version = "1.0" }
 
 [lints.rust]

creusot-std-proc/src/creusot.rs

@@ -20,11 +20,12 @@ pub(crate) use self::{
 use crate::common::{ContractSubject, FnOrMethod};
 use proc_macro::TokenStream as TS1;
 use proc_macro2::{Span, TokenStream};
-use quote::quote;
+use quote::{TokenStreamExt as _, quote};
 use syn::{
     Error, FnArg, Ident, LitStr, Macro, Result, Token, parse,
     parse::{Parse, ParseStream},
     parse_macro_input, parse_quote,
+    punctuated::Punctuated,
     spanned::Spanned as _,
 };
 
@@ -36,21 +37,74 @@ pub fn open_inv_result(_: TS1, tokens: TS1) -> TS1 {
     })
 }
 
-pub fn trusted(_: TS1, tokens: TS1) -> TS1 {
+pub fn trusted(arg: TS1, tokens: TS1) -> TS1 {
     match from_proof_assert(tokens.clone()) {
         Ok(Some(assertion)) => proof_assert_(assertion, true),
         Ok(None) => {
-            let tokens = TokenStream::from(tokens);
-            TS1::from(quote! {
-                #[creusot::decl::trusted]
-                #[allow(creusot::experimental)]
-                #tokens
-            })
+            if arg.is_empty() {
+                let tokens = TokenStream::from(tokens);
+                TS1::from(quote! {
+                    #[creusot::decl::trusted]
+                    #[allow(creusot::experimental)]
+                    #tokens
+                })
+            } else {
+                let args = parse_macro_input!(
+                    arg with Punctuated::<TrustedArg, Token![,]>::parse_separated_nonempty
+                );
+                let mut tokens = tokens.into();
+                for arg in args {
+                    tokens = quote! { #arg #tokens };
+                }
+                TS1::from(tokens)
+            }
         }
         Err(e) => e.into_compile_error().into(),
     }
 }
 
+enum TrustedArg {
+    /// #[trusted(ghost)]
+    Ghost,
+    /// #[trusted(terminates)]
+    Terminates,
+    /// #[trusted(positive(T, U))]
+    Positive(Punctuated<Ident, Token![,]>),
+}
+
+impl Parse for TrustedArg {
+    fn parse(src: ParseStream) -> syn::Result<Self> {
+        use TrustedArg::*;
+        let ident = src.parse::<Ident>()?;
+        if ident == "ghost" {
+            Ok(Ghost)
+        } else if ident == "terminates" {
+            Ok(Terminates)
+        } else if ident == "positive" {
+            let content;
+            syn::parenthesized!(content in src);
+            let params = Punctuated::<Ident, Token![,]>::parse_separated_nonempty(&content)?;
+            Ok(Positive(params))
+        } else {
+            Err(Error::new(
+                ident.span(),
+                "Unexpected `#[trusted]` argument: expected `terminates`, `positive(PARAM)`, or nothing",
+            ))
+        }
+    }
+}
+
+impl quote::ToTokens for TrustedArg {
+    fn to_tokens(&self, stream: &mut TokenStream) {
+        use TrustedArg::*;
+        stream.append_all(match self {
+            Ghost => quote! { #[creusot::decl::trusted_ghost] },
+            Terminates => quote! { #[creusot::decl::trusted_terminates] },
+            Positive(params) => quote! { #[creusot::decl::trusted_positive(#params)] },
+        })
+    }
+}
+
 /// Try to extract the body of a `proof_assert!`.
 /// Error if it is a macro different from `proof_assert!`.
 fn from_proof_assert(tokens: TS1) -> Result<Option<TS1>> {
@@ -60,7 +114,7 @@ fn from_proof_assert(tokens: TS1) -> Result<Option<TS1>> {
     } else {
         Err(Error::new(
             m.path.span(),
-            "Unexpected #[trusted] item: expected `proof_assert!` or a declaration or a closure",
+            "Unexpected `#[trusted]` item: expected `proof_assert!` or a declaration or a closure",
         ))
     }
 }

creusot-std-proc/src/creusot/extern_spec.rs

@@ -17,24 +17,35 @@ use syn::{
 /// The `extern_spec!` macro.
 pub fn extern_spec(tokens: TS1) -> TS1 {
     let externs: ExternSpecs = parse_macro_input!(tokens);
+    match extern_spec_(externs) {
+        Ok(specs) => TS1::from(quote! { #(#specs)* }),
+        Err(err) => err.to_compile_error().into(),
+    }
+}
 
+fn extern_spec_(externs: ExternSpecs) -> Result<Vec<TokenStream>> {
     let mut specs = Vec::new();
-    let externs = match externs.flatten() {
-        Ok(externs) => externs,
-        Err(err) => return TS1::from(err.to_compile_error()),
-    };
-
-    for spec in externs {
-        specs.push(spec.into_tokens());
+    for item in externs.0 {
+        match item {
+            ExternSpecItem::Fun(f) => {
+                for spec in f.flatten()? {
+                    specs.push(spec.into_tokens())
+                }
+            }
+            ExternSpecItem::Type(ty) => specs.push(ty.to_token_stream()),
+        }
     }
-
-    TS1::from(quote! {
-        #(#specs)*
-    })
+    Ok(specs)
 }
 
 #[derive(Debug)]
-struct ExternSpecs(Vec<ExternSpec>);
+struct ExternSpecs(Vec<ExternSpecItem>);
+
+#[derive(Debug)]
+enum ExternSpecItem {
+    Fun(ExternSpec),
+    Type(ExternType),
+}
 
 /// An extern spec is either:
 /// - A module of extern specs
@@ -116,23 +127,20 @@ struct FlatSpec {
     body: Option<Block>,
 }
 
-impl ExternSpecs {
+impl ExternSpec {
     fn flatten(self) -> Result<Vec<FlatSpec>> {
         let mut specs = Vec::new();
-
-        for spec in self.0 {
-            flatten(
-                spec,
-                ExprPath {
-                    attrs: Vec::new(),
-                    qself: None,
-                    path: Path { leading_colon: None, segments: Punctuated::new() },
-                },
-                DocItemName(String::from("extern_spec")),
-                None,
-                &mut specs,
-            )?
-        }
+        flatten(
+            self,
+            ExprPath {
+                attrs: Vec::new(),
+                qself: None,
+                path: Path { leading_colon: None, segments: Punctuated::new() },
+            },
+            DocItemName(String::from("extern_spec")),
+            None,
+            &mut specs,
+        )?;
         Ok(specs)
     }
 }
@@ -778,6 +786,25 @@ impl Parse for ExternSpecs {
     }
 }
 
+impl Parse for ExternSpecItem {
+    fn parse(input: parse::ParseStream) -> Result<Self> {
+        let attrs = input.call(Attribute::parse_outer)?;
+
+        let lookahead = input.lookahead1();
+        if lookahead.peek(Token![type]) {
+            let mut ty = input.call(ExternType::parse)?;
+            ty.attrs = attrs;
+            Ok(ExternSpecItem::Type(ty))
+        } else {
+            let mut e = input.call(ExternSpec::parse)?;
+            if let ExternSpec::Fn(ref mut f) = e {
+                f.attrs = attrs
+            }
+            Ok(ExternSpecItem::Fun(e))
+        }
+    }
+}
+
 impl Parse for ExternSpec {
     fn parse(input: parse::ParseStream) -> Result<Self> {
         let attrs = input.call(Attribute::parse_outer)?;
@@ -793,7 +820,7 @@ impl Parse for ExternSpec {
             || (lookahead.peek(Token![unsafe]) && input.peek2(Token![fn]))
         {
             let mut f: ExternMethod = input.parse()?;
-            f.attrs.extend(attrs);
+            f.attrs = attrs;
             Ok(ExternSpec::Fn(f))
         } else {
             Err(lookahead.error())
@@ -963,3 +990,39 @@ impl Parse for ExternMethod {
         Ok(ExternMethod { span, attrs, sig, body })
     }
 }
+
+#[derive(Debug)]
+struct ExternType {
+    attrs: Vec<Attribute>,
+    path: Path,
+}
+
+impl Parse for ExternType {
+    fn parse(input: parse::ParseStream) -> Result<Self> {
+        let attrs = input.call(Attribute::parse_outer)?;
+        input.parse::<Token![type]>()?;
+        let path = input.parse()?;
+        input.parse::<Token![;]>()?;
+        Ok(Self { attrs, path })
+    }
+}
+
+impl ToTokens for ExternType {
+    fn to_tokens(&self, tokens: &mut TokenStream) {
+        let span = self.path.span();
+        let ident = crate::creusot::generate_unique_ident("extern_type", span);
+        let attrs = &self.attrs;
+        let path = &self.path;
+        let generics = match self.path.segments.last().unwrap().arguments {
+            syn::PathArguments::AngleBracketed(ref generics) => Some(generics),
+            _ => None,
+        };
+        tokens.extend(quote_spanned! { span=>
+            #[allow(dead_code, non_camel_case_types)]
+            #[creusot::extern_type]
+            #[doc(hidden)]
+            #(#attrs)*
+            struct #ident #generics (#path);
+        })
+    }
+}

creusot-std-proc/src/creusot/specs.rs

@@ -159,28 +159,22 @@ pub fn maintains(attr: TS1, body: TS1) -> TS1 {
 
 pub fn check(args: TS1, tokens: TS1) -> TS1 {
     let mode = parse_macro_input!(args as Ident);
-    let (terminates, ghost, ghost_trusted) = if mode == "terminates" {
-        (true, false, false)
+    let ghost = if mode == "terminates" {
+        false
     } else if mode == "ghost" {
-        (true, true, false)
-    } else if mode == "ghost_trusted" {
-        (true, true, true)
+        true
     } else {
         let msg = format!("unknown mode `{mode}`. Accepted modes are `terminates` or `ghost`");
         return quote! { compile_error!(#msg) }.into();
     };
     let mut documentation = TokenStream::new();
     let mut clauses = TokenStream::new();
-    if terminates {
-        documentation.extend(document_spec("terminates", doc::LogicBody::None));
-        clauses.extend(quote!(#[creusot::clause::check_terminates]));
-    }
     if ghost {
         documentation.extend(document_spec("ghost", doc::LogicBody::None));
         clauses.extend(quote!(#[creusot::clause::check_ghost]));
-    }
-    if ghost_trusted {
-        clauses.extend(quote!(#[creusot::clause::check_ghost::trusted]))
+    } else {
+        documentation.extend(document_spec("terminates", doc::LogicBody::None));
+        clauses.extend(quote!(#[creusot::clause::check_terminates]));
     }
     let item = tokens.clone();
     let item = parse_macro_input!(item as ContractSubject);

creusot-std/src/cell/permcell.rs

@@ -22,8 +22,9 @@ use alloc::boxed::Box;
 /// Creusot ensures that every operation on the inner value uses the right [`Perm`] object
 /// created by [`PermCell::new`], ensuring safety in a manner similar to
 /// [ghost_cell](https://docs.rs/ghost-cell/latest/ghost_cell/).
-#[repr(transparent)]
+#[trusted(positive(T))]
 #[opaque]
+#[repr(transparent)]
 pub struct PermCell<T: ?Sized>(UnsafeCell<T>);
 
 impl<T: Sized> Container for PermCell<T> {

creusot-std/src/cell/predcell.rs

@@ -7,6 +7,7 @@ use crate::{logic::Mapping, prelude::*};
 /// Cell over predicates
 ///
 /// A wrapper around `std::cell::Cell` that allows predicates to be used to specify the contents of the cell.
+#[trusted(positive(T))]
 #[opaque]
 #[repr(transparent)]
 pub struct PredCell<T: ?Sized>(core::cell::Cell<T>);

creusot-std/src/ghost/fn_ghost.rs

@@ -40,29 +40,29 @@ impl<I: core::marker::Tuple, F: FnOnce<I>> FnOnce<I> for FnGhostWrapper<F> {
     type Output = F::Output;
 
     #[trusted]
+    #[trusted(ghost)]
     #[requires(self.precondition(args))]
     #[ensures(self.postcondition_once(args, result))]
-    #[check(ghost_trusted)]
     extern "rust-call" fn call_once(self, args: I) -> Self::Output {
         self.0.call_once(args)
     }
 }
 #[cfg(creusot)]
 impl<I: core::marker::Tuple, F: FnMut<I>> FnMut<I> for FnGhostWrapper<F> {
     #[trusted]
+    #[trusted(ghost)]
     #[requires((*self).precondition(args))]
     #[ensures((*self).postcondition_mut(args, ^self, result))]
-    #[check(ghost_trusted)]
     extern "rust-call" fn call_mut(&mut self, args: I) -> Self::Output {
         self.0.call_mut(args)
     }
 }
 #[cfg(creusot)]
 impl<I: core::marker::Tuple, F: Fn<I>> Fn<I> for FnGhostWrapper<F> {
     #[trusted]
+    #[trusted(ghost)]
     #[requires((*self).precondition(args))]
     #[ensures((*self).postcondition(args, result))]
-    #[check(ghost_trusted)]
     extern "rust-call" fn call(&self, args: I) -> Self::Output {
         self.0.call(args)
     }

creusot-std/src/logic/mapping.rs

@@ -17,6 +17,7 @@ use core::marker::PhantomData;
 /// proof_assert!(map.get(1) == 4);
 /// ```
 #[builtin("map.Map.map")]
+#[trusted(positive(B))]
 pub struct Mapping<A: ?Sized, B>(PhantomData<fn(&A) -> B>);
 
 impl<A: ?Sized, B> Mapping<A, B> {

creusot-std/src/std/rc.rs

@@ -47,6 +47,9 @@ impl<T: ?Sized, A: Allocator> View for Rc<T, A> {
 }
 
 extern_spec! {
+    #[trusted(positive(T))]
+    type Rc<T>;
+
     impl<T> Rc<T> {
         #[check(ghost)]
         #[ensures(*result@ == value)]