Add Prusti-ish frontend to Creusot

creusot-contracts-dummy/src/lib.rs

@@ -82,3 +82,43 @@ pub fn derive_deep_model(_: TS1) -> TS1 {
 pub fn derive_resolve(_: TS1) -> TS1 {
     TS1::new()
 }
+
+#[proc_macro_attribute]
+pub fn prusti_requires(_: TS1, tokens: TS1) -> TS1 {
+    tokens
+}
+
+#[proc_macro_attribute]
+pub fn prusti_ensures(_: TS1, tokens: TS1) -> TS1 {
+    tokens
+}
+
+#[proc_macro_attribute]
+pub fn prusti_ensures_expiry(_: TS1, tokens: TS1) -> TS1 {
+    tokens
+}
+
+#[proc_macro_attribute]
+pub fn prusti_logic(_: TS1, _: TS1) -> TS1 {
+    TS1::new()
+}
+
+#[proc_macro_attribute]
+pub fn prusti_logic_prophetic(_: TS1, _: TS1) -> TS1 {
+    TS1::new()
+}
+
+#[proc_macro_attribute]
+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

@@ -7,7 +7,7 @@ use proc_macro2::{Span, TokenStream};
 use quote::{quote, quote_spanned, ToTokens, TokenStreamExt};
 use std::iter;
 use syn::{
-    parse::{discouraged::Speculative, Parse, Result},
+    parse::{discouraged::Speculative, Parse, ParseStream, Parser, Result},
     spanned::Spanned,
     *,
 };
@@ -19,6 +19,8 @@ mod pretyping;
 
 mod derive;
 
+const NONE: Option<Ident> = None; // Replace with Option<!> when it becomes available
+
 trait FilterAttrs<'a> {
     type Ret: Iterator<Item = &'a Attribute>;
 
@@ -175,21 +177,19 @@ fn req_body(p: &Term) -> TokenStream {
     })
 }
 
