Repository: cryspen/hax (language: rust)

Issue:
Allow `impl`s to be opaque
This is needed for https://github.com/hacspec/hax/issues/1070#issuecomment-2476182283, we already have opaque types of which this will be an extension.


Discussion / hints:
We need this for both functions and impls. When we see this `opaque` attribute we should add the `val` in the fsti, and and `assume new name: type` in the fst.
We should make sure that we "kill" the body of opaque stuff early to avoid errors in the engine phases about them.
Let's use this as a first step towards making opaque anything we do not want to handle, including raw mutable pointers, static globals etc. That needs a design document.

Fix patch:
diff --git a/engine/backends/fstar/fstar_ast.ml b/engine/backends/fstar/fstar_ast.ml
index 0ead59bd5..bd8d3a5cd 100644
--- a/engine/backends/fstar/fstar_ast.ml
+++ b/engine/backends/fstar/fstar_ast.ml
@@ -9,6 +9,7 @@ module Ident = FStar_Ident
 
 let dummyRange = Range.dummyRange
 let id ident = Ident.mk_ident (ident, dummyRange)
+let id_prime (ident : Ident.ident) = id (ident.idText ^ "'")
 
 let lid path =
   let init, last = List.(drop_last_exn path, last_exn path) in
@@ -87,6 +88,7 @@ let mk_refined (x : string) (typ : AST.term) (phi : x:AST.term -> AST.term) =
   term @@ AST.Refine (x_bd, phi (term @@ AST.Var (lid_of_id x)))
 
 let type0_term = AST.Name (lid [ "Type0" ]) |> term
+let eqtype_term = AST.Name (lid [ "eqtype" ]) |> term
 
 let parse_string f s =
   let open FStar_Parser_ParseIt in
diff --git a/engine/backends/fstar/fstar_backend.ml b/engine/backends/fstar/fstar_backend.ml
index 3518e40c4..f77e8fc1f 100644
--- a/engine/backends/fstar/fstar_backend.ml
+++ b/engine/backends/fstar/fstar_backend.ml
@@ -875,6 +875,34 @@ struct
       | `VerbatimIntf of string * [ `NoNewline | `Newline ]
       | `Comment of string ]
       list =
+    let is_erased =
+      Attrs.find_unique_attr e.attrs
+        ~f:([%eq: Types.ha_payload] Erased >> Fn.flip Option.some_if ())
+      |> Option.is_some
+    in
+    let erased_impl name ty attrs binders =
+      let name' = F.id_prime name in
+      let pat = F.AST.PatVar (name, None, []) in
+      let term = F.term @@ F.AST.Var (F.lid_of_id @@ name') in
+      let pat, term =
+        match binders with
+        | [] -> (pat, term)
+        | _ ->
+            ( F.AST.PatApp
+                (F.pat pat, List.map ~f:FStarBinder.to_pattern binders),
+              List.fold_left binders ~init:term ~f:(fun term binder ->
+                  let binder_term, binder_imp =
+                    FStarBinder.to_qualified_term binder
+                  in
+                  F.term @@ F.AST.App (term, binder_term, binder_imp)) )
+      in
+      [
+        F.decl ~quals:[ Assumption ] ~fsti:false ~attrs
+        @@ F.AST.Assume (name', ty);
+        F.decl ~fsti:false
+        @@ F.AST.TopLevelLet (NoLetQualifier, [ (F.pat @@ pat, term) ]);
+      ]
+    in
     match e.v with
     | Alias { name; item } ->
         (* These should come from bundled items (in the case of cyclic module dependencies).
@@ -939,7 +967,12 @@ struct
         in
 
         let intf = F.decl ~fsti:true (F.AST.Val (name, arrow_typ)) in
-        if interface_mode then [ impl; intf ] else [ full ]
+
+        let erased = erased_impl name arrow_typ [] generics in
+        let impl, full =
+          if is_erased then (erased, erased) else ([ impl ], [ full ])
+        in
+        if interface_mode then intf :: impl else full
     | TyAlias { name; generics; ty } ->
         let pat =
           F.pat
@@ -972,31 +1005,20 @@ struct
                             |> List.map ~f:to_pattern) ),
                    ty );
                ] )
