fix(engine/F*): self_ -> self for clauses of methods

Consider the following piece of code:
```rust
struct S(pub  u8);

impl S {
    #[hax_lib::requires(self.0 == 0)]
    fn f(&self) {}
}
```

The `requires` annotation produces a standalone function that looks like the following:

```rust
fn requires(self_: S) -> bool {
    self_.0 == 0
}
```

Here, we can't use `self`: this is a reserved keyword in Rust, and we are not in a `impl` context.
Thus, the macro renames `self` into `self_`.
The bug described in #1276 comes from this renaming not being reverted in the engine.

With this commit, when the F* backend inteprets
such clauses, if the function on which a clause
exists have a `self` as first argument, we now
substitute the first argument of the clause
function to replace it with the first argument of
the original function.
In the example above, we replace `self_` with `self`.

This PR also improves the macro to always pick a fresh name, not always `self_`.

Author: W95Psp

engine/backends/fstar/fstar_backend.ml

@@ -867,15 +867,31 @@ struct
         F.mk_refined binder_name (pty span ty) (fun ~x -> pexpr refinement)
     | None -> pty span ty
 
-  (* let prefined_ty span (binder : string) (ty : ty) (refinement : expr) : *)
-  (*     F.AST.term = *)
-  (*   F.mk_refined binder (pty span ty) (pexpr refinement) *)
-
-  let add_clauses_effect_type ~no_tot_abbrev (attrs : attrs) typ : F.AST.typ =
+  let add_clauses_effect_type ~self ~no_tot_abbrev (attrs : attrs) typ :
+      F.AST.typ =
     let attr_term ?keep_last_args ?map_expr kind f =
+      (* A clause on a method with a `self` produces a function whose first argument is `self_`.
+         `subst_self` will substitute that first argument `self_` into the provided local identifier `self`.
+      *)
+      let subst_self : (expr -> expr) option =
+        (* If `self` was present on the original function.  *)
+        let* self = self in
+        (* Lookup the pre/post/decreases function, get the first argument: that is `self`. *)
+        let* self' =
+          let* _, params, _ = Attrs.associated_fn kind attrs in
+          let* first_param = List.hd params in
+          let* { var; _ } = Destruct.pat_PBinding first_param.pat in
+          Some var
+        in
+        let f id = if [%eq: local_ident] self' id then self else id in
+        Some ((U.Mappers.rename_local_idents f)#visit_expr ())
+      in
       Attrs.associated_expr ?keep_last_args kind attrs
       |> Option.map
-           ~f:(Option.value ~default:Fn.id map_expr >> pexpr >> f >> F.term)
+           ~f:
+             (Option.value ~default:Fn.id subst_self
+             >> Option.value ~default:Fn.id map_expr
+             >> pexpr >> f >> F.term)
     in
     let decreases =
       let visitor =
@@ -1030,6 +1046,11 @@ struct
         let is_const = List.is_empty params in
         let ty =
           add_clauses_effect_type
+            ~self:
+              (let* hd = List.hd params in
+               let* { var; _ } = Destruct.pat_PBinding hd.pat in
+               let*? () = String.equal var.name "self" in
+               Some var)
             ~no_tot_abbrev:(ctx.interface_mode && not is_const)
             e.attrs (pty body.span body.typ)
         in

hax-lib/macros/Cargo.toml

@@ -19,7 +19,7 @@ paste = { version = "1.0.15" }
 syn = { version = "2.0", features = ["full", "visit-mut", "visit"] }
 
 [dependencies]
-syn = { version = "2.0", features = ["full", "visit-mut"] }
+syn = { version = "2.0", features = ["full", "visit", "visit-mut"] }
 proc-macro2 = { workspace = true }
 quote = { workspace = true }
 

hax-lib/macros/src/utils.rs

@@ -1,3 +1,5 @@
+use syn::visit::Visit;
+
 use crate::prelude::*;
 use crate::rewrite_self::*;
 
@@ -140,6 +142,29 @@ pub(crate) fn expect_future_expr(e: &Expr) -> Option<std::result::Result<Ident,
     None
 }
 
+#[derive(Default)]
+pub struct IdentCollector {
+    pub idents: Vec<Ident>,
+}
+
+impl<'ast> syn::visit::Visit<'ast> for IdentCollector {
+    fn visit_ident(&mut self, ident: &'ast Ident) {
+        self.idents.push(ident.clone());
+    }
+}
+
+impl IdentCollector {
+    /// Returns a fresh identifier with the given prefix that is not in the collected identifiers.
+    pub fn fresh_ident(&self, prefix: &str) -> Ident {
+        let idents: HashSet<&Ident> = HashSet::from_iter(self.idents.iter());
+        let mk = |s| Ident::new(s, Span::call_site());
+        std::iter::once(mk(prefix))
+            .chain((0u64..).map(|i| Ident::new(&format!("{}{}", prefix, i), Span::call_site())))
+            .find(|ident| !idents.contains(ident))
+            .unwrap()
+    }
+}
+
 /// Rewrites `future(x)` nodes in an expression when (1) `x` is an
 /// ident and (2) the ident `x` is contained in the HashSet.
 struct RewriteFuture(HashSet<String>);
@@ -206,7 +231,12 @@ pub fn make_fn_decoration(
     mut generics: Option<Generics>,
     self_type: Option<Type>,
 ) -> (TokenStream, AttrPayload) {
-    let self_ident: Ident = syn::parse_quote! {self_};
+    let self_ident: Ident = {
+        let mut idents = IdentCollector::default();
+        idents.visit_expr(&phi);
+        idents.visit_signature(&signature);
+        idents.fresh_ident("self_")
+    };
     let error = {
         let mut rewriter = RewriteSelf::new(self_ident, self_type);
         rewriter.visit_expr_mut(&mut phi);

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

@@ -126,6 +126,19 @@ class t_T (v_Self: Type0) = {
   f_v:x0: v_Self -> Prims.Pure v_Self (f_v_pre x0) (fun result -> f_v_post x0 result)
 }
 '''
+"Attributes.Issue_1276_.fst" = '''
+module Attributes.Issue_1276_
+#set-options "--fuel 0 --ifuel 1 --z3rlimit 15"
+open Core
+open FStar.Mul
+
+type t_S = | S : u8 -> t_S
+
+let impl_S__f (self: t_S) (self_ self_0_ self_1_ self_2_: u8)
+    : Prims.Pure Prims.unit
+      (requires self._0 =. mk_u8 0 && self_ =. self_1_ && self_2_ =. mk_u8 9)
+      (fun _ -> Prims.l_True) = ()
+'''
 "Attributes.Nested_refinement_elim.fst" = '''
 module Attributes.Nested_refinement_elim
 #set-options "--fuel 0 --ifuel 1 --z3rlimit 15"

tests/attributes/src/lib.rs

@@ -434,3 +434,13 @@ mod props {
         !(p | y).implies(forall(|x: u8| x <= u8::MAX) & exists(|x: u16| x > 300))
     }
 }
+
+mod issue_1276 {
+    struct S(pub u8);
+
+    #[hax_lib::attributes]
+    impl S {
+        #[hax_lib::requires(self.0 == 0 && self_ == self_1 && self_2 == 9)]
+        fn f(&self, self_: u8, self_0: u8, self_1: u8, self_2: u8) {}
+    }
+}