vstd_extra/resource/storage_protocol/
excl.rs

1//! Exclusive storage protocol resource algebra.
2use vstd::modes::tracked_swap;
3use vstd::prelude::*;
4use vstd::resource::Loc;
5use vstd::resource::exclusive::ExclusiveRA;
6use vstd::resource::storage_protocol::*;
7
8verus! {
9
10pub ghost enum ExclusiveSP<A> {
11    Unit,
12    /// Exclusive ownership of a value.
13    Exclusive(Option<A>),
14    /// Invalid state.
15    Invalid,
16}
17
18impl<A> Protocol<(), A> for ExclusiveSP<A> {
19    open spec fn op(self, other: Self) -> Self {
20        match (self, other) {
21            (ExclusiveSP::Unit, x) => x,
22            (x, ExclusiveSP::Unit) => x,
23            _ => ExclusiveSP::Invalid,
24        }
25    }
26
27    open spec fn rel(self, s: Map<(), A>) -> bool {
28        match self {
29            ExclusiveSP::Unit => s.is_empty(),
30            ExclusiveSP::Exclusive(None) => s.is_empty(),
31            ExclusiveSP::Exclusive(Some(x)) => s =~= map![() => x],
32            ExclusiveSP::Invalid => false,
33        }
34    }
35
36    open spec fn unit() -> Self {
37        ExclusiveSP::Unit
38    }
39
40    proof fn commutative(a: Self, b: Self) {
41    }
42
43    proof fn associative(a: Self, b: Self, c: Self) {
44    }
45
46    proof fn op_unit(a: Self) {
47    }
48}
49
50impl<A> ExclusiveSP<A> {
51    pub open spec fn value(self) -> A {
52        match self {
53            ExclusiveSP::Exclusive(Some(x)) => x,
54            _ => arbitrary(),
55        }
56    }
57
58    pub proof fn lemma_deposits(self, value: A)
59        requires
60            self is Exclusive,
61            self->Exclusive_0 is None,
62        ensures
63            deposits(self, map![() => value], ExclusiveSP::Exclusive(Some(value))),
64    {
65        let m = map![() => value];
66        assert forall|q: Self, s: Map<(), A>|
67            #![auto]
68            Self::rel(Self::op(self, q), s) implies exists|s1: Map<(), A>|
69            #![auto]
70            Self::rel(Self::op(ExclusiveSP::Exclusive(Some(value)), q), s1) && s.dom().disjoint(
71                m.dom(),
72            ) && s.union_prefer_right(m) == s1 by {
73            assert(s == Map::<(), A>::empty());
74            assert(Self::rel(Self::op(ExclusiveSP::Exclusive(Some(value)), q), m));
75            assert(s.dom().disjoint(m.dom()));
76            assert(s.union_prefer_right(m) == m);
77        }
78    }
79}
80
81/// `Exclusive` is a token that stores a tracked object of type `T` and ensures its exclusive ownership.
82/// No two `Exclusive` tokens can have the same id.
83/// The owned tracked object can be borrowed, updated, taken out and put back.
84pub tracked struct Exclusive<T> {
85    tracked r: StorageResource<(), T, ExclusiveSP<T>>,
86}
87
88impl<T> Exclusive<T> {
89    /// Returns the unique identifier.
90    pub closed spec fn id(self) -> Loc {
91        self.r.loc()
92    }
93
94    /// Returns the underlying `ExclP<T>` protocol monoid.
95    pub closed spec fn protocol_monoid(self) -> ExclusiveSP<T> {
96        self.r.value()
97    }
98
99    /// Returns the owned resource.
100    pub open spec fn resource(self) -> T {
101        self.protocol_monoid().value()
102    }
103
104    /// Type invariant.
105    pub open spec fn wf(self) -> bool {
106        self.protocol_monoid() is Exclusive
107    }
108
109    /// Wether the token stores a resource.
110    pub open spec fn has_resource(self) -> bool {
111        self.protocol_monoid()->Exclusive_0 is Some
112    }
113
114    /// Wether the token does not store any resource.
115    pub open spec fn has_no_resource(self) -> bool {
116        self.protocol_monoid()->Exclusive_0 is None
117    }
118
119    #[verifier::type_invariant]
120    closed spec fn type_inv(self) -> bool {
121        self.wf()
122    }
123
124    closed spec fn type_inv_inner(r: ExclusiveSP<T>) -> bool {
125        r is Exclusive
126    }
127
128    /// The existence of two `Exclusive` tokens ensures that they do not have the same id.
129    pub proof fn validate_with_other(tracked &mut self, tracked other: &Self)
130        ensures
131            *old(self) == *final(self),
132            final(self).wf(),
133            final(self).id() != other.id(),
134    {
135        use_type_invariant(&*self);
136        use_type_invariant(other);
137        if self.id() == other.id() {
138            self.r.validate_with_shared(&other.r);
139        }
140    }
141
142    /// Borrows the owned resource.
143    pub proof fn tracked_borrow(tracked &self) -> (tracked res: &T)
144        requires
145            self.has_resource(),
146        ensures
147            *res == self.resource(),
148    {
149        use_type_invariant(&*self);
150        StorageResource::guard(&self.r, map![() => self.resource()]).tracked_borrow(())
151    }
152
153    /// Takes out the owned resource.
154    pub proof fn take_resource(tracked &mut self) -> (tracked res: T)
155        requires
156            old(self).has_resource(),
157        ensures
158            final(self).has_no_resource(),
159            res == old(self).resource(),
160            final(self).wf(),
161    {
162        use_type_invariant(&*self);
163        Self::take_resource_helper(&mut self.r)
164    }
165
166    proof fn take_resource_helper(
167        tracked r: &mut StorageResource<(), T, ExclusiveSP<T>>,
168    ) -> (tracked res: T)
169        requires
170            Self::type_inv_inner(old(r).value()),
171            old(r).value()->Exclusive_0 is Some,
172        ensures
173            Self::type_inv_inner(final(r).value()),
174            final(r).value()->Exclusive_0 is None,
175            final(r).loc() == old(r).loc(),
176            res == old(r).value()->Exclusive_0->0,
177    {
178        let tracked mut tmp = StorageResource::<(), T, ExclusiveSP<T>>::alloc(
179            ExclusiveSP::Unit,
180            Map::tracked_empty(),
181        );
182        tracked_swap(r, &mut tmp);
183        let tracked (mut r1, mut r2) = tmp.withdraw(
184            ExclusiveSP::Exclusive(None),
185            map![()=> tmp.value().value()],
186        );
187        tracked_swap(r, &mut r1);
188        r2.tracked_remove(())
189    }
190
191    /// Puts back the owned resource.
192    pub proof fn put_resource(tracked &mut self, tracked value: T)
193        requires
194            old(self).has_no_resource(),
195        ensures
196            final(self).has_resource(),
197            final(self).resource() == value,
198            final(self).wf(),
199    {
200        use_type_invariant(&*self);
201        Self::put_resource_helper(&mut self.r, value)
202    }
203
204    proof fn put_resource_helper(
205        tracked r: &mut StorageResource<(), T, ExclusiveSP<T>>,
206        tracked value: T,
207    )
208        requires
209            Self::type_inv_inner(old(r).value()),
210            old(r).value()->Exclusive_0 is None,
211        ensures
212            Self::type_inv_inner(final(r).value()),
213            final(r).value()->Exclusive_0 is Some,
214            final(r).loc() == old(r).loc(),
215            final(r).value()->Exclusive_0->0 == value,
216    {
217        let ghost g = value;
218        let tracked mut tmp = StorageResource::<(), T, ExclusiveSP<T>>::alloc(
219            ExclusiveSP::Unit,
220            Map::tracked_empty(),
221        );
222        tracked_swap(r, &mut tmp);
223        let tracked mut m = Map::tracked_empty();
224        m.tracked_insert((), value);
225        tmp.value().lemma_deposits(g);
226        let tracked mut r1 = tmp.deposit(m, ExclusiveSP::Exclusive(Some(g)));
227        tracked_swap(r, &mut r1);
228    }
229
230    /// Updates the owned resource and returns the old resource if it exists.
231    pub proof fn update(tracked &mut self, tracked value: T) -> (tracked res: Option<T>)
232        ensures
233            final(self).has_resource(),
234            final(self).resource() == value,
235            res == if old(self).has_resource() {
236                Some(old(self).resource())
237            } else {
238                None
239            },
240            final(self).wf(),
241    {
242        use_type_invariant(&*self);
243        let tracked mut res = None;
244        if self.has_resource() {
245            res = Some(self.take_resource());
246        }
247        self.put_resource(value);
248        res
249    }
250}
251
252} // verus!
vstd_extra/resource/storage_protocol/excl.rs

vstd_extra/resource/storage_protocol/
excl.rs
