From f4daa5d335da8c2843d3e3e12cbe67172ef2d4fa Mon Sep 17 00:00:00 2001
From: Lucas Franceschino <lucas@cryspen.com>
Date: Tue, 23 Apr 2024 10:12:29 +0200
Subject: [PATCH 1/5] feat(exporter): weaken some useless trait bounds

---
 frontend/exporter/src/types/copied.rs | 14 +++++++-------
 1 file changed, 7 insertions(+), 7 deletions(-)

diff --git a/frontend/exporter/src/types/copied.rs b/frontend/exporter/src/types/copied.rs
index 3e4060d1a..d9488b389 100644
--- a/frontend/exporter/src/types/copied.rs
+++ b/frontend/exporter/src/types/copied.rs
@@ -290,7 +290,7 @@ impl<'tcx, S: BaseState<'tcx>> SInto<S, DefId> for rustc_hir::hir_id::OwnerId {
 #[derive(
     AdtInto, Clone, Debug, Serialize, Deserialize, JsonSchema, Hash, PartialEq, Eq, PartialOrd, Ord,
 )]
-#[args(<'tcx, S: UnderOwnerState<'tcx> + HasThir<'tcx>>, from: rustc_ast::ast::LitFloatType, state: S as gstate)]
+#[args(<'tcx, S: BaseState<'tcx>>, from: rustc_ast::ast::LitFloatType, state: S as gstate)]
 pub enum LitFloatType {
     Suffixed(FloatTy),
     Unsuffixed,
@@ -660,7 +660,7 @@ impl<'tcx, S: UnderOwnerState<'tcx>> SInto<S, Vec<GenericArg>>
 
 /// Reflects both [`rustc_middle::ty::subst::GenericArg`] and [`rustc_middle::ty::subst::GenericArgKind`]
 #[derive(AdtInto)]
-#[args(<'tcx, S: UnderOwnerState<'tcx> + HasThir<'tcx>>, from: rustc_ast::ast::LitIntType, state: S as gstate)]
+#[args(<'tcx, S: BaseState<'tcx>>, from: rustc_ast::ast::LitIntType, state: S as gstate)]
 #[derive(
     Clone, Debug, Serialize, Deserialize, JsonSchema, Hash, PartialEq, Eq, PartialOrd, Ord,
 )]
@@ -1948,7 +1948,7 @@ pub enum StrStyle {
 
 /// Reflects [`rustc_ast::ast::LitKind`]
 #[derive(AdtInto)]
-#[args(<'tcx, S: UnderOwnerState<'tcx> + HasThir<'tcx>>, from: rustc_ast::ast::LitKind, state: S as gstate)]
+#[args(<'tcx, S: BaseState<'tcx>>, from: rustc_ast::ast::LitKind, state: S as gstate)]
 #[derive(
     Clone, Debug, Serialize, Deserialize, JsonSchema, Hash, PartialEq, Eq, PartialOrd, Ord,
 )]
@@ -2000,7 +2000,7 @@ pub enum CommentKind {
 
 /// Reflects [`rustc_ast::ast::AttrArgs`]
 #[derive(AdtInto)]
-#[args(<S>, from: rustc_ast::ast::AttrArgs, state: S as tcx)]
+#[args(<'tcx, S: BaseState<'tcx>>, from: rustc_ast::ast::AttrArgs, state: S as tcx)]
 #[derive(
     Clone, Debug, Serialize, Deserialize, JsonSchema, Hash, PartialEq, Eq, PartialOrd, Ord,
 )]
@@ -2015,7 +2015,7 @@ pub enum AttrArgs {
 
 /// Reflects [`rustc_ast::ast::AttrItem`]
 #[derive(AdtInto)]
-#[args(<S>, from: rustc_ast::ast::AttrItem, state: S as tcx)]
+#[args(<'tcx, S: BaseState<'tcx>>, from: rustc_ast::ast::AttrItem, state: S as tcx)]
 #[derive(
     Clone, Debug, Serialize, Deserialize, JsonSchema, Hash, PartialEq, Eq, PartialOrd, Ord,
 )]
@@ -2034,7 +2034,7 @@ impl<S> SInto<S, String> for rustc_ast::tokenstream::LazyAttrTokenStream {
 
 /// Reflects [`rustc_ast::ast::NormalAttr`]
 #[derive(AdtInto)]
-#[args(<S>, from: rustc_ast::ast::NormalAttr, state: S as tcx)]
+#[args(<'tcx, S: BaseState<'tcx>>, from: rustc_ast::ast::NormalAttr, state: S as tcx)]
 #[derive(
     Clone, Debug, Serialize, Deserialize, JsonSchema, Hash, PartialEq, Eq, PartialOrd, Ord,
 )]
@@ -2045,7 +2045,7 @@ pub struct NormalAttr {
 
 /// Reflects [`rustc_ast::AttrKind`]
 #[derive(AdtInto)]
-#[args(<S>, from: rustc_ast::AttrKind, state: S as tcx)]
+#[args(<'tcx, S: BaseState<'tcx>>, from: rustc_ast::AttrKind, state: S as tcx)]
 #[derive(
     Clone, Debug, Serialize, Deserialize, JsonSchema, Hash, PartialEq, Eq, PartialOrd, Ord,
 )]

