vstd_extra/
ownership.rs

1use vstd::atomic::*;
2use vstd::cell;
3use vstd::prelude::*;
4
5use core::marker::PhantomData;
6use core::ops::Range;
7
8verus! {
9
10pub trait Inv {
11    spec fn inv(self) -> bool;
12}
13
14impl<T: Inv> Inv for Option<T> {
15    open spec fn inv(self) -> bool {
16        match self {
17            Some(t) => t.inv(),
18            None => true,
19        }
20    }
21}
22
23pub trait InvView: Inv + View where <Self as View>::V: Inv {
24    proof fn view_preserves_inv(self)
25        requires
26            self.inv(),
27        ensures
28            self.view().inv(),
29    ;
30}
31
32pub trait OwnerOf where <<Self as OwnerOf>::Owner as View>::V: Inv {
33    /// The owner of the concrete type.
34    /// The Owner must implement `Inv`, indicating that it must
35    /// has a consistent state.
36    type Owner: InvView + Sized;
37
38    spec fn wf(self, owner: Self::Owner) -> bool
39        recommends
40            owner.inv(),
41    ;
42}
43
44pub trait ModelOf: OwnerOf + Sized {
45    open spec fn model(self, owner: Self::Owner) -> <Self::Owner as View>::V
46        recommends
47            self.wf(owner),
48    {
49        owner.view()
50    }
51}
52
53} // verus!
vstd_extra/ownership.rs

vstd_extra/
ownership.rs
