Merge pull request #826 from hacspec/add-unsafe-versions-of-inlining-…

…macros

Add unsafe versions of inlining macros

engine/lib/phases/phase_transform_hax_lib_inline.ml

@@ -80,7 +80,8 @@ module%inlined_contents Make (F : Features.T) = struct
     and quote_of_expr' span (expr : A.expr') =
       match expr with
       | App { f = { e = GlobalVar f; _ }; args = [ payload ]; _ }
-        when Global_ident.eq_name Hax_lib__inline f ->
+        when Global_ident.eq_name Hax_lib__inline f
+             || Global_ident.eq_name Hax_lib__inline_unsafe f ->
           let bindings, str = dexpr payload |> UB.collect_let_bindings in
           let str =
             match

engine/names/src/lib.rs

@@ -51,6 +51,7 @@ fn dummy_hax_concrete_ident_wrapper<I: core::iter::Iterator<Item = u8>>(x: I, mu
     }
 
     let _ = hax_lib::inline("");
+    let _: () = hax_lib::inline_unsafe("");
     use hax_lib::{RefineAs, Refinement};
 
     fn refinements<T: Refinement + Clone, U: RefineAs<T>>(x: T, y: U) -> T {

hax-lib-macros/Cargo.toml

@@ -19,10 +19,12 @@ quote.workspace = true
 syn = { version = "2.0", features = [
     "full",
     "visit-mut",
+    "visit",
     "extra-traits",
     "parsing",
 ] }
 hax-lib-macros-types.workspace = true
+paste = "1.0.15"
 
 [dev-dependencies]
 hax-lib = { path = "../hax-lib" }

hax-lib-macros/src/lib.rs

@@ -195,6 +195,10 @@ pub fn decreases(attr: pm::TokenStream, item: pm::TokenStream) -> pm::TokenStrea
 /// the `ensures` clause, you can refer to such an `&mut` input `x` as
 /// `x` for its "past" value and `future(x)` for its "future" value.
 ///
+/// You can use the (unqualified) macro `fstar!` (`BACKEND!` for any
+/// backend `BACKEND`) to inline F* (or Coq, ProVerif, etc.) code in
+/// the precondition, e.g. `fstar!("true")`.
+///
 /// # Example
 ///
 /// ```
@@ -239,6 +243,10 @@ pub fn requires(attr: pm::TokenStream, item: pm::TokenStream) -> pm::TokenStream
 /// Add a logical postcondition to a function. Note you can use the
 /// `forall` and `exists` operators.
 ///
+/// You can use the (unqualified) macro `fstar!` (`BACKEND!` for any
+/// backend `BACKEND`) to inline F* (or Coq, ProVerif, etc.) code in
+/// the postcondition, e.g. `fstar!("true")`.
+///
 /// # Example
 ///
 /// ```
@@ -657,70 +665,82 @@ macro_rules! make_quoting_item_proc_macro {
 }
 
 macro_rules! make_quoting_proc_macro {
-    ($backend:ident($expr_name:ident, $before_name:ident, $after_name:ident, $replace_name:ident, $cfg_name:ident)) => {
-        #[doc = concat!("Embed ", stringify!($backend), " expression inside a Rust expression. This macro takes only one argument: some raw ", stringify!($backend), " code as a string literal.")]
-        ///
-
-        /// While it is possible to directly write raw backend code,
-        /// sometimes it can be inconvenient. For example, referencing
-        /// Rust names can be a bit cumbersome: for example, the name
-        /// `my_crate::my_module::CONSTANT` might be translated
-        /// differently in a backend (e.g. in the F* backend, it will
-        /// probably be `My_crate.My_module.v_CONSTANT`).
-        ///
+    ($backend:ident) => {
+        paste::paste! {
+            #[doc = concat!("Embed ", stringify!($backend), " expression inside a Rust expression. This macro takes only one argument: some raw ", stringify!($backend), " code as a string literal.")]
+            ///
+
+            /// While it is possible to directly write raw backend code,
+            /// sometimes it can be inconvenient. For example, referencing
+            /// Rust names can be a bit cumbersome: for example, the name
+            /// `my_crate::my_module::CONSTANT` might be translated
+            /// differently in a backend (e.g. in the F* backend, it will
+            /// probably be `My_crate.My_module.v_CONSTANT`).
+            ///
+
+            /// To facilitate this, you can write Rust names directly,
+            /// using the prefix `$`: `f $my_crate::my_module__CONSTANT + 3`
+            /// will be replaced with `f My_crate.My_module.v_CONSTANT + 3`
+            /// in the F* backend for instance.
+
+            /// If you want to refer to the Rust constructor
+            /// `Enum::Variant`, you should write `$$Enum::Variant` (note
+            /// the double dollar).
+
+            /// If the name refers to something polymorphic, you need to
+            /// signal it by adding _any_ type informations,
+            /// e.g. `${my_module::function<()>}`. The curly braces are
+            /// needed for such more complex expressions.
+
+            /// You can also write Rust patterns with the `$?{SYNTAX}`
+            /// syntax, where `SYNTAX` is a Rust pattern. The syntax
+            /// `${EXPR}` also allows any Rust expressions
+            /// `EXPR` to be embedded.
+
+            /// 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();
+                quote!{
+                    #[cfg([< hax_backend_ $backend >])]
+                    {
+                        #ts
+                    }
+                }.into()
+            }
 
-        /// To facilitate this, you can write Rust names directly,
-        /// using the prefix `$`: `f $my_crate::my_module__CONSTANT + 3`
-        /// will be replaced with `f My_crate.My_module.v_CONSTANT + 3`
-        /// in the F* backend for instance.
-
-        /// If you want to refer to the Rust constructor
-        /// `Enum::Variant`, you should write `$$Enum::Variant` (note
-        /// the double dollar).
-
-        /// If the name refers to something polymorphic, you need to
-        /// signal it by adding _any_ type informations,
-        /// e.g. `${my_module::function<()>}`. The curly braces are
-        /// needed for such more complex expressions.
-
-        /// You can also write Rust patterns with the `$?{SYNTAX}`
-        /// syntax, where `SYNTAX` is a Rust pattern. The syntax
-        /// `${EXPR}` also allows any Rust expressions
-        /// `EXPR` to be embedded.
-
-        /// Types can be refered to with the syntax `$:{TYPE}`.
-        #[proc_macro]
-        pub fn $expr_name(payload: pm::TokenStream) -> pm::TokenStream {
-            let ts: TokenStream = quote::expression(payload).into();
-            quote!{
-                #[cfg($cfg_name)]
-                {
-                    #ts
-                }
-            }.into()
-        }
+            #[doc = concat!("The unsafe (because polymorphic: even computationally relevant code can be inlined!) version of `", stringify!($backend), "_expr`.")]
+            #[proc_macro]
+            #[doc(hidden)]
+            pub fn [<$backend _unsafe_expr>](payload: pm::TokenStream) -> pm::TokenStream {
+                let ts: TokenStream = quote::expression(false, payload).into();
+                quote!{
+                    #[cfg([< hax_backend_ $backend >])]
+                    {
+                        #ts
+                    }
+                }.into()
+            }
 
-        make_quoting_item_proc_macro!($backend, $before_name, ItemQuotePosition::Before, $cfg_name);
-        make_quoting_item_proc_macro!($backend, $after_name, ItemQuotePosition::After, $cfg_name);
+            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.")]
-        #[proc_macro_error]
-        #[proc_macro_attribute]
-        pub fn $replace_name(payload: pm::TokenStream, item: pm::TokenStream) -> pm::TokenStream {
-            let item: TokenStream = item.into();
-            let attr = AttrPayload::ItemStatus(ItemStatus::Included { late_skip: true });
-            $before_name(payload, quote!{#attr #item}.into())
+            #[doc = concat!("Replaces a Rust expression 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())
+            }
         }
     };
-    ($backend:ident $payload:tt $($others:tt)+) => {
-        make_quoting_proc_macro!($backend$payload);
-        make_quoting_proc_macro!($($others)+);
+    ($($backend:ident)*) => {
+        $(make_quoting_proc_macro!($backend);)*
     }
 }
 
-make_quoting_proc_macro!(fstar(fstar_expr, fstar_before, fstar_after, fstar_replace, hax_backend_fstar)
-                         coq(coq_expr, coq_before, coq_after, coq_replace, hax_backend_coq)
-                         proverif(proverif_expr, proverif_before, proverif_after, proverif_replace, hax_backend_proverif));
+make_quoting_proc_macro!(fstar coq proverif);
 
 /// Marks a newtype `struct RefinedT(T);` as a refinement type. The
 /// struct should have exactly one unnamed private field.

hax-lib-macros/src/quote.rs

@@ -134,7 +134,7 @@ pub(super) fn item(
     payload: pm::TokenStream,
     item: pm::TokenStream,
 ) -> pm::TokenStream {
-    let expr = TokenStream::from(expression(payload));
+    let expr = TokenStream::from(expression(true, payload));
     let item = TokenStream::from(item);
     let uid = ItemUid::fresh();
     let uid_attr = AttrPayload::Uid(uid.clone());
@@ -162,7 +162,22 @@ pub(super) fn item(
     .into()
 }
 
-pub(super) fn expression(payload: pm::TokenStream) -> pm::TokenStream {
+pub(super) fn detect_future_node_in_expression(e: &syn::Expr) -> bool {
+    struct Visitor(bool);
+    use syn::visit::*;
+    impl<'a> Visit<'a> for Visitor {
+        fn visit_expr(&mut self, e: &'a Expr) {
+            if let Some(Ok(_)) = crate::utils::expect_future_expr(e) {
+                self.0 = true;
+            }
+        }
+    }
+    let mut visitor = Visitor(false);
+    visitor.visit_expr(e);
+    visitor.0
+}
+
+pub(super) fn expression(force_unit: bool, payload: pm::TokenStream) -> pm::TokenStream {
     let (mut backend_code, antiquotes) = {
         let payload = parse_macro_input!(payload as LitStr).value();
         if payload.find(SPLIT_MARK).is_some() {
@@ -178,14 +193,33 @@ pub(super) fn expression(payload: pm::TokenStream) -> pm::TokenStream {
             .collect();
         (quote! {#string}, antiquotes)
     };
-
     for user in antiquotes.iter().rev() {
+        if !force_unit
+            && syn::parse(user.ts.clone())
+                .as_ref()
+                .map(detect_future_node_in_expression)
+                .unwrap_or(false)
+        {
+            let ts: proc_macro2::TokenStream = user.ts.clone().into();
+            return quote! {
+                ::std::compile_error!(concat!("The `future` operator cannot be used within a quote. Hint: move `", stringify!(#ts), "` to a let binding and use the binding name instead."))
+            }.into();
+        }
         let kind = &user.kind;
         backend_code = quote! {
             let #kind = #user;
             #backend_code
         };
     }
 
-    quote! {::hax_lib::inline(#[allow(unused_variables)]{#backend_code})}.into()
+    let function = if force_unit {
+        quote! {inline}
+    } else {
+        quote! {inline_unsafe}
+    };
+
+    quote! {
+        ::hax_lib::#function(#[allow(unused_variables)]{#backend_code})
+    }
+    .into()
 }

hax-lib-macros/src/utils.rs

@@ -17,6 +17,10 @@ impl ToTokens for HaxQuantifiers {
             fn exists<T, F: Fn(T) -> bool>(f: F) -> bool {
                 true
             }
+
+            use ::hax_lib::fstar_unsafe_expr as fstar;
+            use ::hax_lib::coq_unsafe_expr as coq;
+            use ::hax_lib::proverif_unsafe_expr as proverif;
         }
         .to_tokens(tokens)
     }
@@ -133,44 +137,62 @@ fn expect_fn_arg_var_pat(arg: &FnArg) -> Option<(String, syn::Type)> {
     }
 }
 
+pub(crate) enum NotFutureExpr {
+    BadNumberOfArgs,
+    ArgNotIdent,
+}
+
+/// `expect_future_expr(e)` tries to match the pattern
+/// `future(<syn::Ident>)` in expression `e`
+pub(crate) fn expect_future_expr(e: &Expr) -> Option<std::result::Result<Ident, NotFutureExpr>> {
+    if let Expr::Call(call) = e {
+        if call.func.is_ident("future") {
+            return Some(match call.args.iter().collect::<Vec<_>>().as_slice() {
+                [arg] => arg.expect_ident().ok_or(NotFutureExpr::ArgNotIdent),
+                _ => Err(NotFutureExpr::BadNumberOfArgs),
+            });
+        }
+    }
+    None
+}
+
 /// Rewrites `future(x)` nodes in an expression when (1) `x` is an
 /// ident and (2) the ident `x` is contained in the HashSet.
 struct RewriteFuture(HashSet<String>);
 impl VisitMut for RewriteFuture {
     fn visit_expr_mut(&mut self, e: &mut Expr) {
         syn::visit_mut::visit_expr_mut(self, e);
-        if let Expr::Call(call) = e {
-            if call.func.is_ident("future") {
-                let help_message = || match self.0.iter().next() {
+        let error = match expect_future_expr(e) {
+            Some(Ok(arg)) => {
+                let arg = format!("{}", arg);
+                if self.0.contains(&arg) {
+                    let arg = create_future_ident(&arg);
+                    *e = parse_quote! {#arg};
+                    return;
+                }
+                Some(format!("Cannot find an input `{arg}` of type `&mut _`. In the context, `future` can be called on the following inputs: {:?}.", self.0))
+            }
+            Some(Err(error_kind)) => {
+                let message = match error_kind {
+                    NotFutureExpr::BadNumberOfArgs => {
+                        "`future` can only be called with one argument: a `&mut` input name"
+                    }
+                    NotFutureExpr::ArgNotIdent => {
+                        "`future` can only be called with an `&mut` input name"
+                    }
+                };
+                let help_message = match self.0.iter().next() {
                     None => format!(" In the context, there is no `&mut` input."),
                     Some(var) => {
                         format!(" For example, in the context you can write `future({var})`.")
                     }
                 };
-                let error = match call.args.iter().collect::<Vec<_>>().as_slice() {
-                    [arg] => {
-                        if let Some(arg) = arg.expect_ident() {
-                            let arg = format!("{}", arg);
-                            if self.0.contains(&arg) {
-                                let arg = create_future_ident(&arg);
-                                *e = parse_quote! {#arg};
-                                return;
-                            }
-                            format!("Cannot find an input `{arg}` of type `&mut _`. In the context, `future` can be called on the following inputs: {:?}.", self.0)
-                        } else {
-                            format!(
-                                "`future` can only be called with an `&mut` input name.{}",
-                                help_message()
-                            )
-                        }
-                    }
-                    _ => format!(
-                        "`future` can only be called with one argument: a `&mut` input name.{}",
-                        help_message()
-                    ),
-                };
-                *e = parse_quote! {::std::compile_error!(#error)};
+                Some(format!("{message}.{}", help_message))
             }
+            None => None,
+        };
+        if let Some(error) = error {
+            *e = parse_quote! {::std::compile_error!(#error)};
         }
     }
 }

hax-lib/src/lib.rs

@@ -141,6 +141,12 @@ pub fn implies(lhs: bool, rhs: impl Fn() -> bool) -> bool {
 #[doc(hidden)]
 pub fn inline(_: &str) {}
 
+/// Similar to `inline`, but allows for any type. Do not use directly.
+#[doc(hidden)]
+pub fn inline_unsafe<T>(_: &str) -> T {
+    unreachable!()
+}
+
 /// A type that implements `Refinement` should be a newtype for a
 /// type `T`. The field holding the value of type `T` should be
 /// private, and `Refinement` should be the only interface to the