Repository: cryspen/hax (language: rust)

Issue:
Spuritous dropped body in associated constants in inherent impls
We need a reproducer here.


Discussion / hints:
How easy would it be to generate interface and implementation on hax playground?
If you do so, I think even this should show the bug?
https://hax-playground.cryspen.com/#fstar/1c5e17c9ce/gist=242de2a27a905907b2cae4b67cb53399

Or is the bug only appearing in some interaction between the dependency analysis in the -i flag?
@W95Psp please add a comprehensive description.
This might be fixed by #1119

Fix patch:
diff --git a/engine/backends/fstar/fstar_backend.ml b/engine/backends/fstar/fstar_backend.ml
index 921f7f424..714760ff5 100644
--- a/engine/backends/fstar/fstar_backend.ml
+++ b/engine/backends/fstar/fstar_backend.ml
@@ -929,10 +929,11 @@ struct
           F.decl ~fsti:false
           @@ F.AST.TopLevelLet (qualifier, [ (pat, pexpr body) ])
         in
-        let interface_mode = ctx.interface_mode && not (List.is_empty params) in
+        let is_const = List.is_empty params in
         let ty =
-          add_clauses_effect_type ~no_tot_abbrev:interface_mode e.attrs
-            (pty body.span body.typ)
+          add_clauses_effect_type
+            ~no_tot_abbrev:(ctx.interface_mode && not is_const)
+            e.attrs (pty body.span body.typ)
         in
         let arrow_typ =
           F.term
@@ -968,7 +969,8 @@ struct
         let impl, full =
           if is_erased then (erased, erased) else ([ impl ], [ full ])
         in
-        if interface_mode then intf :: impl else full
+        if ctx.interface_mode && ((not is_const) || is_erased) then intf :: impl
+        else full
     | TyAlias { name; generics; ty } ->
         let pat =
           F.pat
diff --git a/engine/lib/import_thir.ml b/engine/lib/import_thir.ml
index 8011d5275..3df61d156 100644
--- a/engine/lib/import_thir.ml
+++ b/engine/lib/import_thir.ml
@@ -1659,9 +1659,14 @@ and c_item_unwrapped ~ident ~type_only (item : Thir.item) : item list =
           let item_def_id = Concrete_ident.of_def_id Impl item.owner_id in
           let attrs = c_item_attrs item.attributes in
           let sub_item_erased_by_user = erased_by_user attrs in
-          let sub_item_erased = sub_item_erased_by_user || type_only in
+          let erased_by_type_only =
+            type_only && match item.kind with Fn _ -> true | _ -> false
+          in
+          let sub_item_erased =
+            sub_item_erased_by_user || erased_by_type_only
+          in
           let attrs =
-            attrs_with_erased type_only sub_item_erased_by_user attrs
+            attrs_with_erased erased_by_type_only sub_item_erased_by_user attrs
           in
           let c_body = if sub_item_erased then c_expr_drop_body else c_body in
 


Test patch:
diff --git a/test-harness/src/snapshots/toolchain__attribute-opaque into-fstar.snap b/test-harness/src/snapshots/toolchain__attribute-opaque into-fstar.snap
index 6373c0b9e..d6c17d867 100644
--- a/test-harness/src/snapshots/toolchain__attribute-opaque into-fstar.snap
+++ b/test-harness/src/snapshots/toolchain__attribute-opaque into-fstar.snap
@@ -123,6 +123,8 @@ val impl_2 (#v_U: Type0) {| i1: Core.Clone.t_Clone v_U |} : t_TrGeneric i32 v_U
 
 val impl__S2__f_s2: Prims.unit -> Prims.Pure Prims.unit Prims.l_True (fun _ -> Prims.l_True)
 
+val v_C:u8
+
 val f (x y: bool) : Prims.Pure bool Prims.l_True (fun _ -> Prims.l_True)
 
 val ff_generic (v_X: usize) (#v_T #v_U: Type0) (x: v_U)