hax_lib/
dummy.rs

1mod abstraction;
2pub use abstraction::*;
3
4pub mod prop;
5pub use prop::*;
6
7pub use int::*;
8
9#[cfg(feature = "macros")]
10pub use crate::proc_macros::*;
11
12#[macro_export]
13macro_rules! debug_assert {
14    ($($arg:tt)*) => {
15        ::core::debug_assert!($($arg)*);
16    };
17}
18
19#[macro_export]
20macro_rules! assert {
21    ($($arg:tt)*) => {
22        ::core::assert!($($arg)*);
23    };
24}
25
26#[macro_export]
27macro_rules! assert_prop {
28    ($($arg:tt)*) => {{}};
29}
30
31#[macro_export]
32macro_rules! assume {
33    ($formula:expr) => {
34        ()
35    };
36}
37
38#[doc(hidden)]
39pub fn inline(_: &str) {}
40
41#[doc(hidden)]
42pub fn inline_unsafe<T>(_: &str) -> T {
43    unreachable!()
44}
45
46#[doc(hidden)]
47pub fn _internal_loop_invariant<T, R: Into<Prop>, P: FnOnce(T) -> R>(_: P) {}
48
49pub trait Refinement {
50    type InnerType;
51    fn new(x: Self::InnerType) -> Self;
52    fn get(self) -> Self::InnerType;
53    fn get_mut(&mut self) -> &mut Self::InnerType;
54    fn invariant(value: Self::InnerType) -> crate::Prop;
55}
56
57pub trait RefineAs<RefinedType> {
58    fn into_checked(self) -> RefinedType;
59}
60
61pub mod int {
62    use core::ops::*;
63
64    #[derive(Copy, Clone, Eq, PartialEq, Ord, PartialOrd)]
65    pub struct Int(pub u8);
66
67    impl Int {
68        pub fn new(x: impl Into<u8>) -> Self {
69            Int(x.into())
70        }
71        pub fn get(self) -> u8 {
72            self.0
73        }
74    }
75
76    impl Add for Int {
77        type Output = Self;
78
79        fn add(self, other: Self) -> Self::Output {
80            Int(self.0 + other.0)
81        }
82    }
83
84    impl Sub for Int {
85        type Output = Self;
86
87        fn sub(self, other: Self) -> Self::Output {
88            Int(self.0 - other.0)
89        }
90    }
91
92    impl Mul for Int {
93        type Output = Self;
94
95        fn mul(self, other: Self) -> Self::Output {
96            Int(self.0 * other.0)
97        }
98    }
99
100    impl Div for Int {
101        type Output = Self;
102
103        fn div(self, other: Self) -> Self::Output {
104            Int(self.0 / other.0)
105        }
106    }
107
108    impl Int {
109        pub fn pow2(self) -> Self {
110            self
111        }
112        pub fn _unsafe_from_str(_s: &str) -> Self {
113            Int(0)
114        }
115    }
116
117    pub trait ToInt {
118        fn to_int(self) -> Int;
119    }
120
121    pub trait Abstraction {
122        type AbstractType;
123        fn lift(self) -> Self::AbstractType;
124    }
125
126    pub trait Concretization<T> {
127        fn concretize(self) -> T;
128    }
129
130    macro_rules! implement_abstraction {
131        ($ty:ident) => {
132            impl Abstraction for $ty {
133                type AbstractType = Int;
134                fn lift(self) -> Self::AbstractType {
135                    Int(0)
136                }
137            }
138            impl ToInt for $ty {
139                fn to_int(self) -> Int {
140                    self.lift()
141                }
142            }
143        };
144        ($($ty:ident)*) => {
145            $(implement_abstraction!($ty);)*
146        };
147    }
148
149    implement_abstraction!(u8 u16 u32 u64 u128 usize);
150    implement_abstraction!(i8 i16 i32 i64 i128 isize);
151
152    macro_rules! implement_concretize {
153        ($ty:ident $method:ident) => {
154            impl Concretization<$ty> for Int {
155                fn concretize(self) -> $ty {
156                    self.0 as $ty
157                }
158            }
159            impl Int {
160                pub fn $method(self) -> $ty {
161                    self.concretize()
162                }
163            }
164        };
165        ($ty:ident $method:ident, $($tt:tt)*) => {
166            implement_concretize!($ty $method);
167            implement_concretize!($($tt)*);
168        };
169        () => {};
170    }
171
172    implement_concretize!(
173        u8    to_u8,
174        u16   to_u16,
175        u32   to_u32,
176        u64   to_u64,
177        u128  to_u128,
178        usize to_usize,
179        i8    to_i8,
180        i16   to_i16,
181        i32   to_i32,
182        i64   to_i64,
183        i128  to_i128,
184        isize to_isize,
185    );
186}
hax_lib/dummy.rs

hax_lib/
dummy.rs
