vstd_extra/resource/storage_protocol/
excl.rs

1//! Exclusive storage protocol resource algebra.
2use vstd::pcm::Loc;
3use vstd::prelude::*;
4use vstd::storage_protocol::*;
5
6verus! {
7
8pub ghost enum ExclP<A> {
9    Unit,
10    /// Exclusive ownership of a value.
11    Excl(Option<A>),
12    /// Invalid state.
13    ExclInvalid,
14}
15
16impl<A> Protocol<(), A> for ExclP<A> {
17    open spec fn op(self, other: Self) -> Self {
18        match (self, other) {
19            (ExclP::Unit, x) => x,
20            (x, ExclP::Unit) => x,
21            _ => ExclP::ExclInvalid,
22        }
23    }
24
25    open spec fn rel(self, s: Map<(), A>) -> bool {
26        match self {
27            ExclP::Unit => s.is_empty(),
28            ExclP::Excl(None) => s.is_empty(),
29            ExclP::Excl(Some(x)) => s =~= map![() => x],
30            ExclP::ExclInvalid => false,
31        }
32    }
33
34    open spec fn unit() -> Self {
35        ExclP::Unit
36    }
37
38    proof fn commutative(a: Self, b: Self) {
39    }
40
41    proof fn associative(a: Self, b: Self, c: Self) {
42    }
43
44    proof fn op_unit(a: Self) {
45    }
46}
47
48impl<A> ExclP<A> {
49    pub open spec fn value(self) -> A {
50        match self {
51            ExclP::Excl(Some(x)) => x,
52            _ => arbitrary(),
53        }
54    }
55
56    pub proof fn lemma_deposits(self, value: A)
57        requires
58            self is Excl,
59            self->Excl_0 is None,
60        ensures
61            deposits(self, map![() => value], ExclP::Excl(Some(value))),
62    {
63        let m = map![() => value];
64        assert forall|q: Self, s: Map<(), A>|
65            #![auto]
66            Self::rel(Self::op(self, q), s) implies exists|s1: Map<(), A>|
67            #![auto]
68            Self::rel(Self::op(ExclP::Excl(Some(value)), q), s1) && s.dom().disjoint(m.dom())
69                && &&s.union_prefer_right(m) == s1 by {
70            assert(s == Map::<(), A>::empty());
71            assert(Self::rel(Self::op(ExclP::Excl(Some(value)), q), m));
72            assert(s.dom().disjoint(m.dom()));
73            assert(s.union_prefer_right(m) == m);
74        }
75    }
76}
77
78} // verus!
vstd_extra/resource/storage_protocol/excl.rs

vstd_extra/resource/storage_protocol/
excl.rs
