From a4552b21f0995b6d9d00ec9845c7e42bb7b1e0f8 Mon Sep 17 00:00:00 2001 From: Lucas Franceschino Date: Tue, 14 May 2024 15:03:46 +0200 Subject: [PATCH] fix(F*): always use `Type0`, never `Type` Using `Type` cause issues, especially in interfaces. An interface with a function with an implicit type parameter typed `Type` means that its universe could be anything, which will never occur in code generated from Rust. --- engine/backends/fstar/fstar_ast.ml | 2 ++ engine/backends/fstar/fstar_backend.ml | 7 +++--- ...oolchain__attribute-opaque into-fstar.snap | 4 ++-- .../toolchain__attributes into-fstar.snap | 2 +- .../toolchain__generics into-fstar.snap | 15 ++++++++----- .../toolchain__include-flag into-fstar.snap | 4 ++-- ..._mut-ref-functionalization into-fstar.snap | 4 ++-- .../toolchain__naming into-fstar.snap | 12 +++++----- .../toolchain__traits into-fstar.snap | 22 +++++++++---------- 9 files changed, 38 insertions(+), 34 deletions(-) diff --git a/engine/backends/fstar/fstar_ast.ml b/engine/backends/fstar/fstar_ast.ml index fae266227..be0074b54 100644 --- a/engine/backends/fstar/fstar_ast.ml +++ b/engine/backends/fstar/fstar_ast.ml @@ -84,6 +84,8 @@ let mk_refined (x : string) (typ : AST.term) (phi : x:AST.term -> AST.term) = let x_bd = mk_e_binder @@ AST.Annotated (x, typ) in term @@ AST.Refine (x_bd, phi (term @@ AST.Var (lid_of_id x))) +let type0_term = AST.Name (lid [ "Type0" ]) |> term + let parse_string f s = let open FStar_Parser_ParseIt in let frag_of_text s = diff --git a/engine/backends/fstar/fstar_backend.ml b/engine/backends/fstar/fstar_backend.ml index 6982db8dd..2eeb97b58 100644 --- a/engine/backends/fstar/fstar_backend.ml +++ b/engine/backends/fstar/fstar_backend.ml @@ -627,8 +627,7 @@ struct let ident = plocal_ident p.ident in match p.kind with | GPLifetime _ -> Error.assertion_failure span "pgeneric_param:LIFETIME" - | GPType { default = _ } -> - { kind; typ = F.term @@ F.AST.Name (F.lid [ "Type" ]); ident } + | GPType { default = _ } -> { kind; typ = F.type0_term; ident } | GPConst { typ } -> { kind = Explicit; typ = pty span typ; ident } let of_generic_constraint span (nth : int) (c : generic_constraint) = @@ -987,7 +986,7 @@ struct } else let generics = FStarBinder.of_generics e.span generics in - let ty = F.term @@ F.AST.Name (F.lid [ "Type" ]) in + let ty = F.type0_term in let arrow_typ = F.term @@ F.AST.Product (List.map ~f:FStarBinder.to_binder generics, ty) @@ -1169,7 +1168,7 @@ struct let fields = match i.ti_v with | TIType bounds -> - let t = F.term @@ F.AST.Name (F.lid [ "Type" ]) in + let t = F.type0_term in (* let constraints = *) (* List.map *) (* ~f:(fun implements -> *) diff --git a/test-harness/src/snapshots/toolchain__attribute-opaque into-fstar.snap b/test-harness/src/snapshots/toolchain__attribute-opaque into-fstar.snap index aac72ec7d..3e5e8e8fb 100644 --- a/test-harness/src/snapshots/toolchain__attribute-opaque into-fstar.snap +++ b/test-harness/src/snapshots/toolchain__attribute-opaque into-fstar.snap @@ -37,7 +37,7 @@ module Attribute_opaque open Core open FStar.Mul -val t_OpaqueEnum (v_X: usize) (#v_T #v_U: Type) : Type +val t_OpaqueEnum (v_X: usize) (#v_T #v_U: Type0) : Type0 -val t_OpaqueStruct (v_X: usize) (#v_T #v_U: Type) : Type +val t_OpaqueStruct (v_X: usize) (#v_T #v_U: Type0) : Type0 ''' diff --git a/test-harness/src/snapshots/toolchain__attributes into-fstar.snap b/test-harness/src/snapshots/toolchain__attributes into-fstar.snap index 0d82a6f3d..0f4fd9f77 100644 --- a/test-harness/src/snapshots/toolchain__attributes into-fstar.snap +++ b/test-harness/src/snapshots/toolchain__attributes into-fstar.snap @@ -62,7 +62,7 @@ let impl__SafeIndex__new (i: usize) : Core.Option.t_Option t_SafeIndex = else Core.Option.Option_None <: Core.Option.t_Option t_SafeIndex [@@ FStar.Tactics.Typeclasses.tcinstance] -let impl_1 (#v_T: Type) : Core.Ops.Index.t_Index (t_Array v_T (sz 10)) t_SafeIndex = +let impl_1 (#v_T: Type0) : Core.Ops.Index.t_Index (t_Array v_T (sz 10)) t_SafeIndex = { f_Output = v_T; f_index_pre = (fun (self: t_Array v_T (sz 10)) (index: t_SafeIndex) -> true); diff --git a/test-harness/src/snapshots/toolchain__generics into-fstar.snap b/test-harness/src/snapshots/toolchain__generics into-fstar.snap index eee521479..3918f8b3a 100644 --- a/test-harness/src/snapshots/toolchain__generics into-fstar.snap +++ b/test-harness/src/snapshots/toolchain__generics into-fstar.snap @@ -35,7 +35,7 @@ module Generics.Defaults_generics open Core open FStar.Mul -type t_Defaults (v_T: Type) (v_N: usize) = | Defaults : t_Array v_T v_N -> t_Defaults v_T v_N +type t_Defaults (v_T: Type0) (v_N: usize) = | Defaults : t_Array v_T v_N -> t_Defaults v_T v_N let f (_: t_Defaults Prims.unit (sz 2)) : Prims.unit = () ''' @@ -45,10 +45,10 @@ module Generics open Core open FStar.Mul -let impl__Bar__inherent_impl_generics (#v_T: Type) (v_N: usize) (x: t_Array v_T v_N) : Prims.unit = +let impl__Bar__inherent_impl_generics (#v_T: Type0) (v_N: usize) (x: t_Array v_T v_N) : Prims.unit = () -class t_Foo (v_Self: Type) = { +class t_Foo (v_Self: Type0) = { f_const_add_pre:v_N: usize -> v_Self -> bool; f_const_add_post:v_N: usize -> v_Self -> usize -> bool; f_const_add:v_N: usize -> x0: v_Self @@ -63,7 +63,10 @@ let impl_Foo_for_usize: t_Foo usize = f_const_add = fun (v_N: usize) (self: usize) -> self +! v_N } -let dup (#v_T: Type) (#[FStar.Tactics.Typeclasses.tcresolve ()] i1: Core.Clone.t_Clone v_T) (x: v_T) +let dup + (#v_T: Type0) + (#[FStar.Tactics.Typeclasses.tcresolve ()] i1: Core.Clone.t_Clone v_T) + (x: v_T) : (v_T & v_T) = Core.Clone.f_clone x, Core.Clone.f_clone x <: (v_T & v_T) let f (v_N x: usize) : usize = (v_N +! v_N <: usize) +! x @@ -72,7 +75,7 @@ let call_f (_: Prims.unit) : usize = (f (sz 10) (sz 3) <: usize) +! sz 3 let g (v_N: usize) - (#v_T: Type) + (#v_T: Type0) (#[FStar.Tactics.Typeclasses.tcresolve ()] i1: Core.Convert.t_Into v_T (t_Array usize v_N)) (arr: v_T) : usize = @@ -117,7 +120,7 @@ let foo (v_LEN: usize) (arr: t_Array usize v_LEN) : usize = let repeat (v_LEN: usize) - (#v_T: Type) + (#v_T: Type0) (#[FStar.Tactics.Typeclasses.tcresolve ()] i1: Core.Marker.t_Copy v_T) (x: v_T) : t_Array v_T v_LEN = Rust_primitives.Hax.repeat x v_LEN diff --git a/test-harness/src/snapshots/toolchain__include-flag into-fstar.snap b/test-harness/src/snapshots/toolchain__include-flag into-fstar.snap index 759bc8f1d..b7b010737 100644 --- a/test-harness/src/snapshots/toolchain__include-flag into-fstar.snap +++ b/test-harness/src/snapshots/toolchain__include-flag into-fstar.snap @@ -32,7 +32,7 @@ module Include_flag open Core open FStar.Mul -class t_Trait (v_Self: Type) = { __marker_trait_t_Trait:Prims.unit } +class t_Trait (v_Self: Type0) = { __marker_trait_t_Trait:Prims.unit } /// Indirect dependencies let main_a_a (_: Prims.unit) : Prims.unit = () @@ -42,7 +42,7 @@ let main_a_b (_: Prims.unit) : Prims.unit = () let main_a_c (_: Prims.unit) : Prims.unit = () /// Direct dependencies -let main_a (#v_T: Type) (#[FStar.Tactics.Typeclasses.tcresolve ()] i1: t_Trait v_T) (x: v_T) +let main_a (#v_T: Type0) (#[FStar.Tactics.Typeclasses.tcresolve ()] i1: t_Trait v_T) (x: v_T) : Prims.unit = let _:Prims.unit = main_a_a () in let _:Prims.unit = main_a_b () in 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 index 13e0089db..62bf174e5 100644 --- a/test-harness/src/snapshots/toolchain__mut-ref-functionalization into-fstar.snap +++ b/test-harness/src/snapshots/toolchain__mut-ref-functionalization into-fstar.snap @@ -32,7 +32,7 @@ module Mut_ref_functionalization open Core open FStar.Mul -class t_FooTrait (v_Self: Type) = { +class t_FooTrait (v_Self: Type0) = { f_z_pre:v_Self -> bool; f_z_post:v_Self -> v_Self -> bool; f_z:x0: v_Self -> Prims.Pure v_Self (f_z_pre x0) (fun result -> f_z_post x0 result) @@ -230,7 +230,7 @@ let j (x: t_Bar) : (t_Bar & u8) = let hax_temp_output:u8 = out1 +! out in x, hax_temp_output <: (t_Bar & u8) -type t_Pair (v_T: Type) = { +type t_Pair (v_T: Type0) = { f_a:v_T; f_b:t_Foo } diff --git a/test-harness/src/snapshots/toolchain__naming into-fstar.snap b/test-harness/src/snapshots/toolchain__naming into-fstar.snap index bada19155..576052fc1 100644 --- a/test-harness/src/snapshots/toolchain__naming into-fstar.snap +++ b/test-harness/src/snapshots/toolchain__naming into-fstar.snap @@ -108,9 +108,9 @@ type t_Foo2 = | Foo2_A : t_Foo2 | Foo2_B { f_x:usize }: t_Foo2 -class t_FooTrait (v_Self: Type) = { f_ASSOCIATED_CONSTANT:usize } +class t_FooTrait (v_Self: Type0) = { f_ASSOCIATED_CONSTANT:usize } -class t_T1 (v_Self: Type) = { __marker_trait_t_T1:Prims.unit } +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 = () } @@ -118,9 +118,9 @@ 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: Type) = { __marker_trait_t_T2_for_a:Prims.unit } +class t_T2_for_a (v_Self: Type0) = { __marker_trait_t_T2_for_a:Prims.unit } -class t_T3_e_for_a (v_Self: Type) = { __marker_trait_t_T3_e_for_a:Prims.unit } +class t_T3_e_for_a (v_Self: Type0) = { __marker_trait_t_T3_e_for_a:Prims.unit } [@@ FStar.Tactics.Typeclasses.tcinstance] let impl_T3_e_e_for_a_for_Foo: t_T3_e_for_a t_Foo = { __marker_trait = () } @@ -128,7 +128,7 @@ let impl_T3_e_e_for_a_for_Foo: t_T3_e_for_a t_Foo = { __marker_trait = () } let v_INHERENT_CONSTANT: usize = sz 3 let constants - (#v_T: Type) + (#v_T: Type0) (#[FStar.Tactics.Typeclasses.tcresolve ()] i1: t_FooTrait v_T) (_: Prims.unit) : usize = f_ASSOCIATED_CONSTANT +! v_INHERENT_CONSTANT @@ -143,7 +143,7 @@ let ff__g__impl_1__g (self: t_Foo) : usize = sz 1 let reserved_names (v_val v_noeq v_of: u8) : u8 = (v_val +! v_noeq <: u8) +! v_of -type t_Arity1 (v_T: Type) = | Arity1 : v_T -> t_Arity1 v_T +type t_Arity1 (v_T: Type0) = | Arity1 : v_T -> t_Arity1 v_T [@@ FStar.Tactics.Typeclasses.tcinstance] let impl_T2_e_for_a_for_Arity1_of_tuple_Foo_u8: t_T2_for_a (t_Arity1 (t_Foo & u8)) = diff --git a/test-harness/src/snapshots/toolchain__traits into-fstar.snap b/test-harness/src/snapshots/toolchain__traits into-fstar.snap index 54e02c515..703fd638b 100644 --- a/test-harness/src/snapshots/toolchain__traits into-fstar.snap +++ b/test-harness/src/snapshots/toolchain__traits into-fstar.snap @@ -35,13 +35,13 @@ module Traits open Core open FStar.Mul -class t_Bar (v_Self: Type) = { +class t_Bar (v_Self: Type0) = { f_bar_pre:v_Self -> bool; f_bar_post:v_Self -> Prims.unit -> bool; f_bar:x0: v_Self -> Prims.Pure Prims.unit (f_bar_pre x0) (fun result -> f_bar_post x0 result) } -let impl_2__method (#v_T: Type) (#[FStar.Tactics.Typeclasses.tcresolve ()] i1: t_Bar v_T) (x: v_T) +let impl_2__method (#v_T: Type0) (#[FStar.Tactics.Typeclasses.tcresolve ()] i1: t_Bar v_T) (x: v_T) : Prims.unit = f_bar x type t_Error = | Error_Fail : t_Error @@ -53,15 +53,15 @@ let impl__Error__for_application_callback (_: Prims.unit) : Prims.unit -> t_Err let t_Error_cast_to_repr (x: t_Error) : isize = match x with | Error_Fail -> isz 0 -class t_Lang (v_Self: Type) = { - f_Var:Type; +class t_Lang (v_Self: Type0) = { + f_Var:Type0; f_s_pre:v_Self -> i32 -> bool; f_s_post:v_Self -> i32 -> (v_Self & f_Var) -> bool; f_s:x0: v_Self -> x1: i32 -> Prims.Pure (v_Self & f_Var) (f_s_pre x0 x1) (fun result -> f_s_post x0 x1 result) } -class t_SuperTrait (v_Self: Type) = { +class t_SuperTrait (v_Self: Type0) = { [@@@ FStar.Tactics.Typeclasses.no_method]_super_4075428158603710007:Core.Clone.t_Clone v_Self; f_function_of_super_trait_pre:v_Self -> bool; f_function_of_super_trait_post:v_Self -> u32 -> bool; @@ -80,8 +80,8 @@ let impl_SuperTrait_for_i32: t_SuperTrait i32 = f_function_of_super_trait = fun (self: i32) -> cast (Core.Num.impl__i32__abs self <: i32) <: u32 } -class t_Foo (v_Self: Type) = { - f_AssocType:Type; +class t_Foo (v_Self: Type0) = { + f_AssocType:Type0; f_AssocType_12975176671554111340:t_SuperTrait f_AssocType; f_AssocType_15292246028710717365:Core.Clone.t_Clone f_AssocType; f_N:usize; @@ -100,7 +100,7 @@ class t_Foo (v_Self: Type) = { } let closure_impl_expr - (#v_I: Type) + (#v_I: Type0) (#[FStar.Tactics.Typeclasses.tcresolve ()] i1: Core.Iter.Traits.Iterator.t_Iterator v_I) (it: v_I) : Alloc.Vec.t_Vec Prims.unit Alloc.Alloc.t_Global = @@ -109,7 +109,7 @@ let closure_impl_expr Core.Iter.Adapters.Map.t_Map v_I (Prims.unit -> Prims.unit)) let closure_impl_expr_fngen - (#v_I #v_F: Type) + (#v_I #v_F: Type0) (#[FStar.Tactics.Typeclasses.tcresolve ()] i2: Core.Iter.Traits.Iterator.t_Iterator v_I) (#[FStar.Tactics.Typeclasses.tcresolve ()] i3: Core.Ops.Function.t_FnMut v_F Prims.unit) (it: v_I) @@ -119,11 +119,11 @@ let closure_impl_expr_fngen <: Core.Iter.Adapters.Map.t_Map v_I v_F) -let f (#v_T: Type) (#[FStar.Tactics.Typeclasses.tcresolve ()] i1: t_Foo v_T) (x: v_T) : Prims.unit = +let f (#v_T: Type0) (#[FStar.Tactics.Typeclasses.tcresolve ()] i1: t_Foo v_T) (x: v_T) : Prims.unit = let _:Prims.unit = f_assoc_f () in f_method_f x -let g (#v_T: Type) (#[FStar.Tactics.Typeclasses.tcresolve ()] i1: t_Foo v_T) (x: i1.f_AssocType) +let g (#v_T: Type0) (#[FStar.Tactics.Typeclasses.tcresolve ()] i1: t_Foo v_T) (x: i1.f_AssocType) : u32 = f_function_of_super_trait x [@@ FStar.Tactics.Typeclasses.tcinstance]