From 9a633b23ca22bfb27179a6c0656865e97afafda4 Mon Sep 17 00:00:00 2001 From: Maxime Buyse Date: Mon, 3 Feb 2025 16:02:23 +0100 Subject: [PATCH 1/6] Remove aliases for struct fields. --- engine/lib/dependencies.ml | 7 ++++++- 1 file changed, 6 insertions(+), 1 deletion(-) diff --git a/engine/lib/dependencies.ml b/engine/lib/dependencies.ml index b743b4dc6..8009f4bdb 100644 --- a/engine/lib/dependencies.ml +++ b/engine/lib/dependencies.ml @@ -523,9 +523,14 @@ module Make (F : Features.T) = struct match origin_item.v with (* We don't want to aliases for constructors of structs with named fields because they can't be imported in F*. Ideally this should be handled by the backend. *) + (* We don't need aliases for fields of structs. *) | Type { variants; is_struct = true; _ } when List.for_all variants ~f:(fun variant -> variant.is_record) - && Concrete_ident.is_constructor from_id -> + && Concrete_ident.is_constructor from_id + || + match List.last (Concrete_ident.to_view from_id).rel_path with + | Some (`Field _) -> true + | _ -> false -> None | Quote _ -> None | _ -> Some { attrs; span = origin_item.span; ident = from_id; v }) From bacca2ef66d7dfdb209b79811cec0abf224606e8 Mon Sep 17 00:00:00 2001 From: Maxime Buyse Date: Mon, 3 Feb 2025 16:58:21 +0100 Subject: [PATCH 2/6] Adapt some core lib names to nbew naming. --- proof-libs/fstar/core/Core.Core_arch.X86.Pclmulqdq.fsti | 2 +- proof-libs/fstar/core/Core.Core_arch.X86.Sse2.fsti | 2 +- proof-libs/fstar/core/Core.Core_arch.X86.fsti | 4 ++-- proof-libs/fstar/core/Core.Core_arch.X86_64_.Sse2.fsti | 2 +- 4 files changed, 5 insertions(+), 5 deletions(-) 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 From 72c8a921151d6ef78806d7650bbe85069fd10715 Mon Sep 17 00:00:00 2001 From: Maxime Buyse Date: Mon, 3 Feb 2025 17:21:40 +0100 Subject: [PATCH 3/6] Filter out more problematic aliases. --- engine/lib/dependencies.ml | 20 +++++++++++++++----- 1 file changed, 15 insertions(+), 5 deletions(-) diff --git a/engine/lib/dependencies.ml b/engine/lib/dependencies.ml index 8009f4bdb..0d142b358 100644 --- a/engine/lib/dependencies.ml +++ b/engine/lib/dependencies.ml @@ -523,16 +523,26 @@ module Make (F : Features.T) = struct match origin_item.v with (* We don't want to aliases for constructors of structs with named fields because they can't be imported in F*. Ideally this should be handled by the backend. *) - (* We don't need aliases for fields of structs. *) | Type { variants; is_struct = true; _ } when List.for_all variants ~f:(fun variant -> variant.is_record) - && Concrete_ident.is_constructor from_id - || - match List.last (Concrete_ident.to_view from_id).rel_path with + && Concrete_ident.is_constructor from_id -> + None + (* We don't need aliases for fields of types. *) + | Type _ + when match List.last (Concrete_ident.to_view from_id).rel_path with | Some (`Field _) -> true | _ -> false -> None - | Quote _ -> None + (* We don't need aliases for methods of trait impls. *) + | Impl _ + when match List.last (Concrete_ident.to_view from_id).rel_path with + | Some (`AssociatedItem _) -> true + | _ -> false -> + None + | Quote _ + (* This is temporary: see https://github.com/cryspen/hax/issues/1285 *) + | Trait _ -> + None | _ -> Some { attrs; span = origin_item.span; ident = from_id; v }) in let rename = From 0f1fc516ad9d444aecfe9d6373435d784772a0d3 Mon Sep 17 00:00:00 2001 From: Maxime Buyse Date: Mon, 3 Feb 2025 17:37:55 +0100 Subject: [PATCH 4/6] Test snapshot with no field include from bundle. --- .../toolchain__cyclic-modules into-fstar.snap | 22 ------------------- 1 file changed, 22 deletions(-) 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} From fe4e1e04a147168122580e7c69dfd7010cfa8211 Mon Sep 17 00:00:00 2001 From: Maxime Buyse Date: Tue, 4 Feb 2025 15:25:48 +0100 Subject: [PATCH 5/6] Keep aliases for trait methods. --- engine/lib/dependencies.ml | 5 ++--- 1 file changed, 2 insertions(+), 3 deletions(-) diff --git a/engine/lib/dependencies.ml b/engine/lib/dependencies.ml index 0d142b358..51eb7f51f 100644 --- a/engine/lib/dependencies.ml +++ b/engine/lib/dependencies.ml @@ -539,10 +539,9 @@ module Make (F : Features.T) = struct | Some (`AssociatedItem _) -> true | _ -> false -> None - | Quote _ + | Quote _ -> None (* This is temporary: see https://github.com/cryspen/hax/issues/1285 *) - | Trait _ -> - None + | Trait { name; _ } when [%equal: concrete_ident] name from_id -> None | _ -> Some { attrs; span = origin_item.span; ident = from_id; v }) in let rename = From 1a045fbf991308e2ee180aca928c22a0f02ed1f9 Mon Sep 17 00:00:00 2001 From: Maxime Buyse Date: Wed, 5 Feb 2025 10:34:55 +0100 Subject: [PATCH 6/6] Use %matches instead of pattern matching. --- engine/lib/dependencies.ml | 14 +++++++------- 1 file changed, 7 insertions(+), 7 deletions(-) diff --git a/engine/lib/dependencies.ml b/engine/lib/dependencies.ml index 51eb7f51f..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 @@ -528,16 +531,13 @@ module Make (F : Features.T) = struct && Concrete_ident.is_constructor from_id -> None (* We don't need aliases for fields of types. *) - | Type _ - when match List.last (Concrete_ident.to_view from_id).rel_path with - | Some (`Field _) -> true - | _ -> false -> + | Type _ when [%matches? Some (`Field _)] (inspect_view_last from_id) + -> None (* We don't need aliases for methods of trait impls. *) | Impl _ - when match List.last (Concrete_ident.to_view from_id).rel_path with - | Some (`AssociatedItem _) -> true - | _ -> false -> + when [%matches? Some (`AssociatedItem _)] + (inspect_view_last from_id) -> None | Quote _ -> None (* This is temporary: see https://github.com/cryspen/hax/issues/1285 *)