Repository: cryspen/hax (language: rust)

Issue:
Trait methods are not moved by bundling
```rust

pub mod main {
    impl Tr for nested::St {
        fn f(self) {}
    }
    pub trait Tr {
        fn f(self);
    }
    
    pub mod nested {
        use super::Tr;
        pub struct St {}
        fn g(x: St) {
            x.f()
        }
    }
}
```
[Open this code snippet in the playground](https://hax-playground.cryspen.com/#fstar/5ca1c13023/gist=c719fd86221ea6fa1645bc719c71b488)

Here `main` and `nested` are bundled together but `x.f()` in `g` is translated to `Main.f_f` instead of just `f_f` because we don't do the renaming of trait methods.



Discussion / hints:

Fix patch:
diff --git a/engine/backends/fstar/fstar_backend.ml b/engine/backends/fstar/fstar_backend.ml
index dc01e4cbd..fe956b435 100644
--- a/engine/backends/fstar/fstar_backend.ml
+++ b/engine/backends/fstar/fstar_backend.ml
@@ -1865,6 +1865,9 @@ let apply_phases (bo : BackendOptions.t) (items : Ast.Rust.item list) :
     (* else *)
     items
   in
+  (* This is a hack that should be removed
+     (see https://github.com/hacspec/hax/issues/1078) *)
+  Dependencies.includes_for_bundled_trait_methods := true;
   let items =
     TransformToInputLanguage.ditems items
     |> List.map ~f:unsize_as_identity
diff --git a/engine/hax-engine.opam b/engine/hax-engine.opam
index af7aeae3e..8143bdf07 100644
--- a/engine/hax-engine.opam
+++ b/engine/hax-engine.opam
@@ -61,5 +61,5 @@ depexts: [
   ["nodejs"] {}
 ]
 pin-depends: [
-  ["ocamlgraph" "git+https://github.com/maximebuyse/ocamlgraph.git#fix-stable-topological-sort"]
-]
\ No newline at end of file
+  ["ocamlgraph.dev" "git+https://github.com/maximebuyse/ocamlgraph.git#fix-stable-topological-sort"]
+]
diff --git a/engine/hax-engine.opam.template b/engine/hax-engine.opam.template
index 593f86aaa..7eb512d76 100644
--- a/engine/hax-engine.opam.template
+++ b/engine/hax-engine.opam.template
@@ -2,5 +2,5 @@ depexts: [
   ["nodejs"] {}
 ]
 pin-depends: [
-  ["ocamlgraph" "git+https://github.com/maximebuyse/ocamlgraph.git#fix-stable-topological-sort"]
-]
\ No newline at end of file
+  ["ocamlgraph.dev" "git+https://github.com/maximebuyse/ocamlgraph.git#fix-stable-topological-sort"]
+]
diff --git a/engine/lib/dependencies.ml b/engine/lib/dependencies.ml
index e314571a1..aecdec51f 100644
--- a/engine/lib/dependencies.ml
+++ b/engine/lib/dependencies.ml
@@ -1,5 +1,9 @@
 open! Prelude
 
+(** This is a hack that should be removed
+    (see https://github.com/hacspec/hax/issues/1078) *)
+let includes_for_bundled_trait_methods = ref false
+
 module Make (F : Features.T) = struct
   module AST = Ast.Make (F)
   module U = Ast_utils.Make (F)
@@ -561,16 +565,33 @@ module Make (F : Features.T) = struct
                     ( name,
                       Concrete_ident.Create.move_under ~new_parent:new_name name
                     )))
+        | Some { v = Trait { items; _ }; _ }
+          when !includes_for_bundled_trait_methods ->
+            List.map items ~f:(fun { ti_ident; _ } ->
+                ( ti_ident,
+                  Concrete_ident.Create.move_under ~new_parent:new_name ti_ident
+                ))
         | _ -> []
       in
       let variant_and_constructors_renamings =
         List.concat_map ~f:variants_renamings renamings
         |> List.concat_map ~f:(fun (old_name, new_name) ->
-               [
-                 (old_name, new_name);
-                 ( Concrete_ident.Create.constructor old_name,
-                   Concrete_ident.Create.constructor new_name );
-               ])
+               let trait_methods_renamings =
+                 match from_ident old_name with
+                 | Some { v = Trait { items; _ }; _ }
+                   when not !includes_for_bundled_trait_methods ->
+                     List.map items ~f:(fun { ti_ident; _ } ->
+                         ( ti_ident,
+                           Concrete_ident.Create.move_under ~new_parent:new_name
+                             ti_ident ))
+                 | _ -> []
+               in
+               trait_methods_renamings
+               @ [
+                   (old_name, new_name);
+                   ( Concrete_ident.Create.constructor old_name,
+                     Concrete_ident.Create.constructor new_name );
+                 ])
       in
       let renamings =
         match
