feat(hax-lib&backend): F*: support for SMT patterns

engine/backends/fstar/fstar_backend.ml

@@ -897,7 +897,7 @@ struct
              >> Option.value ~default:Fn.id map_expr
              >> pexpr >> f >> F.term)
     in
-    let decreases =
+    let extract_any_to_unit_payload =
       let visitor =
         object
           inherit [_] U.Visitors.map as super
@@ -910,9 +910,18 @@ struct
             | _ -> super#visit_expr () e
         end
       in
-      attr_term Decreases ~map_expr:(visitor#visit_expr ()) (fun t ->
+      visitor#visit_expr ()
+    in
+    let decreases =
+      attr_term Decreases ~map_expr:extract_any_to_unit_payload (fun t ->
           F.AST.Decreases (t, None))
     in
+    let smtpat =
+      let smt_pat = F.term_of_lid [ "SMTPat" ] in
+      attr_term SMTPat ~map_expr:extract_any_to_unit_payload (fun t ->
+          let payload = F.mk_e_app smt_pat [ t ] in
+          (F.AST.mkConsList F.dummyRange [ payload ]).tm)
+    in
     let is_lemma = Attrs.lemma attrs in
     let prepost_bundle =
       let trivial_pre = F.term_of_lid [ "Prims"; "l_True" ] in
@@ -935,7 +944,7 @@ struct
     let args =
       (Option.map ~f:(fun (req, ens) -> [ req; ens ]) prepost_bundle
       |> Option.value ~default:[])
-      @ Option.to_list decreases
+      @ Option.to_list decreases @ Option.to_list smtpat
     in
     match args with
     | [] -> typ

engine/lib/attr_payloads.ml

@@ -63,6 +63,7 @@ module AssocRole = struct
       | Requires
       | Ensures
       | Decreases
+      | SMTPat
       | Refine
       | ProcessRead
       | ProcessWrite
@@ -84,6 +85,7 @@ module AssocRole = struct
     | Requires -> Requires
     | Ensures -> Ensures
     | Decreases -> Decreases
+    | SMTPat -> SMTPat
     | Refine -> Refine
     | ItemQuote -> ItemQuote
     | ProcessRead -> ProcessRead

hax-lib/build.rs

@@ -5,6 +5,7 @@ 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;
+pub use hax_lib_macros::fstar_smt_pat as smt_pat;
 ";
 
 fn main() {

hax-lib/macros/src/dummy.rs

@@ -46,6 +46,7 @@ identity_proc_macro_attribute!(
     fstar_after,
     coq_after,
     proverif_after,
+    fstar_smt_pat,
 );
 
 #[proc_macro]

hax-lib/macros/src/implementation.rs

@@ -317,6 +317,18 @@ pub fn decreases(attr: pm::TokenStream, item: pm::TokenStream) -> pm::TokenStrea
     quote! {#requires #attr #item}.into()
 }
 
+/// Allows to add SMT patterns to a lemma.
+/// For more informations about SMT patterns, please take a look here: https://fstar-lang.org/tutorial/book/under_the_hood/uth_smt.html#designing-a-library-with-smt-patterns.
+#[proc_macro_error]
+#[proc_macro_attribute]
+pub fn fstar_smt_pat(attr: pm::TokenStream, item: pm::TokenStream) -> pm::TokenStream {
+    let phi: syn::Expr = parse_macro_input!(attr);
+    let item: FnLike = parse_macro_input!(item);
+    let (requires, attr) =
+        make_fn_decoration(phi, item.sig.clone(), FnDecorationKind::SMTPat, None, None);
+    quote! {#requires #attr #item}.into()
+}
+
 /// Add a logical precondition to a function.
 // Note you can use the `forall` and `exists` operators. (TODO: commented out for now, see #297)
 /// In the case of a function that has one or more `&mut` inputs, in

hax-lib/macros/src/utils.rs

@@ -21,6 +21,7 @@ pub enum FnDecorationKind {
     Requires,
     Ensures { ret_binder: Pat },
     Decreases,
+    SMTPat,
 }
 
 impl ToString for FnDecorationKind {
@@ -29,6 +30,7 @@ impl ToString for FnDecorationKind {
             FnDecorationKind::Requires => "requires".to_string(),
             FnDecorationKind::Ensures { .. } => "ensures".to_string(),
             FnDecorationKind::Decreases { .. } => "decreases".to_string(),
+            FnDecorationKind::SMTPat { .. } => "SMTPat".to_string(),
         }
     }
 }
@@ -39,6 +41,7 @@ impl From<FnDecorationKind> for AssociationRole {
             FnDecorationKind::Requires => AssociationRole::Requires,
             FnDecorationKind::Ensures { .. } => AssociationRole::Ensures,
             FnDecorationKind::Decreases => AssociationRole::Decreases,
+            FnDecorationKind::SMTPat => AssociationRole::SMTPat,
         }
     }
 }
@@ -294,16 +297,17 @@ pub fn make_fn_decoration(
             if let Some(generics) = generics {
                 sig.generics = merge_generics(generics, sig.generics);
             }
-            sig.output = if let FnDecorationKind::Decreases = &kind {
-                syn::parse_quote! { -> () }
-            } else {
-                syn::parse_quote! { -> impl Into<::hax_lib::Prop> }
+            sig.output = match &kind {
+                FnDecorationKind::Decreases | FnDecorationKind::SMTPat => {
+                    syn::parse_quote! { -> () }
+                }
+                _ => syn::parse_quote! { -> impl Into<::hax_lib::Prop> },
             };
             sig
         };
         let uid_attr = AttrPayload::Uid(uid.clone());
         let late_skip = &AttrPayload::ItemStatus(ItemStatus::Included { late_skip: true });
-        if let FnDecorationKind::Decreases = &kind {
+        if let FnDecorationKind::Decreases | FnDecorationKind::SMTPat = &kind {
             phi = parse_quote! {::hax_lib::any_to_unit(#phi)};
         };
         let quantifiers = if let FnDecorationKind::Decreases = &kind {

hax-lib/macros/types/src/lib.rs

@@ -54,6 +54,7 @@ pub enum AssociationRole {
     Requires,
     Ensures,
     Decreases,
+    SMTPat,
     Refine,
     /// A quoted piece of backend code to place after or before the
     /// extraction of the marked item

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

@@ -678,6 +678,11 @@ let add3_lemma (x: u32)
       x <=. mk_u32 10 || x >=. (u32_max /! mk_u32 3 <: u32) ||
       (add3 x x x <: u32) =. (x *! mk_u32 3 <: u32)) = ()
 
+let dummy_function (x: u32) : u32 = x
+
+let apply_dummy_function_lemma (x: u32) : Lemma (ensures x =. (dummy_function x <: u32)) [SMTPat x] =
+  ()
+
 type t_Foo = {
   f_x:u32;
   f_y:f_y: u32{b2t (f_y >. mk_u32 3 <: bool)};

tests/attributes/src/lib.rs

@@ -38,6 +38,14 @@ mod ensures_on_arity_zero_fns {
 #[hax::lemma]
 fn add3_lemma(x: u32) -> Proof<{ x <= 10 || x >= u32_max / 3 || add3(x, x, x) == x * 3 }> {}
 
+fn dummy_function(x: u32) -> u32 {
+    x
+}
+
+#[hax::lemma]
+#[hax::fstar::smt_pat(x)]
+fn apply_dummy_function_lemma(x: u32) -> Proof<{ x == dummy_function(x) }> {}
+
 #[hax::exclude]
 pub fn f<'a, T>(c: bool, x: &'a mut T, y: &'a mut T) -> &'a mut T {
     if c {