Fix integers try from

.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
 

core-models/src/core/convert.rs

@@ -131,24 +131,47 @@ 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,
+    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! {
-    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! {
-    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 u32   usize,
+    isize i128  usize u128,
 }
 
 #[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()
                                 );
                             }
                         }