diff --git a/engine/lib/dependencies.mli b/engine/lib/dependencies.mli
index c4ba68881..ccb14ffce 100644
--- a/engine/lib/dependencies.mli
+++ b/engine/lib/dependencies.mli
@@ -9,3 +9,7 @@ module Make (F : Features.T) : sig
   val filter_by_inclusion_clauses :
     Types.inclusion_clause list -> AST.item list -> AST.item list
 end
+
+val includes_for_bundled_trait_methods : bool ref
+(** This is a hack that should be removed
+    (see https://github.com/hacspec/hax/issues/1078) *)


Test patch:
diff --git a/test-harness/src/snapshots/toolchain__cyclic-modules into-fstar.snap b/test-harness/src/snapshots/toolchain__cyclic-modules into-fstar.snap
index e3ef061c7..077c9eb31 100644
--- a/test-harness/src/snapshots/toolchain__cyclic-modules into-fstar.snap
+++ b/test-harness/src/snapshots/toolchain__cyclic-modules into-fstar.snap
@@ -259,6 +259,56 @@ include Cyclic_modules.M1.Cyclic_bundle_892895908 {b as b}
 
 include Cyclic_modules.M1.Cyclic_bundle_892895908 {c as c}
 '''
+"Cyclic_modules.Moved_trait.Cyclic_bundle_202498800.fst" = '''
+module Cyclic_modules.Moved_trait.Cyclic_bundle_202498800
+#set-options "--fuel 0 --ifuel 1 --z3rlimit 15"
+open Core
+open FStar.Mul
+
+class v_Tr (v_Self: Type0) = {
+  f_f_pre:v_Self -> Type0;
+  f_f_post:v_Self -> Prims.unit -> Type0;
+  f_f:x0: v_Self -> Prims.Pure Prims.unit (f_f_pre x0) (fun result -> f_f_post x0 result)
+}
+
+type t_St = | St : t_St
+
+[@@ FStar.Tactics.Typeclasses.tcinstance]
+let impl: v_Tr t_St =
+  {
+    f_f_pre = (fun (self: t_St) -> true);
+    f_f_post = (fun (self: t_St) (out: Prims.unit) -> true);
+    f_f = fun (self: t_St) -> ()
+  }
+
+let g (x: t_St) : Prims.unit = f_f #t_St #FStar.Tactics.Typeclasses.solve x
+'''
+"Cyclic_modules.Moved_trait.Nested.fst" = '''
+module Cyclic_modules.Moved_trait.Nested
+#set-options "--fuel 0 --ifuel 1 --z3rlimit 15"
+open Core
+open FStar.Mul
+
+include Cyclic_modules.Moved_trait.Cyclic_bundle_202498800 {t_St as t_St}
+
+include Cyclic_modules.Moved_trait.Cyclic_bundle_202498800 {g as g}
+'''
+"Cyclic_modules.Moved_trait.fst" = '''
+module Cyclic_modules.Moved_trait
+#set-options "--fuel 0 --ifuel 1 --z3rlimit 15"
+open Core
+open FStar.Mul
+
+include Cyclic_modules.Moved_trait.Cyclic_bundle_202498800 {impl as impl}
+
+include Cyclic_modules.Moved_trait.Cyclic_bundle_202498800 {v_Tr as v_Tr}
+
+include Cyclic_modules.Moved_trait.Cyclic_bundle_202498800 {f_f_pre as f_f_pre}
+
+include Cyclic_modules.Moved_trait.Cyclic_bundle_202498800 {f_f_post as f_f_post}
+
+include Cyclic_modules.Moved_trait.Cyclic_bundle_202498800 {f_f as f_f}
+'''
 "Cyclic_modules.Rec.fst" = '''
 module Cyclic_modules.Rec
 #set-options "--fuel 0 --ifuel 1 --z3rlimit 15"
diff --git a/tests/cyclic-modules/src/lib.rs b/tests/cyclic-modules/src/lib.rs
index 216a54812..cb45f7b82 100644
--- a/tests/cyclic-modules/src/lib.rs
+++ b/tests/cyclic-modules/src/lib.rs
@@ -178,3 +178,20 @@ pub mod late_skip_b {
         super::late_skip_a::f()
     }
 }
+
+pub mod moved_trait {
+    impl Tr for nested::St {
+        fn f(self) {}
+    }
+    pub trait Tr {
+        fn f(self);
+    }
+
+    pub mod nested {
+        use super::Tr;
+        pub struct St {}
+        fn g(x: St) {
+            x.f()
+        }
+    }
+}