New tests snapshots.

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

@@ -35,11 +35,6 @@ 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
@@ -50,25 +45,30 @@ 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 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,23 +33,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.
-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_Bar = | Bar : t_Bar
 
-let f = f'
+type t_Holder (v_T: Type0) = { f_value:Alloc.Vec.t_Vec v_T Alloc.Alloc.t_Global }
 
-type t_Bar = | Bar : t_Bar
+type t_Param (v_SIZE: usize) = { f_value:t_Array u8 v_SIZE }
 
 /// Non-inherent implementations are extracted, their bodies are not
 /// dropped. This might be a bit surprising: see
@@ -78,8 +66,6 @@ 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
 
@@ -89,8 +75,6 @@ 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
 
@@ -99,4 +83,20 @@ 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.
+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'
 '''