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    // Meta-cell read: borrows only the metadata `M` view of a slot's storage
34    // cell (analogous to `unsafe { ptr.as_ref() }.field` in ../vostd). Requires
35    // `Metadata` to be in scope at the call site. MUST come before the generic
36    // `$perm:expr` arm — otherwise the latter matches greedily, treating
37    // `Meta(perm)` as a function-call expression.
38    ($ptr:expr => $field:tt, Meta($perm:expr)) => {
39        verus_exec_expr!($ptr.borrow(Tracked($perm)).metadata.$field)
40    };
41    ($ptr:expr => $field:tt, $perm:expr) => {
42        verus_exec_expr!($ptr.borrow(Tracked($perm)).$field)
43    };
44    ($ptr:expr => $field1:tt . $field2:tt, $perm:expr) => {
45        verus_exec_expr!($ptr.borrow(Tracked($perm)).$field1.$field2)
46    };
47}
48
49#[macro_export]
50macro_rules! update_field {
51    ($ptr:expr => $field:tt <- $val:expr; $set:expr , $idx:expr) => {
52        verus_exec_expr!(
53        {
54            let tracked mut __own = $set.tracked_remove($idx);
55            let mut __tmp = $ptr.take(Tracked(&mut __own));
56            __tmp.$field = $val;
57            $ptr.put(Tracked(&mut __own), __tmp);
58            proof { $set.tracked_insert($idx, __own); }
59        })
60    };
61    ($ptr:expr => $field1:tt . $field2:tt <- $val:expr; $set:expr , $idx:expr) => {
62        verus_exec_expr!(
63        {
64            let tracked mut __own = $set.tracked_remove($idx);
65            let mut __tmp = $ptr.take(Tracked(&mut __own));
66            __tmp.$field1.$field2 = $val;
67            $ptr.put(Tracked(&mut __own), __tmp);
68            proof { $set.tracked_insert($idx, __own); }
69        })
70    };
71    ($ptr:expr => $field:tt <- $val:expr; $set:expr , $idx:expr, inner) => {
72        verus_exec_expr!(
73        {
74            let tracked mut __own = $set.tracked_remove($idx);
75            let mut __tmp = $ptr.take(Tracked(&mut __own));
76            __tmp.$field = $val;
77            $ptr.put(Tracked(&mut __own.points_to), __tmp);
78            proof { $set.tracked_insert($idx, __own); }
79        })
80    };
81    ($ptr:expr => $field1:tt . $field2:tt <- $val:expr; $set:expr , $idx:expr, inner) => {
82        verus_exec_expr!(
83        {
84            let tracked mut __own = $set.tracked_remove($idx);
85            let mut __tmp = $ptr.take(Tracked(&mut __own));
86            __tmp.$field1.$field2 = $val;
87            $ptr.put(Tracked(&mut __own.points_to), __tmp);
88            proof { $set.tracked_insert($idx, __own); }
89        })
90    };
91    ($ptr:expr => $field:tt <- $val:expr; $perm:expr) => {
92        verus_exec_expr!(
93        {
94            let mut __tmp = $ptr.take(Tracked(&mut $perm));
95            __tmp.$field = $val;
96            $ptr.put(Tracked(&mut $perm), __tmp);
97        })
98    };
99    ($ptr:expr => $field1:tt . $field2:tt <- $val:expr; $perm:expr) => {
100        verus_exec_expr!(
101        {
102            let mut __tmp = $ptr.take(Tracked(&mut $perm));
103            __tmp.$field1.$field2 = $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    ($ptr:expr => $field:tt -= $val:expr; $perm:expr) => {
116        verus_exec_expr!(
117        {
118            let mut __tmp = $ptr.take(Tracked(&mut $perm));
119            __tmp.$field = __tmp.$field - $val;
120            $ptr.put(Tracked(&mut $perm), __tmp);
121        })
122    };
123    // Meta-cell write: mutates a single field of the metadata `M` via a
124    // surgical view on the storage cell, leaving ref_count/in_list/vtable_ptr
125    // perms untouched (analogous to `unsafe { ptr.as_mut() }.field = val` in
126    // ../vostd, but verified). Requires `Metadata` to be in scope.
127    ($ptr:expr => $field:tt <- $val:expr, Meta($perm:expr)) => {
128        verus_exec_expr!(
129        {
130            let __link = $ptr.borrow_mut(Tracked($perm));
131            let __contents = &mut __link.metadata;
132            __contents.$field = $val;
133        })
134    };
135}
136
137pub use crate::{assert, borrow_field, update_field};
vstd_extra/trans_macros.rs

vstd_extra/
trans_macros.rs
