vstd_extra/resource/storage_protocol/
csum.rs

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

vstd_extra/resource/storage_protocol/
csum.rs
