Merge pull request #1075 from cryspen/fix-1068

Move trait methods in cyclic dependencies bundling.

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

engine/hax-engine.opam

@@ -61,5 +61,5 @@ depexts: [
   ["nodejs"] {}
 ]
 pin-depends: [
-  ["ocamlgraph" "git+https://github.com/maximebuyse/ocamlgraph.git#fix-stable-topological-sort"]
-]
+  ["ocamlgraph.dev" "git+https://github.com/maximebuyse/ocamlgraph.git#fix-stable-topological-sort"]
+]

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"]
-]
+  ["ocamlgraph.dev" "git+https://github.com/maximebuyse/ocamlgraph.git#fix-stable-topological-sort"]
+]

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

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

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