Repository: cryspen/hax (language: rust)

Issue:
Stable name for rec bundles
Rec bundles have names that contain a hash. This is problematic because if the content of the bundle changes the name of the generated file also changes which makes it hard to manage projects. We should instead generate a name using the names of the modules that compose the bundle, with a disambiguation only if needed.
clash of impl names in rec bundles (disambiguators are no longer valid)
impls coming from different modules in a recursive bundles don't get a new disambiguator so the names can clash.


Discussion / hints:

Fix patch:
diff --git a/engine/lib/concrete_ident/concrete_ident.ml b/engine/lib/concrete_ident/concrete_ident.ml
index b0d0cc160..75505210d 100644
--- a/engine/lib/concrete_ident/concrete_ident.ml
+++ b/engine/lib/concrete_ident/concrete_ident.ml
@@ -596,17 +596,16 @@ module Create = struct
     let len x = List.length x.def_id.path in
     let compare x y = len x - len y in
     let id = List.min_elt ~compare from |> Option.value_exn in
-    let parent = parent id in
     {
       kind = Kind.Value;
       def_id =
         {
-          parent.def_id with
+          id.def_id with
           path =
-            parent.def_id.path
+            id.def_id.path
             @ [
                 {
-                  data = TypeNs "rec_bundle";
+                  data = TypeNs "cyclic_bundle";
                   disambiguator = [%hash: t list] from;
                 };
               ];
@@ -635,6 +634,17 @@ module Create = struct
   let constructor name =
     let path = name.def_id.path @ [ { data = Ctor; disambiguator = 0 } ] in
     { name with def_id = { name.def_id with path } }
+
+  let add_disambiguator name disambiguator =
+    let path = name.def_id.path in
+    if List.is_empty path then name
+    else
+      (* The following two `exn` function calls cannot fail as the path is not empty. *)
+      let last = List.last_exn path in
+      let path =
+        List.drop_last_exn path @ [ { data = last.data; disambiguator } ]
+      in
+      { name with def_id = { name.def_id with path } }
 end
 
 let lookup_raw_impl_info (impl : t) : Types.impl_infos option =
diff --git a/engine/lib/concrete_ident/concrete_ident.mli b/engine/lib/concrete_ident/concrete_ident.mli
index e87f71b22..545a23da3 100644
--- a/engine/lib/concrete_ident/concrete_ident.mli
+++ b/engine/lib/concrete_ident/concrete_ident.mli
@@ -27,6 +27,7 @@ val eq_name : name -> t -> bool
 val to_debug_string : t -> string
 
 module Create : sig
+  val parent : t -> t
   val fresh_module : from:t list -> t
   val move_under : new_parent:t -> t -> t
 
@@ -37,6 +38,10 @@ module Create : sig
   val map_last : f:(string -> string) -> t -> t
   (** [map_last f ident] applies [f] on the last chunk of [ident]'s
       path if it holds a string *)
+
+  val add_disambiguator : t -> int -> t
+  (** [add_disambiguator ident d] changes the disambiguator on
+      the last chunk of [ident]'s path to [d] *)
 end
 
 type view = { crate : string; path : string list; definition : string }
diff --git a/engine/lib/dependencies.ml b/engine/lib/dependencies.ml
index 6637e60c8..72819746b 100644
--- a/engine/lib/dependencies.ml
+++ b/engine/lib/dependencies.ml
@@ -413,8 +413,12 @@ module Make (F : Features.T) = struct
     in
 
     let transform (bundle : item list) =
+      let module_names =
+        List.map ~f:(ident_of >> Concrete_ident.Create.parent) bundle
+        |> List.dedup_and_sort ~compare:Concrete_ident.compare
+      in
       let ns : Concrete_ident.t =
-        Concrete_ident.Create.fresh_module ~from:(List.map ~f:ident_of bundle)
+        Concrete_ident.Create.fresh_module ~from:module_names
       in
       let new_name_under_ns : Concrete_ident.t -> Concrete_ident.t =
         Concrete_ident.Create.move_under ~new_parent:ns
@@ -431,10 +435,7 @@ module Make (F : Features.T) = struct
             (List.mem duplicates (new_name_under_ns id)
                ~equal:Concrete_ident.equal)
         then id
-        else
-          Concrete_ident.Create.map_last
-            ~f:(fun name -> name ^ (Concrete_ident.hash id |> Int.to_string))
-            id
+        else Concrete_ident.Create.add_disambiguator id (Concrete_ident.hash id)
       in
       let renamings =
         List.map


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 af07fc045..1cb9dc501 100644
--- a/test-harness/src/snapshots/toolchain__cyclic-modules into-fstar.snap
+++ b/test-harness/src/snapshots/toolchain__cyclic-modules into-fstar.snap
@@ -32,7 +32,7 @@ module Cyclic_modules.B
 open Core
 open FStar.Mul
 
-include Cyclic_modules.Rec_bundle_318256792 {g as g}
+include Cyclic_modules.Cyclic_bundle_367033742 {g as g}
 '''
 "Cyclic_modules.C.fst" = '''
 module Cyclic_modules.C
@@ -42,8 +42,24 @@ open FStar.Mul
 
 let i (_: Prims.unit) : Prims.unit = ()
 '''
-"Cyclic_modules.D.Rec_bundle_773034964.fst" = '''
-module Cyclic_modules.D.Rec_bundle_773034964
+"Cyclic_modules.Cyclic_bundle_367033742.fst" = '''
+module Cyclic_modules.Cyclic_bundle_367033742
+#set-options "--fuel 0 --ifuel 1 --z3rlimit 15"
+open Core
+open FStar.Mul
+
+let f (_: Prims.unit) : Prims.unit = ()
+
+let g (_: Prims.unit) : Prims.unit = f ()
+
+let h (_: Prims.unit) : Prims.unit =
+  let _:Prims.unit = g () in
+  Cyclic_modules.C.i ()
+
+let h2 (_: Prims.unit) : Prims.unit = Cyclic_modules.C.i ()
+'''
+"Cyclic_modules.D.Cyclic_bundle_81544935.fst" = '''
+module Cyclic_modules.D.Cyclic_bundle_81544935
 #set-options "--fuel 0 --ifuel 1 --z3rlimit 15"
 open Core
 open FStar.Mul
@@ -62,9 +78,9 @@ module Cyclic_modules.D
 open Core
 open FStar.Mul
 
-include Cyclic_modules.D.Rec_bundle_773034964 {d1 as d1}
+include Cyclic_modules.D.Cyclic_bundle_81544935 {d1 as d1}
 
-include Cyclic_modules.D.Rec_bundle_773034964 {d2 as d2}
+include Cyclic_modules.D.Cyclic_bundle_81544935 {d2 as d2}
 '''
 "Cyclic_modules.De.fst" = '''
 module Cyclic_modules.De
@@ -72,10 +88,10 @@ module Cyclic_modules.De
 open Core
 open FStar.Mul
 
-include Cyclic_modules.D.Rec_bundle_773034964 {de1 as de1}
+include Cyclic_modules.D.Cyclic_bundle_81544935 {de1 as de1}
 '''
-"Cyclic_modules.Disjoint_cycle_a.Rec_bundle_317759688.fst" = '''
-module Cyclic_modules.Disjoint_cycle_a.Rec_bundle_317759688
+"Cyclic_modules.Disjoint_cycle_a.Cyclic_bundle_177270903.fst" = '''
+module Cyclic_modules.Disjoint_cycle_a.Cyclic_bundle_177270903
 #set-options "--fuel 0 --ifuel 1 --z3rlimit 15"
 open Core
 open FStar.Mul
@@ -94,9 +110,9 @@ module Cyclic_modules.Disjoint_cycle_a
 open Core
 open FStar.Mul
 
-include Cyclic_modules.Disjoint_cycle_a.Rec_bundle_317759688 {g as g}
+include Cyclic_modules.Disjoint_cycle_a.Cyclic_bundle_177270903 {g as g}
 
-include Cyclic_modules.Disjoint_cycle_a.Rec_bundle_317759688 {f as f}
+include Cyclic_modules.Disjoint_cycle_a.Cyclic_bundle_177270903 {f as f}
 '''
 "Cyclic_modules.Disjoint_cycle_b.fst" = '''
 module Cyclic_modules.Disjoint_cycle_b
@@ -104,9 +120,9 @@ module Cyclic_modules.Disjoint_cycle_b
 open Core
 open FStar.Mul
 
-include Cyclic_modules.Disjoint_cycle_a.Rec_bundle_317759688 {h as h}
+include Cyclic_modules.Disjoint_cycle_a.Cyclic_bundle_177270903 {h as h}
 
-include Cyclic_modules.Disjoint_cycle_a.Rec_bundle_317759688 {i as i}
+include Cyclic_modules.Disjoint_cycle_a.Cyclic_bundle_177270903 {i as i}
 '''
 "Cyclic_modules.E.fst" = '''
 module Cyclic_modules.E
@@ -114,47 +130,47 @@ module Cyclic_modules.E
 open Core
 open FStar.Mul
 
-include Cyclic_modules.D.Rec_bundle_773034964 {e1 as e1}
+include Cyclic_modules.D.Cyclic_bundle_81544935 {e1 as e1}
 '''
-"Cyclic_modules.Enums_a.fst" = '''
-module Cyclic_modules.Enums_a
+"Cyclic_modules.Enums_a.Cyclic_bundle_1009707801.fst" = '''
+module Cyclic_modules.Enums_a.Cyclic_bundle_1009707801
 #set-options "--fuel 0 --ifuel 1 --z3rlimit 15"
 open Core
 open FStar.Mul
 
-include Cyclic_modules.Enums_b.Rec_bundle_994866580 {t_T240131830 as t_T}
+type t_T_366415196 =
+  | T_366415196_A : t_T_366415196
+  | T_366415196_B : t_T_366415196
+  | T_366415196_C : Alloc.Vec.t_Vec t_T_240131830 Alloc.Alloc.t_Global -> t_T_366415196
 
-include Cyclic_modules.Enums_b.Rec_bundle_994866580 {T240131830_A as T_A}
-
-include Cyclic_modules.Enums_b.Rec_bundle_994866580 {T240131830_B as T_B}
+and t_U =
+  | U_A : t_U
+  | U_B : t_U
+  | U_C : Alloc.Vec.t_Vec t_T_240131830 Alloc.Alloc.t_Global -> t_U
 
-include Cyclic_modules.Enums_b.Rec_bundle_994866580 {T240131830_C as T_C}
+and t_T_240131830 =
+  | T_240131830_A : t_T_240131830
+  | T_240131830_B : t_T_240131830
+  | T_240131830_C : Alloc.Vec.t_Vec t_U Alloc.Alloc.t_Global -> t_T_240131830
+  | T_240131830_D : Alloc.Vec.t_Vec t_T_366415196 Alloc.Alloc.t_Global -> t_T_240131830
 
-include Cyclic_modules.Enums_b.Rec_bundle_994866580 {T240131830_D as T_D}
+let f (_: Prims.unit) : t_T_366415196 = T_366415196_A <: t_T_366415196
 '''
-"Cyclic_modules.Enums_b.Rec_bundle_994866580.fst" = '''
-module Cyclic_modules.Enums_b.Rec_bundle_994866580
+"Cyclic_modules.Enums_a.fst" = '''
+module Cyclic_modules.Enums_a
 #set-options "--fuel 0 --ifuel 1 --z3rlimit 15"
 open Core
 open FStar.Mul
 
-type t_T366415196 =
-  | T366415196_A : t_T366415196
-  | T366415196_B : t_T366415196
-  | T366415196_C : Alloc.Vec.t_Vec t_T240131830 Alloc.Alloc.t_Global -> t_T366415196
+include Cyclic_modules.Enums_a.Cyclic_bundle_1009707801 {t_T_240131830 as t_T}
 
-and t_U =
-  | U_A : t_U
-  | U_B : t_U
-  | U_C : Alloc.Vec.t_Vec t_T240131830 Alloc.Alloc.t_Global -> t_U
+include Cyclic_modules.Enums_a.Cyclic_bundle_1009707801 {T_240131830_A as T_A}
+
+include Cyclic_modules.Enums_a.Cyclic_bundle_1009707801 {T_240131830_B as T_B}
 
-and t_T240131830 =
-  | T240131830_A : t_T240131830
-  | T240131830_B : t_T240131830
-  | T240131830_C : Alloc.Vec.t_Vec t_U Alloc.Alloc.t_Global -> t_T240131830
-  | T240131830_D : Alloc.Vec.t_Vec t_T366415196 Alloc.Alloc.t_Global -> t_T240131830
+include Cyclic_modules.Enums_a.Cyclic_bundle_1009707801 {T_240131830_C as T_C}
 
-let f (_: Prims.unit) : t_T366415196 = T366415196_A <: t_T366415196
+include Cyclic_modules.Enums_a.Cyclic_bundle_1009707801 {T_240131830_D as T_D}
 '''
 "Cyclic_modules.Enums_b.fst" = '''
 module Cyclic_modules.Enums_b
@@ -162,42 +178,42 @@ module Cyclic_modules.Enums_b
 open Core
 open FStar.Mul
 
-include Cyclic_modules.Enums_b.Rec_bundle_994866580 {t_T366415196 as t_T}
+include Cyclic_modules.Enums_a.Cyclic_bundle_1009707801 {t_T_366415196 as t_T}
 
-include Cyclic_modules.Enums_b.Rec_bundle_994866580 {T366415196_A as T_A}
+include Cyclic_modules.Enums_a.Cyclic_bundle_1009707801 {T_366415196_A as T_A}
 
-include Cyclic_modules.Enums_b.Rec_bundle_994866580 {T366415196_B as T_B}
+include Cyclic_modules.Enums_a.Cyclic_bundle_1009707801 {T_366415196_B as T_B}
 
-include Cyclic_modules.Enums_b.Rec_bundle_994866580 {T366415196_C as T_C}
+include Cyclic_modules.Enums_a.Cyclic_bundle_1009707801 {T_366415196_C as T_C}
 
-include Cyclic_modules.Enums_b.Rec_bundle_994866580 {t_U as t_U}
+include Cyclic_modules.Enums_a.Cyclic_bundle_1009707801 {t_U as t_U}
 
-include Cyclic_modules.Enums_b.Rec_bundle_994866580 {U_A as U_A}
+include Cyclic_modules.Enums_a.Cyclic_bundle_1009707801 {U_A as U_A}
 
-include Cyclic_modules.Enums_b.Rec_bundle_994866580 {U_B as U_B}
+include Cyclic_modules.Enums_a.Cyclic_bundle_1009707801 {U_B as U_B}
 
-include Cyclic_modules.Enums_b.Rec_bundle_994866580 {U_C as U_C}
+include Cyclic_modules.Enums_a.Cyclic_bundle_1009707801 {U_C as U_C}
 
-include Cyclic_modules.Enums_b.Rec_bundle_994866580 {f as f}
+include Cyclic_modules.Enums_a.Cyclic_bundle_1009707801 {f as f}
 '''
-"Cyclic_modules.Late_skip_a.fst" = '''
-module Cyclic_modules.Late_skip_a
+"Cyclic_modules.Late_skip_a.Cyclic_bundle_658016071.fst" = '''
+module Cyclic_modules.Late_skip_a.Cyclic_bundle_658016071
 #set-options "--fuel 0 --ifuel 1 --z3rlimit 15"
 open Core
 open FStar.Mul
 
-include Cyclic_modules.Late_skip_b.Rec_bundle_447022631 {f749016415 as f}
+let rec ff_749016415 (_: Prims.unit) : Prims.unit = ff_377825240 ()
+
+and ff_377825240 (_: Prims.unit) : Prims.Pure Prims.unit (requires true) (fun _ -> Prims.l_True) =
+  ff_749016415 ()
 '''
-"Cyclic_modules.Late_skip_b.Rec_bundle_447022631.fst" = '''
-module Cyclic_modules.Late_skip_b.Rec_bundle_447022631
+"Cyclic_modules.Late_skip_a.fst" = '''
+module Cyclic_modules.Late_skip_a
 #set-options "--fuel 0 --ifuel 1 --z3rlimit 15"
 open Core
 open FStar.Mul
 
-let rec f749016415 (_: Prims.unit) : Prims.unit = f377825240 ()
-
-and f377825240 (_: Prims.unit) : Prims.Pure Prims.unit (requires true) (fun _ -> Prims.l_True) =
-  f749016415 ()
+include Cyclic_modules.Late_skip_a.Cyclic_bundle_658016071 {ff_749016415 as f}
 '''
 "Cyclic_modules.Late_skip_b.fst" = '''
 module Cyclic_modules.Late_skip_b
@@ -205,18 +221,10 @@ module Cyclic_modules.Late_skip_b
 open Core
 open FStar.Mul
 
-include Cyclic_modules.Late_skip_b.Rec_bundle_447022631 {f377825240 as f}
-'''
-"Cyclic_modules.M1.fst" = '''
-module Cyclic_modules.M1
-#set-options "--fuel 0 --ifuel 1 --z3rlimit 15"
-open Core
-open FStar.Mul
-
-include Cyclic_modules.M2.Rec_bundle_489499412 {a as a}
+include Cyclic_modules.Late_skip_a.Cyclic_bundle_658016071 {ff_377825240 as f}
 '''
-"Cyclic_modules.M2.Rec_bundle_489499412.fst" = '''
-module Cyclic_modules.M2.Rec_bundle_489499412
+"Cyclic_modules.M1.Cyclic_bundle_892895908.fst" = '''
+module Cyclic_modules.M1.Cyclic_bundle_892895908
 #set-options "--fuel 0 --ifuel 1 --z3rlimit 15"
 open Core
 open FStar.Mul
@@ -231,17 +239,25 @@ let b (_: Prims.unit) : Prims.unit =
   let _:Prims.unit = a () in
   d ()
 '''
+"Cyclic_modules.M1.fst" = '''
+module Cyclic_modules.M1
+#set-options "--fuel 0 --ifuel 1 --z3rlimit 15"
+open Core
+open FStar.Mul
+
+include Cyclic_modules.M1.Cyclic_bundle_892895908 {a as a}
+'''
 "Cyclic_modules.M2.fst" = '''
 module Cyclic_modules.M2
 #set-options "--fuel 0 --ifuel 1 --z3rlimit 15"
 open Core
 open FStar.Mul
 
-include Cyclic_modules.M2.Rec_bundle_489499412 {c as c}
+include Cyclic_modules.M1.Cyclic_bundle_892895908 {c as c}
 
-include Cyclic_modules.M2.Rec_bundle_489499412 {d as d}
+include Cyclic_modules.M1.Cyclic_bundle_892895908 {d as d}
 
-include Cyclic_modules.M2.Rec_bundle_489499412 {b as b}
+include Cyclic_modules.M1.Cyclic_bundle_892895908 {b as b}
 '''
 "Cyclic_modules.Rec.fst" = '''
 module Cyclic_modules.Rec
@@ -273,15 +289,15 @@ and g2 (x: t_T) : t_T =
   | T_t1  -> g1 x
   | T_t2  -> hf x
 '''
-"Cyclic_modules.Rec1_same_name.Rec_bundle_213192514.fst" = '''
-module Cyclic_modules.Rec1_same_name.Rec_bundle_213192514
+"Cyclic_modules.Rec1_same_name.Cyclic_bundle_563905053.fst" = '''
+module Cyclic_modules.Rec1_same_name.Cyclic_bundle_563905053
 #set-options "--fuel 0 --ifuel 1 --z3rlimit 15"
 open Core
 open FStar.Mul
 
-let rec f533409751 (x: i32) : i32 = f91805216 x
+let rec ff_533409751 (x: i32) : i32 = ff_91805216 x
 
-and f91805216 (x: i32) : i32 = if x >. 0l then f533409751 (x -! 1l <: i32) else 0l
+and ff_91805216 (x: i32) : i32 = if x >. 0l then ff_533409751 (x -! 1l <: i32) else 0l
 '''
 "Cyclic_modules.Rec1_same_name.fst" = '''
 module Cyclic_modules.Rec1_same_name
@@ -289,7 +305,7 @@ module Cyclic_modules.Rec1_same_name
 open Core
 open FStar.Mul
 
-include Cyclic_modules.Rec1_same_name.Rec_bundle_213192514 {f533409751 as f}
+include Cyclic_modules.Rec1_same_name.Cyclic_bundle_563905053 {ff_533409751 as f}
 '''
 "Cyclic_modules.Rec2_same_name.fst" = '''
 module Cyclic_modules.Rec2_same_name
@@ -297,42 +313,10 @@ module Cyclic_modules.Rec2_same_name
 open Core
 open FStar.Mul
 
-include Cyclic_modules.Rec1_same_name.Rec_bundle_213192514 {f91805216 as f}
+include Cyclic_modules.Rec1_same_name.Cyclic_bundle_563905053 {ff_91805216 as f}
 '''
-"Cyclic_modules.Rec_bundle_318256792.fst" = '''
-module Cyclic_modules.Rec_bundle_318256792
-#set-options "--fuel 0 --ifuel 1 --z3rlimit 15"
-open Core
-open FStar.Mul
-
-let f (_: Prims.unit) : Prims.unit = ()
-
-let g (_: Prims.unit) : Prims.unit = f ()
-
-let h (_: Prims.unit) : Prims.unit =
-  let _:Prims.unit = g () in
-  Cyclic_modules.C.i ()
-
-let h2 (_: Prims.unit) : Prims.unit = Cyclic_modules.C.i ()
-'''
-"Cyclic_modules.Typ_a.fst" = '''
-module Cyclic_modules.Typ_a
-#set-options "--fuel 0 --ifuel 1 --z3rlimit 15"
-open Core
-open FStar.Mul
-
-include Cyclic_modules.Typ_b.Rec_bundle_546955701 {t_T as t_T}
-
-include Cyclic_modules.Typ_b.Rec_bundle_546955701 {T_T as T_T}
-
-include Cyclic_modules.Typ_b.Rec_bundle_546955701 {t_TRec as t_TRec}
-
-include Cyclic_modules.Typ_b.Rec_bundle_546955701 {TRec_T as TRec_T}
-
-include Cyclic_modules.Typ_b.Rec_bundle_546955701 {TRec_Empty as TRec_Empty}
-'''
-"Cyclic_modules.Typ_b.Rec_bundle_546955701.fst" = '''
-module Cyclic_modules.Typ_b.Rec_bundle_546955701
+"Cyclic_modules.Typ_a.Cyclic_bundle_830459646.fst" = '''
+module Cyclic_modules.Typ_a.Cyclic_bundle_830459646
 #set-options "--fuel 0 --ifuel 1 --z3rlimit 15"
 open Core
 open FStar.Mul
@@ -353,32 +337,48 @@ and t_T1Rec = | T1Rec_T1 : Alloc.Boxed.t_Box t_T2Rec Alloc.Alloc.t_Global -> t_T
 
 and t_T2Rec = | T2Rec_T2 : t_TRec -> t_T2Rec
 '''
+"Cyclic_modules.Typ_a.fst" = '''
+module Cyclic_modules.Typ_a
+#set-options "--fuel 0 --ifuel 1 --z3rlimit 15"
+open Core
+open FStar.Mul
+
+include Cyclic_modules.Typ_a.Cyclic_bundle_830459646 {t_T as t_T}
+
+include Cyclic_modules.Typ_a.Cyclic_bundle_830459646 {T_T as T_T}
+
+include Cyclic_modules.Typ_a.Cyclic_bundle_830459646 {t_TRec as t_TRec}
+
+include Cyclic_modules.Typ_a.Cyclic_bundle_830459646 {TRec_T as TRec_T}
+
+include Cyclic_modules.Typ_a.Cyclic_bundle_830459646 {TRec_Empty as TRec_Empty}
+'''
 "Cyclic_modules.Typ_b.fst" = '''
 module Cyclic_modules.Typ_b
 #set-options "--fuel 0 --ifuel 1 --z3rlimit 15"
 open Core
 open FStar.Mul
 
-include Cyclic_modules.Typ_b.Rec_bundle_546955701 {t_T1 as t_T1}
+include Cyclic_modules.Typ_a.Cyclic_bundle_830459646 {t_T1 as t_T1}
 
-include Cyclic_modules.Typ_b.Rec_bundle_546955701 {T1_T1 as T1_T1}
+include Cyclic_modules.Typ_a.Cyclic_bundle_830459646 {T1_T1 as T1_T1}
 
-include Cyclic_modules.Typ_b.Rec_bundle_546955701 {t_T1_cast_to_repr as t_T1_cast_to_repr}
+include Cyclic_modules.Typ_a.Cyclic_bundle_830459646 {t_T1_cast_to_repr as t_T1_cast_to_repr}
 
-include Cyclic_modules.Typ_b.Rec_bundle_546955701 {t_T2 as t_T2}
+include Cyclic_modules.Typ_a.Cyclic_bundle_830459646 {t_T2 as t_T2}
 
-include Cyclic_modules.Typ_b.Rec_bundle_546955701 {T2_T2 as T2_T2}
+include Cyclic_modules.Typ_a.Cyclic_bundle_830459646 {T2_T2 as T2_T2}
 
-include Cyclic_modules.Typ_b.Rec_bundle_546955701 {t_T1Rec as t_T1Rec}
+include Cyclic_modules.Typ_a.Cyclic_bundle_830459646 {t_T1Rec as t_T1Rec}
 
-include Cyclic_modules.Typ_b.Rec_bundle_546955701 {T1Rec_T1 as T1Rec_T1}
+include Cyclic_modules.Typ_a.Cyclic_bundle_830459646 {T1Rec_T1 as T1Rec_T1}
 
-include Cyclic_modules.Typ_b.Rec_bundle_546955701 {t_T2Rec as t_T2Rec}
+include Cyclic_modules.Typ_a.Cyclic_bundle_830459646 {t_T2Rec as t_T2Rec}
 
-include Cyclic_modules.Typ_b.Rec_bundle_546955701 {T2Rec_T2 as T2Rec_T2}
+include Cyclic_modules.Typ_a.Cyclic_bundle_830459646 {T2Rec_T2 as T2Rec_T2}
 '''
-"Cyclic_modules.Variant_constructor_a.Rec_bundle_584097539.fst" = '''
-module Cyclic_modules.Variant_constructor_a.Rec_bundle_584097539
+"Cyclic_modules.Variant_constructor_a.Cyclic_bundle_748213522.fst" = '''
+module Cyclic_modules.Variant_constructor_a.Cyclic_bundle_748213522
 #set-options "--fuel 0 --ifuel 1 --z3rlimit 15"
 open Core
 open FStar.Mul
@@ -400,15 +400,15 @@ module Cyclic_modules.Variant_constructor_a
 open Core
 open FStar.Mul
 
-include Cyclic_modules.Variant_constructor_a.Rec_bundle_584097539 {t_Context as t_Context}
+include Cyclic_modules.Variant_constructor_a.Cyclic_bundle_748213522 {t_Context as t_Context}
 
-include Cyclic_modules.Variant_constructor_a.Rec_bundle_584097539 {Context_A as Context_A}
+include Cyclic_modules.Variant_constructor_a.Cyclic_bundle_748213522 {Context_A as Context_A}
 
-include Cyclic_modules.Variant_constructor_a.Rec_bundle_584097539 {Context_B as Context_B}
+include Cyclic_modules.Variant_constructor_a.Cyclic_bundle_748213522 {Context_B as Context_B}
 
-include Cyclic_modules.Variant_constructor_a.Rec_bundle_584097539 {test as impl__Context__test}
+include Cyclic_modules.Variant_constructor_a.Cyclic_bundle_748213522 {test as impl__Context__test}
 
-include Cyclic_modules.Variant_constructor_a.Rec_bundle_584097539 {f as f}
+include Cyclic_modules.Variant_constructor_a.Cyclic_bundle_748213522 {f as f}
 '''
 "Cyclic_modules.Variant_constructor_b.fst" = '''
 module Cyclic_modules.Variant_constructor_b
@@ -416,7 +416,7 @@ module Cyclic_modules.Variant_constructor_b
 open Core
 open FStar.Mul
 
-include Cyclic_modules.Variant_constructor_a.Rec_bundle_584097539 {h as h}
+include Cyclic_modules.Variant_constructor_a.Cyclic_bundle_748213522 {h as h}
 '''
 "Cyclic_modules.fst" = '''
 module Cyclic_modules
@@ -424,9 +424,9 @@ module Cyclic_modules
 open Core
 open FStar.Mul
 
-include Cyclic_modules.Rec_bundle_318256792 {f as f}
+include Cyclic_modules.Cyclic_bundle_367033742 {f as f}
 
-include Cyclic_modules.Rec_bundle_318256792 {h as h}
+include Cyclic_modules.Cyclic_bundle_367033742 {h as h}
 
-include Cyclic_modules.Rec_bundle_318256792 {h2 as h2}
+include Cyclic_modules.Cyclic_bundle_367033742 {h2 as h2}
 '''