hax_bounded_integers/
lib.rs

1use hax_lib::Refinement;
2pub mod num_traits;
3
4pub mod _macro_utils {
5    pub use duplicate;
6    pub use paste;
7}
8
9#[doc(hidden)]
10#[macro_export]
11macro_rules! derivate_binop_for_bounded {
12    ($(<$(const $cst_name:ident : $cst_ty:ty),*>)?{$t:ident, $bounded_t:ident}; $($tt:tt)*) => {
13        $crate::derivate_binop_for_bounded!($(<$(const $cst_name:$cst_ty),*>)?{$t, $bounded_t, get, Self::Output}; $($tt)*) ;
14    };
15    ($(<$(const $cst_name:ident : $cst_ty:ty),*>)?{$t:ident, $bounded_t:ident, $get:ident, $out:ty};) => {};
16    ($(<$(const $cst_name:ident : $cst_ty:ty),*>)?{$t:ident, $bounded_t:ident, $get:ident, $out:ty}; ($trait:ident, $meth:ident), $($tt:tt)*) => {
17        $crate::derivate_binop_for_bounded!(@$t, $bounded_t, $trait, $meth, $get, $out, $(<$(const $cst_name:$cst_ty),*>)?);
18        $crate::derivate_binop_for_bounded!($(<$(const $cst_name:$cst_ty),*>)?{$t, $bounded_t, $get, $out}; $($tt)*);
19    };
20    (@$t:ident, $bounded_t:ident, $trait:ident, $meth:ident, $get:ident, $out:ty$(,)?) => {
21        $crate::derivate_binop_for_bounded!(
22            @$t, $bounded_t, $trait, $meth, $get, $out,
23            <const MIN: $t, const MAX: $t>
24        );
25    };
26    (@$t:ident, $bounded_t:ident, $trait:ident, $meth:ident, $get:ident, $out:ty,
27     <$(const $cst_name:ident : $cst_ty:ty),*>
28    ) => {
29        $crate::_macro_utils::paste::paste!{
30            // BoundedT<A, B> <OP> BoundedT<C, D>
31            impl<$(const [< $cst_name _LHS >]: $cst_ty,)* $(const [< $cst_name _RHS >]: $cst_ty,)*>
32                $trait<$bounded_t<$([< $cst_name _RHS >],)*>> for $bounded_t<$([< $cst_name _LHS >],)*>
33            {
34                type Output = $t;
35                #[inline(always)]
36                fn $meth(self, other: $bounded_t<$([< $cst_name _RHS >],)*>) -> $out {
37                    (self.$get()).$meth(other.$get())
38                }
39            }
40
41            // BoundedT<A, B> <OP> T
42            impl<$(const $cst_name: $cst_ty,)*> $trait<$t> for $bounded_t<$($cst_name,)*> {
43                type Output = $t;
44                #[inline(always)]
45                fn $meth(self, other: $t) -> $out {
46                    (self.$get()).$meth(other)
47                }
48            }
49
50
51            // T <OP> BoundedT<A, B>
52            impl<$(const $cst_name: $cst_ty,)*> $trait<$bounded_t<$($cst_name,)*>> for $t {
53                type Output = $t;
54                #[inline(always)]
55                fn $meth(self, other: $bounded_t<$($cst_name,)*>) -> $out {
56                    (self).$meth(other.$get())
57                }
58            }
59        }
60    };
61}
62
63#[doc(hidden)]
64#[macro_export]
65macro_rules! derivate_assign_binop_for_bounded {
66    ($(<$(const $cst_name:ident : $cst_ty:ty),*>)?{$t:ident, $bounded_t:ident}; $($tt:tt)*) => {
67        $crate::derivate_assign_binop_for_bounded!($(<$(const $cst_name:$cst_ty),*>)?{$t, $bounded_t, get, Self::Output}; $($tt)*) ;
68    };
69    ($(<$(const $cst_name:ident : $cst_ty:ty),*>)?{$t:ident, $bounded_t:ident, $get:ident, $out:ty};) => {};
70    ($(<$(const $cst_name:ident : $cst_ty:ty),*>)?{$t:ident, $bounded_t:ident, $get:ident, $out:ty}; ($trait:ident, $meth:ident), $($tt:tt)*) => {
71        $crate::derivate_assign_binop_for_bounded!(@$t, $bounded_t, $trait, $meth, $get, $out, $(<$(const $cst_name:$cst_ty),*>)?);
72        $crate::derivate_assign_binop_for_bounded!($(<$(const $cst_name:$cst_ty),*>)?{$t, $bounded_t, $get, $out}; $($tt)*);
73    };
74    (@$t:ident, $bounded_t:ident, $trait:ident, $meth:ident, $get:ident, $out:ty$(,)?) => {
75        $crate::derivate_assign_binop_for_bounded!(
76            @$t, $bounded_t, $trait, $meth, $get, $out,
77            <const MIN: $t, const MAX: $t>
78        );
79    };
80    (@$t:ident, $bounded_t:ident, $trait:ident, $meth:ident, $get:ident, $out:ty,
81     <$(const $cst_name:ident : $cst_ty:ty),*>
82    ) => {
83        $crate::_macro_utils::paste::paste!{
84            // BoundedT<A, B> <OP> BoundedT<C, D>
85            impl<$(const [< $cst_name _LHS >]: $cst_ty,)* $(const [< $cst_name _RHS >]: $cst_ty,)*>
86                $trait<$bounded_t<$([< $cst_name _RHS >],)*>> for $bounded_t<$([< $cst_name _LHS >],)*>
87            {
88                #[inline(always)]
89                fn $meth(&mut self, other: $bounded_t<$([< $cst_name _RHS >],)*>) {
90                    self.get_mut().$meth(other.$get())
91                }
92            }
93
94            // BoundedT<A, B> <OP> $t
95            impl<$(const [< $cst_name _LHS >]: $cst_ty,)*>
96                $trait<$t> for $bounded_t<$([< $cst_name _LHS >],)*>
97            {
98                #[inline(always)]
99                fn $meth(&mut self, other: $t) {
100                    self.get_mut().$meth(other)
101                }
102            }
103
104            // $t <OP> BoundedT<A, B>
105            impl<$(const [< $cst_name _RHS >]: $cst_ty,)*>
106                $trait<$bounded_t<$([< $cst_name _RHS >],)*>> for $t
107            {
108                #[inline(always)]
109                fn $meth(&mut self, other: $bounded_t<$([< $cst_name _RHS >],)*>) {
110                    self.$meth(other.get())
111                }
112            }
113        }
114    };
115}
116
117#[doc(hidden)]
118#[macro_export]
119macro_rules! derivate_operations_for_bounded {
120    ($bounded_t:ident($t: ident $($bytes:expr)?)$(,)?
121     <$(const $cst_name:ident : $cst_ty:ty),*>
122    ) => {
123          #[$crate::_macro_utils::duplicate::duplicate_item(
124              INTRO_CONSTANTS USE_CONSTANTS;
125              [ $(const $cst_name:$cst_ty),* ] [ $($cst_name),* ];
126          )]
127          #[hax_lib::exclude]
128        const _: () = {
129            use ::core::ops::*;
130            use $crate::num_traits::*;
131            use ::hax_lib::Refinement;
132
133            $crate::derivate_assign_binop_for_bounded!(
134                <INTRO_CONSTANTS>
135                {$t, $bounded_t};
136                (AddAssign, add_assign),
137                (SubAssign, sub_assign),
138                (MulAssign, mul_assign),
139                (DivAssign, div_assign),
140                (RemAssign, rem_assign),
141                (ShlAssign, shl_assign),
142                (ShrAssign, shr_assign),
143                (BitAndAssign, bitand_assign),
144                (BitOrAssign, bitor_assign),
145                (BitXorAssign, bitxor_assign),
146            );
147
148            $crate::derivate_binop_for_bounded!(
149                <INTRO_CONSTANTS>
150                {$t, $bounded_t};
151                (Add, add), (Sub, sub), (Mul, mul), (Div, div), (Rem, rem),
152                (BitOr, bitor), (BitAnd, bitand), (BitXor, bitxor),
153                (Shl, shl), (Shr, shr),
154                (WrappingAdd, wrapping_add), (WrappingSub, wrapping_sub),
155                (WrappingMul, wrapping_mul), (WrappingDiv, wrapping_div),
156            );
157
158            $crate::derivate_binop_for_bounded!(
159                <INTRO_CONSTANTS>
160                {$t, $bounded_t, get, Option<Self::Output>};
161                (CheckedAdd, checked_add), (CheckedSub, checked_sub),
162                (CheckedMul, checked_mul), (CheckedDiv, checked_div),
163            );
164
165            impl<INTRO_CONSTANTS> CheckedNeg for $bounded_t<USE_CONSTANTS> {
166                type Output = $t;
167                #[inline(always)]
168                fn checked_neg(&self) -> Option<$t> {
169                    self.deref().checked_neg()
170                }
171            }
172
173            impl<INTRO_CONSTANTS> Not for $bounded_t<USE_CONSTANTS> {
174                type Output = $t;
175                #[inline(always)]
176                fn not(self) -> Self::Output {
177                    self.deref().not()
178                }
179            }
180
181            impl<INTRO_CONSTANTS> NumOps<Self, $t> for $bounded_t<USE_CONSTANTS> {}
182
183            // impl<INTRO_CONSTANTS> Bounded for $bounded_t<USE_CONSTANTS> {
184            //     #[inline(always)]
185            //     fn min_value() -> Self {
186            //         Self::new(MIN)
187            //     }
188            //     #[inline(always)]
189            //     fn max_value() -> Self {
190            //         Self::new(MAX)
191            //     }
192            // }
193
194            $(
195                impl<INTRO_CONSTANTS> FromBytes for $bounded_t<USE_CONSTANTS> {
196                    type BYTES = [u8; $bytes];
197
198                    #[inline(always)]
199                    fn from_le_bytes(bytes: Self::BYTES) -> Self {
200                        Self::new($t::from_le_bytes(bytes))
201                    }
202                    #[inline(always)]
203                    fn from_be_bytes(bytes: Self::BYTES) -> Self {
204                        Self::new($t::from_be_bytes(bytes))
205                    }
206                }
207
208                impl<INTRO_CONSTANTS> ToBytes for $bounded_t<USE_CONSTANTS> {
209                    #[inline(always)]
210                    fn to_le_bytes(self) -> Self::BYTES {
211                        self.get().to_le_bytes()
212                    }
213                    #[inline(always)]
214                    fn to_be_bytes(self) -> Self::BYTES {
215                        self.get().to_be_bytes()
216                    }
217                }
218            )?
219
220            impl<INTRO_CONSTANTS> Zero for $bounded_t<USE_CONSTANTS> {
221                #[inline(always)]
222                fn zero() -> Self {
223                    Self::new(0)
224                }
225            }
226
227            impl<INTRO_CONSTANTS> One for $bounded_t<USE_CONSTANTS> {
228                #[inline(always)]
229                fn one() -> Self {
230                    Self::new(1)
231                }
232            }
233
234            impl<INTRO_CONSTANTS> MachineInt<$t> for $bounded_t<USE_CONSTANTS> { }
235
236            impl<INTRO_CONSTANTS> BitOps for $bounded_t<USE_CONSTANTS> {
237                type Output = $t;
238
239                #[inline(always)]
240                fn count_ones(self) -> u32 {
241                    self.get().count_ones()
242                }
243                #[inline(always)]
244                fn count_zeros(self) -> u32 {
245                    self.get().count_zeros()
246                }
247                #[inline(always)]
248                fn leading_ones(self) -> u32 {
249                    self.get().leading_ones()
250                }
251                #[inline(always)]
252                fn leading_zeros(self) -> u32 {
253                    self.get().leading_zeros()
254                }
255                #[inline(always)]
256                fn trailing_ones(self) -> u32 {
257                    self.get().trailing_ones()
258                }
259                #[inline(always)]
260                fn trailing_zeros(self) -> u32 {
261                    self.get().trailing_zeros()
262                }
263                #[inline(always)]
264                fn rotate_left(self, n: u32) -> Self::Output {
265                    self.get().rotate_left(n)
266                }
267                #[inline(always)]
268                fn rotate_right(self, n: u32) -> Self::Output {
269                    self.get().rotate_right(n)
270                }
271                #[inline(always)]
272                fn from_be(x: Self) -> Self::Output {
273                    Self::Output::from_be(x.get())
274                }
275                #[inline(always)]
276                fn from_le(x: Self) -> Self::Output {
277                    Self::Output::from_le(x.get())
278                }
279                #[inline(always)]
280                fn to_be(self) -> Self::Output {
281                    Self::Output::to_be(self.get())
282                }
283                #[inline(always)]
284                fn to_le(self) -> Self::Output {
285                    Self::Output::to_le(self.get())
286                }
287                #[inline(always)]
288                fn pow(self, exp: u32) -> Self::Output {
289                    Self::Output::pow(self.get(), exp)
290                }
291            }
292        };
293    }
294}
295
296#[doc(hidden)]
297#[macro_export]
298macro_rules! mk_bounded {
299    ($(#$attr:tt)* $bounded_t:ident<$(const $cst_name:ident : $cst_ty:ty),*>($t: ident $($bytes:expr)?, |$x:ident| $body:expr)$(,)?) => {
300        #[hax_lib::refinement_type(|$x| $body)]
301        #[derive(Clone, Copy, Eq, PartialEq, Ord, PartialOrd, Hash)]
302        $(#$attr)*
303        pub struct $bounded_t<$(const $cst_name : $cst_ty),*>($t);
304        $crate::derivate_operations_for_bounded!($bounded_t($t$($bytes)?)<$(const $cst_name : $cst_ty),*>);
305    };
306    ($bounded_t:ident($t: ident $($bytes:expr)?)$(,)?) => {
307        $crate::mk_bounded!(
308            #[doc = concat!("Bounded ", stringify!($t)," integers. This struct enforces the invariant that values are greater or equal to `MIN` and less or equal to `MAX`.")]
309            $bounded_t<const MIN: $t, const MAX: $t>($t $($bytes)?, |x| x >= MIN && x <= MAX)
310        );
311    };
312    ($bounded_t:ident($t: ident $($bytes:expr)?), $($tt:tt)+) => {
313        $crate::mk_bounded!($bounded_t($t $($bytes)?));
314        $crate::mk_bounded!($($tt)+);
315    };
316}
317
318mk_bounded!(
319    BoundedI8(i8 1),
320    BoundedI16(i16 2),
321    BoundedI32(i32 4),
322    BoundedI64(i64 8),
323    BoundedI128(i128 16),
324    BoundedIsize(isize),
325    BoundedU8(u8 1),
326    BoundedU16(u16 2),
327    BoundedU32(u32 4),
328    BoundedU64(u64 8),
329    BoundedU128(u128 16),
330    BoundedUsize(usize),
331);
332
333/// Makes a refined new type in a very similar way to
334/// `hax_lib::refinement_tyoe`, but derives the various traits an
335/// integer type is expected to implement.
336///
337/// Examples:
338/// ```rust
339/// # use hax_bounded_integers::refinement_int;
340/// refinement_int!(BoundedAbsI16<const B: usize>(i16, 2, |x| x >= -(B as i16) && x <= (B as i16)));
341/// refinement_int!(BoundedAbsIsize<const B: usize>(isize, |x| x >= -(B as isize) && x <= (B as isize)));
342/// ```
343#[macro_export]
344macro_rules! refinement_int {
345    ($(#$attr:tt)* $bounded_t:ident$(<$(const $cst_name:ident : $cst_ty:ty),*$(,)?>)?($t: ident, $($bytes:literal,)? |$x:ident| $body:expr)$(,)?) => {
346        $crate::mk_bounded!($(#$attr)* $bounded_t<$($(const $cst_name:$cst_ty),*)?>($t $($bytes)?, |$x| $body));
347    };
348}
349
350#[hax_lib::exclude]
351const _: () = {
352    impl<const MIN: usize, const MAX: usize, T> core::ops::Index<BoundedUsize<MIN, MAX>> for [T] {
353        type Output = T;
354        #[inline(always)]
355        fn index(&self, index: BoundedUsize<MIN, MAX>) -> &Self::Output {
356            &self[index.get()]
357        }
358    }
359
360    impl<const MIN: usize, const MAX: usize, T> core::ops::IndexMut<BoundedUsize<MIN, MAX>> for [T] {
361        #[inline(always)]
362        fn index_mut(&mut self, index: BoundedUsize<MIN, MAX>) -> &mut Self::Output {
363            &mut self[index.get()]
364        }
365    }
366};
367
368#[test]
369fn tests() {
370    refinement_int!(
371        Test<const B: usize>(i16, 2, |x| B < 32768 && x >= -(B as i16) && x <= (B as i16))
372    );
373
374    use hax_lib::*;
375
376    let mut zzz: Test<123> = (-122).into_checked();
377    zzz += 32;
378
379    let x: BoundedU8<0, 5> = 2.into_checked();
380    let y: BoundedU8<5, 10> = (x + x).into_checked();
381
382    let _ = x >> 3;
383    let _ = x >> BoundedU8::<0, 5>::new(3);
384
385    let _ = x / y;
386    let _ = x * y;
387    let _ = x + y;
388    let _ = y - x;
389
390    let _ = x / 1;
391    let _ = x * 1;
392    let _ = x + 1;
393    let _ = x - 1;
394    let _ = 4 / y;
395    let _ = 4 * y;
396    let _ = 4 + y;
397    let _ = 4 - y;
398}
hax_bounded_integers/lib.rs

hax_bounded_integers/
lib.rs