-    | Type { name; generics; _ }
-      when Attrs.find_unique_attr e.attrs
-             ~f:([%eq: Types.ha_payload] OpaqueType >> Fn.flip Option.some_if ())
-           |> Option.is_some ->
-        if not ctx.interface_mode then
-          Error.raise
-          @@ {
-               kind =
-                 AttributeRejected
-                   {
-                     reason =
-                       "a type cannot be opaque if its module is not extracted \
-                        as an interface";
-                   };
-               span = e.span;
-             }
-        else
-          let generics = FStarBinder.of_generics e.span generics in
-          let ty = F.type0_term in
-          let arrow_typ =
-            F.term
-            @@ F.AST.Product (List.map ~f:FStarBinder.to_binder generics, ty)
-          in
-          let name = F.id @@ U.Concrete_ident_view.to_definition_name name in
-          [ F.decl ~fsti:true (F.AST.Val (name, arrow_typ)) ]
+    | Type { name; generics; _ } when is_erased ->
+        let generics =
+          FStarBinder.of_generics e.span generics
+          |> List.map ~f:FStarBinder.implicit_to_explicit
+        in
+        let ty = F.eqtype_term in
+        let arrow_typ =
+          F.term
+          @@ F.AST.Product (List.map ~f:FStarBinder.to_binder generics, ty)
+        in
+        let name = F.id @@ U.Concrete_ident_view.to_definition_name name in
+        let erased = erased_impl name arrow_typ [] generics in
+        let intf = F.decl ~fsti:true (F.AST.Val (name, arrow_typ)) in
+        if ctx.interface_mode then intf :: erased else erased
     | Type
         {
           name;
@@ -1476,15 +1498,20 @@ struct
           List.exists items ~f:(fun { ii_v; _ } ->
               match ii_v with IIType _ -> true | _ -> false)
         in
-        let impl_val = ctx.interface_mode && not has_type in
         let let_impl = F.AST.TopLevelLet (NoLetQualifier, [ (pat, body) ]) in
-        if impl_val then
-          let generics_binders = List.map ~f:FStarBinder.to_binder generics in
-          let val_type = F.term @@ F.AST.Product (generics_binders, typ) in
-          let v = F.AST.Val (name, val_type) in
-          (F.decls ~fsti:true ~attrs:[ tcinst ] @@ v)
-          @ F.decls ~fsti:false ~attrs:[ tcinst ] let_impl
-        else F.decls ~fsti:ctx.interface_mode ~attrs:[ tcinst ] let_impl
+        let generics_binders = List.map ~f:FStarBinder.to_binder generics in
+        let val_type = F.term @@ F.AST.Product (generics_binders, typ) in
+        let v = F.AST.Val (name, val_type) in
+        let intf = F.decls ~fsti:true ~attrs:[ tcinst ] v in
+        let impl =
+          if is_erased then erased_impl name val_type [ tcinst ] generics
+          else
+            F.decls
+              ~fsti:(ctx.interface_mode && has_type)
+              ~attrs:[ tcinst ] let_impl
+        in
+        let intf = if has_type && not is_erased then [] else intf in
+        if ctx.interface_mode then intf @ impl else impl
     | Quote { quote; _ } ->
         let fstar_opts =
           Attrs.find_unique_attr e.attrs ~f:(function
@@ -1530,8 +1557,7 @@ let make (module M : Attrs.WITH_ITEMS) ctx =
               let ctx = ctx
             end) : S)
 
-let strings_of_item ~signature_only (bo : BackendOptions.t) m items
-    (item : item) :
+let strings_of_item (bo : BackendOptions.t) m items (item : item) :
     ([> `Impl of string | `Intf of string ] * [ `NoNewline | `Newline ]) list =
   let interface_mode' : Types.inclusion_kind =
     List.rev bo.interfaces
@@ -1549,8 +1575,7 @@ let strings_of_item ~signature_only (bo : BackendOptions.t) m items
     |> Option.value ~default:(Types.Excluded : Types.inclusion_kind)
   in
   let interface_mode =
