prusti_contracts/
lib.rs

1#![no_std]
2
3/// A macro for writing a precondition on a function.
4pub use prusti_contracts_proc_macros::requires;
5
6/// A macro for writing a postcondition on a function.
7pub use prusti_contracts_proc_macros::ensures;
8
9/// A macro for writing a pledge on a function.
10pub use prusti_contracts_proc_macros::after_expiry;
11
12/// A macro for writing a two-state pledge on a function.
13pub use prusti_contracts_proc_macros::assert_on_expiry;
14
15/// A macro for marking a function as pure.
16pub use prusti_contracts_proc_macros::pure;
17
18/// A macro for marking a function as trusted.
19pub use prusti_contracts_proc_macros::trusted;
20
21/// A macro for marking a function as opted into verification.
22pub use prusti_contracts_proc_macros::verified;
23
24/// A macro for type invariants.
25pub use prusti_contracts_proc_macros::invariant;
26
27/// A macro for writing a loop body invariant.
28pub use prusti_contracts_proc_macros::body_invariant;
29
30/// A macro for writing assertions using the full prusti specifications
31pub use prusti_contracts_proc_macros::prusti_assert;
32
33/// A macro for writing assumptions using prusti syntax
34pub use prusti_contracts_proc_macros::prusti_assume;
35
36/// A macro for writing refutations using prusti syntax
37pub use prusti_contracts_proc_macros::prusti_refute;
38
39/// A macro for impl blocks that refine trait specifications.
40pub use prusti_contracts_proc_macros::refine_trait_spec;
41
42/// A macro for specifying external functions.
43pub use prusti_contracts_proc_macros::extern_spec;
44
45/// A macro for defining a predicate using prusti expression syntax instead
46/// of just Rust expressions.
47pub use prusti_contracts_proc_macros::predicate;
48
49/// Macro for creating type models.
50pub use prusti_contracts_proc_macros::model;
51
52/// A macro to add trait bounds on a generic type parameter and specifications
53/// which are active only when these bounds are satisfied for a call.
54pub use prusti_contracts_proc_macros::refine_spec;
55
56/// A macro for defining ghost blocks which will be left in for verification
57/// but omitted during compilation.
58pub use prusti_contracts_proc_macros::ghost;
59
60/// A macro to customize how a struct or enum should be printed in a counterexample
61pub use prusti_contracts_proc_macros::print_counterexample;
62
63/// A macro to annotate termination of a function
64pub use prusti_contracts_proc_macros::terminates;
65
66/// A macro to annotate body variant of a loop to prove termination
67pub use prusti_contracts_proc_macros::body_variant;
68
69#[cfg(not(feature = "prusti"))]
70mod private {
71    use core::marker::PhantomData;
72
73    /// A macro for defining a closure with a specification.
74    /// Note: this is a declarative macro defined in this crate
75    /// because declarative macros can't be exported from
76    /// the `prusti-contracts-proc-macros` proc-macro crate.
77    /// See <https://github.com/rust-lang/rust/issues/40090>.
78    #[macro_export]
79    macro_rules! closure {
80        ($condition:ident ($($args:tt)*), $($tail:tt)*) => {
81            $crate::closure!($($tail)*)
82        };
83        ($($tail:tt)*) => {
84            $($tail)*
85        };
86    }
87
88    #[macro_export]
89    macro_rules! prusti_assert_eq {
90        ($left:expr, $right:expr $(,)?) => {};
91    }
92
93    #[macro_export]
94    macro_rules! prusti_assert_ne {
95        ($left:expr, $right:expr $(,)?) => {};
96    }
97
98    /// A sequence type
99    #[non_exhaustive]
100    #[derive(PartialEq, Eq, Copy, Clone)]
101    pub struct Seq<T> {
102        _phantom: PhantomData<T>,
103    }
104
105    /// A map type
106    #[non_exhaustive]
107    #[derive(PartialEq, Eq, Copy, Clone)]
108    pub struct Map<K, V> {
109        _key_phantom: PhantomData<K>,
110        _val_phantom: PhantomData<V>,
111    }
112
113    /// a mathematical (unbounded) integer type
114    /// it should not be constructed from running rust code, hence the private unit inside
115    pub struct Int(());
116
117    #[non_exhaustive]
118    #[derive(PartialEq, Eq, Copy, Clone)]
119    pub struct Ghost<T> {
120        _phantom: PhantomData<T>,
121    }
122}
123
124#[cfg(feature = "prusti")]
125pub mod core_spec;
126
127#[cfg(feature = "prusti")]
128mod private {
129    use core::{marker::PhantomData, ops::*};
130
131    /// A macro for defining a closure with a specification.
132    pub use prusti_contracts_proc_macros::{closure, pure, trusted};
133
134    pub fn prusti_set_union_active_field<T>(_arg: T) {
135        unreachable!();
136    }
137
138    #[pure]
139    pub fn prusti_terminates_trusted() -> Int {
140        Int::new(1)
141    }
142
143    /// a mathematical (unbounded) integer type
144    /// it should not be constructed from running rust code, hence the private unit inside
145    #[derive(Copy, Clone, PartialEq, Eq)]
146    pub struct Int(());
147
148    impl Int {
149        pub fn new(_: i64) -> Self {
150            panic!()
151        }
152
153        pub fn new_usize(_: usize) -> Self {
154            panic!()
155        }
156    }
157
158    macro_rules! __int_dummy_trait_impls__ {
159        ($($trait:ident $fun:ident),*) => {$(
160            impl core::ops::$trait for Int {
161                type Output = Self;
162                fn $fun(self, _other: Self) -> Self {
163                    panic!()
164                }
165            }
166        )*}
167    }
168
169    __int_dummy_trait_impls__!(Add add, Sub sub, Mul mul, Div div, Rem rem);
170
171    #[macro_export]
172    macro_rules! prusti_assert_eq {
173        ($left:expr, $right:expr $(,)?) => {
174            $crate::prusti_assert!($crate::snapshot_equality($left, $right))
175        };
176    }
177
178    #[macro_export]
179    macro_rules! prusti_assert_ne {
180        ($left:expr, $right:expr $(,)?) => {
181            $crate::prusti_assert!(!$crate::snapshot_equality($left, $right))
182        };
183    }
184
185    impl Neg for Int {
186        type Output = Self;
187        fn neg(self) -> Self {
188            panic!()
189        }
190    }
191
192    impl PartialOrd for Int {
193        fn partial_cmp(&self, _other: &Self) -> Option<core::cmp::Ordering> {
194            panic!()
195        }
196    }
197    impl Ord for Int {
198        fn cmp(&self, _other: &Self) -> core::cmp::Ordering {
199            panic!()
200        }
201    }
202
203    /// A sequence type
204    #[non_exhaustive]
205    #[derive(PartialEq, Eq, Copy, Clone)]
206    pub struct Seq<T: Copy> {
207        _phantom: PhantomData<T>,
208    }
209
210    impl<T: Copy> Seq<T> {
211        pub fn empty() -> Self {
212            panic!()
213        }
214        pub fn single(_: T) -> Self {
215            panic!()
216        }
217        pub fn concat(self, _: Self) -> Self {
218            panic!()
219        }
220        pub fn lookup(self, _index: usize) -> T {
221            panic!()
222        }
223        pub fn len(self) -> Int {
224            panic!()
225        }
226    }
227
228    #[macro_export]
229    macro_rules! seq {
230        ($val:expr) => {
231            $crate::Seq::single($val)
232        };
233        ($($val:expr),*) => {
234            $crate::Seq::empty()
235            $(
236                .concat(seq![$val])
237            )*
238        };
239    }
240
241    impl<T: Copy> Index<usize> for Seq<T> {
242        type Output = T;
243        fn index(&self, _: usize) -> &T {
244            panic!()
245        }
246    }
247
248    impl<T: Copy> Index<Int> for Seq<T> {
249        type Output = T;
250        fn index(&self, _: Int) -> &T {
251            panic!()
252        }
253    }
254
255    /// A map type
256    #[non_exhaustive]
257    #[derive(PartialEq, Eq, Copy, Clone)]
258    pub struct Map<K, V> {
259        _key_phantom: PhantomData<K>,
260        _val_phantom: PhantomData<V>,
261    }
262
263    impl<K, V> Map<K, V> {
264        pub fn empty() -> Self {
265            panic!()
266        }
267        pub fn insert(self, _key: K, _val: V) -> Self {
268            panic!()
269        }
270        pub fn delete(self, _key: K) -> Self {
271            panic!()
272        }
273        pub fn len(self) -> Int {
274            panic!()
275        }
276        pub fn lookup(self, _key: K) -> V {
277            panic!()
278        }
279        pub fn contains(self, _key: K) -> bool {
280            panic!()
281        }
282    }
283
284    #[macro_export]
285    macro_rules! map {
286        ($($key:expr => $val:expr),*) => {
287            map!($crate::Map::empty(), $($key => $val),*)
288        };
289        ($existing_map:expr, $($key:expr => $val:expr),*) => {
290            $existing_map
291            $(
292                .insert($key, $val)
293            )*
294        };
295    }
296
297    impl<K, V> core::ops::Index<K> for Map<K, V> {
298        type Output = V;
299        fn index(&self, _key: K) -> &V {
300            panic!()
301        }
302    }
303
304    #[non_exhaustive]
305    #[derive(PartialEq, Eq, Copy, Clone)]
306    pub struct Ghost<T> {
307        _phantom: PhantomData<T>,
308    }
309
310    impl<T> Ghost<T> {
311        pub fn new(_: T) -> Self {
312            panic!()
313        }
314    }
315
316    impl<T> Deref for Ghost<T> {
317        type Target = T;
318        fn deref(&self) -> &T {
319            panic!()
320        }
321    }
322
323    impl<T> DerefMut for Ghost<T> {
324        fn deref_mut(&mut self) -> &mut T {
325            panic!()
326        }
327    }
328}
329
330/// This function is used to evaluate an expression in the context just
331/// before the borrows expires.
332pub fn before_expiry<T>(arg: T) -> T {
333    arg
334}
335
336/// This function is used to evaluate an expression in the “old”
337/// context, that is at the beginning of the method call.
338pub fn old<T>(arg: T) -> T {
339    arg
340}
341
342/// Universal quantifier.
343///
344/// This is a Prusti-internal representation of the `forall` syntax.
345pub fn forall<T, F>(_trigger_set: T, _closure: F) -> bool {
346    true
347}
348
349/// Existential quantifier.
350///
351/// This is a Prusti-internal representation of the `exists` syntax.
352pub fn exists<T, F>(_trigger_set: T, _closure: F) -> bool {
353    true
354}
355
356/// Creates an owned copy of a reference. This should only be used from within
357/// ghost code, as it circumvents the borrow checker.
358pub fn snap<T>(_x: &T) -> T {
359    unimplemented!()
360}
361
362/// Snapshot, "logical", or "mathematical" equality. Compares the in-memory
363/// representation of two instances of the same type, even if there is no
364/// `PartialEq` nor `Copy` implementation. The in-memory representation is
365/// constructed recursively: references are followed, unsafe pointers and cells
366/// are not. Importantly, addresses are not taken into consideration.
367pub fn snapshot_equality<T>(_l: T, _r: T) -> bool {
368    true
369}
370
371pub use private::*;
prusti_contracts/lib.rs

prusti_contracts/
lib.rs
