vstd_extra/
trans_macros.rs

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

vstd_extra/
trans_macros.rs