-    signature_only
-    || not ([%matches? (Types.Excluded : Types.inclusion_kind)] interface_mode')
+    not ([%matches? (Types.Excluded : Types.inclusion_kind)] interface_mode')
   in
   let (module Print) =
     make m
@@ -1561,21 +1586,18 @@ let strings_of_item ~signature_only (bo : BackendOptions.t) m items
         line_width = bo.line_width;
       }
   in
-  let mk_impl = if interface_mode then fun i -> `Impl i else fun i -> `Impl i in
+  let mk_impl i = `Impl i in
   let mk_intf = if interface_mode then fun i -> `Intf i else fun i -> `Impl i in
   let no_impl =
-    signature_only
-    || [%matches? (Types.Included None' : Types.inclusion_kind)] interface_mode'
+    [%matches? (Types.Included None' : Types.inclusion_kind)] interface_mode'
   in
   Print.pitem item
   |> List.filter ~f:(function `Impl _ when no_impl -> false | _ -> true)
   |> List.concat_map ~f:(function
        | `Impl i -> [ (mk_impl (Print.decl_to_string i), `Newline) ]
        | `Intf i -> [ (mk_intf (Print.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) ]
+       | `VerbatimIntf (s, nl) -> [ (mk_intf s, nl) ]
+       | `VerbatimImpl (s, nl) -> [ (`Impl s, nl) ]
        | `Comment s ->
            let s = "(* " ^ s ^ " *)" in
            if interface_mode then [ (`Impl s, `Newline); (`Intf s, `Newline) ]
@@ -1583,8 +1605,8 @@ let strings_of_item ~signature_only (bo : BackendOptions.t) m items
 
 type rec_prefix = NonRec | FirstMutRec | MutRec
 
-let string_of_items ~signature_only ~mod_name ~bundles (bo : BackendOptions.t) m
-    items : string * string =
+let string_of_items ~mod_name ~bundles (bo : BackendOptions.t) m items :
+    string * string =
   let collect_trait_goal_idents =
     object
       inherit [_] Visitors.reduce as super
@@ -1657,7 +1679,7 @@ let string_of_items ~signature_only ~mod_name ~bundles (bo : BackendOptions.t) m
     List.concat_map
       ~f:(fun item ->
         let recursivity_prefix = get_recursivity_prefix item in
-        let strs = strings_of_item ~signature_only bo m items item in
+        let strs = strings_of_item bo m items item in
         match (recursivity_prefix, item.v) with
         | FirstMutRec, Fn _ ->
             replace_in_strs ~pattern:"let" ~with_:"let rec" strs
@@ -1710,20 +1732,8 @@ let translate_as_fstar m (bo : BackendOptions.t) ~(bundles : AST.item list list)
   U.group_items_by_namespace items
   |> Map.to_alist
   |> List.concat_map ~f:(fun (ns, items) ->
-         let signature_only =
-           let is_dropped_body =
-             Concrete_ident.eq_name Rust_primitives__hax__dropped_body
-           in
-           let contains_dropped_body =
-             U.Reducers.collect_concrete_idents#visit_item ()
-             >> Set.exists ~f:is_dropped_body
-           in
-           List.exists ~f:contains_dropped_body items
-         in
          let mod_name = module_name ns in
-         let impl, intf =
-           string_of_items ~signature_only ~mod_name ~bundles bo m items
-         in
+         let impl, intf = string_of_items ~mod_name ~bundles bo m items in
          let make ~ext body =
            if String.is_empty body then None
            else
diff --git a/engine/backends/proverif/proverif_backend.ml b/engine/backends/proverif/proverif_backend.ml
index 3b1c6e56b..95778622b 100644
--- a/engine/backends/proverif/proverif_backend.ml
+++ b/engine/backends/proverif/proverif_backend.ml
@@ -630,8 +630,7 @@ module Make (Options : OPTS) : MAKE = struct
               if
                 Attrs.find_unique_attr item.attrs
                   ~f:
-                    ([%eq: Types.ha_payload] OpaqueType
-                    >> Fn.flip Option.some_if ())
+                    ([%eq: Types.ha_payload] Erased >> Fn.flip Option.some_if ())
                 |> Option.is_some
               then default_lines
               else default_lines ^^ destructor_lines
diff --git a/engine/bin/lib.ml b/engine/bin/lib.ml
index 944089d01..5695dd087 100644
--- a/engine/bin/lib.ml
+++ b/engine/bin/lib.ml
@@ -36,14 +36,14 @@ let import_thir_items (include_clauses : Types.inclusion_clause list)
             include_clauses
           |> List.last
         in
-        let drop_body =
+        let type_only =
           (* Shall we drop the body? *)
           Option.map
             ~f:(fun clause -> [%matches? Types.SignatureOnly] clause.kind)
             most_precise_clause
           |> Option.value ~default:false
         in
-        Import_thir.import_item ~drop_body item)
+        Import_thir.import_item ~type_only item)
       items
     |> List.map ~f:snd
   in
diff --git a/engine/lib/import_thir.ml b/engine/lib/import_thir.ml
index f1f2550db..eb0cd442b 100644
--- a/engine/lib/import_thir.ml
+++ b/engine/lib/import_thir.ml
@@ -1440,29 +1440,66 @@ let cast_of_enum typ_name generics typ thir_span
   in
   { v; span; ident; attrs = [] }
 
-let rec c_item ~ident ~drop_body (item : Thir.item) : item list =
+let rec c_item ~ident ~type_only (item : Thir.item) : item list =
   try
     Span.with_owner_hint item.owner_id (fun _ ->
-        c_item_unwrapped ~ident ~drop_body item)
+        c_item_unwrapped ~ident ~type_only item)
   with Diagnostics.SpanFreeError.Exn payload ->
     let context, kind = Diagnostics.SpanFreeError.payload payload in
     let error = Diagnostics.pretty_print_context_kind context kind in
     let span = Span.of_thir item.span in
     [ make_hax_error_item span ident error ]
 
-and c_item_unwrapped ~ident ~drop_body (item : Thir.item) : item list =
+and c_item_unwrapped ~ident ~type_only (item : Thir.item) : item list =
   let open (val make ~krate:item.owner_id.contents.value.krate : EXPR) in
   if should_skip item.attributes then []
   else
     let span = Span.of_thir item.span in
     let attrs = c_item_attrs item.attributes in
+    (* this is true if the user explicilty requested to erase using the `opaque` macro *)
+    let erased_by_user attrs =
+      Attr_payloads.payloads attrs
+      |> List.exists ~f:(fst >> [%matches? (Erased : Types.ha_payload)])
+    in
+    let item_erased_by_user = erased_by_user attrs in
+    let type_only =
+      type_only
+      && Attr_payloads.payloads attrs
+         |> List.exists ~f:(fst >> [%matches? (NeverErased : Types.ha_payload)])
+         |> not
+    in
+    (* This is true if the item should be erased because we are in type-only mode
+       (Only certain kinds of items are erased in this case). *)
+    let erased_by_type_only =
+      type_only
+      &&
+      match item.kind with
+      | Fn _ | Static _ -> true
+      | Impl { of_trait = Some _; items; _ }
+        when List.exists items ~f:(fun item ->
+                 match item.kind with Type _ -> true | _ -> false)
+             |> not ->
+          true
+      | _ -> false
+    in
+    (* If the item is erased in type-only mode we need to add the Erased attribute.
+       It is already present if the item is erased by user. *)
+    let attrs_with_erased erased_by_type_only erased_by_user attrs =
+      if erased_by_type_only && not erased_by_user then
+        Attr_payloads.to_attr Erased span :: attrs
+      else attrs
+    in
+    let attrs =
+      attrs_with_erased erased_by_type_only item_erased_by_user attrs
+    in
+    let erased = item_erased_by_user || erased_by_type_only in
+
     let mk_one v = { span; v; ident; attrs } in
     let mk v = [ mk_one v ] in
     let drop_body =
-      drop_body
+      erased
       && Attr_payloads.payloads attrs
-         |> List.exists
-              ~f:(fst >> [%matches? (NeverDropBody : Types.ha_payload)])
+         |> List.exists ~f:(fst >> [%matches? (NeverErased : Types.ha_payload)])
          |> not
     in
     let c_body = if drop_body then c_expr_drop_body else c_expr in
@@ -1475,7 +1512,7 @@ and c_item_unwrapped ~ident ~drop_body (item : Thir.item) : item list =
                name =
                  Concrete_ident.of_def_id Value (Option.value_exn item.def_id);
                generics = c_generics generics;
-               body = c_expr body;
+               body = c_body body;
                params = [];
                safety = Safe;
              }
@@ -1499,6 +1536,12 @@ and c_item_unwrapped ~ident ~drop_body (item : Thir.item) : item list =
                params = c_fn_params item.span params;
                safety = csafety safety;
              }
+    | (Enum (_, generics, _) | Struct (_, generics)) when erased ->
+        let generics = c_generics generics in
+        let is_struct = match item.kind with Struct _ -> true | _ -> false in
+        let def_id = Option.value_exn item.def_id in
+        let name = Concrete_ident.of_def_id Type def_id in
+        mk @@ Type { name; generics; variants = []; is_struct }
     | Enum (variants, generics, repr) ->
         let def_id = Option.value_exn item.def_id in
         let generics = c_generics generics in
@@ -1628,6 +1671,13 @@ and c_item_unwrapped ~ident ~drop_body (item : Thir.item) : item list =
         List.map
           ~f:(fun (item : Thir.impl_item) ->
             let item_def_id = Concrete_ident.of_def_id Impl item.owner_id in
+            let attrs = c_item_attrs item.attributes in
+            let sub_item_erased_by_user = erased_by_user attrs in
+            let sub_item_erased = sub_item_erased_by_user || type_only in
+            let attrs =
+              attrs_with_erased type_only sub_item_erased_by_user attrs
+            in
+            let c_body = if sub_item_erased then c_expr_drop_body else c_body in
 
             let v =
               match (item.kind : Thir.impl_item_kind) with
@@ -1663,7 +1713,6 @@ and c_item_unwrapped ~ident ~drop_body (item : Thir.item) : item list =
                      (https://doc.rust-lang.org/reference/items/implementations.html#inherent-implementations)."
             in
             let ident = Concrete_ident.of_def_id Value item.owner_id in
-            let attrs = c_item_attrs item.attributes in
             { span = Span.of_thir item.span; v; ident; attrs })
           items
     | Impl
@@ -1681,11 +1730,66 @@ and c_item_unwrapped ~ident ~drop_body (item : Thir.item) : item list =
             ~f:(fun { attributes; _ } -> not (should_skip attributes))
             items
         in
-        let has_type =
-          List.exists items ~f:(fun item ->
-              match item.kind with Type _ -> true | _ -> false)
+        let items =
+          if erased then
+            [
+              (* Dummy associated item *)
+              {
+                ii_span = Span.of_thir item.span;
+                ii_generics = { params = []; constraints = [] };
+                ii_v =
+                  IIFn
+                    {
+                      body = U.unit_expr span;
+                      params = [ U.make_unit_param span ];
+                    };
+                ii_ident =
+                  Concrete_ident.of_name Value
+                    Rust_primitives__hax__dropped_body;
+                ii_attrs = [];
+              };
+            ]
+          else
+            List.map
+              ~f:(fun (item : Thir.impl_item) ->
+                (* TODO: introduce a Kind.TraitImplItem or
+                   something. Otherwise we have to assume every
+                   backend will see traits and impls as
+                   records. See https://github.com/hacspec/hax/issues/271. *)
+                let ii_ident = Concrete_ident.of_def_id Field item.owner_id in
+                {
+                  ii_span = Span.of_thir item.span;
+                  ii_generics = c_generics item.generics;
+                  ii_v =
+                    (match (item.kind : Thir.impl_item_kind) with
+                    | Fn { body; params; _ } ->
+                        let params =
+                          if List.is_empty params then
+                            [ U.make_unit_param span ]
+                          else List.map ~f:(c_param item.span) params
+                        in
+                        IIFn { body = c_expr body; params }
+                    | Const (_ty, e) -> IIFn { body = c_expr e; params = [] }
+                    | Type { ty; parent_bounds } ->
+                        IIType
+                          {
+                            typ = c_ty item.span ty;
+                            parent_bounds =
+                              List.filter_map
+                                ~f:(fun (clause, impl_expr, span) ->
+                                  let* bound = c_clause span clause in
+                                  match bound with
+                                  | GCType trait_goal ->
+                                      Some
+                                        (c_impl_expr span impl_expr, trait_goal)
+                                  | _ -> None)
+                                parent_bounds;
+                          });
+                  ii_ident;
+                  ii_attrs = c_item_attrs item.attributes;
+                })
+              items
         in
-        let c_e = if has_type then c_expr else c_body in
         mk
         @@ Impl
              {
@@ -1695,49 +1799,7 @@ and c_item_unwrapped ~ident ~drop_body (item : Thir.item) : item list =
                  ( Concrete_ident.of_def_id Trait of_trait.def_id,
                    List.map ~f:(c_generic_value item.span) of_trait.generic_args
                  );
-               items =
-                 List.map
-                   ~f:(fun (item : Thir.impl_item) ->
-                     (* TODO: introduce a Kind.TraitImplItem or
-                        something. Otherwise we have to assume every
-                        backend will see traits and impls as
-                        records. See https://github.com/hacspec/hax/issues/271. *)
-                     let ii_ident =
-                       Concrete_ident.of_def_id Field item.owner_id
-                     in
-                     {
-                       ii_span = Span.of_thir item.span;
-                       ii_generics = c_generics item.generics;
-                       ii_v =
-                         (match (item.kind : Thir.impl_item_kind) with
-                         | Fn { body; params; _ } ->
-                             let params =
-                               if List.is_empty params then
-                                 [ U.make_unit_param span ]
-                               else List.map ~f:(c_param item.span) params
-                             in
-                             IIFn { body = c_e body; params }
-                         | Const (_ty, e) -> IIFn { body = c_e e; params = [] }
-                         | Type { ty; parent_bounds } ->
-                             IIType
-                               {
-                                 typ = c_ty item.span ty;
-                                 parent_bounds =
-                                   List.filter_map
-                                     ~f:(fun (clause, impl_expr, span) ->
-                                       let* bound = c_clause span clause in
-                                       match bound with
-                                       | GCType trait_goal ->
-                                           Some
-                                             ( c_impl_expr span impl_expr,
-                                               trait_goal )
-                                       | _ -> None)
-                                     parent_bounds;
-                               });
-                       ii_ident;
-                       ii_attrs = c_item_attrs item.attributes;
-                     })
-                   items;
+               items;
                parent_bounds =
                  List.filter_map
                    ~f:(fun (clause, impl_expr, span) ->
@@ -1787,7 +1849,7 @@ and c_item_unwrapped ~ident ~drop_body (item : Thir.item) : item list =
     | TraitAlias _ ->
         mk NotImplementedYet
 
-let import_item ~drop_body (item : Thir.item) :
+let import_item ~type_only (item : Thir.item) :
     concrete_ident * (item list * Diagnostics.t list) =
   let ident = Concrete_ident.of_def_id Value item.owner_id in
   let r, reports =
@@ -1797,6 +1859,6 @@ let import_item ~drop_body (item : Thir.item) :
       >> U.Reducers.disambiguate_local_idents
     in
     Diagnostics.Core.capture (fun _ ->
-        c_item item ~ident ~drop_body |> List.map ~f)
+        c_item item ~ident ~type_only |> List.map ~f)
   in
   (ident, (r, reports))
diff --git a/engine/lib/import_thir.mli b/engine/lib/import_thir.mli
index 42a5f2184..370af4c05 100644
--- a/engine/lib/import_thir.mli
+++ b/engine/lib/import_thir.mli
@@ -5,6 +5,6 @@ val import_clause :
   Types.span -> Types.clause -> Ast.Rust.generic_constraint option
 
 val import_item :
-  drop_body:bool ->
+  type_only:bool ->
   Types.item_for__decorated_for__expr_kind ->
   Concrete_ident.t * (Ast.Rust.item list * Diagnostics.t list)
diff --git a/hax-lib/macros/src/dummy.rs b/hax-lib/macros/src/dummy.rs
index 5134763c6..429e04dea 100644
--- a/hax-lib/macros/src/dummy.rs
+++ b/hax-lib/macros/src/dummy.rs
@@ -29,7 +29,9 @@ identity_proc_macro_attribute!(
     process_init,
     process_write,
     process_read,
+    opaque,
     opaque_type,
+    transparent,
     refinement_type,
     fstar_replace,
     coq_replace,
diff --git a/hax-lib/macros/src/implementation.rs b/hax-lib/macros/src/implementation.rs
index f71f1891c..2189232c7 100644
--- a/hax-lib/macros/src/implementation.rs
+++ b/hax-lib/macros/src/implementation.rs
@@ -249,8 +249,8 @@ pub fn lemma(attr: pm::TokenStream, item: pm::TokenStream) -> pm::TokenStream {
             );
         }
     }
-    use AttrPayload::NeverDropBody;
-    quote! { #attr #NeverDropBody #item }.into()
+    use AttrPayload::NeverErased;
+    quote! { #attr #NeverErased #item }.into()
 }
 
 /*
@@ -617,13 +617,32 @@ pub fn attributes(_attr: pm::TokenStream, item: pm::TokenStream) -> pm::TokenStr
     quote! { #item #(#extra_items)* }.into()
 }
 
-/// Mark a struct or an enum opaque: the extraction will assume the
+/// Mark an item opaque: the extraction will assume the
 /// type without revealing its definition.
 #[proc_macro_error]
 #[proc_macro_attribute]
-pub fn opaque_type(_attr: pm::TokenStream, item: pm::TokenStream) -> pm::TokenStream {
+#[deprecated(note = "Please use 'opaque' instead")]
+pub fn opaque_type(attr: pm::TokenStream, item: pm::TokenStream) -> pm::TokenStream {
+    opaque(attr, item)
+}
+
+/// Mark an item opaque: the extraction will assume the
+/// type without revealing its definition.
+#[proc_macro_error]
+#[proc_macro_attribute]
+pub fn opaque(_attr: pm::TokenStream, item: pm::TokenStream) -> pm::TokenStream {
+    let item: Item = parse_macro_input!(item);
+    let attr = AttrPayload::Erased;
+    quote! {#attr #item}.into()
+}
+
+/// Mark an item transparent: the extraction will not
+/// make it opaque regardless of the `-i` flag default.
+#[proc_macro_error]
+#[proc_macro_attribute]
+pub fn transparent(_attr: pm::TokenStream, item: pm::TokenStream) -> pm::TokenStream {
     let item: Item = parse_macro_input!(item);
-    let attr = AttrPayload::OpaqueType;
+    let attr = AttrPayload::NeverErased;
     quote! {#attr #item}.into()
 }
 
diff --git a/hax-lib/macros/src/quote.rs b/hax-lib/macros/src/quote.rs
index d02bdea78..8d13591c4 100644
--- a/hax-lib/macros/src/quote.rs
+++ b/hax-lib/macros/src/quote.rs
@@ -141,14 +141,14 @@ pub(super) fn item(
     };
     let kind_attr = AttrPayload::ItemQuote(kind);
     let status_attr = AttrPayload::ItemStatus(ItemStatus::Included { late_skip: true });
-    use AttrPayload::NeverDropBody;
+    use AttrPayload::NeverErased;
     quote! {
         #assoc_attr
         #item
         #attribute_to_inject
         #status_attr
         const _: () = {
-            #NeverDropBody
+            #NeverErased
             #uid_attr
             #kind_attr
             fn quote_contents() {
diff --git a/hax-lib/macros/src/utils.rs b/hax-lib/macros/src/utils.rs
index c1c974a39..35fe0fa76 100644
--- a/hax-lib/macros/src/utils.rs
+++ b/hax-lib/macros/src/utils.rs
@@ -301,7 +301,7 @@ pub fn make_fn_decoration(
         } else {
             quote! {}
         };
-        use AttrPayload::NeverDropBody;
+        use AttrPayload::NeverErased;
         quote! {
             #[cfg(#DebugOrHaxCfgExpr)]
             #late_skip
@@ -312,7 +312,7 @@ pub fn make_fn_decoration(
                 #uid_attr
                 #late_skip
                 #[allow(unused)]
-                #NeverDropBody
+                #NeverErased
                 #decoration_sig {
                     #phi
                 }
diff --git a/hax-lib/macros/types/src/lib.rs b/hax-lib/macros/types/src/lib.rs
index bbb1d4575..b342a1355 100644
--- a/hax-lib/macros/types/src/lib.rs
+++ b/hax-lib/macros/types/src/lib.rs
@@ -118,7 +118,7 @@ pub enum AttrPayload {
     /// 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)
-    NeverDropBody,
+    NeverErased,
     NewtypeAsRefinement,
     /// Mark an item as a lemma statement to prove in the backend
     Lemma,
@@ -130,8 +130,8 @@ pub enum AttrPayload {
     PVConstructor,
     PVHandwritten,
     TraitMethodNoPrePost,
-    /// Make a type opaque
-    OpaqueType,
+    /// Make an item opaque
+    Erased,
 }
 
 pub const HAX_TOOL: &str = "_hax";
diff --git a/hax-lib/src/proc_macros.rs b/hax-lib/src/proc_macros.rs
index 866c7cfda..65136716f 100644
--- a/hax-lib/src/proc_macros.rs
+++ b/hax-lib/src/proc_macros.rs
@@ -2,8 +2,8 @@
 //! proc-macro crate cannot export anything but procedural macros.
 
 pub use hax_lib_macros::{
-    attributes, ensures, exclude, impl_fn_decoration, include, lemma, loop_invariant, opaque_type,
-    refinement_type, requires, trait_fn_decoration,
+    attributes, ensures, exclude, impl_fn_decoration, include, lemma, loop_invariant, opaque,
+    opaque_type, refinement_type, requires, trait_fn_decoration, transparent,
 };
 
 pub use hax_lib_macros::{
diff --git a/hax-types/src/cli_options/mod.rs b/hax-types/src/cli_options/mod.rs
index f84795be7..d8b1a6551 100644
--- a/hax-types/src/cli_options/mod.rs
+++ b/hax-types/src/cli_options/mod.rs
@@ -303,7 +303,8 @@ pub struct TranslationOptions {
 
     /// {n} - `+:`: only includes the type of the selected items (no
     /// dependencies). This includes full struct and enums, but only
-    /// the type signature of functions, dropping their bodies.
+    /// the type signature of functions and trait impls (except when
+    /// they contain associated types), dropping their bodies.
     #[arg(
         value_parser = parse_inclusion_clause,
         value_delimiter = ' ',


Test patch:
diff --git a/test-harness/src/snapshots/toolchain__attribute-opaque into-fstar.snap b/test-harness/src/snapshots/toolchain__attribute-opaque into-fstar.snap
index 2275da427..6373c0b9e 100644
--- a/test-harness/src/snapshots/toolchain__attribute-opaque into-fstar.snap
+++ b/test-harness/src/snapshots/toolchain__attribute-opaque into-fstar.snap
@@ -29,13 +29,124 @@ stderr = 'Finished `dev` profile [unoptimized + debuginfo] target(s) in XXs'
 diagnostics = []
 
 [stdout.files]
+"Attribute_opaque.fst" = '''
+module Attribute_opaque
+#set-options "--fuel 0 --ifuel 1 --z3rlimit 15"
+open Core
+open FStar.Mul
+
+assume
+val t_OpaqueEnum': v_X: usize -> v_T: Type0 -> v_U: Type0 -> eqtype
+
+let t_OpaqueEnum (v_X: usize) (v_T v_U: Type0) = t_OpaqueEnum' v_X v_T v_U
+
+assume
+val t_OpaqueStruct': v_X: usize -> v_T: Type0 -> v_U: Type0 -> eqtype
+
+let t_OpaqueStruct (v_X: usize) (v_T v_U: Type0) = t_OpaqueStruct' v_X v_T v_U
+
+assume
+val impl__S1__f_s1': Prims.unit -> Prims.Pure Prims.unit Prims.l_True (fun _ -> Prims.l_True)
+
+let impl__S1__f_s1 = impl__S1__f_s1'
+
+[@@ FStar.Tactics.Typeclasses.tcinstance]
+assume
+val impl_2': #v_U: Type0 -> {| i1: Core.Clone.t_Clone v_U |} -> t_TrGeneric i32 v_U
+
+let impl_2 (#v_U: Type0) (#[FStar.Tactics.Typeclasses.tcresolve ()] i1: Core.Clone.t_Clone v_U) =
+  impl_2' #v_U #i1
+
+assume
+val impl__S2__f_s2': Prims.unit -> Prims.Pure Prims.unit Prims.l_True (fun _ -> Prims.l_True)
+
+let impl__S2__f_s2 = impl__S2__f_s2'
+
+assume
+val v_C': u8
+
+let v_C = v_C'
+
+assume
+val f': x: bool -> y: bool -> Prims.Pure bool Prims.l_True (fun _ -> Prims.l_True)
+
+let f = f'
+
+assume
+val ff_generic': v_X: usize -> #v_T: Type0 -> #v_U: Type0 -> x: v_U
+  -> Prims.Pure (t_OpaqueEnum v_X v_T v_U) Prims.l_True (fun _ -> Prims.l_True)
+
+let ff_generic (v_X: usize) (#v_T #v_U: Type0) = ff_generic' v_X #v_T #v_U
+
+assume
+val ff_pre_post': x: bool -> y: bool
+  -> Prims.Pure bool
+      (requires x)
+      (ensures
+        fun result ->
+          let result:bool = result in
+          result =. y)
+
+let ff_pre_post = ff_pre_post'
+
+[@@ FStar.Tactics.Typeclasses.tcinstance]
+assume
+val impl_T_for_u8': t_T u8
+
+let impl_T_for_u8 = impl_T_for_u8'
+'''
 "Attribute_opaque.fsti" = '''
 module Attribute_opaque
 #set-options "--fuel 0 --ifuel 1 --z3rlimit 15"
 open Core
 open FStar.Mul
 
-val t_OpaqueEnum (v_X: usize) (#v_T #v_U: Type0) : Type0
+type t_S1 = | S1 : t_S1
+
+type t_S2 = | S2 : t_S2
+
+val t_OpaqueEnum (v_X: usize) (v_T v_U: Type0) : eqtype
+
+val t_OpaqueStruct (v_X: usize) (v_T v_U: Type0) : eqtype
+
+class t_TrGeneric (v_Self: Type0) (v_U: Type0) = {
+  [@@@ FStar.Tactics.Typeclasses.no_method]_super_6168282666194871449:Core.Clone.t_Clone v_U;
+  f_f_pre:v_U -> Type0;
+  f_f_post:v_U -> v_Self -> Type0;
+  f_f:x0: v_U -> Prims.Pure v_Self (f_f_pre x0) (fun result -> f_f_post x0 result)
+}
+
+val impl__S1__f_s1: Prims.unit -> Prims.Pure Prims.unit Prims.l_True (fun _ -> Prims.l_True)
+
+[@@ FStar.Tactics.Typeclasses.tcinstance]
+val impl_2 (#v_U: Type0) {| i1: Core.Clone.t_Clone v_U |} : t_TrGeneric i32 v_U
+
+val impl__S2__f_s2: Prims.unit -> Prims.Pure Prims.unit Prims.l_True (fun _ -> Prims.l_True)
+
+val f (x y: bool) : Prims.Pure bool Prims.l_True (fun _ -> Prims.l_True)
+
+val ff_generic (v_X: usize) (#v_T #v_U: Type0) (x: v_U)
+    : Prims.Pure (t_OpaqueEnum v_X v_T v_U) Prims.l_True (fun _ -> Prims.l_True)
+
+val ff_pre_post (x y: bool)
+    : Prims.Pure bool
+      (requires x)
+      (ensures
+        fun result ->
+          let result:bool = result in
+          result =. y)
+
+class t_T (v_Self: Type0) = {
+  f_U:Type0;
+  f_c:u8;
+  f_d_pre:Prims.unit -> Type0;
+  f_d_post:Prims.unit -> Prims.unit -> Type0;
+  f_d:x0: Prims.unit -> Prims.Pure Prims.unit (f_d_pre x0) (fun result -> f_d_post x0 result);
+  f_m_pre:self___: v_Self -> x: u8 -> pred: Type0{x =. 0uy ==> pred};
+  f_m_post:v_Self -> u8 -> bool -> Type0;
+  f_m:x0: v_Self -> x1: u8 -> Prims.Pure bool (f_m_pre x0 x1) (fun result -> f_m_post x0 x1 result)
+}
 
-val t_OpaqueStruct (v_X: usize) (#v_T #v_U: Type0) : Type0
+[@@ FStar.Tactics.Typeclasses.tcinstance]
+val impl_T_for_u8:t_T u8
 '''
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 9aaa938a6..dcdee90a4 100644
--- a/test-harness/src/snapshots/toolchain__interface-only into-fstar.snap
+++ b/test-harness/src/snapshots/toolchain__interface-only into-fstar.snap
@@ -27,7 +27,7 @@ stderr = 'Finished `dev` profile [unoptimized + debuginfo] target(s) in XXs'
 diagnostics = []
 
 [stdout.files]
-"Interface_only.fsti" = '''
+"Interface_only.fst" = '''
 module Interface_only
 #set-options "--fuel 0 --ifuel 1 --z3rlimit 15"
 open Core
@@ -39,34 +39,89 @@ type t_Holder (v_T: Type0) = { f_value:Alloc.Vec.t_Vec v_T Alloc.Alloc.t_Global
 
 type t_Param (v_SIZE: usize) = { f_value:t_Array u8 v_SIZE }
 
+class t_T2 (v_Self: Type0) = {
+  f_d_pre:Prims.unit -> Type0;
+  f_d_post:Prims.unit -> Prims.unit -> Type0;
+  f_d:x0: Prims.unit -> Prims.Pure Prims.unit (f_d_pre x0) (fun result -> f_d_post x0 result)
+}
+
+/// Items can be forced to be transparent
+[@@ FStar.Tactics.Typeclasses.tcinstance]
+let impl_T2_for_u8: t_T2 u8 =
+  {
+    f_d_pre = (fun (_: Prims.unit) -> false);
+    f_d_post = (fun (_: Prims.unit) (out: Prims.unit) -> true);
+    f_d = fun (_: Prims.unit) -> ()
+  }
+
 /// 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]
-val impl:Core.Convert.t_From t_Bar Prims.unit
+assume
+val impl': Core.Convert.t_From t_Bar Prims.unit
+
+let impl = impl'
 
 /// If you need to drop the body of a method, please hoist it:
 [@@ FStar.Tactics.Typeclasses.tcinstance]
-val impl_1:Core.Convert.t_From t_Bar u8
+assume
+val impl_1': Core.Convert.t_From t_Bar u8
 
-val from__from: u8 -> Prims.Pure t_Bar Prims.l_True (fun _ -> Prims.l_True)
+let impl_1 = impl_1'
+
+assume
+val from__from': u8 -> t_Bar
+
+let from__from = from__from'
 
 [@@ FStar.Tactics.Typeclasses.tcinstance]
-val impl_2 (#v_T: Type0) : Core.Convert.t_From (t_Holder v_T) Prims.unit
+assume
+val impl_2': #v_T: Type0 -> Core.Convert.t_From (t_Holder v_T) Prims.unit
+
+let impl_2 (#v_T: Type0) = impl_2' #v_T
 
 [@@ FStar.Tactics.Typeclasses.tcinstance]
-val impl_3 (v_SIZE: usize) : Core.Convert.t_From (t_Param v_SIZE) Prims.unit
+assume
+val impl_3': v_SIZE: usize -> Core.Convert.t_From (t_Param v_SIZE) Prims.unit
+
+let impl_3 (v_SIZE: usize) = impl_3' v_SIZE
 
 /// 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))
+assume
+val f': x: u8
+  -> Prims.Pure (t_Array u8 (sz 4))
       (requires x <. 254uy)
       (ensures
         fun r ->
           let r:t_Array u8 (sz 4) = r in
           (r.[ sz 0 ] <: u8) >. x)
+
+let f = f'
+
+assume
+val ff_generic': v_X: usize -> #v_U: Type0 -> v__x: v_U -> t_Param v_X
+
+let ff_generic (v_X: usize) (#v_U: Type0) = ff_generic' v_X #v_U
+
+class t_T (v_Self: Type0) = {
+  f_Assoc:Type0;
+  f_d_pre:Prims.unit -> Type0;
+  f_d_post:Prims.unit -> Prims.unit -> Type0;
+  f_d:x0: Prims.unit -> Prims.Pure Prims.unit (f_d_pre x0) (fun result -> f_d_post x0 result)
+}
+
+/// Impls with associated types are not erased
+[@@ FStar.Tactics.Typeclasses.tcinstance]
+let impl_T_for_u8: t_T u8 =
+  {
+    f_Assoc = u8;
+    f_d_pre = (fun (_: Prims.unit) -> true);
+    f_d_post = (fun (_: Prims.unit) (out: Prims.unit) -> true);
+    f_d = fun (_: Prims.unit) -> ()
+  }
 '''
diff --git a/tests/attribute-opaque/src/lib.rs b/tests/attribute-opaque/src/lib.rs
index 7840b4fa8..28671f800 100644
--- a/tests/attribute-opaque/src/lib.rs
+++ b/tests/attribute-opaque/src/lib.rs
@@ -1,11 +1,85 @@
-#[hax_lib::opaque_type]
+#[hax_lib::opaque]
 struct OpaqueStruct<const X: usize, T, U> {
     field: [T; X],
     other_field: U,
 }
 
-#[hax_lib::opaque_type]
+#[hax_lib::opaque]
 enum OpaqueEnum<const X: usize, T, U> {
     A([T; X]),
     B(U),
 }
+
+#[hax_lib::opaque]
+fn f_generic<const X: usize, T, U>(x: U) -> OpaqueEnum<X, T, U> {
+    OpaqueEnum::B(x)
+}
+
+#[hax_lib::opaque]
+fn f(x: bool, y: bool) -> bool {
+    x && y
+}
+
+#[hax_lib::opaque]
+#[hax_lib::requires(x)]
+#[hax_lib::ensures(|result| result == y)]
+fn f_pre_post(x: bool, y: bool) -> bool {
+    x && y
+}
+
+#[hax_lib::attributes]
+trait T {
+    type U;
+    const c: u8;
+    fn d();
+    #[hax_lib::requires(x == 0)]
+    fn m(&self, x: u8) -> bool;
+}
+
+#[hax_lib::attributes]
+#[hax_lib::opaque]
+impl T for u8 {
+    type U = u8;
+    const c: u8 = 0;
+    fn d() {
+        unsafe {
+            let my_num: i32 = 10;
+            let _my_num_ptr: *const i32 = &my_num;
+            let mut my_speed: i32 = 88;
+            let _my_speed_ptr: *mut i32 = &mut my_speed;
+        }
+    }
+    #[hax_lib::requires(x == 0)]
+    #[hax_lib::ensures(|result| result)]
+    fn m(&self, x: u8) -> bool {
+        *self >= x
+    }
+}
+
+trait TrGeneric<U: Clone> {
+    fn f(x: U) -> Self;
+}
+
+#[hax_lib::opaque]
+impl<U: Clone> TrGeneric<U> for i32 {
+    fn f(_x: U) -> Self {
+        0
+    }
+}
+
+#[hax_lib::opaque]
+const C: u8 = 0 + 0;
+
+struct S1();
+
+impl S1 {
+    #[hax_lib::opaque]
+    fn f_s1() {}
+}
+
+struct S2();
+
+#[hax_lib::opaque]
+impl S2 {
+    fn f_s2() {}
+}
diff --git a/tests/cli/interface-only/src/lib.rs b/tests/cli/interface-only/src/lib.rs
index 411c3de99..1e85ef7fe 100644
--- a/tests/cli/interface-only/src/lib.rs
+++ b/tests/cli/interface-only/src/lib.rs
@@ -65,3 +65,29 @@ impl<const SIZE: usize> From<()> for Param<SIZE> {
         Param { value: [0; SIZE] }
     }
 }
+
+fn f_generic<const X: usize, U>(_x: U) -> Param<X> {
+    Param { value: [0; X] }
+}
+
+trait T {
+    type Assoc;
+    fn d();
+}
+
+/// Impls with associated types are not erased
+impl T for u8 {
+    type Assoc = u8;
+    fn d() {}
+}
+trait T2 {
+    fn d();
+}
+
+/// Items can be forced to be transparent
+#[hax_lib::transparent]
+#[hax_lib::attributes]
+impl T2 for u8 {
+    #[hax_lib::requires(false)]
+    fn d() {}
+}