From d59f84ce01d8381d7df014df1b098f448d28f29c Mon Sep 17 00:00:00 2001
From: Lucas Franceschino <lucas@cryspen.com>
Date: Tue, 23 Apr 2024 10:13:43 +0200
Subject: [PATCH 2/5] feat: add support for `#[doc="..."]` attributes

---
 engine/backends/fstar/fstar_backend.ml        | 77 ++++++++++++++-----
 engine/lib/import_thir.ml                     | 27 ++++---
 frontend/exporter/src/types/copied.rs         | 30 +++++++-
 .../toolchain__attributes into-fstar.snap     |  6 ++
 .../toolchain__generics into-fstar.snap       |  1 +
 .../toolchain__include-flag into-fstar.snap   |  3 +
 .../toolchain__interface-only into-fstar.snap |  9 +++
 .../toolchain__naming into-fstar.snap         | 14 ++++
 .../toolchain__side-effects into-fstar.snap   | 10 ++-
 tests/attributes/src/lib.rs                   |  6 ++
 10 files changed, 151 insertions(+), 32 deletions(-)

diff --git a/engine/backends/fstar/fstar_backend.ml b/engine/backends/fstar/fstar_backend.ml
index cb365d4e1..ec91d8bb5 100644
--- a/engine/backends/fstar/fstar_backend.ml
+++ b/engine/backends/fstar/fstar_backend.ml
@@ -799,8 +799,8 @@ struct
   let rec pitem (e : item) :
       [> `Impl of F.AST.decl
       | `Intf of F.AST.decl
-      | `VerbatimImpl of string
-      | `VerbatimIntf of string
+      | `VerbatimImpl of string * [ `NoNewline | `Newline ]
+      | `VerbatimIntf of string * [ `NoNewline | `Newline ]
       | `Comment of string ]
       list =
     try pitem_unwrapped e
@@ -816,10 +816,27 @@ struct
   and pitem_unwrapped (e : item) :
       [> `Impl of F.AST.decl
       | `Intf of F.AST.decl
-      | `VerbatimImpl of string
-      | `VerbatimIntf of string
+      | `VerbatimImpl of string * [ `NoNewline | `Newline ]
+      | `VerbatimIntf of string * [ `NoNewline | `Newline ]
       | `Comment of string ]
       list =
+    let doc_comments =
+      e.attrs
+      |> List.filter_map ~f:(fun (attr : attr) ->
+             match attr.kind with
+             | DocComment { kind; body } -> Some (kind, body)
+             | _ -> None)
+      |> List.map ~f:(fun (kind, string) ->
+             match kind with
+             | DCKLine ->
+                 String.split_lines string
+                 |> List.map ~f:(fun s -> "///" ^ s)
+                 |> String.concat_lines
+             | DCKBlock -> "(**" ^ string ^ "*)")
+      |> List.map ~f:(fun s -> `VerbatimIntf (s, `NoNewline))
+    in
+    doc_comments
+    @
     match e.v with
     | Alias { name; item } ->
         let pat =
@@ -1272,10 +1289,13 @@ 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 e.span quote) ]
+        (if fstar_opts.intf then
+         [ `VerbatimIntf (pquote e.span quote, `Newline) ]
         else [])
         @
-        if fstar_opts.impl then [ `VerbatimImpl (pquote e.span quote) ] else []
+        if fstar_opts.impl then
+          [ `VerbatimImpl (pquote e.span quote, `Newline) ]
+        else []
     | HaxError details ->
         [
           `Comment
@@ -1291,8 +1311,8 @@ module type S = sig
     item ->
     [> `Impl of F.AST.decl
     | `Intf of F.AST.decl
-    | `VerbatimImpl of string
-    | `VerbatimIntf of string
+    | `VerbatimImpl of string * [ `NoNewline | `Newline ]
+    | `VerbatimIntf of string * [ `NoNewline | `Newline ]
     | `Comment of string ]
     list
 end
@@ -1305,7 +1325,8 @@ let make (module M : Attrs.WITH_ITEMS) ctx =
             end) : S)
 
 let strings_of_item ~signature_only (bo : BackendOptions.t) m items
-    (item : item) : [> `Impl of string | `Intf of string ] list =
+    (item : item) :
+    ([> `Impl of string | `Intf of string ] * [ `NoNewline | `Newline ]) list =
   let interface_mode' : Types.inclusion_kind =
     List.rev bo.interfaces
     |> List.find ~f:(fun (clause : Types.inclusion_clause) ->
@@ -1342,26 +1363,44 @@ let strings_of_item ~signature_only (bo : BackendOptions.t) m items
   Print.pitem item
   |> List.filter ~f:(function `Impl _ when no_impl -> false | _ -> true)
   |> 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 ]
+       | `Impl i -> [ (mk_impl (decl_to_string i), `Newline) ]
+       | `Intf i -> [ (mk_intf (decl_to_string i), `Newline) ]
+       | `VerbatimIntf (s, nl) ->
+           [ ((if interface_mode then `Intf s else `Impl s), nl) ]
+       | `VerbatimImpl (s, nl) ->
+           [ ((if interface_mode then `Impl s else `Impl s), nl) ]
        | `Comment s ->
            let s = "(* " ^ s ^ " *)" in
-           if interface_mode then [ `Impl s; `Intf s ] else [ `Impl s ])
+           if interface_mode then [ (`Impl s, `Newline); (`Intf s, `Newline) ]
+           else [ (`Impl s, `Newline) ])
 
 let string_of_items ~signature_only (bo : BackendOptions.t) m items :
     string * string =
   let strings =
     List.concat_map ~f:(strings_of_item ~signature_only bo m items) items
