From 0248fd3edab9e5739fa2b61d9e0827104a45d7dc Mon Sep 17 00:00:00 2001
From: Lucas Franceschino <lucas@cryspen.com>
Date: Mon, 22 Apr 2024 10:50:17 +0200
Subject: [PATCH 01/21] refactor(engine): make `quote` its own type and
 functions

---
 engine/backends/fstar/fstar_backend.ml | 18 +++---
 engine/lib/ast.ml                      | 10 +--
 engine/lib/ast_visitors.ml             | 88 ++++++++++++++------------
 engine/lib/subtype.ml                  | 17 ++---
 4 files changed, 74 insertions(+), 59 deletions(-)

diff --git a/engine/backends/fstar/fstar_backend.ml b/engine/backends/fstar/fstar_backend.ml
index 97cae64b3..a92600b16 100644
--- a/engine/backends/fstar/fstar_backend.ml
+++ b/engine/backends/fstar/fstar_backend.ml
@@ -573,16 +573,18 @@ struct
              kind = UnsupportedMacro { id = [%show: global_ident] macro };
              span = e.span;
            }
-    | Quote { contents; _ } ->
-        List.map
-          ~f:(function
-            | `Verbatim code -> code
-            | `Expr e -> pexpr e |> term_to_string
-            | `Pat p -> ppat p |> pat_to_string)
-          contents
-        |> String.concat |> F.term_of_string
+    | Quote quote -> pquote quote |> F.term_of_string
     | _ -> .
 
+  and pquote { contents; _ } =
+    List.map
+      ~f:(function
+        | `Verbatim code -> code
+        | `Expr e -> pexpr e |> term_to_string
+        | `Pat p -> ppat p |> pat_to_string)
+      contents
+    |> String.concat
+
   and parm { arm = { arm_pat; body } } = (ppat arm_pat, None, pexpr body)
 
   module FStarBinder = struct
diff --git a/engine/lib/ast.ml b/engine/lib/ast.ml
index bb03c837f..93ed12c44 100644
--- a/engine/lib/ast.ml
+++ b/engine/lib/ast.ml
@@ -258,15 +258,17 @@ functor
         }
       | Closure of { params : pat list; body : expr; captures : expr list }
       | EffectAction of { action : F.monadic_action; argument : expr }
-      | Quote of {
-          contents : [ `Verbatim of string | `Expr of expr | `Pat of pat ] list;
-          witness : F.quote;
-        }
+      | Quote of quote
           (** A quotation is an inlined piece of backend code
               interleaved with Rust code *)
 
     and expr = { e : expr'; span : span; typ : ty }
 
+    and quote = {
+      contents : [ `Verbatim of string | `Expr of expr | `Pat of pat ] list;
+      witness : F.quote;
+    }
+
     and supported_monads =
       | MException of ty
           (** a exception monad, which we use to handle early returns *)
diff --git a/engine/lib/ast_visitors.ml b/engine/lib/ast_visitors.ml
index 64fc30019..14077443f 100644
--- a/engine/lib/ast_visitors.ml
+++ b/engine/lib/ast_visitors.ml
@@ -434,17 +434,7 @@ functor
               in
               let argument = self#visit_expr env record_payload.argument in
               EffectAction { action; argument }
