chore(engine/phases): Drop_metasized: update test snapshots

W95Psp · W95Psp · commit 0f26c35dcc86 · 2025-07-03T12:58:16.000+02:00
diff --git a/test-harness/src/snapshots/toolchain__attribute-opaque into-fstar.snap b/test-harness/src/snapshots/toolchain__attribute-opaque into-fstar.snap
@@ -119,7 +119,6 @@ val ff_pre_post (x y: bool)
           result =. y)
 
 class t_T (v_Self: Type0) = {
-  [@@@ FStar.Tactics.Typeclasses.no_method]_super_4726684624731801277:Core.Marker.t_MetaSized v_Self;
   f_U:Type0;
   f_c:u8;
   f_d_pre:Prims.unit -> Type0;
@@ -134,7 +133,6 @@ class t_T (v_Self: Type0) = {
 val impl_T_for_u8:t_T u8
 
 class t_TrGeneric (v_Self: Type0) (v_U: Type0) = {
-  [@@@ FStar.Tactics.Typeclasses.no_method]_super_4726684624731801277:Core.Marker.t_MetaSized v_Self;
   [@@@ FStar.Tactics.Typeclasses.no_method]_super_17240578109911634293:Core.Clone.t_Clone v_U;
   f_f_pre:v_U -> Type0;
   f_f_post:v_U -> v_Self -> Type0;
diff --git a/test-harness/src/snapshots/toolchain__attributes into-fstar.snap b/test-harness/src/snapshots/toolchain__attributes into-fstar.snap
@@ -155,7 +155,6 @@ open Core
 open FStar.Mul
 
 class t_T (v_Self: Type0) = {
-  [@@@ FStar.Tactics.Typeclasses.no_method]_super_4726684624731801277:Core.Marker.t_MetaSized v_Self;
   f_v_pre:v_Self -> Type0;
   f_v_post:x: v_Self -> x_future: v_Self -> pred: Type0{pred ==> true};
   f_v:x0: v_Self -> Prims.Pure v_Self (f_v_pre x0) (fun result -> f_v_post x0 result)
@@ -215,7 +214,6 @@ let impl_SafeIndex__as_usize (self: t_SafeIndex) : usize = self.f_i
 let impl_1 (#v_T: Type0) : Core.Ops.Index.t_Index (t_Array v_T (mk_usize 10)) t_SafeIndex =
   {
     f_Output = v_T;
-    f_Output_6696274936538609082 = FStar.Tactics.Typeclasses.solve;
     f_index_pre = (fun (self: t_Array v_T (mk_usize 10)) (index: t_SafeIndex) -> true);
     f_index_post = (fun (self: t_Array v_T (mk_usize 10)) (index: t_SafeIndex) (out: v_T) -> true);
     f_index = fun (self: t_Array v_T (mk_usize 10)) (index: t_SafeIndex) -> self.[ index.f_i ]
@@ -252,7 +250,6 @@ open Core
 open FStar.Mul
 
 class t_Operation (v_Self: Type0) = {
-  [@@@ FStar.Tactics.Typeclasses.no_method]_super_4726684624731801277:Core.Marker.t_MetaSized v_Self;
   f_double_pre:x: u8
     -> pred:
       Type0
@@ -309,7 +306,6 @@ let impl_Operation_for_ViaMul: t_Operation t_ViaMul =
   }
 
 class t_TraitWithRequiresAndEnsures (v_Self: Type0) = {
-  [@@@ FStar.Tactics.Typeclasses.no_method]_super_4726684624731801277:Core.Marker.t_MetaSized v_Self;
   f_method_pre:self_: v_Self -> x: u8 -> pred: Type0{x <. mk_u8 100 ==> pred};
   f_method_post:self_: v_Self -> x: u8 -> r: u8 -> pred: Type0{pred ==> r >. mk_u8 88};
   f_method:x0: v_Self -> x1: u8
@@ -404,7 +400,6 @@ let mutation_example
 let impl: Core.Ops.Index.t_Index t_MyArray usize =
   {
     f_Output = u8;
-    f_Output_6696274936538609082 = FStar.Tactics.Typeclasses.solve;
     f_index_pre = (fun (self_: t_MyArray) (index: usize) -> index <. v_MAX);
     f_index_post = (fun (self: t_MyArray) (index: usize) (out: u8) -> true);
     f_index = fun (self: t_MyArray) (index: usize) -> self.[ index ]
@@ -593,7 +588,6 @@ open Core
 open FStar.Mul
 
 class t_Foo (v_Self: Type0) = {
-  [@@@ FStar.Tactics.Typeclasses.no_method]_super_4726684624731801277:Core.Marker.t_MetaSized v_Self;
   f_f_pre:x: u8 -> y: u8
     -> pred:
       Type0
diff --git a/test-harness/src/snapshots/toolchain__dyn into-fstar.snap b/test-harness/src/snapshots/toolchain__dyn into-fstar.snap
@@ -33,7 +33,6 @@ open Core
 open FStar.Mul
 
 class t_Printable (v_Self: Type0) (v_S: Type0) = {
-  [@@@ FStar.Tactics.Typeclasses.no_method]_super_4726684624731801277:Core.Marker.t_MetaSized v_Self;
   f_stringify_pre:v_Self -> Type0;
   f_stringify_post:v_Self -> v_S -> Type0;
   f_stringify:x0: v_Self
diff --git a/test-harness/src/snapshots/toolchain__functions into-fstar.snap b/test-harness/src/snapshots/toolchain__functions into-fstar.snap
@@ -38,7 +38,6 @@ type t_CallableViaDeref = | CallableViaDeref : t_CallableViaDeref
 let impl: Core.Ops.Deref.t_Deref t_CallableViaDeref =
   {
     f_Target = Prims.unit -> bool;
-    f_Target_4695674276362814091 = FStar.Tactics.Typeclasses.solve;
     f_deref_pre = (fun (self: t_CallableViaDeref) -> true);
     f_deref_post = (fun (self: t_CallableViaDeref) (out: (Prims.unit -> bool)) -> true);
     f_deref
diff --git a/test-harness/src/snapshots/toolchain__generics into-fstar.snap b/test-harness/src/snapshots/toolchain__generics into-fstar.snap
@@ -157,7 +157,6 @@ let call_g (_: Prims.unit) : usize =
   mk_usize 3
 
 class t_Foo (v_Self: Type0) = {
-  [@@@ FStar.Tactics.Typeclasses.no_method]_super_4726684624731801277:Core.Marker.t_MetaSized v_Self;
   f_const_add_pre:v_N: usize -> v_Self -> Type0;
   f_const_add_post:v_N: usize -> v_Self -> usize -> Type0;
   f_const_add:v_N: usize -> x0: v_Self
diff --git a/test-harness/src/snapshots/toolchain__include-flag into-coq.snap b/test-harness/src/snapshots/toolchain__include-flag into-coq.snap
@@ -51,10 +51,10 @@ Record Foo_record : Type :=
 #[export]
 Notation "'Foo_Foo_record'" := Build_Foo_record.
 
-Class t_Trait (v_Self : Type) `{t_MetaSized (v_Self)} : Type :=
+Class t_Trait (v_Self : Type) : Type :=
   {
   }.
-Arguments t_Trait (_) {_}.
+Arguments t_Trait (_).
 
 Instance t_Trait_572156424 : t_Trait ((t_Foo)) :=
   {
diff --git a/test-harness/src/snapshots/toolchain__include-flag into-fstar.snap b/test-harness/src/snapshots/toolchain__include-flag into-fstar.snap
@@ -34,9 +34,7 @@ open FStar.Mul
 
 type t_Foo = | Foo : t_Foo
 
-class t_Trait (v_Self: Type0) = {
-  [@@@ FStar.Tactics.Typeclasses.no_method]_super_4726684624731801277:Core.Marker.t_MetaSized v_Self
-}
+class t_Trait (v_Self: Type0) = { __marker_trait_t_Trait:Prims.unit }
 
 [@@ FStar.Tactics.Typeclasses.tcinstance]
 let impl: t_Trait t_Foo = { __marker_trait = () }
diff --git a/test-harness/src/snapshots/toolchain__interface-only into-fstar.snap b/test-harness/src/snapshots/toolchain__interface-only into-fstar.snap
@@ -101,7 +101,6 @@ unfold
 let ff_generic (v_X: usize) (#v_U: Type0) = ff_generic' v_X #v_U
 
 class t_T (v_Self: Type0) = {
-  [@@@ FStar.Tactics.Typeclasses.no_method]_super_4726684624731801277:Core.Marker.t_MetaSized v_Self;
   f_Assoc:Type0;
   f_d_pre:Prims.unit -> Type0;
   f_d_post:Prims.unit -> Prims.unit -> Type0;
@@ -119,7 +118,6 @@ let impl_T_for_u8: t_T u8 =
   }
 
 class t_T2 (v_Self: Type0) = {
-  [@@@ FStar.Tactics.Typeclasses.no_method]_super_4726684624731801277:Core.Marker.t_MetaSized v_Self;
   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)
diff --git a/test-harness/src/snapshots/toolchain__mut-ref-functionalization into-fstar.snap b/test-harness/src/snapshots/toolchain__mut-ref-functionalization into-fstar.snap
@@ -269,7 +269,6 @@ let k
   (Alloc.Vec.t_Vec u8 Alloc.Alloc.t_Global & u16 & Prims.unit & u64)
 
 class t_FooTrait (v_Self: Type0) = {
-  [@@@ FStar.Tactics.Typeclasses.no_method]_super_4726684624731801277:Core.Marker.t_MetaSized v_Self;
   f_z_pre:v_Self -> Type0;
   f_z_post:v_Self -> v_Self -> Type0;
   f_z:x0: v_Self -> Prims.Pure v_Self (f_z_pre x0) (fun result -> f_z_post x0 result)
diff --git a/test-harness/src/snapshots/toolchain__naming into-fstar.snap b/test-harness/src/snapshots/toolchain__naming into-fstar.snap
@@ -172,27 +172,21 @@ let reserved_names (v_val v_noeq v_of: u8) : u8 = (v_val +! v_noeq <: u8) +! v_o
 
 type t_Arity1 (v_T: Type0) = | Arity1 : v_T -> t_Arity1 v_T
 
-class t_T1 (v_Self: Type0) = {
-  [@@@ FStar.Tactics.Typeclasses.no_method]_super_4726684624731801277:Core.Marker.t_MetaSized v_Self
-}
+class t_T1 (v_Self: Type0) = { __marker_trait_t_T1:Prims.unit }
 
 [@@ FStar.Tactics.Typeclasses.tcinstance]
 let impl_T1_for_Foo: t_T1 t_Foo = { __marker_trait = () }
 
 [@@ FStar.Tactics.Typeclasses.tcinstance]
 let impl_T1_for_tuple_Foo_u8: t_T1 (t_Foo & u8) = { __marker_trait = () }
 
-class t_T2_for_a (v_Self: Type0) = {
-  [@@@ FStar.Tactics.Typeclasses.no_method]_super_4726684624731801277:Core.Marker.t_MetaSized v_Self
-}
+class t_T2_for_a (v_Self: Type0) = { __marker_trait_t_T2_for_a:Prims.unit }
 
 [@@ FStar.Tactics.Typeclasses.tcinstance]
 let impl_T2_ee_for_a_for_Arity1_of_tuple_Foo_u8: t_T2_for_a (t_Arity1 (t_Foo & u8)) =
   { __marker_trait = () }
 
-class t_T3_ee_for_a (v_Self: Type0) = {
-  [@@@ FStar.Tactics.Typeclasses.no_method]_super_4726684624731801277:Core.Marker.t_MetaSized v_Self
-}
+class t_T3_ee_for_a (v_Self: Type0) = { __marker_trait_t_T3_ee_for_a:Prims.unit }
 
 [@@ FStar.Tactics.Typeclasses.tcinstance]
 let impl_T3_ee_e_for_a_for_Foo: t_T3_ee_for_a t_Foo = { __marker_trait = () }
@@ -220,10 +214,7 @@ let construct_structs (a b: usize) : Prims.unit =
 
 let v_INHERENT_CONSTANT: usize = mk_usize 3
 
-class t_FooTrait (v_Self: Type0) = {
-  [@@@ FStar.Tactics.Typeclasses.no_method]_super_4726684624731801277:Core.Marker.t_MetaSized v_Self;
-  f_ASSOCIATED_CONSTANT:usize
-}
+class t_FooTrait (v_Self: Type0) = { f_ASSOCIATED_CONSTANT:usize }
 
 let constants
       (#v_T: Type0)
diff --git a/test-harness/src/snapshots/toolchain__side-effects into-fstar.snap b/test-harness/src/snapshots/toolchain__side-effects into-fstar.snap
@@ -34,7 +34,6 @@ open Core
 open FStar.Mul
 
 class t_MyFrom (v_Self: Type0) (v_T: Type0) = {
-  [@@@ FStar.Tactics.Typeclasses.no_method]_super_4726684624731801277:Core.Marker.t_MetaSized v_Self;
   f_my_from_pre:v_T -> Type0;
   f_my_from_post:v_T -> v_Self -> Type0;
   f_my_from:x0: v_T -> Prims.Pure v_Self (f_my_from_pre x0) (fun result -> f_my_from_post x0 result)
diff --git a/test-harness/src/snapshots/toolchain__traits into-fstar.snap b/test-harness/src/snapshots/toolchain__traits into-fstar.snap
@@ -32,18 +32,13 @@ module Traits.Block_size
 open Core
 open FStar.Mul
 
-class t_BlockSizeUser (v_Self: Type0) = {
-  [@@@ FStar.Tactics.Typeclasses.no_method]_super_4726684624731801277:Core.Marker.t_MetaSized v_Self;
-  f_BlockSize:Type0
-}
+class t_BlockSizeUser (v_Self: Type0) = { f_BlockSize:Type0 }
 
 class t_ParBlocksSizeUser (v_Self: Type0) = {
-  [@@@ FStar.Tactics.Typeclasses.no_method]_super_4726684624731801277:Core.Marker.t_MetaSized v_Self;
   [@@@ FStar.Tactics.Typeclasses.no_method]_super_5884559561557426095:t_BlockSizeUser v_Self
 }
 
 class t_BlockBackend (v_Self: Type0) = {
-  [@@@ FStar.Tactics.Typeclasses.no_method]_super_4726684624731801277:Core.Marker.t_MetaSized v_Self;
   [@@@ FStar.Tactics.Typeclasses.no_method]_super_17422710415653782164:t_ParBlocksSizeUser v_Self;
   f_proc_block_pre:Alloc.Vec.t_Vec _ Alloc.Alloc.t_Global -> Type0;
   f_proc_block_post:Alloc.Vec.t_Vec _ Alloc.Alloc.t_Global -> Prims.unit -> Type0;
@@ -57,12 +52,9 @@ module Traits.Default_traits_parameters
 open Core
 open FStar.Mul
 
-class t_Bar (v_Self: Type0) (v_T: Type0) = {
-  [@@@ FStar.Tactics.Typeclasses.no_method]_super_4726684624731801277:Core.Marker.t_MetaSized v_Self
-}
+class t_Bar (v_Self: Type0) (v_T: Type0) = { __marker_trait_t_Bar:Prims.unit }
 
 class t_Foo (v_Self: Type0) = {
-  [@@@ FStar.Tactics.Typeclasses.no_method]_super_4726684624731801277:Core.Marker.t_MetaSized v_Self;
   [@@@ FStar.Tactics.Typeclasses.no_method]_super_7275791365833186636:t_Bar v_Self f_U;
   f_U:Type0
 }
@@ -73,9 +65,7 @@ module Traits.For_clauses.Issue_495_.Minimized_3_
 open Core
 open FStar.Mul
 
-class t_Trait (v_Self: Type0) = {
-  [@@@ FStar.Tactics.Typeclasses.no_method]_super_4726684624731801277:Core.Marker.t_MetaSized v_Self
-}
+class t_Trait (v_Self: Type0) = { __marker_trait_t_Trait:Prims.unit }
 
 [@@ FStar.Tactics.Typeclasses.tcinstance]
 let impl
@@ -158,7 +148,6 @@ open Core
 open FStar.Mul
 
 class t_Foo (v_Self: Type0) (v_T: Type0) = {
-  [@@@ FStar.Tactics.Typeclasses.no_method]_super_4726684624731801277:Core.Marker.t_MetaSized v_Self;
   f_to_t_pre:v_Self -> Type0;
   f_to_t_post:v_Self -> v_T -> Type0;
   f_to_t:x0: v_Self -> Prims.Pure v_T (f_to_t_pre x0) (fun result -> f_to_t_post x0 result)
@@ -175,14 +164,9 @@ module Traits.Impl_expr_in_goal
 open Core
 open FStar.Mul
 
-class t_T1 (v_Self: Type0) = {
-  [@@@ FStar.Tactics.Typeclasses.no_method]_super_4726684624731801277:Core.Marker.t_MetaSized v_Self;
-  f_Assoc:Type0
-}
+class t_T1 (v_Self: Type0) = { f_Assoc:Type0 }
 
-class t_T2 (v_Self: Type0) = {
-  [@@@ FStar.Tactics.Typeclasses.no_method]_super_4726684624731801277:Core.Marker.t_MetaSized v_Self
-}
+class t_T2 (v_Self: Type0) = { __marker_trait_t_T2:Prims.unit }
 
 [@@ FStar.Tactics.Typeclasses.tcinstance]
 let impl
@@ -246,7 +230,6 @@ open Core
 open FStar.Mul
 
 class t_MyTrait (v_Self: Type0) = {
-  [@@@ FStar.Tactics.Typeclasses.no_method]_super_4726684624731801277:Core.Marker.t_MetaSized v_Self;
   f_my_method_pre:v_Self -> Type0;
   f_my_method_post:v_Self -> Prims.unit -> Type0;
   f_my_method:x0: v_Self
@@ -280,7 +263,6 @@ open FStar.Mul
 type t_Type (v_TypeArg: Type0) (v_ConstArg: usize) = { f_field:t_Array v_TypeArg v_ConstArg }
 
 class t_Trait (v_Self: Type0) (v_TypeArg: Type0) (v_ConstArg: usize) = {
-  [@@@ FStar.Tactics.Typeclasses.no_method]_super_4726684624731801277:Core.Marker.t_MetaSized v_Self;
   f_method_pre:
       #v_MethodTypeArg: Type0 ->
       v_MethodConstArg: usize ->
@@ -443,7 +425,6 @@ let associated_function_caller
   ()
 
 class t_SubTrait (v_Self: Type0) (v_TypeArg: Type0) (v_ConstArg: usize) = {
-  [@@@ FStar.Tactics.Typeclasses.no_method]_super_4726684624731801277:Core.Marker.t_MetaSized v_Self;
   [@@@ FStar.Tactics.Typeclasses.no_method]_super_15145771689388873921:t_Trait v_Self
     v_TypeArg
     v_ConstArg;
@@ -461,7 +442,6 @@ type t_Bar (v_FooConst: usize) (v_FooType: Type0) =
   | Bar : t_Array v_FooType v_FooConst -> t_Bar v_FooConst v_FooType
 
 class t_Foo (v_Self: Type0) (v_FooConst: usize) (v_FooType: Type0) = {
-  [@@@ FStar.Tactics.Typeclasses.no_method]_super_4726684624731801277:Core.Marker.t_MetaSized v_Self;
   f_fun_pre:
       v_FunConst: usize ->
       #v_FunType: Type0 ->
@@ -525,13 +505,11 @@ open Core
 open FStar.Mul
 
 class t_Trait1 (v_Self: Type0) = {
-  [@@@ FStar.Tactics.Typeclasses.no_method]_super_4726684624731801277:Core.Marker.t_MetaSized v_Self;
   f_T:Type0;
   f_T_7969211799618487585:t_Trait1 f_T
 }
 
 class t_Trait2 (v_Self: Type0) = {
-  [@@@ FStar.Tactics.Typeclasses.no_method]_super_4726684624731801277:Core.Marker.t_MetaSized v_Self;
   [@@@ FStar.Tactics.Typeclasses.no_method]_super_3259985701465885527:t_Trait1 v_Self;
   f_U:Type0
 }
@@ -552,7 +530,6 @@ open Core
 open FStar.Mul
 
 class t_PolyOp (v_Self: Type0) = {
-  [@@@ FStar.Tactics.Typeclasses.no_method]_super_4726684624731801277:Core.Marker.t_MetaSized v_Self;
   f_op_pre:u32 -> u32 -> Type0;
   f_op_post:u32 -> u32 -> u32 -> Type0;
   f_op:x0: u32 -> x1: u32 -> Prims.Pure u32 (f_op_pre x0 x1) (fun result -> f_op_post x0 x1 result)
@@ -590,7 +567,6 @@ open Core
 open FStar.Mul
 
 class t_SuperTrait (v_Self: Type0) = {
-  [@@@ FStar.Tactics.Typeclasses.no_method]_super_4726684624731801277:Core.Marker.t_MetaSized v_Self;
   [@@@ FStar.Tactics.Typeclasses.no_method]_super_15837849249852401974:Core.Clone.t_Clone v_Self;
   f_function_of_super_trait_pre:v_Self -> Type0;
   f_function_of_super_trait_post:v_Self -> u32 -> Type0;
@@ -612,7 +588,6 @@ let impl: t_SuperTrait i32 =
 type t_Struct = | Struct : t_Struct
 
 class t_Bar (v_Self: Type0) = {
-  [@@@ FStar.Tactics.Typeclasses.no_method]_super_4726684624731801277:Core.Marker.t_MetaSized v_Self;
   f_bar_pre:v_Self -> Type0;
   f_bar_post:v_Self -> Prims.unit -> Type0;
   f_bar:x0: v_Self -> Prims.Pure Prims.unit (f_bar_pre x0) (fun result -> f_bar_post x0 result)
@@ -675,7 +650,6 @@ let uuse_iimpl_trait (_: Prims.unit) : Prims.unit =
   ()
 
 class t_Foo (v_Self: Type0) = {
-  [@@@ FStar.Tactics.Typeclasses.no_method]_super_4726684624731801277:Core.Marker.t_MetaSized v_Self;
   f_AssocType:Type0;
   f_AssocType_1162045947544099865:t_SuperTrait f_AssocType;
   f_N:usize;

Original file line number	Diff line number	Diff line change
`@@ -38,7 +38,6 @@ type t_CallableViaDeref = \| CallableViaDeref : t_CallableViaDeref`
`38`	`38`	`let impl: Core.Ops.Deref.t_Deref t_CallableViaDeref =`
`39`	`39`	`{`
`40`	`40`	`f_Target = Prims.unit -> bool;`
`41`		`- f_Target_4695674276362814091 = FStar.Tactics.Typeclasses.solve;`
`42`	`41`	`f_deref_pre = (fun (self: t_CallableViaDeref) -> true);`
`43`	`42`	`f_deref_post = (fun (self: t_CallableViaDeref) (out: (Prims.unit -> bool)) -> true);`
`44`	`43`	`f_deref`
Original file line number	Diff line number	Diff line change
`@@ -51,10 +51,10 @@ Record Foo_record : Type :=`
`51`	`51`	`#[export]`
`52`	`52`	`Notation "'Foo_Foo_record'" := Build_Foo_record.`
`53`	`53`
`54`		-Class t_Trait (v_Self : Type) `{t_MetaSized (v_Self)} : Type :=
	`54`	`+Class t_Trait (v_Self : Type) : Type :=`
`55`	`55`	`{`
`56`	`56`	`}.`
`57`		`-Arguments t_Trait (_) {_}.`
	`57`	`+Arguments t_Trait (_).`
`58`	`58`
`59`	`59`	`Instance t_Trait_572156424 : t_Trait ((t_Foo)) :=`
`60`	`60`	`{`