Tests for new behaviour of interface-only + new opaque attribute.

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

@@ -23,19 +23,70 @@ info:
       - +**
 ---
 exit = 0
-stderr = 'Finished `dev` profile [unoptimized + debuginfo] target(s) in XXs'
+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'''
 
 [stdout]
 diagnostics = []
 
 [stdout.files]
+"Attribute_opaque.fst" = '''
+module Attribute_opaque
+#set-options "--fuel 0 --ifuel 1 --z3rlimit 15"
+open Core
+open FStar.Mul
+
+[@@ FStar.Tactics.Typeclasses.tcinstance]
+assume
+val impl_T_for_u8': t_T u8
+
+let impl_T_for_u8 = impl_T_for_u8'
+
+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
 
+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

@@ -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
@@ -45,18 +45,47 @@ type t_Param (v_SIZE: usize) = { f_value:t_Array u8 v_SIZE }
 [@@ FStar.Tactics.Typeclasses.tcinstance]
 val impl:Core.Convert.t_From t_Bar Prims.unit
 
+[@@ FStar.Tactics.Typeclasses.tcinstance]
+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
 
-val from__from: u8 -> Prims.Pure t_Bar Prims.l_True (fun _ -> Prims.l_True)
+[@@ FStar.Tactics.Typeclasses.tcinstance]
+assume
+val impl_1': Core.Convert.t_From t_Bar u8
+
+let impl_1 = impl_1'
+
+val from__from: u8 -> t_Bar
+
+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
 
+[@@ FStar.Tactics.Typeclasses.tcinstance]
+assume
+val impl_2': #v_T: Type0 -> Core.Convert.t_From (t_Holder v_T) Prims.unit
+
+let impl_2 = impl_2'
+
 [@@ FStar.Tactics.Typeclasses.tcinstance]
 val impl_3 (v_SIZE: usize) : Core.Convert.t_From (t_Param v_SIZE) Prims.unit
 
+[@@ FStar.Tactics.Typeclasses.tcinstance]
+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.
@@ -69,4 +98,15 @@ val f (x: u8)
         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

@@ -31,4 +31,4 @@ impl T for u8 {
 }
 
 #[hax_lib::opaque]
-const c: u8 = { 0 + 0 };
+const c: u8 = 0 + 0;