From 79acdace4dc2ea269766812f2b901d60c28b908a Mon Sep 17 00:00:00 2001
From: Maxime Buyse <maxime@cryspen.com>
Date: Wed, 6 May 2026 12:22:41 +0200
Subject: [PATCH 1/5] Fix missing tests for TryFrom on integers and wrong i32
 to isize TryFrom.

---
 core-models/src/core/convert.rs | 49 ++++++++++++++++++++++++---------
 1 file changed, 36 insertions(+), 13 deletions(-)

diff --git a/core-models/src/core/convert.rs b/core-models/src/core/convert.rs
index 1c903ea..21ee4d9 100644
--- a/core-models/src/core/convert.rs
+++ b/core-models/src/core/convert.rs
@@ -131,6 +131,23 @@ macro_rules! int_try_from {
     }
 }
 
+macro_rules! int_try_from_trivial {
+    (
+        $($From_t: ident)*,
+        $($To_t: ident)*,
+    ) => {
+        $(
+            #[cfg_attr(hax_backend_lean, hax_lib::exclude)]
+            impl TryFrom<$From_t> for $To_t {
+                type Error = TryFromIntError;
+                fn try_from(x: $From_t) -> Result<$To_t, TryFromIntError> {
+                    Result::Ok(x as $To_t)
+                }
+            }
+        )*
+    }
+}
+
 int_from! {
     u8  u8  u16 u8  u16 u32 u8   u16  u32  u64  usize u8    u16,
     u16 u32 u32 u64 u64 u64 u128 u128 u128 u128 u128  usize usize,
@@ -147,8 +164,14 @@ int_try_from! {
 }
 
 int_try_from! {
-    i16 i32 i32 i32   i64 i64 i64 i64   i128 i128 i128 i128 i128  isize isize isize isize,
-    i8  i8  i16 isize i8  i16 i32 isize i8   i16  i32  i64  isize i8    i16   i32   i64,
+    i16 i32 i32 i64 i64 i64 i64   i128 i128 i128 i128 i128  isize isize isize isize,
+    i8  i8  i16 i8  i16 i32 isize i8   i16  i32  i64  isize i8    i16   i32   i64,
+}
+
+// We assume a 64-bits machine
+int_try_from_trivial!{
+    i32,
+    isize, 
 }
 
 #[cfg(test)]
@@ -201,10 +224,10 @@ mod tests {
                     $(
                         proptest!{
                             #[test]
-                            fn [<test_try_from_$From_t _to_ $To_t>](x in any::<u16>()) {
+                            fn [<test_try_from_$From_t _to_ $To_t>](x in any::<$From_t>()) {
                                 prop_assert_eq!(
-                                    <u8 as super::TryFrom<u16>>::try_from(x.inject()),
-                                    u8::try_from(x).inject()
+                                    <$To_t as super::TryFrom<$From_t>>::try_from(x.inject()),
+                                    $To_t::try_from(x).inject()
                                 );
                             }
                         }
@@ -214,23 +237,23 @@ mod tests {
         }
 
     int_from_test! {
-        u8  u8  u16 u8  u16 u32 u8   u16  u32  u64  u8    u16,
-        u16 u32 u32 u64 u64 u64 u128 u128 u128 u128 usize usize,
+        u8  u8  u16 u8  u16 u32 u8   u16  u32  u64  usize u8    u16,
+        u16 u32 u32 u64 u64 u64 u128 u128 u128 u128 u128 usize usize,
     }
 
     int_from_test! {
-        i8  i8  i16 i8  i16 i32 i8   i16  i32  i64  i8    i16,
-        i16 i32 i32 i64 i64 i64 i128 i128 i128 i128 isize isize,
+        i8  i8  i16 i8  i16 i32 i8   i16  i32  i64  isize i8    i16,
+        i16 i32 i32 i64 i64 i64 i128 i128 i128 i128 i128  isize isize,
     }
 
     int_try_from_test! {
-        u16 u32 u32 u32   u64 u64 u64 u64   u128 u128 u128 u128 u128  usize usize usize usize usize,
-        u8  u8  u16 usize u8  u16 u32 usize u8   u16  u32  u64  usize u8    u16   u32   u64   u128,
+        u16 u32 u32 u32   u64 u64 u64 u64   u128 u128 u128 u128 u128  usize usize usize usize,
+        u8  u8  u16 usize u8  u16 u32 usize u8   u16  u32  u64  usize u8    u16   u32   u64,
     }
 
     int_try_from_test! {
-        i16 i32 i32 i32   i64 i64 i64 i64   i128 i128 i128 i128 i128  isize isize isize isize isize,
-        i8  i8  i16 isize i8  i16 i32 isize i8   i16  i32  i64  isize i8    i16   i32   i64   i128,
+        i16 i32 i32 i32   i64 i64 i64 i64   i128 i128 i128 i128 i128  isize isize isize isize,
+        i8  i8  i16 isize i8  i16 i32 isize i8   i16  i32  i64  isize i8    i16   i32   i64,
     }
 
     proptest! {

From 9459a9400fa123438ce7109c491b09fa601bc838 Mon Sep 17 00:00:00 2001
From: Maxime Buyse <maxime@cryspen.com>
Date: Wed, 6 May 2026 12:23:00 +0200
Subject: [PATCH 2/5] Bump aeneas core-models-lib version.

---
 .github/workflows/ci.yml          |   2 +-
 lean/CoreModels/Funs.lean         | 329 +++++++++++++++---------------
 lean/CoreModels/FunsExternal.lean |  24 +--
 3 files changed, 174 insertions(+), 181 deletions(-)

diff --git a/.github/workflows/ci.yml b/.github/workflows/ci.yml
index 39e06ae..a2c1171 100644
--- a/.github/workflows/ci.yml
+++ b/.github/workflows/ci.yml
@@ -10,7 +10,7 @@ on:
 env:
   RUST_TOOLCHAIN: nightly-2026-02-07
   CHARON_REV:    ed22146b1cd4d0b578006a58b3299d41ecbe0fd4
-  AENEAS_REV:    863909afa638edd449035a56ba76801c57c9213d
+  AENEAS_REV:    b5c45e849a4959ba80526ffd6c19063e72cb354a
   # Where the cache step stages the charon / aeneas binaries.
   AENEAS_DIR: ${{ github.workspace }}/.tools/aeneas
 
diff --git a/lean/CoreModels/Funs.lean b/lean/CoreModels/Funs.lean
index 31f6668..30665a6 100644
--- a/lean/CoreModels/Funs.lean
+++ b/lean/CoreModels/Funs.lean
@@ -1752,30 +1752,6 @@ def I16.Insts.Core_modelsConvertTryFromI32TryFromIntError : convert.TryFrom
   try_from := I16.Insts.Core_modelsConvertTryFromI32TryFromIntError.try_from
 }
 
-/-- [core_models::convert::{core_models::convert::TryFrom<i32, core_models::num::error::TryFromIntError> for isize}::try_from]:
-    Source: 'core-models/src/core/convert.rs', lines 122:16-128:17 -/
-def Isize.Insts.Core_modelsConvertTryFromI32TryFromIntError.try_from
-  (x : Std.I32) :
-  Result (result.Result Std.Isize num.error.TryFromIntError)
-  := do
-  let i ← lift (IScalar.cast .I32 core_models.num.Isize.MAX)
-  if x > i
-  then ok (result.Result.Err ())
-  else
-    let i1 ← lift (IScalar.cast .I32 core_models.num.Isize.MIN)
-    if x < i1
-    then ok (result.Result.Err ())
-    else let i2 ← lift (IScalar.cast .Isize x)
-         ok (result.Result.Ok i2)
-
-/-- Trait implementation: [core_models::convert::{core_models::convert::TryFrom<i32, core_models::num::error::TryFromIntError> for isize}]
-    Source: 'core-models/src/core/convert.rs', lines 120:12-129:13 -/
-@[reducible]
-def Isize.Insts.Core_modelsConvertTryFromI32TryFromIntError : convert.TryFrom
-  Std.Isize Std.I32 num.error.TryFromIntError := {
-  try_from := Isize.Insts.Core_modelsConvertTryFromI32TryFromIntError.try_from
-}
-
 /-- [core_models::convert::{core_models::convert::TryFrom<i64, core_models::num::error::TryFromIntError> for i8}::try_from]:
     Source: 'core-models/src/core/convert.rs', lines 122:16-128:17 -/
 def I8.Insts.Core_modelsConvertTryFromI64TryFromIntError.try_from
@@ -2086,6 +2062,23 @@ def I64.Insts.Core_modelsConvertTryFromIsizeTryFromIntError : convert.TryFrom
   try_from := I64.Insts.Core_modelsConvertTryFromIsizeTryFromIntError.try_from
 }
 
+/-- [core_models::convert::{core_models::convert::TryFrom<i32, core_models::num::error::TryFromIntError> for isize}::try_from]:
+    Source: 'core-models/src/core/convert.rs', lines 143:16-145:17 -/
+def Isize.Insts.Core_modelsConvertTryFromI32TryFromIntError.try_from
+  (x : Std.I32) :
+  Result (result.Result Std.Isize num.error.TryFromIntError)
+  := do
+  let i ← lift (IScalar.cast .Isize x)
+  ok (result.Result.Ok i)
+
+/-- Trait implementation: [core_models::convert::{core_models::convert::TryFrom<i32, core_models::num::error::TryFromIntError> for isize}]
+    Source: 'core-models/src/core/convert.rs', lines 141:12-146:13 -/
+@[reducible]
+def Isize.Insts.Core_modelsConvertTryFromI32TryFromIntError : convert.TryFrom
+  Std.Isize Std.I32 num.error.TryFromIntError := {
+  try_from := Isize.Insts.Core_modelsConvertTryFromI32TryFromIntError.try_from
+}
+
 /-- [core_models::f32::{core_models::f32::f32}::abs]:
     Source: 'core-models/src/core/f32.rs', lines 9:4-11:5 -/
 def f32.f32.abs (x : F64) : Result F64 := do
@@ -3103,15 +3096,15 @@ def num.Usize.overflowing_add
     Source: 'core-models/src/core/num/mod.rs', lines 39:12-47:13 -/
 def num.U8.checked_add
   (x : Std.U8) (y : Std.U8) : Result (option.Option Std.U8) := do
-  let i ← U8.Insts.Hax_libIntToInt.to_int num.U8.MIN
-  let i1 ← U8.Insts.Hax_libIntToInt.to_int x
-  let i2 ← U8.Insts.Hax_libIntToInt.to_int y
+  let i ← hax_lib.U8.Insts.Hax_libIntToInt.to_int num.U8.MIN
+  let i1 ← hax_lib.U8.Insts.Hax_libIntToInt.to_int x
+  let i2 ← hax_lib.U8.Insts.Hax_libIntToInt.to_int y
   let i3 ← hax_lib.int.Int.Insts.Core_modelsOpsArithAddIntInt.add i1 i2
   let b ← hax_lib.int.Int.Insts.Core_modelsCmpPartialOrdInt.le i i3
   if b
   then
     let i4 ← hax_lib.int.Int.Insts.Core_modelsOpsArithAddIntInt.add i1 i2
-    let i5 ← U8.Insts.Hax_libIntToInt.to_int num.U8.MAX
+    let i5 ← hax_lib.U8.Insts.Hax_libIntToInt.to_int num.U8.MAX
     let b1 ← hax_lib.int.Int.Insts.Core_modelsCmpPartialOrdInt.le i4 i5
     if b1
     then let i6 ← x + y
@@ -3123,15 +3116,15 @@ def num.U8.checked_add
     Source: 'core-models/src/core/num/mod.rs', lines 39:12-47:13 -/
 def num.U16.checked_add
   (x : Std.U16) (y : Std.U16) : Result (option.Option Std.U16) := do
-  let i ← U16.Insts.Hax_libIntToInt.to_int num.U16.MIN
-  let i1 ← U16.Insts.Hax_libIntToInt.to_int x
-  let i2 ← U16.Insts.Hax_libIntToInt.to_int y
+  let i ← hax_lib.U16.Insts.Hax_libIntToInt.to_int num.U16.MIN
+  let i1 ← hax_lib.U16.Insts.Hax_libIntToInt.to_int x
+  let i2 ← hax_lib.U16.Insts.Hax_libIntToInt.to_int y
   let i3 ← hax_lib.int.Int.Insts.Core_modelsOpsArithAddIntInt.add i1 i2
   let b ← hax_lib.int.Int.Insts.Core_modelsCmpPartialOrdInt.le i i3
   if b
   then
     let i4 ← hax_lib.int.Int.Insts.Core_modelsOpsArithAddIntInt.add i1 i2
-    let i5 ← U16.Insts.Hax_libIntToInt.to_int num.U16.MAX
+    let i5 ← hax_lib.U16.Insts.Hax_libIntToInt.to_int num.U16.MAX
     let b1 ← hax_lib.int.Int.Insts.Core_modelsCmpPartialOrdInt.le i4 i5
     if b1
     then let i6 ← x + y
@@ -3143,15 +3136,15 @@ def num.U16.checked_add
     Source: 'core-models/src/core/num/mod.rs', lines 39:12-47:13 -/
 def num.U32.checked_add
   (x : Std.U32) (y : Std.U32) : Result (option.Option Std.U32) := do
-  let i ← U32.Insts.Hax_libIntToInt.to_int num.U32.MIN
-  let i1 ← U32.Insts.Hax_libIntToInt.to_int x
-  let i2 ← U32.Insts.Hax_libIntToInt.to_int y
+  let i ← hax_lib.U32.Insts.Hax_libIntToInt.to_int num.U32.MIN
+  let i1 ← hax_lib.U32.Insts.Hax_libIntToInt.to_int x
+  let i2 ← hax_lib.U32.Insts.Hax_libIntToInt.to_int y
   let i3 ← hax_lib.int.Int.Insts.Core_modelsOpsArithAddIntInt.add i1 i2
   let b ← hax_lib.int.Int.Insts.Core_modelsCmpPartialOrdInt.le i i3
   if b
   then
     let i4 ← hax_lib.int.Int.Insts.Core_modelsOpsArithAddIntInt.add i1 i2
-    let i5 ← U32.Insts.Hax_libIntToInt.to_int num.U32.MAX
+    let i5 ← hax_lib.U32.Insts.Hax_libIntToInt.to_int num.U32.MAX
     let b1 ← hax_lib.int.Int.Insts.Core_modelsCmpPartialOrdInt.le i4 i5
     if b1
     then let i6 ← x + y
@@ -3163,15 +3156,15 @@ def num.U32.checked_add
     Source: 'core-models/src/core/num/mod.rs', lines 39:12-47:13 -/
 def num.U64.checked_add
   (x : Std.U64) (y : Std.U64) : Result (option.Option Std.U64) := do
-  let i ← U64.Insts.Hax_libIntToInt.to_int num.U64.MIN
-  let i1 ← U64.Insts.Hax_libIntToInt.to_int x
-  let i2 ← U64.Insts.Hax_libIntToInt.to_int y
+  let i ← hax_lib.U64.Insts.Hax_libIntToInt.to_int num.U64.MIN
+  let i1 ← hax_lib.U64.Insts.Hax_libIntToInt.to_int x
+  let i2 ← hax_lib.U64.Insts.Hax_libIntToInt.to_int y
   let i3 ← hax_lib.int.Int.Insts.Core_modelsOpsArithAddIntInt.add i1 i2
   let b ← hax_lib.int.Int.Insts.Core_modelsCmpPartialOrdInt.le i i3
   if b
   then
     let i4 ← hax_lib.int.Int.Insts.Core_modelsOpsArithAddIntInt.add i1 i2
-    let i5 ← U64.Insts.Hax_libIntToInt.to_int num.U64.MAX
+    let i5 ← hax_lib.U64.Insts.Hax_libIntToInt.to_int num.U64.MAX
     let b1 ← hax_lib.int.Int.Insts.Core_modelsCmpPartialOrdInt.le i4 i5
     if b1
     then let i6 ← x + y
@@ -3183,15 +3176,15 @@ def num.U64.checked_add
     Source: 'core-models/src/core/num/mod.rs', lines 39:12-47:13 -/
 def num.U128.checked_add
   (x : Std.U128) (y : Std.U128) : Result (option.Option Std.U128) := do
-  let i ← U128.Insts.Hax_libIntToInt.to_int num.U128.MIN
-  let i1 ← U128.Insts.Hax_libIntToInt.to_int x
-  let i2 ← U128.Insts.Hax_libIntToInt.to_int y
+  let i ← hax_lib.U128.Insts.Hax_libIntToInt.to_int num.U128.MIN
+  let i1 ← hax_lib.U128.Insts.Hax_libIntToInt.to_int x
+  let i2 ← hax_lib.U128.Insts.Hax_libIntToInt.to_int y
   let i3 ← hax_lib.int.Int.Insts.Core_modelsOpsArithAddIntInt.add i1 i2
   let b ← hax_lib.int.Int.Insts.Core_modelsCmpPartialOrdInt.le i i3
   if b
   then
     let i4 ← hax_lib.int.Int.Insts.Core_modelsOpsArithAddIntInt.add i1 i2
-    let i5 ← U128.Insts.Hax_libIntToInt.to_int num.U128.MAX
+    let i5 ← hax_lib.U128.Insts.Hax_libIntToInt.to_int num.U128.MAX
     let b1 ← hax_lib.int.Int.Insts.Core_modelsCmpPartialOrdInt.le i4 i5
     if b1
     then let i6 ← x + y
@@ -3203,16 +3196,16 @@ def num.U128.checked_add
     Source: 'core-models/src/core/num/mod.rs', lines 39:12-47:13 -/
 def num.Usize.checked_add
   (x : Std.Usize) (y : Std.Usize) : Result (option.Option Std.Usize) := do
-  let i ← Usize.Insts.Hax_libIntToInt.to_int num.Usize.MIN
-  let i1 ← Usize.Insts.Hax_libIntToInt.to_int x
-  let i2 ← Usize.Insts.Hax_libIntToInt.to_int y
+  let i ← hax_lib.Usize.Insts.Hax_libIntToInt.to_int num.Usize.MIN
+  let i1 ← hax_lib.Usize.Insts.Hax_libIntToInt.to_int x
+  let i2 ← hax_lib.Usize.Insts.Hax_libIntToInt.to_int y
   let i3 ← hax_lib.int.Int.Insts.Core_modelsOpsArithAddIntInt.add i1 i2
   let b ← hax_lib.int.Int.Insts.Core_modelsCmpPartialOrdInt.le i i3
   if b
   then
     let i4 ← hax_lib.int.Int.Insts.Core_modelsOpsArithAddIntInt.add i1 i2
     let i5 := num.Usize.MAX
-    let i6 ← Usize.Insts.Hax_libIntToInt.to_int i5
+    let i6 ← hax_lib.Usize.Insts.Hax_libIntToInt.to_int i5
     let b1 ← hax_lib.int.Int.Insts.Core_modelsCmpPartialOrdInt.le i4 i6
     if b1
     then let i7 ← x + y
@@ -3323,15 +3316,15 @@ def num.Usize.overflowing_sub
     Source: 'core-models/src/core/num/mod.rs', lines 61:12-69:13 -/
 def num.U8.checked_sub
   (x : Std.U8) (y : Std.U8) : Result (option.Option Std.U8) := do
-  let i ← U8.Insts.Hax_libIntToInt.to_int num.U8.MIN
-  let i1 ← U8.Insts.Hax_libIntToInt.to_int x
-  let i2 ← U8.Insts.Hax_libIntToInt.to_int y
+  let i ← hax_lib.U8.Insts.Hax_libIntToInt.to_int num.U8.MIN
+  let i1 ← hax_lib.U8.Insts.Hax_libIntToInt.to_int x
+  let i2 ← hax_lib.U8.Insts.Hax_libIntToInt.to_int y
   let i3 ← hax_lib.int.Int.Insts.Core_modelsOpsArithSubIntInt.sub i1 i2
   let b ← hax_lib.int.Int.Insts.Core_modelsCmpPartialOrdInt.le i i3
   if b
   then
     let i4 ← hax_lib.int.Int.Insts.Core_modelsOpsArithSubIntInt.sub i1 i2
-    let i5 ← U8.Insts.Hax_libIntToInt.to_int num.U8.MAX
+    let i5 ← hax_lib.U8.Insts.Hax_libIntToInt.to_int num.U8.MAX
     let b1 ← hax_lib.int.Int.Insts.Core_modelsCmpPartialOrdInt.le i4 i5
     if b1
     then let i6 ← x - y
@@ -3343,15 +3336,15 @@ def num.U8.checked_sub
     Source: 'core-models/src/core/num/mod.rs', lines 61:12-69:13 -/
 def num.U16.checked_sub
   (x : Std.U16) (y : Std.U16) : Result (option.Option Std.U16) := do
-  let i ← U16.Insts.Hax_libIntToInt.to_int num.U16.MIN
-  let i1 ← U16.Insts.Hax_libIntToInt.to_int x
-  let i2 ← U16.Insts.Hax_libIntToInt.to_int y
+  let i ← hax_lib.U16.Insts.Hax_libIntToInt.to_int num.U16.MIN
+  let i1 ← hax_lib.U16.Insts.Hax_libIntToInt.to_int x
+  let i2 ← hax_lib.U16.Insts.Hax_libIntToInt.to_int y
   let i3 ← hax_lib.int.Int.Insts.Core_modelsOpsArithSubIntInt.sub i1 i2
   let b ← hax_lib.int.Int.Insts.Core_modelsCmpPartialOrdInt.le i i3
   if b
   then
     let i4 ← hax_lib.int.Int.Insts.Core_modelsOpsArithSubIntInt.sub i1 i2
-    let i5 ← U16.Insts.Hax_libIntToInt.to_int num.U16.MAX
+    let i5 ← hax_lib.U16.Insts.Hax_libIntToInt.to_int num.U16.MAX
     let b1 ← hax_lib.int.Int.Insts.Core_modelsCmpPartialOrdInt.le i4 i5
     if b1
     then let i6 ← x - y
@@ -3363,15 +3356,15 @@ def num.U16.checked_sub
     Source: 'core-models/src/core/num/mod.rs', lines 61:12-69:13 -/
 def num.U32.checked_sub
   (x : Std.U32) (y : Std.U32) : Result (option.Option Std.U32) := do
-  let i ← U32.Insts.Hax_libIntToInt.to_int num.U32.MIN
-  let i1 ← U32.Insts.Hax_libIntToInt.to_int x
-  let i2 ← U32.Insts.Hax_libIntToInt.to_int y
+  let i ← hax_lib.U32.Insts.Hax_libIntToInt.to_int num.U32.MIN
+  let i1 ← hax_lib.U32.Insts.Hax_libIntToInt.to_int x
+  let i2 ← hax_lib.U32.Insts.Hax_libIntToInt.to_int y
   let i3 ← hax_lib.int.Int.Insts.Core_modelsOpsArithSubIntInt.sub i1 i2
   let b ← hax_lib.int.Int.Insts.Core_modelsCmpPartialOrdInt.le i i3
   if b
   then
     let i4 ← hax_lib.int.Int.Insts.Core_modelsOpsArithSubIntInt.sub i1 i2
-    let i5 ← U32.Insts.Hax_libIntToInt.to_int num.U32.MAX
+    let i5 ← hax_lib.U32.Insts.Hax_libIntToInt.to_int num.U32.MAX
     let b1 ← hax_lib.int.Int.Insts.Core_modelsCmpPartialOrdInt.le i4 i5
     if b1
     then let i6 ← x - y
@@ -3383,15 +3376,15 @@ def num.U32.checked_sub
     Source: 'core-models/src/core/num/mod.rs', lines 61:12-69:13 -/
 def num.U64.checked_sub
   (x : Std.U64) (y : Std.U64) : Result (option.Option Std.U64) := do
-  let i ← U64.Insts.Hax_libIntToInt.to_int num.U64.MIN
-  let i1 ← U64.Insts.Hax_libIntToInt.to_int x
-  let i2 ← U64.Insts.Hax_libIntToInt.to_int y
+  let i ← hax_lib.U64.Insts.Hax_libIntToInt.to_int num.U64.MIN
+  let i1 ← hax_lib.U64.Insts.Hax_libIntToInt.to_int x
+  let i2 ← hax_lib.U64.Insts.Hax_libIntToInt.to_int y
   let i3 ← hax_lib.int.Int.Insts.Core_modelsOpsArithSubIntInt.sub i1 i2
   let b ← hax_lib.int.Int.Insts.Core_modelsCmpPartialOrdInt.le i i3
   if b
   then
     let i4 ← hax_lib.int.Int.Insts.Core_modelsOpsArithSubIntInt.sub i1 i2
-    let i5 ← U64.Insts.Hax_libIntToInt.to_int num.U64.MAX
+    let i5 ← hax_lib.U64.Insts.Hax_libIntToInt.to_int num.U64.MAX
     let b1 ← hax_lib.int.Int.Insts.Core_modelsCmpPartialOrdInt.le i4 i5
     if b1
     then let i6 ← x - y
@@ -3403,15 +3396,15 @@ def num.U64.checked_sub
     Source: 'core-models/src/core/num/mod.rs', lines 61:12-69:13 -/
 def num.U128.checked_sub
   (x : Std.U128) (y : Std.U128) : Result (option.Option Std.U128) := do
-  let i ← U128.Insts.Hax_libIntToInt.to_int num.U128.MIN
-  let i1 ← U128.Insts.Hax_libIntToInt.to_int x
-  let i2 ← U128.Insts.Hax_libIntToInt.to_int y
+  let i ← hax_lib.U128.Insts.Hax_libIntToInt.to_int num.U128.MIN
+  let i1 ← hax_lib.U128.Insts.Hax_libIntToInt.to_int x
+  let i2 ← hax_lib.U128.Insts.Hax_libIntToInt.to_int y
   let i3 ← hax_lib.int.Int.Insts.Core_modelsOpsArithSubIntInt.sub i1 i2
   let b ← hax_lib.int.Int.Insts.Core_modelsCmpPartialOrdInt.le i i3
   if b
   then
     let i4 ← hax_lib.int.Int.Insts.Core_modelsOpsArithSubIntInt.sub i1 i2
-    let i5 ← U128.Insts.Hax_libIntToInt.to_int num.U128.MAX
+    let i5 ← hax_lib.U128.Insts.Hax_libIntToInt.to_int num.U128.MAX
     let b1 ← hax_lib.int.Int.Insts.Core_modelsCmpPartialOrdInt.le i4 i5
     if b1
     then let i6 ← x - y
@@ -3423,16 +3416,16 @@ def num.U128.checked_sub
     Source: 'core-models/src/core/num/mod.rs', lines 61:12-69:13 -/
 def num.Usize.checked_sub
   (x : Std.Usize) (y : Std.Usize) : Result (option.Option Std.Usize) := do
-  let i ← Usize.Insts.Hax_libIntToInt.to_int num.Usize.MIN
-  let i1 ← Usize.Insts.Hax_libIntToInt.to_int x
-  let i2 ← Usize.Insts.Hax_libIntToInt.to_int y
+  let i ← hax_lib.Usize.Insts.Hax_libIntToInt.to_int num.Usize.MIN
+  let i1 ← hax_lib.Usize.Insts.Hax_libIntToInt.to_int x
+  let i2 ← hax_lib.Usize.Insts.Hax_libIntToInt.to_int y
   let i3 ← hax_lib.int.Int.Insts.Core_modelsOpsArithSubIntInt.sub i1 i2
   let b ← hax_lib.int.Int.Insts.Core_modelsCmpPartialOrdInt.le i i3
   if b
   then
     let i4 ← hax_lib.int.Int.Insts.Core_modelsOpsArithSubIntInt.sub i1 i2
     let i5 := num.Usize.MAX
-    let i6 ← Usize.Insts.Hax_libIntToInt.to_int i5
+    let i6 ← hax_lib.Usize.Insts.Hax_libIntToInt.to_int i5
     let b1 ← hax_lib.int.Int.Insts.Core_modelsCmpPartialOrdInt.le i4 i6
     if b1
     then let i7 ← x - y
@@ -3543,15 +3536,15 @@ def num.Usize.overflowing_mul
     Source: 'core-models/src/core/num/mod.rs', lines 83:12-91:13 -/
 def num.U8.checked_mul
   (x : Std.U8) (y : Std.U8) : Result (option.Option Std.U8) := do
-  let i ← U8.Insts.Hax_libIntToInt.to_int num.U8.MIN
-  let i1 ← U8.Insts.Hax_libIntToInt.to_int x
-  let i2 ← U8.Insts.Hax_libIntToInt.to_int y
+  let i ← hax_lib.U8.Insts.Hax_libIntToInt.to_int num.U8.MIN
+  let i1 ← hax_lib.U8.Insts.Hax_libIntToInt.to_int x
+  let i2 ← hax_lib.U8.Insts.Hax_libIntToInt.to_int y
   let i3 ← hax_lib.int.Int.Insts.Core_modelsOpsArithMulIntInt.mul i1 i2
   let b ← hax_lib.int.Int.Insts.Core_modelsCmpPartialOrdInt.le i i3
   if b
   then
     let i4 ← hax_lib.int.Int.Insts.Core_modelsOpsArithMulIntInt.mul i1 i2
-    let i5 ← U8.Insts.Hax_libIntToInt.to_int num.U8.MAX
+    let i5 ← hax_lib.U8.Insts.Hax_libIntToInt.to_int num.U8.MAX
     let b1 ← hax_lib.int.Int.Insts.Core_modelsCmpPartialOrdInt.le i4 i5
     if b1
     then let i6 ← x * y
@@ -3563,15 +3556,15 @@ def num.U8.checked_mul
     Source: 'core-models/src/core/num/mod.rs', lines 83:12-91:13 -/
 def num.U16.checked_mul
   (x : Std.U16) (y : Std.U16) : Result (option.Option Std.U16) := do
-  let i ← U16.Insts.Hax_libIntToInt.to_int num.U16.MIN
-  let i1 ← U16.Insts.Hax_libIntToInt.to_int x
-  let i2 ← U16.Insts.Hax_libIntToInt.to_int y
+  let i ← hax_lib.U16.Insts.Hax_libIntToInt.to_int num.U16.MIN
+  let i1 ← hax_lib.U16.Insts.Hax_libIntToInt.to_int x
+  let i2 ← hax_lib.U16.Insts.Hax_libIntToInt.to_int y
   let i3 ← hax_lib.int.Int.Insts.Core_modelsOpsArithMulIntInt.mul i1 i2
   let b ← hax_lib.int.Int.Insts.Core_modelsCmpPartialOrdInt.le i i3
   if b
   then
     let i4 ← hax_lib.int.Int.Insts.Core_modelsOpsArithMulIntInt.mul i1 i2
-    let i5 ← U16.Insts.Hax_libIntToInt.to_int num.U16.MAX
+    let i5 ← hax_lib.U16.Insts.Hax_libIntToInt.to_int num.U16.MAX
     let b1 ← hax_lib.int.Int.Insts.Core_modelsCmpPartialOrdInt.le i4 i5
     if b1
     then let i6 ← x * y
@@ -3583,15 +3576,15 @@ def num.U16.checked_mul
     Source: 'core-models/src/core/num/mod.rs', lines 83:12-91:13 -/
 def num.U32.checked_mul
   (x : Std.U32) (y : Std.U32) : Result (option.Option Std.U32) := do
-  let i ← U32.Insts.Hax_libIntToInt.to_int num.U32.MIN
-  let i1 ← U32.Insts.Hax_libIntToInt.to_int x
-  let i2 ← U32.Insts.Hax_libIntToInt.to_int y
+  let i ← hax_lib.U32.Insts.Hax_libIntToInt.to_int num.U32.MIN
+  let i1 ← hax_lib.U32.Insts.Hax_libIntToInt.to_int x
+  let i2 ← hax_lib.U32.Insts.Hax_libIntToInt.to_int y
   let i3 ← hax_lib.int.Int.Insts.Core_modelsOpsArithMulIntInt.mul i1 i2
   let b ← hax_lib.int.Int.Insts.Core_modelsCmpPartialOrdInt.le i i3
   if b
   then
     let i4 ← hax_lib.int.Int.Insts.Core_modelsOpsArithMulIntInt.mul i1 i2
-    let i5 ← U32.Insts.Hax_libIntToInt.to_int num.U32.MAX
+    let i5 ← hax_lib.U32.Insts.Hax_libIntToInt.to_int num.U32.MAX
     let b1 ← hax_lib.int.Int.Insts.Core_modelsCmpPartialOrdInt.le i4 i5
     if b1
     then let i6 ← x * y
@@ -3603,15 +3596,15 @@ def num.U32.checked_mul
     Source: 'core-models/src/core/num/mod.rs', lines 83:12-91:13 -/
 def num.U64.checked_mul
   (x : Std.U64) (y : Std.U64) : Result (option.Option Std.U64) := do
-  let i ← U64.Insts.Hax_libIntToInt.to_int num.U64.MIN
-  let i1 ← U64.Insts.Hax_libIntToInt.to_int x
-  let i2 ← U64.Insts.Hax_libIntToInt.to_int y
+  let i ← hax_lib.U64.Insts.Hax_libIntToInt.to_int num.U64.MIN
+  let i1 ← hax_lib.U64.Insts.Hax_libIntToInt.to_int x
+  let i2 ← hax_lib.U64.Insts.Hax_libIntToInt.to_int y
   let i3 ← hax_lib.int.Int.Insts.Core_modelsOpsArithMulIntInt.mul i1 i2
   let b ← hax_lib.int.Int.Insts.Core_modelsCmpPartialOrdInt.le i i3
   if b
   then
     let i4 ← hax_lib.int.Int.Insts.Core_modelsOpsArithMulIntInt.mul i1 i2
-    let i5 ← U64.Insts.Hax_libIntToInt.to_int num.U64.MAX
+    let i5 ← hax_lib.U64.Insts.Hax_libIntToInt.to_int num.U64.MAX
     let b1 ← hax_lib.int.Int.Insts.Core_modelsCmpPartialOrdInt.le i4 i5
     if b1
     then let i6 ← x * y
@@ -3623,15 +3616,15 @@ def num.U64.checked_mul
     Source: 'core-models/src/core/num/mod.rs', lines 83:12-91:13 -/
 def num.U128.checked_mul
   (x : Std.U128) (y : Std.U128) : Result (option.Option Std.U128) := do
-  let i ← U128.Insts.Hax_libIntToInt.to_int num.U128.MIN
-  let i1 ← U128.Insts.Hax_libIntToInt.to_int x
-  let i2 ← U128.Insts.Hax_libIntToInt.to_int y
+  let i ← hax_lib.U128.Insts.Hax_libIntToInt.to_int num.U128.MIN
+  let i1 ← hax_lib.U128.Insts.Hax_libIntToInt.to_int x
+  let i2 ← hax_lib.U128.Insts.Hax_libIntToInt.to_int y
   let i3 ← hax_lib.int.Int.Insts.Core_modelsOpsArithMulIntInt.mul i1 i2
   let b ← hax_lib.int.Int.Insts.Core_modelsCmpPartialOrdInt.le i i3
   if b
   then
     let i4 ← hax_lib.int.Int.Insts.Core_modelsOpsArithMulIntInt.mul i1 i2
-    let i5 ← U128.Insts.Hax_libIntToInt.to_int num.U128.MAX
+    let i5 ← hax_lib.U128.Insts.Hax_libIntToInt.to_int num.U128.MAX
     let b1 ← hax_lib.int.Int.Insts.Core_modelsCmpPartialOrdInt.le i4 i5
     if b1
     then let i6 ← x * y
@@ -3643,16 +3636,16 @@ def num.U128.checked_mul
     Source: 'core-models/src/core/num/mod.rs', lines 83:12-91:13 -/
 def num.Usize.checked_mul
   (x : Std.Usize) (y : Std.Usize) : Result (option.Option Std.Usize) := do
-  let i ← Usize.Insts.Hax_libIntToInt.to_int num.Usize.MIN
-  let i1 ← Usize.Insts.Hax_libIntToInt.to_int x
-  let i2 ← Usize.Insts.Hax_libIntToInt.to_int y
+  let i ← hax_lib.Usize.Insts.Hax_libIntToInt.to_int num.Usize.MIN
+  let i1 ← hax_lib.Usize.Insts.Hax_libIntToInt.to_int x
+  let i2 ← hax_lib.Usize.Insts.Hax_libIntToInt.to_int y
   let i3 ← hax_lib.int.Int.Insts.Core_modelsOpsArithMulIntInt.mul i1 i2
   let b ← hax_lib.int.Int.Insts.Core_modelsCmpPartialOrdInt.le i i3
   if b
   then
     let i4 ← hax_lib.int.Int.Insts.Core_modelsOpsArithMulIntInt.mul i1 i2
     let i5 := num.Usize.MAX
-    let i6 ← Usize.Insts.Hax_libIntToInt.to_int i5
+    let i6 ← hax_lib.Usize.Insts.Hax_libIntToInt.to_int i5
     let b1 ← hax_lib.int.Int.Insts.Core_modelsCmpPartialOrdInt.le i4 i6
     if b1
     then let i7 ← x * y
@@ -4435,15 +4428,15 @@ def num.Isize.overflowing_add
     Source: 'core-models/src/core/num/mod.rs', lines 224:12-232:13 -/
 def num.I8.checked_add
   (x : Std.I8) (y : Std.I8) : Result (option.Option Std.I8) := do
-  let i ← I8.Insts.Hax_libIntToInt.to_int num.I8.MIN
-  let i1 ← I8.Insts.Hax_libIntToInt.to_int x
-  let i2 ← I8.Insts.Hax_libIntToInt.to_int y
+  let i ← hax_lib.I8.Insts.Hax_libIntToInt.to_int num.I8.MIN
+  let i1 ← hax_lib.I8.Insts.Hax_libIntToInt.to_int x
+  let i2 ← hax_lib.I8.Insts.Hax_libIntToInt.to_int y
   let i3 ← hax_lib.int.Int.Insts.Core_modelsOpsArithAddIntInt.add i1 i2
   let b ← hax_lib.int.Int.Insts.Core_modelsCmpPartialOrdInt.le i i3
   if b
   then
     let i4 ← hax_lib.int.Int.Insts.Core_modelsOpsArithAddIntInt.add i1 i2
-    let i5 ← I8.Insts.Hax_libIntToInt.to_int num.I8.MAX
+    let i5 ← hax_lib.I8.Insts.Hax_libIntToInt.to_int num.I8.MAX
     let b1 ← hax_lib.int.Int.Insts.Core_modelsCmpPartialOrdInt.le i4 i5
     if b1
     then let i6 ← x + y
@@ -4455,15 +4448,15 @@ def num.I8.checked_add
     Source: 'core-models/src/core/num/mod.rs', lines 224:12-232:13 -/
 def num.I16.checked_add
   (x : Std.I16) (y : Std.I16) : Result (option.Option Std.I16) := do
-  let i ← I16.Insts.Hax_libIntToInt.to_int num.I16.MIN
-  let i1 ← I16.Insts.Hax_libIntToInt.to_int x
-  let i2 ← I16.Insts.Hax_libIntToInt.to_int y
+  let i ← hax_lib.I16.Insts.Hax_libIntToInt.to_int num.I16.MIN
+  let i1 ← hax_lib.I16.Insts.Hax_libIntToInt.to_int x
+  let i2 ← hax_lib.I16.Insts.Hax_libIntToInt.to_int y
   let i3 ← hax_lib.int.Int.Insts.Core_modelsOpsArithAddIntInt.add i1 i2
   let b ← hax_lib.int.Int.Insts.Core_modelsCmpPartialOrdInt.le i i3
   if b
   then
     let i4 ← hax_lib.int.Int.Insts.Core_modelsOpsArithAddIntInt.add i1 i2
-    let i5 ← I16.Insts.Hax_libIntToInt.to_int num.I16.MAX
+    let i5 ← hax_lib.I16.Insts.Hax_libIntToInt.to_int num.I16.MAX
     let b1 ← hax_lib.int.Int.Insts.Core_modelsCmpPartialOrdInt.le i4 i5
     if b1
     then let i6 ← x + y
@@ -4475,15 +4468,15 @@ def num.I16.checked_add
     Source: 'core-models/src/core/num/mod.rs', lines 224:12-232:13 -/
 def num.I32.checked_add
   (x : Std.I32) (y : Std.I32) : Result (option.Option Std.I32) := do
-  let i ← I32.Insts.Hax_libIntToInt.to_int num.I32.MIN
-  let i1 ← I32.Insts.Hax_libIntToInt.to_int x
-  let i2 ← I32.Insts.Hax_libIntToInt.to_int y
+  let i ← hax_lib.I32.Insts.Hax_libIntToInt.to_int num.I32.MIN
+  let i1 ← hax_lib.I32.Insts.Hax_libIntToInt.to_int x
+  let i2 ← hax_lib.I32.Insts.Hax_libIntToInt.to_int y
   let i3 ← hax_lib.int.Int.Insts.Core_modelsOpsArithAddIntInt.add i1 i2
   let b ← hax_lib.int.Int.Insts.Core_modelsCmpPartialOrdInt.le i i3
   if b
   then
     let i4 ← hax_lib.int.Int.Insts.Core_modelsOpsArithAddIntInt.add i1 i2
-    let i5 ← I32.Insts.Hax_libIntToInt.to_int num.I32.MAX
+    let i5 ← hax_lib.I32.Insts.Hax_libIntToInt.to_int num.I32.MAX
     let b1 ← hax_lib.int.Int.Insts.Core_modelsCmpPartialOrdInt.le i4 i5
     if b1
     then let i6 ← x + y
@@ -4495,15 +4488,15 @@ def num.I32.checked_add
     Source: 'core-models/src/core/num/mod.rs', lines 224:12-232:13 -/
 def num.I64.checked_add
   (x : Std.I64) (y : Std.I64) : Result (option.Option Std.I64) := do
-  let i ← I64.Insts.Hax_libIntToInt.to_int num.I64.MIN
-  let i1 ← I64.Insts.Hax_libIntToInt.to_int x
-  let i2 ← I64.Insts.Hax_libIntToInt.to_int y
+  let i ← hax_lib.I64.Insts.Hax_libIntToInt.to_int num.I64.MIN
+  let i1 ← hax_lib.I64.Insts.Hax_libIntToInt.to_int x
+  let i2 ← hax_lib.I64.Insts.Hax_libIntToInt.to_int y
   let i3 ← hax_lib.int.Int.Insts.Core_modelsOpsArithAddIntInt.add i1 i2
   let b ← hax_lib.int.Int.Insts.Core_modelsCmpPartialOrdInt.le i i3
   if b
   then
     let i4 ← hax_lib.int.Int.Insts.Core_modelsOpsArithAddIntInt.add i1 i2
-    let i5 ← I64.Insts.Hax_libIntToInt.to_int num.I64.MAX
+    let i5 ← hax_lib.I64.Insts.Hax_libIntToInt.to_int num.I64.MAX
     let b1 ← hax_lib.int.Int.Insts.Core_modelsCmpPartialOrdInt.le i4 i5
     if b1
     then let i6 ← x + y
@@ -4515,15 +4508,15 @@ def num.I64.checked_add
     Source: 'core-models/src/core/num/mod.rs', lines 224:12-232:13 -/
 def num.I128.checked_add
   (x : Std.I128) (y : Std.I128) : Result (option.Option Std.I128) := do
-  let i ← I128.Insts.Hax_libIntToInt.to_int num.I128.MIN
-  let i1 ← I128.Insts.Hax_libIntToInt.to_int x
-  let i2 ← I128.Insts.Hax_libIntToInt.to_int y
+  let i ← hax_lib.I128.Insts.Hax_libIntToInt.to_int num.I128.MIN
+  let i1 ← hax_lib.I128.Insts.Hax_libIntToInt.to_int x
+  let i2 ← hax_lib.I128.Insts.Hax_libIntToInt.to_int y
   let i3 ← hax_lib.int.Int.Insts.Core_modelsOpsArithAddIntInt.add i1 i2
   let b ← hax_lib.int.Int.Insts.Core_modelsCmpPartialOrdInt.le i i3
   if b
   then
     let i4 ← hax_lib.int.Int.Insts.Core_modelsOpsArithAddIntInt.add i1 i2
-    let i5 ← I128.Insts.Hax_libIntToInt.to_int num.I128.MAX
+    let i5 ← hax_lib.I128.Insts.Hax_libIntToInt.to_int num.I128.MAX
     let b1 ← hax_lib.int.Int.Insts.Core_modelsCmpPartialOrdInt.le i4 i5
     if b1
     then let i6 ← x + y
@@ -4536,16 +4529,16 @@ def num.I128.checked_add
 def num.Isize.checked_add
   (x : Std.Isize) (y : Std.Isize) : Result (option.Option Std.Isize) := do
   let i := num.Isize.MIN
-  let i1 ← Isize.Insts.Hax_libIntToInt.to_int i
-  let i2 ← Isize.Insts.Hax_libIntToInt.to_int x
-  let i3 ← Isize.Insts.Hax_libIntToInt.to_int y
+  let i1 ← hax_lib.Isize.Insts.Hax_libIntToInt.to_int i
+  let i2 ← hax_lib.Isize.Insts.Hax_libIntToInt.to_int x
+  let i3 ← hax_lib.Isize.Insts.Hax_libIntToInt.to_int y
   let i4 ← hax_lib.int.Int.Insts.Core_modelsOpsArithAddIntInt.add i2 i3
   let b ← hax_lib.int.Int.Insts.Core_modelsCmpPartialOrdInt.le i1 i4
   if b
   then
     let i5 ← hax_lib.int.Int.Insts.Core_modelsOpsArithAddIntInt.add i2 i3
     let i6 := num.Isize.MAX
-    let i7 ← Isize.Insts.Hax_libIntToInt.to_int i6
+    let i7 ← hax_lib.Isize.Insts.Hax_libIntToInt.to_int i6
     let b1 ← hax_lib.int.Int.Insts.Core_modelsCmpPartialOrdInt.le i5 i7
     if b1
     then let i8 ← x + y
@@ -4656,15 +4649,15 @@ def num.Isize.overflowing_sub
     Source: 'core-models/src/core/num/mod.rs', lines 246:12-254:13 -/
 def num.I8.checked_sub
   (x : Std.I8) (y : Std.I8) : Result (option.Option Std.I8) := do
-  let i ← I8.Insts.Hax_libIntToInt.to_int num.I8.MIN
-  let i1 ← I8.Insts.Hax_libIntToInt.to_int x
-  let i2 ← I8.Insts.Hax_libIntToInt.to_int y
+  let i ← hax_lib.I8.Insts.Hax_libIntToInt.to_int num.I8.MIN
+  let i1 ← hax_lib.I8.Insts.Hax_libIntToInt.to_int x
+  let i2 ← hax_lib.I8.Insts.Hax_libIntToInt.to_int y
   let i3 ← hax_lib.int.Int.Insts.Core_modelsOpsArithSubIntInt.sub i1 i2
   let b ← hax_lib.int.Int.Insts.Core_modelsCmpPartialOrdInt.le i i3
   if b
   then
     let i4 ← hax_lib.int.Int.Insts.Core_modelsOpsArithSubIntInt.sub i1 i2
-    let i5 ← I8.Insts.Hax_libIntToInt.to_int num.I8.MAX
+    let i5 ← hax_lib.I8.Insts.Hax_libIntToInt.to_int num.I8.MAX
     let b1 ← hax_lib.int.Int.Insts.Core_modelsCmpPartialOrdInt.le i4 i5
     if b1
     then let i6 ← x - y
@@ -4676,15 +4669,15 @@ def num.I8.checked_sub
     Source: 'core-models/src/core/num/mod.rs', lines 246:12-254:13 -/
 def num.I16.checked_sub
   (x : Std.I16) (y : Std.I16) : Result (option.Option Std.I16) := do
-  let i ← I16.Insts.Hax_libIntToInt.to_int num.I16.MIN
-  let i1 ← I16.Insts.Hax_libIntToInt.to_int x
-  let i2 ← I16.Insts.Hax_libIntToInt.to_int y
+  let i ← hax_lib.I16.Insts.Hax_libIntToInt.to_int num.I16.MIN
+  let i1 ← hax_lib.I16.Insts.Hax_libIntToInt.to_int x
+  let i2 ← hax_lib.I16.Insts.Hax_libIntToInt.to_int y
   let i3 ← hax_lib.int.Int.Insts.Core_modelsOpsArithSubIntInt.sub i1 i2
   let b ← hax_lib.int.Int.Insts.Core_modelsCmpPartialOrdInt.le i i3
   if b
   then
     let i4 ← hax_lib.int.Int.Insts.Core_modelsOpsArithSubIntInt.sub i1 i2
-    let i5 ← I16.Insts.Hax_libIntToInt.to_int num.I16.MAX
+    let i5 ← hax_lib.I16.Insts.Hax_libIntToInt.to_int num.I16.MAX
     let b1 ← hax_lib.int.Int.Insts.Core_modelsCmpPartialOrdInt.le i4 i5
     if b1
     then let i6 ← x - y
@@ -4696,15 +4689,15 @@ def num.I16.checked_sub
     Source: 'core-models/src/core/num/mod.rs', lines 246:12-254:13 -/
 def num.I32.checked_sub
   (x : Std.I32) (y : Std.I32) : Result (option.Option Std.I32) := do
-  let i ← I32.Insts.Hax_libIntToInt.to_int num.I32.MIN
-  let i1 ← I32.Insts.Hax_libIntToInt.to_int x
-  let i2 ← I32.Insts.Hax_libIntToInt.to_int y
+  let i ← hax_lib.I32.Insts.Hax_libIntToInt.to_int num.I32.MIN
+  let i1 ← hax_lib.I32.Insts.Hax_libIntToInt.to_int x
+  let i2 ← hax_lib.I32.Insts.Hax_libIntToInt.to_int y
   let i3 ← hax_lib.int.Int.Insts.Core_modelsOpsArithSubIntInt.sub i1 i2
   let b ← hax_lib.int.Int.Insts.Core_modelsCmpPartialOrdInt.le i i3
   if b
   then
     let i4 ← hax_lib.int.Int.Insts.Core_modelsOpsArithSubIntInt.sub i1 i2
-    let i5 ← I32.Insts.Hax_libIntToInt.to_int num.I32.MAX
+    let i5 ← hax_lib.I32.Insts.Hax_libIntToInt.to_int num.I32.MAX
     let b1 ← hax_lib.int.Int.Insts.Core_modelsCmpPartialOrdInt.le i4 i5
     if b1
     then let i6 ← x - y
@@ -4716,15 +4709,15 @@ def num.I32.checked_sub
     Source: 'core-models/src/core/num/mod.rs', lines 246:12-254:13 -/
 def num.I64.checked_sub
   (x : Std.I64) (y : Std.I64) : Result (option.Option Std.I64) := do
-  let i ← I64.Insts.Hax_libIntToInt.to_int num.I64.MIN
-  let i1 ← I64.Insts.Hax_libIntToInt.to_int x
-  let i2 ← I64.Insts.Hax_libIntToInt.to_int y
+  let i ← hax_lib.I64.Insts.Hax_libIntToInt.to_int num.I64.MIN
+  let i1 ← hax_lib.I64.Insts.Hax_libIntToInt.to_int x
+  let i2 ← hax_lib.I64.Insts.Hax_libIntToInt.to_int y
   let i3 ← hax_lib.int.Int.Insts.Core_modelsOpsArithSubIntInt.sub i1 i2
   let b ← hax_lib.int.Int.Insts.Core_modelsCmpPartialOrdInt.le i i3
   if b
   then
     let i4 ← hax_lib.int.Int.Insts.Core_modelsOpsArithSubIntInt.sub i1 i2
-    let i5 ← I64.Insts.Hax_libIntToInt.to_int num.I64.MAX
+    let i5 ← hax_lib.I64.Insts.Hax_libIntToInt.to_int num.I64.MAX
     let b1 ← hax_lib.int.Int.Insts.Core_modelsCmpPartialOrdInt.le i4 i5
     if b1
     then let i6 ← x - y
@@ -4736,15 +4729,15 @@ def num.I64.checked_sub
     Source: 'core-models/src/core/num/mod.rs', lines 246:12-254:13 -/
 def num.I128.checked_sub
   (x : Std.I128) (y : Std.I128) : Result (option.Option Std.I128) := do
-  let i ← I128.Insts.Hax_libIntToInt.to_int num.I128.MIN
-  let i1 ← I128.Insts.Hax_libIntToInt.to_int x
-  let i2 ← I128.Insts.Hax_libIntToInt.to_int y
+  let i ← hax_lib.I128.Insts.Hax_libIntToInt.to_int num.I128.MIN
+  let i1 ← hax_lib.I128.Insts.Hax_libIntToInt.to_int x
+  let i2 ← hax_lib.I128.Insts.Hax_libIntToInt.to_int y
   let i3 ← hax_lib.int.Int.Insts.Core_modelsOpsArithSubIntInt.sub i1 i2
   let b ← hax_lib.int.Int.Insts.Core_modelsCmpPartialOrdInt.le i i3
   if b
   then
     let i4 ← hax_lib.int.Int.Insts.Core_modelsOpsArithSubIntInt.sub i1 i2
-    let i5 ← I128.Insts.Hax_libIntToInt.to_int num.I128.MAX
+    let i5 ← hax_lib.I128.Insts.Hax_libIntToInt.to_int num.I128.MAX
     let b1 ← hax_lib.int.Int.Insts.Core_modelsCmpPartialOrdInt.le i4 i5
     if b1
     then let i6 ← x - y
@@ -4757,16 +4750,16 @@ def num.I128.checked_sub
 def num.Isize.checked_sub
   (x : Std.Isize) (y : Std.Isize) : Result (option.Option Std.Isize) := do
   let i := num.Isize.MIN
-  let i1 ← Isize.Insts.Hax_libIntToInt.to_int i
-  let i2 ← Isize.Insts.Hax_libIntToInt.to_int x
-  let i3 ← Isize.Insts.Hax_libIntToInt.to_int y
+  let i1 ← hax_lib.Isize.Insts.Hax_libIntToInt.to_int i
+  let i2 ← hax_lib.Isize.Insts.Hax_libIntToInt.to_int x
+  let i3 ← hax_lib.Isize.Insts.Hax_libIntToInt.to_int y
   let i4 ← hax_lib.int.Int.Insts.Core_modelsOpsArithSubIntInt.sub i2 i3
   let b ← hax_lib.int.Int.Insts.Core_modelsCmpPartialOrdInt.le i1 i4
   if b
   then
     let i5 ← hax_lib.int.Int.Insts.Core_modelsOpsArithSubIntInt.sub i2 i3
     let i6 := num.Isize.MAX
-    let i7 ← Isize.Insts.Hax_libIntToInt.to_int i6
+    let i7 ← hax_lib.Isize.Insts.Hax_libIntToInt.to_int i6
     let b1 ← hax_lib.int.Int.Insts.Core_modelsCmpPartialOrdInt.le i5 i7
     if b1
     then let i8 ← x - y
@@ -4877,15 +4870,15 @@ def num.Isize.overflowing_mul
     Source: 'core-models/src/core/num/mod.rs', lines 268:12-276:13 -/
 def num.I8.checked_mul
   (x : Std.I8) (y : Std.I8) : Result (option.Option Std.I8) := do
-  let i ← I8.Insts.Hax_libIntToInt.to_int num.I8.MIN
-  let i1 ← I8.Insts.Hax_libIntToInt.to_int x
-  let i2 ← I8.Insts.Hax_libIntToInt.to_int y
+  let i ← hax_lib.I8.Insts.Hax_libIntToInt.to_int num.I8.MIN
+  let i1 ← hax_lib.I8.Insts.Hax_libIntToInt.to_int x
+  let i2 ← hax_lib.I8.Insts.Hax_libIntToInt.to_int y
   let i3 ← hax_lib.int.Int.Insts.Core_modelsOpsArithMulIntInt.mul i1 i2
   let b ← hax_lib.int.Int.Insts.Core_modelsCmpPartialOrdInt.le i i3
   if b
   then
     let i4 ← hax_lib.int.Int.Insts.Core_modelsOpsArithMulIntInt.mul i1 i2
-    let i5 ← I8.Insts.Hax_libIntToInt.to_int num.I8.MAX
+    let i5 ← hax_lib.I8.Insts.Hax_libIntToInt.to_int num.I8.MAX
     let b1 ← hax_lib.int.Int.Insts.Core_modelsCmpPartialOrdInt.le i4 i5
     if b1
     then let i6 ← x * y
@@ -4897,15 +4890,15 @@ def num.I8.checked_mul
     Source: 'core-models/src/core/num/mod.rs', lines 268:12-276:13 -/
 def num.I16.checked_mul
   (x : Std.I16) (y : Std.I16) : Result (option.Option Std.I16) := do
-  let i ← I16.Insts.Hax_libIntToInt.to_int num.I16.MIN
-  let i1 ← I16.Insts.Hax_libIntToInt.to_int x
-  let i2 ← I16.Insts.Hax_libIntToInt.to_int y
+  let i ← hax_lib.I16.Insts.Hax_libIntToInt.to_int num.I16.MIN
+  let i1 ← hax_lib.I16.Insts.Hax_libIntToInt.to_int x
+  let i2 ← hax_lib.I16.Insts.Hax_libIntToInt.to_int y
   let i3 ← hax_lib.int.Int.Insts.Core_modelsOpsArithMulIntInt.mul i1 i2
   let b ← hax_lib.int.Int.Insts.Core_modelsCmpPartialOrdInt.le i i3
   if b
   then
     let i4 ← hax_lib.int.Int.Insts.Core_modelsOpsArithMulIntInt.mul i1 i2
-    let i5 ← I16.Insts.Hax_libIntToInt.to_int num.I16.MAX
+    let i5 ← hax_lib.I16.Insts.Hax_libIntToInt.to_int num.I16.MAX
     let b1 ← hax_lib.int.Int.Insts.Core_modelsCmpPartialOrdInt.le i4 i5
     if b1
     then let i6 ← x * y
@@ -4917,15 +4910,15 @@ def num.I16.checked_mul
     Source: 'core-models/src/core/num/mod.rs', lines 268:12-276:13 -/
 def num.I32.checked_mul
   (x : Std.I32) (y : Std.I32) : Result (option.Option Std.I32) := do
-  let i ← I32.Insts.Hax_libIntToInt.to_int num.I32.MIN
-  let i1 ← I32.Insts.Hax_libIntToInt.to_int x
-  let i2 ← I32.Insts.Hax_libIntToInt.to_int y
+  let i ← hax_lib.I32.Insts.Hax_libIntToInt.to_int num.I32.MIN
+  let i1 ← hax_lib.I32.Insts.Hax_libIntToInt.to_int x
+  let i2 ← hax_lib.I32.Insts.Hax_libIntToInt.to_int y
   let i3 ← hax_lib.int.Int.Insts.Core_modelsOpsArithMulIntInt.mul i1 i2
   let b ← hax_lib.int.Int.Insts.Core_modelsCmpPartialOrdInt.le i i3
   if b
   then
     let i4 ← hax_lib.int.Int.Insts.Core_modelsOpsArithMulIntInt.mul i1 i2
-    let i5 ← I32.Insts.Hax_libIntToInt.to_int num.I32.MAX
+    let i5 ← hax_lib.I32.Insts.Hax_libIntToInt.to_int num.I32.MAX
     let b1 ← hax_lib.int.Int.Insts.Core_modelsCmpPartialOrdInt.le i4 i5
     if b1
     then let i6 ← x * y
@@ -4937,15 +4930,15 @@ def num.I32.checked_mul
     Source: 'core-models/src/core/num/mod.rs', lines 268:12-276:13 -/
 def num.I64.checked_mul
   (x : Std.I64) (y : Std.I64) : Result (option.Option Std.I64) := do
-  let i ← I64.Insts.Hax_libIntToInt.to_int num.I64.MIN
-  let i1 ← I64.Insts.Hax_libIntToInt.to_int x
-  let i2 ← I64.Insts.Hax_libIntToInt.to_int y
+  let i ← hax_lib.I64.Insts.Hax_libIntToInt.to_int num.I64.MIN
+  let i1 ← hax_lib.I64.Insts.Hax_libIntToInt.to_int x
+  let i2 ← hax_lib.I64.Insts.Hax_libIntToInt.to_int y
   let i3 ← hax_lib.int.Int.Insts.Core_modelsOpsArithMulIntInt.mul i1 i2
   let b ← hax_lib.int.Int.Insts.Core_modelsCmpPartialOrdInt.le i i3
   if b
   then
     let i4 ← hax_lib.int.Int.Insts.Core_modelsOpsArithMulIntInt.mul i1 i2
-    let i5 ← I64.Insts.Hax_libIntToInt.to_int num.I64.MAX
+    let i5 ← hax_lib.I64.Insts.Hax_libIntToInt.to_int num.I64.MAX
     let b1 ← hax_lib.int.Int.Insts.Core_modelsCmpPartialOrdInt.le i4 i5
     if b1
     then let i6 ← x * y
@@ -4957,15 +4950,15 @@ def num.I64.checked_mul
     Source: 'core-models/src/core/num/mod.rs', lines 268:12-276:13 -/
 def num.I128.checked_mul
   (x : Std.I128) (y : Std.I128) : Result (option.Option Std.I128) := do
-  let i ← I128.Insts.Hax_libIntToInt.to_int num.I128.MIN
-  let i1 ← I128.Insts.Hax_libIntToInt.to_int x
-  let i2 ← I128.Insts.Hax_libIntToInt.to_int y
+  let i ← hax_lib.I128.Insts.Hax_libIntToInt.to_int num.I128.MIN
+  let i1 ← hax_lib.I128.Insts.Hax_libIntToInt.to_int x
+  let i2 ← hax_lib.I128.Insts.Hax_libIntToInt.to_int y
   let i3 ← hax_lib.int.Int.Insts.Core_modelsOpsArithMulIntInt.mul i1 i2
   let b ← hax_lib.int.Int.Insts.Core_modelsCmpPartialOrdInt.le i i3
   if b
   then
     let i4 ← hax_lib.int.Int.Insts.Core_modelsOpsArithMulIntInt.mul i1 i2
-    let i5 ← I128.Insts.Hax_libIntToInt.to_int num.I128.MAX
+    let i5 ← hax_lib.I128.Insts.Hax_libIntToInt.to_int num.I128.MAX
     let b1 ← hax_lib.int.Int.Insts.Core_modelsCmpPartialOrdInt.le i4 i5
     if b1
     then let i6 ← x * y
@@ -4978,16 +4971,16 @@ def num.I128.checked_mul
 def num.Isize.checked_mul
   (x : Std.Isize) (y : Std.Isize) : Result (option.Option Std.Isize) := do
   let i := num.Isize.MIN
-  let i1 ← Isize.Insts.Hax_libIntToInt.to_int i
-  let i2 ← Isize.Insts.Hax_libIntToInt.to_int x
-  let i3 ← Isize.Insts.Hax_libIntToInt.to_int y
+  let i1 ← hax_lib.Isize.Insts.Hax_libIntToInt.to_int i
+  let i2 ← hax_lib.Isize.Insts.Hax_libIntToInt.to_int x
+  let i3 ← hax_lib.Isize.Insts.Hax_libIntToInt.to_int y
   let i4 ← hax_lib.int.Int.Insts.Core_modelsOpsArithMulIntInt.mul i2 i3
   let b ← hax_lib.int.Int.Insts.Core_modelsCmpPartialOrdInt.le i1 i4
   if b
   then
     let i5 ← hax_lib.int.Int.Insts.Core_modelsOpsArithMulIntInt.mul i2 i3
     let i6 := num.Isize.MAX
-    let i7 ← Isize.Insts.Hax_libIntToInt.to_int i6
+    let i7 ← hax_lib.Isize.Insts.Hax_libIntToInt.to_int i6
     let b1 ← hax_lib.int.Int.Insts.Core_modelsCmpPartialOrdInt.le i5 i7
     if b1
     then let i8 ← x * y
diff --git a/lean/CoreModels/FunsExternal.lean b/lean/CoreModels/FunsExternal.lean
index 20ed0b1..d9b42c4 100644
--- a/lean/CoreModels/FunsExternal.lean
+++ b/lean/CoreModels/FunsExternal.lean
@@ -95,7 +95,7 @@ def hax_lib.int.Int.Insts.Core_modelsOpsArithMulIntInt.mul
     Name pattern: [hax_lib::int::{hax_lib::int::ToInt<u8>}::to_int]
     Visibility: public -/
 @[rust_fun "hax_lib::int::{hax_lib::int::ToInt<u8>}::to_int"]
-def U8.Insts.Hax_libIntToInt.to_int : Std.U8 → Result hax_lib.int.Int :=
+def hax_lib.U8.Insts.Hax_libIntToInt.to_int : Std.U8 → Result hax_lib.int.Int :=
   fun x => ok (x.val : Int)
 
 /-- [hax_lib::int::{hax_lib::int::ToInt for u16}::to_int]:
@@ -103,7 +103,7 @@ def U8.Insts.Hax_libIntToInt.to_int : Std.U8 → Result hax_lib.int.Int :=
     Name pattern: [hax_lib::int::{hax_lib::int::ToInt<u16>}::to_int]
     Visibility: public -/
 @[rust_fun "hax_lib::int::{hax_lib::int::ToInt<u16>}::to_int"]
-def U16.Insts.Hax_libIntToInt.to_int : Std.U16 → Result hax_lib.int.Int :=
+def hax_lib.U16.Insts.Hax_libIntToInt.to_int : Std.U16 → Result hax_lib.int.Int :=
   fun x => ok (x.val : Int)
 
 /-- [hax_lib::int::{hax_lib::int::ToInt for u32}::to_int]:
@@ -111,7 +111,7 @@ def U16.Insts.Hax_libIntToInt.to_int : Std.U16 → Result hax_lib.int.Int :=
     Name pattern: [hax_lib::int::{hax_lib::int::ToInt<u32>}::to_int]
     Visibility: public -/
 @[rust_fun "hax_lib::int::{hax_lib::int::ToInt<u32>}::to_int"]
-def U32.Insts.Hax_libIntToInt.to_int : Std.U32 → Result hax_lib.int.Int :=
+def hax_lib.U32.Insts.Hax_libIntToInt.to_int : Std.U32 → Result hax_lib.int.Int :=
   fun x => ok (x.val : Int)
 
 /-- [hax_lib::int::{hax_lib::int::ToInt for u64}::to_int]:
@@ -119,7 +119,7 @@ def U32.Insts.Hax_libIntToInt.to_int : Std.U32 → Result hax_lib.int.Int :=
     Name pattern: [hax_lib::int::{hax_lib::int::ToInt<u64>}::to_int]
     Visibility: public -/
 @[rust_fun "hax_lib::int::{hax_lib::int::ToInt<u64>}::to_int"]
-def U64.Insts.Hax_libIntToInt.to_int : Std.U64 → Result hax_lib.int.Int :=
+def hax_lib.U64.Insts.Hax_libIntToInt.to_int : Std.U64 → Result hax_lib.int.Int :=
   fun x => ok (x.val : Int)
 
 /-- [hax_lib::int::{hax_lib::int::ToInt for u128}::to_int]:
@@ -127,7 +127,7 @@ def U64.Insts.Hax_libIntToInt.to_int : Std.U64 → Result hax_lib.int.Int :=
     Name pattern: [hax_lib::int::{hax_lib::int::ToInt<u128>}::to_int]
     Visibility: public -/
 @[rust_fun "hax_lib::int::{hax_lib::int::ToInt<u128>}::to_int"]
-def U128.Insts.Hax_libIntToInt.to_int : Std.U128 → Result hax_lib.int.Int :=
+def hax_lib.U128.Insts.Hax_libIntToInt.to_int : Std.U128 → Result hax_lib.int.Int :=
   fun x => ok (x.val : Int)
 
 /-- [hax_lib::int::{hax_lib::int::ToInt for usize}::to_int]:
@@ -135,7 +135,7 @@ def U128.Insts.Hax_libIntToInt.to_int : Std.U128 → Result hax_lib.int.Int :=
     Name pattern: [hax_lib::int::{hax_lib::int::ToInt<usize>}::to_int]
     Visibility: public -/
 @[rust_fun "hax_lib::int::{hax_lib::int::ToInt<usize>}::to_int"]
-def Usize.Insts.Hax_libIntToInt.to_int : Std.Usize → Result hax_lib.int.Int :=
+def hax_lib.Usize.Insts.Hax_libIntToInt.to_int : Std.Usize → Result hax_lib.int.Int :=
   fun x => ok (x.val : Int)
 
 /-- [hax_lib::int::{hax_lib::int::ToInt for i8}::to_int]:
@@ -143,7 +143,7 @@ def Usize.Insts.Hax_libIntToInt.to_int : Std.Usize → Result hax_lib.int.Int :=
     Name pattern: [hax_lib::int::{hax_lib::int::ToInt<i8>}::to_int]
     Visibility: public -/
 @[rust_fun "hax_lib::int::{hax_lib::int::ToInt<i8>}::to_int"]
-def I8.Insts.Hax_libIntToInt.to_int : Std.I8 → Result hax_lib.int.Int :=
+def hax_lib.I8.Insts.Hax_libIntToInt.to_int : Std.I8 → Result hax_lib.int.Int :=
   fun x => ok x.val
 
 /-- [hax_lib::int::{hax_lib::int::ToInt for i16}::to_int]:
@@ -151,7 +151,7 @@ def I8.Insts.Hax_libIntToInt.to_int : Std.I8 → Result hax_lib.int.Int :=
     Name pattern: [hax_lib::int::{hax_lib::int::ToInt<i16>}::to_int]
     Visibility: public -/
 @[rust_fun "hax_lib::int::{hax_lib::int::ToInt<i16>}::to_int"]
-def I16.Insts.Hax_libIntToInt.to_int : Std.I16 → Result hax_lib.int.Int :=
+def hax_lib.I16.Insts.Hax_libIntToInt.to_int : Std.I16 → Result hax_lib.int.Int :=
   fun x => ok x.val
 
 /-- [hax_lib::int::{hax_lib::int::ToInt for i32}::to_int]:
@@ -159,7 +159,7 @@ def I16.Insts.Hax_libIntToInt.to_int : Std.I16 → Result hax_lib.int.Int :=
     Name pattern: [hax_lib::int::{hax_lib::int::ToInt<i32>}::to_int]
     Visibility: public -/
 @[rust_fun "hax_lib::int::{hax_lib::int::ToInt<i32>}::to_int"]
-def I32.Insts.Hax_libIntToInt.to_int : Std.I32 → Result hax_lib.int.Int :=
+def hax_lib.I32.Insts.Hax_libIntToInt.to_int : Std.I32 → Result hax_lib.int.Int :=
   fun x => ok x.val
 
 /-- [hax_lib::int::{hax_lib::int::ToInt for i64}::to_int]:
@@ -167,7 +167,7 @@ def I32.Insts.Hax_libIntToInt.to_int : Std.I32 → Result hax_lib.int.Int :=
     Name pattern: [hax_lib::int::{hax_lib::int::ToInt<i64>}::to_int]
     Visibility: public -/
 @[rust_fun "hax_lib::int::{hax_lib::int::ToInt<i64>}::to_int"]
-def I64.Insts.Hax_libIntToInt.to_int : Std.I64 → Result hax_lib.int.Int :=
+def hax_lib.I64.Insts.Hax_libIntToInt.to_int : Std.I64 → Result hax_lib.int.Int :=
   fun x => ok x.val
 
 /-- [hax_lib::int::{hax_lib::int::ToInt for i128}::to_int]:
@@ -175,7 +175,7 @@ def I64.Insts.Hax_libIntToInt.to_int : Std.I64 → Result hax_lib.int.Int :=
     Name pattern: [hax_lib::int::{hax_lib::int::ToInt<i128>}::to_int]
     Visibility: public -/
 @[rust_fun "hax_lib::int::{hax_lib::int::ToInt<i128>}::to_int"]
-def I128.Insts.Hax_libIntToInt.to_int : Std.I128 → Result hax_lib.int.Int :=
+def hax_lib.I128.Insts.Hax_libIntToInt.to_int : Std.I128 → Result hax_lib.int.Int :=
   fun x => ok x.val
 
 /-- [hax_lib::int::{hax_lib::int::ToInt for isize}::to_int]:
@@ -183,7 +183,7 @@ def I128.Insts.Hax_libIntToInt.to_int : Std.I128 → Result hax_lib.int.Int :=
     Name pattern: [hax_lib::int::{hax_lib::int::ToInt<isize>}::to_int]
     Visibility: public -/
 @[rust_fun "hax_lib::int::{hax_lib::int::ToInt<isize>}::to_int"]
-def Isize.Insts.Hax_libIntToInt.to_int : Std.Isize → Result hax_lib.int.Int :=
+def hax_lib.Isize.Insts.Hax_libIntToInt.to_int : Std.Isize → Result hax_lib.int.Int :=
   fun x => ok x.val
 
 end core_models

From dc0a6088b1d30018ee5913f4923e6260bf5f8923 Mon Sep 17 00:00:00 2001
From: Maxime Buyse <maxime@cryspen.com>
Date: Wed, 6 May 2026 12:29:48 +0200
Subject: [PATCH 3/5] Fix: size to 128 conversions are TryFrom and not From.

---
 core-models/src/core/convert.rs | 30 +++++++++++++++---------------
 1 file changed, 15 insertions(+), 15 deletions(-)

diff --git a/core-models/src/core/convert.rs b/core-models/src/core/convert.rs
index 21ee4d9..bcc027b 100644
--- a/core-models/src/core/convert.rs
+++ b/core-models/src/core/convert.rs
@@ -149,13 +149,13 @@ macro_rules! int_try_from_trivial {
 }
 
 int_from! {
-    u8  u8  u16 u8  u16 u32 u8   u16  u32  u64  usize u8    u16,
-    u16 u32 u32 u64 u64 u64 u128 u128 u128 u128 u128  usize usize,
+    u8  u8  u16 u8  u16 u32 u8   u16  u32  u64  u8    u16,
+    u16 u32 u32 u64 u64 u64 u128 u128 u128 u128 usize usize,
 }
 
 int_from! {
-    i8  i8  i16 i8  i16 i32 i8   i16  i32  i64  isize i8    i16,
-    i16 i32 i32 i64 i64 i64 i128 i128 i128 i128 i128  isize isize,
+    i8  i8  i16 i8  i16 i32 i8   i16  i32  i64  i8    i16,
+    i16 i32 i32 i64 i64 i64 i128 i128 i128 i128 isize isize,
 }
 
 int_try_from! {
@@ -169,9 +169,9 @@ int_try_from! {
 }
 
 // We assume a 64-bits machine
-int_try_from_trivial!{
-    i32,
-    isize, 
+int_try_from_trivial! {
+    i32   isize usize,
+    isize i128  u128,
 }
 
 #[cfg(test)]
@@ -237,23 +237,23 @@ mod tests {
         }
 
     int_from_test! {
-        u8  u8  u16 u8  u16 u32 u8   u16  u32  u64  usize u8    u16,
-        u16 u32 u32 u64 u64 u64 u128 u128 u128 u128 u128 usize usize,
+        u8  u8  u16 u8  u16 u32 u8   u16  u32  u64  u8    u16,
+        u16 u32 u32 u64 u64 u64 u128 u128 u128 u128 usize usize,
     }
 
     int_from_test! {
-        i8  i8  i16 i8  i16 i32 i8   i16  i32  i64  isize i8    i16,
-        i16 i32 i32 i64 i64 i64 i128 i128 i128 i128 i128  isize isize,
+        i8  i8  i16 i8  i16 i32 i8   i16  i32  i64  i8    i16,
+        i16 i32 i32 i64 i64 i64 i128 i128 i128 i128 isize isize,
     }
 
     int_try_from_test! {
-        u16 u32 u32 u32   u64 u64 u64 u64   u128 u128 u128 u128 u128  usize usize usize usize,
-        u8  u8  u16 usize u8  u16 u32 usize u8   u16  u32  u64  usize u8    u16   u32   u64,
+        u16 u32 u32 u32   u64 u64 u64 u64   u128 u128 u128 u128 u128  usize usize usize usize usize,
+        u8  u8  u16 usize u8  u16 u32 usize u8   u16  u32  u64  usize u8    u16   u32   u64   u128,
     }
 
     int_try_from_test! {
-        i16 i32 i32 i32   i64 i64 i64 i64   i128 i128 i128 i128 i128  isize isize isize isize,
-        i8  i8  i16 isize i8  i16 i32 isize i8   i16  i32  i64  isize i8    i16   i32   i64,
+        i16 i32 i32 i32   i64 i64 i64 i64   i128 i128 i128 i128 i128  isize isize isize isize isize,
+        i8  i8  i16 isize i8  i16 i32 isize i8   i16  i32  i64  isize i8    i16   i32   i64   i128,
     }
 
     proptest! {

From ad1378256af92cb39f19499b4c468e0b6dbf0521 Mon Sep 17 00:00:00 2001
From: Maxime Buyse <maxime@cryspen.com>
Date: Wed, 6 May 2026 13:47:29 +0200
Subject: [PATCH 4/5] chore: re extract lean.

---
 lean/CoreModels/Funs.lean | 62 +++++++++++++++++++++------------------
 1 file changed, 34 insertions(+), 28 deletions(-)

diff --git a/lean/CoreModels/Funs.lean b/lean/CoreModels/Funs.lean
index 30665a6..eb0d8bd 100644
--- a/lean/CoreModels/Funs.lean
+++ b/lean/CoreModels/Funs.lean
@@ -1075,20 +1075,6 @@ def U128.Insts.Core_modelsConvertFromU64 : convert.From Std.U128 Std.U64 := {
   «from» := U128.Insts.Core_modelsConvertFromU64.from
 }
 
-/-- [core_models::convert::{core_models::convert::From<usize> for u128}::from]:
-    Source: 'core-models/src/core/convert.rs', lines 103:16-105:17 -/
-def U128.Insts.Core_modelsConvertFromUsize.from
-  (x : Std.Usize) : Result Std.U128 := do
-  ok (UScalar.cast .U128 x)
-
-/-- Trait implementation: [core_models::convert::{core_models::convert::From<usize> for u128}]
-    Source: 'core-models/src/core/convert.rs', lines 102:12-106:13 -/
-@[reducible]
-def U128.Insts.Core_modelsConvertFromUsize : convert.From Std.U128 Std.Usize
-  := {
-  «from» := U128.Insts.Core_modelsConvertFromUsize.from
-}
-
 /-- [core_models::convert::{core_models::convert::From<u8> for usize}::from]:
     Source: 'core-models/src/core/convert.rs', lines 103:16-105:17 -/
 def Usize.Insts.Core_modelsConvertFromU8.from
@@ -1242,20 +1228,6 @@ def I128.Insts.Core_modelsConvertFromI64 : convert.From Std.I128 Std.I64 := {
   «from» := I128.Insts.Core_modelsConvertFromI64.from
 }
 
-/-- [core_models::convert::{core_models::convert::From<isize> for i128}::from]:
-    Source: 'core-models/src/core/convert.rs', lines 103:16-105:17 -/
-def I128.Insts.Core_modelsConvertFromIsize.from
-  (x : Std.Isize) : Result Std.I128 := do
-  ok (IScalar.cast .I128 x)
-
-/-- Trait implementation: [core_models::convert::{core_models::convert::From<isize> for i128}]
-    Source: 'core-models/src/core/convert.rs', lines 102:12-106:13 -/
-@[reducible]
-def I128.Insts.Core_modelsConvertFromIsize : convert.From Std.I128 Std.Isize
-  := {
-  «from» := I128.Insts.Core_modelsConvertFromIsize.from
-}
-
 /-- [core_models::convert::{core_models::convert::From<i8> for isize}::from]:
     Source: 'core-models/src/core/convert.rs', lines 103:16-105:17 -/
 def Isize.Insts.Core_modelsConvertFromI8.from
@@ -2079,6 +2051,40 @@ def Isize.Insts.Core_modelsConvertTryFromI32TryFromIntError : convert.TryFrom
   try_from := Isize.Insts.Core_modelsConvertTryFromI32TryFromIntError.try_from
 }
 
+/-- [core_models::convert::{core_models::convert::TryFrom<isize, core_models::num::error::TryFromIntError> for i128}::try_from]:
+    Source: 'core-models/src/core/convert.rs', lines 143:16-145:17 -/
+def I128.Insts.Core_modelsConvertTryFromIsizeTryFromIntError.try_from
+  (x : Std.Isize) :
+  Result (result.Result Std.I128 num.error.TryFromIntError)
+  := do
+  let i ← lift (IScalar.cast .I128 x)
+  ok (result.Result.Ok i)
+
+/-- Trait implementation: [core_models::convert::{core_models::convert::TryFrom<isize, core_models::num::error::TryFromIntError> for i128}]
+    Source: 'core-models/src/core/convert.rs', lines 141:12-146:13 -/
+@[reducible]
+def I128.Insts.Core_modelsConvertTryFromIsizeTryFromIntError : convert.TryFrom
+  Std.I128 Std.Isize num.error.TryFromIntError := {
+  try_from := I128.Insts.Core_modelsConvertTryFromIsizeTryFromIntError.try_from
+}
+
+/-- [core_models::convert::{core_models::convert::TryFrom<usize, core_models::num::error::TryFromIntError> for u128}::try_from]:
+    Source: 'core-models/src/core/convert.rs', lines 143:16-145:17 -/
+def U128.Insts.Core_modelsConvertTryFromUsizeTryFromIntError.try_from
+  (x : Std.Usize) :
+  Result (result.Result Std.U128 num.error.TryFromIntError)
+  := do
+  let i ← lift (UScalar.cast .U128 x)
+  ok (result.Result.Ok i)
+
+/-- Trait implementation: [core_models::convert::{core_models::convert::TryFrom<usize, core_models::num::error::TryFromIntError> for u128}]
+    Source: 'core-models/src/core/convert.rs', lines 141:12-146:13 -/
+@[reducible]
+def U128.Insts.Core_modelsConvertTryFromUsizeTryFromIntError : convert.TryFrom
+  Std.U128 Std.Usize num.error.TryFromIntError := {
+  try_from := U128.Insts.Core_modelsConvertTryFromUsizeTryFromIntError.try_from
+}
+
 /-- [core_models::f32::{core_models::f32::f32}::abs]:
     Source: 'core-models/src/core/f32.rs', lines 9:4-11:5 -/
 def f32.f32.abs (x : F64) : Result F64 := do

From e57b9c3729055d34d4376eacf6f1e52a6f54dbf1 Mon Sep 17 00:00:00 2001
From: Maxime Buyse <maxime@cryspen.com>
Date: Thu, 7 May 2026 10:59:22 +0200
Subject: [PATCH 5/5] chore: move u32 to usize TryFrom to trivial macro.

---
 core-models/src/core/convert.rs |  8 +++----
 lean/CoreModels/Funs.lean       | 41 ++++++++++++++-------------------
 2 files changed, 21 insertions(+), 28 deletions(-)

diff --git a/core-models/src/core/convert.rs b/core-models/src/core/convert.rs
index bcc027b..d5a2825 100644
--- a/core-models/src/core/convert.rs
+++ b/core-models/src/core/convert.rs
@@ -159,8 +159,8 @@ int_from! {
 }
 
 int_try_from! {
-    u16 u32 u32 u32   u64 u64 u64 u64   u128 u128 u128 u128 u128  usize usize usize usize,
-    u8  u8  u16 usize u8  u16 u32 usize u8   u16  u32  u64  usize u8    u16   u32   u64,
+    u16 u32 u32 u64 u64 u64 u64   u128 u128 u128 u128 u128  usize usize usize usize,
+    u8  u8  u16 u8  u16 u32 usize u8   u16  u32  u64  usize u8    u16   u32   u64,
 }
 
 int_try_from! {
@@ -170,8 +170,8 @@ int_try_from! {
 
 // We assume a 64-bits machine
 int_try_from_trivial! {
-    i32   isize usize,
-    isize i128  u128,
+    i32   isize u32   usize,
+    isize i128  usize u128,
 }
 
 #[cfg(test)]
diff --git a/lean/CoreModels/Funs.lean b/lean/CoreModels/Funs.lean
index eb0d8bd..2feb4c8 100644
--- a/lean/CoreModels/Funs.lean
+++ b/lean/CoreModels/Funs.lean
@@ -1322,30 +1322,6 @@ def U16.Insts.Core_modelsConvertTryFromU32TryFromIntError : convert.TryFrom
   try_from := U16.Insts.Core_modelsConvertTryFromU32TryFromIntError.try_from
 }
 
-/-- [core_models::convert::{core_models::convert::TryFrom<u32, core_models::num::error::TryFromIntError> for usize}::try_from]:
-    Source: 'core-models/src/core/convert.rs', lines 122:16-128:17 -/
-def Usize.Insts.Core_modelsConvertTryFromU32TryFromIntError.try_from
-  (x : Std.U32) :
-  Result (result.Result Std.Usize num.error.TryFromIntError)
-  := do
-  let i ← lift (UScalar.cast .U32 core_models.num.Usize.MAX)
-  if x > i
-  then ok (result.Result.Err ())
-  else
-    let i1 ← lift (UScalar.cast .U32 core_models.num.Usize.MIN)
-    if x < i1
-    then ok (result.Result.Err ())
-    else let i2 ← lift (UScalar.cast .Usize x)
-         ok (result.Result.Ok i2)
-
-/-- Trait implementation: [core_models::convert::{core_models::convert::TryFrom<u32, core_models::num::error::TryFromIntError> for usize}]
-    Source: 'core-models/src/core/convert.rs', lines 120:12-129:13 -/
-@[reducible]
-def Usize.Insts.Core_modelsConvertTryFromU32TryFromIntError : convert.TryFrom
-  Std.Usize Std.U32 num.error.TryFromIntError := {
-  try_from := Usize.Insts.Core_modelsConvertTryFromU32TryFromIntError.try_from
-}
-
 /-- [core_models::convert::{core_models::convert::TryFrom<u64, core_models::num::error::TryFromIntError> for u8}::try_from]:
     Source: 'core-models/src/core/convert.rs', lines 122:16-128:17 -/
 def U8.Insts.Core_modelsConvertTryFromU64TryFromIntError.try_from
@@ -2068,6 +2044,23 @@ def I128.Insts.Core_modelsConvertTryFromIsizeTryFromIntError : convert.TryFrom
   try_from := I128.Insts.Core_modelsConvertTryFromIsizeTryFromIntError.try_from
 }
 
+/-- [core_models::convert::{core_models::convert::TryFrom<u32, core_models::num::error::TryFromIntError> for usize}::try_from]:
+    Source: 'core-models/src/core/convert.rs', lines 143:16-145:17 -/
+def Usize.Insts.Core_modelsConvertTryFromU32TryFromIntError.try_from
+  (x : Std.U32) :
+  Result (result.Result Std.Usize num.error.TryFromIntError)
+  := do
+  let i ← lift (UScalar.cast .Usize x)
+  ok (result.Result.Ok i)
+
+/-- Trait implementation: [core_models::convert::{core_models::convert::TryFrom<u32, core_models::num::error::TryFromIntError> for usize}]
+    Source: 'core-models/src/core/convert.rs', lines 141:12-146:13 -/
+@[reducible]
+def Usize.Insts.Core_modelsConvertTryFromU32TryFromIntError : convert.TryFrom
+  Std.Usize Std.U32 num.error.TryFromIntError := {
+  try_from := Usize.Insts.Core_modelsConvertTryFromU32TryFromIntError.try_from
+}
+
 /-- [core_models::convert::{core_models::convert::TryFrom<usize, core_models::num::error::TryFromIntError> for u128}::try_from]:
     Source: 'core-models/src/core/convert.rs', lines 143:16-145:17 -/
 def U128.Insts.Core_modelsConvertTryFromUsizeTryFromIntError.try_from