-fn spec_attrs(tag: &Ident) -> TokenStream {
-    let name_tag = format!("{}", quote! { #tag });
+fn spec_attrs(name_tag: &str, prusti_info: impl ToTokens) -> TokenStream {
     quote! {
-         #[creusot::no_translate]
-         #[creusot::item=#name_tag]
-         #[creusot::spec]
+        #[creusot::no_translate]
+        #[creusot::item=#name_tag]
+        #[creusot::spec]
+        #prusti_info
     }
 }
 
 // Generate a token stream for the item representing a specific
 // `requires` or `ensures`
-fn fn_spec_item(tag: Ident, result: Option<FnArg>, p: Term) -> TokenStream {
+fn fn_spec_item(attrs: TokenStream, result: Option<FnArg>, p: Term) -> TokenStream {
     let req_body = req_body(&p);
-    let attrs = spec_attrs(&tag);
-
     quote! {
         #[allow(unused_must_use)]
         let _ =
@@ -199,9 +199,8 @@ fn fn_spec_item(tag: Ident, result: Option<FnArg>, p: Term) -> TokenStream {
     }
 }
 
-fn sig_spec_item(tag: Ident, mut sig: Signature, p: Term) -> TokenStream {
+fn sig_spec_item(attrs: TokenStream, tag: Ident, mut sig: Signature, p: Term) -> TokenStream {
     let req_body = req_body(&p);
-    let attrs = spec_attrs(&tag);
     sig.ident = tag;
     sig.output = parse_quote! { -> bool };
 
@@ -213,6 +212,10 @@ fn sig_spec_item(tag: Ident, mut sig: Signature, p: Term) -> TokenStream {
 
 #[proc_macro_attribute]
 pub fn requires(attr: TS1, tokens: TS1) -> TS1 {
+    requires_helper(attr, tokens, NONE)
+}
+
+fn requires_helper(attr: TS1, tokens: TS1, prusti_info: impl ToTokens) -> TS1 {
     let mut item = parse_macro_input!(tokens as ContractSubject);
     let term = parse_macro_input!(attr as Term);
     item.mark_unused();
@@ -221,17 +224,19 @@ pub fn requires(attr: TS1, tokens: TS1) -> TS1 {
 
     let name_tag = format!("{}", quote! { #req_name });
 
+    let attrs = spec_attrs(&name_tag, prusti_info);
+
     match item {
         ContractSubject::FnOrMethod(fn_or_meth) if fn_or_meth.is_trait_signature() => {
-            let requires_tokens = sig_spec_item(req_name, fn_or_meth.sig.clone(), term);
+            let requires_tokens = sig_spec_item(attrs, req_name, fn_or_meth.sig.clone(), term);
             TS1::from(quote! {
               #requires_tokens
               #[creusot::clause::requires=#name_tag]
               #fn_or_meth
             })
         }
         ContractSubject::FnOrMethod(mut f) => {
-            let requires_tokens = fn_spec_item(req_name, None, term);
+            let requires_tokens = fn_spec_item(attrs, None, term);
 
             f.body.as_mut().map(|b| b.stmts.insert(0, Stmt::Item(Item::Verbatim(requires_tokens))));
             TS1::from(quote! {
@@ -240,7 +245,7 @@ pub fn requires(attr: TS1, tokens: TS1) -> TS1 {
             })
         }
         ContractSubject::Closure(mut clos) => {
-            let requires_tokens = fn_spec_item(req_name, None, term);
+            let requires_tokens = fn_spec_item(attrs, None, term);
             let body = &clos.body;
             *clos.body = parse_quote!({let res = #body; #requires_tokens res});
             TS1::from(quote! {
@@ -253,13 +258,19 @@ pub fn requires(attr: TS1, tokens: TS1) -> TS1 {
 
 #[proc_macro_attribute]
 pub fn ensures(attr: TS1, tokens: TS1) -> TS1 {
+    ensures_helper(attr, tokens, NONE)
+}
+
+fn ensures_helper(attr: TS1, tokens: TS1, prusti_info: impl ToTokens) -> TS1 {
     let mut item = parse_macro_input!(tokens as ContractSubject);
     let term = parse_macro_input!(attr as Term);
     item.mark_unused();
 
     let ens_name = generate_unique_ident(&item.name());
     let name_tag = format!("{}", quote! { #ens_name });
 
+    let attrs = spec_attrs(&name_tag, prusti_info);
+
     match item {
         ContractSubject::FnOrMethod(s) if s.is_trait_signature() => {
             let result = match s.sig.output {
@@ -269,7 +280,7 @@ pub fn ensures(attr: TS1, tokens: TS1) -> TS1 {
 
             let mut sig = s.sig.clone();
             sig.inputs.push(result);
-            let ensures_tokens = sig_spec_item(ens_name, sig, term);
+            let ensures_tokens = sig_spec_item(attrs, ens_name, sig, term);
             TS1::from(quote! {
               #ensures_tokens
               #[creusot::clause::ensures=#name_tag]
@@ -281,7 +292,7 @@ pub fn ensures(attr: TS1, tokens: TS1) -> TS1 {
                 ReturnType::Default => parse_quote! { result : () },
                 ReturnType::Type(_, ref ty) => parse_quote! { result : #ty },
             };
-            let ensures_tokens = fn_spec_item(ens_name, Some(result), term);
+            let ensures_tokens = fn_spec_item(attrs, Some(result), term);
 
             f.body.as_mut().map(|b| b.stmts.insert(0, Stmt::Item(Item::Verbatim(ensures_tokens))));
             TS1::from(quote! {
@@ -291,7 +302,6 @@ pub fn ensures(attr: TS1, tokens: TS1) -> TS1 {
         }
         ContractSubject::Closure(mut clos) => {
             let req_body = req_body(&term);
-            let attrs = spec_attrs(&ens_name);
             let body = &clos.body;
             *clos.body = parse_quote!({
                 let res = #body;
@@ -724,3 +734,94 @@ pub fn derive_deep_model(tokens: TS1) -> TS1 {
 pub fn derive_resolve(tokens: TS1) -> TS1 {
     derive::derive_resolve(tokens)
 }
+
+// Prusti Macros
+#[proc_macro_attribute]
+pub fn prusti_requires(attr: TS1, tokens: TS1) -> TS1 {
+    let prusti_info = quote!(#[creusot::prusti::ts="old"]);
+    requires_helper(attr, tokens, prusti_info)
+}
+
+#[proc_macro_attribute]
+pub fn prusti_ensures(attr: TS1, tokens: TS1) -> TS1 {
+    let prusti_info = quote!(#[creusot::prusti::ts="curr"]);
+    ensures_helper(attr, tokens, prusti_info)
+}
+
+#[proc_macro_attribute]
+pub fn prusti_ensures_expiry(attr: TS1, tokens: TS1) -> TS1 {
+    let parser = |input: ParseStream| {
+        let lookahead = input.lookahead1();
+        if lookahead.peek(Lifetime) {
+            let lt: Lifetime = input.parse()?;
+            let _: Token![,] = input.parse()?;
+            let rest: TokenStream = input.parse()?;
+            Ok((Some(lt), rest))
+        } else {
+            Ok((None, input.parse()?))
+        }
+    };
+    let split = parser.parse(attr);
+    let (lifetime, rest) = match split {
+        Ok(split) => split,
+        Err(err) => return err.into_compile_error().into(),
+    };
+    let prusti_info = match lifetime {
+        Some(lifetime) => {
+            let lifetime_string = format!("{}", lifetime);
+            let lifetime = LitStr::new(&lifetime_string, lifetime.span());
+            quote!(#[creusot::prusti::ts=#lifetime])
+        }
+        None => quote!(#[creusot::prusti::ts="'_"]),
+    };
+    ensures_helper(rest.into(), tokens, prusti_info)
+}
+
+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::#creusot_macro]
+        #tokens
+    })
+}
+
+#[proc_macro_attribute]
+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 {
+    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]
+pub fn prusti_law(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::law]
+        #tokens
+    })
+}

creusot-contracts/src/lib.rs

@@ -150,6 +150,7 @@ pub mod snapshot {
 pub mod ghost_ptr;
 pub mod invariant;
 pub mod model;
+mod prusti;
 pub mod resolve;
 pub mod util;
 pub mod well_founded;
@@ -184,10 +185,25 @@ mod base_prelude {
         slice::SliceExt as _,
     };
 }
+
+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_logic_prophetic as logic_prophetic, prusti_predicate as predicate,
+        prusti_predicate_prophetic as predicate_prophetic, prusti_requires as requires, trusted,
+        variant,
+    };
+}
+
 pub mod prelude {
     pub use crate::{base_prelude::*, macros::*};
 }
 
+pub mod prusti_prelude {
+    pub use crate::{base_prelude::*, prusti::*, prusti_macros::*};
+}
+
 pub use prelude::*;
 
 // The std vec macro uses special magic to construct the array argument