Logical functions aliases

creusot-contracts-proc/src/creusot.rs

@@ -14,7 +14,7 @@ pub(crate) use self::{
     extern_spec::extern_spec,
     logic::{logic, pearlite},
     proof::{ghost, ghost_let, invariant, proof_assert, snapshot},
-    specs::{bitwise_proof, check, ensures, maintains, requires, variant},
+    specs::{bitwise_proof, check, ensures, has_logical_alias, maintains, requires, variant},
 };
 
 use crate::common::{ContractSubject, FnOrMethod};

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

@@ -10,7 +10,7 @@ use crate::{
 use pearlite_syn::{Term, TermPath};
 use proc_macro::TokenStream as TS1;
 use proc_macro2::{Span, TokenStream};
-use quote::quote;
+use quote::{quote, quote_spanned};
 use syn::{
     Attribute, Ident, Item, Path, ReturnType, Signature, Stmt, Token, Type, parenthesized,
     parse::{self, Parse},
@@ -72,6 +72,10 @@ pub fn requires(attr: TS1, tokens: TS1) -> TS1 {
 }
 
 pub fn ensures(attr: TS1, tokens: TS1) -> TS1 {
+    ensures_inner(attr, tokens, false)
+}
+
+fn ensures_inner(attr: TS1, tokens: TS1, logical_alias_path: bool) -> TS1 {
     let documentation = document_spec("ensures", doc::LogicBody::Some(attr.clone()));
 
     let mut item = parse_macro_input!(tokens as ContractSubject);
@@ -80,6 +84,12 @@ pub fn ensures(attr: TS1, tokens: TS1) -> TS1 {
 
     let ens_name = crate::creusot::generate_unique_ident(&item.name(), Span::call_site());
     let name_tag = ens_name.to_string();
+    let logical_alias = if logical_alias_path {
+        quote_spanned! {term.span()=> #[creusot::decl::logical_alias_path = #name_tag]}
+    } else {
+        quote!()
+    };
+
     match item {
         ContractSubject::FnOrMethod(mut s) if s.is_trait_signature() => {
             let attrs = std::mem::take(&mut s.attrs);
@@ -96,6 +106,7 @@ pub fn ensures(attr: TS1, tokens: TS1) -> TS1 {
             TS1::from(quote! {
               #ensures_tokens
               #[creusot::clause::ensures=#name_tag]
+              #logical_alias
               #(#attrs)*
               #documentation
               #s
@@ -113,6 +124,7 @@ pub fn ensures(attr: TS1, tokens: TS1) -> TS1 {
             }
             TS1::from(quote! {
                 #[creusot::clause::ensures=#name_tag]
+                #logical_alias
                 #(#attrs)*
                 #documentation
                 #f
@@ -129,6 +141,7 @@ pub fn ensures(attr: TS1, tokens: TS1) -> TS1 {
                 #ensures_tokens
                 #res_id
             });
+            // FIXME: forbid logical aliases in this case
             TS1::from(quote! {
                 #[creusot::clause::ensures=#name_tag]
                 #clos
@@ -224,6 +237,29 @@ pub fn check(args: TS1, tokens: TS1) -> TS1 {
     result.into()
 }
 
+pub fn has_logical_alias(attr: TS1, tokens: TS1) -> TS1 {
+    let logic_path = match syn::parse::<Path>(attr.clone()) {
+        Ok(path) => path,
+        Err(err) => {
+            return syn::Error::new(err.span(), "`has_logical_alias` should contain a path to a logical function with the same signature").to_compile_error().into()
+        }
+    };
+    let tokens_2 = tokens.clone();
+    let func = parse_macro_input!(tokens_2 as syn::ImplItemFn);
+    let args = func.sig.inputs.iter().map(|a| match a {
+        syn::FnArg::Receiver(receiver) => {
+            let self_t = receiver.self_token;
+            quote!(#self_t)
+        }
+        syn::FnArg::Typed(pat_type) => {
+            let pat = &pat_type.pat;
+            quote!(#pat)
+        }
+    });
+    let ensures_contract = quote_spanned! {logic_path.span()=> result == #logic_path(#(#args),*)};
+    ensures_inner(ensures_contract.into(), tokens, true)
+}
+
 pub fn bitwise_proof(_: TS1, tokens: TS1) -> TS1 {
     let tokens: TokenStream = tokens.into();
     TS1::from(quote! {

creusot-contracts-proc/src/dummy.rs

@@ -112,6 +112,10 @@ pub fn bitwise_proof(_: TS1, tokens: TS1) -> TS1 {
     tokens
 }
 
+pub fn has_logical_alias(_: TS1, tokens: TS1) -> TS1 {
+    tokens
+}
+
 pub fn derive_deep_model(_: TS1) -> TS1 {
     TS1::new()
 }

creusot-contracts-proc/src/lib.rs

@@ -66,6 +66,7 @@ proc_macro_attributes! {
     bitwise_proof
     maintains
     erasure
+    has_logical_alias
 }
 
 macro_rules! proc_macros {

creusot-contracts/src/lib.rs

@@ -487,6 +487,38 @@ pub mod macros {
     pub use base_macros::erasure;
 
     pub(crate) use base_macros::intrinsic;
+
+    /// Defines a _logical alias_ for a program function.
+    ///
+    /// Logical aliases allow you to use the same name for a program and a [`logic`] function.
+    /// Creusot will generate a proof obligation to show that the two functions return
+    /// the same results.
+    ///
+    /// # Example
+    ///
+    /// ```rust
+    /// use creusot_contracts::*;
+    /// pub struct S<T> {
+    ///     t: T,
+    /// }
+    /// impl<T> S<T> {
+    ///     #[has_logical_alias(Self::read_t_logic)]
+    ///     pub fn read_t(&self) -> &T {
+    ///         &self.t
+    ///     }
+    ///
+    ///     #[logic]
+    ///     pub fn read_t_logic(&self) -> &T {
+    ///         &self.t
+    ///     }
+    /// }
+    ///
+    /// // ...
+    ///
+    /// #[requires(s.read_t().view() == 1)]
+    /// pub fn foo(s: S<i32>) { /* ... */ }
+    /// ```
+    pub use base_macros::has_logical_alias;
 }
 
 #[doc(hidden)]

creusot/src/contracts_items/attributes.rs

@@ -1,5 +1,6 @@
 //! Defines all the internal creusot attributes.
 
+use crate::ctx::{HasTyCtxt as _, TranslationCtx};
 use rustc_ast::{
     LitKind, MetaItemInner, Param,
     token::TokenKind,
@@ -13,8 +14,6 @@ use why3::{
     declaration::{Attribute as WAttribute, Meta, MetaArg, MetaIdent},
 };
 
-use crate::ctx::HasTyCtxt as _;
-
 /// Helper macro, converts `creusot::foo::bar` into `["creusot", "foo", "bar"]`.
 macro_rules! path_to_str {
     ([ :: $($p:tt)* ] ; [ $($acc:expr,)* ]) => {
@@ -258,6 +257,40 @@ pub(crate) fn is_open_inv_param(tcx: TyCtxt, p: &Param) -> bool {
     found
 }
 
+/// If a function is annotated with `#[has_logical_alias(f)]`, return the [`DefId`] of `f`.
+pub(crate) fn function_has_logical_alias(
+    ctx: &mut TranslationCtx,
+    def_id: DefId,
+) -> Option<(Span, DefId)> {
+    let attrs = get_attrs(ctx.get_all_attrs(def_id), &["creusot", "decl", "logical_alias_path"]);
+    let attr = match attrs.as_slice() {
+        [] => return None,
+        [a] => a,
+        _ => {
+            ctx.dcx().span_err(
+                attrs.iter().map(|attr| attr.span()).collect::<Vec<_>>(),
+                "A function cannot have multiple logical aliases",
+            );
+            return None;
+        }
+    };
+    let symbol = match &attr.get_normal_item().args {
+        AttrArgs::Eq { expr, .. } => expr.symbol,
+        _ => unreachable!(),
+    };
+    // the `ensures(result == f(args))` clause
+    let ensures_def_id = ctx.creusot_item(symbol).unwrap();
+    let ensures_body =
+        ctx.term(ensures_def_id).expect("no ensures clause associated with this alias");
+    match &ensures_body.1.kind {
+        crate::translation::pearlite::TermKind::Binary { rhs, .. } => match &rhs.kind {
+            crate::translation::pearlite::TermKind::Call { id, .. } => Some((attr.span(), *id)),
+            _ => unreachable!("this should be a function call"),
+        },
+        _ => unreachable!("this should be an equality"),
+    }
+}
+
 fn get_attrs<'a>(attrs: &'a [Attribute], path: &[&str]) -> Vec<&'a Attribute> {
     let mut matched = Vec::new();