fix(backend/fstar): pre/post are Type0 predicates, not boolean pred…

…icates

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

@@ -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

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)
 }

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)
 }

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)
 }

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)
 }
 

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,15 +217,15 @@ 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 ->
       v_Self ->
       v_TypeArg ->
       t_Type v_TypeArg v_ConstArg ->
       Prims.unit
-    -> bool;
+    -> Type0;
   f_method:
       #v_MethodTypeArg: Type0 ->
       v_MethodConstArg: usize ->
@@ -241,15 +241,15 @@ 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 ->
       v_Self ->
       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)