Introduce hax_lib::BACKEND::replace_body attribute

hax-lib/build.rs

@@ -0,0 +1,50 @@
+use std::env;
+use std::fs;
+use std::path::Path;
+
+const FSTAR_EXTRA: &str = r"
+pub use hax_lib_macros::fstar_options as options;
+pub use hax_lib_macros::fstar_verification_status as verification_status;
+";
+
+fn main() {
+    let code = |backend: &str, extra: &str| {
+        format!(
+            r#"
+pub use hax_lib_macros::{backend}_expr as {backend};
+#[doc(hidden)]
+pub use hax_lib_macros::{backend}_unsafe_expr;
+#[doc(hidden)]
+pub use hax_lib_macros::{backend}_prop_expr;
+
+/// Procedular macros that have an effect only for the backend {backend}.
+pub mod {backend} {{
+    #[doc(hidden)]
+    pub use hax_lib_macros::{backend}_unsafe_expr as unsafe_expr;
+    pub use hax_lib_macros::{backend}_prop_expr as prop;
+    pub use hax_lib_macros::{backend}_after as after;
+    pub use hax_lib_macros::{backend}_before as before;
+    pub use hax_lib_macros::{backend}_replace as replace;
+    pub use hax_lib_macros::{backend}_replace_body as replace_body;
+
+    {extra}
+}}
+"#
+        )
+    };
+
+    let out_dir = env::var_os("OUT_DIR").unwrap();
+    let dest_path = Path::new(&out_dir).join("proc_macros_generated.rs");
+    fs::write(
+        &dest_path,
+        [
+            code("fstar", FSTAR_EXTRA),
+            code("proverif", ""),
+            code("coq", ""),
+        ]
+        .join("\n"),
+    )
+    .unwrap();
+
+    println!("cargo::rerun-if-changed=build.rs");
+}

hax-lib/macros/src/dummy.rs

