vstd_extra/
ownership.rs

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

vstd_extra/
ownership.rs
