From 510fee737c3a3f3a40c86675ae2bd578f862ba2b Mon Sep 17 00:00:00 2001 From: Lucas Franceschino Date: Wed, 7 Aug 2024 16:50:52 +0200 Subject: [PATCH] fix(backend/fstar): pre/post are `Type0` predicates, not boolean predicates For a method `f` in a trait, we generate two fields: `f_pre` and `f_post`. Those used to be boolean predicates, because we inherited the type from Rust. This commit changes that: we now enforce `f_pre` and `f_post` to be arrow type with `Type0` as last component. --- engine/backends/fstar/fstar_backend.ml | 116 ++++++++++-------- .../toolchain__attributes into-fstar.snap | 8 +- .../snapshots/toolchain__dyn into-fstar.snap | 4 +- .../toolchain__generics into-fstar.snap | 4 +- ..._mut-ref-functionalization into-fstar.snap | 4 +- .../toolchain__traits into-fstar.snap | 52 ++++---- 6 files changed, 102 insertions(+), 86 deletions(-) diff --git a/engine/backends/fstar/fstar_backend.ml b/engine/backends/fstar/fstar_backend.ml index 5f48597a3..eb4248194 100644 --- a/engine/backends/fstar/fstar_backend.ml +++ b/engine/backends/fstar/fstar_backend.ml @@ -693,9 +693,13 @@ struct let ident = F.id ("x" ^ Int.to_string nth) in { kind = Explicit; ident; typ = pty span typ } - let of_named_typ span name typ : t = + (** Makes an F* binder from a name and an F* type *) + let of_named_fstar_typ span name typ : t = let ident = plocal_ident name in - { kind = Explicit; ident; typ = pty span typ } + { kind = Explicit; ident; typ } + + (** Makes an F* binder from a name and an hax type *) + let of_named_typ span name = pty span >> of_named_fstar_typ span name let to_pattern (x : t) : F.AST.pattern = let subpat = @@ -1167,52 +1171,11 @@ struct [], F.mk_e_app base args )) bounds - | TIFn (TArrow (inputs, output)) + | TIFn ty when Attrs.find_unique_attr i.ti_attrs ~f:(function | TraitMethodNoPrePost -> Some () | _ -> None) - |> Option.is_none -> - let inputs = - List.mapi ~f:(FStarBinder.of_typ e.span) inputs - in - let inputs = generics @ inputs in - let output = pty e.span output in - let ty_pre_post = - let inputs = - List.map ~f:FStarBinder.to_qualified_term inputs - in - let add_pre n = n ^ "_pre" in - let pre_name_str = - U.Concrete_ident_view.to_definition_name - (Concrete_ident.Create.map_last ~f:add_pre i.ti_ident) - in - let pre = - F.mk_app (F.term_of_lid [ pre_name_str ]) inputs - in - let result = F.term_of_lid [ "result" ] in - let add_post n = n ^ "_post" in - let post_name_str = - U.Concrete_ident_view.to_definition_name - (Concrete_ident.Create.map_last ~f:add_post i.ti_ident) - in - let post = - F.mk_app - (F.term_of_lid [ post_name_str ]) - (inputs @ [ (result, Nothing) ]) - in - let post = - F.mk_e_abs - [ F.pat @@ F.AST.PatVar (F.id "result", None, []) ] - post - in - F.mk_e_app - (F.term_of_lid [ "Prims"; "Pure" ]) - [ output; pre; post ] - in - let inputs = List.map ~f:FStarBinder.to_binder inputs in - let ty = F.term @@ F.AST.Product (inputs, ty_pre_post) in - [ (F.id name, None, [], ty) ] - | TIFn ty -> + |> Option.is_some -> let weakest = let h kind = Attrs.associated_fns kind i.ti_attrs @@ -1257,7 +1220,6 @@ struct let expr = renamer#visit_expr () expr in (generics, params, expr, is_req)) in - let ty = pty e.span ty in let ty = let variables = let idents_visitor = U.Reducers.collect_local_idents in @@ -1302,10 +1264,9 @@ struct ~f:(fun (generics, binders, (expr : expr), is_req) -> let result_ident = mk_fresh "pred" in let result_bd = - FStarBinder.of_named_typ expr.span result_ident - expr.typ + FStarBinder.of_named_fstar_typ expr.span + result_ident F.type0_term in - let typ = pty expr.span expr.typ in let expr = U.make_lets !bindings expr in let expr = pexpr expr in let result = @@ -1324,7 +1285,15 @@ struct ( List.map ~f:FStarBinder.to_binder binders, result ) |> F.term) - |> Option.value ~default:ty + |> Option.value_or_thunk ~default:(fun _ -> + let ty = pty e.span ty in + match ty.tm with + | F.AST.Product (inputs, _) -> + { + ty with + tm = F.AST.Product (inputs, F.type0_term); + } + | _ -> F.type0_term) in let ty = @@ -1333,6 +1302,53 @@ struct (generics |> List.map ~f:FStarBinder.to_binder, ty) in [ (F.id name, None, [], ty) ] + | TIFn (TArrow (inputs, output)) -> + let inputs = + List.mapi ~f:(FStarBinder.of_typ e.span) inputs + in + let inputs = generics @ inputs in + let output = pty e.span output in + let ty_pre_post = + let inputs = + List.map ~f:FStarBinder.to_qualified_term inputs + in + let add_pre n = n ^ "_pre" in + let pre_name_str = + U.Concrete_ident_view.to_definition_name + (Concrete_ident.Create.map_last ~f:add_pre i.ti_ident) + in + let pre = + F.mk_app (F.term_of_lid [ pre_name_str ]) inputs + in + let result = F.term_of_lid [ "result" ] in + let add_post n = n ^ "_post" in + let post_name_str = + U.Concrete_ident_view.to_definition_name + (Concrete_ident.Create.map_last ~f:add_post i.ti_ident) + in + let post = + F.mk_app + (F.term_of_lid [ post_name_str ]) + (inputs @ [ (result, Nothing) ]) + in + let post = + F.mk_e_abs + [ F.pat @@ F.AST.PatVar (F.id "result", None, []) ] + post + in + F.mk_e_app + (F.term_of_lid [ "Prims"; "Pure" ]) + [ output; pre; post ] + in + let inputs = List.map ~f:FStarBinder.to_binder inputs in + let ty = F.term @@ F.AST.Product (inputs, ty_pre_post) in + [ (F.id name, None, [], ty) ] + | TIFn non_arrow_ty -> + let inputs = generics in + let output = pty e.span non_arrow_ty in + let inputs = List.map ~f:FStarBinder.to_binder inputs in + let ty = F.term @@ F.AST.Product (inputs, output) in + [ (F.id name, None, [], ty) ] | _ -> . in List.map ~f:Fn.id diff --git a/test-harness/src/snapshots/toolchain__attributes into-fstar.snap b/test-harness/src/snapshots/toolchain__attributes into-fstar.snap index 0cfc69aeb..290866081 100644 --- a/test-harness/src/snapshots/toolchain__attributes into-fstar.snap +++ b/test-harness/src/snapshots/toolchain__attributes into-fstar.snap @@ -89,13 +89,13 @@ open FStar.Mul class t_Operation (v_Self: Type0) = { f_double_pre:x: u8 -> pred: - bool + Type0 { (Rust_primitives.Hax.Int.from_machine x <: Hax_lib.Int.t_Int) <= (127 <: Hax_lib.Int.t_Int) ==> pred }; f_double_post:x: u8 -> result: u8 -> pred: - bool + Type0 { pred ==> ((Rust_primitives.Hax.Int.from_machine x <: Hax_lib.Int.t_Int) * (2 <: Hax_lib.Int.t_Int) <: @@ -105,8 +105,8 @@ class t_Operation (v_Self: Type0) = { } class t_TraitWithRequiresAndEnsures (v_Self: Type0) = { - f_method_pre:self___: v_Self -> x: u8 -> pred: bool{x <. 100uy ==> pred}; - f_method_post:self___: v_Self -> x: u8 -> r: u8 -> pred: bool{pred ==> r >. 88uy}; + f_method_pre:self___: v_Self -> x: u8 -> pred: Type0{x <. 100uy ==> pred}; + f_method_post:self___: v_Self -> x: u8 -> r: u8 -> pred: Type0{pred ==> r >. 88uy}; f_method:x0: v_Self -> x1: u8 -> Prims.Pure u8 (f_method_pre x0 x1) (fun result -> f_method_post x0 x1 result) } diff --git a/test-harness/src/snapshots/toolchain__dyn into-fstar.snap b/test-harness/src/snapshots/toolchain__dyn into-fstar.snap index 668bb7700..209e239dd 100644 --- a/test-harness/src/snapshots/toolchain__dyn into-fstar.snap +++ b/test-harness/src/snapshots/toolchain__dyn into-fstar.snap @@ -33,8 +33,8 @@ open Core open FStar.Mul class t_Printable (v_Self: Type0) (v_S: Type0) = { - f_stringify_pre:v_Self -> bool; - f_stringify_post:v_Self -> v_S -> bool; + f_stringify_pre:v_Self -> Type0; + f_stringify_post:v_Self -> v_S -> Type0; f_stringify:x0: v_Self -> Prims.Pure v_S (f_stringify_pre x0) (fun result -> f_stringify_post x0 result) } diff --git a/test-harness/src/snapshots/toolchain__generics into-fstar.snap b/test-harness/src/snapshots/toolchain__generics into-fstar.snap index ce160e3e5..caa4a97f7 100644 --- a/test-harness/src/snapshots/toolchain__generics into-fstar.snap +++ b/test-harness/src/snapshots/toolchain__generics into-fstar.snap @@ -47,8 +47,8 @@ let impl__Bar__inherent_impl_generics (#v_T: Type0) (v_N: usize) (x: t_Array v_T () 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_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 -> Prims.Pure usize (f_const_add_pre v_N x0) (fun result -> f_const_add_post v_N 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 index 492d1f7e8..e93cd3056 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 @@ -33,8 +33,8 @@ open Core open FStar.Mul class t_FooTrait (v_Self: Type0) = { - f_z_pre:v_Self -> bool; - f_z_post:v_Self -> v_Self -> bool; + 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__traits into-fstar.snap b/test-harness/src/snapshots/toolchain__traits into-fstar.snap index ac287fd42..5cf9b7b62 100644 --- a/test-harness/src/snapshots/toolchain__traits into-fstar.snap +++ b/test-harness/src/snapshots/toolchain__traits into-fstar.snap @@ -40,8 +40,8 @@ class t_ParBlocksSizeUser (v_Self: Type0) = { class t_BlockBackend (v_Self: Type0) = { [@@@ FStar.Tactics.Typeclasses.no_method]_super_15949286759387124191:t_ParBlocksSizeUser v_Self; - f_proc_block_pre:Alloc.Vec.t_Vec _ Alloc.Alloc.t_Global -> bool; - f_proc_block_post:Alloc.Vec.t_Vec _ Alloc.Alloc.t_Global -> Prims.unit -> bool; + 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; f_proc_block:x0: Alloc.Vec.t_Vec _ Alloc.Alloc.t_Global -> Prims.Pure Prims.unit (f_proc_block_pre x0) (fun result -> f_proc_block_post x0 result) } @@ -134,8 +134,8 @@ open Core open FStar.Mul class t_Foo (v_Self: Type0) (v_T: Type0) = { - f_to_t_pre:v_Self -> bool; - f_to_t_post:v_Self -> v_T -> bool; + 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) } @@ -179,8 +179,8 @@ open Core open FStar.Mul class t_MyTrait (v_Self: Type0) = { - f_my_method_pre:v_Self -> bool; - f_my_method_post:v_Self -> Prims.unit -> bool; + f_my_method_pre:v_Self -> Type0; + f_my_method_post:v_Self -> Prims.unit -> Type0; f_my_method:x0: v_Self -> Prims.Pure Prims.unit (f_my_method_pre x0) (fun result -> f_my_method_post x0 result) } @@ -217,7 +217,7 @@ class t_Trait (v_Self: Type0) (v_TypeArg: Type0) (v_ConstArg: usize) = { v_Self -> v_TypeArg -> t_Type v_TypeArg v_ConstArg - -> bool; + -> Type0; f_method_post: #v_MethodTypeArg: Type0 -> v_MethodConstArg: usize -> @@ -225,7 +225,7 @@ class t_Trait (v_Self: Type0) (v_TypeArg: Type0) (v_ConstArg: usize) = { v_TypeArg -> t_Type v_TypeArg v_ConstArg -> Prims.unit - -> bool; + -> Type0; f_method: #v_MethodTypeArg: Type0 -> v_MethodConstArg: usize -> @@ -241,7 +241,7 @@ class t_Trait (v_Self: Type0) (v_TypeArg: Type0) (v_ConstArg: usize) = { v_Self -> v_TypeArg -> t_Type v_TypeArg v_ConstArg - -> bool; + -> Type0; f_associated_function_post: #v_MethodTypeArg: Type0 -> v_MethodConstArg: usize -> @@ -249,7 +249,7 @@ class t_Trait (v_Self: Type0) (v_TypeArg: Type0) (v_ConstArg: usize) = { v_TypeArg -> t_Type v_TypeArg v_ConstArg -> Prims.unit - -> bool; + -> Type0; f_associated_function: #v_MethodTypeArg: Type0 -> v_MethodConstArg: usize -> @@ -392,14 +392,14 @@ class t_Foo (v_Self: Type0) (v_FooConst: usize) (v_FooType: Type0) = { #v_FunType: Type0 -> t_Array v_FooType v_FooConst -> t_Array v_FunType v_FunConst - -> bool; + -> Type0; f_fun_post: v_FunConst: usize -> #v_FunType: Type0 -> t_Array v_FooType v_FooConst -> t_Array v_FunType v_FunConst -> Prims.unit - -> bool; + -> Type0; f_fun: v_FunConst: usize -> #v_FunType: Type0 -> @@ -478,8 +478,8 @@ open Core open FStar.Mul class t_PolyOp (v_Self: Type0) = { - f_op_pre:u32 -> u32 -> bool; - f_op_post:u32 -> u32 -> u32 -> bool; + 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) } @@ -515,8 +515,8 @@ open Core open FStar.Mul class t_Bar (v_Self: Type0) = { - f_bar_pre:v_Self -> bool; - f_bar_post:v_Self -> Prims.unit -> bool; + 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) } @@ -534,16 +534,16 @@ let t_Error_cast_to_repr (x: t_Error) : isize = match x with | Error_Fail -> is 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_pre:v_Self -> i32 -> Type0; + f_s_post:v_Self -> i32 -> (v_Self & f_Var) -> Type0; 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: Type0) = { [@@@ FStar.Tactics.Typeclasses.no_method]_super_9442900250278684536: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; + f_function_of_super_trait_pre:v_Self -> Type0; + f_function_of_super_trait_post:v_Self -> u32 -> Type0; f_function_of_super_trait:x0: v_Self -> Prims.Pure u32 (f_function_of_super_trait_pre x0) @@ -564,16 +564,16 @@ class t_Foo (v_Self: Type0) = { f_AssocType_9316156492785325993:t_SuperTrait f_AssocType; f_AssocType_11693383309247349160:Core.Clone.t_Clone f_AssocType; f_N:usize; - f_assoc_f_pre:Prims.unit -> bool; - f_assoc_f_post:Prims.unit -> Prims.unit -> bool; + f_assoc_f_pre:Prims.unit -> Type0; + f_assoc_f_post:Prims.unit -> Prims.unit -> Type0; f_assoc_f:x0: Prims.unit -> Prims.Pure Prims.unit (f_assoc_f_pre x0) (fun result -> f_assoc_f_post x0 result); - f_method_f_pre:v_Self -> bool; - f_method_f_post:v_Self -> Prims.unit -> bool; + f_method_f_pre:v_Self -> Type0; + f_method_f_post:v_Self -> Prims.unit -> Type0; f_method_f:x0: v_Self -> Prims.Pure Prims.unit (f_method_f_pre x0) (fun result -> f_method_f_post x0 result); - f_assoc_type_pre:{| i3: Core.Marker.t_Copy f_AssocType |} -> f_AssocType -> bool; - f_assoc_type_post:{| i3: Core.Marker.t_Copy f_AssocType |} -> f_AssocType -> Prims.unit -> bool; + f_assoc_type_pre:{| i3: Core.Marker.t_Copy f_AssocType |} -> f_AssocType -> Type0; + f_assoc_type_post:{| i3: Core.Marker.t_Copy f_AssocType |} -> f_AssocType -> Prims.unit -> Type0; f_assoc_type:{| i3: Core.Marker.t_Copy f_AssocType |} -> x0: f_AssocType -> Prims.Pure Prims.unit (f_assoc_type_pre #i3 x0)