-          | Quote { contents; witness } ->
-              let contents =
-                self#visit_list
-                  (fun env -> function
-                    | `Verbatim code -> `Verbatim code
-                    | `Expr e -> `Expr (self#visit_expr env e)
-                    | `Pat p -> `Pat (self#visit_pat env p))
-                  env contents
-              in
-              let witness = self#visit_feature_quote env witness in
-              Quote { contents; witness }
+          | Quote quote -> Quote (self#visit_quote env quote)
 
         method visit_expr (env : 'env) (this : expr) : expr =
           let e = self#visit_expr' env this.e in
@@ -453,6 +443,19 @@ functor
           let out : expr = { e; span; typ } in
           out
 
+        method visit_quote (env : 'env) ({ contents; witness } : quote) : quote
+            =
+          let contents =
+            self#visit_list
+              (fun env -> function
+                | `Verbatim code -> `Verbatim code
+                | `Expr e -> `Expr (self#visit_expr env e)
+                | `Pat p -> `Pat (self#visit_pat env p))
+              env contents
+          in
+          let witness = self#visit_feature_quote env witness in
+          { contents; witness }
+
         method visit_supported_monads (env : 'env) (this : supported_monads)
             : supported_monads =
           match this with
@@ -1461,22 +1464,9 @@ functor
               in
               let reduce_acc = self#plus reduce_acc reduce_acc' in
               (EffectAction { action; argument }, reduce_acc)
-          | Quote { contents; witness } ->
-              let list, reduce_acc =
-                self#visit_list
-                  (fun env -> function
-                    | `Verbatim code -> (`Verbatim code, self#zero)
-                    | `Expr e ->
-                        let e, acc = self#visit_expr env e in
-                        (`Expr e, acc)
-                    | `Pat p ->
-                        let p, acc = self#visit_pat env p in
-                        (`Pat p, acc))
-                  env contents
-              in
-              let witness, reduce_acc' = self#visit_feature_quote env witness in
-              let reduce_acc = self#plus reduce_acc reduce_acc' in
-              (Quote { contents; witness }, reduce_acc)
+          | Quote quote ->
+              let quote, acc = self#visit_quote env quote in
+              (Quote quote, acc)
 
         method visit_expr (env : 'env) (this : expr) : expr * 'acc =
           let e, reduce_acc = self#visit_expr' env this.e in
@@ -1487,6 +1477,24 @@ functor
           let out : expr = { e; span; typ } in
           (out, reduce_acc)
 
+        method visit_quote (env : 'env) ({ contents; witness } : quote)
+            : quote * 'acc =
+          let list, reduce_acc =
+            self#visit_list
+              (fun env -> function
+                | `Verbatim code -> (`Verbatim code, self#zero)
+                | `Expr e ->
+                    let e, acc = self#visit_expr env e in
+                    (`Expr e, acc)
+                | `Pat p ->
+                    let p, acc = self#visit_pat env p in
+                    (`Pat p, acc))
+              env contents
+          in
+          let witness, reduce_acc' = self#visit_feature_quote env witness in
+          let reduce_acc = self#plus reduce_acc reduce_acc' in
+          ({ contents; witness }, reduce_acc)
+
         method visit_supported_monads (env : 'env) (this : supported_monads)
             : supported_monads * 'acc =
           match this with
@@ -2602,18 +2610,7 @@ functor
               let reduce_acc' = self#visit_expr env record_payload.argument in
               let reduce_acc = self#plus reduce_acc reduce_acc' in
               reduce_acc
-          | Quote { contents; witness } ->
-              let reduce_acc =
-                self#visit_list
-                  (fun env -> function
-                    | `Verbatim code -> self#zero
-                    | `Expr e -> self#visit_expr env e
-                    | `Pat p -> self#visit_pat env p)
-                  env contents
-              in
-              let reduce_acc' = self#visit_feature_quote env witness in
-              let reduce_acc = self#plus reduce_acc reduce_acc' in
-              reduce_acc
+          | Quote quote -> self#visit_quote env quote
 
         method visit_expr (env : 'env) (this : expr) : 'acc =
           let reduce_acc = self#visit_expr' env this.e in
@@ -2623,6 +2620,19 @@ functor
           let reduce_acc = self#plus reduce_acc reduce_acc' in
           reduce_acc
 
+        method visit_quote (env : 'env) ({ contents; witness } : quote) : 'acc =
+          let reduce_acc =
+            self#visit_list
+              (fun env -> function
+                | `Verbatim code -> self#zero
+                | `Expr e -> self#visit_expr env e
+                | `Pat p -> self#visit_pat env p)
+              env contents
+          in
+          let reduce_acc' = self#visit_feature_quote env witness in
+          let reduce_acc = self#plus reduce_acc reduce_acc' in
+          reduce_acc
+
         method visit_supported_monads (env : 'env) (this : supported_monads)
             : 'acc =
           match this with
diff --git a/engine/lib/subtype.ml b/engine/lib/subtype.ml
index c793efdea..2e1ae33fb 100644
--- a/engine/lib/subtype.ml
+++ b/engine/lib/subtype.ml
@@ -260,14 +260,15 @@ struct
             body = dexpr body;
             captures = List.map ~f:dexpr captures;
           }
-    | Quote { contents; witness } ->
-        let f = function
-          | `Verbatim code -> `Verbatim code
-          | `Expr e -> `Expr (dexpr e)
-          | `Pat p -> `Pat (dpat p)
-        in
-        Quote
-          { contents = List.map ~f contents; witness = S.quote span witness }
+    | Quote quote -> Quote (dquote span quote)
+
+  and dquote (span : span) ({ contents; witness } : A.quote) : B.quote =
+    let f = function
+      | `Verbatim code -> `Verbatim code
+      | `Expr e -> `Expr (dexpr e)
+      | `Pat p -> `Pat (dpat p)
+    in
+    { contents = List.map ~f contents; witness = S.quote span witness }
 
   and dloop_kind (span : span) (k : A.loop_kind) : B.loop_kind =
     match k with

From 1eb7b869977f48839ad5b38909c171f4d8b79a83 Mon Sep 17 00:00:00 2001
From: Lucas Franceschino <lucas@cryspen.com>
Date: Mon, 22 Apr 2024 17:55:26 +0200
Subject: [PATCH 02/21] fix(engine): better error messages on uncatched error

---
 engine/bin/lib.ml         | 10 +++++++++-
 engine/lib/diagnostics.ml |  4 ++--
 2 files changed, 11 insertions(+), 3 deletions(-)

diff --git a/engine/bin/lib.ml b/engine/bin/lib.ml
index 91ae9e95d..8eb3bf3ea 100644
--- a/engine/bin/lib.ml
+++ b/engine/bin/lib.ml
@@ -126,7 +126,15 @@ let run (options : Types.engine_options) : Types.output =
 let main (options : Types.engine_options) =
   Printexc.record_backtrace true;
   let result =
-    try Ok (run options) with e -> Error (e, Printexc.get_raw_backtrace ())
+    try Ok (run options) with
+    | Hax_engine.Diagnostics.SpanFreeError.Exn exn ->
+        Error
+          ( Failure
+              ("Uncatched hax exception (please report, this should not \
+                appear): "
+              ^ [%show: Hax_engine.Diagnostics.SpanFreeError.t] exn),
+            Printexc.get_raw_backtrace () )
+    | e -> Error (e, Printexc.get_raw_backtrace ())
   in
   match result with
   | Ok results ->
diff --git a/engine/lib/diagnostics.ml b/engine/lib/diagnostics.ml
index f42be273e..c6400e75c 100644
--- a/engine/lib/diagnostics.ml
+++ b/engine/lib/diagnostics.ml
@@ -143,14 +143,14 @@ let failure ~context ~span kind =
   Core.raise_fatal_error { context; kind; span = Span.to_thir span }
 
 module SpanFreeError : sig
-  type t = private Data of Context.t * kind
+  type t = private Data of Context.t * kind [@@deriving show]
 
   exception Exn of t
 
   val payload : t -> Context.t * kind
   val raise : ?span:T.span list -> Context.t -> kind -> 'a
 end = struct
-  type t = Data of Context.t * kind
+  type t = Data of Context.t * kind [@@deriving show]
 
   exception Exn of t
 

From f1709d8a9b8e9d2e43d0911708efcb53c395f6c5 Mon Sep 17 00:00:00 2001
From: Lucas Franceschino <lucas@cryspen.com>
Date: Mon, 22 Apr 2024 17:56:25 +0200
Subject: [PATCH 03/21] feat(engine): introduce a `Quote` node for items

---
 engine/lib/ast.ml                          | 1 +
 engine/lib/ast_visitors.ml                 | 5 +++++
 engine/lib/dependencies.ml                 | 2 +-
 engine/lib/phases/phase_drop_references.ml | 3 ++-
 engine/lib/subtype.ml                      | 1 +
 5 files changed, 10 insertions(+), 2 deletions(-)

diff --git a/engine/lib/ast.ml b/engine/lib/ast.ml
index 93ed12c44..e00ebbe21 100644
--- a/engine/lib/ast.ml
+++ b/engine/lib/ast.ml
@@ -390,6 +390,7 @@ functor
           is_external : bool;
           rename : string option;
         }
+      | Quote of quote
       | HaxError of string
       | NotImplementedYet
 
diff --git a/engine/lib/ast_visitors.ml b/engine/lib/ast_visitors.ml
index 14077443f..c536c9f1e 100644
--- a/engine/lib/ast_visitors.ml
+++ b/engine/lib/ast_visitors.ml
@@ -681,6 +681,7 @@ functor
                 self#visit_option self#visit_string env record_payload.rename
               in
               Use { path; is_external; rename }
+          | Quote quote -> Quote (self#visit_quote env quote)
           | HaxError x0 ->
               let x0 = self#visit_string env x0 in
               HaxError x0
@@ -1825,6 +1826,9 @@ functor
               in
               let reduce_acc = self#plus reduce_acc reduce_acc' in
               (Use { path; is_external; rename }, reduce_acc)
+          | Quote quote ->
+              let quote, acc = self#visit_quote env quote in
+              (Quote quote, acc)
           | HaxError x0 ->
               let x0, reduce_acc = self#visit_string env x0 in
               (HaxError x0, reduce_acc)
@@ -2928,6 +2932,7 @@ functor
               in
               let reduce_acc = self#plus reduce_acc reduce_acc' in
               reduce_acc
+          | Quote quote -> self#visit_quote env quote
           | HaxError x0 ->
               let reduce_acc = self#visit_string env x0 in
               reduce_acc
diff --git a/engine/lib/dependencies.ml b/engine/lib/dependencies.ml
index 7c3aa6179..97e8488a6 100644
--- a/engine/lib/dependencies.ml
+++ b/engine/lib/dependencies.ml
@@ -65,7 +65,7 @@ module Make (F : Features.T) = struct
                   v#visit_impl_expr () ie @ v#visit_impl_ident () ii)
                 parent_bounds
         | Alias { name = _; item } -> v#visit_concrete_ident () item
-        | Use _ | HaxError _ | NotImplementedYet ->
+        | Use _ | Quote _ | HaxError _ | NotImplementedYet ->
             Set.empty (module Concrete_ident)
       in
       set |> Set.to_list
diff --git a/engine/lib/phases/phase_drop_references.ml b/engine/lib/phases/phase_drop_references.ml
index 4e4727695..c576d99ee 100644
--- a/engine/lib/phases/phase_drop_references.ml
+++ b/engine/lib/phases/phase_drop_references.ml
@@ -68,7 +68,8 @@ struct
 
     and dexpr' (span : span) (e : A.expr') : B.expr' =
       match (UA.unbox_underef_expr { e; span; typ = UA.never_typ }).e with
-      | [%inline_arms If + Literal + Array + Block + QuestionMark + Quote] ->
+      | [%inline_arms
+          If + Literal + Array + Block + QuestionMark + "dexpr'.Quote"] ->
           auto
       | Construct { constructor; is_record; is_struct; fields; base } ->
           Construct
diff --git a/engine/lib/subtype.ml b/engine/lib/subtype.ml
index 2e1ae33fb..8a0de5191 100644
--- a/engine/lib/subtype.ml
+++ b/engine/lib/subtype.ml
@@ -470,6 +470,7 @@ struct
             }
       | Alias { name; item } -> B.Alias { name; item }
       | Use { path; is_external; rename } -> B.Use { path; is_external; rename }
+      | Quote quote -> Quote (dquote span quote)
       | HaxError e -> B.HaxError e
       | NotImplementedYet -> B.NotImplementedYet
 

From bd029d559b28f84b09908e6418fb400507a7c1f6 Mon Sep 17 00:00:00 2001
From: Lucas Franceschino <lucas@cryspen.com>
Date: Mon, 22 Apr 2024 17:57:30 +0200
Subject: [PATCH 04/21] fix(engine): catch errors in trait_specs phase

---
 engine/lib/phases/phase_traits_specs.ml | 9 ++++++++-
 1 file changed, 8 insertions(+), 1 deletion(-)

diff --git a/engine/lib/phases/phase_traits_specs.ml b/engine/lib/phases/phase_traits_specs.ml
index 47187c241..3789ada31 100644
--- a/engine/lib/phases/phase_traits_specs.ml
+++ b/engine/lib/phases/phase_traits_specs.ml
@@ -24,7 +24,7 @@ module Make (F : Features.T) =
 
       let ditems (l : A.item list) : B.item list =
         let (module Attrs) = Attrs.with_items l in
-        let f (item : item) : item =
+        let f' (item : item) : item =
           let v =
             match item.v with
             | Trait { name; generics; items } ->
@@ -122,5 +122,12 @@ module Make (F : Features.T) =
           in
           { item with v }
         in
+        let f item =
+          try f' item
+          with Diagnostics.SpanFreeError.Exn (Data (context, kind)) ->
+            let error = Diagnostics.pretty_print_context_kind context kind in
+            let msg = error in
+            B.make_hax_error_item item.span item.ident msg
+        in
         List.map ~f l
     end)

From e3aa419d3f215ab8677367d5d44edd1adf201527 Mon Sep 17 00:00:00 2001
From: Lucas Franceschino <lucas@cryspen.com>
Date: Mon, 22 Apr 2024 17:58:09 +0200
Subject: [PATCH 05/21] fix(engine): fix name of TranformHaxLibInline phase

---
 engine/lib/diagnostics.ml                           | 1 +
 engine/lib/phases/phase_transform_hax_lib_inline.ml | 2 +-
 2 files changed, 2 insertions(+), 1 deletion(-)

diff --git a/engine/lib/diagnostics.ml b/engine/lib/diagnostics.ml
index c6400e75c..70c65dde0 100644
--- a/engine/lib/diagnostics.ml
+++ b/engine/lib/diagnostics.ml
@@ -44,6 +44,7 @@ module Phase = struct
     | SimplifyMatchReturn
     | SimplifyHoisting
     | DropNeedlessReturns
+    | TransformHaxLibInline
     | DummyA
     | DummyB
     | DummyC
diff --git a/engine/lib/phases/phase_transform_hax_lib_inline.ml b/engine/lib/phases/phase_transform_hax_lib_inline.ml
index 879c273f3..b8ee6f948 100644
--- a/engine/lib/phases/phase_transform_hax_lib_inline.ml
+++ b/engine/lib/phases/phase_transform_hax_lib_inline.ml
@@ -13,7 +13,7 @@ module%inlined_contents Make (F : Features.T) = struct
   include
     Phase_utils.MakeBase (F) (FB)
       (struct
-        let phase_id = Diagnostics.Phase.CfIntoMonads
+        let phase_id = Diagnostics.Phase.TransformHaxLibInline
       end)
 
   module Implem : ImplemT.T = struct

From 52d901a7e9e83b0488de12d3141dac7d8de36605 Mon Sep 17 00:00:00 2001
From: Lucas Franceschino <lucas@cryspen.com>
Date: Mon, 22 Apr 2024 17:59:03 +0200
Subject: [PATCH 06/21] feat: proc macro for inlining items

---
 engine/backends/fstar/fstar_backend.ml        | 35 ++++++-
 engine/lib/attr_payloads.ml                   | 91 +++++++++++++------
 .../phases/phase_transform_hax_lib_inline.ml  | 60 +++++++++++-
 hax-lib-macros/src/lib.rs                     | 85 +++++++++++++++--
 hax-lib-macros/src/quote.rs                   | 67 ++++++++++----
 hax-lib-macros/types/src/lib.rs               | 33 +++++++
 tests/attributes/src/lib.rs                   |  9 +-
 7 files changed, 321 insertions(+), 59 deletions(-)

diff --git a/engine/backends/fstar/fstar_backend.ml b/engine/backends/fstar/fstar_backend.ml
index a92600b16..8244e2be6 100644
--- a/engine/backends/fstar/fstar_backend.ml
+++ b/engine/backends/fstar/fstar_backend.ml
@@ -795,7 +795,12 @@ struct
         F.mk_e_app effect (if is_lemma then args else typ :: args)
 
   let rec pitem (e : item) :
-      [> `Impl of F.AST.decl | `Intf of F.AST.decl | `Comment of string ] list =
+      [> `Impl of F.AST.decl
+      | `Intf of F.AST.decl
+      | `VerbatimImpl of string
+      | `VerbatimIntf of string
+      | `Comment of string ]
+      list =
     try pitem_unwrapped e
     with Diagnostics.SpanFreeError.Exn error ->
       let error = Diagnostics.SpanFreeError.payload error in
@@ -807,7 +812,12 @@ struct
       ]
 
   and pitem_unwrapped (e : item) :
-      [> `Impl of F.AST.decl | `Intf of F.AST.decl | `Comment of string ] list =
+      [> `Impl of F.AST.decl
+      | `Intf of F.AST.decl
+      | `VerbatimImpl of string
+      | `VerbatimIntf of string
+      | `Comment of string ]
+      list =
     match e.v with
     | Alias { name; item } ->
         let pat =
@@ -1250,6 +1260,18 @@ struct
         let tcinst = F.term @@ F.AST.Var FStar_Parser_Const.tcinstance_lid in
         F.decls ~fsti:ctx.interface_mode ~attrs:[ tcinst ]
         @@ F.AST.TopLevelLet (NoLetQualifier, [ (pat, body) ])
+    | Quote quote ->
+        let fstar_opts =
+          Attrs.find_unique_attr e.attrs ~f:(function
+            | ItemQuote q -> Some q.fstar_options
+            | _ -> None)
+          |> Option.value_or_thunk ~default:(fun _ ->
+                 Error.assertion_failure e.span
+                   "Malformed `Quote` item: could not find a ItemQuote payload")
+          |> Option.value ~default:Types.{ intf = true; impl = false }
+        in
+        (if fstar_opts.intf then [ `VerbatimIntf (pquote quote) ] else [])
+        @ if fstar_opts.impl then [ `VerbatimImpl (pquote quote) ] else []
     | HaxError details ->
         [
           `Comment
@@ -1263,7 +1285,12 @@ end
 module type S = sig
   val pitem :
     item ->
-    [> `Impl of F.AST.decl | `Intf of F.AST.decl | `Comment of string ] list
+    [> `Impl of F.AST.decl
+    | `Intf of F.AST.decl
+    | `VerbatimImpl of string
+    | `VerbatimIntf of string
+    | `Comment of string ]
+    list
 end
 
 let make (module M : Attrs.WITH_ITEMS) ctx =
@@ -1313,6 +1340,8 @@ let strings_of_item ~signature_only (bo : BackendOptions.t) m items
   |> List.concat_map ~f:(function
        | `Impl i -> [ mk_impl (decl_to_string i) ]
        | `Intf i -> [ mk_intf (decl_to_string i) ]
+       | `VerbatimIntf s -> if interface_mode then [ `Intf s ] else [ `Impl s ]
+       | `VerbatimImpl s -> if interface_mode then [ `Impl s ] else [ `Impl s ]
        | `Comment s ->
            let s = "(* " ^ s ^ " *)" in
            if interface_mode then [ `Impl s; `Intf s ] else [ `Impl s ])
diff --git a/engine/lib/attr_payloads.ml b/engine/lib/attr_payloads.ml
index b2be72b80..36964e184 100644
--- a/engine/lib/attr_payloads.ml
+++ b/engine/lib/attr_payloads.ml
@@ -57,6 +57,7 @@ module AssocRole = struct
       | ProcessWrite
       | ProcessInit
       | ProtocolMessages
+      | ItemQuote
     [@@deriving show, yojson, compare, sexp, eq]
   end
 
@@ -73,6 +74,7 @@ module AssocRole = struct
     | Ensures -> Ensures
     | Decreases -> Decreases
     | Refine -> Refine
+    | ItemQuote -> ItemQuote
     | ProcessRead -> ProcessRead
     | ProcessWrite -> ProcessWrite
     | ProcessInit -> ProcessInit
@@ -137,7 +139,7 @@ module Make (F : Features.T) (Error : Phase_utils.ERROR) = struct
   module type WITH_ITEMS = sig
     val item_uid_map : item UId.Map.t
     val item_of_uid : UId.t -> item
-    val associated_items : attrs -> item AssocRole.Map.t
+    val associated_items_per_roles : attrs -> item list AssocRole.Map.t
     val associated_item : AssocRole.t -> attrs -> item option
 
     val associated_fn :
@@ -146,6 +148,19 @@ module Make (F : Features.T) (Error : Phase_utils.ERROR) = struct
     val associated_expr :
       ?keep_last_args:int -> AssocRole.t -> attrs -> expr option
 
+    val associated_items : AssocRole.t -> attrs -> item list
+
+    val associated_fns :
+      AssocRole.t -> attrs -> (generics * param list * expr) list
+
+    val associated_exprs :
+      ?keep_last_args:int -> AssocRole.t -> attrs -> expr list
+
+    val expect_fn : item -> generics * param list * expr
+
+    val expect_expr :
+      ?keep_last_args:int -> generics * param list * expr -> expr
+
     val associated_expr_rebinding :
       pat list -> AssocRole.t -> attrs -> expr option
     (** Looks up an expression but takes care of rebinding free variables. *)
@@ -201,43 +216,65 @@ module Make (F : Features.T) (Error : Phase_utils.ERROR) = struct
              @@ "Could not find item with UID "
              ^ [%show: UId.t] uid)
 
-    let associated_items : attrs -> item AssocRole.Map.t =
-      let dup role items =
-        let span = List.map ~f:(fun i -> i.span) items |> Span.union_list in
-        Error.assertion_failure span
-        @@ "Cannot associate multiple "
-        ^ [%show: AssocRole.t] role
-      in
+    let associated_items_per_roles : attrs -> item list AssocRole.Map.t =
       raw_associated_item
       >> List.map ~f:(map_snd item_of_uid)
-      >> map_of_alist (module AssocRole) ~dup
+      >> Map.of_alist_multi (module AssocRole)
+
+    let expect_singleton failure = function
+      | [] -> None
+      | [ v ] -> Some v
+      | _ -> failure ()
+    (* Error.assertion_failure span message *)
+
+    let span_of_attrs =
+      List.map ~f:(fun (i : attr) -> i.span) >> Span.union_list
+
+    let find_or_empty role list = Map.find list role |> Option.value ~default:[]
+
+    let associated_items (role : AssocRole.t) (attrs : attrs) : item list =
+      associated_items_per_roles attrs |> find_or_empty role
 
     let associated_item (role : AssocRole.t) (attrs : attrs) : item option =
-      Map.find (associated_items attrs) role
+      associated_items role attrs
+      |> expect_singleton (fun _ ->
+             let span = span_of_attrs attrs in
+             Error.assertion_failure span
+             @@ "Found more than one "
+             ^ [%show: AssocRole.t] role
+             ^ " for this item. Only one is allowed.")
+
+    let expect_fn = function
+      | { v = Fn { generics; params; body; _ }; _ } -> (generics, params, body)
+      | { span; _ } ->
+          Error.assertion_failure span
+            "this associated item was expected to be a `fn` item"
+
+    let expect_expr ?(keep_last_args = 0) (_generics, params, body) =
+      let n =
+        if keep_last_args < 0 then 0 else List.length params - keep_last_args
+      in
+      let params = List.drop params n |> List.map ~f:(fun p -> p.pat) in
+      match params with
+      | [] -> body
+      | _ -> { body with e = Closure { params; body; captures = [] } }
 
     let associated_fn (role : AssocRole.t) :
         attrs -> (generics * param list * expr) option =
-      associated_item role
-      >> Option.map ~f:(function
-           | { v = Fn { generics; params; body; _ }; _ } ->
-               (generics, params, body)
-           | { span; _ } ->
-               Error.assertion_failure span
-                 "this associated item was expected to be a `fn` item")
+      associated_item role >> Option.map ~f:expect_fn
+
+    let associated_fns (role : AssocRole.t) :
+        attrs -> (generics * param list * expr) list =
+      associated_items role >> List.map ~f:expect_fn
 
     (** Looks up an associated expression, optionally keeping `keep_last_args` last arguments. If keep_last_args is negative, then all arguments are kept. *)
     let associated_expr ?(keep_last_args = 0) (role : AssocRole.t) :
         attrs -> expr option =
-      associated_fn role
-      >> Option.map ~f:(fun (_generics, params, body) ->
-             let n =
-               if keep_last_args < 0 then 0
-               else List.length params - keep_last_args
-             in
-             let params = List.drop params n |> List.map ~f:(fun p -> p.pat) in
-             match params with
-             | [] -> body
-             | _ -> { body with e = Closure { params; body; captures = [] } })
+      associated_fn role >> Option.map ~f:(expect_expr ~keep_last_args)
+
+    let associated_exprs ?(keep_last_args = 0) (role : AssocRole.t) :
+        attrs -> expr list =
+      associated_fns role >> List.map ~f:(expect_expr ~keep_last_args)
 
     let associated_expr_rebinding (params : pat list) (role : AssocRole.t)
         (attrs : attrs) : expr option =
diff --git a/engine/lib/phases/phase_transform_hax_lib_inline.ml b/engine/lib/phases/phase_transform_hax_lib_inline.ml
index b8ee6f948..6aa6e657b 100644
--- a/engine/lib/phases/phase_transform_hax_lib_inline.ml
+++ b/engine/lib/phases/phase_transform_hax_lib_inline.ml
@@ -22,6 +22,7 @@ module%inlined_contents Make (F : Features.T) = struct
     module UA = Ast_utils.Make (F)
     module UB = Ast_utils.Make (FB)
     module Visitors = Ast_visitors.Make (FB)
+    module Attrs = Attr_payloads.Make (F) (Error)
 
     module S = struct
       module A = FA
@@ -69,6 +70,14 @@ module%inlined_contents Make (F : Features.T) = struct
       UB.Reducers.collect_global_idents#visit_pat () pat |> Set.choose
 
     let rec dexpr' span (expr : A.expr') : B.expr' =
+      quote_of_expr' span expr
+      |> Option.map ~f:(fun quote : B.expr' -> B.Quote quote)
+      |> Option.value_or_thunk ~default:(fun _ ->
+             [%inline_body dexpr'] span expr)
+
+    and quote_of_expr (expr : A.expr) = quote_of_expr' expr.span expr.e
+
+    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 ->
@@ -122,11 +131,56 @@ module%inlined_contents Make (F : Features.T) = struct
             in
             f verbatim code
           in
-          Quote { contents; witness = Features.On.quote }
-      | [%inline_arms "dexpr'.*"] -> auto
+          Some { contents; witness = Features.On.quote }
+      | _ -> None
       [@@inline_ands bindings_of dexpr - dexpr']
 
-    [%%inline_defs "Item.*"]
+    [%%inline_defs "Item.*" - ditems]
+
+    let ditems items =
+      let (module Attrs) = Attrs.with_items items in
+      let f (item : A.item) =
+        let before, after =
+          let map_fst = List.map ~f:fst in
+          try
+            Attrs.associated_items Attr_payloads.AssocRole.ItemQuote item.attrs
+            |> List.map ~f:(fun assoc_item ->
+                   let e : A.expr =
+                     assoc_item |> Attrs.expect_fn |> Attrs.expect_expr
+                   in
+                   let quote =
+                     UA.Expect.block e |> Option.value ~default:e
+                     |> quote_of_expr
+                     |> Option.value_or_thunk ~default:(fun _ ->
+                            Error.assertion_failure assoc_item.span
+                            @@ "Malformed `Quote` item: `quote_of_expr` \
+                                failed. Expression was:\n"
+                            (* ^ (UA.LiftToFullAst.expr e |> Print_rust.pexpr_str) *)
+                            ^ [%show: A.expr] e)
+                   in
+                   let v : B.item' = Quote quote in
+                   let span = e.span in
+                   let position, attr =
+                     Attrs.find_unique_attr assoc_item.attrs ~f:(function
+                       | ItemQuote q as attr -> Some (q.position, attr)
+                       | _ -> None)
+                     |> Option.value_or_thunk ~default:(fun _ ->
+                            Error.assertion_failure assoc_item.span
+                              "Malformed `Quote` item: could not find a \
+                               ItemQuote payload")
+                   in
+                   let attrs = [ Attr_payloads.to_attr attr assoc_item.span ] in
+                   (B.{ v; span; ident = item.ident; attrs }, position))
+            |> List.partition_tf ~f:(snd >> [%matches? Types.Before])
+            |> map_fst *** map_fst
+          with Diagnostics.SpanFreeError.Exn (Data (context, kind)) ->
+            let error = Diagnostics.pretty_print_context_kind context kind in
+            let msg = error in
+            ([ B.make_hax_error_item item.span item.ident msg ], [])
+        in
+        before @ ditem item @ after
+      in
+      List.concat_map ~f items
   end
 
   include Implem
diff --git a/hax-lib-macros/src/lib.rs b/hax-lib-macros/src/lib.rs
index 4e4ad3611..23c732eaf 100644
--- a/hax-lib-macros/src/lib.rs
+++ b/hax-lib-macros/src/lib.rs
@@ -541,8 +541,63 @@ pub fn pv_handwritten(_attr: pm::TokenStream, item: pm::TokenStream) -> pm::Toke
     quote! {#attr #item}.into()
 }
 
+macro_rules! make_quoting_item_proc_macro {
+    ($backend:ident, $macro_name:ident, $position:expr, $cfg_name:ident) => {
+        #[doc = concat!("This macro inlines verbatim ", stringify!($backend)," code before a Rust item.")]
+        ///
+        /// This macro takes a string literal containing backend
+        /// code. Just as backend expression macros, this literal can
+        /// contains dollar-prefixed Rust names.
+        ///
+        /// Note: when targetting F*, you can prepend a first
+        /// comma-separated argument: `interface`, `impl` or
+        /// `both`. This controls where the code will apprear: in the
+        /// `fst` or `fsti` files or both.
+        #[proc_macro_error]
+        #[proc_macro_attribute]
+        pub fn $macro_name(payload: pm::TokenStream, item: pm::TokenStream) -> pm::TokenStream {
+            let mut fstar_options = None;
+            let item: TokenStream = item.into();
+            // panic!("{itemp:?}");
+            let payload = {
+                let mut tokens = payload.into_iter().peekable();
+                if let Some(pm::TokenTree::Ident(ident)) = tokens.peek() {
+                    let ident_str = format!("{}", ident);
+                    fstar_options = Some(ItemQuoteFStarOpts {
+                        intf: ident_str == "interface" || ident_str == "both",
+                        r#impl: ident_str == "impl" || ident_str == "both",
+                    });
+                    if !matches!(ident_str.as_str(), "impl" | "both" | "interface") {
+                        proc_macro_error::abort!(
+                            ident.span(),
+                            "Expected `impl`, `both` or `interface`"
+                        );
+                    }
+                    // Consume the ident
+                    let _ = tokens.next();
+                    // Expect a comma, fail otherwise
+                    let comma = pm::TokenStream::from_iter(tokens.next().into_iter());
+                    let _: syn::token::Comma = parse_macro_input!(comma);
+                }
+                pm::TokenStream::from_iter(tokens)
+            };
+
+            let ts: TokenStream = quote::item(
+                ItemQuote {
+                    position: $position,
+                    fstar_options,
+                },
+                quote! {#[cfg($cfg_name)]},
+                payload,
+                quote! {#item}.into(),
+            )
+            .into();
+            ts.into()
+        }
+    };
+}
 macro_rules! make_quoting_proc_macro {
-    ($backend:ident($cfg_name:ident)) => {
+    ($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.")]
         ///
 
@@ -572,10 +627,9 @@ macro_rules! make_quoting_proc_macro {
         /// syntax, where `SYNTAX` is a Rust pattern. The syntax
         /// `${EXPR}` also allows any Rust expressions
         /// `EXPR` to be embedded.
-
         #[proc_macro]
-        pub fn $backend(payload: pm::TokenStream) -> pm::TokenStream {
-            let ts: TokenStream = quote::quote(payload).into();
+        pub fn $expr_name(payload: pm::TokenStream) -> pm::TokenStream {
+            let ts: TokenStream = quote::expression(payload).into();
             quote!{
                 #[cfg($cfg_name)]
                 {
@@ -583,13 +637,26 @@ macro_rules! make_quoting_proc_macro {
                 }
             }.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);
+
+        #[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: false });
+            $before_name(payload, quote!{#attr #item}.into())
+        }
     };
-    ($backend:ident($cfg_name:ident) $($others:tt)+) => {
-        make_quoting_proc_macro!($backend($cfg_name));
+    ($backend:ident $payload:tt $($others:tt)+) => {
+        make_quoting_proc_macro!($backend$payload);
         make_quoting_proc_macro!($($others)+);
     }
 }
 
-make_quoting_proc_macro!(fstar(hax_backend_fstar)
-                         coq(hax_backend_coq)
-                         proverif(hax_backend_proverif));
+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));
diff --git a/hax-lib-macros/src/quote.rs b/hax-lib-macros/src/quote.rs
index 7ccf70c9d..8373b97a7 100644
--- a/hax-lib-macros/src/quote.rs
+++ b/hax-lib-macros/src/quote.rs
@@ -124,29 +124,64 @@ fn process_string(s: &str) -> std::result::Result<(String, Vec<Antiquote>), Stri
     Ok((output, antiquotations))
 }
 
-pub(super) fn quote(payload: pm::TokenStream) -> pm::TokenStream {
-    let payload = parse_macro_input!(payload as LitStr).value();
-
-    if payload.find(SPLIT_MARK).is_some() {
-        return quote! {std::compile_error!(std::concat!($SPLIT_MARK, " is reserved"))}.into();
+pub(super) fn item(
+    kind: ItemQuote,
+    attribute_to_inject: TokenStream,
+    payload: pm::TokenStream,
+    item: pm::TokenStream,
+) -> pm::TokenStream {
+    let expr = TokenStream::from(expression(payload));
+    let item = TokenStream::from(item);
+    let uid = ItemUid::fresh();
+    let uid_attr = AttrPayload::Uid(uid.clone());
+    let assoc_attr = AttrPayload::AssociatedItem {
+        role: AssociationRole::ItemQuote,
+        item: uid,
+    };
+    let kind_attr = AttrPayload::ItemQuote(kind);
+    let status_attr = AttrPayload::ItemStatus(ItemStatus::Included { late_skip: true });
+    use AttrPayload::NeverDropBody;
+    quote! {
+        #assoc_attr
+        #item
+        #attribute_to_inject
+        const _: () = {
+            #NeverDropBody
+            #uid_attr
+            #status_attr
+            #kind_attr
+            fn quote_contents() {
+                #expr
+            }
+        };
     }
+    .into()
+}
 
-    let (string, antiquotes) = match process_string(&payload) {
-        Ok(x) => x,
-        Err(message) => return quote! {std::compile_error!(#message)}.into(),
+pub(super) fn expression(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() {
+            return quote! {std::compile_error!(std::concat!($SPLIT_MARK, " is reserved"))}.into();
+        }
+        let (string, antiquotes) = match process_string(&payload) {
+            Ok(x) => x,
+            Err(message) => return quote! {std::compile_error!(#message)}.into(),
+        };
+        let string = proc_macro2::Literal::string(&string);
+        let string: TokenStream = [proc_macro2::TokenTree::Literal(string)]
+            .into_iter()
+            .collect();
+        (quote! {#string}, antiquotes)
     };
-    let string = proc_macro2::Literal::string(&string);
-    let string: TokenStream = [proc_macro2::TokenTree::Literal(string)]
-        .into_iter()
-        .collect();
-    let mut code = quote! {#string};
+
     for user in antiquotes.iter().rev() {
         let kind = &user.kind;
-        code = quote! {
+        backend_code = quote! {
             let #kind = #user;
-            #code
+            #backend_code
         };
     }
 
-    quote! {hax_lib::inline(#[allow(unused_variables)]{#code})}.into()
+    quote! {hax_lib::inline(#[allow(unused_variables)]{#backend_code})}.into()
 }
diff --git a/hax-lib-macros/types/src/lib.rs b/hax-lib-macros/types/src/lib.rs
index aa5fee516..20ccc3723 100644
--- a/hax-lib-macros/types/src/lib.rs
+++ b/hax-lib-macros/types/src/lib.rs
@@ -52,12 +52,43 @@ pub enum AssociationRole {
     Ensures,
     Decreases,
     Refine,
+    /// A quoted piece of backend code to place after or before the
+    /// extraction of the marked item
+    ItemQuote,
     ProcessRead,
     ProcessWrite,
     ProcessInit,
     ProtocolMessages,
 }
 
+#[derive(Debug, Copy, Clone, Serialize, Deserialize)]
+#[cfg_attr(feature = "schemars", derive(schemars::JsonSchema))]
+#[serde(rename = "HaItemQuotePosition")]
+pub enum ItemQuotePosition {
+    /// Should appear just before the item in the extraction
+    Before,
+    /// Should appear right after the item in the extraction
+    After,
+}
+
+#[derive(Debug, Copy, Clone, Serialize, Deserialize)]
+#[cfg_attr(feature = "schemars", derive(schemars::JsonSchema))]
+#[serde(rename = "HaItemQuoteFStarOpts")]
+pub struct ItemQuoteFStarOpts {
+    /// Shall we output this in F* interfaces (`*.fsti` files)?
+    pub intf: bool,
+    /// Shall we output this in F* implementations (`*.fst` files)?
+    pub r#impl: bool,
+}
+
+#[derive(Debug, Copy, Clone, Serialize, Deserialize)]
+#[cfg_attr(feature = "schemars", derive(schemars::JsonSchema))]
+#[serde(rename = "HaItemQuote")]
+pub struct ItemQuote {
+    pub position: ItemQuotePosition,
+    pub fstar_options: Option<ItemQuoteFStarOpts>,
+}
+
 /// Hax only understands one attribute: `#[hax::json(PAYLOAD)]` where
 /// `PAYLOAD` is a JSON serialization of an inhabitant of
 /// `AttrPayload`.
@@ -71,6 +102,8 @@ pub enum AttrPayload {
         item: ItemUid,
     },
     Uid(ItemUid),
+    /// Decides of the position of a item quote
+    ItemQuote(ItemQuote),
     /// Mark an item so that hax never drop its body (this is useful
     /// for pre- and post- conditions of a function we dropped the
     /// body of: pre and post are part of type signature)
diff --git a/tests/attributes/src/lib.rs b/tests/attributes/src/lib.rs
index 7c8dfdf4b..76e16c69c 100644
--- a/tests/attributes/src/lib.rs
+++ b/tests/attributes/src/lib.rs
@@ -124,13 +124,20 @@ mod newtype_pattern {
     }
 }
 
+#[hax::fstar_before(r#"let before_${inlined_code} = "example before""#)]
+#[hax::fstar_after(r#"let ${inlined_code}_after = "example after""#)]
 fn inlined_code(foo: Foo) {
     const V: u8 = 12;
     let v_a = 13;
-    hax::fstar!(
+    hax::fstar_expr!(
         r"let x = ${foo.x} in
           let $?{Foo {y, ..}} = $foo in
           $add3 ((fun _ -> 3ul) $foo) $v_a $V y
         "
     );
 }
+
+#[hax::fstar_replace(r#"unfold let $some_function = "hello from F*""#)]
+fn some_function() -> String {
+    String::from("hello from Rust")
+}

From e387b78e7a9992be680b4eb66379faa1b7043f57 Mon Sep 17 00:00:00 2001
From: Lucas Franceschino <lucas@cryspen.com>
Date: Mon, 22 Apr 2024 18:12:15 +0200
Subject: [PATCH 07/21] fix(engine): do not propagate certain parent attributes

---
 engine/lib/import_thir.ml                           | 13 ++++++++++++-
 hax-lib-macros/src/lib.rs                           |  2 +-
 hax-lib-macros/src/quote.rs                         |  2 +-
 .../snapshots/toolchain__attributes into-fstar.snap | 10 ++++++++++
 tests/attributes/src/lib.rs                         |  2 +-
 5 files changed, 25 insertions(+), 4 deletions(-)

diff --git a/engine/lib/import_thir.ml b/engine/lib/import_thir.ml
index 30ef7c73d..f686fa127 100644
--- a/engine/lib/import_thir.ml
+++ b/engine/lib/import_thir.ml
@@ -123,7 +123,18 @@ let c_attrs : Thir.attribute list -> attrs = List.map ~f:c_attr
 let c_item_attrs (attrs : Thir.item_attributes) : attrs =
   (* TODO: This is a quite coarse approximation, we need to reflect
      that parent/self structure in our AST. *)
-  c_attrs (attrs.attributes @ attrs.parent_attributes)
+  let self = c_attrs attrs.attributes in
+  let parent = c_attrs attrs.parent_attributes in
+  let parent =
+    (* Repeating associateditem or uid is harmful *)
+    List.filter
+      ~f:(fun payload ->
+        match Attr_payloads.payloads [ payload ] with
+        | [ ((Uid _ | AssociatedItem _), _) ] -> false
+        | _ -> true)
+      parent
+  in
+  self @ parent
 
 type extended_literal =
   | EL_Lit of literal
diff --git a/hax-lib-macros/src/lib.rs b/hax-lib-macros/src/lib.rs
index 23c732eaf..dacb12970 100644
--- a/hax-lib-macros/src/lib.rs
+++ b/hax-lib-macros/src/lib.rs
@@ -647,7 +647,7 @@ macro_rules! make_quoting_proc_macro {
         #[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: false });
+            let attr = AttrPayload::ItemStatus(ItemStatus::Included { late_skip: true });
             $before_name(payload, quote!{#attr #item}.into())
         }
     };
diff --git a/hax-lib-macros/src/quote.rs b/hax-lib-macros/src/quote.rs
index 8373b97a7..1bfd99141 100644
--- a/hax-lib-macros/src/quote.rs
+++ b/hax-lib-macros/src/quote.rs
@@ -145,10 +145,10 @@ pub(super) fn item(
         #assoc_attr
         #item
         #attribute_to_inject
+        #status_attr
         const _: () = {
             #NeverDropBody
             #uid_attr
-            #status_attr
             #kind_attr
             fn quote_contents() {
                 #expr
diff --git a/test-harness/src/snapshots/toolchain__attributes into-fstar.snap b/test-harness/src/snapshots/toolchain__attributes into-fstar.snap
index 98d940c6e..a2ec35662 100644
--- a/test-harness/src/snapshots/toolchain__attributes into-fstar.snap	
+++ b/test-harness/src/snapshots/toolchain__attributes into-fstar.snap	
@@ -129,10 +129,16 @@ let add3_lemma (x: u32)
         x <=. 10ul || x >=. (u32_max /! 3ul <: u32) || (add3 x x x <: u32) =. (x *! 3ul <: u32)) =
   ()
 
+let before_inlined_code = "example before"
+
 let inlined_code__V: u8 = 12uy
 
+let inlined_code_after = "example after"
+
 let u32_max: u32 = 90000ul
 
+unfold let some_function _ = "hello from F*"
+
 let add3 (x y z: u32)
     : Prims.Pure u32
       (requires x >. 10ul && y >. 10ul && z >. 10ul && ((x +! y <: u32) +! z <: u32) <. u32_max)
@@ -150,6 +156,8 @@ type t_Foo = {
   f_z:f_z: u32{((f_y +! f_x <: u32) +! f_z <: u32) >. 3ul}
 }
 
+let before_inlined_code = "example before"
+
 let inlined_code (foo: t_Foo) : Prims.unit =
   let vv_a:i32 = 13l in
   let _:Prims.unit =
@@ -158,4 +166,6 @@ let inlined_code (foo: t_Foo) : Prims.unit =
     add3 ((fun _ -> 3ul) foo) vv_a inlined_code__V y
   in
   ()
+
+let inlined_code_after = "example after"
 '''
diff --git a/tests/attributes/src/lib.rs b/tests/attributes/src/lib.rs
index 76e16c69c..b3e788ea7 100644
--- a/tests/attributes/src/lib.rs
+++ b/tests/attributes/src/lib.rs
@@ -137,7 +137,7 @@ fn inlined_code(foo: Foo) {
     );
 }
 
-#[hax::fstar_replace(r#"unfold let $some_function = "hello from F*""#)]
+#[hax::fstar_replace(r#"unfold let $some_function _ = "hello from F*""#)]
 fn some_function() -> String {
     String::from("hello from Rust")
 }

From ff43ce158ab46fd7e0250e8ad065ece47c64e27c Mon Sep 17 00:00:00 2001
From: Lucas Franceschino <lucas@cryspen.com>
Date: Mon, 22 Apr 2024 18:13:15 +0200
Subject: [PATCH 08/21] fix(engine): refresh tests

---
 hax-lib-macros/src/lib.rs                                     | 1 -
 .../src/snapshots/toolchain__attributes into-fstar.snap       | 4 ----
 2 files changed, 5 deletions(-)

diff --git a/hax-lib-macros/src/lib.rs b/hax-lib-macros/src/lib.rs
index dacb12970..fe840799d 100644
--- a/hax-lib-macros/src/lib.rs
+++ b/hax-lib-macros/src/lib.rs
@@ -638,7 +638,6 @@ macro_rules! make_quoting_proc_macro {
             }.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);
 
diff --git a/test-harness/src/snapshots/toolchain__attributes into-fstar.snap b/test-harness/src/snapshots/toolchain__attributes into-fstar.snap
index a2ec35662..6495687f0 100644
--- a/test-harness/src/snapshots/toolchain__attributes into-fstar.snap	
+++ b/test-harness/src/snapshots/toolchain__attributes into-fstar.snap	
@@ -129,12 +129,8 @@ let add3_lemma (x: u32)
         x <=. 10ul || x >=. (u32_max /! 3ul <: u32) || (add3 x x x <: u32) =. (x *! 3ul <: u32)) =
   ()
 
-let before_inlined_code = "example before"
-
 let inlined_code__V: u8 = 12uy
 
-let inlined_code_after = "example after"
-
 let u32_max: u32 = 90000ul
 
 unfold let some_function _ = "hello from F*"

From a75fbbf7ea11f32748551165598e73d3d18b6484 Mon Sep 17 00:00:00 2001
From: Lucas Franceschino <lucas@cryspen.com>
Date: Mon, 22 Apr 2024 18:46:37 +0200
Subject: [PATCH 09/21] fix(examples): `fstar!` -> `fstar_expr!`

---
 examples/barrett/src/lib.rs        | 2 +-
 examples/kyber_compress/src/lib.rs | 8 ++++----
 2 files changed, 5 insertions(+), 5 deletions(-)

diff --git a/examples/barrett/src/lib.rs b/examples/barrett/src/lib.rs
index b5bc7d40e..6317978ed 100644
--- a/examples/barrett/src/lib.rs
+++ b/examples/barrett/src/lib.rs
@@ -38,7 +38,7 @@ pub fn barrett_reduce(value: FieldElement) -> FieldElement {
     // assert!(((quotient as i64) * (FIELD_MODULUS as i64)) < 9223372036854775807);
     let sub = quotient * FIELD_MODULUS;
 
-    hax::fstar!(r"Math.Lemmas.cancel_mul_mod (v $quotient) 3329");
+    hax::fstar_expr!(r"Math.Lemmas.cancel_mul_mod (v $quotient) 3329");
 
     value - sub
 }
diff --git a/examples/kyber_compress/src/lib.rs b/examples/kyber_compress/src/lib.rs
index 71d2d3fc4..11eb50279 100644
--- a/examples/kyber_compress/src/lib.rs
+++ b/examples/kyber_compress/src/lib.rs
@@ -1,4 +1,4 @@
-use hax_lib::{ensures, fstar, requires};
+use hax_lib::{ensures, fstar_expr, requires};
 
 const FIELD_MODULUS: i32 = 3329;
 const UNSIGNED_FIELD_MODULUS: u32 = FIELD_MODULUS as u32;
@@ -8,7 +8,7 @@ const UNSIGNED_FIELD_MODULUS: u32 = FIELD_MODULUS as u32;
 fn get_n_least_significant_bits(n: u8, value: u32) -> u32 {
     let nth_bit = 1 << n;
     let mask = nth_bit - 1;
-    fstar!("Rust_primitives.Integers.logand_mask_lemma $value (v $n)");
+    fstar_expr!("Rust_primitives.Integers.logand_mask_lemma $value (v $n)");
     value & mask
 }
 
@@ -26,7 +26,7 @@ pub fn compress_unsafe(coefficient_bits: u8, fe: u16) -> i32 {
     compressed += UNSIGNED_FIELD_MODULUS;
     compressed /= UNSIGNED_FIELD_MODULUS << 1;
     compressed &= (1 << coefficient_bits) - 1;
-    fstar!("Rust_primitives.Integers.logand_mask_lemma $compressed (v $coefficient_bits)");
+    fstar_expr!("Rust_primitives.Integers.logand_mask_lemma $compressed (v $coefficient_bits)");
     get_n_least_significant_bits(coefficient_bits, compressed) as i32
 }
 
@@ -45,7 +45,7 @@ pub fn compress(coefficient_bits: u8, fe: u16) -> i32 {
     compressed *= 10_321_340;
     compressed >>= 35;
     compressed &= (1 << coefficient_bits) - 1;
-    fstar!("Rust_primitives.Integers.logand_mask_lemma $compressed (v $coefficient_bits)");
+    fstar_expr!("Rust_primitives.Integers.logand_mask_lemma $compressed (v $coefficient_bits)");
     let compressed = compressed as u32;
     get_n_least_significant_bits(coefficient_bits, compressed) as i32
 }

From 85712d7a803e521ab22719168883ccc43c18ae60 Mon Sep 17 00:00:00 2001
From: Lucas Franceschino <lucas@cryspen.com>
Date: Tue, 23 Apr 2024 08:44:24 +0200
Subject: [PATCH 10/21] fix(cli): `--help` formatting

---
 cli/options/src/lib.rs | 17 +++++++++--------
 1 file changed, 9 insertions(+), 8 deletions(-)

diff --git a/cli/options/src/lib.rs b/cli/options/src/lib.rs
index 0cfbf01ce..c50fdc8c8 100644
--- a/cli/options/src/lib.rs
+++ b/cli/options/src/lib.rs
@@ -259,10 +259,11 @@ pub struct TranslationOptions {
     /// prefixed by modifiers are processed from left to right,
     /// excluding or including items. Each pattern selects a number of
     /// item. The modifiers are:
-    ///
-    ///  - `+`: includes the selected items with their dependencies,
-    /// transitively (e.g. if function `f` calls `g` which in turn
-    /// calls `h`, then `+k::f` includes `f`, `g` and `h`)
+
+    /// {n}{n} - `+`: includes the selected items with their
+    /// dependencies, transitively (e.g. if function `f` calls `g`
+    /// which in turn calls `h`, then `+k::f` includes `f`, `g` and
+    /// `h`)
 
     /// {n} - `+~`: includes the selected items with their direct
     /// dependencies only (following the previous example, `+~k::f`
@@ -299,15 +300,15 @@ pub struct BackendOptions {
     /// Enable engine debugging: dumps the AST at each phase.
     ///
     /// The value of `<DEBUG_ENGINE>` can be either:
-    ///
-    ///  - `interactive` (or `i`): enables debugging of the engine,
+
+    /// {n}{n} - `interactive` (or `i`): enables debugging of the engine,
     /// and visualize interactively in a webapp how a crate was
     /// transformed by each phase, both in Rust-like syntax and
     /// browsing directly the internal AST. By default, the webapp is
     /// hosted on `http://localhost:8000`, the port can be override by
     /// setting the `HAX_DEBUGGER_PORT` environment variable.
-    ///
-    /// - `<FILE>` or `file:<FILE>`: outputs the different AST as JSON
+
+    /// {n} - `<FILE>` or `file:<FILE>`: outputs the different AST as JSON
     /// to `<FILE>`. `<FILE>` can be either [-] or a path.
     #[arg(short, long = "debug-engine")]
     pub debug_engine: Option<DebugEngineMode>,

From 815fd46c210b3d3d70048411778977f072c0f8c0 Mon Sep 17 00:00:00 2001
From: Lucas Franceschino <lucas@cryspen.com>
Date: Tue, 23 Apr 2024 11:07:01 +0200
Subject: [PATCH 11/21] chore: link issue

---
 engine/lib/import_thir.ml | 3 ++-
 1 file changed, 2 insertions(+), 1 deletion(-)

diff --git a/engine/lib/import_thir.ml b/engine/lib/import_thir.ml
index f686fa127..e76fd7eaa 100644
--- a/engine/lib/import_thir.ml
+++ b/engine/lib/import_thir.ml
@@ -122,7 +122,8 @@ let c_attrs : Thir.attribute list -> attrs = List.map ~f:c_attr
 
 let c_item_attrs (attrs : Thir.item_attributes) : attrs =
   (* TODO: This is a quite coarse approximation, we need to reflect
-     that parent/self structure in our AST. *)
+     that parent/self structure in our AST. See
+     https://github.com/hacspec/hax/issues/123. *)
   let self = c_attrs attrs.attributes in
   let parent = c_attrs attrs.parent_attributes in
   let parent =

From 374e7ce04a15fa6bd52cc7d5fe6282168083ee3e Mon Sep 17 00:00:00 2001
From: Lucas Franceschino <lucas@cryspen.com>
Date: Tue, 23 Apr 2024 11:08:03 +0200
Subject: [PATCH 12/21] fixup: feat: proc macro for inlining items

---
 hax-lib-macros/src/lib.rs | 1 -
 1 file changed, 1 deletion(-)

diff --git a/hax-lib-macros/src/lib.rs b/hax-lib-macros/src/lib.rs
index fe840799d..26efe75f4 100644
--- a/hax-lib-macros/src/lib.rs
+++ b/hax-lib-macros/src/lib.rs
@@ -558,7 +558,6 @@ macro_rules! make_quoting_item_proc_macro {
         pub fn $macro_name(payload: pm::TokenStream, item: pm::TokenStream) -> pm::TokenStream {
             let mut fstar_options = None;
             let item: TokenStream = item.into();
-            // panic!("{itemp:?}");
             let payload = {
                 let mut tokens = payload.into_iter().peekable();
                 if let Some(pm::TokenTree::Ident(ident)) = tokens.peek() {

From 2acfff4dbaf47313ac3dfc48f50f8a0eb0d1450f Mon Sep 17 00:00:00 2001
From: Lucas Franceschino <lucas@cryspen.com>
Date: Tue, 23 Apr 2024 11:12:16 +0200
Subject: [PATCH 13/21] feat(hax-lib-macros): add documentation

---
 hax-lib-macros/types/src/lib.rs | 11 +++++++++++
 1 file changed, 11 insertions(+)

diff --git a/hax-lib-macros/types/src/lib.rs b/hax-lib-macros/types/src/lib.rs
index 20ccc3723..50ada5751 100644
--- a/hax-lib-macros/types/src/lib.rs
+++ b/hax-lib-macros/types/src/lib.rs
@@ -44,6 +44,9 @@ pub enum ItemStatus {
     Excluded { modeled_by: Option<String> },
 }
 
+/// An item can be associated to another one for multiple reasons:
+/// `AssociationRole` capture the nature of the (directed) relation
+/// between two items
 #[derive(Debug, Copy, Clone, Serialize, Deserialize)]
 #[cfg_attr(feature = "schemars", derive(schemars::JsonSchema))]
 #[serde(rename = "HaAssocRole")]
@@ -61,6 +64,7 @@ pub enum AssociationRole {
     ProtocolMessages,
 }
 
+/// Where should a item quote appear?
 #[derive(Debug, Copy, Clone, Serialize, Deserialize)]
 #[cfg_attr(feature = "schemars", derive(schemars::JsonSchema))]
 #[serde(rename = "HaItemQuotePosition")]
@@ -71,6 +75,7 @@ pub enum ItemQuotePosition {
     After,
 }
 
+/// F*-specific options for item quotes
 #[derive(Debug, Copy, Clone, Serialize, Deserialize)]
 #[cfg_attr(feature = "schemars", derive(schemars::JsonSchema))]
 #[serde(rename = "HaItemQuoteFStarOpts")]
@@ -81,6 +86,9 @@ pub struct ItemQuoteFStarOpts {
     pub r#impl: bool,
 }
 
+/// An item quote is a verbatim piece of backend code included in
+/// Rust. [`ItemQuote`] encodes the various options a item quote can
+/// have.
 #[derive(Debug, Copy, Clone, Serialize, Deserialize)]
 #[cfg_attr(feature = "schemars", derive(schemars::JsonSchema))]
 #[serde(rename = "HaItemQuote")]
@@ -97,8 +105,11 @@ pub struct ItemQuote {
 #[serde(rename = "HaPayload")]
 pub enum AttrPayload {
     ItemStatus(ItemStatus),
+    /// Mark an item as associated with another one
     AssociatedItem {
+        /// What is the nature of the association?
         role: AssociationRole,
+        /// What is the identifier of the target item?
         item: ItemUid,
     },
     Uid(ItemUid),

From 942ae0250b75744d3a9d36f2c0ae3cdae5cc5c38 Mon Sep 17 00:00:00 2001
From: Lucas Franceschino <lucas@cryspen.com>
Date: Tue, 23 Apr 2024 11:52:00 +0200
Subject: [PATCH 14/21] feat(engine): quote: support for type antiquotations

---
 engine/backends/fstar/fstar_backend.ml        | 13 ++++++----
 engine/lib/ast.ml                             |  2 +-
 engine/lib/ast_visitors.ml                    | 11 +++++---
 engine/lib/generic_printer/generic_printer.ml |  3 ++-
 .../phases/phase_transform_hax_lib_inline.ml  | 25 ++++++++++++++++---
 engine/lib/subtype.ml                         |  1 +
 hax-lib-macros/src/lib.rs                     |  2 ++
 hax-lib-macros/src/quote.rs                   | 17 ++++++++-----
 8 files changed, 55 insertions(+), 19 deletions(-)

diff --git a/engine/backends/fstar/fstar_backend.ml b/engine/backends/fstar/fstar_backend.ml
index 8244e2be6..f44a16965 100644
--- a/engine/backends/fstar/fstar_backend.ml
+++ b/engine/backends/fstar/fstar_backend.ml
@@ -573,15 +573,16 @@ struct
              kind = UnsupportedMacro { id = [%show: global_ident] macro };
              span = e.span;
            }
-    | Quote quote -> pquote quote |> F.term_of_string
+    | Quote quote -> pquote e.span quote |> F.term_of_string
     | _ -> .
 
-  and pquote { contents; _ } =
+  and pquote span { contents; _ } =
     List.map
       ~f:(function
         | `Verbatim code -> code
         | `Expr e -> pexpr e |> term_to_string
-        | `Pat p -> ppat p |> pat_to_string)
+        | `Pat p -> ppat p |> pat_to_string
+        | `Typ p -> pty span p |> term_to_string)
       contents
     |> String.concat
 
@@ -1270,8 +1271,10 @@ struct
                    "Malformed `Quote` item: could not find a ItemQuote payload")
           |> Option.value ~default:Types.{ intf = true; impl = false }
         in
-        (if fstar_opts.intf then [ `VerbatimIntf (pquote quote) ] else [])
-        @ if fstar_opts.impl then [ `VerbatimImpl (pquote quote) ] else []
+        (if fstar_opts.intf then [ `VerbatimIntf (pquote e.span quote) ]
+        else [])
+        @
+        if fstar_opts.impl then [ `VerbatimImpl (pquote e.span quote) ] else []
     | HaxError details ->
         [
           `Comment
diff --git a/engine/lib/ast.ml b/engine/lib/ast.ml
index e00ebbe21..b686c9dcc 100644
--- a/engine/lib/ast.ml
+++ b/engine/lib/ast.ml
@@ -265,7 +265,7 @@ functor
     and expr = { e : expr'; span : span; typ : ty }
 
     and quote = {
-      contents : [ `Verbatim of string | `Expr of expr | `Pat of pat ] list;
+      contents : [ `Verbatim of string | `Expr of expr | `Pat of pat | `Typ of ty ] list;
       witness : F.quote;
     }
 
diff --git a/engine/lib/ast_visitors.ml b/engine/lib/ast_visitors.ml
index c536c9f1e..56dc32317 100644
--- a/engine/lib/ast_visitors.ml
+++ b/engine/lib/ast_visitors.ml
@@ -450,7 +450,8 @@ functor
               (fun env -> function
                 | `Verbatim code -> `Verbatim code
                 | `Expr e -> `Expr (self#visit_expr env e)
-                | `Pat p -> `Pat (self#visit_pat env p))
+                | `Pat p -> `Pat (self#visit_pat env p)
+                | `Typ t -> `Typ (self#visit_ty env t))
               env contents
           in
           let witness = self#visit_feature_quote env witness in
@@ -1489,7 +1490,10 @@ functor
                     (`Expr e, acc)
                 | `Pat p ->
                     let p, acc = self#visit_pat env p in
-                    (`Pat p, acc))
+                    (`Pat p, acc)
+                | `Typ t ->
+                    let t, acc = self#visit_ty env t in
+                    (`Typ t, acc))
               env contents
           in
           let witness, reduce_acc' = self#visit_feature_quote env witness in
@@ -2630,7 +2634,8 @@ functor
               (fun env -> function
                 | `Verbatim code -> self#zero
                 | `Expr e -> self#visit_expr env e
-                | `Pat p -> self#visit_pat env p)
+                | `Pat p -> self#visit_pat env p
+                | `Typ t -> self#visit_ty env t)
               env contents
           in
           let reduce_acc' = self#visit_feature_quote env witness in
diff --git a/engine/lib/generic_printer/generic_printer.ml b/engine/lib/generic_printer/generic_printer.ml
index ff1f6754e..1b33c6d77 100644
--- a/engine/lib/generic_printer/generic_printer.ml
+++ b/engine/lib/generic_printer/generic_printer.ml
@@ -230,7 +230,8 @@ module Make (F : Features.T) (View : Concrete_ident.VIEW_API) = struct
                   ~f:(function
                     | `Verbatim code -> string code
                     | `Expr e -> print#expr_at Expr_Quote e
-                    | `Pat p -> print#pat_at Expr_Quote p)
+                    | `Pat p -> print#pat_at Expr_Quote p
+                    | `Typ p -> print#ty_at Expr_Quote p)
                   contents
                 |> concat
             | App _ | Construct _ -> super#expr' ctx e
diff --git a/engine/lib/phases/phase_transform_hax_lib_inline.ml b/engine/lib/phases/phase_transform_hax_lib_inline.ml
index 6aa6e657b..0d448aa6a 100644
--- a/engine/lib/phases/phase_transform_hax_lib_inline.ml
+++ b/engine/lib/phases/phase_transform_hax_lib_inline.ml
@@ -108,14 +108,30 @@ module%inlined_contents Make (F : Features.T) = struct
                 | Some "_pat" ->
                     let pat = extract_pattern e |> Option.value_exn in
                     `Pat pat
+                | Some "_ty" ->
+                    let typ =
+                      match pat.typ with
+                      | TApp { args = [ GType typ ]; _ } -> typ
+                      | _ ->
+                          Stdio.prerr_endline @@ "-pat->" ^ [%show: B.pat] pat;
+                          Stdio.prerr_endline @@ "-expr->"
+                          ^ [%show: B.expr'] e.e;
+                          Error.assertion_failure span
+                            "Malformed call to 'inline': expected type \
+                             `Option<_>`."
+                    in
+                    `Typ typ
                 | _ -> `Expr e)
           in
           let verbatim = split_str ~on:"SPLIT_QUOTE" str in
           let contents =
             let rec f verbatim
                 (code :
-                  [ `Verbatim of string | `Expr of B.expr | `Pat of B.pat ] list)
-                =
+                  [ `Verbatim of string
+                  | `Expr of B.expr
+                  | `Pat of B.pat
+                  | `Typ of B.ty ]
+                  list) =
               match (verbatim, code) with
               | s :: s', code :: code' -> `Verbatim s :: code :: f s' code'
               | [ s ], [] -> [ `Verbatim s ]
@@ -126,7 +142,10 @@ module%inlined_contents Make (F : Features.T) = struct
                   ^ [%show: string list] verbatim
                   ^ "\ncode="
                   ^ [%show:
-                      [ `Verbatim of string | `Expr of B.expr | `Pat of B.pat ]
+                      [ `Verbatim of string
+                      | `Expr of B.expr
+                      | `Pat of B.pat
+                      | `Typ of B.ty ]
                       list] code
             in
             f verbatim code
diff --git a/engine/lib/subtype.ml b/engine/lib/subtype.ml
index 8a0de5191..e55925237 100644
--- a/engine/lib/subtype.ml
+++ b/engine/lib/subtype.ml
@@ -267,6 +267,7 @@ struct
       | `Verbatim code -> `Verbatim code
       | `Expr e -> `Expr (dexpr e)
       | `Pat p -> `Pat (dpat p)
+      | `Typ p -> `Typ (dty span p)
     in
     { contents = List.map ~f contents; witness = S.quote span witness }
 
diff --git a/hax-lib-macros/src/lib.rs b/hax-lib-macros/src/lib.rs
index 26efe75f4..7d7db3b1d 100644
--- a/hax-lib-macros/src/lib.rs
+++ b/hax-lib-macros/src/lib.rs
@@ -626,6 +626,8 @@ macro_rules! make_quoting_proc_macro {
         /// 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();
diff --git a/hax-lib-macros/src/quote.rs b/hax-lib-macros/src/quote.rs
index 1bfd99141..915238220 100644
--- a/hax-lib-macros/src/quote.rs
+++ b/hax-lib-macros/src/quote.rs
@@ -9,7 +9,8 @@
 //! The `<PREFIX>` describes the kind of the antiquotation:
 //!  - empty prefix, the antiquotation is an expression;
 //!  - `?`, the antiquotation is a pattern;
-//!  - `$`, the antiquotation is a constructor name.
+//!  - `$`, the antiquotation is a constructor name;
+//!  - `:`, the antiquotation is a type.
 
 use crate::prelude::*;
 use quote::ToTokens;
@@ -22,6 +23,7 @@ enum AntiquoteKind {
     Expr,
     Constructor,
     Pat,
+    Ty,
 }
 
 impl ToTokens for AntiquoteKind {
@@ -31,6 +33,7 @@ impl ToTokens for AntiquoteKind {
                 Self::Expr => quote! {_expr},
                 Self::Constructor => quote! {_constructor},
                 Self::Pat => quote! {_pat},
+                Self::Ty => quote! {_ty},
             }]
             .into_iter(),
         )
@@ -55,12 +58,13 @@ impl ToTokens for Antiquote {
             AntiquoteKind::Expr => ts,
             AntiquoteKind::Constructor => wrap_pattern(quote! {#ts {..}}),
             AntiquoteKind::Pat => wrap_pattern(ts),
+            AntiquoteKind::Ty => quote! {None::<#ts>},
         };
         tokens.extend([ts].into_iter())
     }
 }
 
-/// Extract antiquotations (`$[?][$]...`, `$[?][$]{...}`) and parses them.
+/// Extract antiquotations (`$[?][$][:]...`, `$[?][$][:]{...}`) and parses them.
 fn process_string(s: &str) -> std::result::Result<(String, Vec<Antiquote>), String> {
     let mut chars = s.chars().peekable();
     let mut antiquotations = vec![];
@@ -70,10 +74,11 @@ fn process_string(s: &str) -> std::result::Result<(String, Vec<Antiquote>), Stri
             '$' => {
                 let mut s = String::new();
                 let mut kind = AntiquoteKind::Expr;
-                if let Some(prefix) = chars.next_if(|ch| *ch == '?' || *ch == '$') {
+                if let Some(prefix) = chars.next_if(|ch| *ch == '?' || *ch == '$' || *ch == ':') {
                     kind = match prefix {
                         '?' => AntiquoteKind::Pat,
                         '$' => AntiquoteKind::Constructor,
+                        ':' => AntiquoteKind::Ty,
                         _ => unreachable!(),
                     };
                 }
@@ -93,9 +98,9 @@ fn process_string(s: &str) -> std::result::Result<(String, Vec<Antiquote>), Stri
                         s.push(ch);
                     }
                 } else {
-                    while let Some(ch) =
-                        chars.next_if(|ch| !matches!(ch, ' ' | '\t' | '\n' | '(' | '{' | ')'))
-                    {
+                    while let Some(ch) = chars.next_if(|ch| {
+                        !matches!(ch, ' ' | '\t' | '\n' | '(' | '{' | ')' | ';' | '!' | '?')
+                    }) {
                         s.push(ch)
                     }
                 }

From 8c7d7f388623d7b0b8d593140ea3313c27e7ff9a Mon Sep 17 00:00:00 2001
From: Lucas Franceschino <lucas@cryspen.com>
Date: Tue, 23 Apr 2024 11:52:13 +0200
Subject: [PATCH 15/21] feat(engine): quote: add replace example

---
 engine/lib/ast.ml                             |  3 +-
 .../toolchain__attributes into-fstar.snap     | 18 ++++++++++
 tests/attributes/src/lib.rs                   | 33 +++++++++++++++++++
 3 files changed, 53 insertions(+), 1 deletion(-)

diff --git a/engine/lib/ast.ml b/engine/lib/ast.ml
index b686c9dcc..992f83007 100644
--- a/engine/lib/ast.ml
+++ b/engine/lib/ast.ml
@@ -265,7 +265,8 @@ functor
     and expr = { e : expr'; span : span; typ : ty }
 
     and quote = {
-      contents : [ `Verbatim of string | `Expr of expr | `Pat of pat | `Typ of ty ] list;
+      contents :
+        [ `Verbatim of string | `Expr of expr | `Pat of pat | `Typ of ty ] list;
       witness : F.quote;
     }
 
diff --git a/test-harness/src/snapshots/toolchain__attributes into-fstar.snap b/test-harness/src/snapshots/toolchain__attributes into-fstar.snap
index 6495687f0..bfeaf0a6c 100644
--- a/test-harness/src/snapshots/toolchain__attributes into-fstar.snap	
+++ b/test-harness/src/snapshots/toolchain__attributes into-fstar.snap	
@@ -26,6 +26,24 @@ exit = 0
 diagnostics = []
 
 [stdout.files]
+"Attributes.Int_model.fst" = '''
+module Attributes.Int_model
+#set-options "--fuel 0 --ifuel 1 --z3rlimit 15"
+open Core
+open FStar.Mul
+
+unfold type t_Int = int
+
+unfold let add x y = x + y
+
+unfold instance impl: Core.Ops.Arith.t_Sub t_Int t_Int =
+  {
+    f_Output = t_Int;
+    f_sub_pre = (fun (self: t_Int) (other: t_Int) -> true);
+    f_sub_post = (fun (self: t_Int) (other: t_Int) (out: t_Int) -> true);
+    f_sub = fun (self: t_Int) (other: t_Int) -> self + other
+  }
+'''
 "Attributes.Newtype_pattern.fst" = '''
 module Attributes.Newtype_pattern
 #set-options "--fuel 0 --ifuel 1 --z3rlimit 15"
diff --git a/tests/attributes/src/lib.rs b/tests/attributes/src/lib.rs
index b3e788ea7..588223924 100644
--- a/tests/attributes/src/lib.rs
+++ b/tests/attributes/src/lib.rs
@@ -141,3 +141,36 @@ fn inlined_code(foo: Foo) {
 fn some_function() -> String {
     String::from("hello from Rust")
 }
+
+/// An minimal example of a model of math integers for F*
+mod int_model {
+    use super::hax;
+    #[hax::fstar_replace(r#"unfold type $:{Int} = int"#)]
+    #[derive(Copy, Clone)]
+    struct Int(u128);
+
+    #[hax::fstar_replace(r#"unfold let ${add} x y = x + y"#)]
+    fn add(x: Int, y: Int) -> Int {
+        Int(x.0 + y.0)
+    }
+
+    use std::ops::Sub;
+    #[hax::fstar_replace(
+        r#"
+unfold instance impl: Core.Ops.Arith.t_Sub $:Int $:Int =
+  {
+    f_Output = $:Int;
+    f_sub_pre = (fun (self: $:Int) (other: $:Int) -> true);
+    f_sub_post = (fun (self: $:Int) (other: $:Int) (out: $:Int) -> true);
+    f_sub = fun (self: $:Int) (other: $:Int) -> self + other
+  }
+"#
+    )]
+    impl Sub for Int {
+        type Output = Self;
+
+        fn sub(self, other: Self) -> Self::Output {
+            Self(self.0 + other.0)
+        }
+    }
+}

From 8e57230276c38896fcd892ea11eb0eaab81aa709 Mon Sep 17 00:00:00 2001
From: Lucas Franceschino <lucas@cryspen.com>
Date: Tue, 23 Apr 2024 12:19:38 +0200
Subject: [PATCH 16/21] feat(engine): print quotations in generic_printer and
 rust_print

---
 engine/lib/generic_printer/generic_printer.ml | 21 +++++++++++--------
 .../generic_printer/generic_printer_base.ml   |  1 +
 engine/lib/print_rust.ml                      | 16 +++++++++++++-
 3 files changed, 28 insertions(+), 10 deletions(-)

diff --git a/engine/lib/generic_printer/generic_printer.ml b/engine/lib/generic_printer/generic_printer.ml
index 1b33c6d77..1193c8e3a 100644
--- a/engine/lib/generic_printer/generic_printer.ml
+++ b/engine/lib/generic_printer/generic_printer.ml
@@ -225,17 +225,19 @@ module Make (F : Features.T) (View : Concrete_ident.VIEW_API) = struct
                 |> wrap_parens
             | MacroInvokation _ -> print#assertion_failure "MacroInvokation"
             | EffectAction _ -> print#assertion_failure "EffectAction"
-            | Quote { contents; _ } ->
-                List.map
-                  ~f:(function
-                    | `Verbatim code -> string code
-                    | `Expr e -> print#expr_at Expr_Quote e
-                    | `Pat p -> print#pat_at Expr_Quote p
-                    | `Typ p -> print#ty_at Expr_Quote p)
-                  contents
-                |> concat
+            | Quote quote -> print#quote quote
             | App _ | Construct _ -> super#expr' ctx e
 
+        method quote { contents; _ } =
+          List.map
+            ~f:(function
+              | `Verbatim code -> string code
+              | `Expr e -> print#expr_at Expr_Quote e
+              | `Pat p -> print#pat_at Expr_Quote p
+              | `Typ p -> print#ty_at Expr_Quote p)
+            contents
+          |> concat
+
         method expr_monadic_let
             : monad:supported_monads * F.monadic_binding ->
               lhs:pat ->
@@ -396,6 +398,7 @@ module Make (F : Features.T) (View : Concrete_ident.VIEW_API) = struct
               string "fn" ^^ space ^^ print#concrete_ident name ^^ generics
               ^^ params
               ^^ iblock braces (print#expr_at Item_Fn_body body)
+          | Quote quote -> print#quote quote
           | _ -> string "item not implemented"
 
         method generic_param' : generic_param fn =
diff --git a/engine/lib/generic_printer/generic_printer_base.ml b/engine/lib/generic_printer/generic_printer_base.ml
index 0a1e67629..3c55d9430 100644
--- a/engine/lib/generic_printer/generic_printer_base.ml
+++ b/engine/lib/generic_printer/generic_printer_base.ml
@@ -354,6 +354,7 @@ module Make (F : Features.T) = struct
       method arm : arm fn
       method expr : par_state -> expr fn
       method item : item fn
+      method quote : quote fn
       method items : item list fn
     end
 
diff --git a/engine/lib/print_rust.ml b/engine/lib/print_rust.ml
index 369a0b005..68ed18b3e 100644
--- a/engine/lib/print_rust.ml
+++ b/engine/lib/print_rust.ml
@@ -215,6 +215,19 @@ module Raw = struct
     | MResult t -> !"MResult<" & pty span t & !">"
     | MOption -> !"MOption"
 
+  and pquote span quote =
+    let ( ! ) = pure span in
+    !"quote!("
+    & List.map
+        ~f:(function
+          | `Verbatim code -> !code
+          | `Expr e -> pexpr e
+          | `Pat p -> ppat p
+          | `Typ t -> pty span t)
+        quote.contents
+      |> concat ~sep:!""
+    & !")"
+
   and pexpr' (e : expr) =
     let ( ! ) = pure e.span in
     match e.e with
@@ -317,7 +330,7 @@ module Raw = struct
     | Closure { params; body; _ } ->
         let params = List.map ~f:ppat params |> concat ~sep:!"," in
         !"(|" & params & !"| {" & pexpr body & !"})"
-    | Quote _ -> !"quotation!(..)"
+    | Quote quote -> pquote e.span quote
   (* | _ -> "todo!()" *)
 
   and plhs (e : lhs) span =
@@ -522,6 +535,7 @@ module Raw = struct
             & !"{"
             & List.map ~f:pimpl_item items |> concat ~sep:!"\n"
             & !"}"
+        | Quote quote -> pquote e.span quote & !";"
         | _ -> raise NotImplemented
       in
       pattrs e.attrs & pi

From 2d78776488c7d81a1df870c69a788c7b0eb9ddff Mon Sep 17 00:00:00 2001
From: Lucas Franceschino <lucas@cryspen.com>
Date: Tue, 23 Apr 2024 12:21:12 +0200
Subject: [PATCH 17/21] feat(engine/pv): handle item kind `Quote`

---
 engine/backends/proverif/proverif_backend.ml | 1 +
 1 file changed, 1 insertion(+)

diff --git a/engine/backends/proverif/proverif_backend.ml b/engine/backends/proverif/proverif_backend.ml
index 983990ebc..84eb582e1 100644
--- a/engine/backends/proverif/proverif_backend.ml
+++ b/engine/backends/proverif/proverif_backend.ml
@@ -624,6 +624,7 @@ module Make (Options : OPTS) : MAKE = struct
                 ^^ separate_map hardline
                      (fun variant -> fun_and_reduc name variant)
                      variants
+          | Quote quote -> print#quote quote
           | _ -> empty
 
         method! expr_let : lhs:pat -> rhs:expr -> expr fn =

From b70104ccba2ae4bdfee854d00b129f89d903894b Mon Sep 17 00:00:00 2001
From: Lucas Franceschino <lucas@cryspen.com>
Date: Wed, 24 Apr 2024 08:31:54 +0200
Subject: [PATCH 18/21] docs(engine): F* backend: `pquote`

---
 engine/backends/fstar/fstar_backend.ml | 1 +
 1 file changed, 1 insertion(+)

diff --git a/engine/backends/fstar/fstar_backend.ml b/engine/backends/fstar/fstar_backend.ml
index f44a16965..cb365d4e1 100644
--- a/engine/backends/fstar/fstar_backend.ml
+++ b/engine/backends/fstar/fstar_backend.ml
@@ -576,6 +576,7 @@ struct
     | Quote quote -> pquote e.span quote |> F.term_of_string
     | _ -> .
 
+  (** Prints a `quote` to a string *)
   and pquote span { contents; _ } =
     List.map
       ~f:(function

From 87a685d4fe13c7c25040a374034e20baccb78d80 Mon Sep 17 00:00:00 2001
From: Lucas Franceschino <lucas@cryspen.com>
Date: Wed, 24 Apr 2024 14:09:52 +0200
Subject: [PATCH 19/21] kfeat(macros): reorganize namespacing

---
 examples/barrett/src/lib.rs        |  2 +-
 examples/kyber_compress/src/lib.rs |  8 ++++----
 hax-lib-macros/Cargo.toml          |  3 +++
 hax-lib-macros/src/lib.rs          |  2 +-
 hax-lib-macros/src/quote.rs        |  2 +-
 hax-lib/Cargo.toml                 |  6 +++++-
 hax-lib/src/lib.rs                 |  5 +++--
 hax-lib/src/proc_macros.rs         | 32 ++++++++++++++++++++++++++++++
 tests/Cargo.lock                   |  1 -
 tests/attributes/Cargo.toml        |  2 +-
 tests/attributes/src/lib.rs        | 20 +++++++++----------
 11 files changed, 61 insertions(+), 22 deletions(-)
 create mode 100644 hax-lib/src/proc_macros.rs

diff --git a/examples/barrett/src/lib.rs b/examples/barrett/src/lib.rs
index 6317978ed..b5bc7d40e 100644
--- a/examples/barrett/src/lib.rs
+++ b/examples/barrett/src/lib.rs
@@ -38,7 +38,7 @@ pub fn barrett_reduce(value: FieldElement) -> FieldElement {
     // assert!(((quotient as i64) * (FIELD_MODULUS as i64)) < 9223372036854775807);
     let sub = quotient * FIELD_MODULUS;
 
-    hax::fstar_expr!(r"Math.Lemmas.cancel_mul_mod (v $quotient) 3329");
+    hax::fstar!(r"Math.Lemmas.cancel_mul_mod (v $quotient) 3329");
 
     value - sub
 }
diff --git a/examples/kyber_compress/src/lib.rs b/examples/kyber_compress/src/lib.rs
index 11eb50279..71d2d3fc4 100644
--- a/examples/kyber_compress/src/lib.rs
+++ b/examples/kyber_compress/src/lib.rs
@@ -1,4 +1,4 @@
-use hax_lib::{ensures, fstar_expr, requires};
+use hax_lib::{ensures, fstar, requires};
 
 const FIELD_MODULUS: i32 = 3329;
 const UNSIGNED_FIELD_MODULUS: u32 = FIELD_MODULUS as u32;
@@ -8,7 +8,7 @@ const UNSIGNED_FIELD_MODULUS: u32 = FIELD_MODULUS as u32;
 fn get_n_least_significant_bits(n: u8, value: u32) -> u32 {
     let nth_bit = 1 << n;
     let mask = nth_bit - 1;
-    fstar_expr!("Rust_primitives.Integers.logand_mask_lemma $value (v $n)");
+    fstar!("Rust_primitives.Integers.logand_mask_lemma $value (v $n)");
     value & mask
 }
 
@@ -26,7 +26,7 @@ pub fn compress_unsafe(coefficient_bits: u8, fe: u16) -> i32 {
     compressed += UNSIGNED_FIELD_MODULUS;
     compressed /= UNSIGNED_FIELD_MODULUS << 1;
     compressed &= (1 << coefficient_bits) - 1;
-    fstar_expr!("Rust_primitives.Integers.logand_mask_lemma $compressed (v $coefficient_bits)");
+    fstar!("Rust_primitives.Integers.logand_mask_lemma $compressed (v $coefficient_bits)");
     get_n_least_significant_bits(coefficient_bits, compressed) as i32
 }
 
@@ -45,7 +45,7 @@ pub fn compress(coefficient_bits: u8, fe: u16) -> i32 {
     compressed *= 10_321_340;
     compressed >>= 35;
     compressed &= (1 << coefficient_bits) - 1;
-    fstar_expr!("Rust_primitives.Integers.logand_mask_lemma $compressed (v $coefficient_bits)");
+    fstar!("Rust_primitives.Integers.logand_mask_lemma $compressed (v $coefficient_bits)");
     let compressed = compressed as u32;
     get_n_least_significant_bits(coefficient_bits, compressed) as i32
 }
diff --git a/hax-lib-macros/Cargo.toml b/hax-lib-macros/Cargo.toml
index 15ed1c009..06605bd67 100644
--- a/hax-lib-macros/Cargo.toml
+++ b/hax-lib-macros/Cargo.toml
@@ -17,3 +17,6 @@ proc-macro2.workspace = true
 quote.workspace = true
 hax-lib-macros-types.workspace = true
 syn = { version = "2.0", features = ["full", "visit-mut", "extra-traits", "parsing"] }
+
+[dev-dependencies]
+hax-lib = { path = "../hax-lib" }
diff --git a/hax-lib-macros/src/lib.rs b/hax-lib-macros/src/lib.rs
index 7d7db3b1d..b612d5547 100644
--- a/hax-lib-macros/src/lib.rs
+++ b/hax-lib-macros/src/lib.rs
@@ -398,7 +398,7 @@ pub fn attributes(_attr: pm::TokenStream, item: pm::TokenStream) -> pm::TokenStr
                                 let (generics, self_ty) = (&item.generics, &item.self_ty);
                                 let where_clause = &generics.where_clause;
                                 ml.tokens = quote! {#decoration, #generics, #where_clause, #self_ty, #tokens};
-                                ml.path = parse_quote! {::hax_lib_macros::impl_fn_decoration};
+                                ml.path = parse_quote! {::hax_lib::impl_fn_decoration};
                             }
                         }
                     }
diff --git a/hax-lib-macros/src/quote.rs b/hax-lib-macros/src/quote.rs
index 915238220..b06927817 100644
--- a/hax-lib-macros/src/quote.rs
+++ b/hax-lib-macros/src/quote.rs
@@ -188,5 +188,5 @@ pub(super) fn expression(payload: pm::TokenStream) -> pm::TokenStream {
         };
     }
 
-    quote! {hax_lib::inline(#[allow(unused_variables)]{#backend_code})}.into()
+    quote! {::hax_lib::inline(#[allow(unused_variables)]{#backend_code})}.into()
 }
diff --git a/hax-lib/Cargo.toml b/hax-lib/Cargo.toml
index 43de0e731..6c3f803ad 100644
--- a/hax-lib/Cargo.toml
+++ b/hax-lib/Cargo.toml
@@ -12,4 +12,8 @@ description = "Hax-specific helpers for Rust programs"
 # See more keys and their definitions at https://doc.rust-lang.org/cargo/reference/manifest.html
 
 [dependencies]
-hax-lib-macros = {path = "../hax-lib-macros"}
+hax-lib-macros = { path = "../hax-lib-macros", optional = true }
+
+[features]
+default = ["macros"]
+macros = ["dep:hax-lib-macros"]
diff --git a/hax-lib/src/lib.rs b/hax-lib/src/lib.rs
index a9286c7ed..549a3393e 100644
--- a/hax-lib/src/lib.rs
+++ b/hax-lib/src/lib.rs
@@ -15,6 +15,9 @@
 
 #![no_std]
 
+mod proc_macros;
+pub use proc_macros::*;
+
 #[doc(hidden)]
 #[cfg(hax)]
 #[macro_export]
@@ -130,8 +133,6 @@ pub fn implies(lhs: bool, rhs: impl Fn() -> bool) -> bool {
     !lhs || rhs()
 }
 
-pub use hax_lib_macros::*;
-
 /// Dummy function that carries a string to be printed as such in the output language
 #[doc(hidden)]
 pub fn inline(_: &str) {}
diff --git a/hax-lib/src/proc_macros.rs b/hax-lib/src/proc_macros.rs
new file mode 100644
index 000000000..24570f386
--- /dev/null
+++ b/hax-lib/src/proc_macros.rs
@@ -0,0 +1,32 @@
+//! This module re-exports macros from `hax-lib-macros` since a
+//! proc-macro crate cannot export anything but procedural macros.
+
+pub use hax_lib_macros::{
+    attributes, ensures, exclude, impl_fn_decoration, include, lemma, opaque_type, requires,
+};
+
+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, $before_name:ident, $after_name:ident, $replace_name:ident, $cfg_name:ident)) => {
+        pub use hax_lib_macros::$expr_name as $backend;
+
+        #[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;
+        }
+    };
+
+    ($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_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));
diff --git a/tests/Cargo.lock b/tests/Cargo.lock
index aaaf2d857..03661228f 100644
--- a/tests/Cargo.lock
+++ b/tests/Cargo.lock
@@ -40,7 +40,6 @@ name = "attributes"
 version = "0.1.0"
 dependencies = [
  "hax-lib",
- "hax-lib-macros",
  "serde",
 ]
 
diff --git a/tests/attributes/Cargo.toml b/tests/attributes/Cargo.toml
index dfe6b8158..aa2261aa7 100644
--- a/tests/attributes/Cargo.toml
+++ b/tests/attributes/Cargo.toml
@@ -4,7 +4,7 @@ version = "0.1.0"
 edition = "2021"
 
 [dependencies]
-hax-lib-macros = { path = "../../hax-lib-macros" }
+# hax-lib-macros = { path = "../../hax-lib-macros" }
 hax-lib = { path = "../../hax-lib" }
 serde = { version = "1.0", features = ["derive"] }
 
diff --git a/tests/attributes/src/lib.rs b/tests/attributes/src/lib.rs
index 588223924..cab615b18 100644
--- a/tests/attributes/src/lib.rs
+++ b/tests/attributes/src/lib.rs
@@ -1,4 +1,4 @@
-use hax_lib_macros as hax;
+use hax_lib as hax;
 
 // dummy max value
 const u32_max: u32 = 90000;
@@ -64,7 +64,7 @@ mod refined_arithmetic {
 }
 
 mod refined_indexes {
-    use hax_lib_macros as hax;
+    use hax_lib as hax;
     const MAX: usize = 10;
     struct MyArray(pub [u8; MAX]);
 
@@ -95,7 +95,7 @@ mod refined_indexes {
     }
 }
 mod newtype_pattern {
-    use hax_lib_macros as hax;
+    use hax_lib as hax;
 
     const MAX: usize = 10;
     #[hax::attributes]
@@ -124,12 +124,12 @@ mod newtype_pattern {
     }
 }
 
-#[hax::fstar_before(r#"let before_${inlined_code} = "example before""#)]
-#[hax::fstar_after(r#"let ${inlined_code}_after = "example after""#)]
+#[hax::fstar::before(r#"let before_${inlined_code} = "example before""#)]
+#[hax::fstar::after(r#"let ${inlined_code}_after = "example after""#)]
 fn inlined_code(foo: Foo) {
     const V: u8 = 12;
     let v_a = 13;
-    hax::fstar_expr!(
+    hax::fstar!(
         r"let x = ${foo.x} in
           let $?{Foo {y, ..}} = $foo in
           $add3 ((fun _ -> 3ul) $foo) $v_a $V y
@@ -137,7 +137,7 @@ fn inlined_code(foo: Foo) {
     );
 }
 
-#[hax::fstar_replace(r#"unfold let $some_function _ = "hello from F*""#)]
+#[hax::fstar::replace(r#"unfold let $some_function _ = "hello from F*""#)]
 fn some_function() -> String {
     String::from("hello from Rust")
 }
@@ -145,17 +145,17 @@ fn some_function() -> String {
 /// An minimal example of a model of math integers for F*
 mod int_model {
     use super::hax;
-    #[hax::fstar_replace(r#"unfold type $:{Int} = int"#)]
+    #[hax::fstar::replace(r#"unfold type $:{Int} = int"#)]
     #[derive(Copy, Clone)]
     struct Int(u128);
 
-    #[hax::fstar_replace(r#"unfold let ${add} x y = x + y"#)]
+    #[hax::fstar::replace(r#"unfold let ${add} x y = x + y"#)]
     fn add(x: Int, y: Int) -> Int {
         Int(x.0 + y.0)
     }
 
     use std::ops::Sub;
-    #[hax::fstar_replace(
+    #[hax::fstar::replace(
         r#"
 unfold instance impl: Core.Ops.Arith.t_Sub $:Int $:Int =
   {

From 1cad3a21a6f4781e56cd9ca934191343cf7b07ec Mon Sep 17 00:00:00 2001
From: Lucas Franceschino <lucas@cryspen.com>
Date: Wed, 24 Apr 2024 14:32:03 +0200
Subject: [PATCH 20/21] chore: upgrade Cargo.lock

---
 Cargo.lock | 1 +
 1 file changed, 1 insertion(+)

diff --git a/Cargo.lock b/Cargo.lock
index 9b0986b5a..dbc10e3a8 100644
--- a/Cargo.lock
+++ b/Cargo.lock
@@ -559,6 +559,7 @@ dependencies = [
 name = "hax-lib-macros"
 version = "0.1.0-pre.1"
 dependencies = [
+ "hax-lib",
  "hax-lib-macros-types",
  "proc-macro-error",
  "proc-macro2",

From 20d3da5a0b172267f56f965bfd0ff5cb3939b92d Mon Sep 17 00:00:00 2001
From: Lucas Franceschino <lucas@cryspen.com>
Date: Wed, 24 Apr 2024 15:45:35 +0200
Subject: [PATCH 21/21] chore(tests): kill commented code

---
 tests/attributes/Cargo.toml | 1 -
 1 file changed, 1 deletion(-)

diff --git a/tests/attributes/Cargo.toml b/tests/attributes/Cargo.toml
index aa2261aa7..406ede1c7 100644
--- a/tests/attributes/Cargo.toml
+++ b/tests/attributes/Cargo.toml
@@ -4,7 +4,6 @@ version = "0.1.0"
 edition = "2021"
 
 [dependencies]
-# hax-lib-macros = { path = "../../hax-lib-macros" }
 hax-lib = { path = "../../hax-lib" }
 serde = { version = "1.0", features = ["derive"] }