From f7193f6043a1744126d4b57e2fcaceeddb11d596 Mon Sep 17 00:00:00 2001
From: Lucas Franceschino <lucas@cryspen.com>
Date: Thu, 16 May 2024 09:37:49 +0200
Subject: [PATCH] feat(hax-lib): drop explicit dependency to `num_bigint` in
 interface

---
 hax-lib/src/int/mod.rs | 35 ++++++++++++++++++++++++++++++-----
 1 file changed, 30 insertions(+), 5 deletions(-)

diff --git a/hax-lib/src/int/mod.rs b/hax-lib/src/int/mod.rs
index c7a1eea81..25e0939a0 100644
--- a/hax-lib/src/int/mod.rs
+++ b/hax-lib/src/int/mod.rs
@@ -89,13 +89,38 @@ pub trait Concretization<T> {
     fn concretize(self) -> T;
 }
 
-impl<T: Into<num_bigint::BigInt>> Abstraction for T {
-    type AbstractType = Int;
-    fn lift(self) -> Self::AbstractType {
-        Int::new(self.into())
-    }
+/// Instead of defining one overloaded instance, which relies
+/// explicitely on `num_bigint`:
+///
+/// ```ignore
+/// impl<T: Into<num_bigint::BigInt>> Abstraction for T {
+///     type AbstractType = Int;
+///     fn lift(self) -> Self::AbstractType {
+///         Int::new(self.into())
+///     }
+/// }
+/// ```
+///
+/// We define an instance per machine type: we don't want the
+/// interface of this module to rely specifically on
+/// `num_bigint`. This module should be a very thin layer.
+macro_rules! implement_abstraction {
+    ($ty:ident) => {
+        impl Abstraction for $ty {
+            type AbstractType = Int;
+            fn lift(self) -> Self::AbstractType {
+                Int::new(num_bigint::BigInt::from(self))
+            }
+        }
+    };
+    ($($ty:ident)*) => {
+        $(implement_abstraction!($ty);)*
+    };
 }
 
+implement_abstraction!(u8 u16 u32 u64 u128 usize);
+implement_abstraction!(i8 i16 i32 i64 i128 isize);
+
 macro_rules! implement_concretize {
     ($ty:ident $method:ident) => {
         impl Concretization<$ty> for Int {