@@ -36,6 +36,9 @@ identity_proc_macro_attribute!(
     fstar_replace,
     coq_replace,
     proverif_replace,
+    fstar_replace_body,
+    coq_replace_body,
+    proverif_replace_body,
     fstar_before,
     coq_before,
     proverif_before,
@@ -82,6 +85,19 @@ pub fn proverif_unsafe_expr(_payload: TokenStream) -> TokenStream {
     unsafe_expr()
 }
 
+#[proc_macro]
+pub fn fstar_prop_expr(_payload: TokenStream) -> TokenStream {
+    quote! {::hax_lib::Prop::from_bool(true)}.into()
+}
+#[proc_macro]
+pub fn coq_prop_expr(_payload: TokenStream) -> TokenStream {
+    quote! {::hax_lib::Prop::from_bool(true)}.into()
+}
+#[proc_macro]
+pub fn proverif_prop_expr(_payload: TokenStream) -> TokenStream {
+    quote! {::hax_lib::Prop::from_bool(true)}.into()
+}
+
 fn not_hax_attribute(attr: &syn::Attribute) -> bool {
     if let Meta::List(ml) = &attr.meta {
         !matches!(expects_path_decoration(&ml.path), Ok(Some(_)))

hax-lib/macros/src/implementation.rs

@@ -820,7 +820,19 @@ macro_rules! make_quoting_proc_macro {
             /// Types can be refered to with the syntax `$:{TYPE}`.
             #[proc_macro]
             pub fn [<$backend _expr>](payload: pm::TokenStream) -> pm::TokenStream {
-                let ts: TokenStream = quote::expression(true, payload).into();
+                let ts: TokenStream = quote::expression(quote::InlineExprType::Unit, payload).into();
+                quote!{
+                    #[cfg([< hax_backend_ $backend >])]
+                    {
+                        #ts
+                    }
+                }.into()
+            }
+
+            #[doc = concat!("The `Prop` version of `", stringify!($backend), "_expr`.")]
+            #[proc_macro]
+            pub fn [<$backend _prop_expr>](payload: pm::TokenStream) -> pm::TokenStream {
+                let ts: TokenStream = quote::expression(quote::InlineExprType::Prop, payload).into();
                 quote!{
                     #[cfg([< hax_backend_ $backend >])]
                     {
@@ -833,7 +845,7 @@ macro_rules! make_quoting_proc_macro {
             #[proc_macro]
             #[doc(hidden)]
             pub fn [<$backend _unsafe_expr>](payload: pm::TokenStream) -> pm::TokenStream {
-                let ts: TokenStream = quote::expression(false, payload).into();
+                let ts: TokenStream = quote::expression(quote::InlineExprType::Anything, payload).into();
                 quote!{
                     #[cfg([< hax_backend_ $backend >])]
                     {
@@ -845,14 +857,35 @@ macro_rules! make_quoting_proc_macro {
             make_quoting_item_proc_macro!($backend, [< $backend _before >], ItemQuotePosition::Before, [< hax_backend_ $backend >]);
             make_quoting_item_proc_macro!($backend, [< $backend _after >], ItemQuotePosition::After, [< hax_backend_ $backend >]);
 
-            #[doc = concat!("Replaces a Rust expression with some verbatim ", stringify!($backend)," code.")]
+            #[doc = concat!("Replaces a Rust item with some verbatim ", stringify!($backend)," code.")]
             #[proc_macro_error]
             #[proc_macro_attribute]
             pub fn [< $backend _replace >](payload: pm::TokenStream, item: pm::TokenStream) -> pm::TokenStream {
                 let item: TokenStream = item.into();
                 let attr = AttrPayload::ItemStatus(ItemStatus::Included { late_skip: true });
                 [< $backend _before >](payload, quote!{#attr #item}.into())
             }
+
+            #[doc = concat!("Replaces the body of a Rust function with some verbatim ", stringify!($backend)," code.")]
+            #[proc_macro_error]
+            #[proc_macro_attribute]
+            pub fn [< $backend _replace_body >](payload: pm::TokenStream, item: pm::TokenStream) -> pm::TokenStream {
+                let payload: TokenStream = payload.into();
+                let item: ItemFn = parse_macro_input!(item);
+                let mut hax_item = item.clone();
+                *hax_item.block.as_mut() = parse_quote!{
+                    {
+                        ::hax_lib::$backend::unsafe_expr!(#payload)
+                    }
+                };
+                quote!{
+                    #[cfg([< hax_backend_ $backend >])]
+                    #hax_item
+
+                    #[cfg(not([< hax_backend_ $backend >]))]
+                    #item
+                }.into()
+            }
         }
     };
     ($($backend:ident)*) => {

hax-lib/macros/src/quote.rs

@@ -131,7 +131,7 @@ pub(super) fn item(
     payload: pm::TokenStream,
     item: pm::TokenStream,
 ) -> pm::TokenStream {
-    let expr = TokenStream::from(expression(true, payload));
+    let expr = TokenStream::from(expression(InlineExprType::Unit, payload));
     let item = TokenStream::from(item);
     let uid = ItemUid::fresh();
     let uid_attr = AttrPayload::Uid(uid.clone());
@@ -174,7 +174,13 @@ pub(super) fn detect_future_node_in_expression(e: &syn::Expr) -> bool {
     visitor.0
 }
 
-pub(super) fn expression(force_unit: bool, payload: pm::TokenStream) -> pm::TokenStream {
+pub(super) enum InlineExprType {
+    Unit,
+    Prop,
+    Anything,
+}
+
+pub(super) fn expression(typ: InlineExprType, payload: pm::TokenStream) -> pm::TokenStream {
     let (mut backend_code, antiquotes) = {
         let payload = parse_macro_input!(payload as LitStr).value();
         if payload.contains(SPLIT_MARK) {
@@ -191,7 +197,7 @@ pub(super) fn expression(force_unit: bool, payload: pm::TokenStream) -> pm::Toke
         (quote! {#string}, antiquotes)
     };
     for user in antiquotes.iter().rev() {
-        if !force_unit
+        if !matches!(typ, InlineExprType::Unit)
             && syn::parse(user.ts.clone())
                 .as_ref()
                 .map(detect_future_node_in_expression)
@@ -209,10 +215,10 @@ pub(super) fn expression(force_unit: bool, payload: pm::TokenStream) -> pm::Toke
         };
     }
 
-    let function = if force_unit {
-        quote! {inline}
-    } else {
-        quote! {inline_unsafe::<::hax_lib::Prop>}
+    let function = match typ {
+        InlineExprType::Unit => quote! {inline},
+        InlineExprType::Prop => quote! {inline_unsafe::<::hax_lib::Prop>},
+        InlineExprType::Anything => quote! {inline_unsafe},
     };
 
     quote! {

hax-lib/macros/src/utils.rs

@@ -6,9 +6,9 @@ pub struct HaxQuantifiers;
 impl ToTokens for HaxQuantifiers {
     fn to_tokens(&self, tokens: &mut proc_macro2::TokenStream) {
         quote! {
-            use ::hax_lib::fstar_unsafe_expr as fstar;
-            use ::hax_lib::coq_unsafe_expr as coq;
-            use ::hax_lib::proverif_unsafe_expr as proverif;
+            use ::hax_lib::fstar::prop as fstar;
+            use ::hax_lib::coq::prop as coq;
+            use ::hax_lib::proverif::prop as proverif;
         }
         .to_tokens(tokens)
     }

hax-lib/src/proc_macros.rs

@@ -10,33 +10,4 @@ pub use hax_lib_macros::{
     process_init, process_read, process_write, protocol_messages, pv_constructor, pv_handwritten,
 };
 
-macro_rules! export_quoting_proc_macros {
-    ($backend:ident($expr_name:ident, $expr_unsafe_name:ident, $before_name:ident, $after_name:ident, $replace_name:ident, $cfg_name:ident $(, {$($extra:tt)+})?)) => {
-        pub use hax_lib_macros::$expr_name as $backend;
-        #[doc(hidden)]
-        pub use hax_lib_macros::$expr_unsafe_name;
-
-        #[doc=concat!("Procedural macros for ", stringify!($backend))]
-        pub mod $backend {
-            pub use hax_lib_macros::$after_name as after;
-            pub use hax_lib_macros::$before_name as before;
-            pub use hax_lib_macros::$replace_name as replace;
-            $($($extra)*)?
-        }
-    };
-
-    ($backend:ident $payload:tt $($others:tt)+) => {
-        export_quoting_proc_macros!($backend$payload);
-        export_quoting_proc_macros!($($others)+);
-    }
-}
-
-export_quoting_proc_macros!(
-    fstar(fstar_expr, fstar_unsafe_expr, fstar_before, fstar_after, fstar_replace, hax_backend_fstar, {
-        pub use hax_lib_macros::fstar_options as options;
-        pub use hax_lib_macros::fstar_verification_status as verification_status;
-    })
-
-    coq(coq_expr, coq_unsafe_expr, coq_before, coq_after, coq_replace, hax_backend_coq)
-
-    proverif(proverif_expr, proverif_unsafe_expr, proverif_before, proverif_after, proverif_replace, hax_backend_proverif));
+include!(concat!(env!("OUT_DIR"), "/proc_macros_generated.rs"));

test-harness/src/snapshots/toolchain__attributes into-fstar.snap

@@ -381,6 +381,26 @@ let t_FieldElement = x: u16{x <=. mk_u16 2347}
 /// Example of a specific constraint on a value
 let t_CompressionFactor = x: u8{x =. mk_u8 4 || x =. mk_u8 5 || x =. mk_u8 10 || x =. mk_u8 11}
 '''
+"Attributes.Replace_body.fst" = '''
+module Attributes.Replace_body
+#set-options "--fuel 0 --ifuel 1 --z3rlimit 15"
+open Core
+open FStar.Mul
+
+let f (x y: u8) : u8 = magic x
+
+type t_Foo = | Foo : t_Foo
+
+let impl_Foo__assoc_fn (self: t_Foo) (x: u8) : Prims.unit = (magic (self <: t_Foo)) x
+
+[@@ FStar.Tactics.Typeclasses.tcinstance]
+let impl_1: Alloc.String.t_ToString t_Foo =
+  {
+    f_to_string_pre = (fun (self: t_Foo) -> true);
+    f_to_string_post = (fun (self: t_Foo) (out: Alloc.String.t_String) -> true);
+    f_to_string = fun (self: t_Foo) -> "The type was t_Foo"
+  }
+'''
 "Attributes.Requires_mut.fst" = '''
 module Attributes.Requires_mut
 #set-options "--fuel 0 --ifuel 1 --z3rlimit 15"

tests/attributes/src/lib.rs

@@ -180,6 +180,24 @@ fn some_function() -> String {
     String::from("hello from Rust")
 }
 
+mod replace_body {
+    #[hax_lib::fstar::replace_body("magic ${x}")]
+    fn f(x: u8, y: u8) -> u8 {
+        1 + 2
+    }
+    struct Foo;
+    impl Foo {
+        #[hax_lib::fstar::replace_body("(magic (${self} <: $:{Self})) ${x}")]
+        fn assoc_fn(&self, x: u8) {}
+    }
+    impl ToString for Foo {
+        #[hax_lib::fstar::replace_body(r#""The type was $:{Self}""#)]
+        fn to_string(&self) -> String {
+            "Hello".into()
+        }
+    }
+}
+
 mod pre_post_on_traits_and_impls {
     use hax_lib::*;