From 9625d1a1c41ce6a1248c6d777b4811e77c4ac2c5 Mon Sep 17 00:00:00 2001
From: Nadrieril <nadrieril+git@gmail.com>
Date: Tue, 1 Jul 2025 13:10:07 +0200
Subject: [PATCH 01/18] Update rustc

---
 cli/driver/src/driver.rs                      |  1 -
 engine/lib/import_thir.ml                     | 18 +++++-----
 flake.lock                                    |  6 ++--
 .../exporter/src/constant_utils/uneval.rs     |  4 +--
 frontend/exporter/src/lib.rs                  |  2 +-
 frontend/exporter/src/sinto.rs                |  6 ++++
 frontend/exporter/src/traits/resolution.rs    |  4 +--
 frontend/exporter/src/types/hir.rs            | 16 ++++-----
 frontend/exporter/src/types/new/full_def.rs   |  5 +--
 frontend/exporter/src/types/ty.rs             |  6 ++--
 rust-toolchain.toml                           |  2 +-
 ...oolchain__attribute-opaque into-fstar.snap |  2 ++
 .../toolchain__attributes into-fstar.snap     |  6 ++++
 .../snapshots/toolchain__dyn into-fstar.snap  | 34 +++++++++---------
 .../toolchain__functions into-fstar.snap      |  1 +
 .../toolchain__generics into-fstar.snap       |  1 +
 .../toolchain__include-flag into-coq.snap     |  4 +--
 .../toolchain__include-flag into-fstar.snap   |  4 ++-
 .../toolchain__interface-only into-fstar.snap |  2 ++
 .../toolchain__literals into-coq.snap         |  5 ++-
 .../toolchain__literals into-fstar.snap       |  2 +-
 ..._mut-ref-functionalization into-fstar.snap |  1 +
 .../toolchain__naming into-fstar.snap         | 36 ++++++++++++-------
 .../toolchain__side-effects into-fstar.snap   |  1 +
 .../toolchain__traits into-fstar.snap         | 36 ++++++++++++++++---
 25 files changed, 133 insertions(+), 72 deletions(-)

diff --git a/cli/driver/src/driver.rs b/cli/driver/src/driver.rs
index a7f1d4e2c..2ec019b8f 100644
--- a/cli/driver/src/driver.rs
+++ b/cli/driver/src/driver.rs
@@ -1,6 +1,5 @@
 #![feature(rustc_private)]
 #![feature(box_patterns)]
-#![feature(concat_idents)]
 #![feature(trait_alias)]
 #![allow(unused_imports)]
 #![allow(unused_variables)]
diff --git a/engine/lib/import_thir.ml b/engine/lib/import_thir.ml
index 821b30d8f..fb2277eef 100644
--- a/engine/lib/import_thir.ml
+++ b/engine/lib/import_thir.ml
@@ -1516,7 +1516,7 @@ and c_item_unwrapped ~ident ~type_only (item : Thir.item) : item list =
   in
   (* TODO: things might be unnamed (e.g. constants) *)
   match (item.kind : Thir.item_kind) with
-  | Const (_, _, generics, body) ->
+  | Const (_, generics, _, body) ->
       mk
       @@ Fn
            {
@@ -1526,14 +1526,14 @@ and c_item_unwrapped ~ident ~type_only (item : Thir.item) : item list =
              params = [];
              safety = Safe;
            }
-  | Static (_, _, true, _) ->
+  | Static (true, _, _, _) ->
       unimplemented ~issue_id:1343 [ item.span ]
         "Mutable static items are not supported."
-  | Static (_, _ty, false, body) ->
+  | Static (false, _, _ty, body) ->
       let name = Concrete_ident.of_def_id ~value:true (assert_item_def_id ()) in
       let generics = { params = []; constraints = [] } in
       mk (Fn { name; generics; body = c_body body; params = []; safety = Safe })
-  | TyAlias (_, ty, generics) ->
+  | TyAlias (_, generics, ty) ->
       mk
       @@ TyAlias
            {
@@ -1552,13 +1552,13 @@ and c_item_unwrapped ~ident ~type_only (item : Thir.item) : item list =
              params = c_fn_params item.span params;
              safety = c_header_safety safety;
            }
-  | (Enum (_, _, generics, _) | Struct (_, _, generics)) when erased ->
+  | (Enum (_, generics, _, _) | Struct (_, generics, _)) when erased ->
       let generics = c_generics generics in
       let is_struct = match item.kind with Struct _ -> true | _ -> false in
       let def_id = assert_item_def_id () in
       let name = Concrete_ident.of_def_id ~value:false def_id in
       mk @@ Type { name; generics; variants = []; is_struct }
-  | Enum (_, variants, generics, repr) ->
+  | Enum (_, generics, variants, repr) ->
       let def_id = assert_item_def_id () in
       let generics = c_generics generics in
       let is_struct = false in
@@ -1616,7 +1616,7 @@ and c_item_unwrapped ~ident ~type_only (item : Thir.item) : item list =
         mk_one (Type { name; generics; variants; is_struct }) :: discs
       in
       if is_primitive then cast_fun :: result else result
-  | Struct (_, v, generics) ->
+  | Struct (_, generics, v) ->
       let generics = c_generics generics in
       let def_id = assert_item_def_id () in
       let is_struct = true in
@@ -1814,7 +1814,9 @@ and c_item_unwrapped ~ident ~type_only (item : Thir.item) : item list =
           {
             path = List.map ~f:(fun x -> fst x.ident) segments;
             is_external =
-              List.exists ~f:(function Err -> true | _ -> false) res;
+              List.exists
+                ~f:(function None | Some Err -> true | _ -> false)
+                res;
             (* TODO: this should represent local/external? *)
             rename;
           }
