Updated tests.

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

@@ -35,21 +35,55 @@ module Attribute_opaque
 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
+
 [@@ FStar.Tactics.Typeclasses.tcinstance]
 assume
 val impl_T_for_u8': t_T u8
 
 let impl_T_for_u8 = impl_T_for_u8'
 
+[@@ FStar.Tactics.Typeclasses.tcinstance]
 assume
-val c': u8
+val impl_1': #v_U: Type0 -> {| i1: Core.Clone.t_Clone v_U |} -> t_TrGeneric i32 v_U
 
-let c = c'
+let impl_1 (#v_U: Type0) (#[FStar.Tactics.Typeclasses.tcresolve ()] i1: Core.Clone.t_Clone v_U) =
+  impl_1' #v_U #i1
+
+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'
 '''
 "Attribute_opaque.fsti" = '''
 module Attribute_opaque
@@ -63,12 +97,33 @@ class t_T (v_Self: 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_OpaqueEnum (v_X: usize) (v_T v_U: Type0) : eqtype
 
-val t_OpaqueStruct (v_X: usize) (#v_T #v_U: Type0) : Type0
+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)
+}
 
 [@@ FStar.Tactics.Typeclasses.tcinstance]
 val impl_T_for_u8:t_T u8
 
+[@@ FStar.Tactics.Typeclasses.tcinstance]
+val impl_1 (#v_U: Type0) {| i1: Core.Clone.t_Clone v_U |} : t_TrGeneric i32 v_U
+
 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)
 '''

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

@@ -39,6 +39,21 @@ 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.
@@ -73,7 +88,7 @@ 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 = impl_2'
+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
@@ -82,7 +97,7 @@ 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 = impl_3'
+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 `+:`
@@ -99,4 +114,26 @@ val f': x: u8
           (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) -> ()
+  }
 '''

tests/attribute-opaque/src/lib.rs

@@ -10,10 +10,23 @@ enum OpaqueEnum<const X: usize, T, U> {
     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
+}
+
 trait T {
     fn d();
 }
@@ -23,12 +36,23 @@ impl T for u8 {
     fn d() {
         unsafe {
             let my_num: i32 = 10;
-            let my_num_ptr: *const i32 = &my_num;
+            let _my_num_ptr: *const i32 = &my_num;
             let mut my_speed: i32 = 88;
-            let my_speed_ptr: *mut i32 = &mut my_speed;
+            let _my_speed_ptr: *mut i32 = &mut my_speed;
         }
     }
 }
 
+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;
+const C: u8 = 0 + 0;

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() {}
+}