-    |> List.map ~f:(function
-         | `Impl s -> `Impl (String.strip s)
-         | `Intf s -> `Intf (String.strip s))
+    |> List.map
+         ~f:
+           ((function
+              | `Impl s -> `Impl (String.strip s)
+              | `Intf s -> `Intf (String.strip s))
+           *** Fn.id)
     |> List.filter
-         ~f:((function `Impl s | `Intf s -> String.is_empty s) >> not)
+         ~f:(fst >> (function `Impl s | `Intf s -> String.is_empty s) >> not)
   in
   let string_for filter =
-    List.filter_map ~f:filter strings |> String.concat ~sep:"\n\n"
+    let l =
+      List.filter_map
+        ~f:(fun (s, space) ->
+          let* s = filter s in
+          Some (s, space))
+        strings
+    in
+    let n = List.length l - 1 in
+    List.mapi
+      ~f:(fun i (s, space) ->
+        s ^ if [%matches? `NoNewline] space || [%eq: int] i n then "" else "\n")
+      l
+    |> String.concat ~sep:"\n"
   in
   ( string_for (function `Impl s -> Some s | _ -> None),
     string_for (function `Intf s -> Some s | _ -> None) )
diff --git a/engine/lib/import_thir.ml b/engine/lib/import_thir.ml
index 376a1c87a..5d1db99fc 100644
--- a/engine/lib/import_thir.ml
+++ b/engine/lib/import_thir.ml
@@ -101,6 +101,19 @@ let c_logical_op : Thir.logical_op -> logical_op = function
 let c_attr (attr : Thir.attribute) : attr =
   let kind =
     match attr.kind with
+    | DocComment (kind, body) ->
+        let kind =
+          match kind with Thir.Line -> DCKLine | Thir.Block -> DCKBlock
+        in
+        DocComment { kind; body }
+    | Normal
+        {
+          item =
+            { args = Eq (_, Hir { symbol; _ }); path = "doc"; tokens = None };
+          tokens = None;
+        } ->
+        DocComment { kind = DCKLine; body = symbol }
+        (* Looks for `#[doc = "something"]` *)
     | Normal { item = { args; path; tokens = subtokens }; tokens } ->
         let args_tokens =
           match args with Delimited { tokens; _ } -> Some tokens | _ -> None
@@ -110,11 +123,6 @@ let c_attr (attr : Thir.attribute) : attr =
           Option.value ~default:"" (args_tokens || tokens || subtokens)
         in
         Tool { path; tokens }
-    | DocComment (kind, body) ->
-        let kind =
-          match kind with Thir.Line -> DCKLine | Thir.Block -> DCKBlock
-        in
-        DocComment { kind; body }
   in
   { kind; span = Span.of_thir attr.span }
 
@@ -125,15 +133,14 @@ let c_item_attrs (attrs : Thir.item_attributes) : attrs =
      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 =
-    (* Repeating associateditem or uid is harmful *)
-    List.filter
-      ~f:(fun payload ->
+    c_attrs attrs.parent_attributes
+    |> List.filter ~f:([%matches? ({ kind = DocComment _; _ } : attr)] >> not)
+    |> (* Repeating associateditem or uid is harmful, same for comments *)
+    List.filter ~f:(fun payload ->
         match Attr_payloads.payloads [ payload ] with
         | [ ((Uid _ | AssociatedItem _), _) ] -> false
         | _ -> true)
-      parent
   in
   self @ parent
 
diff --git a/frontend/exporter/src/types/copied.rs b/frontend/exporter/src/types/copied.rs
index d9488b389..60a2aba72 100644
--- a/frontend/exporter/src/types/copied.rs
+++ b/frontend/exporter/src/types/copied.rs
@@ -2008,9 +2008,35 @@ pub enum AttrArgs {
     Empty,
     Delimited(DelimArgs),
 
+    Eq(Span, AttrArgsEq),
+    // #[todo]
+    // Todo(String),
+}
+
+/// Reflects [`rustc_ast::ast::AttrArgsEq`]
+#[derive(AdtInto)]
+#[args(<'tcx, S: BaseState<'tcx>>, from: rustc_ast::ast::AttrArgsEq, state: S as tcx)]
+#[derive(
+    Clone, Debug, Serialize, Deserialize, JsonSchema, Hash, PartialEq, Eq, PartialOrd, Ord,
+)]
+pub enum AttrArgsEq {
+    Hir(MetaItemLit),
     #[todo]
-    Todo(String),
-    // Eq(Span, AttrArgsEq),
+    Ast(String),
+    // Ast(P<Expr>),
+}
+
+/// Reflects [`rustc_ast::ast::MetaItemLit`]
+#[derive(AdtInto)]
+#[args(<'tcx, S: BaseState<'tcx>>, from: rustc_ast::ast::MetaItemLit, state: S as tcx)]
+#[derive(
+    Clone, Debug, Serialize, Deserialize, JsonSchema, Hash, PartialEq, Eq, PartialOrd, Ord,
+)]
+pub struct MetaItemLit {
+    pub symbol: Symbol,
+    pub suffix: Option<Symbol>,
+    pub kind: LitKind,
+    pub span: Span,
 }
 
 /// Reflects [`rustc_ast::ast::AttrItem`]
