Repository: cryspen/hax (language: rust)

Issue:
Cyclic bundles: `Alias` are created for items with `late_skip`
Typically, `hax_lib` attributes expand to items that are tagged with `late_skip`: a precondition is a boolean-returning function tagged with `late_skip`.
In the cyclic bundle logic, we need to persist that late skip attribute in the `Alias` item if it was present at first in the original item.

```rust
pub mod a {
    pub fn f() {
        super::b::f()
    }
}
pub mod b {
    #[hax_lib::requires(true)]
    pub fn f() {
        super::a::f()
    }
}

```
[Open this code snippet in the playground](https://hax-playground.cryspen.com/#fstar/65dc6ab578/gist=d48f698a4ebc7b0bf9e59d1a9e7a3715)





Discussion / hints:

Fix patch:
diff --git a/engine/lib/dependencies.ml b/engine/lib/dependencies.ml
index a54e28eeb..eb8819ac8 100644
--- a/engine/lib/dependencies.ml
+++ b/engine/lib/dependencies.ml
@@ -383,11 +383,11 @@ module Make (F : Features.T) = struct
     let aliases =
       List.map (old_new :: variants_renamings old_new)
         ~f:(fun (old_ident, new_ident) ->
-          {
-            item with
-            v = Alias { name = old_ident; item = new_ident };
-            attrs = [];
-          })
+          let attrs =
+            List.filter ~f:(fun att -> Attrs.late_skip [ att ]) item.attrs
+          in
+
+          { item with v = Alias { name = old_ident; item = new_ident }; attrs })
     in
     item' :: aliases
 


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 3edbdc730..af07fc045 100644
--- a/test-harness/src/snapshots/toolchain__cyclic-modules into-fstar.snap
+++ b/test-harness/src/snapshots/toolchain__cyclic-modules into-fstar.snap
@@ -180,6 +180,33 @@ include Cyclic_modules.Enums_b.Rec_bundle_994866580 {U_C as U_C}
 
 include Cyclic_modules.Enums_b.Rec_bundle_994866580 {f as f}
 '''
+"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
+
+include Cyclic_modules.Late_skip_b.Rec_bundle_447022631 {f749016415 as f}
+'''
+"Cyclic_modules.Late_skip_b.Rec_bundle_447022631.fst" = '''
+module Cyclic_modules.Late_skip_b.Rec_bundle_447022631
+#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 ()
+'''
+"Cyclic_modules.Late_skip_b.fst" = '''
+module Cyclic_modules.Late_skip_b
+#set-options "--fuel 0 --ifuel 1 --z3rlimit 15"
+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"
diff --git a/tests/Cargo.lock b/tests/Cargo.lock
index 09cd8e14b..3fd42cefa 100644
--- a/tests/Cargo.lock
+++ b/tests/Cargo.lock
@@ -224,6 +224,9 @@ dependencies = [
 [[package]]
 name = "cyclic-modules"
 version = "0.1.0"
+dependencies = [
+ "hax-lib",
+]
 
 [[package]]
 name = "dyn"
diff --git a/tests/cyclic-modules/Cargo.toml b/tests/cyclic-modules/Cargo.toml
index 092cfd078..480511746 100644
--- a/tests/cyclic-modules/Cargo.toml
+++ b/tests/cyclic-modules/Cargo.toml
@@ -4,6 +4,7 @@ version = "0.1.0"
 edition = "2021"
 
 [dependencies]
+hax-lib = { path = "../../hax-lib" }
 
 [package.metadata.hax-tests]
 into."fstar" = { broken = false, snapshot = "stdout", issue_id = "396" }
diff --git a/tests/cyclic-modules/src/lib.rs b/tests/cyclic-modules/src/lib.rs
index b59be2d80..216a54812 100644
--- a/tests/cyclic-modules/src/lib.rs
+++ b/tests/cyclic-modules/src/lib.rs
@@ -166,3 +166,15 @@ pub mod variant_constructor_b {
         super::variant_constructor_a::Context::A(1)
     }
 }
+
+pub mod late_skip_a {
+    pub fn f() {
+        super::late_skip_b::f()
+    }
+}
+pub mod late_skip_b {
+    #[hax_lib::requires(true)]
+    pub fn f() {
+        super::late_skip_a::f()
+    }
+}