feat(hax-lib): drop explicit dependency to num_bigint in interface

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 {

test-harness/src/snapshots/toolchain__literals into-coq.snap

@@ -58,14 +58,6 @@ Definition fn_pointer_cast (_ : unit) : unit :=
       x : int32 -> int32 in
   tt.
 
-Definition numeric (_ : unit) : unit :=
-  let (_ : uint_size) := (@repr WORDSIZE32 123) : uint_size in
-  let (_ : uint_size) := (@repr WORDSIZE32 42) : uint_size in
-  let (_ : uint_size) := (@repr WORDSIZE32 42) : uint_size in
-  let (_ : int32) := (@repr WORDSIZE32 42) : int32 in
-  let (_ : int128) := (@repr WORDSIZE128 22222222222222222222) : int128 in
-  tt.
-
 Definition math_integers (x : t_Int_t) : int8 :=
   let (_ : t_Int_t) := f_lift (@repr WORDSIZE32 3) : t_Int_t in
   let _ := (impl__Int___unsafe_from_str -340282366920938463463374607431768211455000)>.?(impl__Int___unsafe_from_str 340282366920938463463374607431768211455000) : bool in
@@ -90,6 +82,14 @@ Definition math_integers (x : t_Int_t) : int8 :=
   let (_ : uint_size) := impl__Int__to_usize x : uint_size in
   impl__Int__to_u8 (x.+(x.*x)).
 
+Definition numeric (_ : unit) : unit :=
+  let (_ : uint_size) := (@repr WORDSIZE32 123) : uint_size in
+  let (_ : uint_size) := (@repr WORDSIZE32 42) : uint_size in
+  let (_ : uint_size) := (@repr WORDSIZE32 42) : uint_size in
+  let (_ : int32) := (@repr WORDSIZE32 42) : int32 in
+  let (_ : int128) := (@repr WORDSIZE128 22222222222222222222) : int128 in
+  tt.
+
 Definition empty_array (_ : unit) : unit :=
   let (_ : seq int8) := unsize !TODO empty array! : seq int8 in
   tt.

test-harness/src/snapshots/toolchain__literals into-fstar.snap

@@ -35,12 +35,6 @@ module Literals
 open Core
 open FStar.Mul
 
-let _ =
-  (* This module has implicit dependencies, here we make them explicit. *)
-  (* The implicit dependencies arise from typeclasses instances. *)
-  let open Num_bigint.Bigint.Convert in
-  ()
-
 let casts (x8: u8) (x16: u16) (x32: u32) (x64: u64) (xs: usize) : Prims.unit =
   let (_: u64):u64 =
     ((((cast (x8 <: u8) <: u64) +! (cast (x16 <: u16) <: u64) <: u64) +! (cast (x32 <: u32) <: u64)
@@ -115,14 +109,6 @@ let fn_pointer_cast (_: Prims.unit) : Prims.unit =
   let (f: (u32 -> u32)): u32 -> u32 = fun x -> x in
   ()
 
-let numeric (_: Prims.unit) : Prims.unit =
-  let (_: usize):usize = sz 123 in
-  let (_: isize):isize = isz (-42) in
-  let (_: isize):isize = isz 42 in
-  let (_: i32):i32 = (-42l) in
-  let (_: u128):u128 = pub_u128 22222222222222222222 in
-  ()
-
 let math_integers (x: Hax_lib.Int.t_Int)
     : Prims.Pure u8
       (requires x > (0 <: Hax_lib.Int.t_Int) && x < (16 <: Hax_lib.Int.t_Int))
@@ -153,6 +139,14 @@ let math_integers (x: Hax_lib.Int.t_Int)
   let (_: usize):usize = Hax_lib.Int.impl__Int__to_usize x in
   Hax_lib.Int.impl__Int__to_u8 (x + (x * x <: Hax_lib.Int.t_Int) <: Hax_lib.Int.t_Int)
 
+let numeric (_: Prims.unit) : Prims.unit =
+  let (_: usize):usize = sz 123 in
+  let (_: isize):isize = isz (-42) in
+  let (_: isize):isize = isz 42 in
+  let (_: i32):i32 = (-42l) in
+  let (_: u128):u128 = pub_u128 22222222222222222222 in
+  ()
+
 let empty_array (_: Prims.unit) : Prims.unit =
   let (_: t_Slice u8):t_Slice u8 =
     Rust_primitives.unsize (let list:Prims.list u8 = [] in