Merge pull request #1267 from cryspen/fix-mut-borrow-self-ensures-clause

fix(hax-lib/macros): handle correctly `&mut Self` arguments in `ensures`

.github/workflows/test_installs.yml

@@ -22,7 +22,7 @@ jobs:
           - ubuntu-latest
           - ubuntu-20.04
           - macos-latest
-          - macos-12
+          - macos-13
     runs-on: ${{ matrix.os }}
     steps:
     - uses: actions/checkout@v3

hax-lib/macros/src/utils.rs

@@ -218,8 +218,6 @@ pub fn make_fn_decoration(
     mut generics: Option<Generics>,
     self_type: Option<Type>,
 ) -> (TokenStream, AttrPayload) {
-    let uid = ItemUid::fresh();
-    let mut_ref_inputs = unmut_references_in_inputs(&mut signature);
     let self_ident: Ident = syn::parse_quote! {self_};
     let error = {
         let mut rewriter = RewriteSelf::new(self_ident, self_type);
@@ -230,6 +228,8 @@ pub fn make_fn_decoration(
         }
         rewriter.get_error()
     };
+    let uid = ItemUid::fresh();
+    let mut_ref_inputs = unmut_references_in_inputs(&mut signature);
     let decoration = {
         let decoration_sig = {
             let mut sig = signature.clone();

test-harness/src/snapshots/toolchain__attributes into-fstar.snap

@@ -114,6 +114,18 @@ unfold instance impl: Core.Ops.Arith.t_Sub t_Int t_Int =
 
 unfold let add x y = x + y
 '''
+"Attributes.Issue_1266_.fst" = '''
+module Attributes.Issue_1266_
+#set-options "--fuel 0 --ifuel 1 --z3rlimit 15"
+open Core
+open FStar.Mul
+
+class t_T (v_Self: Type0) = {
+  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)
+}
+'''
 "Attributes.Nested_refinement_elim.fst" = '''
 module Attributes.Nested_refinement_elim
 #set-options "--fuel 0 --ifuel 1 --z3rlimit 15"

tests/attributes/src/lib.rs

@@ -381,3 +381,11 @@ mod requires_mut {
         }
     }
 }
+
+mod issue_1266 {
+    #[hax_lib::attributes]
+    trait T {
+        #[hax_lib::ensures(|_|true)]
+        fn v(x: &mut Self);
+    }
+}