Document and correct.

engine/lib/import_thir.ml

@@ -1456,11 +1456,14 @@ and c_item_unwrapped ~ident ~type_only (item : Thir.item) : item list =
   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
+    (* 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
       &&
@@ -1473,6 +1476,8 @@ and c_item_unwrapped ~ident ~type_only (item : Thir.item) : item list =
           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 =
       if erased_by_type_only && not item_erased_by_user then
         Attr_payloads.to_attr Erased span :: attrs
@@ -1718,6 +1723,7 @@ and c_item_unwrapped ~ident ~type_only (item : Thir.item) : item list =
         let items =
           if erased then
             [
+              (* Dummy associated item *)
               {
                 ii_span = Span.of_thir item.span;
                 ii_generics = { params = []; constraints = [] };

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

@@ -130,7 +130,7 @@ pub enum AttrPayload {
     PVConstructor,
     PVHandwritten,
     TraitMethodNoPrePost,
-    /// Make something opaque
+    /// Make an item opaque
     Erased,
 }
 

test-harness/src/snapshots/toolchain__attribute-opaque into-fstar.snap

@@ -23,23 +23,7 @@ info:
       - +**
 ---
 exit = 0
-stderr = '''
-warning: use of deprecated macro `hax_lib::opaque_type`: Please use 'opaque' instead
- --> attribute-opaque/src/lib.rs:1:3
-  |
-1 | #[hax_lib::opaque_type]
-  |   ^^^^^^^^^^^^^^^^^^^^
-  |
-  = note: `#[warn(deprecated)]` on by default
-
-warning: use of deprecated macro `hax_lib::opaque_type`: Please use 'opaque' instead
- --> attribute-opaque/src/lib.rs:7:3
-  |
-7 | #[hax_lib::opaque_type]
-  |   ^^^^^^^^^^^^^^^^^^^^
-
-warning: `attribute-opaque` (lib) generated 2 warnings
-    Finished `dev` profile [unoptimized + debuginfo] target(s) in XXs'''
+stderr = 'Finished `dev` profile [unoptimized + debuginfo] target(s) in XXs'
 
 [stdout]
 diagnostics = []
@@ -51,6 +35,11 @@ module Attribute_opaque
 open Core
 open FStar.Mul
 
+assume
+val f': x: bool -> y: bool -> Prims.Pure bool Prims.l_True (fun _ -> Prims.l_True)
+
+let f = f'
+
 [@@ FStar.Tactics.Typeclasses.tcinstance]
 assume
 val impl_T_for_u8': t_T u8
@@ -61,32 +50,27 @@ assume
 val c': u8
 
 let c = c'
-
-assume
-val f': x: bool -> y: bool -> Prims.Pure bool Prims.l_True (fun _ -> Prims.l_True)
-
-let f = f'
 '''
 "Attribute_opaque.fsti" = '''
 module Attribute_opaque
 #set-options "--fuel 0 --ifuel 1 --z3rlimit 15"
 open Core
 open FStar.Mul
 
+val t_OpaqueStruct (v_X: usize) (#v_T #v_U: Type0) : Type0
+
+val t_OpaqueEnum (v_X: usize) (#v_T #v_U: Type0) : Type0
+
+val f (x y: bool) : Prims.Pure bool Prims.l_True (fun _ -> Prims.l_True)
+
 class t_T (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)
 }
 
-val t_OpaqueEnum (v_X: usize) (#v_T #v_U: Type0) : Type0
-
-val t_OpaqueStruct (v_X: usize) (#v_T #v_U: Type0) : Type0
-
 [@@ FStar.Tactics.Typeclasses.tcinstance]
 val impl_T_for_u8:t_T u8
 
 val c:u8
-
-val f (x y: bool) : Prims.Pure bool Prims.l_True (fun _ -> Prims.l_True)
 '''

test-harness/src/snapshots/toolchain__interface-only into-fstar.snap

@@ -33,11 +33,31 @@ module Interface_only
 open Core
 open FStar.Mul
 
-type t_Bar = | Bar : t_Bar
+/// 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)
+      (ensures
+        fun r ->
+          let r:t_Array u8 (sz 4) = r in
+          (r.[ sz 0 ] <: u8) >. x)
 
-type t_Holder (v_T: Type0) = { f_value:Alloc.Vec.t_Vec v_T Alloc.Alloc.t_Global }
+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)
 
-type t_Param (v_SIZE: usize) = { f_value:t_Array u8 v_SIZE }
+let f = f'
+
+type t_Bar = | Bar : t_Bar
 
 /// Non-inherent implementations are extracted, their bodies are not
 /// dropped. This might be a bit surprising: see
@@ -68,6 +88,8 @@ val from__from': u8 -> t_Bar
 
 let from__from = from__from'
 
+type t_Holder (v_T: Type0) = { f_value:Alloc.Vec.t_Vec v_T Alloc.Alloc.t_Global }
+
 [@@ FStar.Tactics.Typeclasses.tcinstance]
 val impl_2 (#v_T: Type0) : Core.Convert.t_From (t_Holder v_T) Prims.unit
 
@@ -77,6 +99,8 @@ val impl_2': #v_T: Type0 -> Core.Convert.t_From (t_Holder v_T) Prims.unit
 
 let impl_2 = impl_2'
 
+type t_Param (v_SIZE: usize) = { f_value:t_Array u8 v_SIZE }
+
 [@@ FStar.Tactics.Typeclasses.tcinstance]
 val impl_3 (v_SIZE: usize) : Core.Convert.t_From (t_Param v_SIZE) Prims.unit
 
@@ -85,28 +109,4 @@ assume
 val impl_3': v_SIZE: usize -> Core.Convert.t_From (t_Param v_SIZE) Prims.unit
 
 let impl_3 = impl_3'
-
-/// 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)
-      (ensures
-        fun r ->
-          let r:t_Array u8 (sz 4) = r in
-          (r.[ sz 0 ] <: u8) >. x)
-
-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'
 '''

tests/attribute-opaque/src/lib.rs

@@ -1,10 +1,10 @@
-#[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),