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 const fn _internal_loop_invariant<T, R: Into<Prop>, P: FnOnce(T) -> R>(_: &P) {}
48
49#[doc(hidden)]
50pub const fn _internal_while_loop_invariant(_: Prop) {}
51
52#[doc(hidden)]
53pub const fn _internal_loop_decreases(_: int::Int) {}
54
55pub trait Refinement {
56    type InnerType;
57    fn new(x: Self::InnerType) -> Self;
58    fn get(self) -> Self::InnerType;
59    fn get_mut(&mut self) -> &mut Self::InnerType;
60    fn invariant(value: Self::InnerType) -> crate::Prop;
61}
62
63pub trait RefineAs<RefinedType> {
64    fn into_checked(self) -> RefinedType;
65}
66
67pub mod int {
68    use core::ops::*;
69
70    #[macro_export]
71    macro_rules! int {
72        ($lit:expr) => {
73            Int($lit)
74        };
75    }
76
77    #[derive(Copy, Clone, Eq, PartialEq, Ord, PartialOrd)]
78    pub struct Int(pub u8);
79
80    impl Int {
81        pub fn new(x: impl Into<u8>) -> Self {
82            Int(x.into())
83        }
84        pub fn get(self) -> u8 {
85            self.0
86        }
87    }
88
89    impl Add for Int {
90        type Output = Self;
91
92        fn add(self, other: Self) -> Self::Output {
93            Int(self.0 + other.0)
94        }
95    }
96
97    impl Sub for Int {
98        type Output = Self;
99
100        fn sub(self, other: Self) -> Self::Output {
101            Int(self.0 - other.0)
102        }
103    }
104
105    impl Mul for Int {
106        type Output = Self;
107
108        fn mul(self, other: Self) -> Self::Output {
109            Int(self.0 * other.0)
110        }
111    }
112
113    impl Div for Int {
114        type Output = Self;
115
116        fn div(self, other: Self) -> Self::Output {
117            Int(self.0 / other.0)
118        }
119    }
120
121    impl Int {
122        pub fn pow2(self) -> Self {
123            self
124        }
125        pub fn _unsafe_from_str(_s: &str) -> Self {
126            Int(0)
127        }
128        pub fn rem_euclid(&self, v: Self) -> Self {
129            Self::new(self.0.rem_euclid(v.0))
130        }
131    }
132
133    pub trait ToInt {
134        fn to_int(self) -> Int;
135    }
136
137    pub trait Abstraction {
138        type AbstractType;
139        fn lift(self) -> Self::AbstractType;
140    }
141
142    pub trait Concretization<T> {
143        fn concretize(self) -> T;
144    }
145
146    macro_rules! implement_abstraction {
147        ($ty:ident) => {
148            impl Abstraction for $ty {
149                type AbstractType = Int;
150                fn lift(self) -> Self::AbstractType {
151                    Int(0)
152                }
153            }
154            impl ToInt for $ty {
155                fn to_int(self) -> Int {
156                    self.lift()
157                }
158            }
159        };
160        ($($ty:ident)*) => {
161            $(implement_abstraction!($ty);)*
162        };
163    }
164
165    implement_abstraction!(u8 u16 u32 u64 u128 usize);
166    implement_abstraction!(i8 i16 i32 i64 i128 isize);
167
168    macro_rules! implement_concretize {
169        ($ty:ident $method:ident) => {
170            impl Concretization<$ty> for Int {
171                fn concretize(self) -> $ty {
172                    self.0 as $ty
173                }
174            }
175            impl Int {
176                pub fn $method(self) -> $ty {
177                    self.concretize()
178                }
179            }
180        };
181        ($ty:ident $method:ident, $($tt:tt)*) => {
182            implement_concretize!($ty $method);
183            implement_concretize!($($tt)*);
184        };
185        () => {};
186    }
187
188    implement_concretize!(
189        u8    to_u8,
190        u16   to_u16,
191        u32   to_u32,
192        u64   to_u64,
193        u128  to_u128,
194        usize to_usize,
195        i8    to_i8,
196        i16   to_i16,
197        i32   to_i32,
198        i64   to_i64,
199        i128  to_i128,
200        isize to_isize,
201    );
202}
hax_lib/dummy.rs

hax_lib/
dummy.rs
