Pre post impl blocks

.utils/expand.sh

@@ -0,0 +1,8 @@
+#!/usr/bin/env bash
+
+# This script expands a crate so that one can inspect macro expansion
+# by hax. It is a wrapper around `cargo expand` that inject the
+# required rustc flags.
+
+RUSTFLAGS='-Zcrate-attr=register_tool(_hax) -Zcrate-attr=feature(register_tool) --cfg hax_compilation --cfg _hax --cfg hax --cfg hax_backend_fstar --cfg hax' cargo expand "$@"
+

engine/lib/attr_payloads.ml

@@ -161,10 +161,6 @@ module Make (F : Features.T) (Error : Phase_utils.ERROR) = struct
     val expect_expr :
       ?keep_last_args:int -> generics * param list * expr -> expr
 
-    val associated_expr_rebinding :
-      span -> pat list -> AssocRole.t -> attrs -> expr option
-    (** Looks up an expression but takes care of rebinding free variables. *)
-
     val associated_refinement_in_type :
       span -> string list -> attrs -> expr option
     (** For type, there is a special treatment. The name of fields are
@@ -277,55 +273,6 @@ module Make (F : Features.T) (Error : Phase_utils.ERROR) = struct
         attrs -> expr list =
       associated_fns role >> List.map ~f:(expect_expr ~keep_last_args)
 
-    let associated_expr_rebinding span (params : pat list) (role : AssocRole.t)
-        (attrs : attrs) : expr option =
-      let* _, original_params, body = associated_fn role attrs in
-      let original_params =
-        List.map ~f:(fun param -> param.pat) original_params
-      in
-      let vars_of_pat =
-        U.Reducers.collect_local_idents#visit_pat () >> Set.to_list
-      in
-      let original_vars = List.concat_map ~f:vars_of_pat original_params in
-      let target_vars = List.concat_map ~f:vars_of_pat params in
-      let mk_error_message prefix =
-        prefix ^ "\n" ^ "\n - original_vars: "
-        ^ [%show: local_ident list] original_vars
-        ^ "\n - target_vars: "
-        ^ [%show: local_ident list] target_vars
-        ^ "\n\n - original_params: "
-        ^ [%show: pat list] original_params
-        ^ "\n - params: "
-        ^ [%show: pat list] params
-      in
-      let replacements =
-        List.zip_opt original_vars target_vars
-        |> Option.value_or_thunk ~default:(fun _ ->
-               let details =
-                 mk_error_message
-                   "associated_expr_rebinding: zip two lists of different \
-                    lengths (original_vars and target_vars)"
-               in
-               Error.unimplemented ~details span)
-      in
-      let replacements =
-        match Map.of_alist (module Local_ident) replacements with
-        | `Ok replacements -> replacements
-        | `Duplicate_key key ->
-            let details =
-              mk_error_message
-                "associated_expr_rebinding: of_alist failed because `"
-              ^ [%show: local_ident] key
-              ^ "` is a duplicate key. Context: "
-            in
-            Error.unimplemented ~details span
-      in
-      Some
-        ((U.Mappers.rename_local_idents (fun v ->
-              Map.find replacements v |> Option.value ~default:v))
-           #visit_expr
-           () body)
-
     let associated_refinement_in_type span (free_variables : string list) :
         attrs -> expr option =
       associated_fn Refine

engine/lib/phases/phase_traits_specs.ml

@@ -100,44 +100,43 @@ module Make (F : Features.T) =
                   match item.ii_v with
                   | IIFn { params = []; _ } -> []
                   | IIFn { body; params } ->
-                      let out_ident =
-                        U.fresh_local_ident_in
-                          (U.Reducers.collect_local_idents#visit_impl_item ()
-                             item
-                          |> Set.to_list)
-                          "out"
-                      in
-                      let params_pat =
-                        List.map ~f:(fun param -> param.pat) params
-                      in
-                      let pat = U.make_var_pat out_ident body.typ body.span in
-                      let typ = body.typ in
-                      let out = { pat; typ; typ_span = None; attrs = [] } in
+                      (* We always need to produce a pre and a post
+                         condition implementation for each method in
+                         the impl. *)
                       [
-                        {
-                          (mk "pre") with
-                          ii_v =
-                            IIFn
-                              {
-                                body =
-                                  Attrs.associated_expr_rebinding item.ii_span
-                                    params_pat Requires item.ii_attrs
-                                  |> Option.value ~default;
-                                params;
-                              };
-                        };
-                        {
-                          (mk "post") with
-                          ii_v =
-                            IIFn
-                              {
-                                body =
-                                  Attrs.associated_expr_rebinding item.ii_span
-                                    (params_pat @ [ pat ]) Ensures item.ii_attrs
-                                  |> Option.value ~default;
-                                params = params @ [ out ];
-                              };
-                        };
+                        (let params, body =
+                           match Attrs.associated_fn Requires item.ii_attrs with
+                           | Some (_, params, body) -> (params, body)
+                           | None -> (params, default)
+                         in
+                         { (mk "pre") with ii_v = IIFn { body; params } });
+                        (let params, body =
+                           match Attrs.associated_fn Ensures item.ii_attrs with
+                           | Some (_, params, body) -> (params, body)
+                           | None ->
+                               (* There is no explicit post-condition
+                                  on this method. We need to define a
+                                  trivial one. *)
+                               (* Post-condition *always* an extra
+                                  argument in final position for the
+                                  output. *)
+                               let out_ident =
+                                 U.fresh_local_ident_in
+                                   (U.Reducers.collect_local_idents
+                                      #visit_impl_item () item
+                                   |> Set.to_list)
+                                   "out"
+                               in
+                               let pat =
+                                 U.make_var_pat out_ident body.typ body.span
+                               in
+                               let typ = body.typ in
+                               let out =
+                                 { pat; typ; typ_span = None; attrs = [] }
+                               in
+                               (params @ [ out ], default)
+                         in
+                         { (mk "post") with ii_v = IIFn { body; params } });
                       ]
                   | IIType _ -> []
                 in

flake.nix

@@ -159,6 +159,7 @@
                 mkdir -p $out/bin
                 cp ${./.utils/rebuild.sh} $out/bin/rebuild
                 cp ${./.utils/list-names.sh} $out/bin/list-names
+                cp ${./.utils/expand.sh} $out/bin/expand-hax-macros
               '';
           };
           packages = [

tests/attributes/src/lib.rs

@@ -338,3 +338,46 @@ mod verifcation_status {
         let still_not_much = not_much + nothing;
     }
 }