diff --git a/test-harness/src/snapshots/toolchain__attributes into-fstar.snap b/test-harness/src/snapshots/toolchain__attributes into-fstar.snap
index bfeaf0a6c..6998ed94e 100644
--- a/test-harness/src/snapshots/toolchain__attributes into-fstar.snap	
+++ b/test-harness/src/snapshots/toolchain__attributes into-fstar.snap	
@@ -108,6 +108,10 @@ let v_MAX: usize = sz 10
 
 type t_MyArray = | MyArray : t_Array u8 (sz 10) -> t_MyArray
 
+/// Triple dash comment
+(** Multiline double star comment Maecenas blandit accumsan feugiat.
+    Done vitae ullamcorper est.
+    Curabitur id dui eget sem viverra interdum. *)
 let mutation_example
       (use_generic_update_at: t_MyArray)
       (use_specialized_update_at: t_Slice u8)
@@ -153,6 +157,8 @@ let u32_max: u32 = 90000ul
 
 unfold let some_function _ = "hello from F*"
 
+/// A doc comment on `add3`
+///another doc comment on add3
 let add3 (x y z: u32)
     : Prims.Pure u32
       (requires x >. 10ul && y >. 10ul && z >. 10ul && ((x +! y <: u32) +! z <: u32) <. u32_max)
diff --git a/test-harness/src/snapshots/toolchain__generics into-fstar.snap b/test-harness/src/snapshots/toolchain__generics into-fstar.snap
index eee521479..6892c3613 100644
--- a/test-harness/src/snapshots/toolchain__generics into-fstar.snap	
+++ b/test-harness/src/snapshots/toolchain__generics into-fstar.snap	
@@ -63,6 +63,7 @@ let impl_Foo_for_usize: t_Foo usize =
     f_const_add = fun (v_N: usize) (self: usize) -> self +! v_N
   }
 
