Make hax-lib ints executable bigints.

hax-lib/Cargo.toml

@@ -10,12 +10,12 @@ readme = "README.md"
 description = "Hax-specific helpers for Rust programs"
 
 
-[target.'cfg(hax)'.dependencies]
-num-bigint = { version = "0.4", default-features = false }
-num-traits = { version = "0.2", default-features = false }
 
 [dependencies]
 hax-lib-macros = { workspace = true, optional = true }
+num-bigint = { version = "0.4", default-features = false }
+num-traits = { version = "0.2", default-features = false }
+
 
 [features]
 default = ["macros"]

hax-lib/src/dummy.rs

@@ -64,139 +64,4 @@ pub trait RefineAs<RefinedType> {
     fn into_checked(self) -> RefinedType;
 }
 
-pub mod int {
-    use core::ops::*;
-
-    #[macro_export]
-    macro_rules! int {
-        ($lit:expr) => {
-            Int($lit)
-        };
-    }
-
-    #[derive(Copy, Clone, Eq, PartialEq, Ord, PartialOrd)]
-    pub struct Int(pub u8);
-
-    impl Int {
-        pub fn new(x: impl Into<u8>) -> Self {
-            Int(x.into())
-        }
-        pub fn get(self) -> u8 {
-            self.0
-        }
-    }
-
-    impl Add for Int {
-        type Output = Self;
-
-        fn add(self, other: Self) -> Self::Output {
-            Int(self.0 + other.0)
-        }
-    }
-
-    impl Sub for Int {
-        type Output = Self;
-
-        fn sub(self, other: Self) -> Self::Output {
-            Int(self.0 - other.0)
-        }
-    }
-
-    impl Mul for Int {
-        type Output = Self;
-
-        fn mul(self, other: Self) -> Self::Output {
-            Int(self.0 * other.0)
-        }
-    }
-
-    impl Div for Int {
-        type Output = Self;
-
-        fn div(self, other: Self) -> Self::Output {
-            Int(self.0 / other.0)
-        }
-    }
-
-    impl Int {
-        pub fn pow2(self) -> Self {
-            self
-        }
-        pub fn _unsafe_from_str(_s: &str) -> Self {
-            Int(0)
-        }
-        pub fn rem_euclid(&self, v: Self) -> Self {
-            Self::new(self.0.rem_euclid(v.0))
-        }
-    }
-
-    pub trait ToInt {
-        fn to_int(self) -> Int;
-    }
-
-    pub trait Abstraction {
-        type AbstractType;
-        fn lift(self) -> Self::AbstractType;
-    }
-
-    pub trait Concretization<T> {
-        fn concretize(self) -> T;
-    }
-
-    macro_rules! implement_abstraction {
-        ($ty:ident) => {
-            impl Abstraction for $ty {
-                type AbstractType = Int;
-                fn lift(self) -> Self::AbstractType {
-                    Int(0)
-                }
-            }
-            impl ToInt for $ty {
-                fn to_int(self) -> Int {
-                    self.lift()
-                }
-            }
-        };
-        ($($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 {
-                fn concretize(self) -> $ty {
-                    self.0 as $ty
-                }
-            }
-            impl Int {
-                pub fn $method(self) -> $ty {
-                    self.concretize()
-                }
-            }
-        };
-        ($ty:ident $method:ident, $($tt:tt)*) => {
-            implement_concretize!($ty $method);
-            implement_concretize!($($tt)*);
-        };
-        () => {};
-    }
-
-    implement_concretize!(
-        u8    to_u8,
-        u16   to_u16,
-        u32   to_u32,
-        u64   to_u64,
-        u128  to_u128,
-        usize to_usize,
-        i8    to_i8,
-        i16   to_i16,
-        i32   to_i32,
-        i64   to_i64,
-        i128  to_i128,
-        isize to_isize,
-    );
-}
+pub mod int;

hax-lib/src/int/mod.rs

@@ -10,7 +10,7 @@ use super::abstraction::*;
 #[cfg(feature = "macros")]
 pub use hax_lib_macros::int;
 
-/// Mathematical integers for writting specifications. Mathematical
+/// Mathematical integers for writing specifications. Mathematical
 /// integers are unbounded and arithmetic operation on them never over
 /// or underflow.
 #[derive(Copy, Clone, Eq, PartialEq, Ord, PartialOrd, Debug)]