diff --git a/flake.lock b/flake.lock
index 539def0d4..9ce04a43b 100644
--- a/flake.lock
+++ b/flake.lock
@@ -150,11 +150,11 @@
         ]
       },
       "locked": {
-        "lastModified": 1752720268,
-        "narHash": "sha256-XCiJdtXIN09Iv0i1gs5ajJ9CVHk537Gy1iG/4nIdpVI=",
+        "lastModified": 1753066249,
+        "narHash": "sha256-j2UBrfDRIePGx3532Bbb9UeosNX2F73hfOAHtmACfnM=",
         "owner": "oxalica",
         "repo": "rust-overlay",
-        "rev": "dc221f842e9ddc8c0416beae8d77f2ea356b91ae",
+        "rev": "0751b65633a1785743ca44fd7c14a633c54c1f91",
         "type": "github"
       },
       "original": {
diff --git a/frontend/exporter/src/constant_utils/uneval.rs b/frontend/exporter/src/constant_utils/uneval.rs
index 33d18f07d..8f41b2392 100644
--- a/frontend/exporter/src/constant_utils/uneval.rs
+++ b/frontend/exporter/src/constant_utils/uneval.rs
@@ -154,7 +154,7 @@ impl<'tcx, S: UnderOwnerState<'tcx>> SInto<S, ConstantExpr> for ty::Const<'tcx>
         let span = self.default_span(s.base().tcx);
         match self.kind() {
             ty::ConstKind::Param(p) => {
-                let ty = p.find_ty_from_env(s.param_env());
+                let ty = p.find_const_ty_from_env(s.param_env());
                 let kind = ConstantExprKind::ConstRef { id: p.sinto(s) };
                 kind.decorate(ty.sinto(s), span.sinto(s))
             }
@@ -279,7 +279,7 @@ fn op_to_const<'tcx, S: UnderOwnerState<'tcx>>(
     // Helper for struct-likes.
     let read_fields = |of: rustc_const_eval::interpret::OpTy<'tcx>, field_count| {
         (0..field_count).map(move |i| {
-            let field_op = ecx.project_field(&of, i)?;
+            let field_op = ecx.project_field(&of, rustc_abi::FieldIdx::from_usize(i))?;
             op_to_const(s, span, &ecx, field_op)
         })
     };
diff --git a/frontend/exporter/src/lib.rs b/frontend/exporter/src/lib.rs
index fe3b58896..a4c851910 100644
--- a/frontend/exporter/src/lib.rs
+++ b/frontend/exporter/src/lib.rs
@@ -1,9 +1,9 @@
 #![allow(rustdoc::private_intra_doc_links)]
-#![cfg_attr(feature = "rustc", feature(concat_idents))]
 #![cfg_attr(feature = "rustc", feature(if_let_guard))]
 #![cfg_attr(feature = "rustc", feature(let_chains))]
 #![cfg_attr(feature = "rustc", feature(macro_metavar_expr))]
 #![cfg_attr(feature = "rustc", feature(rustc_private))]
+#![cfg_attr(feature = "rustc", feature(sized_hierarchy))]
 #![cfg_attr(feature = "rustc", feature(trait_alias))]
 #![cfg_attr(feature = "rustc", feature(type_changing_struct_update))]
 
diff --git a/frontend/exporter/src/sinto.rs b/frontend/exporter/src/sinto.rs
index fc58f735f..15d65f66b 100644
--- a/frontend/exporter/src/sinto.rs
+++ b/frontend/exporter/src/sinto.rs
@@ -1,9 +1,15 @@
 use crate::prelude::{derive_group, JsonSchema};
 
+#[cfg(not(feature = "rustc"))]
 pub trait SInto<S, To> {
     fn sinto(&self, s: &S) -> To;
 }
 
+#[cfg(feature = "rustc")]
+pub trait SInto<S, To>: std::marker::PointeeSized {
+    fn sinto(&self, s: &S) -> To;
+}
+
 #[macro_export]
 macro_rules! sinto_todo {
     ($($mod:ident)::+, $type:ident$(<$($lts:lifetime),*$(,)?>)? as $renamed:ident) => {
diff --git a/frontend/exporter/src/traits/resolution.rs b/frontend/exporter/src/traits/resolution.rs
index 453a811ae..2b72db07d 100644
--- a/frontend/exporter/src/traits/resolution.rs
+++ b/frontend/exporter/src/traits/resolution.rs
@@ -677,7 +677,7 @@ pub fn shallow_resolve_trait_ref<'tcx>(
     use rustc_middle::traits::CodegenObligationError;
     use rustc_middle::ty::TypeVisitableExt;
     use rustc_trait_selection::traits::{
-        Obligation, ObligationCause, ObligationCtxt, SelectionContext, Unimplemented,
+        Obligation, ObligationCause, ObligationCtxt, SelectionContext, SelectionError,
     };
     // Do the initial selection for the obligation. This yields the
     // shallow result we are looking for -- that is, what specific impl.
@@ -693,7 +693,7 @@ pub fn shallow_resolve_trait_ref<'tcx>(
     let selection = match selcx.poly_select(&obligation) {
         Ok(Some(selection)) => selection,
         Ok(None) => return Err(CodegenObligationError::Ambiguity),
-        Err(Unimplemented) => return Err(CodegenObligationError::Unimplemented),
+        Err(SelectionError::Unimplemented) => return Err(CodegenObligationError::Unimplemented),
         Err(_) => return Err(CodegenObligationError::Ambiguity),
     };
 
diff --git a/frontend/exporter/src/types/hir.rs b/frontend/exporter/src/types/hir.rs
index e4b5a747b..2a80a7837 100644
--- a/frontend/exporter/src/types/hir.rs
+++ b/frontend/exporter/src/types/hir.rs
@@ -535,7 +535,7 @@ pub struct Variant<Body: IsBody> {
 pub struct UsePath {
     pub span: Span,
     #[map(x.iter().map(|res| res.sinto(s)).collect())]
-    pub res: Vec<Res>,
+    pub res: Vec<Option<Res>>,
     pub segments: Vec<PathSegment>,
     #[value(self.segments.iter().last().and_then(|segment| {
             match s.base().tcx.hir_node_by_def_id(segment.hir_id.owner.def_id) {
@@ -620,8 +620,8 @@ pub struct PathSegment {
 pub enum ItemKind<Body: IsBody> {
     ExternCrate(Option<Symbol>, Ident),
     Use(UsePath, UseKind),
-    Static(Ident, Ty, Mutability, Body),
-    Const(Ident, Ty, Generics<Body>, Body),
+    Static(Mutability, Ident, Ty, Body),
+    Const(Ident, Generics<Body>, Ty, Body),
     #[custom_arm(
         hir::ItemKind::Fn{ ident, sig, generics, body, .. } => {
             ItemKind::Fn {
@@ -648,6 +648,7 @@ pub enum ItemKind<Body: IsBody> {
     },
     TyAlias(
         Ident,
+        Generics<Body>,
         #[map({
             let s = &State {
                 base: Base {ty_alias_mode: true, ..s.base()},
@@ -659,20 +660,19 @@ pub enum ItemKind<Body: IsBody> {
             x.sinto(s)
         })]
         Ty,
-        Generics<Body>,
     ),
     Enum(
         Ident,
-        EnumDef<Body>,
         Generics<Body>,
+        EnumDef<Body>,
         #[value({
             let tcx = s.base().tcx;
             tcx.repr_options_of_def(s.owner_id().expect_local()).sinto(s)
         })]
         ReprOptions,
     ),
-    Struct(Ident, VariantData, Generics<Body>),
-    Union(Ident, VariantData, Generics<Body>),
+    Struct(Ident, Generics<Body>, VariantData),
+    Union(Ident, Generics<Body>, VariantData),
     Trait(
         IsAuto,
         Safety,
@@ -916,7 +916,7 @@ impl<'tcx, S: BaseState<'tcx>, Body: IsBody> SInto<S, Item<Body>> for hir::Item<
         let name = match self.kind {
             ExternCrate(_, i)
             | Use(_, hir::UseKind::Single(i))
-            | Static(i, ..)
+            | Static(_, i, ..)
             | Const(i, ..)
             | Fn { ident: i, .. }
             | Macro(i, ..)
diff --git a/frontend/exporter/src/types/new/full_def.rs b/frontend/exporter/src/types/new/full_def.rs
index 951150d21..91a3e49a9 100644
--- a/frontend/exporter/src/types/new/full_def.rs
+++ b/frontend/exporter/src/types/new/full_def.rs
@@ -217,7 +217,7 @@ pub enum FullDefKind<Body> {
         /// `Some` if the item is in the local crate.
         #[value(s.base().tcx.hir_get_if_local(s.owner_id()).map(|node| {
             let rustc_hir::Node::Item(item) = node else { unreachable!() };
-            let rustc_hir::ItemKind::TyAlias(_, ty, _generics) = &item.kind else { unreachable!() };
+            let rustc_hir::ItemKind::TyAlias(_, _generics, ty) = &item.kind else { unreachable!() };
             let mut s = State::from_under_owner(s);
             s.base.ty_alias_mode = true;
             ty.sinto(&s)
@@ -981,7 +981,8 @@ fn closure_once_shim<'tcx>(
 
 #[cfg(feature = "rustc")]
 fn drop_glue_shim<'tcx>(tcx: ty::TyCtxt<'tcx>, def_id: RDefId) -> Option<mir::Body<'tcx>> {
-    let drop_in_place = tcx.require_lang_item(rustc_hir::LangItem::DropInPlace, None);
+    let drop_in_place =
+        tcx.require_lang_item(rustc_hir::LangItem::DropInPlace, rustc_span::DUMMY_SP);
     if !tcx.generics_of(def_id).is_empty() {
         // Hack: layout code panics if it can't fully normalize types, which can happen e.g. with a
         // trait associated type. For now we only translate the glue for monomorphic types.
diff --git a/frontend/exporter/src/types/ty.rs b/frontend/exporter/src/types/ty.rs
index 0438ab5ee..49c9f2651 100644
--- a/frontend/exporter/src/types/ty.rs
+++ b/frontend/exporter/src/types/ty.rs
@@ -544,14 +544,14 @@ impl std::ops::Deref for ItemRef {
 #[cfg(feature = "rustc")]
 impl<'tcx, S: UnderOwnerState<'tcx>> SInto<S, GenericArg> for ty::GenericArg<'tcx> {
     fn sinto(&self, s: &S) -> GenericArg {
-        self.unpack().sinto(s)
+        self.kind().sinto(s)
     }
 }
 
 #[cfg(feature = "rustc")]
 impl<'tcx, S: UnderOwnerState<'tcx>> SInto<S, Vec<GenericArg>> for ty::GenericArgsRef<'tcx> {
     fn sinto(&self, s: &S) -> Vec<GenericArg> {
-        self.iter().map(|v| v.unpack().sinto(s)).collect()
+        self.iter().map(|v| v.kind().sinto(s)).collect()
     }
 }
 
@@ -1169,7 +1169,7 @@ pub enum Term {
 impl<'tcx, S: UnderOwnerState<'tcx>> SInto<S, Term> for ty::Term<'tcx> {
     fn sinto(&self, s: &S) -> Term {
         use ty::TermKind;
-        match self.unpack() {
+        match self.kind() {
             TermKind::Ty(ty) => Term::Ty(ty.sinto(s)),
             TermKind::Const(c) => Term::Const(c.sinto(s)),
         }
diff --git a/rust-toolchain.toml b/rust-toolchain.toml
index f290a30ed..3a87a82e7 100644
--- a/rust-toolchain.toml
+++ b/rust-toolchain.toml
@@ -1,3 +1,3 @@
 [toolchain]
-channel = "nightly-2025-05-26"
+channel = "nightly-2025-06-30"
 components = [ "rustc-dev", "llvm-tools-preview" , "rust-analysis" , "rust-src" , "rustfmt" ]
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 bc99d93be..21d95b115 100644
--- a/test-harness/src/snapshots/toolchain__attribute-opaque into-fstar.snap	
+++ b/test-harness/src/snapshots/toolchain__attribute-opaque into-fstar.snap	
@@ -119,6 +119,7 @@ val ff_pre_post (x y: bool)
           result =. y)
 
 class t_T (v_Self: Type0) = {
+  [@@@ FStar.Tactics.Typeclasses.no_method]_super_4726684624731801277:Core.Marker.t_MetaSized v_Self;
   f_U:Type0;
   f_c:u8;
   f_d_pre:Prims.unit -> Type0;
@@ -133,6 +134,7 @@ class t_T (v_Self: Type0) = {
 val impl_T_for_u8:t_T u8
 
 class t_TrGeneric (v_Self: Type0) (v_U: Type0) = {
+  [@@@ FStar.Tactics.Typeclasses.no_method]_super_4726684624731801277:Core.Marker.t_MetaSized v_Self;
   [@@@ FStar.Tactics.Typeclasses.no_method]_super_17240578109911634293:Core.Clone.t_Clone v_U;
   f_f_pre:v_U -> Type0;
   f_f_post:v_U -> v_Self -> Type0;
diff --git a/test-harness/src/snapshots/toolchain__attributes into-fstar.snap b/test-harness/src/snapshots/toolchain__attributes into-fstar.snap
index 4b29f6b9a..7dca84eb7 100644
--- a/test-harness/src/snapshots/toolchain__attributes into-fstar.snap	
+++ b/test-harness/src/snapshots/toolchain__attributes into-fstar.snap	
@@ -155,6 +155,7 @@ open Core
 open FStar.Mul
 
 class t_T (v_Self: Type0) = {
+  [@@@ FStar.Tactics.Typeclasses.no_method]_super_4726684624731801277:Core.Marker.t_MetaSized v_Self;
   f_v_pre:v_Self -> Type0;
   f_v_post:x: v_Self -> x_future: v_Self -> pred: Type0{pred ==> true};
   f_v:x0: v_Self -> Prims.Pure v_Self (f_v_pre x0) (fun result -> f_v_post x0 result)
@@ -214,6 +215,7 @@ let impl_SafeIndex__as_usize (self: t_SafeIndex) : usize = self.f_i
 let impl_1 (#v_T: Type0) : Core.Ops.Index.t_Index (t_Array v_T (mk_usize 10)) t_SafeIndex =
   {
     f_Output = v_T;
+    f_Output_6696274936538609082 = FStar.Tactics.Typeclasses.solve;
     f_index_pre = (fun (self: t_Array v_T (mk_usize 10)) (index: t_SafeIndex) -> true);
     f_index_post = (fun (self: t_Array v_T (mk_usize 10)) (index: t_SafeIndex) (out: v_T) -> true);
     f_index = fun (self: t_Array v_T (mk_usize 10)) (index: t_SafeIndex) -> self.[ index.f_i ]
@@ -250,6 +252,7 @@ open Core
 open FStar.Mul
 
 class t_Operation (v_Self: Type0) = {
+  [@@@ FStar.Tactics.Typeclasses.no_method]_super_4726684624731801277:Core.Marker.t_MetaSized v_Self;
   f_double_pre:x: u8
     -> pred:
       Type0
@@ -306,6 +309,7 @@ let impl_Operation_for_ViaMul: t_Operation t_ViaMul =
   }
 
 class t_TraitWithRequiresAndEnsures (v_Self: Type0) = {
+  [@@@ FStar.Tactics.Typeclasses.no_method]_super_4726684624731801277:Core.Marker.t_MetaSized v_Self;
   f_method_pre:self_: v_Self -> x: u8 -> pred: Type0{x <. mk_u8 100 ==> pred};
   f_method_post:self_: v_Self -> x: u8 -> r: u8 -> pred: Type0{pred ==> r >. mk_u8 88};
   f_method:x0: v_Self -> x1: u8
@@ -400,6 +404,7 @@ let mutation_example
 let impl: Core.Ops.Index.t_Index t_MyArray usize =
   {
     f_Output = u8;
+    f_Output_6696274936538609082 = FStar.Tactics.Typeclasses.solve;
     f_index_pre = (fun (self_: t_MyArray) (index: usize) -> index <. v_MAX);
     f_index_post = (fun (self: t_MyArray) (index: usize) (out: u8) -> true);
     f_index = fun (self: t_MyArray) (index: usize) -> self.[ index ]
@@ -588,6 +593,7 @@ open Core
 open FStar.Mul
 
 class t_Foo (v_Self: Type0) = {
+  [@@@ FStar.Tactics.Typeclasses.no_method]_super_4726684624731801277:Core.Marker.t_MetaSized v_Self;
   f_f_pre:x: u8 -> y: u8
     -> pred:
       Type0
diff --git a/test-harness/src/snapshots/toolchain__dyn into-fstar.snap b/test-harness/src/snapshots/toolchain__dyn into-fstar.snap
index 0928d26ad..75edb2282 100644
--- a/test-harness/src/snapshots/toolchain__dyn into-fstar.snap	
+++ b/test-harness/src/snapshots/toolchain__dyn into-fstar.snap	
@@ -33,6 +33,7 @@ open Core
 open FStar.Mul
 
 class t_Printable (v_Self: Type0) (v_S: Type0) = {
+  [@@@ FStar.Tactics.Typeclasses.no_method]_super_4726684624731801277:Core.Marker.t_MetaSized v_Self;
   f_stringify_pre:v_Self -> Type0;
   f_stringify_post:v_Self -> v_S -> Type0;
   f_stringify:x0: v_Self
@@ -54,27 +55,28 @@ let print
           Alloc.Boxed.t_Box (dyn 1 (fun z -> t_Printable z Alloc.String.t_String))
             Alloc.Alloc.t_Global)
     : Prims.unit =
+  let args:t_Array Core.Fmt.Rt.t_Argument (mk_usize 1) =
+    let list =
+      [
+        Core.Fmt.Rt.impl__new_display #Alloc.String.t_String
+          (f_stringify #(dyn 1 (fun z -> t_Printable z Alloc.String.t_String))
+              #Alloc.String.t_String
+              #FStar.Tactics.Typeclasses.solve
+              a
+            <:
+            Alloc.String.t_String)
+      ]
+    in
+    FStar.Pervasives.assert_norm (Prims.eq2 (List.Tot.length list) 1);
+    Rust_primitives.Hax.array_of_list 1 list
+  in
   let _:Prims.unit =
-    Std.Io.Stdio.e_print (Core.Fmt.Rt.impl_2__new_v1 (mk_usize 2)
+    Std.Io.Stdio.e_print (Core.Fmt.Rt.impl_1__new_v1 (mk_usize 2)
           (mk_usize 1)
           (let list = [""; "\n"] in
             FStar.Pervasives.assert_norm (Prims.eq2 (List.Tot.length list) 2);
             Rust_primitives.Hax.array_of_list 2 list)
-          (let list =
-              [
-                Core.Fmt.Rt.impl__new_display #Alloc.String.t_String
-                  (f_stringify #(dyn 1 (fun z -> t_Printable z Alloc.String.t_String))
-                      #Alloc.String.t_String
-                      #FStar.Tactics.Typeclasses.solve
-                      a
-                    <:
-                    Alloc.String.t_String)
-                <:
-                Core.Fmt.Rt.t_Argument
-              ]
-            in
-            FStar.Pervasives.assert_norm (Prims.eq2 (List.Tot.length list) 1);
-            Rust_primitives.Hax.array_of_list 1 list)
+          args
         <:
         Core.Fmt.t_Arguments)
   in
diff --git a/test-harness/src/snapshots/toolchain__functions into-fstar.snap b/test-harness/src/snapshots/toolchain__functions into-fstar.snap
index df12b8b6e..f456755a4 100644
--- a/test-harness/src/snapshots/toolchain__functions into-fstar.snap	
+++ b/test-harness/src/snapshots/toolchain__functions into-fstar.snap	
@@ -38,6 +38,7 @@ type t_CallableViaDeref = | CallableViaDeref : t_CallableViaDeref
 let impl: Core.Ops.Deref.t_Deref t_CallableViaDeref =
   {
     f_Target = Prims.unit -> bool;
+    f_Target_4695674276362814091 = FStar.Tactics.Typeclasses.solve;
     f_deref_pre = (fun (self: t_CallableViaDeref) -> true);
     f_deref_post = (fun (self: t_CallableViaDeref) (out: (Prims.unit -> bool)) -> true);
     f_deref
diff --git a/test-harness/src/snapshots/toolchain__generics into-fstar.snap b/test-harness/src/snapshots/toolchain__generics into-fstar.snap
index d42249d1c..c75680dca 100644
--- a/test-harness/src/snapshots/toolchain__generics into-fstar.snap	
+++ b/test-harness/src/snapshots/toolchain__generics into-fstar.snap	
@@ -157,6 +157,7 @@ let call_g (_: Prims.unit) : usize =
   mk_usize 3
 
 class t_Foo (v_Self: Type0) = {
+  [@@@ FStar.Tactics.Typeclasses.no_method]_super_4726684624731801277:Core.Marker.t_MetaSized v_Self;
   f_const_add_pre:v_N: usize -> v_Self -> Type0;
   f_const_add_post:v_N: usize -> v_Self -> usize -> Type0;
   f_const_add:v_N: usize -> x0: v_Self
diff --git a/test-harness/src/snapshots/toolchain__include-flag into-coq.snap b/test-harness/src/snapshots/toolchain__include-flag into-coq.snap
index e0f975a26..b6d4c8c65 100644
--- a/test-harness/src/snapshots/toolchain__include-flag into-coq.snap	
+++ b/test-harness/src/snapshots/toolchain__include-flag into-coq.snap	
@@ -51,10 +51,10 @@ Record Foo_record : Type :=
 #[export]
 Notation "'Foo_Foo_record'" := Build_Foo_record.
 
-Class t_Trait (v_Self : Type) : Type :=
+Class t_Trait (v_Self : Type) `{t_MetaSized (v_Self)} : Type :=
   {
   }.
-Arguments t_Trait (_).
+Arguments t_Trait (_) {_}.
 
 Instance t_Trait_572156424 : t_Trait ((t_Foo)) :=
   {
diff --git a/test-harness/src/snapshots/toolchain__include-flag into-fstar.snap b/test-harness/src/snapshots/toolchain__include-flag into-fstar.snap
index 81212e6dd..45ac83394 100644
--- a/test-harness/src/snapshots/toolchain__include-flag into-fstar.snap	
+++ b/test-harness/src/snapshots/toolchain__include-flag into-fstar.snap	
@@ -34,7 +34,9 @@ open FStar.Mul
 
 type t_Foo = | Foo : t_Foo
 
-class t_Trait (v_Self: Type0) = { __marker_trait_t_Trait:Prims.unit }
+class t_Trait (v_Self: Type0) = {
+  [@@@ FStar.Tactics.Typeclasses.no_method]_super_4726684624731801277:Core.Marker.t_MetaSized v_Self
+}
 
 [@@ FStar.Tactics.Typeclasses.tcinstance]
 let impl: t_Trait t_Foo = { __marker_trait = () }
diff --git a/test-harness/src/snapshots/toolchain__interface-only into-fstar.snap b/test-harness/src/snapshots/toolchain__interface-only into-fstar.snap
index 7d30bbb68..b8c5290cc 100644
--- a/test-harness/src/snapshots/toolchain__interface-only into-fstar.snap	
+++ b/test-harness/src/snapshots/toolchain__interface-only into-fstar.snap	
@@ -101,6 +101,7 @@ unfold
 let ff_generic (v_X: usize) (#v_U: Type0) = ff_generic' v_X #v_U
 
 class t_T (v_Self: Type0) = {
+  [@@@ FStar.Tactics.Typeclasses.no_method]_super_4726684624731801277:Core.Marker.t_MetaSized v_Self;
   f_Assoc:Type0;
   f_d_pre:Prims.unit -> Type0;
   f_d_post:Prims.unit -> Prims.unit -> Type0;
@@ -118,6 +119,7 @@ let impl_T_for_u8: t_T u8 =
   }
 
 class t_T2 (v_Self: Type0) = {
+  [@@@ FStar.Tactics.Typeclasses.no_method]_super_4726684624731801277:Core.Marker.t_MetaSized v_Self;
   f_d_pre:Prims.unit -> Type0;
   f_d_post:Prims.unit -> Prims.unit -> Type0;
   f_d:x0: Prims.unit -> Prims.Pure Prims.unit (f_d_pre x0) (fun result -> f_d_post x0 result)
diff --git a/test-harness/src/snapshots/toolchain__literals into-coq.snap b/test-harness/src/snapshots/toolchain__literals into-coq.snap
index 6c5a0f5e8..640f68231 100644
--- a/test-harness/src/snapshots/toolchain__literals into-coq.snap	
+++ b/test-harness/src/snapshots/toolchain__literals into-coq.snap	
@@ -45,8 +45,7 @@ From Core Require Import Core.
 
 (* NotImplementedYet *)
 
-From Literals Require Import hax_lib.
-Export hax_lib.
+
 
 Definition math_integers (x : t_Int) `{andb (f_gt (x) (impl_Int__e_unsafe_from_str (("0"%string : string)))) (f_lt (x) (impl_Int__e_unsafe_from_str (("16"%string : string)))) = true} : t_u8 :=
   let _ : t_Int := f_lift ((3 : t_usize)) in
@@ -81,7 +80,7 @@ Definition math_integers (x : t_Int) `{andb (f_gt (x) (impl_Int__e_unsafe_from_s
   impl_Int__to_u8 (f_add (x) (f_mul (x) (x))).
 
 Definition panic_with_msg '(_ : unit) : unit :=
-  never_to_any (panic_fmt (impl_2__new_const ([("with msg"%string : string)]))).
+  never_to_any (panic_fmt (impl_1__new_const ([("with msg"%string : string)]))).
 
 Record Foo_record : Type :=
   {
diff --git a/test-harness/src/snapshots/toolchain__literals into-fstar.snap b/test-harness/src/snapshots/toolchain__literals into-fstar.snap
index 35a58078c..23fafa1e1 100644
--- a/test-harness/src/snapshots/toolchain__literals into-fstar.snap	
+++ b/test-harness/src/snapshots/toolchain__literals into-fstar.snap	
@@ -72,7 +72,7 @@ let math_integers (x: Hax_lib.Int.t_Int)
   Hax_lib.Int.impl_Int__to_u8 (x + (x * x <: Hax_lib.Int.t_Int) <: Hax_lib.Int.t_Int)
 
 let panic_with_msg (_: Prims.unit) : Prims.unit =
-  Rust_primitives.Hax.never_to_any (Core.Panicking.panic_fmt (Core.Fmt.Rt.impl_2__new_const (mk_usize
+  Rust_primitives.Hax.never_to_any (Core.Panicking.panic_fmt (Core.Fmt.Rt.impl_1__new_const (mk_usize
               1)
             (let list = ["with msg"] in
               FStar.Pervasives.assert_norm (Prims.eq2 (List.Tot.length list) 1);
diff --git a/test-harness/src/snapshots/toolchain__mut-ref-functionalization into-fstar.snap b/test-harness/src/snapshots/toolchain__mut-ref-functionalization into-fstar.snap
index ac5dff563..38d1d747b 100644
--- a/test-harness/src/snapshots/toolchain__mut-ref-functionalization into-fstar.snap	
+++ b/test-harness/src/snapshots/toolchain__mut-ref-functionalization into-fstar.snap	
@@ -269,6 +269,7 @@ let k
   (Alloc.Vec.t_Vec u8 Alloc.Alloc.t_Global & u16 & Prims.unit & u64)
 
 class t_FooTrait (v_Self: Type0) = {
+  [@@@ FStar.Tactics.Typeclasses.no_method]_super_4726684624731801277:Core.Marker.t_MetaSized v_Self;
   f_z_pre:v_Self -> Type0;
   f_z_post:v_Self -> v_Self -> Type0;
   f_z:x0: v_Self -> Prims.Pure v_Self (f_z_pre x0) (fun result -> f_z_post x0 result)
diff --git a/test-harness/src/snapshots/toolchain__naming into-fstar.snap b/test-harness/src/snapshots/toolchain__naming into-fstar.snap
index cae01d074..9ec3ce4a9 100644
--- a/test-harness/src/snapshots/toolchain__naming into-fstar.snap	
+++ b/test-harness/src/snapshots/toolchain__naming into-fstar.snap	
@@ -33,20 +33,21 @@ open Core
 open FStar.Mul
 
 let debug (label value: u32) : Prims.unit =
+  let args:(u32 & u32) = label, value <: (u32 & u32) in
+  let args:t_Array Core.Fmt.Rt.t_Argument (mk_usize 2) =
+    let list =
+      [Core.Fmt.Rt.impl__new_display #u32 args._1; Core.Fmt.Rt.impl__new_display #u32 args._2]
+    in
+    FStar.Pervasives.assert_norm (Prims.eq2 (List.Tot.length list) 2);
+    Rust_primitives.Hax.array_of_list 2 list
+  in
   let _:Prims.unit =
-    Std.Io.Stdio.e_print (Core.Fmt.Rt.impl_2__new_v1 (mk_usize 3)
+    Std.Io.Stdio.e_print (Core.Fmt.Rt.impl_1__new_v1 (mk_usize 3)
           (mk_usize 2)
           (let list = ["["; "] a="; "\n"] in
             FStar.Pervasives.assert_norm (Prims.eq2 (List.Tot.length list) 3);
             Rust_primitives.Hax.array_of_list 3 list)
-          (let list =
-              [
-                Core.Fmt.Rt.impl__new_display #u32 label <: Core.Fmt.Rt.t_Argument;
-                Core.Fmt.Rt.impl__new_display #u32 value <: Core.Fmt.Rt.t_Argument
-              ]
-            in
-            FStar.Pervasives.assert_norm (Prims.eq2 (List.Tot.length list) 2);
-            Rust_primitives.Hax.array_of_list 2 list)
+          args
         <:
         Core.Fmt.t_Arguments)
   in
@@ -171,7 +172,9 @@ let reserved_names (v_val v_noeq v_of: u8) : u8 = (v_val +! v_noeq <: u8) +! v_o
 
 type t_Arity1 (v_T: Type0) = | Arity1 : v_T -> t_Arity1 v_T
 
-class t_T1 (v_Self: Type0) = { __marker_trait_t_T1:Prims.unit }
+class t_T1 (v_Self: Type0) = {
+  [@@@ FStar.Tactics.Typeclasses.no_method]_super_4726684624731801277:Core.Marker.t_MetaSized v_Self
+}
 
 [@@ FStar.Tactics.Typeclasses.tcinstance]
 let impl_T1_for_Foo: t_T1 t_Foo = { __marker_trait = () }
@@ -179,13 +182,17 @@ let impl_T1_for_Foo: t_T1 t_Foo = { __marker_trait = () }
 [@@ FStar.Tactics.Typeclasses.tcinstance]
 let impl_T1_for_tuple_Foo_u8: t_T1 (t_Foo & u8) = { __marker_trait = () }
 
-class t_T2_for_a (v_Self: Type0) = { __marker_trait_t_T2_for_a:Prims.unit }
+class t_T2_for_a (v_Self: Type0) = {
+  [@@@ FStar.Tactics.Typeclasses.no_method]_super_4726684624731801277:Core.Marker.t_MetaSized v_Self
+}
 
 [@@ FStar.Tactics.Typeclasses.tcinstance]
 let impl_T2_ee_for_a_for_Arity1_of_tuple_Foo_u8: t_T2_for_a (t_Arity1 (t_Foo & u8)) =
   { __marker_trait = () }
 
-class t_T3_ee_for_a (v_Self: Type0) = { __marker_trait_t_T3_ee_for_a:Prims.unit }
+class t_T3_ee_for_a (v_Self: Type0) = {
+  [@@@ FStar.Tactics.Typeclasses.no_method]_super_4726684624731801277:Core.Marker.t_MetaSized v_Self
+}
 
 [@@ FStar.Tactics.Typeclasses.tcinstance]
 let impl_T3_ee_e_for_a_for_Foo: t_T3_ee_for_a t_Foo = { __marker_trait = () }
@@ -213,7 +220,10 @@ let construct_structs (a b: usize) : Prims.unit =
 
 let v_INHERENT_CONSTANT: usize = mk_usize 3
 
-class t_FooTrait (v_Self: Type0) = { f_ASSOCIATED_CONSTANT:usize }
+class t_FooTrait (v_Self: Type0) = {
+  [@@@ FStar.Tactics.Typeclasses.no_method]_super_4726684624731801277:Core.Marker.t_MetaSized v_Self;
+  f_ASSOCIATED_CONSTANT:usize
+}
 
 let constants
       (#v_T: Type0)
diff --git a/test-harness/src/snapshots/toolchain__side-effects into-fstar.snap b/test-harness/src/snapshots/toolchain__side-effects into-fstar.snap
index a92a71909..0a676481d 100644
--- a/test-harness/src/snapshots/toolchain__side-effects into-fstar.snap	
+++ b/test-harness/src/snapshots/toolchain__side-effects into-fstar.snap	
@@ -34,6 +34,7 @@ open Core
 open FStar.Mul
 
 class t_MyFrom (v_Self: Type0) (v_T: Type0) = {
+  [@@@ FStar.Tactics.Typeclasses.no_method]_super_4726684624731801277:Core.Marker.t_MetaSized v_Self;
   f_my_from_pre:v_T -> Type0;
   f_my_from_post:v_T -> v_Self -> Type0;
   f_my_from:x0: v_T -> Prims.Pure v_Self (f_my_from_pre x0) (fun result -> f_my_from_post x0 result)
diff --git a/test-harness/src/snapshots/toolchain__traits into-fstar.snap b/test-harness/src/snapshots/toolchain__traits into-fstar.snap
index 373243c11..fe5fe2c40 100644
--- a/test-harness/src/snapshots/toolchain__traits into-fstar.snap	
+++ b/test-harness/src/snapshots/toolchain__traits into-fstar.snap	
@@ -32,13 +32,18 @@ module Traits.Block_size
 open Core
 open FStar.Mul
 
-class t_BlockSizeUser (v_Self: Type0) = { f_BlockSize:Type0 }
+class t_BlockSizeUser (v_Self: Type0) = {
+  [@@@ FStar.Tactics.Typeclasses.no_method]_super_4726684624731801277:Core.Marker.t_MetaSized v_Self;
+  f_BlockSize:Type0
+}
 
 class t_ParBlocksSizeUser (v_Self: Type0) = {
+  [@@@ FStar.Tactics.Typeclasses.no_method]_super_4726684624731801277:Core.Marker.t_MetaSized v_Self;
   [@@@ FStar.Tactics.Typeclasses.no_method]_super_5884559561557426095:t_BlockSizeUser v_Self
 }
 
 class t_BlockBackend (v_Self: Type0) = {
+  [@@@ FStar.Tactics.Typeclasses.no_method]_super_4726684624731801277:Core.Marker.t_MetaSized v_Self;
   [@@@ FStar.Tactics.Typeclasses.no_method]_super_17422710415653782164:t_ParBlocksSizeUser v_Self;
   f_proc_block_pre:Alloc.Vec.t_Vec _ Alloc.Alloc.t_Global -> Type0;
   f_proc_block_post:Alloc.Vec.t_Vec _ Alloc.Alloc.t_Global -> Prims.unit -> Type0;
@@ -52,9 +57,12 @@ module Traits.Default_traits_parameters
 open Core
 open FStar.Mul
 
-class t_Bar (v_Self: Type0) (v_T: Type0) = { __marker_trait_t_Bar:Prims.unit }
+class t_Bar (v_Self: Type0) (v_T: Type0) = {
+  [@@@ FStar.Tactics.Typeclasses.no_method]_super_4726684624731801277:Core.Marker.t_MetaSized v_Self
+}
 
 class t_Foo (v_Self: Type0) = {
+  [@@@ FStar.Tactics.Typeclasses.no_method]_super_4726684624731801277:Core.Marker.t_MetaSized v_Self;
   [@@@ FStar.Tactics.Typeclasses.no_method]_super_7275791365833186636:t_Bar v_Self f_U;
   f_U:Type0
 }
@@ -65,7 +73,9 @@ module Traits.For_clauses.Issue_495_.Minimized_3_
 open Core
 open FStar.Mul
 
-class t_Trait (v_Self: Type0) = { __marker_trait_t_Trait:Prims.unit }
+class t_Trait (v_Self: Type0) = {
+  [@@@ FStar.Tactics.Typeclasses.no_method]_super_4726684624731801277:Core.Marker.t_MetaSized v_Self
+}
 
 [@@ FStar.Tactics.Typeclasses.tcinstance]
 let impl
@@ -148,6 +158,7 @@ open Core
 open FStar.Mul
 
 class t_Foo (v_Self: Type0) (v_T: Type0) = {
+  [@@@ FStar.Tactics.Typeclasses.no_method]_super_4726684624731801277:Core.Marker.t_MetaSized v_Self;
   f_to_t_pre:v_Self -> Type0;
   f_to_t_post:v_Self -> v_T -> Type0;
   f_to_t:x0: v_Self -> Prims.Pure v_T (f_to_t_pre x0) (fun result -> f_to_t_post x0 result)
@@ -164,9 +175,14 @@ module Traits.Impl_expr_in_goal
 open Core
 open FStar.Mul
 
-class t_T1 (v_Self: Type0) = { f_Assoc:Type0 }
+class t_T1 (v_Self: Type0) = {
+  [@@@ FStar.Tactics.Typeclasses.no_method]_super_4726684624731801277:Core.Marker.t_MetaSized v_Self;
+  f_Assoc:Type0
+}
 
-class t_T2 (v_Self: Type0) = { __marker_trait_t_T2:Prims.unit }
+class t_T2 (v_Self: Type0) = {
+  [@@@ FStar.Tactics.Typeclasses.no_method]_super_4726684624731801277:Core.Marker.t_MetaSized v_Self
+}
 
 [@@ FStar.Tactics.Typeclasses.tcinstance]
 let impl
@@ -230,6 +246,7 @@ open Core
 open FStar.Mul
 
 class t_MyTrait (v_Self: Type0) = {
+  [@@@ FStar.Tactics.Typeclasses.no_method]_super_4726684624731801277:Core.Marker.t_MetaSized v_Self;
   f_my_method_pre:v_Self -> Type0;
   f_my_method_post:v_Self -> Prims.unit -> Type0;
   f_my_method:x0: v_Self
@@ -263,6 +280,7 @@ open FStar.Mul
 type t_Type (v_TypeArg: Type0) (v_ConstArg: usize) = { f_field:t_Array v_TypeArg v_ConstArg }
 
 class t_Trait (v_Self: Type0) (v_TypeArg: Type0) (v_ConstArg: usize) = {
+  [@@@ FStar.Tactics.Typeclasses.no_method]_super_4726684624731801277:Core.Marker.t_MetaSized v_Self;
   f_method_pre:
       #v_MethodTypeArg: Type0 ->
       v_MethodConstArg: usize ->
@@ -425,6 +443,7 @@ let associated_function_caller
   ()
 
 class t_SubTrait (v_Self: Type0) (v_TypeArg: Type0) (v_ConstArg: usize) = {
+  [@@@ FStar.Tactics.Typeclasses.no_method]_super_4726684624731801277:Core.Marker.t_MetaSized v_Self;
   [@@@ FStar.Tactics.Typeclasses.no_method]_super_15145771689388873921:t_Trait v_Self
     v_TypeArg
     v_ConstArg;
@@ -442,6 +461,7 @@ type t_Bar (v_FooConst: usize) (v_FooType: Type0) =
   | Bar : t_Array v_FooType v_FooConst -> t_Bar v_FooConst v_FooType
 
 class t_Foo (v_Self: Type0) (v_FooConst: usize) (v_FooType: Type0) = {
+  [@@@ FStar.Tactics.Typeclasses.no_method]_super_4726684624731801277:Core.Marker.t_MetaSized v_Self;
   f_fun_pre:
       v_FunConst: usize ->
       #v_FunType: Type0 ->
@@ -505,11 +525,13 @@ open Core
 open FStar.Mul
 
 class t_Trait1 (v_Self: Type0) = {
+  [@@@ FStar.Tactics.Typeclasses.no_method]_super_4726684624731801277:Core.Marker.t_MetaSized v_Self;
   f_T:Type0;
   f_T_7969211799618487585:t_Trait1 f_T
 }
 
 class t_Trait2 (v_Self: Type0) = {
+  [@@@ FStar.Tactics.Typeclasses.no_method]_super_4726684624731801277:Core.Marker.t_MetaSized v_Self;
   [@@@ FStar.Tactics.Typeclasses.no_method]_super_3259985701465885527:t_Trait1 v_Self;
   f_U:Type0
 }
@@ -530,6 +552,7 @@ open Core
 open FStar.Mul
 
 class t_PolyOp (v_Self: Type0) = {
+  [@@@ FStar.Tactics.Typeclasses.no_method]_super_4726684624731801277:Core.Marker.t_MetaSized v_Self;
   f_op_pre:u32 -> u32 -> Type0;
   f_op_post:u32 -> u32 -> u32 -> Type0;
   f_op:x0: u32 -> x1: u32 -> Prims.Pure u32 (f_op_pre x0 x1) (fun result -> f_op_post x0 x1 result)
@@ -567,6 +590,7 @@ open Core
 open FStar.Mul
 
 class t_SuperTrait (v_Self: Type0) = {
+  [@@@ FStar.Tactics.Typeclasses.no_method]_super_4726684624731801277:Core.Marker.t_MetaSized v_Self;
   [@@@ FStar.Tactics.Typeclasses.no_method]_super_15837849249852401974:Core.Clone.t_Clone v_Self;
   f_function_of_super_trait_pre:v_Self -> Type0;
   f_function_of_super_trait_post:v_Self -> u32 -> Type0;
@@ -588,6 +612,7 @@ let impl: t_SuperTrait i32 =
 type t_Struct = | Struct : t_Struct
 
 class t_Bar (v_Self: Type0) = {
+  [@@@ FStar.Tactics.Typeclasses.no_method]_super_4726684624731801277:Core.Marker.t_MetaSized v_Self;
   f_bar_pre:v_Self -> Type0;
   f_bar_post:v_Self -> Prims.unit -> Type0;
   f_bar:x0: v_Self -> Prims.Pure Prims.unit (f_bar_pre x0) (fun result -> f_bar_post x0 result)
@@ -650,6 +675,7 @@ let uuse_iimpl_trait (_: Prims.unit) : Prims.unit =
   ()
 
 class t_Foo (v_Self: Type0) = {
+  [@@@ FStar.Tactics.Typeclasses.no_method]_super_4726684624731801277:Core.Marker.t_MetaSized v_Self;
   f_AssocType:Type0;
   f_AssocType_1162045947544099865:t_SuperTrait f_AssocType;
   f_N:usize;

From c9ab370e7c7c27610bddd0eab68fe9131033cf77 Mon Sep 17 00:00:00 2001
From: Lucas Franceschino <lucas@cryspen.com>
Date: Thu, 3 Jul 2025 12:57:22 +0200
Subject: [PATCH 02/18] feat(engine/phases): intro. `Drop_metasized`

---
 engine/lib/phases/phase_drop_metasized.ml  | 192 +++++++++++++++++++++
 engine/lib/phases/phase_drop_metasized.mli |  15 ++
 2 files changed, 207 insertions(+)
 create mode 100644 engine/lib/phases/phase_drop_metasized.ml
 create mode 100644 engine/lib/phases/phase_drop_metasized.mli

diff --git a/engine/lib/phases/phase_drop_metasized.ml b/engine/lib/phases/phase_drop_metasized.ml
new file mode 100644
index 000000000..781b15aa0
--- /dev/null
+++ b/engine/lib/phases/phase_drop_metasized.ml
@@ -0,0 +1,192 @@
+(** This phase gets rid of the MetaSized bound. See https://github.com/cryspen/hax/pull/1534. *)
+
+open! Prelude
+
+module%inlined_contents Make (F : Features.T) = struct
+  open Ast
+  module FA = F
+  module FB = FA
+
+  include
+    Phase_utils.MakeBase (F) (FB)
+      (struct
+        let phase_id = [%auto_phase_name auto]
+      end)
+
+  module UA = Ast_utils.Make (F)
+
+  module Implem : ImplemT.T = struct
+    let metadata = metadata
+
+    module S = struct
+      include Features.SUBTYPE.Id
+    end
+
+    [%%inline_defs dmutability + dsafety_kind]
+
+    let rec dimpl_expr (span : span) (i : A.impl_expr) : B.impl_expr option =
+      let* kind = dimpl_expr_kind span i.kind in
+      let* goal = dtrait_goal span i.goal in
+      Some B.{ kind; goal }
+
+    and dtrait_goal (span : span) (r : A.trait_goal) : B.trait_goal option =
+      let*? _ = not (Concrete_ident.eq_name Core__marker__MetaSized r.trait) in
+      Some
+        B.{ trait = r.trait; args = List.map ~f:(dgeneric_value span) r.args }
+
+    and dimpl_expr_exn message span i =
+      match dimpl_expr span i with
+      | None -> Error.assertion_failure span message
+      | Some impl -> impl
+
+    and dimpl_ident (span : span) (r : A.impl_ident) : B.impl_ident option =
+      let* goal = dtrait_goal span r.goal in
+      Some B.{ goal; name = r.name }
+
+    and dty (span : span) (ty : A.ty) : B.ty =
+      match ty with
+      | TAssociatedType { impl; item } ->
+          let impl =
+            dimpl_expr_exn "MetaSized has no associated type" span impl
+          in
+          TAssociatedType { impl; item }
+      | [%inline_arms "dty.*" - TAssociatedType] -> auto
+
+    and dprojection_predicate (span : span) (r : A.projection_predicate) :
+        B.projection_predicate =
+      {
+        impl = dimpl_expr_exn "MetaSized cannot be projected" span r.impl;
+        assoc_item = r.assoc_item;
+        typ = dty span r.typ;
+      }
+
+    and dimpl_expr_kind (span : span) (i : A.impl_expr_kind) :
+        B.impl_expr_kind option =
+      match i with
+      | Parent { impl; ident } ->
+          let* impl = dimpl_expr span impl in
+          let* ident = dimpl_ident span ident in
+          Some (B.Parent { impl; ident })
+      | Projection { impl; item; ident } ->
+          let impl = dimpl_expr_exn "MetaSized have no projection" span impl in
+          let* ident = dimpl_ident span ident in
+          Some (B.Projection { impl; item; ident })
+      | ImplApp { impl; args } ->
+          let* impl = dimpl_expr span impl in
+          let args = List.filter_map ~f:(dimpl_expr span) args in
+          Some (B.ImplApp { impl; args })
+      | Builtin tr ->
+          let* tr = dtrait_goal span tr in
+          Some (B.Builtin tr)
+      | Concrete tr ->
+          let* tr = dtrait_goal span tr in
+          Some (B.Concrete tr)
+      | [%inline_arms
+          "dimpl_expr_kind.*" - Parent - Projection - ImplApp - Builtin
+          - Concrete] ->
+          map (fun x ->
+              Some
+                (let result : B.impl_expr_kind = x in
+                 result))
+
+    and dexpr' (span : span) (expr : A.expr') : B.expr' =
+      match expr with
+      | App { f; args; generic_args; bounds_impls; trait } ->
+          let dgeneric_values = List.map ~f:(dgeneric_value span) in
+          App
+            {
+              f = dexpr f;
+              args = List.map ~f:dexpr args;
+              generic_args = dgeneric_values generic_args;
+              bounds_impls = List.filter_map ~f:(dimpl_expr span) bounds_impls;
+              trait =
+                Option.map
+                  ~f:
+                    (dimpl_expr_exn "MetaSized have no method" span
+                    *** dgeneric_values)
+                  trait;
+            }
+      | [%inline_arms "dexpr'.*" - App] -> auto
+    [@@inline_ands
+      bindings_of dty - dimpl_expr - dexpr' - dprojection_predicate
+      - dimpl_expr_kind - dty - dimpl_ident]
+
+    let rec dimpl_item' (span : span) (ii : A.impl_item') : B.impl_item' =
+      match ii with
+      | IIType { typ; parent_bounds } ->
+          IIType
+            {
+              typ = dty span typ;
+              parent_bounds =
+                List.filter_map
+                  ~f:(fun (impl, ident) ->
+                    let* impl = dimpl_expr span impl in
+                    let* ident = dimpl_ident span ident in
+                    Some (impl, ident))
+                  parent_bounds;
+            }
+          (* | _ -> Obj.magic () *)
+      | [%inline_arms "dimpl_item'.*" - IIType] -> auto
+
+    and dtrait_item' (span : span) (ti : A.trait_item') : B.trait_item' =
+      match ti with
+      | TIType idents -> TIType (List.filter_map ~f:(dimpl_ident span) idents)
+      | [%inline_arms "dtrait_item'.*" - TIType] -> auto
+
+    and dgeneric_constraint (span : span)
+        (generic_constraint : A.generic_constraint) :
+        B.generic_constraint option =
+      match generic_constraint with
+      | GCLifetime (lf, witness) ->
+          Some (B.GCLifetime (lf, S.lifetime span witness))
+      | GCType impl_ident ->
+          let* impl = dimpl_ident span impl_ident in
+          Some (B.GCType impl)
+      | GCProjection projection ->
+          Some (B.GCProjection (dprojection_predicate span projection))
+
+    and dgenerics (span : span) (g : A.generics) : B.generics =
+      {
+        params = List.map ~f:(dgeneric_param span) g.params;
+        constraints =
+          List.filter_map ~f:(dgeneric_constraint span) g.constraints;
+      }
+
+    and ditem' (span : span) (item : A.item') : B.item' =
+      match item with
+      | Impl
+          {
+            generics;
+            self_ty;
+            of_trait = trait_id, trait_generics;
+            items;
+            parent_bounds;
+            safety;
+          } ->
+          B.Impl
+            {
+              generics = dgenerics span generics;
+              self_ty = dty span self_ty;
+              of_trait =
+                (trait_id, List.map ~f:(dgeneric_value span) trait_generics);
+              items = List.map ~f:dimpl_item items;
+              parent_bounds =
+                List.filter_map
+                  ~f:(fun (impl, ident) ->
+                    let* impl = dimpl_expr span impl in
+                    let* ident = dimpl_ident span ident in
+                    Some (impl, ident))
+                  parent_bounds;
+              safety = dsafety_kind span safety;
+            }
+      | [%inline_arms "ditem'.*" - Impl] -> auto
+    [@@inline_ands
+      "Item.*" - ditem' - dimpl_item' - dtrait_item' - dgeneric_constraint
+      - dgenerics]
+
+    [%%inline_defs ditems]
+  end
+
+  include Implem
+end
+[@@add "subtype.ml"]
diff --git a/engine/lib/phases/phase_drop_metasized.mli b/engine/lib/phases/phase_drop_metasized.mli
new file mode 100644
index 000000000..97a1d8598
--- /dev/null
+++ b/engine/lib/phases/phase_drop_metasized.mli
@@ -0,0 +1,15 @@
+(** This phase gets rid of the MetaSized bound. See https://github.com/cryspen/hax/pull/1534. *)
+
+open! Prelude
+
+module Make (F : Features.T) : sig
+  include module type of struct
+    module FA = F
+    module FB = FA
+    module A = Ast.Make (F)
+    module B = Ast.Make (FB)
+    module ImplemT = Phase_utils.MakePhaseImplemT (A) (B)
+  end
+
+  include ImplemT.T
+end

From 378b25cd07dc9cd19cb1115b8b8886395d002cf0 Mon Sep 17 00:00:00 2001
From: Lucas Franceschino <lucas@cryspen.com>
Date: Thu, 3 Jul 2025 12:57:44 +0200
Subject: [PATCH 03/18] feat(engine/phases): use phase `Drop_metasized` in all
 backends

---
 engine/backends/coq/coq/coq_backend.ml         | 1 +
 engine/backends/coq/ssprove/ssprove_backend.ml | 1 +
 engine/backends/fstar/fstar_backend.ml         | 1 +
 engine/backends/proverif/proverif_backend.ml   | 1 +
 4 files changed, 4 insertions(+)

diff --git a/engine/backends/coq/coq/coq_backend.ml b/engine/backends/coq/coq/coq_backend.ml
index 0040f9cbc..2bf0f73f3 100644
--- a/engine/backends/coq/coq/coq_backend.ml
+++ b/engine/backends/coq/coq/coq_backend.ml
@@ -1086,6 +1086,7 @@ open Phase_utils
 module TransformToInputLanguage =
   [%functor_application
   Phases.Reject.Unsafe(Features.Rust)
+  |> Phases.Drop_metasized
   |> Phases.Reject.RawOrMutPointer
   |> Phases.And_mut_defsite
   |> Phases.Reconstruct_asserts
diff --git a/engine/backends/coq/ssprove/ssprove_backend.ml b/engine/backends/coq/ssprove/ssprove_backend.ml
index 867af31b6..f6057deb3 100644
--- a/engine/backends/coq/ssprove/ssprove_backend.ml
+++ b/engine/backends/coq/ssprove/ssprove_backend.ml
@@ -555,6 +555,7 @@ open Phase_utils
 module TransformToInputLanguage =
   [%functor_application
     Phases.Reject.Unsafe(Features.Rust)
+    |> Phases.Drop_metasized
     |> Phases.Reject.RawOrMutPointer
     |> Phases.And_mut_defsite
     |> Phases.Reconstruct_asserts
diff --git a/engine/backends/fstar/fstar_backend.ml b/engine/backends/fstar/fstar_backend.ml
index 7e1e49494..dd790222f 100644
--- a/engine/backends/fstar/fstar_backend.ml
+++ b/engine/backends/fstar/fstar_backend.ml
@@ -1911,6 +1911,7 @@ module DepGraphR = Dependencies.Make (Features.Rust)
 module TransformToInputLanguage =
   [%functor_application
     Phases.Reject.RawOrMutPointer(Features.Rust)
+  |> Phases.Drop_metasized
   |> Phases.Transform_hax_lib_inline
   |> Phases.Specialize
   |> Phases.Drop_sized_trait
diff --git a/engine/backends/proverif/proverif_backend.ml b/engine/backends/proverif/proverif_backend.ml
index 4ec084c1e..d49531cdd 100644
--- a/engine/backends/proverif/proverif_backend.ml
+++ b/engine/backends/proverif/proverif_backend.ml
@@ -887,6 +887,7 @@ module DepGraphR = Dependencies.Make (Features.Rust)
 module TransformToInputLanguage =
   [%functor_application
   Phases.Reject.Unsafe(Features.Rust)
+  |> Phases.Drop_metasized
   |> Phases.Reject.RawOrMutPointer
   |> Phases.Transform_hax_lib_inline
   |> Phases.Simplify_question_marks

From d5a65cad9ab79b05b8eeb70be83854a7bcc42e78 Mon Sep 17 00:00:00 2001
From: Lucas Franceschino <lucas@cryspen.com>
Date: Thu, 3 Jul 2025 12:58:16 +0200
Subject: [PATCH 04/18] chore(engine/phases): `Drop_metasized`: update test
 snapshots

---
 ...oolchain__attribute-opaque into-fstar.snap |  2 --
 .../toolchain__attributes into-fstar.snap     |  6 ----
 .../snapshots/toolchain__dyn into-fstar.snap  |  1 -
 .../toolchain__functions into-fstar.snap      |  1 -
 .../toolchain__generics into-fstar.snap       |  1 -
 .../toolchain__include-flag into-coq.snap     |  4 +--
 .../toolchain__include-flag into-fstar.snap   |  4 +--
 .../toolchain__interface-only into-fstar.snap |  2 --
 ..._mut-ref-functionalization into-fstar.snap |  1 -
 .../toolchain__naming into-fstar.snap         | 17 +++------
 .../toolchain__side-effects into-fstar.snap   |  1 -
 .../toolchain__traits into-fstar.snap         | 36 +++----------------
 12 files changed, 12 insertions(+), 64 deletions(-)

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 21d95b115..bc99d93be 100644
--- a/test-harness/src/snapshots/toolchain__attribute-opaque into-fstar.snap	
+++ b/test-harness/src/snapshots/toolchain__attribute-opaque into-fstar.snap	
@@ -119,7 +119,6 @@ val ff_pre_post (x y: bool)
           result =. y)
 
 class t_T (v_Self: Type0) = {
-  [@@@ FStar.Tactics.Typeclasses.no_method]_super_4726684624731801277:Core.Marker.t_MetaSized v_Self;
   f_U:Type0;
   f_c:u8;
   f_d_pre:Prims.unit -> Type0;
@@ -134,7 +133,6 @@ class t_T (v_Self: Type0) = {
 val impl_T_for_u8:t_T u8
 
 class t_TrGeneric (v_Self: Type0) (v_U: Type0) = {
-  [@@@ FStar.Tactics.Typeclasses.no_method]_super_4726684624731801277:Core.Marker.t_MetaSized v_Self;
   [@@@ FStar.Tactics.Typeclasses.no_method]_super_17240578109911634293:Core.Clone.t_Clone v_U;
   f_f_pre:v_U -> Type0;
   f_f_post:v_U -> v_Self -> Type0;
diff --git a/test-harness/src/snapshots/toolchain__attributes into-fstar.snap b/test-harness/src/snapshots/toolchain__attributes into-fstar.snap
index 7dca84eb7..4b29f6b9a 100644
--- a/test-harness/src/snapshots/toolchain__attributes into-fstar.snap	
+++ b/test-harness/src/snapshots/toolchain__attributes into-fstar.snap	
@@ -155,7 +155,6 @@ open Core
 open FStar.Mul
 
 class t_T (v_Self: Type0) = {
-  [@@@ FStar.Tactics.Typeclasses.no_method]_super_4726684624731801277:Core.Marker.t_MetaSized v_Self;
   f_v_pre:v_Self -> Type0;
   f_v_post:x: v_Self -> x_future: v_Self -> pred: Type0{pred ==> true};
   f_v:x0: v_Self -> Prims.Pure v_Self (f_v_pre x0) (fun result -> f_v_post x0 result)
@@ -215,7 +214,6 @@ let impl_SafeIndex__as_usize (self: t_SafeIndex) : usize = self.f_i
 let impl_1 (#v_T: Type0) : Core.Ops.Index.t_Index (t_Array v_T (mk_usize 10)) t_SafeIndex =
   {
     f_Output = v_T;
-    f_Output_6696274936538609082 = FStar.Tactics.Typeclasses.solve;
     f_index_pre = (fun (self: t_Array v_T (mk_usize 10)) (index: t_SafeIndex) -> true);
     f_index_post = (fun (self: t_Array v_T (mk_usize 10)) (index: t_SafeIndex) (out: v_T) -> true);
     f_index = fun (self: t_Array v_T (mk_usize 10)) (index: t_SafeIndex) -> self.[ index.f_i ]
@@ -252,7 +250,6 @@ open Core
 open FStar.Mul
 
 class t_Operation (v_Self: Type0) = {
-  [@@@ FStar.Tactics.Typeclasses.no_method]_super_4726684624731801277:Core.Marker.t_MetaSized v_Self;
   f_double_pre:x: u8
     -> pred:
       Type0
@@ -309,7 +306,6 @@ let impl_Operation_for_ViaMul: t_Operation t_ViaMul =
   }
 
 class t_TraitWithRequiresAndEnsures (v_Self: Type0) = {
-  [@@@ FStar.Tactics.Typeclasses.no_method]_super_4726684624731801277:Core.Marker.t_MetaSized v_Self;
   f_method_pre:self_: v_Self -> x: u8 -> pred: Type0{x <. mk_u8 100 ==> pred};
   f_method_post:self_: v_Self -> x: u8 -> r: u8 -> pred: Type0{pred ==> r >. mk_u8 88};
   f_method:x0: v_Self -> x1: u8
@@ -404,7 +400,6 @@ let mutation_example
 let impl: Core.Ops.Index.t_Index t_MyArray usize =
   {
     f_Output = u8;
-    f_Output_6696274936538609082 = FStar.Tactics.Typeclasses.solve;
     f_index_pre = (fun (self_: t_MyArray) (index: usize) -> index <. v_MAX);
     f_index_post = (fun (self: t_MyArray) (index: usize) (out: u8) -> true);
     f_index = fun (self: t_MyArray) (index: usize) -> self.[ index ]
@@ -593,7 +588,6 @@ open Core
 open FStar.Mul
 
 class t_Foo (v_Self: Type0) = {
-  [@@@ FStar.Tactics.Typeclasses.no_method]_super_4726684624731801277:Core.Marker.t_MetaSized v_Self;
   f_f_pre:x: u8 -> y: u8
     -> pred:
       Type0
diff --git a/test-harness/src/snapshots/toolchain__dyn into-fstar.snap b/test-harness/src/snapshots/toolchain__dyn into-fstar.snap
index 75edb2282..916b17337 100644
--- a/test-harness/src/snapshots/toolchain__dyn into-fstar.snap	
+++ b/test-harness/src/snapshots/toolchain__dyn into-fstar.snap	
@@ -33,7 +33,6 @@ open Core
 open FStar.Mul
 
 class t_Printable (v_Self: Type0) (v_S: Type0) = {
-  [@@@ FStar.Tactics.Typeclasses.no_method]_super_4726684624731801277:Core.Marker.t_MetaSized v_Self;
   f_stringify_pre:v_Self -> Type0;
   f_stringify_post:v_Self -> v_S -> Type0;
   f_stringify:x0: v_Self
diff --git a/test-harness/src/snapshots/toolchain__functions into-fstar.snap b/test-harness/src/snapshots/toolchain__functions into-fstar.snap
index f456755a4..df12b8b6e 100644
--- a/test-harness/src/snapshots/toolchain__functions into-fstar.snap	
+++ b/test-harness/src/snapshots/toolchain__functions into-fstar.snap	
@@ -38,7 +38,6 @@ type t_CallableViaDeref = | CallableViaDeref : t_CallableViaDeref
 let impl: Core.Ops.Deref.t_Deref t_CallableViaDeref =
   {
     f_Target = Prims.unit -> bool;
-    f_Target_4695674276362814091 = FStar.Tactics.Typeclasses.solve;
     f_deref_pre = (fun (self: t_CallableViaDeref) -> true);
     f_deref_post = (fun (self: t_CallableViaDeref) (out: (Prims.unit -> bool)) -> true);
     f_deref
diff --git a/test-harness/src/snapshots/toolchain__generics into-fstar.snap b/test-harness/src/snapshots/toolchain__generics into-fstar.snap
index c75680dca..d42249d1c 100644
--- a/test-harness/src/snapshots/toolchain__generics into-fstar.snap	
+++ b/test-harness/src/snapshots/toolchain__generics into-fstar.snap	
@@ -157,7 +157,6 @@ let call_g (_: Prims.unit) : usize =
   mk_usize 3
 
 class t_Foo (v_Self: Type0) = {
-  [@@@ FStar.Tactics.Typeclasses.no_method]_super_4726684624731801277:Core.Marker.t_MetaSized v_Self;
   f_const_add_pre:v_N: usize -> v_Self -> Type0;
   f_const_add_post:v_N: usize -> v_Self -> usize -> Type0;
   f_const_add:v_N: usize -> x0: v_Self
diff --git a/test-harness/src/snapshots/toolchain__include-flag into-coq.snap b/test-harness/src/snapshots/toolchain__include-flag into-coq.snap
index b6d4c8c65..e0f975a26 100644
--- a/test-harness/src/snapshots/toolchain__include-flag into-coq.snap	
+++ b/test-harness/src/snapshots/toolchain__include-flag into-coq.snap	
@@ -51,10 +51,10 @@ Record Foo_record : Type :=
 #[export]
 Notation "'Foo_Foo_record'" := Build_Foo_record.
 
-Class t_Trait (v_Self : Type) `{t_MetaSized (v_Self)} : Type :=
+Class t_Trait (v_Self : Type) : Type :=
   {
   }.
-Arguments t_Trait (_) {_}.
+Arguments t_Trait (_).
 
 Instance t_Trait_572156424 : t_Trait ((t_Foo)) :=
   {
diff --git a/test-harness/src/snapshots/toolchain__include-flag into-fstar.snap b/test-harness/src/snapshots/toolchain__include-flag into-fstar.snap
index 45ac83394..81212e6dd 100644
--- a/test-harness/src/snapshots/toolchain__include-flag into-fstar.snap	
+++ b/test-harness/src/snapshots/toolchain__include-flag into-fstar.snap	
@@ -34,9 +34,7 @@ open FStar.Mul
 
 type t_Foo = | Foo : t_Foo
 
-class t_Trait (v_Self: Type0) = {
-  [@@@ FStar.Tactics.Typeclasses.no_method]_super_4726684624731801277:Core.Marker.t_MetaSized v_Self
-}
+class t_Trait (v_Self: Type0) = { __marker_trait_t_Trait:Prims.unit }
 
 [@@ FStar.Tactics.Typeclasses.tcinstance]
 let impl: t_Trait t_Foo = { __marker_trait = () }
diff --git a/test-harness/src/snapshots/toolchain__interface-only into-fstar.snap b/test-harness/src/snapshots/toolchain__interface-only into-fstar.snap
index b8c5290cc..7d30bbb68 100644
--- a/test-harness/src/snapshots/toolchain__interface-only into-fstar.snap	
+++ b/test-harness/src/snapshots/toolchain__interface-only into-fstar.snap	
@@ -101,7 +101,6 @@ unfold
 let ff_generic (v_X: usize) (#v_U: Type0) = ff_generic' v_X #v_U
 
 class t_T (v_Self: Type0) = {
-  [@@@ FStar.Tactics.Typeclasses.no_method]_super_4726684624731801277:Core.Marker.t_MetaSized v_Self;
   f_Assoc:Type0;
   f_d_pre:Prims.unit -> Type0;
   f_d_post:Prims.unit -> Prims.unit -> Type0;
@@ -119,7 +118,6 @@ let impl_T_for_u8: t_T u8 =
   }
 
 class t_T2 (v_Self: Type0) = {
-  [@@@ FStar.Tactics.Typeclasses.no_method]_super_4726684624731801277:Core.Marker.t_MetaSized v_Self;
   f_d_pre:Prims.unit -> Type0;
   f_d_post:Prims.unit -> Prims.unit -> Type0;
   f_d:x0: Prims.unit -> Prims.Pure Prims.unit (f_d_pre x0) (fun result -> f_d_post x0 result)
diff --git a/test-harness/src/snapshots/toolchain__mut-ref-functionalization into-fstar.snap b/test-harness/src/snapshots/toolchain__mut-ref-functionalization into-fstar.snap
index 38d1d747b..ac5dff563 100644
--- a/test-harness/src/snapshots/toolchain__mut-ref-functionalization into-fstar.snap	
+++ b/test-harness/src/snapshots/toolchain__mut-ref-functionalization into-fstar.snap	
@@ -269,7 +269,6 @@ let k
   (Alloc.Vec.t_Vec u8 Alloc.Alloc.t_Global & u16 & Prims.unit & u64)
 
 class t_FooTrait (v_Self: Type0) = {
-  [@@@ FStar.Tactics.Typeclasses.no_method]_super_4726684624731801277:Core.Marker.t_MetaSized v_Self;
   f_z_pre:v_Self -> Type0;
   f_z_post:v_Self -> v_Self -> Type0;
   f_z:x0: v_Self -> Prims.Pure v_Self (f_z_pre x0) (fun result -> f_z_post x0 result)
diff --git a/test-harness/src/snapshots/toolchain__naming into-fstar.snap b/test-harness/src/snapshots/toolchain__naming into-fstar.snap
index 9ec3ce4a9..cd6dea444 100644
--- a/test-harness/src/snapshots/toolchain__naming into-fstar.snap	
+++ b/test-harness/src/snapshots/toolchain__naming into-fstar.snap	
@@ -172,9 +172,7 @@ let reserved_names (v_val v_noeq v_of: u8) : u8 = (v_val +! v_noeq <: u8) +! v_o
 
 type t_Arity1 (v_T: Type0) = | Arity1 : v_T -> t_Arity1 v_T
 
-class t_T1 (v_Self: Type0) = {
-  [@@@ FStar.Tactics.Typeclasses.no_method]_super_4726684624731801277:Core.Marker.t_MetaSized v_Self
-}
+class t_T1 (v_Self: Type0) = { __marker_trait_t_T1:Prims.unit }
 
 [@@ FStar.Tactics.Typeclasses.tcinstance]
 let impl_T1_for_Foo: t_T1 t_Foo = { __marker_trait = () }
@@ -182,17 +180,13 @@ let impl_T1_for_Foo: t_T1 t_Foo = { __marker_trait = () }
 [@@ FStar.Tactics.Typeclasses.tcinstance]
 let impl_T1_for_tuple_Foo_u8: t_T1 (t_Foo & u8) = { __marker_trait = () }
 
-class t_T2_for_a (v_Self: Type0) = {
-  [@@@ FStar.Tactics.Typeclasses.no_method]_super_4726684624731801277:Core.Marker.t_MetaSized v_Self
-}
+class t_T2_for_a (v_Self: Type0) = { __marker_trait_t_T2_for_a:Prims.unit }
 
 [@@ FStar.Tactics.Typeclasses.tcinstance]
 let impl_T2_ee_for_a_for_Arity1_of_tuple_Foo_u8: t_T2_for_a (t_Arity1 (t_Foo & u8)) =
   { __marker_trait = () }
 
-class t_T3_ee_for_a (v_Self: Type0) = {
-  [@@@ FStar.Tactics.Typeclasses.no_method]_super_4726684624731801277:Core.Marker.t_MetaSized v_Self
-}
+class t_T3_ee_for_a (v_Self: Type0) = { __marker_trait_t_T3_ee_for_a:Prims.unit }
 
 [@@ FStar.Tactics.Typeclasses.tcinstance]
 let impl_T3_ee_e_for_a_for_Foo: t_T3_ee_for_a t_Foo = { __marker_trait = () }
@@ -220,10 +214,7 @@ let construct_structs (a b: usize) : Prims.unit =
 
 let v_INHERENT_CONSTANT: usize = mk_usize 3
 
-class t_FooTrait (v_Self: Type0) = {
-  [@@@ FStar.Tactics.Typeclasses.no_method]_super_4726684624731801277:Core.Marker.t_MetaSized v_Self;
-  f_ASSOCIATED_CONSTANT:usize
-}
+class t_FooTrait (v_Self: Type0) = { f_ASSOCIATED_CONSTANT:usize }
 
 let constants
       (#v_T: Type0)
diff --git a/test-harness/src/snapshots/toolchain__side-effects into-fstar.snap b/test-harness/src/snapshots/toolchain__side-effects into-fstar.snap
index 0a676481d..a92a71909 100644
--- a/test-harness/src/snapshots/toolchain__side-effects into-fstar.snap	
+++ b/test-harness/src/snapshots/toolchain__side-effects into-fstar.snap	
@@ -34,7 +34,6 @@ open Core
 open FStar.Mul
 
 class t_MyFrom (v_Self: Type0) (v_T: Type0) = {
-  [@@@ FStar.Tactics.Typeclasses.no_method]_super_4726684624731801277:Core.Marker.t_MetaSized v_Self;
   f_my_from_pre:v_T -> Type0;
   f_my_from_post:v_T -> v_Self -> Type0;
   f_my_from:x0: v_T -> Prims.Pure v_Self (f_my_from_pre x0) (fun result -> f_my_from_post x0 result)
diff --git a/test-harness/src/snapshots/toolchain__traits into-fstar.snap b/test-harness/src/snapshots/toolchain__traits into-fstar.snap
index fe5fe2c40..373243c11 100644
--- a/test-harness/src/snapshots/toolchain__traits into-fstar.snap	
+++ b/test-harness/src/snapshots/toolchain__traits into-fstar.snap	
@@ -32,18 +32,13 @@ module Traits.Block_size
 open Core
 open FStar.Mul
 
-class t_BlockSizeUser (v_Self: Type0) = {
-  [@@@ FStar.Tactics.Typeclasses.no_method]_super_4726684624731801277:Core.Marker.t_MetaSized v_Self;
-  f_BlockSize:Type0
-}
+class t_BlockSizeUser (v_Self: Type0) = { f_BlockSize:Type0 }
 
 class t_ParBlocksSizeUser (v_Self: Type0) = {
-  [@@@ FStar.Tactics.Typeclasses.no_method]_super_4726684624731801277:Core.Marker.t_MetaSized v_Self;
   [@@@ FStar.Tactics.Typeclasses.no_method]_super_5884559561557426095:t_BlockSizeUser v_Self
 }
 
 class t_BlockBackend (v_Self: Type0) = {
-  [@@@ FStar.Tactics.Typeclasses.no_method]_super_4726684624731801277:Core.Marker.t_MetaSized v_Self;
   [@@@ FStar.Tactics.Typeclasses.no_method]_super_17422710415653782164:t_ParBlocksSizeUser v_Self;
   f_proc_block_pre:Alloc.Vec.t_Vec _ Alloc.Alloc.t_Global -> Type0;
   f_proc_block_post:Alloc.Vec.t_Vec _ Alloc.Alloc.t_Global -> Prims.unit -> Type0;
@@ -57,12 +52,9 @@ module Traits.Default_traits_parameters
 open Core
 open FStar.Mul
 
-class t_Bar (v_Self: Type0) (v_T: Type0) = {
-  [@@@ FStar.Tactics.Typeclasses.no_method]_super_4726684624731801277:Core.Marker.t_MetaSized v_Self
-}
+class t_Bar (v_Self: Type0) (v_T: Type0) = { __marker_trait_t_Bar:Prims.unit }
 
 class t_Foo (v_Self: Type0) = {
-  [@@@ FStar.Tactics.Typeclasses.no_method]_super_4726684624731801277:Core.Marker.t_MetaSized v_Self;
   [@@@ FStar.Tactics.Typeclasses.no_method]_super_7275791365833186636:t_Bar v_Self f_U;
   f_U:Type0
 }
@@ -73,9 +65,7 @@ module Traits.For_clauses.Issue_495_.Minimized_3_
 open Core
 open FStar.Mul
 
-class t_Trait (v_Self: Type0) = {
-  [@@@ FStar.Tactics.Typeclasses.no_method]_super_4726684624731801277:Core.Marker.t_MetaSized v_Self
-}
+class t_Trait (v_Self: Type0) = { __marker_trait_t_Trait:Prims.unit }
 
 [@@ FStar.Tactics.Typeclasses.tcinstance]
 let impl
@@ -158,7 +148,6 @@ open Core
 open FStar.Mul
 
 class t_Foo (v_Self: Type0) (v_T: Type0) = {
-  [@@@ FStar.Tactics.Typeclasses.no_method]_super_4726684624731801277:Core.Marker.t_MetaSized v_Self;
   f_to_t_pre:v_Self -> Type0;
   f_to_t_post:v_Self -> v_T -> Type0;
   f_to_t:x0: v_Self -> Prims.Pure v_T (f_to_t_pre x0) (fun result -> f_to_t_post x0 result)
@@ -175,14 +164,9 @@ module Traits.Impl_expr_in_goal
 open Core
 open FStar.Mul
 
-class t_T1 (v_Self: Type0) = {
-  [@@@ FStar.Tactics.Typeclasses.no_method]_super_4726684624731801277:Core.Marker.t_MetaSized v_Self;
-  f_Assoc:Type0
-}
+class t_T1 (v_Self: Type0) = { f_Assoc:Type0 }
 
-class t_T2 (v_Self: Type0) = {
-  [@@@ FStar.Tactics.Typeclasses.no_method]_super_4726684624731801277:Core.Marker.t_MetaSized v_Self
-}
+class t_T2 (v_Self: Type0) = { __marker_trait_t_T2:Prims.unit }
 
 [@@ FStar.Tactics.Typeclasses.tcinstance]
 let impl
@@ -246,7 +230,6 @@ open Core
 open FStar.Mul
 
 class t_MyTrait (v_Self: Type0) = {
-  [@@@ FStar.Tactics.Typeclasses.no_method]_super_4726684624731801277:Core.Marker.t_MetaSized v_Self;
   f_my_method_pre:v_Self -> Type0;
   f_my_method_post:v_Self -> Prims.unit -> Type0;
   f_my_method:x0: v_Self
@@ -280,7 +263,6 @@ open FStar.Mul
 type t_Type (v_TypeArg: Type0) (v_ConstArg: usize) = { f_field:t_Array v_TypeArg v_ConstArg }
 
 class t_Trait (v_Self: Type0) (v_TypeArg: Type0) (v_ConstArg: usize) = {
-  [@@@ FStar.Tactics.Typeclasses.no_method]_super_4726684624731801277:Core.Marker.t_MetaSized v_Self;
   f_method_pre:
       #v_MethodTypeArg: Type0 ->
       v_MethodConstArg: usize ->
@@ -443,7 +425,6 @@ let associated_function_caller
   ()
 
 class t_SubTrait (v_Self: Type0) (v_TypeArg: Type0) (v_ConstArg: usize) = {
-  [@@@ FStar.Tactics.Typeclasses.no_method]_super_4726684624731801277:Core.Marker.t_MetaSized v_Self;
   [@@@ FStar.Tactics.Typeclasses.no_method]_super_15145771689388873921:t_Trait v_Self
     v_TypeArg
     v_ConstArg;
@@ -461,7 +442,6 @@ type t_Bar (v_FooConst: usize) (v_FooType: Type0) =
   | Bar : t_Array v_FooType v_FooConst -> t_Bar v_FooConst v_FooType
 
 class t_Foo (v_Self: Type0) (v_FooConst: usize) (v_FooType: Type0) = {
-  [@@@ FStar.Tactics.Typeclasses.no_method]_super_4726684624731801277:Core.Marker.t_MetaSized v_Self;
   f_fun_pre:
       v_FunConst: usize ->
       #v_FunType: Type0 ->
@@ -525,13 +505,11 @@ open Core
 open FStar.Mul
 
 class t_Trait1 (v_Self: Type0) = {
-  [@@@ FStar.Tactics.Typeclasses.no_method]_super_4726684624731801277:Core.Marker.t_MetaSized v_Self;
   f_T:Type0;
   f_T_7969211799618487585:t_Trait1 f_T
 }
 
 class t_Trait2 (v_Self: Type0) = {
-  [@@@ FStar.Tactics.Typeclasses.no_method]_super_4726684624731801277:Core.Marker.t_MetaSized v_Self;
   [@@@ FStar.Tactics.Typeclasses.no_method]_super_3259985701465885527:t_Trait1 v_Self;
   f_U:Type0
 }
@@ -552,7 +530,6 @@ open Core
 open FStar.Mul
 
 class t_PolyOp (v_Self: Type0) = {
-  [@@@ FStar.Tactics.Typeclasses.no_method]_super_4726684624731801277:Core.Marker.t_MetaSized v_Self;
   f_op_pre:u32 -> u32 -> Type0;
   f_op_post:u32 -> u32 -> u32 -> Type0;
   f_op:x0: u32 -> x1: u32 -> Prims.Pure u32 (f_op_pre x0 x1) (fun result -> f_op_post x0 x1 result)
@@ -590,7 +567,6 @@ open Core
 open FStar.Mul
 
 class t_SuperTrait (v_Self: Type0) = {
-  [@@@ FStar.Tactics.Typeclasses.no_method]_super_4726684624731801277:Core.Marker.t_MetaSized v_Self;
   [@@@ FStar.Tactics.Typeclasses.no_method]_super_15837849249852401974:Core.Clone.t_Clone v_Self;
   f_function_of_super_trait_pre:v_Self -> Type0;
   f_function_of_super_trait_post:v_Self -> u32 -> Type0;
@@ -612,7 +588,6 @@ let impl: t_SuperTrait i32 =
 type t_Struct = | Struct : t_Struct
 
 class t_Bar (v_Self: Type0) = {
-  [@@@ FStar.Tactics.Typeclasses.no_method]_super_4726684624731801277:Core.Marker.t_MetaSized v_Self;
   f_bar_pre:v_Self -> Type0;
   f_bar_post:v_Self -> Prims.unit -> Type0;
   f_bar:x0: v_Self -> Prims.Pure Prims.unit (f_bar_pre x0) (fun result -> f_bar_post x0 result)
@@ -675,7 +650,6 @@ let uuse_iimpl_trait (_: Prims.unit) : Prims.unit =
   ()
 
 class t_Foo (v_Self: Type0) = {
-  [@@@ FStar.Tactics.Typeclasses.no_method]_super_4726684624731801277:Core.Marker.t_MetaSized v_Self;
   f_AssocType:Type0;
   f_AssocType_1162045947544099865:t_SuperTrait f_AssocType;
   f_N:usize;

From 5a331fd267fc566e024530738a68adaf7c6dd3d6 Mon Sep 17 00:00:00 2001
From: Lucas Franceschino <lucas@cryspen.com>
Date: Thu, 3 Jul 2025 13:01:15 +0200
Subject: [PATCH 05/18] chore(proof-libs): impl disambugator change because of
 rustc

---
 .../proof-libs/coq/coq/generated-core/src/Core_Iter_Range.v   | 4 ++--
 hax-lib/proof-libs/fstar/core/Alloc.Fmt.fsti                  | 2 +-
 hax-lib/proof-libs/fstar/core/Core.Fmt.Rt.fsti                | 2 +-
 3 files changed, 4 insertions(+), 4 deletions(-)

diff --git a/hax-lib/proof-libs/coq/coq/generated-core/src/Core_Iter_Range.v b/hax-lib/proof-libs/coq/coq/generated-core/src/Core_Iter_Range.v
index 64d56e9e3..3bb96d69c 100644
--- a/hax-lib/proof-libs/coq/coq/generated-core/src/Core_Iter_Range.v
+++ b/hax-lib/proof-libs/coq/coq/generated-core/src/Core_Iter_Range.v
@@ -100,7 +100,7 @@ Instance t_RangeIteratorImpl_158276838 `{v_A : Type} `{t_Sized (v_A)} `{t_Step (
   {
     RangeIteratorImpl_impl_f_Item := v_A;
     RangeIteratorImpl_impl_f_spec_next := fun  (self : t_Range ((v_A)))=>
-      let hax_temp_output := never_to_any (panic_fmt (impl_2__new_v1 (["not yet implemented: specification needed"%string]) (impl_1__none (tt)))) in
+      let hax_temp_output := never_to_any (panic_fmt (impl_1__new_v1 (["not yet implemented: specification needed"%string]) (impl_1__none (tt)))) in
       (self,hax_temp_output);
   }.
 
@@ -108,7 +108,7 @@ Instance t_Iterator_416192239 `{v_A : Type} `{t_Sized (v_A)} `{t_Step (v_A)} : t
   {
     Iterator_impl_1_f_Item := v_A;
     Iterator_impl_1_f_next := fun  (self : t_Range ((v_A)))=>
-      let hax_temp_output := never_to_any (panic_fmt (impl_2__new_v1 (["not yet implemented: specification needed"%string]) (impl_1__none (tt)))) in
+      let hax_temp_output := never_to_any (panic_fmt (impl_1__new_v1 (["not yet implemented: specification needed"%string]) (impl_1__none (tt)))) in
       (self,hax_temp_output);
     Iterator_impl_1_f_size_hint := fun  (self : t_Range ((v_A)))=>
       if
diff --git a/hax-lib/proof-libs/fstar/core/Alloc.Fmt.fsti b/hax-lib/proof-libs/fstar/core/Alloc.Fmt.fsti
index 7c0b405af..7668c3a1f 100644
--- a/hax-lib/proof-libs/fstar/core/Alloc.Fmt.fsti
+++ b/hax-lib/proof-libs/fstar/core/Alloc.Fmt.fsti
@@ -3,7 +3,7 @@ open Rust_primitives
 
 include Core.Fmt
 
-val impl_2__new_v1 (sz1:usize) (sz2: usize) (pieces: t_Slice string) (args: Core.Fmt.Rt.t_Argument): t_Arguments
+val impl_1__new_v1 (sz1:usize) (sz2: usize) (pieces: t_Slice string) (args: Core.Fmt.Rt.t_Argument): t_Arguments
 val impl_7__write_fmt (fmt: t_Formatter) (args: t_Arguments): t_Result
 
 val format (args: t_Arguments): string
diff --git a/hax-lib/proof-libs/fstar/core/Core.Fmt.Rt.fsti b/hax-lib/proof-libs/fstar/core/Core.Fmt.Rt.fsti
index f9952dcd2..e059ea523 100644
--- a/hax-lib/proof-libs/fstar/core/Core.Fmt.Rt.fsti
+++ b/hax-lib/proof-libs/fstar/core/Core.Fmt.Rt.fsti
@@ -8,7 +8,7 @@ val impl_4__new_v1_formatted (#t:Type0) (x: t) : t_Argument
 val impl_1__new_binary (#t:Type0) (x: t) : t_Argument
 val impl_1__new_lower_hex (#t:Type0) (x: t) : t_Argument
 val impl_2__new_const (#t:Type0) (#u:Type0) (xconst: t) (yconst: u): t_Argument
-val impl_2__new_v1 (#t1:Type0) (#t2:Type0) (#t3:Type0) (#t4:Type0) 
+val impl_1__new_v1 (#t1:Type0) (#t2:Type0) (#t3:Type0) (#t4:Type0) 
   (x1: t1) (x2: t2) (x3: t3) (x4: t4) : t_Argument
 val impl__new_display (#t:Type0) (x: t): t_Argument
 val impl__new_debug (#t:Type0) (x: t): t_Argument

From 0fd5b75f84dd0d3879bdb18ea6020e410366c436 Mon Sep 17 00:00:00 2001
From: Lucas Franceschino <lucas@cryspen.com>
Date: Thu, 3 Jul 2025 13:06:36 +0200
Subject: [PATCH 06/18] chore(proof-libs): impl disambugator change because of
 rustc

---
 hax-lib/proof-libs/fstar/core/Core.Fmt.Rt.fsti | 2 +-
 1 file changed, 1 insertion(+), 1 deletion(-)

diff --git a/hax-lib/proof-libs/fstar/core/Core.Fmt.Rt.fsti b/hax-lib/proof-libs/fstar/core/Core.Fmt.Rt.fsti
index e059ea523..cab57d432 100644
--- a/hax-lib/proof-libs/fstar/core/Core.Fmt.Rt.fsti
+++ b/hax-lib/proof-libs/fstar/core/Core.Fmt.Rt.fsti
@@ -7,7 +7,7 @@ val impl_1__new_debug (#t:Type0) (x: t): t_Argument
 val impl_4__new_v1_formatted (#t:Type0) (x: t) : t_Argument
 val impl_1__new_binary (#t:Type0) (x: t) : t_Argument
 val impl_1__new_lower_hex (#t:Type0) (x: t) : t_Argument
-val impl_2__new_const (#t:Type0) (#u:Type0) (xconst: t) (yconst: u): t_Argument
+val impl_1__new_const (#t:Type0) (#u:Type0) (xconst: t) (yconst: u): t_Argument
 val impl_1__new_v1 (#t1:Type0) (#t2:Type0) (#t3:Type0) (#t4:Type0) 
   (x1: t1) (x2: t2) (x3: t3) (x4: t4) : t_Argument
 val impl__new_display (#t:Type0) (x: t): t_Argument

From 8379bd1f7f74b92fc74a73478cdbb458f6fbb0b3 Mon Sep 17 00:00:00 2001
From: Lucas Franceschino <lucas@cryspen.com>
Date: Thu, 3 Jul 2025 13:17:04 +0200
Subject: [PATCH 07/18] chore(rustc-tests): update snapshots

---
 .../snapshots/fstar/Coverage.Abort.fst        |  6 +-
 .../snapshots/fstar/Coverage.Assert.fst       | 11 ++--
 .../Coverage.Attr.Trait_impl_inherit.fst      |  4 +-
 .../fstar/Coverage.Auxiliary.Used_crate.fst   | 55 ++++++++++++-------
 .../Coverage.Auxiliary.Used_inline_crate.fst  | 55 ++++++++++++-------
 .../fstar/Coverage.Closure_macro.fst          | 40 ++++++--------
 .../snapshots/fstar/Coverage.Conditions.fst   | 24 ++++----
 .../snapshots/fstar/Coverage.Drop_trait.fst   | 15 ++---
 .../snapshots/fstar/Coverage.Generics.fst     | 15 ++---
 .../snapshots/fstar/Coverage.If_not.fst       |  8 +--
 .../snapshots/fstar/Coverage.Inline.fst       |  6 +-
 .../snapshots/fstar/Coverage.Inline_dead.fst  | 13 +++--
 .../snapshots/fstar/Coverage.Inner_items.fst  | 11 ++--
 .../snapshots/fstar/Coverage.Issue_83601_.fst | 39 +++++++------
 .../fstar/Coverage.Loops_branches.fst         | 38 +++++++------
 .../fstar/Coverage.Macro_in_closure.fst       |  4 +-
 .../Coverage.No_cov_crate.Nested_fns.fst      | 18 +++---
 .../snapshots/fstar/Coverage.No_cov_crate.fst | 12 ++--
 .../snapshots/fstar/Coverage.Overflow.fst     | 49 +++++++++--------
 .../snapshots/fstar/Coverage.Panic_unwind.fst |  6 +-
 .../snapshots/fstar/Coverage.Partial_eq.fst   | 43 ++++++++-------
 .../snapshots/fstar/Coverage.Sort_groups.fst  | 17 +++---
 .../Coverage.Unused_mod.Unused_module.fst     |  2 +-
 .../snapshots/fstar/Coverage.Unused_mod.fst   |  2 +-
 24 files changed, 268 insertions(+), 225 deletions(-)

diff --git a/rustc-coverage-tests/snapshots/fstar/Coverage.Abort.fst b/rustc-coverage-tests/snapshots/fstar/Coverage.Abort.fst
index 2421d61b2..b2199312b 100644
--- a/rustc-coverage-tests/snapshots/fstar/Coverage.Abort.fst
+++ b/rustc-coverage-tests/snapshots/fstar/Coverage.Abort.fst
@@ -7,7 +7,7 @@ let might_abort (should_abort: bool) : Prims.unit =
   if should_abort
   then
     let _:Prims.unit =
-      Std.Io.Stdio.e_print (Core.Fmt.Rt.impl_2__new_const (mk_usize 1)
+      Std.Io.Stdio.e_print (Core.Fmt.Rt.impl_1__new_const (mk_usize 1)
             (let list = ["aborting...\n"] in
               FStar.Pervasives.assert_norm (Prims.eq2 (List.Tot.length list) 1);
               Rust_primitives.Hax.array_of_list 1 list)
@@ -15,7 +15,7 @@ let might_abort (should_abort: bool) : Prims.unit =
           Core.Fmt.t_Arguments)
     in
     let _:Prims.unit = () in
-    Rust_primitives.Hax.never_to_any (Core.Panicking.panic_fmt (Core.Fmt.Rt.impl_2__new_const (mk_usize
+    Rust_primitives.Hax.never_to_any (Core.Panicking.panic_fmt (Core.Fmt.Rt.impl_1__new_const (mk_usize
                 1)
               (let list = ["panics and aborts"] in
                 FStar.Pervasives.assert_norm (Prims.eq2 (List.Tot.length list) 1);
@@ -26,7 +26,7 @@ let might_abort (should_abort: bool) : Prims.unit =
         Rust_primitives.Hax.t_Never)
   else
     let _:Prims.unit =
-      Std.Io.Stdio.e_print (Core.Fmt.Rt.impl_2__new_const (mk_usize 1)
+      Std.Io.Stdio.e_print (Core.Fmt.Rt.impl_1__new_const (mk_usize 1)
             (let list = ["Don't Panic\n"] in
               FStar.Pervasives.assert_norm (Prims.eq2 (List.Tot.length list) 1);
               Rust_primitives.Hax.array_of_list 1 list)
diff --git a/rustc-coverage-tests/snapshots/fstar/Coverage.Assert.fst b/rustc-coverage-tests/snapshots/fstar/Coverage.Assert.fst
index 25c0595e5..bf0e5af85 100644
--- a/rustc-coverage-tests/snapshots/fstar/Coverage.Assert.fst
+++ b/rustc-coverage-tests/snapshots/fstar/Coverage.Assert.fst
@@ -4,15 +4,18 @@ open Core
 open FStar.Mul
 
 let might_fail_assert (one_plus_one: u32) : Prims.unit =
+  let args:t_Array Core.Fmt.Rt.t_Argument (mk_usize 1) =
+    let list = [Core.Fmt.Rt.impl__new_display #u32 one_plus_one] in
+    FStar.Pervasives.assert_norm (Prims.eq2 (List.Tot.length list) 1);
+    Rust_primitives.Hax.array_of_list 1 list
+  in
   let _:Prims.unit =
-    Std.Io.Stdio.e_print (Core.Fmt.Rt.impl_2__new_v1 (mk_usize 2)
+    Std.Io.Stdio.e_print (Core.Fmt.Rt.impl_1__new_v1 (mk_usize 2)
           (mk_usize 1)
           (let list = ["does 1 + 1 = "; "?\n"] in
             FStar.Pervasives.assert_norm (Prims.eq2 (List.Tot.length list) 2);
             Rust_primitives.Hax.array_of_list 2 list)
-          (let list = [Core.Fmt.Rt.impl__new_display #u32 one_plus_one <: Core.Fmt.Rt.t_Argument] in
-            FStar.Pervasives.assert_norm (Prims.eq2 (List.Tot.length list) 1);
-            Rust_primitives.Hax.array_of_list 1 list)
+          args
         <:
         Core.Fmt.t_Arguments)
   in
diff --git a/rustc-coverage-tests/snapshots/fstar/Coverage.Attr.Trait_impl_inherit.fst b/rustc-coverage-tests/snapshots/fstar/Coverage.Attr.Trait_impl_inherit.fst
index 04356340f..ba2090ae0 100644
--- a/rustc-coverage-tests/snapshots/fstar/Coverage.Attr.Trait_impl_inherit.fst
+++ b/rustc-coverage-tests/snapshots/fstar/Coverage.Attr.Trait_impl_inherit.fst
@@ -7,7 +7,7 @@ open FStar.Mul
 Last available AST for this item:
 
 #[path()]#[<cfg>(any(feature = "json"))]#[feature(coverage_attribute)]#[<cfg>(any(feature = "json", feature = "fstar", feature = "fstar-lax", feature =
-"coq"))]#[feature(coverage_attribute)]#[allow(unused_attributes)]#[allow(dead_code)]#[allow(unreachable_code)]#[feature(register_tool)]#[register_tool(_hax)]trait t_T<Self_>{fn f_f((self: Self)) -> tuple0{{let _: tuple0 = {std::io::stdio::e_print(core::fmt::rt::impl_2__new_const::<generic_value!(todo)>(["default\n"]))};{let _: tuple0 = {Tuple0};Tuple0}}}}
+"coq"))]#[feature(coverage_attribute)]#[allow(unused_attributes)]#[allow(dead_code)]#[allow(unreachable_code)]#[feature(register_tool)]#[register_tool(_hax)]trait t_T<Self_>{fn f_f((self: Self)) -> tuple0{{let _: tuple0 = {std::io::stdio::e_print(core::fmt::rt::impl_1__new_const::<generic_value!(todo)>(["default\n"]))};{let _: tuple0 = {Tuple0};Tuple0}}}}
 
 Last AST:
 /** print_rust: pitem: not implemented  (item: { Concrete_ident.T.def_id =
@@ -74,7 +74,7 @@ let impl: t_T t_S =
     =
     fun (self: t_S) ->
       let _:Prims.unit =
-        Std.Io.Stdio.e_print (Core.Fmt.Rt.impl_2__new_const (mk_usize 1)
+        Std.Io.Stdio.e_print (Core.Fmt.Rt.impl_1__new_const (mk_usize 1)
               (let list = ["impl S\n"] in
                 FStar.Pervasives.assert_norm (Prims.eq2 (List.Tot.length list) 1);
                 Rust_primitives.Hax.array_of_list 1 list)
diff --git a/rustc-coverage-tests/snapshots/fstar/Coverage.Auxiliary.Used_crate.fst b/rustc-coverage-tests/snapshots/fstar/Coverage.Auxiliary.Used_crate.fst
index 1d226b104..1afbf88e4 100644
--- a/rustc-coverage-tests/snapshots/fstar/Coverage.Auxiliary.Used_crate.fst
+++ b/rustc-coverage-tests/snapshots/fstar/Coverage.Auxiliary.Used_crate.fst
@@ -14,15 +14,18 @@ let used_only_from_bin_crate_generic_function
       (#[FStar.Tactics.Typeclasses.tcresolve ()] i1: Core.Fmt.t_Debug v_T)
       (arg: v_T)
     : Prims.unit =
+  let args:t_Array Core.Fmt.Rt.t_Argument (mk_usize 1) =
+    let list = [Core.Fmt.Rt.impl__new_debug #v_T arg] in
+    FStar.Pervasives.assert_norm (Prims.eq2 (List.Tot.length list) 1);
+    Rust_primitives.Hax.array_of_list 1 list
+  in
   let _:Prims.unit =
-    Std.Io.Stdio.e_print (Core.Fmt.Rt.impl_2__new_v1 (mk_usize 2)
+    Std.Io.Stdio.e_print (Core.Fmt.Rt.impl_1__new_v1 (mk_usize 2)
           (mk_usize 1)
           (let list = ["used_only_from_bin_crate_generic_function with "; "\n"] in
             FStar.Pervasives.assert_norm (Prims.eq2 (List.Tot.length list) 2);
             Rust_primitives.Hax.array_of_list 2 list)
-          (let list = [Core.Fmt.Rt.impl__new_debug #v_T arg <: Core.Fmt.Rt.t_Argument] in
-            FStar.Pervasives.assert_norm (Prims.eq2 (List.Tot.length list) 1);
-            Rust_primitives.Hax.array_of_list 1 list)
+          args
         <:
         Core.Fmt.t_Arguments)
   in
@@ -34,15 +37,18 @@ let used_only_from_this_lib_crate_generic_function
       (#[FStar.Tactics.Typeclasses.tcresolve ()] i1: Core.Fmt.t_Debug v_T)
       (arg: v_T)
     : Prims.unit =
+  let args:t_Array Core.Fmt.Rt.t_Argument (mk_usize 1) =
+    let list = [Core.Fmt.Rt.impl__new_debug #v_T arg] in
+    FStar.Pervasives.assert_norm (Prims.eq2 (List.Tot.length list) 1);
+    Rust_primitives.Hax.array_of_list 1 list
+  in
   let _:Prims.unit =
-    Std.Io.Stdio.e_print (Core.Fmt.Rt.impl_2__new_v1 (mk_usize 2)
+    Std.Io.Stdio.e_print (Core.Fmt.Rt.impl_1__new_v1 (mk_usize 2)
           (mk_usize 1)
           (let list = ["used_only_from_this_lib_crate_generic_function with "; "\n"] in
             FStar.Pervasives.assert_norm (Prims.eq2 (List.Tot.length list) 2);
             Rust_primitives.Hax.array_of_list 2 list)
-          (let list = [Core.Fmt.Rt.impl__new_debug #v_T arg <: Core.Fmt.Rt.t_Argument] in
-            FStar.Pervasives.assert_norm (Prims.eq2 (List.Tot.length list) 1);
-            Rust_primitives.Hax.array_of_list 1 list)
+          args
         <:
         Core.Fmt.t_Arguments)
   in
@@ -54,15 +60,18 @@ let used_from_bin_crate_and_lib_crate_generic_function
       (#[FStar.Tactics.Typeclasses.tcresolve ()] i1: Core.Fmt.t_Debug v_T)
       (arg: v_T)
     : Prims.unit =
+  let args:t_Array Core.Fmt.Rt.t_Argument (mk_usize 1) =
+    let list = [Core.Fmt.Rt.impl__new_debug #v_T arg] in
+    FStar.Pervasives.assert_norm (Prims.eq2 (List.Tot.length list) 1);
+    Rust_primitives.Hax.array_of_list 1 list
+  in
   let _:Prims.unit =
-    Std.Io.Stdio.e_print (Core.Fmt.Rt.impl_2__new_v1 (mk_usize 2)
+    Std.Io.Stdio.e_print (Core.Fmt.Rt.impl_1__new_v1 (mk_usize 2)
           (mk_usize 1)
           (let list = ["used_from_bin_crate_and_lib_crate_generic_function with "; "\n"] in
             FStar.Pervasives.assert_norm (Prims.eq2 (List.Tot.length list) 2);
             Rust_primitives.Hax.array_of_list 2 list)
-          (let list = [Core.Fmt.Rt.impl__new_debug #v_T arg <: Core.Fmt.Rt.t_Argument] in
-            FStar.Pervasives.assert_norm (Prims.eq2 (List.Tot.length list) 1);
-            Rust_primitives.Hax.array_of_list 1 list)
+          args
         <:
         Core.Fmt.t_Arguments)
   in
@@ -74,17 +83,20 @@ let used_with_same_type_from_bin_crate_and_lib_crate_generic_function
       (#[FStar.Tactics.Typeclasses.tcresolve ()] i1: Core.Fmt.t_Debug v_T)
       (arg: v_T)
     : Prims.unit =
+  let args:t_Array Core.Fmt.Rt.t_Argument (mk_usize 1) =
+    let list = [Core.Fmt.Rt.impl__new_debug #v_T arg] in
+    FStar.Pervasives.assert_norm (Prims.eq2 (List.Tot.length list) 1);
+    Rust_primitives.Hax.array_of_list 1 list
+  in
   let _:Prims.unit =
-    Std.Io.Stdio.e_print (Core.Fmt.Rt.impl_2__new_v1 (mk_usize 2)
+    Std.Io.Stdio.e_print (Core.Fmt.Rt.impl_1__new_v1 (mk_usize 2)
           (mk_usize 1)
           (let list =
               ["used_with_same_type_from_bin_crate_and_lib_crate_generic_function with "; "\n"]
             in
             FStar.Pervasives.assert_norm (Prims.eq2 (List.Tot.length list) 2);
             Rust_primitives.Hax.array_of_list 2 list)
-          (let list = [Core.Fmt.Rt.impl__new_debug #v_T arg <: Core.Fmt.Rt.t_Argument] in
-            FStar.Pervasives.assert_norm (Prims.eq2 (List.Tot.length list) 1);
-            Rust_primitives.Hax.array_of_list 1 list)
+          args
         <:
         Core.Fmt.t_Arguments)
   in
@@ -96,15 +108,18 @@ let unused_generic_function
       (#[FStar.Tactics.Typeclasses.tcresolve ()] i1: Core.Fmt.t_Debug v_T)
       (arg: v_T)
     : Prims.unit =
+  let args:t_Array Core.Fmt.Rt.t_Argument (mk_usize 1) =
+    let list = [Core.Fmt.Rt.impl__new_debug #v_T arg] in
+    FStar.Pervasives.assert_norm (Prims.eq2 (List.Tot.length list) 1);
+    Rust_primitives.Hax.array_of_list 1 list
+  in
   let _:Prims.unit =
-    Std.Io.Stdio.e_print (Core.Fmt.Rt.impl_2__new_v1 (mk_usize 2)
+    Std.Io.Stdio.e_print (Core.Fmt.Rt.impl_1__new_v1 (mk_usize 2)
           (mk_usize 1)
           (let list = ["unused_generic_function with "; "\n"] in
             FStar.Pervasives.assert_norm (Prims.eq2 (List.Tot.length list) 2);
             Rust_primitives.Hax.array_of_list 2 list)
-          (let list = [Core.Fmt.Rt.impl__new_debug #v_T arg <: Core.Fmt.Rt.t_Argument] in
-            FStar.Pervasives.assert_norm (Prims.eq2 (List.Tot.length list) 1);
-            Rust_primitives.Hax.array_of_list 1 list)
+          args
         <:
         Core.Fmt.t_Arguments)
   in
diff --git a/rustc-coverage-tests/snapshots/fstar/Coverage.Auxiliary.Used_inline_crate.fst b/rustc-coverage-tests/snapshots/fstar/Coverage.Auxiliary.Used_inline_crate.fst
index 00520c6fd..7d7aa2ce2 100644
--- a/rustc-coverage-tests/snapshots/fstar/Coverage.Auxiliary.Used_inline_crate.fst
+++ b/rustc-coverage-tests/snapshots/fstar/Coverage.Auxiliary.Used_inline_crate.fst
@@ -14,15 +14,18 @@ let used_only_from_bin_crate_generic_function
       (#[FStar.Tactics.Typeclasses.tcresolve ()] i1: Core.Fmt.t_Debug v_T)
       (arg: v_T)
     : Prims.unit =
+  let args:t_Array Core.Fmt.Rt.t_Argument (mk_usize 1) =
+    let list = [Core.Fmt.Rt.impl__new_debug #v_T arg] in
+    FStar.Pervasives.assert_norm (Prims.eq2 (List.Tot.length list) 1);
+    Rust_primitives.Hax.array_of_list 1 list
+  in
   let _:Prims.unit =
-    Std.Io.Stdio.e_print (Core.Fmt.Rt.impl_2__new_v1 (mk_usize 2)
+    Std.Io.Stdio.e_print (Core.Fmt.Rt.impl_1__new_v1 (mk_usize 2)
           (mk_usize 1)
           (let list = ["used_only_from_bin_crate_generic_function with "; "\n"] in
             FStar.Pervasives.assert_norm (Prims.eq2 (List.Tot.length list) 2);
             Rust_primitives.Hax.array_of_list 2 list)
-          (let list = [Core.Fmt.Rt.impl__new_debug #v_T arg <: Core.Fmt.Rt.t_Argument] in
-            FStar.Pervasives.assert_norm (Prims.eq2 (List.Tot.length list) 1);
-            Rust_primitives.Hax.array_of_list 1 list)
+          args
         <:
         Core.Fmt.t_Arguments)
   in
@@ -34,15 +37,18 @@ let used_only_from_this_lib_crate_generic_function
       (#[FStar.Tactics.Typeclasses.tcresolve ()] i1: Core.Fmt.t_Debug v_T)
       (arg: v_T)
     : Prims.unit =
+  let args:t_Array Core.Fmt.Rt.t_Argument (mk_usize 1) =
+    let list = [Core.Fmt.Rt.impl__new_debug #v_T arg] in
+    FStar.Pervasives.assert_norm (Prims.eq2 (List.Tot.length list) 1);
+    Rust_primitives.Hax.array_of_list 1 list
+  in
   let _:Prims.unit =
-    Std.Io.Stdio.e_print (Core.Fmt.Rt.impl_2__new_v1 (mk_usize 2)
+    Std.Io.Stdio.e_print (Core.Fmt.Rt.impl_1__new_v1 (mk_usize 2)
           (mk_usize 1)
           (let list = ["used_only_from_this_lib_crate_generic_function with "; "\n"] in
             FStar.Pervasives.assert_norm (Prims.eq2 (List.Tot.length list) 2);
             Rust_primitives.Hax.array_of_list 2 list)
-          (let list = [Core.Fmt.Rt.impl__new_debug #v_T arg <: Core.Fmt.Rt.t_Argument] in
-            FStar.Pervasives.assert_norm (Prims.eq2 (List.Tot.length list) 1);
-            Rust_primitives.Hax.array_of_list 1 list)
+          args
         <:
         Core.Fmt.t_Arguments)
   in
@@ -54,15 +60,18 @@ let used_from_bin_crate_and_lib_crate_generic_function
       (#[FStar.Tactics.Typeclasses.tcresolve ()] i1: Core.Fmt.t_Debug v_T)
       (arg: v_T)
     : Prims.unit =
+  let args:t_Array Core.Fmt.Rt.t_Argument (mk_usize 1) =
+    let list = [Core.Fmt.Rt.impl__new_debug #v_T arg] in
+    FStar.Pervasives.assert_norm (Prims.eq2 (List.Tot.length list) 1);
+    Rust_primitives.Hax.array_of_list 1 list
+  in
   let _:Prims.unit =
-    Std.Io.Stdio.e_print (Core.Fmt.Rt.impl_2__new_v1 (mk_usize 2)
+    Std.Io.Stdio.e_print (Core.Fmt.Rt.impl_1__new_v1 (mk_usize 2)
           (mk_usize 1)
           (let list = ["used_from_bin_crate_and_lib_crate_generic_function with "; "\n"] in
             FStar.Pervasives.assert_norm (Prims.eq2 (List.Tot.length list) 2);
             Rust_primitives.Hax.array_of_list 2 list)
-          (let list = [Core.Fmt.Rt.impl__new_debug #v_T arg <: Core.Fmt.Rt.t_Argument] in
-            FStar.Pervasives.assert_norm (Prims.eq2 (List.Tot.length list) 1);
-            Rust_primitives.Hax.array_of_list 1 list)
+          args
         <:
         Core.Fmt.t_Arguments)
   in
@@ -74,17 +83,20 @@ let used_with_same_type_from_bin_crate_and_lib_crate_generic_function
       (#[FStar.Tactics.Typeclasses.tcresolve ()] i1: Core.Fmt.t_Debug v_T)
       (arg: v_T)
     : Prims.unit =
+  let args:t_Array Core.Fmt.Rt.t_Argument (mk_usize 1) =
+    let list = [Core.Fmt.Rt.impl__new_debug #v_T arg] in
+    FStar.Pervasives.assert_norm (Prims.eq2 (List.Tot.length list) 1);
+    Rust_primitives.Hax.array_of_list 1 list
+  in
   let _:Prims.unit =
-    Std.Io.Stdio.e_print (Core.Fmt.Rt.impl_2__new_v1 (mk_usize 2)
+    Std.Io.Stdio.e_print (Core.Fmt.Rt.impl_1__new_v1 (mk_usize 2)
           (mk_usize 1)
           (let list =
               ["used_with_same_type_from_bin_crate_and_lib_crate_generic_function with "; "\n"]
             in
             FStar.Pervasives.assert_norm (Prims.eq2 (List.Tot.length list) 2);
             Rust_primitives.Hax.array_of_list 2 list)
-          (let list = [Core.Fmt.Rt.impl__new_debug #v_T arg <: Core.Fmt.Rt.t_Argument] in
-            FStar.Pervasives.assert_norm (Prims.eq2 (List.Tot.length list) 1);
-            Rust_primitives.Hax.array_of_list 1 list)
+          args
         <:
         Core.Fmt.t_Arguments)
   in
@@ -96,15 +108,18 @@ let unused_generic_function
       (#[FStar.Tactics.Typeclasses.tcresolve ()] i1: Core.Fmt.t_Debug v_T)
       (arg: v_T)
     : Prims.unit =
+  let args:t_Array Core.Fmt.Rt.t_Argument (mk_usize 1) =
+    let list = [Core.Fmt.Rt.impl__new_debug #v_T arg] in
+    FStar.Pervasives.assert_norm (Prims.eq2 (List.Tot.length list) 1);
+    Rust_primitives.Hax.array_of_list 1 list
+  in
   let _:Prims.unit =
-    Std.Io.Stdio.e_print (Core.Fmt.Rt.impl_2__new_v1 (mk_usize 2)
+    Std.Io.Stdio.e_print (Core.Fmt.Rt.impl_1__new_v1 (mk_usize 2)
           (mk_usize 1)
           (let list = ["unused_generic_function with "; "\n"] in
             FStar.Pervasives.assert_norm (Prims.eq2 (List.Tot.length list) 2);
             Rust_primitives.Hax.array_of_list 2 list)
-          (let list = [Core.Fmt.Rt.impl__new_debug #v_T arg <: Core.Fmt.Rt.t_Argument] in
-            FStar.Pervasives.assert_norm (Prims.eq2 (List.Tot.length list) 1);
-            Rust_primitives.Hax.array_of_list 1 list)
+          args
         <:
         Core.Fmt.t_Arguments)
   in
diff --git a/rustc-coverage-tests/snapshots/fstar/Coverage.Closure_macro.fst b/rustc-coverage-tests/snapshots/fstar/Coverage.Closure_macro.fst
index 93864eac0..dc9cacaf3 100644
--- a/rustc-coverage-tests/snapshots/fstar/Coverage.Closure_macro.fst
+++ b/rustc-coverage-tests/snapshots/fstar/Coverage.Closure_macro.fst
@@ -12,7 +12,7 @@ let load_configuration_files (_: Prims.unit)
 
 let main (_: Prims.unit) : Core.Result.t_Result Prims.unit Alloc.String.t_String =
   let _:Prims.unit =
-    Std.Io.Stdio.e_print (Core.Fmt.Rt.impl_2__new_const (mk_usize 1)
+    Std.Io.Stdio.e_print (Core.Fmt.Rt.impl_1__new_const (mk_usize 1)
           (let list = ["Starting service\n"] in
             FStar.Pervasives.assert_norm (Prims.eq2 (List.Tot.length list) 1);
             Rust_primitives.Hax.array_of_list 1 list)
@@ -29,22 +29,19 @@ let main (_: Prims.unit) : Core.Result.t_Result Prims.unit Alloc.String.t_String
         Core.Result.t_Result Alloc.String.t_String Alloc.String.t_String)
       (fun e ->
           let e:Alloc.String.t_String = e in
+          let args:t_Array Core.Fmt.Rt.t_Argument (mk_usize 1) =
+            let list = [Core.Fmt.Rt.impl__new_display #Alloc.String.t_String e] in
+            FStar.Pervasives.assert_norm (Prims.eq2 (List.Tot.length list) 1);
+            Rust_primitives.Hax.array_of_list 1 list
+          in
           let message:Alloc.String.t_String =
             Core.Hint.must_use #Alloc.String.t_String
-              (Alloc.Fmt.format (Core.Fmt.Rt.impl_2__new_v1 (mk_usize 1)
+              (Alloc.Fmt.format (Core.Fmt.Rt.impl_1__new_v1 (mk_usize 1)
                       (mk_usize 1)
                       (let list = ["Error loading configs: "] in
                         FStar.Pervasives.assert_norm (Prims.eq2 (List.Tot.length list) 1);
                         Rust_primitives.Hax.array_of_list 1 list)
-                      (let list =
-                          [
-                            Core.Fmt.Rt.impl__new_display #Alloc.String.t_String e
-                            <:
-                            Core.Fmt.Rt.t_Argument
-                          ]
-                        in
-                        FStar.Pervasives.assert_norm (Prims.eq2 (List.Tot.length list) 1);
-                        Rust_primitives.Hax.array_of_list 1 list)
+                      args
                     <:
                     Core.Fmt.t_Arguments)
                 <:
@@ -52,21 +49,18 @@ let main (_: Prims.unit) : Core.Result.t_Result Prims.unit Alloc.String.t_String
           in
           if (Alloc.String.impl_String__len message <: usize) >. mk_usize 0
           then
+            let args:t_Array Core.Fmt.Rt.t_Argument (mk_usize 1) =
+              let list = [Core.Fmt.Rt.impl__new_display #Alloc.String.t_String message] in
+              FStar.Pervasives.assert_norm (Prims.eq2 (List.Tot.length list) 1);
+              Rust_primitives.Hax.array_of_list 1 list
+            in
             let _:Prims.unit =
-              Std.Io.Stdio.e_print (Core.Fmt.Rt.impl_2__new_v1 (mk_usize 2)
+              Std.Io.Stdio.e_print (Core.Fmt.Rt.impl_1__new_v1 (mk_usize 2)
                     (mk_usize 1)
                     (let list = [""; "\n"] in
                       FStar.Pervasives.assert_norm (Prims.eq2 (List.Tot.length list) 2);
                       Rust_primitives.Hax.array_of_list 2 list)
-                    (let list =
-                        [
-                          Core.Fmt.Rt.impl__new_display #Alloc.String.t_String message
-                          <:
-                          Core.Fmt.Rt.t_Argument
-                        ]
-                      in
-                      FStar.Pervasives.assert_norm (Prims.eq2 (List.Tot.length list) 1);
-                      Rust_primitives.Hax.array_of_list 1 list)
+                    args
                   <:
                   Core.Fmt.t_Arguments)
             in
@@ -83,7 +77,7 @@ let main (_: Prims.unit) : Core.Result.t_Result Prims.unit Alloc.String.t_String
               if (Core.Str.impl_str__len "error" <: usize) >. mk_usize 0
               then
                 let _:Prims.unit =
-                  Std.Io.Stdio.e_print (Core.Fmt.Rt.impl_2__new_const (mk_usize 1)
+                  Std.Io.Stdio.e_print (Core.Fmt.Rt.impl_1__new_const (mk_usize 1)
                         (let list = ["no msg\n"] in
                           FStar.Pervasives.assert_norm (Prims.eq2 (List.Tot.length list) 1);
                           Rust_primitives.Hax.array_of_list 1 list)
@@ -94,7 +88,7 @@ let main (_: Prims.unit) : Core.Result.t_Result Prims.unit Alloc.String.t_String
                 ()
               else
                 let _:Prims.unit =
-                  Std.Io.Stdio.e_print (Core.Fmt.Rt.impl_2__new_const (mk_usize 1)
+                  Std.Io.Stdio.e_print (Core.Fmt.Rt.impl_1__new_const (mk_usize 1)
                         (let list = ["error\n"] in
                           FStar.Pervasives.assert_norm (Prims.eq2 (List.Tot.length list) 1);
                           Rust_primitives.Hax.array_of_list 1 list)
diff --git a/rustc-coverage-tests/snapshots/fstar/Coverage.Conditions.fst b/rustc-coverage-tests/snapshots/fstar/Coverage.Conditions.fst
index f60d96438..2e60b95a5 100644
--- a/rustc-coverage-tests/snapshots/fstar/Coverage.Conditions.fst
+++ b/rustc-coverage-tests/snapshots/fstar/Coverage.Conditions.fst
@@ -105,7 +105,7 @@ let main (_: Prims.unit) : Prims.unit =
             else
               let should_be_reachable:i32 = countdown in
               let _:Prims.unit =
-                Std.Io.Stdio.e_print (Core.Fmt.Rt.impl_2__new_const (mk_usize 1)
+                Std.Io.Stdio.e_print (Core.Fmt.Rt.impl_1__new_const (mk_usize 1)
                       (let list = ["reached\n"] in
                         FStar.Pervasives.assert_norm (Prims.eq2 (List.Tot.length list) 1);
                         Rust_primitives.Hax.array_of_list 1 list)
@@ -188,7 +188,7 @@ let main (_: Prims.unit) : Prims.unit =
               else
                 let should_be_reachable:i32 = countdown in
                 let _:Prims.unit =
-                  Std.Io.Stdio.e_print (Core.Fmt.Rt.impl_2__new_const (mk_usize 1)
+                  Std.Io.Stdio.e_print (Core.Fmt.Rt.impl_1__new_const (mk_usize 1)
                         (let list = ["reached\n"] in
                           FStar.Pervasives.assert_norm (Prims.eq2 (List.Tot.length list) 1);
                           Rust_primitives.Hax.array_of_list 1 list)
@@ -261,7 +261,7 @@ let main (_: Prims.unit) : Prims.unit =
           else
             let should_be_reachable:i32 = countdown in
             let _:Prims.unit =
-              Std.Io.Stdio.e_print (Core.Fmt.Rt.impl_2__new_const (mk_usize 1)
+              Std.Io.Stdio.e_print (Core.Fmt.Rt.impl_1__new_const (mk_usize 1)
                     (let list = ["reached\n"] in
                       FStar.Pervasives.assert_norm (Prims.eq2 (List.Tot.length list) 1);
                       Rust_primitives.Hax.array_of_list 1 list)
@@ -357,7 +357,7 @@ let main (_: Prims.unit) : Prims.unit =
               else
                 let should_be_reachable:i32 = countdown in
                 let _:Prims.unit =
-                  Std.Io.Stdio.e_print (Core.Fmt.Rt.impl_2__new_const (mk_usize 1)
+                  Std.Io.Stdio.e_print (Core.Fmt.Rt.impl_1__new_const (mk_usize 1)
                         (let list = ["reached\n"] in
                           FStar.Pervasives.assert_norm (Prims.eq2 (List.Tot.length list) 1);
                           Rust_primitives.Hax.array_of_list 1 list)
@@ -440,7 +440,7 @@ let main (_: Prims.unit) : Prims.unit =
                 else
                   let should_be_reachable:i32 = countdown in
                   let _:Prims.unit =
-                    Std.Io.Stdio.e_print (Core.Fmt.Rt.impl_2__new_const (mk_usize 1)
+                    Std.Io.Stdio.e_print (Core.Fmt.Rt.impl_1__new_const (mk_usize 1)
                           (let list = ["reached\n"] in
                             FStar.Pervasives.assert_norm (Prims.eq2 (List.Tot.length list) 1);
                             Rust_primitives.Hax.array_of_list 1 list)
@@ -513,7 +513,7 @@ let main (_: Prims.unit) : Prims.unit =
             else
               let should_be_reachable:i32 = countdown in
               let _:Prims.unit =
-                Std.Io.Stdio.e_print (Core.Fmt.Rt.impl_2__new_const (mk_usize 1)
+                Std.Io.Stdio.e_print (Core.Fmt.Rt.impl_1__new_const (mk_usize 1)
                       (let list = ["reached\n"] in
                         FStar.Pervasives.assert_norm (Prims.eq2 (List.Tot.length list) 1);
                         Rust_primitives.Hax.array_of_list 1 list)
@@ -621,7 +621,7 @@ let main (_: Prims.unit) : Prims.unit =
               else
                 let should_be_reachable:i32 = countdown in
                 let _:Prims.unit =
-                  Std.Io.Stdio.e_print (Core.Fmt.Rt.impl_2__new_const (mk_usize 1)
+                  Std.Io.Stdio.e_print (Core.Fmt.Rt.impl_1__new_const (mk_usize 1)
                         (let list = ["reached\n"] in
                           FStar.Pervasives.assert_norm (Prims.eq2 (List.Tot.length list) 1);
                           Rust_primitives.Hax.array_of_list 1 list)
@@ -704,7 +704,7 @@ let main (_: Prims.unit) : Prims.unit =
                 else
                   let should_be_reachable:i32 = countdown in
                   let _:Prims.unit =
-                    Std.Io.Stdio.e_print (Core.Fmt.Rt.impl_2__new_const (mk_usize 1)
+                    Std.Io.Stdio.e_print (Core.Fmt.Rt.impl_1__new_const (mk_usize 1)
                           (let list = ["reached\n"] in
                             FStar.Pervasives.assert_norm (Prims.eq2 (List.Tot.length list) 1);
                             Rust_primitives.Hax.array_of_list 1 list)
@@ -777,7 +777,7 @@ let main (_: Prims.unit) : Prims.unit =
             else
               let should_be_reachable:i32 = countdown in
               let _:Prims.unit =
-                Std.Io.Stdio.e_print (Core.Fmt.Rt.impl_2__new_const (mk_usize 1)
+                Std.Io.Stdio.e_print (Core.Fmt.Rt.impl_1__new_const (mk_usize 1)
                       (let list = ["reached\n"] in
                         FStar.Pervasives.assert_norm (Prims.eq2 (List.Tot.length list) 1);
                         Rust_primitives.Hax.array_of_list 1 list)
@@ -873,7 +873,7 @@ let main (_: Prims.unit) : Prims.unit =
                 else
                   let should_be_reachable:i32 = countdown in
                   let _:Prims.unit =
-                    Std.Io.Stdio.e_print (Core.Fmt.Rt.impl_2__new_const (mk_usize 1)
+                    Std.Io.Stdio.e_print (Core.Fmt.Rt.impl_1__new_const (mk_usize 1)
                           (let list = ["reached\n"] in
                             FStar.Pervasives.assert_norm (Prims.eq2 (List.Tot.length list) 1);
                             Rust_primitives.Hax.array_of_list 1 list)
@@ -957,7 +957,7 @@ let main (_: Prims.unit) : Prims.unit =
                   else
                     let should_be_reachable:i32 = countdown in
                     let _:Prims.unit =
-                      Std.Io.Stdio.e_print (Core.Fmt.Rt.impl_2__new_const (mk_usize 1)
+                      Std.Io.Stdio.e_print (Core.Fmt.Rt.impl_1__new_const (mk_usize 1)
                             (let list = ["reached\n"] in
                               FStar.Pervasives.assert_norm (Prims.eq2 (List.Tot.length list) 1);
                               Rust_primitives.Hax.array_of_list 1 list)
@@ -1030,7 +1030,7 @@ let main (_: Prims.unit) : Prims.unit =
               else
                 let should_be_reachable:i32 = countdown in
                 let _:Prims.unit =
-                  Std.Io.Stdio.e_print (Core.Fmt.Rt.impl_2__new_const (mk_usize 1)
+                  Std.Io.Stdio.e_print (Core.Fmt.Rt.impl_1__new_const (mk_usize 1)
                         (let list = ["reached\n"] in
                           FStar.Pervasives.assert_norm (Prims.eq2 (List.Tot.length list) 1);
                           Rust_primitives.Hax.array_of_list 1 list)
diff --git a/rustc-coverage-tests/snapshots/fstar/Coverage.Drop_trait.fst b/rustc-coverage-tests/snapshots/fstar/Coverage.Drop_trait.fst
index c8db9b6cf..95ffd8e15 100644
--- a/rustc-coverage-tests/snapshots/fstar/Coverage.Drop_trait.fst
+++ b/rustc-coverage-tests/snapshots/fstar/Coverage.Drop_trait.fst
@@ -13,17 +13,18 @@ let impl: Core.Ops.Drop.t_Drop t_Firework =
     f_drop
     =
     fun (self: t_Firework) ->
+      let args:t_Array Core.Fmt.Rt.t_Argument (mk_usize 1) =
+        let list = [Core.Fmt.Rt.impl__new_display #i32 self.f_strength] in
+        FStar.Pervasives.assert_norm (Prims.eq2 (List.Tot.length list) 1);
+        Rust_primitives.Hax.array_of_list 1 list
+      in
       let _:Prims.unit =
-        Std.Io.Stdio.e_print (Core.Fmt.Rt.impl_2__new_v1 (mk_usize 2)
+        Std.Io.Stdio.e_print (Core.Fmt.Rt.impl_1__new_v1 (mk_usize 2)
               (mk_usize 1)
               (let list = ["BOOM times "; "!!!\n"] in
                 FStar.Pervasives.assert_norm (Prims.eq2 (List.Tot.length list) 2);
                 Rust_primitives.Hax.array_of_list 2 list)
-              (let list =
-                  [Core.Fmt.Rt.impl__new_display #i32 self.f_strength <: Core.Fmt.Rt.t_Argument]
-                in
-                FStar.Pervasives.assert_norm (Prims.eq2 (List.Tot.length list) 1);
-                Rust_primitives.Hax.array_of_list 1 list)
+              args
             <:
             Core.Fmt.t_Arguments)
       in
@@ -37,7 +38,7 @@ let main (_: Prims.unit) : Core.Result.t_Result Prims.unit u8 =
   if true
   then
     let _:Prims.unit =
-      Std.Io.Stdio.e_print (Core.Fmt.Rt.impl_2__new_const (mk_usize 1)
+      Std.Io.Stdio.e_print (Core.Fmt.Rt.impl_1__new_const (mk_usize 1)
             (let list = ["Exiting with error...\n"] in
               FStar.Pervasives.assert_norm (Prims.eq2 (List.Tot.length list) 1);
               Rust_primitives.Hax.array_of_list 1 list)
diff --git a/rustc-coverage-tests/snapshots/fstar/Coverage.Generics.fst b/rustc-coverage-tests/snapshots/fstar/Coverage.Generics.fst
index 069b00db0..00bd52ee1 100644
--- a/rustc-coverage-tests/snapshots/fstar/Coverage.Generics.fst
+++ b/rustc-coverage-tests/snapshots/fstar/Coverage.Generics.fst
@@ -29,17 +29,18 @@ let impl_1
     f_drop
     =
     fun (self: t_Firework v_T) ->
+      let args:t_Array Core.Fmt.Rt.t_Argument (mk_usize 1) =
+        let list = [Core.Fmt.Rt.impl__new_display #v_T self.f_strength] in
+        FStar.Pervasives.assert_norm (Prims.eq2 (List.Tot.length list) 1);
+        Rust_primitives.Hax.array_of_list 1 list
+      in
       let _:Prims.unit =
-        Std.Io.Stdio.e_print (Core.Fmt.Rt.impl_2__new_v1 (mk_usize 2)
+        Std.Io.Stdio.e_print (Core.Fmt.Rt.impl_1__new_v1 (mk_usize 2)
               (mk_usize 1)
               (let list = ["BOOM times "; "!!!\n"] in
                 FStar.Pervasives.assert_norm (Prims.eq2 (List.Tot.length list) 2);
                 Rust_primitives.Hax.array_of_list 2 list)
-              (let list =
-                  [Core.Fmt.Rt.impl__new_display #v_T self.f_strength <: Core.Fmt.Rt.t_Argument]
-                in
-                FStar.Pervasives.assert_norm (Prims.eq2 (List.Tot.length list) 1);
-                Rust_primitives.Hax.array_of_list 1 list)
+              args
             <:
             Core.Fmt.t_Arguments)
       in
@@ -56,7 +57,7 @@ let main (_: Prims.unit) : Core.Result.t_Result Prims.unit u8 =
   if true
   then
     let _:Prims.unit =
-      Std.Io.Stdio.e_print (Core.Fmt.Rt.impl_2__new_const (mk_usize 1)
+      Std.Io.Stdio.e_print (Core.Fmt.Rt.impl_1__new_const (mk_usize 1)
             (let list = ["Exiting with error...\n"] in
               FStar.Pervasives.assert_norm (Prims.eq2 (List.Tot.length list) 1);
               Rust_primitives.Hax.array_of_list 1 list)
diff --git a/rustc-coverage-tests/snapshots/fstar/Coverage.If_not.fst b/rustc-coverage-tests/snapshots/fstar/Coverage.If_not.fst
index 7ca500049..c7d0ce014 100644
--- a/rustc-coverage-tests/snapshots/fstar/Coverage.If_not.fst
+++ b/rustc-coverage-tests/snapshots/fstar/Coverage.If_not.fst
@@ -8,7 +8,7 @@ let if_not (cond: bool) : Prims.unit =
     if ~.cond
     then
       let _:Prims.unit =
-        Std.Io.Stdio.e_print (Core.Fmt.Rt.impl_2__new_const (mk_usize 1)
+        Std.Io.Stdio.e_print (Core.Fmt.Rt.impl_1__new_const (mk_usize 1)
               (let list = ["cond was false\n"] in
                 FStar.Pervasives.assert_norm (Prims.eq2 (List.Tot.length list) 1);
                 Rust_primitives.Hax.array_of_list 1 list)
@@ -22,7 +22,7 @@ let if_not (cond: bool) : Prims.unit =
     if ~.cond
     then
       let _:Prims.unit =
-        Std.Io.Stdio.e_print (Core.Fmt.Rt.impl_2__new_const (mk_usize 1)
+        Std.Io.Stdio.e_print (Core.Fmt.Rt.impl_1__new_const (mk_usize 1)
               (let list = ["cond was false\n"] in
                 FStar.Pervasives.assert_norm (Prims.eq2 (List.Tot.length list) 1);
                 Rust_primitives.Hax.array_of_list 1 list)
@@ -35,7 +35,7 @@ let if_not (cond: bool) : Prims.unit =
   if ~.cond
   then
     let _:Prims.unit =
-      Std.Io.Stdio.e_print (Core.Fmt.Rt.impl_2__new_const (mk_usize 1)
+      Std.Io.Stdio.e_print (Core.Fmt.Rt.impl_1__new_const (mk_usize 1)
             (let list = ["cond was false\n"] in
               FStar.Pervasives.assert_norm (Prims.eq2 (List.Tot.length list) 1);
               Rust_primitives.Hax.array_of_list 1 list)
@@ -46,7 +46,7 @@ let if_not (cond: bool) : Prims.unit =
     ()
   else
     let _:Prims.unit =
-      Std.Io.Stdio.e_print (Core.Fmt.Rt.impl_2__new_const (mk_usize 1)
+      Std.Io.Stdio.e_print (Core.Fmt.Rt.impl_1__new_const (mk_usize 1)
             (let list = ["cond was true\n"] in
               FStar.Pervasives.assert_norm (Prims.eq2 (List.Tot.length list) 1);
               Rust_primitives.Hax.array_of_list 1 list)
diff --git a/rustc-coverage-tests/snapshots/fstar/Coverage.Inline.fst b/rustc-coverage-tests/snapshots/fstar/Coverage.Inline.fst
index 68c3296a8..96d2ac383 100644
--- a/rustc-coverage-tests/snapshots/fstar/Coverage.Inline.fst
+++ b/rustc-coverage-tests/snapshots/fstar/Coverage.Inline.fst
@@ -25,11 +25,11 @@ let display
     : Prims.unit =
   let _:Prims.unit =
     Rust_primitives.Hax.failure "(FunctionalizeLoops) something is not implemented yet.This is discussed in issue https://github.com/hacspec/hax/issues/405.\nPlease upvote or comment this issue if you see this error message.\nLoop without mutation"
-      "{\n for x in (core::iter::traits::collect::f_into_iter(xs)) {\n {\n let _: tuple0 = {\n std::io::stdio::e_print(\n core::fmt::rt::impl_2__new_v1::<\n generic_value!(todo),\n generic_value!(todo),\n >([\"\"], [c..."
+      "{\n for x in (core::iter::traits::collect::f_into_iter(xs)) {\n {\n let args: [core::fmt::rt::t_Argument; 1] = {\n [core::fmt::rt::impl__new_display::<T>(x)]\n };\n {\n let _: tuple0 = {\n std::io::stdio::e_p..."
 
   in
   let _:Prims.unit =
-    Std.Io.Stdio.e_print (Core.Fmt.Rt.impl_2__new_const (mk_usize 1)
+    Std.Io.Stdio.e_print (Core.Fmt.Rt.impl_1__new_const (mk_usize 1)
           (let list = ["\n"] in
             FStar.Pervasives.assert_norm (Prims.eq2 (List.Tot.length list) 1);
             Rust_primitives.Hax.array_of_list 1 list)
@@ -40,7 +40,7 @@ let display
   ()
 
 let error (_: Prims.unit) : Prims.unit =
-  Rust_primitives.Hax.never_to_any (Core.Panicking.panic_fmt (Core.Fmt.Rt.impl_2__new_const (mk_usize
+  Rust_primitives.Hax.never_to_any (Core.Panicking.panic_fmt (Core.Fmt.Rt.impl_1__new_const (mk_usize
               1)
             (let list = ["error"] in
               FStar.Pervasives.assert_norm (Prims.eq2 (List.Tot.length list) 1);
diff --git a/rustc-coverage-tests/snapshots/fstar/Coverage.Inline_dead.fst b/rustc-coverage-tests/snapshots/fstar/Coverage.Inline_dead.fst
index 44e1ff1e3..65091dd0a 100644
--- a/rustc-coverage-tests/snapshots/fstar/Coverage.Inline_dead.fst
+++ b/rustc-coverage-tests/snapshots/fstar/Coverage.Inline_dead.fst
@@ -8,17 +8,18 @@ let dead (_: Prims.unit) : u32 = mk_u32 42
 let live (v_B: bool) (_: Prims.unit) : u32 = if v_B then dead () else mk_u32 0
 
 let main (_: Prims.unit) : Prims.unit =
+  let args:t_Array Core.Fmt.Rt.t_Argument (mk_usize 1) =
+    let list = [Core.Fmt.Rt.impl__new_display #u32 (live false () <: u32)] in
+    FStar.Pervasives.assert_norm (Prims.eq2 (List.Tot.length list) 1);
+    Rust_primitives.Hax.array_of_list 1 list
+  in
   let _:Prims.unit =
-    Std.Io.Stdio.e_print (Core.Fmt.Rt.impl_2__new_v1 (mk_usize 2)
+    Std.Io.Stdio.e_print (Core.Fmt.Rt.impl_1__new_v1 (mk_usize 2)
           (mk_usize 1)
           (let list = [""; "\n"] in
             FStar.Pervasives.assert_norm (Prims.eq2 (List.Tot.length list) 2);
             Rust_primitives.Hax.array_of_list 2 list)
-          (let list =
-              [Core.Fmt.Rt.impl__new_display #u32 (live false () <: u32) <: Core.Fmt.Rt.t_Argument]
-            in
-            FStar.Pervasives.assert_norm (Prims.eq2 (List.Tot.length list) 1);
-            Rust_primitives.Hax.array_of_list 1 list)
+          args
         <:
         Core.Fmt.t_Arguments)
   in
diff --git a/rustc-coverage-tests/snapshots/fstar/Coverage.Inner_items.fst b/rustc-coverage-tests/snapshots/fstar/Coverage.Inner_items.fst
index 2e5ac967c..f6d870fde 100644
--- a/rustc-coverage-tests/snapshots/fstar/Coverage.Inner_items.fst
+++ b/rustc-coverage-tests/snapshots/fstar/Coverage.Inner_items.fst
@@ -14,15 +14,18 @@ let main__t_in_mod__v_IN_MOD_CONST: u32 = mk_u32 1000
 let main__in_func (a: u32) : Prims.unit =
   let b:u32 = mk_u32 1 in
   let c:u32 = a +! b in
+  let args:t_Array Core.Fmt.Rt.t_Argument (mk_usize 1) =
+    let list = [Core.Fmt.Rt.impl__new_display #u32 c] in
+    FStar.Pervasives.assert_norm (Prims.eq2 (List.Tot.length list) 1);
+    Rust_primitives.Hax.array_of_list 1 list
+  in
   let _:Prims.unit =
-    Std.Io.Stdio.e_print (Core.Fmt.Rt.impl_2__new_v1 (mk_usize 2)
+    Std.Io.Stdio.e_print (Core.Fmt.Rt.impl_1__new_v1 (mk_usize 2)
           (mk_usize 1)
           (let list = ["c = "; "\n"] in
             FStar.Pervasives.assert_norm (Prims.eq2 (List.Tot.length list) 2);
             Rust_primitives.Hax.array_of_list 2 list)
-          (let list = [Core.Fmt.Rt.impl__new_display #u32 c <: Core.Fmt.Rt.t_Argument] in
-            FStar.Pervasives.assert_norm (Prims.eq2 (List.Tot.length list) 1);
-            Rust_primitives.Hax.array_of_list 1 list)
+          args
         <:
         Core.Fmt.t_Arguments)
   in
diff --git a/rustc-coverage-tests/snapshots/fstar/Coverage.Issue_83601_.fst b/rustc-coverage-tests/snapshots/fstar/Coverage.Issue_83601_.fst
index c26f2240c..456fe3b9d 100644
--- a/rustc-coverage-tests/snapshots/fstar/Coverage.Issue_83601_.fst
+++ b/rustc-coverage-tests/snapshots/fstar/Coverage.Issue_83601_.fst
@@ -44,47 +44,50 @@ let main (_: Prims.unit) : Prims.unit =
     match baz, (Foo (mk_u32 1) <: t_Foo) <: (t_Foo & t_Foo) with
     | left_val, right_val -> Hax_lib.v_assert (~.(left_val =. right_val <: bool) <: bool)
   in
+  let args:t_Array Core.Fmt.Rt.t_Argument (mk_usize 1) =
+    let list = [Core.Fmt.Rt.impl__new_debug #t_Foo (Foo (mk_u32 1) <: t_Foo)] in
+    FStar.Pervasives.assert_norm (Prims.eq2 (List.Tot.length list) 1);
+    Rust_primitives.Hax.array_of_list 1 list
+  in
   let _:Prims.unit =
-    Std.Io.Stdio.e_print (Core.Fmt.Rt.impl_2__new_v1 (mk_usize 2)
+    Std.Io.Stdio.e_print (Core.Fmt.Rt.impl_1__new_v1 (mk_usize 2)
           (mk_usize 1)
           (let list = [""; "\n"] in
             FStar.Pervasives.assert_norm (Prims.eq2 (List.Tot.length list) 2);
             Rust_primitives.Hax.array_of_list 2 list)
-          (let list =
-              [
-                Core.Fmt.Rt.impl__new_debug #t_Foo (Foo (mk_u32 1) <: t_Foo)
-                <:
-                Core.Fmt.Rt.t_Argument
-              ]
-            in
-            FStar.Pervasives.assert_norm (Prims.eq2 (List.Tot.length list) 1);
-            Rust_primitives.Hax.array_of_list 1 list)
+          args
         <:
         Core.Fmt.t_Arguments)
   in
   let _:Prims.unit = () in
+  let args:t_Array Core.Fmt.Rt.t_Argument (mk_usize 1) =
+    let list = [Core.Fmt.Rt.impl__new_debug #t_Foo bar] in
+    FStar.Pervasives.assert_norm (Prims.eq2 (List.Tot.length list) 1);
+    Rust_primitives.Hax.array_of_list 1 list
+  in
   let _:Prims.unit =
-    Std.Io.Stdio.e_print (Core.Fmt.Rt.impl_2__new_v1 (mk_usize 2)
+    Std.Io.Stdio.e_print (Core.Fmt.Rt.impl_1__new_v1 (mk_usize 2)
           (mk_usize 1)
           (let list = [""; "\n"] in
             FStar.Pervasives.assert_norm (Prims.eq2 (List.Tot.length list) 2);
             Rust_primitives.Hax.array_of_list 2 list)
-          (let list = [Core.Fmt.Rt.impl__new_debug #t_Foo bar <: Core.Fmt.Rt.t_Argument] in
-            FStar.Pervasives.assert_norm (Prims.eq2 (List.Tot.length list) 1);
-            Rust_primitives.Hax.array_of_list 1 list)
+          args
         <:
         Core.Fmt.t_Arguments)
   in
   let _:Prims.unit = () in
+  let args:t_Array Core.Fmt.Rt.t_Argument (mk_usize 1) =
+    let list = [Core.Fmt.Rt.impl__new_debug #t_Foo baz] in
+    FStar.Pervasives.assert_norm (Prims.eq2 (List.Tot.length list) 1);
+    Rust_primitives.Hax.array_of_list 1 list
+  in
   let _:Prims.unit =
-    Std.Io.Stdio.e_print (Core.Fmt.Rt.impl_2__new_v1 (mk_usize 2)
+    Std.Io.Stdio.e_print (Core.Fmt.Rt.impl_1__new_v1 (mk_usize 2)
           (mk_usize 1)
           (let list = [""; "\n"] in
             FStar.Pervasives.assert_norm (Prims.eq2 (List.Tot.length list) 2);
             Rust_primitives.Hax.array_of_list 2 list)
-          (let list = [Core.Fmt.Rt.impl__new_debug #t_Foo baz <: Core.Fmt.Rt.t_Argument] in
-            FStar.Pervasives.assert_norm (Prims.eq2 (List.Tot.length list) 1);
-            Rust_primitives.Hax.array_of_list 1 list)
+          args
         <:
         Core.Fmt.t_Arguments)
   in
diff --git a/rustc-coverage-tests/snapshots/fstar/Coverage.Loops_branches.fst b/rustc-coverage-tests/snapshots/fstar/Coverage.Loops_branches.fst
index 1e5ec879d..be8b66179 100644
--- a/rustc-coverage-tests/snapshots/fstar/Coverage.Loops_branches.fst
+++ b/rustc-coverage-tests/snapshots/fstar/Coverage.Loops_branches.fst
@@ -30,7 +30,7 @@ let impl: Core.Fmt.t_Debug t_DebugTest =
         in
         let tmp0, out:(Core.Fmt.t_Formatter & Core.Result.t_Result Prims.unit Core.Fmt.t_Error) =
           Core.Fmt.impl_11__write_fmt f
-            (Core.Fmt.Rt.impl_2__new_const (mk_usize 1)
+            (Core.Fmt.Rt.impl_1__new_const (mk_usize 1)
                 (let list = ["cool"] in
                   FStar.Pervasives.assert_norm (Prims.eq2 (List.Tot.length list) 1);
                   Rust_primitives.Hax.array_of_list 1 list)
@@ -62,7 +62,7 @@ let impl: Core.Fmt.t_Debug t_DebugTest =
                       let tmp0, out:(Core.Fmt.t_Formatter &
                         Core.Result.t_Result Prims.unit Core.Fmt.t_Error) =
                         Core.Fmt.impl_11__write_fmt f
-                          (Core.Fmt.Rt.impl_2__new_const (mk_usize 1)
+                          (Core.Fmt.Rt.impl_1__new_const (mk_usize 1)
                               (let list = ["cool"] in
                                 FStar.Pervasives.assert_norm (Prims.eq2 (List.Tot.length list) 1);
                                 Rust_primitives.Hax.array_of_list 1 list)
@@ -148,7 +148,7 @@ let impl: Core.Fmt.t_Debug t_DebugTest =
                   let tmp0, out:(Core.Fmt.t_Formatter &
                     Core.Result.t_Result Prims.unit Core.Fmt.t_Error) =
                     Core.Fmt.impl_11__write_fmt f
-                      (Core.Fmt.Rt.impl_2__new_const (mk_usize 1)
+                      (Core.Fmt.Rt.impl_1__new_const (mk_usize 1)
                           (let list = ["cool"] in
                             FStar.Pervasives.assert_norm (Prims.eq2 (List.Tot.length list) 1);
                             Rust_primitives.Hax.array_of_list 1 list)
@@ -254,7 +254,7 @@ let impl_1: Core.Fmt.t_Display t_DisplayTest =
                   let tmp0, out:(Core.Fmt.t_Formatter &
                     Core.Result.t_Result Prims.unit Core.Fmt.t_Error) =
                     Core.Fmt.impl_11__write_fmt f
-                      (Core.Fmt.Rt.impl_2__new_const (mk_usize 1)
+                      (Core.Fmt.Rt.impl_1__new_const (mk_usize 1)
                           (let list = ["cool"] in
                             FStar.Pervasives.assert_norm (Prims.eq2 (List.Tot.length list) 1);
                             Rust_primitives.Hax.array_of_list 1 list)
@@ -312,7 +312,7 @@ let impl_1: Core.Fmt.t_Display t_DisplayTest =
         in
         let tmp0, out:(Core.Fmt.t_Formatter & Core.Result.t_Result Prims.unit Core.Fmt.t_Error) =
           Core.Fmt.impl_11__write_fmt f
-            (Core.Fmt.Rt.impl_2__new_const (mk_usize 1)
+            (Core.Fmt.Rt.impl_1__new_const (mk_usize 1)
                 (let list = ["cool"] in
                   FStar.Pervasives.assert_norm (Prims.eq2 (List.Tot.length list) 1);
                   Rust_primitives.Hax.array_of_list 1 list)
@@ -351,7 +351,7 @@ let impl_1: Core.Fmt.t_Display t_DisplayTest =
                       let tmp0, out:(Core.Fmt.t_Formatter &
                         Core.Result.t_Result Prims.unit Core.Fmt.t_Error) =
                         Core.Fmt.impl_11__write_fmt f
-                          (Core.Fmt.Rt.impl_2__new_const (mk_usize 1)
+                          (Core.Fmt.Rt.impl_1__new_const (mk_usize 1)
                               (let list = ["cool"] in
                                 FStar.Pervasives.assert_norm (Prims.eq2 (List.Tot.length list) 1);
                                 Rust_primitives.Hax.array_of_list 1 list)
@@ -411,33 +411,35 @@ let impl_1: Core.Fmt.t_Display t_DisplayTest =
 
 let main (_: Prims.unit) : Prims.unit =
   let debug_test:t_DebugTest = DebugTest <: t_DebugTest in
+  let args:t_Array Core.Fmt.Rt.t_Argument (mk_usize 1) =
+    let list = [Core.Fmt.Rt.impl__new_debug #t_DebugTest debug_test] in
+    FStar.Pervasives.assert_norm (Prims.eq2 (List.Tot.length list) 1);
+    Rust_primitives.Hax.array_of_list 1 list
+  in
   let _:Prims.unit =
-    Std.Io.Stdio.e_print (Core.Fmt.Rt.impl_2__new_v1 (mk_usize 2)
+    Std.Io.Stdio.e_print (Core.Fmt.Rt.impl_1__new_v1 (mk_usize 2)
           (mk_usize 1)
           (let list = [""; "\n"] in
             FStar.Pervasives.assert_norm (Prims.eq2 (List.Tot.length list) 2);
             Rust_primitives.Hax.array_of_list 2 list)
-          (let list =
-              [Core.Fmt.Rt.impl__new_debug #t_DebugTest debug_test <: Core.Fmt.Rt.t_Argument]
-            in
-            FStar.Pervasives.assert_norm (Prims.eq2 (List.Tot.length list) 1);
-            Rust_primitives.Hax.array_of_list 1 list)
+          args
         <:
         Core.Fmt.t_Arguments)
   in
   let _:Prims.unit = () in
   let display_test:t_DisplayTest = DisplayTest <: t_DisplayTest in
+  let args:t_Array Core.Fmt.Rt.t_Argument (mk_usize 1) =
+    let list = [Core.Fmt.Rt.impl__new_display #t_DisplayTest display_test] in
+    FStar.Pervasives.assert_norm (Prims.eq2 (List.Tot.length list) 1);
+    Rust_primitives.Hax.array_of_list 1 list
+  in
   let _:Prims.unit =
-    Std.Io.Stdio.e_print (Core.Fmt.Rt.impl_2__new_v1 (mk_usize 2)
+    Std.Io.Stdio.e_print (Core.Fmt.Rt.impl_1__new_v1 (mk_usize 2)
           (mk_usize 1)
           (let list = [""; "\n"] in
             FStar.Pervasives.assert_norm (Prims.eq2 (List.Tot.length list) 2);
             Rust_primitives.Hax.array_of_list 2 list)
-          (let list =
-              [Core.Fmt.Rt.impl__new_display #t_DisplayTest display_test <: Core.Fmt.Rt.t_Argument]
-            in
-            FStar.Pervasives.assert_norm (Prims.eq2 (List.Tot.length list) 1);
-            Rust_primitives.Hax.array_of_list 1 list)
+          args
         <:
         Core.Fmt.t_Arguments)
   in
diff --git a/rustc-coverage-tests/snapshots/fstar/Coverage.Macro_in_closure.fst b/rustc-coverage-tests/snapshots/fstar/Coverage.Macro_in_closure.fst
index f225df678..2647d48df 100644
--- a/rustc-coverage-tests/snapshots/fstar/Coverage.Macro_in_closure.fst
+++ b/rustc-coverage-tests/snapshots/fstar/Coverage.Macro_in_closure.fst
@@ -7,7 +7,7 @@ let v_NO_BLOCK:  Prims.unit -> Prims.unit =
   fun temp_0_ ->
     let _:Prims.unit = temp_0_ in
     let _:Prims.unit =
-      Std.Io.Stdio.e_print (Core.Fmt.Rt.impl_2__new_const (mk_usize 1)
+      Std.Io.Stdio.e_print (Core.Fmt.Rt.impl_1__new_const (mk_usize 1)
             (let list = ["hello\n"] in
               FStar.Pervasives.assert_norm (Prims.eq2 (List.Tot.length list) 1);
               Rust_primitives.Hax.array_of_list 1 list)
@@ -20,7 +20,7 @@ let v_WITH_BLOCK:  Prims.unit -> Prims.unit =
   fun temp_0_ ->
     let _:Prims.unit = temp_0_ in
     let _:Prims.unit =
-      Std.Io.Stdio.e_print (Core.Fmt.Rt.impl_2__new_const (mk_usize 1)
+      Std.Io.Stdio.e_print (Core.Fmt.Rt.impl_1__new_const (mk_usize 1)
             (let list = ["hello\n"] in
               FStar.Pervasives.assert_norm (Prims.eq2 (List.Tot.length list) 1);
               Rust_primitives.Hax.array_of_list 1 list)
diff --git a/rustc-coverage-tests/snapshots/fstar/Coverage.No_cov_crate.Nested_fns.fst b/rustc-coverage-tests/snapshots/fstar/Coverage.No_cov_crate.Nested_fns.fst
index 1aa969a36..453968305 100644
--- a/rustc-coverage-tests/snapshots/fstar/Coverage.No_cov_crate.Nested_fns.fst
+++ b/rustc-coverage-tests/snapshots/fstar/Coverage.No_cov_crate.Nested_fns.fst
@@ -7,7 +7,7 @@ let outer_not_covered__inner (is_true: bool) : Prims.unit =
   if is_true
   then
     let _:Prims.unit =
-      Std.Io.Stdio.e_print (Core.Fmt.Rt.impl_2__new_const (mk_usize 1)
+      Std.Io.Stdio.e_print (Core.Fmt.Rt.impl_1__new_const (mk_usize 1)
             (let list = ["called and covered\n"] in
               FStar.Pervasives.assert_norm (Prims.eq2 (List.Tot.length list) 1);
               Rust_primitives.Hax.array_of_list 1 list)
@@ -18,7 +18,7 @@ let outer_not_covered__inner (is_true: bool) : Prims.unit =
     ()
   else
     let _:Prims.unit =
-      Std.Io.Stdio.e_print (Core.Fmt.Rt.impl_2__new_const (mk_usize 1)
+      Std.Io.Stdio.e_print (Core.Fmt.Rt.impl_1__new_const (mk_usize 1)
             (let list = ["absolutely not covered\n"] in
               FStar.Pervasives.assert_norm (Prims.eq2 (List.Tot.length list) 1);
               Rust_primitives.Hax.array_of_list 1 list)
@@ -30,7 +30,7 @@ let outer_not_covered__inner (is_true: bool) : Prims.unit =
 
 let outer_not_covered (is_true: bool) : Prims.unit =
   let _:Prims.unit =
-    Std.Io.Stdio.e_print (Core.Fmt.Rt.impl_2__new_const (mk_usize 1)
+    Std.Io.Stdio.e_print (Core.Fmt.Rt.impl_1__new_const (mk_usize 1)
           (let list = ["called but not covered\n"] in
             FStar.Pervasives.assert_norm (Prims.eq2 (List.Tot.length list) 1);
             Rust_primitives.Hax.array_of_list 1 list)
@@ -45,7 +45,7 @@ let outer__inner_not_covered (is_true: bool) : Prims.unit =
   if is_true
   then
     let _:Prims.unit =
-      Std.Io.Stdio.e_print (Core.Fmt.Rt.impl_2__new_const (mk_usize 1)
+      Std.Io.Stdio.e_print (Core.Fmt.Rt.impl_1__new_const (mk_usize 1)
             (let list = ["called but not covered\n"] in
               FStar.Pervasives.assert_norm (Prims.eq2 (List.Tot.length list) 1);
               Rust_primitives.Hax.array_of_list 1 list)
@@ -56,7 +56,7 @@ let outer__inner_not_covered (is_true: bool) : Prims.unit =
     ()
   else
     let _:Prims.unit =
-      Std.Io.Stdio.e_print (Core.Fmt.Rt.impl_2__new_const (mk_usize 1)
+      Std.Io.Stdio.e_print (Core.Fmt.Rt.impl_1__new_const (mk_usize 1)
             (let list = ["absolutely not covered\n"] in
               FStar.Pervasives.assert_norm (Prims.eq2 (List.Tot.length list) 1);
               Rust_primitives.Hax.array_of_list 1 list)
@@ -68,7 +68,7 @@ let outer__inner_not_covered (is_true: bool) : Prims.unit =
 
 let outer (is_true: bool) : Prims.unit =
   let _:Prims.unit =
-    Std.Io.Stdio.e_print (Core.Fmt.Rt.impl_2__new_const (mk_usize 1)
+    Std.Io.Stdio.e_print (Core.Fmt.Rt.impl_1__new_const (mk_usize 1)
           (let list = ["called and covered\n"] in
             FStar.Pervasives.assert_norm (Prims.eq2 (List.Tot.length list) 1);
             Rust_primitives.Hax.array_of_list 1 list)
@@ -83,7 +83,7 @@ let outer_both_covered__inner (is_true: bool) : Prims.unit =
   if is_true
   then
     let _:Prims.unit =
-      Std.Io.Stdio.e_print (Core.Fmt.Rt.impl_2__new_const (mk_usize 1)
+      Std.Io.Stdio.e_print (Core.Fmt.Rt.impl_1__new_const (mk_usize 1)
             (let list = ["called and covered\n"] in
               FStar.Pervasives.assert_norm (Prims.eq2 (List.Tot.length list) 1);
               Rust_primitives.Hax.array_of_list 1 list)
@@ -94,7 +94,7 @@ let outer_both_covered__inner (is_true: bool) : Prims.unit =
     ()
   else
     let _:Prims.unit =
-      Std.Io.Stdio.e_print (Core.Fmt.Rt.impl_2__new_const (mk_usize 1)
+      Std.Io.Stdio.e_print (Core.Fmt.Rt.impl_1__new_const (mk_usize 1)
             (let list = ["absolutely not covered\n"] in
               FStar.Pervasives.assert_norm (Prims.eq2 (List.Tot.length list) 1);
               Rust_primitives.Hax.array_of_list 1 list)
@@ -106,7 +106,7 @@ let outer_both_covered__inner (is_true: bool) : Prims.unit =
 
 let outer_both_covered (is_true: bool) : Prims.unit =
   let _:Prims.unit =
-    Std.Io.Stdio.e_print (Core.Fmt.Rt.impl_2__new_const (mk_usize 1)
+    Std.Io.Stdio.e_print (Core.Fmt.Rt.impl_1__new_const (mk_usize 1)
           (let list = ["called and covered\n"] in
             FStar.Pervasives.assert_norm (Prims.eq2 (List.Tot.length list) 1);
             Rust_primitives.Hax.array_of_list 1 list)
diff --git a/rustc-coverage-tests/snapshots/fstar/Coverage.No_cov_crate.fst b/rustc-coverage-tests/snapshots/fstar/Coverage.No_cov_crate.fst
index 2596c888d..dd83efe36 100644
--- a/rustc-coverage-tests/snapshots/fstar/Coverage.No_cov_crate.fst
+++ b/rustc-coverage-tests/snapshots/fstar/Coverage.No_cov_crate.fst
@@ -11,7 +11,7 @@ let _ =
 
 let do_not_add_coverage_1_ (_: Prims.unit) : Prims.unit =
   let _:Prims.unit =
-    Std.Io.Stdio.e_print (Core.Fmt.Rt.impl_2__new_const (mk_usize 1)
+    Std.Io.Stdio.e_print (Core.Fmt.Rt.impl_1__new_const (mk_usize 1)
           (let list = ["called but not covered\n"] in
             FStar.Pervasives.assert_norm (Prims.eq2 (List.Tot.length list) 1);
             Rust_primitives.Hax.array_of_list 1 list)
@@ -23,7 +23,7 @@ let do_not_add_coverage_1_ (_: Prims.unit) : Prims.unit =
 
 let do_not_add_coverage_2_ (_: Prims.unit) : Prims.unit =
   let _:Prims.unit =
-    Std.Io.Stdio.e_print (Core.Fmt.Rt.impl_2__new_const (mk_usize 1)
+    Std.Io.Stdio.e_print (Core.Fmt.Rt.impl_1__new_const (mk_usize 1)
           (let list = ["called but not covered\n"] in
             FStar.Pervasives.assert_norm (Prims.eq2 (List.Tot.length list) 1);
             Rust_primitives.Hax.array_of_list 1 list)
@@ -35,7 +35,7 @@ let do_not_add_coverage_2_ (_: Prims.unit) : Prims.unit =
 
 let do_not_add_coverage_not_called (_: Prims.unit) : Prims.unit =
   let _:Prims.unit =
-    Std.Io.Stdio.e_print (Core.Fmt.Rt.impl_2__new_const (mk_usize 1)
+    Std.Io.Stdio.e_print (Core.Fmt.Rt.impl_1__new_const (mk_usize 1)
           (let list = ["not called and not covered\n"] in
             FStar.Pervasives.assert_norm (Prims.eq2 (List.Tot.length list) 1);
             Rust_primitives.Hax.array_of_list 1 list)
@@ -47,7 +47,7 @@ let do_not_add_coverage_not_called (_: Prims.unit) : Prims.unit =
 
 let add_coverage_1_ (_: Prims.unit) : Prims.unit =
   let _:Prims.unit =
-    Std.Io.Stdio.e_print (Core.Fmt.Rt.impl_2__new_const (mk_usize 1)
+    Std.Io.Stdio.e_print (Core.Fmt.Rt.impl_1__new_const (mk_usize 1)
           (let list = ["called and covered\n"] in
             FStar.Pervasives.assert_norm (Prims.eq2 (List.Tot.length list) 1);
             Rust_primitives.Hax.array_of_list 1 list)
@@ -59,7 +59,7 @@ let add_coverage_1_ (_: Prims.unit) : Prims.unit =
 
 let add_coverage_2_ (_: Prims.unit) : Prims.unit =
   let _:Prims.unit =
-    Std.Io.Stdio.e_print (Core.Fmt.Rt.impl_2__new_const (mk_usize 1)
+    Std.Io.Stdio.e_print (Core.Fmt.Rt.impl_1__new_const (mk_usize 1)
           (let list = ["called and covered\n"] in
             FStar.Pervasives.assert_norm (Prims.eq2 (List.Tot.length list) 1);
             Rust_primitives.Hax.array_of_list 1 list)
@@ -71,7 +71,7 @@ let add_coverage_2_ (_: Prims.unit) : Prims.unit =
 
 let add_coverage_not_called (_: Prims.unit) : Prims.unit =
   let _:Prims.unit =
-    Std.Io.Stdio.e_print (Core.Fmt.Rt.impl_2__new_const (mk_usize 1)
+    Std.Io.Stdio.e_print (Core.Fmt.Rt.impl_1__new_const (mk_usize 1)
           (let list = ["not called but covered\n"] in
             FStar.Pervasives.assert_norm (Prims.eq2 (List.Tot.length list) 1);
             Rust_primitives.Hax.array_of_list 1 list)
diff --git a/rustc-coverage-tests/snapshots/fstar/Coverage.Overflow.fst b/rustc-coverage-tests/snapshots/fstar/Coverage.Overflow.fst
index 8b0241ab1..c8dbe6bf1 100644
--- a/rustc-coverage-tests/snapshots/fstar/Coverage.Overflow.fst
+++ b/rustc-coverage-tests/snapshots/fstar/Coverage.Overflow.fst
@@ -8,7 +8,7 @@ let might_overflow (to_add: u32) : u32 =
     if to_add >. mk_u32 5
     then
       let _:Prims.unit =
-        Std.Io.Stdio.e_print (Core.Fmt.Rt.impl_2__new_const (mk_usize 1)
+        Std.Io.Stdio.e_print (Core.Fmt.Rt.impl_1__new_const (mk_usize 1)
               (let list = ["this will probably overflow\n"] in
                 FStar.Pervasives.assert_norm (Prims.eq2 (List.Tot.length list) 1);
                 Rust_primitives.Hax.array_of_list 1 list)
@@ -19,27 +19,28 @@ let might_overflow (to_add: u32) : u32 =
       ()
   in
   let add_to:u32 = Core.Num.impl_u32__MAX -! mk_u32 5 in
+  let args:(u32 & u32) = add_to, to_add <: (u32 & u32) in
+  let args:t_Array Core.Fmt.Rt.t_Argument (mk_usize 2) =
+    let list =
+      [Core.Fmt.Rt.impl__new_display #u32 args._1; Core.Fmt.Rt.impl__new_display #u32 args._2]
+    in
+    FStar.Pervasives.assert_norm (Prims.eq2 (List.Tot.length list) 2);
+    Rust_primitives.Hax.array_of_list 2 list
+  in
   let _:Prims.unit =
-    Std.Io.Stdio.e_print (Core.Fmt.Rt.impl_2__new_v1 (mk_usize 3)
+    Std.Io.Stdio.e_print (Core.Fmt.Rt.impl_1__new_v1 (mk_usize 3)
           (mk_usize 2)
           (let list = ["does "; " + "; " overflow?\n"] in
             FStar.Pervasives.assert_norm (Prims.eq2 (List.Tot.length list) 3);
             Rust_primitives.Hax.array_of_list 3 list)
-          (let list =
-              [
-                Core.Fmt.Rt.impl__new_display #u32 add_to <: Core.Fmt.Rt.t_Argument;
-                Core.Fmt.Rt.impl__new_display #u32 to_add <: Core.Fmt.Rt.t_Argument
-              ]
-            in
-            FStar.Pervasives.assert_norm (Prims.eq2 (List.Tot.length list) 2);
-            Rust_primitives.Hax.array_of_list 2 list)
+          args
         <:
         Core.Fmt.t_Arguments)
   in
   let _:Prims.unit = () in
   let result:u32 = to_add +! add_to in
   let _:Prims.unit =
-    Std.Io.Stdio.e_print (Core.Fmt.Rt.impl_2__new_const (mk_usize 1)
+    Std.Io.Stdio.e_print (Core.Fmt.Rt.impl_1__new_const (mk_usize 1)
           (let list = ["continuing after overflow check\n"] in
             FStar.Pervasives.assert_norm (Prims.eq2 (List.Tot.length list) 1);
             Rust_primitives.Hax.array_of_list 1 list)
@@ -68,17 +69,18 @@ let main (_: Prims.unit) : Core.Result.t_Result Prims.unit u8 =
             if countdown =. mk_i32 1
             then
               let result:u32 = might_overflow (mk_u32 10) in
+              let args:t_Array Core.Fmt.Rt.t_Argument (mk_usize 1) =
+                let list = [Core.Fmt.Rt.impl__new_display #u32 result] in
+                FStar.Pervasives.assert_norm (Prims.eq2 (List.Tot.length list) 1);
+                Rust_primitives.Hax.array_of_list 1 list
+              in
               let _:Prims.unit =
-                Std.Io.Stdio.e_print (Core.Fmt.Rt.impl_2__new_v1 (mk_usize 2)
+                Std.Io.Stdio.e_print (Core.Fmt.Rt.impl_1__new_v1 (mk_usize 2)
                       (mk_usize 1)
                       (let list = ["Result: "; "\n"] in
                         FStar.Pervasives.assert_norm (Prims.eq2 (List.Tot.length list) 2);
                         Rust_primitives.Hax.array_of_list 2 list)
-                      (let list =
-                          [Core.Fmt.Rt.impl__new_display #u32 result <: Core.Fmt.Rt.t_Argument]
-                        in
-                        FStar.Pervasives.assert_norm (Prims.eq2 (List.Tot.length list) 1);
-                        Rust_primitives.Hax.array_of_list 1 list)
+                      args
                     <:
                     Core.Fmt.t_Arguments)
               in
@@ -88,17 +90,18 @@ let main (_: Prims.unit) : Core.Result.t_Result Prims.unit u8 =
               if countdown <. mk_i32 5
               then
                 let result:u32 = might_overflow (mk_u32 1) in
+                let args:t_Array Core.Fmt.Rt.t_Argument (mk_usize 1) =
+                  let list = [Core.Fmt.Rt.impl__new_display #u32 result] in
+                  FStar.Pervasives.assert_norm (Prims.eq2 (List.Tot.length list) 1);
+                  Rust_primitives.Hax.array_of_list 1 list
+                in
                 let _:Prims.unit =
-                  Std.Io.Stdio.e_print (Core.Fmt.Rt.impl_2__new_v1 (mk_usize 2)
+                  Std.Io.Stdio.e_print (Core.Fmt.Rt.impl_1__new_v1 (mk_usize 2)
                         (mk_usize 1)
                         (let list = ["Result: "; "\n"] in
                           FStar.Pervasives.assert_norm (Prims.eq2 (List.Tot.length list) 2);
                           Rust_primitives.Hax.array_of_list 2 list)
-                        (let list =
-                            [Core.Fmt.Rt.impl__new_display #u32 result <: Core.Fmt.Rt.t_Argument]
-                          in
-                          FStar.Pervasives.assert_norm (Prims.eq2 (List.Tot.length list) 1);
-                          Rust_primitives.Hax.array_of_list 1 list)
+                        args
                       <:
                       Core.Fmt.t_Arguments)
                 in
diff --git a/rustc-coverage-tests/snapshots/fstar/Coverage.Panic_unwind.fst b/rustc-coverage-tests/snapshots/fstar/Coverage.Panic_unwind.fst
index 635c1938a..8778578c1 100644
--- a/rustc-coverage-tests/snapshots/fstar/Coverage.Panic_unwind.fst
+++ b/rustc-coverage-tests/snapshots/fstar/Coverage.Panic_unwind.fst
@@ -7,7 +7,7 @@ let might_panic (should_panic: bool) : Prims.unit =
   if should_panic
   then
     let _:Prims.unit =
-      Std.Io.Stdio.e_print (Core.Fmt.Rt.impl_2__new_const (mk_usize 1)
+      Std.Io.Stdio.e_print (Core.Fmt.Rt.impl_1__new_const (mk_usize 1)
             (let list = ["panicking...\n"] in
               FStar.Pervasives.assert_norm (Prims.eq2 (List.Tot.length list) 1);
               Rust_primitives.Hax.array_of_list 1 list)
@@ -15,7 +15,7 @@ let might_panic (should_panic: bool) : Prims.unit =
           Core.Fmt.t_Arguments)
     in
     let _:Prims.unit = () in
-    Rust_primitives.Hax.never_to_any (Core.Panicking.panic_fmt (Core.Fmt.Rt.impl_2__new_const (mk_usize
+    Rust_primitives.Hax.never_to_any (Core.Panicking.panic_fmt (Core.Fmt.Rt.impl_1__new_const (mk_usize
                 1)
               (let list = ["panics"] in
                 FStar.Pervasives.assert_norm (Prims.eq2 (List.Tot.length list) 1);
@@ -26,7 +26,7 @@ let might_panic (should_panic: bool) : Prims.unit =
         Rust_primitives.Hax.t_Never)
   else
     let _:Prims.unit =
-      Std.Io.Stdio.e_print (Core.Fmt.Rt.impl_2__new_const (mk_usize 1)
+      Std.Io.Stdio.e_print (Core.Fmt.Rt.impl_1__new_const (mk_usize 1)
             (let list = ["Don't Panic\n"] in
               FStar.Pervasives.assert_norm (Prims.eq2 (List.Tot.length list) 1);
               Rust_primitives.Hax.array_of_list 1 list)
diff --git a/rustc-coverage-tests/snapshots/fstar/Coverage.Partial_eq.fst b/rustc-coverage-tests/snapshots/fstar/Coverage.Partial_eq.fst
index d8ec281f8..6f6313509 100644
--- a/rustc-coverage-tests/snapshots/fstar/Coverage.Partial_eq.fst
+++ b/rustc-coverage-tests/snapshots/fstar/Coverage.Partial_eq.fst
@@ -59,30 +59,35 @@ let impl_Version__new (major minor patch: usize) : t_Version =
 let main (_: Prims.unit) : Prims.unit =
   let version_3_2_1_:t_Version = impl_Version__new (mk_usize 3) (mk_usize 2) (mk_usize 1) in
   let version_3_3_0_:t_Version = impl_Version__new (mk_usize 3) (mk_usize 3) (mk_usize 0) in
+  let args:(t_Version & t_Version & bool) =
+    version_3_2_1_,
+    version_3_3_0_,
+    Core.Cmp.f_lt #t_Version
+      #t_Version
+      #FStar.Tactics.Typeclasses.solve
+      version_3_2_1_
+      version_3_3_0_
+    <:
+    (t_Version & t_Version & bool)
+  in
+  let args:t_Array Core.Fmt.Rt.t_Argument (mk_usize 3) =
+    let list =
+      [
+        Core.Fmt.Rt.impl__new_debug #t_Version args._1;
+        Core.Fmt.Rt.impl__new_debug #t_Version args._2;
+        Core.Fmt.Rt.impl__new_display #bool args._3
+      ]
+    in
+    FStar.Pervasives.assert_norm (Prims.eq2 (List.Tot.length list) 3);
+    Rust_primitives.Hax.array_of_list 3 list
+  in
   let _:Prims.unit =
-    Std.Io.Stdio.e_print (Core.Fmt.Rt.impl_2__new_v1 (mk_usize 4)
+    Std.Io.Stdio.e_print (Core.Fmt.Rt.impl_1__new_v1 (mk_usize 4)
           (mk_usize 3)
           (let list = [""; " < "; " = "; "\n"] in
             FStar.Pervasives.assert_norm (Prims.eq2 (List.Tot.length list) 4);
             Rust_primitives.Hax.array_of_list 4 list)
-          (let list =
-              [
-                Core.Fmt.Rt.impl__new_debug #t_Version version_3_2_1_ <: Core.Fmt.Rt.t_Argument;
-                Core.Fmt.Rt.impl__new_debug #t_Version version_3_3_0_ <: Core.Fmt.Rt.t_Argument;
-                Core.Fmt.Rt.impl__new_display #bool
-                  (Core.Cmp.f_lt #t_Version
-                      #t_Version
-                      #FStar.Tactics.Typeclasses.solve
-                      version_3_2_1_
-                      version_3_3_0_
-                    <:
-                    bool)
-                <:
-                Core.Fmt.Rt.t_Argument
-              ]
-            in
-            FStar.Pervasives.assert_norm (Prims.eq2 (List.Tot.length list) 3);
-            Rust_primitives.Hax.array_of_list 3 list)
+          args
         <:
         Core.Fmt.t_Arguments)
   in
diff --git a/rustc-coverage-tests/snapshots/fstar/Coverage.Sort_groups.fst b/rustc-coverage-tests/snapshots/fstar/Coverage.Sort_groups.fst
index a19adfc3c..c1ad4d15d 100644
--- a/rustc-coverage-tests/snapshots/fstar/Coverage.Sort_groups.fst
+++ b/rustc-coverage-tests/snapshots/fstar/Coverage.Sort_groups.fst
@@ -12,21 +12,18 @@ let _ =
 let generic_fn (#v_T: Type0) (cond: bool) : Prims.unit =
   if cond
   then
+    let args:t_Array Core.Fmt.Rt.t_Argument (mk_usize 1) =
+      let list = [Core.Fmt.Rt.impl__new_display #string (Core.Any.type_name #v_T () <: string)] in
+      FStar.Pervasives.assert_norm (Prims.eq2 (List.Tot.length list) 1);
+      Rust_primitives.Hax.array_of_list 1 list
+    in
     let _:Prims.unit =
-      Std.Io.Stdio.e_print (Core.Fmt.Rt.impl_2__new_v1 (mk_usize 2)
+      Std.Io.Stdio.e_print (Core.Fmt.Rt.impl_1__new_v1 (mk_usize 2)
             (mk_usize 1)
             (let list = [""; "\n"] in
               FStar.Pervasives.assert_norm (Prims.eq2 (List.Tot.length list) 2);
               Rust_primitives.Hax.array_of_list 2 list)
-            (let list =
-                [
-                  Core.Fmt.Rt.impl__new_display #string (Core.Any.type_name #v_T () <: string)
-                  <:
-                  Core.Fmt.Rt.t_Argument
-                ]
-              in
-              FStar.Pervasives.assert_norm (Prims.eq2 (List.Tot.length list) 1);
-              Rust_primitives.Hax.array_of_list 1 list)
+            args
           <:
           Core.Fmt.t_Arguments)
     in
diff --git a/rustc-coverage-tests/snapshots/fstar/Coverage.Unused_mod.Unused_module.fst b/rustc-coverage-tests/snapshots/fstar/Coverage.Unused_mod.Unused_module.fst
index 238db510e..0ceffc9d5 100644
--- a/rustc-coverage-tests/snapshots/fstar/Coverage.Unused_mod.Unused_module.fst
+++ b/rustc-coverage-tests/snapshots/fstar/Coverage.Unused_mod.Unused_module.fst
@@ -5,7 +5,7 @@ open FStar.Mul
 
 let never_called_function (_: Prims.unit) : Prims.unit =
   let _:Prims.unit =
-    Std.Io.Stdio.e_print (Core.Fmt.Rt.impl_2__new_const (mk_usize 1)
+    Std.Io.Stdio.e_print (Core.Fmt.Rt.impl_1__new_const (mk_usize 1)
           (let list = ["I am never called\n"] in
             FStar.Pervasives.assert_norm (Prims.eq2 (List.Tot.length list) 1);
             Rust_primitives.Hax.array_of_list 1 list)
diff --git a/rustc-coverage-tests/snapshots/fstar/Coverage.Unused_mod.fst b/rustc-coverage-tests/snapshots/fstar/Coverage.Unused_mod.fst
index 654c155ce..a54b35f14 100644
--- a/rustc-coverage-tests/snapshots/fstar/Coverage.Unused_mod.fst
+++ b/rustc-coverage-tests/snapshots/fstar/Coverage.Unused_mod.fst
@@ -5,7 +5,7 @@ open FStar.Mul
 
 let main (_: Prims.unit) : Prims.unit =
   let _:Prims.unit =
-    Std.Io.Stdio.e_print (Core.Fmt.Rt.impl_2__new_const (mk_usize 1)
+    Std.Io.Stdio.e_print (Core.Fmt.Rt.impl_1__new_const (mk_usize 1)
           (let list = ["hello world!\n"] in
             FStar.Pervasives.assert_norm (Prims.eq2 (List.Tot.length list) 1);
             Rust_primitives.Hax.array_of_list 1 list)

From 75546c39c5ff89dc3b15f993c1ffa2e0d277e936 Mon Sep 17 00:00:00 2001
From: Nadrieril <nadrieril+git@gmail.com>
Date: Wed, 9 Jul 2025 11:28:24 +0200
Subject: [PATCH 08/18] Update rustc again

---
 engine/lib/import_thir.ml             |  2 --
 frontend/exporter/Cargo.toml          |  2 +-
 frontend/exporter/src/lib.rs          |  1 -
 frontend/exporter/src/types/def_id.rs |  9 +++++++++
 frontend/exporter/src/types/hir.rs    |  4 ++--
 frontend/exporter/src/types/ty.rs     | 21 ++++++++++++---------
 rust-toolchain.toml                   |  2 +-
 7 files changed, 25 insertions(+), 16 deletions(-)

diff --git a/engine/lib/import_thir.ml b/engine/lib/import_thir.ml
index fb2277eef..a9751c2aa 100644
--- a/engine/lib/import_thir.ml
+++ b/engine/lib/import_thir.ml
@@ -1105,8 +1105,6 @@ end) : EXPR = struct
         match non_traits with
         | [] -> TDyn { witness = W.dyn; goals }
         | _ -> assertion_failure [ span ] "type Dyn with non trait predicate")
-    | Dynamic (_, _, DynStar) ->
-        unimplemented ~issue_id:931 [ span ] "type DynStar"
     | Coroutine _ ->
         unimplemented ~issue_id:924 [ span ]
           "Got type `Coroutine`: coroutines are not supported by hax"
diff --git a/frontend/exporter/Cargo.toml b/frontend/exporter/Cargo.toml
index 35ed4c09a..f19eb4381 100644
--- a/frontend/exporter/Cargo.toml
+++ b/frontend/exporter/Cargo.toml
@@ -1,10 +1,10 @@
 [package]
 name = "hax-frontend-exporter"
+edition = "2024"
 version.workspace = true
 authors.workspace = true
 license.workspace = true
 homepage.workspace = true
-edition.workspace = true
 repository.workspace = true
 readme.workspace = true
 description = "Provides mirrors of the algebraic data types used in the Rust compilers, removing indirections and inlining various pieces of information."
diff --git a/frontend/exporter/src/lib.rs b/frontend/exporter/src/lib.rs
index a4c851910..ef6af0388 100644
--- a/frontend/exporter/src/lib.rs
+++ b/frontend/exporter/src/lib.rs
@@ -1,6 +1,5 @@
 #![allow(rustdoc::private_intra_doc_links)]
 #![cfg_attr(feature = "rustc", feature(if_let_guard))]
-#![cfg_attr(feature = "rustc", feature(let_chains))]
 #![cfg_attr(feature = "rustc", feature(macro_metavar_expr))]
 #![cfg_attr(feature = "rustc", feature(rustc_private))]
 #![cfg_attr(feature = "rustc", feature(sized_hierarchy))]
diff --git a/frontend/exporter/src/types/def_id.rs b/frontend/exporter/src/types/def_id.rs
index c0a10edc5..14196789c 100644
--- a/frontend/exporter/src/types/def_id.rs
+++ b/frontend/exporter/src/types/def_id.rs
@@ -21,6 +21,8 @@ use crate::{AdtInto, JsonSchema};
 use {rustc_hir as hir, rustc_hir::def_id::DefId as RDefId, rustc_middle::ty};
 
 pub type Symbol = String;
+#[cfg(not(feature = "extract_names_mode"))]
+pub type ByteSymbol = Vec<u8>;
 
 #[cfg(all(not(feature = "extract_names_mode"), feature = "rustc"))]
 impl<'t, S> SInto<S, Symbol> for rustc_span::symbol::Symbol {
@@ -29,6 +31,13 @@ impl<'t, S> SInto<S, Symbol> for rustc_span::symbol::Symbol {
     }
 }
 
+#[cfg(all(not(feature = "extract_names_mode"), feature = "rustc"))]
+impl<'t, S> SInto<S, ByteSymbol> for rustc_span::symbol::ByteSymbol {
+    fn sinto(&self, _s: &S) -> ByteSymbol {
+        self.as_byte_str().to_owned()
+    }
+}
+
 /// Reflects [`hir::Safety`]
 #[cfg_attr(not(feature = "extract_names_mode"), derive(AdtInto, JsonSchema))]
 #[cfg_attr(not(feature = "extract_names_mode"), args(<S>, from: hir::Safety, state: S as _s))]
diff --git a/frontend/exporter/src/types/hir.rs b/frontend/exporter/src/types/hir.rs
index 2a80a7837..3e38ef9a3 100644
--- a/frontend/exporter/src/types/hir.rs
+++ b/frontend/exporter/src/types/hir.rs
@@ -1051,8 +1051,8 @@ pub enum StrStyle {
 #[derive(Clone, Debug, JsonSchema, Hash, PartialEq, Eq, PartialOrd, Ord)]
 pub enum LitKind {
     Str(Symbol, StrStyle),
-    ByteStr(Vec<u8>, StrStyle),
-    CStr(Vec<u8>, StrStyle),
+    ByteStr(ByteSymbol, StrStyle),
+    CStr(ByteSymbol, StrStyle),
     Byte(u8),
     Char(char),
     Int(
diff --git a/frontend/exporter/src/types/ty.rs b/frontend/exporter/src/types/ty.rs
index 49c9f2651..a1b71c76e 100644
--- a/frontend/exporter/src/types/ty.rs
+++ b/frontend/exporter/src/types/ty.rs
@@ -94,22 +94,22 @@ pub struct ExistentialProjection {
 #[args(<S>, from: ty::DynKind, state: S as _s)]
 pub enum DynKind {
     Dyn,
-    DynStar,
 }
 
 /// Reflects [`ty::BoundTyKind`]
 #[derive_group(Serializers)]
 #[derive(AdtInto, Clone, Debug, JsonSchema, Hash, PartialEq, Eq, PartialOrd, Ord)]
-#[args(<'tcx, S: UnderOwnerState<'tcx>>, from: ty::BoundTyKind, state: S as gstate)]
+#[args(<'tcx, S: UnderOwnerState<'tcx>>, from: ty::BoundTyKind, state: S as s)]
 pub enum BoundTyKind {
     Anon,
+    #[custom_arm(&FROM_TYPE::Param(def_id) => TO_TYPE::Param(def_id.sinto(s), s.base().tcx.item_name(def_id).sinto(s)),)]
     Param(DefId, Symbol),
 }
 
 /// Reflects [`ty::BoundTy`]
 #[derive_group(Serializers)]
 #[derive(AdtInto, Clone, Debug, JsonSchema, Hash, PartialEq, Eq, PartialOrd, Ord)]
-#[args(<'tcx, S: UnderOwnerState<'tcx>>, from: ty::BoundTy, state: S as gstate)]
+#[args(<'tcx, S: UnderOwnerState<'tcx>>, from: ty::BoundTy, state: S as s)]
 pub struct BoundTy {
     pub var: BoundVar,
     pub kind: BoundTyKind,
@@ -120,9 +120,11 @@ sinto_as_usize!(rustc_middle::ty, BoundVar);
 /// Reflects [`ty::BoundRegionKind`]
 #[derive_group(Serializers)]
 #[derive(AdtInto, Clone, Debug, JsonSchema, Hash, PartialEq, Eq, PartialOrd, Ord)]
-#[args(<'tcx, S: UnderOwnerState<'tcx>>, from: ty::BoundRegionKind, state: S as gstate)]
+#[args(<'tcx, S: UnderOwnerState<'tcx>>, from: ty::BoundRegionKind, state: S as s)]
 pub enum BoundRegionKind {
     Anon,
+    NamedAnon(Symbol),
+    #[custom_arm(&FROM_TYPE::Named(def_id) => TO_TYPE::Named(def_id.sinto(s), s.base().tcx.item_name(def_id).sinto(s)),)]
     Named(DefId, Symbol),
     ClosureEnv,
 }
@@ -130,7 +132,7 @@ pub enum BoundRegionKind {
 /// Reflects [`ty::BoundRegion`]
 #[derive_group(Serializers)]
 #[derive(AdtInto, Clone, Debug, JsonSchema, Hash, PartialEq, Eq, PartialOrd, Ord)]
-#[args(<'tcx, S: UnderOwnerState<'tcx>>, from: ty::BoundRegion, state: S as gstate)]
+#[args(<'tcx, S: UnderOwnerState<'tcx>>, from: ty::BoundRegion, state: S as s)]
 pub struct BoundRegion {
     pub var: BoundVar,
     pub kind: BoundRegionKind,
@@ -370,7 +372,7 @@ impl VariantDef {
 /// Reflects [`ty::EarlyParamRegion`]
 #[derive_group(Serializers)]
 #[derive(AdtInto, Clone, Debug, JsonSchema, Hash, PartialEq, Eq, PartialOrd, Ord)]
-#[args(<'tcx, S: UnderOwnerState<'tcx>>, from: ty::EarlyParamRegion, state: S as gstate)]
+#[args(<'tcx, S: UnderOwnerState<'tcx>>, from: ty::EarlyParamRegion, state: S as s)]
 pub struct EarlyParamRegion {
     pub index: u32,
     pub name: Symbol,
@@ -379,7 +381,7 @@ pub struct EarlyParamRegion {
 /// Reflects [`ty::LateParamRegion`]
 #[derive_group(Serializers)]
 #[derive(AdtInto, Clone, Debug, JsonSchema, Hash, PartialEq, Eq, PartialOrd, Ord)]
-#[args(<'tcx, S: UnderOwnerState<'tcx>>, from: ty::LateParamRegion, state: S as gstate)]
+#[args(<'tcx, S: UnderOwnerState<'tcx>>, from: ty::LateParamRegion, state: S as s)]
 pub struct LateParamRegion {
     pub scope: DefId,
     pub kind: LateParamRegionKind,
@@ -388,9 +390,11 @@ pub struct LateParamRegion {
 /// Reflects [`ty::LateParamRegionKind`]
 #[derive_group(Serializers)]
 #[derive(AdtInto, Clone, Debug, JsonSchema, Hash, PartialEq, Eq, PartialOrd, Ord)]
-#[args(<'tcx, S: UnderOwnerState<'tcx>>, from: ty::LateParamRegionKind, state: S as gstate)]
+#[args(<'tcx, S: UnderOwnerState<'tcx>>, from: ty::LateParamRegionKind, state: S as s)]
 pub enum LateParamRegionKind {
     Anon(u32),
+    NamedAnon(u32, Symbol),
+    #[custom_arm(&FROM_TYPE::Named(def_id) => TO_TYPE::Named(def_id.sinto(s), s.base().tcx.item_name(def_id).sinto(s)),)]
     Named(DefId, Symbol),
     ClosureEnv,
 }
@@ -1078,7 +1082,6 @@ pub enum PointerCoercion {
     ClosureFnPointer(Safety),
     MutToConstPointer,
     ArrayToPointer,
-    DynStar,
     Unsize,
 }
 
diff --git a/rust-toolchain.toml b/rust-toolchain.toml
index 3a87a82e7..1f96d2c9e 100644
--- a/rust-toolchain.toml
+++ b/rust-toolchain.toml
@@ -1,3 +1,3 @@
 [toolchain]
-channel = "nightly-2025-06-30"
+channel = "nightly-2025-07-08"
 components = [ "rustc-dev", "llvm-tools-preview" , "rust-analysis" , "rust-src" , "rustfmt" ]

From fc5af673c131d1c054b8132b1f2df1a2936b588c Mon Sep 17 00:00:00 2001
From: Nadrieril <nadrieril+git@gmail.com>
Date: Mon, 21 Jul 2025 14:34:38 +0200
Subject: [PATCH 09/18] Update rustc again

---
 engine/lib/import_thir.ml                   |  6 +++--
 frontend/exporter/src/comments.rs           |  2 +-
 frontend/exporter/src/sinto.rs              | 16 ------------
 frontend/exporter/src/types/hir.rs          | 28 +++++++--------------
 frontend/exporter/src/types/mod.rs          |  3 ---
 frontend/exporter/src/types/new/full_def.rs |  2 +-
 frontend/exporter/src/types/ty.rs           |  3 +--
 rust-toolchain.toml                         |  2 +-
 8 files changed, 17 insertions(+), 45 deletions(-)

diff --git a/engine/lib/import_thir.ml b/engine/lib/import_thir.ml
index a9751c2aa..30dbc12b7 100644
--- a/engine/lib/import_thir.ml
+++ b/engine/lib/import_thir.ml
@@ -1641,7 +1641,7 @@ and c_item_unwrapped ~ident ~type_only (item : Thir.item) : item list =
       let variants = [ v ] in
       let name = Concrete_ident.of_def_id ~value:false def_id in
       mk @@ Type { name; generics; variants; is_struct }
-  | Trait (No, safety, _, generics, _bounds, items) ->
+  | Trait (NotConst, No, safety, _, generics, _bounds, items) ->
       let items =
         List.filter
           ~f:(fun { attributes; _ } -> not (should_skip attributes))
@@ -1664,8 +1664,10 @@ and c_item_unwrapped ~ident ~type_only (item : Thir.item) : item list =
       let items = List.map ~f:c_trait_item items in
       let safety = csafety safety in
       mk @@ Trait { name; generics; items; safety }
-  | Trait (Yes, _, _, _, _, _) ->
+  | Trait (_, Yes, _, _, _, _, _) ->
       unimplemented ~issue_id:930 [ item.span ] "Auto trait"
+  | Trait (Const, _, _, _, _, _, _) ->
+      unimplemented ~issue_id:930 [ item.span ] "Const trait"
   | Impl { of_trait = None; generics; items; _ } ->
       let items =
         List.filter
diff --git a/frontend/exporter/src/comments.rs b/frontend/exporter/src/comments.rs
index 0baecd941..08bfcc102 100644
--- a/frontend/exporter/src/comments.rs
+++ b/frontend/exporter/src/comments.rs
@@ -21,7 +21,7 @@ pub fn comments_of_file(path: PathBuf) -> std::io::Result<Vec<(Span, String)>> {
 
     let mut comments = vec![];
     let (mut pos, mut line, mut col) = (0, 0, 0);
-    for token in rustc_lexer::tokenize(source) {
+    for token in rustc_lexer::tokenize(source, rustc_lexer::FrontmatterAllowed::Yes) {
         let len = token.len as usize;
         let sub = &source[pos..(pos + len)];
         let lo = Loc { line, col };
diff --git a/frontend/exporter/src/sinto.rs b/frontend/exporter/src/sinto.rs
index 15d65f66b..3e775ceac 100644
--- a/frontend/exporter/src/sinto.rs
+++ b/frontend/exporter/src/sinto.rs
@@ -1,5 +1,3 @@
-use crate::prelude::{derive_group, JsonSchema};
-
 #[cfg(not(feature = "rustc"))]
 pub trait SInto<S, To> {
     fn sinto(&self, s: &S) -> To;
@@ -45,20 +43,6 @@ macro_rules! sinto_as_usize {
     }
 }
 
-#[allow(dead_code)]
-mod test {
-    #[derive(Debug)]
-    pub struct Foo(usize);
-    impl Foo {
-        pub fn as_usize(&self) -> usize {
-            self.0
-        }
-    }
-}
-
-sinto_todo!(test, Foo);
-// sinto_as_usize!(test, Foo);
-
 impl<S, LL, RR, L: SInto<S, LL>, R: SInto<S, RR>> SInto<S, (LL, RR)> for (L, R) {
     fn sinto(&self, s: &S) -> (LL, RR) {
         (self.0.sinto(s), self.1.sinto(s))
diff --git a/frontend/exporter/src/types/hir.rs b/frontend/exporter/src/types/hir.rs
index 3e38ef9a3..188b96ef8 100644
--- a/frontend/exporter/src/types/hir.rs
+++ b/frontend/exporter/src/types/hir.rs
@@ -225,10 +225,10 @@ pub struct Generics<Body: IsBody> {
 }
 
 #[cfg(feature = "rustc")]
-impl<'tcx, S: UnderOwnerState<'tcx>, Body: IsBody> SInto<S, ImplItem<Body>> for hir::ImplItemRef {
+impl<'tcx, S: UnderOwnerState<'tcx>, Body: IsBody> SInto<S, ImplItem<Body>> for hir::ImplItemId {
     fn sinto(&self, s: &S) -> ImplItem<Body> {
         let tcx: rustc_middle::ty::TyCtxt = s.base().tcx;
-        let impl_item = tcx.hir_impl_item(self.id);
+        let impl_item = tcx.hir_impl_item(*self);
         let s = with_owner_id(s.base(), (), (), impl_item.owner_id.to_def_id());
         impl_item.sinto(&s)
     }
@@ -393,17 +393,6 @@ pub enum ImplItemKind<Body: IsBody> {
     },
 }
 
-/// Reflects [`hir::AssocItemKind`]
-#[derive(AdtInto)]
-#[args(<'tcx, S: UnderOwnerState<'tcx>>, from: hir::AssocItemKind, state: S as tcx)]
-#[derive_group(Serializers)]
-#[derive(Clone, Debug, JsonSchema)]
-pub enum AssocItemKind {
-    Const,
-    Fn { has_self: bool },
-    Type,
-}
-
 /// Reflects [`hir::Impl`].
 #[derive(AdtInto)]
 #[args(<'tcx, S: UnderOwnerState<'tcx> >, from: hir::Impl<'tcx>, state: S as s)]
@@ -674,6 +663,7 @@ pub enum ItemKind<Body: IsBody> {
     Struct(Ident, Generics<Body>, VariantData),
     Union(Ident, Generics<Body>, VariantData),
     Trait(
+        Constness,
         IsAuto,
         Safety,
         Ident,
@@ -741,11 +731,11 @@ impl<'tcx, S: UnderOwnerState<'tcx>, Body: IsBody> SInto<S, EnumDef<Body>> for h
 }
 
 #[cfg(feature = "rustc")]
-impl<'a, S: UnderOwnerState<'a>, Body: IsBody> SInto<S, TraitItem<Body>> for hir::TraitItemRef {
+impl<'a, S: UnderOwnerState<'a>, Body: IsBody> SInto<S, TraitItem<Body>> for hir::TraitItemId {
     fn sinto(&self, s: &S) -> TraitItem<Body> {
-        let s = with_owner_id(s.base(), (), (), self.id.owner_id.to_def_id());
+        let s = with_owner_id(s.base(), (), (), self.owner_id.to_def_id());
         let tcx: rustc_middle::ty::TyCtxt = s.base().tcx;
-        tcx.hir_trait_item(self.id).sinto(&s)
+        tcx.hir_trait_item(*self).sinto(&s)
     }
 }
 
@@ -785,10 +775,10 @@ pub struct ForeignItem<Body: IsBody> {
 }
 
 #[cfg(feature = "rustc")]
-impl<'a, S: UnderOwnerState<'a>, Body: IsBody> SInto<S, ForeignItem<Body>> for hir::ForeignItemRef {
+impl<'a, S: UnderOwnerState<'a>, Body: IsBody> SInto<S, ForeignItem<Body>> for hir::ForeignItemId {
     fn sinto(&self, s: &S) -> ForeignItem<Body> {
         let tcx: rustc_middle::ty::TyCtxt = s.base().tcx;
-        tcx.hir_foreign_item(self.id).sinto(s)
+        tcx.hir_foreign_item(*self).sinto(s)
     }
 }
 
@@ -925,7 +915,7 @@ impl<'tcx, S: BaseState<'tcx>, Body: IsBody> SInto<S, Item<Body>> for hir::Item<
             | Enum(i, ..)
             | Struct(i, ..)
             | Union(i, ..)
-            | Trait(_, _, i, ..)
+            | Trait(_, _, _, i, ..)
             | TraitAlias(i, ..) => i.name.to_ident_string(),
             Use(..) | ForeignMod { .. } | GlobalAsm { .. } | Impl { .. } => String::new(),
         };
diff --git a/frontend/exporter/src/types/mod.rs b/frontend/exporter/src/types/mod.rs
index e70f2ce3c..51d089708 100644
--- a/frontend/exporter/src/types/mod.rs
+++ b/frontend/exporter/src/types/mod.rs
@@ -1,6 +1,3 @@
-// There's a conflict between `mir::ScalarInt`and `todo::ScalarInt` but it doesn't matter.
-#![allow(ambiguous_glob_reexports)]
-
 mod def_id;
 mod hir;
 mod mir;
diff --git a/frontend/exporter/src/types/new/full_def.rs b/frontend/exporter/src/types/new/full_def.rs
index 91a3e49a9..953d4f0fb 100644
--- a/frontend/exporter/src/types/new/full_def.rs
+++ b/frontend/exporter/src/types/new/full_def.rs
@@ -735,7 +735,7 @@ fn get_foreign_mod_children<'tcx>(tcx: ty::TyCtxt<'tcx>, def_id: RDefId) -> Vec<
             .expect_foreign_mod()
             .1
             .iter()
-            .map(|foreign_item_ref| foreign_item_ref.id.owner_id.to_def_id())
+            .map(|foreign_item_ref| foreign_item_ref.owner_id.to_def_id())
             .collect(),
         None => vec![],
     }
diff --git a/frontend/exporter/src/types/ty.rs b/frontend/exporter/src/types/ty.rs
index a1b71c76e..bf71fb173 100644
--- a/frontend/exporter/src/types/ty.rs
+++ b/frontend/exporter/src/types/ty.rs
@@ -1085,8 +1085,6 @@ pub enum PointerCoercion {
     Unsize,
 }
 
-sinto_todo!(rustc_middle::ty, ScalarInt);
-
 /// Reflects [`ty::FnSig`]
 #[derive_group(Serializers)]
 #[derive(AdtInto, Clone, Debug, JsonSchema, Hash, PartialEq, Eq, PartialOrd, Ord)]
@@ -1231,6 +1229,7 @@ pub enum ClauseKind {
     WellFormed(Term),
     ConstEvaluatable(ConstantExpr),
     HostEffect(HostEffectPredicate),
+    UnstableFeature(Symbol),
 }
 
 sinto_todo!(rustc_middle::ty, HostEffectPredicate<'tcx>);
diff --git a/rust-toolchain.toml b/rust-toolchain.toml
index 1f96d2c9e..5cadcd938 100644
--- a/rust-toolchain.toml
+++ b/rust-toolchain.toml
@@ -1,3 +1,3 @@
 [toolchain]
-channel = "nightly-2025-07-08"
+channel = "nightly-2025-07-20"
 components = [ "rustc-dev", "llvm-tools-preview" , "rust-analysis" , "rust-src" , "rustfmt" ]

From e2b90fc63f803dc9521dff4aa189d5f48dcd598e Mon Sep 17 00:00:00 2001
From: Nadrieril <nadrieril+git@gmail.com>
Date: Mon, 21 Jul 2025 14:42:39 +0200
Subject: [PATCH 10/18] Remove charon CI job

Charon uses its own fork of hax for the time being.
---
 .github/workflows/charon.yml | 17 -----------------
 1 file changed, 17 deletions(-)
 delete mode 100644 .github/workflows/charon.yml

diff --git a/.github/workflows/charon.yml b/.github/workflows/charon.yml
deleted file mode 100644
index bda7df442..000000000
--- a/.github/workflows/charon.yml
+++ /dev/null
@@ -1,17 +0,0 @@
-on:
-  pull_request:
-  workflow_dispatch:
-
-jobs:
-  charon:
-    runs-on: ubuntu-latest
-    steps:
-      - uses: DeterminateSystems/nix-installer-action@main
-      - uses: actions/checkout@v4
-        with:
-          repository: AeneasVerif/charon
-      - run: |
-          cd charon
-          cargo update -p hax-frontend-exporter --precise ${{ github.sha }}
-          cargo update -p hax-frontend-exporter-options --precise ${{ github.sha }}
-      - run: nix build -L

From 1a071ac870521ad784267f479e295d097d44db5a Mon Sep 17 00:00:00 2001
From: Lucas Franceschino <lucas@cryspen.com>
Date: Mon, 21 Jul 2025 14:48:55 +0200
Subject: [PATCH 11/18] chore: dune fmt

---
 engine/lib/phases/phase_drop_metasized.ml  | 3 ++-
 engine/lib/phases/phase_drop_metasized.mli | 3 ++-
 2 files changed, 4 insertions(+), 2 deletions(-)

diff --git a/engine/lib/phases/phase_drop_metasized.ml b/engine/lib/phases/phase_drop_metasized.ml
index 781b15aa0..5e1ebd77d 100644
--- a/engine/lib/phases/phase_drop_metasized.ml
+++ b/engine/lib/phases/phase_drop_metasized.ml
@@ -1,4 +1,5 @@
-(** This phase gets rid of the MetaSized bound. See https://github.com/cryspen/hax/pull/1534. *)
+(** This phase gets rid of the MetaSized bound. See
+    https://github.com/cryspen/hax/pull/1534. *)
 
 open! Prelude
 
diff --git a/engine/lib/phases/phase_drop_metasized.mli b/engine/lib/phases/phase_drop_metasized.mli
index 97a1d8598..01bb072cc 100644
--- a/engine/lib/phases/phase_drop_metasized.mli
+++ b/engine/lib/phases/phase_drop_metasized.mli
@@ -1,4 +1,5 @@
-(** This phase gets rid of the MetaSized bound. See https://github.com/cryspen/hax/pull/1534. *)
+(** This phase gets rid of the MetaSized bound. See
+    https://github.com/cryspen/hax/pull/1534. *)
 
 open! Prelude
 

From 7a8bb9b806337242c6188fb69b3222b5b84af255 Mon Sep 17 00:00:00 2001
From: Nadrieril <nadrieril+git@gmail.com>
Date: Mon, 21 Jul 2025 14:53:57 +0200
Subject: [PATCH 12/18] Update test outputs

---
 .../toolchain__attributes into-fstar.snap     | 206 ++++++++++++------
 .../toolchain__lean-tests into-lean.snap      |  44 +---
 .../toolchain__literals into-coq.snap         |  40 +++-
 .../toolchain__literals into-fstar.snap       |  55 +++--
 4 files changed, 221 insertions(+), 124 deletions(-)

diff --git a/test-harness/src/snapshots/toolchain__attributes into-fstar.snap b/test-harness/src/snapshots/toolchain__attributes into-fstar.snap
index 4b29f6b9a..e9e8f1d58 100644
--- a/test-harness/src/snapshots/toolchain__attributes into-fstar.snap	
+++ b/test-harness/src/snapshots/toolchain__attributes into-fstar.snap	
@@ -20,10 +20,27 @@ info:
     include_flag: ~
     backend_options: ~
 ---
-exit = 0
-
-[stdout]
-diagnostics = []
+exit = 1
+[[stdout.diagnostics]]
+message = '''
+(AST import) something is not implemented yet.This is discussed in issue https://github.com/hacspec/hax/issues/156.
+Please upvote or comment this issue if you see this error message.
+Sorry, Hax does not support declare-first let bindings (see https://doc.rust-lang.org/rust-by-example/variable_bindings/declare.html) for now.'''
+spans = ['Span { lo: Loc { line: 301, col: 17 }, hi: Loc { line: 301, col: 22 }, filename: Real(LocalPath("/home/nadrieril/wip/work/hax/hax-bounded-integers/src/lib.rs")), rust_span_data: None }']
+
+[[stdout.diagnostics]]
+message = '''
+(AST import) something is not implemented yet.This is discussed in issue https://github.com/hacspec/hax/issues/156.
+Please upvote or comment this issue if you see this error message.
+Sorry, Hax does not support declare-first let bindings (see https://doc.rust-lang.org/rust-by-example/variable_bindings/declare.html) for now.'''
+spans = ['Span { lo: Loc { line: 301, col: 30 }, hi: Loc { line: 301, col: 32 }, filename: Real(LocalPath("/home/nadrieril/wip/work/hax/hax-bounded-integers/src/lib.rs")), rust_span_data: None }']
+
+[[stdout.diagnostics]]
+message = '''
+(AST import) something is not implemented yet.This is discussed in issue https://github.com/hacspec/hax/issues/156.
+Please upvote or comment this issue if you see this error message.
+Sorry, Hax does not support declare-first let bindings (see https://doc.rust-lang.org/rust-by-example/variable_bindings/declare.html) for now.'''
+spans = ['Span { lo: Loc { line: 295, col: 19 }, hi: Loc { line: 295, col: 24 }, filename: Real(LocalPath("attributes/src/lib.rs")), rust_span_data: None }']
 
 [stdout.files]
 "Attributes.Ensures_on_arity_zero_fns.fst" = '''
@@ -57,25 +74,24 @@ open FStar.Mul
 type t_Dummy = | Dummy : t_Dummy
 
 [@@ FStar.Tactics.Typeclasses.tcinstance]
-assume
-val impl_1': Core.Marker.t_StructuralPartialEq t_Dummy
-
-unfold
-let impl_1 = impl_1'
+let impl_1: Core.Marker.t_StructuralPartialEq t_Dummy = { __marker_trait = () }
 
 [@@ FStar.Tactics.Typeclasses.tcinstance]
-assume
-val impl_2': Core.Cmp.t_PartialEq t_Dummy t_Dummy
-
-unfold
-let impl_2 = impl_2'
+let impl_2: Core.Cmp.t_PartialEq t_Dummy t_Dummy =
+  {
+    f_eq_pre = (fun (self: t_Dummy) (other: t_Dummy) -> true);
+    f_eq_post = (fun (self: t_Dummy) (other: t_Dummy) (out: bool) -> true);
+    f_eq = fun (self: t_Dummy) (other: t_Dummy) -> true
+  }
 
 [@@ FStar.Tactics.Typeclasses.tcinstance]
-assume
-val impl': Core.Cmp.t_Eq t_Dummy
-
-unfold
-let impl = impl'
+let impl: Core.Cmp.t_Eq t_Dummy =
+  {
+    _super_5579681813951091494 = FStar.Tactics.Typeclasses.solve;
+    f_assert_receiver_is_total_eq_pre = (fun (self: t_Dummy) -> true);
+    f_assert_receiver_is_total_eq_post = (fun (self: t_Dummy) (out: Prims.unit) -> true);
+    f_assert_receiver_is_total_eq = fun (self: t_Dummy) -> ()
+  }
 
 let impl_Dummy__f (self: t_Dummy)
     : Prims.Pure t_Dummy
@@ -129,14 +145,21 @@ open FStar.Mul
 
 unfold type t_Int = int
 
-let impl_1: Core.Clone.t_Clone t_Int = { f_clone = (fun x -> x) }
-
 [@@ FStar.Tactics.Typeclasses.tcinstance]
-assume
-val impl': Core.Marker.t_Copy t_Int
+let impl_1: Core.Clone.t_Clone t_Int =
+  {
+    f_clone_pre = (fun (self: t_Int) -> true);
+    f_clone_post = (fun (self: t_Int) (out: t_Int) -> true);
+    f_clone
+    =
+    fun (self: t_Int) ->
+      Rust_primitives.Hax.failure "(AST import) something is not implemented yet.This is discussed in issue https://github.com/hacspec/hax/issues/156.\nPlease upvote or comment this issue if you see this error message.\nSorry, Hax does not support declare-first let bindings (see https://doc.rust-lang.org/rust-by-example/variable_bindings/declare.html) for now."
+        ""
+  }
 
-unfold
-let impl = impl'
+[@@ FStar.Tactics.Typeclasses.tcinstance]
+let impl: Core.Marker.t_Copy t_Int =
+  { _super_15837849249852401974 = FStar.Tactics.Typeclasses.solve }
 
 unfold let add x y = x + y
 
@@ -471,56 +494,117 @@ let t_BoundedAbsI16 (v_B: usize) =
       (Rust_primitives.Hax.Int.from_machine x <: Hax_lib.Int.t_Int) <=
       (Rust_primitives.Hax.Int.from_machine v_B <: Hax_lib.Int.t_Int) }
 
-let impl (v_B: usize) : Core.Clone.t_Clone (t_BoundedAbsI16 v_B) = { f_clone = (fun x -> x) }
-
 [@@ FStar.Tactics.Typeclasses.tcinstance]
-assume
-val impl_1': v_B: usize -> Core.Marker.t_Copy (t_BoundedAbsI16 v_B)
-
-unfold
-let impl_1 (v_B: usize) = impl_1' v_B
+let impl (v_B: usize) : Core.Clone.t_Clone (t_BoundedAbsI16 v_B) =
+  {
+    f_clone_pre = (fun (self: t_BoundedAbsI16 v_B) -> true);
+    f_clone_post = (fun (self: t_BoundedAbsI16 v_B) (out: t_BoundedAbsI16 v_B) -> true);
+    f_clone
+    =
+    fun (self: t_BoundedAbsI16 v_B) ->
+      Rust_primitives.Hax.failure "(AST import) something is not implemented yet.This is discussed in issue https://github.com/hacspec/hax/issues/156.\nPlease upvote or comment this issue if you see this error message.\nSorry, Hax does not support declare-first let bindings (see https://doc.rust-lang.org/rust-by-example/variable_bindings/declare.html) for now."
+        ""
+  }
 
 [@@ FStar.Tactics.Typeclasses.tcinstance]
-assume
-val impl_3': v_B: usize -> Core.Marker.t_StructuralPartialEq (t_BoundedAbsI16 v_B)
-
-unfold
-let impl_3 (v_B: usize) = impl_3' v_B
+let impl_1 (v_B: usize) : Core.Marker.t_Copy (t_BoundedAbsI16 v_B) =
+  { _super_15837849249852401974 = FStar.Tactics.Typeclasses.solve }
 
 [@@ FStar.Tactics.Typeclasses.tcinstance]
-assume
-val impl_4': v_B: usize -> Core.Cmp.t_PartialEq (t_BoundedAbsI16 v_B) (t_BoundedAbsI16 v_B)
-
-unfold
-let impl_4 (v_B: usize) = impl_4' v_B
+let impl_3 (v_B: usize) : Core.Marker.t_StructuralPartialEq (t_BoundedAbsI16 v_B) =
+  { __marker_trait = () }
 
 [@@ FStar.Tactics.Typeclasses.tcinstance]
-assume
-val impl_2': v_B: usize -> Core.Cmp.t_Eq (t_BoundedAbsI16 v_B)
-
-unfold
-let impl_2 (v_B: usize) = impl_2' v_B
+let impl_4 (v_B: usize) : Core.Cmp.t_PartialEq (t_BoundedAbsI16 v_B) (t_BoundedAbsI16 v_B) =
+  {
+    f_eq_pre = (fun (self: t_BoundedAbsI16 v_B) (other: t_BoundedAbsI16 v_B) -> true);
+    f_eq_post = (fun (self: t_BoundedAbsI16 v_B) (other: t_BoundedAbsI16 v_B) (out: bool) -> true);
+    f_eq = fun (self: t_BoundedAbsI16 v_B) (other: t_BoundedAbsI16 v_B) -> self._0 =. other._0
+  }
 
 [@@ FStar.Tactics.Typeclasses.tcinstance]
-assume
-val impl_6': v_B: usize -> Core.Cmp.t_PartialOrd (t_BoundedAbsI16 v_B) (t_BoundedAbsI16 v_B)
-
-unfold
-let impl_6 (v_B: usize) = impl_6' v_B
+let impl_2 (v_B: usize) : Core.Cmp.t_Eq (t_BoundedAbsI16 v_B) =
+  {
+    _super_5579681813951091494 = FStar.Tactics.Typeclasses.solve;
+    f_assert_receiver_is_total_eq_pre = (fun (self: t_BoundedAbsI16 v_B) -> true);
+    f_assert_receiver_is_total_eq_post = (fun (self: t_BoundedAbsI16 v_B) (out: Prims.unit) -> true);
+    f_assert_receiver_is_total_eq
+    =
+    fun (self: t_BoundedAbsI16 v_B) ->
+      Rust_primitives.Hax.failure "(AST import) something is not implemented yet.This is discussed in issue https://github.com/hacspec/hax/issues/156.\nPlease upvote or comment this issue if you see this error message.\nSorry, Hax does not support declare-first let bindings (see https://doc.rust-lang.org/rust-by-example/variable_bindings/declare.html) for now."
+        ""
+  }
 
 [@@ FStar.Tactics.Typeclasses.tcinstance]
-assume
-val impl_5': v_B: usize -> Core.Cmp.t_Ord (t_BoundedAbsI16 v_B)
-
-unfold
-let impl_5 (v_B: usize) = impl_5' v_B
+let impl_6 (v_B: usize) : Core.Cmp.t_PartialOrd (t_BoundedAbsI16 v_B) (t_BoundedAbsI16 v_B) =
+  {
+    _super_17767811571638026139 = FStar.Tactics.Typeclasses.solve;
+    f_partial_cmp_pre = (fun (self: t_BoundedAbsI16 v_B) (other: t_BoundedAbsI16 v_B) -> true);
+    f_partial_cmp_post
+    =
+    (fun
+        (self: t_BoundedAbsI16 v_B)
+        (other: t_BoundedAbsI16 v_B)
+        (out: Core.Option.t_Option Core.Cmp.t_Ordering)
+        ->
+        true);
+    f_partial_cmp
+    =
+    fun (self: t_BoundedAbsI16 v_B) (other: t_BoundedAbsI16 v_B) ->
+      Core.Cmp.f_partial_cmp #i16 #i16 #FStar.Tactics.Typeclasses.solve self._0 other._0
+  }
 
 [@@ FStar.Tactics.Typeclasses.tcinstance]
-assume
-val impl_7': v_B: usize -> Core.Hash.t_Hash (t_BoundedAbsI16 v_B)
+let impl_5 (v_B: usize) : Core.Cmp.t_Ord (t_BoundedAbsI16 v_B) =
+  {
+    _super_8562072132021960682 = FStar.Tactics.Typeclasses.solve;
+    _super_17650760217149814164 = FStar.Tactics.Typeclasses.solve;
+    f_cmp_pre = (fun (self: t_BoundedAbsI16 v_B) (other: t_BoundedAbsI16 v_B) -> true);
+    f_cmp_post
+    =
+    (fun (self: t_BoundedAbsI16 v_B) (other: t_BoundedAbsI16 v_B) (out: Core.Cmp.t_Ordering) -> true
+    );
+    f_cmp
+    =
+    fun (self: t_BoundedAbsI16 v_B) (other: t_BoundedAbsI16 v_B) ->
+      Core.Cmp.f_cmp #i16 #FStar.Tactics.Typeclasses.solve self._0 other._0
+  }
 
-unfold
-let impl_7 (v_B: usize) = impl_7' v_B
+[@@ FStar.Tactics.Typeclasses.tcinstance]
+let impl_7 (v_B: usize) : Core.Hash.t_Hash (t_BoundedAbsI16 v_B) =
+  {
+    f_hash_pre
+    =
+    (fun
+        (#e_ee_H: Type0)
+        (#[FStar.Tactics.Typeclasses.tcresolve ()] i1: Core.Hash.t_Hasher e_ee_H)
+        (self: t_BoundedAbsI16 v_B)
+        (state: e_ee_H)
+        ->
+        true);
+    f_hash_post
+    =
+    (fun
+        (#e_ee_H: Type0)
+        (#[FStar.Tactics.Typeclasses.tcresolve ()] i1: Core.Hash.t_Hasher e_ee_H)
+        (self: t_BoundedAbsI16 v_B)
+        (state: e_ee_H)
+        (out: e_ee_H)
+        ->
+        true);
+    f_hash
+    =
+    fun
+      (#e_ee_H: Type0)
+      (#[FStar.Tactics.Typeclasses.tcresolve ()] i1: Core.Hash.t_Hasher e_ee_H)
+      (self: t_BoundedAbsI16 v_B)
+      (state: e_ee_H)
+      ->
+      let state:e_ee_H =
+        Core.Hash.f_hash #i16 #FStar.Tactics.Typeclasses.solve #e_ee_H self._0 state
+      in
+      state
+  }
 
 let double_abs_i16 (v_N v_M: usize) (x: t_BoundedAbsI16 v_N)
     : Prims.Pure (t_BoundedAbsI16 v_M)
diff --git a/test-harness/src/snapshots/toolchain__lean-tests into-lean.snap b/test-harness/src/snapshots/toolchain__lean-tests into-lean.snap
index de38d8c02..e1124f973 100644
--- a/test-harness/src/snapshots/toolchain__lean-tests into-lean.snap	
+++ b/test-harness/src/snapshots/toolchain__lean-tests into-lean.snap	
@@ -20,38 +20,12 @@ info:
     include_flag: ~
     backend_options: ~
 ---
-exit = 0
-stderr = 'Finished `dev` profile [unoptimized + debuginfo] target(s) in XXs'
-
-[stdout]
-diagnostics = []
-
-[stdout.files]
-"lean_tests.lean" = '''
--- Experimental lean backend for Hax
--- Comment the following line to not import the prelude (requires the Lib.lean file) : 
-import Lib
-
-
-
--- unimplemented yet
-
-def FORTYTWO  : usize := 42
-
-def returns42 (_ : hax_Tuple0) : usize := FORTYTWO
-
-def add_two_numbers (x : usize) (y : usize) : usize := (hax_machine_int_add x y)
-
-def letBinding (x : usize) (y : usize) : usize :=
-  let useless := (.constr_hax_Tuple0 : hax_Tuple0);
-  let result1 := (hax_machine_int_add x y);
-  let result2 := (hax_machine_int_add result1 2);
-  (hax_machine_int_add result2 1)
-
-def closure (_ : hax_Tuple0) : i32 :=
-  let x := 41;
-  let f := (fun y => (hax_machine_int_add y x));
-  (ops_function_Fn_call f
-    (.constr_hax_Tuple1 {hax_Tuple1_Tuple0 := 1} : (hax_Tuple1 i32)))
-
-abbrev UsizeAlias := usize'''
+exit = 1
+stderr = """
+Finished `dev` profile [unoptimized + debuginfo] target(s) in XXs
+
+thread 'main' panicked at rust-engine/src/ocaml_engine.rs:88:14:
+called `Result::unwrap()` on an `Err` value: Os { code: 2, kind: NotFound, message: \"No such file or directory\" }
+note: run with `RUST_BACKTRACE=1` environment variable to display a backtrace
+\u001B[1m\u001B[91merror\u001B[0m: \u001B[1mhax: hax-engine exited with non-zero code 101\u001B[0m"""
+stdout = ''
diff --git a/test-harness/src/snapshots/toolchain__literals into-coq.snap b/test-harness/src/snapshots/toolchain__literals into-coq.snap
index 640f68231..ad692c47c 100644
--- a/test-harness/src/snapshots/toolchain__literals into-coq.snap	
+++ b/test-harness/src/snapshots/toolchain__literals into-coq.snap	
@@ -20,11 +20,23 @@ info:
     include_flag: ~
     backend_options: ~
 ---
-exit = 0
-stderr = 'Finished `dev` profile [unoptimized + debuginfo] target(s) in XXs'
-
-[stdout]
-diagnostics = []
+exit = 1
+stderr = """
+Finished `dev` profile [unoptimized + debuginfo] target(s) in XXs
+\u001B[1m\u001B[91merror\u001B[0m: \u001B[1m[HAX0001] (AST import) something is not implemented yet.This is discussed in issue https://github.com/hacspec/hax/issues/156.
+Please upvote or comment this issue if you see this error message.
+Sorry, Hax does not support declare-first let bindings (see https://doc.rust-lang.org/rust-by-example/variable_bindings/declare.html) for now.\u001B[0m
+  \u001B[1m\u001B[94m-->\u001B[0m literals/src/lib.rs:43:21
+\u001B[1m\u001B[94m   |\u001B[0m
+\u001B[1m\u001B[94m43 |\u001B[0m #[derive(PartialEq, Eq)]
+\u001B[1m\u001B[94m   |\u001B[0m\u001B[1m\u001B[91m                     ^^\u001B[0m
+\u001B[1m\u001B[94m   |\u001B[0m"""
+[[stdout.diagnostics]]
+message = '''
+(AST import) something is not implemented yet.This is discussed in issue https://github.com/hacspec/hax/issues/156.
+Please upvote or comment this issue if you see this error message.
+Sorry, Hax does not support declare-first let bindings (see https://doc.rust-lang.org/rust-by-example/variable_bindings/declare.html) for now.'''
+spans = ['Span { lo: Loc { line: 43, col: 20 }, hi: Loc { line: 43, col: 22 }, filename: Real(LocalPath("literals/src/lib.rs")), rust_span_data: None }']
 
 [stdout.files]
 "Literals.v" = '''
@@ -91,11 +103,23 @@ Record Foo_record : Type :=
 #[export] Instance settable_Foo_record : Settable _ :=
   settable! (Build_Foo_record) <Foo_f_field>.
 
+Instance t_StructuralPartialEq_61223753 : t_StructuralPartialEq ((t_Foo)) :=
+  {
+  }.
 
+Instance t_PartialEq_662037409 : t_PartialEq ((t_Foo)) ((t_Foo)) :=
+  {
+    implaabbcc_t_PartialEq_f_eq := fun  (self : t_Foo) (other : t_Foo)=>
+      f_eq (f_field self) (f_field other);
+  }.
 
-
-
-
+Instance t_Eq_795626685 : t_Eq ((t_Foo)) :=
+  {
+    implaabbcc_t_Eq_f_assert_receiver_is_total_eq := fun  (self : t_Foo)=>
+      failure (("(AST import) something is not implemented yet.This is discussed in issue https://github.com/hacspec/hax/issues/156.
+Please upvote or comment this issue if you see this error message.
+Sorry, Hax does not support declare-first let bindings (see https://doc.rust-lang.org/rust-by-example/variable_bindings/declare.html) for now."%string : string)) ((""%string : string));
+  }.
 
 Definition v_CONSTANT : t_Foo :=
   Foo ((3 : t_u8)).
diff --git a/test-harness/src/snapshots/toolchain__literals into-fstar.snap b/test-harness/src/snapshots/toolchain__literals into-fstar.snap
index 23fafa1e1..c748af566 100644
--- a/test-harness/src/snapshots/toolchain__literals into-fstar.snap	
+++ b/test-harness/src/snapshots/toolchain__literals into-fstar.snap	
@@ -20,11 +20,23 @@ info:
     include_flag: ~
     backend_options: ~
 ---
-exit = 0
-stderr = 'Finished `dev` profile [unoptimized + debuginfo] target(s) in XXs'
-
-[stdout]
-diagnostics = []
+exit = 1
+stderr = """
+Finished `dev` profile [unoptimized + debuginfo] target(s) in XXs
+\u001B[1m\u001B[91merror\u001B[0m: \u001B[1m[HAX0001] (AST import) something is not implemented yet.This is discussed in issue https://github.com/hacspec/hax/issues/156.
+Please upvote or comment this issue if you see this error message.
+Sorry, Hax does not support declare-first let bindings (see https://doc.rust-lang.org/rust-by-example/variable_bindings/declare.html) for now.\u001B[0m
+  \u001B[1m\u001B[94m-->\u001B[0m literals/src/lib.rs:43:21
+\u001B[1m\u001B[94m   |\u001B[0m
+\u001B[1m\u001B[94m43 |\u001B[0m #[derive(PartialEq, Eq)]
+\u001B[1m\u001B[94m   |\u001B[0m\u001B[1m\u001B[91m                     ^^\u001B[0m
+\u001B[1m\u001B[94m   |\u001B[0m"""
+[[stdout.diagnostics]]
+message = '''
+(AST import) something is not implemented yet.This is discussed in issue https://github.com/hacspec/hax/issues/156.
+Please upvote or comment this issue if you see this error message.
+Sorry, Hax does not support declare-first let bindings (see https://doc.rust-lang.org/rust-by-example/variable_bindings/declare.html) for now.'''
+spans = ['Span { lo: Loc { line: 43, col: 20 }, hi: Loc { line: 43, col: 22 }, filename: Real(LocalPath("literals/src/lib.rs")), rust_span_data: None }']
 
 [stdout.files]
 "Literals.fst" = '''
@@ -85,25 +97,28 @@ let panic_with_msg (_: Prims.unit) : Prims.unit =
 type t_Foo = { f_field:u8 }
 
 [@@ FStar.Tactics.Typeclasses.tcinstance]
-assume
-val impl': Core.Marker.t_StructuralPartialEq t_Foo
-
-unfold
-let impl = impl'
+let impl: Core.Marker.t_StructuralPartialEq t_Foo = { __marker_trait = () }
 
 [@@ FStar.Tactics.Typeclasses.tcinstance]
-assume
-val impl_1': Core.Cmp.t_PartialEq t_Foo t_Foo
-
-unfold
-let impl_1 = impl_1'
+let impl_1: Core.Cmp.t_PartialEq t_Foo t_Foo =
+  {
+    f_eq_pre = (fun (self: t_Foo) (other: t_Foo) -> true);
+    f_eq_post = (fun (self: t_Foo) (other: t_Foo) (out: bool) -> true);
+    f_eq = fun (self: t_Foo) (other: t_Foo) -> self.f_field =. other.f_field
+  }
 
 [@@ FStar.Tactics.Typeclasses.tcinstance]
-assume
-val impl_2': Core.Cmp.t_Eq t_Foo
-
-unfold
-let impl_2 = impl_2'
+let impl_2: Core.Cmp.t_Eq t_Foo =
+  {
+    _super_5579681813951091494 = FStar.Tactics.Typeclasses.solve;
+    f_assert_receiver_is_total_eq_pre = (fun (self: t_Foo) -> true);
+    f_assert_receiver_is_total_eq_post = (fun (self: t_Foo) (out: Prims.unit) -> true);
+    f_assert_receiver_is_total_eq
+    =
+    fun (self: t_Foo) ->
+      Rust_primitives.Hax.failure "(AST import) something is not implemented yet.This is discussed in issue https://github.com/hacspec/hax/issues/156.\nPlease upvote or comment this issue if you see this error message.\nSorry, Hax does not support declare-first let bindings (see https://doc.rust-lang.org/rust-by-example/variable_bindings/declare.html) for now."
+        ""
+  }
 
 let v_CONSTANT: t_Foo = { f_field = mk_u8 3 } <: t_Foo
 

From b8622304ca2dbb4e1baab8a8432e3827fbbd7c0d Mon Sep 17 00:00:00 2001
From: Lucas Franceschino <lucas@cryspen.com>
Date: Mon, 21 Jul 2025 15:29:26 +0200
Subject: [PATCH 13/18] feat(frontend/exporter): exhaustive support for
 `AttributeKind`

---
 frontend/exporter/src/types/attributes.rs | 301 ++++++++++++++++++++++
 frontend/exporter/src/types/hir.rs        |  32 ---
 frontend/exporter/src/types/mod.rs        |   2 +
 3 files changed, 303 insertions(+), 32 deletions(-)
 create mode 100644 frontend/exporter/src/types/attributes.rs

diff --git a/frontend/exporter/src/types/attributes.rs b/frontend/exporter/src/types/attributes.rs
new file mode 100644
index 000000000..eeb9af537
--- /dev/null
+++ b/frontend/exporter/src/types/attributes.rs
@@ -0,0 +1,301 @@
+//! Copies of the types related to attributes.
+//! Such types are mostly contained in the crate `rustc_attr_data_structures`.
+
+use crate::prelude::*;
+
+/// Reflects [`rustc_attr_data_structures::AttributeKind`]
+#[derive(AdtInto)]
+#[args(<'tcx, S: BaseState<'tcx>>, from: rustc_attr_data_structures::AttributeKind, state: S as tcx)]
+#[derive_group(Serializers)]
+#[derive(Clone, Debug, JsonSchema, Hash, PartialEq, Eq, PartialOrd, Ord)]
+pub enum AttributeKind {
+    Align {
+        align: Align,
+        span: Span,
+    },
+    AllowConstFnUnstable(Vec<Symbol>, Span),
+    AllowIncoherentImpl(Span),
+    AllowInternalUnstable(Vec<(Symbol, Span)>, Span),
+    AsPtr(Span),
+    AutomaticallyDerived(Span),
+    BodyStability {
+        stability: DefaultBodyStability,
+        span: Span,
+    },
+    CoherenceIsCore,
+    Coinductive(Span),
+    Cold(Span),
+    Confusables {
+        symbols: Vec<Symbol>,
+        first_span: Span,
+    },
+    ConstContinue(Span),
+    ConstStability {
+        stability: PartialConstStability,
+        span: Span,
+    },
+    ConstStabilityIndirect,
+    ConstTrait(Span),
+    Coverage(Span, CoverageStatus),
+    DenyExplicitImpl(Span),
+    Deprecation {
+        deprecation: Deprecation,
+        span: Span,
+    },
+    DoNotImplementViaObject(Span),
+    DocComment {
+        style: AttrStyle,
+        kind: CommentKind,
+        span: Span,
+        comment: Symbol,
+    },
+    Dummy,
+    ExportName {
+        name: Symbol,
+        span: Span,
+    },
+    ExportStable,
+    FfiConst(Span),
+    FfiPure(Span),
+    Fundamental,
+    Ignore {
+        span: Span,
+        reason: Option<Symbol>,
+    },
+    Inline(InlineAttr, Span),
+    LinkName {
+        name: Symbol,
+        span: Span,
+    },
+    LinkOrdinal {
+        ordinal: u16,
+        span: Span,
+    },
+    LinkSection {
+        name: Symbol,
+        span: Span,
+    },
+    LoopMatch(Span),
+    MacroTransparency(Transparency),
+    Marker(Span),
+    MayDangle(Span),
+    MustUse {
+        span: Span,
+        reason: Option<Symbol>,
+    },
+    Naked(Span),
+    NoImplicitPrelude(Span),
+    NoMangle(Span),
+    NonExhaustive(Span),
+    OmitGdbPrettyPrinterSection,
+    Optimize(OptimizeAttr, Span),
+    ParenSugar(Span),
+    PassByValue(Span),
+    Path(Symbol, Span),
+    Pointee(Span),
+    PubTransparent(Span),
+    Repr {
+        reprs: Vec<(ReprAttr, Span)>,
+        first_span: Span,
+    },
+    RustcLayoutScalarValidRangeEnd(u128, Span),
+    RustcLayoutScalarValidRangeStart(u128, Span),
+    RustcObjectLifetimeDefault,
+    SkipDuringMethodDispatch {
+        array: bool,
+        boxed_slice: bool,
+        span: Span,
+    },
+    SpecializationTrait(Span),
+    Stability {
+        stability: Stability,
+        span: Span,
+    },
+    StdInternalSymbol(Span),
+    TargetFeature(Vec<(Symbol, Span)>, Span),
+    TrackCaller(Span),
+    TypeConst(Span),
+    UnsafeSpecializationMarker(Span),
+    UnstableFeatureBound(Vec<(Symbol, Span)>),
+    Used {
+        used_by: UsedBy,
+        span: Span,
+    },
+}
+
+/// Reflects [`rustc_span::hygiene::Transparency`]
+#[derive_group(Serializers)]
+#[derive(AdtInto, Clone, Debug, JsonSchema, Hash, PartialEq, Eq, PartialOrd, Ord)]
+#[args(<'tcx, S>, from: rustc_span::hygiene::Transparency, state: S as _s)]
+pub enum Transparency {
+    Transparent,
+    SemiOpaque,
+    Opaque,
+}
+
+/// Reflects [`rustc_attr_data_structures::Stability`]
+#[derive_group(Serializers)]
+#[derive(AdtInto, Clone, Debug, JsonSchema, Hash, PartialEq, Eq, PartialOrd, Ord)]
+#[args(<'tcx, S>, from: rustc_attr_data_structures::Stability, state: S as _s)]
+pub struct Stability {
+    pub level: StabilityLevel,
+    pub feature: Symbol,
+}
+
+/// Reflects [`rustc_attr_data_structures::DefaultBodyStability`]
+#[derive_group(Serializers)]
+#[derive(AdtInto, Clone, Debug, JsonSchema, Hash, PartialEq, Eq, PartialOrd, Ord)]
+#[args(<'tcx, S>, from: rustc_attr_data_structures::DefaultBodyStability, state: S as _s)]
+pub struct DefaultBodyStability {
+    pub level: StabilityLevel,
+    pub feature: Symbol,
+}
+
+/// Reflects [`rustc_attr_data_structures::Deprecation`]
+#[derive_group(Serializers)]
+#[derive(AdtInto, Clone, Debug, JsonSchema, Hash, PartialEq, Eq, PartialOrd, Ord)]
+#[args(<'tcx, S>, from: rustc_attr_data_structures::Deprecation, state: S as _s)]
+pub struct Deprecation {
+    pub since: DeprecatedSince,
+    pub note: Option<Symbol>,
+    pub suggestion: Option<Symbol>,
+}
+
+/// Reflects [`rustc_attr_data_structures::DeprecatedSince`]
+#[derive_group(Serializers)]
+#[derive(AdtInto, Clone, Debug, JsonSchema, Hash, PartialEq, Eq, PartialOrd, Ord)]
+#[args(<'tcx, S>, from: rustc_attr_data_structures::DeprecatedSince, state: S as _s)]
+pub enum DeprecatedSince {
+    RustcVersion(RustcVersion),
+    Future,
+    NonStandard(Symbol),
+    Unspecified,
+    Err,
+}
+
+/// Reflects [`rustc_attr_data_structures::ReprAttr`]
+#[derive_group(Serializers)]
+#[derive(AdtInto, Clone, Debug, JsonSchema, Hash, PartialEq, Eq, PartialOrd, Ord)]
+#[args(<'tcx, S>, from: rustc_attr_data_structures::ReprAttr, state: S as _s)]
+pub enum ReprAttr {
+    ReprInt(IntType),
+    ReprRust,
+    ReprC,
+    ReprPacked(Align),
+    ReprSimd,
+    ReprTransparent,
+    ReprAlign(Align),
+}
+
+/// Reflects [`rustc_attr_data_structures::IntType`]
+#[derive_group(Serializers)]
+#[derive(AdtInto, Clone, Debug, JsonSchema, Hash, PartialEq, Eq, PartialOrd, Ord)]
+#[args(<'tcx, S>, from: rustc_attr_data_structures::IntType, state: S as _s)]
+pub enum IntType {
+    SignedInt(IntTy),
+    UnsignedInt(UintTy),
+}
+
+/// Reflects [`rustc_attr_data_structures::UsedBy`]
+#[derive_group(Serializers)]
+#[derive(AdtInto, Clone, Debug, JsonSchema, Hash, PartialEq, Eq, PartialOrd, Ord)]
+#[args(<'tcx, S>, from: rustc_attr_data_structures::UsedBy, state: S as _s)]
+pub enum UsedBy {
+    Compiler,
+    Linker,
+}
+
+/// Reflects [`rustc_attr_data_structures::StabilityLevel`]
+#[derive_group(Serializers)]
+#[derive(AdtInto, Clone, Debug, JsonSchema, Hash, PartialEq, Eq, PartialOrd, Ord)]
+#[args(<'tcx, S>, from: rustc_attr_data_structures::StabilityLevel, state: S as _s)]
+pub enum StabilityLevel {
+    Unstable {
+        reason: UnstableReason,
+        #[map(x.map(|x| x.get()))]
+        issue: Option<u32>,
+        is_soft: bool,
+        implied_by: Option<Symbol>,
+        old_name: Option<Symbol>,
+    },
+    Stable {
+        since: StableSince,
+        allowed_through_unstable_modules: Option<Symbol>,
+    },
+}
+
+/// Reflects [`rustc_attr_data_structures::CoverageStatus`]
+#[derive_group(Serializers)]
+#[derive(AdtInto, Clone, Debug, JsonSchema, Hash, PartialEq, Eq, PartialOrd, Ord)]
+#[args(<'tcx, S>, from: rustc_attr_data_structures::CoverageStatus, state: S as _s)]
+pub enum CoverageStatus {
+    On,
+    Off,
+}
+
+/// Reflects [`rustc_attr_data_structures::PartialConstStability`]
+#[derive_group(Serializers)]
+#[derive(AdtInto, Clone, Debug, JsonSchema, Hash, PartialEq, Eq, PartialOrd, Ord)]
+#[args(<'tcx, S>, from: rustc_attr_data_structures::PartialConstStability, state: S as _s)]
+pub struct PartialConstStability {
+    pub level: StabilityLevel,
+    pub feature: Symbol,
+    pub promotable: bool,
+}
+
+/// Reflects [`rustc_attr_data_structures::RustcVersion`]
+#[derive_group(Serializers)]
+#[derive(AdtInto, Clone, Debug, JsonSchema, Hash, PartialEq, Eq, PartialOrd, Ord)]
+#[args(<'tcx, S>, from: rustc_attr_data_structures::RustcVersion, state: S as _s)]
+pub struct RustcVersion {
+    pub major: u16,
+    pub minor: u16,
+    pub patch: u16,
+}
+
+/// Reflects [`rustc_attr_data_structures::StableSince`]
+#[derive_group(Serializers)]
+#[derive(AdtInto, Clone, Debug, JsonSchema, Hash, PartialEq, Eq, PartialOrd, Ord)]
+#[args(<'tcx, S>, from: rustc_attr_data_structures::StableSince, state: S as _s)]
+pub enum StableSince {
+    Version(RustcVersion),
+    Current,
+    #[custom_arm(rustc_attr_data_structures::StableSince::Err(_) => StableSince::Err,)]
+    Err,
+}
+
+/// Reflects [`rustc_attr_data_structures::UnstableReason`]
+#[derive_group(Serializers)]
+#[derive(AdtInto, Clone, Debug, JsonSchema, Hash, PartialEq, Eq, PartialOrd, Ord)]
+#[args(<'tcx, S>, from: rustc_attr_data_structures::UnstableReason, state: S as _s)]
+pub enum UnstableReason {
+    None,
+    Default,
+    Some(Symbol),
+}
+
+/// Reflects [`rustc_attr_data_structures::OptimizeAttr`]
+#[derive_group(Serializers)]
+#[derive(AdtInto, Clone, Debug, JsonSchema, Hash, PartialEq, Eq, PartialOrd, Ord)]
+#[args(<'tcx, S>, from: rustc_attr_data_structures::OptimizeAttr, state: S as _s)]
+pub enum OptimizeAttr {
+    Default,
+    DoNotOptimize,
+    Speed,
+    Size,
+}
+
+/// Reflects [`rustc_attr_data_structures::InlineAttr`]
+#[derive_group(Serializers)]
+#[derive(AdtInto, Clone, Debug, JsonSchema, Hash, PartialEq, Eq, PartialOrd, Ord)]
+#[args(<'tcx, S: BaseState<'tcx>>, from: rustc_attr_data_structures::InlineAttr, state: S as _s)]
+pub enum InlineAttr {
+    None,
+    Hint,
+    Always,
+    Never,
+    Force {
+        attr_span: Span,
+        reason: Option<Symbol>,
+    },
+}
diff --git a/frontend/exporter/src/types/hir.rs b/frontend/exporter/src/types/hir.rs
index 188b96ef8..efa665ea0 100644
--- a/frontend/exporter/src/types/hir.rs
+++ b/frontend/exporter/src/types/hir.rs
@@ -970,38 +970,6 @@ pub enum Attribute {
     Parsed(AttributeKind),
     Unparsed(AttrItem),
 }
-
-/// Reflects [`rustc_attr_data_structures::AttributeKind`]
-#[derive(AdtInto)]
-#[args(<'tcx, S: BaseState<'tcx>>, from: rustc_attr_data_structures::AttributeKind, state: S as tcx)]
-#[derive_group(Serializers)]
-#[derive(Clone, Debug, JsonSchema, Hash, PartialEq, Eq, PartialOrd, Ord)]
-pub enum AttributeKind {
-    DocComment {
-        style: AttrStyle,
-        kind: CommentKind,
-        span: Span,
-        comment: Symbol,
-    },
-    #[todo]
-    Other(String),
-}
-
-/// Reflects [`rustc_attr_data_structures::InlineAttr`]
-#[derive_group(Serializers)]
-#[derive(AdtInto, Clone, Debug, JsonSchema, Hash, PartialEq, Eq, PartialOrd, Ord)]
-#[args(<'tcx, S: BaseState<'tcx>>, from: rustc_attr_data_structures::InlineAttr, state: S as _s)]
-pub enum InlineAttr {
-    None,
-    Hint,
-    Always,
-    Never,
-    Force {
-        attr_span: Span,
-        reason: Option<Symbol>,
-    },
-}
-
 /// Reflects [`rustc_ast::ast::BindingMode`]
 #[derive(AdtInto)]
 #[args(<S>, from: rustc_ast::ast::BindingMode, state: S as s)]
diff --git a/frontend/exporter/src/types/mod.rs b/frontend/exporter/src/types/mod.rs
index 51d089708..7c1787389 100644
--- a/frontend/exporter/src/types/mod.rs
+++ b/frontend/exporter/src/types/mod.rs
@@ -1,3 +1,4 @@
+mod attributes;
 mod def_id;
 mod hir;
 mod mir;
@@ -7,6 +8,7 @@ mod span;
 mod thir;
 mod ty;
 
+pub use attributes::*;
 pub use def_id::*;
 pub use hir::*;
 pub use mir::*;

From c84710197be5eacb43e3a603dba4f0bc77bce562 Mon Sep 17 00:00:00 2001
From: Lucas Franceschino <lucas@cryspen.com>
Date: Mon, 21 Jul 2025 15:30:07 +0200
Subject: [PATCH 14/18] fix(engine): rustc emits attr. "automatically_derived"
 in a different format

---
 engine/lib/import_thir.ml | 2 +-
 1 file changed, 1 insertion(+), 1 deletion(-)

diff --git a/engine/lib/import_thir.ml b/engine/lib/import_thir.ml
index 30dbc12b7..c093d6061 100644
--- a/engine/lib/import_thir.ml
+++ b/engine/lib/import_thir.ml
@@ -1375,7 +1375,7 @@ let is_automatically_derived (attrs : Thir.attribute list) =
     ~f:(function
       (* This will break once these attributes get properly parsed. It will
           then be very easy to parse them correctly *)
-      | Unparsed { path; _ } -> String.equal path "automatically_derived"
+      | Parsed (AutomaticallyDerived _) -> true
       | _ -> false)
     attrs
 

From 823522b33b8d9615939bc2ab3c2137fd3ffe5f1f Mon Sep 17 00:00:00 2001
From: Lucas Franceschino <lucas@cryspen.com>
Date: Mon, 21 Jul 2025 15:46:30 +0200
Subject: [PATCH 15/18] fix(engine): "automatically_derived": reintroduce in
 engine

---
 engine/lib/import_thir.ml | 4 ++++
 1 file changed, 4 insertions(+)

diff --git a/engine/lib/import_thir.ml b/engine/lib/import_thir.ml
index c093d6061..db9297f8b 100644
--- a/engine/lib/import_thir.ml
+++ b/engine/lib/import_thir.ml
@@ -118,6 +118,10 @@ let c_attr (attr : Thir.attribute) : attr option =
       in
       let kind = DocComment { kind; body = comment } in
       Some { kind; span = Span.of_thir span }
+  | Parsed (AutomaticallyDerived span) ->
+      (* Restore behavior before PR #1534 *)
+      let kind = Tool { path = "automatically_derived"; tokens = "" } in
+      Some { kind; span = Span.of_thir span }
   | Unparsed { args = Eq { expr = { symbol; _ }; _ }; path = "doc"; span; _ } ->
       (* Looks for `#[doc = "something"]` *)
       let kind = DocComment { kind = DCKLine; body = symbol } in

From 6d1129bd70edd61aa6163d7189732b911d66b9d7 Mon Sep 17 00:00:00 2001
From: Lucas Franceschino <lucas@cryspen.com>
Date: Mon, 21 Jul 2025 15:47:51 +0200
Subject: [PATCH 16/18] chore: update snapshots

---
 .../toolchain__attributes into-fstar.snap     | 206 ++++++------------
 .../toolchain__lean-tests into-lean.snap      |  44 +++-
 .../toolchain__literals into-coq.snap         |  40 +---
 .../toolchain__literals into-fstar.snap       |  55 ++---
 4 files changed, 124 insertions(+), 221 deletions(-)

diff --git a/test-harness/src/snapshots/toolchain__attributes into-fstar.snap b/test-harness/src/snapshots/toolchain__attributes into-fstar.snap
index e9e8f1d58..4b29f6b9a 100644
--- a/test-harness/src/snapshots/toolchain__attributes into-fstar.snap	
+++ b/test-harness/src/snapshots/toolchain__attributes into-fstar.snap	
@@ -20,27 +20,10 @@ info:
     include_flag: ~
     backend_options: ~
 ---
-exit = 1
-[[stdout.diagnostics]]
-message = '''
-(AST import) something is not implemented yet.This is discussed in issue https://github.com/hacspec/hax/issues/156.
-Please upvote or comment this issue if you see this error message.
-Sorry, Hax does not support declare-first let bindings (see https://doc.rust-lang.org/rust-by-example/variable_bindings/declare.html) for now.'''
-spans = ['Span { lo: Loc { line: 301, col: 17 }, hi: Loc { line: 301, col: 22 }, filename: Real(LocalPath("/home/nadrieril/wip/work/hax/hax-bounded-integers/src/lib.rs")), rust_span_data: None }']
-
-[[stdout.diagnostics]]
-message = '''
-(AST import) something is not implemented yet.This is discussed in issue https://github.com/hacspec/hax/issues/156.
-Please upvote or comment this issue if you see this error message.
-Sorry, Hax does not support declare-first let bindings (see https://doc.rust-lang.org/rust-by-example/variable_bindings/declare.html) for now.'''
-spans = ['Span { lo: Loc { line: 301, col: 30 }, hi: Loc { line: 301, col: 32 }, filename: Real(LocalPath("/home/nadrieril/wip/work/hax/hax-bounded-integers/src/lib.rs")), rust_span_data: None }']
-
-[[stdout.diagnostics]]
-message = '''
-(AST import) something is not implemented yet.This is discussed in issue https://github.com/hacspec/hax/issues/156.
-Please upvote or comment this issue if you see this error message.
-Sorry, Hax does not support declare-first let bindings (see https://doc.rust-lang.org/rust-by-example/variable_bindings/declare.html) for now.'''
-spans = ['Span { lo: Loc { line: 295, col: 19 }, hi: Loc { line: 295, col: 24 }, filename: Real(LocalPath("attributes/src/lib.rs")), rust_span_data: None }']
+exit = 0
+
+[stdout]
+diagnostics = []
 
 [stdout.files]
 "Attributes.Ensures_on_arity_zero_fns.fst" = '''
@@ -74,24 +57,25 @@ open FStar.Mul
 type t_Dummy = | Dummy : t_Dummy
 
 [@@ FStar.Tactics.Typeclasses.tcinstance]
-let impl_1: Core.Marker.t_StructuralPartialEq t_Dummy = { __marker_trait = () }
+assume
+val impl_1': Core.Marker.t_StructuralPartialEq t_Dummy
+
+unfold
+let impl_1 = impl_1'
 
 [@@ FStar.Tactics.Typeclasses.tcinstance]
-let impl_2: Core.Cmp.t_PartialEq t_Dummy t_Dummy =
-  {
-    f_eq_pre = (fun (self: t_Dummy) (other: t_Dummy) -> true);
-    f_eq_post = (fun (self: t_Dummy) (other: t_Dummy) (out: bool) -> true);
-    f_eq = fun (self: t_Dummy) (other: t_Dummy) -> true
-  }
+assume
+val impl_2': Core.Cmp.t_PartialEq t_Dummy t_Dummy
+
+unfold
+let impl_2 = impl_2'
 
 [@@ FStar.Tactics.Typeclasses.tcinstance]
-let impl: Core.Cmp.t_Eq t_Dummy =
-  {
-    _super_5579681813951091494 = FStar.Tactics.Typeclasses.solve;
-    f_assert_receiver_is_total_eq_pre = (fun (self: t_Dummy) -> true);
-    f_assert_receiver_is_total_eq_post = (fun (self: t_Dummy) (out: Prims.unit) -> true);
-    f_assert_receiver_is_total_eq = fun (self: t_Dummy) -> ()
-  }
+assume
+val impl': Core.Cmp.t_Eq t_Dummy
+
+unfold
+let impl = impl'
 
 let impl_Dummy__f (self: t_Dummy)
     : Prims.Pure t_Dummy
@@ -145,21 +129,14 @@ open FStar.Mul
 
 unfold type t_Int = int
 
-[@@ FStar.Tactics.Typeclasses.tcinstance]
-let impl_1: Core.Clone.t_Clone t_Int =
-  {
-    f_clone_pre = (fun (self: t_Int) -> true);
-    f_clone_post = (fun (self: t_Int) (out: t_Int) -> true);
-    f_clone
-    =
-    fun (self: t_Int) ->
-      Rust_primitives.Hax.failure "(AST import) something is not implemented yet.This is discussed in issue https://github.com/hacspec/hax/issues/156.\nPlease upvote or comment this issue if you see this error message.\nSorry, Hax does not support declare-first let bindings (see https://doc.rust-lang.org/rust-by-example/variable_bindings/declare.html) for now."
-        ""
-  }
+let impl_1: Core.Clone.t_Clone t_Int = { f_clone = (fun x -> x) }
 
 [@@ FStar.Tactics.Typeclasses.tcinstance]
-let impl: Core.Marker.t_Copy t_Int =
-  { _super_15837849249852401974 = FStar.Tactics.Typeclasses.solve }
+assume
+val impl': Core.Marker.t_Copy t_Int
+
+unfold
+let impl = impl'
 
 unfold let add x y = x + y
 
@@ -494,117 +471,56 @@ let t_BoundedAbsI16 (v_B: usize) =
       (Rust_primitives.Hax.Int.from_machine x <: Hax_lib.Int.t_Int) <=
       (Rust_primitives.Hax.Int.from_machine v_B <: Hax_lib.Int.t_Int) }
 
-[@@ FStar.Tactics.Typeclasses.tcinstance]
-let impl (v_B: usize) : Core.Clone.t_Clone (t_BoundedAbsI16 v_B) =
-  {
-    f_clone_pre = (fun (self: t_BoundedAbsI16 v_B) -> true);
-    f_clone_post = (fun (self: t_BoundedAbsI16 v_B) (out: t_BoundedAbsI16 v_B) -> true);
-    f_clone
-    =
-    fun (self: t_BoundedAbsI16 v_B) ->
-      Rust_primitives.Hax.failure "(AST import) something is not implemented yet.This is discussed in issue https://github.com/hacspec/hax/issues/156.\nPlease upvote or comment this issue if you see this error message.\nSorry, Hax does not support declare-first let bindings (see https://doc.rust-lang.org/rust-by-example/variable_bindings/declare.html) for now."
-        ""
-  }
+let impl (v_B: usize) : Core.Clone.t_Clone (t_BoundedAbsI16 v_B) = { f_clone = (fun x -> x) }
 
 [@@ FStar.Tactics.Typeclasses.tcinstance]
-let impl_1 (v_B: usize) : Core.Marker.t_Copy (t_BoundedAbsI16 v_B) =
-  { _super_15837849249852401974 = FStar.Tactics.Typeclasses.solve }
+assume
+val impl_1': v_B: usize -> Core.Marker.t_Copy (t_BoundedAbsI16 v_B)
+
+unfold
+let impl_1 (v_B: usize) = impl_1' v_B
 
 [@@ FStar.Tactics.Typeclasses.tcinstance]
-let impl_3 (v_B: usize) : Core.Marker.t_StructuralPartialEq (t_BoundedAbsI16 v_B) =
-  { __marker_trait = () }
+assume
+val impl_3': v_B: usize -> Core.Marker.t_StructuralPartialEq (t_BoundedAbsI16 v_B)
+
+unfold
+let impl_3 (v_B: usize) = impl_3' v_B
 
 [@@ FStar.Tactics.Typeclasses.tcinstance]
-let impl_4 (v_B: usize) : Core.Cmp.t_PartialEq (t_BoundedAbsI16 v_B) (t_BoundedAbsI16 v_B) =
-  {
-    f_eq_pre = (fun (self: t_BoundedAbsI16 v_B) (other: t_BoundedAbsI16 v_B) -> true);
-    f_eq_post = (fun (self: t_BoundedAbsI16 v_B) (other: t_BoundedAbsI16 v_B) (out: bool) -> true);
-    f_eq = fun (self: t_BoundedAbsI16 v_B) (other: t_BoundedAbsI16 v_B) -> self._0 =. other._0
-  }
+assume
+val impl_4': v_B: usize -> Core.Cmp.t_PartialEq (t_BoundedAbsI16 v_B) (t_BoundedAbsI16 v_B)
+
+unfold
+let impl_4 (v_B: usize) = impl_4' v_B
 
 [@@ FStar.Tactics.Typeclasses.tcinstance]
-let impl_2 (v_B: usize) : Core.Cmp.t_Eq (t_BoundedAbsI16 v_B) =
-  {
-    _super_5579681813951091494 = FStar.Tactics.Typeclasses.solve;
-    f_assert_receiver_is_total_eq_pre = (fun (self: t_BoundedAbsI16 v_B) -> true);
-    f_assert_receiver_is_total_eq_post = (fun (self: t_BoundedAbsI16 v_B) (out: Prims.unit) -> true);
-    f_assert_receiver_is_total_eq
-    =
-    fun (self: t_BoundedAbsI16 v_B) ->
-      Rust_primitives.Hax.failure "(AST import) something is not implemented yet.This is discussed in issue https://github.com/hacspec/hax/issues/156.\nPlease upvote or comment this issue if you see this error message.\nSorry, Hax does not support declare-first let bindings (see https://doc.rust-lang.org/rust-by-example/variable_bindings/declare.html) for now."
-        ""
-  }
+assume
+val impl_2': v_B: usize -> Core.Cmp.t_Eq (t_BoundedAbsI16 v_B)
+
+unfold
+let impl_2 (v_B: usize) = impl_2' v_B
 
 [@@ FStar.Tactics.Typeclasses.tcinstance]
-let impl_6 (v_B: usize) : Core.Cmp.t_PartialOrd (t_BoundedAbsI16 v_B) (t_BoundedAbsI16 v_B) =
-  {
-    _super_17767811571638026139 = FStar.Tactics.Typeclasses.solve;
-    f_partial_cmp_pre = (fun (self: t_BoundedAbsI16 v_B) (other: t_BoundedAbsI16 v_B) -> true);
-    f_partial_cmp_post
-    =
-    (fun
-        (self: t_BoundedAbsI16 v_B)
-        (other: t_BoundedAbsI16 v_B)
-        (out: Core.Option.t_Option Core.Cmp.t_Ordering)
-        ->
-        true);
-    f_partial_cmp
-    =
-    fun (self: t_BoundedAbsI16 v_B) (other: t_BoundedAbsI16 v_B) ->
-      Core.Cmp.f_partial_cmp #i16 #i16 #FStar.Tactics.Typeclasses.solve self._0 other._0
-  }
+assume
+val impl_6': v_B: usize -> Core.Cmp.t_PartialOrd (t_BoundedAbsI16 v_B) (t_BoundedAbsI16 v_B)
+
+unfold
+let impl_6 (v_B: usize) = impl_6' v_B
 
 [@@ FStar.Tactics.Typeclasses.tcinstance]
-let impl_5 (v_B: usize) : Core.Cmp.t_Ord (t_BoundedAbsI16 v_B) =
-  {
-    _super_8562072132021960682 = FStar.Tactics.Typeclasses.solve;
-    _super_17650760217149814164 = FStar.Tactics.Typeclasses.solve;
-    f_cmp_pre = (fun (self: t_BoundedAbsI16 v_B) (other: t_BoundedAbsI16 v_B) -> true);
-    f_cmp_post
-    =
-    (fun (self: t_BoundedAbsI16 v_B) (other: t_BoundedAbsI16 v_B) (out: Core.Cmp.t_Ordering) -> true
-    );
-    f_cmp
-    =
-    fun (self: t_BoundedAbsI16 v_B) (other: t_BoundedAbsI16 v_B) ->
-      Core.Cmp.f_cmp #i16 #FStar.Tactics.Typeclasses.solve self._0 other._0
-  }
+assume
+val impl_5': v_B: usize -> Core.Cmp.t_Ord (t_BoundedAbsI16 v_B)
+
+unfold
+let impl_5 (v_B: usize) = impl_5' v_B
 
 [@@ FStar.Tactics.Typeclasses.tcinstance]
-let impl_7 (v_B: usize) : Core.Hash.t_Hash (t_BoundedAbsI16 v_B) =
-  {
-    f_hash_pre
-    =
-    (fun
-        (#e_ee_H: Type0)
-        (#[FStar.Tactics.Typeclasses.tcresolve ()] i1: Core.Hash.t_Hasher e_ee_H)
-        (self: t_BoundedAbsI16 v_B)
-        (state: e_ee_H)
-        ->
-        true);
-    f_hash_post
-    =
-    (fun
-        (#e_ee_H: Type0)
-        (#[FStar.Tactics.Typeclasses.tcresolve ()] i1: Core.Hash.t_Hasher e_ee_H)
-        (self: t_BoundedAbsI16 v_B)
-        (state: e_ee_H)
-        (out: e_ee_H)
-        ->
-        true);
-    f_hash
-    =
-    fun
-      (#e_ee_H: Type0)
-      (#[FStar.Tactics.Typeclasses.tcresolve ()] i1: Core.Hash.t_Hasher e_ee_H)
-      (self: t_BoundedAbsI16 v_B)
-      (state: e_ee_H)
-      ->
-      let state:e_ee_H =
-        Core.Hash.f_hash #i16 #FStar.Tactics.Typeclasses.solve #e_ee_H self._0 state
-      in
-      state
-  }
+assume
+val impl_7': v_B: usize -> Core.Hash.t_Hash (t_BoundedAbsI16 v_B)
+
+unfold
+let impl_7 (v_B: usize) = impl_7' v_B
 
 let double_abs_i16 (v_N v_M: usize) (x: t_BoundedAbsI16 v_N)
     : Prims.Pure (t_BoundedAbsI16 v_M)
diff --git a/test-harness/src/snapshots/toolchain__lean-tests into-lean.snap b/test-harness/src/snapshots/toolchain__lean-tests into-lean.snap
index e1124f973..de38d8c02 100644
--- a/test-harness/src/snapshots/toolchain__lean-tests into-lean.snap	
+++ b/test-harness/src/snapshots/toolchain__lean-tests into-lean.snap	
@@ -20,12 +20,38 @@ info:
     include_flag: ~
     backend_options: ~
 ---
-exit = 1
-stderr = """
-Finished `dev` profile [unoptimized + debuginfo] target(s) in XXs
-
-thread 'main' panicked at rust-engine/src/ocaml_engine.rs:88:14:
-called `Result::unwrap()` on an `Err` value: Os { code: 2, kind: NotFound, message: \"No such file or directory\" }
-note: run with `RUST_BACKTRACE=1` environment variable to display a backtrace
-\u001B[1m\u001B[91merror\u001B[0m: \u001B[1mhax: hax-engine exited with non-zero code 101\u001B[0m"""
-stdout = ''
+exit = 0
+stderr = 'Finished `dev` profile [unoptimized + debuginfo] target(s) in XXs'
+
+[stdout]
+diagnostics = []
+
+[stdout.files]
+"lean_tests.lean" = '''
+-- Experimental lean backend for Hax
+-- Comment the following line to not import the prelude (requires the Lib.lean file) : 
+import Lib
+
+
+
+-- unimplemented yet
+
+def FORTYTWO  : usize := 42
+
+def returns42 (_ : hax_Tuple0) : usize := FORTYTWO
+
+def add_two_numbers (x : usize) (y : usize) : usize := (hax_machine_int_add x y)
+
+def letBinding (x : usize) (y : usize) : usize :=
+  let useless := (.constr_hax_Tuple0 : hax_Tuple0);
+  let result1 := (hax_machine_int_add x y);
+  let result2 := (hax_machine_int_add result1 2);
+  (hax_machine_int_add result2 1)
+
+def closure (_ : hax_Tuple0) : i32 :=
+  let x := 41;
+  let f := (fun y => (hax_machine_int_add y x));
+  (ops_function_Fn_call f
+    (.constr_hax_Tuple1 {hax_Tuple1_Tuple0 := 1} : (hax_Tuple1 i32)))
+
+abbrev UsizeAlias := usize'''
diff --git a/test-harness/src/snapshots/toolchain__literals into-coq.snap b/test-harness/src/snapshots/toolchain__literals into-coq.snap
index ad692c47c..640f68231 100644
--- a/test-harness/src/snapshots/toolchain__literals into-coq.snap	
+++ b/test-harness/src/snapshots/toolchain__literals into-coq.snap	
@@ -20,23 +20,11 @@ info:
     include_flag: ~
     backend_options: ~
 ---
-exit = 1
-stderr = """
-Finished `dev` profile [unoptimized + debuginfo] target(s) in XXs
-\u001B[1m\u001B[91merror\u001B[0m: \u001B[1m[HAX0001] (AST import) something is not implemented yet.This is discussed in issue https://github.com/hacspec/hax/issues/156.
-Please upvote or comment this issue if you see this error message.
-Sorry, Hax does not support declare-first let bindings (see https://doc.rust-lang.org/rust-by-example/variable_bindings/declare.html) for now.\u001B[0m
-  \u001B[1m\u001B[94m-->\u001B[0m literals/src/lib.rs:43:21
-\u001B[1m\u001B[94m   |\u001B[0m
-\u001B[1m\u001B[94m43 |\u001B[0m #[derive(PartialEq, Eq)]
-\u001B[1m\u001B[94m   |\u001B[0m\u001B[1m\u001B[91m                     ^^\u001B[0m
-\u001B[1m\u001B[94m   |\u001B[0m"""
-[[stdout.diagnostics]]
-message = '''
-(AST import) something is not implemented yet.This is discussed in issue https://github.com/hacspec/hax/issues/156.
-Please upvote or comment this issue if you see this error message.
-Sorry, Hax does not support declare-first let bindings (see https://doc.rust-lang.org/rust-by-example/variable_bindings/declare.html) for now.'''
-spans = ['Span { lo: Loc { line: 43, col: 20 }, hi: Loc { line: 43, col: 22 }, filename: Real(LocalPath("literals/src/lib.rs")), rust_span_data: None }']
+exit = 0
+stderr = 'Finished `dev` profile [unoptimized + debuginfo] target(s) in XXs'
+
+[stdout]
+diagnostics = []
 
 [stdout.files]
 "Literals.v" = '''
@@ -103,23 +91,11 @@ Record Foo_record : Type :=
 #[export] Instance settable_Foo_record : Settable _ :=
   settable! (Build_Foo_record) <Foo_f_field>.
 
-Instance t_StructuralPartialEq_61223753 : t_StructuralPartialEq ((t_Foo)) :=
-  {
-  }.
 
-Instance t_PartialEq_662037409 : t_PartialEq ((t_Foo)) ((t_Foo)) :=
-  {
-    implaabbcc_t_PartialEq_f_eq := fun  (self : t_Foo) (other : t_Foo)=>
-      f_eq (f_field self) (f_field other);
-  }.
 
-Instance t_Eq_795626685 : t_Eq ((t_Foo)) :=
-  {
-    implaabbcc_t_Eq_f_assert_receiver_is_total_eq := fun  (self : t_Foo)=>
-      failure (("(AST import) something is not implemented yet.This is discussed in issue https://github.com/hacspec/hax/issues/156.
-Please upvote or comment this issue if you see this error message.
-Sorry, Hax does not support declare-first let bindings (see https://doc.rust-lang.org/rust-by-example/variable_bindings/declare.html) for now."%string : string)) ((""%string : string));
-  }.
+
+
+
 
 Definition v_CONSTANT : t_Foo :=
   Foo ((3 : t_u8)).
diff --git a/test-harness/src/snapshots/toolchain__literals into-fstar.snap b/test-harness/src/snapshots/toolchain__literals into-fstar.snap
index c748af566..23fafa1e1 100644
--- a/test-harness/src/snapshots/toolchain__literals into-fstar.snap	
+++ b/test-harness/src/snapshots/toolchain__literals into-fstar.snap	
@@ -20,23 +20,11 @@ info:
     include_flag: ~
     backend_options: ~
 ---
-exit = 1
-stderr = """
-Finished `dev` profile [unoptimized + debuginfo] target(s) in XXs
-\u001B[1m\u001B[91merror\u001B[0m: \u001B[1m[HAX0001] (AST import) something is not implemented yet.This is discussed in issue https://github.com/hacspec/hax/issues/156.
-Please upvote or comment this issue if you see this error message.
-Sorry, Hax does not support declare-first let bindings (see https://doc.rust-lang.org/rust-by-example/variable_bindings/declare.html) for now.\u001B[0m
-  \u001B[1m\u001B[94m-->\u001B[0m literals/src/lib.rs:43:21
-\u001B[1m\u001B[94m   |\u001B[0m
-\u001B[1m\u001B[94m43 |\u001B[0m #[derive(PartialEq, Eq)]
-\u001B[1m\u001B[94m   |\u001B[0m\u001B[1m\u001B[91m                     ^^\u001B[0m
-\u001B[1m\u001B[94m   |\u001B[0m"""
-[[stdout.diagnostics]]
-message = '''
-(AST import) something is not implemented yet.This is discussed in issue https://github.com/hacspec/hax/issues/156.
-Please upvote or comment this issue if you see this error message.
-Sorry, Hax does not support declare-first let bindings (see https://doc.rust-lang.org/rust-by-example/variable_bindings/declare.html) for now.'''
-spans = ['Span { lo: Loc { line: 43, col: 20 }, hi: Loc { line: 43, col: 22 }, filename: Real(LocalPath("literals/src/lib.rs")), rust_span_data: None }']
+exit = 0
+stderr = 'Finished `dev` profile [unoptimized + debuginfo] target(s) in XXs'
+
+[stdout]
+diagnostics = []
 
 [stdout.files]
 "Literals.fst" = '''
@@ -97,28 +85,25 @@ let panic_with_msg (_: Prims.unit) : Prims.unit =
 type t_Foo = { f_field:u8 }
 
 [@@ FStar.Tactics.Typeclasses.tcinstance]
-let impl: Core.Marker.t_StructuralPartialEq t_Foo = { __marker_trait = () }
+assume
+val impl': Core.Marker.t_StructuralPartialEq t_Foo
+
+unfold
+let impl = impl'
 
 [@@ FStar.Tactics.Typeclasses.tcinstance]
-let impl_1: Core.Cmp.t_PartialEq t_Foo t_Foo =
-  {
-    f_eq_pre = (fun (self: t_Foo) (other: t_Foo) -> true);
-    f_eq_post = (fun (self: t_Foo) (other: t_Foo) (out: bool) -> true);
-    f_eq = fun (self: t_Foo) (other: t_Foo) -> self.f_field =. other.f_field
-  }
+assume
+val impl_1': Core.Cmp.t_PartialEq t_Foo t_Foo
+
+unfold
+let impl_1 = impl_1'
 
 [@@ FStar.Tactics.Typeclasses.tcinstance]
-let impl_2: Core.Cmp.t_Eq t_Foo =
-  {
-    _super_5579681813951091494 = FStar.Tactics.Typeclasses.solve;
-    f_assert_receiver_is_total_eq_pre = (fun (self: t_Foo) -> true);
-    f_assert_receiver_is_total_eq_post = (fun (self: t_Foo) (out: Prims.unit) -> true);
-    f_assert_receiver_is_total_eq
-    =
-    fun (self: t_Foo) ->
-      Rust_primitives.Hax.failure "(AST import) something is not implemented yet.This is discussed in issue https://github.com/hacspec/hax/issues/156.\nPlease upvote or comment this issue if you see this error message.\nSorry, Hax does not support declare-first let bindings (see https://doc.rust-lang.org/rust-by-example/variable_bindings/declare.html) for now."
-        ""
-  }
+assume
+val impl_2': Core.Cmp.t_Eq t_Foo
+
+unfold
+let impl_2 = impl_2'
 
 let v_CONSTANT: t_Foo = { f_field = mk_u8 3 } <: t_Foo
 

From 4d0da17cbd77958eee4b41f0af4ee9562364a921 Mon Sep 17 00:00:00 2001
From: Lucas Franceschino <lucas@cryspen.com>
Date: Mon, 21 Jul 2025 16:15:28 +0200
Subject: [PATCH 17/18] chore(frontend/exporter): drop some attribute support
 for now

We are probably not going to use most of attribute
kinds. After chatting with @nadrieril, for easing
rustc updates, I'm dropping most of the attributes
kinds, hinding them behind a `Todo` variant.
---
 frontend/exporter/src/types/attributes.rs | 218 +---------------------
 1 file changed, 7 insertions(+), 211 deletions(-)

diff --git a/frontend/exporter/src/types/attributes.rs b/frontend/exporter/src/types/attributes.rs
index eeb9af537..46daa568b 100644
--- a/frontend/exporter/src/types/attributes.rs
+++ b/frontend/exporter/src/types/attributes.rs
@@ -13,142 +13,31 @@ pub enum AttributeKind {
         align: Align,
         span: Span,
     },
-    AllowConstFnUnstable(Vec<Symbol>, Span),
-    AllowIncoherentImpl(Span),
-    AllowInternalUnstable(Vec<(Symbol, Span)>, Span),
-    AsPtr(Span),
     AutomaticallyDerived(Span),
-    BodyStability {
-        stability: DefaultBodyStability,
-        span: Span,
-    },
-    CoherenceIsCore,
-    Coinductive(Span),
-    Cold(Span),
-    Confusables {
-        symbols: Vec<Symbol>,
-        first_span: Span,
-    },
-    ConstContinue(Span),
-    ConstStability {
-        stability: PartialConstStability,
-        span: Span,
-    },
-    ConstStabilityIndirect,
-    ConstTrait(Span),
     Coverage(Span, CoverageStatus),
-    DenyExplicitImpl(Span),
     Deprecation {
         deprecation: Deprecation,
         span: Span,
     },
-    DoNotImplementViaObject(Span),
     DocComment {
         style: AttrStyle,
         kind: CommentKind,
         span: Span,
         comment: Symbol,
     },
-    Dummy,
-    ExportName {
-        name: Symbol,
-        span: Span,
-    },
-    ExportStable,
-    FfiConst(Span),
-    FfiPure(Span),
-    Fundamental,
     Ignore {
         span: Span,
         reason: Option<Symbol>,
     },
-    Inline(InlineAttr, Span),
-    LinkName {
-        name: Symbol,
-        span: Span,
-    },
-    LinkOrdinal {
-        ordinal: u16,
-        span: Span,
-    },
-    LinkSection {
-        name: Symbol,
-        span: Span,
-    },
-    LoopMatch(Span),
-    MacroTransparency(Transparency),
     Marker(Span),
     MayDangle(Span),
     MustUse {
         span: Span,
         reason: Option<Symbol>,
     },
-    Naked(Span),
-    NoImplicitPrelude(Span),
-    NoMangle(Span),
-    NonExhaustive(Span),
-    OmitGdbPrettyPrinterSection,
-    Optimize(OptimizeAttr, Span),
-    ParenSugar(Span),
-    PassByValue(Span),
     Path(Symbol, Span),
-    Pointee(Span),
-    PubTransparent(Span),
-    Repr {
-        reprs: Vec<(ReprAttr, Span)>,
-        first_span: Span,
-    },
-    RustcLayoutScalarValidRangeEnd(u128, Span),
-    RustcLayoutScalarValidRangeStart(u128, Span),
-    RustcObjectLifetimeDefault,
-    SkipDuringMethodDispatch {
-        array: bool,
-        boxed_slice: bool,
-        span: Span,
-    },
-    SpecializationTrait(Span),
-    Stability {
-        stability: Stability,
-        span: Span,
-    },
-    StdInternalSymbol(Span),
-    TargetFeature(Vec<(Symbol, Span)>, Span),
-    TrackCaller(Span),
-    TypeConst(Span),
-    UnsafeSpecializationMarker(Span),
-    UnstableFeatureBound(Vec<(Symbol, Span)>),
-    Used {
-        used_by: UsedBy,
-        span: Span,
-    },
-}
-
-/// Reflects [`rustc_span::hygiene::Transparency`]
-#[derive_group(Serializers)]
-#[derive(AdtInto, Clone, Debug, JsonSchema, Hash, PartialEq, Eq, PartialOrd, Ord)]
-#[args(<'tcx, S>, from: rustc_span::hygiene::Transparency, state: S as _s)]
-pub enum Transparency {
-    Transparent,
-    SemiOpaque,
-    Opaque,
-}
-
-/// Reflects [`rustc_attr_data_structures::Stability`]
-#[derive_group(Serializers)]
-#[derive(AdtInto, Clone, Debug, JsonSchema, Hash, PartialEq, Eq, PartialOrd, Ord)]
-#[args(<'tcx, S>, from: rustc_attr_data_structures::Stability, state: S as _s)]
-pub struct Stability {
-    pub level: StabilityLevel,
-    pub feature: Symbol,
-}
-
-/// Reflects [`rustc_attr_data_structures::DefaultBodyStability`]
-#[derive_group(Serializers)]
-#[derive(AdtInto, Clone, Debug, JsonSchema, Hash, PartialEq, Eq, PartialOrd, Ord)]
-#[args(<'tcx, S>, from: rustc_attr_data_structures::DefaultBodyStability, state: S as _s)]
-pub struct DefaultBodyStability {
-    pub level: StabilityLevel,
-    pub feature: Symbol,
+    #[todo]
+    Todo(String),
 }
 
 /// Reflects [`rustc_attr_data_structures::Deprecation`]
@@ -173,76 +62,6 @@ pub enum DeprecatedSince {
     Err,
 }
 
-/// Reflects [`rustc_attr_data_structures::ReprAttr`]
-#[derive_group(Serializers)]
-#[derive(AdtInto, Clone, Debug, JsonSchema, Hash, PartialEq, Eq, PartialOrd, Ord)]
-#[args(<'tcx, S>, from: rustc_attr_data_structures::ReprAttr, state: S as _s)]
-pub enum ReprAttr {
-    ReprInt(IntType),
-    ReprRust,
-    ReprC,
-    ReprPacked(Align),
-    ReprSimd,
-    ReprTransparent,
-    ReprAlign(Align),
-}
-
-/// Reflects [`rustc_attr_data_structures::IntType`]
-#[derive_group(Serializers)]
-#[derive(AdtInto, Clone, Debug, JsonSchema, Hash, PartialEq, Eq, PartialOrd, Ord)]
-#[args(<'tcx, S>, from: rustc_attr_data_structures::IntType, state: S as _s)]
-pub enum IntType {
-    SignedInt(IntTy),
-    UnsignedInt(UintTy),
-}
-
-/// Reflects [`rustc_attr_data_structures::UsedBy`]
-#[derive_group(Serializers)]
-#[derive(AdtInto, Clone, Debug, JsonSchema, Hash, PartialEq, Eq, PartialOrd, Ord)]
-#[args(<'tcx, S>, from: rustc_attr_data_structures::UsedBy, state: S as _s)]
-pub enum UsedBy {
-    Compiler,
-    Linker,
-}
-
-/// Reflects [`rustc_attr_data_structures::StabilityLevel`]
-#[derive_group(Serializers)]
-#[derive(AdtInto, Clone, Debug, JsonSchema, Hash, PartialEq, Eq, PartialOrd, Ord)]
-#[args(<'tcx, S>, from: rustc_attr_data_structures::StabilityLevel, state: S as _s)]
-pub enum StabilityLevel {
-    Unstable {
-        reason: UnstableReason,
-        #[map(x.map(|x| x.get()))]
-        issue: Option<u32>,
-        is_soft: bool,
-        implied_by: Option<Symbol>,
-        old_name: Option<Symbol>,
-    },
-    Stable {
-        since: StableSince,
-        allowed_through_unstable_modules: Option<Symbol>,
-    },
-}
-
-/// Reflects [`rustc_attr_data_structures::CoverageStatus`]
-#[derive_group(Serializers)]
-#[derive(AdtInto, Clone, Debug, JsonSchema, Hash, PartialEq, Eq, PartialOrd, Ord)]
-#[args(<'tcx, S>, from: rustc_attr_data_structures::CoverageStatus, state: S as _s)]
-pub enum CoverageStatus {
-    On,
-    Off,
-}
-
-/// Reflects [`rustc_attr_data_structures::PartialConstStability`]
-#[derive_group(Serializers)]
-#[derive(AdtInto, Clone, Debug, JsonSchema, Hash, PartialEq, Eq, PartialOrd, Ord)]
-#[args(<'tcx, S>, from: rustc_attr_data_structures::PartialConstStability, state: S as _s)]
-pub struct PartialConstStability {
-    pub level: StabilityLevel,
-    pub feature: Symbol,
-    pub promotable: bool,
-}
-
 /// Reflects [`rustc_attr_data_structures::RustcVersion`]
 #[derive_group(Serializers)]
 #[derive(AdtInto, Clone, Debug, JsonSchema, Hash, PartialEq, Eq, PartialOrd, Ord)]
@@ -253,36 +72,13 @@ pub struct RustcVersion {
     pub patch: u16,
 }
 
-/// Reflects [`rustc_attr_data_structures::StableSince`]
-#[derive_group(Serializers)]
-#[derive(AdtInto, Clone, Debug, JsonSchema, Hash, PartialEq, Eq, PartialOrd, Ord)]
-#[args(<'tcx, S>, from: rustc_attr_data_structures::StableSince, state: S as _s)]
-pub enum StableSince {
-    Version(RustcVersion),
-    Current,
-    #[custom_arm(rustc_attr_data_structures::StableSince::Err(_) => StableSince::Err,)]
-    Err,
-}
-
-/// Reflects [`rustc_attr_data_structures::UnstableReason`]
-#[derive_group(Serializers)]
-#[derive(AdtInto, Clone, Debug, JsonSchema, Hash, PartialEq, Eq, PartialOrd, Ord)]
-#[args(<'tcx, S>, from: rustc_attr_data_structures::UnstableReason, state: S as _s)]
-pub enum UnstableReason {
-    None,
-    Default,
-    Some(Symbol),
-}
-
-/// Reflects [`rustc_attr_data_structures::OptimizeAttr`]
+/// Reflects [`rustc_attr_data_structures::CoverageStatus`]
 #[derive_group(Serializers)]
 #[derive(AdtInto, Clone, Debug, JsonSchema, Hash, PartialEq, Eq, PartialOrd, Ord)]
-#[args(<'tcx, S>, from: rustc_attr_data_structures::OptimizeAttr, state: S as _s)]
-pub enum OptimizeAttr {
-    Default,
-    DoNotOptimize,
-    Speed,
-    Size,
+#[args(<'tcx, S>, from: rustc_attr_data_structures::CoverageStatus, state: S as _s)]
+pub enum CoverageStatus {
+    On,
+    Off,
 }
 
 /// Reflects [`rustc_attr_data_structures::InlineAttr`]

From 51849642d4cc494aca4f13b643f84eb00faedeb5 Mon Sep 17 00:00:00 2001
From: Lucas Franceschino <lucas@cryspen.com>
Date: Mon, 21 Jul 2025 16:52:01 +0200
Subject: [PATCH 18/18] chore: update rustc-coverage-tests

---
 .../snapshots/fstar/Coverage.Attr.Trait_impl_inherit.fst        | 2 +-
 1 file changed, 1 insertion(+), 1 deletion(-)

diff --git a/rustc-coverage-tests/snapshots/fstar/Coverage.Attr.Trait_impl_inherit.fst b/rustc-coverage-tests/snapshots/fstar/Coverage.Attr.Trait_impl_inherit.fst
index ba2090ae0..964a2565b 100644
--- a/rustc-coverage-tests/snapshots/fstar/Coverage.Attr.Trait_impl_inherit.fst
+++ b/rustc-coverage-tests/snapshots/fstar/Coverage.Attr.Trait_impl_inherit.fst
@@ -6,7 +6,7 @@ open FStar.Mul
 (* item error backend: (reject_TraitItemDefault) ExplicitRejection { reason: "a node of kind [Trait_item_default] have been found in the AST" }
 Last available AST for this item:
 
-#[path()]#[<cfg>(any(feature = "json"))]#[feature(coverage_attribute)]#[<cfg>(any(feature = "json", feature = "fstar", feature = "fstar-lax", feature =
+#[<cfg>(any(feature = "json"))]#[feature(coverage_attribute)]#[<cfg>(any(feature = "json", feature = "fstar", feature = "fstar-lax", feature =
 "coq"))]#[feature(coverage_attribute)]#[allow(unused_attributes)]#[allow(dead_code)]#[allow(unreachable_code)]#[feature(register_tool)]#[register_tool(_hax)]trait t_T<Self_>{fn f_f((self: Self)) -> tuple0{{let _: tuple0 = {std::io::stdio::e_print(core::fmt::rt::impl_1__new_const::<generic_value!(todo)>(["default\n"]))};{let _: tuple0 = {Tuple0};Tuple0}}}}
 
 Last AST: