vstd_extra/
trans_macros.rs

1use vstd::prelude::*;
2
3use crate::panic::*;
4
5#[macro_export]
6macro_rules! assert {
7    ($cond:expr) => {
8        if !($cond) {
9            $crate::panic::panic_diverge()
10        }
11    };
12    ($cond:expr, $msg:literal) => {
13        if !($cond) {
14            $crate::panic::panic_diverge()
15        }
16    };
17}
18
19#[macro_export]
20macro_rules! assert_eq {
21    ($l:expr, $r:expr) => {
22        if ($l != $r) {
23            $crate::panic::panic_diverge()
24        }
25    };
26}
27
28#[macro_export]
29macro_rules! borrow_field {
30    ($ptr:expr) => {
31        $ptr
32    };
33    ($ptr:expr => $field:tt, $perm:expr) => {
34        verus_exec_expr!($ptr.borrow(Tracked($perm)).$field)
35    };
36    ($ptr:expr => $field1:tt . $field2:tt, $perm:expr) => {
37        verus_exec_expr!($ptr.borrow(Tracked($perm)).$field1.$field2)
38    };
39}
40
41#[macro_export]
42macro_rules! update_field {
43    ($ptr:expr => $field:tt <- $val:expr; $set:expr , $idx:expr) => {
44        verus_exec_expr!(
45        {
46            let tracked mut __own = $set.tracked_remove($idx);
47            let mut __tmp = $ptr.take(Tracked(&mut __own));
48            __tmp.$field = $val;
49            $ptr.put(Tracked(&mut __own), __tmp);
50            proof { $set.tracked_insert($idx, __own); }
51        })
52    };
53    ($ptr:expr => $field1:tt . $field2:tt <- $val:expr; $set:expr , $idx:expr) => {
54        verus_exec_expr!(
55        {
56            let tracked mut __own = $set.tracked_remove($idx);
57            let mut __tmp = $ptr.take(Tracked(&mut __own));
58            __tmp.$field1.$field2 = $val;
59            $ptr.put(Tracked(&mut __own), __tmp);
60            proof { $set.tracked_insert($idx, __own); }
61        })
62    };
63    ($ptr:expr => $field:tt <- $val:expr; $set:expr , $idx:expr, inner) => {
64        verus_exec_expr!(
65        {
66            let tracked mut __own = $set.tracked_remove($idx);
67            let mut __tmp = $ptr.take(Tracked(&mut __own));
68            __tmp.$field = $val;
69            $ptr.put(Tracked(&mut __own.points_to), __tmp);
70            proof { $set.tracked_insert($idx, __own); }
71        })
72    };
73    ($ptr:expr => $field1:tt . $field2:tt <- $val:expr; $set:expr , $idx:expr, inner) => {
74        verus_exec_expr!(
75        {
76            let tracked mut __own = $set.tracked_remove($idx);
77            let mut __tmp = $ptr.take(Tracked(&mut __own));
78            __tmp.$field1.$field2 = $val;
79            $ptr.put(Tracked(&mut __own.points_to), __tmp);
80            proof { $set.tracked_insert($idx, __own); }
81        })
82    };
83    ($ptr:expr => $field:tt <- $val:expr; $perm:expr) => {
84        verus_exec_expr!(
85        {
86            let mut __tmp = $ptr.take(Tracked(&mut $perm));
87            __tmp.$field = $val;
88            $ptr.put(Tracked(&mut $perm), __tmp);
89        })
90    };
91    ($ptr:expr => $field1:tt . $field2:tt <- $val:expr; $perm:expr) => {
92        verus_exec_expr!(
93        {
94            let mut __tmp = $ptr.take(Tracked(&mut $perm));
95            __tmp.$field1.$field2 = $val;
96            $ptr.put(Tracked(&mut $perm), __tmp);
97        })
98    };
99    ($ptr:expr => $field:tt += $val:expr; $perm:expr) => {
100        verus_exec_expr!(
101        {
102            let mut __tmp = $ptr.take(Tracked(&mut $perm));
103            __tmp.$field = __tmp.$field + $val;
104            $ptr.put(Tracked(&mut $perm), __tmp);
105        })
106    };
107    ($ptr:expr => $field:tt -= $val:expr; $perm:expr) => {
108        verus_exec_expr!(
109        {
110            let mut __tmp = $ptr.take(Tracked(&mut $perm));
111            __tmp.$field = __tmp.$field - $val;
112            $ptr.put(Tracked(&mut $perm), __tmp);
113        })
114    }
115}
116
117pub use crate::{assert, borrow_field, update_field};
vstd_extra/trans_macros.rs

vstd_extra/
trans_macros.rs
