hax_lib/int/
mod.rs

1use core::fmt;
2use core::ops::*;
3use num_traits::cast::ToPrimitive;
4
5mod bigint;
6use bigint::*;
7
8use super::abstraction::*;
9
10#[cfg(feature = "macros")]
11pub use hax_lib_macros::int;
12
13/// Mathematical integers for writting specifications. Mathematical
14/// integers are unbounded and arithmetic operation on them never over
15/// or underflow.
16///
17/// They are executable, but they are limited to a fixed number of bytes,
18/// so that they can carry the `Copy` trait. The backends model them as
19/// true mathematical integers anyway.
20#[derive(Copy, Clone, Eq, PartialEq, Ord, PartialOrd, Debug)]
21pub struct Int(BigInt);
22
23impl fmt::Display for Int {
24    fn fmt(&self, f: &mut fmt::Formatter<'_>) -> fmt::Result {
25        write!(f, "{}", self.get())
26    }
27}
28
29impl Int {
30    fn new(x: impl Into<num_bigint::BigInt>) -> Self {
31        Int(BigInt::new(&x.into()))
32    }
33    fn get(self) -> num_bigint::BigInt {
34        self.0.get()
35    }
36}
37
38impl Add for Int {
39    type Output = Self;
40
41    fn add(self, other: Self) -> Self::Output {
42        Self::new(self.get() + other.get())
43    }
44}
45
46impl Neg for Int {
47    type Output = Self;
48
49    fn neg(self) -> Self::Output {
50        Self::new(-self.get())
51    }
52}
53
54impl Sub for Int {
55    type Output = Self;
56
57    fn sub(self, other: Self) -> Self::Output {
58        Self::new(self.get() - other.get())
59    }
60}
61
62impl Mul for Int {
63    type Output = Self;
64
65    fn mul(self, other: Self) -> Self::Output {
66        Self::new(self.get() * other.get())
67    }
68}
69
70impl Div for Int {
71    type Output = Self;
72
73    fn div(self, other: Self) -> Self::Output {
74        Self::new(self.get() / other.get())
75    }
76}
77
78impl Int {
79    /// Raises `2` at the power `self`. Panics when `self` is negative.
80    pub fn pow2(self) -> Self {
81        use num_traits::Pow;
82        let exponent = self
83            .get()
84            .to_biguint()
85            .expect("`Int::pow2`: the exponent must be non-negative");
86        Self::new(Pow::pow(num_bigint::BigInt::from(2u8), exponent))
87    }
88
89    /// Constructs a `Int` out of a string literal. This function
90    /// assumes its argument consists only of decimal digits, with
91    /// optionally a minus sign prefix.
92    pub fn _unsafe_from_str(s: &str) -> Self {
93        use core::str::FromStr;
94        Self::new(num_bigint::BigInt::from_str(s).unwrap())
95    }
96
97    pub fn rem_euclid(&self, v: Self) -> Self {
98        use num_traits::Euclid;
99        Self::new(self.get().rem_euclid(&v.get()))
100    }
101}
102
103#[cfg(feature = "macros")]
104pub trait ToInt {
105    fn to_int(self) -> Int;
106}
107
108/// Instead of defining one overloaded instance, which relies
109/// explicitely on `num_bigint`:
110///
111/// ```ignore
112/// impl<T: Into<num_bigint::BigInt>> Abstraction for T {
113///     type AbstractType = Int;
114///     fn lift(self) -> Self::AbstractType {
115///         Int::new(self.into())
116///     }
117/// }
118/// ```
119///
120/// We define an instance per machine type: we don't want the
121/// interface of this module to rely specifically on
122/// `num_bigint`. This module should be a very thin layer.
123macro_rules! implement_abstraction {
124    ($ty:ident) => {
125        impl Abstraction for $ty {
126            type AbstractType = Int;
127            fn lift(self) -> Self::AbstractType {
128                Int::new(num_bigint::BigInt::from(self))
129            }
130        }
131        impl ToInt for $ty {
132            fn to_int(self) -> Int {
133                self.lift()
134            }
135        }
136    };
137    ($($ty:ident)*) => {
138        $(implement_abstraction!($ty);)*
139    };
140}
141
142implement_abstraction!(u8 u16 u32 u64 u128 usize);
143implement_abstraction!(i8 i16 i32 i64 i128 isize);
144
145macro_rules! implement_concretize {
146    ($ty:ident $method:ident) => {
147        impl Concretization<$ty> for Int {
148            fn concretize(self) -> $ty {
149                let concretized = self.get().$method();
150                debug_assert!(concretized.is_some());
151                concretized.unwrap().into()
152            }
153        }
154        impl Int {
155            pub fn $method(self) -> $ty {
156                self.concretize()
157            }
158        }
159    };
160    ($ty:ident $method:ident, $($tt:tt)*) => {
161        implement_concretize!($ty $method);
162        implement_concretize!($($tt)*);
163    };
164    () => {};
165}
166
167implement_concretize!(
168    u8    to_u8,
169    u16   to_u16,
170    u32   to_u32,
171    u64   to_u64,
172    u128  to_u128,
173    usize to_usize,
174    i8    to_i8,
175    i16   to_i16,
176    i32   to_i32,
177    i64   to_i64,
178    i128  to_i128,
179    isize to_isize,
180);
hax_lib/int/mod.rs

hax_lib/int/
mod.rs
