Repository: cryspen/hax (language: rust)

Issue:
Import of name from bundle that doesn't exist
This is a regression form #1199, here is a reproducer:
```rust
mod a {
    pub fn g(){super::b::h()}
    
    struct A();

    impl A {
        fn f() {
            struct Test(i32);
        }
    }
}
mod b {
    pub fn h(){super::a::g()}
}
```
[Open this code snippet in the playground](https://hax-playground.cryspen.com/#fstar/83818105f1/gist=53c1d590a0b913f65dd352bada6f66a6)

F* laxing fails with: `Definition Playground.Bundle.impl__f___0 cannot be found`.
This is because of `include Playground.Bundle {impl__f___0 as impl_A__f___0}`
Here we have an alias for the `._0` accessor for the anonymous field in `Test` but `Test` is defined inside an impl methods which messes with the name.


Discussion / hints:
I think one way to solve that would be to completely remove aliases for `_<n>` accessors of tuple structs. It seems that this is ok and in a case like:
```rust
mod a {
    pub fn g(){super::b::h()}
    
    pub struct A(pub i32);

}
mod b {
    pub fn h(){super::a::g()}
}

fn f(x: a::A) -> i32 {
    x.0
}
```
[Open this code snippet in the playground](https://hax-playground.cryspen.com/#fstar/83818105f1/gist=6d446cc27037586e8b607459c01fe95f)

Lax-checking still works without the `include Playground.Bundle {_0 as _0}` in `Playground.A.fst`.

@W95Psp Do you think this would be ok? And how can we identify a name that corresponds to one of these accessors?
Other thing we should probably not produce aliases for: traits. Example:

```rust
mod encoder {
    trait Encode {
        fn encode();
    }

    pub fn foo(){
        super::user::something();
    }
}

mod user {
    pub fn something() {
        super::encoder::foo();
    }
}

```
[Open this code snippet in the playground](https://hax-playground.cryspen.com/#fstar+tc/83818105f1/gist=8da5a3c639073940c66c096d7d457ec2)
Here we have `include Playground.Bundle {t_Encode as t_Encode}` which gives this laxing error: `Definition Playground.Bundle.__proj__Mkt_Encode__item__v_Self cannot be found`
I think that indeed not producing aliases for field names makes sense.
In `dependencies.ml` we can add another condition to the filter when we build up the `aliases` list, to know if a concrete ident points to a field, you can project its view (with https://hax.cryspen.com/engine/docs/hax-engine/Hax_engine/Concrete_ident/index.html#val-to_view), and then inspect the last segment of the relpath of the view.

However, for the traits, I think that's a problem in F*: currently, `include ... {some_trait}` detects that `some_trait` is a type definition and thus automatically includes all possible related names.
For now, we can filter them out, but we should file an issue on hax to fix it, and probably on F* as well (if we have a simple reproducer).

Fix patch:
diff --git a/engine/lib/dependencies.ml b/engine/lib/dependencies.ml
index b743b4dc6..91aa2da1a 100644
--- a/engine/lib/dependencies.ml
+++ b/engine/lib/dependencies.ml
@@ -513,6 +513,9 @@ module Make (F : Features.T) = struct
                (idents_of item))
     in
     let aliases =
+      let inspect_view_last id =
+        List.last (Concrete_ident.to_view id).rel_path
+      in
       List.filter_map renamings ~f:(fun (origin_item, (from_id, to_id)) ->
           let attrs =
             List.filter
@@ -527,7 +530,18 @@ module Make (F : Features.T) = struct
             when List.for_all variants ~f:(fun variant -> variant.is_record)
                  && Concrete_ident.is_constructor from_id ->
               None
+          (* We don't need aliases for fields of types. *)
+          | Type _ when [%matches? Some (`Field _)] (inspect_view_last from_id)
+            ->
+              None
+          (* We don't need aliases for methods of trait impls. *)
+          | Impl _
+            when [%matches? Some (`AssociatedItem _)]
+                   (inspect_view_last from_id) ->
+              None
           | Quote _ -> None
+          (* This is temporary: see https://github.com/cryspen/hax/issues/1285 *)
+          | Trait { name; _ } when [%equal: concrete_ident] name from_id -> None
           | _ -> Some { attrs; span = origin_item.span; ident = from_id; v })
     in
     let rename =
diff --git a/proof-libs/fstar/core/Core.Core_arch.X86.Pclmulqdq.fsti b/proof-libs/fstar/core/Core.Core_arch.X86.Pclmulqdq.fsti
index b249cb49a..ddb9222be 100644
--- a/proof-libs/fstar/core/Core.Core_arch.X86.Pclmulqdq.fsti
+++ b/proof-libs/fstar/core/Core.Core_arch.X86.Pclmulqdq.fsti
@@ -1,3 +1,3 @@
 module Core.Core_arch.X86.Pclmulqdq
 
-val v__mm_clmulepi64_si128 : Rust_primitives.Integers.i32 -> Core.Core_arch.X86.t____m128i -> Core.Core_arch.X86.t____m128i -> Core.Core_arch.X86.t____m128i
+val e_mm_clmulepi64_si128 : Rust_primitives.Integers.i32 -> Core.Core_arch.X86.t_e_ee_m128i -> Core.Core_arch.X86.t_e_ee_m128i -> Core.Core_arch.X86.t_e_ee_m128i
diff --git a/proof-libs/fstar/core/Core.Core_arch.X86.Sse2.fsti b/proof-libs/fstar/core/Core.Core_arch.X86.Sse2.fsti
index 9e2419879..549a82f82 100644
--- a/proof-libs/fstar/core/Core.Core_arch.X86.Sse2.fsti
+++ b/proof-libs/fstar/core/Core.Core_arch.X86.Sse2.fsti
@@ -1,3 +1,3 @@
 module Core.Core_arch.X86.Sse2
 
-val v__mm_set_epi64x: Rust_primitives.Integers.i64 -> Rust_primitives.Integers.i64 -> Core.Core_arch.X86.t____m128i
+val e_mm_set_epi64x: Rust_primitives.Integers.i64 -> Rust_primitives.Integers.i64 -> Core.Core_arch.X86.t_e_ee_m128i
diff --git a/proof-libs/fstar/core/Core.Core_arch.X86.fsti b/proof-libs/fstar/core/Core.Core_arch.X86.fsti
index 5056e0e34..2305bd249 100644
--- a/proof-libs/fstar/core/Core.Core_arch.X86.fsti
+++ b/proof-libs/fstar/core/Core.Core_arch.X86.fsti
@@ -1,5 +1,5 @@
 module Core.Core_arch.X86
 
-val t____m128i:Type0
+val t_e_ee_m128i:Type0
 
-val t____m256i:Type0
+val t_e_ee_m256i:Type0
diff --git a/proof-libs/fstar/core/Core.Core_arch.X86_64_.Sse2.fsti b/proof-libs/fstar/core/Core.Core_arch.X86_64_.Sse2.fsti
index 48fbe8e42..a04253e2c 100644
--- a/proof-libs/fstar/core/Core.Core_arch.X86_64_.Sse2.fsti
+++ b/proof-libs/fstar/core/Core.Core_arch.X86_64_.Sse2.fsti
@@ -1,3 +1,3 @@
 module Core.Core_arch.X86_64_.Sse2
 
-val v__mm_cvtsi128_si64: Core.Core_arch.X86.t____m128i -> Rust_primitives.Integers.i64
+val e_mm_cvtsi128_si64: Core.Core_arch.X86.t_e_ee_m128i -> Rust_primitives.Integers.i64


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 d0f4a2af0..eed36bb37 100644
--- a/test-harness/src/snapshots/toolchain__cyclic-modules into-fstar.snap
+++ b/test-harness/src/snapshots/toolchain__cyclic-modules into-fstar.snap
@@ -247,11 +247,7 @@ include Cyclic_modules.Bundle_enums_a {T_B__from__enums_a as T_B}
 
 include Cyclic_modules.Bundle_enums_a {T_C__from__enums_a as T_C}
 
-include Cyclic_modules.Bundle_enums_a {_0 as _0}
-
 include Cyclic_modules.Bundle_enums_a {T_D as T_D}
-
-include Cyclic_modules.Bundle_enums_a {_0 as _0}
 '''
 "Cyclic_modules.Enums_b.fst" = '''
 module Cyclic_modules.Enums_b
@@ -267,8 +263,6 @@ include Cyclic_modules.Bundle_enums_a {U_B as U_B}
 
 include Cyclic_modules.Bundle_enums_a {U_C as U_C}
 
-include Cyclic_modules.Bundle_enums_a {_0 as _0}
-
 include Cyclic_modules.Bundle_enums_a {t_T__from__enums_b as t_T}
 
 include Cyclic_modules.Bundle_enums_a {T_A as T_A}
@@ -277,8 +271,6 @@ include Cyclic_modules.Bundle_enums_a {T_B as T_B}
 
 include Cyclic_modules.Bundle_enums_a {T_C as T_C}
 
-include Cyclic_modules.Bundle_enums_a {_0 as _0}
-
 include Cyclic_modules.Bundle_enums_a {f as f}
 '''
 "Cyclic_modules.Late_skip_a.fst" = '''
@@ -373,15 +365,11 @@ include Cyclic_modules.Bundle_typ_a {t_TRec as t_TRec}
 
 include Cyclic_modules.Bundle_typ_a {TRec_T as TRec_T}
 
-include Cyclic_modules.Bundle_typ_a {_0 as _0}
-
 include Cyclic_modules.Bundle_typ_a {TRec_Empty as TRec_Empty}
 
 include Cyclic_modules.Bundle_typ_a {t_T as t_T}
 
 include Cyclic_modules.Bundle_typ_a {T_T as T_T}
-
-include Cyclic_modules.Bundle_typ_a {_0 as _0}
 '''
 "Cyclic_modules.Typ_b.fst" = '''
 module Cyclic_modules.Typ_b
@@ -393,14 +381,10 @@ include Cyclic_modules.Bundle_typ_a {t_T1Rec as t_T1Rec}
 
 include Cyclic_modules.Bundle_typ_a {T1Rec_T1 as T1Rec_T1}
 
-include Cyclic_modules.Bundle_typ_a {_0 as _0}
-
 include Cyclic_modules.Bundle_typ_a {t_T2Rec as t_T2Rec}
 
 include Cyclic_modules.Bundle_typ_a {T2Rec_T2 as T2Rec_T2}
 
-include Cyclic_modules.Bundle_typ_a {_0 as _0}
-
 include Cyclic_modules.Bundle_typ_a {t_T1_cast_to_repr as t_T1_cast_to_repr}
 
 include Cyclic_modules.Bundle_typ_a {t_T1 as t_T1}
@@ -410,8 +394,6 @@ include Cyclic_modules.Bundle_typ_a {T1_T1 as T1_T1}
 include Cyclic_modules.Bundle_typ_a {t_T2 as t_T2}
 
 include Cyclic_modules.Bundle_typ_a {T2_T2 as T2_T2}
-
-include Cyclic_modules.Bundle_typ_a {_0 as _0}
 '''
 "Cyclic_modules.Variant_constructor_a.fst" = '''
 module Cyclic_modules.Variant_constructor_a
@@ -423,12 +405,8 @@ include Cyclic_modules.Bundle_variant_constructor_a {t_Context as t_Context}
 
 include Cyclic_modules.Bundle_variant_constructor_a {Context_A as Context_A}
 
-include Cyclic_modules.Bundle_variant_constructor_a {_0 as _0}
-
 include Cyclic_modules.Bundle_variant_constructor_a {Context_B as Context_B}
 
-include Cyclic_modules.Bundle_variant_constructor_a {_0 as _0}
-
 include Cyclic_modules.Bundle_variant_constructor_a {f as f}
 
 include Cyclic_modules.Bundle_variant_constructor_a {impl__test as impl_Context__test}