vstd_extra/resource/storage_protocol/
csum.rs

1//! Sum-type storage protocol.
2use core::panic;
3
4use crate::sum::*;
5use vstd::math::add;
6use vstd::pcm::Loc;
7use vstd::pervasive::arbitrary;
8use vstd::prelude::*;
9use vstd::prelude::*;
10use vstd::storage_protocol::*;
11
12verus! {
13
14/// A sum-type protocol monoid that stores a tracked object of either type A or type B.
15///
16/// The knowledge of the existence of a specific type of resource can be shared up to TOTAL pieces,
17/// but only one piece has the exclusive ownership of the resource,
18/// allowing arbitrary withdrawing, depositing, or updating.
19pub ghost enum CsumP<A, B, const TOTAL: u64> {
20    /// The unit element, only for technical reasons, not intended to be used directly.
21    Unit,
22    /// The left side of the sum, with an optional resource, a fraction, and a boolean indicating whether it is the exclusive owner of the resource.
23    Cinl(Option<A>, int, bool),
24    /// The right side of the sum, with an optional resource, a fraction, and a boolean indicating whether it is the exclusive owner of the resource.
25    Cinr(Option<B>, int, bool),
26    /// An invalid state, used to represent an invalid combination of resources.
27    CsumInvalid,
28}
29
30impl<A, B, const TOTAL: u64> Protocol<(), Sum<A, B>> for CsumP<A, B, TOTAL> {
31    open spec fn op(self, other: Self) -> Self {
32        match (self, other) {
33            (CsumP::Unit, x) => x,
34            (x, CsumP::Unit) => x,
35            (CsumP::Cinl(ov1, n1, b1), CsumP::Cinl(ov2, n2, b2)) => {
36                if !self.is_valid() || !other.is_valid() || n1 + n2 > TOTAL || b1 && b2
37                    || ov1 is Some && ov2 is Some {
38                    CsumP::CsumInvalid
39                } else {
40                    CsumP::Cinl(
41                        if ov1 is Some {
42                            ov1
43                        } else {
44                            ov2
45                        },
46                        n1 + n2,
47                        b1 || b2,
48                    )
49                }
50            },
51            (CsumP::Cinr(ov1, n1, b1), CsumP::Cinr(ov2, n2, b2)) => {
52                if !self.is_valid() || !other.is_valid() || n1 + n2 > TOTAL || b1 && b2
53                    || ov1 is Some && ov2 is Some {
54                    CsumP::CsumInvalid
55                } else {
56                    CsumP::Cinr(
57                        if ov1 is Some {
58                            ov1
59                        } else {
60                            ov2
61                        },
62                        n1 + n2,
63                        b1 || b2,
64                    )
65                }
66            },
67            _ => CsumP::CsumInvalid,
68        }
69    }
70
71    open spec fn rel(self, s: Map<(), Sum<A, B>>) -> bool {
72        match self {
73            CsumP::Unit => s.is_empty(),
74            CsumP::Cinl(None, n, true) => 0 <= n <= TOTAL && s.is_empty(),
75            CsumP::Cinl(Some(a), n, true) => 0 <= n <= TOTAL && s.contains_key(()) && s[()]
76                == Sum::<A, B>::Left(a),
77            CsumP::Cinr(None, n, true) => 0 <= n <= TOTAL && s.is_empty(),
78            CsumP::Cinr(Some(b), n, true) => 0 <= n <= TOTAL && s.contains_key(()) && s[()]
79                == Sum::<A, B>::Right(b),
80            _ => false,
81        }
82    }
83
84    open spec fn unit() -> Self {
85        CsumP::Unit
86    }
87
88    proof fn commutative(a: Self, b: Self) {
89    }
90
91    proof fn associative(a: Self, b: Self, c: Self) {
92    }
93
94    proof fn op_unit(a: Self) {
95    }
96}
97
98impl<A, B, const TOTAL: u64> CsumP<A, B, TOTAL> {
99    /// Whether the protocol monoid is currently in the left state.
100    pub open spec fn is_left(self) -> bool {
101        self is Cinl
102    }
103
104    /// Whether the protocol monoid is currently in the right state.
105    pub open spec fn is_right(self) -> bool {
106        self is Cinr
107    }
108
109    /// Whether the protocol monoid is an exclusive owner of a resource.
110    pub open spec fn is_resource_owner(self) -> bool {
111        match self {
112            CsumP::Cinl(_, _, b) | CsumP::Cinr(_, _, b) => b,
113            _ => false,
114        }
115    }
116
117    /// Whether the protocol monoid currently owns a resource, only meaningful when it is the exclusive owner.
118    pub open spec fn has_resource(self) -> bool {
119        match self {
120            CsumP::Cinl(ov, n, true) => ov is Some,
121            CsumP::Cinr(ov, n, true) => ov is Some,
122            _ => false,
123        }
124    }
125
126    /// Whether the protocol monoid has had its resource taken, only meaningful when it is the exclusive owner.
127    pub open spec fn has_no_resource(self) -> bool {
128        match self {
129            CsumP::Cinl(ov, n, true) => ov is None,
130            CsumP::Cinr(ov, n, true) => ov is None,
131            _ => false,
132        }
133    }
134
135    /// The resource stored in the protocol monoid.
136    pub open spec fn resource(self) -> Sum<A, B> {
137        match self {
138            CsumP::Cinl(Some(a), n, true) => Sum::Left(a),
139            CsumP::Cinr(Some(b), n, true) => Sum::Right(b),
140            _ => arbitrary(),
141        }
142    }
143
144    /// The fraction of the resource knowledge.
145    pub open spec fn frac(self) -> int {
146        match self {
147            CsumP::Cinl(_, n, _) | CsumP::Cinr(_, n, _) => n,
148            _ => 1,
149        }
150    }
151
152    /// The invariant of the protocol monoid.
153    pub open spec fn is_valid(self) -> bool {
154        match self {
155            CsumP::Unit => true,
156            CsumP::Cinl(ov, n, b) => 0 < n <= TOTAL && (ov is Some ==> b),
157            CsumP::Cinr(ov, n, b) => 0 < n <= TOTAL && (ov is Some ==> b),
158            _ => false,
159        }
160    }
161
162    pub proof fn lemma_withdraws_left(self)
163        requires
164            self.is_left(),
165            self.is_resource_owner(),
166            self.has_resource(),
167            self.is_valid(),
168        ensures
169            withdraws(self, CsumP::Cinl(None, self.frac(), true), map![()=>self.resource()]),
170    {
171        match self {
172            CsumP::Cinl(Some(a), n, true) => {
173                let resource = Sum::<A, B>::Left(a);
174                let resource_map = map![() => resource];
175                let new_protocol_monoid = CsumP::<A, B, TOTAL>::Cinl(None, n, true);
176                assert forall|q: Self, t1: Map<(), Sum<A, B>>|
177                    #![auto]
178                    CsumP::rel(CsumP::op(self, q), t1) implies exists|t2: Map<(), Sum<A, B>>|
179                    #![auto]
180                    CsumP::rel(CsumP::op(new_protocol_monoid, q), t2) && t2.dom().disjoint(
181                        resource_map.dom(),
182                    ) && t1 =~= t2.union_prefer_right(resource_map) by {
183                    let t2 = Map::empty();
184                    assert(CsumP::rel(CsumP::op(new_protocol_monoid, q), t2));
185                    assert(t2.dom().disjoint(resource_map.dom()));
186                    assert(t1 =~= t2.union_prefer_right(resource_map));
187                }
188            },
189            _ => {
190                assert(false);
191            },
192        }
193    }
194
195    pub proof fn lemma_withdraws_right(self)
196        requires
197            self.is_resource_owner(),
198            self.is_right(),
199            self.has_resource(),
200            self.is_valid(),
201        ensures
202            withdraws(self, CsumP::Cinr(None, self.frac(), true), map![()=>self.resource()]),
203    {
204        match self {
205            CsumP::Cinr(Some(b), n, true) => {
206                let resource = Sum::<A, B>::Right(b);
207                let resource_map = map![() => resource];
208                let new_protocol_monoid = CsumP::<A, B, TOTAL>::Cinr(None, n, true);
209                assert forall|q: Self, t1: Map<(), Sum<A, B>>|
210                    #![auto]
211                    CsumP::rel(CsumP::op(self, q), t1) implies exists|t2: Map<(), Sum<A, B>>|
212                    #![auto]
213                    CsumP::rel(CsumP::op(new_protocol_monoid, q), t2) && t2.dom().disjoint(
214                        resource_map.dom(),
215                    ) && t1 =~= t2.union_prefer_right(resource_map) by {
216                    let t2 = Map::empty();
217                    assert(CsumP::rel(CsumP::op(new_protocol_monoid, q), t2));
218                    assert(t2.dom().disjoint(resource_map.dom()));
219                    assert(t1 =~= t2.union_prefer_right(resource_map));
220                }
221            },
222            _ => {
223                assert(false);
224            },
225        }
226    }
227
228    pub proof fn lemma_deposit_left(self, a: A)
229        requires
230            self.is_resource_owner(),
231            self.is_left(),
232            self.has_no_resource(),
233            self.is_valid(),
234        ensures
235            deposits(self, map![()=>Sum::Left(a)], CsumP::Cinl(Some(a), self.frac(), true)),
236    {
237        let resource_map = map![()=>Sum::Left(a)];
238        let empty_map: Map<(), Sum<A, B>> = Map::empty();
239        let new_protocol_monoid = CsumP::<A, B, TOTAL>::Cinl(Some(a), self.frac(), true);
240        assert forall|q: Self, t1: Map<(), Sum<A, B>>|
241            CsumP::rel(CsumP::op(self, q), t1) implies exists|t2: Map<(), Sum<A, B>>|
242            {
243                #[trigger] CsumP::rel(CsumP::op(new_protocol_monoid, q), t2) && t1.dom().disjoint(
244                    resource_map.dom(),
245                ) && t1.union_prefer_right(resource_map) == t2
246            } by {
247            assert(CsumP::rel(CsumP::op(new_protocol_monoid, q), resource_map));
248        }
249    }
250
251    pub proof fn lemma_deposit_right(self, b: B)
252        requires
253            self.is_resource_owner(),
254            self.is_right(),
255            self.has_no_resource(),
256            self.is_valid(),
257        ensures
258            deposits(self, map![()=>Sum::Right(b)], CsumP::Cinr(Some(b), self.frac(), true)),
259    {
260        let resource_map = map![()=>Sum::Right(b)];
261        let empty_map: Map<(), Sum<A, B>> = Map::empty();
262        let new_protocol_monoid = CsumP::<A, B, TOTAL>::Cinr(Some(b), self.frac(), true);
263        assert forall|q: Self, t1: Map<(), Sum<A, B>>|
264            CsumP::rel(CsumP::op(self, q), t1) implies exists|t2: Map<(), Sum<A, B>>|
265            {
266                #[trigger] CsumP::rel(CsumP::op(new_protocol_monoid, q), t2) && t1.dom().disjoint(
267                    resource_map.dom(),
268                ) && t1.union_prefer_right(resource_map) == t2
269            } by {
270            assert(CsumP::rel(CsumP::op(new_protocol_monoid, q), resource_map));
271        }
272    }
273
274    pub proof fn lemma_updates_none(self)
275        requires
276            self.is_left() || self.is_right(),
277            self.frac() == TOTAL,
278            self.is_resource_owner(),
279            self.has_no_resource(),
280        ensures
281            updates(self, CsumP::Cinl(None, self.frac(), true)),
282            updates(self, CsumP::Cinr(None, self.frac(), true)),
283    {
284    }
285}
286
287} // verus!
vstd_extra/resource/storage_protocol/csum.rs

vstd_extra/resource/storage_protocol/
csum.rs