+/// Test defaults types and constants
 let dup (#v_T: Type) (#[FStar.Tactics.Typeclasses.tcresolve ()] i1: Core.Clone.t_Clone v_T) (x: v_T)
     : (v_T & v_T) = Core.Clone.f_clone x, Core.Clone.f_clone x <: (v_T & v_T)
 
diff --git a/test-harness/src/snapshots/toolchain__include-flag into-fstar.snap b/test-harness/src/snapshots/toolchain__include-flag into-fstar.snap
index 86e4eb07f..759bc8f1d 100644
--- a/test-harness/src/snapshots/toolchain__include-flag into-fstar.snap	
+++ b/test-harness/src/snapshots/toolchain__include-flag into-fstar.snap	
@@ -34,12 +34,14 @@ open FStar.Mul
 
 class t_Trait (v_Self: Type) = { __marker_trait_t_Trait:Prims.unit }
 
+/// Indirect dependencies
 let main_a_a (_: Prims.unit) : Prims.unit = ()
 
 let main_a_b (_: Prims.unit) : Prims.unit = ()
 
 let main_a_c (_: Prims.unit) : Prims.unit = ()
 
+/// Direct dependencies
 let main_a (#v_T: Type) (#[FStar.Tactics.Typeclasses.tcresolve ()] i1: t_Trait v_T) (x: v_T)
     : Prims.unit =
   let _:Prims.unit = main_a_a () in
@@ -76,6 +78,7 @@ type t_Foo = | Foo : t_Foo
 [@@ FStar.Tactics.Typeclasses.tcinstance]
 let impl_Trait_for_Foo: t_Trait t_Foo = { __marker_trait = () }
 
+/// Entrypoint
 let main (_: Prims.unit) : Prims.unit =
   let _:Prims.unit = main_a (Foo <: t_Foo) in
   let _:Prims.unit = main_b () in
diff --git a/test-harness/src/snapshots/toolchain__interface-only into-fstar.snap b/test-harness/src/snapshots/toolchain__interface-only into-fstar.snap
index 9d392ab5e..b3a95740d 100644
--- a/test-harness/src/snapshots/toolchain__interface-only into-fstar.snap	
+++ b/test-harness/src/snapshots/toolchain__interface-only into-fstar.snap	
@@ -35,6 +35,11 @@ module Interface_only
 open Core
 open FStar.Mul
 
+/// This item contains unsafe blocks and raw references, two features
+/// not supported by hax. Thanks to the `-i` flag and the `+:`
+/// modifier, `f` is still extractable as an interface.
+/// Expressions within type are still extracted, as well as pre- and
+/// post-conditions.
 val f (x: u8)
     : Prims.Pure (t_Array u8 (sz 4))
       (requires x <. 254uy)
@@ -45,6 +50,9 @@ val f (x: u8)
 
 type t_Bar = | Bar : t_Bar
 
+/// Non-inherent implementations are extracted, their bodies are not
+/// dropped. This might be a bit surprising: see
+/// https://github.com/hacspec/hax/issues/616.
 [@@ FStar.Tactics.Typeclasses.tcinstance]
 let impl: Core.Convert.t_From t_Bar Prims.unit =
   {
@@ -55,6 +63,7 @@ let impl: Core.Convert.t_From t_Bar Prims.unit =
 
 val from__from: u8 -> Prims.Pure t_Bar Prims.l_True (fun _ -> Prims.l_True)
 
+/// If you need to drop the body of a method, please hoist it:
 [@@ FStar.Tactics.Typeclasses.tcinstance]
 let impl_1: Core.Convert.t_From t_Bar u8 =
   {
diff --git a/test-harness/src/snapshots/toolchain__naming into-fstar.snap b/test-harness/src/snapshots/toolchain__naming into-fstar.snap
index abfe8b043..b679b28e8 100644
--- a/test-harness/src/snapshots/toolchain__naming into-fstar.snap	
+++ b/test-harness/src/snapshots/toolchain__naming into-fstar.snap	
@@ -32,6 +32,8 @@ module Naming.Ambiguous_names
 open Core
 open FStar.Mul
 
+/// This macro surround a given expression with a let binding for
+/// an identifier `a` and a print of that `a`.
 let debug (label value: u32) : Prims.unit =
   let _:Prims.unit =
     Std.Io.Stdio.v__print (Core.Fmt.impl_2__new_v1 (Rust_primitives.unsize (let list =
@@ -56,6 +58,7 @@ let debug (label value: u32) : Prims.unit =
   in
   ()
 
+/// `f` stacks mutliple let bindings declaring different `a`s.
 let f (_: Prims.unit) : Prims.unit =
   let a_1_:u32 = 104ul in
   let a_2_:u32 = 205ul in
@@ -66,6 +69,13 @@ let f (_: Prims.unit) : Prims.unit =
   let _:Prims.unit = debug 1ul a_1_ in
   debug 4ul a
 
+/// `f` is expanded into `f_expand` below, while the execution of `f` gives:
+/// ```plaintext
+///  [3] a=306
+///  [2] a=205
+///  [1] a=104
+///  [last] a=123
+/// ```
 let ff_expand (_: Prims.unit) : Prims.unit =
   let a:i32 = 104l in
   let a:i32 = 205l in
@@ -117,6 +127,10 @@ class t_T3_e_for_a (v_Self: Type) = { __marker_trait_t_T3_e_for_a:Prims.unit }
 [@@ FStar.Tactics.Typeclasses.tcinstance]
 let impl_T3_e_e_for_a_for_Foo: t_T3_e_for_a t_Foo = { __marker_trait = () }
 
+/// Test for ambiguous local names renaming: when two local vars are
+/// ambiguous by name but not by their internal IDs.
+/// Such situation can occur playing with *hygenic* macros.
+/// Also, this happens with some internal Rustc rewrite. (e.g. assignment of tuples)
 let v_INHERENT_CONSTANT: usize = sz 3
 
 let constants
diff --git a/test-harness/src/snapshots/toolchain__side-effects into-fstar.snap b/test-harness/src/snapshots/toolchain__side-effects into-fstar.snap
index 5ae7f9b1a..ee3c46e86 100644
--- a/test-harness/src/snapshots/toolchain__side-effects into-fstar.snap	
+++ b/test-harness/src/snapshots/toolchain__side-effects into-fstar.snap	
@@ -1,6 +1,5 @@
 ---
 source: test-harness/src/harness.rs
-assertion_line: 214
 expression: snapshot
 info:
   kind:
@@ -36,15 +35,18 @@ module Side_effects
 open Core
 open FStar.Mul
 
+/// Helper function
 let add3 (x y z: u32) : u32 =
   Core.Num.impl__u32__wrapping_add (Core.Num.impl__u32__wrapping_add x y <: u32) z
 
+/// Question mark without error coercion
 let direct_result_question_mark (y: Core.Result.t_Result Prims.unit u32)
     : Core.Result.t_Result i8 u32 =
   match y with
   | Core.Result.Result_Ok _ -> Core.Result.Result_Ok 0y <: Core.Result.t_Result i8 u32
   | Core.Result.Result_Err err -> Core.Result.Result_Err err <: Core.Result.t_Result i8 u32
 
+/// Question mark with an error coercion
 let direct_result_question_mark_coercion (y: Core.Result.t_Result i8 u16)
     : Core.Result.t_Result i8 u32 =
   match y with
@@ -52,6 +54,7 @@ let direct_result_question_mark_coercion (y: Core.Result.t_Result i8 u16)
   | Core.Result.Result_Err err ->
     Core.Result.Result_Err (Core.Convert.f_from err) <: Core.Result.t_Result i8 u32
 
+/// Exercise early returns with control flow and loops
 let early_returns (x: u32) : u32 =
   Rust_primitives.Hax.Control_flow_monad.Mexception.run (let! _:Prims.unit =
         if x >. 3ul
@@ -104,6 +107,7 @@ let early_returns (x: u32) : u32 =
       <:
       Core.Ops.Control_flow.t_ControlFlow u32 u32)
 
+/// Exercise local mutation with control flow and loops
 let local_mutation (x: u32) : u32 =
   let y:u32 = 0ul in
   let x:u32 = Core.Num.impl__u32__wrapping_add x 1ul in
@@ -144,6 +148,7 @@ let local_mutation (x: u32) : u32 =
     let x:u32 = hoist15 in
     Core.Num.impl__u32__wrapping_add x y
 
+/// Test question mark on `Option`s with some control flow
 let options (x y: Core.Option.t_Option u8) (z: Core.Option.t_Option u64) : Core.Option.t_Option u8 =
   Rust_primitives.Hax.Control_flow_monad.Mexception.run (match x with
       | Core.Option.Option_Some hoist19 ->
@@ -249,6 +254,7 @@ let options (x y: Core.Option.t_Option u8) (z: Core.Option.t_Option u64) : Core.
         <:
         Core.Ops.Control_flow.t_ControlFlow (Core.Option.t_Option u8) (Core.Option.t_Option u8))
 
+/// Test question mark on `Result`s with local mutation
 let question_mark (x: u32) : Core.Result.t_Result u32 u32 =
   Rust_primitives.Hax.Control_flow_monad.Mexception.run (let! x:u32 =
         if x >. 40ul
@@ -300,6 +306,7 @@ type t_Bar = {
   f_b:(t_Array (bool & bool) (sz 6) & bool)
 }
 
+/// Combine `?` and early return
 let monad_lifting (x: u8) : Core.Result.t_Result t_A t_B =
   Rust_primitives.Hax.Control_flow_monad.Mexception.run (if x >. 123uy <: bool
       then
@@ -336,6 +343,7 @@ type t_Foo = {
   f_bar:t_Bar
 }
 
+/// Test assignation on non-trivial places
 let assign_non_trivial_lhs (foo: t_Foo) : t_Foo =
   let foo:t_Foo = { foo with f_x = true } <: t_Foo in
   let foo:t_Foo = { foo with f_bar = { foo.f_bar with f_a = true } <: t_Bar } <: t_Foo in
diff --git a/tests/attributes/src/lib.rs b/tests/attributes/src/lib.rs
index cab615b18..76a05cd69 100644
--- a/tests/attributes/src/lib.rs
+++ b/tests/attributes/src/lib.rs
@@ -3,6 +3,8 @@ use hax_lib as hax;
 // dummy max value
 const u32_max: u32 = 90000;
 
+/// A doc comment on `add3`
+#[doc = "another doc comment on add3"]
 #[hax::requires(x > 10 && y > 10 && z > 10 && x + y + z < u32_max)]
 #[hax::ensures(|result| hax_lib::implies(true, || result > 32))]
 fn add3(x: u32, y: u32, z: u32) -> u32 {
@@ -84,6 +86,10 @@ mod refined_indexes {
         }
     }
 
+    /// Triple dash comment
+    /** Multiline double star comment Maecenas blandit accumsan feugiat.
+    Done vitae ullamcorper est.
+    Curabitur id dui eget sem viverra interdum. */
     fn mutation_example(
         use_generic_update_at: &mut MyArray,
         use_specialized_update_at: &mut [u8],

From b1d8788e4a609061221117bc2dcb21f3a260482b Mon Sep 17 00:00:00 2001
From: Lucas Franceschino <lucas@cryspen.com>
Date: Thu, 25 Apr 2024 07:06:17 +0200
Subject: [PATCH 3/5] fix(fstar): print comments only if the item is printed as
 well

---
 engine/backends/fstar/fstar_backend.ml        | 40 ++++++++++---------
 .../toolchain__generics into-fstar.snap       |  1 -
 .../toolchain__naming into-fstar.snap         |  6 ---
 3 files changed, 22 insertions(+), 25 deletions(-)

diff --git a/engine/backends/fstar/fstar_backend.ml b/engine/backends/fstar/fstar_backend.ml
index ec91d8bb5..c92c59a57 100644
--- a/engine/backends/fstar/fstar_backend.ml
+++ b/engine/backends/fstar/fstar_backend.ml
@@ -796,6 +796,22 @@ struct
         in
         F.mk_e_app effect (if is_lemma then args else typ :: args)
 
+  (** Prints doc comments out of a list of attributes *)
+  let pdoc_comments attrs =
+    attrs
+    |> List.filter_map ~f:(fun (attr : attr) ->
+           match attr.kind with
+           | DocComment { kind; body } -> Some (kind, body)
+           | _ -> None)
+    |> List.map ~f:(fun (kind, string) ->
+           match kind with
+           | DCKLine ->
+               String.split_lines string
+               |> List.map ~f:(fun s -> "///" ^ s)
+               |> String.concat_lines
+           | DCKBlock -> "(**" ^ string ^ "*)")
+    |> List.map ~f:(fun s -> `VerbatimIntf (s, `NoNewline))
+
   let rec pitem (e : item) :
       [> `Impl of F.AST.decl
       | `Intf of F.AST.decl
@@ -803,7 +819,12 @@ struct
       | `VerbatimIntf of string * [ `NoNewline | `Newline ]
       | `Comment of string ]
       list =
-    try pitem_unwrapped e
+    try
+      match pitem_unwrapped e with
+      | [] -> []
+      | printed_items ->
+          (* Print comments only for items that are being printed *)
+          pdoc_comments e.attrs @ printed_items
     with Diagnostics.SpanFreeError.Exn error ->
       let error = Diagnostics.SpanFreeError.payload error in
       let error = [%show: Diagnostics.Context.t * Diagnostics.kind] error in
@@ -820,23 +841,6 @@ struct
       | `VerbatimIntf of string * [ `NoNewline | `Newline ]
       | `Comment of string ]
       list =
-    let doc_comments =
-      e.attrs
-      |> List.filter_map ~f:(fun (attr : attr) ->
-             match attr.kind with
-             | DocComment { kind; body } -> Some (kind, body)
-             | _ -> None)
-      |> List.map ~f:(fun (kind, string) ->
-             match kind with
-             | DCKLine ->
-                 String.split_lines string
-                 |> List.map ~f:(fun s -> "///" ^ s)
-                 |> String.concat_lines
-             | DCKBlock -> "(**" ^ string ^ "*)")
-      |> List.map ~f:(fun s -> `VerbatimIntf (s, `NoNewline))
-    in
-    doc_comments
-    @
     match e.v with
     | Alias { name; item } ->
         let pat =
diff --git a/test-harness/src/snapshots/toolchain__generics into-fstar.snap b/test-harness/src/snapshots/toolchain__generics into-fstar.snap
index 6892c3613..eee521479 100644
--- a/test-harness/src/snapshots/toolchain__generics into-fstar.snap	
+++ b/test-harness/src/snapshots/toolchain__generics into-fstar.snap	
@@ -63,7 +63,6 @@ let impl_Foo_for_usize: t_Foo usize =
     f_const_add = fun (v_N: usize) (self: usize) -> self +! v_N
   }
 
-/// Test defaults types and constants
 let dup (#v_T: Type) (#[FStar.Tactics.Typeclasses.tcresolve ()] i1: Core.Clone.t_Clone v_T) (x: v_T)
     : (v_T & v_T) = Core.Clone.f_clone x, Core.Clone.f_clone x <: (v_T & v_T)
 
diff --git a/test-harness/src/snapshots/toolchain__naming into-fstar.snap b/test-harness/src/snapshots/toolchain__naming into-fstar.snap
index b679b28e8..bada19155 100644
--- a/test-harness/src/snapshots/toolchain__naming into-fstar.snap	
+++ b/test-harness/src/snapshots/toolchain__naming into-fstar.snap	
@@ -32,8 +32,6 @@ module Naming.Ambiguous_names
 open Core
 open FStar.Mul
 
-/// This macro surround a given expression with a let binding for
-/// an identifier `a` and a print of that `a`.
 let debug (label value: u32) : Prims.unit =
   let _:Prims.unit =
     Std.Io.Stdio.v__print (Core.Fmt.impl_2__new_v1 (Rust_primitives.unsize (let list =
@@ -127,10 +125,6 @@ class t_T3_e_for_a (v_Self: Type) = { __marker_trait_t_T3_e_for_a:Prims.unit }
 [@@ FStar.Tactics.Typeclasses.tcinstance]
 let impl_T3_e_e_for_a_for_Foo: t_T3_e_for_a t_Foo = { __marker_trait = () }
 
-/// Test for ambiguous local names renaming: when two local vars are
-/// ambiguous by name but not by their internal IDs.
-/// Such situation can occur playing with *hygenic* macros.
-/// Also, this happens with some internal Rustc rewrite. (e.g. assignment of tuples)
 let v_INHERENT_CONSTANT: usize = sz 3
 
 let constants

From a03c1b4f3a75e604fe0548e086b06caffca4109e Mon Sep 17 00:00:00 2001
From: Lucas Franceschino <lucas@cryspen.com>
Date: Wed, 24 Apr 2024 17:59:36 +0200
Subject: [PATCH 4/5] fix(test-harness): `hax-engine-names-extract` needs hax
 in PATH

This commit fixes the test harness: since
https://github.com/hacspec/hax/pull/428, the test harness silently
assumes hax is in PATH while building the crate
`hax-engine-names-extract`.

This crate `hax-engine-names-extract` is used at build time by the
engine to list and import the Rust names we rely on.

`hax-engine-names-extract` itself requires the Rust part of hax at
build time.

This PR fixes the test harness so that:
 1. it asks cargo to build `cargo-hax` and the driver
 2. it looks for the path of `cargo-hax` & driver just built (somewhere local in `target/bin/something/someting`), injects thoses paths as env vars in a `cargo build --bin hax-engine-names-extract`;
 3. it compiles the engine with the three paths mentioned above (which are required by the engine at compile time);
 4. it runs full hax (frontend + engine) on the actual tests;
 5. compare with snapshots.
---
 engine/names/extract/build.rs       |  3 ++-
 test-harness/src/command_hax_ext.rs | 22 ++++++++++++++++++----
 2 files changed, 20 insertions(+), 5 deletions(-)

diff --git a/engine/names/extract/build.rs b/engine/names/extract/build.rs
index e9482ce69..00400f27b 100644
--- a/engine/names/extract/build.rs
+++ b/engine/names/extract/build.rs
@@ -123,7 +123,8 @@ fn target_dir(suffix: &str) -> camino::Utf8PathBuf {
 }
 
 fn get_json() -> String {
-    let mut cmd = Command::new("cargo-hax");
+    let mut cmd =
+        Command::new(std::env::var("HAX_CARGO_COMMAND_PATH").unwrap_or("cargo-hax".to_string()));
     cmd.args([
         "hax",
         "-C",
diff --git a/test-harness/src/command_hax_ext.rs b/test-harness/src/command_hax_ext.rs
index ff404a25f..ff830bc8c 100644
--- a/test-harness/src/command_hax_ext.rs
+++ b/test-harness/src/command_hax_ext.rs
@@ -33,9 +33,23 @@ impl CommandHaxExt for Command {
                 let root = std::env::current_dir().unwrap();
                 let root = root.parent().unwrap();
                 let engine_dir = root.join("engine");
-                // Make sure binaries are built
+                // Make sure binaries are built. Note this doesn't
+                // include `hax-engine-names-extract`: its build
+                // script requires the driver and CLI of `hax` to be
+                // available.
                 assert!(Command::new("cargo")
-                        .args(&["build", "--workspace", "--bins"])
+                            .args(&["build", "--bins"])
+                            .status()
+                            .unwrap()
+                            .success());
+                let cargo_hax = cargo_bin(CARGO_HAX);
+                let driver = cargo_bin("driver-hax-frontend-exporter");
+                // Now the driver & CLI are installed, call `cargo
+                // build` injecting their paths
+                assert!(Command::new("cargo")
+                        .args(&["build", "--workspace", "--bin", "hax-engine-names-extract"])
+                        .env("HAX_CARGO_COMMAND_PATH", &cargo_hax)
+                        .env("HAX_RUSTC_DRIVER_BINARY", &driver)
                         .status()
                         .unwrap()
                         .success());
@@ -49,8 +63,8 @@ impl CommandHaxExt for Command {
                         .unwrap()
                         .success());
                 Some(Paths {
-                    driver: cargo_bin("driver-hax-frontend-exporter"),
-                    cargo_hax: cargo_bin(CARGO_HAX),
+                    driver,
+                    cargo_hax,
                     engine: engine_dir.join("_build/install/default/bin/hax-engine"),
                 })
             };

From 6d243517b2f292eb08ae991d4053b8717fc268d0 Mon Sep 17 00:00:00 2001
From: Aymeric Fromherz <aymeric.fromherz@inria.fr>
Date: Thu, 25 Apr 2024 17:32:17 +0200
Subject: [PATCH 5/5] Fix typo in frontend error message

---
 frontend/exporter/src/traits.rs | 2 +-
 1 file changed, 1 insertion(+), 1 deletion(-)

diff --git a/frontend/exporter/src/traits.rs b/frontend/exporter/src/traits.rs
index 09ea00209..e7bcdaac9 100644
--- a/frontend/exporter/src/traits.rs
+++ b/frontend/exporter/src/traits.rs
@@ -492,7 +492,7 @@ pub fn select_trait_candidate<'tcx, S: UnderOwnerState<'tcx>>(
         Ok(selection) => selection,
         Err(error) => fatal!(
             s,
-            "Cannot hanlde error `{:?}` selecting `{:?}`",
+            "Cannot handle error `{:?}` selecting `{:?}`",
             error,
             trait_ref
         ),