feat(engine/specialize): monorphize to_int into from_machine

cryspen · Feb 18, 2025 · 927c221 · 927c221
1 parent 96967d4
commit 927c221
Show file tree

Hide file tree

Showing 2 changed files with 3 additions and 0 deletions.
diff --git a/engine/lib/phases/phase_specialize.ml b/engine/lib/phases/phase_specialize.ml
@@ -174,6 +174,8 @@ module Make (F : Features.T) =
             rint_rint_any Core__cmp__PartialEq__eq Rust_primitives__hax__int__eq;
             any_int Hax_lib__abstraction__Abstraction__lift
               Rust_primitives__hax__int__from_machine;
+            any_int Hax_lib__int__ToInt__to_int
+              Rust_primitives__hax__int__from_machine;
             int_any Hax_lib__abstraction__Concretization__concretize
               Rust_primitives__hax__int__into_machine;
           ]

diff --git a/engine/names/src/lib.rs b/engine/names/src/lib.rs
@@ -82,6 +82,7 @@ fn dummy_hax_concrete_ident_wrapper<I: core::iter::Iterator<Item = u8>>(x: I, mu
     {
         use hax_lib::*;
         let a: Int = 3u8.lift();
+        let _: Int = 3u8.to_int();
         let _ = a.clone().pow2();
         let _ = Int::_unsafe_from_str("1");
         let _: u32 = a.concretize();