+
+mod requires_mut {
+    use hax_lib::int::*;
+
+    #[hax_lib::attributes]
+    trait Foo {
+        #[hax_lib::requires(x.lift() + y.lift() < int!(254))]
+        #[hax_lib::ensures(|output_variable| output_variable == *future(y))]
+        fn f(x: u8, y: &mut u8) -> u8;
+
+        fn g(x: u8, y: u8) -> u8;
+        fn h(x: u8, y: u8);
+        fn i(x: u8, y: &mut u8);
+    }
+
+    #[hax_lib::attributes]
+    impl Foo for () {
+        #[hax_lib::requires(x.lift() + y.lift() < int!(254))]
+        #[hax_lib::ensures(|output_variable| output_variable == *future(y))]
+        fn f(x: u8, y: &mut u8) -> u8 {
+            *y += x;
+            *y
+        }
+
+        #[hax_lib::requires(true)]
+        #[hax_lib::ensures(|output_variable| output_variable == y)]
+        fn g(x: u8, y: u8) -> u8 {
+            y
+        }
+
+        #[hax_lib::requires(true)]
+        #[hax_lib::ensures(|output_variable| output_variable == ())]
+        fn h(x: u8, y: u8) {
+            ()
+        }
+
+        #[hax_lib::requires(true)]
+        #[hax_lib::ensures(|out| *future(y) == *y)]
+        fn i(x: u8, y: &mut u8) {
+            ()
+        }
+    }
+}